[auto-reverse] apply reversible selection

auto_reverse_sequent.ml

@@ -1,6 +1,8 @@
+let auto_reverse_selection = true
+
 let auto_reverse_sequent_with_exceptions request_as_json =
     let sequent = Raw_sequent.sequent_from_json request_as_json in
-    let proof = Proof.rec_apply_reversible_rule (Hypothesis_proof sequent) in
+    let proof = Proof.rec_apply_reversible_rule (not auto_reverse_selection) (Hypothesis_proof sequent) in
     Proof.to_json proof;;
 
 let auto_reverse_sequent request_as_json =

proof.ml

@@ -223,34 +223,60 @@ let try_rule_request sequent rule_request =
     try from_sequent_and_rule_request sequent rule_request
     with Rule_exception _ -> raise NotApplicable;;
 
-let apply_reversible_rule proof =
+let is_atomic_zero_selection_sequent sequent = 
+  let n = get_formula_position is_whynot sequent in
+  let head, formula, tail = head_formula_tail n sequent in
+  List.for_all is_atomic_or_zero (head @ tail) &&
+  (not (List.mem formula sequent))
+
+let is_reversible_selection_sequent = function
+  | [f1; f2; Whynot _] when dual f1 = f2 -> false
+  | [f1; Whynot _; f2] when dual f1 = f2 -> false
+  | [Whynot _; f1; f2] when dual f1 = f2 -> false
+  | s -> is_atomic_zero_selection_sequent s
+
+let try_rule_selection sequent n =
+  let head, formula, tail = head_formula_tail n sequent in
+  match formula with
+    Whynot e -> Contraction_proof (head, e, tail,
+                  (Dereliction_proof (head, e, Whynot e :: tail,
+                     (Hypothesis_proof (head @ [e;  Whynot e] @ tail)))))
+  | _ -> raise NotApplicable
+
+(* selection tells if selection rule already applied *)
+let apply_reversible_rule selection proof =
     let sequent = get_conclusion proof in
-    try try_rule_request sequent (Top (get_formula_position is_top sequent))
+    try try_rule_request sequent (Top (get_formula_position is_top sequent)), selection
         with NotApplicable ->
-    try try_rule_request sequent (Bottom (get_formula_position is_bottom sequent))
+    try try_rule_request sequent (Bottom (get_formula_position is_bottom sequent)), selection
         with NotApplicable ->
-    try try_rule_request sequent (Par (get_formula_position is_par sequent))
+    try try_rule_request sequent (Par (get_formula_position is_par sequent)), selection
         with NotApplicable ->
-    try try_rule_request sequent (Dereliction (get_formula_position is_double_whynot sequent))
+    try try_rule_request sequent (Dereliction (get_formula_position is_double_whynot sequent)), selection
         with NotApplicable ->
-    try try_rule_request sequent (With (get_formula_position is_with sequent))
+    try try_rule_request sequent (With (get_formula_position is_with sequent)), selection
         with NotApplicable ->
-    try try_rule_request sequent (Promotion (get_formula_position is_ofcourse sequent))
+    try try_rule_request sequent (Promotion (get_formula_position is_ofcourse sequent)), selection
         with NotApplicable ->
-    try try_rule_request sequent One
+    try try_rule_request sequent One, selection
         with NotApplicable ->
-    try if List.length sequent = 1 then try_rule_request sequent (Tensor 0) else raise NotApplicable
+    try if List.length sequent = 1 then try_rule_request sequent (Tensor 0), selection
+        else raise NotApplicable
         with NotApplicable ->
-    try try_rule_request sequent Axiom
+    try try_rule_request sequent Axiom, selection
         with NotApplicable ->
-    proof;;
+    try if not selection && is_reversible_selection_sequent sequent
+        then try_rule_selection sequent (get_formula_position is_whynot sequent), true
+        else raise NotApplicable
+        with NotApplicable ->
+    proof, selection;;
 
-let rec rec_apply_reversible_rule proof =
-    let new_proof = apply_reversible_rule proof in
+let rec rec_apply_reversible_rule selection proof =
+    let new_proof, new_selection = apply_reversible_rule selection proof in
     match new_proof with
         | Hypothesis_proof _ -> new_proof
         | _ -> let premises = get_premises new_proof in
-            let new_premises = List.map rec_apply_reversible_rule premises in
+            let new_premises = List.map (rec_apply_reversible_rule new_selection) premises in
             set_premises new_proof new_premises;;
 
 (* PROOF -> RULE REQUEST *)
@@ -460,4 +486,4 @@ let rec commute_permutations proof current_permutation =
         let new_proof = set_premises proof [commute_permutations p []] in
         if is_identity then new_proof else Exchange_proof (get_conclusion proof, perm, new_proof)
     | Exchange_proof (_, permutation, p) -> commute_permutations p (permute permutation perm)
-    | Hypothesis_proof s -> Hypothesis_proof (permute s perm);;
+    | Hypothesis_proof s -> Hypothesis_proof (permute s perm);;

sequent.ml

@@ -74,9 +74,11 @@ let get_unique_variable_names sequent =
 let is_top = function | Top -> true | _ -> false;;
 let is_bottom = function | Bottom -> true | _ -> false;;
 let is_par = function | Par _ -> true | _ -> false;;
+let is_whynot = function | Whynot _ -> true | _ -> false;;
 let is_double_whynot = function | Whynot (Whynot _) -> true | _ -> false;;
 let is_with = function | With _ -> true | _ -> false;;
 let is_ofcourse = function | Ofcourse _ -> true | _ -> false;;
+let is_atomic_or_zero = function | Litt _ | Dual _ | Zero -> true | _ -> false;;
 
 
 (* SEQUENT -> COQ *)