diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/builtins.rs (renamed from dhall/src/semantics/builtins.rs) | 153 |
1 files changed, 134 insertions, 19 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/builtins.rs index 6007a92..67929a0 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/builtins.rs @@ -1,15 +1,91 @@ +use std::collections::{BTreeMap, HashMap}; +use std::convert::TryInto; + +use crate::operations::{BinOp, OpKind}; use crate::semantics::{ skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv, }; -use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; use crate::syntax::{ - BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText, - InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr, - V, + Const, Expr, ExprKind, InterpolatedText, InterpolatedTextContents, Label, + NaiveDouble, NumKind, Span, UnspannedExpr, V, }; -use std::collections::HashMap; -use std::convert::TryInto; + +/// Built-ins +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] +pub enum Builtin { + Bool, + Natural, + Integer, + Double, + Text, + List, + Optional, + OptionalNone, + NaturalBuild, + NaturalFold, + NaturalIsZero, + NaturalEven, + NaturalOdd, + NaturalToInteger, + NaturalShow, + NaturalSubtract, + IntegerToDouble, + IntegerShow, + IntegerNegate, + IntegerClamp, + DoubleShow, + ListBuild, + ListFold, + ListLength, + ListHead, + ListLast, + ListIndexed, + ListReverse, + OptionalFold, + OptionalBuild, + TextShow, +} + +impl Builtin { + pub fn parse(s: &str) -> Option<Self> { + use Builtin::*; + match s { + "Bool" => Some(Bool), + "Natural" => Some(Natural), + "Integer" => Some(Integer), + "Double" => Some(Double), + "Text" => Some(Text), + "List" => Some(List), + "Optional" => Some(Optional), + "None" => Some(OptionalNone), + "Natural/build" => Some(NaturalBuild), + "Natural/fold" => Some(NaturalFold), + "Natural/isZero" => Some(NaturalIsZero), + "Natural/even" => Some(NaturalEven), + "Natural/odd" => Some(NaturalOdd), + "Natural/toInteger" => Some(NaturalToInteger), + "Natural/show" => Some(NaturalShow), + "Natural/subtract" => Some(NaturalSubtract), + "Integer/toDouble" => Some(IntegerToDouble), + "Integer/show" => Some(IntegerShow), + "Integer/negate" => Some(IntegerNegate), + "Integer/clamp" => Some(IntegerClamp), + "Double/show" => Some(DoubleShow), + "List/build" => Some(ListBuild), + "List/fold" => Some(ListFold), + "List/length" => Some(ListLength), + "List/head" => Some(ListHead), + "List/last" => Some(ListLast), + "List/indexed" => Some(ListIndexed), + "List/reverse" => Some(ListReverse), + "Optional/fold" => Some(OptionalFold), + "Optional/build" => Some(OptionalBuild), + "Text/show" => Some(TextShow), + _ => None, + } + } +} /// A partially applied builtin. /// Invariant: the evaluation of the given args must not be able to progress further @@ -34,10 +110,10 @@ impl BuiltinClosure { HirKind::Expr(self.args.iter().fold( ExprKind::Builtin(self.b), |acc, v| { - ExprKind::App( + ExprKind::Op(OpKind::App( Hir::new(HirKind::Expr(acc), Span::Artificial), v.to_hir(venv), - ) + )) }, )) } @@ -59,19 +135,19 @@ macro_rules! make_type { rc(ExprKind::Var(V(stringify!($var).into(), 0))) }; (Optional $ty:ident) => { - rc(ExprKind::App( + rc(ExprKind::Op(OpKind::App( rc(ExprKind::Builtin(Builtin::Optional)), make_type!($ty) - )) + ))) }; (List $($rest:tt)*) => { - rc(ExprKind::App( + rc(ExprKind::Op(OpKind::App( rc(ExprKind::Builtin(Builtin::List)), make_type!($($rest)*) - )) + ))) }; ({ $($label:ident : $ty:ident),* }) => {{ - let mut kts = DupTreeMap::new(); + let mut kts = BTreeMap::new(); $( kts.insert( Label::from(stringify!($label)), @@ -214,10 +290,10 @@ macro_rules! make_closure { }; (List $($ty:tt)*) => {{ let ty = make_closure!($($ty)*); - rc(ExprKind::App( + rc(ExprKind::Op(OpKind::App( rc(ExprKind::Builtin(Builtin::List)), ty - )) + ))) }}; (Some($($v:tt)*)) => { rc(ExprKind::SomeLit( @@ -225,20 +301,20 @@ macro_rules! make_closure { )) }; (1 + $($v:tt)*) => { - rc(ExprKind::BinOp( + rc(ExprKind::Op(OpKind::BinOp( BinOp::NaturalPlus, make_closure!($($v)*), rc(ExprKind::Num(NumKind::Natural(1))) - )) + ))) }; ([ $($head:tt)* ] # $($tail:tt)*) => {{ let head = make_closure!($($head)*); let tail = make_closure!($($tail)*); - rc(ExprKind::BinOp( + rc(ExprKind::Op(OpKind::BinOp( BinOp::ListAppend, rc(ExprKind::NEListLit(vec![head])), tail, - )) + ))) }}; } @@ -491,3 +567,42 @@ impl std::cmp::PartialEq for BuiltinClosure { } } impl std::cmp::Eq for BuiltinClosure {} + +impl std::fmt::Display for Builtin { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + use Builtin::*; + f.write_str(match *self { + Bool => "Bool", + Natural => "Natural", + Integer => "Integer", + Double => "Double", + Text => "Text", + List => "List", + Optional => "Optional", + OptionalNone => "None", + NaturalBuild => "Natural/build", + NaturalFold => "Natural/fold", + NaturalIsZero => "Natural/isZero", + NaturalEven => "Natural/even", + NaturalOdd => "Natural/odd", + NaturalToInteger => "Natural/toInteger", + NaturalShow => "Natural/show", + NaturalSubtract => "Natural/subtract", + IntegerToDouble => "Integer/toDouble", + IntegerNegate => "Integer/negate", + IntegerClamp => "Integer/clamp", + IntegerShow => "Integer/show", + DoubleShow => "Double/show", + ListBuild => "List/build", + ListFold => "List/fold", + ListLength => "List/length", + ListHead => "List/head", + ListLast => "List/last", + ListIndexed => "List/indexed", + ListReverse => "List/reverse", + OptionalFold => "Optional/fold", + OptionalBuild => "Optional/build", + TextShow => "Text/show", + }) + } +} |