dhall/
builtins.rs

1use std::collections::{BTreeMap, HashMap};
2use std::convert::TryInto;
3
4use crate::operations::{BinOp, OpKind};
5use crate::semantics::{nze, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv};
6use crate::syntax::Const::Type;
7use crate::syntax::{
8    Const, Expr, ExprKind, InterpolatedText, InterpolatedTextContents, Label,
9    NaiveDouble, NumKind, Span, UnspannedExpr, V,
10};
11use crate::{Ctxt, Parsed};
12
13/// Built-ins
14#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
15pub enum Builtin {
16    Bool,
17    Natural,
18    Integer,
19    Double,
20    Text,
21    List,
22    Optional,
23    OptionalNone,
24    NaturalBuild,
25    NaturalFold,
26    NaturalIsZero,
27    NaturalEven,
28    NaturalOdd,
29    NaturalToInteger,
30    NaturalShow,
31    NaturalSubtract,
32    IntegerToDouble,
33    IntegerShow,
34    IntegerNegate,
35    IntegerClamp,
36    DoubleShow,
37    ListBuild,
38    ListFold,
39    ListLength,
40    ListHead,
41    ListLast,
42    ListIndexed,
43    ListReverse,
44    TextShow,
45    TextReplace,
46}
47
48impl Builtin {
49    pub fn parse(s: &str) -> Option<Self> {
50        use Builtin::*;
51        match s {
52            "Bool" => Some(Bool),
53            "Natural" => Some(Natural),
54            "Integer" => Some(Integer),
55            "Double" => Some(Double),
56            "Text" => Some(Text),
57            "List" => Some(List),
58            "Optional" => Some(Optional),
59            "None" => Some(OptionalNone),
60            "Natural/build" => Some(NaturalBuild),
61            "Natural/fold" => Some(NaturalFold),
62            "Natural/isZero" => Some(NaturalIsZero),
63            "Natural/even" => Some(NaturalEven),
64            "Natural/odd" => Some(NaturalOdd),
65            "Natural/toInteger" => Some(NaturalToInteger),
66            "Natural/show" => Some(NaturalShow),
67            "Natural/subtract" => Some(NaturalSubtract),
68            "Integer/toDouble" => Some(IntegerToDouble),
69            "Integer/show" => Some(IntegerShow),
70            "Integer/negate" => Some(IntegerNegate),
71            "Integer/clamp" => Some(IntegerClamp),
72            "Double/show" => Some(DoubleShow),
73            "List/build" => Some(ListBuild),
74            "List/fold" => Some(ListFold),
75            "List/length" => Some(ListLength),
76            "List/head" => Some(ListHead),
77            "List/last" => Some(ListLast),
78            "List/indexed" => Some(ListIndexed),
79            "List/reverse" => Some(ListReverse),
80            "Text/show" => Some(TextShow),
81            "Text/replace" => Some(TextReplace),
82            _ => None,
83        }
84    }
85}
86
87/// A partially applied builtin.
88/// Invariant: the evaluation of the given args must not be able to progress further
89#[derive(Debug, Clone)]
90pub struct BuiltinClosure<'cx> {
91    env: NzEnv<'cx>,
92    b: Builtin,
93    /// Arguments applied to the closure so far.
94    args: Vec<Nir<'cx>>,
95}
96
97impl<'cx> BuiltinClosure<'cx> {
98    pub fn new(b: Builtin, env: NzEnv<'cx>) -> NirKind<'cx> {
99        apply_builtin(b, Vec::new(), env)
100    }
101    pub fn apply(&self, a: Nir<'cx>) -> NirKind<'cx> {
102        use std::iter::once;
103        let args = self.args.iter().cloned().chain(once(a)).collect();
104        apply_builtin(self.b, args, self.env.clone())
105    }
106    pub fn to_hirkind(&self, venv: VarEnv) -> HirKind<'cx> {
107        HirKind::Expr(self.args.iter().fold(
108            ExprKind::Builtin(self.b),
109            |acc, v| {
110                ExprKind::Op(OpKind::App(
111                    Hir::new(HirKind::Expr(acc), Span::Artificial),
112                    v.to_hir(venv),
113                ))
114            },
115        ))
116    }
117}
118
119pub fn rc(x: UnspannedExpr) -> Expr {
120    Expr::new(x, Span::Artificial)
121}
122
123// Ad-hoc macro to help construct the types of builtins
124macro_rules! make_type {
125    (Type) => { rc(ExprKind::Const(Const::Type)) };
126    (Bool) => { rc(ExprKind::Builtin(Builtin::Bool)) };
127    (Natural) => { rc(ExprKind::Builtin(Builtin::Natural)) };
128    (Integer) => { rc(ExprKind::Builtin(Builtin::Integer)) };
129    (Double) => { rc(ExprKind::Builtin(Builtin::Double)) };
130    (Text) => { rc(ExprKind::Builtin(Builtin::Text)) };
131    ($var:ident) => {
132        rc(ExprKind::Var(V(stringify!($var).into(), 0)))
133    };
134    (Optional $ty:ident) => {
135        rc(ExprKind::Op(OpKind::App(
136            rc(ExprKind::Builtin(Builtin::Optional)),
137            make_type!($ty)
138        )))
139    };
140    (List $($rest:tt)*) => {
141        rc(ExprKind::Op(OpKind::App(
142            rc(ExprKind::Builtin(Builtin::List)),
143            make_type!($($rest)*)
144        )))
145    };
146    ({ $($label:ident : $ty:ident),* }) => {{
147        let mut kts = BTreeMap::new();
148        $(
149            kts.insert(
150                Label::from(stringify!($label)),
151                make_type!($ty),
152            );
153        )*
154        rc(ExprKind::RecordType(kts))
155    }};
156    ($ty:ident -> $($rest:tt)*) => {
157        rc(ExprKind::Pi(
158            "_".into(),
159            make_type!($ty),
160            make_type!($($rest)*)
161        ))
162    };
163    (($($arg:tt)*) -> $($rest:tt)*) => {
164        rc(ExprKind::Pi(
165            "_".into(),
166            make_type!($($arg)*),
167            make_type!($($rest)*)
168        ))
169    };
170    (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
171        rc(ExprKind::Pi(
172            stringify!($var).into(),
173            make_type!($($ty)*),
174            make_type!($($rest)*)
175        ))
176    };
177}
178
179pub fn type_of_builtin<'cx>(cx: Ctxt<'cx>, b: Builtin) -> Hir<'cx> {
180    use Builtin::*;
181    let expr = match b {
182        Bool | Natural | Integer | Double | Text => make_type!(Type),
183        List | Optional => make_type!(
184            Type -> Type
185        ),
186
187        NaturalFold => make_type!(
188            Natural ->
189            forall (natural: Type) ->
190            forall (succ: natural -> natural) ->
191            forall (zero: natural) ->
192            natural
193        ),
194        NaturalBuild => make_type!(
195            (forall (natural: Type) ->
196                forall (succ: natural -> natural) ->
197                forall (zero: natural) ->
198                natural) ->
199            Natural
200        ),
201        NaturalIsZero | NaturalEven | NaturalOdd => make_type!(
202            Natural -> Bool
203        ),
204        NaturalToInteger => make_type!(Natural -> Integer),
205        NaturalShow => make_type!(Natural -> Text),
206        NaturalSubtract => make_type!(Natural -> Natural -> Natural),
207
208        IntegerToDouble => make_type!(Integer -> Double),
209        IntegerShow => make_type!(Integer -> Text),
210        IntegerNegate => make_type!(Integer -> Integer),
211        IntegerClamp => make_type!(Integer -> Natural),
212
213        DoubleShow => make_type!(Double -> Text),
214        TextShow => make_type!(Text -> Text),
215        TextReplace => make_type!(
216            forall (needle: Text) ->
217            forall (replacement: Text) ->
218            forall (haystack: Text) ->
219            Text
220        ),
221        ListBuild => make_type!(
222            forall (a: Type) ->
223            (forall (list: Type) ->
224                forall (cons: a -> list -> list) ->
225                forall (nil: list) ->
226                list) ->
227            List a
228        ),
229        ListFold => make_type!(
230            forall (a: Type) ->
231            (List a) ->
232            forall (list: Type) ->
233            forall (cons: a -> list -> list) ->
234            forall (nil: list) ->
235            list
236        ),
237        ListLength => make_type!(forall (a: Type) -> (List a) -> Natural),
238        ListHead | ListLast => {
239            make_type!(forall (a: Type) -> (List a) -> Optional a)
240        }
241        ListIndexed => make_type!(
242            forall (a: Type) ->
243            (List a) ->
244            List { index: Natural, value: a }
245        ),
246        ListReverse => make_type!(
247            forall (a: Type) -> (List a) -> List a
248        ),
249
250        OptionalNone => make_type!(
251            forall (A: Type) -> Optional A
252        ),
253    };
254    Parsed::from_expr_without_imports(expr)
255        .resolve(cx)
256        .unwrap()
257        .0
258}
259
260// Ad-hoc macro to help construct closures
261macro_rules! make_closure {
262    (var($var:ident)) => {{
263        rc(ExprKind::Var(V(
264            Label::from(stringify!($var)).into(),
265            0
266        )))
267    }};
268    (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{
269        let var = Label::from(stringify!($var));
270        let ty = make_closure!($($ty)*);
271        let body = make_closure!($($body)*);
272        rc(ExprKind::Lam(var, ty, body))
273    }};
274    (Type) => {
275        rc(ExprKind::Const(Type))
276    };
277    (Natural) => {
278        rc(ExprKind::Builtin(Builtin::Natural))
279    };
280    (List $($ty:tt)*) => {{
281        let ty = make_closure!($($ty)*);
282        rc(ExprKind::Op(OpKind::App(
283            rc(ExprKind::Builtin(Builtin::List)),
284            ty
285        )))
286    }};
287    (Some($($v:tt)*)) => {
288        rc(ExprKind::SomeLit(
289            make_closure!($($v)*)
290        ))
291    };
292    (1 + $($v:tt)*) => {
293        rc(ExprKind::Op(OpKind::BinOp(
294            BinOp::NaturalPlus,
295            make_closure!($($v)*),
296            rc(ExprKind::Num(NumKind::Natural(1)))
297        )))
298    };
299    ([ $($head:tt)* ] # $($tail:tt)*) => {{
300        let head = make_closure!($($head)*);
301        let tail = make_closure!($($tail)*);
302        rc(ExprKind::Op(OpKind::BinOp(
303            BinOp::ListAppend,
304            rc(ExprKind::NEListLit(vec![head])),
305            tail,
306        )))
307    }};
308}
309
310#[allow(clippy::cognitive_complexity)]
311fn apply_builtin<'cx>(
312    b: Builtin,
313    args: Vec<Nir<'cx>>,
314    env: NzEnv<'cx>,
315) -> NirKind<'cx> {
316    let cx = env.cx();
317    use NirKind::*;
318    use NumKind::{Bool, Double, Integer, Natural};
319
320    // Small helper enum
321    enum Ret<'cx> {
322        NirKind(NirKind<'cx>),
323        Nir(Nir<'cx>),
324        DoneAsIs,
325    }
326    let make_closure = |e| {
327        Parsed::from_expr_without_imports(e)
328            .resolve(cx)
329            .unwrap()
330            .typecheck(cx)
331            .unwrap()
332            .as_hir()
333            .eval(env.clone())
334    };
335
336    let ret = match (b, args.as_slice()) {
337        (Builtin::Bool, [])
338        | (Builtin::Natural, [])
339        | (Builtin::Integer, [])
340        | (Builtin::Double, [])
341        | (Builtin::Text, []) => Ret::NirKind(BuiltinType(b)),
342        (Builtin::Optional, [t]) => Ret::NirKind(OptionalType(t.clone())),
343        (Builtin::List, [t]) => Ret::NirKind(ListType(t.clone())),
344
345        (Builtin::OptionalNone, [t]) => {
346            Ret::NirKind(EmptyOptionalLit(t.clone()))
347        }
348        (Builtin::NaturalIsZero, [n]) => match &*n.kind() {
349            Num(Natural(n)) => Ret::NirKind(Num(Bool(*n == 0))),
350            _ => Ret::DoneAsIs,
351        },
352        (Builtin::NaturalEven, [n]) => match &*n.kind() {
353            Num(Natural(n)) => Ret::NirKind(Num(Bool(*n % 2 == 0))),
354            _ => Ret::DoneAsIs,
355        },
356        (Builtin::NaturalOdd, [n]) => match &*n.kind() {
357            Num(Natural(n)) => Ret::NirKind(Num(Bool(*n % 2 != 0))),
358            _ => Ret::DoneAsIs,
359        },
360        (Builtin::NaturalToInteger, [n]) => match &*n.kind() {
361            Num(Natural(n)) => Ret::NirKind(Num(Integer(*n as i64))),
362            _ => Ret::DoneAsIs,
363        },
364        (Builtin::NaturalShow, [n]) => match &*n.kind() {
365            Num(Natural(n)) => Ret::Nir(Nir::from_text(n)),
366            _ => Ret::DoneAsIs,
367        },
368        (Builtin::NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
369            (Num(Natural(a)), Num(Natural(b))) => {
370                Ret::NirKind(Num(Natural(if b > a { b - a } else { 0 })))
371            }
372            (Num(Natural(0)), _) => Ret::Nir(b.clone()),
373            (_, Num(Natural(0))) => Ret::NirKind(Num(Natural(0))),
374            _ if a == b => Ret::NirKind(Num(Natural(0))),
375            _ => Ret::DoneAsIs,
376        },
377        (Builtin::IntegerShow, [n]) => match &*n.kind() {
378            Num(Integer(n)) => {
379                let s = if *n < 0 {
380                    n.to_string()
381                } else {
382                    format!("+{}", n)
383                };
384                Ret::Nir(Nir::from_text(s))
385            }
386            _ => Ret::DoneAsIs,
387        },
388        (Builtin::IntegerToDouble, [n]) => match &*n.kind() {
389            Num(Integer(n)) => {
390                Ret::NirKind(Num(Double(NaiveDouble::from(*n as f64))))
391            }
392            _ => Ret::DoneAsIs,
393        },
394        (Builtin::IntegerNegate, [n]) => match &*n.kind() {
395            Num(Integer(n)) => Ret::NirKind(Num(Integer(-n))),
396            _ => Ret::DoneAsIs,
397        },
398        (Builtin::IntegerClamp, [n]) => match &*n.kind() {
399            Num(Integer(n)) => {
400                Ret::NirKind(Num(Natural((*n).try_into().unwrap_or(0))))
401            }
402            _ => Ret::DoneAsIs,
403        },
404        (Builtin::DoubleShow, [n]) => match &*n.kind() {
405            Num(Double(n)) => Ret::Nir(Nir::from_text(n)),
406            _ => Ret::DoneAsIs,
407        },
408        (Builtin::TextShow, [v]) => match &*v.kind() {
409            TextLit(tlit) => {
410                if let Some(s) = tlit.as_text() {
411                    // Printing InterpolatedText takes care of all the escaping
412                    let txt: InterpolatedText<Expr> =
413                        std::iter::once(InterpolatedTextContents::Text(s))
414                            .collect();
415                    Ret::Nir(Nir::from_text(txt))
416                } else {
417                    Ret::DoneAsIs
418                }
419            }
420            _ => Ret::DoneAsIs,
421        },
422        (Builtin::TextReplace, [needle, replacement, haystack]) => {
423            // Helper to match a Nir as a text literal
424            fn nir_to_string(n: &Nir) -> Option<String> {
425                match &*n.kind() {
426                    TextLit(n_lit) => n_lit.as_text(),
427                    _ => None,
428                }
429            }
430
431            // The needle needs to be fully evaluated as Text otherwise no
432            // progress can be made
433            match nir_to_string(needle) {
434                // When the needle is empty the haystack is returned untouched
435                Some(n) if n.is_empty() => Ret::Nir(haystack.clone()),
436                Some(n) => {
437                    // The haystack needs to be fully evaluated as Text otherwise no
438                    // progress can be made
439                    if let Some(h) = nir_to_string(haystack) {
440                        // Fast case when replacement is fully evaluated
441                        if let Some(r) = nir_to_string(replacement) {
442                            Ret::Nir(Nir::from_text(h.replace(&n, &r)))
443                        } else {
444                            use itertools::Itertools;
445
446                            let parts = h.split(&n).map(|s| {
447                                InterpolatedTextContents::Text(s.to_string())
448                            });
449                            let replacement = InterpolatedTextContents::Expr(
450                                replacement.clone(),
451                            );
452
453                            Ret::Nir(Nir::from_kind(NirKind::TextLit(
454                                nze::nir::TextLit::new(Itertools::intersperse(
455                                    parts,
456                                    replacement,
457                                )),
458                            )))
459                        }
460                    } else {
461                        Ret::DoneAsIs
462                    }
463                }
464                _ => Ret::DoneAsIs,
465            }
466        }
467        (Builtin::ListLength, [_, l]) => match &*l.kind() {
468            EmptyListLit(_) => Ret::NirKind(Num(Natural(0))),
469            NEListLit(xs) => Ret::NirKind(Num(Natural(xs.len() as u64))),
470            _ => Ret::DoneAsIs,
471        },
472        (Builtin::ListHead, [_, l]) => match &*l.kind() {
473            EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())),
474            NEListLit(xs) => {
475                Ret::NirKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
476            }
477            _ => Ret::DoneAsIs,
478        },
479        (Builtin::ListLast, [_, l]) => match &*l.kind() {
480            EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())),
481            NEListLit(xs) => Ret::NirKind(NEOptionalLit(
482                xs.iter().rev().next().unwrap().clone(),
483            )),
484            _ => Ret::DoneAsIs,
485        },
486        (Builtin::ListReverse, [_, l]) => match &*l.kind() {
487            EmptyListLit(n) => Ret::NirKind(EmptyListLit(n.clone())),
488            NEListLit(xs) => {
489                Ret::NirKind(NEListLit(xs.iter().rev().cloned().collect()))
490            }
491            _ => Ret::DoneAsIs,
492        },
493        (Builtin::ListIndexed, [t, l]) => {
494            match l.kind() {
495                EmptyListLit(_) | NEListLit(_) => {
496                    // Construct the returned record type: { index: Natural, value: t }
497                    let mut kts = HashMap::new();
498                    kts.insert(
499                        "index".into(),
500                        Nir::from_builtin(cx, Builtin::Natural),
501                    );
502                    kts.insert("value".into(), t.clone());
503                    let t = Nir::from_kind(RecordType(kts));
504
505                    // Construct the new list, with added indices
506                    let list = match l.kind() {
507                        EmptyListLit(_) => EmptyListLit(t),
508                        NEListLit(xs) => NEListLit(
509                            xs.iter()
510                                .enumerate()
511                                .map(|(i, e)| {
512                                    let mut kvs = HashMap::new();
513                                    kvs.insert(
514                                        "index".into(),
515                                        Nir::from_kind(Num(Natural(i as u64))),
516                                    );
517                                    kvs.insert("value".into(), e.clone());
518                                    Nir::from_kind(RecordLit(kvs))
519                                })
520                                .collect(),
521                        ),
522                        _ => unreachable!(),
523                    };
524                    Ret::NirKind(list)
525                }
526                _ => Ret::DoneAsIs,
527            }
528        }
529        (Builtin::ListBuild, [t, f]) => {
530            let list_t = Nir::from_builtin(cx, Builtin::List).app(t.clone());
531            Ret::Nir(
532                f.app(list_t)
533                    .app(
534                        make_closure(make_closure!(
535                            λ(T : Type) ->
536                            λ(a : var(T)) ->
537                            λ(as : List var(T)) ->
538                            [ var(a) ] # var(as)
539                        ))
540                        .app(t.clone()),
541                    )
542                    .app(EmptyListLit(t.clone()).into_nir()),
543            )
544        }
545        (Builtin::ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
546            EmptyListLit(_) => Ret::Nir(nil.clone()),
547            NEListLit(xs) => {
548                let mut v = nil.clone();
549                for x in xs.iter().cloned().rev() {
550                    v = cons.app(x).app(v);
551                }
552                Ret::Nir(v)
553            }
554            _ => Ret::DoneAsIs,
555        },
556        (Builtin::NaturalBuild, [f]) => Ret::Nir(
557            f.app(Nir::from_builtin(cx, Builtin::Natural))
558                .app(make_closure(make_closure!(
559                    λ(x : Natural) ->
560                    1 + var(x)
561                )))
562                .app(Num(Natural(0)).into_nir()),
563        ),
564
565        (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
566            Num(Natural(0)) => Ret::Nir(zero.clone()),
567            Num(Natural(n)) => {
568                let fold = Nir::from_builtin(cx, Builtin::NaturalFold)
569                    .app(Num(Natural(n - 1)).into_nir())
570                    .app(t.clone())
571                    .app(succ.clone())
572                    .app(zero.clone());
573                Ret::Nir(succ.app(fold))
574            }
575            _ => Ret::DoneAsIs,
576        },
577        _ => Ret::DoneAsIs,
578    };
579    match ret {
580        Ret::NirKind(v) => v,
581        Ret::Nir(v) => v.kind().clone(),
582        Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, env }),
583    }
584}
585
586impl<'cx> std::cmp::PartialEq for BuiltinClosure<'cx> {
587    fn eq(&self, other: &Self) -> bool {
588        self.b == other.b && self.args == other.args
589    }
590}
591impl<'cx> std::cmp::Eq for BuiltinClosure<'cx> {}
592
593impl std::fmt::Display for Builtin {
594    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
595        use Builtin::*;
596        f.write_str(match *self {
597            Bool => "Bool",
598            Natural => "Natural",
599            Integer => "Integer",
600            Double => "Double",
601            Text => "Text",
602            List => "List",
603            Optional => "Optional",
604            OptionalNone => "None",
605            NaturalBuild => "Natural/build",
606            NaturalFold => "Natural/fold",
607            NaturalIsZero => "Natural/isZero",
608            NaturalEven => "Natural/even",
609            NaturalOdd => "Natural/odd",
610            NaturalToInteger => "Natural/toInteger",
611            NaturalShow => "Natural/show",
612            NaturalSubtract => "Natural/subtract",
613            IntegerToDouble => "Integer/toDouble",
614            IntegerNegate => "Integer/negate",
615            IntegerClamp => "Integer/clamp",
616            IntegerShow => "Integer/show",
617            DoubleShow => "Double/show",
618            ListBuild => "List/build",
619            ListFold => "List/fold",
620            ListLength => "List/length",
621            ListHead => "List/head",
622            ListLast => "List/last",
623            ListIndexed => "List/indexed",
624            ListReverse => "List/reverse",
625            TextShow => "Text/show",
626            TextReplace => "Text/replace",
627        })
628    }
629}
dhall/builtins.rs

dhall/
builtins.rs
