From f63571c9a6b532f64b415de27bb0ee6cc358388d Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 11 Oct 2018 21:31:23 +0100 Subject: Change the function type in the AST Changes the representation of function types in the ast from Typ_fn : typ -> typ to Typ_fn : typ list -> typ to more accurately represent their use in the various backends, where we often compile functions to either their curried representations as in Lem and Isabelle, or just multiple argument functions in C. There's still some oddity because a single pattern in a function clause can bind against multiple arguments, and maybe we want to forbid this in the future. The syntax also hasn't changed (yet), so in theory this change shouldn't break anything (but it invariably will...). In the future we would ideally require that a function with N arguments has exactly N patterns in its declaration, one for each argument so f : (x, y) -> z f _ = ... would be disallowed (as _ matches both x and y), forcing f(_, _) = z this would simply quite a few things, Also we could have a different syntax for function argument lists and tuples, because it's rather hard to define a function that actually takes a tuple with the syntax how it is now. Some issues I noticed when doing this refactoring: Line 1926 of Coq translation. untuple_args_pat is maybe no longer needed? However there's still some funnyness where a pattern can be used to bind multiple function arguments so maybe it still is. Line 2306 of monomorphisation. I simplified the logic here. I think it's equivalent now, but I could be wrong. Line 4517 of rewrites. I'm not sure what make_cstr_mappings is doing here, but hopefully the simpler version is the same. --- src/ast_util.ml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index b9ab21b2..1d0689e4 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -296,7 +296,7 @@ let bool_typ = mk_id_typ (mk_id "bool") let string_typ = mk_id_typ (mk_id "string") let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)])) let tuple_typ typs = mk_typ (Typ_tup typs) -let function_typ typ1 typ2 eff = mk_typ (Typ_fn (typ1, typ2, eff)) +let function_typ arg_typs ret_typ eff = mk_typ (Typ_fn (arg_typs, ret_typ, eff)) let vector_typ n ord typ = mk_typ (Typ_app (mk_id "vector", @@ -613,8 +613,11 @@ and string_of_typ_aux = function | Typ_var kid -> string_of_kid kid | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")" | Typ_app (id, args) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")" - | Typ_fn (typ_arg, typ_ret, eff) -> - string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff + | Typ_fn ([typ_arg], typ_ret, eff) -> + string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff + | Typ_fn (typ_args, typ_ret, eff) -> + "(" ^ string_of_list ", " string_of_typ typ_args ^ ") -> " + ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff | Typ_bidir (typ1, typ2) -> string_of_typ typ1 ^ " <-> " ^ string_of_typ typ2 | Typ_exist (kids, nc, typ) -> "{" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}" @@ -901,8 +904,8 @@ module Typ = struct | Typ_internal_unknown, Typ_internal_unknown -> 0 | Typ_id id1, Typ_id id2 -> Id.compare id1 id2 | Typ_var kid1, Typ_var kid2 -> Kid.compare kid1 kid2 - | Typ_fn (t1,t2,e1), Typ_fn (t3,t4,e2) -> - (match compare t1 t3 with + | Typ_fn (ts1,t2,e1), Typ_fn (ts3,t4,e2) -> + (match Util.compare_list compare ts1 ts3 with | 0 -> (match compare t2 t4 with | 0 -> effect_compare e1 e2 | n -> n) @@ -1084,7 +1087,7 @@ let rec tyvars_of_typ (Typ_aux (t,_)) = | Typ_internal_unknown -> KidSet.empty | Typ_id _ -> KidSet.empty | Typ_var kid -> KidSet.singleton kid - | Typ_fn (t1,t2,_) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2) + | Typ_fn (ts, t, _) -> List.fold_left KidSet.union (tyvars_of_typ t) (List.map tyvars_of_typ ts) | Typ_bidir (t1, t2) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2) | Typ_tup ts -> List.fold_left (fun s t -> KidSet.union s (tyvars_of_typ t)) @@ -1345,7 +1348,8 @@ let rec locate_typ l (Typ_aux (typ_aux, _)) = | Typ_internal_unknown -> Typ_internal_unknown | Typ_id id -> Typ_id (locate_id l id) | Typ_var kid -> Typ_var (locate_kid l kid) - | Typ_fn (arg_typ, ret_typ, effect) -> Typ_fn (locate_typ l arg_typ, locate_typ l ret_typ, locate_effect l effect) + | Typ_fn (arg_typs, ret_typ, effect) -> + Typ_fn (List.map (locate_typ l) arg_typs, locate_typ l ret_typ, locate_effect l effect) | Typ_bidir (typ1, typ2) -> Typ_bidir (locate_typ l typ1, locate_typ l typ2) | Typ_tup typs -> Typ_tup (List.map (locate_typ l) typs) | Typ_exist (kids, constr, typ) -> Typ_exist (List.map (locate_kid l) kids, locate_nc l constr, locate_typ l typ) -- cgit v1.2.3 From 5471af45fd04169eb184371dcd8f791e507eab6f Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 24 Oct 2018 17:25:47 +0100 Subject: Add constraint synonyms Currently not enabled by default, the flag -Xconstraint_synonyms enables them For generating constraints in ASL parser, we want to be able to give names to the constraints that we attach to certain variables. It's slightly awkward right now when constraints get long complicated because the entire constraint always has to be typed out in full whenever it appears, and there's no way to abstract away from that. This adds constraint synonyms, which work much like type synonyms except for constraints, e.g. constraint Size('n) = 'n in {1, 2, 4, 8} | 128 <= 'n <= 256 these constraints can then be used instead of the full constraint, e.g. val f : forall 'n, where Size('n). int('n) -> unit Unfortunatly we need to have a keyword to 'call' the constraint synonym otherwise the grammer stops being LR(1). This could be resolved by parsing all constraints into Parse_ast.atyp and then de-sugaring them into constraints, which is what happens for n-expressions already, but that would require quite a bit of work on the parser. To avoid this forcing changes to any other parts of Sail, the intended invariant is that all constraints appearing anywhere in a type-checked AST have no constraint synonyms, so they don't have to worry about matching on NC_app, or calling Env.expand_typquant_synonyms (which isn't even exported for this reason). --- src/ast_util.ml | 27 ++++++++++++++++++++++----- 1 file changed, 22 insertions(+), 5 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index 1d0689e4..9966742e 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -329,7 +329,7 @@ let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2)) let nc_true = mk_nc NC_true let nc_false = mk_nc NC_false -let rec nc_negate (NC_aux (nc, _)) = +let rec nc_negate (NC_aux (nc, l)) = match nc with | NC_bounded_ge (n1, n2) -> nc_lt n1 n2 | NC_bounded_le (n1, n2) -> nc_gt n1 n2 @@ -343,6 +343,8 @@ let rec nc_negate (NC_aux (nc, _)) = | NC_set (kid, [int]) -> nc_neq (nvar kid) (nconstant int) | NC_set (kid, int :: ints) -> mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints))))) + | NC_app _ -> + raise (Reporting_basic.err_unreachable l __POS__ "tried to negate constraint with unexpanded synonym") let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown) @@ -379,6 +381,10 @@ let quant_split typq = let qis = quant_items typq in List.concat (List.map qi_kopt qis), List.concat (List.map qi_nc qis) +let quant_map_items f = function + | TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_no_forall, l) + | TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (List.map f qis), l) + let unaux_nexp (Nexp_aux (nexp, _)) = nexp let unaux_order (Ord_aux (ord, _)) = ord let unaux_typ (Typ_aux (typ, _)) = typ @@ -523,8 +529,8 @@ let def_loc = function | DEF_scattered (SD_aux (_, (l, _))) | DEF_reg_dec (DEC_aux (_, (l, _))) | DEF_fixity (_, _, Id_aux (_, l)) - | DEF_overload (Id_aux (_, l), _) -> - l + | DEF_overload (Id_aux (_, l), _) -> l + | DEF_constraint (Id_aux (_, l), _, _) -> l | DEF_internal_mutrec _ -> Parse_ast.Unknown let string_of_id = function @@ -638,12 +644,17 @@ and string_of_n_constraint = function "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_set (kid, ns), _) -> string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}" + | NC_aux (NC_app (id, nexps), _) -> + "where " ^ string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_nexp nexps ^ ")" | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" +let string_of_kinded_id = function + | KOpt_aux (KOpt_none kid, _) -> string_of_kid kid + | KOpt_aux (KOpt_kind (k, kid), _) -> "(" ^ string_of_kid kid ^ " : " ^ string_of_kind k ^ ")" + let string_of_quant_item_aux = function - | QI_id (KOpt_aux (KOpt_none kid, _)) -> string_of_kid kid - | QI_id (KOpt_aux (KOpt_kind (k, kid), _)) -> "(" ^ string_of_kid kid ^ " :: " ^ string_of_kind k ^ ")" + | QI_id kopt -> string_of_kinded_id kopt | QI_const constr -> string_of_n_constraint constr let string_of_quant_item = function @@ -884,6 +895,8 @@ module NC = struct | NC_or (nc1,nc2), NC_or (nc3,nc4) | NC_and (nc1,nc2), NC_and (nc3,nc4) -> lex_ord compare compare nc1 nc3 nc2 nc4 + | NC_app (id1, nexps1), NC_app (id2, nexps2) + -> lex_ord (Id.compare) (Util.compare_list Nexp.compare) id1 id2 nexps1 nexps2 | NC_true, NC_true | NC_false, NC_false -> 0 @@ -894,6 +907,7 @@ module NC = struct | NC_set _, _ -> -1 | _, NC_set _ -> 1 | NC_or _, _ -> -1 | _, NC_or _ -> 1 | NC_and _, _ -> -1 | _, NC_and _ -> 1 + | NC_app _, _ -> -1 | _, NC_app _ -> 1 | NC_true, _ -> -1 | _, NC_true -> 1 end @@ -1079,6 +1093,8 @@ let rec tyvars_of_nc (NC_aux (nc, _)) = | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> KidSet.union (tyvars_of_nc nc1) (tyvars_of_nc nc2) + | NC_app (id, nexps) -> + List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps) | NC_true | NC_false -> KidSet.empty @@ -1338,6 +1354,7 @@ let rec locate_nc l (NC_aux (nc_aux, _)) = | NC_set (kid, nums) -> NC_set (locate_kid l kid, nums) | NC_or (nc1, nc2) -> NC_or (locate_nc l nc1, locate_nc l nc2) | NC_and (nc1, nc2) -> NC_and (locate_nc l nc1, locate_nc l nc2) + | NC_app (id, nexps) -> NC_app (id, List.map (locate_nexp l) nexps) | NC_true -> NC_true | NC_false -> NC_false in -- cgit v1.2.3 From 5298e209f0ae12e51f3050888e18ad9be09543e4 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 31 Oct 2018 14:56:19 +0000 Subject: Improve error messages for unsolved function quantifiers For example, for a function like ``` val aget_X : forall 'n, 0 <= 'n <= 31. int('n) -> bits(64) function test(n : int) -> unit = { let y = aget_X(n); () } ``` we get the message > Could not resolve quantifiers for aget_X (0 <= 'ex7# & 'ex7# <= 31) > > Try adding named type variables for n : atom('ex7#) > > The property (0 <= n & n <= 31) must hold which suggests adding a name for the type variable 'ex7#, and gives the property in terms of the variable n. If we give n a type variable name: ``` val test : int -> unit function test(n as 'N) = { let y = aget_X(n); () } ``` It will suggest a constraint involving the type variable name > Could not resolve quantifiers for aget_X (0 <= 'ex6# & 'ex6# <= 31) > > Try adding the constraint (0 <= 'N & 'N <= 31) --- src/ast_util.ml | 133 ++++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 129 insertions(+), 4 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index 9966742e..9490366f 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -1082,7 +1082,7 @@ let rec tyvars_of_nexp (Nexp_aux (nexp,_)) = | Nexp_neg n -> tyvars_of_nexp n | Nexp_app (_, nexps) -> List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps) -let rec tyvars_of_nc (NC_aux (nc, _)) = +let rec tyvars_of_constraint (NC_aux (nc, _)) = match nc with | NC_equal (nexp1, nexp2) | NC_bounded_ge (nexp1, nexp2) @@ -1092,7 +1092,7 @@ let rec tyvars_of_nc (NC_aux (nc, _)) = | NC_set (kid, _) -> KidSet.singleton kid | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> - KidSet.union (tyvars_of_nc nc1) (tyvars_of_nc nc2) + KidSet.union (tyvars_of_constraint nc1) (tyvars_of_constraint nc2) | NC_app (id, nexps) -> List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps) | NC_true @@ -1112,7 +1112,7 @@ let rec tyvars_of_typ (Typ_aux (t,_)) = List.fold_left (fun s ta -> KidSet.union s (tyvars_of_typ_arg ta)) KidSet.empty tas | Typ_exist (kids, nc, t) -> - let s = KidSet.union (tyvars_of_typ t) (tyvars_of_nc nc) in + let s = KidSet.union (tyvars_of_typ t) (tyvars_of_constraint nc) in List.fold_left (fun s k -> KidSet.remove k s) s kids and tyvars_of_typ_arg (Typ_arg_aux (ta,_)) = match ta with @@ -1123,7 +1123,7 @@ and tyvars_of_typ_arg (Typ_arg_aux (ta,_)) = let tyvars_of_quant_item (QI_aux (qi, _)) = match qi with | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) -> KidSet.singleton kid - | QI_const nc -> tyvars_of_nc nc + | QI_const nc -> tyvars_of_constraint nc let is_kid_generated kid = String.contains (string_of_kid kid) '#' @@ -1488,3 +1488,128 @@ and locate_fexps : 'a. l -> 'a fexps -> 'a fexps = fun l (FES_aux (FES_Fexps (fe and locate_fexp : 'a. l -> 'a fexp -> 'a fexp = fun l (FE_aux (FE_Fexp (id, exp), (_, annot))) -> FE_aux (FE_Fexp (locate_id l id, locate l exp), (l, annot)) + +(**************************************************************************) +(* 1. Substitutions *) +(**************************************************************************) + +let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv subst nexp, l) +and nexp_subst_aux sv subst = function + | Nexp_id v -> Nexp_id v + | Nexp_var kid -> if Kid.compare kid sv = 0 then subst else Nexp_var kid + | Nexp_constant c -> Nexp_constant c + | Nexp_times (nexp1, nexp2) -> Nexp_times (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) + | Nexp_sum (nexp1, nexp2) -> Nexp_sum (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) + | Nexp_minus (nexp1, nexp2) -> Nexp_minus (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) + | Nexp_app (id, nexps) -> Nexp_app (id, List.map (nexp_subst sv subst) nexps) + | Nexp_exp nexp -> Nexp_exp (nexp_subst sv subst nexp) + | Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp) + +let rec nexp_set_to_or l subst = function + | [] -> raise (Reporting_basic.err_unreachable l __POS__ "Empty set in constraint") + | [int] -> NC_equal (subst, nconstant int) + | (int :: ints) -> NC_or (mk_nc (NC_equal (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints)) + +let rec nc_subst_nexp sv subst (NC_aux (nc, l)) = NC_aux (nc_subst_nexp_aux l sv subst nc, l) +and nc_subst_nexp_aux l sv subst = function + | NC_equal (n1, n2) -> NC_equal (nexp_subst sv subst n1, nexp_subst sv subst n2) + | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2) + | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2) + | NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2) + | NC_set (kid, ints) as set_nc -> + if Kid.compare kid sv = 0 + then nexp_set_to_or l (mk_nexp subst) ints + else set_nc + | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2) + | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2) + | NC_app (id, nexps) -> NC_app (id, List.map (nexp_subst sv subst) nexps) + | NC_false -> NC_false + | NC_true -> NC_true + +let rec typ_subst_nexp sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_nexp_aux sv subst typ, l) +and typ_subst_nexp_aux sv subst = function + | Typ_internal_unknown -> Typ_internal_unknown + | Typ_id v -> Typ_id v + | Typ_var kid -> Typ_var kid + | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_nexp sv subst) arg_typs, typ_subst_nexp sv subst ret_typ, effs) + | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2) + | Typ_tup typs -> Typ_tup (List.map (typ_subst_nexp sv subst) typs) + | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args) + | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) + | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv subst nc, typ_subst_nexp sv subst typ) +and typ_subst_arg_nexp sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_nexp_aux sv subst arg, l) +and typ_subst_arg_nexp_aux sv subst = function + | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp) + | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_nexp sv subst typ) + | Typ_arg_order ord -> Typ_arg_order ord + +let rec typ_subst_typ sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_typ_aux sv subst typ, l) +and typ_subst_typ_aux sv subst = function + | Typ_internal_unknown -> Typ_internal_unknown + | Typ_id v -> Typ_id v + | Typ_var kid -> if Kid.compare kid sv = 0 then subst else Typ_var kid + | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_typ sv subst) arg_typs, typ_subst_typ sv subst ret_typ, effs) + | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2) + | Typ_tup typs -> Typ_tup (List.map (typ_subst_typ sv subst) typs) + | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_typ sv subst) args) + | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_typ sv subst typ) +and typ_subst_arg_typ sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_typ_aux sv subst arg, l) +and typ_subst_arg_typ_aux sv subst = function + | Typ_arg_nexp nexp -> Typ_arg_nexp nexp + | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_typ sv subst typ) + | Typ_arg_order ord -> Typ_arg_order ord + +let order_subst_aux sv subst = function + | Ord_var kid -> if Kid.compare kid sv = 0 then subst else Ord_var kid + | Ord_inc -> Ord_inc + | Ord_dec -> Ord_dec + +let order_subst sv subst (Ord_aux (ord, l)) = Ord_aux (order_subst_aux sv subst ord, l) + +let rec typ_subst_order sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_order_aux sv subst typ, l) +and typ_subst_order_aux sv subst = function + | Typ_internal_unknown -> Typ_internal_unknown + | Typ_id v -> Typ_id v + | Typ_var kid -> Typ_var kid + | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_order sv subst) arg_typs, typ_subst_order sv subst ret_typ, effs) + | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2) + | Typ_tup typs -> Typ_tup (List.map (typ_subst_order sv subst) typs) + | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_order sv subst) args) + | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_order sv subst typ) +and typ_subst_arg_order sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_order_aux sv subst arg, l) +and typ_subst_arg_order_aux sv subst = function + | Typ_arg_nexp nexp -> Typ_arg_nexp nexp + | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_order sv subst typ) + | Typ_arg_order ord -> Typ_arg_order (order_subst sv subst ord) + +let rec typ_subst_kid sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_kid_aux sv subst typ, l) +and typ_subst_kid_aux sv subst = function + | Typ_internal_unknown -> Typ_internal_unknown + | Typ_id v -> Typ_id v + | Typ_var kid -> if Kid.compare kid sv = 0 then Typ_var subst else Typ_var kid + | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_kid sv subst) arg_typs, typ_subst_kid sv subst ret_typ, effs) + | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2) + | Typ_tup typs -> Typ_tup (List.map (typ_subst_kid sv subst) typs) + | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_kid sv subst) args) + | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) + | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv (Nexp_var subst) nc, typ_subst_kid sv subst typ) +and typ_subst_arg_kid sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_kid_aux sv subst arg, l) +and typ_subst_arg_kid_aux sv subst = function + | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv (Nexp_var subst) nexp) + | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_kid sv subst typ) + | Typ_arg_order ord -> Typ_arg_order (order_subst sv (Ord_var subst) ord) + +let quant_item_subst_kid_aux sv subst = function + | QI_id (KOpt_aux (KOpt_none kid, l)) as qid -> + if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_none subst, l)) else qid + | QI_id (KOpt_aux (KOpt_kind (k, kid), l)) as qid -> + if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_kind (k, subst), l)) else qid + | QI_const nc -> QI_const (nc_subst_nexp sv (Nexp_var subst) nc) + +let quant_item_subst_kid sv subst (QI_aux (quant, l)) = QI_aux (quant_item_subst_kid_aux sv subst quant, l) + +let typquant_subst_kid_aux sv subst = function + | TypQ_tq quants -> TypQ_tq (List.map (quant_item_subst_kid sv subst) quants) + | TypQ_no_forall -> TypQ_no_forall + +let typquant_subst_kid sv subst (TypQ_aux (typq, l)) = TypQ_aux (typquant_subst_kid_aux sv subst typq, l) -- cgit v1.2.3 From 001e28b487c8a4cb2a25519a3acc8ac8c1aaabf5 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 31 Oct 2018 15:43:56 +0000 Subject: Rename Reporting_basic to Reporting There is no Reporting_complex, so it's not clear what the basic is intended to signify anyway. Add a GitHub issue link to any err_unreachable errors (as they are all bugs) --- src/ast_util.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index 9490366f..a0b75fc2 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -344,7 +344,7 @@ let rec nc_negate (NC_aux (nc, l)) = | NC_set (kid, int :: ints) -> mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints))))) | NC_app _ -> - raise (Reporting_basic.err_unreachable l __POS__ "tried to negate constraint with unexpanded synonym") + raise (Reporting.err_unreachable l __POS__ "tried to negate constraint with unexpanded synonym") let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown) @@ -828,13 +828,13 @@ let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) = (fun (FCL_aux (FCL_Funcl (id, _), _)) id' -> match id' with | Some id' -> if string_of_id id' = string_of_id id then Some id' - else raise (Reporting_basic.err_typ l + else raise (Reporting.err_typ l ("Function declaration expects all definitions to have the same name, " ^ string_of_id id ^ " differs from other definitions of " ^ string_of_id id')) | None -> Some id) funcls None) with | Some id -> id - | None -> raise (Reporting_basic.err_typ l "funcl list is empty") + | None -> raise (Reporting.err_typ l "funcl list is empty") let id_of_type_def_aux = function | TD_abbrev (id, _, _) @@ -959,7 +959,7 @@ module TypMap = Map.Make(Typ) let rec nexp_frees (Nexp_aux (nexp, l)) = match nexp with - | Nexp_id _ -> raise (Reporting_basic.err_typ l "Unimplemented Nexp_id in nexp_frees") + | Nexp_id _ -> raise (Reporting.err_typ l "Unimplemented Nexp_id in nexp_frees") | Nexp_var kid -> KidSet.singleton kid | Nexp_constant _ -> KidSet.empty | Nexp_times (n1, n2) -> KidSet.union (nexp_frees n1) (nexp_frees n2) @@ -977,7 +977,7 @@ let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) = let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with | LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot) | _ -> - raise (Reporting_basic.err_unreachable l __POS__ + raise (Reporting.err_unreachable l __POS__ ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in rewrap (E_tuple (List.map get_id les)) | LEXP_vector (lexp, e) -> rewrap (E_vector_access (lexp_to_exp lexp, e)) @@ -1016,7 +1016,7 @@ let typ_app_args_of = function | Typ_aux (Typ_app (Id_aux (Id c,_), targs), l) -> (c, List.map (fun (Typ_arg_aux (a,_)) -> a) targs, l) | Typ_aux (_, l) as typ -> - raise (Reporting_basic.err_typ l + raise (Reporting.err_typ l ("typ_app_args_of called on non-app type " ^ string_of_typ typ)) let rec vector_typ_args_of typ = match typ_app_args_of typ with @@ -1024,7 +1024,7 @@ let rec vector_typ_args_of typ = match typ_app_args_of typ with (nexp_simp len, ord, etyp) | ("register", [Typ_arg_typ rtyp], _) -> vector_typ_args_of rtyp | (_, _, l) -> - raise (Reporting_basic.err_typ l + raise (Reporting.err_typ l ("vector_typ_args_of called on non-vector type " ^ string_of_typ typ)) let vector_start_index typ = @@ -1032,13 +1032,13 @@ let vector_start_index typ = match ord with | Ord_aux (Ord_inc, _) -> nint 0 | Ord_aux (Ord_dec, _) -> nexp_simp (nminus len (nint 1)) - | _ -> raise (Reporting_basic.err_typ (typ_loc typ) "Can't calculate start index without order") + | _ -> raise (Reporting.err_typ (typ_loc typ) "Can't calculate start index without order") let is_order_inc = function | Ord_aux (Ord_inc, _) -> true | Ord_aux (Ord_dec, _) -> false | Ord_aux (Ord_var _, l) -> - raise (Reporting_basic.err_unreachable l __POS__ "is_order_inc called on vector with variable ordering") + raise (Reporting.err_unreachable l __POS__ "is_order_inc called on vector with variable ordering") let is_bit_typ = function | Typ_aux (Typ_id (Id_aux (Id "bit", _)), _) -> true @@ -1506,7 +1506,7 @@ and nexp_subst_aux sv subst = function | Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp) let rec nexp_set_to_or l subst = function - | [] -> raise (Reporting_basic.err_unreachable l __POS__ "Empty set in constraint") + | [] -> raise (Reporting.err_unreachable l __POS__ "Empty set in constraint") | [int] -> NC_equal (subst, nconstant int) | (int :: ints) -> NC_or (mk_nc (NC_equal (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints)) -- cgit v1.2.3 From 1eedc27eeca4496bada669b700a59283cc6932e9 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 31 Oct 2018 16:53:18 +0000 Subject: Remove Parse_ast.Int, add unique locations Remove Parse_ast.Int (for internal locations) as this was unused. Add a Parse_ast.Unique constructor to create unique locations. Change locate_X functions to take a function modifying locations, rather than just replacing them and add a function unique : l -> l that makes locations unique, such that `locate unique X` will make a locations in X unique. --- src/ast_util.ml | 259 ++++++++++++++++++++++++++++++-------------------------- 1 file changed, 137 insertions(+), 122 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index a0b75fc2..3cd2f361 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -1320,174 +1320,189 @@ let hex_to_bin hex = (* Functions for working with locations *) -let locate_id l (Id_aux (name, _)) = Id_aux (name, l) +let locate_id f (Id_aux (name, l)) = Id_aux (name, f l) -let locate_kid l (Kid_aux (name, _)) = Kid_aux (name, l) +let locate_kid f (Kid_aux (name, l)) = Kid_aux (name, f l) -let locate_lit l (L_aux (lit, _)) = L_aux (lit, l) +let locate_lit f (L_aux (lit, l)) = L_aux (lit, f l) -let locate_base_effect l (BE_aux (base_effect, _)) = BE_aux (base_effect, l) +let locate_base_effect f (BE_aux (base_effect, l)) = BE_aux (base_effect, f l) -let locate_effect l (Effect_aux (Effect_set effects, _)) = - Effect_aux (Effect_set (List.map (locate_base_effect l) effects), l) +let locate_effect f (Effect_aux (Effect_set effects, l)) = + Effect_aux (Effect_set (List.map (locate_base_effect f) effects), f l) -let rec locate_nexp l (Nexp_aux (nexp_aux, _)) = +let locate_order f (Ord_aux (ord_aux, l)) = + let ord_aux = match ord_aux with + | Ord_inc -> Ord_inc + | Ord_dec -> Ord_dec + | Ord_var v -> Ord_var (locate_kid f v) + in + Ord_aux (ord_aux, f l) + +let rec locate_nexp f (Nexp_aux (nexp_aux, l)) = let nexp_aux = match nexp_aux with - | Nexp_id id -> Nexp_id (locate_id l id) - | Nexp_var kid -> Nexp_var (locate_kid l kid) + | Nexp_id id -> Nexp_id (locate_id f id) + | Nexp_var kid -> Nexp_var (locate_kid f kid) | Nexp_constant n -> Nexp_constant n - | Nexp_app (id, nexps) -> Nexp_app (locate_id l id, List.map (locate_nexp l) nexps) - | Nexp_times (nexp1, nexp2) -> Nexp_times (locate_nexp l nexp1, locate_nexp l nexp2) - | Nexp_sum (nexp1, nexp2) -> Nexp_sum (locate_nexp l nexp1, locate_nexp l nexp2) - | Nexp_minus (nexp1, nexp2) -> Nexp_minus (locate_nexp l nexp1, locate_nexp l nexp2) - | Nexp_exp nexp -> Nexp_exp (locate_nexp l nexp) - | Nexp_neg nexp -> Nexp_neg (locate_nexp l nexp) + | Nexp_app (id, nexps) -> Nexp_app (locate_id f id, List.map (locate_nexp f) nexps) + | Nexp_times (nexp1, nexp2) -> Nexp_times (locate_nexp f nexp1, locate_nexp f nexp2) + | Nexp_sum (nexp1, nexp2) -> Nexp_sum (locate_nexp f nexp1, locate_nexp f nexp2) + | Nexp_minus (nexp1, nexp2) -> Nexp_minus (locate_nexp f nexp1, locate_nexp f nexp2) + | Nexp_exp nexp -> Nexp_exp (locate_nexp f nexp) + | Nexp_neg nexp -> Nexp_neg (locate_nexp f nexp) in - Nexp_aux (nexp_aux, l) + Nexp_aux (nexp_aux, f l) -let rec locate_nc l (NC_aux (nc_aux, _)) = +let rec locate_nc f (NC_aux (nc_aux, l)) = let nc_aux = match nc_aux with - | NC_equal (nexp1, nexp2) -> NC_equal (locate_nexp l nexp1, locate_nexp l nexp2) - | NC_bounded_ge (nexp1, nexp2) -> NC_bounded_ge (locate_nexp l nexp1, locate_nexp l nexp2) - | NC_bounded_le (nexp1, nexp2) -> NC_bounded_le (locate_nexp l nexp1, locate_nexp l nexp2) - | NC_not_equal (nexp1, nexp2) -> NC_not_equal (locate_nexp l nexp1, locate_nexp l nexp2) - | NC_set (kid, nums) -> NC_set (locate_kid l kid, nums) - | NC_or (nc1, nc2) -> NC_or (locate_nc l nc1, locate_nc l nc2) - | NC_and (nc1, nc2) -> NC_and (locate_nc l nc1, locate_nc l nc2) - | NC_app (id, nexps) -> NC_app (id, List.map (locate_nexp l) nexps) + | NC_equal (nexp1, nexp2) -> NC_equal (locate_nexp f nexp1, locate_nexp f nexp2) + | NC_bounded_ge (nexp1, nexp2) -> NC_bounded_ge (locate_nexp f nexp1, locate_nexp f nexp2) + | NC_bounded_le (nexp1, nexp2) -> NC_bounded_le (locate_nexp f nexp1, locate_nexp f nexp2) + | NC_not_equal (nexp1, nexp2) -> NC_not_equal (locate_nexp f nexp1, locate_nexp f nexp2) + | NC_set (kid, nums) -> NC_set (locate_kid f kid, nums) + | NC_or (nc1, nc2) -> NC_or (locate_nc f nc1, locate_nc f nc2) + | NC_and (nc1, nc2) -> NC_and (locate_nc f nc1, locate_nc f nc2) + | NC_app (id, nexps) -> NC_app (id, List.map (locate_nexp f) nexps) | NC_true -> NC_true | NC_false -> NC_false in - NC_aux (nc_aux, l) + NC_aux (nc_aux, f l) -let rec locate_typ l (Typ_aux (typ_aux, _)) = +let rec locate_typ f (Typ_aux (typ_aux, l)) = let typ_aux = match typ_aux with | Typ_internal_unknown -> Typ_internal_unknown - | Typ_id id -> Typ_id (locate_id l id) - | Typ_var kid -> Typ_var (locate_kid l kid) + | Typ_id id -> Typ_id (locate_id f id) + | Typ_var kid -> Typ_var (locate_kid f kid) | Typ_fn (arg_typs, ret_typ, effect) -> - Typ_fn (List.map (locate_typ l) arg_typs, locate_typ l ret_typ, locate_effect l effect) - | Typ_bidir (typ1, typ2) -> Typ_bidir (locate_typ l typ1, locate_typ l typ2) - | Typ_tup typs -> Typ_tup (List.map (locate_typ l) typs) - | Typ_exist (kids, constr, typ) -> Typ_exist (List.map (locate_kid l) kids, locate_nc l constr, locate_typ l typ) - | Typ_app (id, typ_args) -> Typ_app (locate_id l id, List.map (locate_typ_arg l) typ_args) + Typ_fn (List.map (locate_typ f) arg_typs, locate_typ f ret_typ, locate_effect f effect) + | Typ_bidir (typ1, typ2) -> Typ_bidir (locate_typ f typ1, locate_typ f typ2) + | Typ_tup typs -> Typ_tup (List.map (locate_typ f) typs) + | Typ_exist (kids, constr, typ) -> Typ_exist (List.map (locate_kid f) kids, locate_nc f constr, locate_typ f typ) + | Typ_app (id, typ_args) -> Typ_app (locate_id f id, List.map (locate_typ_arg f) typ_args) in - Typ_aux (typ_aux, l) + Typ_aux (typ_aux, f l) -and locate_typ_arg l (Typ_arg_aux (typ_arg_aux, _)) = +and locate_typ_arg f (Typ_arg_aux (typ_arg_aux, l)) = let typ_arg_aux = match typ_arg_aux with - | Typ_arg_nexp nexp -> Typ_arg_nexp nexp - | Typ_arg_typ typ -> Typ_arg_typ (locate_typ l typ) - | Typ_arg_order ord -> Typ_arg_order ord + | Typ_arg_nexp nexp -> Typ_arg_nexp (locate_nexp f nexp) + | Typ_arg_typ typ -> Typ_arg_typ (locate_typ f typ) + | Typ_arg_order ord -> Typ_arg_order (locate_order f ord) in - Typ_arg_aux (typ_arg_aux, l) + Typ_arg_aux (typ_arg_aux, f l) -let rec locate_typ_pat l (TP_aux (tp_aux, _)) = +let rec locate_typ_pat f (TP_aux (tp_aux, l)) = let tp_aux = match tp_aux with | TP_wild -> TP_wild - | TP_var kid -> TP_var (locate_kid l kid) - | TP_app (id, tps) -> TP_app (locate_id l id, List.map (locate_typ_pat l) tps) + | TP_var kid -> TP_var (locate_kid f kid) + | TP_app (id, tps) -> TP_app (locate_id f id, List.map (locate_typ_pat f) tps) in - TP_aux (tp_aux, l) + TP_aux (tp_aux, f l) -let rec locate_pat : 'a. l -> 'a pat -> 'a pat = fun l (P_aux (p_aux, (_, annot))) -> +let rec locate_pat : 'a. (l -> l) -> 'a pat -> 'a pat = fun f (P_aux (p_aux, (l, annot))) -> let p_aux = match p_aux with - | P_lit lit -> P_lit (locate_lit l lit) + | P_lit lit -> P_lit (locate_lit f lit) | P_wild -> P_wild - | P_or (pat1, pat2) -> P_or (locate_pat l pat1, locate_pat l pat2) - | P_not pat -> P_not (locate_pat l pat) - | P_as (pat, id) -> P_as (locate_pat l pat, locate_id l id) - | P_typ (typ, pat) -> P_typ (locate_typ l typ, locate_pat l pat) - | P_id id -> P_id (locate_id l id) - | P_var (pat, typ_pat) -> P_var (locate_pat l pat, locate_typ_pat l typ_pat) - | P_app (id, pats) -> P_app (locate_id l id, List.map (locate_pat l) pats) - | P_record (fpats, semi) -> P_record (List.map (locate_fpat l) fpats, semi) - | P_vector pats -> P_vector (List.map (locate_pat l) pats) - | P_vector_concat pats -> P_vector_concat (List.map (locate_pat l) pats) - | P_tup pats -> P_tup (List.map (locate_pat l) pats) - | P_list pats -> P_list (List.map (locate_pat l) pats) - | P_cons (hd_pat, tl_pat) -> P_cons (locate_pat l hd_pat, locate_pat l tl_pat) - | P_string_append pats -> P_string_append (List.map (locate_pat l) pats) + | P_or (pat1, pat2) -> P_or (locate_pat f pat1, locate_pat f pat2) + | P_not pat -> P_not (locate_pat f pat) + | P_as (pat, id) -> P_as (locate_pat f pat, locate_id f id) + | P_typ (typ, pat) -> P_typ (locate_typ f typ, locate_pat f pat) + | P_id id -> P_id (locate_id f id) + | P_var (pat, typ_pat) -> P_var (locate_pat f pat, locate_typ_pat f typ_pat) + | P_app (id, pats) -> P_app (locate_id f id, List.map (locate_pat f) pats) + | P_record (fpats, semi) -> P_record (List.map (locate_fpat f) fpats, semi) + | P_vector pats -> P_vector (List.map (locate_pat f) pats) + | P_vector_concat pats -> P_vector_concat (List.map (locate_pat f) pats) + | P_tup pats -> P_tup (List.map (locate_pat f) pats) + | P_list pats -> P_list (List.map (locate_pat f) pats) + | P_cons (hd_pat, tl_pat) -> P_cons (locate_pat f hd_pat, locate_pat f tl_pat) + | P_string_append pats -> P_string_append (List.map (locate_pat f) pats) in - P_aux (p_aux, (l, annot)) + P_aux (p_aux, (f l, annot)) -and locate_fpat : 'a. l -> 'a fpat -> 'a fpat = fun l (FP_aux (FP_Fpat (id, pat), (_, annot))) -> - FP_aux (FP_Fpat (locate_id l id, locate_pat l pat), (l, annot)) +and locate_fpat : 'a. (l -> l) -> 'a fpat -> 'a fpat = fun f (FP_aux (FP_Fpat (id, pat), (l, annot))) -> + FP_aux (FP_Fpat (locate_id f id, locate_pat f pat), (f l, annot)) -let rec locate : 'a. l -> 'a exp -> 'a exp = fun l (E_aux (e_aux, (_, annot))) -> +let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, annot))) -> let e_aux = match e_aux with - | E_block exps -> E_block (List.map (locate l) exps) - | E_nondet exps -> E_nondet (List.map (locate l) exps) - | E_id id -> E_id (locate_id l id) - | E_lit lit -> E_lit (locate_lit l lit) - | E_cast (typ, exp) -> E_cast (locate_typ l typ, locate l exp) - | E_app (f, exps) -> E_app (locate_id l f, List.map (locate l) exps) - | E_app_infix (exp1, op, exp2) -> E_app_infix (locate l exp1, locate_id l op, locate l exp2) - | E_tuple exps -> E_tuple (List.map (locate l) exps) - | E_if (cond_exp, then_exp, else_exp) -> E_if (locate l cond_exp, locate l then_exp, locate l else_exp) - | E_loop (loop, cond, body) -> E_loop (loop, locate l cond, locate l body) + | E_block exps -> E_block (List.map (locate f) exps) + | E_nondet exps -> E_nondet (List.map (locate f) exps) + | E_id id -> E_id (locate_id f id) + | E_lit lit -> E_lit (locate_lit f lit) + | E_cast (typ, exp) -> E_cast (locate_typ f typ, locate f exp) + | E_app (id, exps) -> E_app (locate_id f id, List.map (locate f) exps) + | E_app_infix (exp1, op, exp2) -> E_app_infix (locate f exp1, locate_id f op, locate f exp2) + | E_tuple exps -> E_tuple (List.map (locate f) exps) + | E_if (cond_exp, then_exp, else_exp) -> E_if (locate f cond_exp, locate f then_exp, locate f else_exp) + | E_loop (loop, cond, body) -> E_loop (loop, locate f cond, locate f body) | E_for (id, exp1, exp2, exp3, ord, exp4) -> - E_for (locate_id l id, locate l exp1, locate l exp2, locate l exp3, ord, locate l exp4) - | E_vector exps -> E_vector (List.map (locate l) exps) - | E_vector_access (exp1, exp2) -> E_vector_access (locate l exp1, locate l exp2) - | E_vector_subrange (exp1, exp2, exp3) -> E_vector_subrange (locate l exp1, locate l exp2, locate l exp3) - | E_vector_update (exp1, exp2, exp3) -> E_vector_update (locate l exp1, locate l exp2, locate l exp3) + E_for (locate_id f id, locate f exp1, locate f exp2, locate f exp3, ord, locate f exp4) + | E_vector exps -> E_vector (List.map (locate f) exps) + | E_vector_access (exp1, exp2) -> E_vector_access (locate f exp1, locate f exp2) + | E_vector_subrange (exp1, exp2, exp3) -> E_vector_subrange (locate f exp1, locate f exp2, locate f exp3) + | E_vector_update (exp1, exp2, exp3) -> E_vector_update (locate f exp1, locate f exp2, locate f exp3) | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> - E_vector_update_subrange (locate l exp1, locate l exp2, locate l exp3, locate l exp4) + E_vector_update_subrange (locate f exp1, locate f exp2, locate f exp3, locate f exp4) | E_vector_append (exp1, exp2) -> - E_vector_append (locate l exp1, locate l exp2) - | E_list exps -> E_list (List.map (locate l) exps) - | E_cons (exp1, exp2) -> E_cons (locate l exp1, locate l exp2) - | E_record fexps -> E_record (locate_fexps l fexps) - | E_record_update (exp, fexps) -> E_record_update (locate l exp, locate_fexps l fexps) - | E_field (exp, id) -> E_field (locate l exp, locate_id l id) - | E_case (exp, cases) -> E_case (locate l exp, List.map (locate_pexp l) cases) - | E_let (letbind, exp) -> E_let (locate_letbind l letbind, locate l exp) - | E_assign (lexp, exp) -> E_assign (locate_lexp l lexp, locate l exp) - | E_sizeof nexp -> E_sizeof (locate_nexp l nexp) - | E_return exp -> E_return (locate l exp) - | E_exit exp -> E_exit (locate l exp) - | E_ref id -> E_ref (locate_id l id) - | E_throw exp -> E_throw (locate l exp) - | E_try (exp, cases) -> E_try (locate l exp, List.map (locate_pexp l) cases) - | E_assert (exp, message) -> E_assert (locate l exp, locate l message) - | E_constraint constr -> E_constraint (locate_nc l constr) - | E_var (lexp, exp1, exp2) -> E_var (locate_lexp l lexp, locate l exp1, locate l exp2) - | E_internal_plet (pat, exp1, exp2) -> E_internal_plet (locate_pat l pat, locate l exp1, locate l exp2) - | E_internal_return exp -> E_internal_return (locate l exp) + E_vector_append (locate f exp1, locate f exp2) + | E_list exps -> E_list (List.map (locate f) exps) + | E_cons (exp1, exp2) -> E_cons (locate f exp1, locate f exp2) + | E_record fexps -> E_record (locate_fexps f fexps) + | E_record_update (exp, fexps) -> E_record_update (locate f exp, locate_fexps f fexps) + | E_field (exp, id) -> E_field (locate f exp, locate_id f id) + | E_case (exp, cases) -> E_case (locate f exp, List.map (locate_pexp f) cases) + | E_let (letbind, exp) -> E_let (locate_letbind f letbind, locate f exp) + | E_assign (lexp, exp) -> E_assign (locate_lexp f lexp, locate f exp) + | E_sizeof nexp -> E_sizeof (locate_nexp f nexp) + | E_return exp -> E_return (locate f exp) + | E_exit exp -> E_exit (locate f exp) + | E_ref id -> E_ref (locate_id f id) + | E_throw exp -> E_throw (locate f exp) + | E_try (exp, cases) -> E_try (locate f exp, List.map (locate_pexp f) cases) + | E_assert (exp, message) -> E_assert (locate f exp, locate f message) + | E_constraint constr -> E_constraint (locate_nc f constr) + | E_var (lexp, exp1, exp2) -> E_var (locate_lexp f lexp, locate f exp1, locate f exp2) + | E_internal_plet (pat, exp1, exp2) -> E_internal_plet (locate_pat f pat, locate f exp1, locate f exp2) + | E_internal_return exp -> E_internal_return (locate f exp) | E_internal_value value -> E_internal_value value in - E_aux (e_aux, (l, annot)) + E_aux (e_aux, (f l, annot)) -and locate_letbind : 'a. l -> 'a letbind -> 'a letbind = fun l (LB_aux (LB_val (pat, exp), (_, annot))) -> - LB_aux (LB_val (locate_pat l pat, locate l exp), (l, annot)) +and locate_letbind : 'a. (l -> l) -> 'a letbind -> 'a letbind = fun f (LB_aux (LB_val (pat, exp), (l, annot))) -> + LB_aux (LB_val (locate_pat f pat, locate f exp), (f l, annot)) -and locate_pexp : 'a. l -> 'a pexp -> 'a pexp = fun l (Pat_aux (pexp_aux, (_, annot))) -> +and locate_pexp : 'a. (l -> l) -> 'a pexp -> 'a pexp = fun f (Pat_aux (pexp_aux, (l, annot))) -> let pexp_aux = match pexp_aux with - | Pat_exp (pat, exp) -> Pat_exp (locate_pat l pat, locate l exp) - | Pat_when (pat, guard, exp) -> Pat_when (locate_pat l pat, locate l guard, locate l exp) + | Pat_exp (pat, exp) -> Pat_exp (locate_pat f pat, locate f exp) + | Pat_when (pat, guard, exp) -> Pat_when (locate_pat f pat, locate f guard, locate f exp) in - Pat_aux (pexp_aux, (l, annot)) + Pat_aux (pexp_aux, (f l, annot)) -and locate_lexp : 'a. l -> 'a lexp -> 'a lexp = fun l (LEXP_aux (lexp_aux, (_, annot))) -> +and locate_lexp : 'a. (l -> l) -> 'a lexp -> 'a lexp = fun f (LEXP_aux (lexp_aux, (l, annot))) -> let lexp_aux = match lexp_aux with - | LEXP_id id -> LEXP_id (locate_id l id) - | LEXP_deref exp -> LEXP_deref (locate l exp) - | LEXP_memory (id, exps) -> LEXP_memory (locate_id l id, List.map (locate l) exps) - | LEXP_cast (typ, id) -> LEXP_cast (locate_typ l typ, locate_id l id) - | LEXP_tup lexps -> LEXP_tup (List.map (locate_lexp l) lexps) - | LEXP_vector_concat lexps -> LEXP_vector_concat (List.map (locate_lexp l) lexps) - | LEXP_vector (lexp, exp) -> LEXP_vector (locate_lexp l lexp, locate l exp) - | LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (locate_lexp l lexp, locate l exp1, locate l exp2) - | LEXP_field (lexp, id) -> LEXP_field (locate_lexp l lexp, locate_id l id) + | LEXP_id id -> LEXP_id (locate_id f id) + | LEXP_deref exp -> LEXP_deref (locate f exp) + | LEXP_memory (id, exps) -> LEXP_memory (locate_id f id, List.map (locate f) exps) + | LEXP_cast (typ, id) -> LEXP_cast (locate_typ f typ, locate_id f id) + | LEXP_tup lexps -> LEXP_tup (List.map (locate_lexp f) lexps) + | LEXP_vector_concat lexps -> LEXP_vector_concat (List.map (locate_lexp f) lexps) + | LEXP_vector (lexp, exp) -> LEXP_vector (locate_lexp f lexp, locate f exp) + | LEXP_vector_range (lexp, exp1, exp2) -> LEXP_vector_range (locate_lexp f lexp, locate f exp1, locate f exp2) + | LEXP_field (lexp, id) -> LEXP_field (locate_lexp f lexp, locate_id f id) in - LEXP_aux (lexp_aux, (l, annot)) + LEXP_aux (lexp_aux, (f l, annot)) + +and locate_fexps : 'a. (l -> l) -> 'a fexps -> 'a fexps = fun f (FES_aux (FES_Fexps (fexps, semi), (l, annot))) -> + FES_aux (FES_Fexps (List.map (locate_fexp f) fexps, semi), (f l, annot)) + +and locate_fexp : 'a. (l -> l) -> 'a fexp -> 'a fexp = fun f (FE_aux (FE_Fexp (id, exp), (l, annot))) -> + FE_aux (FE_Fexp (locate_id f id, locate f exp), (f l, annot)) -and locate_fexps : 'a. l -> 'a fexps -> 'a fexps = fun l (FES_aux (FES_Fexps (fexps, semi), (_, annot))) -> - FES_aux (FES_Fexps (List.map (locate_fexp l) fexps, semi), (l, annot)) +let unique_ref = ref 0 -and locate_fexp : 'a. l -> 'a fexp -> 'a fexp = fun l (FE_aux (FE_Fexp (id, exp), (_, annot))) -> - FE_aux (FE_Fexp (locate_id l id, locate l exp), (l, annot)) +let unique l = + let l = Parse_ast.Unique (!unique_ref, l) in + incr unique_ref; + l (**************************************************************************) (* 1. Substitutions *) -- cgit v1.2.3 From c54f60b713087e33758c63dc110fe02d3fea29c9 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 1 Nov 2018 17:26:01 +0000 Subject: Changes to enable analysing type errors in ASL parser Also some pretty printer improvements Make all the tests use the same colours for green/red/yellow --- src/ast_util.ml | 44 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index 3cd2f361..61bc9ba3 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -270,6 +270,47 @@ and nexp_simp_aux = function end | nexp -> nexp +let rec constraint_simp (NC_aux (nc_aux, l)) = + let nc_aux = match nc_aux with + | NC_equal (nexp1, nexp2) -> + let nexp1, nexp2 = nexp_simp nexp1, nexp_simp nexp2 in + if nexp_identical nexp1 nexp2 then + NC_true + else + NC_equal (nexp1, nexp2) + + | NC_and (nc1, nc2) -> + let nc1, nc2 = constraint_simp nc1, constraint_simp nc2 in + begin match nc1, nc2 with + | NC_aux (NC_true, _), NC_aux (nc, _) -> nc + | NC_aux (nc, _), NC_aux (NC_true, _) -> nc + | _, _ -> NC_and (nc1, nc2) + end + + | NC_or (nc1, nc2) -> + let nc1, nc2 = constraint_simp nc1, constraint_simp nc2 in + begin match nc1, nc2 with + | NC_aux (NC_false, _), NC_aux (nc, _) -> nc + | NC_aux (nc, _), NC_aux (NC_false, _) -> nc + | NC_aux (NC_true, _), NC_aux (nc, _) -> NC_true + | NC_aux (nc, _), NC_aux (NC_true, _) -> NC_true + | _, _ -> NC_or (nc1, nc2) + end + + | _ -> nc_aux + in + NC_aux (nc_aux, l) + +let rec constraint_conj (NC_aux (nc_aux, l) as nc) = + match nc_aux with + | NC_and (nc1, nc2) -> constraint_conj nc1 @ constraint_conj nc2 + | _ -> [nc] + +let rec constraint_disj (NC_aux (nc_aux, l) as nc) = + match nc_aux with + | NC_or (nc1, nc2) -> constraint_disj nc1 @ constraint_disj nc2 + | _ -> [nc] + let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown) let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown) @@ -618,9 +659,10 @@ and string_of_typ_aux = function | Typ_id id -> string_of_id id | Typ_var kid -> string_of_kid kid | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")" + | Typ_app (id, args) when Id.compare id (mk_id "atom") = 0 -> "int(" ^ string_of_list ", " string_of_typ_arg args ^ ")" | Typ_app (id, args) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")" | Typ_fn ([typ_arg], typ_ret, eff) -> - string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff + string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff | Typ_fn (typ_args, typ_ret, eff) -> "(" ^ string_of_list ", " string_of_typ typ_args ^ ") -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff -- cgit v1.2.3 From 21e94e35b56b86d56b720ac2a38d22020f41fc19 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 5 Nov 2018 16:55:13 +0000 Subject: Ensure type-synonyms are handled correctly in register dependencies We need to ensure that we expand type-synonyms when calculating which types a register depends on during topological sorting in order to place the undefined_type function in the correct place, even when type is indirected through a function. --- src/ast_util.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index 61bc9ba3..f0b6508b 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -888,6 +888,13 @@ let id_of_type_def (TD_aux (td_aux, _)) = id_of_type_def_aux td_aux let id_of_val_spec (VS_aux (VS_val_spec (_, id, _, _), _)) = id +let id_of_dec_spec (DEC_aux (ds_aux, _)) = + match ds_aux with + | DEC_reg (_, id) -> id + | DEC_config (id, _, _) -> id + | DEC_alias (id, _) -> id + | DEC_typ_alias (_, id, _) -> id + let ids_of_def = function | DEF_kind (KD_aux (KD_nabbrev (_, id, _, _), _)) -> IdSet.singleton id | DEF_type td -> IdSet.singleton (id_of_type_def td) -- cgit v1.2.3 From c631ae96bbe9d659a8b3dbb1fc0c7ac812c2d43f Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 15 Nov 2018 15:13:06 +0000 Subject: ast_utils: simplify numeric constraints in inequalities. --- src/ast_util.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index f0b6508b..71b3299a 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -296,7 +296,10 @@ let rec constraint_simp (NC_aux (nc_aux, l)) = | NC_aux (nc, _), NC_aux (NC_true, _) -> NC_true | _, _ -> NC_or (nc1, nc2) end - + | NC_bounded_ge (nexp1, nexp2) -> + NC_bounded_ge (nexp_simp nexp1, nexp_simp nexp2) + | NC_bounded_le (nexp1, nexp2) -> + NC_bounded_le (nexp_simp nexp1, nexp_simp nexp2) | _ -> nc_aux in NC_aux (nc_aux, l) -- cgit v1.2.3 From 626c68dad5ea79da7776b4628e5ae22ca742669e Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 16 Nov 2018 18:28:17 +0000 Subject: Canonicalise functions types in val specs This brings Sail closer to MiniSail, and means that type my_range 'n 'm = {'o, 'n <= 'o <= 'm. int('o)} will work on the left hand side of a function type in the same way as a regular built-in range type. This means that in principle neither range nor int need be built-in types, as both can be implemented in terms of int('n) (atom internally). It also means we can easily identify type variables that need to be made into implict arguments, with the criterion for that being simply any type variable that doesn't appear in a base type on the LHS of the function, or only appears on the RHS. --- src/ast_util.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index f0b6508b..037fd1a7 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -399,6 +399,13 @@ let mk_effect effs = let no_effect = mk_effect [] +let quant_add qi typq = + match qi, typq with + | QI_aux (QI_const (NC_aux (NC_true, _)), _), _ -> typq + | QI_aux (QI_id _, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qi :: qis), l) + | QI_aux (QI_const nc, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qis @ [qi]), l) + | _, TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_tq [qi], l) + let quant_items : typquant -> quant_item list = function | TypQ_aux (TypQ_tq qis, _) -> qis | TypQ_aux (TypQ_no_forall, _) -> [] -- cgit v1.2.3 From 666062ce4d97fe48307d1feb5bb4eb32087b177a Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 30 Nov 2018 19:33:50 +0000 Subject: Remove constraint synonyms They weren't needed for ASL parser like I thought they would be, and they increase the complexity of dealing with constraints throughout Sail, so just remove them. Also fix some compiler warnings --- src/ast_util.ml | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index d61c96ed..14638b88 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -387,8 +387,6 @@ let rec nc_negate (NC_aux (nc, l)) = | NC_set (kid, [int]) -> nc_neq (nvar kid) (nconstant int) | NC_set (kid, int :: ints) -> mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints))))) - | NC_app _ -> - raise (Reporting.err_unreachable l __POS__ "tried to negate constraint with unexpanded synonym") let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown) @@ -581,8 +579,8 @@ let def_loc = function | DEF_reg_dec (DEC_aux (_, (l, _))) | DEF_fixity (_, _, Id_aux (_, l)) | DEF_overload (Id_aux (_, l), _) -> l - | DEF_constraint (Id_aux (_, l), _, _) -> l | DEF_internal_mutrec _ -> Parse_ast.Unknown + | DEF_pragma (_, _, l) -> l let string_of_id = function | Id_aux (Id v, _) -> v @@ -696,8 +694,6 @@ and string_of_n_constraint = function "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_set (kid, ns), _) -> string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}" - | NC_aux (NC_app (id, nexps), _) -> - "where " ^ string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_nexp nexps ^ ")" | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" @@ -954,8 +950,6 @@ module NC = struct | NC_or (nc1,nc2), NC_or (nc3,nc4) | NC_and (nc1,nc2), NC_and (nc3,nc4) -> lex_ord compare compare nc1 nc3 nc2 nc4 - | NC_app (id1, nexps1), NC_app (id2, nexps2) - -> lex_ord (Id.compare) (Util.compare_list Nexp.compare) id1 id2 nexps1 nexps2 | NC_true, NC_true | NC_false, NC_false -> 0 @@ -966,7 +960,6 @@ module NC = struct | NC_set _, _ -> -1 | _, NC_set _ -> 1 | NC_or _, _ -> -1 | _, NC_or _ -> 1 | NC_and _, _ -> -1 | _, NC_and _ -> 1 - | NC_app _, _ -> -1 | _, NC_app _ -> 1 | NC_true, _ -> -1 | _, NC_true -> 1 end @@ -1152,8 +1145,6 @@ let rec tyvars_of_constraint (NC_aux (nc, _)) = | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> KidSet.union (tyvars_of_constraint nc1) (tyvars_of_constraint nc2) - | NC_app (id, nexps) -> - List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_nexp nexps) | NC_true | NC_false -> KidSet.empty @@ -1421,7 +1412,6 @@ let rec locate_nc f (NC_aux (nc_aux, l)) = | NC_set (kid, nums) -> NC_set (locate_kid f kid, nums) | NC_or (nc1, nc2) -> NC_or (locate_nc f nc1, locate_nc f nc2) | NC_and (nc1, nc2) -> NC_and (locate_nc f nc1, locate_nc f nc2) - | NC_app (id, nexps) -> NC_app (id, List.map (locate_nexp f) nexps) | NC_true -> NC_true | NC_false -> NC_false in @@ -1596,7 +1586,6 @@ and nc_subst_nexp_aux l sv subst = function else set_nc | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2) | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2) - | NC_app (id, nexps) -> NC_app (id, List.map (nexp_subst sv subst) nexps) | NC_false -> NC_false | NC_true -> NC_true -- cgit v1.2.3 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. --- src/ast_util.ml | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) (limited to 'src/ast_util.ml') 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 -- cgit v1.2.3 From df3ea2e6da387ead7cba1e27632768e563696502 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 4 Dec 2018 14:53:23 +0000 Subject: Remove FES_Fexps constructor This makes dealing with records and field expressions in Sail much nicer because the constructors are no longer stacked together like matryoshka dolls with unnecessary layers. Previously to get the fields of a record it would be either E_aux (E_record (FES_aux (FES_Fexps (fexps, _), _)), _) but now it is simply: E_aux (E_record fexps, _) --- src/ast_util.ml | 25 ++++++++----------------- 1 file changed, 8 insertions(+), 17 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index ffe4c90e..48750ab7 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -393,7 +393,6 @@ let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown let mk_typquant qis = TypQ_aux (TypQ_tq qis, Parse_ast.Unknown) let mk_fexp id exp = FE_aux (FE_Fexp (id, exp), no_annot) -let mk_fexps fexps = FES_aux (FES_Fexps (fexps, false), no_annot) let mk_effect effs = Effect_aux (Effect_set (List.map (fun be_aux -> BE_aux (be_aux, Parse_ast.Unknown)) effs), Parse_ast.Unknown) @@ -461,8 +460,8 @@ and map_exp_annot_aux f = function | E_vector_append (exp1, exp2) -> E_vector_append (map_exp_annot f exp1, map_exp_annot f exp2) | E_list xs -> E_list (List.map (map_exp_annot f) xs) | E_cons (exp1, exp2) -> E_cons (map_exp_annot f exp1, map_exp_annot f exp2) - | E_record fexps -> E_record (map_fexps_annot f fexps) - | E_record_update (exp, fexps) -> E_record_update (map_exp_annot f exp, map_fexps_annot f fexps) + | E_record fexps -> E_record (List.map (map_fexp_annot f) fexps) + | E_record_update (exp, fexps) -> E_record_update (map_exp_annot f exp, List.map (map_fexp_annot f) fexps) | E_field (exp, id) -> E_field (map_exp_annot f exp, id) | E_case (exp, cases) -> E_case (map_exp_annot f exp, List.map (map_pexp_annot f) cases) | E_try (exp, cases) -> E_try (map_exp_annot f exp, List.map (map_pexp_annot f) cases) @@ -482,7 +481,6 @@ and map_opt_default_annot f (Def_val_aux (df, annot)) = Def_val_aux (map_opt_def and map_opt_default_annot_aux f = function | Def_val_empty -> Def_val_empty | Def_val_dec exp -> Def_val_dec (map_exp_annot f exp) -and map_fexps_annot f (FES_aux (FES_Fexps (fexps, b), annot)) = FES_aux (FES_Fexps (List.map (map_fexp_annot f) fexps, b), f annot) and map_fexp_annot f (FE_aux (FE_Fexp (id, exp), annot)) = FE_aux (FE_Fexp (id, map_exp_annot f exp), f annot) and map_pexp_annot f (Pat_aux (pexp, annot)) = Pat_aux (map_pexp_annot_aux f pexp, f annot) and map_pexp_annot_aux f = function @@ -770,9 +768,9 @@ let rec string_of_exp (E_aux (exp, _)) = | E_throw exp -> "throw " ^ string_of_exp exp | E_cons (x, xs) -> string_of_exp x ^ " :: " ^ string_of_exp xs | E_list xs -> "[|" ^ string_of_list ", " string_of_exp xs ^ "|]" - | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) -> + | E_record_update (exp, fexps) -> "{ " ^ string_of_exp exp ^ " with " ^ string_of_list "; " string_of_fexp fexps ^ " }" - | E_record (FES_aux (FES_Fexps (fexps, _), _)) -> + | E_record fexps -> "{ " ^ string_of_list "; " string_of_fexp fexps ^ " }" | E_var (lexp, binding, exp) -> "var " ^ string_of_lexp lexp ^ " = " ^ string_of_exp binding ^ " in " ^ string_of_exp exp | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")" @@ -1290,8 +1288,8 @@ let rec subst id value (E_aux (e_aux, annot) as exp) = | E_list exps -> E_list (List.map (subst id value) exps) | E_cons (exp1, exp2) -> E_cons (subst id value exp1, subst id value exp2) - | E_record fexps -> E_record (subst_fexps id value fexps) - | E_record_update (exp, fexps) -> E_record_update (subst id value exp, subst_fexps id value fexps) + | E_record fexps -> E_record (List.map (subst_fexp id value) fexps) + | E_record_update (exp, fexps) -> E_record_update (subst id value exp, List.map (subst_fexp id value) fexps) | E_field (exp, id') -> E_field (subst id value exp, id') | E_case (exp, pexps) -> @@ -1336,10 +1334,6 @@ and subst_pexp id value (Pat_aux (pexp_aux, annot)) = in Pat_aux (pexp_aux, annot) - -and subst_fexps id value (FES_aux (FES_Fexps (fexps, flag), annot)) = - FES_aux (FES_Fexps (List.map (subst_fexp id value) fexps, flag), annot) - and subst_fexp id value (FE_aux (FE_Fexp (id', exp), annot)) = FE_aux (FE_Fexp (id', subst id value exp), annot) @@ -1493,8 +1487,8 @@ let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, ann E_vector_append (locate f exp1, locate f exp2) | E_list exps -> E_list (List.map (locate f) exps) | E_cons (exp1, exp2) -> E_cons (locate f exp1, locate f exp2) - | E_record fexps -> E_record (locate_fexps f fexps) - | E_record_update (exp, fexps) -> E_record_update (locate f exp, locate_fexps f fexps) + | E_record fexps -> E_record (List.map (locate_fexp f) fexps) + | E_record_update (exp, fexps) -> E_record_update (locate f exp, List.map (locate_fexp f) fexps) | E_field (exp, id) -> E_field (locate f exp, locate_id f id) | E_case (exp, cases) -> E_case (locate f exp, List.map (locate_pexp f) cases) | E_let (letbind, exp) -> E_let (locate_letbind f letbind, locate f exp) @@ -1538,9 +1532,6 @@ and locate_lexp : 'a. (l -> l) -> 'a lexp -> 'a lexp = fun f (LEXP_aux (lexp_aux in LEXP_aux (lexp_aux, (f l, annot)) -and locate_fexps : 'a. (l -> l) -> 'a fexps -> 'a fexps = fun f (FES_aux (FES_Fexps (fexps, semi), (l, annot))) -> - FES_aux (FES_Fexps (List.map (locate_fexp f) fexps, semi), (f l, annot)) - and locate_fexp : 'a. (l -> l) -> 'a fexp -> 'a fexp = fun f (FE_aux (FE_Fexp (id, exp), (l, annot))) -> FE_aux (FE_Fexp (locate_id f id, locate f exp), (f l, annot)) -- cgit v1.2.3 From 272d9565ef7f48baa0982a291c7fde8497ab0cd9 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 5 Dec 2018 20:49:38 +0000 Subject: Re-factor initial check Mostly this is to change how we desugar types in order to make us more flexible with what we can parse as a valid constraint as type. Previously the structure of the initial check forced some awkward limitations on what was parseable due to how the parse AST is set up. As part of this, I've taken the de-scattering of scattered functions out of the initial check, and moved it to a re-writing step after type-checking, where I think it logically belongs. This doesn't change much right now, but opens up some more possibilities in the future: Since scattered functions are now typechecked normally, any future module system for Sail would be able to handle them specially, and the Latex documentation backend can now document scattered functions explicitly, rather than relying on hackish 'de-scattering' logic to present documentation as the functions originally appeared. This has one slight breaking change which is that union clauses must appear before their uses in scattered functions, so union ast = Foo : unit function clause execute(Foo()) is ok, but function clause execute(Foo()) union ast = Foo : unit is not. Previously this worked because the de-scattering moved union clauses upwards before type-checking, but as this now happens after type-checking they must appear in the correct order. This doesn't occur in ARM, RISC-V, MIPS, but did appear in Cheri and I submitted a pull request to re-order the places where it happens. --- src/ast_util.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index 48750ab7..e9153f7a 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -436,6 +436,7 @@ let quant_map_items f = function let unaux_nexp (Nexp_aux (nexp, _)) = nexp let unaux_order (Ord_aux (ord, _)) = ord let unaux_typ (Typ_aux (typ, _)) = typ +let unaux_kind (K_aux (k, _)) = k let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f annot) and map_exp_annot_aux f = function -- cgit v1.2.3 From 2c25110ad2f5e636239ba65a2154aae79ffa253c Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 7 Dec 2018 21:53:29 +0000 Subject: Working on better flow typing for ASL On a new branch because it's completely broken everything for now --- src/ast_util.ml | 168 ++++++++++++++++++++++++++------------------------------ 1 file changed, 77 insertions(+), 91 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index e9153f7a..788008d1 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -370,23 +370,16 @@ let nc_lt n1 n2 = nc_lteq (nsum n1 (nint 1)) n2 let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nint 1)) let nc_and nc1 nc2 = mk_nc (NC_and (nc1, nc2)) let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2)) +let nc_var kid = mk_nc (NC_var kid) let nc_true = mk_nc NC_true let nc_false = mk_nc NC_false -let rec nc_negate (NC_aux (nc, l)) = - match nc with - | NC_bounded_ge (n1, n2) -> nc_lt n1 n2 - | NC_bounded_le (n1, n2) -> nc_gt n1 n2 - | NC_equal (n1, n2) -> nc_neq n1 n2 - | NC_not_equal (n1, n2) -> nc_eq n1 n2 - | NC_and (n1, n2) -> mk_nc (NC_or (nc_negate n1, nc_negate n2)) - | NC_or (n1, n2) -> mk_nc (NC_and (nc_negate n1, nc_negate n2)) - | NC_false -> mk_nc NC_true - | NC_true -> mk_nc NC_false - | NC_set (kid, []) -> nc_false - | NC_set (kid, [int]) -> nc_neq (nvar kid) (nconstant int) - | NC_set (kid, int :: ints) -> - mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints))))) +let arg_nexp ?loc:(l=Parse_ast.Unknown) n = Typ_arg_aux (Typ_arg_nexp n, l) +let arg_order ?loc:(l=Parse_ast.Unknown) ord = Typ_arg_aux (Typ_arg_order ord, l) +let arg_typ ?loc:(l=Parse_ast.Unknown) typ = Typ_arg_aux (Typ_arg_typ typ, l) +let arg_bool ?loc:(l=Parse_ast.Unknown) nc = Typ_arg_aux (Typ_arg_bool nc, l) + +let nc_not nc = mk_nc (NC_app (mk_id "not", [arg_bool nc])) let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown) @@ -437,6 +430,7 @@ let unaux_nexp (Nexp_aux (nexp, _)) = nexp let unaux_order (Ord_aux (ord, _)) = ord let unaux_typ (Typ_aux (typ, _)) = typ let unaux_kind (K_aux (k, _)) = k +let unaux_constraint (NC_aux (nc, _)) = nc let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f annot) and map_exp_annot_aux f = function @@ -628,6 +622,7 @@ let string_of_kind_aux = function | K_type -> "Type" | K_int -> "Int" | K_order -> "Order" + | K_bool -> "Bool" let string_of_kind (K_aux (k, _)) = string_of_kind_aux k @@ -680,6 +675,7 @@ and string_of_typ_arg_aux = function | Typ_arg_nexp n -> string_of_nexp n | Typ_arg_typ typ -> string_of_typ typ | Typ_arg_order o -> string_of_order o + | Typ_arg_bool nc -> string_of_n_constraint nc and string_of_n_constraint = function | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2 @@ -691,6 +687,8 @@ and string_of_n_constraint = function "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_set (kid, ns), _) -> string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}" + | NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")" + | NC_aux (NC_var v, _) -> string_of_kid v | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" @@ -1142,10 +1140,13 @@ let rec tyvars_of_constraint (NC_aux (nc, _)) = | NC_or (nc1, nc2) | NC_and (nc1, nc2) -> KidSet.union (tyvars_of_constraint nc1) (tyvars_of_constraint nc2) + | NC_app (id, args) -> + List.fold_left (fun s t -> KidSet.union s (tyvars_of_typ_arg t)) KidSet.empty args + | NC_var kid -> KidSet.singleton kid | NC_true | NC_false -> KidSet.empty -let rec tyvars_of_typ (Typ_aux (t,_)) = +and tyvars_of_typ (Typ_aux (t,_)) = match t with | Typ_internal_unknown -> KidSet.empty | Typ_id _ -> KidSet.empty @@ -1166,6 +1167,7 @@ and tyvars_of_typ_arg (Typ_arg_aux (ta,_)) = | Typ_arg_nexp nexp -> tyvars_of_nexp nexp | Typ_arg_typ typ -> tyvars_of_typ typ | Typ_arg_order _ -> KidSet.empty + | Typ_arg_bool nc -> tyvars_of_constraint nc let tyvars_of_quant_item (QI_aux (qi, _)) = match qi with | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) -> @@ -1547,10 +1549,26 @@ let unique l = (* 1. Substitutions *) (**************************************************************************) +let order_subst_aux sv subst = function + | Ord_var kid -> + begin match subst with + | Typ_arg_aux (Typ_arg_order ord, _) when Kid.compare kid sv = 0 -> + unaux_order ord + | _ -> Ord_var kid + end + | Ord_inc -> Ord_inc + | Ord_dec -> Ord_dec + +let order_subst sv subst (Ord_aux (ord, l)) = Ord_aux (order_subst_aux sv subst ord, l) + let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv subst nexp, l) and nexp_subst_aux sv subst = function - | Nexp_id v -> Nexp_id v - | Nexp_var kid -> if Kid.compare kid sv = 0 then subst else Nexp_var kid + | Nexp_var kid -> + begin match subst with + | Typ_arg_aux (Typ_arg_nexp n, _) when Kid.compare kid sv = 0 -> unaux_nexp n + | _ -> Nexp_var kid + end + | Nexp_id id -> Nexp_id id | Nexp_constant c -> Nexp_constant c | Nexp_times (nexp1, nexp2) -> Nexp_times (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) | Nexp_sum (nexp1, nexp2) -> Nexp_sum (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) @@ -1564,100 +1582,68 @@ let rec nexp_set_to_or l subst = function | [int] -> NC_equal (subst, nconstant int) | (int :: ints) -> NC_or (mk_nc (NC_equal (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints)) -let rec nc_subst_nexp sv subst (NC_aux (nc, l)) = NC_aux (nc_subst_nexp_aux l sv subst nc, l) -and nc_subst_nexp_aux l sv subst = function +let rec constraint_subst sv subst (NC_aux (nc, l)) = NC_aux (constraint_subst_aux l sv subst nc, l) +and constraint_subst_aux l sv subst = function | NC_equal (n1, n2) -> NC_equal (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_set (kid, ints) as set_nc -> - if Kid.compare kid sv = 0 - then nexp_set_to_or l (mk_nexp subst) ints - else set_nc - | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2) - | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2) + begin match subst with + | Typ_arg_aux (Typ_arg_nexp n, _) when Kid.compare kid sv = 0 -> + nexp_set_to_or l n ints + | _ -> set_nc + end + | NC_or (nc1, nc2) -> NC_or (constraint_subst sv subst nc1, constraint_subst sv subst nc2) + | NC_and (nc1, nc2) -> NC_and (constraint_subst sv subst nc1, constraint_subst sv subst nc2) + | NC_app (id, args) -> NC_app (id, List.map (typ_arg_subst sv subst) args) + | NC_var kid -> + begin match subst with + | Typ_arg_aux (Typ_arg_bool nc, _) when Kid.compare kid sv = 0 -> + unaux_constraint nc + | _ -> NC_var kid + end | NC_false -> NC_false | NC_true -> NC_true -let rec typ_subst_nexp sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_nexp_aux sv subst typ, l) -and typ_subst_nexp_aux sv subst = function +and typ_subst sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_aux sv subst typ, l) +and typ_subst_aux sv subst = function | Typ_internal_unknown -> Typ_internal_unknown | Typ_id v -> Typ_id v - | Typ_var kid -> Typ_var kid - | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_nexp sv subst) arg_typs, typ_subst_nexp sv subst ret_typ, effs) - | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2) - | Typ_tup typs -> Typ_tup (List.map (typ_subst_nexp sv subst) typs) - | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args) + | Typ_var kid -> + begin match subst with + | Typ_arg_aux (Typ_arg_typ typ, _) when Kid.compare kid sv = 0 -> + unaux_typ typ + | _ -> Typ_var kid + end + | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst sv subst) arg_typs, typ_subst sv subst ret_typ, effs) + | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst sv subst typ1, typ_subst sv subst typ2) + | Typ_tup typs -> Typ_tup (List.map (typ_subst sv subst) typs) + | Typ_app (f, args) -> Typ_app (f, List.map (typ_arg_subst sv subst) args) | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) - | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv subst nc, typ_subst_nexp sv subst typ) -and typ_subst_arg_nexp sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_nexp_aux sv subst arg, l) -and typ_subst_arg_nexp_aux sv subst = function - | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp) - | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_nexp sv subst typ) - | Typ_arg_order ord -> Typ_arg_order ord + | Typ_exist (kids, nc, typ) -> Typ_exist (kids, constraint_subst sv subst nc, typ_subst sv subst typ) -let rec typ_subst_typ sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_typ_aux sv subst typ, l) -and typ_subst_typ_aux sv subst = function - | Typ_internal_unknown -> Typ_internal_unknown - | Typ_id v -> Typ_id v - | Typ_var kid -> if Kid.compare kid sv = 0 then subst else Typ_var kid - | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_typ sv subst) arg_typs, typ_subst_typ sv subst ret_typ, effs) - | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2) - | Typ_tup typs -> Typ_tup (List.map (typ_subst_typ sv subst) typs) - | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_typ sv subst) args) - | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_typ sv subst typ) -and typ_subst_arg_typ sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_typ_aux sv subst arg, l) -and typ_subst_arg_typ_aux sv subst = function - | Typ_arg_nexp nexp -> Typ_arg_nexp nexp - | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_typ sv subst typ) - | Typ_arg_order ord -> Typ_arg_order ord - -let order_subst_aux sv subst = function - | Ord_var kid -> if Kid.compare kid sv = 0 then subst else Ord_var kid - | Ord_inc -> Ord_inc - | Ord_dec -> Ord_dec - -let order_subst sv subst (Ord_aux (ord, l)) = Ord_aux (order_subst_aux sv subst ord, l) - -let rec typ_subst_order sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_order_aux sv subst typ, l) -and typ_subst_order_aux sv subst = function - | Typ_internal_unknown -> Typ_internal_unknown - | Typ_id v -> Typ_id v - | Typ_var kid -> Typ_var kid - | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_order sv subst) arg_typs, typ_subst_order sv subst ret_typ, effs) - | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2) - | Typ_tup typs -> Typ_tup (List.map (typ_subst_order sv subst) typs) - | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_order sv subst) args) - | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_order sv subst typ) -and typ_subst_arg_order sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_order_aux sv subst arg, l) -and typ_subst_arg_order_aux sv subst = function - | Typ_arg_nexp nexp -> Typ_arg_nexp nexp - | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_order sv subst typ) +and typ_arg_subst sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_arg_subst_aux sv subst arg, l) +and typ_arg_subst_aux sv subst = function + | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp) + | Typ_arg_typ typ -> Typ_arg_typ (typ_subst sv subst typ) | Typ_arg_order ord -> Typ_arg_order (order_subst sv subst ord) + | Typ_arg_bool nc -> Typ_arg_bool (constraint_subst sv subst nc) -let rec typ_subst_kid sv subst (Typ_aux (typ, l)) = Typ_aux (typ_subst_kid_aux sv subst typ, l) -and typ_subst_kid_aux sv subst = function - | Typ_internal_unknown -> Typ_internal_unknown - | Typ_id v -> Typ_id v - | Typ_var kid -> if Kid.compare kid sv = 0 then Typ_var subst else Typ_var kid - | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_kid sv subst) arg_typs, typ_subst_kid sv subst ret_typ, effs) - | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2) - | Typ_tup typs -> Typ_tup (List.map (typ_subst_kid sv subst) typs) - | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_kid sv subst) args) - | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) - | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc_subst_nexp sv (Nexp_var subst) nc, typ_subst_kid sv subst typ) -and typ_subst_arg_kid sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_subst_arg_kid_aux sv subst arg, l) -and typ_subst_arg_kid_aux sv subst = function - | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv (Nexp_var subst) nexp) - | Typ_arg_typ typ -> Typ_arg_typ (typ_subst_kid sv subst typ) - | Typ_arg_order ord -> Typ_arg_order (order_subst sv (Ord_var subst) ord) +let subst_kid subst sv v x = + x + |> subst sv (mk_typ_arg (Typ_arg_bool (nc_var v))) + |> subst sv (mk_typ_arg (Typ_arg_nexp (nvar v))) + |> subst sv (mk_typ_arg (Typ_arg_order (Ord_aux (Ord_var v, Parse_ast.Unknown)))) + |> subst sv (mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var v)))) let quant_item_subst_kid_aux sv subst = function | QI_id (KOpt_aux (KOpt_none kid, l)) as qid -> if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_none subst, l)) else qid | QI_id (KOpt_aux (KOpt_kind (k, kid), l)) as qid -> if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_kind (k, subst), l)) else qid - | QI_const nc -> QI_const (nc_subst_nexp sv (Nexp_var subst) nc) + | QI_const nc -> + QI_const (subst_kid constraint_subst sv subst nc) let quant_item_subst_kid sv subst (QI_aux (quant, l)) = QI_aux (quant_item_subst_kid_aux sv subst quant, l) -- cgit v1.2.3 From d8f0854ca9d80d3af8d6a4aaec778643eda9421c Mon Sep 17 00:00:00 2001 From: Alasdair Date: Sat, 8 Dec 2018 01:06:28 +0000 Subject: Compiling again Change Typ_arg_ to A_. We use it a lot more now typ_arg is used instead of uvar as the result of unify. Plus A_ could either stand for argument, or Any/A type which is quite appropriate in most use cases. Restore instantiation info in infer_funapp'. Ideally we would save this instead of recomputing it ever time we need it. However I checked and there are over 300 places in the code that would need to be changed to add an extra argument to E_app. Still some issues causing specialisation to fail however. Improve the error message when we swap how we infer/check an l-expression, as this could previously cause the actual cause of a type-checking failure to be effectively hidden. --- src/ast_util.ml | 122 ++++++++++++++++++++++++++++++-------------------------- 1 file changed, 65 insertions(+), 57 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index 788008d1..f6b8317d 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -315,7 +315,7 @@ let rec constraint_disj (NC_aux (nc_aux, l) as nc) = | _ -> [nc] let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown) -let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) +let mk_typ_arg arg = A_aux (arg, Parse_ast.Unknown) let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown) let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown) @@ -330,23 +330,23 @@ let unit_typ = mk_id_typ (mk_id "unit") let bit_typ = mk_id_typ (mk_id "bit") let real_typ = mk_id_typ (mk_id "real") let app_typ id args = mk_typ (Typ_app (id, args)) -let register_typ typ = mk_typ (Typ_app (mk_id "register", [mk_typ_arg (Typ_arg_typ typ)])) +let register_typ typ = mk_typ (Typ_app (mk_id "register", [mk_typ_arg (A_typ typ)])) let atom_typ nexp = - mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp))])) + mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (A_nexp (nexp_simp nexp))])) let range_typ nexp1 nexp2 = - mk_typ (Typ_app (mk_id "range", [mk_typ_arg (Typ_arg_nexp (nexp_simp nexp1)); - mk_typ_arg (Typ_arg_nexp (nexp_simp nexp2))])) + mk_typ (Typ_app (mk_id "range", [mk_typ_arg (A_nexp (nexp_simp nexp1)); + mk_typ_arg (A_nexp (nexp_simp nexp2))])) let bool_typ = mk_id_typ (mk_id "bool") let string_typ = mk_id_typ (mk_id "string") -let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)])) +let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (A_typ typ)])) let tuple_typ typs = mk_typ (Typ_tup typs) let function_typ arg_typs ret_typ eff = mk_typ (Typ_fn (arg_typs, ret_typ, eff)) let vector_typ n ord typ = mk_typ (Typ_app (mk_id "vector", - [mk_typ_arg (Typ_arg_nexp (nexp_simp n)); - mk_typ_arg (Typ_arg_order ord); - mk_typ_arg (Typ_arg_typ typ)])) + [mk_typ_arg (A_nexp (nexp_simp n)); + mk_typ_arg (A_order ord); + mk_typ_arg (A_typ typ)])) let exc_typ = mk_id_typ (mk_id "exception") @@ -374,10 +374,10 @@ let nc_var kid = mk_nc (NC_var kid) let nc_true = mk_nc NC_true let nc_false = mk_nc NC_false -let arg_nexp ?loc:(l=Parse_ast.Unknown) n = Typ_arg_aux (Typ_arg_nexp n, l) -let arg_order ?loc:(l=Parse_ast.Unknown) ord = Typ_arg_aux (Typ_arg_order ord, l) -let arg_typ ?loc:(l=Parse_ast.Unknown) typ = Typ_arg_aux (Typ_arg_typ typ, l) -let arg_bool ?loc:(l=Parse_ast.Unknown) nc = Typ_arg_aux (Typ_arg_bool nc, l) +let arg_nexp ?loc:(l=Parse_ast.Unknown) n = A_aux (A_nexp n, l) +let arg_order ?loc:(l=Parse_ast.Unknown) ord = A_aux (A_order ord, l) +let arg_typ ?loc:(l=Parse_ast.Unknown) typ = A_aux (A_typ typ, l) +let arg_bool ?loc:(l=Parse_ast.Unknown) nc = A_aux (A_bool nc, l) let nc_not nc = mk_nc (NC_app (mk_id "not", [arg_bool nc])) @@ -426,6 +426,14 @@ let quant_map_items f = function | TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_no_forall, l) | TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (List.map f qis), l) +let is_quant_kopt = function + | QI_aux (QI_id _, _) -> true + | _ -> false + +let is_quant_constraint = function + | QI_aux (QI_const _, _) -> true + | _ -> false + let unaux_nexp (Nexp_aux (nexp, _)) = nexp let unaux_order (Ord_aux (ord, _)) = ord let unaux_typ (Typ_aux (typ, _)) = typ @@ -670,12 +678,12 @@ and string_of_typ_aux = function | Typ_exist (kids, nc, typ) -> "{" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}" and string_of_typ_arg = function - | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg + | A_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg and string_of_typ_arg_aux = function - | Typ_arg_nexp n -> string_of_nexp n - | Typ_arg_typ typ -> string_of_typ typ - | Typ_arg_order o -> string_of_order o - | Typ_arg_bool nc -> string_of_n_constraint nc + | A_nexp n -> string_of_nexp n + | A_typ typ -> string_of_typ typ + | A_order o -> string_of_order o + | A_bool nc -> string_of_n_constraint nc and string_of_n_constraint = function | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2 @@ -993,13 +1001,13 @@ module Typ = struct | Typ_bidir _, _ -> -1 | _, Typ_bidir _ -> 1 | Typ_tup _, _ -> -1 | _, Typ_tup _ -> 1 | Typ_exist _, _ -> -1 | _, Typ_exist _ -> 1 - and arg_compare (Typ_arg_aux (ta1,_)) (Typ_arg_aux (ta2,_)) = + and arg_compare (A_aux (ta1,_)) (A_aux (ta2,_)) = match ta1, ta2 with - | Typ_arg_nexp n1, Typ_arg_nexp n2 -> Nexp.compare n1 n2 - | Typ_arg_typ t1, Typ_arg_typ t2 -> compare t1 t2 - | Typ_arg_order o1, Typ_arg_order o2 -> order_compare o1 o2 - | Typ_arg_nexp _, _ -> -1 | _, Typ_arg_nexp _ -> 1 - | Typ_arg_typ _, _ -> -1 | _, Typ_arg_typ _ -> 1 + | A_nexp n1, A_nexp n2 -> Nexp.compare n1 n2 + | A_typ t1, A_typ t2 -> compare t1 t2 + | A_order o1, A_order o2 -> order_compare o1 o2 + | A_nexp _, _ -> -1 | _, A_nexp _ -> 1 + | A_typ _, _ -> -1 | _, A_typ _ -> 1 end module TypMap = Map.Make(Typ) @@ -1055,21 +1063,21 @@ let is_ref_typ (Typ_aux (typ_aux, _)) = match typ_aux with let rec is_vector_typ = function | Typ_aux (Typ_app (Id_aux (Id "vector",_), [_;_;_]), _) -> true - | Typ_aux (Typ_app (Id_aux (Id "register",_), [Typ_arg_aux (Typ_arg_typ rtyp,_)]), _) -> + | Typ_aux (Typ_app (Id_aux (Id "register",_), [A_aux (A_typ rtyp,_)]), _) -> is_vector_typ rtyp | _ -> false let typ_app_args_of = function | Typ_aux (Typ_app (Id_aux (Id c,_), targs), l) -> - (c, List.map (fun (Typ_arg_aux (a,_)) -> a) targs, l) + (c, List.map (fun (A_aux (a,_)) -> a) targs, l) | Typ_aux (_, l) as typ -> raise (Reporting.err_typ l ("typ_app_args_of called on non-app type " ^ string_of_typ typ)) let rec vector_typ_args_of typ = match typ_app_args_of typ with - | ("vector", [Typ_arg_nexp len; Typ_arg_order ord; Typ_arg_typ etyp], l) -> + | ("vector", [A_nexp len; A_order ord; A_typ etyp], l) -> (nexp_simp len, ord, etyp) - | ("register", [Typ_arg_typ rtyp], _) -> vector_typ_args_of rtyp + | ("register", [A_typ rtyp], _) -> vector_typ_args_of rtyp | (_, _, l) -> raise (Reporting.err_typ l ("vector_typ_args_of called on non-vector type " ^ string_of_typ typ)) @@ -1162,12 +1170,12 @@ and tyvars_of_typ (Typ_aux (t,_)) = | Typ_exist (kids, nc, t) -> let s = KidSet.union (tyvars_of_typ t) (tyvars_of_constraint nc) in List.fold_left (fun s k -> KidSet.remove k s) s kids -and tyvars_of_typ_arg (Typ_arg_aux (ta,_)) = +and tyvars_of_typ_arg (A_aux (ta,_)) = match ta with - | Typ_arg_nexp nexp -> tyvars_of_nexp nexp - | Typ_arg_typ typ -> tyvars_of_typ typ - | Typ_arg_order _ -> KidSet.empty - | Typ_arg_bool nc -> tyvars_of_constraint nc + | A_nexp nexp -> tyvars_of_nexp nexp + | A_typ typ -> tyvars_of_typ typ + | A_order _ -> KidSet.empty + | A_bool nc -> tyvars_of_constraint nc let tyvars_of_quant_item (QI_aux (qi, _)) = match qi with | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) -> @@ -1184,7 +1192,7 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) = | Typ_app (_,[size;_;_]) when mwords && is_bitvector_typ typ -> wrap (E_app (mk_id "undefined_bitvector", undefined_of_typ_args mwords l annot size)) typ - | Typ_app (atom, [Typ_arg_aux (Typ_arg_nexp i, _)]) when string_of_id atom = "atom" -> + | Typ_app (atom, [A_aux (A_nexp i, _)]) when string_of_id atom = "atom" -> wrap (E_sizeof i) typ | Typ_app (id, args) -> wrap (E_app (prepend_id "undefined_" id, @@ -1199,11 +1207,11 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) = case when re-writing those functions. *) wrap (E_id (prepend_id "typ_" (id_of_kid kid))) typ | Typ_internal_unknown | Typ_bidir _ | Typ_fn _ | Typ_exist _ -> assert false (* Typ_exist should be re-written *) -and undefined_of_typ_args mwords l annot (Typ_arg_aux (typ_arg_aux, _) as typ_arg) = +and undefined_of_typ_args mwords l annot (A_aux (typ_arg_aux, _) as typ_arg) = match typ_arg_aux with - | Typ_arg_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))] - | Typ_arg_typ typ -> [undefined_of_typ mwords l annot typ] - | Typ_arg_order _ -> [] + | A_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))] + | A_typ typ -> [undefined_of_typ mwords l annot typ] + | A_order _ -> [] let destruct_pexp (Pat_aux (pexp,ann)) = match pexp with @@ -1426,13 +1434,13 @@ let rec locate_typ f (Typ_aux (typ_aux, l)) = in Typ_aux (typ_aux, f l) -and locate_typ_arg f (Typ_arg_aux (typ_arg_aux, l)) = +and locate_typ_arg f (A_aux (typ_arg_aux, l)) = let typ_arg_aux = match typ_arg_aux with - | Typ_arg_nexp nexp -> Typ_arg_nexp (locate_nexp f nexp) - | Typ_arg_typ typ -> Typ_arg_typ (locate_typ f typ) - | Typ_arg_order ord -> Typ_arg_order (locate_order f ord) + | A_nexp nexp -> A_nexp (locate_nexp f nexp) + | A_typ typ -> A_typ (locate_typ f typ) + | A_order ord -> A_order (locate_order f ord) in - Typ_arg_aux (typ_arg_aux, f l) + A_aux (typ_arg_aux, f l) let rec locate_typ_pat f (TP_aux (tp_aux, l)) = let tp_aux = match tp_aux with @@ -1552,7 +1560,7 @@ let unique l = let order_subst_aux sv subst = function | Ord_var kid -> begin match subst with - | Typ_arg_aux (Typ_arg_order ord, _) when Kid.compare kid sv = 0 -> + | A_aux (A_order ord, _) when Kid.compare kid sv = 0 -> unaux_order ord | _ -> Ord_var kid end @@ -1565,7 +1573,7 @@ let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv s and nexp_subst_aux sv subst = function | Nexp_var kid -> begin match subst with - | Typ_arg_aux (Typ_arg_nexp n, _) when Kid.compare kid sv = 0 -> unaux_nexp n + | A_aux (A_nexp n, _) when Kid.compare kid sv = 0 -> unaux_nexp n | _ -> Nexp_var kid end | Nexp_id id -> Nexp_id id @@ -1590,7 +1598,7 @@ and constraint_subst_aux l sv subst = function | NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_set (kid, ints) as set_nc -> begin match subst with - | Typ_arg_aux (Typ_arg_nexp n, _) when Kid.compare kid sv = 0 -> + | A_aux (A_nexp n, _) when Kid.compare kid sv = 0 -> nexp_set_to_or l n ints | _ -> set_nc end @@ -1599,7 +1607,7 @@ and constraint_subst_aux l sv subst = function | NC_app (id, args) -> NC_app (id, List.map (typ_arg_subst sv subst) args) | NC_var kid -> begin match subst with - | Typ_arg_aux (Typ_arg_bool nc, _) when Kid.compare kid sv = 0 -> + | A_aux (A_bool nc, _) when Kid.compare kid sv = 0 -> unaux_constraint nc | _ -> NC_var kid end @@ -1612,7 +1620,7 @@ and typ_subst_aux sv subst = function | Typ_id v -> Typ_id v | Typ_var kid -> begin match subst with - | Typ_arg_aux (Typ_arg_typ typ, _) when Kid.compare kid sv = 0 -> + | A_aux (A_typ typ, _) when Kid.compare kid sv = 0 -> unaux_typ typ | _ -> Typ_var kid end @@ -1623,19 +1631,19 @@ and typ_subst_aux sv subst = function | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) | Typ_exist (kids, nc, typ) -> Typ_exist (kids, constraint_subst sv subst nc, typ_subst sv subst typ) -and typ_arg_subst sv subst (Typ_arg_aux (arg, l)) = Typ_arg_aux (typ_arg_subst_aux sv subst arg, l) +and typ_arg_subst sv subst (A_aux (arg, l)) = A_aux (typ_arg_subst_aux sv subst arg, l) and typ_arg_subst_aux sv subst = function - | Typ_arg_nexp nexp -> Typ_arg_nexp (nexp_subst sv subst nexp) - | Typ_arg_typ typ -> Typ_arg_typ (typ_subst sv subst typ) - | Typ_arg_order ord -> Typ_arg_order (order_subst sv subst ord) - | Typ_arg_bool nc -> Typ_arg_bool (constraint_subst sv subst nc) + | A_nexp nexp -> A_nexp (nexp_subst sv subst nexp) + | A_typ typ -> A_typ (typ_subst sv subst typ) + | A_order ord -> A_order (order_subst sv subst ord) + | A_bool nc -> A_bool (constraint_subst sv subst nc) let subst_kid subst sv v x = x - |> subst sv (mk_typ_arg (Typ_arg_bool (nc_var v))) - |> subst sv (mk_typ_arg (Typ_arg_nexp (nvar v))) - |> subst sv (mk_typ_arg (Typ_arg_order (Ord_aux (Ord_var v, Parse_ast.Unknown)))) - |> subst sv (mk_typ_arg (Typ_arg_typ (mk_typ (Typ_var v)))) + |> subst sv (mk_typ_arg (A_bool (nc_var v))) + |> subst sv (mk_typ_arg (A_nexp (nvar v))) + |> subst sv (mk_typ_arg (A_order (Ord_aux (Ord_var v, Parse_ast.Unknown)))) + |> subst sv (mk_typ_arg (A_typ (mk_typ (Typ_var v)))) let quant_item_subst_kid_aux sv subst = function | QI_id (KOpt_aux (KOpt_none kid, l)) as qid -> -- cgit v1.2.3 From 5bc5f5dee8921f8d24260dae54177e00c291fcb1 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Mon, 10 Dec 2018 20:39:16 +0000 Subject: Various changes: * Improve type inference for numeric if statements (if_infer test) * Correctly handle constraints for existentially quantified constructors (constraint_ctor test) * Canonicalise all numeric types in function arguments, which triggers some weird edge cases between parametric polymorphism and subtyping of numeric arguments * Because of this eq_int, eq_range, and eq_atom etc become identical * Avoid duplicating destruct_exist in Env * Handle some odd subtyping cases better --- src/ast_util.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index f6b8317d..46afe599 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -368,12 +368,17 @@ let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown) let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown) let nc_lt n1 n2 = nc_lteq (nsum n1 (nint 1)) n2 let nc_gt n1 n2 = nc_gteq n1 (nsum n2 (nint 1)) -let nc_and nc1 nc2 = mk_nc (NC_and (nc1, nc2)) let nc_or nc1 nc2 = mk_nc (NC_or (nc1, nc2)) let nc_var kid = mk_nc (NC_var kid) let nc_true = mk_nc NC_true let nc_false = mk_nc NC_false +let nc_and nc1 nc2 = + match nc1, nc2 with + | _, NC_aux (NC_true, _) -> nc1 + | NC_aux (NC_true, _), _ -> nc2 + | _, _ -> mk_nc (NC_and (nc1, nc2)) + let arg_nexp ?loc:(l=Parse_ast.Unknown) n = A_aux (A_nexp n, l) let arg_order ?loc:(l=Parse_ast.Unknown) ord = A_aux (A_order ord, l) let arg_typ ?loc:(l=Parse_ast.Unknown) typ = A_aux (A_typ typ, l) @@ -685,7 +690,7 @@ and string_of_typ_arg_aux = function | A_order o -> string_of_order o | A_bool nc -> string_of_n_constraint nc and string_of_n_constraint = function - | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 + | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " == " ^ string_of_nexp n2 | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2 | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2 | NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2 -- cgit v1.2.3 From ab4b9ca4f7cab45b6a2a13d0ef125dcf9c276a06 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 11 Dec 2018 19:54:14 +0000 Subject: Fix all tests with type checking changes --- src/ast_util.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index 46afe599..8544700b 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -818,8 +818,9 @@ and string_of_pat (P_aux (pat, l)) = | P_vector_concat pats -> string_of_list " @ " string_of_pat pats | P_vector pats -> "[" ^ string_of_list ", " string_of_pat pats ^ "]" | P_as (pat, id) -> "(" ^ string_of_pat pat ^ " as " ^ string_of_id id ^ ")" + | P_string_append [] -> "\"\"" | P_string_append pats -> string_of_list " ^ " string_of_pat pats - | _ -> "PAT" + | P_record _ -> "PAT" and string_of_mpat (MP_aux (pat, l)) = match pat with -- cgit v1.2.3 From c65aecd008d34102f4c95649113ed7f9afcc903b Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 12 Dec 2018 00:49:32 +0000 Subject: Fix various boolean type-variable related issues Remove some dead code in Pretty_print_common Start thinking a bit about Minisail-esque syntactic sugar in initial_check --- src/ast_util.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index 8544700b..6c67e6e7 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -143,6 +143,10 @@ let is_typ_kopt = function | KOpt_aux (KOpt_kind (K_aux (K_type, _), _), _) -> true | _ -> false +let is_bool_kopt = function + | KOpt_aux (KOpt_kind (K_aux (K_bool, _), _), _) -> true + | _ -> false + let string_of_kid = function | Kid_aux (Var v, _) -> v @@ -321,6 +325,9 @@ let mk_infix_id str = Id_aux (DeIid str, Parse_ast.Unknown) let mk_id_typ id = Typ_aux (Typ_id id, Parse_ast.Unknown) +let mk_kopt kind_aux id = + KOpt_aux (KOpt_kind (K_aux (kind_aux, Parse_ast.Unknown), id), Parse_ast.Unknown) + let mk_ord ord_aux = Ord_aux (ord_aux, Parse_ast.Unknown) let unknown_typ = mk_typ Typ_internal_unknown @@ -673,6 +680,7 @@ and string_of_typ_aux = function | Typ_var kid -> string_of_kid kid | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")" | Typ_app (id, args) when Id.compare id (mk_id "atom") = 0 -> "int(" ^ string_of_list ", " string_of_typ_arg args ^ ")" + | Typ_app (id, args) when Id.compare id (mk_id "atom_bool") = 0 -> "bool(" ^ string_of_list ", " string_of_typ_arg args ^ ")" | Typ_app (id, args) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")" | Typ_fn ([typ_arg], typ_ret, eff) -> string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff -- cgit v1.2.3 From cdf287dfb69275e479d79ebc0d305e365dd3ee7b Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 12 Dec 2018 01:45:20 +0000 Subject: Remove KOpt_none constructor We should infer type variable kinds better in initial_check.ml, but we really don't want to have to deal with that everywhere, especially when we can no longer easily cheat and assume KOpt_none implies K_int. --- src/ast_util.ml | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index 6c67e6e7..bd7a51bb 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -126,13 +126,11 @@ let mk_letbind pat exp = LB_aux (LB_val (pat, exp), no_annot) let mk_val_spec vs_aux = DEF_spec (VS_aux (vs_aux, no_annot)) -let kopt_kid (KOpt_aux (kopt_aux, _)) = - match kopt_aux with - | KOpt_none kid | KOpt_kind (_, kid) -> kid +let kopt_kid (KOpt_aux (KOpt_kind (_, kid), _)) = kid +let kopt_kind (KOpt_aux (KOpt_kind (k, _), _)) = k let is_nat_kopt = function | KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> true - | KOpt_aux (KOpt_none _, _) -> true | _ -> false let is_order_kopt = function @@ -713,9 +711,7 @@ and string_of_n_constraint = function | NC_aux (NC_true, _) -> "true" | NC_aux (NC_false, _) -> "false" -let string_of_kinded_id = function - | KOpt_aux (KOpt_none kid, _) -> string_of_kid kid - | KOpt_aux (KOpt_kind (k, kid), _) -> "(" ^ string_of_kid kid ^ " : " ^ string_of_kind k ^ ")" +let string_of_kinded_id (KOpt_aux (KOpt_kind (k, kid), _)) = "(" ^ string_of_kid kid ^ " : " ^ string_of_kind k ^ ")" let string_of_quant_item_aux = function | QI_id kopt -> string_of_kinded_id kopt @@ -1192,7 +1188,7 @@ and tyvars_of_typ_arg (A_aux (ta,_)) = | A_bool nc -> tyvars_of_constraint nc let tyvars_of_quant_item (QI_aux (qi, _)) = match qi with - | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) -> + | QI_id (KOpt_aux (KOpt_kind (_, kid), _)) -> KidSet.singleton kid | QI_const nc -> tyvars_of_constraint nc @@ -1660,8 +1656,6 @@ let subst_kid subst sv v x = |> subst sv (mk_typ_arg (A_typ (mk_typ (Typ_var v)))) let quant_item_subst_kid_aux sv subst = function - | QI_id (KOpt_aux (KOpt_none kid, l)) as qid -> - if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_none subst, l)) else qid | QI_id (KOpt_aux (KOpt_kind (k, kid), l)) as qid -> if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_kind (k, subst), l)) else qid | QI_const nc -> -- cgit v1.2.3 From ed5b58ba3a5a73253565edcb6460d2b48f56f887 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 12 Dec 2018 03:42:10 +0000 Subject: Generalise existentials for non-integer type variables --- src/ast_util.ml | 63 ++++++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 54 insertions(+), 9 deletions(-) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index bd7a51bb..02e297cb 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -128,7 +128,7 @@ let mk_val_spec vs_aux = let kopt_kid (KOpt_aux (KOpt_kind (_, kid), _)) = kid let kopt_kind (KOpt_aux (KOpt_kind (k, _), _)) = k - + let is_nat_kopt = function | KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> true | _ -> false @@ -144,7 +144,7 @@ let is_typ_kopt = function let is_bool_kopt = function | KOpt_aux (KOpt_kind (K_aux (K_bool, _), _), _) -> true | _ -> false - + let string_of_kid = function | Kid_aux (Var v, _) -> v @@ -153,6 +153,27 @@ module Kid = struct let compare kid1 kid2 = String.compare (string_of_kid kid1) (string_of_kid kid2) end +module Kind = struct + type t = kind + let compare (K_aux (aux1, _)) (K_aux (aux2, _)) = + match aux1, aux2 with + | K_int, K_int -> 0 + | K_type, K_type -> 0 + | K_order, K_order -> 0 + | K_bool, K_bool -> 0 + | K_int, _ -> 1 | _, K_int -> -1 + | K_type, _ -> 1 | _, K_type -> -1 + | K_order, _ -> 1 | _, K_order -> -1 +end + +module KOpt = struct + type t = kinded_id + let compare kopt1 kopt2 = + let lex_ord c1 c2 = if c1 = 0 then c2 else c1 in + lex_ord (Kid.compare (kopt_kid kopt1) (kopt_kid kopt2)) + (Kind.compare (kopt_kind kopt1) (kopt_kind kopt2)) +end + module Id = struct type t = id let compare id1 id2 = @@ -200,6 +221,8 @@ module Bindings = Map.Make(Id) module IdSet = Set.Make(Id) module KBindings = Map.Make(Kid) module KidSet = Set.Make(Kid) +module KOptSet = Set.Make(KOpt) +module KOptMap = Map.Make(KOpt) module NexpSet = Set.Make(Nexp) module NexpMap = Map.Make(Nexp) @@ -389,6 +412,13 @@ let arg_order ?loc:(l=Parse_ast.Unknown) ord = A_aux (A_order ord, l) let arg_typ ?loc:(l=Parse_ast.Unknown) typ = A_aux (A_typ typ, l) let arg_bool ?loc:(l=Parse_ast.Unknown) nc = A_aux (A_bool nc, l) +let arg_kopt (KOpt_aux (KOpt_kind (K_aux (k, _), v), l)) = + match k with + | K_int -> arg_nexp (nvar v) + | K_order -> arg_order (Ord_aux (Ord_var v, l)) + | K_bool -> arg_bool (nc_var v) + | K_type -> arg_typ (mk_typ (Typ_var v)) + let nc_not nc = mk_nc (NC_app (mk_id "not", [arg_bool nc])) let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown) @@ -644,6 +674,9 @@ let string_of_kind_aux = function let string_of_kind (K_aux (k, _)) = string_of_kind_aux k +let string_of_kinded_id (KOpt_aux (KOpt_kind (k, kid), _)) = + "(" ^ string_of_kid kid ^ " : " ^ string_of_kind k ^ ")" + let string_of_base_effect = function | BE_aux (beff, _) -> string_of_base_effect_aux beff @@ -687,7 +720,7 @@ and string_of_typ_aux = function ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff | Typ_bidir (typ1, typ2) -> string_of_typ typ1 ^ " <-> " ^ string_of_typ typ2 | Typ_exist (kids, nc, typ) -> - "{" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}" + "{" ^ string_of_list " " string_of_kinded_id kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}" and string_of_typ_arg = function | A_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg and string_of_typ_arg_aux = function @@ -995,7 +1028,7 @@ module Typ = struct | n -> n) | Typ_tup ts1, Typ_tup ts2 -> Util.compare_list compare ts1 ts2 | Typ_exist (ks1,nc1,t1), Typ_exist (ks2,nc2,t2) -> - (match Util.compare_list Kid.compare ks1 ks2 with + (match Util.compare_list KOpt.compare ks1 ks2 with | 0 -> (match NC.compare nc1 nc2 with | 0 -> compare t1 t2 | n -> n) @@ -1016,8 +1049,10 @@ module Typ = struct | A_nexp n1, A_nexp n2 -> Nexp.compare n1 n2 | A_typ t1, A_typ t2 -> compare t1 t2 | A_order o1, A_order o2 -> order_compare o1 o2 + | A_bool nc1, A_bool nc2 -> NC.compare nc1 nc2 | A_nexp _, _ -> -1 | _, A_nexp _ -> 1 | A_typ _, _ -> -1 | _, A_typ _ -> 1 + | A_order _, _ -> -1 | _, A_order _ -> 1 end module TypMap = Map.Make(Typ) @@ -1179,7 +1214,7 @@ and tyvars_of_typ (Typ_aux (t,_)) = KidSet.empty tas | Typ_exist (kids, nc, t) -> let s = KidSet.union (tyvars_of_typ t) (tyvars_of_constraint nc) in - List.fold_left (fun s k -> KidSet.remove k s) s kids + List.fold_left (fun s k -> KidSet.remove k s) s (List.map kopt_kid kids) and tyvars_of_typ_arg (A_aux (ta,_)) = match ta with | A_nexp nexp -> tyvars_of_nexp nexp @@ -1387,6 +1422,11 @@ let locate_id f (Id_aux (name, l)) = Id_aux (name, f l) let locate_kid f (Kid_aux (name, l)) = Kid_aux (name, f l) +let locate_kind f (K_aux (kind, l)) = K_aux (kind, f l) + +let locate_kinded_id f (KOpt_aux (KOpt_kind (k, kid), l)) = + KOpt_aux (KOpt_kind (locate_kind f k, locate_kid f kid), f l) + let locate_lit f (L_aux (lit, l)) = L_aux (lit, f l) let locate_base_effect f (BE_aux (base_effect, l)) = BE_aux (base_effect, f l) @@ -1427,10 +1467,12 @@ let rec locate_nc f (NC_aux (nc_aux, l)) = | NC_and (nc1, nc2) -> NC_and (locate_nc f nc1, locate_nc f nc2) | NC_true -> NC_true | NC_false -> NC_false + | NC_var v -> NC_var (locate_kid f v) + | NC_app (id, args) -> NC_app (locate_id f id, List.map (locate_typ_arg f) args) in NC_aux (nc_aux, f l) -let rec locate_typ f (Typ_aux (typ_aux, l)) = +and locate_typ f (Typ_aux (typ_aux, l)) = let typ_aux = match typ_aux with | Typ_internal_unknown -> Typ_internal_unknown | Typ_id id -> Typ_id (locate_id f id) @@ -1439,7 +1481,7 @@ let rec locate_typ f (Typ_aux (typ_aux, l)) = Typ_fn (List.map (locate_typ f) arg_typs, locate_typ f ret_typ, locate_effect f effect) | Typ_bidir (typ1, typ2) -> Typ_bidir (locate_typ f typ1, locate_typ f typ2) | Typ_tup typs -> Typ_tup (List.map (locate_typ f) typs) - | Typ_exist (kids, constr, typ) -> Typ_exist (List.map (locate_kid f) kids, locate_nc f constr, locate_typ f typ) + | Typ_exist (kopts, constr, typ) -> Typ_exist (List.map (locate_kinded_id f) kopts, locate_nc f constr, locate_typ f typ) | Typ_app (id, typ_args) -> Typ_app (locate_id f id, List.map (locate_typ_arg f) typ_args) in Typ_aux (typ_aux, f l) @@ -1449,6 +1491,7 @@ and locate_typ_arg f (A_aux (typ_arg_aux, l)) = | A_nexp nexp -> A_nexp (locate_nexp f nexp) | A_typ typ -> A_typ (locate_typ f typ) | A_order ord -> A_order (locate_order f ord) + | A_bool nc -> A_bool (locate_nc f nc) in A_aux (typ_arg_aux, f l) @@ -1638,8 +1681,10 @@ and typ_subst_aux sv subst = function | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst sv subst typ1, typ_subst sv subst typ2) | Typ_tup typs -> Typ_tup (List.map (typ_subst sv subst) typs) | Typ_app (f, args) -> Typ_app (f, List.map (typ_arg_subst sv subst) args) - | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) - | Typ_exist (kids, nc, typ) -> Typ_exist (kids, constraint_subst sv subst nc, typ_subst sv subst typ) + | Typ_exist (kopts, nc, typ) when KidSet.mem sv (KidSet.of_list (List.map kopt_kid kopts)) -> + Typ_exist (kopts, nc, typ) + | Typ_exist (kopts, nc, typ) -> + Typ_exist (kopts, constraint_subst sv subst nc, typ_subst sv subst typ) and typ_arg_subst sv subst (A_aux (arg, l)) = A_aux (typ_arg_subst_aux sv subst arg, l) and typ_arg_subst_aux sv subst = function -- cgit v1.2.3 From 56fb5bf999d7cc900d6535da4168e220862d3d9c Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 12 Dec 2018 17:37:13 +0000 Subject: Add a test case for various simple boolean properties test/typecheck/pass/tautology.sail constaints tests of various boolean properties, e.g. // de Morgan _prove(constraint(not('p | 'q) <--> not('p) & not('q))); _prove(constraint(not('p & 'q) <--> not('p) | not('q))); introduce a new _not_prove case which allows us to assert in tests that a constraint is not provable. This test essentially tests that constraints map to sensible problems in the SMT solver, without testing flow typing or any other features. Add a script test/typecheck/update_errors.sh, which regenerates the expected error messages. Testing that type-checking failures is important, but can be brittle when the error messages change for inconsequential reasons. This script automates fixing this. Also ensure that this test case works correctly in Lem --- src/ast_util.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/ast_util.ml') diff --git a/src/ast_util.ml b/src/ast_util.ml index 02e297cb..a771291e 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -739,6 +739,8 @@ and string_of_n_constraint = function "(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")" | NC_aux (NC_set (kid, ns), _) -> string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}" + | NC_aux (NC_app (Id_aux (DeIid op, _), [arg1; arg2]), _) -> + "(" ^ string_of_typ_arg arg1 ^ " " ^ op ^ " " ^ string_of_typ_arg arg2 ^ ")" | NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")" | NC_aux (NC_var v, _) -> string_of_kid v | NC_aux (NC_true, _) -> "true" -- cgit v1.2.3