diff options
| -rw-r--r-- | src/rewrites.ml | 49 | ||||
| -rw-r--r-- | src/type_check.ml | 4 | ||||
| -rw-r--r-- | src/type_check.mli | 8 |
3 files changed, 40 insertions, 21 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index 6a8c21b0..1ab2a9e0 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2768,28 +2768,35 @@ let rewrite_defs_internal_lets = ; rewrite_defs = rewrite_defs_base } -let rewrite_pexps_with_guards rewrite_pat = - let rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) = - let guards = ref [] in - match pexp_aux with - | Pat_exp (pat, exp) -> - begin - let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in - match !guards with - | [] -> pexp - | (g :: gs) -> - let guard_annot = (fst annot, Some (env_of exp, bool_typ, no_effect)) in - Pat_aux (Pat_when (pat, List.fold_left (fun g g' -> E_aux (E_app (mk_id "and_bool", [g; g']), guard_annot)) g gs, exp), annot) - end - | Pat_when (pat, guard, exp) -> - begin - let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in - let guard_annot = (fst annot, Some (env_of exp, bool_typ, no_effect)) in - Pat_aux (Pat_when (pat, List.fold_left (fun g g' -> E_aux (E_app (mk_id "and_bool", [g; g']), guard_annot)) guard !guards, exp), annot) - end - in +let fold_guards guards = + match guards with + | [] -> (mk_exp (E_lit (mk_lit L_true))) + | g :: gs -> List.fold_left (fun g g' -> mk_exp (E_app (mk_id "and_bool", [strip_exp g; strip_exp g']))) g gs + + +let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot annot)) as pexp) = + let guards = ref [] in + + match pexp_aux with + | Pat_exp (pat, exp) -> + begin + let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in + match !guards with + | [] -> pexp + | gs -> + let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp gs |> fold_guards, strip_exp exp)) in + check_case (env_of_annot annot) (pat_typ_of pat) unchecked_pexp (typ_of_annot annot) + end + | Pat_when (pat, guard, exp) -> + begin + let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in + let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp !guards |> fold_guards, strip_exp exp)) in + check_case (env_of_annot annot) (pat_typ_of pat) unchecked_pexp (typ_of_annot annot) + end + +let pexp_rewriters rewrite_pexp = let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } @@ -2808,7 +2815,7 @@ let rewrite_defs_pat_lits = P_aux (P_id id, p_annot) | p_aux, p_annot -> P_aux (p_aux, p_annot) in - rewrite_pexps_with_guards rewrite_pat + pexp_rewriters (rewrite_pexp_with_guards rewrite_pat) (* Now all expressions have no blocks anymore, any term is a sequence of let-expressions, * internal let-expressions, or internal plet-expressions ended by a term that does not diff --git a/src/type_check.ml b/src/type_check.ml index 5c72983a..63fab70e 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1906,6 +1906,10 @@ let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot) let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot) +let typ_of_pexp (Pat_aux (_, (l, tannot))) = typ_of_annot (l, tannot) + +let env_of_pexp (Pat_aux (_, (l, tannot))) = env_of_annot (l, tannot) + (* Flow typing *) let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with diff --git a/src/type_check.mli b/src/type_check.mli index a047db9c..c0359516 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -203,6 +203,9 @@ val strip_exp : 'a exp -> unit exp (** Strip the type annotations from a pattern *) val strip_pat : 'a pat -> unit pat +(** Strip the type annotations from a pattern-expression *) +val strip_pexp : 'a pexp -> unit pexp + (** Strip the type annotations from an l-expression *) val strip_lexp : 'a lexp -> unit lexp @@ -218,6 +221,8 @@ val check_exp : Env.t -> unit exp -> typ -> tannot exp val infer_exp : Env.t -> unit exp -> tannot exp +val check_case : Env.t -> typ -> unit pexp -> typ -> tannot pexp + val prove : Env.t -> n_constraint -> bool val solve : Env.t -> nexp -> Big_int.num option @@ -245,6 +250,9 @@ val typ_of_annot : Ast.l * tannot -> typ val pat_typ_of : tannot pat -> typ val pat_env_of : tannot pat -> Env.t +val typ_of_pexp : tannot pexp -> typ +val env_of_pexp : tannot pexp -> Env.t + val effect_of : tannot exp -> effect val effect_of_pat : tannot pat -> effect val effect_of_annot : tannot -> effect |