From 4babac95199fa10226263ac608693e4e1dcbf708 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 15 Sep 2023 00:26:50 +0100 Subject: [PATCH] Refactor type environment First, split the typing environment into a local and global environment. Second, move the typing environment to a separate module Type_env which is re-exported by Type_check as Env. Some common definitions and the setup for type-errors are moved to Type_internal (which should not be used outside the type checker, as the name suggests) --- src/bin/repl.ml | 5 +- src/bin/sail.ml | 7 +- src/lib/ast_util.ml | 2 + src/lib/ast_util.mli | 2 + src/lib/constant_fold.ml | 2 +- src/lib/interpreter.ml | 5 +- src/lib/jib_compile.ml | 4 +- src/lib/monomorphise.ml | 5 +- src/lib/property.ml | 1 + src/lib/rewrites.ml | 44 +- src/lib/type_check.ml | 1440 +--------------------- src/lib/type_check.mli | 45 +- src/lib/type_env.ml | 1286 +++++++++++++++++++ src/lib/type_env.mli | 208 ++++ src/lib/type_error.ml | 2 + src/lib/type_error.mli | 8 +- src/lib/type_internal.ml | 304 +++++ src/sail_c_backend/c_backend.ml | 2 +- src/sail_coq_backend/pretty_print_coq.ml | 2 +- src/sail_smt_backend/jib_smt.ml | 2 +- 20 files changed, 1856 insertions(+), 1520 deletions(-) create mode 100644 src/lib/type_env.ml create mode 100644 src/lib/type_env.mli create mode 100644 src/lib/type_internal.ml diff --git a/src/bin/repl.ml b/src/bin/repl.ml index 3b1bf2db7..705be2007 100644 --- a/src/bin/repl.ml +++ b/src/bin/repl.ml @@ -450,8 +450,7 @@ let handle_input' istate input = let nc = Initial_check.constraint_of_string arg in { istate with env = Type_check.Env.add_constraint nc istate.env } | ":v" | ":verbose" -> - Type_check.opt_tc_debug := (!Type_check.opt_tc_debug + 1) mod 3; - print_endline ("Verbosity: " ^ string_of_int !Type_check.opt_tc_debug); + Type_check.set_tc_debug (int_of_string arg); istate | ":clear" -> if arg = "on" || arg = "true" then { istate with clear = true } @@ -664,7 +663,7 @@ let handle_input istate input = | Failure str -> print_endline ("Error: " ^ str); istate - | Type_check.Type_error (_, err) -> + | Type_error.Type_error (_, err) -> print_endline (Type_error.string_of_type_error err); istate | Reporting.Fatal_error err -> diff --git a/src/bin/sail.ml b/src/bin/sail.ml index d052023a9..a873ee349 100644 --- a/src/bin/sail.ml +++ b/src/bin/sail.ml @@ -204,7 +204,7 @@ let rec options = " choose SMT solver. Supported solvers are z3 (default), alt-ergo, cvc4, mathsat, vampire and yices." ); ( "-smt_linearize", - Arg.Set Type_check.opt_smt_linearize, + Arg.Set Type_env.opt_smt_linearize, "(experimental) force linearization for constraints involving exponentials" ); ("-Oconstant_fold", Arg.Set Constant_fold.optimize_constant_fold, " apply constant folding optimizations"); @@ -222,10 +222,7 @@ let rec options = ); ("-ddump_initial_ast", Arg.Set Frontend.opt_ddump_initial_ast, " (debug) dump the initial ast to stdout"); ("-ddump_tc_ast", Arg.Set Frontend.opt_ddump_tc_ast, " (debug) dump the typechecked ast to stdout"); - ( "-dtc_verbose", - Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity), - " (debug) verbose typechecker output: 0 is silent" - ); + ("-dtc_verbose", Arg.Int Type_check.set_tc_debug, " (debug) verbose typechecker output: 0 is silent"); ("-dsmt_verbose", Arg.Set Constraint.opt_smt_verbose, " (debug) print SMTLIB constraints sent to SMT solver"); ("-dmagic_hash", Arg.Set Initial_check.opt_magic_hash, " (debug) allow special character # in identifiers"); ( "-dprofile", diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index cf4033d0d..895fb1471 100644 --- a/src/lib/ast_util.ml +++ b/src/lib/ast_util.ml @@ -819,6 +819,8 @@ and map_loop_measure_annot f = function Loop (loop, exp) -> Loop (loop, map_exp_ let def_loc (DEF_aux (_, annot)) = annot.loc +let deinfix = function Id_aux (Id v, l) -> Id_aux (Operator v, l) | Id_aux (Operator v, l) -> Id_aux (Operator v, l) + let id_of_kid = function Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l) let kid_of_id = function Id_aux (Id v, l) -> Kid_aux (Var ("'" ^ v), l) | Id_aux (Operator _, _) -> assert false diff --git a/src/lib/ast_util.mli b/src/lib/ast_util.mli index ce00a1971..a35489df3 100644 --- a/src/lib/ast_util.mli +++ b/src/lib/ast_util.mli @@ -459,6 +459,8 @@ val id_of_dec_spec : 'a dec_spec -> id (** {2 Functions for manipulating identifiers} *) +val deinfix : id -> id + val id_of_kid : kid -> id val kid_of_id : id -> kid diff --git a/src/lib/constant_fold.ml b/src/lib/constant_fold.ml index f5f663c78..63af77315 100644 --- a/src/lib/constant_fold.ml +++ b/src/lib/constant_fold.ml @@ -209,7 +209,7 @@ let rw_exp fixed target ok not_ok istate = try ok (); Type_check.check_exp (env_of_annot annot) exp (typ_of_annot annot) - with Type_error (l, err) -> + with Type_error.Type_error (l, err) -> (* A type error here would be unexpected, so don't ignore it! *) Reporting.warn "" l ("Type error when folding constants in " diff --git a/src/lib/interpreter.ml b/src/lib/interpreter.ml index 29d91c551..34e2d7c1f 100644 --- a/src/lib/interpreter.ml +++ b/src/lib/interpreter.ml @@ -122,12 +122,13 @@ let value_of_exp = function E_aux (E_internal_value v, _) -> v | _ -> failwith " let fallthrough = let open Type_check in + let open Type_error in try let env = initial_env |> Env.add_scattered_variant (mk_id "exception") (mk_typquant []) in check_case env exc_typ (mk_pexp (Pat_exp (mk_pat (P_id (mk_id "exn")), mk_exp (E_throw (mk_exp (E_id (mk_id "exn"))))))) unit_typ - with Type_error (l, err) -> Reporting.unreachable l __POS__ (Type_error.string_of_type_error err) + with Type_error (l, err) -> Reporting.unreachable l __POS__ (string_of_type_error err) (**************************************************************************) (* 1. Interpreter Monad *) @@ -864,7 +865,7 @@ let rec eval_frame' = function let eval_frame frame = try eval_frame' frame - with Type_check.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) + with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) let default_effect_interp state eff = let lstate, gstate = state in diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 724bc476f..4a4ec9aa0 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -560,7 +560,7 @@ module Make (C : CONFIG) = struct (* If we can't find a function in local_env, fall back to the global env - this happens when representing assertions, exit, etc as functions in the IR. *) - try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env + try Env.get_val_spec id ctx.local_env with Type_error.Type_error _ -> Env.get_val_spec id ctx.tc_env in let arg_typs, ret_typ = match fn_typ with Typ_fn (arg_typs, ret_typ) -> (arg_typs, ret_typ) | _ -> assert false in let ctx' = { ctx with local_env = Env.add_typquant (id_loc id) quant ctx.tc_env } in @@ -1363,7 +1363,7 @@ module Make (C : CONFIG) = struct let compile_funcl ctx id pat guard exp = (* Find the function's type. *) let quant, Typ_aux (fn_typ, _) = - try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env + try Env.get_val_spec id ctx.local_env with Type_error.Type_error _ -> Env.get_val_spec id ctx.tc_env in let arg_typs, ret_typ = match fn_typ with Typ_fn (arg_typs, ret_typ) -> (arg_typs, ret_typ) | _ -> assert false in diff --git a/src/lib/monomorphise.ml b/src/lib/monomorphise.ml index e0792fd0d..382af3e4d 100644 --- a/src/lib/monomorphise.ml +++ b/src/lib/monomorphise.ml @@ -77,6 +77,7 @@ open Ast_defs open Ast_util module Big_int = Nat_big_num open Type_check +open Type_error let opt_mwords = ref false @@ -3884,7 +3885,9 @@ module BitvectorSizeCasts = struct let arg_typ' = subst_unifiers unifiers arg_typ in arg_typ' end - | _ -> typ_error l ("Malformed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ) + | _ -> + raise + (Reporting.err_typ l ("Malformed constructor " ^ string_of_id f ^ " with type " ^ string_of_typ ctor_typ)) in (* Push the cast down, including through constructors *) diff --git a/src/lib/property.ml b/src/lib/property.ml index 7a30f43e5..d751c18d6 100644 --- a/src/lib/property.ml +++ b/src/lib/property.ml @@ -86,6 +86,7 @@ let find_properties { defs; _ } = let add_property_guards props ast = let open Type_check in + let open Type_error in let rec add_property_guards' acc = function | (DEF_aux (DEF_fundef (FD_aux (FD_function (r_opt, t_opt, funcls), fd_aux) as fdef), def_annot) as def) :: defs -> begin diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml index 707ff4568..3306cf150 100644 --- a/src/lib/rewrites.ml +++ b/src/lib/rewrites.ml @@ -2131,7 +2131,7 @@ let rewrite_vector_concat_assignments env defs = in begin try check_exp env full_exp unit_typ - with Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) + with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) end ) else E_aux (e_aux, annot) @@ -2158,7 +2158,7 @@ let rewrite_tuple_assignments env defs = let let_exp = mk_exp (E_let (mk_letbind pat (strip_exp exp'), block)) in begin try check_exp env let_exp unit_typ - with Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) + with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) end | _ -> E_aux (e_aux, annot) in @@ -2930,7 +2930,7 @@ let rewrite_ast_pat_string_append env = let mapping_inner_typ = match Env.get_val_spec (mk_id mapping_prefix_func) env with | _, Typ_aux (Typ_fn (_, Typ_aux (Typ_app (_, [A_aux (A_typ typ, _)]), _)), _) -> typ - | _ -> typ_error Parse_ast.Unknown "mapping prefix func without correct function type?" + | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "mapping prefix func without correct function type?" in let s_id = fresh_stringappend_id () in @@ -4032,30 +4032,6 @@ let rewrite_ast_realize_mappings effect_info env ast = ) in - typ_debug - ( lazy - (Printf.sprintf "forwards for mapping %s: %s\n%!" (string_of_id id) - (Pretty_print_sail.doc_fundef forwards_fun |> Pretty_print_sail.to_string) - ) - ); - typ_debug - ( lazy - (Printf.sprintf "backwards for mapping %s: %s\n%!" (string_of_id id) - (Pretty_print_sail.doc_fundef backwards_fun |> Pretty_print_sail.to_string) - ) - ); - typ_debug - ( lazy - (Printf.sprintf "forwards matches for mapping %s: %s\n%!" (string_of_id id) - (Pretty_print_sail.doc_fundef forwards_matches_fun |> Pretty_print_sail.to_string) - ) - ); - typ_debug - ( lazy - (Printf.sprintf "backwards matches for mapping %s: %s\n%!" (string_of_id id) - (Pretty_print_sail.doc_fundef backwards_matches_fun |> Pretty_print_sail.to_string) - ) - ); let forwards_fun, _ = Type_check.check_fundef env def_annot forwards_fun in let backwards_fun, _ = Type_check.check_fundef env def_annot backwards_fun in let forwards_matches_fun, _ = Type_check.check_fundef env def_annot forwards_matches_fun in @@ -4084,12 +4060,6 @@ let rewrite_ast_realize_mappings effect_info env ast = FD_aux (FD_function (non_rec, no_tannot, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, empty_uannot)) in - typ_debug - ( lazy - (Printf.sprintf "forwards prefix matches for mapping %s: %s\n%!" (string_of_id id) - (Pretty_print_sail.doc_fundef forwards_prefix_fun |> Pretty_print_sail.to_string) - ) - ); let forwards_prefix_fun, _ = Type_check.check_fundef env def_annot forwards_prefix_fun in forwards_prefix_fun end @@ -4110,12 +4080,6 @@ let rewrite_ast_realize_mappings effect_info env ast = FD_aux (FD_function (non_rec, no_tannot, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, empty_uannot)) in - typ_debug - ( lazy - (Printf.sprintf "backwards prefix matches for mapping %s: %s\n%!" (string_of_id id) - (Pretty_print_sail.doc_fundef backwards_prefix_fun |> Pretty_print_sail.to_string) - ) - ); let backwards_prefix_fun, _ = Type_check.check_fundef env def_annot backwards_prefix_fun in backwards_prefix_fun end @@ -5141,7 +5105,7 @@ let rewrite effect_info env rewriters ast = (1, (ast, effect_info, env)) rewriters ) - with Type_check.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) + with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) let () = let open Interactive in diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 6f9ee93b9..c08b32736 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -73,10 +73,9 @@ open Lazy module Big_int = Nat_big_num -(* opt_tc_debug controls the verbosity of the type checker. 0 is - silent, 1 prints a tree of the type derivation and 2 is like 1 but - with much more debug information. *) -let opt_tc_debug = ref 0 +open Type_internal + +let set_tc_debug level = opt_tc_debug := level (* opt_no_lexp_bounds_check turns off the bounds checking in vector assignments in l-expressions *) @@ -86,87 +85,9 @@ let opt_no_lexp_bounds_check = ref false We prefer not to do it for latex output but it is otherwise a good idea. *) let opt_expand_valspec = ref true -(* Linearize cases involving power where we would otherwise require - the SMT solver to use non-linear arithmetic. *) -let opt_smt_linearize = ref false - (* Don't expand bitfields (when using old syntax), used for LaTeX output *) let opt_no_bitfield_expansion = ref false -let depth = ref 0 - -let rec indent n = match n with 0 -> "" | n -> "| " ^ indent (n - 1) - -(* Lazily evaluate debugging message. This can make a big performance - difference; for example, repeated calls to string_of_exp can be costly for - deeply nested expressions, e.g. with long sequences of monadic binds. *) -let typ_debug ?(level = 1) m = if !opt_tc_debug > level then prerr_endline (indent !depth ^ Lazy.force m) else () - -let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ Lazy.force m) else () - -type constraint_reason = (Ast.l * string) option - -type type_error = - (* First parameter is the error that caused us to start doing type - coercions, the second is the errors encountered by all possible - coercions *) - | Err_no_casts of uannot exp * typ * typ * type_error * type_error list - | Err_no_overloading of id * (id * type_error) list - | Err_unresolved_quants of id * quant_item list * (mut * typ) Bindings.t * n_constraint list - | Err_failed_constraint of n_constraint * (mut * typ) Bindings.t * n_constraint list - | Err_subtype of typ * typ * n_constraint option * (constraint_reason * n_constraint) list * Ast.l KBindings.t - | Err_no_num_ident of id - | Err_other of string - | Err_inner of type_error * Parse_ast.l * string * string option * type_error - -let err_because (error1, l, error2) = Err_inner (error1, l, "Caused by", None, error2) - -type env = { - top_val_specs : (typquant * typ) Bindings.t; - defined_val_specs : IdSet.t; - locals : (mut * typ) Bindings.t; - top_letbinds : IdSet.t; - union_ids : (typquant * typ) Bindings.t; - registers : typ Bindings.t; - variants : (typquant * type_union list) Bindings.t; - scattered_variant_envs : env Bindings.t; - mappings : (typquant * typ * typ) Bindings.t; - typ_vars : (Ast.l * kind_aux) KBindings.t; - shadow_vars : int KBindings.t; - typ_synonyms : (typquant * typ_arg) Bindings.t; - typ_params : typquant Bindings.t; - overloads : id list Bindings.t; - enums : (bool * IdSet.t) Bindings.t; - records : (typquant * (typ * id) list) Bindings.t; - accessors : (typquant * typ) Bindings.t; - externs : extern Bindings.t; - allow_bindings : bool; - constraints : (constraint_reason * n_constraint) list; - default_order : order option; - ret_typ : typ option; - poly_undefineds : bool; - prove : (env -> n_constraint -> bool) option; - allow_unknowns : bool; - bitfields : (typ * index_range Bindings.t) Bindings.t; - toplevel : l option; - outcomes : (typquant * typ * kinded_id list * id list * env) Bindings.t; - outcome_typschm : (typquant * typ) option; - outcome_instantiation : (Ast.l * typ) KBindings.t; -} - -exception Type_error of l * type_error - -let typ_error l m = raise (Type_error (l, Err_other m)) - -let typ_raise l err = raise (Type_error (l, err)) - -let deinfix = function Id_aux (Id v, l) -> Id_aux (Operator v, l) | Id_aux (Operator v, l) -> Id_aux (Operator v, l) - -let field_name rec_id id = - match (rec_id, id) with Id_aux (Id r, _), Id_aux (Id v, l) -> Id_aux (Id (r ^ "." ^ v), l) | _, _ -> assert false - -let string_of_bind (typquant, typ) = string_of_typquant typquant ^ ". " ^ string_of_typ typ - let orig_kid (Kid_aux (Var v, l) as kid) = try let i = String.rindex v '#' in @@ -197,81 +118,6 @@ let is_atom (Typ_aux (typ_aux, _)) = let is_atom_bool (Typ_aux (typ_aux, _)) = match typ_aux with Typ_app (f, [_]) when string_of_id f = "atom_bool" -> true | _ -> false -let rec unloc_id = function - | Id_aux (Id x, _) -> Id_aux (Id x, Parse_ast.Unknown) - | Id_aux (Operator x, _) -> Id_aux (Operator x, Parse_ast.Unknown) - -and unloc_kid = function Kid_aux (Var x, _) -> Kid_aux (Var x, Parse_ast.Unknown) - -and unloc_nexp_aux = function - | Nexp_id id -> Nexp_id (unloc_id id) - | Nexp_var kid -> Nexp_var (unloc_kid kid) - | Nexp_constant n -> Nexp_constant n - | Nexp_app (id, nexps) -> Nexp_app (id, List.map unloc_nexp nexps) - | Nexp_times (nexp1, nexp2) -> Nexp_times (unloc_nexp nexp1, unloc_nexp nexp2) - | Nexp_sum (nexp1, nexp2) -> Nexp_sum (unloc_nexp nexp1, unloc_nexp nexp2) - | Nexp_minus (nexp1, nexp2) -> Nexp_minus (unloc_nexp nexp1, unloc_nexp nexp2) - | Nexp_exp nexp -> Nexp_exp (unloc_nexp nexp) - | Nexp_neg nexp -> Nexp_neg (unloc_nexp nexp) - -and unloc_nexp = function Nexp_aux (nexp_aux, _) -> Nexp_aux (unloc_nexp_aux nexp_aux, Parse_ast.Unknown) - -and unloc_n_constraint_aux = function - | NC_equal (nexp1, nexp2) -> NC_equal (unloc_nexp nexp1, unloc_nexp nexp2) - | NC_bounded_ge (nexp1, nexp2) -> NC_bounded_ge (unloc_nexp nexp1, unloc_nexp nexp2) - | NC_bounded_gt (nexp1, nexp2) -> NC_bounded_gt (unloc_nexp nexp1, unloc_nexp nexp2) - | NC_bounded_le (nexp1, nexp2) -> NC_bounded_le (unloc_nexp nexp1, unloc_nexp nexp2) - | NC_bounded_lt (nexp1, nexp2) -> NC_bounded_lt (unloc_nexp nexp1, unloc_nexp nexp2) - | NC_not_equal (nexp1, nexp2) -> NC_not_equal (unloc_nexp nexp1, unloc_nexp nexp2) - | NC_set (kid, nums) -> NC_set (unloc_kid kid, nums) - | NC_or (nc1, nc2) -> NC_or (unloc_n_constraint nc1, unloc_n_constraint nc2) - | NC_and (nc1, nc2) -> NC_and (unloc_n_constraint nc1, unloc_n_constraint nc2) - | NC_var kid -> NC_var (unloc_kid kid) - | NC_app (id, args) -> NC_app (unloc_id id, List.map unloc_typ_arg args) - | NC_true -> NC_true - | NC_false -> NC_false - -and unloc_n_constraint = function NC_aux (nc_aux, _) -> NC_aux (unloc_n_constraint_aux nc_aux, Parse_ast.Unknown) - -and unloc_typ_arg = function A_aux (typ_arg_aux, _) -> A_aux (unloc_typ_arg_aux typ_arg_aux, Parse_ast.Unknown) - -and unloc_typ_arg_aux = function - | A_nexp nexp -> A_nexp (unloc_nexp nexp) - | A_typ typ -> A_typ (unloc_typ typ) - | A_bool nc -> A_bool (unloc_n_constraint nc) - -and unloc_typ_aux : typ_aux -> typ_aux = function - | Typ_internal_unknown -> Typ_internal_unknown - | Typ_id id -> Typ_id (unloc_id id) - | Typ_var kid -> Typ_var (unloc_kid kid) - | Typ_fn (arg_typs, ret_typ) -> Typ_fn (List.map unloc_typ arg_typs, unloc_typ ret_typ) - | Typ_bidir (typ1, typ2) -> Typ_bidir (unloc_typ typ1, unloc_typ typ2) - | Typ_tuple typs -> Typ_tuple (List.map unloc_typ typs) - | Typ_exist (kopts, constr, typ) -> - Typ_exist (List.map unloc_kinded_id kopts, unloc_n_constraint constr, unloc_typ typ) - | Typ_app (id, args) -> Typ_app (unloc_id id, List.map unloc_typ_arg args) - -and unloc_typ : typ -> typ = function Typ_aux (typ_aux, _) -> Typ_aux (unloc_typ_aux typ_aux, Parse_ast.Unknown) - -and unloc_typq = function TypQ_aux (typq_aux, _) -> TypQ_aux (unloc_typq_aux typq_aux, Parse_ast.Unknown) - -and unloc_typq_aux = function - | TypQ_no_forall -> TypQ_no_forall - | TypQ_tq quants -> TypQ_tq (List.map unloc_quant_item quants) - -and unloc_quant_item = function QI_aux (qi_aux, _) -> QI_aux (unloc_qi_aux qi_aux, Parse_ast.Unknown) - -and unloc_qi_aux = function - | QI_id kinded_id -> QI_id (unloc_kinded_id kinded_id) - | QI_constraint constr -> QI_constraint (unloc_n_constraint constr) - -and unloc_kinded_id = function - | KOpt_aux (kinded_id_aux, _) -> KOpt_aux (unloc_kinded_id_aux kinded_id_aux, Parse_ast.Unknown) - -and unloc_kinded_id_aux = function KOpt_kind (kind, kid) -> KOpt_kind (unloc_kind kind, unloc_kid kid) - -and unloc_kind = function K_aux (k_aux, _) -> K_aux (k_aux, Parse_ast.Unknown) - let rec typ_constraints (Typ_aux (typ_aux, _)) = match typ_aux with | Typ_internal_unknown -> [] @@ -286,33 +132,6 @@ let rec typ_constraints (Typ_aux (typ_aux, _)) = and typ_arg_constraints (A_aux (typ_arg_aux, _)) = match typ_arg_aux with A_nexp _ -> [] | A_typ typ -> typ_constraints typ | A_bool nc -> [nc] -let rec typ_nexps (Typ_aux (typ_aux, _)) = - match typ_aux with - | Typ_internal_unknown -> [] - | Typ_id _ -> [] - | Typ_var _ -> [] - | Typ_tuple typs -> List.concat (List.map typ_nexps typs) - | Typ_app (_, args) -> List.concat (List.map typ_arg_nexps args) - | Typ_exist (_, _, typ) -> typ_nexps typ - | Typ_fn (arg_typs, ret_typ) -> List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ - | Typ_bidir (typ1, typ2) -> typ_nexps typ1 @ typ_nexps typ2 - -and typ_arg_nexps (A_aux (typ_arg_aux, _)) = - match typ_arg_aux with A_nexp n -> [n] | A_typ typ -> typ_nexps typ | A_bool nc -> constraint_nexps nc - -and constraint_nexps (NC_aux (nc_aux, _)) = - match nc_aux with - | NC_equal (n1, n2) - | NC_bounded_ge (n1, n2) - | NC_bounded_le (n1, n2) - | NC_bounded_gt (n1, n2) - | NC_bounded_lt (n1, n2) - | NC_not_equal (n1, n2) -> - [n1; n2] - | NC_set _ | NC_true | NC_false | NC_var _ -> [] - | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> constraint_nexps nc1 @ constraint_nexps nc2 - | NC_app (_, args) -> List.concat (List.map typ_arg_nexps args) - (* Replace A_nexp nexp with A_nexp nexp' in typ, intended for use after typ_nexps. *) let rec replace_nexp_typ nexp nexp' (Typ_aux (typ_aux, l) as typ) = let rep_typ = replace_nexp_typ nexp nexp' in @@ -362,1248 +181,29 @@ and replace_nc_typ_arg nc nc' (A_aux (typ_arg_aux, l) as arg) = | A_typ typ -> A_aux (A_typ (replace_nc_typ nc nc' typ), l) | A_bool nc'' -> if NC.compare nc nc'' == 0 then A_aux (A_bool nc', l) else arg -(* Return a KidSet containing all the type variables appearing in - nexp, where nexp occurs underneath a Nexp_exp, i.e. 2^nexp *) -let rec nexp_power_variables (Nexp_aux (aux, _)) = - match aux with - | Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) -> - KidSet.union (nexp_power_variables n1) (nexp_power_variables n2) - | Nexp_neg n -> nexp_power_variables n - | Nexp_id _ | Nexp_var _ | Nexp_constant _ -> KidSet.empty - | Nexp_app (_, ns) -> List.fold_left KidSet.union KidSet.empty (List.map nexp_power_variables ns) - | Nexp_exp n -> tyvars_of_nexp n - -let constraint_power_variables nc = - List.fold_left KidSet.union KidSet.empty (List.map nexp_power_variables (constraint_nexps nc)) - let rec name_pat (P_aux (aux, _)) = match aux with | P_id id | P_as (_, id) -> Some ("_" ^ string_of_id id) | P_typ (_, pat) | P_var (pat, _) -> name_pat pat | _ -> None -let ex_counter = ref 0 - -let fresh_existential l k = - let fresh = Kid_aux (Var ("'ex" ^ string_of_int !ex_counter ^ "#"), l) in - incr ex_counter; - mk_kopt ~loc:l k fresh - -let named_existential l k = function Some n -> mk_kopt ~loc:l k (mk_kid n) | None -> fresh_existential l k - -let destruct_exist_plain ?(name = None) typ = - match typ with - | Typ_aux (Typ_exist ([kopt], nc, typ), l) -> - let kid, fresh = (kopt_kid kopt, named_existential l (unaux_kind (kopt_kind kopt)) name) in - let nc = constraint_subst kid (arg_kopt fresh) nc in - let typ = typ_subst kid (arg_kopt fresh) typ in - Some ([fresh], nc, typ) - | Typ_aux (Typ_exist (kopts, nc, typ), _) -> - let add_num i = match name with Some n -> Some (n ^ string_of_int i) | None -> None in - let fresh_kopts = - List.mapi - (fun i kopt -> (kopt_kid kopt, named_existential (kopt_loc kopt) (unaux_kind (kopt_kind kopt)) (add_num i))) - kopts - in - let nc = List.fold_left (fun nc (kid, fresh) -> constraint_subst kid (arg_kopt fresh) nc) nc fresh_kopts in - let typ = List.fold_left (fun typ (kid, fresh) -> typ_subst kid (arg_kopt fresh) typ) typ fresh_kopts in - Some (List.map snd fresh_kopts, nc, typ) - | _ -> None - -(** Destructure and canonicalise a numeric type into a list of type - variables, a constraint on those type variables, and an - N-expression that represents that numeric type in the - environment. For example: - - {'n, 'n <= 10. atom('n)} => ['n], 'n <= 10, 'n - - int => ['n], true, 'n (where x is fresh) - - atom('n) => [], true, 'n -**) -let destruct_numeric ?(name = None) typ = - match (destruct_exist_plain ~name typ, typ) with - | Some (kids, nc, Typ_aux (Typ_app (id, [A_aux (A_nexp nexp, _)]), _)), _ when string_of_id id = "atom" -> - Some (List.map kopt_kid kids, nc, nexp) - | None, Typ_aux (Typ_app (id, [A_aux (A_nexp nexp, _)]), _) when string_of_id id = "atom" -> Some ([], nc_true, nexp) - | None, Typ_aux (Typ_app (id, [A_aux (A_nexp lo, _); A_aux (A_nexp hi, _)]), l) when string_of_id id = "range" -> - let kid = kopt_kid (named_existential l K_int name) in - Some ([kid], nc_and (nc_lteq lo (nvar kid)) (nc_lteq (nvar kid) hi), nvar kid) - | None, Typ_aux (Typ_id id, l) when string_of_id id = "nat" -> - let kid = kopt_kid (named_existential l K_int name) in - Some ([kid], nc_lteq (nint 0) (nvar kid), nvar kid) - | None, Typ_aux (Typ_id id, l) when string_of_id id = "int" -> - let kid = kopt_kid (named_existential l K_int name) in - Some ([kid], nc_true, nvar kid) - | _, _ -> None - -let destruct_boolean ?name:(_ = None) = function - | Typ_aux (Typ_id (Id_aux (Id "bool", _)), l) -> - let kid = kopt_kid (fresh_existential l K_bool) in - Some (kid, nc_var kid) - | _ -> None - -let destruct_exist ?(name = None) typ = - match destruct_numeric ~name typ with - | Some (kids, nc, nexp) -> Some (List.map (mk_kopt K_int) kids, nc, atom_typ nexp) - | None -> ( - match destruct_boolean ~name typ with - | Some (kid, nc) -> Some ([mk_kopt K_bool kid], nc_true, atom_bool_typ nc) - | None -> destruct_exist_plain ~name typ - ) - -let adding = Util.("Adding " |> darkgray |> clear) - -let counter = ref 0 - -let fresh_kid ?(kid = mk_kid "") _env = - let suffix = if Kid.compare kid (mk_kid "") = 0 then "#" else "#" ^ string_of_id (id_of_kid kid) in - let fresh = Kid_aux (Var ("'fv" ^ string_of_int !counter ^ suffix), Parse_ast.Unknown) in - incr counter; - fresh - -let freshen_kid env kid (typq, typ) = - if KidSet.mem kid (KidSet.of_list (List.map kopt_kid (quant_kopts typq))) then ( - let fresh = fresh_kid ~kid env in - (typquant_subst_kid kid fresh typq, subst_kid typ_subst kid fresh typ) - ) - else (typq, typ) - -let freshen_bind env bind = - List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) - (**************************************************************************) -(* 1. Environment *) +(* 1. The Typing Environment *) (**************************************************************************) +type env = Type_env.env + module Env : sig - type t = env - val add_val_spec : ?ignore_duplicate:bool -> id -> typquant * typ -> t -> t - val add_outcome : id -> typquant * typ * kinded_id list * id list * t -> t -> t - val update_val_spec : id -> typquant * typ -> t -> t - val define_val_spec : id -> t -> t - val get_defined_val_specs : t -> IdSet.t - val get_val_spec : id -> t -> typquant * typ - val get_val_specs : t -> (typquant * typ) Bindings.t - val get_val_spec_orig : id -> t -> typquant * typ - val get_outcome : l -> id -> t -> typquant * typ * kinded_id list * id list * t - val get_outcome_instantiation : t -> (Ast.l * typ) KBindings.t - val add_outcome_variable : Ast.l -> kid -> typ -> t -> t - val union_constructor_info : id -> t -> (int * int * id * type_union) option - val is_union_constructor : id -> t -> bool - val is_singleton_union_constructor : id -> t -> bool - val is_mapping : id -> t -> bool - val add_record : id -> typquant -> (typ * id) list -> t -> t - val is_record : id -> t -> bool - val get_record : id -> t -> typquant * (typ * id) list - val get_records : t -> (typquant * (typ * id) list) Bindings.t - val get_accessor_fn : id -> id -> t -> typquant * typ - val get_accessor : id -> id -> t -> typquant * typ * typ - val add_local : id -> mut * typ -> t -> t - val get_locals : t -> (mut * typ) Bindings.t - val add_toplevel_lets : IdSet.t -> t -> t - val get_toplevel_lets : t -> IdSet.t - val is_variant : id -> t -> bool - val add_variant : id -> typquant * type_union list -> t -> t - val add_scattered_variant : id -> typquant -> t -> t - val add_variant_clause : id -> type_union -> t -> t - val get_variant : id -> t -> typquant * type_union list - val get_variants : t -> (typquant * type_union list) Bindings.t - val get_scattered_variant_env : id -> t -> t - val add_union_id : id -> typquant * typ -> t -> t - val get_union_id : id -> t -> typquant * typ - val is_register : id -> t -> bool - val get_register : id -> t -> typ - val get_registers : t -> typ Bindings.t - val add_register : id -> typ -> t -> t - val is_mutable : id -> t -> bool - val get_constraints : t -> n_constraint list - val get_constraint_reasons : t -> (constraint_reason * n_constraint) list - val add_constraint : ?reason:Ast.l * string -> n_constraint -> t -> t - val add_typquant : l -> typquant -> t -> t - val get_typ_var : kid -> t -> kind_aux - val get_typ_var_loc_opt : kid -> t -> Ast.l option - val get_typ_vars : t -> kind_aux KBindings.t - val get_typ_var_locs : t -> Ast.l KBindings.t - val shadows : kid -> t -> int - val add_typ_var_shadow : l -> kinded_id -> t -> t * kid option - val add_typ_var : l -> kinded_id -> t -> t - val get_ret_typ : t -> typ option - val add_ret_typ : typ -> t -> t - val add_typ_synonym : id -> typquant -> typ_arg -> t -> t - val get_typ_synonyms : t -> (typquant * typ_arg) Bindings.t - val bound_typ_id : t -> id -> bool - val add_overloads : l -> id -> id list -> t -> t - val get_overloads : id -> t -> id list - val is_extern : id -> t -> string -> bool - val add_extern : id -> extern -> t -> t - val get_extern : id -> t -> string -> string - val get_default_order : t -> order - val get_default_order_opt : t -> order option - val set_default_order : order -> t -> t - val add_enum : id -> id list -> t -> t - val add_scattered_enum : id -> t -> t - val add_enum_clause : id -> id -> t -> t - val get_enum : id -> t -> id list - val get_enums : t -> IdSet.t Bindings.t - val allow_polymorphic_undefineds : t -> t - val polymorphic_undefineds : t -> bool - val lookup_id : id -> t -> typ lvar - val expand_synonyms : t -> typ -> typ - val expand_nexp_synonyms : t -> nexp -> nexp - val expand_constraint_synonyms : t -> n_constraint -> n_constraint - val base_typ_of : t -> typ -> typ - val allow_unknowns : t -> bool - val set_allow_unknowns : bool -> t -> t - val is_bitfield : id -> t -> bool - val add_bitfield : id -> typ -> index_range Bindings.t -> t -> t - val get_bitfield : id -> t -> typ * index_range Bindings.t - - val no_bindings : t -> t - - (* Well formedness-checks *) - val wf_typ : t -> typ -> unit - val wf_constraint : ?exs:KidSet.t -> t -> n_constraint -> unit - - (* Some of the code in the environment needs to use the smt solver, - which is defined below. To break the circularity this would cause - (as the prove code depends on the environment), we add a - reference to the prover to the initial environment. *) - val set_prover : (t -> n_constraint -> bool) option -> t -> t - - (* This must not be exported, initial_env sets up a correct initial - environment. *) - val empty : t - - val builtin_typs : typquant Bindings.t + include module type of Type_env end = struct - type t = env - - let empty = - { - top_val_specs = Bindings.empty; - defined_val_specs = IdSet.empty; - locals = Bindings.empty; - top_letbinds = IdSet.empty; - union_ids = Bindings.empty; - registers = Bindings.empty; - variants = Bindings.empty; - scattered_variant_envs = Bindings.empty; - mappings = Bindings.empty; - typ_vars = KBindings.empty; - shadow_vars = KBindings.empty; - typ_synonyms = Bindings.empty; - typ_params = Bindings.empty; - overloads = Bindings.empty; - enums = Bindings.empty; - records = Bindings.empty; - accessors = Bindings.empty; - externs = Bindings.empty; - allow_bindings = true; - constraints = []; - default_order = None; - ret_typ = None; - poly_undefineds = false; - prove = None; - allow_unknowns = false; - bitfields = Bindings.empty; - toplevel = None; - outcomes = Bindings.empty; - outcome_typschm = None; - outcome_instantiation = KBindings.empty; - } - - let set_prover f env = { env with prove = f } - - let allow_unknowns env = env.allow_unknowns - let set_allow_unknowns b env = { env with allow_unknowns = b } - - (* First, we define how type variables are added to the - environment. If we add a new variable shadowing a previous - variable, we need to modify the environment so the shadowed - variable is renamed. We can't just remove it because it may be - referenced by constraints. *) - let shadows v env = match KBindings.find_opt v env.shadow_vars with Some n -> n | None -> 0 - - let add_typ_var_shadow l (KOpt_aux (KOpt_kind (K_aux (k, _), v), _)) env = - if KBindings.mem v env.typ_vars then begin - let n = match KBindings.find_opt v env.shadow_vars with Some n -> n | None -> 0 in - let s_l, s_k = KBindings.find v env.typ_vars in - let s_v = Kid_aux (Var (string_of_kid v ^ "#" ^ string_of_int n), l) in - typ_print - ( lazy - (Printf.sprintf "%stype variable (shadowing %s) %s : %s" adding (string_of_kid s_v) (string_of_kid v) - (string_of_kind_aux k) - ) - ); - ( { - env with - constraints = - List.map (fun (l, nc) -> (l, constraint_subst v (arg_kopt (mk_kopt s_k s_v)) nc)) env.constraints; - typ_vars = KBindings.add v (l, k) (KBindings.add s_v (s_l, s_k) env.typ_vars); - locals = Bindings.map (fun (mut, typ) -> (mut, typ_subst v (arg_kopt (mk_kopt s_k s_v)) typ)) env.locals; - shadow_vars = KBindings.add v (n + 1) env.shadow_vars; - }, - Some s_v - ) - end - else begin - typ_print (lazy (adding ^ "type variable " ^ string_of_kid v ^ " : " ^ string_of_kind_aux k)); - ({ env with typ_vars = KBindings.add v (l, k) env.typ_vars }, None) - end - - let add_typ_var l kopt env = fst (add_typ_var_shadow l kopt env) - - let get_typ_var_loc_opt kid env = - match KBindings.find_opt kid env.typ_vars with Some (l, _) -> Some l | None -> None - - let get_typ_var kid env = - try snd (KBindings.find kid env.typ_vars) - with Not_found -> typ_error (kid_loc kid) ("No type variable " ^ string_of_kid kid) - - let get_typ_vars env = KBindings.map snd env.typ_vars - let get_typ_var_locs env = KBindings.map fst env.typ_vars - - let k_counter = ref 0 - let k_name () = - let kid = mk_kid ("k#" ^ string_of_int !k_counter) in - incr k_counter; - kid - - let kinds_typq kinds = mk_typquant (List.map (fun k -> mk_qi_id k (k_name ())) kinds) - - let builtin_typs = - List.fold_left - (fun m (name, kinds) -> Bindings.add (mk_id name) (kinds_typq kinds) m) - Bindings.empty - [ - ("range", [K_int; K_int]); - ("atom", [K_int]); - ("implicit", [K_int]); - ("vector", [K_int; K_type]); - ("bitvector", [K_int]); - ("register", [K_type]); - ("bit", []); - ("unit", []); - ("int", []); - ("nat", []); - ("bool", []); - ("real", []); - ("list", [K_type]); - ("string", []); - ("itself", [K_int]); - ("atom_bool", [K_bool]); - ("float16", []); - ("float32", []); - ("float64", []); - ("float128", []); - ("float_rounding_mode", []); - ] - - let bound_typ_id env id = - Bindings.mem id env.typ_synonyms || Bindings.mem id env.variants || Bindings.mem id env.records - || Bindings.mem id env.enums || Bindings.mem id builtin_typs - - let get_binding_loc env id = - let find map = - Bindings.bindings map |> List.find (fun (id', _) -> Id.compare id id' = 0) |> fun (id', _) -> Some (id_loc id') - in - if Bindings.mem id builtin_typs then None - else if Bindings.mem id env.variants then find env.variants - else if Bindings.mem id env.records then find env.records - else if Bindings.mem id env.enums then find env.enums - else if Bindings.mem id env.typ_synonyms then find env.typ_synonyms - else None - - let already_bound str id env = - match get_binding_loc env id with - | Some l -> - typ_raise (id_loc id) - (Err_inner - ( Err_other ("Cannot create " ^ str ^ " type " ^ string_of_id id ^ ", name is already bound"), - l, - "", - Some "previous binding", - Err_other "" - ) - ) - | None -> - let suffix = if Bindings.mem id builtin_typs then " as a built-in type" else "" in - typ_error (id_loc id) ("Cannot create " ^ str ^ " type " ^ string_of_id id ^ ", name is already bound" ^ suffix) - - let bound_ctor_fn env id = Bindings.mem id env.top_val_specs || Bindings.mem id env.union_ids - - let get_ctor_fn_binding_loc env id = - let find map = - Bindings.bindings map |> List.find (fun (id', _) -> Id.compare id id' = 0) |> fun (id', _) -> Some (id_loc id') - in - if Bindings.mem id env.top_val_specs then find env.top_val_specs - else if Bindings.mem id env.union_ids then find env.union_ids - else None - - let already_bound_ctor_fn str id env = - match get_ctor_fn_binding_loc env id with - | Some l -> - typ_raise (id_loc id) - (Err_inner - ( Err_other - ("Cannot create " ^ str ^ " " ^ string_of_id id - ^ ", name is already bound to a union constructor or function" - ), - l, - "", - Some "previous binding", - Err_other "" - ) - ) - | None -> - Reporting.unreachable (id_loc id) __POS__ - ("Could not find original binding for duplicate " ^ str ^ " called " ^ string_of_id id) - - let get_overloads id env = try Bindings.find id env.overloads with Not_found -> [] - - let add_overloads l id ids env = - typ_print (lazy (adding ^ "overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]")); - List.iter - (fun overload -> - if not (bound_ctor_fn env overload || Bindings.mem overload env.overloads) then - typ_error - (Hint ("unbound identifier", id_loc overload, l)) - ("Cannot create or extend overload " ^ string_of_id id ^ ", " ^ string_of_id overload ^ " is not bound") - ) - ids; - let existing = try Bindings.find id env.overloads with Not_found -> [] in - { env with overloads = Bindings.add id (existing @ ids) env.overloads } - - let infer_kind env id = - if Bindings.mem id builtin_typs then Bindings.find id builtin_typs - else if Bindings.mem id env.variants then fst (Bindings.find id env.variants) - else if Bindings.mem id env.records then fst (Bindings.find id env.records) - else if Bindings.mem id env.enums then mk_typquant [] - else if Bindings.mem id env.typ_synonyms then - typ_error (id_loc id) ("Cannot infer kind of type synonym " ^ string_of_id id) - else typ_error (id_loc id) ("Cannot infer kind of " ^ string_of_id id) - - let check_args_typquant id env args typq = - let kopts, ncs = quant_split typq in - let rec subst_args kopts args = - match (kopts, args) with - | kopt :: kopts, (A_aux (A_nexp _, _) as arg) :: args when is_int_kopt kopt -> - List.map (constraint_subst (kopt_kid kopt) arg) (subst_args kopts args) - | kopt :: kopts, A_aux (A_typ _, _) :: args when is_typ_kopt kopt -> subst_args kopts args - | kopt :: kopts, A_aux (A_bool _, _) :: args when is_bool_kopt kopt -> subst_args kopts args - | [], [] -> ncs - | _, A_aux (_, l) :: _ -> typ_error l ("Error when processing type quantifer arguments " ^ string_of_typquant typq) - | _, _ -> typ_error Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq) - in - let ncs = subst_args kopts args in - if match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false then () - else - typ_error (id_loc id) - ("Could not prove " - ^ string_of_list ", " string_of_n_constraint ncs - ^ " for type constructor " ^ string_of_id id - ) - - let mk_synonym typq typ_arg = - let kopts, ncs = quant_split typq in - let kopts = List.map (fun kopt -> (kopt, fresh_existential (kopt_loc kopt) (unaux_kind (kopt_kind kopt)))) kopts in - let ncs = - List.map - (fun nc -> - List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts - ) - ncs - in - let typ_arg = - List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts - in - let kopts = List.map snd kopts in - let rec subst_args env l kopts args = - match (kopts, args) with - | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_int_kopt kopt -> - let typ_arg, ncs = subst_args env l kopts args in - ( typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg, - List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs - ) - | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt -> - let typ_arg, ncs = subst_args env l kopts args in - (typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg, ncs) - | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt -> - let typ_arg, ncs = subst_args env l kopts args in - (typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs) - | [], [] -> (typ_arg, ncs) - | _, _ -> typ_error l "Synonym applied to bad arguments" - in - fun l env args -> - let typ_arg, ncs = subst_args env l kopts args in - if match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false then typ_arg - else - typ_error l - ("Could not prove constraints " - ^ string_of_list ", " string_of_n_constraint ncs - ^ " in type synonym " ^ string_of_typ_arg typ_arg ^ " with " - ^ Util.string_of_list ", " string_of_n_constraint (List.map snd env.constraints) - ) - - let get_typ_synonym id env = - match Bindings.find_opt id env.typ_synonyms with Some (typq, arg) -> mk_synonym typq arg | None -> raise Not_found - - let get_typ_synonyms env = env.typ_synonyms - - let get_constraints env = List.map snd env.constraints - - let get_constraint_reasons env = env.constraints - - let wf_debug str f x exs = - typ_debug ~level:2 - (lazy ("wf_" ^ str ^ ": " ^ f x ^ " exs: " ^ Util.string_of_list ", " string_of_kid (KidSet.elements exs))) - - (* Check if a type, order, n-expression or constraint is - well-formed. Throws a type error if the type is badly formed. *) - let rec wf_typ' ?(exs = KidSet.empty) env (Typ_aux (typ_aux, l) as typ) = - match typ_aux with - | Typ_id id when bound_typ_id env id -> - let typq = infer_kind env id in - if quant_kopts typq != [] then - typ_error l ("Type constructor " ^ string_of_id id ^ " expected " ^ string_of_typquant typq) - else () - | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id) - | Typ_var kid -> begin - match KBindings.find kid env.typ_vars with - | _, K_type -> () - | _, k -> - typ_error l - ("Type variable " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ ^ " is " ^ string_of_kind_aux k - ^ " rather than Type" - ) - | exception Not_found -> - typ_error l ("Unbound type variable " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ) - end - | Typ_fn (arg_typs, ret_typ) -> - List.iter (wf_typ' ~exs env) arg_typs; - wf_typ' ~exs env ret_typ - | Typ_bidir (typ1, typ2) when unloc_typ typ1 = unloc_typ typ2 -> - typ_error l "Bidirectional types cannot be the same on both sides" - | Typ_bidir (typ1, typ2) -> - wf_typ' ~exs env typ1; - wf_typ' ~exs env typ2 - | Typ_tuple typs -> List.iter (wf_typ' ~exs env) typs - | Typ_app (id, [(A_aux (A_nexp _, _) as arg)]) when string_of_id id = "implicit" -> wf_typ_arg ~exs env arg - | Typ_app (id, args) when bound_typ_id env id -> - List.iter (wf_typ_arg ~exs env) args; - check_args_typquant id env args (infer_kind env id) - | Typ_app (id, _) -> typ_error l ("Undefined type " ^ string_of_id id) - | Typ_exist ([], _, _) -> typ_error l "Existential must have some type variables" - | Typ_exist (kopts, nc, typ) when KidSet.is_empty exs -> - wf_constraint ~exs:(KidSet.of_list (List.map kopt_kid kopts)) env nc; - wf_typ' ~exs:(KidSet.of_list (List.map kopt_kid kopts)) env typ - | Typ_exist (_, _, _) -> typ_error l "Nested existentials are not allowed" - | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" - - and wf_typ_arg ?(exs = KidSet.empty) env (A_aux (typ_arg_aux, _)) = - match typ_arg_aux with - | A_nexp nexp -> wf_nexp ~exs env nexp - | A_typ typ -> wf_typ' ~exs env typ - | A_bool nc -> wf_constraint ~exs env nc - - and wf_nexp ?(exs = KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) = - wf_debug "nexp" string_of_nexp nexp exs; - match nexp_aux with - | Nexp_id id -> typ_error l ("Undefined type synonym " ^ string_of_id id) - | Nexp_var kid when KidSet.mem kid exs -> () - | Nexp_var kid -> begin - match get_typ_var kid env with - | K_int -> () - | kind -> - typ_error l - ("Constraint is badly formed, " ^ string_of_kid kid ^ " has kind " ^ string_of_kind_aux kind - ^ " but should have kind Int" - ) - end - | Nexp_constant _ -> () - | Nexp_app (_, nexps) -> List.iter (fun n -> wf_nexp ~exs env n) nexps - | Nexp_times (nexp1, nexp2) -> - wf_nexp ~exs env nexp1; - wf_nexp ~exs env nexp2 - | Nexp_sum (nexp1, nexp2) -> - wf_nexp ~exs env nexp1; - wf_nexp ~exs env nexp2 - | Nexp_minus (nexp1, nexp2) -> - wf_nexp ~exs env nexp1; - wf_nexp ~exs env nexp2 - | Nexp_exp nexp -> wf_nexp ~exs env nexp (* MAYBE: Could put restrictions on what is allowed here *) - | Nexp_neg nexp -> wf_nexp ~exs env nexp - - and wf_constraint ?(exs = KidSet.empty) env (NC_aux (nc_aux, l) as nc) = - wf_debug "constraint" string_of_n_constraint nc exs; - match nc_aux with - | NC_equal (n1, n2) -> - wf_nexp ~exs env n1; - wf_nexp ~exs env n2 - | NC_not_equal (n1, n2) -> - wf_nexp ~exs env n1; - wf_nexp ~exs env n2 - | NC_bounded_ge (n1, n2) -> - wf_nexp ~exs env n1; - wf_nexp ~exs env n2 - | NC_bounded_gt (n1, n2) -> - wf_nexp ~exs env n1; - wf_nexp ~exs env n2 - | NC_bounded_le (n1, n2) -> - wf_nexp ~exs env n1; - wf_nexp ~exs env n2 - | NC_bounded_lt (n1, n2) -> - wf_nexp ~exs env n1; - wf_nexp ~exs env n2 - | NC_set (kid, _) when KidSet.mem kid exs -> () - | NC_set (kid, _) -> begin - match get_typ_var kid env with - | K_int -> () - | kind -> - typ_error l - ("Set constraint is badly formed, " ^ string_of_kid kid ^ " has kind " ^ string_of_kind_aux kind - ^ " but should have kind Int" - ) - end - | NC_or (nc1, nc2) -> - wf_constraint ~exs env nc1; - wf_constraint ~exs env nc2 - | NC_and (nc1, nc2) -> - wf_constraint ~exs env nc1; - wf_constraint ~exs env nc2 - | NC_app (_, args) -> List.iter (wf_typ_arg ~exs env) args - | NC_var kid when KidSet.mem kid exs -> () - | NC_var kid -> begin - match get_typ_var kid env with - | K_bool -> () - | kind -> typ_error l (string_of_kid kid ^ " has kind " ^ string_of_kind_aux kind ^ " but should have kind Bool") - end - | NC_true | NC_false -> () - - let rec expand_constraint_synonyms env (NC_aux (aux, l) as nc) = - match aux with - | NC_or (nc1, nc2) -> NC_aux (NC_or (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l) - | NC_and (nc1, nc2) -> NC_aux (NC_and (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l) - | NC_equal (n1, n2) -> NC_aux (NC_equal (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) - | NC_not_equal (n1, n2) -> NC_aux (NC_not_equal (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) - | NC_bounded_le (n1, n2) -> NC_aux (NC_bounded_le (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) - | NC_bounded_lt (n1, n2) -> NC_aux (NC_bounded_lt (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) - | NC_bounded_ge (n1, n2) -> NC_aux (NC_bounded_ge (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) - | NC_bounded_gt (n1, n2) -> NC_aux (NC_bounded_gt (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) - | NC_app (id, args) -> ( - try - begin - match get_typ_synonym id env l env args with - | A_aux (A_bool nc, _) -> expand_constraint_synonyms env nc - | arg -> - typ_error l ("Expected Bool when expanding synonym " ^ string_of_id id ^ " got " ^ string_of_typ_arg arg) - end - with Not_found -> NC_aux (NC_app (id, List.map (expand_arg_synonyms env) args), l) - ) - | NC_true | NC_false | NC_var _ | NC_set _ -> nc - - and expand_nexp_synonyms env (Nexp_aux (aux, l) as nexp) = - match aux with - | Nexp_app (id, args) -> ( - try - begin - match get_typ_synonym id env l env [] with - | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp - | _ -> typ_error l ("Expected Int when expanding synonym " ^ string_of_id id) - end - with Not_found -> Nexp_aux (Nexp_app (id, List.map (expand_nexp_synonyms env) args), l) - ) - | Nexp_id id -> ( - try - begin - match get_typ_synonym id env l env [] with - | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp - | _ -> typ_error l ("Expected Int when expanding synonym " ^ string_of_id id) - end - with Not_found -> nexp - ) - | Nexp_times (nexp1, nexp2) -> - Nexp_aux (Nexp_times (expand_nexp_synonyms env nexp1, expand_nexp_synonyms env nexp2), l) - | Nexp_sum (nexp1, nexp2) -> Nexp_aux (Nexp_sum (expand_nexp_synonyms env nexp1, expand_nexp_synonyms env nexp2), l) - | Nexp_minus (nexp1, nexp2) -> - Nexp_aux (Nexp_minus (expand_nexp_synonyms env nexp1, expand_nexp_synonyms env nexp2), l) - | Nexp_exp nexp -> Nexp_aux (Nexp_exp (expand_nexp_synonyms env nexp), l) - | Nexp_neg nexp -> Nexp_aux (Nexp_neg (expand_nexp_synonyms env nexp), l) - | Nexp_var kid -> Nexp_aux (Nexp_var kid, l) - | Nexp_constant n -> Nexp_aux (Nexp_constant n, l) - - and expand_synonyms env (Typ_aux (typ, l)) = - match typ with - | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l) - | Typ_tuple typs -> Typ_aux (Typ_tuple (List.map (expand_synonyms env) typs), l) - | Typ_fn (arg_typs, ret_typ) -> - Typ_aux (Typ_fn (List.map (expand_synonyms env) arg_typs, expand_synonyms env ret_typ), l) - | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2), l) - | Typ_app (id, args) -> ( - try - begin - match get_typ_synonym id env l env args with - | A_aux (A_typ typ, _) -> expand_synonyms env typ - | _ -> typ_error l ("Expected Type when expanding synonym " ^ string_of_id id) - end - with Not_found -> Typ_aux (Typ_app (id, List.map (expand_arg_synonyms env) args), l) - ) - | Typ_id id -> ( - try - begin - match get_typ_synonym id env l env [] with - | A_aux (A_typ typ, _) -> expand_synonyms env typ - | _ -> typ_error l ("Expected Type when expanding synonym " ^ string_of_id id) - end - with Not_found -> Typ_aux (Typ_id id, l) - ) - | Typ_exist (kopts, nc, typ) -> - let nc = expand_constraint_synonyms env nc in - - (* When expanding an existential synonym we need to take care - to add the type variables and constraints to the - environment, so we can check constraints attached to type - synonyms within the existential. Furthermore, we must take - care to avoid clobbering any existing type variables in - scope while doing this. *) - let rebindings = ref [] in - - let rename_kopt (KOpt_aux (KOpt_kind (k, kid), l) as kopt) = - if KBindings.mem kid env.typ_vars then KOpt_aux (KOpt_kind (k, prepend_kid "syn#" kid), l) else kopt - in - let add_typ_var env (KOpt_aux (KOpt_kind (k, kid), l)) = - try - let l, _ = KBindings.find kid env.typ_vars in - rebindings := kid :: !rebindings; - { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) (l, unaux_kind k) env.typ_vars } - with Not_found -> { env with typ_vars = KBindings.add kid (l, unaux_kind k) env.typ_vars } - in - - let env = List.fold_left add_typ_var env kopts in - let kopts = List.map rename_kopt kopts in - let nc = - List.fold_left - (fun nc kid -> constraint_subst kid (arg_nexp (nvar (prepend_kid "syn#" kid))) nc) - nc !rebindings - in - let typ = - List.fold_left (fun typ kid -> typ_subst kid (arg_nexp (nvar (prepend_kid "syn#" kid))) typ) typ !rebindings - in - let env = add_constraint nc env in - Typ_aux (Typ_exist (kopts, nc, expand_synonyms env typ), l) - | Typ_var v -> Typ_aux (Typ_var v, l) - - and expand_arg_synonyms env (A_aux (typ_arg, l)) = - match typ_arg with - | A_typ typ -> A_aux (A_typ (expand_synonyms env typ), l) - | A_bool nc -> A_aux (A_bool (expand_constraint_synonyms env nc), l) - | A_nexp nexp -> A_aux (A_nexp (expand_nexp_synonyms env nexp), l) - - and add_constraint ?reason constr env = - let (NC_aux (nc_aux, l) as constr) = constraint_simp (expand_constraint_synonyms env constr) in - wf_constraint env constr; - let power_vars = constraint_power_variables constr in - if KidSet.cardinal power_vars > 1 && !opt_smt_linearize then - typ_error l - ("Cannot add constraint " ^ string_of_n_constraint constr - ^ " where more than two variables appear within an exponential" - ) - else if KidSet.cardinal power_vars = 1 && !opt_smt_linearize then ( - let v = KidSet.choose power_vars in - let constrs = List.fold_left nc_and nc_true (get_constraints env) in - begin - match Constraint.solve_all_smt l constrs v with - | Some solutions -> - typ_print - ( lazy - (Util.("Linearizing " |> red |> clear) - ^ string_of_n_constraint constr ^ " for " ^ string_of_kid v ^ " in " - ^ Util.string_of_list ", " Big_int.to_string solutions - ) - ); - let linearized = - List.fold_left - (fun c s -> - nc_or c (nc_and (nc_eq (nvar v) (nconstant s)) (constraint_subst v (arg_nexp (nconstant s)) constr)) - ) - nc_false solutions - in - typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint linearized)); - { env with constraints = (reason, linearized) :: env.constraints } - | None -> - typ_error l - ("Type variable " ^ string_of_kid v ^ " must have a finite number of solutions to add " - ^ string_of_n_constraint constr - ) - end - ) - else ( - match nc_aux with - | NC_true -> env - | _ -> - typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint constr)); - { env with constraints = (reason, constr) :: env.constraints } - ) - - let add_typquant l quant env = - let rec add_quant_item env = function QI_aux (qi, _) -> add_quant_item_aux env qi - and add_quant_item_aux env = function - | QI_constraint constr -> add_constraint constr env - | QI_id kopt -> add_typ_var l kopt env - in - match quant with - | TypQ_aux (TypQ_no_forall, _) -> env - | TypQ_aux (TypQ_tq quants, _) -> List.fold_left add_quant_item env quants - - let wf_typ env (Typ_aux (_, l) as typ) = - let typ = expand_synonyms env typ in - wf_debug "typ" string_of_typ typ KidSet.empty; - incr depth; - try - wf_typ' env typ; - decr depth - with Type_error (err_l, err) -> - decr depth; - typ_raise l (err_because (Err_other "Well-formedness check failed for type", err_l, err)) - - let add_typ_synonym id typq arg env = - if bound_typ_id env id then - typ_error (id_loc id) - ("Cannot define type synonym " ^ string_of_id id ^ ", as a type or synonym with that name already exists") - else ( - let typq = - quant_map_items - (function - | QI_aux (QI_constraint nexp, aux) -> QI_aux (QI_constraint (expand_constraint_synonyms env nexp), aux) - | quant_item -> quant_item - ) - typq - in - typ_print - ( lazy - (adding ^ "type synonym " ^ string_of_id id ^ ", " ^ string_of_typquant typq ^ " = " ^ string_of_typ_arg arg) - ); - { - env with - typ_synonyms = - Bindings.add id (typq, expand_arg_synonyms (add_typquant (id_loc id) typq env) arg) env.typ_synonyms; - } - ) - - let get_val_spec_orig id env = - try Bindings.find id env.top_val_specs - with Not_found -> typ_error (id_loc id) ("No type signature found for " ^ string_of_id id) - - let get_val_spec id env = - try - let bind = Bindings.find id env.top_val_specs in - typ_debug - ( lazy - ("get_val_spec: Env has " - ^ string_of_list ", " - (fun (kid, (_, k)) -> string_of_kid kid ^ " => " ^ string_of_kind_aux k) - (KBindings.bindings env.typ_vars) - ) - ); - let bind' = - List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) - in - typ_debug (lazy ("get_val_spec: freshened to " ^ string_of_bind bind')); - bind' - with Not_found -> typ_error (id_loc id) ("No type declaration found for " ^ string_of_id id) - - let get_val_specs env = env.top_val_specs - - let add_union_id id bind env = - if bound_ctor_fn env id then already_bound_ctor_fn "union constructor" id env - else begin - typ_print (lazy (adding ^ "union identifier " ^ string_of_id id ^ " : " ^ string_of_bind bind)); - { env with union_ids = Bindings.add id bind env.union_ids } - end - - let get_union_id id env = - match Bindings.find_opt id env.union_ids with - | Some bind -> List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) - | None -> typ_error (id_loc id) ("No union constructor found for " ^ string_of_id id) - - let rec valid_implicits env start = function - | Typ_aux (Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var _, _)), _)]), l) :: rest -> - if start then valid_implicits env true rest - else typ_error l "Arguments are invalid, implicit arguments must come before all other arguments" - | Typ_aux (Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp _, l)]), _) :: _ -> - typ_error l "Implicit argument must contain a single type variable" - | _ :: rest -> valid_implicits env false rest - | [] -> () - - let rec update_val_spec id (typq, typ) env = - let typq_env = add_typquant (id_loc id) typq env in - begin - match expand_synonyms typq_env typ with - | Typ_aux (Typ_fn (arg_typs, ret_typ), l) -> - valid_implicits env true arg_typs; - - (* We perform some canonicalisation for function types where existentials appear on the left, so - ({'n, 'n >= 2, int('n)}, foo) -> bar - would become - forall 'n, 'n >= 2. (int('n), foo) -> bar - this enforces the invariant that all things on the left of functions are 'base types' (i.e. without existentials) - *) - let base_args = List.map (fun typ -> destruct_exist (expand_synonyms typq_env typ)) arg_typs in - let existential_arg typq = function - | None -> typq - | Some (exs, nc, _) -> - List.fold_left (fun typq kopt -> quant_add (mk_qi_kopt kopt) typq) (quant_add (mk_qi_nc nc) typq) exs - in - let typq = List.fold_left existential_arg typq base_args in - let arg_typs = List.map2 (fun typ -> function Some (_, _, typ) -> typ | None -> typ) arg_typs base_args in - let typ = Typ_aux (Typ_fn (arg_typs, ret_typ), l) in - typ_print (lazy (adding ^ "val " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ))); - { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs } - | Typ_aux (Typ_bidir (typ1, typ2), _) -> - let env = add_mapping id (typq, typ1, typ2) env in - typ_print (lazy (adding ^ "mapping " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ))); - { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs } - | _ -> typ_error (id_loc id) "val definition must have a mapping or function type" - end - - and add_val_spec ?(ignore_duplicate = false) id (bind_typq, bind_typ) env = - if (not (Bindings.mem id env.top_val_specs)) || ignore_duplicate then update_val_spec id (bind_typq, bind_typ) env - else if ignore_duplicate then env - else ( - let previous_loc = - match Bindings.choose_opt (Bindings.filter (fun key _ -> Id.compare id key = 0) env.top_val_specs) with - | Some (prev_id, _) -> id_loc prev_id - | None -> Parse_ast.Unknown - in - let open Error_format in - Reporting.format_warn ~once_from:__POS__ - ("Duplicate function type definition for " ^ string_of_id id) - (id_loc id) - (Seq - [ - Line "This duplicate definition is being ignored!"; - Location ("", Some "previous definition here", previous_loc, Seq []); - ] - ); - env - ) - - and add_outcome id (typq, typ, params, vals, outcome_env) env = - { env with outcomes = Bindings.add id (typq, typ, params, vals, outcome_env) env.outcomes } - - and get_outcome l id env = - match Bindings.find_opt id env.outcomes with - | Some outcome -> outcome - | None -> typ_error l ("Outcome " ^ string_of_id id ^ " does not exist") - - and add_mapping id (typq, typ1, typ2) env = - typ_print (lazy (adding ^ "mapping " ^ string_of_id id)); - let forwards_id = mk_id (string_of_id id ^ "_forwards") in - let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in - let backwards_id = mk_id (string_of_id id ^ "_backwards") in - let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in - let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2), Parse_ast.Unknown) in - let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ), Parse_ast.Unknown) in - let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1), Parse_ast.Unknown) in - let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ), Parse_ast.Unknown) in - let env = - { env with mappings = Bindings.add id (typq, typ1, typ2) env.mappings } - |> add_val_spec ~ignore_duplicate:true forwards_id (typq, forwards_typ) - |> add_val_spec ~ignore_duplicate:true backwards_id (typq, backwards_typ) - |> add_val_spec ~ignore_duplicate:true forwards_matches_id (typq, forwards_matches_typ) - |> add_val_spec ~ignore_duplicate:true backwards_matches_id (typq, backwards_matches_typ) - in - let prefix_id = mk_id (string_of_id id ^ "_matches_prefix") in - if unloc_typ typ1 = string_typ then ( - let forwards_prefix_typ = - Typ_aux - ( Typ_fn ([typ1], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)]), - Parse_ast.Unknown - ) - in - add_val_spec ~ignore_duplicate:true prefix_id (typq, forwards_prefix_typ) env - ) - else if unloc_typ typ2 = string_typ then ( - let backwards_prefix_typ = - Typ_aux - ( Typ_fn ([typ2], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)]), - Parse_ast.Unknown - ) - in - add_val_spec ~ignore_duplicate:true prefix_id (typq, backwards_prefix_typ) env - ) - else env - - let get_outcome_instantiation env = env.outcome_instantiation - - let add_outcome_variable l kid typ env = - { env with outcome_instantiation = KBindings.add kid (l, typ) env.outcome_instantiation } - - let define_val_spec id env = - if IdSet.mem id env.defined_val_specs then - typ_error (id_loc id) ("Function " ^ string_of_id id ^ " has already been declared") - else { env with defined_val_specs = IdSet.add id env.defined_val_specs } - - let get_defined_val_specs env = env.defined_val_specs - - let is_ctor id (Tu_aux (tu, _)) = - match tu with Tu_ty_id (_, ctor_id) when Id.compare id ctor_id = 0 -> true | _ -> false - - let union_constructor_info id env = - let type_unions = List.map (fun (id, (_, tus)) -> (id, tus)) (Bindings.bindings env.variants) in - Util.find_map - (fun (union_id, tus) -> - Option.map (fun (n, tu) -> (n, List.length tus, union_id, tu)) (Util.find_index_opt (is_ctor id) tus) - ) - type_unions - - let is_union_constructor id env = - let type_unions = List.concat (List.map (fun (_, (_, tus)) -> tus) (Bindings.bindings env.variants)) in - List.exists (is_ctor id) type_unions - - let is_singleton_union_constructor id env = - let type_unions = List.map (fun (_, (_, tus)) -> tus) (Bindings.bindings env.variants) in - match List.find (List.exists (is_ctor id)) type_unions with l -> List.length l = 1 | exception Not_found -> false - - let is_mapping id env = Bindings.mem id env.mappings - - let add_enum' is_scattered id ids env = - if bound_typ_id env id then already_bound "enum" id env - else ( - typ_print (lazy (adding ^ "enum " ^ string_of_id id)); - { env with enums = Bindings.add id (is_scattered, IdSet.of_list ids) env.enums } - ) - - let add_scattered_enum id env = add_enum' true id [] env - let add_enum id ids env = add_enum' false id ids env - - let add_enum_clause id member env = - match Bindings.find_opt id env.enums with - | Some (true, members) -> - if IdSet.mem member members then - typ_error (id_loc id) ("Enumeration " ^ string_of_id id ^ " already has a member " ^ string_of_id member) - else { env with enums = Bindings.add id (true, IdSet.add member members) env.enums } - | Some (false, _) -> - let prev_id, _ = Bindings.find_first (fun prev_id -> Id.compare id prev_id = 0) env.enums in - typ_error - (Parse_ast.Hint ("Declared as regular enumeration here", id_loc prev_id, id_loc id)) - ("Enumeration " ^ string_of_id id ^ " is not scattered - cannot add a new member with 'enum clause'") - | None -> typ_error (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist") - - let get_enum id env = - match Bindings.find_opt id env.enums with - | Some (_, enum) -> IdSet.elements enum - | None -> typ_error (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist") - - let get_enums env = Bindings.map snd env.enums - - let is_record id env = Bindings.mem id env.records - - let get_record id env = Bindings.find id env.records - - let get_records env = env.records - - let add_record id typq fields env = - let fields = List.map (fun (typ, id) -> (expand_synonyms env typ, id)) fields in - if bound_typ_id env id then already_bound "struct" id env - else ( - typ_print (lazy (adding ^ "record " ^ string_of_id id)); - let rec record_typ_args = function - | [] -> [] - | QI_aux (QI_id kopt, _) :: qis when is_int_kopt kopt -> - mk_typ_arg (A_nexp (nvar (kopt_kid kopt))) :: record_typ_args qis - | QI_aux (QI_id kopt, _) :: qis when is_typ_kopt kopt -> - mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt)))) :: record_typ_args qis - | _ :: qis -> record_typ_args qis - in - let rectyp = - match record_typ_args (quant_items typq) with [] -> mk_id_typ id | args -> mk_typ (Typ_app (id, args)) - in - let fold_accessors accs (typ, fid) = - let acc_typ = mk_typ (Typ_fn ([rectyp], typ)) in - typ_print - ( lazy - (indent 1 ^ adding ^ "accessor " ^ string_of_id id ^ "." ^ string_of_id fid ^ " :: " - ^ string_of_bind (typq, acc_typ) - ) - ); - Bindings.add (field_name id fid) (typq, acc_typ) accs - in - { - env with - records = Bindings.add id (typq, fields) env.records; - accessors = List.fold_left fold_accessors env.accessors fields; - } - ) - - let get_accessor_fn rec_id id env = - let freshen_bind bind = - List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) - in - try freshen_bind (Bindings.find (field_name rec_id id) env.accessors) - with Not_found -> typ_error (id_loc id) ("No accessor found for " ^ string_of_id (field_name rec_id id)) - - let get_accessor rec_id id env = - match get_accessor_fn rec_id id env with - (* All accessors should have a single argument (the record itself) *) - | typq, Typ_aux (Typ_fn ([rec_typ], field_typ), _) -> (typq, rec_typ, field_typ) - | _ -> typ_error (id_loc id) ("Accessor with non-function type found for " ^ string_of_id (field_name rec_id id)) - - let is_mutable id env = - try - let mut, _ = Bindings.find id env.locals in - match mut with Mutable -> true | Immutable -> false - with Not_found -> false - - let string_of_mtyp (mut, typ) = - match mut with Immutable -> string_of_typ typ | Mutable -> "ref<" ^ string_of_typ typ ^ ">" - - let add_local id mtyp env = - if not env.allow_bindings then typ_error (id_loc id) "Bindings are not allowed in this context" else (); - wf_typ env (snd mtyp); - if Bindings.mem id env.top_val_specs then - typ_error (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name") - else (); - typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp)); - { env with locals = Bindings.add id mtyp env.locals; top_letbinds = IdSet.remove id env.top_letbinds } - - let add_toplevel_lets ids env = { env with top_letbinds = IdSet.union ids env.top_letbinds } - - let get_toplevel_lets env = env.top_letbinds - - let is_variant id env = Bindings.mem id env.variants - - let add_variant id (typq, constructors) env = - let constructors = - List.map - (fun (Tu_aux (Tu_ty_id (typ, id), l)) -> - Tu_aux (Tu_ty_id (expand_synonyms (add_typquant l typq env) typ, id), l) - ) - constructors - in - if bound_typ_id env id then already_bound "union" id env - else ( - typ_print (lazy (adding ^ "variant " ^ string_of_id id)); - { env with variants = Bindings.add id (typq, constructors) env.variants } - ) - - let add_scattered_variant id typq env = - if bound_typ_id env id then already_bound "scattered union" id env - else ( - typ_print (lazy (adding ^ "scattered variant " ^ string_of_id id)); - { - env with - variants = Bindings.add id (typq, []) env.variants; - scattered_variant_envs = Bindings.add id env env.scattered_variant_envs; - } - ) - - let add_variant_clause id tu env = - match Bindings.find_opt id env.variants with - | Some (typq, tus) -> { env with variants = Bindings.add id (typq, tus @ [tu]) env.variants } - | None -> typ_error (id_loc id) ("scattered union " ^ string_of_id id ^ " not found") - - let get_variants env = env.variants - - let get_variant id env = - match Bindings.find_opt id env.variants with - | Some (typq, tus) -> (typq, tus) - | None -> typ_error (id_loc id) ("union " ^ string_of_id id ^ " not found") - - let get_scattered_variant_env id env = - match Bindings.find_opt id env.scattered_variant_envs with - | Some env' -> env' - | None -> typ_error (id_loc id) ("scattered union " ^ string_of_id id ^ " has not been declared") - - let is_register id env = Bindings.mem id env.registers - - 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 get_registers env = env.registers - - let is_extern id env backend = - try not (Ast_util.extern_assoc backend (Bindings.find_opt id env.externs) = None) with Not_found -> false - - let add_extern id ext env = { env with externs = Bindings.add id ext env.externs } - - let get_extern id env backend = - try - match Ast_util.extern_assoc backend (Bindings.find_opt id env.externs) with - | Some ext -> ext - | None -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id) - with Not_found -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id) - - let add_register id typ env = - wf_typ env typ; - if Bindings.mem id env.registers then typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound") - else begin - typ_print (lazy (adding ^ "register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ)); - { env with registers = Bindings.add id typ env.registers } - end - - let get_locals env = env.locals - - let lookup_id id env = - try - let mut, typ = Bindings.find id env.locals in - Local (mut, typ) - with Not_found -> ( - try - let typ = Bindings.find id env.registers in - Register typ - with Not_found -> ( - try - let enum, _ = List.find (fun (_, (_, ctors)) -> IdSet.mem id ctors) (Bindings.bindings env.enums) in - Enum (mk_typ (Typ_id enum)) - with Not_found -> Unbound id - ) - ) - - let get_ret_typ env = env.ret_typ - - let add_ret_typ typ env = { env with ret_typ = Some typ } - - let no_bindings env = { env with allow_bindings = false } - - let get_default_order env = - match env.default_order with None -> typ_error Parse_ast.Unknown "No default order has been set" | Some ord -> ord - - let get_default_order_opt env = env.default_order - - let set_default_order o env = - match o with - | Ord_aux (_, l) -> ( - match env.default_order with - | None -> { env with default_order = Some o } - | Some _ -> typ_error l "Cannot change default order once already set" - ) - - let base_typ_of env typ = - let rec aux (Typ_aux (t, a)) = - let rewrap t = Typ_aux (t, a) in - match t with - | Typ_fn (arg_typs, ret_typ) -> rewrap (Typ_fn (List.map aux arg_typs, aux ret_typ)) - | Typ_tuple ts -> rewrap (Typ_tuple (List.map aux ts)) - | Typ_app (r, [A_aux (A_typ rtyp, _)]) when string_of_id r = "register" -> aux rtyp - | Typ_app (id, targs) -> rewrap (Typ_app (id, List.map aux_arg targs)) - | t -> rewrap t - and aux_arg (A_aux (targ, a)) = - let rewrap targ = A_aux (targ, a) in - match targ with A_typ typ -> rewrap (A_typ (aux typ)) | targ -> rewrap targ - in - aux (expand_synonyms env typ) - - let is_bitfield id env = Bindings.mem id env.bitfields - - let get_bitfield id env = Bindings.find id env.bitfields - - let add_bitfield id typ ranges env = { env with bitfields = Bindings.add id (typ, ranges) env.bitfields } - - let allow_polymorphic_undefineds env = { env with poly_undefineds = true } - - let polymorphic_undefineds env = env.poly_undefineds + include Type_env end +let destruct_numeric = Type_internal.destruct_numeric +let destruct_boolean = Type_internal.destruct_boolean +let destruct_exist = Type_internal.destruct_exist +let destruct_exist_plain = Type_internal.destruct_exist_plain + let get_bitfield_ranges id env = snd (Env.get_bitfield id env) let get_bitfield_range id field env = try Bindings.find_opt field (get_bitfield_ranges id env) with Not_found -> None @@ -2682,7 +1282,7 @@ and rewrite_nc_aux l env = type tannot' = { env : Env.t; typ : typ; - mutable monadic : effect; + monadic : effect; expected : typ option; instantiation : typ_arg KBindings.t option; } @@ -2914,7 +1514,7 @@ let check_function_instantiation l id env bind1 bind2 = let direction check (typq1, typ1) (typq2, typ2) = if quant_items typq1 <> [] && quant_items typq2 <> [] then ( let check_env = Env.add_typquant l typq1 env in - let typq2, typ2 = freshen_bind check_env (typq2, typ2) in + let typq2, typ2 = Env.freshen_bind check_env (typq2, typ2) in let unifiers = try unify l check_env (quant_kopts typq2 |> List.map kopt_kid |> KidSet.of_list) typ2 typ1 with Unification_error (l, m) -> typ_error l ("Unification error: " ^ m) @@ -5660,14 +4260,14 @@ and check_outcome : Env.t -> outcome_spec -> uannot def list -> outcome_spec * t | def -> typ_error (def_loc def) "Forbidden definition in outcome block" in typ_print (lazy (Util.("Check outcome " |> cyan |> clear) ^ string_of_id id ^ " : " ^ string_of_typschm typschm)); - match env.toplevel with + match Env.is_toplevel env with | None -> begin incr depth; try - let local_env = { (add_typ_vars l params env) with toplevel = Some l } in + let local_env = add_typ_vars l params env in wf_typschm local_env typschm; let quant, typ = match typschm with TypSchm_aux (TypSchm_ts (typq, typ), _) -> (typq, typ) in - let local_env = { local_env with outcome_typschm = Some (quant, typ) } in + let local_env = Env.set_outcome_typschm ~outcome_loc:l (quant, typ) local_env in List.iter valid_outcome_def defs; let defs, local_env = check_defs local_env defs in let vals = @@ -5691,7 +4291,7 @@ and check_outcome : Env.t -> outcome_spec -> uannot def list -> outcome_spec * t and check_impldef : Env.t -> def_annot -> uannot funcl -> tannot def list * Env.t = fun env def_annot (FCL_aux (FCL_funcl (id, _), (fcl_def_annot, _)) as funcl) -> typ_print (lazy (Util.("Check impl " |> cyan |> clear) ^ string_of_id id)); - match env.outcome_typschm with + match Env.get_outcome_typschm_opt env with | Some (quant, typ) -> let funcl_env = Env.add_typquant fcl_def_annot.loc quant env in ([DEF_aux (DEF_impl (check_funcl funcl_env funcl typ), def_annot)], env) @@ -5765,7 +4365,7 @@ and check_outcome_instantiation : List.iter (fun (id_from, id_to, decl_l) -> let to_typq, to_typ = Env.get_val_spec id_to env in - let from_typq, from_typ = Env.get_val_spec id_from outcome_env in + let from_typq, from_typ = Env.get_val_spec_orig id_from outcome_env in typ_debug (lazy (string_of_bind (to_typq, to_typ))); let from_typ = diff --git a/src/lib/type_check.mli b/src/lib/type_check.mli index 5b7afffa1..0fb004248 100644 --- a/src/lib/type_check.mli +++ b/src/lib/type_check.mli @@ -72,11 +72,11 @@ open Ast_defs open Ast_util module Big_int = Nat_big_num -(** [opt_tc_debug] controls the verbosity of the type checker. 0 is +(** [set_tc_debug] controls the verbosity of the type checker. 0 is silent, 1 prints a tree of the type derivation and 2 is like 1 but with much more debugging information. 3 is the highest level, and is even more verbose still. *) -val opt_tc_debug : int ref +val set_tc_debug : int -> unit (** [opt_no_lexp_bounds_check] turns off the bounds checking in vector assignments in l-expressions. *) @@ -87,36 +87,13 @@ val opt_no_lexp_bounds_check : bool ref otherwise a good idea. *) val opt_expand_valspec : bool ref -(** Linearize cases involving power where we would otherwise require - the SMT solver to use non-linear arithmetic. *) -val opt_smt_linearize : bool ref - (** Don't expand bitfields (when using old syntax), used for LaTeX output *) val opt_no_bitfield_expansion : bool ref -(** {2 Type errors} *) - -type constraint_reason = (Ast.l * string) option - -type type_error = - | Err_no_casts of uannot exp * typ * typ * type_error * type_error list - | Err_no_overloading of id * (id * type_error) list - | Err_unresolved_quants of id * quant_item list * (mut * typ) Bindings.t * n_constraint list - | Err_failed_constraint of n_constraint * (mut * typ) Bindings.t * n_constraint list - | Err_subtype of typ * typ * n_constraint option * (constraint_reason * n_constraint) list * Ast.l KBindings.t - | Err_no_num_ident of id - | Err_other of string - | Err_inner of type_error * Ast.l * string * string option * type_error +(** {2 Environments} *) type env -exception Type_error of l * type_error - -val typ_debug : ?level:int -> string Lazy.t -> unit -val typ_print : string Lazy.t -> unit - -(** {2 Environments} *) - (** The env module defines the internal type checking environment, and contains functions that operate on that state. *) module Env : sig @@ -198,7 +175,7 @@ module Env : sig val get_variants : t -> (typquant * type_union list) Bindings.t - (** Return type is: quantifier, argument type, return type, effect *) + (** Return type is: quantifier, argument type, return type *) val get_accessor : id -> id -> t -> typquant * typ * typ (** If the environment is checking a function, then this will get @@ -342,18 +319,6 @@ val strip_typedef : tannot type_def -> uannot type_def val strip_def : tannot def -> uannot def val strip_ast : tannot ast -> uannot ast -(** Remove location information from types for comparison purposes *) -val unloc_typ : typ -> typ - -val unloc_typq : typquant -> typquant -val unloc_id : id -> id -val unloc_kid : kid -> kid -val unloc_nexp_aux : nexp_aux -> nexp_aux -val unloc_nexp : nexp -> nexp -val unloc_n_constraint_aux : n_constraint_aux -> n_constraint_aux -val unloc_n_constraint : n_constraint -> n_constraint -val unloc_typ_aux : typ_aux -> typ_aux - (** {2 Checking expressions and patterns} *) (** Check an expression has some type. Returns a fully annotated @@ -414,8 +379,6 @@ val bind_pat : Env.t -> uannot pat -> typ -> tannot pat * Env.t * uannot Ast.exp on patterns that have previously been type checked. *) val bind_pat_no_guard : Env.t -> uannot pat -> typ -> tannot pat * Env.t -val typ_error : Ast.l -> string -> 'a - val tc_assume : n_constraint -> tannot exp -> tannot exp (** {2 Destructuring type annotations} diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml new file mode 100644 index 000000000..5137b0a23 --- /dev/null +++ b/src/lib/type_env.ml @@ -0,0 +1,1286 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2021 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(****************************************************************************) + +open Ast +open Ast_util +open Util + +module Big_int = Nat_big_num + +open Type_internal + +(* Linearize cases involving power where we would otherwise require + the SMT solver to use non-linear arithmetic. *) +let opt_smt_linearize = ref false + +module IdPair = struct + type t = id * id + let compare (a, b) (c, d) = + let x = Id.compare a c in + if x = 0 then Id.compare b d else x +end + +module IdPairMap = Map.Make (IdPair) + +type ('a, 'b) generic_env_item = { item : 'a; loc : 'b } + +type 'a env_item = ('a, Parse_ast.l) generic_env_item + +type 'a multiple_env_item = ('a, Parse_ast.l list) generic_env_item + +let mk_item ~loc:l item = { item; loc = l } + +let get_item item = item.item + +let item_loc item = item.loc + +type global_env = { + default_order : order option; + val_specs : (typquant * typ) env_item Bindings.t; + defined_val_specs : IdSet.t; + externs : extern Bindings.t; + mappings : (typquant * typ * typ) env_item Bindings.t; + unions : (typquant * type_union list) env_item Bindings.t; + union_ids : (typquant * typ) env_item Bindings.t; + scattered_union_envs : global_env Bindings.t; + enums : (bool * IdSet.t) env_item Bindings.t; + records : (typquant * (typ * id) list) env_item Bindings.t; + synonyms : (typquant * typ_arg) env_item Bindings.t; + accessors : (typquant * typ) env_item IdPairMap.t; + bitfields : (typ * index_range Bindings.t) env_item Bindings.t; + letbinds : typ env_item Bindings.t; + registers : typ env_item Bindings.t; + overloads : id list multiple_env_item Bindings.t; + outcomes : (typquant * typ * kinded_id list * id list * (typquant * typ) env_item Bindings.t) env_item Bindings.t; + outcome_instantiation : (Ast.l * typ) KBindings.t; +} + +let empty_global_env = + { + default_order = None; + val_specs = Bindings.empty; + defined_val_specs = IdSet.empty; + externs = Bindings.empty; + mappings = Bindings.empty; + unions = Bindings.empty; + union_ids = Bindings.empty; + scattered_union_envs = Bindings.empty; + enums = Bindings.empty; + records = Bindings.empty; + accessors = IdPairMap.empty; + synonyms = Bindings.empty; + bitfields = Bindings.empty; + letbinds = Bindings.empty; + registers = Bindings.empty; + overloads = Bindings.empty; + outcomes = Bindings.empty; + outcome_instantiation = KBindings.empty; + } + +type env = { + global : global_env; + locals : (mut * typ) Bindings.t; + typ_vars : (Ast.l * kind_aux) KBindings.t; + shadow_vars : int KBindings.t; + allow_bindings : bool; + constraints : (constraint_reason * n_constraint) list; + ret_typ : typ option; + poly_undefineds : bool; + prove : (env -> n_constraint -> bool) option; + allow_unknowns : bool; + toplevel : l option; + outcome_typschm : (typquant * typ) option; +} + +type t = env + +let update_global f env = { env with global = f env.global } + +let empty = + { + global = empty_global_env; + locals = Bindings.empty; + typ_vars = KBindings.empty; + shadow_vars = KBindings.empty; + allow_bindings = true; + constraints = []; + ret_typ = None; + poly_undefineds = false; + prove = None; + allow_unknowns = false; + toplevel = None; + outcome_typschm = None; + } + +let counter = ref 0 + +let fresh_kid ?(kid = mk_kid "") _env = + let suffix = if Kid.compare kid (mk_kid "") = 0 then "#" else "#" ^ string_of_id (id_of_kid kid) in + let fresh = Kid_aux (Var ("'fv" ^ string_of_int !counter ^ suffix), Parse_ast.Unknown) in + incr counter; + fresh + +let freshen_kid env kid (typq, typ) = + if KidSet.mem kid (KidSet.of_list (List.map kopt_kid (quant_kopts typq))) then ( + let fresh = fresh_kid ~kid env in + (typquant_subst_kid kid fresh typq, subst_kid typ_subst kid fresh typ) + ) + else (typq, typ) + +let freshen_bind env bind = + List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) + +let set_prover f env = { env with prove = f } + +let allow_unknowns env = env.allow_unknowns +let set_allow_unknowns b env = { env with allow_unknowns = b } + +(* First, we define how type variables are added to the + environment. If we add a new variable shadowing a previous + variable, we need to modify the environment so the shadowed + variable is renamed. We can't just remove it because it may be + referenced by constraints. *) +let shadows v env = match KBindings.find_opt v env.shadow_vars with Some n -> n | None -> 0 + +let add_typ_var_shadow l (KOpt_aux (KOpt_kind (K_aux (k, _), v), _)) env = + if KBindings.mem v env.typ_vars then begin + let n = match KBindings.find_opt v env.shadow_vars with Some n -> n | None -> 0 in + let s_l, s_k = KBindings.find v env.typ_vars in + let s_v = Kid_aux (Var (string_of_kid v ^ "#" ^ string_of_int n), l) in + typ_print + ( lazy + (Printf.sprintf "%stype variable (shadowing %s) %s : %s" adding (string_of_kid s_v) (string_of_kid v) + (string_of_kind_aux k) + ) + ); + ( { + env with + constraints = List.map (fun (l, nc) -> (l, constraint_subst v (arg_kopt (mk_kopt s_k s_v)) nc)) env.constraints; + typ_vars = KBindings.add v (l, k) (KBindings.add s_v (s_l, s_k) env.typ_vars); + locals = Bindings.map (fun (mut, typ) -> (mut, typ_subst v (arg_kopt (mk_kopt s_k s_v)) typ)) env.locals; + shadow_vars = KBindings.add v (n + 1) env.shadow_vars; + }, + Some s_v + ) + end + else begin + typ_print (lazy (adding ^ "type variable " ^ string_of_kid v ^ " : " ^ string_of_kind_aux k)); + ({ env with typ_vars = KBindings.add v (l, k) env.typ_vars }, None) + end + +let add_typ_var l kopt env = fst (add_typ_var_shadow l kopt env) + +let get_typ_var_loc_opt kid env = match KBindings.find_opt kid env.typ_vars with Some (l, _) -> Some l | None -> None + +let get_typ_var kid env = + try snd (KBindings.find kid env.typ_vars) + with Not_found -> typ_error (kid_loc kid) ("No type variable " ^ string_of_kid kid) + +let get_typ_vars env = KBindings.map snd env.typ_vars +let get_typ_var_locs env = KBindings.map fst env.typ_vars + +let k_counter = ref 0 +let k_name () = + let kid = mk_kid ("k#" ^ string_of_int !k_counter) in + incr k_counter; + kid + +let kinds_typq kinds = mk_typquant (List.map (fun k -> mk_qi_id k (k_name ())) kinds) + +let builtin_typs = + List.fold_left + (fun m (name, kinds) -> Bindings.add (mk_id name) (kinds_typq kinds) m) + Bindings.empty + [ + ("range", [K_int; K_int]); + ("atom", [K_int]); + ("implicit", [K_int]); + ("vector", [K_int; K_type]); + ("bitvector", [K_int]); + ("register", [K_type]); + ("bit", []); + ("unit", []); + ("int", []); + ("nat", []); + ("bool", []); + ("real", []); + ("list", [K_type]); + ("string", []); + ("itself", [K_int]); + ("atom_bool", [K_bool]); + ("float16", []); + ("float32", []); + ("float64", []); + ("float128", []); + ("float_rounding_mode", []); + ] + +let bound_typ_id env id = + Bindings.mem id env.global.synonyms || Bindings.mem id env.global.unions || Bindings.mem id env.global.records + || Bindings.mem id env.global.enums || Bindings.mem id builtin_typs + +let get_binding_loc env id = + let find map = Some (item_loc (Bindings.find id map)) in + if Bindings.mem id builtin_typs then None + else if Bindings.mem id env.global.unions then find env.global.unions + else if Bindings.mem id env.global.records then find env.global.records + else if Bindings.mem id env.global.enums then find env.global.enums + else if Bindings.mem id env.global.synonyms then find env.global.synonyms + else None + +let already_bound str id env = + match get_binding_loc env id with + | Some l -> + typ_raise (id_loc id) + (Err_inner + ( Err_other ("Cannot create " ^ str ^ " type " ^ string_of_id id ^ ", name is already bound"), + l, + "", + Some "previous binding", + Err_other "" + ) + ) + | None -> + let suffix = if Bindings.mem id builtin_typs then " as a built-in type" else "" in + typ_error (id_loc id) ("Cannot create " ^ str ^ " type " ^ string_of_id id ^ ", name is already bound" ^ suffix) + +let bound_ctor_fn env id = Bindings.mem id env.global.val_specs || Bindings.mem id env.global.union_ids + +let get_ctor_fn_binding_loc env id = + if Bindings.mem id env.global.val_specs then Some (item_loc (Bindings.find id env.global.val_specs)) + else if Bindings.mem id env.global.union_ids then Some (item_loc (Bindings.find id env.global.union_ids)) + else None + +let already_bound_ctor_fn str id env = + match get_ctor_fn_binding_loc env id with + | Some l -> + typ_raise (id_loc id) + (Err_inner + ( Err_other + ("Cannot create " ^ str ^ " " ^ string_of_id id + ^ ", name is already bound to a union constructor or function" + ), + l, + "", + Some "previous binding", + Err_other "" + ) + ) + | None -> + Reporting.unreachable (id_loc id) __POS__ + ("Could not find original binding for duplicate " ^ str ^ " called " ^ string_of_id id) + +let get_overloads id env = try get_item (Bindings.find id env.global.overloads) with Not_found -> [] + +let add_overloads l id ids env = + typ_print (lazy (adding ^ "overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]")); + List.iter + (fun overload -> + if not (bound_ctor_fn env overload || Bindings.mem overload env.global.overloads) then + typ_error + (Hint ("unbound identifier", id_loc overload, l)) + ("Cannot create or extend overload " ^ string_of_id id ^ ", " ^ string_of_id overload ^ " is not bound") + ) + ids; + match Bindings.find_opt id env.global.overloads with + | Some existing -> + update_global + (fun global -> + { + global with + overloads = + Bindings.add id (mk_item ~loc:(l :: item_loc existing) (get_item existing @ ids)) global.overloads; + } + ) + env + | None -> + update_global + (fun global -> { global with overloads = Bindings.add id (mk_item ~loc:[l] ids) global.overloads }) + env + +let infer_kind env id = + if Bindings.mem id builtin_typs then Bindings.find id builtin_typs + else if Bindings.mem id env.global.unions then fst (get_item (Bindings.find id env.global.unions)) + else if Bindings.mem id env.global.records then fst (get_item (Bindings.find id env.global.records)) + else if Bindings.mem id env.global.enums then mk_typquant [] + else if Bindings.mem id env.global.synonyms then + typ_error (id_loc id) ("Cannot infer kind of type synonym " ^ string_of_id id) + else typ_error (id_loc id) ("Cannot infer kind of " ^ string_of_id id) + +let check_args_typquant id env args typq = + let kopts, ncs = quant_split typq in + let rec subst_args kopts args = + match (kopts, args) with + | kopt :: kopts, (A_aux (A_nexp _, _) as arg) :: args when is_int_kopt kopt -> + List.map (constraint_subst (kopt_kid kopt) arg) (subst_args kopts args) + | kopt :: kopts, A_aux (A_typ _, _) :: args when is_typ_kopt kopt -> subst_args kopts args + | kopt :: kopts, A_aux (A_bool _, _) :: args when is_bool_kopt kopt -> subst_args kopts args + | [], [] -> ncs + | _, A_aux (_, l) :: _ -> typ_error l ("Error when processing type quantifer arguments " ^ string_of_typquant typq) + | _, _ -> typ_error Parse_ast.Unknown ("Error when processing type quantifer arguments " ^ string_of_typquant typq) + in + let ncs = subst_args kopts args in + if match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false then () + else + typ_error (id_loc id) + ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id) + +let mk_synonym typq typ_arg = + let kopts, ncs = quant_split typq in + let kopts = List.map (fun kopt -> (kopt, fresh_existential (kopt_loc kopt) (unaux_kind (kopt_kind kopt)))) kopts in + let ncs = + List.map + (fun nc -> List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts) + ncs + in + let typ_arg = + List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts + in + let kopts = List.map snd kopts in + let rec subst_args env l kopts args = + match (kopts, args) with + | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_int_kopt kopt -> + let typ_arg, ncs = subst_args env l kopts args in + ( typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg, + List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs + ) + | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt -> + let typ_arg, ncs = subst_args env l kopts args in + (typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg, ncs) + | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt -> + let typ_arg, ncs = subst_args env l kopts args in + (typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs) + | [], [] -> (typ_arg, ncs) + | _, _ -> typ_error l "Synonym applied to bad arguments" + in + fun l env args -> + let typ_arg, ncs = subst_args env l kopts args in + if match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false then typ_arg + else + typ_error l + ("Could not prove constraints " + ^ string_of_list ", " string_of_n_constraint ncs + ^ " in type synonym " ^ string_of_typ_arg typ_arg ^ " with " + ^ Util.string_of_list ", " string_of_n_constraint (List.map snd env.constraints) + ) + +let get_typ_synonym id env = + match Option.map get_item (Bindings.find_opt id env.global.synonyms) with + | Some (typq, arg) -> mk_synonym typq arg + | None -> raise Not_found + +let get_typ_synonyms env = Bindings.map get_item env.global.synonyms + +let get_constraints env = List.map snd env.constraints + +let get_constraint_reasons env = env.constraints + +let wf_debug str f x exs = + typ_debug ~level:2 + (lazy ("wf_" ^ str ^ ": " ^ f x ^ " exs: " ^ Util.string_of_list ", " string_of_kid (KidSet.elements exs))) + +(* Check if a type, order, n-expression or constraint is + well-formed. Throws a type error if the type is badly formed. *) +let rec wf_typ' ?(exs = KidSet.empty) env (Typ_aux (typ_aux, l) as typ) = + match typ_aux with + | Typ_id id when bound_typ_id env id -> + let typq = infer_kind env id in + if quant_kopts typq != [] then + typ_error l ("Type constructor " ^ string_of_id id ^ " expected " ^ string_of_typquant typq) + else () + | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id) + | Typ_var kid -> begin + match KBindings.find kid env.typ_vars with + | _, K_type -> () + | _, k -> + typ_error l + ("Type variable " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ ^ " is " ^ string_of_kind_aux k + ^ " rather than Type" + ) + | exception Not_found -> + typ_error l ("Unbound type variable " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ) + end + | Typ_fn (arg_typs, ret_typ) -> + List.iter (wf_typ' ~exs env) arg_typs; + wf_typ' ~exs env ret_typ + | Typ_bidir (typ1, typ2) when unloc_typ typ1 = unloc_typ typ2 -> + typ_error l "Bidirectional types cannot be the same on both sides" + | Typ_bidir (typ1, typ2) -> + wf_typ' ~exs env typ1; + wf_typ' ~exs env typ2 + | Typ_tuple typs -> List.iter (wf_typ' ~exs env) typs + | Typ_app (id, [(A_aux (A_nexp _, _) as arg)]) when string_of_id id = "implicit" -> wf_typ_arg ~exs env arg + | Typ_app (id, args) when bound_typ_id env id -> + List.iter (wf_typ_arg ~exs env) args; + check_args_typquant id env args (infer_kind env id) + | Typ_app (id, _) -> typ_error l ("Undefined type " ^ string_of_id id) + | Typ_exist ([], _, _) -> typ_error l "Existential must have some type variables" + | Typ_exist (kopts, nc, typ) when KidSet.is_empty exs -> + wf_constraint ~exs:(KidSet.of_list (List.map kopt_kid kopts)) env nc; + wf_typ' ~exs:(KidSet.of_list (List.map kopt_kid kopts)) env typ + | Typ_exist (_, _, _) -> typ_error l "Nested existentials are not allowed" + | Typ_internal_unknown -> Reporting.unreachable l __POS__ "escaped Typ_internal_unknown" + +and wf_typ_arg ?(exs = KidSet.empty) env (A_aux (typ_arg_aux, _)) = + match typ_arg_aux with + | A_nexp nexp -> wf_nexp ~exs env nexp + | A_typ typ -> wf_typ' ~exs env typ + | A_bool nc -> wf_constraint ~exs env nc + +and wf_nexp ?(exs = KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) = + wf_debug "nexp" string_of_nexp nexp exs; + match nexp_aux with + | Nexp_id id -> typ_error l ("Undefined type synonym " ^ string_of_id id) + | Nexp_var kid when KidSet.mem kid exs -> () + | Nexp_var kid -> begin + match get_typ_var kid env with + | K_int -> () + | kind -> + typ_error l + ("Constraint is badly formed, " ^ string_of_kid kid ^ " has kind " ^ string_of_kind_aux kind + ^ " but should have kind Int" + ) + end + | Nexp_constant _ -> () + | Nexp_app (_, nexps) -> List.iter (fun n -> wf_nexp ~exs env n) nexps + | Nexp_times (nexp1, nexp2) -> + wf_nexp ~exs env nexp1; + wf_nexp ~exs env nexp2 + | Nexp_sum (nexp1, nexp2) -> + wf_nexp ~exs env nexp1; + wf_nexp ~exs env nexp2 + | Nexp_minus (nexp1, nexp2) -> + wf_nexp ~exs env nexp1; + wf_nexp ~exs env nexp2 + | Nexp_exp nexp -> wf_nexp ~exs env nexp (* MAYBE: Could put restrictions on what is allowed here *) + | Nexp_neg nexp -> wf_nexp ~exs env nexp + +and wf_constraint ?(exs = KidSet.empty) env (NC_aux (nc_aux, l) as nc) = + wf_debug "constraint" string_of_n_constraint nc exs; + match nc_aux with + | NC_equal (n1, n2) -> + wf_nexp ~exs env n1; + wf_nexp ~exs env n2 + | NC_not_equal (n1, n2) -> + wf_nexp ~exs env n1; + wf_nexp ~exs env n2 + | NC_bounded_ge (n1, n2) -> + wf_nexp ~exs env n1; + wf_nexp ~exs env n2 + | NC_bounded_gt (n1, n2) -> + wf_nexp ~exs env n1; + wf_nexp ~exs env n2 + | NC_bounded_le (n1, n2) -> + wf_nexp ~exs env n1; + wf_nexp ~exs env n2 + | NC_bounded_lt (n1, n2) -> + wf_nexp ~exs env n1; + wf_nexp ~exs env n2 + | NC_set (kid, _) when KidSet.mem kid exs -> () + | NC_set (kid, _) -> begin + match get_typ_var kid env with + | K_int -> () + | kind -> + typ_error l + ("Set constraint is badly formed, " ^ string_of_kid kid ^ " has kind " ^ string_of_kind_aux kind + ^ " but should have kind Int" + ) + end + | NC_or (nc1, nc2) -> + wf_constraint ~exs env nc1; + wf_constraint ~exs env nc2 + | NC_and (nc1, nc2) -> + wf_constraint ~exs env nc1; + wf_constraint ~exs env nc2 + | NC_app (_, args) -> List.iter (wf_typ_arg ~exs env) args + | NC_var kid when KidSet.mem kid exs -> () + | NC_var kid -> begin + match get_typ_var kid env with + | K_bool -> () + | kind -> typ_error l (string_of_kid kid ^ " has kind " ^ string_of_kind_aux kind ^ " but should have kind Bool") + end + | NC_true | NC_false -> () + +let rec expand_constraint_synonyms env (NC_aux (aux, l) as nc) = + match aux with + | NC_or (nc1, nc2) -> NC_aux (NC_or (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l) + | NC_and (nc1, nc2) -> NC_aux (NC_and (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l) + | NC_equal (n1, n2) -> NC_aux (NC_equal (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) + | NC_not_equal (n1, n2) -> NC_aux (NC_not_equal (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) + | NC_bounded_le (n1, n2) -> NC_aux (NC_bounded_le (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) + | NC_bounded_lt (n1, n2) -> NC_aux (NC_bounded_lt (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) + | NC_bounded_ge (n1, n2) -> NC_aux (NC_bounded_ge (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) + | NC_bounded_gt (n1, n2) -> NC_aux (NC_bounded_gt (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) + | NC_app (id, args) -> ( + try + begin + match get_typ_synonym id env l env args with + | A_aux (A_bool nc, _) -> expand_constraint_synonyms env nc + | arg -> + typ_error l ("Expected Bool when expanding synonym " ^ string_of_id id ^ " got " ^ string_of_typ_arg arg) + end + with Not_found -> NC_aux (NC_app (id, List.map (expand_arg_synonyms env) args), l) + ) + | NC_true | NC_false | NC_var _ | NC_set _ -> nc + +and expand_nexp_synonyms env (Nexp_aux (aux, l) as nexp) = + match aux with + | Nexp_app (id, args) -> ( + try + begin + match get_typ_synonym id env l env [] with + | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp + | _ -> typ_error l ("Expected Int when expanding synonym " ^ string_of_id id) + end + with Not_found -> Nexp_aux (Nexp_app (id, List.map (expand_nexp_synonyms env) args), l) + ) + | Nexp_id id -> ( + try + begin + match get_typ_synonym id env l env [] with + | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp + | _ -> typ_error l ("Expected Int when expanding synonym " ^ string_of_id id) + end + with Not_found -> nexp + ) + | Nexp_times (nexp1, nexp2) -> + Nexp_aux (Nexp_times (expand_nexp_synonyms env nexp1, expand_nexp_synonyms env nexp2), l) + | Nexp_sum (nexp1, nexp2) -> Nexp_aux (Nexp_sum (expand_nexp_synonyms env nexp1, expand_nexp_synonyms env nexp2), l) + | Nexp_minus (nexp1, nexp2) -> + Nexp_aux (Nexp_minus (expand_nexp_synonyms env nexp1, expand_nexp_synonyms env nexp2), l) + | Nexp_exp nexp -> Nexp_aux (Nexp_exp (expand_nexp_synonyms env nexp), l) + | Nexp_neg nexp -> Nexp_aux (Nexp_neg (expand_nexp_synonyms env nexp), l) + | Nexp_var kid -> Nexp_aux (Nexp_var kid, l) + | Nexp_constant n -> Nexp_aux (Nexp_constant n, l) + +and expand_synonyms env (Typ_aux (typ, l)) = + match typ with + | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l) + | Typ_tuple typs -> Typ_aux (Typ_tuple (List.map (expand_synonyms env) typs), l) + | Typ_fn (arg_typs, ret_typ) -> + Typ_aux (Typ_fn (List.map (expand_synonyms env) arg_typs, expand_synonyms env ret_typ), l) + | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2), l) + | Typ_app (id, args) -> ( + try + begin + match get_typ_synonym id env l env args with + | A_aux (A_typ typ, _) -> expand_synonyms env typ + | _ -> typ_error l ("Expected Type when expanding synonym " ^ string_of_id id) + end + with Not_found -> Typ_aux (Typ_app (id, List.map (expand_arg_synonyms env) args), l) + ) + | Typ_id id -> ( + try + begin + match get_typ_synonym id env l env [] with + | A_aux (A_typ typ, _) -> expand_synonyms env typ + | _ -> typ_error l ("Expected Type when expanding synonym " ^ string_of_id id) + end + with Not_found -> Typ_aux (Typ_id id, l) + ) + | Typ_exist (kopts, nc, typ) -> + let nc = expand_constraint_synonyms env nc in + + (* When expanding an existential synonym we need to take care + to add the type variables and constraints to the + environment, so we can check constraints attached to type + synonyms within the existential. Furthermore, we must take + care to avoid clobbering any existing type variables in + scope while doing this. *) + let rebindings = ref [] in + + let rename_kopt (KOpt_aux (KOpt_kind (k, kid), l) as kopt) = + if KBindings.mem kid env.typ_vars then KOpt_aux (KOpt_kind (k, prepend_kid "syn#" kid), l) else kopt + in + let add_typ_var env (KOpt_aux (KOpt_kind (k, kid), l)) = + try + let l, _ = KBindings.find kid env.typ_vars in + rebindings := kid :: !rebindings; + { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) (l, unaux_kind k) env.typ_vars } + with Not_found -> { env with typ_vars = KBindings.add kid (l, unaux_kind k) env.typ_vars } + in + + let env = List.fold_left add_typ_var env kopts in + let kopts = List.map rename_kopt kopts in + let nc = + List.fold_left (fun nc kid -> constraint_subst kid (arg_nexp (nvar (prepend_kid "syn#" kid))) nc) nc !rebindings + in + let typ = + List.fold_left (fun typ kid -> typ_subst kid (arg_nexp (nvar (prepend_kid "syn#" kid))) typ) typ !rebindings + in + let env = add_constraint nc env in + Typ_aux (Typ_exist (kopts, nc, expand_synonyms env typ), l) + | Typ_var v -> Typ_aux (Typ_var v, l) + +and expand_arg_synonyms env (A_aux (typ_arg, l)) = + match typ_arg with + | A_typ typ -> A_aux (A_typ (expand_synonyms env typ), l) + | A_bool nc -> A_aux (A_bool (expand_constraint_synonyms env nc), l) + | A_nexp nexp -> A_aux (A_nexp (expand_nexp_synonyms env nexp), l) + +and add_constraint ?reason constr env = + let (NC_aux (nc_aux, l) as constr) = constraint_simp (expand_constraint_synonyms env constr) in + wf_constraint env constr; + let power_vars = constraint_power_variables constr in + if KidSet.cardinal power_vars > 1 && !opt_smt_linearize then + typ_error l + ("Cannot add constraint " ^ string_of_n_constraint constr + ^ " where more than two variables appear within an exponential" + ) + else if KidSet.cardinal power_vars = 1 && !opt_smt_linearize then ( + let v = KidSet.choose power_vars in + let constrs = List.fold_left nc_and nc_true (get_constraints env) in + begin + match Constraint.solve_all_smt l constrs v with + | Some solutions -> + typ_print + ( lazy + (Util.("Linearizing " |> red |> clear) + ^ string_of_n_constraint constr ^ " for " ^ string_of_kid v ^ " in " + ^ Util.string_of_list ", " Big_int.to_string solutions + ) + ); + let linearized = + List.fold_left + (fun c s -> + nc_or c (nc_and (nc_eq (nvar v) (nconstant s)) (constraint_subst v (arg_nexp (nconstant s)) constr)) + ) + nc_false solutions + in + typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint linearized)); + { env with constraints = (reason, linearized) :: env.constraints } + | None -> + typ_error l + ("Type variable " ^ string_of_kid v ^ " must have a finite number of solutions to add " + ^ string_of_n_constraint constr + ) + end + ) + else ( + match nc_aux with + | NC_true -> env + | _ -> + typ_print (lazy (adding ^ "constraint " ^ string_of_n_constraint constr)); + { env with constraints = (reason, constr) :: env.constraints } + ) + +let add_typquant l quant env = + let rec add_quant_item env = function QI_aux (qi, _) -> add_quant_item_aux env qi + and add_quant_item_aux env = function + | QI_constraint constr -> add_constraint constr env + | QI_id kopt -> add_typ_var l kopt env + in + match quant with + | TypQ_aux (TypQ_no_forall, _) -> env + | TypQ_aux (TypQ_tq quants, _) -> List.fold_left add_quant_item env quants + +let wf_typ env (Typ_aux (_, l) as typ) = + let typ = expand_synonyms env typ in + wf_debug "typ" string_of_typ typ KidSet.empty; + incr depth; + try + wf_typ' env typ; + decr depth + with Type_error (err_l, err) -> + decr depth; + typ_raise l (err_because (Err_other "Well-formedness check failed for type", err_l, err)) + +let add_typ_synonym id typq arg env = + if bound_typ_id env id then + typ_error (id_loc id) + ("Cannot define type synonym " ^ string_of_id id ^ ", as a type or synonym with that name already exists") + else ( + let typq = + quant_map_items + (function + | QI_aux (QI_constraint nexp, aux) -> QI_aux (QI_constraint (expand_constraint_synonyms env nexp), aux) + | quant_item -> quant_item + ) + typq + in + typ_print + ( lazy + (adding ^ "type synonym " ^ string_of_id id ^ ", " ^ string_of_typquant typq ^ " = " ^ string_of_typ_arg arg) + ); + update_global + (fun global -> + { + global with + synonyms = + Bindings.add id + (mk_item ~loc:(id_loc id) (typq, expand_arg_synonyms (add_typquant (id_loc id) typq env) arg)) + global.synonyms; + } + ) + env + ) + +let get_val_spec_orig id env = + try get_item (Bindings.find id env.global.val_specs) + with Not_found -> typ_error (id_loc id) ("No type signature found for " ^ string_of_id id) + +let get_val_spec id env = + try + let bind = get_item (Bindings.find id env.global.val_specs) in + typ_debug + ( lazy + ("get_val_spec: Env has " + ^ string_of_list ", " + (fun (kid, (_, k)) -> string_of_kid kid ^ " => " ^ string_of_kind_aux k) + (KBindings.bindings env.typ_vars) + ) + ); + let bind' = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in + typ_debug (lazy ("get_val_spec: freshened to " ^ string_of_bind bind')); + bind' + with Not_found -> typ_error (id_loc id) ("No type declaration found for " ^ string_of_id id) + +let get_val_specs env = Bindings.map get_item env.global.val_specs + +let add_union_id id bind env = + if bound_ctor_fn env id then already_bound_ctor_fn "union constructor" id env + else ( + typ_print (lazy (adding ^ "union identifier " ^ string_of_id id ^ " : " ^ string_of_bind bind)); + update_global + (fun global -> { global with union_ids = Bindings.add id { item = bind; loc = id_loc id } global.union_ids }) + env + ) + +let get_union_id id env = + match Option.map get_item (Bindings.find_opt id env.global.union_ids) with + | Some bind -> List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) + | None -> typ_error (id_loc id) ("No union constructor found for " ^ string_of_id id) + +let rec valid_implicits env start = function + | Typ_aux (Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp (Nexp_aux (Nexp_var _, _)), _)]), l) :: rest -> + if start then valid_implicits env true rest + else typ_error l "Arguments are invalid, implicit arguments must come before all other arguments" + | Typ_aux (Typ_app (Id_aux (Id "implicit", _), [A_aux (A_nexp _, l)]), _) :: _ -> + typ_error l "Implicit argument must contain a single type variable" + | _ :: rest -> valid_implicits env false rest + | [] -> () + +let rec update_val_spec id (typq, typ) env = + let typq_env = add_typquant (id_loc id) typq env in + begin + match expand_synonyms typq_env typ with + | Typ_aux (Typ_fn (arg_typs, ret_typ), l) -> + valid_implicits env true arg_typs; + + (* We perform some canonicalisation for function types where existentials appear on the left, so + ({'n, 'n >= 2, int('n)}, foo) -> bar + would become + forall 'n, 'n >= 2. (int('n), foo) -> bar + this enforces the invariant that all things on the left of functions are 'base types' (i.e. without existentials) + *) + let base_args = List.map (fun typ -> destruct_exist (expand_synonyms typq_env typ)) arg_typs in + let existential_arg typq = function + | None -> typq + | Some (exs, nc, _) -> + List.fold_left (fun typq kopt -> quant_add (mk_qi_kopt kopt) typq) (quant_add (mk_qi_nc nc) typq) exs + in + let typq = List.fold_left existential_arg typq base_args in + let arg_typs = List.map2 (fun typ -> function Some (_, _, typ) -> typ | None -> typ) arg_typs base_args in + let typ = Typ_aux (Typ_fn (arg_typs, ret_typ), l) in + typ_print (lazy (adding ^ "val " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ))); + update_global + (fun global -> + { global with val_specs = Bindings.add id (mk_item ~loc:(id_loc id) (typq, typ)) global.val_specs } + ) + env + | Typ_aux (Typ_bidir (typ1, typ2), _) -> + let env = add_mapping id (typq, typ1, typ2) env in + typ_print (lazy (adding ^ "mapping " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ))); + update_global + (fun global -> + { global with val_specs = Bindings.add id (mk_item ~loc:(id_loc id) (typq, typ)) global.val_specs } + ) + env + | _ -> typ_error (id_loc id) "val definition must have a mapping or function type" + end + +and add_val_spec ?(ignore_duplicate = false) id (bind_typq, bind_typ) env = + if (not (Bindings.mem id env.global.val_specs)) || ignore_duplicate then update_val_spec id (bind_typq, bind_typ) env + else if ignore_duplicate then env + else ( + let previous_loc = + match Bindings.choose_opt (Bindings.filter (fun key _ -> Id.compare id key = 0) env.global.val_specs) with + | Some (prev_id, _) -> id_loc prev_id + | None -> Parse_ast.Unknown + in + let open Error_format in + Reporting.format_warn ~once_from:__POS__ + ("Duplicate function type definition for " ^ string_of_id id) + (id_loc id) + (Seq + [ + Line "This duplicate definition is being ignored!"; + Location ("", Some "previous definition here", previous_loc, Seq []); + ] + ); + env + ) + +and add_outcome id (typq, typ, params, vals, outcome_env) env = + update_global + (fun global -> + { + global with + outcomes = + Bindings.add id + (mk_item ~loc:(id_loc id) (typq, typ, params, vals, outcome_env.global.val_specs)) + global.outcomes; + } + ) + env + +and get_outcome l id env = + match Option.map get_item (Bindings.find_opt id env.global.outcomes) with + | Some (typq, typ, params, vals, val_specs) -> + (typq, typ, params, vals, { empty with global = { empty_global_env with val_specs } }) + | None -> typ_error l ("Outcome " ^ string_of_id id ^ " does not exist") + +and add_mapping id (typq, typ1, typ2) env = + typ_print (lazy (adding ^ "mapping " ^ string_of_id id)); + let forwards_id = mk_id (string_of_id id ^ "_forwards") in + let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in + let backwards_id = mk_id (string_of_id id ^ "_backwards") in + let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in + let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2), Parse_ast.Unknown) in + let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ), Parse_ast.Unknown) in + let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1), Parse_ast.Unknown) in + let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ), Parse_ast.Unknown) in + let env = + env + |> update_global (fun global -> + { global with mappings = Bindings.add id (mk_item ~loc:(id_loc id) (typq, typ1, typ2)) global.mappings } + ) + |> add_val_spec ~ignore_duplicate:true forwards_id (typq, forwards_typ) + |> add_val_spec ~ignore_duplicate:true backwards_id (typq, backwards_typ) + |> add_val_spec ~ignore_duplicate:true forwards_matches_id (typq, forwards_matches_typ) + |> add_val_spec ~ignore_duplicate:true backwards_matches_id (typq, backwards_matches_typ) + in + let prefix_id = mk_id (string_of_id id ^ "_matches_prefix") in + if unloc_typ typ1 = string_typ then ( + let forwards_prefix_typ = + Typ_aux + ( Typ_fn ([typ1], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)]), + Parse_ast.Unknown + ) + in + add_val_spec ~ignore_duplicate:true prefix_id (typq, forwards_prefix_typ) env + ) + else if unloc_typ typ2 = string_typ then ( + let backwards_prefix_typ = + Typ_aux + ( Typ_fn ([typ2], app_typ (mk_id "option") [A_aux (A_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)]), + Parse_ast.Unknown + ) + in + add_val_spec ~ignore_duplicate:true prefix_id (typq, backwards_prefix_typ) env + ) + else env + +let get_outcome_instantiation env = env.global.outcome_instantiation + +let add_outcome_variable l kid typ env = + update_global + (fun global -> { global with outcome_instantiation = KBindings.add kid (l, typ) global.outcome_instantiation }) + env + +let set_outcome_typschm ~outcome_loc:l (quant, typ) env = + { env with outcome_typschm = Some (quant, typ); toplevel = Some l } + +let get_outcome_typschm_opt env = env.outcome_typschm + +let define_val_spec id env = + if IdSet.mem id env.global.defined_val_specs then + typ_error (id_loc id) ("Function " ^ string_of_id id ^ " has already been declared") + else update_global (fun global -> { global with defined_val_specs = IdSet.add id global.defined_val_specs }) env + +let get_defined_val_specs env = env.global.defined_val_specs + +let is_ctor id (Tu_aux (tu, _)) = + match tu with Tu_ty_id (_, ctor_id) when Id.compare id ctor_id = 0 -> true | _ -> false + +let union_constructor_info id env = + let type_unions = List.map (fun (id, { item = _, tus; _ }) -> (id, tus)) (Bindings.bindings env.global.unions) in + Util.find_map + (fun (union_id, tus) -> + Option.map (fun (n, tu) -> (n, List.length tus, union_id, tu)) (Util.find_index_opt (is_ctor id) tus) + ) + type_unions + +let is_union_constructor id env = + let type_unions = + List.concat (List.map (fun (_, { item = _, tus; _ }) -> tus) (Bindings.bindings env.global.unions)) + in + List.exists (is_ctor id) type_unions + +let is_singleton_union_constructor id env = + let type_unions = List.map (fun (_, { item = _, tus; _ }) -> tus) (Bindings.bindings env.global.unions) in + match List.find (List.exists (is_ctor id)) type_unions with l -> List.length l = 1 | exception Not_found -> false + +let is_mapping id env = Bindings.mem id env.global.mappings + +let add_enum' is_scattered id ids env = + if bound_typ_id env id then already_bound "enum" id env + else ( + typ_print (lazy (adding ^ "enum " ^ string_of_id id)); + update_global + (fun global -> + { + global with + enums = Bindings.add id (mk_item ~loc:(id_loc id) (is_scattered, IdSet.of_list ids)) global.enums; + } + ) + env + ) + +let add_scattered_enum id env = add_enum' true id [] env +let add_enum id ids env = add_enum' false id ids env + +let add_enum_clause id member env = + match Bindings.find_opt id env.global.enums with + | Some ({ item = true, members; _ } as item) -> + if IdSet.mem member members then + typ_error (id_loc id) ("Enumeration " ^ string_of_id id ^ " already has a member " ^ string_of_id member) + else + update_global + (fun global -> + { global with enums = Bindings.add id { item with item = (true, IdSet.add member members) } global.enums } + ) + env + | Some { item = false, _; loc = l } -> + typ_error + (Parse_ast.Hint ("Declared as regular enumeration here", l, id_loc id)) + ("Enumeration " ^ string_of_id id ^ " is not scattered - cannot add a new member with 'enum clause'") + | None -> typ_error (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist") + +let get_enum id env = + match Option.map get_item (Bindings.find_opt id env.global.enums) with + | Some (_, enum) -> IdSet.elements enum + | None -> typ_error (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist") + +let get_enums env = Bindings.map (fun item -> item |> get_item |> snd) env.global.enums + +let is_record id env = Bindings.mem id env.global.records + +let get_record id env = get_item (Bindings.find id env.global.records) + +let get_records env = Bindings.map get_item env.global.records + +let add_record id typq fields env = + let fields = List.map (fun (typ, id) -> (expand_synonyms env typ, id)) fields in + if bound_typ_id env id then already_bound "struct" id env + else ( + typ_print (lazy (adding ^ "struct " ^ string_of_id id)); + let rec record_typ_args = function + | [] -> [] + | QI_aux (QI_id kopt, _) :: qis when is_int_kopt kopt -> + mk_typ_arg (A_nexp (nvar (kopt_kid kopt))) :: record_typ_args qis + | QI_aux (QI_id kopt, _) :: qis when is_typ_kopt kopt -> + mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt)))) :: record_typ_args qis + | _ :: qis -> record_typ_args qis + in + let record_typ = + match record_typ_args (quant_items typq) with [] -> mk_id_typ id | args -> mk_typ (Typ_app (id, args)) + in + let fold_accessors accessors (typ, field) = + let accessor_typ = mk_typ (Typ_fn ([record_typ], typ)) in + typ_print + ( lazy + (indent 1 ^ adding ^ "field accessor " ^ string_of_id id ^ "." ^ string_of_id field ^ " :: " + ^ string_of_bind (typq, accessor_typ) + ) + ); + IdPairMap.add (id, field) (mk_item ~loc:(id_loc field) (typq, accessor_typ)) accessors + in + update_global + (fun global -> + { + global with + records = Bindings.add id (mk_item ~loc:(id_loc id) (typq, fields)) global.records; + accessors = List.fold_left fold_accessors global.accessors fields; + } + ) + env + ) + +let get_accessor_fn record_id field env = + let freshen_bind bind = + List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) + in + try freshen_bind (get_item (IdPairMap.find (record_id, field) env.global.accessors)) + with Not_found -> + typ_error (id_loc field) ("No field accessor found for " ^ string_of_id record_id ^ "." ^ string_of_id field) + +let get_accessor record_id field env = + match get_accessor_fn record_id field env with + (* All accessors should have a single argument (the record itself) *) + | typq, Typ_aux (Typ_fn ([record_typ], field_typ), _) -> (typq, record_typ, field_typ) + | _ -> + typ_error (id_loc field) + ("Field accessor with non-function type found for " ^ string_of_id record_id ^ "." ^ string_of_id field) + +let is_mutable id env = + let to_bool = function Mutable -> true | Immutable -> false in + match Bindings.find_opt id env.locals with Some (mut, _) -> to_bool mut | None -> false + +let string_of_mtyp (mut, typ) = + match mut with Immutable -> string_of_typ typ | Mutable -> "ref<" ^ string_of_typ typ ^ ">" + +let add_local id mtyp env = + if not env.allow_bindings then typ_error (id_loc id) "Bindings are not allowed in this context"; + wf_typ env (snd mtyp); + if Bindings.mem id env.global.val_specs then + typ_error (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name") + else (); + typ_print (lazy (adding ^ "local binding " ^ string_of_id id ^ " : " ^ string_of_mtyp mtyp)); + { env with locals = Bindings.add id mtyp env.locals } + +(* Promote a set of identifiers from local bindings to top-level global letbindings *) +let add_toplevel_lets ids (env : env) = + IdSet.fold + (fun id (env : env) -> + match Bindings.find_opt id env.locals with + | Some (_, typ) -> + let env = { env with locals = Bindings.remove id env.locals } in + update_global + (fun global -> { global with letbinds = Bindings.add id (mk_item ~loc:(id_loc id) typ) global.letbinds }) + env + | None -> env + ) + ids env + +let get_toplevel_lets env = Bindings.bindings env.global.letbinds |> List.map fst |> IdSet.of_list + +let is_variant id env = Bindings.mem id env.global.unions + +let add_variant id (typq, constructors) env = + let constructors = + List.map + (fun (Tu_aux (Tu_ty_id (typ, id), l)) -> Tu_aux (Tu_ty_id (expand_synonyms (add_typquant l typq env) typ, id), l)) + constructors + in + if bound_typ_id env id then already_bound "union" id env + else ( + typ_print (lazy (adding ^ "variant " ^ string_of_id id)); + update_global + (fun global -> + { global with unions = Bindings.add id (mk_item ~loc:(id_loc id) (typq, constructors)) global.unions } + ) + env + ) + +let add_scattered_variant id typq env = + if bound_typ_id env id then already_bound "scattered union" id env + else ( + typ_print (lazy (adding ^ "scattered variant " ^ string_of_id id)); + update_global + (fun global -> + { + global with + unions = Bindings.add id (mk_item ~loc:(id_loc id) (typq, [])) global.unions; + scattered_union_envs = Bindings.add id env.global global.scattered_union_envs; + } + ) + env + ) + +let add_variant_clause id tu env = + match Bindings.find_opt id env.global.unions with + | Some ({ item = typq, tus; _ } as item) -> + update_global + (fun global -> { global with unions = Bindings.add id { item with item = (typq, tus @ [tu]) } global.unions }) + env + | None -> typ_error (id_loc id) ("scattered union " ^ string_of_id id ^ " not found") + +let get_variants env = Bindings.map get_item env.global.unions + +let get_variant id env = + match Option.map get_item (Bindings.find_opt id env.global.unions) with + | Some (typq, tus) -> (typq, tus) + | None -> typ_error (id_loc id) ("union " ^ string_of_id id ^ " not found") + +let get_scattered_variant_env id env = + match Bindings.find_opt id env.global.scattered_union_envs with + | Some global_env -> { env with global = global_env } + | None -> typ_error (id_loc id) ("scattered union " ^ string_of_id id ^ " has not been declared") + +let is_register id env = Bindings.mem id env.global.registers + +let get_register id env = + match Option.map get_item (Bindings.find_opt id env.global.registers) with + | Some typ -> typ + | None -> typ_error (id_loc id) ("No register binding found for " ^ string_of_id id) + +let get_registers env = Bindings.map get_item env.global.registers + +let is_extern id env backend = + try not (Ast_util.extern_assoc backend (Bindings.find_opt id env.global.externs) = None) with Not_found -> false + +let add_extern id ext env = + update_global (fun global -> { global with externs = Bindings.add id ext global.externs }) env + +let get_extern id env backend = + try + match Ast_util.extern_assoc backend (Bindings.find_opt id env.global.externs) with + | Some ext -> ext + | None -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id) + with Not_found -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id) + +let add_register id typ env = + wf_typ env typ; + if Bindings.mem id env.global.registers then + typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound") + else ( + typ_print (lazy (adding ^ "register binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ)); + update_global + (fun global -> { global with registers = Bindings.add id (mk_item ~loc:(id_loc id) typ) global.registers }) + env + ) + +let get_locals env = + Bindings.fold + (fun id { item = typ; _ } locals -> + if not (Bindings.mem id locals) then Bindings.add id (Immutable, typ) locals else locals + ) + env.global.letbinds env.locals + +let lookup_id id env = + match Bindings.find_opt id env.locals with + | Some (mut, typ) -> Local (mut, typ) + | None -> ( + match Bindings.find_opt id env.global.letbinds with + | Some { item = typ; _ } -> Local (Immutable, typ) + | None -> ( + match Bindings.find_opt id env.global.registers with + | Some { item = typ; _ } -> Register typ + | None -> ( + match + List.find_opt (fun (_, { item = _, ctors }) -> IdSet.mem id ctors) (Bindings.bindings env.global.enums) + with + | Some (enum, _) -> Enum (mk_typ (Typ_id enum)) + | None -> Unbound id + ) + ) + ) + +let get_ret_typ env = env.ret_typ + +let add_ret_typ typ env = { env with ret_typ = Some typ } + +let no_bindings env = { env with allow_bindings = false } + +let get_default_order env = + match env.global.default_order with + | None -> typ_error Parse_ast.Unknown "No default order has been set" + | Some ord -> ord + +let get_default_order_opt env = env.global.default_order + +let set_default_order o env = + match o with + | Ord_aux (_, l) -> ( + match env.global.default_order with + | None -> update_global (fun global -> { global with default_order = Some o }) env + | Some _ -> typ_error l "Cannot change default order once already set" + ) + +let base_typ_of env typ = + let rec aux (Typ_aux (t, a)) = + let rewrap t = Typ_aux (t, a) in + match t with + | Typ_fn (arg_typs, ret_typ) -> rewrap (Typ_fn (List.map aux arg_typs, aux ret_typ)) + | Typ_tuple ts -> rewrap (Typ_tuple (List.map aux ts)) + | Typ_app (r, [A_aux (A_typ rtyp, _)]) when string_of_id r = "register" -> aux rtyp + | Typ_app (id, targs) -> rewrap (Typ_app (id, List.map aux_arg targs)) + | t -> rewrap t + and aux_arg (A_aux (targ, a)) = + let rewrap targ = A_aux (targ, a) in + match targ with A_typ typ -> rewrap (A_typ (aux typ)) | targ -> rewrap targ + in + aux (expand_synonyms env typ) + +let is_bitfield id env = Bindings.mem id env.global.bitfields + +let get_bitfield id env = + match Option.map get_item (Bindings.find_opt id env.global.bitfields) with + | Some bitfield -> bitfield + | None -> typ_error (id_loc id) ("Could not find bitfield " ^ string_of_id id) + +let add_bitfield id typ ranges env = + update_global + (fun global -> { global with bitfields = Bindings.add id (mk_item ~loc:(id_loc id) (typ, ranges)) global.bitfields }) + env + +let allow_polymorphic_undefineds env = { env with poly_undefineds = true } + +let polymorphic_undefineds env = env.poly_undefineds + +let is_toplevel env = env.toplevel diff --git a/src/lib/type_env.mli b/src/lib/type_env.mli new file mode 100644 index 000000000..b4ff3fed9 --- /dev/null +++ b/src/lib/type_env.mli @@ -0,0 +1,208 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2021 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(****************************************************************************) + +open Ast +open Ast_util + +(** Linearize cases involving power where we would otherwise require + the SMT solver to use non-linear arithmetic. *) +val opt_smt_linearize : bool ref + +type global_env + +type env + +type t = env + +val freshen_bind : t -> typquant * typ -> typquant * typ + +val get_default_order : t -> order +val get_default_order_opt : t -> order option +val set_default_order : order -> t -> t + +val add_val_spec : ?ignore_duplicate:bool -> id -> typquant * typ -> t -> t +val update_val_spec : id -> typquant * typ -> t -> t +val define_val_spec : id -> t -> t +val get_defined_val_specs : t -> IdSet.t +val get_val_spec : id -> t -> typquant * typ +val get_val_specs : t -> (typquant * typ) Bindings.t +val get_val_spec_orig : id -> t -> typquant * typ + +val add_outcome : id -> typquant * typ * kinded_id list * id list * t -> t -> t +val get_outcome : l -> id -> t -> typquant * typ * kinded_id list * id list * t +val get_outcome_instantiation : t -> (Ast.l * typ) KBindings.t +val add_outcome_variable : l -> kid -> typ -> t -> t +val set_outcome_typschm : outcome_loc:l -> typquant * typ -> t -> t +val get_outcome_typschm_opt : t -> (typquant * typ) option + +val is_variant : id -> t -> bool +val add_variant : id -> typquant * type_union list -> t -> t +val add_scattered_variant : id -> typquant -> t -> t +val add_variant_clause : id -> type_union -> t -> t +val get_variant : id -> t -> typquant * type_union list +val get_variants : t -> (typquant * type_union list) Bindings.t +val get_scattered_variant_env : id -> t -> t +val union_constructor_info : id -> t -> (int * int * id * type_union) option +val is_union_constructor : id -> t -> bool +val is_singleton_union_constructor : id -> t -> bool +val add_union_id : id -> typquant * typ -> t -> t +val get_union_id : id -> t -> typquant * typ + +val is_mapping : id -> t -> bool + +val add_record : id -> typquant -> (typ * id) list -> t -> t +val is_record : id -> t -> bool +val get_record : id -> t -> typquant * (typ * id) list +val get_records : t -> (typquant * (typ * id) list) Bindings.t +val get_accessor_fn : id -> id -> t -> typquant * typ +val get_accessor : id -> id -> t -> typquant * typ * typ + +val add_local : id -> mut * typ -> t -> t +val get_locals : t -> (mut * typ) Bindings.t +val is_mutable : id -> t -> bool + +val add_toplevel_lets : IdSet.t -> t -> t +val get_toplevel_lets : t -> IdSet.t + +val is_register : id -> t -> bool +val get_register : id -> t -> typ +val get_registers : t -> typ Bindings.t +val add_register : id -> typ -> t -> t + +val get_constraints : t -> n_constraint list +val get_constraint_reasons : t -> ((Ast.l * string) option * n_constraint) list +val add_constraint : ?reason:Ast.l * string -> n_constraint -> t -> t + +val add_typquant : l -> typquant -> t -> t + +val get_typ_var : kid -> t -> kind_aux +val get_typ_var_loc_opt : kid -> t -> Ast.l option +val get_typ_vars : t -> kind_aux KBindings.t +val get_typ_var_locs : t -> Ast.l KBindings.t + +val shadows : kid -> t -> int +val add_typ_var_shadow : l -> kinded_id -> t -> t * kid option +val add_typ_var : l -> kinded_id -> t -> t + +val get_ret_typ : t -> typ option +val add_ret_typ : typ -> t -> t + +val add_typ_synonym : id -> typquant -> typ_arg -> t -> t +val get_typ_synonyms : t -> (typquant * typ_arg) Bindings.t + +val bound_typ_id : t -> id -> bool + +val add_overloads : l -> id -> id list -> t -> t +val get_overloads : id -> t -> id list + +val is_extern : id -> t -> string -> bool +val add_extern : id -> extern -> t -> t +val get_extern : id -> t -> string -> string + +val add_enum : id -> id list -> t -> t +val add_scattered_enum : id -> t -> t +val add_enum_clause : id -> id -> t -> t +val get_enum : id -> t -> id list +val get_enums : t -> IdSet.t Bindings.t + +val allow_polymorphic_undefineds : t -> t +val polymorphic_undefineds : t -> bool + +val lookup_id : id -> t -> typ lvar + +val expand_synonyms : t -> typ -> typ +val expand_nexp_synonyms : t -> nexp -> nexp +val expand_constraint_synonyms : t -> n_constraint -> n_constraint + +val base_typ_of : t -> typ -> typ + +val allow_unknowns : t -> bool +val set_allow_unknowns : bool -> t -> t + +val is_bitfield : id -> t -> bool +val add_bitfield : id -> typ -> index_range Bindings.t -> t -> t +val get_bitfield : id -> t -> typ * index_range Bindings.t + +val no_bindings : t -> t + +val is_toplevel : t -> l option + +(* Well formedness-checks *) +val wf_typ : t -> typ -> unit +val wf_constraint : ?exs:KidSet.t -> t -> n_constraint -> unit + +(** Some of the code in the environment needs to use the smt solver, + which is defined below. To break the circularity this would cause + (as the prove code depends on the environment), we add a reference + to the prover to the initial environment. *) +val set_prover : (t -> n_constraint -> bool) option -> t -> t + +(** This should not be used outside the type checker, as initial_env + sets up a correct initial environment. *) +val empty : t + +val builtin_typs : typquant Bindings.t diff --git a/src/lib/type_error.ml b/src/lib/type_error.ml index cc282e074..a9d77da99 100644 --- a/src/lib/type_error.ml +++ b/src/lib/type_error.ml @@ -71,6 +71,8 @@ open Ast_defs open Ast_util open Type_check +include Type_internal + let opt_explain_all_variables = ref false let opt_explain_constraints = ref false diff --git a/src/lib/type_error.mli b/src/lib/type_error.mli index 5baeacb7d..a12f3e167 100644 --- a/src/lib/type_error.mli +++ b/src/lib/type_error.mli @@ -81,15 +81,19 @@ val opt_explain_all_variables : bool ref into detail about how they were derived *) val opt_explain_constraints : bool ref +type type_error + +exception Type_error of Parse_ast.l * type_error + type suggestion = Suggest_add_constraint of Ast.n_constraint | Suggest_none (** Analyze an unresolved quantifier type error *) val analyze_unresolved_quant : (Ast_util.mut * Ast.typ) Ast_util.Bindings.t -> Ast.n_constraint list -> Ast.quant_item -> suggestion -val collapse_errors : Type_check.type_error -> Type_check.type_error +val collapse_errors : type_error -> type_error -val string_of_type_error : Type_check.type_error -> string +val string_of_type_error : type_error -> string val check_defs : Type_check.Env.t -> uannot Ast.def list -> Type_check.tannot Ast.def list * Type_check.Env.t diff --git a/src/lib/type_internal.ml b/src/lib/type_internal.ml new file mode 100644 index 000000000..1bca68fa2 --- /dev/null +++ b/src/lib/type_internal.ml @@ -0,0 +1,304 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2021 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(****************************************************************************) + +(* Note: Everything useful in this module is re-exported by other + Type_ modules that implement the type system, so this module should + not be imported elsewhere. *) + +open Ast +open Ast_util +open Util + +module Big_int = Nat_big_num + +(* opt_tc_debug controls the verbosity of the type checker. 0 is + silent, 1 prints a tree of the type derivation and 2 is like 1 but + with much more debug information. *) +let opt_tc_debug = ref 0 + +let depth = ref 0 + +let rec indent n = match n with 0 -> "" | n -> "| " ^ indent (n - 1) + +(* Lazily evaluate debugging message. This can make a big performance + difference; for example, repeated calls to string_of_exp can be costly for + deeply nested expressions, e.g. with long sequences of monadic binds. *) +let typ_debug ?(level = 1) m = if !opt_tc_debug > level then prerr_endline (indent !depth ^ Lazy.force m) else () + +let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ Lazy.force m) else () + +let adding = Util.("Adding " |> darkgray |> clear) + +type constraint_reason = (Ast.l * string) option + +type type_error = + (* First parameter is the error that caused us to start doing type + coercions, the second is the errors encountered by all possible + coercions *) + | Err_no_casts of uannot exp * typ * typ * type_error * type_error list + | Err_no_overloading of id * (id * type_error) list + | Err_unresolved_quants of id * quant_item list * (mut * typ) Bindings.t * n_constraint list + | Err_failed_constraint of n_constraint * (mut * typ) Bindings.t * n_constraint list + | Err_subtype of typ * typ * n_constraint option * (constraint_reason * n_constraint) list * Ast.l KBindings.t + | Err_no_num_ident of id + | Err_other of string + | Err_inner of type_error * Parse_ast.l * string * string option * type_error + +let err_because (error1, l, error2) = Err_inner (error1, l, "Caused by", None, error2) + +exception Type_error of l * type_error + +let typ_error l m = raise (Type_error (l, Err_other m)) + +let typ_raise l err = raise (Type_error (l, err)) + +let string_of_bind (typquant, typ) = string_of_typquant typquant ^ ". " ^ string_of_typ typ + +(* unloc_X functions remove location information from AST nodes, so we can use structural equality *) + +let rec unloc_id = function + | Id_aux (Id x, _) -> Id_aux (Id x, Parse_ast.Unknown) + | Id_aux (Operator x, _) -> Id_aux (Operator x, Parse_ast.Unknown) + +and unloc_kid = function Kid_aux (Var x, _) -> Kid_aux (Var x, Parse_ast.Unknown) + +and unloc_nexp_aux = function + | Nexp_id id -> Nexp_id (unloc_id id) + | Nexp_var kid -> Nexp_var (unloc_kid kid) + | Nexp_constant n -> Nexp_constant n + | Nexp_app (id, nexps) -> Nexp_app (id, List.map unloc_nexp nexps) + | Nexp_times (nexp1, nexp2) -> Nexp_times (unloc_nexp nexp1, unloc_nexp nexp2) + | Nexp_sum (nexp1, nexp2) -> Nexp_sum (unloc_nexp nexp1, unloc_nexp nexp2) + | Nexp_minus (nexp1, nexp2) -> Nexp_minus (unloc_nexp nexp1, unloc_nexp nexp2) + | Nexp_exp nexp -> Nexp_exp (unloc_nexp nexp) + | Nexp_neg nexp -> Nexp_neg (unloc_nexp nexp) + +and unloc_nexp = function Nexp_aux (nexp_aux, _) -> Nexp_aux (unloc_nexp_aux nexp_aux, Parse_ast.Unknown) + +and unloc_n_constraint_aux = function + | NC_equal (nexp1, nexp2) -> NC_equal (unloc_nexp nexp1, unloc_nexp nexp2) + | NC_bounded_ge (nexp1, nexp2) -> NC_bounded_ge (unloc_nexp nexp1, unloc_nexp nexp2) + | NC_bounded_gt (nexp1, nexp2) -> NC_bounded_gt (unloc_nexp nexp1, unloc_nexp nexp2) + | NC_bounded_le (nexp1, nexp2) -> NC_bounded_le (unloc_nexp nexp1, unloc_nexp nexp2) + | NC_bounded_lt (nexp1, nexp2) -> NC_bounded_lt (unloc_nexp nexp1, unloc_nexp nexp2) + | NC_not_equal (nexp1, nexp2) -> NC_not_equal (unloc_nexp nexp1, unloc_nexp nexp2) + | NC_set (kid, nums) -> NC_set (unloc_kid kid, nums) + | NC_or (nc1, nc2) -> NC_or (unloc_n_constraint nc1, unloc_n_constraint nc2) + | NC_and (nc1, nc2) -> NC_and (unloc_n_constraint nc1, unloc_n_constraint nc2) + | NC_var kid -> NC_var (unloc_kid kid) + | NC_app (id, args) -> NC_app (unloc_id id, List.map unloc_typ_arg args) + | NC_true -> NC_true + | NC_false -> NC_false + +and unloc_n_constraint = function NC_aux (nc_aux, _) -> NC_aux (unloc_n_constraint_aux nc_aux, Parse_ast.Unknown) + +and unloc_typ_arg = function A_aux (typ_arg_aux, _) -> A_aux (unloc_typ_arg_aux typ_arg_aux, Parse_ast.Unknown) + +and unloc_typ_arg_aux = function + | A_nexp nexp -> A_nexp (unloc_nexp nexp) + | A_typ typ -> A_typ (unloc_typ typ) + | A_bool nc -> A_bool (unloc_n_constraint nc) + +and unloc_typ_aux : typ_aux -> typ_aux = function + | Typ_internal_unknown -> Typ_internal_unknown + | Typ_id id -> Typ_id (unloc_id id) + | Typ_var kid -> Typ_var (unloc_kid kid) + | Typ_fn (arg_typs, ret_typ) -> Typ_fn (List.map unloc_typ arg_typs, unloc_typ ret_typ) + | Typ_bidir (typ1, typ2) -> Typ_bidir (unloc_typ typ1, unloc_typ typ2) + | Typ_tuple typs -> Typ_tuple (List.map unloc_typ typs) + | Typ_exist (kopts, constr, typ) -> + Typ_exist (List.map unloc_kinded_id kopts, unloc_n_constraint constr, unloc_typ typ) + | Typ_app (id, args) -> Typ_app (unloc_id id, List.map unloc_typ_arg args) + +and unloc_typ : typ -> typ = function Typ_aux (typ_aux, _) -> Typ_aux (unloc_typ_aux typ_aux, Parse_ast.Unknown) + +and unloc_typq = function TypQ_aux (typq_aux, _) -> TypQ_aux (unloc_typq_aux typq_aux, Parse_ast.Unknown) + +and unloc_typq_aux = function + | TypQ_no_forall -> TypQ_no_forall + | TypQ_tq quants -> TypQ_tq (List.map unloc_quant_item quants) + +and unloc_quant_item = function QI_aux (qi_aux, _) -> QI_aux (unloc_qi_aux qi_aux, Parse_ast.Unknown) + +and unloc_qi_aux = function + | QI_id kinded_id -> QI_id (unloc_kinded_id kinded_id) + | QI_constraint constr -> QI_constraint (unloc_n_constraint constr) + +and unloc_kinded_id = function + | KOpt_aux (kinded_id_aux, _) -> KOpt_aux (unloc_kinded_id_aux kinded_id_aux, Parse_ast.Unknown) + +and unloc_kinded_id_aux = function KOpt_kind (kind, kid) -> KOpt_kind (unloc_kind kind, unloc_kid kid) + +and unloc_kind = function K_aux (k_aux, _) -> K_aux (k_aux, Parse_ast.Unknown) + +let rec typ_nexps (Typ_aux (typ_aux, _)) = + match typ_aux with + | Typ_internal_unknown -> [] + | Typ_id _ -> [] + | Typ_var _ -> [] + | Typ_tuple typs -> List.concat (List.map typ_nexps typs) + | Typ_app (_, args) -> List.concat (List.map typ_arg_nexps args) + | Typ_exist (_, _, typ) -> typ_nexps typ + | Typ_fn (arg_typs, ret_typ) -> List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ + | Typ_bidir (typ1, typ2) -> typ_nexps typ1 @ typ_nexps typ2 + +and typ_arg_nexps (A_aux (typ_arg_aux, _)) = + match typ_arg_aux with A_nexp n -> [n] | A_typ typ -> typ_nexps typ | A_bool nc -> constraint_nexps nc + +and constraint_nexps (NC_aux (nc_aux, _)) = + match nc_aux with + | NC_equal (n1, n2) + | NC_bounded_ge (n1, n2) + | NC_bounded_le (n1, n2) + | NC_bounded_gt (n1, n2) + | NC_bounded_lt (n1, n2) + | NC_not_equal (n1, n2) -> + [n1; n2] + | NC_set _ | NC_true | NC_false | NC_var _ -> [] + | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> constraint_nexps nc1 @ constraint_nexps nc2 + | NC_app (_, args) -> List.concat (List.map typ_arg_nexps args) + +(* Return a KidSet containing all the type variables appearing in + nexp, where nexp occurs underneath a Nexp_exp, i.e. 2^nexp *) +let rec nexp_power_variables (Nexp_aux (aux, _)) = + match aux with + | Nexp_times (n1, n2) | Nexp_sum (n1, n2) | Nexp_minus (n1, n2) -> + KidSet.union (nexp_power_variables n1) (nexp_power_variables n2) + | Nexp_neg n -> nexp_power_variables n + | Nexp_id _ | Nexp_var _ | Nexp_constant _ -> KidSet.empty + | Nexp_app (_, ns) -> List.fold_left KidSet.union KidSet.empty (List.map nexp_power_variables ns) + | Nexp_exp n -> tyvars_of_nexp n + +let constraint_power_variables nc = + List.fold_left KidSet.union KidSet.empty (List.map nexp_power_variables (constraint_nexps nc)) + +let ex_counter = ref 0 + +let fresh_existential l k = + let fresh = Kid_aux (Var ("'ex" ^ string_of_int !ex_counter ^ "#"), l) in + incr ex_counter; + mk_kopt ~loc:l k fresh + +let named_existential l k = function Some n -> mk_kopt ~loc:l k (mk_kid n) | None -> fresh_existential l k + +let destruct_exist_plain ?(name = None) typ = + match typ with + | Typ_aux (Typ_exist ([kopt], nc, typ), l) -> + let kid, fresh = (kopt_kid kopt, named_existential l (unaux_kind (kopt_kind kopt)) name) in + let nc = constraint_subst kid (arg_kopt fresh) nc in + let typ = typ_subst kid (arg_kopt fresh) typ in + Some ([fresh], nc, typ) + | Typ_aux (Typ_exist (kopts, nc, typ), _) -> + let add_num i = match name with Some n -> Some (n ^ string_of_int i) | None -> None in + let fresh_kopts = + List.mapi + (fun i kopt -> (kopt_kid kopt, named_existential (kopt_loc kopt) (unaux_kind (kopt_kind kopt)) (add_num i))) + kopts + in + let nc = List.fold_left (fun nc (kid, fresh) -> constraint_subst kid (arg_kopt fresh) nc) nc fresh_kopts in + let typ = List.fold_left (fun typ (kid, fresh) -> typ_subst kid (arg_kopt fresh) typ) typ fresh_kopts in + Some (List.map snd fresh_kopts, nc, typ) + | _ -> None + +(** Destructure and canonicalise a numeric type into a list of type + variables, a constraint on those type variables, and an + N-expression that represents that numeric type in the + environment. For example: + - {'n, 'n <= 10. atom('n)} => ['n], 'n <= 10, 'n + - int => ['n], true, 'n (where x is fresh) + - atom('n) => [], true, 'n +**) +let destruct_numeric ?(name = None) typ = + match (destruct_exist_plain ~name typ, typ) with + | Some (kids, nc, Typ_aux (Typ_app (id, [A_aux (A_nexp nexp, _)]), _)), _ when string_of_id id = "atom" -> + Some (List.map kopt_kid kids, nc, nexp) + | None, Typ_aux (Typ_app (id, [A_aux (A_nexp nexp, _)]), _) when string_of_id id = "atom" -> Some ([], nc_true, nexp) + | None, Typ_aux (Typ_app (id, [A_aux (A_nexp lo, _); A_aux (A_nexp hi, _)]), l) when string_of_id id = "range" -> + let kid = kopt_kid (named_existential l K_int name) in + Some ([kid], nc_and (nc_lteq lo (nvar kid)) (nc_lteq (nvar kid) hi), nvar kid) + | None, Typ_aux (Typ_id id, l) when string_of_id id = "nat" -> + let kid = kopt_kid (named_existential l K_int name) in + Some ([kid], nc_lteq (nint 0) (nvar kid), nvar kid) + | None, Typ_aux (Typ_id id, l) when string_of_id id = "int" -> + let kid = kopt_kid (named_existential l K_int name) in + Some ([kid], nc_true, nvar kid) + | _, _ -> None + +let destruct_boolean ?name:(_ = None) = function + | Typ_aux (Typ_id (Id_aux (Id "bool", _)), l) -> + let kid = kopt_kid (fresh_existential l K_bool) in + Some (kid, nc_var kid) + | _ -> None + +let destruct_exist ?(name = None) typ = + match destruct_numeric ~name typ with + | Some (kids, nc, nexp) -> Some (List.map (mk_kopt K_int) kids, nc, atom_typ nexp) + | None -> ( + match destruct_boolean ~name typ with + | Some (kid, nc) -> Some ([mk_kopt K_bool kid], nc_true, atom_bool_typ nc) + | None -> destruct_exist_plain ~name typ + ) diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index e7faf815b..a2d92fcac 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -2107,7 +2107,7 @@ let compile_ast env effect_info output_chan c_includes ast = ^^ model_main ^^ hardline ^^ end_extern_cpp ^^ hardline ) |> output_string output_chan - with Type_error (l, err) -> + with Type_error.Type_error (l, err) -> c_error ~loc:l ("Unexpected type error when compiling to C:\n" ^ Type_error.string_of_type_error err) let compile_ast_clib env effect_info ast codegen = diff --git a/src/sail_coq_backend/pretty_print_coq.ml b/src/sail_coq_backend/pretty_print_coq.ml index 692b68329..6c0b5950a 100644 --- a/src/sail_coq_backend/pretty_print_coq.ml +++ b/src/sail_coq_backend/pretty_print_coq.ml @@ -3477,7 +3477,7 @@ let pp_ast_coq (types_file, types_modules) (defs_file, defs_modules) type_defs_m hardline; ] ) - with Type_check.Type_error (l, err) -> + with Type_error.Type_error (l, err) -> let extra = "\nError during Coq printing\n" ^ if Printexc.backtrace_status () then "\n" ^ Printexc.get_backtrace () else "(backtracing unavailable)" diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index e1acf3997..8ab062de8 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -2356,4 +2356,4 @@ let generate_smt props name_file env effect_info ast = try let cdefs, _, ctx = compile env effect_info ast in smt_cdefs props [] name_file ctx cdefs cdefs - with Type_check.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) + with Type_error.Type_error (l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err))