Parse existentials

Author: coord-e

src/annot.rs

@@ -12,6 +12,7 @@ use rustc_ast::token::{BinOpToken, Delimiter, LitKind, Token, TokenKind};
 use rustc_ast::tokenstream::{RefTokenTreeCursor, Spacing, TokenStream, TokenTree};
 use rustc_index::IndexVec;
 use rustc_span::symbol::Ident;
+use std::collections::HashMap;
 
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
@@ -185,6 +186,7 @@ impl<T> FormulaOrTerm<T> {
 struct Parser<'a, T> {
     resolver: T,
     cursor: RefTokenTreeCursor<'a>,
+    formula_existentials: HashMap<String, chc::Sort>,
 }
 
 impl<'a, T> Parser<'a, T>
@@ -232,6 +234,15 @@ where
         }
     }
 
+    fn expect_next_ident(&mut self) -> Result<Ident> {
+        let t = self.next_token("ident")?;
+        if let Some((ident, _)) = t.ident() {
+            Ok(ident)
+        } else {
+            Err(ParseAttrError::unexpected_token("ident", t.clone()))
+        }
+    }
+
     fn consume(&mut self) {
         self.cursor.next().unwrap();
     }
@@ -296,6 +307,7 @@ where
                 let mut parser = Parser {
                     resolver: self.boxed_resolver(),
                     cursor: s.trees(),
+                    formula_existentials: self.formula_existentials.clone(),
                 };
                 let formula_or_term = parser.parse_formula_or_term_or_tuple()?;
                 parser.end_of_input()?;
