liquid_fixpoint/
parser.rs

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

liquid_fixpoint/
parser.rs
