#include <stdio.h>
#include <errno.h>


// Writes a public constant value to the desired file.
void write_constant(FILE* file, const char* name,
                    const char* type, const int val)
{
   fprintf(file, "pub const %s: %s = %d;\n", name, type, val);
}

// Writes the header of the errno file.
void write_file_header(FILE* file)
{
   fprintf(file, "// This was generated by a build script to obtain\n");
   fprintf(file, "// the correct values of C preprocessor values to\n");
   fprintf(file, "// be used as errno constant values.\n");
}


int main(int argc, char *argv[])
{
   char* filename;
   FILE* output_file;

   // This requires a filename to be given for writing to.
   if (argc == 2)
   {
      filename = argv[1];
   }
   else if (argc > 2 || argc < 2)
   {
      printf("\nThis program requires a filename be given.\n\n");
      return 1;
   }

   // Open a file for writing.
   output_file = fopen(filename, "w");

   // Write the errno file header.
   write_file_header(output_file);

   // Write the errno constants we are trying to capture.
   write_constant(output_file, "EDOM", "CInt", EDOM);
   write_constant(output_file, "ERANGE", "CInt", ERANGE);
   write_constant(output_file, "EILSEQ", "CInt", EILSEQ);

   // Close the file.
   fclose(output_file);
   return 0;
}