From db1375eccd1e6943b504cd54ed17eb8f4d19c25f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 6 Feb 2020 17:35:54 +0000 Subject: Remove most reliance on types stored in Value --- dhall/src/semantics/nze/normalize.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index a00b7ff..3a981f4 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -17,14 +17,14 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { closure.apply(a).to_whnf_check_type(ty) } ValueKind::AppliedBuiltin(closure) => { - closure.apply(a, f.get_type().unwrap(), ty) + closure.apply(a, f.get_type_not_sort(), ty) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), a, kts.clone(), uniont.clone(), - f.get_type().unwrap(), + f.get_type_not_sort(), ), _ => ValueKind::PartialExpr(ExprKind::App(f, a)), } @@ -349,7 +349,7 @@ pub(crate) fn normalize_one_layer( UnionType(kts) => Ret::ValueKind(UnionConstructor( l.clone(), kts.clone(), - v.get_type().unwrap(), + v.get_type_not_sort(), )), PartialExpr(ExprKind::BinOp( BinOp::RightBiasedRecordMerge, @@ -536,7 +536,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind { } TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { let val = val.eval(env); - body.eval(&env.insert_value(val)).kind().clone() + body.eval(&env.insert_value_noty(val)).kind().clone() } TyExprKind::Expr(e) => { let ty = match tye.get_type() { -- cgit v1.2.3 From 5870a46d5ab5810901198f03ed461d5c3bb5aa8a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 6 Feb 2020 17:58:48 +0000 Subject: Remove move type propagation through Value --- dhall/src/semantics/nze/normalize.rs | 124 ++++++++++------------------------- 1 file changed, 33 insertions(+), 91 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 3a981f4..c660fce 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -6,18 +6,16 @@ use crate::semantics::{ Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value, ValueKind, }; -use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, -}; +use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents}; use crate::Normalized; -pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { +pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind { match f.kind() { ValueKind::LamClosure { closure, .. } => { - closure.apply(a).to_whnf_check_type(ty) + closure.apply(a).kind().clone() } ValueKind::AppliedBuiltin(closure) => { - closure.apply(a, f.get_type_not_sort(), ty) + closure.apply(a, f.get_type_not_sort()) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), @@ -102,12 +100,7 @@ enum Ret<'a> { Expr(ExprKind), } -fn apply_binop<'a>( - o: BinOp, - x: &'a Value, - y: &'a Value, - ty: &Value, -) -> Option> { +fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { use BinOp::{ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, @@ -194,19 +187,12 @@ fn apply_binop<'a>( Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let kts = match ty.kind() { - RecordType(kts) => kts, - _ => unreachable!("Internal type error"), - }; - let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { - Ok(Value::from_partial_expr( - ExprKind::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), - ), - kts.get(k).expect("Internal type error").clone(), - )) + let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |_, v1, v2| { + Ok(Value::from_partial_expr(ExprKind::BinOp( + RecursiveRecordMerge, + v1.clone(), + v2.clone(), + ))) })?; Ret::ValueKind(RecordLit(kvs)) } @@ -217,14 +203,11 @@ fn apply_binop<'a>( kts_y, // If the Label exists for both records, then we hit the recursive case. |_, l: &Value, r: &Value| { - Ok(Value::from_partial_expr( - ExprKind::BinOp( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - ), - ty.clone(), - )) + Ok(Value::from_partial_expr(ExprKind::BinOp( + RecursiveRecordTypeMerge, + l.clone(), + r.clone(), + ))) }, )?; Ret::ValueKind(RecordType(kts)) @@ -240,7 +223,6 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprKind, - ty: &Value, env: &NzEnv, ) -> ValueKind { use ValueKind::{ @@ -318,7 +300,7 @@ pub(crate) fn normalize_one_layer( } } } - ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { + ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) { Some(ret) => ret, None => Ret::Expr(expr), }, @@ -335,7 +317,6 @@ pub(crate) fn normalize_one_layer( PartialExpr(ExprKind::Projection(v2, _)) => { return normalize_one_layer( ExprKind::Projection(v2.clone(), ls.clone()), - ty, env, ) } @@ -361,45 +342,26 @@ pub(crate) fn normalize_one_layer( None => { return normalize_one_layer( ExprKind::Field(x.clone(), l.clone()), - ty, env, ) } }, (RecordLit(kvs), _) => match kvs.get(l) { Some(r) => Ret::Expr(ExprKind::Field( - Value::from_kind_and_type( - PartialExpr(ExprKind::BinOp( - BinOp::RightBiasedRecordMerge, - Value::from_kind_and_type( - RecordLit({ - let mut kvs = HashMap::new(); - kvs.insert(l.clone(), r.clone()); - kvs - }), - Value::from_kind_and_type( - RecordType({ - let mut kvs = HashMap::new(); - kvs.insert( - l.clone(), - r.get_type_not_sort(), - ); - kvs - }), - r.get_type_not_sort() - .get_type_not_sort(), - ), - ), - y.clone(), - )), - v.get_type_not_sort(), - ), + Value::from_kind(PartialExpr(ExprKind::BinOp( + BinOp::RightBiasedRecordMerge, + Value::from_kind(RecordLit({ + let mut kvs = HashMap::new(); + kvs.insert(l.clone(), r.clone()); + kvs + })), + y.clone(), + ))), l.clone(), )), None => { return normalize_one_layer( ExprKind::Field(y.clone(), l.clone()), - ty, env, ) } @@ -416,7 +378,6 @@ pub(crate) fn normalize_one_layer( None => { return normalize_one_layer( ExprKind::Field(y.clone(), l.clone()), - ty, env, ) } @@ -426,7 +387,6 @@ pub(crate) fn normalize_one_layer( None => { return normalize_one_layer( ExprKind::Field(x.clone(), l.clone()), - ty, env, ) } @@ -482,22 +442,9 @@ pub(crate) fn normalize_one_layer( .sorted_by_key(|(k, _)| k.clone()) .map(|(k, v)| { let mut rec = HashMap::new(); - let mut rec_ty = HashMap::new(); rec.insert("mapKey".into(), Value::from_text(k)); rec.insert("mapValue".into(), v.clone()); - rec_ty.insert( - "mapKey".into(), - Value::from_builtin(Builtin::Text), - ); - rec_ty.insert("mapValue".into(), v.get_type_not_sort()); - - Value::from_kind_and_type( - ValueKind::RecordLit(rec), - Value::from_kind_and_type( - ValueKind::RecordType(rec_ty), - Value::from_const(Const::Type), - ), - ) + Value::from_kind(ValueKind::RecordLit(rec)) }) .collect(), )), @@ -507,8 +454,8 @@ pub(crate) fn normalize_one_layer( match ret { Ret::ValueKind(v) => v, - Ret::Value(v) => v.to_whnf_check_type(ty), - Ret::ValueRef(v) => v.to_whnf_check_type(ty), + Ret::Value(v) => v.kind().clone(), + Ret::ValueRef(v) => v.kind().clone(), Ret::Expr(expr) => ValueKind::PartialExpr(expr), } } @@ -521,17 +468,16 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind { let annot = annot.eval(env); ValueKind::LamClosure { binder: Binder::new(binder.clone()), - annot: annot.clone(), - closure: Closure::new(annot, env, body.clone()), + annot: annot, + closure: Closure::new(env, body.clone()), } } TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { let annot = annot.eval(env); - let closure = Closure::new(annot.clone(), env, body.clone()); ValueKind::PiClosure { binder: Binder::new(binder.clone()), annot, - closure, + closure: Closure::new(env, body.clone()), } } TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { @@ -539,12 +485,8 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind { body.eval(&env.insert_value_noty(val)).kind().clone() } TyExprKind::Expr(e) => { - let ty = match tye.get_type() { - Ok(ty) => ty, - Err(_) => return ValueKind::Const(Const::Sort), - }; let e = e.map_ref(|tye| tye.eval(env)); - normalize_one_layer(e, &ty, env) + normalize_one_layer(e, env) } } } -- cgit v1.2.3 From 27031b3739ff9f2043e64130a4c5699d0f9233e8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:23:59 +0000 Subject: Add Hir as untyped alternative to TyExpr --- dhall/src/semantics/nze/normalize.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index c660fce..b5949f5 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -3,8 +3,8 @@ use std::collections::HashMap; use crate::semantics::NzEnv; use crate::semantics::{ - Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value, - ValueKind, + Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, TyExpr, TyExprKind, + Value, ValueKind, }; use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents}; use crate::Normalized; -- cgit v1.2.3 From 6c90d356c9a4a5bbeb88f25ad0ab499ba1503eae Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:53:55 +0000 Subject: Remove most TyExpr from normalization --- dhall/src/semantics/nze/normalize.rs | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index b5949f5..acb2e51 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -3,8 +3,7 @@ use std::collections::HashMap; use crate::semantics::NzEnv; use crate::semantics::{ - Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, TyExpr, TyExprKind, - Value, ValueKind, + Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind, }; use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents}; use crate::Normalized; @@ -460,11 +459,11 @@ pub(crate) fn normalize_one_layer( } } -/// Normalize a TyExpr into WHNF -pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind { - match tye.kind() { - TyExprKind::Var(var) => env.lookup_val(var), - TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { +/// Normalize Hir into WHNF +pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind { + match hir.kind() { + HirKind::Var(var) => env.lookup_val(var), + HirKind::Expr(ExprKind::Lam(binder, annot, body)) => { let annot = annot.eval(env); ValueKind::LamClosure { binder: Binder::new(binder.clone()), @@ -472,7 +471,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind { closure: Closure::new(env, body.clone()), } } - TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { + HirKind::Expr(ExprKind::Pi(binder, annot, body)) => { let annot = annot.eval(env); ValueKind::PiClosure { binder: Binder::new(binder.clone()), @@ -480,12 +479,12 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind { closure: Closure::new(env, body.clone()), } } - TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { + HirKind::Expr(ExprKind::Let(_, None, val, body)) => { let val = val.eval(env); body.eval(&env.insert_value_noty(val)).kind().clone() } - TyExprKind::Expr(e) => { - let e = e.map_ref(|tye| tye.eval(env)); + HirKind::Expr(e) => { + let e = e.map_ref(|hir| hir.eval(env)); normalize_one_layer(e, env) } } -- cgit v1.2.3 From 5688ed654eee258bf8ffc8761ce693c73a0242d5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:58:11 +0000 Subject: Remove extra types stored in Value --- dhall/src/semantics/nze/normalize.rs | 24 ++++++++---------------- 1 file changed, 8 insertions(+), 16 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') 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), }, -- cgit v1.2.3 From 35cc98dc767247f4881866de40c7d8dd82eba8a5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:30:32 +0000 Subject: Remove types from NzEnv --- dhall/src/semantics/nze/normalize.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 981d894..d12146a 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -473,7 +473,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind { } HirKind::Expr(ExprKind::Let(_, None, val, body)) => { let val = val.eval(env); - body.eval(&env.insert_value_noty(val)).kind().clone() + body.eval(&env.insert_value(val, ())).kind().clone() } HirKind::Expr(e) => { let e = e.map_ref(|hir| hir.eval(env)); -- cgit v1.2.3 From 5a2538d174fd36a8ed7f4fa344b9583fc48bd977 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2020 13:12:13 +0000 Subject: Remove the Embed variant from ExprKind --- dhall/src/semantics/nze/normalize.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index d12146a..03b91a5 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -6,7 +6,6 @@ use crate::semantics::{ Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind, }; use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents}; -use crate::Normalized; pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind { match f.kind() { @@ -90,7 +89,7 @@ enum Ret<'a> { ValueKind(ValueKind), Value(Value), ValueRef(&'a Value), - Expr(ExprKind), + Expr(ExprKind), } fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { @@ -215,7 +214,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { } pub(crate) fn normalize_one_layer( - expr: ExprKind, + expr: ExprKind, env: &NzEnv, ) -> ValueKind { use ValueKind::{ @@ -233,7 +232,6 @@ pub(crate) fn normalize_one_layer( ExprKind::Lam(..) | ExprKind::Pi(..) | ExprKind::Let(..) - | ExprKind::Embed(_) | ExprKind::Var(_) => { unreachable!("This case should have been handled in typecheck") } -- cgit v1.2.3 From 40bee3cdcb9ac0c76996feeceb6ca160a6bd8b42 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2020 19:04:44 +0000 Subject: Introduce LitKind to factor out common enum nodes --- dhall/src/semantics/nze/normalize.rs | 86 +++++++++++++++++++----------------- 1 file changed, 45 insertions(+), 41 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 03b91a5..4111190 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -5,7 +5,9 @@ use crate::semantics::NzEnv; use crate::semantics::{ Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind, }; -use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents}; +use crate::syntax::{ + BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind, +}; pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind { match f.kind() { @@ -98,40 +100,44 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge, TextAppend, }; - use ValueKind::{ - BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, - }; + use LitKind::{Bool, Natural}; + use ValueKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType}; + Some(match (o, x.kind(), y.kind()) { - (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y), - (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x), - (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)), - (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)), + (BoolAnd, Lit(Bool(true)), _) => Ret::ValueRef(y), + (BoolAnd, _, Lit(Bool(true))) => Ret::ValueRef(x), + (BoolAnd, Lit(Bool(false)), _) => Ret::ValueKind(Lit(Bool(false))), + (BoolAnd, _, Lit(Bool(false))) => Ret::ValueKind(Lit(Bool(false))), (BoolAnd, _, _) if x == y => Ret::ValueRef(x), - (BoolOr, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)), - (BoolOr, _, BoolLit(true)) => Ret::ValueKind(BoolLit(true)), - (BoolOr, BoolLit(false), _) => Ret::ValueRef(y), - (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x), + (BoolOr, Lit(Bool(true)), _) => Ret::ValueKind(Lit(Bool(true))), + (BoolOr, _, Lit(Bool(true))) => Ret::ValueKind(Lit(Bool(true))), + (BoolOr, Lit(Bool(false)), _) => Ret::ValueRef(y), + (BoolOr, _, Lit(Bool(false))) => Ret::ValueRef(x), (BoolOr, _, _) if x == y => Ret::ValueRef(x), - (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y), - (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x), - (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)), - (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)), - (BoolNE, BoolLit(false), _) => Ret::ValueRef(y), - (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x), - (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)), - (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)), + (BoolEQ, Lit(Bool(true)), _) => Ret::ValueRef(y), + (BoolEQ, _, Lit(Bool(true))) => Ret::ValueRef(x), + (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => { + Ret::ValueKind(Lit(Bool(x == y))) + } + (BoolEQ, _, _) if x == y => Ret::ValueKind(Lit(Bool(true))), + (BoolNE, Lit(Bool(false)), _) => Ret::ValueRef(y), + (BoolNE, _, Lit(Bool(false))) => Ret::ValueRef(x), + (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => { + Ret::ValueKind(Lit(Bool(x != y))) + } + (BoolNE, _, _) if x == y => Ret::ValueKind(Lit(Bool(false))), - (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y), - (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), - (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueKind(NaturalLit(x + y)) - } - (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)), - (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)), - (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y), - (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x), - (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueKind(NaturalLit(x * y)) + (NaturalPlus, Lit(Natural(0)), _) => Ret::ValueRef(y), + (NaturalPlus, _, Lit(Natural(0))) => Ret::ValueRef(x), + (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => { + Ret::ValueKind(Lit(Natural(x + y))) + } + (NaturalTimes, Lit(Natural(0)), _) => Ret::ValueKind(Lit(Natural(0))), + (NaturalTimes, _, Lit(Natural(0))) => Ret::ValueKind(Lit(Natural(0))), + (NaturalTimes, Lit(Natural(1)), _) => Ret::ValueRef(y), + (NaturalTimes, _, Lit(Natural(1))) => Ret::ValueRef(x), + (NaturalTimes, Lit(Natural(x)), Lit(Natural(y))) => { + Ret::ValueKind(Lit(Natural(x * y))) } (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y), @@ -217,10 +223,11 @@ pub(crate) fn normalize_one_layer( expr: ExprKind, env: &NzEnv, ) -> ValueKind { + use LitKind::Bool; use ValueKind::{ - BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, - NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit, - RecordType, UnionConstructor, UnionLit, UnionType, + EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit, + PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, + UnionType, }; let ret = match expr { @@ -240,10 +247,7 @@ pub(crate) fn normalize_one_layer( ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)), ExprKind::Assert(_) => Ret::Expr(expr), ExprKind::App(v, a) => Ret::Value(v.app(a)), - ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), - ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)), - ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)), - ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), + ExprKind::Lit(l) => Ret::ValueKind(Lit(l.clone())), ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match t.kind() { @@ -279,12 +283,12 @@ pub(crate) fn normalize_one_layer( } ExprKind::BoolIf(ref b, ref e1, ref e2) => { match b.kind() { - BoolLit(true) => Ret::ValueRef(e1), - BoolLit(false) => Ret::ValueRef(e2), + Lit(Bool(true)) => Ret::ValueRef(e1), + Lit(Bool(false)) => Ret::ValueRef(e2), _ => { match (e1.kind(), e2.kind()) { // Simplify `if b then True else False` - (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b), + (Lit(Bool(true)), Lit(Bool(false))) => Ret::ValueRef(b), _ if e1 == e2 => Ret::ValueRef(e1), _ => Ret::Expr(expr), } -- cgit v1.2.3 From d65d639ff93691adbf0a208edb99736003bc64bd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 15 Feb 2020 19:05:26 +0000 Subject: Factor some tck code to avoid needing get_type_tyexpr --- dhall/src/semantics/nze/normalize.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 4111190..c8dd5ae 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -475,7 +475,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind { } HirKind::Expr(ExprKind::Let(_, None, val, body)) => { let val = val.eval(env); - body.eval(&env.insert_value(val, ())).kind().clone() + body.eval(env.insert_value(val, ())).kind().clone() } HirKind::Expr(e) => { let e = e.map_ref(|hir| hir.eval(env)); -- cgit v1.2.3 From 5057144ed99bc4e1a76a0840dd39fc1bd862665c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 15 Feb 2020 19:10:52 +0000 Subject: Desugar Completion during resolution --- dhall/src/semantics/nze/normalize.rs | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index c8dd5ae..0e09511 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -231,17 +231,16 @@ pub(crate) fn normalize_one_layer( }; let ret = match expr { - ExprKind::Import(_) => unreachable!( - "There should remain no imports in a resolved expression" - ), - // Those cases have already been completely handled in the typechecking phase (using - // `RetWhole`), so they won't appear here. - ExprKind::Lam(..) - | ExprKind::Pi(..) - | ExprKind::Let(..) - | ExprKind::Var(_) => { - unreachable!("This case should have been handled in typecheck") + ExprKind::Import(..) | ExprKind::Completion(..) => { + unreachable!("This case should have been handled in resolution") } + ExprKind::Var(..) + | ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) => unreachable!( + "This case should have been handled in normalize_hir_whnf" + ), + ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(Value::from_const(c)), ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)), @@ -391,7 +390,6 @@ pub(crate) fn normalize_one_layer( ExprKind::ProjectionByExpr(_, _) => { unimplemented!("selection by expression") } - ExprKind::Completion(_, _) => unimplemented!("record completion"), ExprKind::Merge(ref handlers, ref variant, _) => { match handlers.kind() { -- cgit v1.2.3 From 130de8cea49c848a06174c61c747d9414a5c71b7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 16 Feb 2020 19:06:23 +0000 Subject: Start requiring Universe to build a Type --- dhall/src/semantics/nze/normalize.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 0e09511..c2d2dc2 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -471,7 +471,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind { closure: Closure::new(env, body.clone()), } } - HirKind::Expr(ExprKind::Let(_, None, val, body)) => { + HirKind::Expr(ExprKind::Let(_, _, val, body)) => { let val = val.eval(env); body.eval(env.insert_value(val, ())).kind().clone() } -- cgit v1.2.3 From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:22:06 +0000 Subject: Rename Value to Nir --- dhall/src/semantics/nze/normalize.rs | 243 +++++++++++++++++------------------ 1 file changed, 115 insertions(+), 128 deletions(-) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index c2d2dc2..4c2aa33 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -3,41 +3,39 @@ use std::collections::HashMap; use crate::semantics::NzEnv; use crate::semantics::{ - Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind, + Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit, }; use crate::syntax::{ BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind, }; -pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind { +pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind { match f.kind() { - ValueKind::LamClosure { closure, .. } => { - closure.apply(a).kind().clone() + NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(), + NirKind::AppliedBuiltin(closure) => closure.apply(a), + NirKind::UnionConstructor(l, kts) => { + NirKind::UnionLit(l.clone(), a, kts.clone()) } - ValueKind::AppliedBuiltin(closure) => closure.apply(a), - ValueKind::UnionConstructor(l, kts) => { - ValueKind::UnionLit(l.clone(), a, kts.clone()) - } - _ => ValueKind::PartialExpr(ExprKind::App(f, a)), + _ => NirKind::PartialExpr(ExprKind::App(f, a)), } } pub(crate) fn squash_textlit( - elts: impl Iterator>, -) -> Vec> { + elts: impl Iterator>, +) -> Vec> { use std::mem::replace; use InterpolatedTextContents::{Expr, Text}; fn inner( - elts: impl Iterator>, + elts: impl Iterator>, crnt_str: &mut String, - ret: &mut Vec>, + ret: &mut Vec>, ) { for contents in elts { match contents { Text(s) => crnt_str.push_str(&s), Expr(e) => match e.kind() { - ValueKind::TextLit(elts2) => { + NirKind::TextLit(elts2) => { inner(elts2.iter().cloned(), crnt_str, ret) } _ => { @@ -88,85 +86,77 @@ where // Small helper enum to avoid repetition enum Ret<'a> { - ValueKind(ValueKind), - Value(Value), - ValueRef(&'a Value), - Expr(ExprKind), + NirKind(NirKind), + Nir(Nir), + NirRef(&'a Nir), + Expr(ExprKind), } -fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { +fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { use BinOp::{ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge, TextAppend, }; use LitKind::{Bool, Natural}; - use ValueKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType}; + use NirKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType}; Some(match (o, x.kind(), y.kind()) { - (BoolAnd, Lit(Bool(true)), _) => Ret::ValueRef(y), - (BoolAnd, _, Lit(Bool(true))) => Ret::ValueRef(x), - (BoolAnd, Lit(Bool(false)), _) => Ret::ValueKind(Lit(Bool(false))), - (BoolAnd, _, Lit(Bool(false))) => Ret::ValueKind(Lit(Bool(false))), - (BoolAnd, _, _) if x == y => Ret::ValueRef(x), - (BoolOr, Lit(Bool(true)), _) => Ret::ValueKind(Lit(Bool(true))), - (BoolOr, _, Lit(Bool(true))) => Ret::ValueKind(Lit(Bool(true))), - (BoolOr, Lit(Bool(false)), _) => Ret::ValueRef(y), - (BoolOr, _, Lit(Bool(false))) => Ret::ValueRef(x), - (BoolOr, _, _) if x == y => Ret::ValueRef(x), - (BoolEQ, Lit(Bool(true)), _) => Ret::ValueRef(y), - (BoolEQ, _, Lit(Bool(true))) => Ret::ValueRef(x), - (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => { - Ret::ValueKind(Lit(Bool(x == y))) - } - (BoolEQ, _, _) if x == y => Ret::ValueKind(Lit(Bool(true))), - (BoolNE, Lit(Bool(false)), _) => Ret::ValueRef(y), - (BoolNE, _, Lit(Bool(false))) => Ret::ValueRef(x), - (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => { - Ret::ValueKind(Lit(Bool(x != y))) - } - (BoolNE, _, _) if x == y => Ret::ValueKind(Lit(Bool(false))), + (BoolAnd, Lit(Bool(true)), _) => Ret::NirRef(y), + (BoolAnd, _, Lit(Bool(true))) => Ret::NirRef(x), + (BoolAnd, Lit(Bool(false)), _) => Ret::NirKind(Lit(Bool(false))), + (BoolAnd, _, Lit(Bool(false))) => Ret::NirKind(Lit(Bool(false))), + (BoolAnd, _, _) if x == y => Ret::NirRef(x), + (BoolOr, Lit(Bool(true)), _) => Ret::NirKind(Lit(Bool(true))), + (BoolOr, _, Lit(Bool(true))) => Ret::NirKind(Lit(Bool(true))), + (BoolOr, Lit(Bool(false)), _) => Ret::NirRef(y), + (BoolOr, _, Lit(Bool(false))) => Ret::NirRef(x), + (BoolOr, _, _) if x == y => Ret::NirRef(x), + (BoolEQ, Lit(Bool(true)), _) => Ret::NirRef(y), + (BoolEQ, _, Lit(Bool(true))) => Ret::NirRef(x), + (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x == y))), + (BoolEQ, _, _) if x == y => Ret::NirKind(Lit(Bool(true))), + (BoolNE, Lit(Bool(false)), _) => Ret::NirRef(y), + (BoolNE, _, Lit(Bool(false))) => Ret::NirRef(x), + (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x != y))), + (BoolNE, _, _) if x == y => Ret::NirKind(Lit(Bool(false))), - (NaturalPlus, Lit(Natural(0)), _) => Ret::ValueRef(y), - (NaturalPlus, _, Lit(Natural(0))) => Ret::ValueRef(x), + (NaturalPlus, Lit(Natural(0)), _) => Ret::NirRef(y), + (NaturalPlus, _, Lit(Natural(0))) => Ret::NirRef(x), (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => { - Ret::ValueKind(Lit(Natural(x + y))) + Ret::NirKind(Lit(Natural(x + y))) } - (NaturalTimes, Lit(Natural(0)), _) => Ret::ValueKind(Lit(Natural(0))), - (NaturalTimes, _, Lit(Natural(0))) => Ret::ValueKind(Lit(Natural(0))), - (NaturalTimes, Lit(Natural(1)), _) => Ret::ValueRef(y), - (NaturalTimes, _, Lit(Natural(1))) => Ret::ValueRef(x), + (NaturalTimes, Lit(Natural(0)), _) => Ret::NirKind(Lit(Natural(0))), + (NaturalTimes, _, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))), + (NaturalTimes, Lit(Natural(1)), _) => Ret::NirRef(y), + (NaturalTimes, _, Lit(Natural(1))) => Ret::NirRef(x), (NaturalTimes, Lit(Natural(x)), Lit(Natural(y))) => { - Ret::ValueKind(Lit(Natural(x * y))) + Ret::NirKind(Lit(Natural(x * y))) } - (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y), - (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind( - NEListLit(xs.iter().chain(ys.iter()).cloned().collect()), - ), + (ListAppend, EmptyListLit(_), _) => Ret::NirRef(y), + (ListAppend, _, EmptyListLit(_)) => Ret::NirRef(x), + (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::NirKind(NEListLit( + xs.iter().chain(ys.iter()).cloned().collect(), + )), - (TextAppend, ValueKind::TextLit(x), _) if x.is_empty() => { - Ret::ValueRef(y) - } - (TextAppend, _, ValueKind::TextLit(y)) if y.is_empty() => { - Ret::ValueRef(x) - } - (TextAppend, ValueKind::TextLit(x), ValueKind::TextLit(y)) => { - Ret::ValueKind(ValueKind::TextLit(x.concat(y))) - } - (TextAppend, ValueKind::TextLit(x), _) => Ret::ValueKind( - ValueKind::TextLit(x.concat(&TextLit::interpolate(y.clone()))), - ), - (TextAppend, _, ValueKind::TextLit(y)) => Ret::ValueKind( - ValueKind::TextLit(TextLit::interpolate(x.clone()).concat(y)), - ), + (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => Ret::NirRef(y), + (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => Ret::NirRef(x), + (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => { + Ret::NirKind(NirKind::TextLit(x.concat(y))) + } + (TextAppend, NirKind::TextLit(x), _) => Ret::NirKind(NirKind::TextLit( + x.concat(&TextLit::interpolate(y.clone())), + )), + (TextAppend, _, NirKind::TextLit(y)) => Ret::NirKind(NirKind::TextLit( + TextLit::interpolate(x.clone()).concat(y), + )), (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ValueRef(x) + Ret::NirRef(x) } (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ValueRef(y) + Ret::NirRef(y) } (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let mut kvs = kvs2.clone(); @@ -174,25 +164,25 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { // Insert only if key not already present kvs.entry(x.clone()).or_insert_with(|| v.clone()); } - Ret::ValueKind(RecordLit(kvs)) + Ret::NirKind(RecordLit(kvs)) } - (RightBiasedRecordMerge, _, _) if x == y => Ret::ValueRef(y), + (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y), (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ValueRef(x) + Ret::NirRef(x) } (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ValueRef(y) + Ret::NirRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |_, v1, v2| { - Ok(Value::from_partial_expr(ExprKind::BinOp( + Ok(Nir::from_partial_expr(ExprKind::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), ))) })?; - Ret::ValueKind(RecordLit(kvs)) + Ret::NirKind(RecordLit(kvs)) } (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => { @@ -200,31 +190,28 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { kts_x, kts_y, // If the Label exists for both records, then we hit the recursive case. - |_, l: &Value, r: &Value| { - Ok(Value::from_partial_expr(ExprKind::BinOp( + |_, l: &Nir, r: &Nir| { + Ok(Nir::from_partial_expr(ExprKind::BinOp( RecursiveRecordTypeMerge, l.clone(), r.clone(), ))) }, )?; - Ret::ValueKind(RecordType(kts)) + Ret::NirKind(RecordType(kts)) } (Equivalence, _, _) => { - Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone())) + Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone())) } _ => return None, }) } -pub(crate) fn normalize_one_layer( - expr: ExprKind, - env: &NzEnv, -) -> ValueKind { +pub(crate) fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { use LitKind::Bool; - use ValueKind::{ + use NirKind::{ EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit, PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, UnionType, @@ -241,54 +228,54 @@ pub(crate) fn normalize_one_layer( "This case should have been handled in normalize_hir_whnf" ), - ExprKind::Annot(x, _) => Ret::Value(x), - ExprKind::Const(c) => Ret::Value(Value::from_const(c)), - ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)), + ExprKind::Annot(x, _) => Ret::Nir(x), + ExprKind::Const(c) => Ret::Nir(Nir::from_const(c)), + ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)), ExprKind::Assert(_) => Ret::Expr(expr), - ExprKind::App(v, a) => Ret::Value(v.app(a)), - ExprKind::Lit(l) => Ret::ValueKind(Lit(l.clone())), - ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), + ExprKind::App(v, a) => Ret::Nir(v.app(a)), + ExprKind::Lit(l) => Ret::NirKind(Lit(l.clone())), + ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match t.kind() { - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, .. }) if args.len() == 1 => args[0].clone(), _ => panic!("internal type error"), }; - Ret::ValueKind(ValueKind::EmptyListLit(arg)) + Ret::NirKind(NirKind::EmptyListLit(arg)) } ExprKind::NEListLit(elts) => { - Ret::ValueKind(NEListLit(elts.into_iter().collect())) + Ret::NirKind(NEListLit(elts.into_iter().collect())) } ExprKind::RecordLit(kvs) => { - Ret::ValueKind(RecordLit(kvs.into_iter().collect())) + Ret::NirKind(RecordLit(kvs.into_iter().collect())) } ExprKind::RecordType(kvs) => { - Ret::ValueKind(RecordType(kvs.into_iter().collect())) + Ret::NirKind(RecordType(kvs.into_iter().collect())) } ExprKind::UnionType(kvs) => { - Ret::ValueKind(UnionType(kvs.into_iter().collect())) + Ret::NirKind(UnionType(kvs.into_iter().collect())) } ExprKind::TextLit(elts) => { let tlit = TextLit::new(elts.into_iter()); // Simplify bare interpolation if let Some(v) = tlit.as_single_expr() { - Ret::Value(v.clone()) + Ret::Nir(v.clone()) } else { - Ret::ValueKind(ValueKind::TextLit(tlit)) + Ret::NirKind(NirKind::TextLit(tlit)) } } ExprKind::BoolIf(ref b, ref e1, ref e2) => { match b.kind() { - Lit(Bool(true)) => Ret::ValueRef(e1), - Lit(Bool(false)) => Ret::ValueRef(e2), + Lit(Bool(true)) => Ret::NirRef(e1), + Lit(Bool(false)) => Ret::NirRef(e2), _ => { match (e1.kind(), e2.kind()) { // Simplify `if b then True else False` - (Lit(Bool(true)), Lit(Bool(false))) => Ret::ValueRef(b), - _ if e1 == e2 => Ret::ValueRef(e1), + (Lit(Bool(true)), Lit(Bool(false))) => Ret::NirRef(b), + _ if e1 == e2 => Ret::NirRef(e1), _ => Ret::Expr(expr), } } @@ -300,10 +287,10 @@ pub(crate) fn normalize_one_layer( }, ExprKind::Projection(_, ref ls) if ls.is_empty() => { - Ret::ValueKind(RecordLit(HashMap::new())) + Ret::NirKind(RecordLit(HashMap::new())) } ExprKind::Projection(ref v, ref ls) => match v.kind() { - RecordLit(kvs) => Ret::ValueKind(RecordLit( + RecordLit(kvs) => Ret::NirKind(RecordLit( ls.iter() .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) .collect(), @@ -318,11 +305,11 @@ pub(crate) fn normalize_one_layer( }, ExprKind::Field(ref v, ref l) => match v.kind() { RecordLit(kvs) => match kvs.get(l) { - Some(r) => Ret::Value(r.clone()), + Some(r) => Ret::Nir(r.clone()), None => Ret::Expr(expr), }, UnionType(kts) => { - Ret::ValueKind(UnionConstructor(l.clone(), kts.clone())) + Ret::NirKind(UnionConstructor(l.clone(), kts.clone())) } PartialExpr(ExprKind::BinOp( BinOp::RightBiasedRecordMerge, @@ -330,7 +317,7 @@ pub(crate) fn normalize_one_layer( y, )) => match (x.kind(), y.kind()) { (_, RecordLit(kvs)) => match kvs.get(l) { - Some(r) => Ret::Value(r.clone()), + Some(r) => Ret::Nir(r.clone()), None => { return normalize_one_layer( ExprKind::Field(x.clone(), l.clone()), @@ -340,9 +327,9 @@ pub(crate) fn normalize_one_layer( }, (RecordLit(kvs), _) => match kvs.get(l) { Some(r) => Ret::Expr(ExprKind::Field( - Value::from_kind(PartialExpr(ExprKind::BinOp( + Nir::from_kind(PartialExpr(ExprKind::BinOp( BinOp::RightBiasedRecordMerge, - Value::from_kind(RecordLit({ + Nir::from_kind(RecordLit({ let mut kvs = HashMap::new(); kvs.insert(l.clone(), r.clone()); kvs @@ -395,19 +382,19 @@ pub(crate) fn normalize_one_layer( match handlers.kind() { RecordLit(kvs) => match variant.kind() { UnionConstructor(l, _) => match kvs.get(l) { - Some(h) => Ret::Value(h.clone()), + Some(h) => Ret::Nir(h.clone()), None => Ret::Expr(expr), }, UnionLit(l, v, _) => match kvs.get(l) { - Some(h) => Ret::Value(h.app(v.clone())), + Some(h) => Ret::Nir(h.app(v.clone())), None => Ret::Expr(expr), }, EmptyOptionalLit(_) => match kvs.get(&"None".into()) { - Some(h) => Ret::Value(h.clone()), + Some(h) => Ret::Nir(h.clone()), None => Ret::Expr(expr), }, NEOptionalLit(v) => match kvs.get(&"Some".into()) { - Some(h) => Ret::Value(h.app(v.clone())), + Some(h) => Ret::Nir(h.app(v.clone())), None => Ret::Expr(expr), }, _ => Ret::Expr(expr), @@ -418,24 +405,24 @@ pub(crate) fn normalize_one_layer( ExprKind::ToMap(ref v, ref annot) => match v.kind() { RecordLit(kvs) if kvs.is_empty() => { match annot.as_ref().map(|v| v.kind()) { - Some(ValueKind::AppliedBuiltin(BuiltinClosure { + Some(NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, .. })) if args.len() == 1 => { - Ret::ValueKind(EmptyListLit(args[0].clone())) + Ret::NirKind(EmptyListLit(args[0].clone())) } _ => Ret::Expr(expr), } } - RecordLit(kvs) => Ret::ValueKind(NEListLit( + RecordLit(kvs) => Ret::NirKind(NEListLit( kvs.iter() .sorted_by_key(|(k, _)| k.clone()) .map(|(k, v)| { let mut rec = HashMap::new(); - rec.insert("mapKey".into(), Value::from_text(k)); + rec.insert("mapKey".into(), Nir::from_text(k)); rec.insert("mapValue".into(), v.clone()); - Value::from_kind(ValueKind::RecordLit(rec)) + Nir::from_kind(NirKind::RecordLit(rec)) }) .collect(), )), @@ -444,20 +431,20 @@ pub(crate) fn normalize_one_layer( }; match ret { - Ret::ValueKind(v) => v, - Ret::Value(v) => v.kind().clone(), - Ret::ValueRef(v) => v.kind().clone(), - Ret::Expr(expr) => ValueKind::PartialExpr(expr), + Ret::NirKind(v) => v, + Ret::Nir(v) => v.kind().clone(), + Ret::NirRef(v) => v.kind().clone(), + Ret::Expr(expr) => NirKind::PartialExpr(expr), } } /// Normalize Hir into WHNF -pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind { +pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind { match hir.kind() { HirKind::Var(var) => env.lookup_val(var), HirKind::Expr(ExprKind::Lam(binder, annot, body)) => { let annot = annot.eval(env); - ValueKind::LamClosure { + NirKind::LamClosure { binder: Binder::new(binder.clone()), annot: annot, closure: Closure::new(env, body.clone()), @@ -465,7 +452,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind { } HirKind::Expr(ExprKind::Pi(binder, annot, body)) => { let annot = annot.eval(env); - ValueKind::PiClosure { + NirKind::PiClosure { binder: Binder::new(binder.clone()), annot, closure: Closure::new(env, body.clone()), -- cgit v1.2.3 From 7cbfc1a0d32766a383d1f48902502adaa2234d2f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 19:12:31 +0000 Subject: Avoid re-typechecking after import --- dhall/src/semantics/nze/normalize.rs | 1 + 1 file changed, 1 insertion(+) (limited to 'dhall/src/semantics/nze/normalize.rs') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 4c2aa33..604db8f 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -442,6 +442,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind { match hir.kind() { HirKind::Var(var) => env.lookup_val(var), + HirKind::Import(hir, _) => normalize_hir_whnf(env, hir), HirKind::Expr(ExprKind::Lam(binder, annot, body)) => { let annot = annot.eval(env); NirKind::LamClosure { -- cgit v1.2.3