diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/monomorphise.ml | 11 | ||||
| -rw-r--r-- | src/process_file.ml | 8 |
2 files changed, 17 insertions, 2 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index f458716b..2b6da219 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -3416,6 +3416,17 @@ let rec sets_from_assert e = [E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); E_aux (E_lit (L_aux (L_num i,_)),_)]) -> (check_kid kid; [i]) + (* TODO: Now that E_constraint is re-written by the typechecker, + we'll end up with the following for the above - some of this + function is probably redundant now *) + | E_app (Id_aux (Id "eq_int",_), + [E_aux (E_app (Id_aux (Id "__id", _), [E_aux (E_id id, annot)]), _); + E_aux (E_lit (L_aux (L_num i,_)),_)]) -> + begin match typ_of_annot annot with + | Typ_aux (Typ_app (Id_aux (Id "atom", _), [A_aux (A_nexp (Nexp_aux (Nexp_var kid, _)), _)]), _) -> + check_kid kid; [i] + | _ -> raise Not_found + end | _ -> raise Not_found in try let is = aux e in diff --git a/src/process_file.ml b/src/process_file.ml index e8f255ff..94a6cd3e 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -90,9 +90,13 @@ let parse_file ?loc:(l=Parse_ast.Unknown) (f : string) : Parse_ast.defs = (* Simple preprocessor features for conditional file loading *) module StringSet = Set.Make(String) -let symbols = ref StringSet.empty +let default_symbols = + List.fold_left (fun set str -> StringSet.add str set) StringSet.empty + [ "FEATURE_IMPLICITS" ] -let clear_symbols () = symbols := StringSet.empty +let symbols = ref default_symbols + +let clear_symbols () = symbols := default_symbols let cond_pragma l defs = let depth = ref 0 in |