From 08e1d8ece4314b56d64fa08595c2e043b97896d1 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 17:19:31 +0100 Subject: Split off operations from main expr enum --- dhall/src/semantics/nze/nir.rs | 46 ++++++++++++++++++++++-------------------- 1 file changed, 24 insertions(+), 22 deletions(-) (limited to 'dhall/src/semantics/nze/nir.rs') diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index e0d227e..73c3f30 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -8,7 +8,7 @@ use crate::semantics::{ }; use crate::syntax::{ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, - NumKind, Span, + NumKind, OpKind, Span, }; use crate::ToExprOptions; @@ -190,24 +190,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,31 +229,33 @@ 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)), }), }; -- cgit v1.2.3 From 7efdbd11db0f54f065d4dc41f0cab4b158d4515c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 18:33:58 +0100 Subject: Factor our operations in normalization --- dhall/src/semantics/nze/nir.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/nze/nir.rs') diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index 73c3f30..2b7a819 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -3,7 +3,7 @@ use std::rc::Rc; use crate::semantics::nze::lazy; use crate::semantics::{ - apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder, + apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder, BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv, }; use crate::syntax::{ @@ -309,7 +309,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), } } -- cgit v1.2.3 From 28c36acc8af1e3ece9512c98aa9fd70fedf1b252 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 18:47:17 +0100 Subject: Avoid a few allocations --- dhall/src/semantics/nze/nir.rs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics/nze/nir.rs') diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index 2b7a819..0dff105 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -111,8 +111,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 +147,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 { -- cgit v1.2.3 From cd3b11cc8bd7c4397071d1d3b4b9020b7d5ff2ad Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 21:33:45 +0100 Subject: Only need to store OpKind in Nir --- dhall/src/semantics/nze/nir.rs | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) (limited to 'dhall/src/semantics/nze/nir.rs') diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index 0dff105..88123d8 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -74,25 +74,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), - RecordType(HashMap), + ListType(Nir), RecordLit(HashMap), - UnionType(HashMap>), + RecordType(HashMap), UnionConstructor(Label, HashMap>), UnionLit(Label, Nir, HashMap>), - TextLit(TextLit), + UnionType(HashMap>), Equivalence(Nir, Nir), - /// Invariant: evaluation must not be able to progress with `normalize_one_layer`. - PartialExpr(ExprKind), + 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), } impl Nir { @@ -258,7 +260,8 @@ impl Nir { 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))), }), }; -- cgit v1.2.3 From fff4c46e09d4edf25eba737f4d71bfdb1dbf4a82 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 22:11:54 +0100 Subject: Extract operation-related code to a new module --- dhall/src/semantics/nze/nir.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/nze/nir.rs') diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index 88123d8..5c67c02 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -1,6 +1,7 @@ use std::collections::HashMap; use std::rc::Rc; +use crate::operations::OpKind; use crate::semantics::nze::lazy; use crate::semantics::{ apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder, @@ -8,7 +9,7 @@ use crate::semantics::{ }; use crate::syntax::{ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, - NumKind, OpKind, Span, + NumKind, Span, }; use crate::ToExprOptions; -- cgit v1.2.3 From 2cf9169e1a21e1196e0265847abcfa904e2d45a3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 22:13:36 +0100 Subject: Move builtins module up a level --- dhall/src/semantics/nze/nir.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/nze/nir.rs') diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index 5c67c02..e2a0113 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -1,11 +1,12 @@ use std::collections::HashMap; use std::rc::Rc; +use crate::builtins::BuiltinClosure; use crate::operations::OpKind; use crate::semantics::nze::lazy; use crate::semantics::{ - apply_any, normalize_hir, 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, -- cgit v1.2.3 From 56efd2ac39149d8652bd625fbf0679c10823b137 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 22:24:15 +0100 Subject: Move BinOp and Builtin definitions in the relevant module --- dhall/src/semantics/nze/nir.rs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/nze/nir.rs') diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index e2a0113..12f1b14 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -1,16 +1,15 @@ use std::collections::HashMap; use std::rc::Rc; -use crate::builtins::BuiltinClosure; -use crate::operations::OpKind; +use crate::builtins::{Builtin, BuiltinClosure}; +use crate::operations::{BinOp, OpKind}; use crate::semantics::nze::lazy; use crate::semantics::{ 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; -- cgit v1.2.3