Commit 29e1d937 authored by Andrei Paskevich's avatar Andrei Paskevich

remove program pattern constructors

it is safer to construct the whole pattern from an untyped skeleton
in a top-down way, than to check the ghostness/mutability on each
constructor application.
parent 27436a2f
......@@ -139,85 +139,6 @@ type ppattern = {
ppat_effect : effect;
}
let ppat_is_wild pp = match pp.ppat_pattern.pat_node with
| Pwild -> true
| _ -> false
let ppat_wild vtv =
if vtv.vtv_mut <> None then Loc.errorm "Wildcard patterns are immutable";
{ ppat_pattern = pat_wild (ty_of_ity vtv.vtv_ity);
ppat_vtv = vtv;
ppat_effect = eff_empty; }
let ppat_var pv =
{ ppat_pattern = pat_var pv.pv_vs;
ppat_vtv = pv.pv_vtv;
ppat_effect = eff_empty; }
let ppat_plapp pls ppl vtv =
if vtv.vtv_mut <> None then
Loc.errorm "Only variable patterns can be mutable";
if pls.pl_hidden then raise (HiddenPLS pls.pl_ls);
let sbs = ity_match ity_subst_empty pls.pl_value.vtv_ity vtv.vtv_ity in
let mtch eff arg pp =
ignore (ity_match sbs arg.vtv_ity pp.ppat_vtv.vtv_ity);
let ghost = pp.ppat_vtv.vtv_ghost in
if ghost <> (vtv.vtv_ghost || arg.vtv_ghost) then
Loc.errorm "Ghost pattern in a non-ghost context";
let effect = eff_union eff pp.ppat_effect in
let arg_mut = if pls.pl_rdonly then None else arg.vtv_mut in
match arg_mut, pp.ppat_vtv.vtv_mut with
| _ when ppat_is_wild pp ->
effect
| Some r1, Some r2 ->
ignore (reg_match sbs r1 r2);
eff_read ~ghost effect (reg_full_inst sbs r1)
| Some r1, None ->
eff_read ~ghost effect (reg_full_inst sbs r1)
| None, None ->
effect
| None, Some _ ->
Loc.errorm "Mutable pattern in a non-mutable position"
in
let eff = try List.fold_left2 mtch eff_empty pls.pl_args ppl with
| Not_found -> raise (Pattern.ConstructorExpected pls.pl_ls)
| Invalid_argument _ -> raise (Term.BadArity
(pls.pl_ls, List.length pls.pl_args, List.length ppl)) in
let pl = List.map (fun pp -> pp.ppat_pattern) ppl in
{ ppat_pattern = pat_app pls.pl_ls pl (ty_of_ity vtv.vtv_ity);
ppat_vtv = vtv;
ppat_effect = if vtv.vtv_ghost then eff_ghostify eff else eff; }
let ppat_lapp ls ppl vtv = ppat_plapp (fake_pls ls) ppl vtv
let ppat_or p1 p2 =
ity_equal_check p1.ppat_vtv.vtv_ity p2.ppat_vtv.vtv_ity;
if p1.ppat_vtv.vtv_ghost <> p2.ppat_vtv.vtv_ghost then
Loc.errorm "Ghost pattern in a non-ghost context";
if p1.ppat_vtv.vtv_mut <> None || p2.ppat_vtv.vtv_mut <> None then
Loc.errorm "Mutable patterns are not allowed under OR";
{ ppat_pattern = pat_or p1.ppat_pattern p2.ppat_pattern;
ppat_vtv = p1.ppat_vtv;
ppat_effect = eff_union p1.ppat_effect p2.ppat_effect; }
let ppat_as pp pv =
ity_equal_check pp.ppat_vtv.vtv_ity pv.pv_vtv.vtv_ity;
if pp.ppat_vtv.vtv_ghost <> pv.pv_vtv.vtv_ghost then
Loc.errorm "Ghost pattern in a non-ghost context";
let vtv = match pp.ppat_vtv.vtv_mut, pv.pv_vtv.vtv_mut with
| Some r1, Some r2 ->
if not (reg_equal r1 r2) then raise (RegionMismatch (r1,r2));
pp.ppat_vtv (* the two vtv's are identical *)
| Some _, None -> pp.ppat_vtv
| None, Some _ -> pv.pv_vtv
| None, None -> pv.pv_vtv
in
{ ppat_pattern = pat_as pp.ppat_pattern pv.pv_vs;
ppat_vtv = vtv;
ppat_effect = pp.ppat_effect; }
(* reconstruct a pattern from an untyped skeleton *)
type pre_ppattern =
| PPwild
| PPvar of preid
......@@ -256,9 +177,9 @@ let make_ppattern pp vtv =
let arg_mut = if pls.pl_rdonly then None else arg.vtv_mut in
let mut = Opt.map (reg_full_inst sbs) arg_mut in
let pp = make (vty_value ~ghost ?mut ity) pp in
if ppat_is_wild pp then pp.ppat_effect, pp else
Opt.fold (eff_read ~ghost) pp.ppat_effect mut, pp
in
match pp.ppat_pattern.pat_node with
| Pwild -> pp.ppat_effect, pp
| _ -> Opt.fold (eff_read ~ghost) pp.ppat_effect mut, pp in
let ppl = try List.map2 mtch pls.pl_args ppl with
| Not_found -> raise (Pattern.ConstructorExpected pls.pl_ls)
| Invalid_argument _ -> raise (Term.BadArity
......
......@@ -62,13 +62,6 @@ type ppattern = private {
ppat_effect : effect;
}
val ppat_wild : vty_value -> ppattern
val ppat_var : pvsymbol -> ppattern
val ppat_plapp : plsymbol -> ppattern list -> vty_value -> ppattern
val ppat_lapp : lsymbol -> ppattern list -> vty_value -> ppattern
val ppat_or : ppattern -> ppattern -> ppattern
val ppat_as : ppattern -> pvsymbol -> ppattern
type pre_ppattern =
| PPwild
| PPvar of preid
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment