diff options
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r-- | dhall/src/semantics/nze/env.rs | 6 | ||||
-rw-r--r-- | dhall/src/semantics/nze/mod.rs | 8 | ||||
-rw-r--r-- | dhall/src/semantics/nze/nir.rs | 140 | ||||
-rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 100 | ||||
-rw-r--r-- | dhall/src/semantics/nze/var.rs | 4 |
5 files changed, 94 insertions, 164 deletions
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs index ef2bee6..ec99dbe 100644 --- a/dhall/src/semantics/nze/env.rs +++ b/dhall/src/semantics/nze/env.rs @@ -1,7 +1,7 @@ use crate::semantics::{AlphaVar, Nir, NirKind}; #[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub(crate) enum NzVar { +pub enum NzVar { /// Reverse-debruijn index: counts number of binders from the bottom of the stack. Bound(usize), /// Fake fresh variable generated for expression equality checking. @@ -17,11 +17,11 @@ enum EnvItem<Type> { } #[derive(Debug, Clone)] -pub(crate) struct ValEnv<Type> { +pub struct ValEnv<Type> { items: Vec<EnvItem<Type>>, } -pub(crate) type NzEnv = ValEnv<()>; +pub type NzEnv = ValEnv<()>; impl NzVar { pub fn new(idx: usize) -> Self { diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs index 2648339..23022e0 100644 --- a/dhall/src/semantics/nze/mod.rs +++ b/dhall/src/semantics/nze/mod.rs @@ -3,7 +3,7 @@ pub mod lazy; pub mod nir; pub mod normalize; pub mod var; -pub(crate) use env::*; -pub(crate) use nir::*; -pub(crate) use normalize::*; -pub(crate) use var::*; +pub use env::*; +pub use nir::*; +pub use normalize::*; +pub use var::*; diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs index 32ef590..e0d227e 100644 --- a/dhall/src/semantics/nze/nir.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -7,10 +7,10 @@ use crate::semantics::{ BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv, }; use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind, - Span, + BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, + NumKind, Span, }; -use crate::{NormalizedExpr, ToExprOptions}; +use crate::ToExprOptions; /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation /// automatically. Uses a Rc<RefCell> to share computation. @@ -19,7 +19,7 @@ use crate::{NormalizedExpr, ToExprOptions}; /// normalize as needed. /// Stands for "Normalized intermediate representation" #[derive(Clone)] -pub(crate) struct Nir(Rc<NirInternal>); +pub struct Nir(Rc<NirInternal>); #[derive(Debug)] struct NirInternal { @@ -28,7 +28,7 @@ struct NirInternal { /// An unevaluated subexpression #[derive(Debug, Clone)] -pub(crate) enum Thunk { +pub enum Thunk { /// A completely unnormalized expression. Thunk { env: NzEnv, body: Hir }, /// A partially normalized expression that may need to go through `normalize_one_layer`. @@ -37,7 +37,7 @@ pub(crate) enum Thunk { /// An unevaluated subexpression that takes an argument. #[derive(Debug, Clone)] -pub(crate) enum Closure { +pub enum Closure { /// Normal closure Closure { env: NzEnv, body: Hir }, /// Closure that ignores the argument passed @@ -48,7 +48,7 @@ pub(crate) enum Closure { // Invariant: this must not contain interpolations that are themselves TextLits, and contiguous // text values must be merged. #[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) struct TextLit(Vec<InterpolatedTextContents<Nir>>); +pub struct TextLit(Vec<InterpolatedTextContents<Nir>>); /// This represents a value in Weak Head Normal Form (WHNF). This means that the value is /// normalized up to the first constructor, but subexpressions may not be fully normalized. @@ -58,7 +58,7 @@ pub(crate) struct TextLit(Vec<InterpolatedTextContents<Nir>>); /// In particular, this means that once we get a `NirKind`, it can be considered immutable, and /// we only need to recursively normalize its sub-`Nir`s to get to the NF. #[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum NirKind { +pub enum NirKind { /// Closures LamClosure { binder: Binder, @@ -70,13 +70,17 @@ pub(crate) enum NirKind { annot: Nir, closure: Closure, }, - AppliedBuiltin(BuiltinClosure<Nir>), + AppliedBuiltin(BuiltinClosure), Var(NzVar), Const(Const), - Lit(LitKind), + // Must be a number type, Bool or Text + BuiltinType(Builtin), + Num(NumKind), + OptionalType(Nir), EmptyOptionalLit(Nir), NEOptionalLit(Nir), + ListType(Nir), // EmptyListLit(t) means `[] : List t`, not `[] : t` EmptyListLit(Nir), NEListLit(Vec<Nir>), @@ -93,34 +97,34 @@ pub(crate) enum NirKind { impl Nir { /// Construct a Nir from a completely unnormalized expression. - pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Nir { + pub fn new_thunk(env: NzEnv, hir: Hir) -> Nir { NirInternal::from_thunk(Thunk::new(env, hir)).into_nir() } /// Construct a Nir from a partially normalized expression that's not in WHNF. - pub(crate) fn from_partial_expr(e: ExprKind<Nir>) -> Nir { + pub fn from_partial_expr(e: ExprKind<Nir>) -> Nir { // TODO: env let env = NzEnv::new(); NirInternal::from_thunk(Thunk::from_partial_expr(env, e)).into_nir() } /// Make a Nir from a NirKind - pub(crate) fn from_kind(v: NirKind) -> Nir { + pub fn from_kind(v: NirKind) -> Nir { NirInternal::from_whnf(v).into_nir() } - pub(crate) fn from_const(c: Const) -> Self { + pub fn from_const(c: Const) -> Self { let v = NirKind::Const(c); NirInternal::from_whnf(v).into_nir() } - pub(crate) fn from_builtin(b: Builtin) -> Self { + pub fn from_builtin(b: Builtin) -> Self { Self::from_builtin_env(b, &NzEnv::new()) } - pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self { + pub fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self { Nir::from_kind(NirKind::from_builtin_env(b, env.clone())) } - pub(crate) fn from_text(txt: impl ToString) -> Self { + pub fn from_text(txt: impl ToString) -> Self { Nir::from_kind(NirKind::TextLit(TextLit::from_text(txt.to_string()))) } - pub(crate) fn as_const(&self) -> Option<Const> { + pub fn as_const(&self) -> Option<Const> { match &*self.kind() { NirKind::Const(c) => Some(*c), _ => None, @@ -128,26 +132,22 @@ impl Nir { } /// This is what you want if you want to pattern-match on the value. - pub(crate) fn kind(&self) -> &NirKind { + pub fn kind(&self) -> &NirKind { self.0.kind() } - pub(crate) fn to_type(&self, u: impl Into<Universe>) -> Type { + pub fn to_type(&self, u: impl Into<Universe>) -> Type { Type::new(self.clone(), u.into()) } /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { + pub fn to_expr(&self, opts: ToExprOptions) -> Expr { self.to_hir_noenv().to_expr(opts) } - pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr { + pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr { self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv) } - pub(crate) fn normalize(&self) { - self.0.normalize() - } - - pub(crate) fn app(&self, v: Nir) -> Nir { + pub fn app(&self, v: Nir) -> Nir { Nir::from_kind(apply_any(self.clone(), v)) } @@ -188,12 +188,21 @@ impl Nir { closure.to_hir(venv), ), NirKind::Const(c) => ExprKind::Const(*c), - NirKind::Lit(l) => ExprKind::Lit(l.clone()), + NirKind::BuiltinType(b) => ExprKind::Builtin(*b), + NirKind::Num(l) => ExprKind::Num(l.clone()), + NirKind::OptionalType(t) => ExprKind::App( + Nir::from_builtin(Builtin::Optional).to_hir(venv), + t.to_hir(venv), + ), NirKind::EmptyOptionalLit(n) => ExprKind::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( + Nir::from_builtin(Builtin::List).to_hir(venv), + t.to_hir(venv), + ), NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new( HirKind::Expr(ExprKind::App( Nir::from_builtin(Builtin::List).to_hir(venv), @@ -274,75 +283,18 @@ impl NirInternal { fn kind(&self) -> &NirKind { &self.kind } - fn normalize(&self) { - self.kind().normalize(); - } } impl NirKind { - pub(crate) fn into_nir(self) -> Nir { + pub fn into_nir(self) -> Nir { Nir::from_kind(self) } - pub(crate) fn normalize(&self) { - match self { - NirKind::Var(..) | NirKind::Const(_) | NirKind::Lit(_) => {} - - NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => { - tth.normalize(); - } - - NirKind::NEOptionalLit(th) => { - th.normalize(); - } - NirKind::LamClosure { annot, closure, .. } - | NirKind::PiClosure { annot, closure, .. } => { - annot.normalize(); - closure.normalize(); - } - NirKind::AppliedBuiltin(closure) => closure.normalize(), - NirKind::NEListLit(elts) => { - for x in elts.iter() { - x.normalize(); - } - } - NirKind::RecordLit(kvs) => { - for x in kvs.values() { - x.normalize(); - } - } - NirKind::RecordType(kvs) => { - for x in kvs.values() { - x.normalize(); - } - } - NirKind::UnionType(kts) | NirKind::UnionConstructor(_, kts) => { - for x in kts.values().flatten() { - x.normalize(); - } - } - NirKind::UnionLit(_, v, kts) => { - v.normalize(); - for x in kts.values().flatten() { - x.normalize(); - } - } - NirKind::TextLit(tlit) => tlit.normalize(), - NirKind::Equivalence(x, y) => { - x.normalize(); - y.normalize(); - } - NirKind::PartialExpr(e) => { - e.map_ref(Nir::normalize); - } - } - } - - pub(crate) fn from_builtin(b: Builtin) -> NirKind { + pub fn from_builtin(b: Builtin) -> NirKind { NirKind::from_builtin_env(b, NzEnv::new()) } - pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind { - NirKind::AppliedBuiltin(BuiltinClosure::new(b, env)) + pub fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind { + BuiltinClosure::new(b, env) } } @@ -390,9 +342,6 @@ impl Closure { } } - // TODO: somehow normalize the body. Might require to pass an env. - pub fn normalize(&self) {} - /// Convert this closure to a Hir expression pub fn to_hir(&self, venv: VarEnv) -> Hir { self.apply_var(NzVar::new(venv.size())) @@ -456,13 +405,6 @@ impl TextLit { pub fn iter(&self) -> impl Iterator<Item = &InterpolatedTextContents<Nir>> { self.0.iter() } - /// Normalize the contained values. This does not break the invariant because we have already - /// ensured that no contained values normalize to a TextLit. - pub fn normalize(&self) { - for x in self.0.iter() { - x.map_ref(Nir::normalize); - } - } } impl lazy::Eval<NirKind> for Thunk { diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 79d55e8..570e106 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -2,14 +2,10 @@ use itertools::Itertools; use std::collections::HashMap; use crate::semantics::NzEnv; -use crate::semantics::{ - Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit, -}; -use crate::syntax::{ - BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind, -}; +use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit}; +use crate::syntax::{BinOp, ExprKind, InterpolatedTextContents, NumKind}; -pub(crate) 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), @@ -20,7 +16,7 @@ pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind { } } -pub(crate) fn squash_textlit( +pub fn squash_textlit( elts: impl Iterator<Item = InterpolatedTextContents<Nir>>, ) -> Vec<InterpolatedTextContents<Nir>> { use std::mem::replace; @@ -58,7 +54,7 @@ pub(crate) fn squash_textlit( ret } -pub(crate) fn merge_maps<K, V, F>( +pub fn merge_maps<K, V, F>( map1: &HashMap<K, V>, map2: &HashMap<K, V>, mut f: F, @@ -99,40 +95,40 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> { NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge, TextAppend, }; - use LitKind::{Bool, Natural}; - use NirKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType}; + use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType}; + use NumKind::{Bool, Natural}; Some(match (o, x.kind(), y.kind()) { - (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, 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, 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, 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, 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))), + (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, 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))) + (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, 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))) + (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), @@ -211,13 +207,13 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> { } #[allow(clippy::cognitive_complexity)] -pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { - use LitKind::Bool; +pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { use NirKind::{ - EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit, + EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, UnionType, }; + use NumKind::Bool; let ret = match expr { ExprKind::Import(..) | ExprKind::Completion(..) => { @@ -235,15 +231,11 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { 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::Lit(l) => Ret::NirKind(Lit(l)), + ExprKind::Num(l) => Ret::NirKind(Num(l)), ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match t.kind() { - NirKind::AppliedBuiltin(BuiltinClosure { - b: Builtin::List, - args, - .. - }) if args.len() == 1 => args[0].clone(), + NirKind::ListType(t) => t.clone(), _ => panic!("internal type error"), }; Ret::NirKind(NirKind::EmptyListLit(arg)) @@ -271,12 +263,12 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { } ExprKind::BoolIf(ref b, ref e1, ref e2) => { match b.kind() { - Lit(Bool(true)) => Ret::NirRef(e1), - Lit(Bool(false)) => Ret::NirRef(e2), + Num(Bool(true)) => Ret::NirRef(e1), + Num(Bool(false)) => Ret::NirRef(e2), _ => { match (e1.kind(), e2.kind()) { // Simplify `if b then True else False` - (Lit(Bool(true)), Lit(Bool(false))) => Ret::NirRef(b), + (Num(Bool(true)), Num(Bool(false))) => Ret::NirRef(b), _ if e1 == e2 => Ret::NirRef(e1), _ => Ret::Expr(expr), } @@ -442,12 +434,8 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { 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::AppliedBuiltin(BuiltinClosure { - b: Builtin::List, - args, - .. - })) if args.len() == 1 => { - Ret::NirKind(EmptyListLit(args[0].clone())) + Some(NirKind::ListType(t)) => { + Ret::NirKind(EmptyListLit(t.clone())) } _ => Ret::Expr(expr), } @@ -476,7 +464,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind { } /// Normalize Hir into WHNF -pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind { +pub 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), diff --git a/dhall/src/semantics/nze/var.rs b/dhall/src/semantics/nze/var.rs index 413c759..302dbb7 100644 --- a/dhall/src/semantics/nze/var.rs +++ b/dhall/src/semantics/nze/var.rs @@ -8,10 +8,10 @@ pub struct Binder { } impl Binder { - pub(crate) fn new(name: Label) -> Self { + pub fn new(name: Label) -> Self { Binder { name } } - pub(crate) fn to_label(&self) -> Label { + pub fn to_label(&self) -> Label { self.clone().into() } } |