diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/initial_check.ml | 18 | ||||
| -rw-r--r-- | src/initial_check.mli | 4 | ||||
| -rw-r--r-- | src/process_file.ml | 10 | ||||
| -rw-r--r-- | src/process_file.mli | 6 | ||||
| -rw-r--r-- | src/sail.ml | 2 |
5 files changed, 14 insertions, 26 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 7be3a940..4d6db996 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -112,7 +112,7 @@ let typ_error l msg opt_id opt_var opt_kind = | None,Some(v),None -> ": " ^ (var_to_string v) | None,None,Some(kind) -> " " ^ (kind_to_string kind) | _ -> ""))) - + let to_ast_id (Parse_ast.Id_aux(id,l)) = Id_aux( (match id with | Parse_ast.Id(x) -> Id(x) @@ -144,16 +144,8 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) match t with | Parse_ast.ATyp_aux(t,l) -> Typ_aux( (match t with - | Parse_ast.ATyp_id(id) -> - let id = to_ast_id id in - let mk = Envmap.apply k_env (id_to_string id) in - (match mk with - | Some(k) -> (match k.k with - | K_Typ -> Typ_id id - | K_infer -> k.k <- K_Typ; Typ_id id - | _ -> typ_error l "Required an identifier with kind Type, encountered " (Some id) None (Some k)) - | None -> typ_error l "Encountered an unbound type identifier" (Some id) None None) - | Parse_ast.ATyp_var(v) -> + | Parse_ast.ATyp_id(id) -> Typ_id (to_ast_id id) + | Parse_ast.ATyp_var(v) -> let v = to_ast_var v in let mk = Envmap.apply k_env (var_to_string v) in (match mk with @@ -1005,6 +997,6 @@ let initial_kind_env = ("implicit", {k = K_Lam( [{k = K_Nat}], {k=K_Typ})} ); ] -let process_ast defs = - let (ast, _, _) = to_ast Nameset.empty initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs in +let process_ast order defs = + let (ast, _, _) = to_ast Nameset.empty initial_kind_env order defs in ast diff --git a/src/initial_check.mli b/src/initial_check.mli index 063a0131..ed4eb0bf 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -42,7 +42,5 @@ open Ast -val process_ast : Parse_ast.defs -> unit defs +val process_ast : order -> Parse_ast.defs -> unit defs - - diff --git a/src/process_file.ml b/src/process_file.ml index 315e44bb..c9a4f178 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -82,14 +82,12 @@ let parse_file (f : string) : Parse_ast.defs = | Lexer.LexError(s,p) -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) +let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs -(*Should add a flag to say whether we want to consider Oinc or Odec the default order *) -let convert_ast (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast defs +let load_file_no_check order f = convert_ast order (parse_file f) -let load_file_no_check f = convert_ast (parse_file f) - -let load_file env f = - let ast = convert_ast (parse_file f) in +let load_file order env f = + let ast = convert_ast order (parse_file f) in Type_check.check env ast let opt_new_typecheck = ref false diff --git a/src/process_file.mli b/src/process_file.mli index 6defc7ba..9907b743 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -41,15 +41,15 @@ (**************************************************************************) val parse_file : string -> Parse_ast.defs -val convert_ast : Parse_ast.defs -> unit Ast.defs +val convert_ast : Ast.order -> Parse_ast.defs -> unit Ast.defs val check_ast: unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t val monomorphise_ast : ((string * int) * string) list -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs -val load_file_no_check : string -> unit Ast.defs -val load_file : Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t +val load_file_no_check : Ast.order -> string -> unit Ast.defs +val load_file : Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t val opt_new_typecheck : bool ref val opt_just_check : bool ref diff --git a/src/sail.ml b/src/sail.ml index 3500b213..c7c14a67 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -132,7 +132,7 @@ let main() = let ast = List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes) -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in - let ast = convert_ast ast in + let ast = convert_ast Type_check.inc_ord ast in let (ast, type_envs) = check_ast ast in let (ast, type_envs) = |