Commit 39252658 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Split_goal: preserve trivial subgoals under "keep_on_simp"

parent 9be7caa2
...@@ -83,11 +83,11 @@ let split_case_2 kn forig spl pos acc t bl = ...@@ -83,11 +83,11 @@ let split_case_2 kn forig spl pos acc t bl =
let f = Pattern.compile_bare ~mk_case ~mk_let [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 spl acc f
let asym_split = Term.asym_label
let stop_split = Ident.create_label "stop_split" let stop_split = Ident.create_label "stop_split"
let asym f = Slab.mem asym_split f.t_label
let stop f = Slab.mem stop_split f.t_label let stop f = Slab.mem stop_split f.t_label
let asym f = Slab.mem Term.asym_label f.t_label
let keep f = Slab.mem Term.keep_on_simp_label f.t_label
let unstop f = let unstop f =
t_label ?loc:f.t_loc (Slab.remove stop_split f.t_label) f t_label ?loc:f.t_loc (Slab.remove stop_split f.t_label) f
...@@ -101,7 +101,7 @@ type split = { ...@@ -101,7 +101,7 @@ type split = {
let rec split_pos ro acc f = match f.t_node with let rec split_pos ro acc f = match f.t_node with
| _ when ro.stop_label && stop f -> unstop f :: acc | _ when ro.stop_label && stop f -> unstop f :: acc
| Ttrue -> acc | Ttrue -> if keep f then f::acc else acc
| Tfalse -> f::acc | Tfalse -> f::acc
| Tapp _ -> f::acc | Tapp _ -> f::acc
| Tbinop (Tand,f1,f2) when ro.respect_as && asym f1 -> | Tbinop (Tand,f1,f2) when ro.respect_as && asym f1 ->
...@@ -147,7 +147,7 @@ let rec split_pos ro acc f = match f.t_node with ...@@ -147,7 +147,7 @@ let rec split_pos ro acc f = match f.t_node with
and split_neg ro acc f = match f.t_node with and split_neg ro acc f = match f.t_node with
| _ when ro.stop_label && stop f -> unstop f :: acc | _ when ro.stop_label && stop f -> unstop f :: acc
| Ttrue -> f::acc | Ttrue -> f::acc
| Tfalse -> acc | Tfalse -> if keep f then f::acc else acc
| Tapp _ -> f::acc | Tapp _ -> f::acc
| Tbinop (Tand,_,_) when ro.right_only -> f::acc | Tbinop (Tand,_,_) when ro.right_only -> f::acc
| Tbinop (Tand,f1,f2) -> | Tbinop (Tand,f1,f2) ->
...@@ -280,7 +280,7 @@ let ls_of_var v = ...@@ -280,7 +280,7 @@ let ls_of_var v =
let rec split_intro pr dl acc f = let rec split_intro pr dl acc f =
let rsp = split_intro pr dl in let rsp = split_intro pr dl in
match f.t_node with match f.t_node with
| Ttrue -> acc | Ttrue when not (keep f) -> acc
| Tbinop (Tand,f1,f2) when asym f1 -> | Tbinop (Tand,f1,f2) when asym f1 ->
rsp (rsp acc (t_implies f1 f2)) f1 rsp (rsp acc (t_implies f1 f2)) f1
| Tbinop (Tand,f1,f2) -> | Tbinop (Tand,f1,f2) ->
......
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