Commit 09d56ba9 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch '264-destruct-improvement-with-if-then-else-2' into 'master'

Resolve "destruct improvement with if then else"

Closes #264

See merge request !85
parents 07638376 1a9a65ba
use list.List
use list.Length
use int.Int
constant x: int
predicate p int
(**********************)
(* Simple destruction *)
(**********************)
axiom H: if x = 42 then p 1 else p 2
goal g: p 3
use list.List
use list.Length
use int.Int
goal g: p 0
constant l: list int
axiom H': match l with
axiom H1: match l with
| Nil -> p 4
| Cons x y -> p (x+length y)
| Cons _ (Cons y Nil) -> p y
......@@ -21,19 +24,64 @@ axiom H': match l with
| Cons _ (Cons _ (Cons _ _)) -> p 5
end
goal g': p 6
goal g1: p 1
(**********************)
(* As and or patterns *)
(**********************)
axiom H'': match l with
axiom H2: match l with
| Nil -> p 1
| Cons x Nil | Cons _ (Cons x Nil) -> p x
| Cons _ (Cons _ _ as l') -> p (length l')
| Cons _ (Cons _ _ as l1) -> p (length l1)
end
goal g'': p 7
goal g2: p 2
axiom H''': match l with
| Cons _ (Cons _ _ as l') as l'' -> p (length l'+length l'')
axiom H3: match l with
| Cons _ (Cons _ _ as l1) as l2 -> p (length l1+length l2)
| _ -> p 0
end
goal g''': p 8
\ No newline at end of file
goal g3: p 3
(*************************)
(* Recursive destruction *)
(*************************)
axiom H4:
if p x then
(if p (x+1) then
p 1
else
p 2)
else p 3
goal g4: p 4
axiom H5: match l with
| Cons x (Cons y _) ->
if x = y then
p 1 \/ p 2
else
p 3 /\ p 4
| _ -> true
end
(*********************************************************************************)
(* Interaction between recursive destruction of conditionals and of implications *)
(*********************************************************************************)
goal g5: p 5
axiom H6: p 1 -> if p 2 then p 3 else p 4
goal g6: p 6
axiom H7: if p 1 then p 2 -> p 3 else p 4
goal g7: p 7
axiom H8: if p 1 then if p 2 then (p 3 -> p 4) else p 5 else p 6
goal g8: p 8
\ No newline at end of file
......@@ -14,37 +14,117 @@
</goal>
</transf>
</goal>
<goal name="g&#39;">
<transf name="destruct" arg1="H&#39;">
<goal name="g&#39;.0">
<goal name="g1">
<transf name="destruct" arg1="H1">
<goal name="g1.0">
</goal>
<goal name="g&#39;.1">
<goal name="g1.1">
</goal>
<goal name="g&#39;.2">
<goal name="g1.2">
</goal>
<goal name="g&#39;.3">
<goal name="g1.3">
</goal>
<goal name="g&#39;.4">
<goal name="g1.4">
</goal>
</transf>
</goal>
<goal name="g&#39;&#39;">
<transf name="destruct" arg1="H&#39;&#39;">
<goal name="g&#39;&#39;.0">
<goal name="g2">
<transf name="destruct" arg1="H2">
<goal name="g2.0">
</goal>
<goal name="g&#39;&#39;.1">
<goal name="g2.1">
</goal>
<goal name="g&#39;&#39;.2">
<goal name="g2.2">
</goal>
<goal name="g&#39;&#39;.3">
<goal name="g2.3">
</goal>
</transf>
</goal>
<goal name="g&#39;&#39;&#39;">
<transf name="destruct" arg1="H&#39;&#39;&#39;">
<goal name="g&#39;&#39;&#39;.0">
<goal name="g3">
<transf name="destruct" arg1="H3">
<goal name="g3.0">
</goal>
<goal name="g&#39;&#39;&#39;.1">
<goal name="g3.1">
</goal>
</transf>
</goal>
<goal name="g4">
<transf name="destruct" arg1="H4">
<goal name="g4.0">
</goal>
<goal name="g4.1">
</goal>
</transf>
<transf name="destruct_rec" arg1="H4">
<goal name="g4.0">
</goal>
<goal name="g4.1">
</goal>
<goal name="g4.2">
</goal>
</transf>
</goal>
<goal name="g5">
<transf name="destruct" arg1="H5">
<goal name="g5.0">
</goal>
<goal name="g5.1">
</goal>
</transf>
<transf name="destruct_rec" arg1="H5">
<goal name="g5.0">
</goal>
<goal name="g5.1">
</goal>
<goal name="g5.2">
</goal>
<goal name="g5.3">
</goal>
</transf>
</goal>
<goal name="g6">
<transf name="destruct" arg1="H6">
<goal name="g6.0" expl="destruct premise">
</goal>
<goal name="g6.1">
</goal>
</transf>
<transf name="destruct_rec" arg1="H6">
<goal name="g6.0" expl="destruct premise">
</goal>
<goal name="g6.1">
</goal>
<goal name="g6.2">
</goal>
</transf>
</goal>
<goal name="g7">
<transf name="destruct" arg1="H7">
<goal name="g7.0">
</goal>
<goal name="g7.1">
</goal>
</transf>
<transf name="destruct_rec" arg1="H7">
<goal name="g7.0">
</goal>
<goal name="g7.1">
</goal>
</transf>
</goal>
<goal name="g8">
<transf name="destruct" arg1="H8">
<goal name="g8.0">
</goal>
<goal name="g8.1">
</goal>
</transf>
<transf name="destruct_rec" arg1="H8">
<goal name="g8.0">
</goal>
<goal name="g8.1">
</goal>
<goal name="g8.2">
</goal>
</transf>
</goal>
......
......@@ -161,6 +161,59 @@ let destruct_term ?names replace (x: term) : Task.task tlist =
trans
end
(** [expand p] returns a list of triples [(bindings, equalities, term)], where
1. [bindings] map pattern variables in [p] to term variables in [term]
2. [equalities] contain equalities between pattern variables from [as]
patterns, term variables, and terms
3. [term] corresponds to [p] under [bindings] and [equalities] *)
let rec expand (p:pattern) : ((vsymbol option * lsymbol) list * (vsymbol * lsymbol * term) list * term) list =
match p.pat_node with
| Pwild ->
let ls =
let id = Ident.id_fresh "_" in
create_lsymbol id [] (Some p.pat_ty)
in
[[None, ls], [], t_app ls [] ls.ls_value]
| Pvar v ->
let ls =
let id = Ident.id_clone v.vs_name in
create_lsymbol id [] (Some p.pat_ty)
in
[[Some v, ls], [], t_app ls [] ls.ls_value]
| Papp (ls, args) ->
let rec aux args =
match args with
| [] -> [[], [], []] (* really. *)
| arg::args' ->
let for_args' (x, eqs, t) (x', eqs', l) =
x@x', eqs@eqs', t::l
in
let for_arg l' arg =
List.map (for_args' arg) l'
in
List.flatten
(List.map (for_arg (aux args'))
(expand arg))
in
let for_arg (bds, eqs, args) =
bds, eqs, t_app ls args (Some p.pat_ty)
in
List.map for_arg (aux args)
| Por (p1, p2) ->
expand p1 @ expand p2
| Pas (p, v) ->
let ls =
let id = Ident.id_clone v.vs_name in
create_lsymbol id [] (Some p.pat_ty)
in
let for_t (bds, eqs, t) =
let eqs' = eqs@[(v, ls, t)] in
let t' = t_app ls [] ls.ls_value in
bds, eqs', t'
in
List.map for_t (expand p)
(* Type used to tag new declarations inside the destruct function. *)
type is_destructed =
| Axiom_term of term
......@@ -268,59 +321,50 @@ let destruct_fmla ~recursive (t: term) =
else
(* The hypothesis is trivial because Cs1 <> Cs2 thus useless *)
[[]]
| Tif (t1, t2, t3) -> [
[Axiom_term t1; Axiom_term t2];
[Axiom_term (t_not t1); Axiom_term t3];
]
| Tcase (t, tbs) ->
let for_case tb =
let p, t' = t_open_branch tb in
let rec expand p : ((vsymbol option * lsymbol) list * (vsymbol * lsymbol * term) list * term) list =
match p.pat_node with
| Pwild ->
let id = Ident.id_fresh "_" in
let ls = create_lsymbol id [] (Some p.pat_ty) in
[[None, ls], [], t_app ls [] ls.ls_value]
| Pvar v ->
let id = Ident.id_clone v.vs_name in
let ls = create_lsymbol id [] (Some p.pat_ty) in
[[Some v, ls], [], t_app ls [] ls.ls_value]
| Papp (ls, args) ->
let rec aux args =
match args with
| [] -> [[], [], []] (* really. *)
| arg::args' ->
let l1 = expand arg in
let l2 = aux args' in
List.flatten
(List.map (fun (x, eqs, t) ->
List.map (fun (y, eqs', l) ->
x@y, eqs@eqs', t::l)
l2)
l1)
in
List.map (fun (bds, eqs, args) -> bds, eqs, t_app ls args (Some p.pat_ty)) (aux args)
| Por (p1, p2) ->
let l1 = expand p1 in
let l2 = expand p2 in
l1 @ l2
| Pas (p, v) ->
let id = Ident.id_clone v.vs_name in
let ls = create_lsymbol id [] (Some p.pat_ty) in
List.map (fun (bds, eqs, t) -> bds, eqs@[(v, ls, t)], t_app ls [] ls.ls_value) (expand p)
in
let for_expansion (bds, eqs, t'') =
let mvs = List.fold_left (fun acc vls -> match vls with Some v, ls -> Mvs.add v (t_app ls [] ls.ls_value) acc | None, _ -> acc) Mvs.empty bds in
let mvs = List.fold_left (fun acc (vs, ls, _) -> Mvs.add vs (t_app ls [] ls.ls_value) acc) mvs eqs in
List.map (fun (_, ls) -> Param (create_param_decl ls)) bds @
List.map (fun (_, ls, t) -> Param (create_logic_decl [make_ls_defn ls [] t])) eqs @
[Axiom_term (t_equ t t'');
Axiom_term (t_subst mvs t')]
| Tif (t1, t2, t3) ->
let ts2 =
destruct_fmla_exception ~toplevel:false t2 |>
List.map (fun ts -> Axiom_term t1 :: ts)
in
let ts3 =
destruct_fmla_exception ~toplevel:false t3 |>
List.map (fun ts -> Axiom_term (t_not t1) :: ts)
in
ts2 @ ts3
| Tcase (t, tbs) when toplevel ->
let for_branch tb =
let pat, rhs = t_open_branch tb in
let for_expansion (bds, eqs, t') =
let mvs =
let for_binding acc vls =
match vls with
| Some v, ls -> Mvs.add v (t_app ls [] ls.ls_value) acc
| None, _ -> acc
in
List.fold_left for_binding Mvs.empty bds in
let mvs =
let for_eq acc (vs, ls, _) =
Mvs.add vs (t_app ls [] ls.ls_value) acc
in
List.fold_left for_eq mvs eqs
in
let for_rhs rhs' =
let mk_const (_, ls) = Param (create_param_decl ls) in
let mk_eq_axiom (_, ls, t) = Param (create_logic_decl [make_ls_defn ls [] t]) in
List.map mk_const bds @
List.map mk_eq_axiom eqs @
[Axiom_term (t_equ t t')] @
rhs'
in
t_subst mvs rhs |>
destruct_fmla_exception ~toplevel:false |>
List.map for_rhs
in
List.map for_expansion (expand p)
List.map for_expansion (expand pat)
in
List.map for_branch tbs |>
List.flatten |>
List.flatten
(List.map for_case tbs)
| _ -> raise (Arg_trans ("destruct"))
in
destruct_fmla ~toplevel:true t
......
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