improving translation of subproof rule

carcara/src/translation/alethe_signature/theory.rs

@@ -86,17 +86,22 @@ impl AletheTheory {
         }
     }
 
-    // Utilities to help in the translation of steps using specific rules.
+    // Utilities to help in the translation of steps that use specific rules.
 
     // Helps in extracting the lhs and rhs of a conclusion clause of
     // the form (@cl ("=", t1, t2)).
-    // PRE: {conclusion is a EunoiaTerm of the form (@cl ("=", t1, t2)) }
-    pub fn extract_eq_lhs_rhs(conclusion: &EunoiaTerm) -> (EunoiaTerm, EunoiaTerm) {
+    // PRE: {conclusion is an EunoiaTerm of the form (@cl ("=", t1, t2)) }
+    pub fn extract_eq_lhs_rhs(&self, conclusion: &EunoiaTerm) -> (EunoiaTerm, EunoiaTerm) {
         match conclusion {
             // TODO: just assuming that cl and clause are correct
-            EunoiaTerm::App(.., clause) => match clause.as_slice() {
-                [EunoiaTerm::App(.., lhs_rhs)] => match lhs_rhs.as_slice() {
-                    [lhs, rhs] => (lhs.clone(), rhs.clone()),
+            EunoiaTerm::App(cl, clause) => match clause.as_slice() {
+                [EunoiaTerm::App(eq, lhs_rhs)] => match lhs_rhs.as_slice() {
+                    [lhs, rhs] => {
+                        assert!(*cl == self.cl);
+                        assert!(*eq == self.eq);
+                        (lhs.clone(), rhs.clone())
+                    }
+
                     _ => panic!(),
                 },
 
@@ -108,6 +113,31 @@ impl AletheTheory {
             }
         }
     }
+
+    // Helps in extracting the consequent of an implication in the form
+    // (@cl (not p1 or p2)).
+    // PRE: {conclusion is an EunoiaTerm of the form (@cl (not p1 or p2)) }
+    pub fn extract_consequent(&self, conclusion: &EunoiaTerm) -> EunoiaTerm {
+        match conclusion {
+            // @cl
+            EunoiaTerm::App(cl, disjuncts) => match disjuncts.as_slice() {
+                [.., consequent] => {
+                    // NOTE: not checking the structure of remaining disjuncts
+                    assert!(*cl == self.cl);
+                    consequent.clone()
+                }
+
+                _ => {
+                    println!("Actual conclusion: {:?}", conclusion);
+                    panic!()
+                }
+            },
+
+            _ => {
+                panic!();
+            }
+        }
+    }
 }
 
 impl Default for AletheTheory {

carcara/src/translation/eunoia.rs

@@ -689,7 +689,7 @@ impl EunoiaTranslator {
                 eunoia_arguments.push(EunoiaTerm::Id("context".to_owned()));
 
                 // Extract lhs and rhs
-                let (lhs, rhs) = AletheTheory::extract_eq_lhs_rhs(&conclusion);
+                let (lhs, rhs) = self.alethe_signature.extract_eq_lhs_rhs(&conclusion);
                 eunoia_arguments.push(lhs);
                 eunoia_arguments.push(rhs);
 
@@ -724,7 +724,7 @@ impl EunoiaTranslator {
                 eunoia_arguments.push(EunoiaTerm::Id("context".to_owned()));
 
                 // Extract lhs and rhs
-                let (lhs, rhs) = AletheTheory::extract_eq_lhs_rhs(&conclusion);
+                let (lhs, rhs) = self.alethe_signature.extract_eq_lhs_rhs(&conclusion);
 
                 eunoia_arguments.push(lhs);
 
@@ -752,19 +752,24 @@ impl EunoiaTranslator {
 
             "subproof" => {
                 // TODO: check this
-                // The command gets the formula proven through
-                // an "assumption", hence, we use StepPop.
-                // The discharged assumptions (received through the
-                // "discharge" formal parameter), will be passed to
-                // our mechanization in Eunoia as :assumption
-                let mut implied_conclusion: EunoiaTerm = conclusion;
+                // The command (as mechanized in Eunoia) gets the formula proven
+                // through an "assumption", hence, we use StepPop.
+                // The discharged assumptions (specified, in Alethe, through the
+                // "discharge" formal parameter), will be pushed
+                let mut implied_conclusion: EunoiaTerm =
+                    self.alethe_signature.extract_consequent(&conclusion);
+
+                // Assuming that the conclusion is of the form
+                // not φ1, ..., not φn, ψ
+                // extract ψ
+                let premise = self.alethe_signature.extract_consequent(&conclusion);
 
                 discharge.iter().for_each(|assumption| {
                     // TODO: we are discarding vector premises
                     match assumption.deref() {
                         ProofNode::Assume { id: _, depth: _, term } => {
                             implied_conclusion = EunoiaTerm::App(
-                                self.alethe_signature.or.clone(),
+                                self.alethe_signature.cl.clone(),
                                 vec![
                                     EunoiaTerm::App(
                                         self.alethe_signature.not.clone(),
@@ -778,7 +783,7 @@ impl EunoiaTranslator {
                                 name: id.to_owned(),
                                 conclusion_clause: Some(implied_conclusion.clone()),
                                 rule: self.alethe_signature.subproof.clone(),
-                                premises: EunoiaList { list: Vec::new() },
+                                premises: EunoiaList { list: vec![premise.clone()] },
                                 arguments: EunoiaList { list: eunoia_arguments.clone() },
                             });
                         }

carcara/src/translation/tests/alethe_signature/Alethe.eo

@@ -102,18 +102,19 @@
 )
 
 ;TODO
-(program check_subproof ((Premises Bool) (Conclusion Bool))
-  (Bool Bool) Bool
+(program check_subproof ((Premises Bool) (Conclusion Bool) (Conclusion_given Bool))
+  (Bool Bool Bool) Bool
   (
-   ((check_subproof Premises Conclusion) true)
+   ((check_subproof Premises Conclusion Conclusion_given) true)
   )
 )
 
 ;TODO: test if the list here works well
-(declare-rule subproof ((F Bool))
+(declare-rule subproof ((F Bool) (G Bool :list))
   ; TODO: why is it an assumption?
   :assumption F ;has no cl!
-  :requires (((check_subproof (not F) eo::conclusion) true))
+  :premises (G)
+  :requires (((check_subproof (not F) G eo::conclusion) true))
   :conclusion-given
 )