Pretty printer. Modified tests for EunoiaTranslator, using Printer. S…

…cripts for generation of Alethe certificates, transpilation and checking with Ethos

carcara/src/ast/printer.rs

@@ -50,7 +50,7 @@ pub fn write_lia_smt_instance(
     printer.write_lia_smt_instance(clause)
 }
 
-trait PrintProof {
+pub trait PrintProof {
     fn write_proof(&mut self, proof: &Proof) -> io::Result<()>;
 }
 

carcara/src/translation/alethe_signature/theory.rs

@@ -1,55 +1,60 @@
 /// Definition of Alethe in Eunoia, following [AletheInAlf](https://github.com/cvc5/aletheinalf/).
 use std::string::String;
 // TODO: import everything once
-use crate::translation::eunoia_ast::EunoiaConsAttr::*;
-use crate::translation::eunoia_ast::EunoiaKindParam::*;
-use crate::translation::eunoia_ast::EunoiaTerm::*;
-use crate::translation::eunoia_ast::EunoiaType::*;
-use crate::translation::eunoia_ast::EunoiaTypeAttr::*;
 use crate::translation::eunoia_ast::*;
 
 // TODO: THIS IS ONLY DONE TO AVOID THE COMPLEXITIES OF DECLARING
 // AND DEALING WITH GLOBALS IN RUST.
 pub struct AletheTheory {
-    // Built-in operators
-    pub cl: EunoiaCommand,
-    pub ite: EunoiaCommand,
-    // Contexts
+    // Built-in operators.
+    pub cl: Symbol,
+    pub ite: Symbol,
+
+    // Logical operators.
+    pub and: Symbol,
+
+    // Comparison.
+    pub eq: Symbol,
+    pub lt: Symbol,
+    pub le: Symbol,
+    pub gt: Symbol,
+    pub ge: Symbol,
+
+    // Rules' names.
+    pub let_rule: Symbol,
+
+    // Context representation and manipulation.
+    // To bind variables in a context.
+    pub var: Symbol,
+
+    // Binders.
+    pub let_binder: Symbol,
 }
 
 impl AletheTheory {
     pub fn new() -> Self {
         AletheTheory {
-            cl: EunoiaCommand::DeclareConst {
-                name: String::from("@cl"),
-                eunoia_type: EunoiaTerm::Type(Fun(Vec::new(), vec![Bool, Bool], Box::new(Bool))),
-                attrs: vec![RightAssocNil(False)],
-            },
-            ite: EunoiaCommand::DeclareConst {
-                name: String::from("ite"),
-                eunoia_type: EunoiaTerm::Type(Fun(
-                    vec![KindParam(
-                        EunoiaType::Type,
-                        vec![EunoiaTypeAttr::Var(String::from("A")), Implicit],
-                    )],
-                    vec![Bool, Name(String::from("A")), Name(String::from("A"))],
-                    Box::new(Name(String::from("A"))),
-                )),
-                attrs: Vec::new(),
-            },
-        }
-    }
+            cl: String::from("@cl"),
+            ite: String::from("ite"),
+
+            // Logical operators.
+            and: String::from("and"),
+
+            // Comparison.
+            eq: String::from("="),
+            lt: String::from("<"),
+            le: String::from("<="),
+            gt: String::from(">"),
+            ge: String::from(">="),
+
+            // Rules' names.
+            let_rule: String::from("let_elim"),
 
-    /// Accessors: simple API to query "Alethe in Eunoia"'s signature.
-    pub fn get_cl_symbol(&self) -> Symbol {
-        // TODO: some better type-error free way of accessing cl.name?
-        match &self.cl {
-            EunoiaCommand::DeclareConst { name, .. } => name.clone(),
+            // Context representation and manipulation.
+            var: String::from("@var"),
 
-            _ => {
-                // NOTE: it shouldn't be defined as something else...
-                panic!()
-            }
+            // Binders.
+            let_binder: String::from("@let"),
         }
     }
 }