@@ -305,9 +317,17 @@ where
         };
 
         let formula_or_term = if let Some((ident, _)) = t.ident() {
-            match ident.as_str() {
-                "true" => FormulaOrTerm::Formula(chc::Formula::top()),
-                "false" => FormulaOrTerm::Formula(chc::Formula::bottom()),
+            match (
+                ident.as_str(),
+                self.formula_existentials.get(ident.name.as_str()),
+            ) {
+                ("true", _) => FormulaOrTerm::Formula(chc::Formula::top()),
+                ("false", _) => FormulaOrTerm::Formula(chc::Formula::bottom()),
+                (_, Some(sort)) => {
+                    let var =
+                        chc::Term::FormulaExistentialVar(sort.clone(), ident.name.to_string());
+                    FormulaOrTerm::Term(var, sort.clone())
+                }
                 _ => {
                     let (v, sort) = self.resolve(ident)?;
                     FormulaOrTerm::Term(chc::Term::var(v), sort)
@@ -575,8 +595,102 @@ where
         Ok(formula_or_term)
     }
 
+    fn parse_exists(&mut self) -> Result<FormulaOrTerm<T::Output>> {
+        match self.look_ahead_token(0) {
+            Some(Token {
+                kind: TokenKind::Ident(sym, _),
+                ..
+            }) if sym.as_str() == "exists" => {
+                self.consume();
+                let mut vars = Vec::new();
+                loop {
+                    let ident = self.expect_next_ident()?;
+                    self.expect_next_token(TokenKind::Colon, ":")?;
+                    let sort = self.parse_sort()?;
+                    vars.push((ident.name.to_string(), sort));
+                    match self.next_token(". or ,")? {
+                        Token {
+                            kind: TokenKind::Comma,
+                            ..
+                        } => {}
+                        Token {
+                            kind: TokenKind::Dot,
+                            ..
+                        } => break,
+                        t => return Err(ParseAttrError::unexpected_token("., or ,", t.clone())),
+                    }
+                }
+                self.formula_existentials.extend(vars.iter().cloned());
+                let formula = self
+                    .parse_formula_or_term()?
+                    .into_formula()
+                    .ok_or_else(|| ParseAttrError::unexpected_term("in exists formula"))?;
+                for (name, _) in &vars {
+                    self.formula_existentials.remove(name);
+                }
+                return Ok(FormulaOrTerm::Formula(chc::Formula::exists(vars, formula)));
+            }
+            _ => self.parse_binop_5(),
+        }
+    }
+
     fn parse_formula_or_term(&mut self) -> Result<FormulaOrTerm<T::Output>> {
-        self.parse_binop_5()
+        self.parse_exists()
+    }
+
+    fn parse_sort(&mut self) -> Result<chc::Sort> {
+        let tt = self.next_token_tree("sort")?.clone();
+        match tt {
+            TokenTree::Token(
+                Token {
+                    kind: TokenKind::Ident(sym, _),
+                    ..
+                },
+                _,
+            ) => {
+                let sort = match sym.as_str() {
+                    "bool" => chc::Sort::bool(),
+                    "int" => chc::Sort::int(),
+                    "string" => unimplemented!(),
+                    "null" => chc::Sort::null(),
+                    "fn" => unimplemented!(),
+                    _ => unimplemented!(),
+                };
+                Ok(sort)
+            }
+            //TokenTree::Token(
+            //    Token {
+            //        kind: TokenKind::Gt,
+            //        ..
+            //    },
+            //    _,
+            //) => {
+            //}
+            TokenTree::Delimited(_, _, Delimiter::Parenthesis, ts) => {
+                let mut parser = Parser {
+                    resolver: self.boxed_resolver(),
+                    cursor: ts.trees(),
+                    formula_existentials: self.formula_existentials.clone(),
+                };
+                let mut sorts = Vec::new();
+                loop {
+                    sorts.push(parser.parse_sort()?);
+                    match parser.look_ahead_token(0) {
+                        Some(Token {
+                            kind: TokenKind::Comma,
+                            ..
+                        }) => {
+                            parser.consume();
+                        }
+                        None => break,
+                        Some(t) => return Err(ParseAttrError::unexpected_token(",", t.clone())),
+                    }
+                }
+                parser.end_of_input()?;
+                Ok(chc::Sort::tuple(sorts).into())
+            }
+            t => Err(ParseAttrError::unexpected_token_tree("sort", t.clone())),
+        }
     }
 
     fn parse_ty(&mut self) -> Result<rty::Type<T::Output>> {
@@ -662,6 +776,7 @@ where
                 let mut parser = Parser {
                     resolver: self.boxed_resolver(),
                     cursor: ts.trees(),
+                    formula_existentials: self.formula_existentials.clone(),
                 };
                 let mut rtys = Vec::new();
                 loop {
@@ -697,6 +812,7 @@ where
         let mut parser = Parser {
             resolver: self.boxed_resolver(),
             cursor: ts.trees(),
+            formula_existentials: self.formula_existentials.clone(),
         };
         let self_ident = if matches!(
             parser.look_ahead_token(1),
@@ -720,6 +836,7 @@ where
         let mut parser = Parser {
             resolver: RefinementResolver::new(self.boxed_resolver()),
             cursor: parser.cursor,
+            formula_existentials: self.formula_existentials.clone(),
         };
         if let Some(self_ident) = self_ident {
             parser.resolver.set_self(self_ident, ty.to_sort());
@@ -859,6 +976,7 @@ where
         let mut parser = Parser {
             resolver: &self.resolver,
             cursor: ts.trees(),
+            formula_existentials: Default::default(),
         };
         let rty = parser.parse_rty()?;
         parser.end_of_input()?;
@@ -869,6 +987,7 @@ where
         let mut parser = Parser {
             resolver: &self.resolver,
             cursor: ts.trees(),
+            formula_existentials: Default::default(),
         };
         let formula = parser.parse_annot_formula()?;
         parser.end_of_input()?;

src/chc.rs

@@ -1228,6 +1228,10 @@ impl<V> Formula<V> {
         }
     }
 
+    pub fn exists(vars: Vec<(String, Sort)>, body: Self) -> Self {
+        Formula::Exists(vars, Box::new(body))
+    }
+
     pub fn subst_var<F, W>(self, f: F) -> Formula<W>
     where
         F: FnMut(V) -> Term<W>,