diff options
| -rw-r--r-- | dhall/src/semantics/builtins.rs | 28 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 24 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/value.rs | 15 |
3 files changed, 20 insertions, 47 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 423364d..715e045 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -19,10 +19,6 @@ pub(crate) struct BuiltinClosure<Value> { pub b: Builtin, /// Arguments applied to the closure so far. pub args: Vec<Value>, - /// Keeps the types of the partial applications around to be able to convert back to TyExpr. - /// If the args so far are `x_1`, ..., `x_n`, this contains the types of `b`, `b x1`, ..., - /// `b x_1 x_2 ... x_(n-1)`. - pub types: Vec<Value>, } impl BuiltinClosure<Value> { @@ -31,15 +27,13 @@ impl BuiltinClosure<Value> { env, b, args: Vec::new(), - types: Vec::new(), } } - pub fn apply(&self, a: Value, f_ty: Value) -> ValueKind { + pub fn apply(&self, a: Value) -> ValueKind { use std::iter::once; let args = self.args.iter().cloned().chain(once(a.clone())).collect(); - let types = self.types.iter().cloned().chain(once(f_ty)).collect(); - apply_builtin(self.b, args, types, self.env.clone()) + apply_builtin(self.b, args, self.env.clone()) } /// This doesn't break the invariant because we already checked that the appropriate arguments /// did not normalize to something that allows evaluation to proceed. @@ -49,9 +43,9 @@ impl BuiltinClosure<Value> { } } pub fn to_hirkind(&self, venv: VarEnv) -> HirKind { - HirKind::Expr(self.args.iter().zip(self.types.iter()).fold( + HirKind::Expr(self.args.iter().fold( ExprKind::Builtin(self.b), - |acc, (v, ty)| { + |acc, v| { ExprKind::App( Hir::new(HirKind::Expr(acc), Span::Artificial), v.to_hir(venv), @@ -260,12 +254,7 @@ macro_rules! make_closure { } #[allow(clippy::cognitive_complexity)] -fn apply_builtin( - b: Builtin, - args: Vec<Value>, - types: Vec<Value>, - env: NzEnv, -) -> ValueKind { +fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind { use Builtin::*; use ValueKind::*; @@ -493,12 +482,7 @@ fn apply_builtin( match ret { Ret::ValueKind(v) => v, Ret::Value(v) => v.kind().clone(), - Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { - b, - args, - types, - env, - }), + Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, env }), } } diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index acb2e51..981d894 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -13,16 +13,10 @@ pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind { ValueKind::LamClosure { closure, .. } => { closure.apply(a).kind().clone() } - ValueKind::AppliedBuiltin(closure) => { - closure.apply(a, f.get_type_not_sort()) + ValueKind::AppliedBuiltin(closure) => closure.apply(a), + ValueKind::UnionConstructor(l, kts) => { + ValueKind::UnionLit(l.clone(), a, kts.clone()) } - ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( - l.clone(), - a, - kts.clone(), - uniont.clone(), - f.get_type_not_sort(), - ), _ => ValueKind::PartialExpr(ExprKind::App(f, a)), } } @@ -326,11 +320,9 @@ pub(crate) fn normalize_one_layer( Some(r) => Ret::Value(r.clone()), None => Ret::Expr(expr), }, - UnionType(kts) => Ret::ValueKind(UnionConstructor( - l.clone(), - kts.clone(), - v.get_type_not_sort(), - )), + UnionType(kts) => { + Ret::ValueKind(UnionConstructor(l.clone(), kts.clone())) + } PartialExpr(ExprKind::BinOp( BinOp::RightBiasedRecordMerge, x, @@ -402,11 +394,11 @@ pub(crate) fn normalize_one_layer( ExprKind::Merge(ref handlers, ref variant, _) => { match handlers.kind() { RecordLit(kvs) => match variant.kind() { - UnionConstructor(l, _, _) => match kvs.get(l) { + UnionConstructor(l, _) => match kvs.get(l) { Some(h) => Ret::Value(h.clone()), None => Ret::Expr(expr), }, - UnionLit(l, v, _, _, _) => match kvs.get(l) { + UnionLit(l, v, _) => match kvs.get(l) { Some(h) => Ret::Value(h.app(v.clone())), None => Ret::Expr(expr), }, diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index d05c545..a771b91 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -93,10 +93,8 @@ pub(crate) enum ValueKind { RecordType(HashMap<Label, Value>), RecordLit(HashMap<Label, Value>), UnionType(HashMap<Label, Option<Value>>), - // Also keep the type of the uniontype around - UnionConstructor(Label, HashMap<Label, Option<Value>>, Value), - // Also keep the type of the uniontype and the constructor around - UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value), + UnionConstructor(Label, HashMap<Label, Option<Value>>), + UnionLit(Label, Value, HashMap<Label, Option<Value>>), TextLit(TextLit), Equivalence(Value, Value), /// Invariant: evaluation must not be able to progress with `normalize_one_layer`? @@ -298,14 +296,14 @@ impl Value { .collect(), ), ValueKind::UnionType(kts) => map_uniontype(kts), - ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field( + ValueKind::UnionConstructor(l, kts) => ExprKind::Field( Hir::new( HirKind::Expr(map_uniontype(kts)), Span::Artificial, ), l.clone(), ), - ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App( + ValueKind::UnionLit(l, v, kts) => ExprKind::App( Hir::new( HirKind::Expr(ExprKind::Field( Hir::new( @@ -418,13 +416,12 @@ impl ValueKind { x.normalize(); } } - ValueKind::UnionType(kts) - | ValueKind::UnionConstructor(_, kts, _) => { + ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { for x in kts.values().flat_map(|opt| opt) { x.normalize(); } } - ValueKind::UnionLit(_, v, kts, _, _) => { + ValueKind::UnionLit(_, v, kts) => { v.normalize(); for x in kts.values().flat_map(|opt| opt) { x.normalize(); |