diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lexer.mll | 1 | ||||
| -rw-r--r-- | src/parser.mly | 2 | ||||
| -rw-r--r-- | src/rewrites.ml | 3 | ||||
| -rw-r--r-- | src/type_check.ml | 2 |
4 files changed, 7 insertions, 1 deletions
diff --git a/src/lexer.mll b/src/lexer.mll index f3d93d95..616c42b4 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -128,6 +128,7 @@ let kw_table = ("forall", (fun _ -> Forall)); ("foreach", (fun _ -> Foreach)); ("function", (fun x -> Function_)); + ("mapping", (fun _ -> Mapping)); ("overload", (fun _ -> Overload)); ("throw", (fun _ -> Throw)); ("try", (fun _ -> Try)); diff --git a/src/parser.mly b/src/parser.mly index cf2d50a7..17bc56f1 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -1250,6 +1250,8 @@ scattered_clause: def: | fun_def { DEF_fundef $1 } + | map_def + { DEF_mapdef $1 } | Fixity { let (prec, n, op) = $1 in DEF_fixity (prec, n, Id_aux (Id op, loc $startpos $endpos)) } | val_spec_def diff --git a/src/rewrites.ml b/src/rewrites.ml index 2b5a1f94..8a222431 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2836,7 +2836,8 @@ let rec rewrite_defs_pat_string_append = in let builtins = [ - ("integer", ("maybe_atoi", int_typ)); + ("int", ("maybe_int_of_prefix", int_typ)); + ("nat", ("maybe_nat_of_prefix", nat_typ)); ] in let (new_pat, new_guards, new_expr) = diff --git a/src/type_check.ml b/src/type_check.ml index 523802cc..29b1775f 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -377,6 +377,7 @@ end = struct union_ids : (typquant * typ) Bindings.t; registers : typ Bindings.t; variants : (typquant * type_union list) Bindings.t; + mappings : (typquant * typ) Bindings.t; typ_vars : base_kind_aux KBindings.t; typ_synonyms : (t -> typ_arg list -> typ) Bindings.t; num_defs : nexp Bindings.t; @@ -403,6 +404,7 @@ end = struct union_ids = Bindings.empty; registers = Bindings.empty; variants = Bindings.empty; + mappings = Bindings.empty; typ_vars = KBindings.empty; typ_synonyms = Bindings.empty; num_defs = Bindings.empty; |