summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r--dhall/src/semantics/nze/nir.rs84
-rw-r--r--dhall/src/semantics/nze/normalize.rs406
2 files changed, 94 insertions, 396 deletions
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index e0d227e..12f1b14 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -1,14 +1,15 @@
use std::collections::HashMap;
use std::rc::Rc;
+use crate::builtins::{Builtin, BuiltinClosure};
+use crate::operations::{BinOp, OpKind};
use crate::semantics::nze::lazy;
use crate::semantics::{
- apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
- BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
+ apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder, Hir,
+ HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
};
use crate::syntax::{
- BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
- NumKind, Span,
+ Const, Expr, ExprKind, InterpolatedTextContents, Label, NumKind, Span,
};
use crate::ToExprOptions;
@@ -74,25 +75,27 @@ pub enum NirKind {
Var(NzVar),
Const(Const),
+ Num(NumKind),
// Must be a number type, Bool or Text
BuiltinType(Builtin),
- Num(NumKind),
- OptionalType(Nir),
+ TextLit(TextLit),
EmptyOptionalLit(Nir),
NEOptionalLit(Nir),
- ListType(Nir),
+ OptionalType(Nir),
// EmptyListLit(t) means `[] : List t`, not `[] : t`
EmptyListLit(Nir),
NEListLit(Vec<Nir>),
- RecordType(HashMap<Label, Nir>),
+ ListType(Nir),
RecordLit(HashMap<Label, Nir>),
- UnionType(HashMap<Label, Option<Nir>>),
+ RecordType(HashMap<Label, Nir>),
UnionConstructor(Label, HashMap<Label, Option<Nir>>),
UnionLit(Label, Nir, HashMap<Label, Option<Nir>>),
- TextLit(TextLit),
+ UnionType(HashMap<Label, Option<Nir>>),
Equivalence(Nir, Nir),
- /// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
- PartialExpr(ExprKind<Nir>),
+ Assert(Nir),
+ /// Invariant: evaluation must not be able to progress with `normalize_operation`.
+ /// This is used when an operation couldn't proceed further, for example because of variables.
+ Op(OpKind<Nir>),
}
impl Nir {
@@ -111,8 +114,7 @@ impl Nir {
NirInternal::from_whnf(v).into_nir()
}
pub fn from_const(c: Const) -> Self {
- let v = NirKind::Const(c);
- NirInternal::from_whnf(v).into_nir()
+ Self::from_kind(NirKind::Const(c))
}
pub fn from_builtin(b: Builtin) -> Self {
Self::from_builtin_env(b, &NzEnv::new())
@@ -148,7 +150,10 @@ impl Nir {
}
pub fn app(&self, v: Nir) -> Nir {
- Nir::from_kind(apply_any(self.clone(), v))
+ Nir::from_kind(self.app_to_kind(v))
+ }
+ pub fn app_to_kind(&self, v: Nir) -> NirKind {
+ apply_any(self, v)
}
pub fn to_hir(&self, venv: VarEnv) -> Hir {
@@ -190,24 +195,24 @@ impl Nir {
NirKind::Const(c) => ExprKind::Const(*c),
NirKind::BuiltinType(b) => ExprKind::Builtin(*b),
NirKind::Num(l) => ExprKind::Num(l.clone()),
- NirKind::OptionalType(t) => ExprKind::App(
+ NirKind::OptionalType(t) => ExprKind::Op(OpKind::App(
Nir::from_builtin(Builtin::Optional).to_hir(venv),
t.to_hir(venv),
- ),
- NirKind::EmptyOptionalLit(n) => ExprKind::App(
+ )),
+ NirKind::EmptyOptionalLit(n) => ExprKind::Op(OpKind::App(
Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
n.to_hir(venv),
- ),
+ )),
NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
- NirKind::ListType(t) => ExprKind::App(
+ NirKind::ListType(t) => ExprKind::Op(OpKind::App(
Nir::from_builtin(Builtin::List).to_hir(venv),
t.to_hir(venv),
- ),
+ )),
NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
- HirKind::Expr(ExprKind::App(
+ HirKind::Expr(ExprKind::Op(OpKind::App(
Nir::from_builtin(Builtin::List).to_hir(venv),
n.to_hir(venv),
- )),
+ ))),
Span::Artificial,
)),
NirKind::NEListLit(elts) => ExprKind::NEListLit(
@@ -229,32 +234,35 @@ impl Nir {
.collect(),
),
NirKind::UnionType(kts) => map_uniontype(kts),
- NirKind::UnionConstructor(l, kts) => ExprKind::Field(
- Hir::new(
- HirKind::Expr(map_uniontype(kts)),
- Span::Artificial,
- ),
- l.clone(),
- ),
- NirKind::UnionLit(l, v, kts) => ExprKind::App(
+ NirKind::UnionConstructor(l, kts) => {
+ ExprKind::Op(OpKind::Field(
+ Hir::new(
+ HirKind::Expr(map_uniontype(kts)),
+ Span::Artificial,
+ ),
+ l.clone(),
+ ))
+ }
+ NirKind::UnionLit(l, v, kts) => ExprKind::Op(OpKind::App(
Hir::new(
- HirKind::Expr(ExprKind::Field(
+ HirKind::Expr(ExprKind::Op(OpKind::Field(
Hir::new(
HirKind::Expr(map_uniontype(kts)),
Span::Artificial,
),
l.clone(),
- )),
+ ))),
Span::Artificial,
),
v.to_hir(venv),
- ),
- NirKind::Equivalence(x, y) => ExprKind::BinOp(
+ )),
+ NirKind::Equivalence(x, y) => ExprKind::Op(OpKind::BinOp(
BinOp::Equivalence,
x.to_hir(venv),
y.to_hir(venv),
- ),
- NirKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
+ )),
+ NirKind::Assert(x) => ExprKind::Assert(x.to_hir(venv)),
+ NirKind::Op(e) => ExprKind::Op(e.map_ref(|v| v.to_hir(venv))),
}),
};
@@ -307,7 +315,7 @@ impl Thunk {
}
fn eval(self) -> NirKind {
match self {
- Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
+ Thunk::Thunk { env, body } => normalize_hir(&env, &body),
Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
}
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 570e106..d042f3f 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -1,18 +1,18 @@
-use itertools::Itertools;
use std::collections::HashMap;
+use crate::operations::{normalize_operation, OpKind};
use crate::semantics::NzEnv;
use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit};
-use crate::syntax::{BinOp, ExprKind, InterpolatedTextContents, NumKind};
+use crate::syntax::{ExprKind, InterpolatedTextContents};
-pub fn apply_any(f: Nir, a: Nir) -> NirKind {
+pub fn apply_any(f: &Nir, a: Nir) -> NirKind {
match f.kind() {
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())
}
- _ => NirKind::PartialExpr(ExprKind::App(f, a)),
+ _ => NirKind::Op(OpKind::App(f.clone(), a)),
}
}
@@ -81,393 +81,83 @@ where
kvs
}
-// Small helper enum to avoid repetition
-enum Ret<'a> {
- NirKind(NirKind),
- Nir(Nir),
- NirRef(&'a Nir),
- Expr(ExprKind<Nir>),
-}
-
-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 NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType};
- use NumKind::{Bool, Natural};
-
- Some(match (o, x.kind(), y.kind()) {
- (BoolAnd, Num(Bool(true)), _) => Ret::NirRef(y),
- (BoolAnd, _, Num(Bool(true))) => Ret::NirRef(x),
- (BoolAnd, Num(Bool(false)), _) => Ret::NirKind(Num(Bool(false))),
- (BoolAnd, _, Num(Bool(false))) => Ret::NirKind(Num(Bool(false))),
- (BoolAnd, _, _) if x == y => Ret::NirRef(x),
- (BoolOr, Num(Bool(true)), _) => Ret::NirKind(Num(Bool(true))),
- (BoolOr, _, Num(Bool(true))) => Ret::NirKind(Num(Bool(true))),
- (BoolOr, Num(Bool(false)), _) => Ret::NirRef(y),
- (BoolOr, _, Num(Bool(false))) => Ret::NirRef(x),
- (BoolOr, _, _) if x == y => Ret::NirRef(x),
- (BoolEQ, Num(Bool(true)), _) => Ret::NirRef(y),
- (BoolEQ, _, Num(Bool(true))) => Ret::NirRef(x),
- (BoolEQ, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x == y))),
- (BoolEQ, _, _) if x == y => Ret::NirKind(Num(Bool(true))),
- (BoolNE, Num(Bool(false)), _) => Ret::NirRef(y),
- (BoolNE, _, Num(Bool(false))) => Ret::NirRef(x),
- (BoolNE, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x != y))),
- (BoolNE, _, _) if x == y => Ret::NirKind(Num(Bool(false))),
-
- (NaturalPlus, Num(Natural(0)), _) => Ret::NirRef(y),
- (NaturalPlus, _, Num(Natural(0))) => Ret::NirRef(x),
- (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => {
- Ret::NirKind(Num(Natural(x + y)))
- }
- (NaturalTimes, Num(Natural(0)), _) => Ret::NirKind(Num(Natural(0))),
- (NaturalTimes, _, Num(Natural(0))) => Ret::NirKind(Num(Natural(0))),
- (NaturalTimes, Num(Natural(1)), _) => Ret::NirRef(y),
- (NaturalTimes, _, Num(Natural(1))) => Ret::NirRef(x),
- (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => {
- Ret::NirKind(Num(Natural(x * y)))
- }
-
- (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, 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),
- )),
+pub type Ret = NirKind;
- (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::NirRef(x)
- }
- (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::NirRef(y)
- }
- (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
- let mut kvs = kvs2.clone();
- for (x, v) in kvs1 {
- // Insert only if key not already present
- kvs.entry(x.clone()).or_insert_with(|| v.clone());
- }
- Ret::NirKind(RecordLit(kvs))
- }
- (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y),
-
- (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::NirRef(x)
- }
- (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::NirRef(y)
- }
- (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
- let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| {
- Nir::from_partial_expr(ExprKind::BinOp(
- RecursiveRecordMerge,
- v1.clone(),
- v2.clone(),
- ))
- });
- Ret::NirKind(RecordLit(kvs))
- }
-
- (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
- let kts = merge_maps(
- kts_x,
- kts_y,
- // If the Label exists for both records, then we hit the recursive case.
- |_, l: &Nir, r: &Nir| {
- Nir::from_partial_expr(ExprKind::BinOp(
- RecursiveRecordTypeMerge,
- l.clone(),
- r.clone(),
- ))
- },
- );
- Ret::NirKind(RecordType(kts))
- }
-
- (Equivalence, _, _) => {
- Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone()))
- }
-
- _ => return None,
- })
+pub fn ret_nir(x: Nir) -> Ret {
+ ret_ref(&x)
+}
+pub fn ret_kind(x: NirKind) -> Ret {
+ x
+}
+pub fn ret_ref(x: &Nir) -> Ret {
+ x.kind().clone()
+}
+pub fn ret_op(x: OpKind<Nir>) -> Ret {
+ NirKind::Op(x)
}
-#[allow(clippy::cognitive_complexity)]
pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
use NirKind::{
- EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num,
- PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
+ Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType,
UnionType,
};
- use NumKind::Bool;
- let ret = match expr {
- ExprKind::Import(..) | ExprKind::Completion(..) => {
- unreachable!("This case should have been handled in resolution")
- }
+ match expr {
ExprKind::Var(..)
| ExprKind::Lam(..)
| ExprKind::Pi(..)
- | ExprKind::Let(..) => unreachable!(
- "This case should have been handled in normalize_hir_whnf"
- ),
+ | ExprKind::Let(..) => {
+ unreachable!("This case should have been handled in normalize_hir")
+ }
- 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::Nir(v.app(a)),
- ExprKind::Num(l) => Ret::NirKind(Num(l)),
- ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)),
+ ExprKind::Const(c) => ret_kind(Const(c)),
+ ExprKind::Num(l) => ret_kind(Num(l)),
+ ExprKind::Builtin(b) => {
+ ret_kind(NirKind::from_builtin_env(b, env.clone()))
+ }
+ ExprKind::TextLit(elts) => {
+ let tlit = TextLit::new(elts.into_iter());
+ // Simplify bare interpolation
+ if let Some(v) = tlit.as_single_expr() {
+ ret_ref(v)
+ } else {
+ ret_kind(NirKind::TextLit(tlit))
+ }
+ }
+ ExprKind::SomeLit(e) => ret_kind(NEOptionalLit(e)),
ExprKind::EmptyListLit(t) => {
let arg = match t.kind() {
NirKind::ListType(t) => t.clone(),
_ => panic!("internal type error"),
};
- Ret::NirKind(NirKind::EmptyListLit(arg))
+ ret_kind(NirKind::EmptyListLit(arg))
}
ExprKind::NEListLit(elts) => {
- Ret::NirKind(NEListLit(elts.into_iter().collect()))
+ ret_kind(NEListLit(elts.into_iter().collect()))
}
ExprKind::RecordLit(kvs) => {
- Ret::NirKind(RecordLit(kvs.into_iter().collect()))
+ ret_kind(RecordLit(kvs.into_iter().collect()))
}
ExprKind::RecordType(kvs) => {
- Ret::NirKind(RecordType(kvs.into_iter().collect()))
+ ret_kind(RecordType(kvs.into_iter().collect()))
}
ExprKind::UnionType(kvs) => {
- 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::Nir(v.clone())
- } else {
- Ret::NirKind(NirKind::TextLit(tlit))
- }
- }
- ExprKind::BoolIf(ref b, ref e1, ref e2) => {
- match b.kind() {
- Num(Bool(true)) => Ret::NirRef(e1),
- Num(Bool(false)) => Ret::NirRef(e2),
- _ => {
- match (e1.kind(), e2.kind()) {
- // Simplify `if b then True else False`
- (Num(Bool(true)), Num(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) {
- Some(ret) => ret,
- None => Ret::Expr(expr),
- },
-
- ExprKind::Field(ref v, ref field) => match v.kind() {
- RecordLit(kvs) => match kvs.get(field) {
- Some(r) => Ret::Nir(r.clone()),
- None => Ret::Expr(expr),
- },
- UnionType(kts) => {
- Ret::NirKind(UnionConstructor(field.clone(), kts.clone()))
- }
- PartialExpr(ExprKind::Projection(x, _)) => {
- return normalize_one_layer(
- ExprKind::Field(x.clone(), field.clone()),
- env,
- )
- }
- PartialExpr(ExprKind::BinOp(
- BinOp::RightBiasedRecordMerge,
- x,
- y,
- )) => match (x.kind(), y.kind()) {
- (_, RecordLit(kvs)) => match kvs.get(field) {
- Some(r) => Ret::Nir(r.clone()),
- None => {
- return normalize_one_layer(
- ExprKind::Field(x.clone(), field.clone()),
- env,
- )
- }
- },
- (RecordLit(kvs), _) => match kvs.get(field) {
- Some(r) => Ret::Expr(ExprKind::Field(
- Nir::from_kind(PartialExpr(ExprKind::BinOp(
- BinOp::RightBiasedRecordMerge,
- Nir::from_kind(RecordLit(
- Some((field.clone(), r.clone()))
- .into_iter()
- .collect(),
- )),
- y.clone(),
- ))),
- field.clone(),
- )),
- None => {
- return normalize_one_layer(
- ExprKind::Field(y.clone(), field.clone()),
- env,
- )
- }
- },
- _ => Ret::Expr(expr),
- },
- PartialExpr(ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y)) => {
- match (x.kind(), y.kind()) {
- (RecordLit(kvs), _) => match kvs.get(field) {
- Some(r) => Ret::Expr(ExprKind::Field(
- Nir::from_kind(PartialExpr(ExprKind::BinOp(
- BinOp::RecursiveRecordMerge,
- Nir::from_kind(RecordLit(
- Some((field.clone(), r.clone()))
- .into_iter()
- .collect(),
- )),
- y.clone(),
- ))),
- field.clone(),
- )),
- None => {
- return normalize_one_layer(
- ExprKind::Field(y.clone(), field.clone()),
- env,
- )
- }
- },
- (_, RecordLit(kvs)) => match kvs.get(field) {
- Some(r) => Ret::Expr(ExprKind::Field(
- Nir::from_kind(PartialExpr(ExprKind::BinOp(
- BinOp::RecursiveRecordMerge,
- x.clone(),
- Nir::from_kind(RecordLit(
- Some((field.clone(), r.clone()))
- .into_iter()
- .collect(),
- )),
- ))),
- field.clone(),
- )),
- None => {
- return normalize_one_layer(
- ExprKind::Field(x.clone(), field.clone()),
- env,
- )
- }
- },
- _ => Ret::Expr(expr),
- }
- }
- _ => Ret::Expr(expr),
- },
- ExprKind::Projection(_, ref ls) if ls.is_empty() => {
- Ret::NirKind(RecordLit(HashMap::new()))
+ ret_kind(UnionType(kvs.into_iter().collect()))
}
- ExprKind::Projection(ref v, ref ls) => match v.kind() {
- RecordLit(kvs) => Ret::NirKind(RecordLit(
- ls.iter()
- .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
- .collect(),
- )),
- PartialExpr(ExprKind::Projection(v2, _)) => {
- return normalize_one_layer(
- ExprKind::Projection(v2.clone(), ls.clone()),
- env,
- )
- }
- _ => Ret::Expr(expr),
- },
- ExprKind::ProjectionByExpr(ref v, ref t) => match t.kind() {
- RecordType(kts) => {
- return normalize_one_layer(
- ExprKind::Projection(
- v.clone(),
- kts.keys().cloned().collect(),
- ),
- env,
- )
- }
- _ => Ret::Expr(expr),
- },
-
- ExprKind::Merge(ref handlers, ref variant, _) => {
- match handlers.kind() {
- RecordLit(kvs) => match variant.kind() {
- 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::Nir(h.app(v.clone())),
- None => Ret::Expr(expr),
- },
- EmptyOptionalLit(_) => match kvs.get(&"None".into()) {
- Some(h) => Ret::Nir(h.clone()),
- None => Ret::Expr(expr),
- },
- NEOptionalLit(v) => match kvs.get(&"Some".into()) {
- Some(h) => Ret::Nir(h.app(v.clone())),
- None => Ret::Expr(expr),
- },
- _ => Ret::Expr(expr),
- },
- _ => Ret::Expr(expr),
- }
+ ExprKind::Op(ref op) => normalize_operation(op),
+ ExprKind::Annot(x, _) => ret_nir(x),
+ ExprKind::Assert(x) => ret_kind(Assert(x)),
+ ExprKind::Import(..) => {
+ unreachable!("This case should have been handled in resolution")
}
- ExprKind::ToMap(ref v, ref annot) => match v.kind() {
- RecordLit(kvs) if kvs.is_empty() => {
- match annot.as_ref().map(|v| v.kind()) {
- Some(NirKind::ListType(t)) => {
- Ret::NirKind(EmptyListLit(t.clone()))
- }
- _ => Ret::Expr(expr),
- }
- }
- RecordLit(kvs) => Ret::NirKind(NEListLit(
- kvs.iter()
- .sorted_by_key(|(k, _)| *k)
- .map(|(k, v)| {
- let mut rec = HashMap::new();
- rec.insert("mapKey".into(), Nir::from_text(k));
- rec.insert("mapValue".into(), v.clone());
- Nir::from_kind(NirKind::RecordLit(rec))
- })
- .collect(),
- )),
- _ => Ret::Expr(expr),
- },
- };
-
- match ret {
- 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 fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
+pub fn normalize_hir(env: &NzEnv, hir: &Hir) -> NirKind {
match hir.kind() {
HirKind::Var(var) => env.lookup_val(*var),
- HirKind::Import(hir, _) => normalize_hir_whnf(env, hir),
+ HirKind::Import(hir, _) => normalize_hir(env, hir),
HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
let annot = annot.eval(env);
NirKind::LamClosure {
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-09 07:42:24 +0000