From 945c8b10a9498d0606f4226bc18d03ef806184f2 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 4 Dec 2018 13:42:01 +0000 Subject: Simplify kinds in the AST Rather than having K_aux (K_kind [BK_aux (BK_int, _)], _) represent the Int kind, we now just have K_aux (K_int, _). Since the language is first order we have no need for fancy kinds in the AST. --- language/sail.ott | 10 +---- src/ast_util.ml | 24 ++++++------ src/ast_util.mli | 5 +-- src/initial_check.ml | 34 ++++++----------- src/monomorphise.ml | 12 +++--- src/parse_ast.ml | 30 +++++---------- src/parser.mly | 19 ++++------ src/pretty_print_coq.ml | 8 ++-- src/return_analysis.ml | 2 +- src/rewrites.ml | 4 +- src/specialize.ml | 4 +- src/type_check.ml | 98 +++++++++++++++++++++++-------------------------- src/type_check.mli | 6 +-- 13 files changed, 106 insertions(+), 150 deletions(-) diff --git a/language/sail.ott b/language/sail.ott index 2875c951..4ce08415 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -1,4 +1,4 @@ -%% +% %% Grammar for user language. Generates ./src/ast.ml %% @@ -169,19 +169,13 @@ kid :: '' ::= grammar -base_kind :: 'BK_' ::= +kind :: 'K_' ::= {{ com base kind}} {{ aux _ l }} | Type :: :: type {{ com kind of types }} | Int :: :: int {{ com kind of natural number size expressions }} | Order :: :: order {{ com kind of vector order specifications }} -kind :: 'K_' ::= - {{ com kinds}} - {{ aux _ l }} - | base_kind1 -> ... -> base_kindn :: :: kind -% we'll never use ...-> Nat , .. Order , .. or Effects - nexp :: 'Nexp_' ::= {{ com numeric expression, of kind Int }} {{ aux _ l }} diff --git a/src/ast_util.ml b/src/ast_util.ml index 14638b88..ffe4c90e 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -106,13 +106,13 @@ let mk_funcl id pat body = FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, body), let mk_qi_nc nc = QI_aux (QI_const nc, Parse_ast.Unknown) -let mk_qi_id bk kid = +let mk_qi_id k kid = let kopt = - KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (bk, Parse_ast.Unknown)], Parse_ast.Unknown), kid), Parse_ast.Unknown) + KOpt_aux (KOpt_kind (K_aux (k, Parse_ast.Unknown), kid), Parse_ast.Unknown) in QI_aux (QI_id kopt, Parse_ast.Unknown) -let mk_qi_kopt kopt =QI_aux (QI_id kopt, Parse_ast.Unknown) +let mk_qi_kopt kopt = QI_aux (QI_id kopt, Parse_ast.Unknown) let mk_fundef funcls = let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in @@ -131,16 +131,16 @@ let kopt_kid (KOpt_aux (kopt_aux, _)) = | KOpt_none kid | KOpt_kind (_, kid) -> kid let is_nat_kopt = function - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_int, _)], _), _), _) -> true + | KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> true | KOpt_aux (KOpt_none _, _) -> true | _ -> false let is_order_kopt = function - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), _), _) -> true + | KOpt_aux (KOpt_kind (K_aux (K_order, _), _), _) -> true | _ -> false let is_typ_kopt = function - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), _), _) -> true + | KOpt_aux (KOpt_kind (K_aux (K_type, _), _), _) -> true | _ -> false let string_of_kid = function @@ -625,14 +625,12 @@ let string_of_base_effect_aux = function (*| BE_lset -> "lset" | BE_lret -> "lret"*) -let string_of_base_kind_aux = function - | BK_type -> "Type" - | BK_int -> "Int" - | BK_order -> "Order" +let string_of_kind_aux = function + | K_type -> "Type" + | K_int -> "Int" + | K_order -> "Order" -let string_of_base_kind (BK_aux (bk, _)) = string_of_base_kind_aux bk - -let string_of_kind (K_aux (K_kind bks, _)) = string_of_list " -> " string_of_base_kind bks +let string_of_kind (K_aux (k, _)) = string_of_kind_aux k let string_of_base_effect = function | BE_aux (beff, _) -> string_of_base_effect_aux beff diff --git a/src/ast_util.mli b/src/ast_util.mli index 8f555744..b7979e88 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -85,7 +85,7 @@ val mk_fundef : (unit funcl) list -> unit def val mk_val_spec : val_spec_aux -> unit def val mk_typschm : typquant -> typ -> typschm val mk_typquant : quant_item list -> typquant -val mk_qi_id : base_kind_aux -> kid -> quant_item +val mk_qi_id : kind_aux -> kid -> quant_item val mk_qi_nc : n_constraint -> quant_item val mk_qi_kopt : kinded_id -> quant_item val mk_fexp : id -> unit exp -> unit fexp @@ -207,8 +207,7 @@ val def_loc : 'a def -> Parse_ast.l val string_of_id : id -> string val string_of_kid : kid -> string val string_of_base_effect_aux : base_effect_aux -> string -val string_of_base_kind_aux : base_kind_aux -> string -val string_of_base_kind : base_kind -> string +val string_of_kind_aux : kind_aux -> string val string_of_kind : kind -> string val string_of_base_effect : base_effect -> string val string_of_effect : effect -> string diff --git a/src/initial_check.ml b/src/initial_check.ml index b442ae97..d1efb374 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -149,23 +149,11 @@ let to_ast_id (Parse_ast.Id_aux(id, l)) = let to_ast_var (Parse_ast.Kid_aux(Parse_ast.Var v,l)) = Kid_aux(Var v,l) -let to_ast_base_kind (Parse_ast.BK_aux(k,l')) = +let to_ast_kind (Parse_ast.K_aux(k,l')) = match k with - | Parse_ast.BK_type -> BK_aux(BK_type,l'), { k = K_Typ} - | Parse_ast.BK_int -> BK_aux(BK_int,l'), { k = K_Nat } - | Parse_ast.BK_order -> BK_aux(BK_order,l'), { k = K_Ord } - -let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),l)) : (Ast.kind * kind) = - match klst with - | [] -> raise (Reporting.err_unreachable l __POS__ "Kind with empty kindlist encountered") - | [k] -> let k_ast,k_typ = to_ast_base_kind k in - K_aux(K_kind([k_ast]),l), k_typ - | ks -> let k_pairs = List.map to_ast_base_kind ks in - let reverse_typs = List.rev (List.map snd k_pairs) in - let ret,args = List.hd reverse_typs, List.rev (List.tl reverse_typs) in - match ret.k with - | K_Typ -> K_aux(K_kind(List.map fst k_pairs), l), { k = K_Lam(args,ret) } - | _ -> typ_error l "Type constructor must have an -> kind ending in Type" None None None + | Parse_ast.K_type -> K_aux(K_type,l'), { k = K_Typ} + | Parse_ast.K_int -> K_aux(K_int,l'), { k = K_Nat } + | Parse_ast.K_order -> K_aux(K_order,l'), { k = K_Ord } let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) : Ast.typ = (* let _ = Printf.eprintf "to_ast_typ\n" in*) @@ -392,7 +380,7 @@ let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant | Parse_ast.KOpt_kind(k,v) -> let v = to_ast_var v in let key = var_to_string v in - let kind,ktyp = to_ast_kind k_env k in + let kind,ktyp = to_ast_kind k in v,key,Some(kind),Some(ktyp) in if (Nameset.mem key local_names) @@ -639,13 +627,13 @@ and to_ast_record_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp let to_ast_default (names, k_env, default_order) (default : Parse_ast.default_typing_spec) : default_spec envs_out = match default with - | Parse_ast.DT_aux(Parse_ast.DT_order(bk,o),l) -> - let k,k_typ = to_ast_base_kind bk in + | Parse_ast.DT_aux(Parse_ast.DT_order(k,o),l) -> + let k,k_typ = to_ast_kind k in (match (k,o) with - | (BK_aux(BK_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_inc,lo)) -> + | (K_aux(K_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_inc,lo)) -> let default_order = Ord_aux(Ord_inc,lo) in DT_aux(DT_order default_order,l),(names,k_env,default_order) - | (BK_aux(BK_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_dec,lo)) -> + | (K_aux(K_order, _), Parse_ast.ATyp_aux(Parse_ast.ATyp_dec,lo)) -> let default_order = Ord_aux(Ord_dec,lo) in DT_aux(DT_order default_order,l),(names,k_env,default_order) | _ -> typ_error l "Inc and Dec must have kind Order" None None None) @@ -732,7 +720,7 @@ let to_ast_kdef (names, k_env, def_ord) (td:Parse_ast.kind_def) : unit kind_def match td with | Parse_ast.KD_aux (Parse_ast.KD_nabbrev (kind, id, name_scm_opt, atyp), l) -> let id = to_ast_id id in - let (kind, k) = to_ast_kind k_env kind in + let (kind, k) = to_ast_kind kind in KD_aux (KD_nabbrev (kind, id, to_ast_namescm name_scm_opt, to_ast_nexp k_env atyp), (l, ())) let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt = @@ -1257,7 +1245,7 @@ let generate_enum_functions vs_ids (Defs defs) = if IdSet.mem name vs_ids then [] else [ enum_val_spec name - [mk_qi_id BK_int kid; mk_qi_nc (range_constraint kid)] + [mk_qi_id K_int kid; mk_qi_nc (range_constraint kid)] (function_typ [atom_typ (nvar kid)] (mk_typ (Typ_id id)) no_effect); mk_fundef [funcl] ] in diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 0d7fd6e5..6a262df6 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -749,7 +749,7 @@ let reduce_cast typ exp l annot = let typ' = Env.base_typ_of env typ in match exp, destruct_exist env typ' with | E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' -> - let nc_env = Env.add_typ_var l kid BK_int env in + let nc_env = Env.add_typ_var l kid K_int env in let nc_env = Env.add_constraint (nc_eq (nvar kid) (nconstant n)) nc_env in if prove nc_env nc then exp @@ -2774,7 +2774,7 @@ let update_env_new_kids env deps typ_env_pre typ_env_post = let kbound = KBindings.merge (fun k x y -> match x,y with - | Some bk, None -> Some bk + | Some k, None -> Some k | _ -> None) (Env.get_typ_vars typ_env_post) (Env.get_typ_vars typ_env_pre) @@ -3190,7 +3190,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) = { env with kid_deps = List.fold_left (fun kds kid -> KBindings.add kid deps kds) env.kid_deps kids }, Env.add_constraint nc - (List.fold_left (fun tenv kid -> Env.add_typ_var l kid BK_int tenv) tenv kids), + (List.fold_left (fun tenv kid -> Env.add_typ_var l kid K_int tenv) tenv kids), typ in if is_bitvector_typ typ then @@ -4031,9 +4031,9 @@ let fill_in_type env typ = let tyvars = tyvars_of_typ typ in let subst = KidSet.fold (fun kid subst -> match Env.get_typ_var kid env with - | BK_type - | BK_order -> subst - | BK_int -> + | K_type + | K_order -> subst + | K_int -> (match solve env (nvar kid) with | None -> subst | Some n -> KBindings.add kid (nconstant n) subst)) tyvars KBindings.empty in diff --git a/src/parse_ast.ml b/src/parse_ast.ml index c50977ed..38854d48 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -70,15 +70,15 @@ type x = text (* identifier *) type ix = text (* infix identifier *) type -base_kind_aux = (* base kind *) - BK_type (* kind of types *) - | BK_int (* kind of natural number size expressions *) - | BK_order (* kind of vector order specifications *) +kind_aux = (* base kind *) + K_type (* kind of types *) + | K_int (* kind of natural number size expressions *) + | K_order (* kind of vector order specifications *) type -base_kind = - BK_aux of base_kind_aux * l +kind = + K_aux of kind_aux * l type @@ -110,13 +110,7 @@ id_aux = (* Identifier *) Id of x | DeIid of x (* remove infix status *) - -type -kind_aux = (* kinds *) - K_kind of (base_kind) list - - -type +type base_effect = BE_aux of base_effect_aux * l @@ -130,13 +124,7 @@ type id = Id_aux of id_aux * l - -type -kind = - K_aux of kind_aux * l - - -type +type atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *) ATyp_id of id (* identifier *) | ATyp_var of kid (* ticked variable *) @@ -425,7 +413,7 @@ name_scm_opt = type default_typing_spec_aux = (* Default kinding or typing assumption, and default order for literal vectors and vector shorthands *) - DT_order of base_kind * atyp + DT_order of kind * atyp type mpat_aux = (* Mapping pattern. Mostly the same as normal patterns but only constructible parts *) diff --git a/src/parser.mly b/src/parser.mly index cd655217..fd6c9373 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -585,17 +585,13 @@ typ_list: | typ Comma typ_list { $1 :: $3 } -base_kind: +kind: | Int - { BK_aux (BK_int, loc $startpos $endpos) } + { K_aux (K_int, loc $startpos $endpos) } | TYPE - { BK_aux (BK_type, loc $startpos $endpos) } + { K_aux (K_type, loc $startpos $endpos) } | Order - { BK_aux (BK_order, loc $startpos $endpos) } - -kind: - | base_kind - { K_aux (K_kind [$1], loc $startpos $endpos) } + { K_aux (K_order, loc $startpos $endpos) } kopt: | Lparen kid Colon kind Rparen @@ -1393,9 +1389,9 @@ register_def: { mk_reg_dec (DEC_config ($3, $5, $7)) $startpos $endpos } default_def: - | Default base_kind Inc + | Default kind Inc { mk_default (DT_order ($2, mk_typ ATyp_inc $startpos($3) $endpos)) $startpos $endpos } - | Default base_kind Dec + | Default kind Dec { mk_default (DT_order ($2, mk_typ ATyp_dec $startpos($3) $endpos)) $startpos $endpos } scattered_def: @@ -1449,8 +1445,7 @@ def: | default_def { DEF_default $1 } | Constant id Eq typ - { DEF_kind (KD_aux (KD_nabbrev (K_aux (K_kind [BK_aux (BK_int, loc $startpos($1) $endpos($1))], - loc $startpos($1) $endpos($1)), $2, mk_namesectn, $4), + { DEF_kind (KD_aux (KD_nabbrev (K_aux (K_int, loc $startpos($1) $endpos($1)), $2, mk_namesectn, $4), loc $startpos $endpos)) } | Mutual Lcurly fun_def_list Rcurly { DEF_internal_mutrec $3 } diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 630d5b1e..4b466326 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -598,12 +598,12 @@ let doc_quant_item_id ctx delimit (QI_aux (qi,_)) = | QI_id (KOpt_aux (KOpt_none kid,_)) -> if KBindings.mem kid ctx.kid_id_renames then None else Some (delimit (separate space [doc_var ctx kid; colon; string "Z"])) - | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (kind,_)],_),kid),_)) -> begin + | QI_id (KOpt_aux (KOpt_kind (K_aux (kind,_),kid),_)) -> begin if KBindings.mem kid ctx.kid_id_renames then None else match kind with - | BK_type -> Some (delimit (separate space [doc_var ctx kid; colon; string "Type"])) - | BK_int -> Some (delimit (separate space [doc_var ctx kid; colon; string "Z"])) - | BK_order -> None + | K_type -> Some (delimit (separate space [doc_var ctx kid; colon; string "Type"])) + | K_int -> Some (delimit (separate space [doc_var ctx kid; colon; string "Z"])) + | K_order -> None end | QI_id _ -> failwith "Quantifier with multiple kinds" | QI_const nc -> None diff --git a/src/return_analysis.ml b/src/return_analysis.ml index f60366fc..06565b01 100644 --- a/src/return_analysis.ml +++ b/src/return_analysis.ml @@ -114,7 +114,7 @@ let existentialize_annot funcl_annot annot = when Id.compare ty_id (mk_id "atom") = 0 -> let tyvars = Env.get_typ_vars funcl_env |> KBindings.bindings in let toplevel_kids = - List.filter (fun (kid, bk) -> match bk with BK_int -> true | _ -> false) tyvars |> List.map fst |> KidSet.of_list + List.filter (fun (kid, k) -> match k with K_int -> true | _ -> false) tyvars |> List.map fst |> KidSet.of_list in let new_kids = KidSet.diff (tyvars_of_nexp nexp) toplevel_kids in diff --git a/src/rewrites.ml b/src/rewrites.ml index f10c0059..2734e91f 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2096,7 +2096,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) = let quant_tyvars = List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item qis) in let typ_tyvars = tyvars_of_typ fun_typ in let new_tyvars = KidSet.diff typ_tyvars quant_tyvars in - List.map (mk_qi_id BK_int) (KidSet.elements new_tyvars) + List.map (mk_qi_id K_int) (KidSet.elements new_tyvars) in let typquant = match typquant with | TypQ_aux (TypQ_tq qis, l) -> @@ -2108,7 +2108,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) = in TypQ_aux (TypQ_tq qis, l) | _ -> - TypQ_aux (TypQ_tq (List.map (mk_qi_id BK_int) (KidSet.elements (tyvars_of_typ fun_typ))), l) + TypQ_aux (TypQ_tq (List.map (mk_qi_id K_int) (KidSet.elements (tyvars_of_typ fun_typ))), l) in let val_spec = VS_aux (VS_val_spec diff --git a/src/specialize.ml b/src/specialize.ml index 4d7a997f..6e625176 100644 --- a/src/specialize.ml +++ b/src/specialize.ml @@ -319,8 +319,8 @@ let specialize_id_valspec instantiations id ast = (* Remove type variables from the type quantifier. *) let kopts, constraints = quant_split typq in let kopts = List.filter (fun kopt -> not (is_typ_kopt kopt || is_order_kopt kopt)) kopts in - let typq = mk_typquant (List.map (mk_qi_id BK_type) typ_frees - @ List.map (mk_qi_id BK_int) int_frees + let typq = mk_typquant (List.map (mk_qi_id K_type) typ_frees + @ List.map (mk_qi_id K_int) int_frees @ List.map mk_qi_kopt kopts @ List.map mk_qi_nc constraints) in let typschm = mk_typschm typq typ in diff --git a/src/type_check.ml b/src/type_check.ml index 866aa071..d39ce27d 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -209,11 +209,7 @@ and strip_kinded_id_aux = function | KOpt_none kid -> KOpt_none (strip_kid kid) | KOpt_kind (kind, kid) -> KOpt_kind (strip_kind kind, strip_kid kid) and strip_kind = function - | K_aux (k_aux, _) -> K_aux (strip_kind_aux k_aux, Parse_ast.Unknown) -and strip_kind_aux = function - | K_kind base_kinds -> K_kind (List.map strip_base_kind base_kinds) -and strip_base_kind = function - | BK_aux (bk_aux, _) -> BK_aux (bk_aux, Parse_ast.Unknown) + | K_aux (k_aux, _) -> K_aux (k_aux, Parse_ast.Unknown) let adding = Util.("Adding " |> darkgray |> clear) @@ -250,11 +246,11 @@ module Env : sig val is_mutable : id -> t -> bool val get_constraints : t -> n_constraint list val add_constraint : n_constraint -> t -> t - val get_typ_var : kid -> t -> base_kind_aux + val get_typ_var : kid -> t -> kind_aux val get_typ_var_loc : kid -> t -> Ast.l - val get_typ_vars : t -> base_kind_aux KBindings.t + val get_typ_vars : t -> kind_aux KBindings.t val get_typ_var_locs : t -> Ast.l KBindings.t - val add_typ_var : l -> kid -> base_kind_aux -> t -> t + val add_typ_var : l -> kid -> kind_aux -> t -> t val get_ret_typ : t -> typ option val add_ret_typ : typ -> t -> t val add_typ_synonym : id -> (t -> typ_arg list -> typ) -> t -> t @@ -320,7 +316,7 @@ end = struct registers : (effect * effect * typ) Bindings.t; variants : (typquant * type_union list) Bindings.t; mappings : (typquant * typ * typ) Bindings.t; - typ_vars : (Ast.l * base_kind_aux) KBindings.t; + typ_vars : (Ast.l * kind_aux) KBindings.t; typ_synonyms : (t -> typ_arg list -> typ) Bindings.t; num_defs : nexp Bindings.t; overloads : (id list) Bindings.t; @@ -388,26 +384,26 @@ end = struct let get_typ_vars env = KBindings.map snd env.typ_vars let get_typ_var_locs env = KBindings.map fst env.typ_vars - let bk_counter = ref 0 - let bk_name () = let kid = mk_kid ("bk#" ^ string_of_int !bk_counter) in incr bk_counter; kid + 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 (bk_name ())) kinds) + 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", [BK_int; BK_int]); - ("atom", [BK_int]); - ("vector", [BK_int; BK_order; BK_type]); - ("register", [BK_type]); + [ ("range", [K_int; K_int]); + ("atom", [K_int]); + ("vector", [K_int; K_order; K_type]); + ("register", [K_type]); ("bit", []); ("unit", []); ("int", []); ("nat", []); ("bool", []); ("real", []); - ("list", [BK_type]); + ("list", [K_type]); ("string", []); - ("itself", [BK_int]) + ("itself", [K_int]) ] let builtin_mappings = @@ -517,10 +513,10 @@ end = struct try let (l, _) = KBindings.find kid env.typ_vars in rebindings := kid :: !rebindings; - { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) (l, BK_int) env.typ_vars } + { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) (l, K_int) env.typ_vars } with | Not_found -> - { env with typ_vars = KBindings.add kid (l, BK_int) env.typ_vars } + { env with typ_vars = KBindings.add kid (l, K_int) env.typ_vars } in let env = List.fold_left add_typ_var env kids in @@ -612,9 +608,9 @@ end = struct | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id) | Typ_var kid -> begin match KBindings.find kid env.typ_vars with - | (_, BK_type) -> () + | (_, K_type) -> () | (_, k) -> typ_error l ("Kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ - ^ " is " ^ string_of_base_kind_aux k ^ " rather than Type") + ^ " is " ^ string_of_kind_aux k ^ " rather than Type") | exception Not_found -> typ_error l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ) end @@ -646,10 +642,10 @@ end = struct | Nexp_var kid -> begin match get_typ_var kid env with - | BK_int -> () + | K_int -> () | kind -> typ_error l ("Constraint is badly formed, " ^ string_of_kid kid ^ " has kind " - ^ string_of_base_kind_aux kind ^ " but should have kind Int") + ^ string_of_kind_aux kind ^ " but should have kind Int") end | Nexp_constant _ -> () | Nexp_app (id, nexps) -> @@ -665,10 +661,10 @@ end = struct | Ord_var kid -> begin match get_typ_var kid env with - | BK_order -> () + | K_order -> () | kind -> typ_error l ("Order is badly formed, " ^ string_of_kid kid ^ " has kind " - ^ string_of_base_kind_aux kind ^ " but should have kind Order") + ^ string_of_kind_aux kind ^ " but should have kind Order") end | Ord_inc | Ord_dec -> () and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc_aux, l) as nc) = @@ -681,10 +677,10 @@ end = struct | NC_set (kid, _) when KidSet.mem kid exs -> () | NC_set (kid, _) -> begin match get_typ_var kid env with - | BK_int -> () + | K_int -> () | kind -> typ_error l ("Set constraint is badly formed, " ^ string_of_kid kid ^ " has kind " - ^ string_of_base_kind_aux kind ^ " but should have kind Int") + ^ string_of_kind_aux kind ^ " but should have kind Int") end | NC_or (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2 | NC_and (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2 @@ -716,7 +712,7 @@ end = struct 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, (_, bk)) -> string_of_kid kid ^ " => " ^ string_of_base_kind_aux bk) (KBindings.bindings env.typ_vars))); + 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' @@ -752,7 +748,7 @@ end = struct let existential_arg typq = function | None -> typq | Some (exs, nc, _) -> - List.fold_left (fun typq kid -> quant_add (mk_qi_id BK_int kid) typq) (quant_add (mk_qi_nc nc) typq) exs + List.fold_left (fun typq kid -> quant_add (mk_qi_id K_int kid) 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 @@ -1003,7 +999,7 @@ end = struct then typ_error (kid_loc kid) ("type variable " ^ string_of_kid kid ^ " is already bound") else begin - typ_print (lazy (adding ^ "type variable " ^ string_of_kid kid ^ " : " ^ string_of_base_kind_aux k)); + typ_print (lazy (adding ^ "type variable " ^ string_of_kid kid ^ " : " ^ string_of_kind_aux k)); { env with typ_vars = KBindings.add kid (l, k) env.typ_vars } end @@ -1116,9 +1112,8 @@ let add_typquant l (quant : typquant) (env : Env.t) : Env.t = | QI_aux (qi, _) -> add_quant_item_aux env qi and add_quant_item_aux env = function | QI_const constr -> Env.add_constraint constr env - | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var l kid BK_int env - | QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (k, _)], _), kid), _)) -> Env.add_typ_var l kid k env - | QI_id (KOpt_aux (_, l)) -> typ_error l "Type variable had non base kinds!" + | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var l kid K_int env + | QI_id (KOpt_aux (KOpt_kind (K_aux (k, _), kid), _)) -> Env.add_typ_var l kid k env in match quant with | TypQ_aux (TypQ_no_forall, _) -> env @@ -1150,10 +1145,10 @@ let destruct_exist env typ = | _ -> None let add_existential l kids nc env = - let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env kids in + let env = List.fold_left (fun env kid -> Env.add_typ_var l kid K_int env) env kids in Env.add_constraint nc env -let add_typ_vars l kids env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env kids +let add_typ_vars l kids env = List.fold_left (fun env kid -> Env.add_typ_var l kid K_int env) env kids let is_exist = function | Typ_aux (Typ_exist (_, _, _), _) -> true @@ -1344,7 +1339,7 @@ let solve env nexp = try KBindings.find kid !bindings with | Not_found -> fresh_var kid in - let env = Env.add_typ_var Parse_ast.Unknown (mk_kid "solve#") BK_int env in + let env = Env.add_typ_var Parse_ast.Unknown (mk_kid "solve#") K_int env in let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env)) (nc_constraint env var_of (nc_eq (nvar (mk_kid "solve#")) nexp)) in @@ -1868,7 +1863,7 @@ let rec subtyp l env (Typ_aux (typ_aux1, _) as typ1) (Typ_aux (typ_aux2, _) as t let env = match existential_kids, existential_nc with | [], None -> env | _, Some enc -> - let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env existential_kids in + let env = List.fold_left (fun env kid -> Env.add_typ_var l kid K_int env) env existential_kids in Env.add_constraint enc env | _, None -> assert false (* Cannot have existential_kids without existential_nc *) in @@ -1945,16 +1940,16 @@ let infer_lit env (L_aux (lit_aux, l) as lit) = | L_undef -> typ_error l "Cannot infer the type of undefined" let is_nat_kid kid = function - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_int, _)], _), kid'), _) -> Kid.compare kid kid' = 0 + | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid'), _) -> Kid.compare kid kid' = 0 | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0 | _ -> false let is_order_kid kid = function - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), kid'), _) -> Kid.compare kid kid' = 0 + | KOpt_aux (KOpt_kind (K_aux (K_order, _), kid'), _) -> Kid.compare kid kid' = 0 | _ -> false let is_typ_kid kid = function - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid'), _) -> Kid.compare kid kid' = 0 + | KOpt_aux (KOpt_kind (K_aux (K_type, _), kid'), _) -> Kid.compare kid kid' = 0 | _ -> false let rec instantiate_quants quants kid uvar = match quants with @@ -2883,7 +2878,7 @@ and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _) begin match typ_nexps typ with | [nexp] -> - Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid BK_int env) + Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid K_int env) | [] -> typ_error l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to") | nexps -> @@ -2896,7 +2891,7 @@ and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_arg_aux (typ_ match typ_pat_aux, typ_arg_aux with | TP_wild, _ -> env | TP_var kid, Typ_arg_nexp nexp -> - Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid BK_int env) + Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var l kid K_int env) | _, Typ_arg_typ typ -> bind_typ_pat env typ_pat typ | _, Typ_arg_order _ -> typ_error l "Cannot bind type pattern against order" | _, _ -> typ_error l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat) @@ -3238,7 +3233,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = match destruct_numeric env (typ_of inferred_f), destruct_numeric env (typ_of inferred_t) with | Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) -> let loop_kid = mk_kid ("loop_" ^ string_of_id v) in - let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env (loop_kid :: kids1 @ kids2) in + let env = List.fold_left (fun env kid -> Env.add_typ_var l kid K_int env) env (loop_kid :: kids1 @ kids2) in let env = Env.add_constraint (nc_and nc1 nc2) env in let env = Env.add_constraint (nc_and (nc_lteq nexp1 (nvar loop_kid)) (nc_lteq (nvar loop_kid) nexp2)) env in let loop_vtyp = atom_typ (nvar loop_kid) in @@ -3392,7 +3387,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = | [], None -> env | _, Some enc -> let enc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid ex_tag kid)) nc) enc ex_kids in - let env = List.fold_left (fun env kid -> Env.add_typ_var l (prepend_kid ex_tag kid) BK_int env) env ex_kids in + let env = List.fold_left (fun env kid -> Env.add_typ_var l (prepend_kid ex_tag kid) K_int env) env ex_kids in Env.add_constraint enc env | _, None -> assert false (* Cannot have ex_kids without ex_nc *) in @@ -3428,7 +3423,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = typ_debug (lazy (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers))); if ex_kids = [] then () else (typ_debug (lazy ("EX GOAL: " ^ string_of_option string_of_n_constraint ex_nc)); ex_goal := ex_nc); record_unifiers unifiers; - let env = List.fold_left (fun env kid -> Env.add_typ_var l kid BK_int env) env ex_kids in + let env = List.fold_left (fun env kid -> Env.add_typ_var l kid K_int env) env ex_kids in let typs' = List.map (subst_unifiers unifiers) typs in let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in let ret_typ' = @@ -4385,12 +4380,11 @@ let kinded_id_arg kind_id = let typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) in match kind_id with | KOpt_aux (KOpt_none kid, _) -> typ_arg (Typ_arg_nexp (nvar kid)) - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_int, _)], _), kid), _) -> typ_arg (Typ_arg_nexp (nvar kid)) - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), kid), _) -> + | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid), _) -> typ_arg (Typ_arg_nexp (nvar kid)) + | KOpt_aux (KOpt_kind (K_aux (K_order, _), kid), _) -> typ_arg (Typ_arg_order (Ord_aux (Ord_var kid, Parse_ast.Unknown))) - | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid), _) -> + | KOpt_aux (KOpt_kind (K_aux (K_type, _), kid), _) -> typ_arg (Typ_arg_typ (mk_typ (Typ_var kid))) - | KOpt_aux (KOpt_kind (K_aux (K_kind kinds, _), kid), l) -> typ_error l "Badly formed kind" let fold_union_quant quants (QI_aux (qi, l)) = match qi with @@ -4401,7 +4395,7 @@ let check_type_union env variant typq (Tu_aux (tu, l)) = let ret_typ = app_typ variant (List.fold_left fold_union_quant [] (quant_items typq)) in match tu with | Tu_ty_id (Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) as typ, v) -> - let typq = mk_typquant (List.map (mk_qi_id BK_type) (KidSet.elements (typ_frees typ))) in + let typq = mk_typquant (List.map (mk_qi_id K_type) (KidSet.elements (typ_frees typ))) in env |> Env.add_union_id v (typq, typ) |> Env.add_val_spec v (typq, typ) @@ -4441,7 +4435,7 @@ let mk_synonym typq typ = let check_kinddef env (KD_aux (kdef, (l, _))) = let kd_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented kind def") in match kdef with - | KD_nabbrev ((K_aux(K_kind([BK_aux (BK_int, _)]),_) as kind), id, nmscm, nexp) -> + | KD_nabbrev (K_aux (K_int, _) as kind, id, nmscm, nexp) -> [DEF_kind (KD_aux (KD_nabbrev (kind, id, nmscm, nexp), (l, None)))], Env.add_num_def id nexp env | _ -> kd_err () diff --git a/src/type_check.mli b/src/type_check.mli index 1081af08..f08272de 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -127,13 +127,13 @@ module Env : sig val add_constraint : n_constraint -> t -> t - val get_typ_var : kid -> t -> base_kind_aux + val get_typ_var : kid -> t -> kind_aux - val get_typ_vars : t -> base_kind_aux KBindings.t + val get_typ_vars : t -> kind_aux KBindings.t val get_typ_var_locs : t -> Ast.l KBindings.t - val add_typ_var : Ast.l -> kid -> base_kind_aux -> t -> t + val add_typ_var : Ast.l -> kid -> kind_aux -> t -> t val is_record : id -> t -> bool -- cgit v1.2.3