diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 77 | ||||
| -rw-r--r-- | dhall/src/semantics/core/visitor.rs | 14 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 23 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/mod.rs | 2 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 14 |
5 files changed, 93 insertions, 37 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 7086616..f470019 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -10,7 +10,7 @@ use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{ Normalized, NormalizedExpr, ToExprOptions, Typed, }; -use crate::semantics::{TyExpr, TyExprKind}; +use crate::semantics::{TyExpr, TyExprKind, Type}; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, Span, @@ -75,8 +75,10 @@ pub(crate) enum ValueKind<Value> { RecordType(HashMap<Label, Value>), RecordLit(HashMap<Label, Value>), UnionType(HashMap<Label, Option<Value>>), - UnionConstructor(Label, HashMap<Label, Option<Value>>), - UnionLit(Label, Value, HashMap<Label, Option<Value>>), + // Also keep the type of the uniontype around + UnionConstructor(Label, HashMap<Label, Option<Value>>, Type), + // Also keep the type of the uniontype and the constructor around + UnionLit(Label, Value, HashMap<Label, Option<Value>>, Type, Type), // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and // contiguous text values must be merged. TextLit(Vec<InterpolatedTextContents<Value>>), @@ -296,28 +298,40 @@ impl Value { } // TODO: properly recover intermediate types; `None` is a time-bomb here. - let rc = - |expr| TyExpr::new(TyExprKind::Expr(expr), None, Span::Artificial); - let self_kind = self_kind.map_ref(|v| v.to_tyexpr()); let expr = match self_kind { ValueKind::Var(_) => unreachable!(), ValueKind::Lam(x, t, e) => ExprKind::Lam(x.to_label(), t, e), ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e), - ValueKind::AppliedBuiltin(b, args) => args - .into_iter() - .fold(ExprKind::Builtin(b), |acc, v| ExprKind::App(rc(acc), v)), + ValueKind::AppliedBuiltin(b, args) => { + args.into_iter().fold(ExprKind::Builtin(b), |acc, v| { + ExprKind::App( + TyExpr::new( + TyExprKind::Expr(acc), + None, // TODO + Span::Artificial, + ), + v, + ) + }) + } ValueKind::Const(c) => ExprKind::Const(c), ValueKind::BoolLit(b) => ExprKind::BoolLit(b), ValueKind::NaturalLit(n) => ExprKind::NaturalLit(n), ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n), ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n), - ValueKind::EmptyOptionalLit(n) => { - ExprKind::App(rc(ExprKind::Builtin(Builtin::OptionalNone)), n) - } + ValueKind::EmptyOptionalLit(n) => ExprKind::App( + builtin_to_value(Builtin::OptionalNone).to_tyexpr(), + n, + ), ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), - ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(rc( - ExprKind::App(rc(ExprKind::Builtin(Builtin::List)), n), + ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(TyExpr::new( + TyExprKind::Expr(ExprKind::App( + builtin_to_value(Builtin::List).to_tyexpr(), + n, + )), + Some(const_to_value(Const::Type)), + Span::Artificial, )), ValueKind::NEListLit(elts) => ExprKind::NEListLit(elts), ValueKind::RecordLit(kvs) => { @@ -329,15 +343,31 @@ impl Value { ValueKind::UnionType(kts) => { ExprKind::UnionType(kts.into_iter().collect()) } - ValueKind::UnionConstructor(l, kts) => ExprKind::Field( - rc(ExprKind::UnionType(kts.into_iter().collect())), + ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field( + TyExpr::new( + TyExprKind::Expr(ExprKind::UnionType( + kts.into_iter().collect(), + )), + Some(t), + Span::Artificial, + ), l, ), - ValueKind::UnionLit(l, v, kts) => ExprKind::App( - rc(ExprKind::Field( - rc(ExprKind::UnionType(kts.into_iter().collect())), - l, - )), + ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App( + TyExpr::new( + TyExprKind::Expr(ExprKind::Field( + TyExpr::new( + TyExprKind::Expr(ExprKind::UnionType( + kts.into_iter().collect(), + )), + Some(uniont), + Span::Artificial, + ), + l, + )), + Some(ctort), + Span::Artificial, + ), v, ), ValueKind::TextLit(elts) => { @@ -483,12 +513,13 @@ impl ValueKind<Value> { x.normalize_mut(); } } - ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { + ValueKind::UnionType(kts) + | ValueKind::UnionConstructor(_, kts, _) => { for x in kts.values_mut().flat_map(|opt| opt) { x.normalize_mut(); } } - ValueKind::UnionLit(_, v, kts) => { + ValueKind::UnionLit(_, v, kts, _, _) => { v.normalize_mut(); for x in kts.values_mut().flat_map(|opt| opt) { x.normalize_mut(); diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs index e61a649..a449f6c 100644 --- a/dhall/src/semantics/core/visitor.rs +++ b/dhall/src/semantics/core/visitor.rs @@ -94,12 +94,16 @@ where RecordType(kts) => RecordType(v.visit_map(kts)?), RecordLit(kvs) => RecordLit(v.visit_map(kvs)?), UnionType(kts) => UnionType(v.visit_optmap(kts)?), - UnionConstructor(l, kts) => { - UnionConstructor(l.clone(), v.visit_optmap(kts)?) - } - UnionLit(l, t, kts) => { - UnionLit(l.clone(), v.visit_val(t)?, v.visit_optmap(kts)?) + UnionConstructor(l, kts, t) => { + UnionConstructor(l.clone(), v.visit_optmap(kts)?, t.clone()) } + UnionLit(l, x, kts, uniont, ctort) => UnionLit( + l.clone(), + v.visit_val(x)?, + v.visit_optmap(kts)?, + uniont.clone(), + ctort.clone(), + ), TextLit(ts) => TextLit( ts.iter() .map(|t| t.traverse_ref(|e| v.visit_val(e))) diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 541a196..f0a6a8c 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -374,9 +374,13 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> { let args = args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(*b, args, ty) } - ValueKind::UnionConstructor(l, kts) => { - ValueKind::UnionLit(l.clone(), a, kts.clone()) - } + ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( + l.clone(), + a, + kts.clone(), + uniont.clone(), + f.get_type().unwrap(), + ), _ => { drop(f_borrow); ValueKind::PartialExpr(ExprKind::App(f, a)) @@ -692,9 +696,11 @@ pub(crate) fn normalize_one_layer( Ret::Expr(expr) } }, - UnionType(kts) => { - Ret::ValueKind(UnionConstructor(l.clone(), kts.clone())) - } + UnionType(kts) => Ret::ValueKind(UnionConstructor( + l.clone(), + kts.clone(), + v.get_type().unwrap(), + )), _ => { drop(v_borrow); Ret::Expr(expr) @@ -710,7 +716,8 @@ pub(crate) fn normalize_one_layer( let handlers_borrow = handlers.as_whnf(); let variant_borrow = variant.as_whnf(); match (&*handlers_borrow, &*variant_borrow) { - (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) { + (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l) + { Some(h) => Ret::Value(h.clone()), None => { drop(handlers_borrow); @@ -718,7 +725,7 @@ pub(crate) fn normalize_one_layer( Ret::Expr(expr) } }, - (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { + (RecordLit(kvs), UnionLit(l, v, _, _, _)) => match kvs.get(l) { Some(h) => Ret::Value(h.app(v.clone())), None => { drop(handlers_borrow); diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs index 407605d..ba95847 100644 --- a/dhall/src/semantics/tck/mod.rs +++ b/dhall/src/semantics/tck/mod.rs @@ -1,2 +1,4 @@ +pub mod context; pub mod tyexpr; +pub mod typecheck; pub(crate) use tyexpr::*; diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index f0fcdd1..36cae04 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,4 +1,6 @@ #![allow(dead_code)] +use crate::error::{TypeError, TypeMessage}; +use crate::semantics::core::context::TyCtx; use crate::semantics::core::var::AlphaVar; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; @@ -33,11 +35,21 @@ impl TyExpr { pub fn kind(&self) -> &TyExprKind { &*self.kind } + pub fn get_type(&self) -> Result<Type, TypeError> { + match &self.ty { + Some(t) => Ok(t.clone()), + None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)), + } + } /// Converts a value back to the corresponding AST expression. - pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr { + pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { tyexpr_to_expr(self, opts, &mut Vec::new()) } + // TODO: temporary hack + pub fn to_value(&self) -> Value { + todo!() + } } fn tyexpr_to_expr<'a>( |