diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/process_file.ml | 4 | ||||
| -rw-r--r-- | src/process_file.mli | 1 | ||||
| -rw-r--r-- | src/sail.ml | 3 | ||||
| -rw-r--r-- | src/type_check_new.ml | 72 | ||||
| -rw-r--r-- | src/type_check_new.mli | 5 |
5 files changed, 77 insertions, 8 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 12a067e1..63e42219 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -89,6 +89,7 @@ let initi_check_ast (defs : Type_internal.tannot Ast.defs) : (Type_internal.tann Initial_check_full_ast.to_checked_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs let opt_new_typecheck = ref false +let opt_just_check = ref false let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs * Type_check.envs = let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env; @@ -102,6 +103,9 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast. if !opt_new_typecheck then let _ = Type_check_new.check Type_check_new.initial_env defs in () else (); + if !opt_just_check + then exit 0 + else (); Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob,Envmap.empty)) defs let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs diff --git a/src/process_file.mli b/src/process_file.mli index bfc719cc..4c703dd2 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -49,6 +49,7 @@ val rewrite_ast_lem : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast. val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs val opt_new_typecheck : bool ref +val opt_just_check : bool ref type out_type = | Lem_ast_out diff --git a/src/sail.ml b/src/sail.ml index 343a677c..0bdcf4ab 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -89,6 +89,9 @@ let options = Arg.align ([ ( "-new_typecheck", Arg.Set opt_new_typecheck, " use new typechecker with Z3 constraint solving (experimental)"); + ( "-just_check", + Arg.Tuple [Arg.Set opt_new_typecheck; Arg.Set opt_just_check], + " terminate immediately after typechecking, implies -new_typecheck"); ( "-v", Arg.Set opt_print_version, " print version"); diff --git a/src/type_check_new.ml b/src/type_check_new.ml index 01527f73..495d52b7 100644 --- a/src/type_check_new.ml +++ b/src/type_check_new.ml @@ -45,7 +45,7 @@ open Ast open Util open Big_int -let debug = ref 1 +let debug = ref 2 let depth = ref 0 let rec indent n = match n with @@ -333,13 +333,17 @@ module KBindings = Map.Make(Kid) module KidSet = Set.Make(Kid) type mut = Immutable | Mutable - + +type lvar = Register of typ | Local of mut * typ | Unbound + module Env : sig type t val get_val_spec : id -> t -> typquant * typ val add_val_spec : id -> typquant * typ -> t -> t val get_local : id -> t -> mut * typ val add_local : id -> mut * typ -> t -> t + val get_register : id -> t -> typ + val add_register : id -> typ -> t -> t val is_mutable : id -> t -> bool val get_constraints : t -> n_constraint list val add_constraint : n_constraint -> t -> t @@ -352,6 +356,7 @@ module Env : sig val get_default_order : t -> order val set_default_order_inc : t -> t val set_default_order_dec : t -> t + val lookup_id : id -> t -> lvar val fresh_kid : t -> kid val expand_synonyms : t -> typ -> typ val empty : t @@ -359,6 +364,7 @@ end = struct type t = { top_val_specs : (typquant * typ) Bindings.t; locals : (mut * typ) Bindings.t; + registers : typ Bindings.t; typ_vars : base_kind_aux KBindings.t; typ_synonyms : (typ_arg list -> typ) Bindings.t; constraints : n_constraint list; @@ -369,6 +375,7 @@ end = struct let empty = { top_val_specs = Bindings.empty; locals = Bindings.empty; + registers = Bindings.empty; typ_vars = KBindings.empty; typ_synonyms = Bindings.empty; constraints = []; @@ -428,6 +435,30 @@ end = struct { env with locals = Bindings.add id mtyp env.locals } end + let get_register id env = + try Bindings.find id env.registers with + | Not_found -> typ_error (id_loc id) ("No register binding found for " ^ string_of_id id) + + let add_register id typ env = + if Bindings.mem id env.registers + then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound") + else + begin + typ_print ("Adding register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ); + { env with registers = Bindings.add id typ env.registers } + end + + let lookup_id id env = + try + let (mut, typ) = Bindings.find id env.locals in + Local (mut, typ) + with + | Not_found -> + begin + try Register (Bindings.find id env.registers) with + | Not_found -> Unbound + end + let get_typ_var kid env = try KBindings.find kid env.typ_vars with | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid) @@ -919,11 +950,35 @@ let rec bind_pat env (P_aux (pat_aux, (l, _)) as pat) (Typ_aux (typ_aux, _) as t and bind_lexp env (LEXP_aux (lexp_aux, (l, _))) typ = let annot_lexp lexp typ = LEXP_aux (lexp, (l, Some (env, typ))) in match lexp_aux with - | LEXP_id v -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env + | LEXP_id v -> + begin + match Env.lookup_id v env with + | Local (Immutable, _) -> typ_error l ("Cannot modify or shadow let-bound constant " ^ string_of_id v) + | Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env + | Register vtyp -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env + | Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env + end | LEXP_cast (typ_annot, v) -> begin - subtyp l env typ typ_annot; - annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env + match Env.lookup_id v env with + | Local (Immutable, _) -> typ_error l ("Cannot modify or shadow let-bound constant " ^ string_of_id v) + | Local (Mutable, vtyp) -> + begin + subtyp l env typ typ_annot; + subtyp l env typ_annot vtyp; + annot_lexp (LEXP_cast (typ_annot, v)) typ, env + end + | Register vtyp -> + begin + subtyp l env typ typ_annot; + subtyp l env typ_annot vtyp; + annot_lexp (LEXP_cast (typ_annot, v)) typ, env + end + | Unbound -> + begin + subtyp l env typ typ_annot; + annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env + end end | LEXP_tup lexps -> begin @@ -1223,9 +1278,10 @@ let rec check_def env def = | DEF_val letdef -> cd_err () | DEF_spec vs -> check_val_spec env vs | DEF_default default -> check_default env default - | DEF_reg_dec(DEC_aux(DEC_reg(typ,id), (l,annot))) -> cd_err () - | DEF_reg_dec(DEC_aux(DEC_alias(id,aspec), (l,annot))) -> cd_err () - | DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))) -> cd_err () + | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, _))) -> + DEF_reg_dec (DEC_aux (DEC_reg (typ, id), (l, None))), Env.add_register id typ env + | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err () + | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err () | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker") | DEF_comm (DC_comm str) -> DEF_comm (DC_comm str), env | DEF_comm (DC_comm_struct def) -> diff --git a/src/type_check_new.mli b/src/type_check_new.mli index 54140267..bcf95b34 100644 --- a/src/type_check_new.mli +++ b/src/type_check_new.mli @@ -45,12 +45,16 @@ open Ast type mut = Immutable | Mutable +type lvar = Register of typ | Local of mut * typ | Unbound + module Env : sig type t val get_val_spec : id -> t -> typquant * typ val add_val_spec : id -> typquant * typ -> t -> t val get_local : id -> t -> mut * typ val add_local : id -> mut * typ -> t -> t + val get_register : id -> t -> typ + val add_register : id -> typ -> t -> t val is_mutable : id -> t -> bool val get_constraints : t -> n_constraint list val add_constraint : n_constraint -> t -> t @@ -60,6 +64,7 @@ module Env : sig val add_ret_typ : typ -> t -> t val add_typ_synonym : id -> (typ_arg list -> typ) -> t -> t val get_typ_synonym : id -> t -> typ_arg list -> typ + val lookup_id : id -> t -> lvar val fresh_kid : t -> kid val expand_synonyms : t -> typ -> typ val empty : t |