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

liquid_fixpoint/
parser.rs
