liquid_fixpoint/
parser.rs

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

liquid_fixpoint/
parser.rs
