Commit 19b60049 authored by Andrei Paskevich's avatar Andrei Paskevich

Split_goal: restore aggressive splitting for split_premises

turns out, Alt-Ergo really dislikes unsplitted premises
parent 30fd6bb4
...@@ -19,6 +19,7 @@ type split = { ...@@ -19,6 +19,7 @@ type split = {
byso_split : bool; byso_split : bool;
side_split : bool; side_split : bool;
stop_split : bool; stop_split : bool;
asym_split : bool;
intro_mode : bool; intro_mode : bool;
comp_match : known_map option; comp_match : known_map option;
} }
...@@ -227,7 +228,7 @@ let rec split_core sp f = ...@@ -227,7 +228,7 @@ let rec split_core sp f =
let (&&&) = alias2 f1 f2 t_and in let (&&&) = alias2 f1 f2 t_and in
let sf1 = rc f1 and sf2 = rc f2 in let sf1 = rc f1 and sf2 = rc f2 in
let fwd = sf1.fwd &&& sf2.fwd and bwd = sf1.bwd &&& sf2.bwd in let fwd = sf1.fwd &&& sf2.fwd and bwd = sf1.bwd &&& sf2.bwd in
let asym = not sp.intro_mode && asym f1 in let asym = sp.asym_split && asym f1 in
let nf2, cn2 = ncaset [] sf2 in let nf2, cn2 = ncaset [] sf2 in
let sd = if asym then [sf1.side] else [] in let sd = if asym then [sf1.side] else [] in
let dp = nf2::sd in let dp = nf2::sd in
...@@ -252,7 +253,7 @@ let rec split_core sp f = ...@@ -252,7 +253,7 @@ let rec split_core sp f =
let (>->) = alias2 f1 f2 t_implies in let (>->) = alias2 f1 f2 t_implies in
let sf1 = rc f1 and sf2 = rc f2 in let sf1 = rc f1 and sf2 = rc f2 in
let fwd = sf1.bwd >-> sf2.fwd and bwd = sf1.fwd >-> sf2.bwd in let fwd = sf1.bwd >-> sf2.fwd and bwd = sf1.fwd >-> sf2.bwd in
let asym = not sp.intro_mode && asym f1 in let asym = sp.asym_split && asym f1 in
let sd = [sf1.side] in let sd = [sf1.side] in
let neg1 = nclose sf1.pos in let neg1 = nclose sf1.pos in
let neg2 = if not asym then sf2.neg else let neg2 = if not asym then sf2.neg else
...@@ -269,7 +270,7 @@ let rec split_core sp f = ...@@ -269,7 +270,7 @@ let rec split_core sp f =
let (|||) = alias2 f1 f2 t_or in let (|||) = alias2 f1 f2 t_or in
let sf1 = rc f1 and sf2 = rc f2 in let sf1 = rc f1 and sf2 = rc f2 in
let fwd = sf1.fwd ||| sf2.fwd and bwd = sf1.bwd ||| sf2.bwd in let fwd = sf1.fwd ||| sf2.fwd and bwd = sf1.bwd ||| sf2.bwd in
let asym = not sp.intro_mode && asym f1 in let asym = sp.asym_split && asym f1 in
let sd = if asym then [sf2.side] else [] in let sd = if asym then [sf2.side] else [] in
let pf2, cp2 = pcaset [] sf2 in let pf2, cp2 = pcaset [] sf2 in
let dp = sf2.pos::sd in let dp = sf2.pos::sd in
...@@ -428,6 +429,7 @@ let full_split kn = { ...@@ -428,6 +429,7 @@ let full_split kn = {
byso_split = false; byso_split = false;
side_split = true; side_split = true;
stop_split = false; stop_split = false;
asym_split = true;
intro_mode = false; intro_mode = false;
comp_match = kn; comp_match = kn;
} }
...@@ -436,7 +438,8 @@ let right_split kn = { (full_split kn) with right_only = true } ...@@ -436,7 +438,8 @@ let right_split kn = { (full_split kn) with right_only = true }
let full_proof kn = { (full_split kn) with stop_split = true; let full_proof kn = { (full_split kn) with stop_split = true;
byso_split = true } byso_split = true }
let right_proof kn = { (full_proof kn) with right_only = true } let right_proof kn = { (full_proof kn) with right_only = true }
let full_intro kn = { (full_split kn) with intro_mode = true; let full_intro kn = { (full_split kn) with asym_split = false;
intro_mode = true;
stop_split = true } stop_split = true }
let right_intro kn = { (full_intro kn) with right_only = true } let right_intro kn = { (full_intro kn) with right_only = true }
...@@ -474,7 +477,7 @@ let split_axiom sp pr f = ...@@ -474,7 +477,7 @@ let split_axiom sp pr f =
let make_prop f = let make_prop f =
let pr = create_prsymbol (id_clone pr.pr_name) in let pr = create_prsymbol (id_clone pr.pr_name) in
create_prop_decl Paxiom pr f in create_prop_decl Paxiom pr f in
let sp = { sp with intro_mode = true; byso_split = false } in let sp = { sp with asym_split = false; byso_split = false } in
match split_pos sp f with match split_pos sp f with
| [f] -> [create_prop_decl Paxiom pr f] | [f] -> [create_prop_decl Paxiom pr f]
| fl -> List.map make_prop fl | fl -> List.map make_prop fl
......
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