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

liquid_fixpoint/
parser.rs
