Make the generation of the lem_ast numeric constants automatic for all numbers below 129

2 files changed, 11 insertions, 63 deletions

diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 02e18f66..379b3a15 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -69,38 +69,12 @@ let kwd ppf s = fprintf ppf "%s" s
 let base ppf s = fprintf ppf "%s" s
 let quot_string ppf s = fprintf ppf "\"%s\"" s
 
-let lemnum default n = match n with
-  | 0   -> "zero"
-  | 1   -> "one"
-  | 2   -> "two"
-  | 3   -> "three"
-  | 4   -> "four"
-  | 5   -> "five"
-  | 6   -> "six"
-  | 7   -> "seven"
-  | 8   -> "eight"
-  | 15  -> "fifteen"
-  | 16  -> "sixteen"
-  | 20  -> "twenty"
-  | 23  -> "twentythree"
-  | 24  -> "twentyfour"
-  | 30  -> "thirty"
-  | 31  -> "thirtyone"
-  | 32  -> "thirtytwo"
-  | 35  -> "thirtyfive"
-  | 39  -> "thirtynine"
-  | 40  -> "forty"
-  | 47  -> "fortyseven"
-  | 48  -> "fortyeight"
-  | 55  -> "fiftyfive"
-  | 56  -> "fiftysix"
-  | 57  -> "fiftyseven"
-  | 61  -> "sixtyone"
-  | 63  -> "sixtythree"
-  | 64  -> "sixtyfour"
-  | 127 -> "onetwentyseven"
-  | 128 -> "onetwentyeight"
-  | _   -> if n >= 0 then default n else ("(zero - " ^ (default (abs n)) ^ ")")
+let lemnum default n =
+  if 0 <= n && n <= 128 then
+    "int" ^ string_of_int n
+  else if n >= 0 then
+    default n
+  else ("(zero - " ^ (default (abs n)) ^ ")")
 
 let pp_format_id (Id_aux(i,_)) =
   match i with
diff --git a/src/process_file.ml b/src/process_file.ml
index ab18f3ad..4c70400c 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -175,6 +175,10 @@ let output_lem filename libs defs =
   close_output_with_check ext_ot;
   close_output_with_check ext_o
 
+let rec iterate (f : int -> unit) (n : int) : unit =
+  if n = 0 then ()
+  else (f n; iterate f (n - 1))
+
 let output1 libpath out_arg filename defs  =
   let f' = Filename.basename (Filename.chop_extension filename) in
     match out_arg with
@@ -185,37 +189,7 @@ let output1 libpath out_arg filename defs  =
           Format.fprintf o "open import Interp_ast@\n";
 	  Format.fprintf o "open import Pervasives@\n";
           Format.fprintf o "(*Supply common numeric constants at the right type to alleviate repeated calls to typeclass macro*)\n";
-          Format.fprintf o "let zero  : integer = integerFromNat 0\n";
-          Format.fprintf o "let one   : integer = integerFromNat 1\n";
-          Format.fprintf o "let two   : integer = integerFromNat 2\n";
-          Format.fprintf o "let three : integer = integerFromNat 3\n";
-          Format.fprintf o "let four  : integer = integerFromNat 4\n";
-          Format.fprintf o "let five  : integer = integerFromNat 5\n";
-          Format.fprintf o "let six   : integer = integerFromNat 6\n";
-          Format.fprintf o "let seven : integer = integerFromNat 7\n";
-          Format.fprintf o "let eight : integer = integerFromNat 8\n";
-          Format.fprintf o "let fifteen : integer = integerFromNat 15\n";
-          Format.fprintf o "let sixteen : integer = integerFromNat 16\n";
-          Format.fprintf o "let twenty  : integer = integerFromNat 20\n";
-          Format.fprintf o "let twentythree : integer = integerFromNat 23\n";
-          Format.fprintf o "let twentyfour  : integer = integerFromNat 24\n";
-          Format.fprintf o "let thirty : integer = integerFromNat 30\n";
-          Format.fprintf o "let thirtyone  : integer = integerFromNat 31\n";
-          Format.fprintf o "let thirtytwo  : integer = integerFromNat 32\n";
-          Format.fprintf o "let thirtyfive : integer = integerFromNat 35\n";
-          Format.fprintf o "let thirtynine : integer = integerFromNat 39\n";
-          Format.fprintf o "let forty : integer = integerFromNat 40\n";
-          Format.fprintf o "let fortyseven : integer = integerFromNat 47\n";
-          Format.fprintf o "let fortyeight : integer = integerFromNat 48\n";
-          Format.fprintf o "let fiftyfive  : integer = integerFromNat 55\n";
-          Format.fprintf o "let fiftysix   : integer = integerFromNat 56\n";
-          Format.fprintf o "let fiftyseven : integer = integerFromNat 57\n";
-          Format.fprintf o "let sixtyone   : integer = integerFromNat 61\n";
-          Format.fprintf o "let sixtythree : integer = integerFromNat 63\n";
-          Format.fprintf o "let sixtyfour  : integer = integerFromNat 64\n";
-          Format.fprintf o "let onetwentyseven : integer = integerFromNat 127\n";
-          Format.fprintf o "let onetwentyeight : integer = integerFromNat 128\n";
-                    
+          iterate (fun n -> Format.fprintf o "let int%i : integer = integerFromNat %i\n" (n - 1) (n - 1)) 129;
           Format.fprintf o "let defs = ";
 	  Pretty_print.pp_lem_defs o defs;
 	  close_output_with_check ext_o