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/builtins.rs | 28 ++--- dhall/src/semantics/nze/nir.rs | 46 +++++---- dhall/src/semantics/nze/normalize.rs | 182 +++++++++++++++++++-------------- dhall/src/semantics/resolve/resolve.rs | 21 ++-- dhall/src/semantics/tck/typecheck.rs | 35 ++++--- 5 files changed, 171 insertions(+), 141 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 6007a92..45be448 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -5,8 +5,8 @@ use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; use crate::syntax::{ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText, - InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr, - V, + InterpolatedTextContents, Label, NaiveDouble, NumKind, OpKind, Span, + UnspannedExpr, V, }; use std::collections::HashMap; use std::convert::TryInto; @@ -34,10 +34,10 @@ impl BuiltinClosure { HirKind::Expr(self.args.iter().fold( ExprKind::Builtin(self.b), |acc, v| { - ExprKind::App( + ExprKind::Op(OpKind::App( Hir::new(HirKind::Expr(acc), Span::Artificial), v.to_hir(venv), - ) + )) }, )) } @@ -59,16 +59,16 @@ macro_rules! make_type { rc(ExprKind::Var(V(stringify!($var).into(), 0))) }; (Optional $ty:ident) => { - rc(ExprKind::App( + rc(ExprKind::Op(OpKind::App( rc(ExprKind::Builtin(Builtin::Optional)), make_type!($ty) - )) + ))) }; (List $($rest:tt)*) => { - rc(ExprKind::App( + rc(ExprKind::Op(OpKind::App( rc(ExprKind::Builtin(Builtin::List)), make_type!($($rest)*) - )) + ))) }; ({ $($label:ident : $ty:ident),* }) => {{ let mut kts = DupTreeMap::new(); @@ -214,10 +214,10 @@ macro_rules! make_closure { }; (List $($ty:tt)*) => {{ let ty = make_closure!($($ty)*); - rc(ExprKind::App( + rc(ExprKind::Op(OpKind::App( rc(ExprKind::Builtin(Builtin::List)), ty - )) + ))) }}; (Some($($v:tt)*)) => { rc(ExprKind::SomeLit( @@ -225,20 +225,20 @@ macro_rules! make_closure { )) }; (1 + $($v:tt)*) => { - rc(ExprKind::BinOp( + rc(ExprKind::Op(OpKind::BinOp( BinOp::NaturalPlus, make_closure!($($v)*), rc(ExprKind::Num(NumKind::Natural(1))) - )) + ))) }; ([ $($head:tt)* ] # $($tail:tt)*) => {{ let head = make_closure!($($head)*); let tail = make_closure!($($tail)*); - rc(ExprKind::BinOp( + rc(ExprKind::Op(OpKind::BinOp( BinOp::ListAppend, rc(ExprKind::NEListLit(vec![head])), tail, - )) + ))) }}; } 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)), }), }; diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 570e106..ebf4ae1 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -3,7 +3,9 @@ use std::collections::HashMap; use crate::semantics::NzEnv; use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit}; -use crate::syntax::{BinOp, ExprKind, InterpolatedTextContents, NumKind}; +use crate::syntax::{ + BinOp, ExprKind, InterpolatedTextContents, NumKind, OpKind, +}; pub fn apply_any(f: Nir, a: Nir) -> NirKind { match f.kind() { @@ -12,7 +14,7 @@ pub fn apply_any(f: Nir, a: Nir) -> NirKind { NirKind::UnionConstructor(l, kts) => { NirKind::UnionLit(l.clone(), a, kts.clone()) } - _ => NirKind::PartialExpr(ExprKind::App(f, a)), + _ => NirKind::PartialExpr(ExprKind::Op(OpKind::App(f, a))), } } @@ -173,11 +175,11 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| { - Nir::from_partial_expr(ExprKind::BinOp( + Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), - )) + ))) }); Ret::NirKind(RecordLit(kvs)) } @@ -188,11 +190,11 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { 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( + Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp( RecursiveRecordTypeMerge, l.clone(), r.clone(), - )) + ))) }, ); Ret::NirKind(RecordType(kts)) @@ -216,7 +218,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { use NumKind::Bool; let ret = match expr { - ExprKind::Import(..) | ExprKind::Completion(..) => { + ExprKind::Import(..) | ExprKind::Op(OpKind::Completion(..)) => { unreachable!("This case should have been handled in resolution") } ExprKind::Var(..) @@ -230,7 +232,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { 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::Op(OpKind::App(v, a)) => Ret::Nir(v.app(a)), ExprKind::Num(l) => Ret::NirKind(Num(l)), ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { @@ -261,7 +263,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { Ret::NirKind(NirKind::TextLit(tlit)) } } - ExprKind::BoolIf(ref b, ref e1, ref e2) => { + ExprKind::Op(OpKind::BoolIf(ref b, ref e1, ref e2)) => { match b.kind() { Num(Bool(true)) => Ret::NirRef(e1), Num(Bool(false)) => Ret::NirRef(e2), @@ -275,12 +277,14 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { } } } - ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) { - Some(ret) => ret, - None => Ret::Expr(expr), - }, + ExprKind::Op(OpKind::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() { + ExprKind::Op(OpKind::Field(ref v, ref field)) => match v.kind() { RecordLit(kvs) => match kvs.get(field) { Some(r) => Ret::Nir(r.clone()), None => Ret::Expr(expr), @@ -288,53 +292,65 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { UnionType(kts) => { Ret::NirKind(UnionConstructor(field.clone(), kts.clone())) } - PartialExpr(ExprKind::Projection(x, _)) => { + PartialExpr(ExprKind::Op(OpKind::Projection(x, _))) => { return normalize_one_layer( - ExprKind::Field(x.clone(), field.clone()), + ExprKind::Op(OpKind::Field(x.clone(), field.clone())), env, ) } - PartialExpr(ExprKind::BinOp( + PartialExpr(ExprKind::Op(OpKind::BinOp( BinOp::RightBiasedRecordMerge, x, y, - )) => match (x.kind(), y.kind()) { + ))) => 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()), + ExprKind::Op(OpKind::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(), + Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( + Nir::from_kind(PartialExpr(ExprKind::Op( + OpKind::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()), + ExprKind::Op(OpKind::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( + PartialExpr(ExprKind::Op(OpKind::BinOp( + BinOp::RecursiveRecordMerge, + x, + y, + ))) => match (x.kind(), y.kind()) { + (RecordLit(kvs), _) => match kvs.get(field) { + Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( + Nir::from_kind(PartialExpr(ExprKind::Op( + OpKind::BinOp( BinOp::RecursiveRecordMerge, Nir::from_kind(RecordLit( Some((field.clone(), r.clone())) @@ -342,19 +358,24 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { .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( + ), + ))), + field.clone(), + ))), + None => { + return normalize_one_layer( + ExprKind::Op(OpKind::Field( + y.clone(), + field.clone(), + )), + env, + ) + } + }, + (_, RecordLit(kvs)) => match kvs.get(field) { + Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( + Nir::from_kind(PartialExpr(ExprKind::Op( + OpKind::BinOp( BinOp::RecursiveRecordMerge, x.clone(), Nir::from_kind(RecordLit( @@ -362,52 +383,57 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { .into_iter() .collect(), )), - ))), - field.clone(), - )), - None => { - return normalize_one_layer( - ExprKind::Field(x.clone(), field.clone()), - env, - ) - } - }, - _ => Ret::Expr(expr), - } - } + ), + ))), + field.clone(), + ))), + None => { + return normalize_one_layer( + ExprKind::Op(OpKind::Field( + x.clone(), + field.clone(), + )), + env, + ) + } + }, + _ => Ret::Expr(expr), + }, _ => Ret::Expr(expr), }, - ExprKind::Projection(_, ref ls) if ls.is_empty() => { + ExprKind::Op(OpKind::Projection(_, ref ls)) if ls.is_empty() => { Ret::NirKind(RecordLit(HashMap::new())) } - ExprKind::Projection(ref v, ref ls) => match v.kind() { + ExprKind::Op(OpKind::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, _)) => { + PartialExpr(ExprKind::Op(OpKind::Projection(v2, _))) => { return normalize_one_layer( - ExprKind::Projection(v2.clone(), ls.clone()), + ExprKind::Op(OpKind::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, - ) + ExprKind::Op(OpKind::ProjectionByExpr(ref v, ref t)) => { + match t.kind() { + RecordType(kts) => { + return normalize_one_layer( + ExprKind::Op(OpKind::Projection( + v.clone(), + kts.keys().cloned().collect(), + )), + env, + ) + } + _ => Ret::Expr(expr), } - _ => Ret::Expr(expr), - }, + } - ExprKind::Merge(ref handlers, ref variant, _) => { + ExprKind::Op(OpKind::Merge(ref handlers, ref variant, _)) => { match handlers.kind() { RecordLit(kvs) => match variant.kind() { UnionConstructor(l, _) => match kvs.get(l) { @@ -431,7 +457,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { _ => Ret::Expr(expr), } } - ExprKind::ToMap(ref v, ref annot) => match v.kind() { + ExprKind::Op(OpKind::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)) => { diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index 6e50fa6..3e0022f 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -11,7 +11,7 @@ use crate::syntax; use crate::syntax::map::DupTreeMap; use crate::syntax::{ BinOp, Builtin, Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, - ImportTarget, Span, UnspannedExpr, URL, + ImportTarget, OpKind, Span, UnspannedExpr, URL, }; use crate::{Parsed, Resolved}; @@ -179,12 +179,13 @@ impl ImportLocation { }; let asloc_ty = make_aslocation_uniontype(); - let expr = mkexpr(ExprKind::Field(asloc_ty, field_name.into())); + let expr = + mkexpr(ExprKind::Op(OpKind::Field(asloc_ty, field_name.into()))); match arg { - Some(arg) => mkexpr(ExprKind::App( + Some(arg) => mkexpr(ExprKind::Op(OpKind::App( expr, mkexpr(ExprKind::TextLit(arg.into())), - )), + ))), None => expr, } } @@ -261,21 +262,21 @@ fn resolve_one_import( /// Desugar the first level of the expression. fn desugar(expr: &Expr) -> Cow<'_, Expr> { match expr.kind() { - ExprKind::Completion(ty, compl) => { + ExprKind::Op(OpKind::Completion(ty, compl)) => { let ty_field_default = Expr::new( - ExprKind::Field(ty.clone(), "default".into()), + ExprKind::Op(OpKind::Field(ty.clone(), "default".into())), expr.span(), ); let merged = Expr::new( - ExprKind::BinOp( + ExprKind::Op(OpKind::BinOp( BinOp::RightBiasedRecordMerge, ty_field_default, compl.clone(), - ), + )), expr.span(), ); let ty_field_type = Expr::new( - ExprKind::Field(ty.clone(), "Type".into()), + ExprKind::Op(OpKind::Field(ty.clone(), "Type".into())), expr.span(), ); Cow::Owned(Expr::new( @@ -304,7 +305,7 @@ fn traverse_resolve_expr( .format(), )?, }, - ExprKind::BinOp(BinOp::ImportAlt, l, r) => { + ExprKind::Op(OpKind::BinOp(BinOp::ImportAlt, l, r)) => { match traverse_resolve_expr(name_env, l, f) { Ok(l) => l, Err(_) => { diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index c3334b5..8f3fcb2 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -9,7 +9,8 @@ use crate::semantics::{ Type, }; use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span, + BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, OpKind, + Span, }; fn check_rectymerge( @@ -75,7 +76,7 @@ fn type_one_layer( let span_err = |msg: &str| mk_span_err(span.clone(), msg); let ty = match &ekind { - ExprKind::Import(..) | ExprKind::Completion(..) => { + ExprKind::Import(..) | ExprKind::Op(OpKind::Completion(..)) => { unreachable!("This case should have been handled in resolution") } ExprKind::Var(..) @@ -222,7 +223,7 @@ fn type_one_layer( Type::from_const(k) } - ExprKind::Field(scrut, x) => { + ExprKind::Op(OpKind::Field(scrut, x)) => { match scrut.ty().kind() { NirKind::RecordType(kts) => match kts.get(&x) { Some(val) => Type::new_infer_universe(env, val.clone())?, @@ -261,7 +262,7 @@ fn type_one_layer( } t } - ExprKind::App(f, arg) => { + ExprKind::Op(OpKind::App(f, arg)) => { match f.ty().kind() { // TODO: store Type in closure NirKind::PiClosure { annot, closure, .. } => { @@ -309,7 +310,7 @@ fn type_one_layer( ), } } - ExprKind::BoolIf(x, y, z) => { + ExprKind::Op(OpKind::BoolIf(x, y, z)) => { if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } @@ -322,7 +323,7 @@ fn type_one_layer( y.ty().clone() } - ExprKind::BinOp(BinOp::RightBiasedRecordMerge, x, y) => { + ExprKind::Op(OpKind::BinOp(BinOp::RightBiasedRecordMerge, x, y)) => { let x_type = x.ty(); let y_type = y.ty(); @@ -344,22 +345,22 @@ fn type_one_layer( let u = max(x.ty().ty(), y.ty().ty()); Nir::from_kind(NirKind::RecordType(kts)).to_type(u) } - ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { + ExprKind::Op(OpKind::BinOp(BinOp::RecursiveRecordMerge, x, y)) => { check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?; let hir = Hir::new( - HirKind::Expr(ExprKind::BinOp( + HirKind::Expr(ExprKind::Op(OpKind::BinOp( BinOp::RecursiveRecordTypeMerge, x.ty().to_hir(env.as_varenv()), y.ty().to_hir(env.as_varenv()), - )), + ))), span.clone(), ); let x_u = x.ty().ty(); let y_u = y.ty().ty(); Type::new(hir.eval(env), max(x_u, y_u)) } - ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => { + ExprKind::Op(OpKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y)) => { check_rectymerge(&span, env, x.eval(env), y.eval(env))?; // A RecordType's type is always a const @@ -367,7 +368,7 @@ fn type_one_layer( let yk = y.ty().as_const().unwrap(); Type::from_const(max(xk, yk)) } - ExprKind::BinOp(BinOp::ListAppend, l, r) => { + ExprKind::Op(OpKind::BinOp(BinOp::ListAppend, l, r)) => { match l.ty().kind() { NirKind::ListType(..) => {} _ => return span_err("BinOpTypeMismatch"), @@ -379,7 +380,7 @@ fn type_one_layer( l.ty().clone() } - ExprKind::BinOp(BinOp::Equivalence, l, r) => { + ExprKind::Op(OpKind::BinOp(BinOp::Equivalence, l, r)) => { if l.ty() != r.ty() { return span_err("EquivalenceTypeMismatch"); } @@ -389,7 +390,7 @@ fn type_one_layer( Type::from_const(Const::Type) } - ExprKind::BinOp(o, l, r) => { + ExprKind::Op(OpKind::BinOp(o, l, r)) => { let t = Type::from_builtin(match o { BinOp::BoolAnd | BinOp::BoolOr @@ -415,7 +416,7 @@ fn type_one_layer( t } - ExprKind::Merge(record, union, type_annot) => { + ExprKind::Op(OpKind::Merge(record, union, type_annot)) => { let record_type = record.ty(); let handlers = match record_type.kind() { NirKind::RecordType(kts) => kts, @@ -554,7 +555,7 @@ fn type_one_layer( (None, None) => return span_err("MergeEmptyNeedsAnnotation"), } } - ExprKind::ToMap(record, annot) => { + ExprKind::Op(OpKind::ToMap(record, annot)) => { if record.ty().ty().as_const() != Some(Const::Type) { return span_err("`toMap` only accepts records of type `Type`"); } @@ -624,7 +625,7 @@ fn type_one_layer( output_type } } - ExprKind::Projection(record, labels) => { + ExprKind::Op(OpKind::Projection(record, labels)) => { let record_type = record.ty(); let kts = match record_type.kind() { NirKind::RecordType(kts) => kts, @@ -652,7 +653,7 @@ fn type_one_layer( Nir::from_kind(NirKind::RecordType(new_kts)), )? } - ExprKind::ProjectionByExpr(record, selection) => { + ExprKind::Op(OpKind::ProjectionByExpr(record, selection)) => { let record_type = record.ty(); let rec_kts = match record_type.kind() { NirKind::RecordType(kts) => kts, -- cgit v1.2.3 From 531fdb1757a97a3accc8e836a1ff3a3977c37bfe Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 17:51:53 +0100 Subject: Factor out operations in typecheck --- dhall/src/semantics/tck/typecheck.rs | 851 ++++++++++++++++++----------------- 1 file changed, 436 insertions(+), 415 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 8f3fcb2..28d08b9 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -66,206 +66,263 @@ pub fn mk_span_err(span: Span, msg: S) -> Result { ) } -/// When all sub-expressions have been typed, check the remaining toplevel -/// layer. -fn type_one_layer( +fn type_of_binop( env: &TyEnv, - ekind: ExprKind>, span: Span, + op: BinOp, + l: &Tir<'_>, + r: &Tir<'_>, ) -> Result { let span_err = |msg: &str| mk_span_err(span.clone(), msg); + use BinOp::*; + use NirKind::{ListType, RecordType}; - let ty = match &ekind { - ExprKind::Import(..) | ExprKind::Op(OpKind::Completion(..)) => { - unreachable!("This case should have been handled in resolution") - } - ExprKind::Var(..) - | ExprKind::Const(Const::Sort) - | ExprKind::Lam(..) - | ExprKind::Pi(..) - | ExprKind::Let(..) - | ExprKind::Annot(..) => { - unreachable!("This case should have been handled in type_with") - } + Ok(match op { + RightBiasedRecordMerge => { + let x_type = l.ty(); + let y_type = r.ty(); - ExprKind::Const(Const::Type) => Type::from_const(Const::Kind), - ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort), - ExprKind::Builtin(b) => { - let t_hir = type_of_builtin(*b); - typecheck(&t_hir)?.eval_to_type(env)? - } - ExprKind::Num(NumKind::Bool(_)) => Type::from_builtin(Builtin::Bool), - ExprKind::Num(NumKind::Natural(_)) => { - Type::from_builtin(Builtin::Natural) - } - ExprKind::Num(NumKind::Integer(_)) => { - Type::from_builtin(Builtin::Integer) - } - ExprKind::Num(NumKind::Double(_)) => { - Type::from_builtin(Builtin::Double) + // Extract the LHS record type + let kts_x = match x_type.kind() { + RecordType(kts) => kts, + _ => return span_err("MustCombineRecord"), + }; + // Extract the RHS record type + let kts_y = match y_type.kind() { + RecordType(kts) => kts, + _ => return span_err("MustCombineRecord"), + }; + + // Union the two records, prefering + // the values found in the RHS. + let kts = merge_maps(kts_x, kts_y, |_, _, r_t| r_t.clone()); + + let u = max(l.ty().ty(), r.ty().ty()); + Nir::from_kind(RecordType(kts)).to_type(u) } - ExprKind::TextLit(interpolated) => { - let text_type = Type::from_builtin(Builtin::Text); - for contents in interpolated.iter() { - use InterpolatedTextContents::Expr; - if let Expr(x) = contents { - if *x.ty() != text_type { - return span_err("InvalidTextInterpolation"); - } - } - } - text_type + RecursiveRecordMerge => { + check_rectymerge(&span, env, l.ty().to_nir(), r.ty().to_nir())?; + + let hir = Hir::new( + HirKind::Expr(ExprKind::Op(OpKind::BinOp( + RecursiveRecordTypeMerge, + l.ty().to_hir(env.as_varenv()), + r.ty().to_hir(env.as_varenv()), + ))), + span.clone(), + ); + let x_u = l.ty().ty(); + let y_u = r.ty().ty(); + Type::new(hir.eval(env), max(x_u, y_u)) } - ExprKind::EmptyListLit(t) => { - let t = t.eval_to_type(env)?; - match t.kind() { - NirKind::ListType(..) => {} - _ => return span_err("InvalidListType"), - }; - t + RecursiveRecordTypeMerge => { + check_rectymerge(&span, env, l.eval(env), r.eval(env))?; + + // A RecordType's type is always a const + let xk = l.ty().as_const().unwrap(); + let yk = r.ty().as_const().unwrap(); + Type::from_const(max(xk, yk)) } - ExprKind::NEListLit(xs) => { - let mut iter = xs.iter(); - let x = iter.next().unwrap(); - for y in iter { - if x.ty() != y.ty() { - return span_err("InvalidListElement"); - } + ListAppend => { + match l.ty().kind() { + ListType(..) => {} + _ => return span_err("BinOpTypeMismatch"), } - if x.ty().ty().as_const() != Some(Const::Type) { - return span_err("InvalidListType"); + + if l.ty() != r.ty() { + return span_err("BinOpTypeMismatch"); } - let t = x.ty().to_nir(); - Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type) + l.ty().clone() } - ExprKind::SomeLit(x) => { - if x.ty().ty().as_const() != Some(Const::Type) { - return span_err("InvalidOptionalType"); + Equivalence => { + if l.ty() != r.ty() { + return span_err("EquivalenceTypeMismatch"); + } + if l.ty().ty().as_const() != Some(Const::Type) { + return span_err("EquivalenceArgumentsMustBeTerms"); } - let t = x.ty().to_nir(); - Nir::from_builtin(Builtin::Optional) - .app(t) - .to_type(Const::Type) + Type::from_const(Const::Type) } - ExprKind::RecordLit(kvs) => { - use std::collections::hash_map::Entry; - let mut kts = HashMap::new(); - // An empty record type has type Type - let mut k = Const::Type; - for (x, v) in kvs { - // Check for duplicated entries - match kts.entry(x.clone()) { - Entry::Occupied(_) => { - return span_err("RecordTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(v.ty().to_nir()), - }; + op => { + let t = Type::from_builtin(match op { + BoolAnd | BoolOr | BoolEQ | BoolNE => Builtin::Bool, + NaturalPlus | NaturalTimes => Builtin::Natural, + TextAppend => Builtin::Text, + ListAppend + | RightBiasedRecordMerge + | RecursiveRecordMerge + | RecursiveRecordTypeMerge + | Equivalence => unreachable!(), + ImportAlt => unreachable!("ImportAlt leftover in tck"), + }); - // Check that the fields have a valid kind - match v.ty().ty().as_const() { - Some(c) => k = max(k, c), - None => return span_err("InvalidFieldType"), - } + if *l.ty() != t { + return span_err("BinOpTypeMismatch"); } - Nir::from_kind(NirKind::RecordType(kts)).to_type(k) + if *r.ty() != t { + return span_err("BinOpTypeMismatch"); + } + + t } - ExprKind::RecordType(kts) => { - use std::collections::hash_map::Entry; - let mut seen_fields = HashMap::new(); - // An empty record type has type Type - let mut k = Const::Type; + }) +} - for (x, t) in kts { - // Check for duplicated entries - match seen_fields.entry(x.clone()) { - Entry::Occupied(_) => { - return span_err("RecordTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(()), - }; +fn type_of_merge( + env: &TyEnv, + span: Span, + record: &Tir<'_>, + scrut: &Tir<'_>, + type_annot: Option<&Tir<'_>>, +) -> Result { + let span_err = |msg: &str| mk_span_err(span.clone(), msg); + use NirKind::{OptionalType, PiClosure, RecordType, UnionType}; - // Check the type is a Const and compute final type - match t.ty().as_const() { - Some(c) => k = max(k, c), - None => return span_err("InvalidFieldType"), - } - } + let record_type = scrut.ty(); + let handlers = match record_type.kind() { + RecordType(kts) => kts, + _ => return span_err("Merge1ArgMustBeRecord"), + }; - Type::from_const(k) + let scrut_type = scrut.ty(); + let variants = match scrut_type.kind() { + UnionType(kts) => Cow::Borrowed(kts), + OptionalType(ty) => { + let mut kts = HashMap::new(); + kts.insert("None".into(), None); + kts.insert("Some".into(), Some(ty.clone())); + Cow::Owned(kts) } - ExprKind::UnionType(kts) => { - use std::collections::hash_map::Entry; - let mut seen_fields = HashMap::new(); - // Check that all types are the same const - let mut k = None; - for (x, t) in kts { - if let Some(t) = t { - match (k, t.ty().as_const()) { - (None, Some(k2)) => k = Some(k2), - (Some(k1), Some(k2)) if k1 == k2 => {} - _ => return span_err("InvalidFieldType"), - } - } - match seen_fields.entry(x) { - Entry::Occupied(_) => { - return span_err("UnionTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(()), - }; - } + _ => return span_err("Merge2ArgMustBeUnionOrOptional"), + }; - // An empty union type has type Type; - // an union type with only unary variants also has type Type - let k = k.unwrap_or(Const::Type); + let mut inferred_type = None; + for (x, handler_type) in handlers { + let handler_return_type: Type = match variants.get(x) { + // Union alternative with type + Some(Some(variant_type)) => match handler_type.kind() { + PiClosure { closure, annot, .. } => { + if variant_type != annot { + return mkerr( + ErrorBuilder::new(format!( + "Wrong handler input type" + )) + .span_err( + span, + format!("in this merge expression",), + ) + .span_err( + record.span(), + format!( + "the handler for `{}` expects a value of \ + type: `{}`", + x, + annot.to_expr_tyenv(env) + ), + ) + .span_err( + scrut.span(), + format!( + "but the corresponding variant has type: \ + `{}`", + variant_type.to_expr_tyenv(env) + ), + ) + .format(), + ); + } - Type::from_const(k) - } - ExprKind::Op(OpKind::Field(scrut, x)) => { - match scrut.ty().kind() { - NirKind::RecordType(kts) => match kts.get(&x) { - Some(val) => Type::new_infer_universe(env, val.clone())?, - None => return span_err("MissingRecordField"), - }, - NirKind::Const(_) => { - let scrut = scrut.eval_to_type(env)?; - match scrut.kind() { - NirKind::UnionType(kts) => match kts.get(x) { - // Constructor has type T -> < x: T, ... > - Some(Some(ty)) => { - Nir::from_kind(NirKind::PiClosure { - binder: Binder::new(x.clone()), - annot: ty.clone(), - closure: Closure::new_constant( - scrut.to_nir(), - ), - }) - .to_type(scrut.ty()) - } - Some(None) => scrut, - None => return span_err("MissingUnionField"), - }, - _ => return span_err("NotARecord"), + // TODO: this actually doesn't check anything yet + match closure.remove_binder() { + Ok(v) => Type::new_infer_universe(env, v.clone())?, + Err(()) => { + return span_err("MergeReturnTypeIsDependent") + } } } - _ => return span_err("NotARecord"), + _ => { + return mkerr( + ErrorBuilder::new(format!( + "merge handler is not a function" + )) + .span_err(span, format!("in this merge expression")) + .span_err( + record.span(), + format!( + "the handler for `{}` has type: `{}`", + x, + handler_type.to_expr_tyenv(env) + ), + ) + .span_help( + scrut.span(), + format!( + "the corresponding variant has type: `{}`", + variant_type.to_expr_tyenv(env) + ), + ) + .help(format!( + "a handler for this variant must be a function \ + that takes an input of type: `{}`", + variant_type.to_expr_tyenv(env) + )) + .format(), + ) + } + }, + // Union alternative without type + Some(None) => Type::new_infer_universe(env, handler_type.clone())?, + None => return span_err("MergeHandlerMissingVariant"), + }; + match &inferred_type { + None => inferred_type = Some(handler_return_type), + Some(t) => { + if t != &handler_return_type { + return span_err("MergeHandlerTypeMismatch"); + } } } - ExprKind::Assert(t) => { - let t = t.eval_to_type(env)?; - match t.kind() { - NirKind::Equivalence(x, y) if x == y => {} - NirKind::Equivalence(..) => return span_err("AssertMismatch"), - _ => return span_err("AssertMustTakeEquivalence"), + } + for x in variants.keys() { + if !handlers.contains_key(x) { + return span_err("MergeVariantMissingHandler"); + } + } + + let type_annot = type_annot + .as_ref() + .map(|t| t.eval_to_type(env)) + .transpose()?; + Ok(match (inferred_type, type_annot) { + (Some(t1), Some(t2)) => { + if t1 != t2 { + return span_err("MergeAnnotMismatch"); } - t + t1 } - ExprKind::Op(OpKind::App(f, arg)) => { + (Some(t), None) => t, + (None, Some(t)) => t, + (None, None) => return span_err("MergeEmptyNeedsAnnotation"), + }) +} + +fn type_of_operation( + env: &TyEnv, + span: Span, + opkind: &OpKind>, +) -> Result { + let span_err = |msg: &str| mk_span_err(span.clone(), msg); + use NirKind::{ListType, PiClosure, RecordType, UnionType}; + use OpKind::*; + + Ok(match opkind { + App(f, arg) => { match f.ty().kind() { // TODO: store Type in closure - NirKind::PiClosure { annot, closure, .. } => { + PiClosure { annot, closure, .. } => { if arg.ty().as_nir() != annot { return mkerr( ErrorBuilder::new(format!( @@ -310,7 +367,8 @@ fn type_one_layer( ), } } - ExprKind::Op(OpKind::BoolIf(x, y, z)) => { + BinOp(o, l, r) => type_of_binop(env, span, *o, l, r)?, + BoolIf(x, y, z) => { if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } @@ -323,245 +381,16 @@ fn type_one_layer( y.ty().clone() } - ExprKind::Op(OpKind::BinOp(BinOp::RightBiasedRecordMerge, x, y)) => { - let x_type = x.ty(); - let y_type = y.ty(); - - // Extract the LHS record type - let kts_x = match x_type.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("MustCombineRecord"), - }; - // Extract the RHS record type - let kts_y = match y_type.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("MustCombineRecord"), - }; - - // Union the two records, prefering - // the values found in the RHS. - let kts = merge_maps(kts_x, kts_y, |_, _, r_t| r_t.clone()); - - let u = max(x.ty().ty(), y.ty().ty()); - Nir::from_kind(NirKind::RecordType(kts)).to_type(u) + Merge(record, scrut, type_annot) => { + type_of_merge(env, span, record, scrut, type_annot.as_ref())? } - ExprKind::Op(OpKind::BinOp(BinOp::RecursiveRecordMerge, x, y)) => { - check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?; - - let hir = Hir::new( - HirKind::Expr(ExprKind::Op(OpKind::BinOp( - BinOp::RecursiveRecordTypeMerge, - x.ty().to_hir(env.as_varenv()), - y.ty().to_hir(env.as_varenv()), - ))), - span.clone(), - ); - let x_u = x.ty().ty(); - let y_u = y.ty().ty(); - Type::new(hir.eval(env), max(x_u, y_u)) - } - ExprKind::Op(OpKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y)) => { - check_rectymerge(&span, env, x.eval(env), y.eval(env))?; - - // A RecordType's type is always a const - let xk = x.ty().as_const().unwrap(); - let yk = y.ty().as_const().unwrap(); - Type::from_const(max(xk, yk)) - } - ExprKind::Op(OpKind::BinOp(BinOp::ListAppend, l, r)) => { - match l.ty().kind() { - NirKind::ListType(..) => {} - _ => return span_err("BinOpTypeMismatch"), - } - - if l.ty() != r.ty() { - return span_err("BinOpTypeMismatch"); - } - - l.ty().clone() - } - ExprKind::Op(OpKind::BinOp(BinOp::Equivalence, l, r)) => { - if l.ty() != r.ty() { - return span_err("EquivalenceTypeMismatch"); - } - if l.ty().ty().as_const() != Some(Const::Type) { - return span_err("EquivalenceArgumentsMustBeTerms"); - } - - Type::from_const(Const::Type) - } - ExprKind::Op(OpKind::BinOp(o, l, r)) => { - let t = Type::from_builtin(match o { - BinOp::BoolAnd - | BinOp::BoolOr - | BinOp::BoolEQ - | BinOp::BoolNE => Builtin::Bool, - BinOp::NaturalPlus | BinOp::NaturalTimes => Builtin::Natural, - BinOp::TextAppend => Builtin::Text, - BinOp::ListAppend - | BinOp::RightBiasedRecordMerge - | BinOp::RecursiveRecordMerge - | BinOp::RecursiveRecordTypeMerge - | BinOp::Equivalence => unreachable!(), - BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"), - }); - - if *l.ty() != t { - return span_err("BinOpTypeMismatch"); - } - - if *r.ty() != t { - return span_err("BinOpTypeMismatch"); - } - - t - } - ExprKind::Op(OpKind::Merge(record, union, type_annot)) => { - let record_type = record.ty(); - let handlers = match record_type.kind() { - NirKind::RecordType(kts) => kts, - _ => return span_err("Merge1ArgMustBeRecord"), - }; - - let union_type = union.ty(); - let variants = match union_type.kind() { - NirKind::UnionType(kts) => Cow::Borrowed(kts), - NirKind::OptionalType(ty) => { - let mut kts = HashMap::new(); - kts.insert("None".into(), None); - kts.insert("Some".into(), Some(ty.clone())); - Cow::Owned(kts) - } - _ => return span_err("Merge2ArgMustBeUnionOrOptional"), - }; - - let mut inferred_type = None; - for (x, handler_type) in handlers { - let handler_return_type: Type = match variants.get(x) { - // Union alternative with type - Some(Some(variant_type)) => match handler_type.kind() { - NirKind::PiClosure { closure, annot, .. } => { - if variant_type != annot { - return mkerr( - ErrorBuilder::new(format!( - "Wrong handler input type" - )) - .span_err( - span, - format!("in this merge expression",), - ) - .span_err( - record.span(), - format!( - "the handler for `{}` expects a \ - value of type: `{}`", - x, - annot.to_expr_tyenv(env) - ), - ) - .span_err( - union.span(), - format!( - "but the corresponding variant \ - has type: `{}`", - variant_type.to_expr_tyenv(env) - ), - ) - .format(), - ); - } - - // TODO: this actually doesn't check anything yet - match closure.remove_binder() { - Ok(v) => { - Type::new_infer_universe(env, v.clone())? - } - Err(()) => { - return span_err( - "MergeReturnTypeIsDependent", - ) - } - } - } - _ => { - return mkerr( - ErrorBuilder::new(format!( - "merge handler is not a function" - )) - .span_err( - span, - format!("in this merge expression"), - ) - .span_err( - record.span(), - format!( - "the handler for `{}` has type: `{}`", - x, - handler_type.to_expr_tyenv(env) - ), - ) - .span_help( - union.span(), - format!( - "the corresponding variant has type: \ - `{}`", - variant_type.to_expr_tyenv(env) - ), - ) - .help(format!( - "a handler for this variant must be a \ - function that takes an input of type: \ - `{}`", - variant_type.to_expr_tyenv(env) - )) - .format(), - ) - } - }, - // Union alternative without type - Some(None) => { - Type::new_infer_universe(env, handler_type.clone())? - } - None => return span_err("MergeHandlerMissingVariant"), - }; - match &inferred_type { - None => inferred_type = Some(handler_return_type), - Some(t) => { - if t != &handler_return_type { - return span_err("MergeHandlerTypeMismatch"); - } - } - } - } - for x in variants.keys() { - if !handlers.contains_key(x) { - return span_err("MergeVariantMissingHandler"); - } - } - - let type_annot = type_annot - .as_ref() - .map(|t| t.eval_to_type(env)) - .transpose()?; - match (inferred_type, type_annot) { - (Some(t1), Some(t2)) => { - if t1 != t2 { - return span_err("MergeAnnotMismatch"); - } - t1 - } - (Some(t), None) => t, - (None, Some(t)) => t, - (None, None) => return span_err("MergeEmptyNeedsAnnotation"), - } - } - ExprKind::Op(OpKind::ToMap(record, annot)) => { + ToMap(record, annot) => { if record.ty().ty().as_const() != Some(Const::Type) { return span_err("`toMap` only accepts records of type `Type`"); } let record_t = record.ty(); let kts = match record_t.kind() { - NirKind::RecordType(kts) => kts, + RecordType(kts) => kts, _ => { return span_err("The argument to `toMap` must be a record") } @@ -581,11 +410,11 @@ fn type_one_layer( let err_msg = "The type of `toMap x` must be of the form \ `List { mapKey : Text, mapValue : T }`"; let arg = match annot_val.kind() { - NirKind::ListType(t) => t, + ListType(t) => t, _ => return span_err(err_msg), }; let kts = match arg.kind() { - NirKind::RecordType(kts) => kts, + RecordType(kts) => kts, _ => return span_err(err_msg), }; if kts.len() != 2 { @@ -614,7 +443,7 @@ fn type_one_layer( kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text)); kts.insert("mapValue".into(), entry_type); let output_type: Type = Nir::from_builtin(Builtin::List) - .app(Nir::from_kind(NirKind::RecordType(kts))) + .app(Nir::from_kind(RecordType(kts))) .to_type(Const::Type); if let Some(annot) = annot { let annot_val = annot.eval_to_type(env)?; @@ -625,10 +454,36 @@ fn type_one_layer( output_type } } - ExprKind::Op(OpKind::Projection(record, labels)) => { + Field(scrut, x) => { + match scrut.ty().kind() { + RecordType(kts) => match kts.get(&x) { + Some(val) => Type::new_infer_universe(env, val.clone())?, + None => return span_err("MissingRecordField"), + }, + NirKind::Const(_) => { + let scrut = scrut.eval_to_type(env)?; + match scrut.kind() { + UnionType(kts) => match kts.get(x) { + // Constructor has type T -> < x: T, ... > + Some(Some(ty)) => Nir::from_kind(PiClosure { + binder: Binder::new(x.clone()), + annot: ty.clone(), + closure: Closure::new_constant(scrut.to_nir()), + }) + .to_type(scrut.ty()), + Some(None) => scrut, + None => return span_err("MissingUnionField"), + }, + _ => return span_err("NotARecord"), + } + } + _ => return span_err("NotARecord"), + } + } + Projection(record, labels) => { let record_type = record.ty(); let kts = match record_type.kind() { - NirKind::RecordType(kts) => kts, + RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), }; @@ -648,21 +503,18 @@ fn type_one_layer( }; } - Type::new_infer_universe( - env, - Nir::from_kind(NirKind::RecordType(new_kts)), - )? + Type::new_infer_universe(env, Nir::from_kind(RecordType(new_kts)))? } - ExprKind::Op(OpKind::ProjectionByExpr(record, selection)) => { + ProjectionByExpr(record, selection) => { let record_type = record.ty(); let rec_kts = match record_type.kind() { - NirKind::RecordType(kts) => kts, + RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), }; let selection_val = selection.eval_to_type(env)?; let sel_kts = match selection_val.kind() { - NirKind::RecordType(kts) => kts, + RecordType(kts) => kts, _ => return span_err("ProjectionByExprTakesRecordType"), }; @@ -679,13 +531,182 @@ fn type_one_layer( selection_val } - }; + Completion(..) => { + unreachable!("This case should have been handled in resolution") + } + }) +} - Ok(ty) +/// When all sub-expressions have been typed, check the remaining toplevel +/// layer. +fn type_one_layer( + env: &TyEnv, + ekind: ExprKind>, + span: Span, +) -> Result { + let span_err = |msg: &str| mk_span_err(span.clone(), msg); + + Ok(match &ekind { + ExprKind::Import(..) => { + unreachable!("This case should have been handled in resolution") + } + ExprKind::Var(..) + | ExprKind::Const(Const::Sort) + | ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) + | ExprKind::Annot(..) => { + unreachable!("This case should have been handled in type_with") + } + + ExprKind::Const(Const::Type) => Type::from_const(Const::Kind), + ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort), + ExprKind::Num(num) => Type::from_builtin(match num { + NumKind::Bool(_) => Builtin::Bool, + NumKind::Natural(_) => Builtin::Natural, + NumKind::Integer(_) => Builtin::Integer, + NumKind::Double(_) => Builtin::Double, + }), + ExprKind::Builtin(b) => { + let t_hir = type_of_builtin(*b); + typecheck(&t_hir)?.eval_to_type(env)? + } + ExprKind::TextLit(interpolated) => { + let text_type = Type::from_builtin(Builtin::Text); + for contents in interpolated.iter() { + use InterpolatedTextContents::Expr; + if let Expr(x) = contents { + if *x.ty() != text_type { + return span_err("InvalidTextInterpolation"); + } + } + } + text_type + } + ExprKind::SomeLit(x) => { + if x.ty().ty().as_const() != Some(Const::Type) { + return span_err("InvalidOptionalType"); + } + + let t = x.ty().to_nir(); + Nir::from_builtin(Builtin::Optional) + .app(t) + .to_type(Const::Type) + } + ExprKind::EmptyListLit(t) => { + let t = t.eval_to_type(env)?; + match t.kind() { + NirKind::ListType(..) => {} + _ => return span_err("InvalidListType"), + }; + t + } + ExprKind::NEListLit(xs) => { + let mut iter = xs.iter(); + let x = iter.next().unwrap(); + for y in iter { + if x.ty() != y.ty() { + return span_err("InvalidListElement"); + } + } + if x.ty().ty().as_const() != Some(Const::Type) { + return span_err("InvalidListType"); + } + + let t = x.ty().to_nir(); + Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type) + } + ExprKind::RecordLit(kvs) => { + use std::collections::hash_map::Entry; + let mut kts = HashMap::new(); + // An empty record type has type Type + let mut k = Const::Type; + for (x, v) in kvs { + // Check for duplicated entries + match kts.entry(x.clone()) { + Entry::Occupied(_) => { + return span_err("RecordTypeDuplicateField") + } + Entry::Vacant(e) => e.insert(v.ty().to_nir()), + }; + + // Check that the fields have a valid kind + match v.ty().ty().as_const() { + Some(c) => k = max(k, c), + None => return span_err("InvalidFieldType"), + } + } + + Nir::from_kind(NirKind::RecordType(kts)).to_type(k) + } + ExprKind::RecordType(kts) => { + use std::collections::hash_map::Entry; + let mut seen_fields = HashMap::new(); + // An empty record type has type Type + let mut k = Const::Type; + + for (x, t) in kts { + // Check for duplicated entries + match seen_fields.entry(x.clone()) { + Entry::Occupied(_) => { + return span_err("RecordTypeDuplicateField") + } + Entry::Vacant(e) => e.insert(()), + }; + + // Check the type is a Const and compute final type + match t.ty().as_const() { + Some(c) => k = max(k, c), + None => return span_err("InvalidFieldType"), + } + } + + Type::from_const(k) + } + ExprKind::UnionType(kts) => { + use std::collections::hash_map::Entry; + let mut seen_fields = HashMap::new(); + // Check that all types are the same const + let mut k = None; + for (x, t) in kts { + if let Some(t) = t { + match (k, t.ty().as_const()) { + (None, Some(k2)) => k = Some(k2), + (Some(k1), Some(k2)) if k1 == k2 => {} + _ => return span_err("InvalidFieldType"), + } + } + match seen_fields.entry(x) { + Entry::Occupied(_) => { + return span_err("UnionTypeDuplicateField") + } + Entry::Vacant(e) => e.insert(()), + }; + } + + // An empty union type has type Type; + // an union type with only unary variants also has type Type + let k = k.unwrap_or(Const::Type); + + Type::from_const(k) + } + ExprKind::Op(op) => type_of_operation(env, span, op)?, + ExprKind::Assert(t) => { + let t = t.eval_to_type(env)?; + match t.kind() { + NirKind::Equivalence(x, y) if x == y => {} + NirKind::Equivalence(..) => return span_err("AssertMismatch"), + _ => return span_err("AssertMustTakeEquivalence"), + } + t + } + }) } /// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation /// to compare with. +// We pass the annotation to avoid duplicating the annot checking logic. I hope one day we can use +// it to handle the annotations in merge/toMap/etc. uniformly. pub fn type_with<'hir>( env: &TyEnv, hir: &'hir Hir, @@ -781,7 +802,7 @@ pub fn type_with<'hir>( Ok(tir) } -/// Typecheck an expression and return the expression annotated with types if type-checking +/// Typecheck an expression and return the expression annotated with its type if type-checking /// succeeded, or an error if type-checking failed. pub fn typecheck<'hir>(hir: &'hir Hir) -> Result, TypeError> { type_with(&TyEnv::new(), hir, None) -- 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 +- dhall/src/semantics/nze/normalize.rs | 553 ++++++++++++++++------------------- 2 files changed, 257 insertions(+), 300 deletions(-) (limited to 'dhall/src/semantics') 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), } } diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index ebf4ae1..bf37a3c 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -4,7 +4,7 @@ use std::collections::HashMap; use crate::semantics::NzEnv; use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit}; use crate::syntax::{ - BinOp, ExprKind, InterpolatedTextContents, NumKind, OpKind, + BinOp, ExprKind, InterpolatedTextContents, Label, NumKind, OpKind, }; pub fn apply_any(f: Nir, a: Nir) -> NirKind { @@ -83,79 +83,82 @@ where kvs } -// Small helper enum to avoid repetition -enum Ret<'a> { - NirKind(NirKind), - Nir(Nir), - NirRef(&'a Nir), - Expr(ExprKind), +type Ret = NirKind; + +fn ret_nir(x: Nir) -> Ret { + ret_ref(&x) +} +fn ret_kind(x: NirKind) -> Ret { + x +} +fn ret_ref(x: &Nir) -> Ret { + x.kind().clone() +} +fn ret_expr(x: ExprKind) -> Ret { + NirKind::PartialExpr(x) } -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, - }; +fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Option { + use BinOp::*; 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))), + (BoolAnd, Num(Bool(true)), _) => ret_ref(y), + (BoolAnd, _, Num(Bool(true))) => ret_ref(x), + (BoolAnd, Num(Bool(false)), _) => ret_kind(Num(Bool(false))), + (BoolAnd, _, Num(Bool(false))) => ret_kind(Num(Bool(false))), + (BoolAnd, _, _) if x == y => ret_ref(x), + (BoolOr, Num(Bool(true)), _) => ret_kind(Num(Bool(true))), + (BoolOr, _, Num(Bool(true))) => ret_kind(Num(Bool(true))), + (BoolOr, Num(Bool(false)), _) => ret_ref(y), + (BoolOr, _, Num(Bool(false))) => ret_ref(x), + (BoolOr, _, _) if x == y => ret_ref(x), + (BoolEQ, Num(Bool(true)), _) => ret_ref(y), + (BoolEQ, _, Num(Bool(true))) => ret_ref(x), + (BoolEQ, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x == y))), + (BoolEQ, _, _) if x == y => ret_kind(Num(Bool(true))), + (BoolNE, Num(Bool(false)), _) => ret_ref(y), + (BoolNE, _, Num(Bool(false))) => ret_ref(x), + (BoolNE, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x != y))), + (BoolNE, _, _) if x == y => ret_kind(Num(Bool(false))), - (NaturalPlus, Num(Natural(0)), _) => Ret::NirRef(y), - (NaturalPlus, _, Num(Natural(0))) => Ret::NirRef(x), + (NaturalPlus, Num(Natural(0)), _) => ret_ref(y), + (NaturalPlus, _, Num(Natural(0))) => ret_ref(x), (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => { - Ret::NirKind(Num(Natural(x + y))) + ret_kind(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(0)), _) => ret_kind(Num(Natural(0))), + (NaturalTimes, _, Num(Natural(0))) => ret_kind(Num(Natural(0))), + (NaturalTimes, Num(Natural(1)), _) => ret_ref(y), + (NaturalTimes, _, Num(Natural(1))) => ret_ref(x), (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => { - Ret::NirKind(Num(Natural(x * y))) + ret_kind(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(), - )), + (ListAppend, EmptyListLit(_), _) => ret_ref(y), + (ListAppend, _, EmptyListLit(_)) => ret_ref(x), + (ListAppend, NEListLit(xs), NEListLit(ys)) => { + ret_kind(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), _) if x.is_empty() => ret_ref(y), + (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => ret_ref(x), (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => { - Ret::NirKind(NirKind::TextLit(x.concat(y))) + ret_kind(NirKind::TextLit(x.concat(y))) } - (TextAppend, NirKind::TextLit(x), _) => Ret::NirKind(NirKind::TextLit( + (TextAppend, NirKind::TextLit(x), _) => ret_kind(NirKind::TextLit( x.concat(&TextLit::interpolate(y.clone())), )), - (TextAppend, _, NirKind::TextLit(y)) => Ret::NirKind(NirKind::TextLit( + (TextAppend, _, NirKind::TextLit(y)) => ret_kind(NirKind::TextLit( TextLit::interpolate(x.clone()).concat(y), )), (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::NirRef(x) + ret_ref(x) } (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::NirRef(y) + ret_ref(y) } (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let mut kvs = kvs2.clone(); @@ -163,15 +166,15 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { // Insert only if key not already present kvs.entry(x.clone()).or_insert_with(|| v.clone()); } - Ret::NirKind(RecordLit(kvs)) + ret_kind(RecordLit(kvs)) } - (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y), + (RightBiasedRecordMerge, _, _) if x == y => ret_ref(y), (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::NirRef(x) + ret_ref(x) } (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::NirRef(y) + ret_ref(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| { @@ -181,7 +184,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { v2.clone(), ))) }); - Ret::NirKind(RecordLit(kvs)) + ret_kind(RecordLit(kvs)) } (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => { @@ -197,276 +200,153 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { ))) }, ); - Ret::NirKind(RecordType(kts)) + ret_kind(RecordType(kts)) } (Equivalence, _, _) => { - Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone())) + ret_kind(NirKind::Equivalence(x.clone(), y.clone())) } _ => return None, }) } -#[allow(clippy::cognitive_complexity)] -pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { - use NirKind::{ - EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, - PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, - UnionType, - }; - use NumKind::Bool; - - let ret = match expr { - ExprKind::Import(..) | ExprKind::Op(OpKind::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" - ), +fn normalize_field(v: &Nir, field: &Label) -> Option { + use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge}; + use ExprKind::Op; + use NirKind::{PartialExpr, RecordLit, UnionConstructor, UnionType}; + use OpKind::{BinOp, Field, Projection}; - 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::Op(OpKind::App(v, a)) => Ret::Nir(v.app(a)), - ExprKind::Num(l) => Ret::NirKind(Num(l)), - ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)), - ExprKind::EmptyListLit(t) => { - let arg = match t.kind() { - NirKind::ListType(t) => t.clone(), - _ => panic!("internal type error"), - }; - Ret::NirKind(NirKind::EmptyListLit(arg)) - } - ExprKind::NEListLit(elts) => { - Ret::NirKind(NEListLit(elts.into_iter().collect())) - } - ExprKind::RecordLit(kvs) => { - Ret::NirKind(RecordLit(kvs.into_iter().collect())) - } - ExprKind::RecordType(kvs) => { - Ret::NirKind(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::Op(OpKind::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::Op(OpKind::BinOp(o, ref x, ref y)) => { - match apply_binop(o, x, y) { - Some(ret) => ret, - None => Ret::Expr(expr), - } + Some(match v.kind() { + RecordLit(kvs) => match kvs.get(field) { + Some(r) => ret_nir(r.clone()), + None => return None, + }, + UnionType(kts) => { + ret_kind(UnionConstructor(field.clone(), kts.clone())) } - - ExprKind::Op(OpKind::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::Op(OpKind::Projection(x, _))) => { - return normalize_one_layer( - ExprKind::Op(OpKind::Field(x.clone(), field.clone())), - env, - ) - } - PartialExpr(ExprKind::Op(OpKind::BinOp( - BinOp::RightBiasedRecordMerge, - x, - y, - ))) => match (x.kind(), y.kind()) { + PartialExpr(Op(Projection(x, _))) => return normalize_field(x, field), + PartialExpr(Op(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::Op(OpKind::Field( - x.clone(), - field.clone(), - )), - env, - ) - } + Some(r) => ret_nir(r.clone()), + None => return normalize_field(x, field), }, (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( - Nir::from_kind(PartialExpr(ExprKind::Op( - OpKind::BinOp( - BinOp::RightBiasedRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ), - ))), + Some(r) => ret_expr(Op(Field( + Nir::from_kind(PartialExpr(Op(BinOp( + RightBiasedRecordMerge, + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + y.clone(), + )))), field.clone(), ))), - None => { - return normalize_one_layer( - ExprKind::Op(OpKind::Field( - y.clone(), - field.clone(), - )), - env, - ) - } + None => return normalize_field(y, field), }, - _ => Ret::Expr(expr), - }, - PartialExpr(ExprKind::Op(OpKind::BinOp( - BinOp::RecursiveRecordMerge, - x, - y, - ))) => match (x.kind(), y.kind()) { + _ => return None, + } + } + PartialExpr(Op(BinOp(RecursiveRecordMerge, x, y))) => { + match (x.kind(), y.kind()) { (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( - Nir::from_kind(PartialExpr(ExprKind::Op( - OpKind::BinOp( - BinOp::RecursiveRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ), - ))), + Some(r) => ret_expr(Op(Field( + Nir::from_kind(PartialExpr(Op(BinOp( + RecursiveRecordMerge, + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + y.clone(), + )))), field.clone(), ))), - None => { - return normalize_one_layer( - ExprKind::Op(OpKind::Field( - y.clone(), - field.clone(), - )), - env, - ) - } + None => return normalize_field(y, field), }, (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => Ret::Expr(ExprKind::Op(OpKind::Field( - Nir::from_kind(PartialExpr(ExprKind::Op( - OpKind::BinOp( - BinOp::RecursiveRecordMerge, - x.clone(), - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - ), - ))), + Some(r) => ret_expr(Op(Field( + Nir::from_kind(PartialExpr(Op(BinOp( + RecursiveRecordMerge, + x.clone(), + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + )))), field.clone(), ))), - None => { - return normalize_one_layer( - ExprKind::Op(OpKind::Field( - x.clone(), - field.clone(), - )), - env, - ) - } + None => return normalize_field(x, field), }, - _ => Ret::Expr(expr), - }, - _ => Ret::Expr(expr), - }, - ExprKind::Op(OpKind::Projection(_, ref ls)) if ls.is_empty() => { - Ret::NirKind(RecordLit(HashMap::new())) - } - ExprKind::Op(OpKind::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::Op(OpKind::Projection(v2, _))) => { - return normalize_one_layer( - ExprKind::Op(OpKind::Projection(v2.clone(), ls.clone())), - env, - ) - } - _ => Ret::Expr(expr), - }, - ExprKind::Op(OpKind::ProjectionByExpr(ref v, ref t)) => { - match t.kind() { - RecordType(kts) => { - return normalize_one_layer( - ExprKind::Op(OpKind::Projection( - v.clone(), - kts.keys().cloned().collect(), - )), - env, - ) - } - _ => Ret::Expr(expr), + _ => return None, } } + _ => return None, + }) +} - ExprKind::Op(OpKind::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), +fn normalize_operation(opkind: &OpKind) -> Option { + use ExprKind::Op; + use NirKind::{ + EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, + PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, + }; + use NumKind::Bool; + use OpKind::*; + + Some(match opkind { + App(v, a) => ret_nir(v.app(a.clone())), + BinOp(o, x, y) => return normalize_binop(*o, x, y), + BoolIf(b, e1, e2) => { + match b.kind() { + Num(Bool(true)) => ret_ref(e1), + Num(Bool(false)) => ret_ref(e2), + _ => { + match (e1.kind(), e2.kind()) { + // Simplify `if b then True else False` + (Num(Bool(true)), Num(Bool(false))) => ret_ref(b), + _ if e1 == e2 => ret_ref(e1), + _ => return None, + } + } } } - ExprKind::Op(OpKind::ToMap(ref v, ref annot)) => match v.kind() { + Merge(handlers, variant, _) => match handlers.kind() { + RecordLit(kvs) => match variant.kind() { + UnionConstructor(l, _) => match kvs.get(l) { + Some(h) => ret_nir(h.clone()), + None => return None, + }, + UnionLit(l, v, _) => match kvs.get(l) { + Some(h) => ret_nir(h.app(v.clone())), + None => return None, + }, + EmptyOptionalLit(_) => match kvs.get(&"None".into()) { + Some(h) => ret_nir(h.clone()), + None => return None, + }, + NEOptionalLit(v) => match kvs.get(&"Some".into()) { + Some(h) => ret_nir(h.app(v.clone())), + None => return None, + }, + _ => return None, + }, + _ => return None, + }, + ToMap(v, 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_kind(EmptyListLit(t.clone())) } - _ => Ret::Expr(expr), + _ => return None, } } - RecordLit(kvs) => Ret::NirKind(NEListLit( + RecordLit(kvs) => ret_kind(NEListLit( kvs.iter() .sorted_by_key(|(k, _)| *k) .map(|(k, v)| { @@ -477,23 +357,100 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { }) .collect(), )), - _ => Ret::Expr(expr), + _ => return None, + }, + Field(v, field) => return normalize_field(v, field), + Projection(_, ls) if ls.is_empty() => { + ret_kind(RecordLit(HashMap::new())) + } + Projection(v, ls) => match v.kind() { + RecordLit(kvs) => ret_kind(RecordLit( + ls.iter() + .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) + .collect(), + )), + PartialExpr(Op(Projection(v2, _))) => { + return normalize_operation(&Projection(v2.clone(), ls.clone())) + } + _ => return None, + }, + ProjectionByExpr(v, t) => match t.kind() { + RecordType(kts) => { + return normalize_operation(&Projection( + v.clone(), + kts.keys().cloned().collect(), + )) + } + _ => return None, }, + Completion(..) => { + unreachable!("This case should have been handled in resolution") + } + }) +} + +pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { + use NirKind::{ + NEListLit, NEOptionalLit, Num, RecordLit, RecordType, UnionType, }; - match ret { - Ret::NirKind(v) => v, - Ret::Nir(v) => v.kind().clone(), - Ret::NirRef(v) => v.kind().clone(), - Ret::Expr(expr) => NirKind::PartialExpr(expr), + match expr { + ExprKind::Var(..) + | ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) => { + unreachable!("This case should have been handled in normalize_hir") + } + + ExprKind::Const(c) => ret_nir(Nir::from_const(c)), + ExprKind::Num(l) => ret_kind(Num(l)), + ExprKind::Builtin(b) => ret_nir(Nir::from_builtin_env(b, env)), + 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_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_kind(NirKind::EmptyListLit(arg)) + } + ExprKind::NEListLit(elts) => { + ret_kind(NEListLit(elts.into_iter().collect())) + } + ExprKind::RecordLit(kvs) => { + ret_kind(RecordLit(kvs.into_iter().collect())) + } + ExprKind::RecordType(kvs) => { + ret_kind(RecordType(kvs.into_iter().collect())) + } + ExprKind::UnionType(kvs) => { + ret_kind(UnionType(kvs.into_iter().collect())) + } + ExprKind::Op(ref op) => match normalize_operation(op) { + Some(ret) => ret, + None => ret_expr(expr), + }, + ExprKind::Annot(x, _) => ret_nir(x), + ExprKind::Assert(_) => ret_expr(expr), + ExprKind::Import(..) => { + unreachable!("This case should have been handled in resolution") + } } } /// 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 { -- 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 +++++--- dhall/src/semantics/nze/normalize.rs | 28 +++++++++++++++------------- 2 files changed, 20 insertions(+), 16 deletions(-) (limited to 'dhall/src/semantics') 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 { diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index bf37a3c..f6782af 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -7,14 +7,14 @@ use crate::syntax::{ BinOp, ExprKind, InterpolatedTextContents, Label, NumKind, OpKind, }; -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::Op(OpKind::App(f, a))), + _ => NirKind::PartialExpr(ExprKind::Op(OpKind::App(f.clone(), a))), } } @@ -219,7 +219,7 @@ fn normalize_field(v: &Nir, field: &Label) -> Option { Some(match v.kind() { RecordLit(kvs) => match kvs.get(field) { - Some(r) => ret_nir(r.clone()), + Some(r) => ret_ref(r), None => return None, }, UnionType(kts) => { @@ -229,7 +229,7 @@ fn normalize_field(v: &Nir, field: &Label) -> Option { PartialExpr(Op(BinOp(RightBiasedRecordMerge, x, y))) => { match (x.kind(), y.kind()) { (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_nir(r.clone()), + Some(r) => ret_ref(r), None => return normalize_field(x, field), }, (RecordLit(kvs), _) => match kvs.get(field) { @@ -299,7 +299,7 @@ fn normalize_operation(opkind: &OpKind) -> Option { use OpKind::*; Some(match opkind { - App(v, a) => ret_nir(v.app(a.clone())), + App(v, a) => ret_kind(v.app_to_kind(a.clone())), BinOp(o, x, y) => return normalize_binop(*o, x, y), BoolIf(b, e1, e2) => { match b.kind() { @@ -318,19 +318,19 @@ fn normalize_operation(opkind: &OpKind) -> Option { Merge(handlers, variant, _) => match handlers.kind() { RecordLit(kvs) => match variant.kind() { UnionConstructor(l, _) => match kvs.get(l) { - Some(h) => ret_nir(h.clone()), + Some(h) => ret_ref(h), None => return None, }, UnionLit(l, v, _) => match kvs.get(l) { - Some(h) => ret_nir(h.app(v.clone())), + Some(h) => ret_kind(h.app_to_kind(v.clone())), None => return None, }, EmptyOptionalLit(_) => match kvs.get(&"None".into()) { - Some(h) => ret_nir(h.clone()), + Some(h) => ret_ref(h), None => return None, }, NEOptionalLit(v) => match kvs.get(&"Some".into()) { - Some(h) => ret_nir(h.app(v.clone())), + Some(h) => ret_kind(h.app_to_kind(v.clone())), None => return None, }, _ => return None, @@ -391,7 +391,7 @@ fn normalize_operation(opkind: &OpKind) -> Option { pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { use NirKind::{ - NEListLit, NEOptionalLit, Num, RecordLit, RecordType, UnionType, + Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, UnionType, }; match expr { @@ -402,14 +402,16 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { unreachable!("This case should have been handled in normalize_hir") } - ExprKind::Const(c) => ret_nir(Nir::from_const(c)), + ExprKind::Const(c) => ret_kind(Const(c)), ExprKind::Num(l) => ret_kind(Num(l)), - ExprKind::Builtin(b) => ret_nir(Nir::from_builtin_env(b, env)), + 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_nir(v.clone()) + ret_ref(v) } else { ret_kind(NirKind::TextLit(tlit)) } -- cgit v1.2.3 From 60db959ef9bb49065769155494f49cf1b46bb835 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 18:49:36 +0100 Subject: oops --- dhall/src/semantics/tck/typecheck.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 28d08b9..427b39d 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -181,7 +181,7 @@ fn type_of_merge( let span_err = |msg: &str| mk_span_err(span.clone(), msg); use NirKind::{OptionalType, PiClosure, RecordType, UnionType}; - let record_type = scrut.ty(); + let record_type = record.ty(); let handlers = match record_type.kind() { RecordType(kts) => kts, _ => return span_err("Merge1ArgMustBeRecord"), -- cgit v1.2.3 From 4ed17cb88df732d3ce3d09e2bfd0b7c855309094 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 Apr 2020 19:08:51 +0100 Subject: Fix normalization bug --- dhall/src/semantics/nze/normalize.rs | 98 ++++++++++++++++++------------------ 1 file changed, 49 insertions(+), 49 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index f6782af..532d2e4 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -97,13 +97,16 @@ fn ret_ref(x: &Nir) -> Ret { fn ret_expr(x: ExprKind) -> Ret { NirKind::PartialExpr(x) } +fn ret_op(x: OpKind) -> Ret { + ret_expr(ExprKind::Op(x)) +} -fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Option { +fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret { use BinOp::*; use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType}; use NumKind::{Bool, Natural}; - Some(match (o, x.kind(), y.kind()) { + match (o, x.kind(), y.kind()) { (BoolAnd, Num(Bool(true)), _) => ret_ref(y), (BoolAnd, _, Num(Bool(true))) => ret_ref(x), (BoolAnd, Num(Bool(false)), _) => ret_kind(Num(Bool(false))), @@ -207,33 +210,34 @@ fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Option { ret_kind(NirKind::Equivalence(x.clone(), y.clone())) } - _ => return None, - }) + _ => ret_op(OpKind::BinOp(o, x.clone(), y.clone())), + } } -fn normalize_field(v: &Nir, field: &Label) -> Option { +fn normalize_field(v: &Nir, field: &Label) -> Ret { use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge}; use ExprKind::Op; use NirKind::{PartialExpr, RecordLit, UnionConstructor, UnionType}; use OpKind::{BinOp, Field, Projection}; + let nothing_to_do = || ret_op(Field(v.clone(), field.clone())); - Some(match v.kind() { + match v.kind() { RecordLit(kvs) => match kvs.get(field) { Some(r) => ret_ref(r), - None => return None, + None => nothing_to_do(), }, UnionType(kts) => { ret_kind(UnionConstructor(field.clone(), kts.clone())) } - PartialExpr(Op(Projection(x, _))) => return normalize_field(x, field), + PartialExpr(Op(Projection(x, _))) => normalize_field(x, field), PartialExpr(Op(BinOp(RightBiasedRecordMerge, x, y))) => { match (x.kind(), y.kind()) { (_, RecordLit(kvs)) => match kvs.get(field) { Some(r) => ret_ref(r), - None => return normalize_field(x, field), + None => normalize_field(x, field), }, (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_expr(Op(Field( + Some(r) => ret_op(Field( Nir::from_kind(PartialExpr(Op(BinOp( RightBiasedRecordMerge, Nir::from_kind(RecordLit( @@ -244,16 +248,16 @@ fn normalize_field(v: &Nir, field: &Label) -> Option { y.clone(), )))), field.clone(), - ))), - None => return normalize_field(y, field), + )), + None => normalize_field(y, field), }, - _ => return None, + _ => nothing_to_do(), } } PartialExpr(Op(BinOp(RecursiveRecordMerge, x, y))) => { match (x.kind(), y.kind()) { (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_expr(Op(Field( + Some(r) => ret_op(Field( Nir::from_kind(PartialExpr(Op(BinOp( RecursiveRecordMerge, Nir::from_kind(RecordLit( @@ -264,11 +268,11 @@ fn normalize_field(v: &Nir, field: &Label) -> Option { y.clone(), )))), field.clone(), - ))), - None => return normalize_field(y, field), + )), + None => normalize_field(y, field), }, (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_expr(Op(Field( + Some(r) => ret_op(Field( Nir::from_kind(PartialExpr(Op(BinOp( RecursiveRecordMerge, x.clone(), @@ -279,17 +283,17 @@ fn normalize_field(v: &Nir, field: &Label) -> Option { )), )))), field.clone(), - ))), - None => return normalize_field(x, field), + )), + None => normalize_field(x, field), }, - _ => return None, + _ => nothing_to_do(), } } - _ => return None, - }) + _ => nothing_to_do(), + } } -fn normalize_operation(opkind: &OpKind) -> Option { +fn normalize_operation(opkind: &OpKind) -> Ret { use ExprKind::Op; use NirKind::{ EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, @@ -297,10 +301,11 @@ fn normalize_operation(opkind: &OpKind) -> Option { }; use NumKind::Bool; use OpKind::*; + let nothing_to_do = || ret_op(opkind.clone()); - Some(match opkind { + match opkind { App(v, a) => ret_kind(v.app_to_kind(a.clone())), - BinOp(o, x, y) => return normalize_binop(*o, x, y), + BinOp(o, x, y) => normalize_binop(*o, x, y), BoolIf(b, e1, e2) => { match b.kind() { Num(Bool(true)) => ret_ref(e1), @@ -310,7 +315,7 @@ fn normalize_operation(opkind: &OpKind) -> Option { // Simplify `if b then True else False` (Num(Bool(true)), Num(Bool(false))) => ret_ref(b), _ if e1 == e2 => ret_ref(e1), - _ => return None, + _ => nothing_to_do(), } } } @@ -319,23 +324,23 @@ fn normalize_operation(opkind: &OpKind) -> Option { RecordLit(kvs) => match variant.kind() { UnionConstructor(l, _) => match kvs.get(l) { Some(h) => ret_ref(h), - None => return None, + None => nothing_to_do(), }, UnionLit(l, v, _) => match kvs.get(l) { Some(h) => ret_kind(h.app_to_kind(v.clone())), - None => return None, + None => nothing_to_do(), }, EmptyOptionalLit(_) => match kvs.get(&"None".into()) { Some(h) => ret_ref(h), - None => return None, + None => nothing_to_do(), }, NEOptionalLit(v) => match kvs.get(&"Some".into()) { Some(h) => ret_kind(h.app_to_kind(v.clone())), - None => return None, + None => nothing_to_do(), }, - _ => return None, + _ => nothing_to_do(), }, - _ => return None, + _ => nothing_to_do(), }, ToMap(v, annot) => match v.kind() { RecordLit(kvs) if kvs.is_empty() => { @@ -343,7 +348,7 @@ fn normalize_operation(opkind: &OpKind) -> Option { Some(NirKind::ListType(t)) => { ret_kind(EmptyListLit(t.clone())) } - _ => return None, + _ => nothing_to_do(), } } RecordLit(kvs) => ret_kind(NEListLit( @@ -357,9 +362,9 @@ fn normalize_operation(opkind: &OpKind) -> Option { }) .collect(), )), - _ => return None, + _ => nothing_to_do(), }, - Field(v, field) => return normalize_field(v, field), + Field(v, field) => normalize_field(v, field), Projection(_, ls) if ls.is_empty() => { ret_kind(RecordLit(HashMap::new())) } @@ -370,23 +375,21 @@ fn normalize_operation(opkind: &OpKind) -> Option { .collect(), )), PartialExpr(Op(Projection(v2, _))) => { - return normalize_operation(&Projection(v2.clone(), ls.clone())) + normalize_operation(&Projection(v2.clone(), ls.clone())) } - _ => return None, + _ => nothing_to_do(), }, ProjectionByExpr(v, t) => match t.kind() { - RecordType(kts) => { - return normalize_operation(&Projection( - v.clone(), - kts.keys().cloned().collect(), - )) - } - _ => return None, + RecordType(kts) => normalize_operation(&Projection( + v.clone(), + kts.keys().cloned().collect(), + )), + _ => nothing_to_do(), }, Completion(..) => { unreachable!("This case should have been handled in resolution") } - }) + } } pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { @@ -436,10 +439,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { ExprKind::UnionType(kvs) => { ret_kind(UnionType(kvs.into_iter().collect())) } - ExprKind::Op(ref op) => match normalize_operation(op) { - Some(ret) => ret, - None => ret_expr(expr), - }, + ExprKind::Op(ref op) => normalize_operation(op), ExprKind::Annot(x, _) => ret_nir(x), ExprKind::Assert(_) => ret_expr(expr), ExprKind::Import(..) => { -- 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 +++--- dhall/src/semantics/nze/normalize.rs | 138 +++++++++++++++++------------------ 2 files changed, 77 insertions(+), 82 deletions(-) (limited to 'dhall/src/semantics') 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))), }), }; diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 532d2e4..c0e41cb 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -14,7 +14,7 @@ pub fn apply_any(f: &Nir, a: Nir) -> NirKind { NirKind::UnionConstructor(l, kts) => { NirKind::UnionLit(l.clone(), a, kts.clone()) } - _ => NirKind::PartialExpr(ExprKind::Op(OpKind::App(f.clone(), a))), + _ => NirKind::Op(OpKind::App(f.clone(), a)), } } @@ -94,11 +94,8 @@ fn ret_kind(x: NirKind) -> Ret { fn ret_ref(x: &Nir) -> Ret { x.kind().clone() } -fn ret_expr(x: ExprKind) -> Ret { - NirKind::PartialExpr(x) -} fn ret_op(x: OpKind) -> Ret { - ret_expr(ExprKind::Op(x)) + NirKind::Op(x) } fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret { @@ -216,8 +213,7 @@ fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret { fn normalize_field(v: &Nir, field: &Label) -> Ret { use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge}; - use ExprKind::Op; - use NirKind::{PartialExpr, RecordLit, UnionConstructor, UnionType}; + use NirKind::{Op, RecordLit, UnionConstructor, UnionType}; use OpKind::{BinOp, Field, Projection}; let nothing_to_do = || ret_op(Field(v.clone(), field.clone())); @@ -229,75 +225,70 @@ fn normalize_field(v: &Nir, field: &Label) -> Ret { UnionType(kts) => { ret_kind(UnionConstructor(field.clone(), kts.clone())) } - PartialExpr(Op(Projection(x, _))) => normalize_field(x, field), - PartialExpr(Op(BinOp(RightBiasedRecordMerge, x, y))) => { - match (x.kind(), y.kind()) { - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_ref(r), - None => normalize_field(x, field), - }, - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(PartialExpr(Op(BinOp( - RightBiasedRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - )))), - field.clone(), - )), - None => normalize_field(y, field), - }, - _ => nothing_to_do(), - } - } - PartialExpr(Op(BinOp(RecursiveRecordMerge, x, y))) => { - match (x.kind(), y.kind()) { - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(PartialExpr(Op(BinOp( - RecursiveRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - )))), - field.clone(), - )), - None => normalize_field(y, field), - }, - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(PartialExpr(Op(BinOp( - RecursiveRecordMerge, - x.clone(), - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - )))), - field.clone(), - )), - None => normalize_field(x, field), - }, - _ => nothing_to_do(), - } - } + Op(Projection(x, _)) => normalize_field(x, field), + Op(BinOp(RightBiasedRecordMerge, x, y)) => match (x.kind(), y.kind()) { + (_, RecordLit(kvs)) => match kvs.get(field) { + Some(r) => ret_ref(r), + None => normalize_field(x, field), + }, + (RecordLit(kvs), _) => match kvs.get(field) { + Some(r) => ret_op(Field( + Nir::from_kind(Op(BinOp( + RightBiasedRecordMerge, + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + y.clone(), + ))), + field.clone(), + )), + None => normalize_field(y, field), + }, + _ => nothing_to_do(), + }, + Op(BinOp(RecursiveRecordMerge, x, y)) => match (x.kind(), y.kind()) { + (RecordLit(kvs), _) => match kvs.get(field) { + Some(r) => ret_op(Field( + Nir::from_kind(Op(BinOp( + RecursiveRecordMerge, + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + y.clone(), + ))), + field.clone(), + )), + None => normalize_field(y, field), + }, + (_, RecordLit(kvs)) => match kvs.get(field) { + Some(r) => ret_op(Field( + Nir::from_kind(Op(BinOp( + RecursiveRecordMerge, + x.clone(), + Nir::from_kind(RecordLit( + Some((field.clone(), r.clone())) + .into_iter() + .collect(), + )), + ))), + field.clone(), + )), + None => normalize_field(x, field), + }, + _ => nothing_to_do(), + }, _ => nothing_to_do(), } } fn normalize_operation(opkind: &OpKind) -> Ret { - use ExprKind::Op; use NirKind::{ - EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, - PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit, + EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, Op, + RecordLit, RecordType, UnionConstructor, UnionLit, }; use NumKind::Bool; use OpKind::*; @@ -374,7 +365,7 @@ fn normalize_operation(opkind: &OpKind) -> Ret { .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) .collect(), )), - PartialExpr(Op(Projection(v2, _))) => { + Op(Projection(v2, _)) => { normalize_operation(&Projection(v2.clone(), ls.clone())) } _ => nothing_to_do(), @@ -394,7 +385,8 @@ fn normalize_operation(opkind: &OpKind) -> Ret { pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { use NirKind::{ - Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, UnionType, + Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, + UnionType, }; match expr { @@ -441,7 +433,7 @@ pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { } ExprKind::Op(ref op) => normalize_operation(op), ExprKind::Annot(x, _) => ret_nir(x), - ExprKind::Assert(_) => ret_expr(expr), + ExprKind::Assert(x) => ret_kind(Assert(x)), ExprKind::Import(..) => { unreachable!("This case should have been handled in resolution") } -- 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/builtins.rs | 5 +- dhall/src/semantics/nze/nir.rs | 3 +- dhall/src/semantics/nze/normalize.rs | 301 +------------------ dhall/src/semantics/resolve/resolve.rs | 3 +- dhall/src/semantics/tck/typecheck.rs | 515 +-------------------------------- 5 files changed, 18 insertions(+), 809 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 45be448..f65e8d1 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -1,3 +1,4 @@ +use crate::operations::OpKind; use crate::semantics::{ skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv, }; @@ -5,8 +6,8 @@ use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; use crate::syntax::{ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText, - InterpolatedTextContents, Label, NaiveDouble, NumKind, OpKind, Span, - UnspannedExpr, V, + InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr, + V, }; use std::collections::HashMap; use std::convert::TryInto; 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; diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index c0e41cb..d042f3f 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -1,11 +1,9 @@ -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, Label, NumKind, OpKind, -}; +use crate::syntax::{ExprKind, InterpolatedTextContents}; pub fn apply_any(f: &Nir, a: Nir) -> NirKind { match f.kind() { @@ -83,306 +81,21 @@ where kvs } -type Ret = NirKind; +pub type Ret = NirKind; -fn ret_nir(x: Nir) -> Ret { +pub fn ret_nir(x: Nir) -> Ret { ret_ref(&x) } -fn ret_kind(x: NirKind) -> Ret { +pub fn ret_kind(x: NirKind) -> Ret { x } -fn ret_ref(x: &Nir) -> Ret { +pub fn ret_ref(x: &Nir) -> Ret { x.kind().clone() } -fn ret_op(x: OpKind) -> Ret { +pub fn ret_op(x: OpKind) -> Ret { NirKind::Op(x) } -fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret { - use BinOp::*; - use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType}; - use NumKind::{Bool, Natural}; - - match (o, x.kind(), y.kind()) { - (BoolAnd, Num(Bool(true)), _) => ret_ref(y), - (BoolAnd, _, Num(Bool(true))) => ret_ref(x), - (BoolAnd, Num(Bool(false)), _) => ret_kind(Num(Bool(false))), - (BoolAnd, _, Num(Bool(false))) => ret_kind(Num(Bool(false))), - (BoolAnd, _, _) if x == y => ret_ref(x), - (BoolOr, Num(Bool(true)), _) => ret_kind(Num(Bool(true))), - (BoolOr, _, Num(Bool(true))) => ret_kind(Num(Bool(true))), - (BoolOr, Num(Bool(false)), _) => ret_ref(y), - (BoolOr, _, Num(Bool(false))) => ret_ref(x), - (BoolOr, _, _) if x == y => ret_ref(x), - (BoolEQ, Num(Bool(true)), _) => ret_ref(y), - (BoolEQ, _, Num(Bool(true))) => ret_ref(x), - (BoolEQ, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x == y))), - (BoolEQ, _, _) if x == y => ret_kind(Num(Bool(true))), - (BoolNE, Num(Bool(false)), _) => ret_ref(y), - (BoolNE, _, Num(Bool(false))) => ret_ref(x), - (BoolNE, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x != y))), - (BoolNE, _, _) if x == y => ret_kind(Num(Bool(false))), - - (NaturalPlus, Num(Natural(0)), _) => ret_ref(y), - (NaturalPlus, _, Num(Natural(0))) => ret_ref(x), - (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => { - ret_kind(Num(Natural(x + y))) - } - (NaturalTimes, Num(Natural(0)), _) => ret_kind(Num(Natural(0))), - (NaturalTimes, _, Num(Natural(0))) => ret_kind(Num(Natural(0))), - (NaturalTimes, Num(Natural(1)), _) => ret_ref(y), - (NaturalTimes, _, Num(Natural(1))) => ret_ref(x), - (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => { - ret_kind(Num(Natural(x * y))) - } - - (ListAppend, EmptyListLit(_), _) => ret_ref(y), - (ListAppend, _, EmptyListLit(_)) => ret_ref(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => { - ret_kind(NEListLit(xs.iter().chain(ys.iter()).cloned().collect())) - } - - (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => ret_ref(y), - (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => ret_ref(x), - (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => { - ret_kind(NirKind::TextLit(x.concat(y))) - } - (TextAppend, NirKind::TextLit(x), _) => ret_kind(NirKind::TextLit( - x.concat(&TextLit::interpolate(y.clone())), - )), - (TextAppend, _, NirKind::TextLit(y)) => ret_kind(NirKind::TextLit( - TextLit::interpolate(x.clone()).concat(y), - )), - - (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - ret_ref(x) - } - (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - ret_ref(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_kind(RecordLit(kvs)) - } - (RightBiasedRecordMerge, _, _) if x == y => ret_ref(y), - - (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - ret_ref(x) - } - (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - ret_ref(y) - } - (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| { - Nir::from_partial_expr(ExprKind::Op(OpKind::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), - ))) - }); - ret_kind(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::Op(OpKind::BinOp( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - ))) - }, - ); - ret_kind(RecordType(kts)) - } - - (Equivalence, _, _) => { - ret_kind(NirKind::Equivalence(x.clone(), y.clone())) - } - - _ => ret_op(OpKind::BinOp(o, x.clone(), y.clone())), - } -} - -fn normalize_field(v: &Nir, field: &Label) -> Ret { - use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge}; - use NirKind::{Op, RecordLit, UnionConstructor, UnionType}; - use OpKind::{BinOp, Field, Projection}; - let nothing_to_do = || ret_op(Field(v.clone(), field.clone())); - - match v.kind() { - RecordLit(kvs) => match kvs.get(field) { - Some(r) => ret_ref(r), - None => nothing_to_do(), - }, - UnionType(kts) => { - ret_kind(UnionConstructor(field.clone(), kts.clone())) - } - Op(Projection(x, _)) => normalize_field(x, field), - Op(BinOp(RightBiasedRecordMerge, x, y)) => match (x.kind(), y.kind()) { - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_ref(r), - None => normalize_field(x, field), - }, - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(Op(BinOp( - RightBiasedRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ))), - field.clone(), - )), - None => normalize_field(y, field), - }, - _ => nothing_to_do(), - }, - Op(BinOp(RecursiveRecordMerge, x, y)) => match (x.kind(), y.kind()) { - (RecordLit(kvs), _) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(Op(BinOp( - RecursiveRecordMerge, - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - y.clone(), - ))), - field.clone(), - )), - None => normalize_field(y, field), - }, - (_, RecordLit(kvs)) => match kvs.get(field) { - Some(r) => ret_op(Field( - Nir::from_kind(Op(BinOp( - RecursiveRecordMerge, - x.clone(), - Nir::from_kind(RecordLit( - Some((field.clone(), r.clone())) - .into_iter() - .collect(), - )), - ))), - field.clone(), - )), - None => normalize_field(x, field), - }, - _ => nothing_to_do(), - }, - _ => nothing_to_do(), - } -} - -fn normalize_operation(opkind: &OpKind) -> Ret { - use NirKind::{ - EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, Op, - RecordLit, RecordType, UnionConstructor, UnionLit, - }; - use NumKind::Bool; - use OpKind::*; - let nothing_to_do = || ret_op(opkind.clone()); - - match opkind { - App(v, a) => ret_kind(v.app_to_kind(a.clone())), - BinOp(o, x, y) => normalize_binop(*o, x, y), - BoolIf(b, e1, e2) => { - match b.kind() { - Num(Bool(true)) => ret_ref(e1), - Num(Bool(false)) => ret_ref(e2), - _ => { - match (e1.kind(), e2.kind()) { - // Simplify `if b then True else False` - (Num(Bool(true)), Num(Bool(false))) => ret_ref(b), - _ if e1 == e2 => ret_ref(e1), - _ => nothing_to_do(), - } - } - } - } - Merge(handlers, variant, _) => match handlers.kind() { - RecordLit(kvs) => match variant.kind() { - UnionConstructor(l, _) => match kvs.get(l) { - Some(h) => ret_ref(h), - None => nothing_to_do(), - }, - UnionLit(l, v, _) => match kvs.get(l) { - Some(h) => ret_kind(h.app_to_kind(v.clone())), - None => nothing_to_do(), - }, - EmptyOptionalLit(_) => match kvs.get(&"None".into()) { - Some(h) => ret_ref(h), - None => nothing_to_do(), - }, - NEOptionalLit(v) => match kvs.get(&"Some".into()) { - Some(h) => ret_kind(h.app_to_kind(v.clone())), - None => nothing_to_do(), - }, - _ => nothing_to_do(), - }, - _ => nothing_to_do(), - }, - ToMap(v, annot) => match v.kind() { - RecordLit(kvs) if kvs.is_empty() => { - match annot.as_ref().map(|v| v.kind()) { - Some(NirKind::ListType(t)) => { - ret_kind(EmptyListLit(t.clone())) - } - _ => nothing_to_do(), - } - } - RecordLit(kvs) => ret_kind(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(), - )), - _ => nothing_to_do(), - }, - Field(v, field) => normalize_field(v, field), - Projection(_, ls) if ls.is_empty() => { - ret_kind(RecordLit(HashMap::new())) - } - Projection(v, ls) => match v.kind() { - RecordLit(kvs) => ret_kind(RecordLit( - ls.iter() - .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone()))) - .collect(), - )), - Op(Projection(v2, _)) => { - normalize_operation(&Projection(v2.clone(), ls.clone())) - } - _ => nothing_to_do(), - }, - ProjectionByExpr(v, t) => match t.kind() { - RecordType(kts) => normalize_operation(&Projection( - v.clone(), - kts.keys().cloned().collect(), - )), - _ => nothing_to_do(), - }, - Completion(..) => { - unreachable!("This case should have been handled in resolution") - } - } -} - pub fn normalize_one_layer(expr: ExprKind, env: &NzEnv) -> NirKind { use NirKind::{ Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType, diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index 3e0022f..bbcd240 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -6,12 +6,13 @@ use url::Url; use crate::error::ErrorBuilder; use crate::error::{Error, ImportError}; +use crate::operations::OpKind; use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type}; use crate::syntax; use crate::syntax::map::DupTreeMap; use crate::syntax::{ BinOp, Builtin, Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, - ImportTarget, OpKind, Span, UnspannedExpr, URL, + ImportTarget, Span, UnspannedExpr, URL, }; use crate::{Parsed, Resolved}; diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 427b39d..7481f07 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -1,51 +1,15 @@ -use std::borrow::Cow; use std::cmp::max; use std::collections::HashMap; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; -use crate::semantics::merge_maps; +use crate::operations::typecheck_operation; use crate::semantics::{ - type_of_builtin, Binder, Closure, Hir, HirKind, Nir, NirKind, Tir, TyEnv, - Type, + type_of_builtin, Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type, }; use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, OpKind, - Span, + Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span, }; -fn check_rectymerge( - span: &Span, - env: &TyEnv, - x: Nir, - y: Nir, -) -> Result<(), TypeError> { - let kts_x = match x.kind() { - NirKind::RecordType(kts) => kts, - _ => { - return mk_span_err( - span.clone(), - "RecordTypeMergeRequiresRecordType", - ) - } - }; - let kts_y = match y.kind() { - NirKind::RecordType(kts) => kts, - _ => { - return mk_span_err( - span.clone(), - "RecordTypeMergeRequiresRecordType", - ) - } - }; - for (k, tx) in kts_x { - if let Some(ty) = kts_y.get(k) { - // TODO: store Type in RecordType ? - check_rectymerge(span, env, tx.clone(), ty.clone())?; - } - } - Ok(()) -} - fn function_check(a: Const, b: Const) -> Const { if b == Const::Type { Const::Type @@ -66,477 +30,6 @@ pub fn mk_span_err(span: Span, msg: S) -> Result { ) } -fn type_of_binop( - env: &TyEnv, - span: Span, - op: BinOp, - l: &Tir<'_>, - r: &Tir<'_>, -) -> Result { - let span_err = |msg: &str| mk_span_err(span.clone(), msg); - use BinOp::*; - use NirKind::{ListType, RecordType}; - - Ok(match op { - RightBiasedRecordMerge => { - let x_type = l.ty(); - let y_type = r.ty(); - - // Extract the LHS record type - let kts_x = match x_type.kind() { - RecordType(kts) => kts, - _ => return span_err("MustCombineRecord"), - }; - // Extract the RHS record type - let kts_y = match y_type.kind() { - RecordType(kts) => kts, - _ => return span_err("MustCombineRecord"), - }; - - // Union the two records, prefering - // the values found in the RHS. - let kts = merge_maps(kts_x, kts_y, |_, _, r_t| r_t.clone()); - - let u = max(l.ty().ty(), r.ty().ty()); - Nir::from_kind(RecordType(kts)).to_type(u) - } - RecursiveRecordMerge => { - check_rectymerge(&span, env, l.ty().to_nir(), r.ty().to_nir())?; - - let hir = Hir::new( - HirKind::Expr(ExprKind::Op(OpKind::BinOp( - RecursiveRecordTypeMerge, - l.ty().to_hir(env.as_varenv()), - r.ty().to_hir(env.as_varenv()), - ))), - span.clone(), - ); - let x_u = l.ty().ty(); - let y_u = r.ty().ty(); - Type::new(hir.eval(env), max(x_u, y_u)) - } - RecursiveRecordTypeMerge => { - check_rectymerge(&span, env, l.eval(env), r.eval(env))?; - - // A RecordType's type is always a const - let xk = l.ty().as_const().unwrap(); - let yk = r.ty().as_const().unwrap(); - Type::from_const(max(xk, yk)) - } - ListAppend => { - match l.ty().kind() { - ListType(..) => {} - _ => return span_err("BinOpTypeMismatch"), - } - - if l.ty() != r.ty() { - return span_err("BinOpTypeMismatch"); - } - - l.ty().clone() - } - Equivalence => { - if l.ty() != r.ty() { - return span_err("EquivalenceTypeMismatch"); - } - if l.ty().ty().as_const() != Some(Const::Type) { - return span_err("EquivalenceArgumentsMustBeTerms"); - } - - Type::from_const(Const::Type) - } - op => { - let t = Type::from_builtin(match op { - BoolAnd | BoolOr | BoolEQ | BoolNE => Builtin::Bool, - NaturalPlus | NaturalTimes => Builtin::Natural, - TextAppend => Builtin::Text, - ListAppend - | RightBiasedRecordMerge - | RecursiveRecordMerge - | RecursiveRecordTypeMerge - | Equivalence => unreachable!(), - ImportAlt => unreachable!("ImportAlt leftover in tck"), - }); - - if *l.ty() != t { - return span_err("BinOpTypeMismatch"); - } - - if *r.ty() != t { - return span_err("BinOpTypeMismatch"); - } - - t - } - }) -} - -fn type_of_merge( - env: &TyEnv, - span: Span, - record: &Tir<'_>, - scrut: &Tir<'_>, - type_annot: Option<&Tir<'_>>, -) -> Result { - let span_err = |msg: &str| mk_span_err(span.clone(), msg); - use NirKind::{OptionalType, PiClosure, RecordType, UnionType}; - - let record_type = record.ty(); - let handlers = match record_type.kind() { - RecordType(kts) => kts, - _ => return span_err("Merge1ArgMustBeRecord"), - }; - - let scrut_type = scrut.ty(); - let variants = match scrut_type.kind() { - UnionType(kts) => Cow::Borrowed(kts), - OptionalType(ty) => { - let mut kts = HashMap::new(); - kts.insert("None".into(), None); - kts.insert("Some".into(), Some(ty.clone())); - Cow::Owned(kts) - } - _ => return span_err("Merge2ArgMustBeUnionOrOptional"), - }; - - let mut inferred_type = None; - for (x, handler_type) in handlers { - let handler_return_type: Type = match variants.get(x) { - // Union alternative with type - Some(Some(variant_type)) => match handler_type.kind() { - PiClosure { closure, annot, .. } => { - if variant_type != annot { - return mkerr( - ErrorBuilder::new(format!( - "Wrong handler input type" - )) - .span_err( - span, - format!("in this merge expression",), - ) - .span_err( - record.span(), - format!( - "the handler for `{}` expects a value of \ - type: `{}`", - x, - annot.to_expr_tyenv(env) - ), - ) - .span_err( - scrut.span(), - format!( - "but the corresponding variant has type: \ - `{}`", - variant_type.to_expr_tyenv(env) - ), - ) - .format(), - ); - } - - // TODO: this actually doesn't check anything yet - match closure.remove_binder() { - Ok(v) => Type::new_infer_universe(env, v.clone())?, - Err(()) => { - return span_err("MergeReturnTypeIsDependent") - } - } - } - _ => { - return mkerr( - ErrorBuilder::new(format!( - "merge handler is not a function" - )) - .span_err(span, format!("in this merge expression")) - .span_err( - record.span(), - format!( - "the handler for `{}` has type: `{}`", - x, - handler_type.to_expr_tyenv(env) - ), - ) - .span_help( - scrut.span(), - format!( - "the corresponding variant has type: `{}`", - variant_type.to_expr_tyenv(env) - ), - ) - .help(format!( - "a handler for this variant must be a function \ - that takes an input of type: `{}`", - variant_type.to_expr_tyenv(env) - )) - .format(), - ) - } - }, - // Union alternative without type - Some(None) => Type::new_infer_universe(env, handler_type.clone())?, - None => return span_err("MergeHandlerMissingVariant"), - }; - match &inferred_type { - None => inferred_type = Some(handler_return_type), - Some(t) => { - if t != &handler_return_type { - return span_err("MergeHandlerTypeMismatch"); - } - } - } - } - for x in variants.keys() { - if !handlers.contains_key(x) { - return span_err("MergeVariantMissingHandler"); - } - } - - let type_annot = type_annot - .as_ref() - .map(|t| t.eval_to_type(env)) - .transpose()?; - Ok(match (inferred_type, type_annot) { - (Some(t1), Some(t2)) => { - if t1 != t2 { - return span_err("MergeAnnotMismatch"); - } - t1 - } - (Some(t), None) => t, - (None, Some(t)) => t, - (None, None) => return span_err("MergeEmptyNeedsAnnotation"), - }) -} - -fn type_of_operation( - env: &TyEnv, - span: Span, - opkind: &OpKind>, -) -> Result { - let span_err = |msg: &str| mk_span_err(span.clone(), msg); - use NirKind::{ListType, PiClosure, RecordType, UnionType}; - use OpKind::*; - - Ok(match opkind { - App(f, arg) => { - match f.ty().kind() { - // TODO: store Type in closure - PiClosure { annot, closure, .. } => { - if arg.ty().as_nir() != annot { - return mkerr( - ErrorBuilder::new(format!( - "wrong type of function argument" - )) - .span_err( - f.span(), - format!( - "this expects an argument of type: {}", - annot.to_expr_tyenv(env), - ), - ) - .span_err( - arg.span(), - format!( - "but this has type: {}", - arg.ty().to_expr_tyenv(env), - ), - ) - .note(format!( - "expected type `{}`\n found type `{}`", - annot.to_expr_tyenv(env), - arg.ty().to_expr_tyenv(env), - )) - .format(), - ); - } - - let arg_nf = arg.eval(env); - Type::new_infer_universe(env, closure.apply(arg_nf))? - } - _ => return mkerr( - ErrorBuilder::new(format!( - "expected function, found `{}`", - f.ty().to_expr_tyenv(env) - )) - .span_err( - f.span(), - format!("function application requires a function",), - ) - .format(), - ), - } - } - BinOp(o, l, r) => type_of_binop(env, span, *o, l, r)?, - BoolIf(x, y, z) => { - if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) { - return span_err("InvalidPredicate"); - } - if y.ty().ty().as_const() != Some(Const::Type) { - return span_err("IfBranchMustBeTerm"); - } - if y.ty() != z.ty() { - return span_err("IfBranchMismatch"); - } - - y.ty().clone() - } - Merge(record, scrut, type_annot) => { - type_of_merge(env, span, record, scrut, type_annot.as_ref())? - } - ToMap(record, annot) => { - if record.ty().ty().as_const() != Some(Const::Type) { - return span_err("`toMap` only accepts records of type `Type`"); - } - let record_t = record.ty(); - let kts = match record_t.kind() { - RecordType(kts) => kts, - _ => { - return span_err("The argument to `toMap` must be a record") - } - }; - - if kts.is_empty() { - let annot = if let Some(annot) = annot { - annot - } else { - return span_err( - "`toMap` applied to an empty record requires a type \ - annotation", - ); - }; - let annot_val = annot.eval_to_type(env)?; - - let err_msg = "The type of `toMap x` must be of the form \ - `List { mapKey : Text, mapValue : T }`"; - let arg = match annot_val.kind() { - ListType(t) => t, - _ => return span_err(err_msg), - }; - let kts = match arg.kind() { - RecordType(kts) => kts, - _ => return span_err(err_msg), - }; - if kts.len() != 2 { - return span_err(err_msg); - } - match kts.get(&"mapKey".into()) { - Some(t) if *t == Nir::from_builtin(Builtin::Text) => {} - _ => return span_err(err_msg), - } - match kts.get(&"mapValue".into()) { - Some(_) => {} - None => return span_err(err_msg), - } - annot_val - } else { - let entry_type = kts.iter().next().unwrap().1.clone(); - for (_, t) in kts.iter() { - if *t != entry_type { - return span_err( - "Every field of the record must have the same type", - ); - } - } - - let mut kts = HashMap::new(); - kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text)); - kts.insert("mapValue".into(), entry_type); - let output_type: Type = Nir::from_builtin(Builtin::List) - .app(Nir::from_kind(RecordType(kts))) - .to_type(Const::Type); - if let Some(annot) = annot { - let annot_val = annot.eval_to_type(env)?; - if output_type != annot_val { - return span_err("Annotation mismatch"); - } - } - output_type - } - } - Field(scrut, x) => { - match scrut.ty().kind() { - RecordType(kts) => match kts.get(&x) { - Some(val) => Type::new_infer_universe(env, val.clone())?, - None => return span_err("MissingRecordField"), - }, - NirKind::Const(_) => { - let scrut = scrut.eval_to_type(env)?; - match scrut.kind() { - UnionType(kts) => match kts.get(x) { - // Constructor has type T -> < x: T, ... > - Some(Some(ty)) => Nir::from_kind(PiClosure { - binder: Binder::new(x.clone()), - annot: ty.clone(), - closure: Closure::new_constant(scrut.to_nir()), - }) - .to_type(scrut.ty()), - Some(None) => scrut, - None => return span_err("MissingUnionField"), - }, - _ => return span_err("NotARecord"), - } - } - _ => return span_err("NotARecord"), - } - } - Projection(record, labels) => { - let record_type = record.ty(); - let kts = match record_type.kind() { - RecordType(kts) => kts, - _ => return span_err("ProjectionMustBeRecord"), - }; - - let mut new_kts = HashMap::new(); - for l in labels { - match kts.get(l) { - None => return span_err("ProjectionMissingEntry"), - Some(t) => { - use std::collections::hash_map::Entry; - match new_kts.entry(l.clone()) { - Entry::Occupied(_) => { - return span_err("ProjectionDuplicateField") - } - Entry::Vacant(e) => e.insert(t.clone()), - } - } - }; - } - - Type::new_infer_universe(env, Nir::from_kind(RecordType(new_kts)))? - } - ProjectionByExpr(record, selection) => { - let record_type = record.ty(); - let rec_kts = match record_type.kind() { - RecordType(kts) => kts, - _ => return span_err("ProjectionMustBeRecord"), - }; - - let selection_val = selection.eval_to_type(env)?; - let sel_kts = match selection_val.kind() { - RecordType(kts) => kts, - _ => return span_err("ProjectionByExprTakesRecordType"), - }; - - for (l, sel_ty) in sel_kts { - match rec_kts.get(l) { - Some(rec_ty) => { - if rec_ty != sel_ty { - return span_err("ProjectionWrongType"); - } - } - None => return span_err("ProjectionMissingEntry"), - } - } - - selection_val - } - Completion(..) => { - unreachable!("This case should have been handled in resolution") - } - }) -} - /// When all sub-expressions have been typed, check the remaining toplevel /// layer. fn type_one_layer( @@ -690,7 +183,7 @@ fn type_one_layer( Type::from_const(k) } - ExprKind::Op(op) => type_of_operation(env, span, op)?, + ExprKind::Op(op) => typecheck_operation(env, span, op)?, ExprKind::Assert(t) => { let t = t.eval_to_type(env)?; match t.kind() { -- 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/builtins.rs | 494 ----------------------------------- dhall/src/semantics/mod.rs | 2 - dhall/src/semantics/nze/nir.rs | 5 +- dhall/src/semantics/tck/typecheck.rs | 5 +- 4 files changed, 5 insertions(+), 501 deletions(-) delete mode 100644 dhall/src/semantics/builtins.rs (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs deleted file mode 100644 index f65e8d1..0000000 --- a/dhall/src/semantics/builtins.rs +++ /dev/null @@ -1,494 +0,0 @@ -use crate::operations::OpKind; -use crate::semantics::{ - skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv, -}; -use crate::syntax::map::DupTreeMap; -use crate::syntax::Const::Type; -use crate::syntax::{ - BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText, - InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr, - V, -}; -use std::collections::HashMap; -use std::convert::TryInto; - -/// A partially applied builtin. -/// Invariant: the evaluation of the given args must not be able to progress further -#[derive(Debug, Clone)] -pub struct BuiltinClosure { - env: NzEnv, - b: Builtin, - /// Arguments applied to the closure so far. - args: Vec, -} - -impl BuiltinClosure { - pub fn new(b: Builtin, env: NzEnv) -> NirKind { - apply_builtin(b, Vec::new(), env) - } - pub fn apply(&self, a: Nir) -> NirKind { - use std::iter::once; - let args = self.args.iter().cloned().chain(once(a)).collect(); - apply_builtin(self.b, args, self.env.clone()) - } - pub fn to_hirkind(&self, venv: VarEnv) -> HirKind { - HirKind::Expr(self.args.iter().fold( - ExprKind::Builtin(self.b), - |acc, v| { - ExprKind::Op(OpKind::App( - Hir::new(HirKind::Expr(acc), Span::Artificial), - v.to_hir(venv), - )) - }, - )) - } -} - -pub fn rc(x: UnspannedExpr) -> Expr { - Expr::new(x, Span::Artificial) -} - -// Ad-hoc macro to help construct the types of builtins -macro_rules! make_type { - (Type) => { rc(ExprKind::Const(Const::Type)) }; - (Bool) => { rc(ExprKind::Builtin(Builtin::Bool)) }; - (Natural) => { rc(ExprKind::Builtin(Builtin::Natural)) }; - (Integer) => { rc(ExprKind::Builtin(Builtin::Integer)) }; - (Double) => { rc(ExprKind::Builtin(Builtin::Double)) }; - (Text) => { rc(ExprKind::Builtin(Builtin::Text)) }; - ($var:ident) => { - rc(ExprKind::Var(V(stringify!($var).into(), 0))) - }; - (Optional $ty:ident) => { - rc(ExprKind::Op(OpKind::App( - rc(ExprKind::Builtin(Builtin::Optional)), - make_type!($ty) - ))) - }; - (List $($rest:tt)*) => { - rc(ExprKind::Op(OpKind::App( - rc(ExprKind::Builtin(Builtin::List)), - make_type!($($rest)*) - ))) - }; - ({ $($label:ident : $ty:ident),* }) => {{ - let mut kts = DupTreeMap::new(); - $( - kts.insert( - Label::from(stringify!($label)), - make_type!($ty), - ); - )* - rc(ExprKind::RecordType(kts)) - }}; - ($ty:ident -> $($rest:tt)*) => { - rc(ExprKind::Pi( - "_".into(), - make_type!($ty), - make_type!($($rest)*) - )) - }; - (($($arg:tt)*) -> $($rest:tt)*) => { - rc(ExprKind::Pi( - "_".into(), - make_type!($($arg)*), - make_type!($($rest)*) - )) - }; - (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - rc(ExprKind::Pi( - stringify!($var).into(), - make_type!($($ty)*), - make_type!($($rest)*) - )) - }; -} - -pub fn type_of_builtin(b: Builtin) -> Hir { - use Builtin::*; - let expr = match b { - Bool | Natural | Integer | Double | Text => make_type!(Type), - List | Optional => make_type!( - Type -> Type - ), - - NaturalFold => make_type!( - Natural -> - forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural - ), - NaturalBuild => make_type!( - (forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural) -> - Natural - ), - NaturalIsZero | NaturalEven | NaturalOdd => make_type!( - Natural -> Bool - ), - NaturalToInteger => make_type!(Natural -> Integer), - NaturalShow => make_type!(Natural -> Text), - NaturalSubtract => make_type!(Natural -> Natural -> Natural), - - IntegerToDouble => make_type!(Integer -> Double), - IntegerShow => make_type!(Integer -> Text), - IntegerNegate => make_type!(Integer -> Integer), - IntegerClamp => make_type!(Integer -> Natural), - - DoubleShow => make_type!(Double -> Text), - TextShow => make_type!(Text -> Text), - - ListBuild => make_type!( - forall (a: Type) -> - (forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list) -> - List a - ), - ListFold => make_type!( - forall (a: Type) -> - (List a) -> - forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list - ), - ListLength => make_type!(forall (a: Type) -> (List a) -> Natural), - ListHead | ListLast => { - make_type!(forall (a: Type) -> (List a) -> Optional a) - } - ListIndexed => make_type!( - forall (a: Type) -> - (List a) -> - List { index: Natural, value: a } - ), - ListReverse => make_type!( - forall (a: Type) -> (List a) -> List a - ), - - OptionalBuild => make_type!( - forall (a: Type) -> - (forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional) -> - Optional a - ), - OptionalFold => make_type!( - forall (a: Type) -> - (Optional a) -> - forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional - ), - OptionalNone => make_type!( - forall (A: Type) -> Optional A - ), - }; - skip_resolve_expr(&expr).unwrap() -} - -// Ad-hoc macro to help construct closures -macro_rules! make_closure { - (var($var:ident)) => {{ - rc(ExprKind::Var(V( - Label::from(stringify!($var)).into(), - 0 - ))) - }}; - (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{ - let var = Label::from(stringify!($var)); - let ty = make_closure!($($ty)*); - let body = make_closure!($($body)*); - rc(ExprKind::Lam(var, ty, body)) - }}; - (Type) => { - rc(ExprKind::Const(Type)) - }; - (Natural) => { - rc(ExprKind::Builtin(Builtin::Natural)) - }; - (List $($ty:tt)*) => {{ - let ty = make_closure!($($ty)*); - rc(ExprKind::Op(OpKind::App( - rc(ExprKind::Builtin(Builtin::List)), - ty - ))) - }}; - (Some($($v:tt)*)) => { - rc(ExprKind::SomeLit( - make_closure!($($v)*) - )) - }; - (1 + $($v:tt)*) => { - rc(ExprKind::Op(OpKind::BinOp( - BinOp::NaturalPlus, - make_closure!($($v)*), - rc(ExprKind::Num(NumKind::Natural(1))) - ))) - }; - ([ $($head:tt)* ] # $($tail:tt)*) => {{ - let head = make_closure!($($head)*); - let tail = make_closure!($($tail)*); - rc(ExprKind::Op(OpKind::BinOp( - BinOp::ListAppend, - rc(ExprKind::NEListLit(vec![head])), - tail, - ))) - }}; -} - -#[allow(clippy::cognitive_complexity)] -fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { - use NirKind::*; - use NumKind::{Bool, Double, Integer, Natural}; - - // Small helper enum - enum Ret { - NirKind(NirKind), - Nir(Nir), - DoneAsIs, - } - let make_closure = |e| { - typecheck(&skip_resolve_expr(&e).unwrap()) - .unwrap() - .eval(env.clone()) - }; - - let ret = match (b, args.as_slice()) { - (Builtin::Bool, []) - | (Builtin::Natural, []) - | (Builtin::Integer, []) - | (Builtin::Double, []) - | (Builtin::Text, []) => Ret::NirKind(BuiltinType(b)), - (Builtin::Optional, [t]) => Ret::NirKind(OptionalType(t.clone())), - (Builtin::List, [t]) => Ret::NirKind(ListType(t.clone())), - - (Builtin::OptionalNone, [t]) => { - Ret::NirKind(EmptyOptionalLit(t.clone())) - } - (Builtin::NaturalIsZero, [n]) => match &*n.kind() { - Num(Natural(n)) => Ret::NirKind(Num(Bool(*n == 0))), - _ => Ret::DoneAsIs, - }, - (Builtin::NaturalEven, [n]) => match &*n.kind() { - Num(Natural(n)) => Ret::NirKind(Num(Bool(*n % 2 == 0))), - _ => Ret::DoneAsIs, - }, - (Builtin::NaturalOdd, [n]) => match &*n.kind() { - Num(Natural(n)) => Ret::NirKind(Num(Bool(*n % 2 != 0))), - _ => Ret::DoneAsIs, - }, - (Builtin::NaturalToInteger, [n]) => match &*n.kind() { - Num(Natural(n)) => Ret::NirKind(Num(Integer(*n as isize))), - _ => Ret::DoneAsIs, - }, - (Builtin::NaturalShow, [n]) => match &*n.kind() { - Num(Natural(n)) => Ret::Nir(Nir::from_text(n)), - _ => Ret::DoneAsIs, - }, - (Builtin::NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) { - (Num(Natural(a)), Num(Natural(b))) => { - Ret::NirKind(Num(Natural(if b > a { b - a } else { 0 }))) - } - (Num(Natural(0)), _) => Ret::Nir(b.clone()), - (_, Num(Natural(0))) => Ret::NirKind(Num(Natural(0))), - _ if a == b => Ret::NirKind(Num(Natural(0))), - _ => Ret::DoneAsIs, - }, - (Builtin::IntegerShow, [n]) => match &*n.kind() { - Num(Integer(n)) => { - let s = if *n < 0 { - n.to_string() - } else { - format!("+{}", n) - }; - Ret::Nir(Nir::from_text(s)) - } - _ => Ret::DoneAsIs, - }, - (Builtin::IntegerToDouble, [n]) => match &*n.kind() { - Num(Integer(n)) => { - Ret::NirKind(Num(Double(NaiveDouble::from(*n as f64)))) - } - _ => Ret::DoneAsIs, - }, - (Builtin::IntegerNegate, [n]) => match &*n.kind() { - Num(Integer(n)) => Ret::NirKind(Num(Integer(-n))), - _ => Ret::DoneAsIs, - }, - (Builtin::IntegerClamp, [n]) => match &*n.kind() { - Num(Integer(n)) => { - Ret::NirKind(Num(Natural((*n).try_into().unwrap_or(0)))) - } - _ => Ret::DoneAsIs, - }, - (Builtin::DoubleShow, [n]) => match &*n.kind() { - Num(Double(n)) => Ret::Nir(Nir::from_text(n)), - _ => Ret::DoneAsIs, - }, - (Builtin::TextShow, [v]) => match &*v.kind() { - TextLit(tlit) => { - if let Some(s) = tlit.as_text() { - // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText = - std::iter::once(InterpolatedTextContents::Text(s)) - .collect(); - Ret::Nir(Nir::from_text(txt)) - } else { - Ret::DoneAsIs - } - } - _ => Ret::DoneAsIs, - }, - (Builtin::ListLength, [_, l]) => match &*l.kind() { - EmptyListLit(_) => Ret::NirKind(Num(Natural(0))), - NEListLit(xs) => Ret::NirKind(Num(Natural(xs.len()))), - _ => Ret::DoneAsIs, - }, - (Builtin::ListHead, [_, l]) => match &*l.kind() { - EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => { - Ret::NirKind(NEOptionalLit(xs.iter().next().unwrap().clone())) - } - _ => Ret::DoneAsIs, - }, - (Builtin::ListLast, [_, l]) => match &*l.kind() { - EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => Ret::NirKind(NEOptionalLit( - xs.iter().rev().next().unwrap().clone(), - )), - _ => Ret::DoneAsIs, - }, - (Builtin::ListReverse, [_, l]) => match &*l.kind() { - EmptyListLit(n) => Ret::NirKind(EmptyListLit(n.clone())), - NEListLit(xs) => { - Ret::NirKind(NEListLit(xs.iter().rev().cloned().collect())) - } - _ => Ret::DoneAsIs, - }, - (Builtin::ListIndexed, [t, l]) => { - match l.kind() { - EmptyListLit(_) | NEListLit(_) => { - // Construct the returned record type: { index: Natural, value: t } - let mut kts = HashMap::new(); - kts.insert( - "index".into(), - Nir::from_builtin(Builtin::Natural), - ); - kts.insert("value".into(), t.clone()); - let t = Nir::from_kind(RecordType(kts)); - - // Construct the new list, with added indices - let list = match l.kind() { - EmptyListLit(_) => EmptyListLit(t), - NEListLit(xs) => NEListLit( - xs.iter() - .enumerate() - .map(|(i, e)| { - let mut kvs = HashMap::new(); - kvs.insert( - "index".into(), - Nir::from_kind(Num(Natural(i))), - ); - kvs.insert("value".into(), e.clone()); - Nir::from_kind(RecordLit(kvs)) - }) - .collect(), - ), - _ => unreachable!(), - }; - Ret::NirKind(list) - } - _ => Ret::DoneAsIs, - } - } - (Builtin::ListBuild, [t, f]) => { - let list_t = Nir::from_builtin(Builtin::List).app(t.clone()); - Ret::Nir( - f.app(list_t) - .app( - make_closure(make_closure!( - λ(T : Type) -> - λ(a : var(T)) -> - λ(as : List var(T)) -> - [ var(a) ] # var(as) - )) - .app(t.clone()), - ) - .app(EmptyListLit(t.clone()).into_nir()), - ) - } - (Builtin::ListFold, [_, l, _, cons, nil]) => match &*l.kind() { - EmptyListLit(_) => Ret::Nir(nil.clone()), - NEListLit(xs) => { - let mut v = nil.clone(); - for x in xs.iter().cloned().rev() { - v = cons.app(x).app(v); - } - Ret::Nir(v) - } - _ => Ret::DoneAsIs, - }, - (Builtin::OptionalBuild, [t, f]) => { - let optional_t = - Nir::from_builtin(Builtin::Optional).app(t.clone()); - Ret::Nir( - f.app(optional_t) - .app( - make_closure(make_closure!( - λ(T : Type) -> - λ(a : var(T)) -> - Some(var(a)) - )) - .app(t.clone()), - ) - .app(EmptyOptionalLit(t.clone()).into_nir()), - ) - } - (Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() { - EmptyOptionalLit(_) => Ret::Nir(nothing.clone()), - NEOptionalLit(x) => Ret::Nir(just.app(x.clone())), - _ => Ret::DoneAsIs, - }, - (Builtin::NaturalBuild, [f]) => Ret::Nir( - f.app(Nir::from_builtin(Builtin::Natural)) - .app(make_closure(make_closure!( - λ(x : Natural) -> - 1 + var(x) - ))) - .app(Num(Natural(0)).into_nir()), - ), - - (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() { - Num(Natural(0)) => Ret::Nir(zero.clone()), - Num(Natural(n)) => { - let fold = Nir::from_builtin(Builtin::NaturalFold) - .app(Num(Natural(n - 1)).into_nir()) - .app(t.clone()) - .app(succ.clone()) - .app(zero.clone()); - Ret::Nir(succ.app(fold)) - } - _ => Ret::DoneAsIs, - }, - _ => Ret::DoneAsIs, - }; - match ret { - Ret::NirKind(v) => v, - Ret::Nir(v) => v.kind().clone(), - Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, env }), - } -} - -impl std::cmp::PartialEq for BuiltinClosure { - fn eq(&self, other: &Self) -> bool { - self.b == other.b && self.args == other.args - } -} -impl std::cmp::Eq for BuiltinClosure {} diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 468d8b1..a488c31 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,9 +1,7 @@ -pub mod builtins; pub mod nze; pub mod parse; pub mod resolve; pub mod tck; -pub use self::builtins::*; pub use self::nze::*; pub use self::resolve::*; pub use self::tck::*; 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, diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 7481f07..a31f15c 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -1,11 +1,10 @@ use std::cmp::max; use std::collections::HashMap; +use crate::builtins::type_of_builtin; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::operations::typecheck_operation; -use crate::semantics::{ - type_of_builtin, Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type, -}; +use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type}; use crate::syntax::{ Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span, }; -- 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 +++---- dhall/src/semantics/resolve/resolve.rs | 7 ++++--- dhall/src/semantics/tck/tir.rs | 3 ++- dhall/src/semantics/tck/typecheck.rs | 6 ++---- 4 files changed, 11 insertions(+), 12 deletions(-) (limited to 'dhall/src/semantics') 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; diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index bbcd240..cd5232a 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -4,15 +4,16 @@ use std::env; use std::path::PathBuf; use url::Url; +use crate::builtins::Builtin; use crate::error::ErrorBuilder; use crate::error::{Error, ImportError}; -use crate::operations::OpKind; +use crate::operations::{BinOp, OpKind}; use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type}; use crate::syntax; use crate::syntax::map::DupTreeMap; use crate::syntax::{ - BinOp, Builtin, Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, - ImportTarget, Span, UnspannedExpr, URL, + Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, Span, + UnspannedExpr, URL, }; use crate::{Parsed, Resolved}; diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs index 89a8027..ec15a1f 100644 --- a/dhall/src/semantics/tck/tir.rs +++ b/dhall/src/semantics/tck/tir.rs @@ -1,6 +1,7 @@ +use crate::builtins::Builtin; use crate::error::{ErrorBuilder, TypeError}; use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv}; -use crate::syntax::{Builtin, Const, Expr, Span}; +use crate::syntax::{Const, Expr, Span}; /// The type of a type. 0 is `Type`, 1 is `Kind`, etc... #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)] diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index a31f15c..c6300d9 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -1,13 +1,11 @@ use std::cmp::max; use std::collections::HashMap; -use crate::builtins::type_of_builtin; +use crate::builtins::{type_of_builtin, Builtin}; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::operations::typecheck_operation; use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type}; -use crate::syntax::{ - Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span, -}; +use crate::syntax::{Const, ExprKind, InterpolatedTextContents, NumKind, Span}; fn function_check(a: Const, b: Const) -> Const { if b == Const::Type { -- cgit v1.2.3 From 092b7208ffd22f8facc7af387ac307e59208d52c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 7 Apr 2020 11:19:36 +0100 Subject: Move duplicate field checking to parser --- dhall/src/semantics/resolve/resolve.rs | 4 +-- dhall/src/semantics/tck/typecheck.rs | 61 ++++++++++++---------------------- 2 files changed, 24 insertions(+), 41 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index cd5232a..e96f16b 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -1,5 +1,6 @@ use itertools::Itertools; use std::borrow::Cow; +use std::collections::BTreeMap; use std::env; use std::path::PathBuf; use url::Url; @@ -10,7 +11,6 @@ use crate::error::{Error, ImportError}; use crate::operations::{BinOp, OpKind}; use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type}; use crate::syntax; -use crate::syntax::map::DupTreeMap; use crate::syntax::{ Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, Span, UnspannedExpr, URL, @@ -199,7 +199,7 @@ fn mkexpr(kind: UnspannedExpr) -> Expr { fn make_aslocation_uniontype() -> Expr { let text_type = mkexpr(ExprKind::Builtin(Builtin::Text)); - let mut union = DupTreeMap::default(); + let mut union = BTreeMap::default(); union.insert("Local".into(), Some(text_type.clone())); union.insert("Remote".into(), Some(text_type.clone())); union.insert("Environment".into(), Some(text_type)); diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index c6300d9..45a3055 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -1,5 +1,4 @@ use std::cmp::max; -use std::collections::HashMap; use crate::builtins::{type_of_builtin, Builtin}; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; @@ -107,71 +106,55 @@ fn type_one_layer( Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type) } ExprKind::RecordLit(kvs) => { - use std::collections::hash_map::Entry; - let mut kts = HashMap::new(); // An empty record type has type Type let mut k = Const::Type; - for (x, v) in kvs { - // Check for duplicated entries - match kts.entry(x.clone()) { - Entry::Occupied(_) => { - return span_err("RecordTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(v.ty().to_nir()), - }; - + for (_, v) in kvs { // Check that the fields have a valid kind match v.ty().ty().as_const() { Some(c) => k = max(k, c), - None => return span_err("InvalidFieldType"), + None => return mk_span_err(v.span(), "InvalidFieldType"), } } + let kts = kvs + .iter() + .map(|(x, v)| (x.clone(), v.ty().to_nir())) + .collect(); + Nir::from_kind(NirKind::RecordType(kts)).to_type(k) } ExprKind::RecordType(kts) => { - use std::collections::hash_map::Entry; - let mut seen_fields = HashMap::new(); // An empty record type has type Type let mut k = Const::Type; - - for (x, t) in kts { - // Check for duplicated entries - match seen_fields.entry(x.clone()) { - Entry::Occupied(_) => { - return span_err("RecordTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(()), - }; - + for (_, t) in kts { // Check the type is a Const and compute final type match t.ty().as_const() { Some(c) => k = max(k, c), - None => return span_err("InvalidFieldType"), + None => return mk_span_err(t.span(), "InvalidFieldType"), } } Type::from_const(k) } ExprKind::UnionType(kts) => { - use std::collections::hash_map::Entry; - let mut seen_fields = HashMap::new(); // Check that all types are the same const let mut k = None; - for (x, t) in kts { + for (_, t) in kts { if let Some(t) = t { - match (k, t.ty().as_const()) { - (None, Some(k2)) => k = Some(k2), - (Some(k1), Some(k2)) if k1 == k2 => {} - _ => return span_err("InvalidFieldType"), + let c = match t.ty().as_const() { + Some(c) => c, + None => { + return mk_span_err(t.span(), "InvalidVariantType") + } + }; + match k { + None => k = Some(c), + Some(k) if k == c => {} + _ => { + return mk_span_err(t.span(), "InvalidVariantType") + } } } - match seen_fields.entry(x) { - Entry::Occupied(_) => { - return span_err("UnionTypeDuplicateField") - } - Entry::Vacant(e) => e.insert(()), - }; } // An empty union type has type Type; -- cgit v1.2.3 From 214a3c998a3358849495b54a60d46f626b131f0a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 7 Apr 2020 12:07:59 +0100 Subject: Clippy --- dhall/src/semantics/tck/typecheck.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 45a3055..361e1b4 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -108,7 +108,7 @@ fn type_one_layer( ExprKind::RecordLit(kvs) => { // An empty record type has type Type let mut k = Const::Type; - for (_, v) in kvs { + for v in kvs.values() { // Check that the fields have a valid kind match v.ty().ty().as_const() { Some(c) => k = max(k, c), @@ -126,7 +126,7 @@ fn type_one_layer( ExprKind::RecordType(kts) => { // An empty record type has type Type let mut k = Const::Type; - for (_, t) in kts { + for t in kts.values() { // Check the type is a Const and compute final type match t.ty().as_const() { Some(c) => k = max(k, c), @@ -139,7 +139,7 @@ fn type_one_layer( ExprKind::UnionType(kts) => { // Check that all types are the same const let mut k = None; - for (_, t) in kts { + for t in kts.values() { if let Some(t) = t { let c = match t.ty().as_const() { Some(c) => c, -- cgit v1.2.3