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

liquid_fixpoint/
parser.rs
