Commit cb7e440d authored by Andrei Paskevich's avatar Andrei Paskevich

Pattern: simplify and extend the interface

parent ee160187
......@@ -671,9 +671,9 @@ let find_prop_decl kn pr =
let check_match kn d =
let rec check () t = match t.t_node with
| Tcase (t1,bl) ->
let find ts = List.map fst (find_constructors kn ts) in
let bl = List.map (fun b -> let p,t = t_open_branch b in [p],t) bl in
ignore (Loc.try3 ?loc:t.t_loc Pattern.CompileTerm.compile find [t1] bl);
let get_constructors ts = List.map fst (find_constructors kn ts) in
let pl = List.map (fun b -> let p,_ = t_open_branch b in [p]) bl in
Loc.try2 ?loc:t.t_loc (Pattern.check_compile ~get_constructors) [t1] pl;
t_fold check () t
| _ -> t_fold check () t
in
......
......@@ -13,23 +13,12 @@ open Ident
open Ty
open Term
module type Action = sig
type action
type branch
val mk_let : vsymbol -> term -> action -> action
val mk_branch : pattern -> action -> branch
val mk_case : term -> branch list -> action
end
exception ConstructorExpected of lsymbol * ty
exception NonExhaustive of pattern list
exception Bare
module Compile (X : Action) = struct
open X
let compile constructors tl rl =
let compile ~get_constructors ~mk_case ~mk_let 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
......@@ -41,7 +30,7 @@ let compile constructors tl rl =
(* extract the set of constructors *)
let bare,css = match ty.ty_node with
| Tyapp (ts,_) ->
begin try false, Sls.of_list (constructors ts)
begin try false, Sls.of_list (get_constructors ts)
with Bare -> true, Sls.empty end
| Tyvar _ -> false, Sls.empty
in
......@@ -132,30 +121,42 @@ let compile constructors tl rl =
Mls.set_submap css types
in
let base = if no_wilds then []
else [mk_branch (pat_wild ty) (comp_wilds ())]
else [pat_wild ty, comp_wilds ()]
in
let add cs ql acc =
let get_vs q = create_vsymbol (id_fresh "x") q.pat_ty in
let vl = List.rev_map get_vs ql in
let pl = List.rev_map pat_var vl in
let al = List.rev_map t_var vl in
mk_branch (pat_app cs pl ty) (comp_cases cs al) :: acc
(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
let compile_bare ~mk_case ~mk_let tl rl =
let get_constructors _ = raise Bare in
try compile ~get_constructors ~mk_case ~mk_let tl rl
with NonExhaustive _ -> raise (NonExhaustive [])
end
module CompileTerm = Compile (struct
type action = term
type branch = term_branch
let mk_let v s t = t_let_close_simp v s t
let mk_branch p t = t_close_branch p t
let mk_case t bl = t_case t bl
end)
let check_compile ~get_constructors tl = function
| [] ->
let pl = List.map (fun t -> pat_wild (t_type t)) tl in
raise (NonExhaustive pl)
| (pl::_) as ppl ->
let mkt p = t_var (create_vsymbol (id_fresh "_") p.pat_ty) in
let tl = if tl = [] then List.map mkt pl else tl in
let rl = List.map (fun pl -> pl, ()) ppl in
let mk_case _ _ = () and mk_let _ _ _ = () in
compile ~get_constructors ~mk_case ~mk_let tl rl
let is_exhaustive tl = function
| [] -> false
| (pl::_) as ppl ->
let mkt p = t_var (create_vsymbol (id_fresh "_") p.pat_ty) in
let tl = if tl = [] then List.map mkt pl else tl in
let rl = List.map (fun pl -> pl, true) ppl in
let get_constructors _ = raise Bare in
let mk_case _ _ = true and mk_let _ _ _ = true in
try compile ~get_constructors ~mk_case ~mk_let tl rl
with NonExhaustive _ -> false
......@@ -9,35 +9,45 @@
(* *)
(********************************************************************)
(* Compilation of pattern-matching *)
(* Pattern compilation *)
open Ty
open Term
module type Action = sig
type action
type branch
val mk_let : vsymbol -> term -> action -> action
val mk_branch : pattern -> action -> branch
val mk_case : term -> branch list -> action
end
exception ConstructorExpected of lsymbol * ty
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
val compile :
get_constructors:(tysymbol -> lsymbol list) ->
mk_case:(term -> (pattern * 'a) list -> 'a) ->
mk_let:(vsymbol -> term -> 'a -> 'a) ->
term list -> (pattern list * 'a) list -> 'a
(** [compile get_constructors mk_case mk_let terms branches]
returns a composition of match- and let-terms equivalent
to [match terms with branches], where every pattern is
either a constructor applied to a list of variables, or
a wildcard pattern.
Raises [NonExhaustive patterns] where [patterns] is the
list of non-covered patterns. The check is permissive:
[match Cons t tl with Cons x xl -> ...] is accepted and
compiled into [match t, tl with x, xl -> ...]. *)
val compile_bare :
mk_case:(term -> (pattern * 'a) list -> 'a) ->
mk_let:(vsymbol -> term -> 'a -> 'a) ->
term list -> (pattern list * 'a) list -> 'a
(** [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
val check_compile :
get_constructors:(tysymbol -> lsymbol list) ->
term list -> pattern list list -> unit
(** [check_compile] verfies that the pattern list is exhaustive
and raises [NonExhaustive patterns] if it is not. If the term
list argument is empty, it is treated as a list of variables
of appropriate types. *)
val is_exhaustive : term list -> pattern list list -> bool
(** [is_exhaustive] checks if the pattern list is exhaustive.
If the term list argument is empty, it is treated as a list
of variables of appropriate types. *)
......@@ -55,9 +55,9 @@ let is_infinite_ty inf_ts ma_map =
let rec rewriteT t = match t.t_node with
| Tcase (t,bl) ->
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
Pattern.CompileTerm.compile_bare [t] bl
let mk_b b = let p,t = t_open_branch b in [p], rewriteT t in
let mk_case = t_case_close and mk_let = t_let_close_simp in
Pattern.compile_bare ~mk_case ~mk_let [t] (List.map mk_b bl)
| _ -> t_map rewriteT t
let compile_match = Trans.decl (fun d -> [decl_map rewriteT d]) None
......
......@@ -51,7 +51,8 @@ let apply_projection kn ls t = match t.t_node with
let flat_case t bl =
let mk_b b = let p,t = t_open_branch b in [p],t in
Pattern.CompileTerm.compile_bare [t] (List.map mk_b bl)
let mk_case = t_case_close and mk_let = t_let_close_simp in
Pattern.compile_bare ~mk_case ~mk_let [t] (List.map mk_b bl)
let rec add_quant kn (vl,tl,f) v =
let ty = v.vs_ty in
......
......@@ -37,14 +37,6 @@ let split_case forig spl pos acc tl bl =
let compiled = Ident.create_label "split_goal: compiled match"
module Compile = Pattern.Compile (struct
type action = term
type branch = term_branch
let mk_let v s t = t_let_close_simp v s t
let mk_branch p t = t_close_branch p t
let mk_case t bl = t_label_add compiled (t_case t bl)
end)
let split_case_2 kn forig spl pos acc t bl =
let vs = create_vsymbol (id_fresh "q") (t_type t) in
let tv = t_var vs in
......@@ -85,8 +77,10 @@ let split_case_2 kn forig spl pos acc t bl =
let forig = t_label ?loc:forig.t_loc lab forig in
split_case_2 kn forig spl pos acc t bl
else
let mk_let = t_let_close_simp in
let mk_case t bl = t_label_add compiled (t_case_close t bl) in
let mk_b b = let p,f = t_open_branch b in [p], f in
let f = Compile.compile_bare [t] (List.map mk_b bl) in
let f = Pattern.compile_bare ~mk_case ~mk_let [t] (List.map mk_b bl) in
spl acc f
let asym_split = Term.asym_label
......
......@@ -267,14 +267,10 @@ let find_definition kn ps =
let check_match lkn _kn d =
let rec checkE () e = match e.e_node with
| Ecase (e1,bl) ->
let typ = ty_of_ity (ity_of_expr e1) in
let tye = ty_of_ity (ity_of_expr e) in
let t_p = t_var (create_vsymbol (id_fresh "x") typ) in
let t_e = t_var (create_vsymbol (id_fresh "y") tye) in
let bl = List.map (fun (pp,_) -> [pp.ppat_pattern], t_e) bl in
let get ts = List.map fst (Decl.find_constructors lkn ts) in
ignore (Loc.try3 ?loc:e.e_loc Pattern.CompileTerm.compile get [t_p] bl);
| Ecase (_,bl) ->
let pl = List.map (fun (pp,_) -> [pp.ppat_pattern]) bl in
let get_constructors s = List.map fst (Decl.find_constructors lkn s) in
Loc.try2 ?loc:e.e_loc (Pattern.check_compile ~get_constructors) [] pl;
e_fold checkE () e
| _ -> e_fold checkE () e
in
......
......@@ -1142,15 +1142,10 @@ and try_expr keep_loc uloc env ({de_dvty = (argl,res)} as de0) =
xs, create_pvsymbol (id_fresh "_") xs.xs_ity, e
| bl ->
let pv = create_pvsymbol (id_fresh "res") xs.xs_ity in
let bl = try
let conv (p,_) = [p.ppat_pattern], t_void in
let comp = Pattern.CompileTerm.compile_bare in
ignore (comp [t_var pv.pv_vs] (List.rev_map conv bl));
bl
with Pattern.NonExhaustive _ ->
let _, pp = make_ppattern PPwild pv.pv_ity in
(pp, e_raise xs (e_value pv) (ity_of_dity res)) :: bl
in
let pl = List.rev_map (fun (p,_) -> [p.ppat_pattern]) bl in
let bl = if Pattern.is_exhaustive [t_var pv.pv_vs] pl
then bl else let _,pp = make_ppattern PPwild pv.pv_ity in
(pp, e_raise xs (e_value pv) (ity_of_dity res)) :: bl in
xs, pv, e_case (e_value pv) (List.rev bl)
in
e_try e1 (List.rev_map mk_branch xsl)
......
......@@ -1307,15 +1307,11 @@ and expr_desc lenv loc de = match de.de_desc with
xs, create_pvsymbol (id_fresh "void") p.ppat_ity, e
| 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 bl = try
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
let pl = List.rev_map (fun (p,_) -> [p.ppat_pattern]) bl in
let bl = if Pattern.is_exhaustive [t_var pv.pv_vs] pl
then bl else let ity = ity_of_dity (snd de.de_type) in
let _, pp = make_ppattern PPwild pv.pv_ity in
(pp, e_raise xs (e_value pv) ity) :: bl
in
(pp, e_raise xs (e_value pv) ity) :: bl in
xs, pv, e_case (e_value pv) (List.rev bl)
in
e_try e1 (List.rev_map mk_branch xsl)
......
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