liquid_fixpoint/
parser.rs

1use std::fmt;
2
3use crate::{
4    BinOp, BinRel, Bind, Constant, Constraint, Expr, Identifier, KVarDecl, Pred, Qualifier, Sort,
5    SortCtor, Types,
6    constraint_with_env::ConstraintWithEnv,
7    sexp::{Atom, ParseError as SexpParseError, Parser as SexpParser, Sexp},
8};
9
10#[derive(Debug)]
11pub enum ParseError {
12    SexpParseError(SexpParseError),
13    MalformedSexpError(&'static str),
14}
15
16pub struct ParsingTypes;
17impl Types for ParsingTypes {
18    type Sort = String;
19    type KVar = String;
20    type Var = String;
21    type Tag = String;
22    type String = String;
23}
24
25impl Identifier for String {
26    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
27        write!(f, "{self}")
28    }
29}
30
31fn parse_bv_size(sexp: &Sexp) -> Result<Sort<ParsingTypes>, ParseError> {
32    match sexp {
33        Sexp::Atom(Atom::S(s)) if s.starts_with("Size") => {
34            let maybe_size = s
35                .strip_prefix("Size")
36                .and_then(|sz_str| sz_str.parse::<u32>().ok());
37            if let Some(size) = maybe_size {
38                Ok(Sort::BvSize(size))
39            } else {
40                Err(ParseError::MalformedSexpError("Could not parse number for bvsize"))
41            }
42        }
43        _ => {
44            Err(ParseError::MalformedSexpError("Expected bitvec size to be in the form Size{\\d+}"))
45        }
46    }
47}
48
49fn parse_func_sort(_sexp: &Sexp) -> Result<Sort<ParsingTypes>, ParseError> {
50    Err(ParseError::MalformedSexpError("Func sort hole"))
51}
52
53fn parse_bitvec_sort(sexp: &Sexp) -> Result<Sort<ParsingTypes>, ParseError> {
54    match sexp {
55        Sexp::List(items) if items.len() == 2 => {
56            let bitvec_size = parse_bv_size(&items[1])?;
57            Ok(Sort::BitVec(Box::new(bitvec_size)))
58        }
59        _ => Err(ParseError::MalformedSexpError("Expected list of length 2 for bitvec sort")),
60    }
61}
62
63fn parse_list_sort(sexp: &Sexp) -> Result<Sort<ParsingTypes>, ParseError> {
64    match sexp {
65        Sexp::List(items) => {
66            let args = items[1..]
67                .to_vec()
68                .iter()
69                .map(parse_sort)
70                .collect::<Result<Vec<Sort<ParsingTypes>>, ParseError>>()?;
71            match &items[0] {
72                Sexp::Atom(Atom::S(s)) if s == "func" => parse_func_sort(sexp),
73                Sexp::Atom(Atom::S(s)) if s == "Set_Set" && args.len() == 1 => {
74                    Ok(Sort::App(SortCtor::Set, args))
75                }
76                Sexp::Atom(Atom::S(s)) if s == "Map_t" && args.len() == 2 => {
77                    Ok(Sort::App(SortCtor::Map, args))
78                }
79                Sexp::Atom(Atom::S(s)) if s == "BitVec" && args.len() == 1 => {
80                    parse_bitvec_sort(sexp)
81                }
82                _ => Err(ParseError::MalformedSexpError("Unexpected sort constructor encountered")),
83            }
84        }
85        _ => Err(ParseError::MalformedSexpError("Expected list for func or app sort")),
86    }
87}
88
89fn parse_sort(sexp: &Sexp) -> Result<Sort<ParsingTypes>, ParseError> {
90    match sexp {
91        Sexp::List(_items) => parse_list_sort(sexp),
92        Sexp::Atom(Atom::S(s)) if s == "Int" || s == "int" => Ok(Sort::Int),
93        Sexp::Atom(Atom::S(s)) if s == "Bool" || s == "bool" => Ok(Sort::Bool),
94        Sexp::Atom(Atom::S(s)) if s == "Real" || s == "real" => Ok(Sort::Real),
95        Sexp::Atom(Atom::S(s)) if s == "Str" || s == "str" => Ok(Sort::Str),
96        Sexp::Atom(Atom::S(s)) if s.starts_with("Size") => parse_bv_size(sexp),
97        // Sexp::Atom(Atom::S(ref s)) => Ok(Sort::Var(s.clone())),
98        _ => Err(ParseError::MalformedSexpError("Unknown sort encountered")),
99    }
100}
101
102fn parse_bind(sexp: &Sexp) -> Result<Bind<ParsingTypes>, ParseError> {
103    match sexp {
104        Sexp::List(items) => {
105            match &items[0] {
106                Sexp::List(name_and_sort) => {
107                    let name = match &name_and_sort[0] {
108                        Sexp::Atom(Atom::S(s)) => Ok(s.clone()),
109                        _ => {
110                            Err(ParseError::MalformedSexpError("Expected bind name to be a string"))
111                        }
112                    }?;
113                    let sort = parse_sort(&name_and_sort[1])?;
114                    let pred = parse_pred_inner(&items[1])?;
115                    Ok(Bind { name, sort, pred })
116                }
117                _ => Err(ParseError::MalformedSexpError("Expected list for name and sort in bind")),
118            }
119        }
120        _ => Err(ParseError::MalformedSexpError("Expected list for bind")),
121    }
122}
123
124fn parse_forall(sexp: &Sexp) -> Result<Constraint<ParsingTypes>, ParseError> {
125    match sexp {
126        Sexp::List(items) => {
127            match &items[0] {
128                Sexp::Atom(Atom::S(s)) if s == "forall" => {
129                    let bind = parse_bind(&items[1])?;
130                    let c = sexp_to_constraint_inner(&items[2])?;
131                    Ok(Constraint::ForAll(bind, Box::new(c)))
132                }
133                _ => {
134                    Err(ParseError::MalformedSexpError("Expected forall to start with \"forall\""))
135                }
136            }
137        }
138        _ => Err(ParseError::MalformedSexpError("Expected list for forall expression")),
139    }
140}
141
142fn parse_conj(sexp: &Sexp) -> Result<Constraint<ParsingTypes>, ParseError> {
143    match sexp {
144        Sexp::List(items) => {
145            match &items[0] {
146                Sexp::Atom(Atom::S(s)) if s == "and" => {
147                    items[1..]
148                        .to_vec()
149                        .iter()
150                        .map(sexp_to_constraint_inner)
151                        .collect::<Result<_, _>>()
152                        .map(Constraint::Conj)
153                }
154                _ => {
155                    Err(ParseError::MalformedSexpError("Expected conjuction to start with \"and\""))
156                }
157            }
158        }
159        _ => Err(ParseError::MalformedSexpError("Expected list for constraint conjunction")),
160    }
161}
162
163fn parse_let(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
164    match sexp {
165        Sexp::List(items) => {
166            through_nested_list(&items[1], |bottom| {
167                match bottom {
168                    Sexp::List(var_and_binding) => {
169                        match &var_and_binding[0] {
170                            Sexp::Atom(Atom::S(s)) => {
171                                let binding = parse_expr_possibly_nested(&var_and_binding[1])?;
172                                let body = parse_expr_possibly_nested(&items[2])?;
173                                Ok(Expr::Let(s.clone(), Box::new([binding, body])))
174                            }
175                            _ => {
176                                Err(ParseError::MalformedSexpError(
177                                    "Expected variable name to be string",
178                                ))
179                            }
180                        }
181                    }
182                    _ => Err(ParseError::MalformedSexpError("Expected list for var and binding")),
183                }
184            })
185        }
186        _ => Err(ParseError::MalformedSexpError("Expected list for let")),
187    }
188}
189
190fn parse_binary_op(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
191    match sexp {
192        Sexp::List(items) => {
193            let exp1 = parse_expr_possibly_nested(&items[1])?;
194            let exp2 = parse_expr_possibly_nested(&items[2])?;
195            let exp_pair = Box::new([exp1, exp2]);
196            match &items[0] {
197                Sexp::Atom(Atom::S(s)) if s == "+" => Ok(Expr::BinaryOp(BinOp::Add, exp_pair)),
198                Sexp::Atom(Atom::S(s)) if s == "-" => Ok(Expr::BinaryOp(BinOp::Sub, exp_pair)),
199                Sexp::Atom(Atom::S(s)) if s == "*" => Ok(Expr::BinaryOp(BinOp::Mul, exp_pair)),
200                Sexp::Atom(Atom::S(s)) if s == "/" => Ok(Expr::BinaryOp(BinOp::Div, exp_pair)),
201                Sexp::Atom(Atom::S(s)) if s == "mod" => Ok(Expr::BinaryOp(BinOp::Mod, exp_pair)),
202                _ => Err(ParseError::MalformedSexpError("Unsupported atom")),
203            }
204        }
205        _ => Err(ParseError::MalformedSexpError("Expected list for binary operation")),
206    }
207}
208
209fn parse_atom(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
210    match sexp {
211        Sexp::List(items) => {
212            let exp1 = parse_expr_possibly_nested(&items[1])?;
213            let exp2 = parse_expr_possibly_nested(&items[2])?;
214            let exp_pair = Box::new([exp1, exp2]);
215            match &items[0] {
216                Sexp::Atom(Atom::S(s)) if s == "=" => Ok(Expr::Atom(BinRel::Eq, exp_pair)),
217                Sexp::Atom(Atom::S(s)) if s == "!=" => Ok(Expr::Atom(BinRel::Ne, exp_pair)),
218                Sexp::Atom(Atom::S(s)) if s == "<=" => Ok(Expr::Atom(BinRel::Le, exp_pair)),
219                Sexp::Atom(Atom::S(s)) if s == "<" => Ok(Expr::Atom(BinRel::Lt, exp_pair)),
220                Sexp::Atom(Atom::S(s)) if s == ">=" => Ok(Expr::Atom(BinRel::Ge, exp_pair)),
221                Sexp::Atom(Atom::S(s)) if s == ">" => Ok(Expr::Atom(BinRel::Gt, exp_pair)),
222                _ => Err(ParseError::MalformedSexpError("Unsupported atom")),
223            }
224        }
225        _ => Err(ParseError::MalformedSexpError("Expected list for atom")),
226    }
227}
228
229fn parse_iff(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
230    match sexp {
231        Sexp::List(items) => {
232            match &items[0] {
233                Sexp::Atom(Atom::S(s)) if s == "<=>" => {
234                    let exp1 = parse_expr_possibly_nested(&items[1])?;
235                    let exp2 = parse_expr_possibly_nested(&items[2])?;
236                    Ok(Expr::Iff(Box::new([exp1, exp2])))
237                }
238                _ => Err(ParseError::MalformedSexpError("Expected iff to start with \"<=>\"")),
239            }
240        }
241        _ => Err(ParseError::MalformedSexpError("Expected list for iff")),
242    }
243}
244
245fn parse_imp(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
246    match sexp {
247        Sexp::List(items) => {
248            match &items[0] {
249                Sexp::Atom(Atom::S(s)) if s == "=>" => {
250                    let exp1 = parse_expr_possibly_nested(&items[1])?;
251                    let exp2 = parse_expr_possibly_nested(&items[2])?;
252                    Ok(Expr::Imp(Box::new([exp1, exp2])))
253                }
254                _ => Err(ParseError::MalformedSexpError("Expected imp to start with \"=>\"")),
255            }
256        }
257        _ => Err(ParseError::MalformedSexpError("Expected list for implication")),
258    }
259}
260
261fn parse_not(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
262    match sexp {
263        Sexp::List(items) => Ok(Expr::Not(Box::new(parse_expr_possibly_nested(&items[1])?))),
264        _ => Err(ParseError::MalformedSexpError("Expected list for \"not\"")),
265    }
266}
267
268fn parse_or(sexp: &Sexp) -> Result<Expr<ParsingTypes>, 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(parse_expr_possibly_nested)
277                        .collect::<Result<_, _>>()
278                        .map(Expr::Or)
279                }
280                _ => {
281                    Err(ParseError::MalformedSexpError(
282                        "Expected \"or\" expression to start with \"or\"",
283                    ))
284                }
285            }
286        }
287        _ => Err(ParseError::MalformedSexpError("Expected list for \"or\"")),
288    }
289}
290
291fn parse_and(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
292    match sexp {
293        Sexp::List(items) => {
294            match &items[0] {
295                Sexp::Atom(Atom::S(s)) if s == "and" => {
296                    items[1..]
297                        .to_vec()
298                        .iter()
299                        .map(parse_expr_possibly_nested)
300                        .collect::<Result<_, _>>()
301                        .map(Expr::And)
302                }
303                _ => {
304                    Err(ParseError::MalformedSexpError(
305                        "Expected \"and\" expression to start with \"and\"",
306                    ))
307                }
308            }
309        }
310        _ => Err(ParseError::MalformedSexpError("Expected list for \"and\"")),
311    }
312}
313
314fn parse_neg(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
315    match sexp {
316        Sexp::List(items) => Ok(Expr::Neg(Box::new(parse_expr_possibly_nested(&items[1])?))),
317        _ => Err(ParseError::MalformedSexpError("Expected list for neg")),
318    }
319}
320
321fn parse_app(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
322    match sexp {
323        Sexp::List(items) => {
324            let exp1 = parse_expr_possibly_nested(&items[0])?;
325            let args: Vec<Expr<ParsingTypes>> = items[1..]
326                .to_vec()
327                .iter()
328                .map(parse_expr_possibly_nested)
329                .collect::<Result<_, _>>()?;
330            Ok(Expr::App(Box::new(exp1), args))
331        }
332        _ => Err(ParseError::MalformedSexpError("Expected list for app")),
333    }
334}
335
336fn size_form_bv_sort(sort: Sort<ParsingTypes>) -> Result<u32, ParseError> {
337    match sort {
338        Sort::BitVec(ref bv_size_box) => {
339            match **bv_size_box {
340                Sort::BvSize(size) => Ok(size),
341                _ => Err(ParseError::MalformedSexpError("BitVec sort should contain BvSize sort")),
342            }
343        }
344        _ => Err(ParseError::MalformedSexpError("Expected BitVec variant to be provided")),
345    }
346}
347
348fn parse_bitvec(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
349    match sexp {
350        Sexp::List(items) => {
351            match &items[1] {
352                Sexp::Atom(Atom::Q(lit)) if lit.starts_with("#b") => {
353                    let bitvec = u128::from_str_radix(&lit[3..], 2).expect("Invalid binary string");
354                    let bvsize = size_form_bv_sort(parse_bitvec_sort(&items[2])?)?;
355                    Ok(Expr::Constant(Constant::BitVec(bitvec, bvsize)))
356                }
357                _ => Err(ParseError::MalformedSexpError("Expected binary literal for bitvec")),
358            }
359        }
360        _ => Err(ParseError::MalformedSexpError("Expected list for bitvector literal")),
361    }
362}
363
364fn through_nested_list<T, F>(sexp: &Sexp, at_bottom: F) -> T
365where
366    F: Fn(&Sexp) -> T,
367{
368    let mut current = sexp;
369    while let Sexp::List(items) = current {
370        if items.len() == 1 {
371            current = &items[0];
372        } else {
373            break;
374        }
375    }
376    at_bottom(current)
377}
378
379fn parse_expr_possibly_nested(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
380    through_nested_list(sexp, parse_expr)
381}
382
383fn parse_expr(sexp: &Sexp) -> Result<Expr<ParsingTypes>, ParseError> {
384    match sexp {
385        Sexp::List(items) => {
386            match &items[0] {
387                Sexp::Atom(Atom::S(s)) if s == "let" => parse_let(sexp),
388                Sexp::Atom(Atom::S(s)) if s == "not" => parse_not(sexp),
389                Sexp::Atom(Atom::S(s)) if s == "or" => parse_or(sexp),
390                Sexp::Atom(Atom::S(s)) if s == "and" => parse_and(sexp),
391                Sexp::Atom(Atom::S(s)) if s == "lit" => parse_bitvec(sexp),
392                Sexp::Atom(Atom::S(s)) if s == "-" && items.len() == 2 => parse_neg(sexp),
393                Sexp::Atom(Atom::S(s)) if matches!(s.as_str(), "+" | "-" | "*" | "/" | "mod") => {
394                    parse_binary_op(sexp)
395                }
396                Sexp::Atom(Atom::S(s))
397                    if matches!(s.as_str(), "=" | "!=" | "<" | "<=" | ">" | ">=") =>
398                {
399                    parse_atom(sexp)
400                }
401                Sexp::Atom(Atom::S(s)) if s == "<=>" => parse_iff(sexp),
402                Sexp::Atom(Atom::S(s)) if s == "=>" => parse_imp(sexp),
403                _ => parse_app(sexp),
404            }
405        }
406        Sexp::Atom(Atom::S(s)) => Ok(Expr::Var(s.clone())),
407        Sexp::Atom(Atom::Q(s)) => Ok(Expr::Constant(Constant::String(s.clone()))),
408        Sexp::Atom(Atom::B(b)) => Ok(Expr::Constant(Constant::Boolean(*b))),
409        Sexp::Atom(Atom::I(i)) => Ok(Expr::Constant(Constant::Numeral(*i as u128))),
410        Sexp::Atom(Atom::F(f)) => Ok(Expr::Constant(Constant::Real(*f as u128))),
411    }
412}
413
414fn parse_kvar(sexp: &Sexp) -> Result<Pred<ParsingTypes>, ParseError> {
415    match sexp {
416        Sexp::List(items) => {
417            if items.len() < 2 {
418                Err(ParseError::MalformedSexpError(
419                    "Kvar application requires at least two elements",
420                ))
421            } else {
422                let maybe_strs: Option<Vec<String>> =
423                    items
424                        .iter()
425                        .map(|s| {
426                            if let Sexp::Atom(Atom::S(sym)) = s { Some(sym.clone()) } else { None }
427                        })
428                        .collect();
429                match maybe_strs {
430                    Some(strs) => Ok(Pred::KVar(strs[0].clone(), strs[1..].to_vec())),
431                    _ => {
432                        Err(ParseError::MalformedSexpError(
433                            "Expected all list elements to be strings",
434                        ))
435                    }
436                }
437            }
438        }
439        _ => Err(ParseError::MalformedSexpError("Expected list for kvar")),
440    }
441}
442
443fn parse_pred_inner(sexp: &Sexp) -> Result<Pred<ParsingTypes>, ParseError> {
444    match sexp {
445        Sexp::List(items) => {
446            match &items[0] {
447                Sexp::Atom(Atom::S(s)) if s == "and" => {
448                    items[1..]
449                        .to_vec()
450                        .iter()
451                        .map(parse_pred_inner)
452                        .collect::<Result<_, _>>()
453                        .map(Pred::And)
454                }
455                Sexp::Atom(Atom::S(s)) if s.starts_with("$") => parse_kvar(sexp),
456                _ => parse_expr_possibly_nested(sexp).map(Pred::Expr),
457            }
458        }
459        _ => Err(ParseError::MalformedSexpError("Expected list for pred")),
460    }
461}
462
463fn parse_tagged_pred(sexp: &Sexp) -> Result<Constraint<ParsingTypes>, ParseError> {
464    match sexp {
465        Sexp::List(items) => {
466            match &items[2] {
467                Sexp::Atom(Atom::Q(s)) => {
468                    let pred = parse_pred_inner(&items[1])?;
469                    Ok(Constraint::Pred(pred, Some(s.clone())))
470                }
471                _ => Err(ParseError::MalformedSexpError("Expected quoted string for tag")),
472            }
473        }
474        _ => Err(ParseError::MalformedSexpError("Expected list for tagged predicate")),
475    }
476}
477
478fn parse_pred(sexp: &Sexp) -> Result<Constraint<ParsingTypes>, ParseError> {
479    if let Sexp::List(items) = sexp
480        && let Sexp::Atom(Atom::S(s)) = &items[0]
481        && s == "tag"
482    {
483        return parse_tagged_pred(sexp);
484    }
485    let pred = parse_pred_inner(sexp)?;
486    Ok(Constraint::Pred(pred, None))
487}
488
489fn sexp_to_constraint_inner(sexp: &Sexp) -> Result<Constraint<ParsingTypes>, ParseError> {
490    match sexp {
491        Sexp::List(items) => {
492            match &items[0] {
493                Sexp::Atom(Atom::S(s)) if s == "forall" => parse_forall(sexp),
494                Sexp::Atom(Atom::S(s)) if s == "and" => parse_conj(sexp),
495                _ => parse_pred(sexp),
496            }
497        }
498        _ => Err(ParseError::MalformedSexpError("Expected constraint body to be list")),
499    }
500}
501
502fn sexp_to_constraint(sexp: &Sexp) -> Result<Constraint<ParsingTypes>, ParseError> {
503    match sexp {
504        Sexp::List(items) => {
505            match &items[0] {
506                Sexp::Atom(Atom::S(atom)) if atom == "constraint" => {
507                    sexp_to_constraint_inner(&items[1])
508                }
509                _ => {
510                    Err(ParseError::MalformedSexpError(
511                        "Expected constraint definition to start with \"constraint\"",
512                    ))
513                }
514            }
515        }
516        _ => Err(ParseError::MalformedSexpError("Expected list for constraint definition")),
517    }
518}
519
520fn parse_kvar_decl_args(sexp: &Sexp) -> Result<Vec<Sort<ParsingTypes>>, ParseError> {
521    match sexp {
522        Sexp::List(items) => items.iter().map(parse_sort).collect(),
523        _ => Err(ParseError::MalformedSexpError("Expected list of sorts for kvar declaration")),
524    }
525}
526
527fn sexp_to_kvar_decl_inner(sexp: &Sexp) -> Result<KVarDecl<ParsingTypes>, ParseError> {
528    match sexp {
529        Sexp::List(items) => {
530            match &items[1] {
531                Sexp::Atom(Atom::S(s)) if s.starts_with("$") => {
532                    let sorts = parse_kvar_decl_args(&items[2])?;
533                    Ok(KVarDecl { kvid: s.clone(), sorts, comment: String::new() })
534                }
535                _ => Err(ParseError::MalformedSexpError("Expected kvar name to start with $")),
536            }
537        }
538        _ => Err(ParseError::MalformedSexpError("Expected list for kvar declaration")),
539    }
540}
541
542fn sexp_to_kvar_decl(sexp: &Sexp) -> Result<KVarDecl<ParsingTypes>, ParseError> {
543    match sexp {
544        Sexp::List(items) => {
545            match &items[0] {
546                Sexp::Atom(Atom::S(atom)) if atom == "var" => sexp_to_kvar_decl_inner(sexp),
547                _ => {
548                    Err(ParseError::MalformedSexpError(
549                        "Expected kvar declaration to start with \"var\"",
550                    ))
551                }
552            }
553        }
554        _ => Err(ParseError::MalformedSexpError("Expected list for constraint definition")),
555    }
556}
557
558fn parse_qualifier_arg(sexp: &Sexp) -> Result<(String, Sort<ParsingTypes>), ParseError> {
559    match sexp {
560        Sexp::List(items) => {
561            if let Sexp::Atom(Atom::S(var_name)) = &items[0] {
562                let arg_sort = parse_sort(&items[1])?;
563                Ok((var_name.clone(), arg_sort))
564            } else {
565                Err(ParseError::MalformedSexpError(
566                    "Expected qualifier argument to have variable name",
567                ))
568            }
569        }
570        _ => Err(ParseError::MalformedSexpError("Expected list for qualifier argument")),
571    }
572}
573
574fn parse_qualifier_args(sexp: &Sexp) -> Result<Vec<(String, Sort<ParsingTypes>)>, ParseError> {
575    match sexp {
576        Sexp::List(args) => args.iter().map(parse_qualifier_arg).collect(),
577        _ => Err(ParseError::MalformedSexpError("Expected list for qualifier arguments")),
578    }
579}
580
581fn sexp_to_qualifier_inner(sexp: &Sexp) -> Result<Qualifier<ParsingTypes>, ParseError> {
582    match sexp {
583        Sexp::List(items) => {
584            if let Sexp::Atom(Atom::S(name)) = &items[1] {
585                let qualifier_args = parse_qualifier_args(&items[2])?;
586                let qualifier_body = parse_expr_possibly_nested(&items[3])?;
587                Ok(Qualifier { name: name.clone(), args: qualifier_args, body: qualifier_body })
588            } else {
589                Err(ParseError::MalformedSexpError(
590                    "Expected qualifier declaration to provide name",
591                ))
592            }
593        }
594        _ => Err(ParseError::MalformedSexpError("Expected list for qualifier declaration")),
595    }
596}
597
598fn sexp_to_qualifier(sexp: &Sexp) -> Result<Qualifier<ParsingTypes>, ParseError> {
599    match sexp {
600        Sexp::List(items) => {
601            match &items[0] {
602                Sexp::Atom(Atom::S(atom)) if atom == "qualif" => sexp_to_qualifier_inner(sexp),
603                _ => {
604                    Err(ParseError::MalformedSexpError(
605                        "Expected qualifier declaration to start with \"qualif\"",
606                    ))
607                }
608            }
609        }
610        _ => Err(ParseError::MalformedSexpError("Expected list for qualifier declaration")),
611    }
612}
613
614// pub fn parse_constraint(input: &str) -> Result<Constraint<ParsingTypes>, ParseError> {
615//     let mut sexp_parser = SexpParser::new(input);
616//     let sexp = sexp_parser.parse().map_err(ParseError::SexpParseError)?;
617//     sexp_to_constraint(&sexp)
618// }
619
620pub fn parse_constraint_with_kvars(
621    input: &str,
622) -> Result<ConstraintWithEnv<ParsingTypes>, ParseError> {
623    let mut sexp_parser = SexpParser::new(input);
624    let sexps = sexp_parser
625        .parse_all()
626        .map_err(ParseError::SexpParseError)?;
627    let mut kvar_decls = Vec::new();
628    let mut qualifiers = Vec::new();
629    for sexp in sexps {
630        if let Ok(kvar_decl) = sexp_to_kvar_decl(&sexp) {
631            kvar_decls.push(kvar_decl);
632        } else if let Ok(qualifier) = sexp_to_qualifier(&sexp) {
633            qualifiers.push(qualifier);
634        } else if let Ok(constraint) = sexp_to_constraint(&sexp) {
635            return Ok(ConstraintWithEnv::new(vec![], kvar_decls, qualifiers, vec![], constraint));
636        }
637    }
638    Err(ParseError::MalformedSexpError("No constraint found"))
639}
liquid_fixpoint/parser.rs

liquid_fixpoint/
parser.rs
