From 8efe97cd6d8140ebebf4d71e597f497dea385964 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 4 Mar 2019 15:48:09 +0000 Subject: Do not store type synonyms as functions in the environment --- src/sail.ml | 2 +- src/type_check.ml | 112 ++++++++++++------------- test/typecheck/pass/Replicate/v2.expect | 2 +- test/typecheck/pass/exist_synonym/v3.expect | 7 +- test/typecheck/pass/exist_synonym/v4.expect | 7 +- test/typecheck/pass/existential_ast/v3.expect | 2 +- test/typecheck/pass/existential_ast3/v1.expect | 8 +- test/typecheck/pass/existential_ast3/v2.expect | 8 +- test/typecheck/pass/existential_ast3/v3.expect | 2 +- test/typecheck/pass/if_infer/v1.expect | 4 +- test/typecheck/pass/if_infer/v2.expect | 4 +- 11 files changed, 81 insertions(+), 77 deletions(-) diff --git a/src/sail.ml b/src/sail.ml index 949663d4..2a15f26e 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -467,7 +467,7 @@ let main() = if !opt_memo_z3 then Constraint.save_digests () else () end -let _ = try +let _ = try begin try ignore (main ()) with Failure s -> raise (Reporting.err_general Parse_ast.Unknown ("Failure " ^ s)) diff --git a/src/type_check.ml b/src/type_check.ml index 5bc3cc2d..c1689a82 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -112,7 +112,7 @@ type env = mappings : (typquant * typ * typ) Bindings.t; typ_vars : (Ast.l * kind_aux) KBindings.t; shadow_vars : int KBindings.t; - typ_synonyms : (Ast.l -> env -> typ_arg list -> typ_arg) Bindings.t; + typ_synonyms : (typquant * typ_arg) Bindings.t; overloads : (id list) Bindings.t; flow : (typ -> typ) Bindings.t; enums : IdSet.t Bindings.t; @@ -435,7 +435,7 @@ module Env : sig 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 -> (Ast.l -> t -> typ_arg list -> typ_arg) -> t -> t + val add_typ_synonym : id -> typquant -> typ_arg -> t -> t val get_typ_synonym : id -> t -> Ast.l -> t -> typ_arg list -> typ_arg val add_overloads : id -> id list -> t -> t val get_overloads : id -> t -> id list @@ -614,6 +614,53 @@ end = struct then () else typ_error env (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id) + let add_typ_synonym id typq arg env = + if Bindings.mem id env.typ_synonyms then + typ_error env (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists") + else + begin + typ_print (lazy (adding ^ "type synonym " ^ string_of_id id)); + { env with typ_synonyms = Bindings.add id (typq, arg) env.typ_synonyms } + end + + let mk_synonym typq typ_arg = + let kopts, ncs = quant_split typq in + let kopts = List.map (fun kopt -> kopt, fresh_existential (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_order arg, _) :: args when is_order_kopt kopt -> + let typ_arg, ncs = subst_args env l kopts args in + typ_arg_subst (kopt_kid kopt) (arg_order 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 env l "Synonym applied to bad arguments" + in + fun l env args -> + let typ_arg, ncs = subst_args env l kopts args in + if List.for_all (env.prove env) ncs + then typ_arg + else typ_error env 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 env.constraints) + + let get_typ_synonym id env = + begin match Bindings.find_opt id env.typ_synonyms with + | Some (typq, arg) -> mk_synonym typq arg + | None -> raise Not_found + end + let rec expand_constraint_synonyms env (NC_aux (aux, l) as nc) = typ_debug ~level:2 (lazy ("Expanding " ^ string_of_n_constraint nc)); match aux with @@ -625,7 +672,7 @@ end = struct | NC_bounded_ge (n1, n2) -> NC_aux (NC_bounded_ge (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l) | NC_app (id, args) -> (try - begin match Bindings.find id env.typ_synonyms l env args with + begin match get_typ_synonym id env l env args with | A_aux (A_bool nc, _) -> expand_constraint_synonyms env nc | arg -> typ_error env l ("Expected Bool when expanding synonym " ^ string_of_id id ^ " got " ^ string_of_typ_arg arg) end @@ -637,7 +684,7 @@ end = struct match aux with | Nexp_app (id, args) -> (try - begin match Bindings.find id env.typ_synonyms l env [] with + begin match get_typ_synonym id env l env [] with | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp | _ -> typ_error env l ("Expected Int when expanding synonym " ^ string_of_id id) end @@ -645,7 +692,7 @@ end = struct | Not_found -> Nexp_aux (Nexp_app (id, List.map (expand_nexp_synonyms env) args), l)) | Nexp_id id -> (try - begin match Bindings.find id env.typ_synonyms l env [] with + begin match get_typ_synonym id env l env [] with | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp | _ -> typ_error env l ("Expected Int when expanding synonym " ^ string_of_id id) end @@ -666,7 +713,7 @@ end = struct | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2), l) | Typ_app (id, args) -> (try - begin match Bindings.find id env.typ_synonyms l env args with + begin match get_typ_synonym id env l env args with | A_aux (A_typ typ, _) -> expand_synonyms env typ | _ -> typ_error env l ("Expected Type when expanding synonym " ^ string_of_id id) end @@ -674,7 +721,7 @@ end = struct | Not_found -> Typ_aux (Typ_app (id, List.map (expand_synonyms_arg env) args), l)) | Typ_id id -> (try - begin match Bindings.find id env.typ_synonyms l env [] with + begin match get_typ_synonym id env l env [] with | A_aux (A_typ typ, _) -> expand_synonyms env typ | _ -> typ_error env l ("Expected Type when expanding synonym " ^ string_of_id id) end @@ -1227,17 +1274,6 @@ end = struct typ_print (lazy (adding ^ "cast " ^ string_of_id cast)); { env with casts = cast :: env.casts } - let add_typ_synonym id synonym env = - if Bindings.mem id env.typ_synonyms - then typ_error env (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists") - else - begin - typ_print (lazy (adding ^ "type synonym " ^ string_of_id id)); - { env with typ_synonyms = Bindings.add id synonym env.typ_synonyms } - end - - let get_typ_synonym id env = Bindings.find id env.typ_synonyms - let get_default_order env = match env.default_order with | None -> typ_error env Parse_ast.Unknown ("No default order has been set") @@ -4872,44 +4908,13 @@ let check_type_union env variant typq (Tu_aux (tu, l)) = |> Env.add_val_spec v (typq, typ') (* FIXME: This code is duplicated with general kind-checking code in environment, can they be merged? *) -let mk_synonym typq typ_arg = - let kopts, ncs = quant_split typq in - let kopts = List.map (fun kopt -> kopt, fresh_existential (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_order arg, _) :: args when is_order_kopt kopt -> - let typ_arg, ncs = subst_args env l kopts args in - typ_arg_subst (kopt_kid kopt) (arg_order 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 env l "Synonym applied to bad arguments" - in - fun l env args -> - let typ_arg, ncs = subst_args env l kopts args in - if List.for_all (prove __POS__ env) ncs - then typ_arg - else typ_error env Parse_ast.Unknown ("Could not prove constraints " ^ string_of_list ", " string_of_n_constraint ncs - ^ " in type synonym " ^ string_of_typ_arg typ_arg - ^ " with " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)) let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t = fun env (TD_aux (tdef, (l, _))) -> let td_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Typedef") in match tdef with | TD_abbrev (id, typq, typ_arg) -> - [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ_arg) env + [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id typq typ_arg env | TD_record (id, typq, fields, _) -> [DEF_type (TD_aux (tdef, (l, None)))], Env.add_record id typq fields env | TD_variant (id, typq, arms, _) -> @@ -5018,13 +5023,6 @@ and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list let initial_env = Env.empty |> Env.add_prover (prove __POS__) - (* |> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args))) *) - - (* Internal functions for Monomorphise.AtomToItself *) - - (* |> Env.add_val_spec (mk_id "int") - * (TypQ_aux (TypQ_no_forall, Parse_ast.Unknown), Typ_aux (Typ_bidir (int_typ, string_typ), Parse_ast.Unknown)) *) - |> Env.add_extern (mk_id "size_itself_int") (fun _ -> Some "size_itself_int") |> Env.add_val_spec (mk_id "size_itself_int") (TypQ_aux (TypQ_tq [QI_aux (QI_id (mk_kopt K_int (mk_kid "n")), diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index 6ca2fc40..62992f2c 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -2,7 +2,7 @@ Type error: [Replicate/v2.sail]:10:4-30 10 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Tried performing type coercion from {('ex41# : Int), true. vector(('M * 'ex41#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x))) +  | Tried performing type coercion from {('ex80# : Int), true. vector(('M * 'ex80#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect index c237ae2d..d63918b4 100644 --- a/test/typecheck/pass/exist_synonym/v3.expect +++ b/test/typecheck/pass/exist_synonym/v3.expect @@ -1,3 +1,6 @@ Type error: -Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) - +[exist_synonym/v3.sail]:9:38-47 +9 |val test : forall 'n, 0 <= 'n <= 100. regno('n) -> unit +  | ^-------^ +  | Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) +  | diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect index abb232cb..8157c64f 100644 --- a/test/typecheck/pass/exist_synonym/v4.expect +++ b/test/typecheck/pass/exist_synonym/v4.expect @@ -1,3 +1,6 @@ Type error: -Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) - +[exist_synonym/v4.sail]:9:35-44 +9 |val test : forall 'n, 0 <= 2 <= 4. regno('n) -> unit +  | ^-------^ +  | Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8) +  | diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index 1b6239bb..af2cf65f 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/test/typecheck/pass/existential_ast/v3.expect @@ -3,5 +3,5 @@ Type error: 26 | Some(Ctor1(a, x, c))  | ^------------^  | Could not resolve quantifiers for Ctor1 -  | * datasize('ex59#) +  | * datasize('ex157#)  | diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect index a1975425..e904aa61 100644 --- a/test/typecheck/pass/existential_ast3/v1.expect +++ b/test/typecheck/pass/existential_ast3/v1.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))  | Coercion failed because: -  | (int(33), int('ex62#)) is not a subtype of (int('ex57#), int('ex58#)) +  | (int(33), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#))  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex57# bound here +  |  | 'ex114# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex58# bound here +  |  | 'ex115# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex62# bound here +  |  | 'ex119# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect index 1ac6c87c..fdd13607 100644 --- a/test/typecheck/pass/existential_ast3/v2.expect +++ b/test/typecheck/pass/existential_ast3/v2.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))  | Coercion failed because: -  | (int(31), int('ex62#)) is not a subtype of (int('ex57#), int('ex58#)) +  | (int(31), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#))  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex57# bound here +  |  | 'ex114# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex58# bound here +  |  | 'ex115# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex62# bound here +  |  | 'ex119# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect index 05dcd0a1..2432e632 100644 --- a/test/typecheck/pass/existential_ast3/v3.expect +++ b/test/typecheck/pass/existential_ast3/v3.expect @@ -3,5 +3,5 @@ Type error: 25 | Some(Ctor(64, unsigned(0b0 @ b @ a)))  | ^-----------------------------^  | Could not resolve quantifiers for Ctor -  | * (datasize(64) & (0 <= 'ex78# & ('ex78# + 1) <= 64)) +  | * (datasize(64) & (0 <= 'ex158# & ('ex158# + 1) <= 64))  | diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index c3b453f2..a63f28f1 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex39# & ('ex39# + 1) <= 3) +  | * (0 <= 'ex76# & ('ex76# + 1) <= 3)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex42# & ('ex42# + 1) <= 3) +  | * (0 <= 'ex79# & ('ex79# + 1) <= 3)  | diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index ba2ad410..f37d215f 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex39# & ('ex39# + 1) <= 4) +  | * (0 <= 'ex76# & ('ex76# + 1) <= 4)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex42# & ('ex42# + 1) <= 4) +  | * (0 <= 'ex79# & ('ex79# + 1) <= 4)  | -- cgit v1.2.3