summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/semantics/core/value.rs47
-rw-r--r--dhall/src/semantics/phase/normalize.rs20
-rw-r--r--dhall/src/semantics/tck/typecheck.rs208
-rw-r--r--tests_buffer1
4 files changed, 172 insertions, 104 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 71c5c65..3dcbd38 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -56,10 +56,15 @@ pub(crate) enum Form {
}
#[derive(Debug, Clone)]
-pub(crate) struct Closure {
- arg_ty: Value,
- env: NzEnv,
- body: TyExpr,
+pub(crate) enum Closure {
+ /// Normal closure
+ Closure {
+ arg_ty: Value,
+ env: NzEnv,
+ body: TyExpr,
+ },
+ /// Closure that ignores the argument passed
+ ConstantClosure { env: NzEnv, body: TyExpr },
}
#[derive(Debug, Clone, PartialEq, Eq)]
@@ -696,21 +701,41 @@ impl<V> ValueKind<V> {
impl Closure {
pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self {
- Closure {
+ Closure::Closure {
arg_ty,
env: env.clone(),
body,
}
}
+ pub fn new_constant(env: &NzEnv, body: TyExpr) -> Self {
+ Closure::ConstantClosure {
+ env: env.clone(),
+ body,
+ }
+ }
pub fn apply(&self, val: Value) -> Value {
- self.body.normalize_whnf(&self.env.insert_value(val))
+ match self {
+ Closure::Closure { env, body, .. } => {
+ body.normalize_whnf(&env.insert_value(val))
+ }
+ Closure::ConstantClosure { env, body, .. } => {
+ body.normalize_whnf(env)
+ }
+ }
}
pub fn apply_var(&self, var: NzVar) -> Value {
- let val = Value::from_kind_and_type(
- ValueKind::Var(AlphaVar::default(), var),
- self.arg_ty.clone(),
- );
- self.apply(val)
+ match self {
+ Closure::Closure { arg_ty, .. } => {
+ let val = Value::from_kind_and_type(
+ ValueKind::Var(AlphaVar::default(), var),
+ arg_ty.clone(),
+ );
+ self.apply(val)
+ }
+ Closure::ConstantClosure { env, body, .. } => {
+ body.normalize_whnf(env)
+ }
+ }
}
}
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index a11cb75..532dae3 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -855,17 +855,30 @@ pub(crate) enum NzEnvItem {
#[derive(Debug, Clone)]
pub(crate) struct NzEnv {
items: Vec<NzEnvItem>,
+ vars: QuoteEnv,
}
impl NzEnv {
pub fn new() -> Self {
- NzEnv { items: Vec::new() }
+ NzEnv {
+ items: Vec::new(),
+ vars: QuoteEnv::new(),
+ }
}
pub fn construct(items: Vec<NzEnvItem>) -> Self {
- NzEnv { items }
+ let vars = QuoteEnv::construct(
+ items
+ .iter()
+ .filter(|i| match i {
+ NzEnvItem::Kept(_) => true,
+ NzEnvItem::Replaced(_) => false,
+ })
+ .count(),
+ );
+ NzEnv { items, vars }
}
pub fn as_quoteenv(&self) -> QuoteEnv {
- QuoteEnv::construct(self.items.len())
+ self.vars
}
pub fn to_alpha_tyenv(&self) -> TyEnv {
TyEnv::from_nzenv_alpha(self)
@@ -874,6 +887,7 @@ impl NzEnv {
pub fn insert_type(&self, t: Value) -> Self {
let mut env = self.clone();
env.items.push(NzEnvItem::Kept(t));
+ env.vars = env.vars.insert();
env
}
pub fn insert_value(&self, e: Value) -> Self {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index e2619b5..1b8f261 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -7,7 +7,7 @@ use std::collections::HashMap;
use crate::error::{TypeError, TypeMessage};
use crate::semantics::core::context::TyCtx;
-use crate::semantics::nze::{NameEnv, QuoteEnv};
+use crate::semantics::nze::{NameEnv, NzVar, QuoteEnv};
use crate::semantics::phase::normalize::{merge_maps, NzEnv};
use crate::semantics::phase::typecheck::{
builtin_to_value, const_to_value, type_of_builtin,
@@ -44,7 +44,7 @@ impl TyEnv {
}
}
pub fn as_quoteenv(&self) -> QuoteEnv {
- self.names.as_quoteenv()
+ self.items.as_quoteenv()
}
pub fn as_nzenv(&self) -> &NzEnv {
&self.items
@@ -262,8 +262,7 @@ fn type_one_layer(
ValueKind::PiClosure {
binder: Binder::new(x.clone()),
annot: ty.clone(),
- closure: Closure::new(
- ty.clone(),
+ closure: Closure::new_constant(
env.as_nzenv(),
scrut.clone(),
),
@@ -300,6 +299,15 @@ fn type_one_layer(
}
x_ty
}
+ ExprKind::Assert(t) => {
+ let t = t.normalize_whnf(env.as_nzenv());
+ match &*t.as_whnf() {
+ ValueKind::Equivalence(x, y) if x == y => {}
+ ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
+ _ => return mkerr("AssertMustTakeEquivalence"),
+ }
+ t
+ }
ExprKind::App(f, arg) => {
let tf = f.get_type()?;
let tf_borrow = tf.as_whnf();
@@ -458,88 +466,109 @@ fn type_one_layer(
t
}
- // ExprKind::Merge(record, union, type_annot) => {
- // let record_type = record.get_type()?;
- // let record_borrow = record_type.as_whnf();
- // let handlers = match &*record_borrow {
- // ValueKind::RecordType(kts) => kts,
- // _ => return mkerr("Merge1ArgMustBeRecord"),
- // };
-
- // let union_type = union.get_type()?;
- // let union_borrow = union_type.as_whnf();
- // let variants = match &*union_borrow {
- // ValueKind::UnionType(kts) => Cow::Borrowed(kts),
- // ValueKind::AppliedBuiltin(
- // syntax::Builtin::Optional,
- // args,
- // _,
- // ) if args.len() == 1 => {
- // let ty = &args[0];
- // let mut kts = HashMap::new();
- // kts.insert("None".into(), None);
- // kts.insert("Some".into(), Some(ty.clone()));
- // Cow::Owned(kts)
- // }
- // _ => return mkerr("Merge2ArgMustBeUnionOrOptional"),
- // };
-
- // let mut inferred_type = None;
- // for (x, handler_type) in handlers {
- // let handler_return_type =
- // match variants.get(x) {
- // // Union alternative with type
- // Some(Some(variant_type)) => {
- // let handler_type_borrow = handler_type.as_whnf();
- // let (tx, tb) = match &*handler_type_borrow {
- // ValueKind::Pi(_, tx, tb) => (tx, tb),
- // _ => return mkerr("NotAFunction"),
- // };
-
- // if variant_type != tx {
- // return mkerr("TypeMismatch");
- // }
-
- // // Extract `tb` from under the binder. Fails if the variable was used
- // // in `tb`.
- // match tb.over_binder() {
- // Some(x) => x,
- // None => return mkerr(
- // "MergeHandlerReturnTypeMustNotBeDependent",
- // ),
- // }
- // }
- // // Union alternative without type
- // Some(None) => handler_type.clone(),
- // None => return mkerr("MergeHandlerMissingVariant"),
- // };
- // match &inferred_type {
- // None => inferred_type = Some(handler_return_type),
- // Some(t) => {
- // if t != &handler_return_type {
- // return mkerr("MergeHandlerTypeMismatch");
- // }
- // }
- // }
- // }
- // for x in variants.keys() {
- // if !handlers.contains_key(x) {
- // return mkerr("MergeVariantMissingHandler");
- // }
- // }
-
- // match (inferred_type, type_annot.as_ref()) {
- // (Some(t1), Some(t2)) => {
- // if &t1 != t2 {
- // return mkerr("MergeAnnotMismatch");
- // }
- // RetTypeOnly(t1)
- // }
- // (Some(t), None) => RetTypeOnly(t),
- // (None, Some(t)) => RetTypeOnly(t.clone()),
- // (None, None) => return mkerr("MergeEmptyNeedsAnnotation"),
- // }
- // }
+ ExprKind::Merge(record, union, type_annot) => {
+ let record_type = record.get_type()?;
+ let record_borrow = record_type.as_whnf();
+ let handlers = match &*record_borrow {
+ ValueKind::RecordType(kts) => kts,
+ _ => return mkerr("Merge1ArgMustBeRecord"),
+ };
+
+ let union_type = union.get_type()?;
+ let union_borrow = union_type.as_whnf();
+ let variants = match &*union_borrow {
+ ValueKind::UnionType(kts) => Cow::Borrowed(kts),
+ ValueKind::AppliedBuiltin(
+ syntax::Builtin::Optional,
+ args,
+ _,
+ _,
+ ) if args.len() == 1 => {
+ let ty = &args[0];
+ let mut kts = HashMap::new();
+ kts.insert("None".into(), None);
+ kts.insert("Some".into(), Some(ty.clone()));
+ Cow::Owned(kts)
+ }
+ _ => return mkerr("Merge2ArgMustBeUnionOrOptional"),
+ };
+
+ let mut inferred_type = None;
+ for (x, handler_type) in handlers {
+ let handler_return_type = match variants.get(x) {
+ // Union alternative with type
+ Some(Some(variant_type)) => {
+ let handler_type_borrow = handler_type.as_whnf();
+ match &*handler_type_borrow {
+ ValueKind::Pi(_, tx, tb) => {
+ if variant_type != tx {
+ return mkerr("MergeHandlerTypeMismatch");
+ }
+
+ // Extract `tb` from under the binder. Fails if the variable was used
+ // in `tb`.
+ match tb.over_binder() {
+ Some(x) => x,
+ None => return mkerr(
+ "MergeHandlerReturnTypeMustNotBeDependent",
+ ),
+ }
+ }
+ ValueKind::PiClosure { closure, annot, .. } => {
+ if variant_type != annot {
+ // return mkerr("MergeHandlerTypeMismatch");
+ return mkerr(format!(
+ "MergeHandlerTypeMismatch: {:#?} != {:#?}",
+ variant_type,
+ annot
+ ));
+ }
+
+ let v = NzVar::fresh();
+ // TODO: handle case where variable is used in closure
+ closure.apply_var(v)
+ }
+ _ => return mkerr("NotAFunction"),
+ }
+ }
+ // Union alternative without type
+ Some(None) => handler_type.clone(),
+ None => return mkerr("MergeHandlerMissingVariant"),
+ };
+ match &inferred_type {
+ None => inferred_type = Some(handler_return_type),
+ Some(t) => {
+ if t != &handler_return_type {
+ // return mkerr("MergeHandlerTypeMismatch");
+ return mkerr(format!(
+ "MergeHandlerTypeMismatch: {:#?} != {:#?}",
+ t, handler_return_type,
+ ));
+ }
+ }
+ }
+ }
+ for x in variants.keys() {
+ if !handlers.contains_key(x) {
+ return mkerr("MergeVariantMissingHandler");
+ }
+ }
+
+ let type_annot = type_annot
+ .as_ref()
+ .map(|t| t.normalize_whnf(env.as_nzenv()));
+ match (inferred_type, type_annot) {
+ (Some(t1), Some(t2)) => {
+ if t1 != t2 {
+ return mkerr("MergeAnnotMismatch");
+ }
+ t1
+ }
+ (Some(t), None) => t,
+ (None, Some(t)) => t,
+ (None, None) => return mkerr("MergeEmptyNeedsAnnotation"),
+ }
+ }
ExprKind::ToMap(_, _) => unimplemented!("toMap"),
ExprKind::Projection(record, labels) => {
let record_type = record.get_type()?;
@@ -574,7 +603,6 @@ fn type_one_layer(
unimplemented!("selection by expression")
}
ExprKind::Completion(_, _) => unimplemented!("record completion"),
- _ => Value::from_const(Const::Type), // TODO
})
}
@@ -592,14 +620,14 @@ pub(crate) fn type_with(
ExprKind::Lam(binder, annot, body) => {
let annot = type_with(env, annot)?;
let annot_nf = annot.normalize_whnf(env.as_nzenv());
- let body =
- type_with(&env.insert_type(&binder, annot_nf.clone()), body)?;
+ let body_env = env.insert_type(&binder, annot_nf.clone());
+ let body = type_with(&body_env, body)?;
let body_ty = body.get_type()?;
let ty = TyExpr::new(
TyExprKind::Expr(ExprKind::Pi(
binder.clone(),
annot.clone(),
- body_ty.to_tyexpr(env.as_quoteenv().insert()),
+ body_ty.to_tyexpr(body_env.as_quoteenv()),
)),
Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
Span::Artificial,
diff --git a/tests_buffer b/tests_buffer
index a872503..e5e1705 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -48,6 +48,7 @@ success/
somehow test that the recordtype from List/indexed has a type in both empty and nonempty cases
somehow test types added to the Foo/build closures
λ(x : ∀(a : Type) → a) → x
+ let X = 0 in λ(T : Type) → λ(x : T) → 1
failure/
merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-29 09:13:25 +0000