diff options
Diffstat (limited to 'dhall/src/semantics/tck')
| -rw-r--r-- | dhall/src/semantics/tck/env.rs | 4 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/tir.rs | 26 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 90 |
3 files changed, 58 insertions, 62 deletions
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index f290c02..17b3cfe 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -1,4 +1,4 @@ -use crate::semantics::{AlphaVar, NameEnv, NzEnv, NzVar, Type, ValEnv, Value}; +use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv}; use crate::syntax::Label; /// Environment for indexing variables. @@ -61,7 +61,7 @@ impl TyEnv { items: self.items.insert_type(ty), } } - pub fn insert_value(&self, x: &Label, e: Value, ty: Type) -> Self { + pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self { TyEnv { names: self.names.insert(x), items: self.items.insert_value(e, ty), diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs index 800d1b7..908bf8f 100644 --- a/dhall/src/semantics/tck/tir.rs +++ b/dhall/src/semantics/tck/tir.rs @@ -1,5 +1,5 @@ use crate::error::{ErrorBuilder, TypeError}; -use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv}; +use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv}; use crate::syntax::{Builtin, Const, Span}; use crate::{NormalizedExpr, ToExprOptions}; @@ -10,7 +10,7 @@ pub(crate) struct Universe(u8); /// An expression representing a type #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) struct Type { - val: Value, + val: Nir, univ: Universe, } @@ -44,7 +44,7 @@ impl Universe { } impl Type { - pub fn new(val: Value, univ: Universe) -> Self { + pub fn new(val: Nir, univ: Universe) -> Self { Type { val, univ } } /// Creates a new Type and infers its universe by re-typechecking its value. @@ -52,7 +52,7 @@ impl Type { /// PiClosure. pub fn new_infer_universe( env: &TyEnv, - val: Value, + val: Nir, ) -> Result<Self, TypeError> { let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const(); let u = match c { @@ -65,7 +65,7 @@ impl Type { Ok(Type::new(val, u)) } pub fn from_const(c: Const) -> Self { - Self::new(Value::from_const(c), c.to_universe().next()) + Self::new(Nir::from_const(c), c.to_universe().next()) } pub fn from_builtin(b: Builtin) -> Self { use Builtin::*; @@ -74,7 +74,7 @@ impl Type { _ => unreachable!("this builtin is not a type: {}", b), } - Self::new(Value::from_builtin(b), Universe::from_const(Const::Type)) + Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type)) } /// Get the type of this type @@ -82,19 +82,19 @@ impl Type { self.univ } - pub fn to_value(&self) -> Value { + pub fn to_nir(&self) -> Nir { self.val.clone() } - pub fn as_value(&self) -> &Value { + pub fn as_nir(&self) -> &Nir { &self.val } - pub fn into_value(self) -> Value { + pub fn into_nir(self) -> Nir { self.val } pub fn as_const(&self) -> Option<Const> { self.val.as_const() } - pub fn kind(&self) -> &ValueKind { + pub fn kind(&self) -> &NirKind { self.val.kind() } @@ -136,7 +136,7 @@ impl Tir { } /// Eval the Tir. It will actually get evaluated only as needed on demand. - pub fn eval(&self, env: impl Into<NzEnv>) -> Value { + pub fn eval(&self, env: impl Into<NzEnv>) -> Nir { self.as_hir().eval(env.into()) } pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> { @@ -175,11 +175,11 @@ impl Tir { } /// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as /// needed on demand. - pub fn eval_closed_expr(&self) -> Value { + pub fn eval_closed_expr(&self) -> Nir { self.eval(NzEnv::new()) } /// Eval a closed Tir fully and recursively; - pub fn rec_eval_closed_expr(&self) -> Value { + pub fn rec_eval_closed_expr(&self) -> Nir { let val = self.eval_closed_expr(); val.normalize(); val diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 7bf15af..42a9165 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -5,8 +5,8 @@ use std::collections::HashMap; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::semantics::merge_maps; use crate::semantics::{ - type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Tir, TyEnv, - Type, Value, ValueKind, + type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, + NirKind, Tir, TyEnv, Type, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, @@ -15,11 +15,11 @@ use crate::syntax::{ fn check_rectymerge( span: &Span, env: &TyEnv, - x: Value, - y: Value, + x: Nir, + y: Nir, ) -> Result<(), TypeError> { let kts_x = match x.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => { return mk_span_err( span.clone(), @@ -28,7 +28,7 @@ fn check_rectymerge( } }; let kts_y = match y.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => { return mk_span_err( span.clone(), @@ -118,7 +118,7 @@ fn type_one_layer( ExprKind::EmptyListLit(t) => { let t = t.eval_to_type(env)?; match t.kind() { - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, .. @@ -139,18 +139,16 @@ fn type_one_layer( return span_err("InvalidListType"); } - let t = x.ty().to_value(); - Value::from_builtin(Builtin::List) - .app(t) - .to_type(Const::Type) + 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_value(); - Value::from_builtin(Builtin::Optional) + let t = x.ty().to_nir(); + Nir::from_builtin(Builtin::Optional) .app(t) .to_type(Const::Type) } @@ -165,7 +163,7 @@ fn type_one_layer( Entry::Occupied(_) => { return span_err("RecordTypeDuplicateField") } - Entry::Vacant(e) => e.insert(v.ty().to_value()), + Entry::Vacant(e) => e.insert(v.ty().to_nir()), }; // Check that the fields have a valid kind @@ -175,7 +173,7 @@ fn type_one_layer( } } - Value::from_kind(ValueKind::RecordType(kts)).to_type(k) + Nir::from_kind(NirKind::RecordType(kts)).to_type(k) } ExprKind::RecordType(kts) => { use std::collections::hash_map::Entry; @@ -230,21 +228,21 @@ fn type_one_layer( } ExprKind::Field(scrut, x) => { match scrut.ty().kind() { - ValueKind::RecordType(kts) => match kts.get(&x) { + NirKind::RecordType(kts) => match kts.get(&x) { Some(val) => Type::new_infer_universe(env, val.clone())?, None => return span_err("MissingRecordField"), }, - ValueKind::Const(_) => { + NirKind::Const(_) => { let scrut = scrut.eval_to_type(env)?; match scrut.kind() { - ValueKind::UnionType(kts) => match kts.get(x) { + NirKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > Some(Some(ty)) => { - Value::from_kind(ValueKind::PiClosure { + Nir::from_kind(NirKind::PiClosure { binder: Binder::new(x.clone()), annot: ty.clone(), closure: Closure::new_constant( - scrut.to_value(), + scrut.to_nir(), ), }) .to_type(scrut.ty()) @@ -261,10 +259,8 @@ fn type_one_layer( ExprKind::Assert(t) => { let t = t.eval_to_type(env)?; match t.kind() { - ValueKind::Equivalence(x, y) if x == y => {} - ValueKind::Equivalence(..) => { - return span_err("AssertMismatch") - } + NirKind::Equivalence(x, y) if x == y => {} + NirKind::Equivalence(..) => return span_err("AssertMismatch"), _ => return span_err("AssertMustTakeEquivalence"), } t @@ -272,8 +268,8 @@ fn type_one_layer( ExprKind::App(f, arg) => { match f.ty().kind() { // TODO: store Type in closure - ValueKind::PiClosure { annot, closure, .. } => { - if arg.ty().as_value() != annot { + NirKind::PiClosure { annot, closure, .. } => { + if arg.ty().as_nir() != annot { return mkerr( ErrorBuilder::new(format!( "wrong type of function argument" @@ -318,7 +314,7 @@ fn type_one_layer( } } ExprKind::BoolIf(x, y, z) => { - if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) { + if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } if y.ty().ty().as_const() != Some(Const::Type) { @@ -336,12 +332,12 @@ fn type_one_layer( // Extract the LHS record type let kts_x = match x_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("MustCombineRecord"), }; // Extract the RHS record type let kts_y = match y_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("MustCombineRecord"), }; @@ -352,10 +348,10 @@ fn type_one_layer( })?; let u = max(x.ty().ty(), y.ty().ty()); - Value::from_kind(ValueKind::RecordType(kts)).to_type(u) + Nir::from_kind(NirKind::RecordType(kts)).to_type(u) } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { - check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?; + check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?; let hir = Hir::new( HirKind::Expr(ExprKind::BinOp( @@ -379,7 +375,7 @@ fn type_one_layer( } ExprKind::BinOp(BinOp::ListAppend, l, r) => { match l.ty().kind() { - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, .. }) => {} @@ -431,14 +427,14 @@ fn type_one_layer( ExprKind::Merge(record, union, type_annot) => { let record_type = record.ty(); let handlers = match record_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("Merge1ArgMustBeRecord"), }; let union_type = union.ty(); let variants = match union_type.kind() { - ValueKind::UnionType(kts) => Cow::Borrowed(kts), - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::UnionType(kts) => Cow::Borrowed(kts), + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::Optional, args, .. @@ -457,7 +453,7 @@ fn type_one_layer( 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, .. } => { + NirKind::PiClosure { closure, annot, .. } => { if variant_type != annot { return mkerr( ErrorBuilder::new(format!( @@ -578,7 +574,7 @@ fn type_one_layer( } let record_t = record.ty(); let kts = match record_t.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => { return span_err("The argument to `toMap` must be a record") } @@ -598,7 +594,7 @@ 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() { - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, .. @@ -606,14 +602,14 @@ fn type_one_layer( _ => return span_err(err_msg), }; let kts = match arg.kind() { - ValueKind::RecordType(kts) => kts, + 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 == Value::from_builtin(Builtin::Text) => {} + Some(t) if *t == Nir::from_builtin(Builtin::Text) => {} _ => return span_err(err_msg), } match kts.get(&"mapValue".into()) { @@ -632,10 +628,10 @@ fn type_one_layer( } let mut kts = HashMap::new(); - kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text)); + kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text)); kts.insert("mapValue".into(), entry_type); - let output_type: Type = Value::from_builtin(Builtin::List) - .app(Value::from_kind(ValueKind::RecordType(kts))) + 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)?; @@ -649,7 +645,7 @@ fn type_one_layer( ExprKind::Projection(record, labels) => { let record_type = record.ty(); let kts = match record_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), }; @@ -671,19 +667,19 @@ fn type_one_layer( Type::new_infer_universe( env, - Value::from_kind(ValueKind::RecordType(new_kts)), + Nir::from_kind(NirKind::RecordType(new_kts)), )? } ExprKind::ProjectionByExpr(record, selection) => { let record_type = record.ty(); let rec_kts = match record_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), }; let selection_val = selection.eval_to_type(env)?; let sel_kts = match selection_val.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("ProjectionByExprTakesRecordType"), }; |