From 7683b0d762cf0df489ad4bc006e8db2358e81cf4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 Jan 2020 21:50:04 +0000 Subject: Implement assert & merge and fix more bugs --- dhall/src/semantics/core/value.rs | 47 ++++++++++++++++++++++++++++++--------- 1 file changed, 36 insertions(+), 11 deletions(-) (limited to 'dhall/src/semantics/core') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 71c5c65..3dcbd38 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -56,10 +56,15 @@ pub(crate) enum Form { } #[derive(Debug, Clone)] -pub(crate) struct Closure { - arg_ty: Value, - env: NzEnv, - body: TyExpr, +pub(crate) enum Closure { + /// Normal closure + Closure { + arg_ty: Value, + env: NzEnv, + body: TyExpr, + }, + /// Closure that ignores the argument passed + ConstantClosure { env: NzEnv, body: TyExpr }, } #[derive(Debug, Clone, PartialEq, Eq)] @@ -696,21 +701,41 @@ impl ValueKind { impl Closure { pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self { - Closure { + Closure::Closure { arg_ty, env: env.clone(), body, } } + pub fn new_constant(env: &NzEnv, body: TyExpr) -> Self { + Closure::ConstantClosure { + env: env.clone(), + body, + } + } pub fn apply(&self, val: Value) -> Value { - self.body.normalize_whnf(&self.env.insert_value(val)) + match self { + Closure::Closure { env, body, .. } => { + body.normalize_whnf(&env.insert_value(val)) + } + Closure::ConstantClosure { env, body, .. } => { + body.normalize_whnf(env) + } + } } pub fn apply_var(&self, var: NzVar) -> Value { - let val = Value::from_kind_and_type( - ValueKind::Var(AlphaVar::default(), var), - self.arg_ty.clone(), - ); - self.apply(val) + match self { + Closure::Closure { arg_ty, .. } => { + let val = Value::from_kind_and_type( + ValueKind::Var(AlphaVar::default(), var), + arg_ty.clone(), + ); + self.apply(val) + } + Closure::ConstantClosure { env, body, .. } => { + body.normalize_whnf(env) + } + } } } -- cgit v1.2.3