Commit 8a427f54 authored by Sylvain Dailler's avatar Sylvain Dailler

destruct: first step simplification

parent 255164f9
...@@ -52,19 +52,23 @@ ...@@ -52,19 +52,23 @@
</theory> </theory>
<theory name="Unsoundness"> <theory name="Unsoundness">
<goal name="t1"> <goal name="t1">
<transf name="destruct_rec" arg1="H">
<goal name="t1.0">
<transf name="destruct_rec" arg1="H1">
<goal name="t1.0.0" expl="destruct premise">
</goal>
<goal name="t1.0.1">
</goal>
</transf>
</goal>
</transf>
</goal> </goal>
</theory> </theory>
<theory name="Incompleteness"> <theory name="Incompleteness">
<goal name="t1"> <goal name="t1">
<transf name="destruct_rec" arg1="H"> <transf name="destruct_rec" arg1="H">
<goal name="t1.0" expl="destruct premise"> <goal name="t1.0">
<proof prover="0"><result status="unknown" time="0.00"/></proof> <proof prover="0" obsolete="true"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="t1.1" expl="destruct premise">
<proof prover="0"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="t1.2" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -141,29 +145,5 @@ ...@@ -141,29 +145,5 @@
</transf> </transf>
</goal> </goal>
</theory> </theory>
<theory name="Tsurfail">
<goal name="t">
<transf name="destruct_rec" arg1="H">
<goal name="t.0" expl="destruct premise">
</goal>
<goal name="t.1" expl="destruct premise">
</goal>
<goal name="t.2">
</goal>
</transf>
</goal>
</theory>
<theory name="Tfail">
<goal name="G">
<transf name="destruct_rec" arg1="H">
<goal name="G.0" expl="destruct premise">
</goal>
<goal name="G.1" expl="destruct premise">
</goal>
<goal name="G.2">
</goal>
</transf>
</goal>
</theory>
</file> </file>
</why3session> </why3session>
...@@ -149,24 +149,22 @@ let destruct_term ~recursive (t: term) = ...@@ -149,24 +149,22 @@ let destruct_term ~recursive (t: term) =
l.ls_constr <> 0 l.ls_constr <> 0
in in
(* Check if a new goal is created in the branch *) (* Main recursive function:
let contains_goal l = [toplevel] when true, removing implications is allowed. Become false as
List.exists (fun x -> match x with | Goal_term _ -> true | _ -> false) l soon as we destruct non-implication construct
in *)
let rec destruct_term ~toplevel (t: term) =
(* Main function *) let destruct_term_exception ~toplevel t =
let rec destruct_term (t: term) =
let destruct_term_exception t =
if not recursive then [[Axiom_term t]] else if not recursive then [[Axiom_term t]] else
match destruct_term t with match destruct_term ~toplevel t with
| exception _ -> [[Axiom_term t]] | exception _ -> [[Axiom_term t]]
| l -> l | l -> l
in in
match t.t_node with match t.t_node with
| Tbinop (Tand, t1, t2) -> | Tbinop (Tand, t1, t2) ->
let l1 = destruct_term_exception t1 in let l1 = destruct_term_exception ~toplevel:false t1 in
let l2 = destruct_term_exception t2 in let l2 = destruct_term_exception ~toplevel:false t2 in
(* For each parallel branch of l1 we have to append *all* parallel (* For each parallel branch of l1 we have to append *all* parallel
branch of l2 which are not new goals. In case of new goals, we are branch of l2 which are not new goals. In case of new goals, we are
not allowed to use the left/right conclusions to prove the goal. not allowed to use the left/right conclusions to prove the goal.
...@@ -177,25 +175,19 @@ let destruct_term ~recursive (t: term) = ...@@ -177,25 +175,19 @@ let destruct_term ~recursive (t: term) =
(* TODO efficiency: this is not expected to work on very large terms (* TODO efficiency: this is not expected to work on very large terms
with tons of Tand/Tor. *) with tons of Tand/Tor. *)
List.fold_left (fun par_acc seq_list1 -> List.fold_left (fun par_acc seq_list1 ->
if contains_goal seq_list1 then List.fold_left (fun par_acc seq_list2 ->
par_acc @ [seq_list1] par_acc @ [seq_list1 @ seq_list2]) par_acc l2
else
List.fold_left (fun par_acc seq_list2 ->
if contains_goal seq_list2 then
par_acc @ [seq_list2]
else
par_acc @ [seq_list1 @ seq_list2]) par_acc l2
) [] l1 ) [] l1
| Tbinop (Tor, t1, t2) -> | Tbinop (Tor, t1, t2) ->
let l1 = destruct_term_exception t1 in let l1 = destruct_term_exception ~toplevel:false t1 in
let l2 = destruct_term_exception t2 in let l2 = destruct_term_exception ~toplevel:false t2 in
(* The two branch are completely disjoint. We just concatenate them to (* The two branch are completely disjoint. We just concatenate them to
ensure they are done in parallel *) ensure they are done in parallel *)
l1 @ l2 l1 @ l2
| Tbinop (Timplies, t1, t2) -> | Tbinop (Timplies, t1, t2) when toplevel ->
(* The premises is converted to a goal. The rest is recursively (* The premises is converted to a goal. The rest is recursively
destructed in parallel. *) destructed in parallel. *)
let l2 = destruct_term_exception t2 in let l2 = destruct_term_exception ~toplevel t2 in
[Goal_term t1] :: l2 [Goal_term t1] :: l2
| Tquant (Texists, tb) -> | Tquant (Texists, tb) ->
let (vsl, tr, te) = Term.t_open_quant tb in let (vsl, tr, te) = Term.t_open_quant tb in
...@@ -209,7 +201,7 @@ let destruct_term ~recursive (t: term) = ...@@ -209,7 +201,7 @@ let destruct_term ~recursive (t: term) =
let new_t = t_quant_close Texists tl tr part_t in let new_t = t_quant_close Texists tl tr part_t in
(* The recursive call is done after new symbols are introduced so we (* The recursive call is done after new symbols are introduced so we
readd the new decls to every generated list. *) readd the new decls to every generated list. *)
let l_t = destruct_term_exception new_t in let l_t = destruct_term_exception ~toplevel:false new_t in
List.map (fun x -> Param x_decl :: x) l_t List.map (fun x -> Param x_decl :: x) l_t
with with
| Ty.TypeMismatch (ty1, ty2) -> | Ty.TypeMismatch (ty1, ty2) ->
...@@ -237,7 +229,7 @@ let destruct_term ~recursive (t: term) = ...@@ -237,7 +229,7 @@ let destruct_term ~recursive (t: term) =
| Tnot {t_node = Tapp (ls, | Tnot {t_node = Tapp (ls,
[{t_node = Tapp (cs1, _); _}; {t_node = Tapp (cs2, _); _}]); _} [{t_node = Tapp (cs1, _); _}; {t_node = Tapp (cs2, _); _}]); _}
when ls_equal ls ps_equ && is_constructor cs1 && is_constructor cs2 -> when ls_equal ls ps_equ && is_constructor cs1 && is_constructor cs2 ->
(* Cs1 [l1] <> Cs2 [l2] *) (* Cs1 [l1] = Cs2 [l2] *)
if ls_equal cs1 cs2 then if ls_equal cs1 cs2 then
[[Axiom_term t]] [[Axiom_term t]]
else else
...@@ -245,7 +237,7 @@ let destruct_term ~recursive (t: term) = ...@@ -245,7 +237,7 @@ let destruct_term ~recursive (t: term) =
[[]] [[]]
| _ -> raise (Arg_trans ("destruct")) | _ -> raise (Arg_trans ("destruct"))
in in
destruct_term t destruct_term ~toplevel:true t
(* Destruct the head term of an hypothesis if it is either (* Destruct the head term of an hypothesis if it is either
conjunction, disjunction or exists *) conjunction, disjunction or exists *)
......
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