diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 40325ba5..9586b6a6 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -163,6 +163,38 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo Format.fprintf o "(* %s *)@\n" (generated_line filename); 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 fourty : integer = integerFromNat 40\n"; + Format.fprintf o "let fourtyseven : integer = integerFromNat 47\n"; + Format.fprintf o "let fourtyeight : 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"; + Format.fprintf o "let defs = "; Pretty_print.pp_lem_defs o defs; close_output_with_check ext_o |