Commit 43aeab83 authored by Andrei Paskevich's avatar Andrei Paskevich

Pattern: add compile_bare which does not require known_map

In pattern compilation, we only need to know the full list of
constructors for a given type, whenever
1. we want to check that a symbol used in a pattern is indeed
   a constructor;
2. we want to check for non-exhaustive matching and return an
   example of a non-covered pattern, if any.
Thus, we need to give Pattern.compile access to the current
known_map whenever we check new declarations in Decl or Mlw_decl.
However, once we have checked the patterns, we do not need the
full constructor lists just to compile the match expressions.
Just knowing the number of constructors (provided in ls_constr)
is enough to detect non-exhaustive matching during compilation.
parent c6e73ee5
......@@ -24,10 +24,13 @@ end
exception ConstructorExpected of lsymbol * ty
exception NonExhaustive of pattern list
exception Bare
module Compile (X : Action) = struct
open X
open X
let rec compile constructors tl rl = match tl,rl with
let compile constructors tl rl =
let rec compile tl rl = match tl,rl with
| _, [] -> (* no actions *)
let pl = List.map (fun t -> pat_wild (t_type t)) tl in
raise (NonExhaustive pl)
......@@ -36,12 +39,15 @@ module Compile (X : Action) = struct
| t :: tl, _ -> (* process the leftmost column *)
let ty = t_type t in
(* extract the set of constructors *)
let css = match ty.ty_node with
let bare,css = match ty.ty_node with
| Tyapp (ts,_) ->
let csl = constructors ts in
List.fold_left (fun s cs -> Sls.add cs s) Sls.empty csl
| Tyvar _ ->
Sls.empty
begin try false, Sls.of_list (constructors ts)
with Bare -> true, Sls.empty end
| Tyvar _ -> false, Sls.empty
in
(* if bare, only check fs.ls_constr *)
let is_constr fs =
fs.ls_constr > 0 && (bare || Sls.mem fs css)
in
(* map every constructor occurring at the head
* of the pattern list to the list of its args *)
......@@ -50,7 +56,7 @@ module Compile (X : Action) = struct
| Pwild | Pvar _ -> acc
| Pas (p,_) -> populate acc p
| Por (p,q) -> populate (populate acc p) q
| Papp (fs,pl) when Sls.mem fs css -> Mls.add fs pl acc
| Papp (fs,pl) when is_constr fs -> Mls.add fs pl acc
| Papp (fs,_) -> raise (ConstructorExpected (fs,ty))
in
let populate acc (pl,_) = populate acc (List.hd pl) in
......@@ -88,7 +94,7 @@ module Compile (X : Action) = struct
in
(* how to proceed if [t] is [Tapp(cs,al)] and [cs] is in [cases] *)
let comp_cases cs al =
try compile constructors (List.rev_append al tl) (Mls.find cs cases)
try compile (List.rev_append al tl) (Mls.find cs cases)
with NonExhaustive pl ->
let rec cont acc vl pl = match vl,pl with
| (_::vl), (p::pl) -> cont (p::acc) vl pl
......@@ -99,7 +105,7 @@ module Compile (X : Action) = struct
in
(* how to proceed if [t] is not covered by [cases] *)
let comp_wilds () =
try compile constructors tl wilds
try compile tl wilds
with NonExhaustive pl ->
let find_cs cs =
if Mls.mem cs types then () else
......@@ -115,11 +121,17 @@ module Compile (X : Action) = struct
match t.t_node with
| _ when Mls.is_empty types ->
comp_wilds ()
| Tapp (cs,al) when Sls.mem cs css ->
| Tapp (cs,al) when is_constr cs ->
if Mls.mem cs types then comp_cases cs al else comp_wilds ()
| _ ->
let base =
if Mls.set_submap css types then []
let no_wilds =
if bare then
let cs,_ = Mls.choose types in
Mls.cardinal types = cs.ls_constr
else
Mls.set_submap css types
in
let base = if no_wilds then []
else [mk_branch (pat_wild ty) (comp_wilds ())]
in
let add cs ql acc =
......@@ -130,6 +142,12 @@ module Compile (X : Action) = struct
mk_branch (pat_app cs pl ty) (comp_cases cs al) :: acc
in
mk_case t (Mls.fold add types base)
in
compile tl rl
let compile_bare tl rl =
try compile (fun _ -> raise Bare) tl rl
with NonExhaustive _ -> raise (NonExhaustive [])
end
......
......@@ -28,9 +28,16 @@ exception NonExhaustive of pattern list
module Compile (X : Action) : sig
val compile : (tysymbol -> lsymbol list) ->
term list -> (pattern list * X.action) list -> X.action
val compile_bare :
term list -> (pattern list * X.action) list -> X.action
(** [compile_bare] does not compute non-covered patterns *)
end
module CompileTerm : sig
val compile : (tysymbol -> lsymbol list) ->
term list -> (pattern list * term) list -> term
val compile_bare :
term list -> (pattern list * term) list -> term
end
......@@ -52,22 +52,15 @@ let is_infinite_ty inf_ts ma_map =
(** Compile match patterns *)
let rec rewriteT kn t = match t.t_node with
let rec rewriteT t = match t.t_node with
| Tcase (t,bl) ->
let t = rewriteT kn t in
let mk_b (p,t) = ([p], rewriteT kn t) in
let t = rewriteT t in
let mk_b (p,t) = ([p], rewriteT t) in
let bl = List.map (fun b -> mk_b (t_open_branch b)) bl in
let find_constructors kn ts = List.map fst (find_constructors kn ts) in
Pattern.CompileTerm.compile (find_constructors kn) [t] bl
| _ -> t_map (rewriteT kn) t
Pattern.CompileTerm.compile_bare [t] bl
| _ -> t_map rewriteT t
let comp t task =
let fn = rewriteT t.task_known in
match t.task_decl.td_node with
| Decl d -> add_decl task (decl_map fn d)
| _ -> add_tdecl task t.task_decl
let compile_match = Trans.fold comp None
let compile_match = Trans.decl (fun d -> [decl_map rewriteT d]) None
(** Eliminate algebraic types and match statements *)
......
......@@ -49,10 +49,9 @@ let apply_projection kn ls t = match t.t_node with
List.fold_left2 find t_true tl pjl
| _ -> assert false
let flat_case kn t bl =
let flat_case t bl =
let mk_b b = let p,t = t_open_branch b in [p],t in
let find_constructors kn ts = List.map fst (find_constructors kn ts) in
Pattern.CompileTerm.compile (find_constructors kn) [t] (List.map mk_b bl)
Pattern.CompileTerm.compile_bare [t] (List.map mk_b bl)
let rec add_quant kn (vl,tl,f) v =
let ty = v.vs_ty in
......@@ -129,7 +128,7 @@ let eval_match ~inline kn t =
let_map eval env t1 tb2
| Tcase (t1, bl1) ->
let t1 = eval env t1 in
let fn env t2 = eval env (Loc.try3 ?loc:t.t_loc flat_case kn t2 bl1) in
let fn env t2 = eval env (Loc.try2 ?loc:t.t_loc flat_case t2 bl1) in
begin try dive_to_constructor kn fn env t1
with Exit -> branch_map eval env t1 bl1 end
| Tquant (q, qf) ->
......
......@@ -86,8 +86,7 @@ let split_case_2 kn forig spl pos acc t bl =
split_case_2 kn forig spl pos acc t bl
else
let mk_b b = let p,f = t_open_branch b in [p], f in
let find ts = List.map fst (find_constructors kn ts) in
let f = Compile.compile find [t] (List.map mk_b bl) in
let f = Compile.compile_bare [t] (List.map mk_b bl) in
spl acc f
let asym_split = Term.asym_label
......
......@@ -1308,10 +1308,8 @@ and expr_desc lenv loc de = match de.de_desc with
| bl ->
let pv = create_pvsymbol (id_fresh "res") xs.xs_ity in
let pl = List.rev_map (fun (p,_) -> [p.ppat_pattern],t_void) bl in
let lkn = Theory.get_known (get_theory lenv.mod_uc) in
let find ts = List.map fst (Decl.find_constructors lkn ts) in
let bl = try
ignore (Pattern.CompileTerm.compile find [t_var pv.pv_vs] pl);
ignore (Pattern.CompileTerm.compile_bare [t_var pv.pv_vs] pl);
bl
with Pattern.NonExhaustive _ ->
let ity = ity_of_dity (snd de.de_type) in
......
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