From 42fcde5653e967f093b60bce42bcbf122a3e8ed0 Mon Sep 17 00:00:00 2001 From: Mallku2 Date: Tue, 19 Nov 2024 14:50:32 -0300 Subject: [PATCH] improving translation of subproof rule --- .../translation/alethe_signature/theory.rs | 42 ++++++++++++++++--- carcara/src/translation/eunoia.rs | 25 ++++++----- .../tests/alethe_signature/Alethe.eo | 11 ++--- 3 files changed, 57 insertions(+), 21 deletions(-) diff --git a/carcara/src/translation/alethe_signature/theory.rs b/carcara/src/translation/alethe_signature/theory.rs index 2761d238..166757ab 100644 --- a/carcara/src/translation/alethe_signature/theory.rs +++ b/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 { diff --git a/carcara/src/translation/eunoia.rs b/carcara/src/translation/eunoia.rs index 6c6d9050..7b2b9603 100644 --- a/carcara/src/translation/eunoia.rs +++ b/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() }, }); } diff --git a/carcara/src/translation/tests/alethe_signature/Alethe.eo b/carcara/src/translation/tests/alethe_signature/Alethe.eo index c136aa26..8ecb6f86 100644 --- a/carcara/src/translation/tests/alethe_signature/Alethe.eo +++ b/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 )