summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/builtins.rs493
-rw-r--r--dhall/src/semantics/mod.rs2
-rw-r--r--dhall/src/semantics/nze/nir.rs84
-rw-r--r--dhall/src/semantics/nze/normalize.rs406
-rw-r--r--dhall/src/semantics/resolve/resolve.rs29
-rw-r--r--dhall/src/semantics/tck/tir.rs3
-rw-r--r--dhall/src/semantics/tck/typecheck.rs603
7 files changed, 161 insertions, 1459 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
deleted file mode 100644
index 6007a92..0000000
--- a/dhall/src/semantics/builtins.rs
+++ /dev/null
@@ -1,493 +0,0 @@
-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<Nir>,
-}
-
-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::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::App(
- rc(ExprKind::Builtin(Builtin::Optional)),
- make_type!($ty)
- ))
- };
- (List $($rest:tt)*) => {
- rc(ExprKind::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::App(
- rc(ExprKind::Builtin(Builtin::List)),
- ty
- ))
- }};
- (Some($($v:tt)*)) => {
- rc(ExprKind::SomeLit(
- make_closure!($($v)*)
- ))
- };
- (1 + $($v:tt)*) => {
- rc(ExprKind::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(
- BinOp::ListAppend,
- rc(ExprKind::NEListLit(vec![head])),
- tail,
- ))
- }};
-}
-
-#[allow(clippy::cognitive_complexity)]
-fn apply_builtin(b: Builtin, args: Vec<Nir>, 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<Expr> =
- 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 e0d227e..12f1b14 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -1,14 +1,15 @@
use std::collections::HashMap;
use std::rc::Rc;
+use crate::builtins::{Builtin, BuiltinClosure};
+use crate::operations::{BinOp, OpKind};
use crate::semantics::nze::lazy;
use crate::semantics::{
- apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
- BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
+ apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder, Hir,
+ HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
};
use crate::syntax::{
- BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
- NumKind, Span,
+ Const, Expr, ExprKind, InterpolatedTextContents, Label, NumKind, Span,
};
use crate::ToExprOptions;
@@ -74,25 +75,27 @@ pub enum NirKind {
Var(NzVar),
Const(Const),
+ Num(NumKind),
// Must be a number type, Bool or Text
BuiltinType(Builtin),
- Num(NumKind),
- OptionalType(Nir),
+ TextLit(TextLit),
EmptyOptionalLit(Nir),
NEOptionalLit(Nir),
- ListType(Nir),
+ OptionalType(Nir),
// EmptyListLit(t) means `[] : List t`, not `[] : t`
EmptyListLit(Nir),
NEListLit(Vec<Nir>),
- RecordType(HashMap<Label, Nir>),
+ ListType(Nir),
RecordLit(HashMap<Label, Nir>),
- UnionType(HashMap<Label, Option<Nir>>),
+ RecordType(HashMap<Label, Nir>),
UnionConstructor(Label, HashMap<Label, Option<Nir>>),
UnionLit(Label, Nir, HashMap<Label, Option<Nir>>),
- TextLit(TextLit),
+ UnionType(HashMap<Label, Option<Nir>>),
Equivalence(Nir, Nir),
- /// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
- PartialExpr(ExprKind<Nir>),
+ Assert(Nir),
+ /// Invariant: evaluation must not be able to progress with `normalize_operation`.
+ /// This is used when an operation couldn't proceed further, for example because of variables.
+ Op(OpKind<Nir>),
}
impl Nir {
@@ -111,8 +114,7 @@ impl Nir {
NirInternal::from_whnf(v).into_nir()
}
pub fn from_const(c: Const) -> Self {
- let v = NirKind::Const(c);
- NirInternal::from_whnf(v).into_nir()
+ Self::from_kind(NirKind::Const(c))
}
pub fn from_builtin(b: Builtin) -> Self {
Self::from_builtin_env(b, &NzEnv::new())
@@ -148,7 +150,10 @@ impl Nir {
}
pub fn app(&self, v: Nir) -> Nir {
- Nir::from_kind(apply_any(self.clone(), v))
+ Nir::from_kind(self.app_to_kind(v))
+ }
+ pub fn app_to_kind(&self, v: Nir) -> NirKind {
+ apply_any(self, v)
}
pub fn to_hir(&self, venv: VarEnv) -> Hir {
@@ -190,24 +195,24 @@ impl Nir {
NirKind::Const(c) => ExprKind::Const(*c),
NirKind::BuiltinType(b) => ExprKind::Builtin(*b),
NirKind::Num(l) => ExprKind::Num(l.clone()),
- NirKind::OptionalType(t) => ExprKind::App(
+ NirKind::OptionalType(t) => ExprKind::Op(OpKind::App(
Nir::from_builtin(Builtin::Optional).to_hir(venv),
t.to_hir(venv),
- ),
- NirKind::EmptyOptionalLit(n) => ExprKind::App(
+ )),
+ NirKind::EmptyOptionalLit(n) => ExprKind::Op(OpKind::App(
Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
n.to_hir(venv),
- ),
+ )),
NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
- NirKind::ListType(t) => ExprKind::App(
+ NirKind::ListType(t) => ExprKind::Op(OpKind::App(
Nir::from_builtin(Builtin::List).to_hir(venv),
t.to_hir(venv),
- ),
+ )),
NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
- HirKind::Expr(ExprKind::App(
+ HirKind::Expr(ExprKind::Op(OpKind::App(
Nir::from_builtin(Builtin::List).to_hir(venv),
n.to_hir(venv),
- )),
+ ))),
Span::Artificial,
)),
NirKind::NEListLit(elts) => ExprKind::NEListLit(
@@ -229,32 +234,35 @@ impl Nir {
.collect(),
),
NirKind::UnionType(kts) => map_uniontype(kts),
- NirKind::UnionConstructor(l, kts) => ExprKind::Field(
- Hir::new(
- HirKind::Expr(map_uniontype(kts)),
- Span::Artificial,
- ),
- l.clone(),
- ),
- NirKind::UnionLit(l, v, kts) => ExprKind::App(
+ NirKind::UnionConstructor(l, kts) => {
+ ExprKind::Op(OpKind::Field(
+ Hir::new(
+ HirKind::Expr(map_uniontype(kts)),
+ Span::Artificial,
+ ),
+ l.clone(),
+ ))
+ }
+ NirKind::UnionLit(l, v, kts) => ExprKind::Op(OpKind::App(
Hir::new(
- HirKind::Expr(ExprKind::Field(
+ HirKind::Expr(ExprKind::Op(OpKind::Field(
Hir::new(
HirKind::Expr(map_uniontype(kts)),
Span::Artificial,
),
l.clone(),
- )),
+ ))),
Span::Artificial,
),
v.to_hir(venv),
- ),
- NirKind::Equivalence(x, y) => ExprKind::BinOp(
+ )),
+ NirKind::Equivalence(x, y) => ExprKind::Op(OpKind::BinOp(
BinOp::Equivalence,
x.to_hir(venv),
y.to_hir(venv),
- ),
- NirKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
+ )),
+ NirKind::Assert(x) => ExprKind::Assert(x.to_hir(venv)),
+ NirKind::Op(e) => ExprKind::Op(e.map_ref(|v| v.to_hir(venv))),
}),
};
@@ -307,7 +315,7 @@ impl Thunk {
}
fn eval(self) -> NirKind {
match self {
- Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
+ Thunk::Thunk { env, body } => normalize_hir(&env, &body),
Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
}
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 570e106..d042f3f 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -1,18 +1,18 @@
-use itertools::Itertools;
use std::collections::HashMap;
+use crate::operations::{normalize_operation, OpKind};
use crate::semantics::NzEnv;
use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit};
-use crate::syntax::{BinOp, ExprKind, InterpolatedTextContents, NumKind};
+use crate::syntax::{ExprKind, InterpolatedTextContents};
-pub fn apply_any(f: Nir, a: Nir) -> NirKind {
+pub fn apply_any(f: &Nir, a: Nir) -> NirKind {
match f.kind() {
NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(),
NirKind::AppliedBuiltin(closure) => closure.apply(a),
NirKind::UnionConstructor(l, kts) => {
NirKind::UnionLit(l.clone(), a, kts.clone())
}
- _ => NirKind::PartialExpr(ExprKind::App(f, a)),
+ _ => NirKind::Op(OpKind::App(f.clone(), a)),
}
}
@@ -81,393 +81,83 @@ where
kvs
}
-// Small helper enum to avoid repetition
-enum Ret<'a> {
- NirKind(NirKind),
- Nir(Nir),
- NirRef(&'a Nir),
- Expr(ExprKind<Nir>),
-}
-
-fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> {
- use BinOp::{
- BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
- NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
- RightBiasedRecordMerge, TextAppend,
- };
- use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType};
- use NumKind::{Bool, Natural};
-
- Some(match (o, x.kind(), y.kind()) {
- (BoolAnd, Num(Bool(true)), _) => Ret::NirRef(y),
- (BoolAnd, _, Num(Bool(true))) => Ret::NirRef(x),
- (BoolAnd, Num(Bool(false)), _) => Ret::NirKind(Num(Bool(false))),
- (BoolAnd, _, Num(Bool(false))) => Ret::NirKind(Num(Bool(false))),
- (BoolAnd, _, _) if x == y => Ret::NirRef(x),
- (BoolOr, Num(Bool(true)), _) => Ret::NirKind(Num(Bool(true))),
- (BoolOr, _, Num(Bool(true))) => Ret::NirKind(Num(Bool(true))),
- (BoolOr, Num(Bool(false)), _) => Ret::NirRef(y),
- (BoolOr, _, Num(Bool(false))) => Ret::NirRef(x),
- (BoolOr, _, _) if x == y => Ret::NirRef(x),
- (BoolEQ, Num(Bool(true)), _) => Ret::NirRef(y),
- (BoolEQ, _, Num(Bool(true))) => Ret::NirRef(x),
- (BoolEQ, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x == y))),
- (BoolEQ, _, _) if x == y => Ret::NirKind(Num(Bool(true))),
- (BoolNE, Num(Bool(false)), _) => Ret::NirRef(y),
- (BoolNE, _, Num(Bool(false))) => Ret::NirRef(x),
- (BoolNE, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x != y))),
- (BoolNE, _, _) if x == y => Ret::NirKind(Num(Bool(false))),
-
- (NaturalPlus, Num(Natural(0)), _) => Ret::NirRef(y),
- (NaturalPlus, _, Num(Natural(0))) => Ret::NirRef(x),
- (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => {
- Ret::NirKind(Num(Natural(x + y)))
- }
- (NaturalTimes, Num(Natural(0)), _) => Ret::NirKind(Num(Natural(0))),
- (NaturalTimes, _, Num(Natural(0))) => Ret::NirKind(Num(Natural(0))),
- (NaturalTimes, Num(Natural(1)), _) => Ret::NirRef(y),
- (NaturalTimes, _, Num(Natural(1))) => Ret::NirRef(x),
- (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => {
- Ret::NirKind(Num(Natural(x * y)))
- }
-
- (ListAppend, EmptyListLit(_), _) => Ret::NirRef(y),
- (ListAppend, _, EmptyListLit(_)) => Ret::NirRef(x),
- (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::NirKind(NEListLit(
- xs.iter().chain(ys.iter()).cloned().collect(),
- )),
-
- (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => Ret::NirRef(y),
- (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => Ret::NirRef(x),
- (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => {
- Ret::NirKind(NirKind::TextLit(x.concat(y)))
- }
- (TextAppend, NirKind::TextLit(x), _) => Ret::NirKind(NirKind::TextLit(
- x.concat(&TextLit::interpolate(y.clone())),
- )),
- (TextAppend, _, NirKind::TextLit(y)) => Ret::NirKind(NirKind::TextLit(
- TextLit::interpolate(x.clone()).concat(y),
- )),
+pub type Ret = NirKind;
- (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::NirRef(x)
- }
- (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::NirRef(y)
- }
- (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
- let mut kvs = kvs2.clone();
- for (x, v) in kvs1 {
- // Insert only if key not already present
- kvs.entry(x.clone()).or_insert_with(|| v.clone());
- }
- Ret::NirKind(RecordLit(kvs))
- }
- (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y),
-
- (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::NirRef(x)
- }
- (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::NirRef(y)
- }
- (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
- let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| {
- Nir::from_partial_expr(ExprKind::BinOp(
- RecursiveRecordMerge,
- v1.clone(),
- v2.clone(),
- ))
- });
- Ret::NirKind(RecordLit(kvs))
- }
-
- (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
- let kts = merge_maps(
- kts_x,
- kts_y,
- // If the Label exists for both records, then we hit the recursive case.
- |_, l: &Nir, r: &Nir| {
- Nir::from_partial_expr(ExprKind::BinOp(
- RecursiveRecordTypeMerge,
- l.clone(),
- r.clone(),
- ))
- },
- );
- Ret::NirKind(RecordType(kts))
- }
-
- (Equivalence, _, _) => {
- Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone()))
- }
-
- _ => return None,
- })
+pub fn ret_nir(x: Nir) -> Ret {
+ ret_ref(&x)
+}
+pub fn ret_kind(x: NirKind) -> Ret {
+ x
+}
+pub fn ret_ref(x: &Nir) -> Ret {
+ x.kind().clone()
+}
+pub fn ret_op(x: OpKind<Nir>) -> Ret {
+ NirKind::Op(x)
}
-#[allow(clippy::cognitive_complexity)]
pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
use NirKind::{
- EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num,
- PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
+ Assert, Const, NEListLit, NEOptionalLit, Num, RecordLit, RecordType,
UnionType,
};
- use NumKind::Bool;
- let ret = match expr {
- ExprKind::Import(..) | ExprKind::Completion(..) => {
- unreachable!("This case should have been handled in resolution")
- }
+ match expr {
ExprKind::Var(..)
| ExprKind::Lam(..)
| ExprKind::Pi(..)
- | ExprKind::Let(..) => unreachable!(
- "This case should have been handled in normalize_hir_whnf"
- ),
+ | ExprKind::Let(..) => {
+ unreachable!("This case should have been handled in normalize_hir")
+ }
- ExprKind::Annot(x, _) => Ret::Nir(x),
- ExprKind::Const(c) => Ret::Nir(Nir::from_const(c)),
- ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)),
- ExprKind::Assert(_) => Ret::Expr(expr),
- ExprKind::App(v, a) => Ret::Nir(v.app(a)),
- ExprKind::Num(l) => Ret::NirKind(Num(l)),
- ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)),
+ ExprKind::Const(c) => ret_kind(Const(c)),
+ ExprKind::Num(l) => ret_kind(Num(l)),
+ ExprKind::Builtin(b) => {
+ ret_kind(NirKind::from_builtin_env(b, env.clone()))
+ }
+ ExprKind::TextLit(elts) => {
+ let tlit = TextLit::new(elts.into_iter());
+ // Simplify bare interpolation
+ if let Some(v) = tlit.as_single_expr() {
+ ret_ref(v)
+ } else {
+ ret_kind(NirKind::TextLit(tlit))
+ }
+ }
+ ExprKind::SomeLit(e) => ret_kind(NEOptionalLit(e)),
ExprKind::EmptyListLit(t) => {
let arg = match t.kind() {
NirKind::ListType(t) => t.clone(),
_ => panic!("internal type error"),
};
- Ret::NirKind(NirKind::EmptyListLit(arg))
+ ret_kind(NirKind::EmptyListLit(arg))
}
ExprKind::NEListLit(elts) => {
- Ret::NirKind(NEListLit(elts.into_iter().collect()))
+ ret_kind(NEListLit(elts.into_iter().collect()))
}
ExprKind::RecordLit(kvs) => {
- Ret::NirKind(RecordLit(kvs.into_iter().collect()))
+ ret_kind(RecordLit(kvs.into_iter().collect()))
}
ExprKind::RecordType(kvs) => {
- Ret::NirKind(RecordType(kvs.into_iter().collect()))
+ ret_kind(RecordType(kvs.into_iter().collect()))
}
ExprKind::UnionType(kvs) => {
- Ret::NirKind(UnionType(kvs.into_iter().collect()))
- }
- ExprKind::TextLit(elts) => {
- let tlit = TextLit::new(elts.into_iter());
- // Simplify bare interpolation
- if let Some(v) = tlit.as_single_expr() {
- Ret::Nir(v.clone())
- } else {
- Ret::NirKind(NirKind::TextLit(tlit))
- }
- }
- ExprKind::BoolIf(ref b, ref e1, ref e2) => {
- match b.kind() {
- Num(Bool(true)) => Ret::NirRef(e1),
- Num(Bool(false)) => Ret::NirRef(e2),
- _ => {
- match (e1.kind(), e2.kind()) {
- // Simplify `if b then True else False`
- (Num(Bool(true)), Num(Bool(false))) => Ret::NirRef(b),
- _ if e1 == e2 => Ret::NirRef(e1),
- _ => Ret::Expr(expr),
- }
- }
- }
- }
- ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
- Some(ret) => ret,
- None => Ret::Expr(expr),
- },
-
- ExprKind::Field(ref v, ref field) => match v.kind() {
- RecordLit(kvs) => match kvs.get(field) {
- Some(r) => Ret::Nir(r.clone()),
- None => Ret::Expr(expr),
- },
- UnionType(kts) => {
- Ret::NirKind(UnionConstructor(field.clone(), kts.clone()))
- }
- PartialExpr(ExprKind::Projection(x, _)) => {
- return normalize_one_layer(
- ExprKind::Field(x.clone(), field.clone()),
- env,
- )
- }
- PartialExpr(ExprKind::BinOp(
- BinOp::RightBiasedRecordMerge,
- x,
- y,
- )) => match (x.kind(), y.kind()) {
- (_, RecordLit(kvs)) => match kvs.get(field) {
- Some(r) => Ret::Nir(r.clone()),
- None => {
- return normalize_one_layer(
- ExprKind::Field(x.clone(), field.clone()),
- env,
- )
- }
- },
- (RecordLit(kvs), _) => match kvs.get(field) {
- Some(r) => Ret::Expr(ExprKind::Field(
- Nir::from_kind(PartialExpr(ExprKind::BinOp(
- BinOp::RightBiasedRecordMerge,
- Nir::from_kind(RecordLit(
- Some((field.clone(), r.clone()))
- .into_iter()
- .collect(),
- )),
- y.clone(),
- ))),
- field.clone(),
- )),
- None => {
- return normalize_one_layer(
- ExprKind::Field(y.clone(), field.clone()),
- env,
- )
- }
- },
- _ => Ret::Expr(expr),
- },
- PartialExpr(ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y)) => {
- match (x.kind(), y.kind()) {
- (RecordLit(kvs), _) => match kvs.get(field) {
- Some(r) => Ret::Expr(ExprKind::Field(
- Nir::from_kind(PartialExpr(ExprKind::BinOp(
- BinOp::RecursiveRecordMerge,
- Nir::from_kind(RecordLit(
- Some((field.clone(), r.clone()))
- .into_iter()
- .collect(),
- )),
- y.clone(),
- ))),
- field.clone(),
- )),
- None => {
- return normalize_one_layer(
- ExprKind::Field(y.clone(), field.clone()),
- env,
- )
- }
- },
- (_, RecordLit(kvs)) => match kvs.get(field) {
- Some(r) => Ret::Expr(ExprKind::Field(
- Nir::from_kind(PartialExpr(ExprKind::BinOp(
- BinOp::RecursiveRecordMerge,
- x.clone(),
- Nir::from_kind(RecordLit(
- Some((field.clone(), r.clone()))
- .into_iter()
- .collect(),
- )),
- ))),
- field.clone(),
- )),
- None => {
- return normalize_one_layer(
- ExprKind::Field(x.clone(), field.clone()),
- env,
- )
- }
- },
- _ => Ret::Expr(expr),
- }
- }
- _ => Ret::Expr(expr),
- },
- ExprKind::Projection(_, ref ls) if ls.is_empty() => {
- Ret::NirKind(RecordLit(HashMap::new()))
+ ret_kind(UnionType(kvs.into_iter().collect()))
}
- ExprKind::Projection(ref v, ref ls) => match v.kind() {
- RecordLit(kvs) => Ret::NirKind(RecordLit(
- ls.iter()
- .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
- .collect(),
- )),
- PartialExpr(ExprKind::Projection(v2, _)) => {
- return normalize_one_layer(
- ExprKind::Projection(v2.clone(), ls.clone()),
- env,
- )
- }
- _ => Ret::Expr(expr),
- },
- ExprKind::ProjectionByExpr(ref v, ref t) => match t.kind() {
- RecordType(kts) => {
- return normalize_one_layer(
- ExprKind::Projection(
- v.clone(),
- kts.keys().cloned().collect(),
- ),
- env,
- )
- }
- _ => Ret::Expr(expr),
- },
-
- ExprKind::Merge(ref handlers, ref variant, _) => {
- match handlers.kind() {
- RecordLit(kvs) => match variant.kind() {
- UnionConstructor(l, _) => match kvs.get(l) {
- Some(h) => Ret::Nir(h.clone()),
- None => Ret::Expr(expr),
- },
- UnionLit(l, v, _) => match kvs.get(l) {
- Some(h) => Ret::Nir(h.app(v.clone())),
- None => Ret::Expr(expr),
- },
- EmptyOptionalLit(_) => match kvs.get(&"None".into()) {
- Some(h) => Ret::Nir(h.clone()),
- None => Ret::Expr(expr),
- },
- NEOptionalLit(v) => match kvs.get(&"Some".into()) {
- Some(h) => Ret::Nir(h.app(v.clone())),
- None => Ret::Expr(expr),
- },
- _ => Ret::Expr(expr),
- },
- _ => Ret::Expr(expr),
- }
+ ExprKind::Op(ref op) => normalize_operation(op),
+ ExprKind::Annot(x, _) => ret_nir(x),
+ ExprKind::Assert(x) => ret_kind(Assert(x)),
+ ExprKind::Import(..) => {
+ unreachable!("This case should have been handled in resolution")
}
- ExprKind::ToMap(ref v, ref annot) => match v.kind() {
- RecordLit(kvs) if kvs.is_empty() => {
- match annot.as_ref().map(|v| v.kind()) {
- Some(NirKind::ListType(t)) => {
- Ret::NirKind(EmptyListLit(t.clone()))
- }
- _ => Ret::Expr(expr),
- }
- }
- RecordLit(kvs) => Ret::NirKind(NEListLit(
- kvs.iter()
- .sorted_by_key(|(k, _)| *k)
- .map(|(k, v)| {
- let mut rec = HashMap::new();
- rec.insert("mapKey".into(), Nir::from_text(k));
- rec.insert("mapValue".into(), v.clone());
- Nir::from_kind(NirKind::RecordLit(rec))
- })
- .collect(),
- )),
- _ => Ret::Expr(expr),
- },
- };
-
- match ret {
- Ret::NirKind(v) => v,
- Ret::Nir(v) => v.kind().clone(),
- Ret::NirRef(v) => v.kind().clone(),
- Ret::Expr(expr) => NirKind::PartialExpr(expr),
}
}
/// Normalize Hir into WHNF
-pub fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
+pub fn normalize_hir(env: &NzEnv, hir: &Hir) -> NirKind {
match hir.kind() {
HirKind::Var(var) => env.lookup_val(*var),
- HirKind::Import(hir, _) => normalize_hir_whnf(env, hir),
+ HirKind::Import(hir, _) => normalize_hir(env, hir),
HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
let annot = annot.eval(env);
NirKind::LamClosure {
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 6e50fa6..e96f16b 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -1,17 +1,19 @@
use itertools::Itertools;
use std::borrow::Cow;
+use std::collections::BTreeMap;
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::{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};
@@ -179,12 +181,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,
}
}
@@ -196,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));
@@ -261,21 +264,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 +307,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/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 c3334b5..361e1b4 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -1,49 +1,10 @@
-use std::borrow::Cow;
use std::cmp::max;
-use std::collections::HashMap;
+use crate::builtins::{type_of_builtin, Builtin};
use crate::error::{ErrorBuilder, TypeError, TypeMessage};
-use crate::semantics::merge_maps;
-use crate::semantics::{
- type_of_builtin, Binder, Closure, Hir, HirKind, Nir, NirKind, Tir, TyEnv,
- Type,
-};
-use crate::syntax::{
- BinOp, 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(())
-}
+use crate::operations::typecheck_operation;
+use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type};
+use crate::syntax::{Const, ExprKind, InterpolatedTextContents, NumKind, Span};
fn function_check(a: Const, b: Const) -> Const {
if b == Const::Type {
@@ -74,8 +35,8 @@ fn type_one_layer(
) -> Result<Type, TypeError> {
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
- let ty = match &ekind {
- ExprKind::Import(..) | ExprKind::Completion(..) => {
+ Ok(match &ekind {
+ ExprKind::Import(..) => {
unreachable!("This case should have been handled in resolution")
}
ExprKind::Var(..)
@@ -89,20 +50,16 @@ fn type_one_layer(
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::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)
- }
ExprKind::TextLit(interpolated) => {
let text_type = Type::from_builtin(Builtin::Text);
for contents in interpolated.iter() {
@@ -115,6 +72,16 @@ fn type_one_layer(
}
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() {
@@ -138,82 +105,56 @@ fn type_one_layer(
let t = x.ty().to_nir();
Nir::from_builtin(Builtin::List).app(t).to_type(Const::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::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.values() {
// 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.values() {
// 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.values() {
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;
@@ -222,36 +163,7 @@ fn type_one_layer(
Type::from_const(k)
}
- ExprKind::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"),
- }
- }
- _ => return span_err("NotARecord"),
- }
- }
+ ExprKind::Op(op) => typecheck_operation(env, span, op)?,
ExprKind::Assert(t) => {
let t = t.eval_to_type(env)?;
match t.kind() {
@@ -261,430 +173,13 @@ fn type_one_layer(
}
t
}
- ExprKind::App(f, arg) => {
- match f.ty().kind() {
- // TODO: store Type in closure
- NirKind::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(),
- ),
- }
- }
- ExprKind::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()
- }
- ExprKind::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)
- }
- ExprKind::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(
- 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) => {
- 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::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::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::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::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::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,
- _ => {
- 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() {
- NirKind::ListType(t) => t,
- _ => return span_err(err_msg),
- };
- let kts = match arg.kind() {
- NirKind::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(NirKind::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
- }
- }
- ExprKind::Projection(record, labels) => {
- let record_type = record.ty();
- let kts = match record_type.kind() {
- NirKind::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(NirKind::RecordType(new_kts)),
- )?
- }
- ExprKind::ProjectionByExpr(record, selection) => {
- let record_type = record.ty();
- let rec_kts = match record_type.kind() {
- NirKind::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,
- _ => 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
- }
- };
-
- Ok(ty)
+ })
}
/// `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,
@@ -780,7 +275,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<Tir<'hir>, TypeError> {
type_with(&TyEnv::new(), hir, None)
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-08 16:40:38 +0000