Adds support for Strings and Regular Expressions operators in AST

carcara/src/ast/mod.rs

@@ -272,6 +272,107 @@ pub enum Operator {
 
     /// The `store` operator.
     Store,
+
+    // Strings
+    /// The `str.++` operator.
+    StrConcat,
+
+    /// The `str.len` operator.
+    StrLen,
+
+    /// The `str.<` operator.
+    LexOrdering,
+
+    /// The `str.<=` operator.
+    ReflexiveClosure,
+
+    /// The `str.at` operator.
+    CharAt,
+
+    /// The `str.substr` operator.
+    Substring,
+
+    /// The `str.prefixof` operator.
+    PrefixOf,
+
+    /// The `str.suffixof` operator.
+    SuffixOf,
+
+    /// The `str.contains` operator.
+    Contains,
+
+    /// The `str.indexof` operator.
+    IndexOf,
+
+    /// The `str.replace` operator.
+    Replace,
+
+    /// The `str.replace_all` operator.
+    ReplaceAll,
+
+    /// The `str.replace_re` operator.
+    ReplaceRe,
+
+    /// The `str.replace_re_all` operator.
+    ReplaceReAll,
+
+    /// The `str.is_digit` operator.
+    StrIsDigit,
+
+    /// The `str.to_code` operator.
+    StrToCode,
+
+    /// The `str.from_code` operator.
+    StrFromCode,
+
+    /// The `str.to_int` operator.
+    StrToInt,
+
+    /// The `str.from_int` operator.
+    StrFromInt,
+
+    // Regular Expressions
+    /// The `str.to_re` operator.
+    StrToRe,
+
+    /// The `str.in_re` operator.
+    StrInRe,
+
+    /// The `re.none` operator.
+    ReNone,
+
+    /// The `re.all` operator.
+    ReAll,
+
+    /// The `re.allchar` operator.
+    ReAllChar,
+
+    /// The `re.++` operator.
+    ReConcat,
+
+    /// The `re.union` operator.
+    ReUnion,
+
+    /// The `re.inter` operator.
+    ReIntersection,
+
+    /// The `re.*` operator.
+    ReKleeneClosure,
+
+    /// The `re.comp` operator.
+    ReComplement,
+
+    /// The `re.diff` operator.
+    ReDiff,
+
+    /// The `re.+` operator.
+    ReKleeneCross,
+
+    /// The `re.opt` operator.
+    ReOption,
+
+    /// The `re.range` operator.
+    ReRange,
 }
 
 impl_str_conversion_traits!(Operator {
@@ -301,6 +402,41 @@ impl_str_conversion_traits!(Operator {
 
     Select: "select",
     Store: "store",
+
+    StrConcat: "str.++",
+    StrLen: "str.len",
+    LexOrdering: "str.<",
+    ReflexiveClosure: "str.<=",
+    CharAt: "str.at",
+    Substring: "str.substr",
+    PrefixOf: "str.prefixof",
+    SuffixOf: "str.suffixof",
+    Contains: "str.contains",
+    IndexOf: "str.indexof",
+    Replace: "str.replace",
+    ReplaceAll: "str.replace_all",
+    ReplaceRe: "str.replace_re",
+    ReplaceReAll: "str.replace_re_all",
+    StrIsDigit: "str.is_digit",
+    StrToCode: "str.to_code",
+    StrFromCode: "str.from_code",
+    StrToInt: "str.to_int",
+    StrFromInt: "str.from_int",
+
+    StrToRe: "str.to_re",
+    StrInRe: "str.in_re",
+    ReNone: "re.none",
+    ReAll: "re.all",
+    ReAllChar: "re.allchar",
+    ReConcat: "re.++",
+    ReUnion: "re.union",
+    ReIntersection: "re.inter",
+    ReKleeneClosure: "re.*",
+    ReComplement: "re.comp",
+    ReDiff: "re.diff",
+    ReKleeneCross: "re.+",
+    ReOption: "re.opt",
+    ReRange: "re.range",
 });
 
 /// A variable and an associated sort.
@@ -333,6 +469,9 @@ pub enum Sort {
     /// The `String` primitive sort.
     String,
 
+    /// The `RegLan` primitive sort.
+    RegLan,
+
     /// An `Array` sort.
     ///
     /// The two associated terms are the sort arguments for this sort.

carcara/src/ast/pool/mod.rs

@@ -116,7 +116,14 @@ impl PrimitivePool {
                 | Operator::GreaterThan
                 | Operator::LessEq
                 | Operator::GreaterEq
-                | Operator::IsInt => Sort::Bool,
+                | Operator::IsInt
+                | Operator::LexOrdering
+                | Operator::ReflexiveClosure
+                | Operator::PrefixOf
+                | Operator::SuffixOf
+                | Operator::Contains
+                | Operator::StrIsDigit
+                | Operator::StrInRe => Sort::Bool,
                 Operator::Ite => self.compute_sort(&args[1]).as_sort().unwrap().clone(),
                 Operator::Add | Operator::Sub | Operator::Mult => {
                     if args
@@ -135,6 +142,31 @@ impl PrimitivePool {
                     _ => unreachable!(),
                 },
                 Operator::Store => self.compute_sort(&args[0]).as_sort().unwrap().clone(),
+                Operator::StrLen | Operator::IndexOf | Operator::StrToCode | Operator::StrToInt => {
+                    Sort::Int
+                }
+                Operator::StrConcat
+                | Operator::CharAt
+                | Operator::Substring
+                | Operator::Replace
+                | Operator::ReplaceAll
+                | Operator::ReplaceRe
+                | Operator::ReplaceReAll
+                | Operator::StrFromCode
+                | Operator::StrFromInt => Sort::String,
+                Operator::StrToRe
+                | Operator::ReNone
+                | Operator::ReAll
+                | Operator::ReAllChar
+                | Operator::ReConcat
+                | Operator::ReUnion
+                | Operator::ReIntersection
+                | Operator::ReKleeneClosure
+                | Operator::ReComplement
+                | Operator::ReDiff
+                | Operator::ReKleeneCross
+                | Operator::ReOption
+                | Operator::ReRange => Sort::RegLan,
             },
             Term::App(f, _) => {
                 match self.compute_sort(f).as_sort().unwrap() {

carcara/src/ast/printer.rs

@@ -426,6 +426,7 @@ impl fmt::Display for Sort {
             Sort::Int => write!(f, "Int"),
             Sort::Real => write!(f, "Real"),
             Sort::String => write!(f, "String"),
+            Sort::RegLan => write!(f, "RegLan"),
             Sort::Array(x, y) => write_s_expr(f, "Array", &[x, y]),
         }
     }

carcara/src/parser/mod.rs

@@ -102,10 +102,12 @@ impl<'a, R: BufRead> Parser<'a, R> {
     pub fn new(pool: &'a mut PrimitivePool, config: Config, input: R) -> CarcaraResult<Self> {
         let mut state = ParserState::default();
         let bool_sort = pool.add(Term::Sort(Sort::Bool));
+
         for iden in ["true", "false"] {
             let iden = HashCache::new(Ident::Simple(iden.to_owned()));
             state.symbol_table.insert(iden, bool_sort.clone());
         }
+
         let mut lexer = Lexer::new(input)?;
         let (current_token, current_position) = lexer.next_token()?;
         Ok(Parser {
@@ -327,6 +329,87 @@ impl<'a, R: BufRead> Parser<'a, R> {
                     }
                 }
             }
+            Operator::StrConcat => {
+                assert_num_args(&args, 2..)?;
+                for s in sorts {
+                    SortError::assert_eq(&Sort::String, s.as_sort().unwrap())?;
+                }
+            }
+            Operator::StrLen | Operator::StrIsDigit | Operator::StrToCode | Operator::StrToInt => {
+                assert_num_args(&args, 1)?;
+                SortError::assert_eq(&Sort::String, sorts[0].as_sort().unwrap())?;
+            }
+            Operator::LexOrdering
+            | Operator::ReflexiveClosure
+            | Operator::PrefixOf
+            | Operator::SuffixOf
+            | Operator::Contains
+            | Operator::ReRange => {
+                assert_num_args(&args, 2)?;
+                SortError::assert_eq(&Sort::String, sorts[0].as_sort().unwrap())?;
+                SortError::assert_eq(&Sort::String, sorts[1].as_sort().unwrap())?;
+            }
+            Operator::CharAt => {
+                assert_num_args(&args, 2)?;
+                SortError::assert_eq(&Sort::String, sorts[0].as_sort().unwrap())?;
+                SortError::assert_eq(&Sort::Int, sorts[1].as_sort().unwrap())?;
+            }
+            Operator::Substring => {
+                assert_num_args(&args, 3)?;
+                SortError::assert_eq(&Sort::String, sorts[0].as_sort().unwrap())?;
+                SortError::assert_eq(&Sort::Int, sorts[1].as_sort().unwrap())?;
+                SortError::assert_eq(&Sort::Int, sorts[2].as_sort().unwrap())?;
+            }
+            Operator::IndexOf => {
+                assert_num_args(&args, 3)?;
+                SortError::assert_eq(&Sort::String, sorts[0].as_sort().unwrap())?;
+                SortError::assert_eq(&Sort::String, sorts[1].as_sort().unwrap())?;
+                SortError::assert_eq(&Sort::Int, sorts[2].as_sort().unwrap())?;
+            }
+            Operator::Replace | Operator::ReplaceAll => {
+                assert_num_args(&args, 3)?;
+                SortError::assert_eq(&Sort::String, sorts[0].as_sort().unwrap())?;
+                SortError::assert_eq(&Sort::String, sorts[1].as_sort().unwrap())?;
+                SortError::assert_eq(&Sort::String, sorts[2].as_sort().unwrap())?;
+            }
+            Operator::StrFromCode | Operator::StrFromInt => {
+                assert_num_args(&args, 1)?;
+                SortError::assert_eq(&Sort::Int, sorts[0].as_sort().unwrap())?;
+            }
+            Operator::StrToRe => {
+                assert_num_args(&args, 1)?;
+                SortError::assert_eq(&Sort::String, sorts[0].as_sort().unwrap())?;
+            }
+            Operator::StrInRe => {
+                assert_num_args(&args, 2)?;
+                SortError::assert_eq(&Sort::String, sorts[0].as_sort().unwrap())?;
+                SortError::assert_eq(&Sort::RegLan, sorts[1].as_sort().unwrap())?;
+            }
+            Operator::ReNone | Operator::ReAll | Operator::ReAllChar => {
+                assert_num_args(&args, 0)?;
+            }
+            Operator::ReConcat
+            | Operator::ReUnion
+            | Operator::ReIntersection
+            | Operator::ReDiff => {
+                assert_num_args(&args, 2..)?;
+                for s in sorts {
+                    SortError::assert_eq(&Sort::RegLan, s.as_sort().unwrap())?;
+                }
+            }
+            Operator::ReKleeneClosure
+            | Operator::ReComplement
+            | Operator::ReKleeneCross
+            | Operator::ReOption => {
+                assert_num_args(&args, 1)?;
+                SortError::assert_eq(&Sort::RegLan, sorts[0].as_sort().unwrap())?;
+            }
+            Operator::ReplaceRe | Operator::ReplaceReAll => {
+                assert_num_args(&args, 3)?;
+                SortError::assert_eq(&Sort::String, sorts[0].as_sort().unwrap())?;
+                SortError::assert_eq(&Sort::RegLan, sorts[1].as_sort().unwrap())?;
+                SortError::assert_eq(&Sort::String, sorts[2].as_sort().unwrap())?;
+            }
         }
         Ok(self.pool.add(Term::Op(op, args)))
     }
@@ -973,6 +1056,11 @@ impl<'a, R: BufRead> Parser<'a, R> {
                             pos,
                         ));
                     }
+                } else if let Ok(op) = Operator::from_str(&s) {
+                    let args = Vec::new();
+
+                    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))?
@@ -1223,15 +1311,14 @@ impl<'a, R: BufRead> Parser<'a, R> {
         };
 
         let sort = match name.as_str() {
-            "Bool" | "Int" | "Real" | "String" if !args.is_empty() => Err(Error::Parser(
-                ParserError::WrongNumberOfArgs(0.into(), args.len()),
-                pos,
-            )),
+            "Bool" | "Int" | "Real" | "String" | "RegLan" if !args.is_empty() => Err(
+                Error::Parser(ParserError::WrongNumberOfArgs(0.into(), args.len()), pos),
+            ),
             "Bool" => Ok(Sort::Bool),
             "Int" => Ok(Sort::Int),
             "Real" => Ok(Sort::Real),
             "String" => Ok(Sort::String),
-
+            "RegLan" => Ok(Sort::RegLan),
             "Array" => match args.as_slice() {
                 [x, y] => Ok(Sort::Array(x.clone(), y.clone())),
                 _ => Err(Error::Parser(