diff options
Diffstat (limited to 'src/ast_util.ml')
| -rw-r--r-- | src/ast_util.ml | 698 |
1 files changed, 473 insertions, 225 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index b9ab21b2..a771291e 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 @@ -126,21 +126,23 @@ 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_kind [BK_aux (BK_int, _)], _), _), _) -> true - | KOpt_aux (KOpt_none _, _) -> true + | KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> 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 is_bool_kopt = function + | KOpt_aux (KOpt_kind (K_aux (K_bool, _), _), _) -> true | _ -> false let string_of_kid = function @@ -151,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 = @@ -198,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) @@ -270,13 +295,60 @@ 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_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) + +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_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) 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 @@ -286,23 +358,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 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", - [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") @@ -324,38 +396,49 @@ 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 rec nc_negate (NC_aux (nc, _)) = - 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 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) +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) 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) 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, _) -> [] @@ -379,9 +462,23 @@ 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 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 +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 @@ -406,8 +503,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) @@ -427,7 +524,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 @@ -523,9 +619,9 @@ 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_internal_mutrec _ -> Parse_ast.Unknown + | DEF_pragma (_, _, l) -> l let string_of_id = function | Id_aux (Id v, _) -> v @@ -570,14 +666,16 @@ 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" + | K_bool -> "Bool" -let string_of_base_kind (BK_aux (bk, _)) = string_of_base_kind_aux bk +let string_of_kind (K_aux (k, _)) = string_of_kind_aux k -let string_of_kind (K_aux (K_kind bks, _)) = string_of_list " -> " string_of_base_kind bks +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 @@ -612,20 +710,26 @@ 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) 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) -> + | 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 ^ "}" + "{" ^ string_of_list " " string_of_kinded_id 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 + | 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_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 @@ -635,12 +739,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_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" | NC_aux (NC_false, _) -> "false" +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_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 @@ -710,9 +819,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 ^ ")" @@ -748,8 +857,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 @@ -814,13 +924,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, _, _) @@ -832,6 +942,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) @@ -901,8 +1018,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) @@ -913,7 +1030,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) @@ -929,20 +1046,22 @@ 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_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) 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) @@ -960,7 +1079,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)) @@ -991,23 +1110,23 @@ 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_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 - | ("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_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 = @@ -1015,13 +1134,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 @@ -1065,7 +1184,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) @@ -1075,16 +1194,19 @@ 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, 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 | 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)) @@ -1093,18 +1215,19 @@ 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 - List.fold_left (fun s k -> KidSet.remove k s) s kids -and tyvars_of_typ_arg (Typ_arg_aux (ta,_)) = + let s = KidSet.union (tyvars_of_typ t) (tyvars_of_constraint nc) in + 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 - | Typ_arg_nexp nexp -> tyvars_of_nexp nexp - | Typ_arg_typ typ -> tyvars_of_typ typ - | Typ_arg_order _ -> KidSet.empty + | 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)), _)) -> + | QI_id (KOpt_aux (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) '#' @@ -1116,7 +1239,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, @@ -1131,11 +1254,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 @@ -1223,8 +1346,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) -> @@ -1269,10 +1392,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) @@ -1301,169 +1420,298 @@ 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_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_base_effect l (BE_aux (base_effect, _)) = BE_aux (base_effect, l) +let locate_lit f (L_aux (lit, l)) = L_aux (lit, 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_base_effect f (BE_aux (base_effect, l)) = BE_aux (base_effect, f 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 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 l (Nexp_aux (nexp_aux, _)) = +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_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_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, l) + NC_aux (nc_aux, f l) -let rec locate_typ l (Typ_aux (typ_aux, _)) = +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 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_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_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 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 (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, l) + Typ_aux (typ_aux, f l) -and locate_typ_arg l (Typ_arg_aux (typ_arg_aux, _)) = +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 nexp - | Typ_arg_typ typ -> Typ_arg_typ (locate_typ l typ) - | Typ_arg_order ord -> Typ_arg_order 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) + | A_bool nc -> A_bool (locate_nc f nc) in - Typ_arg_aux (typ_arg_aux, l) + A_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 (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) + | 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_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)) + +let unique_ref = ref 0 -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 l = + let l = Parse_ast.Unique (!unique_ref, l) in + incr unique_ref; + l -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 order_subst_aux sv subst = function + | Ord_var kid -> + begin match subst with + | A_aux (A_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_var kid -> + begin match subst with + | A_aux (A_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) + | 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.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 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 -> + begin match subst with + | A_aux (A_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 + | A_aux (A_bool nc, _) when Kid.compare kid sv = 0 -> + unaux_constraint nc + | _ -> NC_var kid + end + | NC_false -> NC_false + | NC_true -> NC_true + +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 -> + begin match subst with + | A_aux (A_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 (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 + | 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 (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_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 (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) + +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) |