summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml20
-rw-r--r--src/ast_util.mli1
-rw-r--r--src/rewrites.ml50
-rw-r--r--src/type_check.mli2
4 files changed, 54 insertions, 19 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index e58842d2..229b0994 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -862,6 +862,20 @@ 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, _)) =
+ match nc with
+ | NC_equal (nexp1, nexp2)
+ | NC_bounded_ge (nexp1, nexp2)
+ | NC_bounded_le (nexp1, nexp2)
+ | NC_not_equal (nexp1, nexp2) ->
+ KidSet.union (tyvars_of_nexp nexp1) (tyvars_of_nexp nexp2)
+ | NC_set (kid, _) -> KidSet.singleton kid
+ | NC_or (nc1, nc2)
+ | NC_and (nc1, nc2) ->
+ KidSet.union (tyvars_of_nc nc1) (tyvars_of_nc nc2)
+ | NC_true
+ | NC_false -> KidSet.empty
+
let rec tyvars_of_typ (Typ_aux (t,_)) =
match t with
| Typ_id _ -> KidSet.empty
@@ -873,8 +887,8 @@ let rec tyvars_of_typ (Typ_aux (t,_)) =
| Typ_app (_,tas) ->
List.fold_left (fun s ta -> KidSet.union s (tyvars_of_typ_arg ta))
KidSet.empty tas
- | Typ_exist (kids,_,t) ->
- let s = tyvars_of_typ t in
+ | 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,_)) =
match ta with
@@ -882,6 +896,8 @@ and tyvars_of_typ_arg (Typ_arg_aux (ta,_)) =
| Typ_arg_typ typ -> tyvars_of_typ typ
| Typ_arg_order _ -> KidSet.empty
+let is_kid_generated kid = String.contains (string_of_kid kid) '#'
+
let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) =
let wrap e_aux typ = E_aux (e_aux, (l, annot typ)) in
match typ_aux with
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 5d2b01b8..3302c573 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -289,6 +289,7 @@ val union_effects : effect -> effect -> effect
val tyvars_of_nexp : nexp -> KidSet.t
val tyvars_of_typ : typ -> KidSet.t
+val is_kid_generated : kid -> bool
val undefined_of_typ : bool -> Ast.l -> (typ -> 'annot) -> typ -> 'annot exp
diff --git a/src/rewrites.ml b/src/rewrites.ml
index ec5d5f6d..e3f9a93e 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -103,6 +103,23 @@ let effectful_effs = function
| _ -> true
) effs
+
+let lookup_generated_kid env kid =
+ let match_kid_nc kid = function
+ | NC_aux (NC_equal (Nexp_aux (Nexp_var kid1, _), Nexp_aux (Nexp_var kid2, _)), _)
+ when Kid.compare kid kid2 = 0 && not (is_kid_generated kid1) -> kid1
+ | _ -> kid
+ in
+ List.fold_left match_kid_nc kid (Env.get_constraints env)
+
+let add_p_typ typ (P_aux (paux, annot) as pat) =
+ let env = pat_env_of pat in
+ let generated_kids typ = KidSet.filter is_kid_generated (tyvars_of_typ typ) in
+ let subst_kid kid typ = typ_subst_kid kid (lookup_generated_kid env kid) typ in
+ let typ' = KidSet.fold subst_kid (generated_kids typ) typ in
+ if KidSet.is_empty (generated_kids typ') then P_aux (P_typ (typ', pat), annot) else pat
+
+
let effectful eaux = effectful_effs (effect_of (propagate_exp_effect eaux))
let effectful_pexp pexp = effectful_effs (snd (propagate_pexp_effect pexp))
@@ -691,7 +708,7 @@ let remove_vector_concat_pat pat =
let id_pat =
match typ_opt with
- | Some typ -> P_aux (P_typ (typ, P_aux (P_id child,cannot)), cannot)
+ | Some typ -> add_p_typ typ (P_aux (P_id child,cannot))
| None -> P_aux (P_id child,cannot) in
let letbind = fix_eff_lb (LB_aux (LB_val (id_pat,subv),cannot)) in
(letbind,
@@ -2176,8 +2193,8 @@ let rewrite_defs_remove_blocks =
let l = get_loc_exp v in
let env = env_of v in
let typ = typ_of v in
- let wild = P_typ (typ, annot_pat P_wild l env typ) in
- let e_aux = E_let (annot_letbind (wild, v) l env typ, body) in
+ let wild = add_p_typ typ (annot_pat P_wild l env typ) in
+ let e_aux = E_let (annot_letbind (unaux_pat wild, v) l env typ, body) in
propagate_exp_effect (annot_exp e_aux l env (typ_of body)) in
let rec f l = function
@@ -2202,7 +2219,6 @@ let rewrite_defs_remove_blocks =
}
-
let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
(* body is a function : E_id variable -> actual body *)
let (E_aux (_,(l,annot))) = v in
@@ -2210,13 +2226,13 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
| Some (env, Typ_aux (Typ_id tid, _), eff) when string_of_id tid = "unit" ->
let body = body (annot_exp (E_lit (mk_lit L_unit)) l env unit_typ) in
let body_typ = try typ_of body with _ -> unit_typ in
- let wild = P_typ (typ_of v, annot_pat P_wild l env (typ_of v)) in
- let lb = annot_letbind (wild, v) l env unit_typ in
+ let wild = add_p_typ (typ_of v) (annot_pat P_wild l env (typ_of v)) in
+ let lb = annot_letbind (unaux_pat wild, v) l env unit_typ in
propagate_exp_effect (annot_exp (E_let (lb, body)) l env body_typ)
| Some (env, typ, eff) ->
let id = fresh_id "w__" l in
- let pat = P_typ (typ_of v, annot_pat (P_id id) l env (typ_of v)) in
- let lb = annot_letbind (pat, v) l env typ in
+ let pat = add_p_typ (typ_of v) (annot_pat (P_id id) l env (typ_of v)) in
+ let lb = annot_letbind (unaux_pat pat, v) l env typ in
let body = body (annot_exp (E_id id) l env typ) in
propagate_exp_effect (annot_exp (E_let (lb, body)) l env (typ_of body))
| None ->
@@ -2507,7 +2523,7 @@ let rewrite_defs_internal_lets =
let rec pat_of_local_lexp (LEXP_aux (lexp, ((l, _) as annot))) = match lexp with
| LEXP_id id -> P_aux (P_id id, annot)
- | LEXP_cast (typ, id) -> P_aux (P_typ (typ, P_aux (P_id id, annot)), annot)
+ | LEXP_cast (typ, id) -> add_p_typ typ (P_aux (P_id id, annot))
| LEXP_tup lexps -> P_aux (P_tup (List.map pat_of_local_lexp lexps), annot)
| _ -> raise (Reporting_basic.err_unreachable l "unexpected local lexp") in
@@ -2532,7 +2548,7 @@ let rewrite_defs_internal_lets =
| LEXP_aux (LEXP_id id, annot) ->
(P_id id, annot)
| LEXP_aux (LEXP_cast (typ, id), annot) ->
- (P_typ (typ, P_aux (P_id id, annot)), annot)
+ (unaux_pat (add_p_typ typ (P_aux (P_id id, annot))), annot)
| _ -> failwith "E_var with unexpected lexp" in
if effectful exp1 then
E_internal_plet (P_aux (paux, annot), exp1, exp2)
@@ -2615,10 +2631,10 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| [] -> annot_pat P_wild l env unit_typ
| [pat] ->
let typ = pat_typ_of pat in
- annot_pat (P_typ (typ, pat)) l env typ
+ add_p_typ typ pat
| pats ->
let typ = tuple_typ (List.map pat_typ_of pats) in
- annot_pat (P_typ (typ, annot_pat (P_tup pats) l env typ)) l env typ in
+ add_p_typ typ (annot_pat (P_tup pats) l env typ) in
let rec add_vars overwrite ((E_aux (expaux,annot)) as exp) vars =
match expaux with
@@ -2682,9 +2698,9 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let lvar_kid = mk_kid ("loop_" ^ string_of_id id) in
let lvar_nc = nc_and (nc_lteq lower (nvar lvar_kid)) (nc_lteq (nvar lvar_kid) upper) in
let lvar_typ = mk_typ (Typ_exist ([lvar_kid], lvar_nc, atom_typ (nvar lvar_kid))) in
- let lvar_pat = P_typ (lvar_typ, annot_pat (P_var (
+ let lvar_pat = unaux_pat (add_p_typ lvar_typ (annot_pat (P_var (
annot_pat (P_id id) el env (atom_typ (nvar lvar_kid)),
- TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ) in
+ TP_aux (TP_var lvar_kid, gen_loc el))) el env lvar_typ)) in
let lb = annot_letbind (lvar_pat, exp1) el env lvar_typ in
let body = annot_exp (E_let (lb, exp4)) el env (typ_of exp4) in
let v = annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; tuple_exp vars; body])) el env (typ_of body) in
@@ -2746,7 +2762,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| E_assign (lexp,vexp) ->
let mk_id_pat id = match Env.lookup_id id env with
| Local (_, typ) ->
- annot_pat (P_typ (typ, annot_pat (P_id id) pl env typ)) pl env typ
+ add_p_typ typ (annot_pat (P_id id) pl env typ)
| _ ->
raise (Reporting_basic.err_unreachable pl
("Failed to look up type of variable " ^ string_of_id id)) in
@@ -2758,7 +2774,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let pat = annot_pat (P_id id) pl env (typ_of vexp) in
Added_vars (vexp, mk_id_pat id)
| LEXP_aux (LEXP_cast (typ,id),annot) ->
- let pat = annot_pat (P_typ (typ, annot_pat (P_id id) pl env (typ_of vexp))) pl env typ in
+ let pat = add_p_typ typ (annot_pat (P_id id) pl env (typ_of vexp)) in
Added_vars (vexp,pat)
| LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i),((l1,_) as annot)) ->
let eid = annot_exp (E_id id) l2 env (typ_of_annot annot2) in
@@ -2792,7 +2808,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| LEXP_aux (LEXP_id id, _) ->
P_id id, typ_of v
| LEXP_aux (LEXP_cast (typ, id), _) ->
- P_typ (typ, annot_pat (P_id id) l env (typ_of v)), typ
+ unaux_pat (add_p_typ typ (annot_pat (P_id id) l env (typ_of v))), typ
| _ ->
raise (Reporting_basic.err_unreachable l
"E_var with a lexp that is not a variable") in
diff --git a/src/type_check.mli b/src/type_check.mli
index 340cf6e0..b03e2e00 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -266,6 +266,8 @@ val string_of_uvar : uvar -> string
val subst_unifiers : uvar KBindings.t -> typ -> typ
+val typ_subst_kid : kid -> kid -> typ -> typ
+
val unify : l -> Env.t -> typ -> typ -> uvar KBindings.t * kid list * n_constraint option
val alpha_equivalent : Env.t -> typ -> typ -> bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 19:40:32 +0000