liquid_fixpoint/
parser.rs

1use std::fmt;
2
3use indexmap::IndexMap;
4use itertools::Itertools;
5
6use crate::{
7    BinOp, BinRel, Bind, Constant, Expr, Identifier, Pred, Sort, SortCtor, ThyFunc, Types,
8    constraint::Quantifier,
9    sexp::{Atom, ParseError as SexpParseError, Sexp},
10};
11
12#[derive(Debug)]
13pub enum ParseError {
14    SexpParseError(SexpParseError),
15    MalformedSexpError(String),
16}
17
18impl ParseError {
19    pub fn err(msg: impl Into<String>) -> Self {
20        ParseError::MalformedSexpError(msg.into())
21    }
22}
23
24impl Identifier for String {
25    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
26        write!(f, "{self}")
27    }
28}
29
30pub trait FromSexp<T: Types> {
31    fn fresh_var(&mut self) -> T::Var;
32    // These are the only methods required to implement FromSexp
33    fn var(&self, name: &str) -> Result<T::Var, ParseError>;
34    fn kvar(&self, name: &str) -> Result<T::KVar, ParseError>;
35    fn string(&self, s: &str) -> Result<T::String, ParseError>;
36    fn sort(&self, name: &str) -> Result<T::Sort, ParseError>;
37    fn into_wrapper(self) -> FromSexpWrapper<T, Self>
38    where
39        Self: Sized,
40    {
41        FromSexpWrapper { parser: self, _phantom: std::marker::PhantomData, scopes: vec![] }
42    }
43}
44
45pub struct FromSexpWrapper<T: Types, Parser> {
46    pub parser: Parser,
47    pub _phantom: std::marker::PhantomData<T>,
48    scopes: Vec<IndexMap<String, T::Var>>,
49}
50
51type KvarSolution<T> = (Vec<(<T as Types>::Var, Sort<T>)>, Expr<T>);
52
53impl<T, Parser: FromSexp<T>> FromSexpWrapper<T, Parser>
54where
55    T: Types,
56{
57    fn parse_bv_size(&self, sexp: &Sexp) -> Result<Sort<T>, ParseError> {
58        match sexp {
59            Sexp::Atom(Atom::S(s)) if s.starts_with("Size") => {
60                let maybe_size = s
61                    .strip_prefix("Size")
62                    .and_then(|sz_str| sz_str.parse::<u32>().ok());
63                if let Some(size) = maybe_size {
64                    Ok(Sort::BvSize(size))
65                } else {
66                    Err(ParseError::err("Could not parse number for bvsize"))
67                }
68            }
69            _ => Err(ParseError::err("Expected bitvec size to be in the form Size{\\d+}")),
70        }
71    }
72
73    pub fn parse_name(&self, sexp: &Sexp) -> Result<T::Var, ParseError> {
74        let name = match sexp {
75            Sexp::Atom(Atom::S(s)) => self.parser.var(s),
76            _ => Err(ParseError::err("Expected bind name to be a string")),
77        }?;
78        Ok(name)
79    }
80
81    pub fn parse_bind(&mut self, sexp: &Sexp) -> Result<Bind<T>, ParseError> {
82        match sexp {
83            Sexp::List(items) => {
84                match &items[0] {
85                    Sexp::List(name_and_sort) => {
86                        let name = self.parse_name(&name_and_sort[0])?;
87                        let sort = self.parse_sort(&name_and_sort[1])?;
88                        let pred = self.parse_pred_inner(&items[1])?;
89                        Ok(Bind { name, sort, pred })
90                    }
91                    _ => Err(ParseError::err("Expected list for name and sort in bind")),
92                }
93            }
94            _ => Err(ParseError::err("Expected list for bind")),
95        }
96    }
97
98    fn parse_pred_inner(&mut self, sexp: &Sexp) -> Result<Pred<T>, ParseError> {
99        match sexp {
100            Sexp::List(items) => {
101                match &items[0] {
102                    Sexp::Atom(Atom::S(s)) if s == "and" => {
103                        items[1..]
104                            .to_vec()
105                            .iter()
106                            .map(|item| self.parse_pred_inner(item))
107                            .try_collect()
108                            .map(Pred::And)
109                    }
110                    Sexp::Atom(Atom::S(s)) if s.starts_with("$") => self.parse_kvar(sexp),
111                    _ => self.parse_expr_possibly_nested(sexp).map(Pred::Expr),
112                }
113            }
114            _ => Err(ParseError::err("Expected list for pred")),
115        }
116    }
117
118    pub fn parse_kvar(&self, sexp: &Sexp) -> Result<Pred<T>, ParseError> {
119        match sexp {
120            Sexp::List(items) => {
121                if items.len() < 2 {
122                    Err(ParseError::err("Kvar application requires at least two elements"))
123                } else {
124                    let maybe_strs: Option<Vec<String>> = items
125                        .iter()
126                        .map(|s| {
127                            if let Sexp::Atom(Atom::S(sym)) = s { Some(sym.clone()) } else { None }
128                        })
129                        .collect();
130                    match maybe_strs {
131                        Some(strs) => {
132                            let kvar = self.parser.kvar(&strs[0])?;
133                            let mut args = vec![];
134                            for s in &strs[1..] {
135                                args.push(Expr::Var(self.parser.var(s)?));
136                            }
137                            Ok(Pred::KVar(kvar, args))
138                        }
139                        _ => Err(ParseError::err("Expected all list elements to be strings")),
140                    }
141                }
142            }
143            _ => Err(ParseError::err("Expected list for kvar")),
144        }
145    }
146
147    fn parse_expr_possibly_nested(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
148        through_nested_list(sexp, |s| self.parse_expr(s))
149    }
150
151    fn parse_is_ctor(&mut self, ctor_name: &str, arg: &Sexp) -> Result<Expr<T>, ParseError> {
152        let ctor = self.parser.var(ctor_name)?;
153        let arg = self.parse_expr(arg)?;
154        Ok(Expr::IsCtor(ctor, Box::new(arg)))
155    }
156
157    fn parse_if(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
158        match sexp {
159            Sexp::List(items) => {
160                let condition = self.parse_expr_possibly_nested(&items[1])?;
161                let pos_val = self.parse_expr_possibly_nested(&items[2])?;
162                let neg_val = self.parse_expr_possibly_nested(&items[3])?;
163                Ok(Expr::IfThenElse(Box::new([condition, pos_val, neg_val])))
164            }
165            _ => Err(ParseError::err("Expected list for if-else")),
166        }
167    }
168
169    pub fn parse_expr(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
170        match sexp {
171            Sexp::List(items) => {
172                if let Sexp::Atom(Atom::S(s)) = &items[0] {
173                    match s.as_str() {
174                        "cast" => self.parse_expr(&items[1]),
175                        "exists" => self.parse_exists(&items[1..]),
176                        "let" => self.parse_let(sexp),
177                        "not" => self.parse_not(sexp),
178                        "or" => self.parse_or(sexp),
179                        "and" => self.parse_and(sexp),
180                        "lit" => parse_bitvec(sexp),
181                        "if" => self.parse_if(sexp),
182                        "-" if items.len() == 2 => self.parse_neg(sexp),
183                        "+" | "-" | "*" | "/" | "mod" => self.parse_binary_op(sexp),
184                        "=" | "!=" | "<" | "<=" | ">" | ">=" => self.parse_atom(sexp),
185                        "<=>" => self.parse_iff(sexp),
186                        "=>" => self.parse_imp(sexp),
187                        "cast_as_int" => self.parse_expr(&items[1]), // some odd thing that fixpoint-hs seems to add for sets...
188                        _ if s.starts_with("is$") => self.parse_is_ctor(&s[3..], &items[1]),
189                        _ => self.parse_app(sexp),
190                    }
191                } else {
192                    self.parse_app(sexp)
193                }
194            }
195            Sexp::Atom(Atom::S(s)) => {
196                if let Some(thy_func) = parse_thy_func(s) {
197                    Ok(Expr::ThyFunc(thy_func))
198                } else if let Some(bv) = self.parse_bound_var(s) {
199                    Ok(bv)
200                } else {
201                    Ok(Expr::Var(self.parser.var(s)?))
202                }
203            }
204            Sexp::Atom(Atom::Q(s)) => Ok(Expr::Constant(Constant::String(self.parser.string(s)?))),
205            Sexp::Atom(Atom::B(b)) => Ok(Expr::Constant(Constant::Boolean(*b))),
206            Sexp::Atom(Atom::I(i)) => Ok(Expr::Constant(Constant::Numeral(*i))),
207            Sexp::Atom(Atom::F(_f)) => {
208                unimplemented!("Float parsing not supported in fixpoint (see Constant::Real)")
209            }
210        }
211    }
212
213    fn parse_neg(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
214        match sexp {
215            Sexp::List(items) => {
216                Ok(Expr::Neg(Box::new(self.parse_expr_possibly_nested(&items[1])?)))
217            }
218            _ => Err(ParseError::err("Expected list for neg")),
219        }
220    }
221
222    fn parse_not(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
223        match sexp {
224            Sexp::List(items) => {
225                Ok(Expr::Not(Box::new(self.parse_expr_possibly_nested(&items[1])?)))
226            }
227            _ => Err(ParseError::err("Expected list for \"not\"")),
228        }
229    }
230
231    fn parse_iff(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
232        match sexp {
233            Sexp::List(items) => {
234                match &items[0] {
235                    Sexp::Atom(Atom::S(s)) if s == "<=>" => {
236                        let exp1 = self.parse_expr_possibly_nested(&items[1])?;
237                        let exp2 = self.parse_expr_possibly_nested(&items[2])?;
238                        Ok(Expr::Iff(Box::new([exp1, exp2])))
239                    }
240                    _ => Err(ParseError::err("Expected iff to start with \"<=>\"")),
241                }
242            }
243            _ => Err(ParseError::err("Expected list for iff")),
244        }
245    }
246
247    fn parse_imp(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
248        match sexp {
249            Sexp::List(items) => {
250                match &items[0] {
251                    Sexp::Atom(Atom::S(s)) if s == "=>" => {
252                        let exp1 = self.parse_expr_possibly_nested(&items[1])?;
253                        let exp2 = self.parse_expr_possibly_nested(&items[2])?;
254                        Ok(Expr::Imp(Box::new([exp1, exp2])))
255                    }
256                    _ => Err(ParseError::err("Expected imp to start with \"=>\"")),
257                }
258            }
259            _ => Err(ParseError::err("Expected list for implication")),
260        }
261    }
262
263    fn parse_and(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
264        match sexp {
265            Sexp::List(items) => {
266                match &items[0] {
267                    Sexp::Atom(Atom::S(s)) if s == "and" => {
268                        items[1..]
269                            .to_vec()
270                            .iter()
271                            .map(|sexp| self.parse_expr_possibly_nested(sexp))
272                            .try_collect()
273                            .map(Expr::And)
274                    }
275                    _ => Err(ParseError::err("Expected \"and\" expression to start with \"and\"")),
276                }
277            }
278            _ => Err(ParseError::err("Expected list for \"and\"")),
279        }
280    }
281
282    fn parse_or(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
283        match sexp {
284            Sexp::List(items) => {
285                match &items[0] {
286                    Sexp::Atom(Atom::S(s)) if s == "or" => {
287                        items[1..]
288                            .to_vec()
289                            .iter()
290                            .map(|sexp| self.parse_expr_possibly_nested(sexp))
291                            .try_collect()
292                            .map(Expr::Or)
293                    }
294                    _ => Err(ParseError::err("Expected \"or\" expression to start with \"or\"")),
295                }
296            }
297            _ => Err(ParseError::err("Expected list for \"or\"")),
298        }
299    }
300
301    fn parse_atom(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
302        match sexp {
303            Sexp::List(items) => {
304                let exp1 = self.parse_expr_possibly_nested(&items[1])?;
305                let exp2 = self.parse_expr_possibly_nested(&items[2])?;
306                let exp_pair = Box::new([exp1, exp2]);
307                match &items[0] {
308                    Sexp::Atom(Atom::S(s)) if s == "=" => Ok(Expr::Atom(BinRel::Eq, exp_pair)),
309                    Sexp::Atom(Atom::S(s)) if s == "!=" => Ok(Expr::Atom(BinRel::Ne, exp_pair)),
310                    Sexp::Atom(Atom::S(s)) if s == "<=" => Ok(Expr::Atom(BinRel::Le, exp_pair)),
311                    Sexp::Atom(Atom::S(s)) if s == "<" => Ok(Expr::Atom(BinRel::Lt, exp_pair)),
312                    Sexp::Atom(Atom::S(s)) if s == ">=" => Ok(Expr::Atom(BinRel::Ge, exp_pair)),
313                    Sexp::Atom(Atom::S(s)) if s == ">" => Ok(Expr::Atom(BinRel::Gt, exp_pair)),
314                    _ => Err(ParseError::err("Unsupported atom")),
315                }
316            }
317            _ => Err(ParseError::err("Expected list for atom")),
318        }
319    }
320
321    fn parse_app(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
322        match sexp {
323            Sexp::List(items) => {
324                let Sexp::List(inner) = &items[0] else {
325                    Err(ParseError::err("Expected list for inner func"))?
326                };
327                match &inner[1] {
328                    Sexp::Atom(Atom::S(s)) if s == "apply" => {
329                        let func_sort = self.parse_sort(&inner[2])?;
330                        let func = self.parse_expr_possibly_nested(&items[1])?;
331                        Ok(Expr::App(Box::new(func), None, vec![], Some(func_sort)))
332                    }
333                    _ => {
334                        let args: Vec<Expr<T>> = items[1..]
335                            .to_vec()
336                            .iter()
337                            .map(|sexp| self.parse_expr_possibly_nested(sexp))
338                            .try_collect()?;
339                        Ok(Expr::App(
340                            Box::new(self.parse_expr_possibly_nested(&items[0])?),
341                            None,
342                            args,
343                            None,
344                        ))
345                    }
346                }
347            }
348            _ => Err(ParseError::err("Expected list for app")),
349        }
350    }
351
352    fn parse_binary_op(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
353        match sexp {
354            Sexp::List(items) => {
355                let exp1 = self.parse_expr_possibly_nested(&items[1])?;
356                let exp2 = self.parse_expr_possibly_nested(&items[2])?;
357                let exp_pair = Box::new([exp1, exp2]);
358                match &items[0] {
359                    Sexp::Atom(Atom::S(s)) if s == "+" => Ok(Expr::BinaryOp(BinOp::Add, exp_pair)),
360                    Sexp::Atom(Atom::S(s)) if s == "-" => Ok(Expr::BinaryOp(BinOp::Sub, exp_pair)),
361                    Sexp::Atom(Atom::S(s)) if s == "*" => Ok(Expr::BinaryOp(BinOp::Mul, exp_pair)),
362                    Sexp::Atom(Atom::S(s)) if s == "/" => Ok(Expr::BinaryOp(BinOp::Div, exp_pair)),
363                    Sexp::Atom(Atom::S(s)) if s == "mod" => {
364                        Ok(Expr::BinaryOp(BinOp::Mod, exp_pair))
365                    }
366                    _ => Err(ParseError::err("Unsupported atom")),
367                }
368            }
369            _ => Err(ParseError::err("Expected list for binary operation")),
370        }
371    }
372
373    fn parse_exists(&mut self, items: &[Sexp]) -> Result<Expr<T>, ParseError> {
374        let [Sexp::List(var_sorts), body] = items else {
375            return Err(ParseError::err("Expected list for vars and sorts in exists"));
376        };
377        let mut names = Vec::new();
378        let mut sorts = Vec::new();
379        for var_sort in var_sorts {
380            if let Sexp::List(items) = var_sort
381                && let [var, sort] = &items[..]
382            {
383                let Sexp::Atom(Atom::S(name)) = var else {
384                    return Err(ParseError::err("Expected variable name to be string {var:?}"));
385                };
386                names.push(name.clone());
387                sorts.push(self.parse_sort(sort)?);
388            } else {
389                return Err(ParseError::err(format!(
390                    "Expected list for var and sort in exists {var_sort:?}"
391                )));
392            }
393        }
394        self.push_scope(&names);
395        let body = self.parse_expr_possibly_nested(body)?;
396        let mut scope = self.pop_scope().unwrap();
397        let bound = names
398            .iter()
399            .zip(sorts)
400            .map(|(name, sort)| (scope.swap_remove(name).unwrap(), sort))
401            .collect();
402        Ok(Expr::Quantifier(Quantifier::Exists, bound, Box::new(body)))
403    }
404
405    fn parse_let(&mut self, sexp: &Sexp) -> Result<Expr<T>, ParseError> {
406        match sexp {
407            Sexp::List(items) => {
408                through_nested_list(&items[1], |bottom| {
409                    match bottom {
410                        Sexp::List(var_and_binding) => {
411                            match &var_and_binding[0] {
412                                Sexp::Atom(Atom::S(s)) => {
413                                    let binding =
414                                        self.parse_expr_possibly_nested(&var_and_binding[1])?;
415                                    let body = self.parse_expr_possibly_nested(&items[2])?;
416                                    let var = self.parser.var(s)?;
417                                    Ok(Expr::Let(var, Box::new([binding, body])))
418                                }
419                                _ => Err(ParseError::err("Expected variable name to be string")),
420                            }
421                        }
422                        _ => Err(ParseError::err("Expected list for var and binding")),
423                    }
424                })
425            }
426            _ => Err(ParseError::err("Expected list for let")),
427        }
428    }
429
430    fn parse_list_sort(&self, sexp: &Sexp) -> Result<Sort<T>, ParseError> {
431        let Sexp::List(items) = sexp else {
432            return Err(ParseError::err("Expected list for func or app sort"));
433        };
434        if items.is_empty() {
435            return Err(ParseError::err("Empty list encountered when parsing sort"));
436        }
437        let Sexp::Atom(Atom::S(ctor)) = &items[0] else {
438            return Err(ParseError::err("Unexpected sort constructor encountered"));
439        };
440        if ctor == "func" && items.len() == 4 {
441            return self.parse_func_sort(&items[1..]);
442        }
443        if ctor == "function" && items.len() == 3 {
444            let input = self.parse_sort(&items[1])?;
445            let output = self.parse_sort(&items[2])?;
446            return Ok(Sort::mk_func(0, vec![input], output));
447        }
448        let args: Vec<_> = items[1..]
449            .to_vec()
450            .iter()
451            .map(|sexp| self.parse_sort(sexp))
452            .try_collect()?;
453        if ctor == "Set_Set" && args.len() == 1 {
454            return Ok(Sort::App(SortCtor::Set, args));
455        }
456        if (ctor == "Map_t" || ctor == "Array_t") && args.len() == 2 {
457            return Ok(Sort::App(SortCtor::Map, args));
458        }
459        if ctor == "BitVec" && args.len() == 1 {
460            return parse_bitvec_sort(sexp);
461        }
462        let ctor = SortCtor::Data(self.parser.sort(ctor)?);
463        Ok(Sort::App(ctor, args))
464    }
465
466    pub fn parse_sort(&self, sexp: &Sexp) -> Result<Sort<T>, ParseError> {
467        match sexp {
468            Sexp::List(_items) => self.parse_list_sort(sexp),
469            Sexp::Atom(Atom::S(s)) => {
470                if s == "Int" || s == "int" {
471                    Ok(Sort::Int)
472                } else if s == "Bool" || s == "bool" {
473                    Ok(Sort::Bool)
474                } else if s == "Real" || s == "real" {
475                    Ok(Sort::Real)
476                } else if s == "Str" || s == "str" {
477                    Ok(Sort::Str)
478                } else if s.starts_with("Size") {
479                    self.parse_bv_size(sexp)
480                } else if let Some(idx_rparen) = s.strip_prefix("@(")
481                    && let Some(s_idx) = idx_rparen.strip_suffix(")")
482                    && let Ok(idx) = s_idx.parse::<usize>()
483                {
484                    Ok(Sort::Var(idx))
485                } else {
486                    let ctor = SortCtor::Data(self.parser.sort(s)?);
487                    Ok(Sort::App(ctor, vec![]))
488                }
489            }
490            // Sexp::Atom(Atom::S(ref s)) => Ok(Sort::Var(s.clone())),
491            _ => panic!("Unknown sort encountered {sexp:?}"), // Err(ParseError::err(format!("Unknown sort encountered {sexp:?}"))),
492        }
493    }
494
495    fn parse_func_sort(&self, items: &[Sexp]) -> Result<Sort<T>, ParseError> {
496        if let Sexp::Atom(Atom::I(params)) = &items[0]
497            && let Sexp::List(inputs) = &items[1]
498        {
499            let params = *params as usize;
500            let inputs: Vec<_> = inputs
501                .iter()
502                .map(|sexp| self.parse_sort(sexp))
503                .try_collect()?;
504            let output = self.parse_sort(&items[2])?;
505            Ok(Sort::mk_func(params, inputs, output))
506        } else {
507            Err(ParseError::err("Expected arity to be an integer"))
508        }
509    }
510
511    pub fn parse_solution(&mut self, sexp: &Sexp) -> Result<KvarSolution<T>, ParseError> {
512        if let Sexp::List(items) = sexp
513            && let [_lambda, params, body] = &items[..]
514            && let Sexp::List(sexp_params) = params
515        {
516            let mut kvar_args = vec![];
517            let mut sorts = vec![];
518
519            for param in sexp_params {
520                if let Sexp::List(bind) = param
521                    && let [_name, sort] = &bind[..]
522                    && let Sexp::Atom(Atom::S(s)) = _name
523                {
524                    kvar_args.push(s.clone());
525                    sorts.push(sort);
526                } else {
527                    return Err(ParseError::err("expected parameter names to be symbols"));
528                }
529            }
530            let sorts: Vec<_> = sorts
531                .into_iter()
532                .map(|sexp| self.parse_sort(sexp))
533                .try_collect()?;
534            self.push_scope(&kvar_args);
535
536            let expr = self.parse_expr(body)?;
537
538            let mut scope = self.pop_scope().unwrap();
539            let bound = kvar_args
540                .iter()
541                .zip(sorts)
542                .map(|(name, sort)| (scope.swap_remove(name).unwrap(), sort))
543                .collect();
544            Ok((bound, expr))
545        } else {
546            Err(ParseError::err("expected (lambda (params) body)"))
547        }
548    }
549
550    fn push_scope(&mut self, names: &[String]) {
551        self.scopes.push(
552            names
553                .iter()
554                .cloned()
555                .map(|name| (name, self.parser.fresh_var()))
556                .collect(),
557        );
558    }
559
560    fn pop_scope(&mut self) -> Option<IndexMap<String, T::Var>> {
561        self.scopes.pop()
562    }
563
564    fn parse_bound_var(&self, name: &str) -> Option<Expr<T>> {
565        for scope in self.scopes.iter().rev() {
566            if let Some(var) = scope.get(name) {
567                return Some(Expr::Var(var.clone()));
568            }
569        }
570        None
571    }
572}
573
574fn parse_bv_size<T: Types>(sexp: &Sexp) -> Result<Sort<T>, ParseError> {
575    match sexp {
576        Sexp::Atom(Atom::S(s)) if s.starts_with("Size") => {
577            let maybe_size = s
578                .strip_prefix("Size")
579                .and_then(|sz_str| sz_str.parse::<u32>().ok());
580            if let Some(size) = maybe_size {
581                Ok(Sort::BvSize(size))
582            } else {
583                Err(ParseError::err("Could not parse number for bvsize"))
584            }
585        }
586        _ => Err(ParseError::err("Expected bitvec size to be in the form Size{\\d+}")),
587    }
588}
589
590fn parse_bitvec_sort<T: Types>(sexp: &Sexp) -> Result<Sort<T>, ParseError> {
591    match sexp {
592        Sexp::List(items) if items.len() == 2 => {
593            let bitvec_size = parse_bv_size(&items[1])?;
594            Ok(Sort::BitVec(Box::new(bitvec_size)))
595        }
596        _ => Err(ParseError::err("Expected list of length 2 for bitvec sort")),
597    }
598}
599
600fn size_form_bv_sort(sort: Sort<StringTypes>) -> Result<u32, ParseError> {
601    match sort {
602        Sort::BitVec(ref bv_size_box) => {
603            match **bv_size_box {
604                Sort::BvSize(size) => Ok(size),
605                _ => Err(ParseError::err("BitVec sort should contain BvSize sort")),
606            }
607        }
608        _ => Err(ParseError::err("Expected BitVec variant to be provided")),
609    }
610}
611
612fn parse_bitvec<PT: Types>(sexp: &Sexp) -> Result<Expr<PT>, ParseError> {
613    match sexp {
614        Sexp::List(items) => {
615            match &items[1] {
616                Sexp::Atom(Atom::Q(lit)) if lit.starts_with("#b") => {
617                    let bitvec = u128::from_str_radix(&lit[3..], 2).expect("Invalid binary string");
618                    let bvsize = size_form_bv_sort(parse_bitvec_sort(&items[2])?)?;
619                    Ok(Expr::Constant(Constant::BitVec(bitvec, bvsize)))
620                }
621                _ => Err(ParseError::err("Expected binary literal for bitvec")),
622            }
623        }
624        _ => Err(ParseError::err("Expected list for bitvector literal")),
625    }
626}
627
628fn parse_thy_func(name: &str) -> Option<ThyFunc> {
629    match name {
630        // STRINGS
631        "strLen" => Some(ThyFunc::StrLen),
632
633        // BIT VECTORS - conversions
634        "int_to_bv8" => Some(ThyFunc::IntToBv8),
635        "bv8_to_int" => Some(ThyFunc::Bv8ToInt),
636        "int_to_bv32" => Some(ThyFunc::IntToBv32),
637        "bv32_to_int" => Some(ThyFunc::Bv32ToInt),
638        "int_to_bv64" => Some(ThyFunc::IntToBv64),
639        "bv64_to_int" => Some(ThyFunc::Bv64ToInt),
640
641        // BIT VECTORS - comparisons
642        "bvule" => Some(ThyFunc::BvUle),
643        "bvsle" => Some(ThyFunc::BvSle),
644        "bvuge" => Some(ThyFunc::BvUge),
645        "bvsge" => Some(ThyFunc::BvSge),
646        "bvugt" => Some(ThyFunc::BvUgt),
647        "bvsgt" => Some(ThyFunc::BvSgt),
648        "bvult" => Some(ThyFunc::BvUlt),
649        "bvslt" => Some(ThyFunc::BvSlt),
650
651        // BIT VECTORS - arithmetic/logical operations
652        "bvudiv" => Some(ThyFunc::BvUdiv),
653        "bvsdiv" => Some(ThyFunc::BvSdiv),
654        "bvurem" => Some(ThyFunc::BvUrem),
655        "bvsrem" => Some(ThyFunc::BvSrem),
656        "bvlshr" => Some(ThyFunc::BvLshr),
657        "bvashr" => Some(ThyFunc::BvAshr),
658        "bvand" => Some(ThyFunc::BvAnd),
659        "bvor" => Some(ThyFunc::BvOr),
660        "bvxor" => Some(ThyFunc::BvXor),
661        "bvnot" => Some(ThyFunc::BvNot),
662        "bvadd" => Some(ThyFunc::BvAdd),
663        "bvneg" => Some(ThyFunc::BvNeg),
664        "bvsub" => Some(ThyFunc::BvSub),
665        "bvmul" => Some(ThyFunc::BvMul),
666        "bvshl" => Some(ThyFunc::BvShl),
667
668        // SETS
669        "Set_empty" => Some(ThyFunc::SetEmpty),
670        "Set_sng" => Some(ThyFunc::SetSng),
671        "Set_cup" => Some(ThyFunc::SetCup),
672        "Set_cap" => Some(ThyFunc::SetCap),
673        "Set_dif" => Some(ThyFunc::SetDif),
674        "Set_mem" => Some(ThyFunc::SetMem),
675        "Set_sub" => Some(ThyFunc::SetSub),
676
677        // MAPS
678        "Map_default" => Some(ThyFunc::MapDefault),
679        "Map_select" | "arr_select_m" => Some(ThyFunc::MapSelect),
680        "Map_store" | "arr_store_m" => Some(ThyFunc::MapStore),
681
682        // Note: BvZeroExtend and BvSignExtend have parametric forms like "app (_ zero_extend N)"
683        // These would need special parsing in the caller
684        _ => None,
685    }
686}
687
688fn through_nested_list<T, F>(sexp: &Sexp, mut at_bottom: F) -> T
689where
690    F: FnMut(&Sexp) -> T,
691{
692    let mut current = sexp;
693    while let Sexp::List(items) = current {
694        if items.len() == 1 {
695            current = &items[0];
696        } else {
697            break;
698        }
699    }
700    at_bottom(current)
701}
702
703/// Trivial implementation of Types using `String` for all associated types -----------------------------------
704pub struct StringTypes;
705impl Types for StringTypes {
706    type Sort = String;
707    type KVar = String;
708    type Var = String;
709    type Tag = String;
710    type String = String;
711    type Real = String;
712}
713
714impl FromSexp<StringTypes> for StringTypes {
715    fn fresh_var(&mut self) -> <StringTypes as Types>::Var {
716        todo!()
717    }
718    fn var(&self, name: &str) -> Result<String, ParseError> {
719        Ok(name.to_string())
720    }
721
722    fn kvar(&self, name: &str) -> Result<String, ParseError> {
723        Ok(name.to_string())
724    }
725
726    fn string(&self, s: &str) -> Result<String, ParseError> {
727        Ok(s.to_string())
728    }
729
730    fn sort(&self, name: &str) -> Result<String, ParseError> {
731        Ok(name.to_string())
732    }
733}
liquid_fixpoint/parser.rs

liquid_fixpoint/
parser.rs
