summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/lib.rs2
-rw-r--r--dhall/src/semantics/hir.rs6
-rw-r--r--dhall/src/semantics/nze/value.rs5
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs54
-rw-r--r--dhall/src/semantics/tck/typecheck.rs111
5 files changed, 121 insertions, 57 deletions
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index ad54c9f..144cac5 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -120,7 +120,7 @@ impl Typed {
}
pub(crate) fn get_type(&self) -> Result<Normalized, TypeError> {
- Ok(Normalized(self.0.ty().clone()))
+ Ok(Normalized(self.0.ty().clone().into_value()))
}
}
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index c8258ff..d0a8a96 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -1,6 +1,6 @@
#![allow(dead_code)]
use crate::error::TypeError;
-use crate::semantics::{type_with, NameEnv, NzEnv, TyEnv, TyExpr, Value};
+use crate::semantics::{type_with, NameEnv, NzEnv, TyEnv, TyExpr, Type, Value};
use crate::syntax::{Expr, ExprKind, Span, V};
use crate::{NormalizedExpr, ToExprOptions};
@@ -79,6 +79,10 @@ impl Hir {
pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
Value::new_thunk(env.into(), self.clone())
}
+ /// Evaluate to a Type.
+ pub fn eval_to_type(&self, env: impl Into<NzEnv>) -> Type {
+ self.eval(env).into()
+ }
/// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
/// needed on demand.
pub fn eval_closed_expr(&self) -> Value {
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 3a5b5b5..f31fd6c 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
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, VarEnv,
+ BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, VarEnv,
};
use crate::syntax::{
BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
@@ -139,6 +139,9 @@ impl Value {
self.0.kind()
}
+ pub(crate) fn to_type(&self) -> Type {
+ self.clone().into()
+ }
/// Converts a value back to the corresponding AST expression.
pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
if opts.normalize {
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index dfb4397..4999899 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,17 +1,53 @@
use crate::error::TypeError;
-use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value};
-use crate::syntax::{Const, Span};
+use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value, ValueKind, VarEnv};
+use crate::syntax::{Builtin, Const, Span};
use crate::{NormalizedExpr, ToExprOptions};
-pub(crate) type Type = Value;
+/// An expression representing a type
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) struct Type {
+ val: Value,
+}
-// A hir expression plus its inferred type.
+/// A hir expression plus its inferred type.
#[derive(Debug, Clone)]
pub(crate) struct TyExpr {
hir: Hir,
ty: Type,
}
+impl Type {
+ pub fn from_const(c: Const) -> Self {
+ Value::from_const(c).into()
+ }
+ pub fn from_builtin(b: Builtin) -> Self {
+ Value::from_builtin(b).into()
+ }
+
+ pub fn to_value(&self) -> Value {
+ self.val.clone()
+ }
+ pub fn as_value(&self) -> &Value {
+ &self.val
+ }
+ pub fn into_value(self) -> Value {
+ self.val
+ }
+ pub fn as_const(&self) -> Option<Const> {
+ self.val.as_const()
+ }
+ pub fn kind(&self) -> &ValueKind {
+ self.val.kind()
+ }
+
+ pub fn to_hir(&self, venv: VarEnv) -> Hir {
+ self.val.to_hir(venv)
+ }
+ pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+ self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
+ }
+}
+
impl TyExpr {
pub fn new(kind: HirKind, ty: Type, span: Span) -> Self {
TyExpr {
@@ -52,6 +88,10 @@ impl TyExpr {
pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
self.as_hir().eval(env.into())
}
+ /// Evaluate to a Type.
+ pub fn eval_to_type(&self, env: impl Into<NzEnv>) -> Type {
+ self.eval(env).into()
+ }
/// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
/// needed on demand.
pub fn eval_closed_expr(&self) -> Value {
@@ -64,3 +104,9 @@ impl TyExpr {
val
}
}
+
+impl From<Value> for Type {
+ fn from(x: Value) -> Type {
+ Type { val: x }
+ }
+}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 36f7173..dd996ae 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -38,7 +38,8 @@ fn check_rectymerge(
};
for (k, tx) in kts_x {
if let Some(ty) = kts_y.get(k) {
- check_rectymerge(span, env, tx.clone(), ty.clone())?;
+ // TODO: store Type in RecordType ?
+ check_rectymerge(span, env, tx.clone().into(), ty.clone().into())?;
}
}
Ok(())
@@ -105,7 +106,7 @@ fn type_one_layer(
.format(),
);
}
- let body_env = env.insert_type(&binder, annot.eval(env));
+ let body_env = env.insert_type(&binder, annot.eval_to_type(env));
if body.get_kind(&body_env)?.is_none() {
return span_err("Invalid output type");
}
@@ -117,7 +118,7 @@ fn type_one_layer(
)),
span.clone(),
)
- .eval(env)
+ .eval_to_type(env)
}
ExprKind::Pi(_, annot, body) => {
let ks = match annot.ty().as_const() {
@@ -148,29 +149,29 @@ fn type_one_layer(
_ => return span_err("Invalid output type"),
};
- Value::from_const(function_check(ks, kt))
+ Type::from_const(function_check(ks, kt))
}
ExprKind::Let(_, _, _, body) => body.ty().clone(),
- ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
- ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
+ 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);
let t_tyexpr = typecheck(&t_hir)?;
- t_tyexpr.eval(env)
+ t_tyexpr.eval_to_type(env)
}
- ExprKind::Lit(LitKind::Bool(_)) => Value::from_builtin(Builtin::Bool),
+ ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
ExprKind::Lit(LitKind::Natural(_)) => {
- Value::from_builtin(Builtin::Natural)
+ Type::from_builtin(Builtin::Natural)
}
ExprKind::Lit(LitKind::Integer(_)) => {
- Value::from_builtin(Builtin::Integer)
+ Type::from_builtin(Builtin::Integer)
}
ExprKind::Lit(LitKind::Double(_)) => {
- Value::from_builtin(Builtin::Double)
+ Type::from_builtin(Builtin::Double)
}
ExprKind::TextLit(interpolated) => {
- let text_type = Value::from_builtin(Builtin::Text);
+ let text_type = Type::from_builtin(Builtin::Text);
for contents in interpolated.iter() {
use InterpolatedTextContents::Expr;
if let Expr(x) = contents {
@@ -182,7 +183,7 @@ fn type_one_layer(
text_type
}
ExprKind::EmptyListLit(t) => {
- let t = t.eval(env);
+ let t = t.eval_to_type(env);
match t.kind() {
ValueKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
@@ -205,16 +206,16 @@ fn type_one_layer(
return span_err("InvalidListType");
}
- let t = x.ty().clone();
- Value::from_builtin(Builtin::List).app(t)
+ let t = x.ty().to_value();
+ Value::from_builtin(Builtin::List).app(t).to_type()
}
ExprKind::SomeLit(x) => {
if x.get_kind(env)? != Some(Const::Type) {
return span_err("InvalidOptionalType");
}
- let t = x.ty().clone();
- Value::from_builtin(Builtin::Optional).app(t)
+ let t = x.ty().to_value();
+ Value::from_builtin(Builtin::Optional).app(t).to_type()
}
ExprKind::RecordLit(kvs) => {
use std::collections::hash_map::Entry;
@@ -225,7 +226,7 @@ fn type_one_layer(
Entry::Occupied(_) => {
return span_err("RecordTypeDuplicateField")
}
- Entry::Vacant(e) => e.insert(v.ty().clone()),
+ Entry::Vacant(e) => e.insert(v.ty().to_value()),
};
// Check that the fields have a valid kind
@@ -235,7 +236,7 @@ fn type_one_layer(
}
}
- Value::from_kind(ValueKind::RecordType(kts))
+ Value::from_kind(ValueKind::RecordType(kts)).to_type()
}
ExprKind::RecordType(kts) => {
use std::collections::hash_map::Entry;
@@ -259,7 +260,7 @@ fn type_one_layer(
}
}
- Value::from_const(k)
+ Type::from_const(k)
}
ExprKind::UnionType(kts) => {
use std::collections::hash_map::Entry;
@@ -286,17 +287,17 @@ fn type_one_layer(
// an union type with only unary variants also has type Type
let k = k.unwrap_or(Const::Type);
- Value::from_const(k)
+ Type::from_const(k)
}
ExprKind::Field(scrut, x) => {
match scrut.ty().kind() {
ValueKind::RecordType(kts) => match kts.get(&x) {
- Some(tth) => tth.clone(),
+ Some(val) => val.clone().to_type(),
None => return span_err("MissingRecordField"),
},
// TODO: branch here only when scrut.ty() is a Const
_ => {
- let scrut_nf = scrut.eval(env);
+ let scrut_nf = scrut.eval_to_type(env);
match scrut_nf.kind() {
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
@@ -304,8 +305,11 @@ fn type_one_layer(
Value::from_kind(ValueKind::PiClosure {
binder: Binder::new(x.clone()),
annot: ty.clone(),
- closure: Closure::new_constant(scrut_nf),
+ closure: Closure::new_constant(
+ scrut_nf.into_value(),
+ ),
})
+ .to_type()
}
Some(None) => scrut_nf,
None => return span_err("MissingUnionField"),
@@ -316,7 +320,7 @@ fn type_one_layer(
}
}
ExprKind::Assert(t) => {
- let t = t.eval(env);
+ let t = t.eval_to_type(env);
match t.kind() {
ValueKind::Equivalence(x, y) if x == y => {}
ValueKind::Equivalence(..) => {
@@ -328,8 +332,9 @@ fn type_one_layer(
}
ExprKind::App(f, arg) => {
match f.ty().kind() {
+ // TODO: store Type in closure
ValueKind::PiClosure { annot, closure, .. } => {
- if arg.ty() != annot {
+ if arg.ty().as_value() != annot {
return mkerr(
ErrorBuilder::new(format!(
"wrong type of function argument"
@@ -358,7 +363,7 @@ fn type_one_layer(
}
let arg_nf = arg.eval(env);
- closure.apply(arg_nf)
+ closure.apply(arg_nf).to_type()
}
_ => return mkerr(
ErrorBuilder::new(format!(
@@ -407,7 +412,7 @@ fn type_one_layer(
Ok(r_t.clone())
})?;
- Value::from_kind(ValueKind::RecordType(kts))
+ Value::from_kind(ValueKind::RecordType(kts)).to_type()
}
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?;
@@ -420,15 +425,20 @@ fn type_one_layer(
)),
span.clone(),
)
- .eval(env)
+ .eval_to_type(env)
}
ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
- check_rectymerge(&span, env, x.eval(env), y.eval(env))?;
+ check_rectymerge(
+ &span,
+ env,
+ x.eval_to_type(env),
+ y.eval_to_type(env),
+ )?;
// A RecordType's type is always a const
let xk = x.ty().as_const().unwrap();
let yk = y.ty().as_const().unwrap();
- Value::from_const(max(xk, yk))
+ Type::from_const(max(xk, yk))
}
ExprKind::BinOp(BinOp::ListAppend, l, r) => {
match l.ty().kind() {
@@ -453,10 +463,10 @@ fn type_one_layer(
return span_err("EquivalenceArgumentsMustBeTerms");
}
- Value::from_const(Const::Type)
+ Type::from_const(Const::Type)
}
ExprKind::BinOp(o, l, r) => {
- let t = Value::from_builtin(match o {
+ let t = Type::from_builtin(match o {
BinOp::BoolAnd
| BinOp::BoolOr
| BinOp::BoolEQ
@@ -507,7 +517,7 @@ fn type_one_layer(
let mut inferred_type = None;
for (x, handler_type) in handlers {
- let handler_return_type = match variants.get(x) {
+ let handler_return_type: Type = match variants.get(x) {
// Union alternative with type
Some(Some(variant_type)) => match handler_type.kind() {
ValueKind::PiClosure { closure, annot, .. } => {
@@ -542,7 +552,7 @@ fn type_one_layer(
}
match closure.remove_binder() {
- Ok(v) => v,
+ Ok(v) => v.to_type(),
Err(()) => {
return span_err(
"MergeReturnTypeIsDependent",
@@ -586,7 +596,7 @@ fn type_one_layer(
}
},
// Union alternative without type
- Some(None) => handler_type.clone(),
+ Some(None) => handler_type.clone().to_type(),
None => return span_err("MergeHandlerMissingVariant"),
};
match &inferred_type {
@@ -604,7 +614,7 @@ fn type_one_layer(
}
}
- let type_annot = type_annot.as_ref().map(|t| t.eval(env));
+ let type_annot = type_annot.as_ref().map(|t| t.eval_to_type(env));
match (inferred_type, type_annot) {
(Some(t1), Some(t2)) => {
if t1 != t2 {
@@ -638,7 +648,7 @@ fn type_one_layer(
annotation",
);
};
- let annot_val = annot.eval(env);
+ 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 }`";
@@ -679,10 +689,11 @@ fn type_one_layer(
let mut kts = HashMap::new();
kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
kts.insert("mapValue".into(), entry_type);
- let output_type = Value::from_builtin(Builtin::List)
- .app(Value::from_kind(ValueKind::RecordType(kts)));
+ let output_type: Type = Value::from_builtin(Builtin::List)
+ .app(Value::from_kind(ValueKind::RecordType(kts)))
+ .to_type();
if let Some(annot) = annot {
- let annot_val = annot.eval(env);
+ let annot_val = annot.eval_to_type(env);
if output_type != annot_val {
return span_err("Annotation mismatch");
}
@@ -713,7 +724,7 @@ fn type_one_layer(
};
}
- Value::from_kind(ValueKind::RecordType(new_kts))
+ Value::from_kind(ValueKind::RecordType(new_kts)).to_type()
}
ExprKind::ProjectionByExpr(record, selection) => {
let record_type = record.ty();
@@ -722,7 +733,7 @@ fn type_one_layer(
_ => return span_err("ProjectionMustBeRecord"),
};
- let selection_val = selection.eval(env);
+ let selection_val = selection.eval_to_type(env);
let sel_kts = match selection_val.kind() {
ValueKind::RecordType(kts) => kts,
_ => return span_err("ProjectionByExprTakesRecordType"),
@@ -781,9 +792,9 @@ pub(crate) fn type_with(
HirKind::Expr(ExprKind::Annot(x, t)) => {
let t = match t.kind() {
HirKind::Expr(ExprKind::Const(Const::Sort)) => {
- Value::from_const(Const::Sort)
+ Type::from_const(Const::Sort)
}
- _ => type_with(env, t, None)?.eval(env),
+ _ => type_with(env, t, None)?.eval_to_type(env),
};
type_with(env, x, Some(t))
}
@@ -791,21 +802,21 @@ pub(crate) fn type_with(
let ekind = match ekind {
ExprKind::Lam(binder, annot, body) => {
let annot = type_with(env, annot, None)?;
- let annot_nf = annot.eval(env);
+ let annot_nf = annot.eval_to_type(env);
let body_env = env.insert_type(binder, annot_nf);
let body = type_with(&body_env, body, None)?;
ExprKind::Lam(binder.clone(), annot, body)
}
ExprKind::Pi(binder, annot, body) => {
let annot = type_with(env, annot, None)?;
- let annot_nf = annot.eval(env);
- let body_env = env.insert_type(binder, annot_nf);
+ let annot_val = annot.eval_to_type(env);
+ let body_env = env.insert_type(binder, annot_val);
let body = type_with(&body_env, body, None)?;
ExprKind::Pi(binder.clone(), annot, body)
}
ExprKind::Let(binder, annot, val, body) => {
let val_annot = if let Some(t) = annot {
- Some(type_with(env, t, None)?.eval(env))
+ Some(type_with(env, t, None)?.eval_to_type(env))
} else {
None
};
@@ -831,6 +842,6 @@ pub(crate) fn typecheck(hir: &Hir) -> Result<TyExpr, TypeError> {
/// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> {
- let ty = typecheck(&ty)?.eval(&TyEnv::new());
+ let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new());
type_with(&TyEnv::new(), hir, Some(ty))
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 16:44:26 +0000