Enforce that variables can only be simple symbols

carcara/src/ast/mod.rs

@@ -544,7 +544,7 @@ pub enum Term {
     Const(Constant),
 
     /// A variable, consisting of an identifier and a sort.
-    Var(Ident, Rc<Term>),
+    Var(String, Rc<Term>),
 
     /// An application of a function to one or more terms.
     App(Rc<Term>, Vec<Rc<Term>>),
@@ -570,7 +570,7 @@ pub enum Term {
 
 impl From<SortedVar> for Term {
     fn from(var: SortedVar) -> Self {
-        Term::Var(Ident::Simple(var.0), var.1)
+        Term::Var(var.0, var.1)
     }
 }
 
@@ -592,7 +592,7 @@ impl Term {
 
     /// Constructs a new variable term.
     pub fn new_var(name: impl Into<String>, sort: Rc<Term>) -> Self {
-        Term::Var(Ident::Simple(name.into()), sort)
+        Term::Var(name.into(), sort)
     }
 
     /// Returns the sort of this term. This does not make use of a cache --- if possible, prefer to
@@ -666,14 +666,13 @@ impl Term {
 
     /// Returns `true` if the term is a variable.
     pub fn is_var(&self) -> bool {
-        matches!(self, Term::Var(Ident::Simple(_), _))
+        matches!(self, Term::Var(_, _))
     }
 
-    /// Tries to extract the variable name from a term. Returns `Some` if the term is a variable
-    /// with a simple identifier.
+    /// Tries to extract the variable name from a term. Returns `Some` if the term is a variable.
     pub fn as_var(&self) -> Option<&str> {
         match self {
-            Term::Var(Ident::Simple(var), _) => Some(var.as_str()),
+            Term::Var(var, _) => Some(var.as_str()),
             _ => None,
         }
     }
@@ -720,7 +719,7 @@ impl Term {
 
     /// Returns `true` if the term is the boolean constant `true`.
     pub fn is_bool_true(&self) -> bool {
-        if let Term::Var(Ident::Simple(name), sort) = self {
+        if let Term::Var(name, sort) = self {
             sort.as_sort() == Some(&Sort::Bool) && name == "true"
         } else {
             false
@@ -729,7 +728,7 @@ impl Term {
 
     /// Returns `true` if the term is the boolean constant `false`.
     pub fn is_bool_false(&self) -> bool {
-        if let Term::Var(Ident::Simple(name), sort) = self {
+        if let Term::Var(name, sort) = self {
             sort.as_sort() == Some(&Sort::Bool) && name == "false"
         } else {
             false
@@ -828,20 +827,3 @@ pub enum Constant {
     /// A string literal term.
     String(String),
 }
-
-/// An identifier.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
-pub enum Ident {
-    /// A simple identifier, consisting of a symbol.
-    Simple(String),
-
-    /// An indexed identifier, consisting of a symbol and one or more indices.
-    Indexed(String, Vec<IdentIndex>),
-}
-
-/// An index for an indexed identifier. This can be either a numeral or a symbol.
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
-pub enum IdentIndex {
-    Numeral(u64),
-    Symbol(String),
-}

carcara/src/ast/polyeq.rs

@@ -7,9 +7,7 @@
 //! - `alpha_equiv` compares terms by alpha-equivalence, meaning it implements equality of terms
 //! modulo renaming of bound variables.
 
-use super::{
-    BindingList, Ident, Operator, ProofArg, ProofCommand, ProofStep, Rc, Sort, Subproof, Term,
-};
+use super::{BindingList, Operator, ProofArg, ProofCommand, ProofStep, Rc, Sort, Subproof, Term};
 use crate::utils::HashMapStack;
 use std::time::{Duration, Instant};
 
@@ -192,16 +190,14 @@ impl Polyeq for Term {
     fn eq(comp: &mut PolyeqComparator, a: &Self, b: &Self) -> bool {
         match (a, b) {
             (Term::Const(a), Term::Const(b)) => a == b,
-            (Term::Var(Ident::Simple(a), a_sort), Term::Var(Ident::Simple(b), b_sort))
-                if comp.de_bruijn_map.is_some() =>
-            {
+            (Term::Var(a, a_sort), Term::Var(b, b_sort)) if comp.de_bruijn_map.is_some() => {
                 // If we are checking for alpha-equivalence, and we encounter two variables, we
                 // check that they are equivalent using the De Bruijn map
-                let db = comp.de_bruijn_map.as_mut().unwrap();
-                db.compare(a, b) && Polyeq::eq(comp, a_sort, b_sort)
-            }
-            (Term::Var(a, a_sort), Term::Var(b, b_sort)) => {
-                a == b && Polyeq::eq(comp, a_sort, b_sort)
+                if let Some(db) = comp.de_bruijn_map.as_mut() {
+                    db.compare(a, b) && Polyeq::eq(comp, a_sort, b_sort)
+                } else {
+                    a == b && Polyeq::eq(comp, a_sort, b_sort)
+                }
             }
             (Term::App(f_a, args_a), Term::App(f_b, args_b)) => {
                 Polyeq::eq(comp, f_a, f_b) && Polyeq::eq(comp, args_a, args_b)

carcara/src/ast/printer.rs

@@ -174,7 +174,7 @@ impl<'a> AlethePrinter<'a> {
     fn write_raw_term(&mut self, term: &Term) -> io::Result<()> {
         match term {
             Term::Const(c) => write!(self.inner, "{}", c),
-            Term::Var(iden, _) => write!(self.inner, "{}", iden),
+            Term::Var(name, _) => write!(self.inner, "{}", quote_symbol(name)),
             Term::App(func, args) => self.write_s_expr(func, args),
             Term::Op(op, args) => self.write_s_expr(op, args),
             Term::Sort(sort) => write!(self.inner, "{}", sort),
@@ -364,26 +364,6 @@ impl fmt::Display for Constant {
     }
 }
 
-impl fmt::Display for Ident {
-    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        match self {
-            Ident::Simple(s) => write!(f, "{}", quote_symbol(s)),
-            Ident::Indexed(s, indices) => {
-                write_s_expr(f, format!("_ {}", quote_symbol(s)), indices)
-            }
-        }
-    }
-}
-
-impl fmt::Display for IdentIndex {
-    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        match self {
-            IdentIndex::Numeral(n) => write!(f, "{}", n),
-            IdentIndex::Symbol(s) => write!(f, "{}", quote_symbol(s)),
-        }
-    }
-}
-
 impl fmt::Display for Quantifier {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
         write!(

carcara/src/parser/error.rs

@@ -1,10 +1,6 @@
 //! The types for parser errors.
 
-use crate::{
-    ast::{Ident, Sort},
-    parser::Token,
-    utils::Range,
-};
+use crate::{ast::Sort, parser::Token, utils::Range};
 use rug::Integer;
 use std::fmt;
 use thiserror::Error;
@@ -55,7 +51,7 @@ pub enum ParserError {
 
     /// The parser encountered an identifier that was not defined.
     #[error("identifier '{0}' is not defined")]
-    UndefinedIden(Ident),
+    UndefinedIden(String),
 
     /// The parser encountered a sort that was not defined.
     #[error("sort '{0}' is not defined")]

carcara/src/parser/mod.rs

@@ -77,7 +77,7 @@ enum AnchorArg {
 /// pool used by the parser.
 #[derive(Default)]
 struct ParserState {
-    symbol_table: HashMapStack<HashCache<Ident>, Rc<Term>>,
+    symbol_table: HashMapStack<HashCache<String>, Rc<Term>>,
     function_defs: IndexMap<String, FunctionDef>,
     sort_declarations: IndexMap<String, usize>,
     step_ids: HashMapStack<HashCache<String>, usize>,
@@ -104,7 +104,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
         let bool_sort = pool.add(Term::Sort(Sort::Bool));
 
         for iden in ["true", "false"] {
-            let iden = HashCache::new(Ident::Simple(iden.to_owned()));
+            let iden = HashCache::new(iden.to_owned());
             state.symbol_table.insert(iden, bool_sort.clone());
         }
 
@@ -145,9 +145,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
 
     /// Inserts a `SortedVar` into the parser symbol table.
     fn insert_sorted_var(&mut self, (symbol, sort): SortedVar) {
-        self.state
-            .symbol_table
-            .insert(HashCache::new(Ident::Simple(symbol)), sort);
+        self.state.symbol_table.insert(HashCache::new(symbol), sort);
     }
 
     /// Shortcut for `self.problem.as_mut().unwrap().0`
@@ -161,7 +159,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
     }
 
     /// Constructs and sort checks a variable term.
-    fn make_var(&mut self, iden: Ident) -> Result<Rc<Term>, ParserError> {
+    fn make_var(&mut self, iden: String) -> Result<Rc<Term>, ParserError> {
         let cached = HashCache::new(iden);
         let sort = match self.state.symbol_table.get(&cached) {
             Some(s) => s.clone(),
@@ -1062,8 +1060,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
                     self.make_op(op, args)
                         .map_err(|err| Error::Parser(err, pos))?
                 } else {
-                    self.make_var(Ident::Simple(s))
-                        .map_err(|err| Error::Parser(err, pos))?
+                    self.make_var(s).map_err(|err| Error::Parser(err, pos))?
                 });
             }
             (Token::OpenParen, _) => return self.parse_application(),