diff options
Diffstat (limited to 'dhall/src/semantics/nze/normalize.rs')
| -rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 413 |
1 files changed, 167 insertions, 246 deletions
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index a00b7ff..604db8f 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -3,49 +3,39 @@ use std::collections::HashMap; use crate::semantics::NzEnv; use crate::semantics::{ - Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value, - ValueKind, + Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit, }; use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, + BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind, }; -use crate::Normalized; -pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { +pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind { match f.kind() { - ValueKind::LamClosure { closure, .. } => { - closure.apply(a).to_whnf_check_type(ty) + 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, f.get_type().unwrap(), ty) - } - ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( - l.clone(), - a, - kts.clone(), - uniont.clone(), - f.get_type().unwrap(), - ), - _ => ValueKind::PartialExpr(ExprKind::App(f, a)), + _ => NirKind::PartialExpr(ExprKind::App(f, a)), } } pub(crate) fn squash_textlit( - elts: impl Iterator<Item = InterpolatedTextContents<Value>>, -) -> Vec<InterpolatedTextContents<Value>> { + elts: impl Iterator<Item = InterpolatedTextContents<Nir>>, +) -> Vec<InterpolatedTextContents<Nir>> { use std::mem::replace; use InterpolatedTextContents::{Expr, Text}; fn inner( - elts: impl Iterator<Item = InterpolatedTextContents<Value>>, + elts: impl Iterator<Item = InterpolatedTextContents<Nir>>, crnt_str: &mut String, - ret: &mut Vec<InterpolatedTextContents<Value>>, + ret: &mut Vec<InterpolatedTextContents<Nir>>, ) { 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) } _ => { @@ -96,86 +86,77 @@ where // Small helper enum to avoid repetition enum Ret<'a> { - ValueKind(ValueKind), - Value(Value), - ValueRef(&'a Value), - Expr(ExprKind<Value, Normalized>), + NirKind(NirKind), + Nir(Nir), + NirRef(&'a Nir), + Expr(ExprKind<Nir>), } -fn apply_binop<'a>( - o: BinOp, - x: &'a Value, - y: &'a Value, - ty: &Value, -) -> Option<Ret<'a>> { +fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> { use BinOp::{ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge, TextAppend, }; - use ValueKind::{ - BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, - }; + use LitKind::{Bool, Natural}; + use NirKind::{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, _, _) 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, _, _) 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)), + (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, NaturalLit(0), _) => Ret::ValueRef(y), - (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), - (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueKind(NaturalLit(x + y)) + (NaturalPlus, Lit(Natural(0)), _) => Ret::NirRef(y), + (NaturalPlus, _, Lit(Natural(0))) => Ret::NirRef(x), + (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => { + Ret::NirKind(Lit(Natural(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)) + (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::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, 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, 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), _) => 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(); @@ -183,32 +164,25 @@ fn apply_binop<'a>( // 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 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(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)) => { @@ -216,118 +190,107 @@ fn apply_binop<'a>( 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( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - ), - ty.clone(), - )) + |_, 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<Value, Normalized>, - ty: &Value, - env: &NzEnv, -) -> ValueKind { - use ValueKind::{ - BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, - NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit, - RecordType, UnionConstructor, UnionLit, UnionType, +pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { + use LitKind::Bool; + use NirKind::{ + EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit, + PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, + UnionType, }; 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::Embed(_) - | 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::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::Var(..) + | ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) => unreachable!( + "This case should have been handled in normalize_hir_whnf" + ), + + 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::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::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() { - BoolLit(true) => Ret::ValueRef(e1), - BoolLit(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` - (BoolLit(true), BoolLit(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), } } } } - 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), }, 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(), @@ -335,7 +298,6 @@ pub(crate) fn normalize_one_layer( PartialExpr(ExprKind::Projection(v2, _)) => { return normalize_one_layer( ExprKind::Projection(v2.clone(), ls.clone()), - ty, env, ) } @@ -343,63 +305,42 @@ 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(), - v.get_type().unwrap(), - )), + UnionType(kts) => { + Ret::NirKind(UnionConstructor(l.clone(), kts.clone())) + } PartialExpr(ExprKind::BinOp( BinOp::RightBiasedRecordMerge, x, 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()), - 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(), - ), + Nir::from_kind(PartialExpr(ExprKind::BinOp( + BinOp::RightBiasedRecordMerge, + Nir::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 +357,6 @@ pub(crate) fn normalize_one_layer( None => { return normalize_one_layer( ExprKind::Field(y.clone(), l.clone()), - ty, env, ) } @@ -426,7 +366,6 @@ pub(crate) fn normalize_one_layer( None => { return normalize_one_layer( ExprKind::Field(x.clone(), l.clone()), - ty, env, ) } @@ -438,25 +377,24 @@ 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() { RecordLit(kvs) => match variant.kind() { - UnionConstructor(l, _, _) => match kvs.get(l) { - Some(h) => Ret::Value(h.clone()), + UnionConstructor(l, _) => match kvs.get(l) { + 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())), + UnionLit(l, v, _) => match kvs.get(l) { + 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), @@ -467,37 +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(); - let mut rec_ty = HashMap::new(); - rec.insert("mapKey".into(), Value::from_text(k)); + rec.insert("mapKey".into(), Nir::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), - ), - ) + Nir::from_kind(NirKind::RecordLit(rec)) }) .collect(), )), @@ -506,45 +431,41 @@ 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::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 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) -> 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); - ValueKind::LamClosure { + NirKind::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)) => { + HirKind::Expr(ExprKind::Pi(binder, annot, body)) => { let annot = annot.eval(env); - let closure = Closure::new(annot.clone(), env, body.clone()); - ValueKind::PiClosure { + NirKind::PiClosure { binder: Binder::new(binder.clone()), annot, - closure, + closure: Closure::new(env, body.clone()), } } - TyExprKind::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() + body.eval(env.insert_value(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) + HirKind::Expr(e) => { + let e = e.map_ref(|hir| hir.eval(env)); + normalize_one_layer(e, env) } } } |