summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2020-11-02 04:06:05 +0000
committerNadrieril2020-11-03 23:18:58 +0000
commit85d946016d67515aa70fa01338512e3fd7df408e (patch)
treecaebbfed831184bdf443d0b0f28dd38eea26354e /dhall
parent9e8ae42b2742e27a70a7fb8ea79ae21060d43fc1 (diff)
Typecheck `with` using mutation
Diffstat (limited to '')
-rw-r--r--dhall/src/operations/typecheck.rs63
-rw-r--r--dhall/src/semantics/tck/tir.rs3
-rw-r--r--dhall/src/semantics/tck/typecheck.rs4
3 files changed, 25 insertions, 45 deletions
diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs
index 9329aff..3016fea 100644
--- a/dhall/src/operations/typecheck.rs
+++ b/dhall/src/operations/typecheck.rs
@@ -48,8 +48,8 @@ fn typecheck_binop(
env: &TyEnv,
span: Span,
op: BinOp,
- l: &Tir<'_>,
- r: &Tir<'_>,
+ l: Tir<'_>,
+ r: Tir<'_>,
) -> Result<Type, TypeError> {
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
use BinOp::*;
@@ -290,7 +290,7 @@ fn typecheck_merge(
pub fn typecheck_operation(
env: &TyEnv,
span: Span,
- opkind: &OpKind<Tir<'_>>,
+ opkind: OpKind<Tir<'_>>,
) -> Result<Type, TypeError> {
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
use NirKind::{ListType, PiClosure, RecordType, UnionType};
@@ -345,7 +345,7 @@ pub fn typecheck_operation(
),
}
}
- BinOp(o, l, r) => typecheck_binop(env, span, *o, l, r)?,
+ BinOp(o, l, r) => typecheck_binop(env, span, o, l, r)?,
BoolIf(x, y, z) => {
if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
return span_err("InvalidPredicate");
@@ -360,7 +360,7 @@ pub fn typecheck_operation(
y.ty().clone()
}
Merge(record, scrut, type_annot) => {
- typecheck_merge(env, span, record, scrut, type_annot.as_ref())?
+ typecheck_merge(env, span, &record, &scrut, type_annot.as_ref())?
}
ToMap(record, annot) => {
if record.ty().ty().as_const() != Some(Const::Type) {
@@ -434,14 +434,14 @@ pub fn typecheck_operation(
}
Field(scrut, x) => {
match scrut.ty().kind() {
- RecordType(kts) => match kts.get(x) {
+ 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() {
- UnionType(kts) => match kts.get(x) {
+ UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => Nir::from_kind(PiClosure {
binder: Binder::new(x.clone()),
@@ -467,7 +467,7 @@ pub fn typecheck_operation(
let mut new_kts = HashMap::new();
for l in labels {
- match kts.get(l) {
+ match kts.get(&l) {
None => return span_err("ProjectionMissingEntry"),
Some(t) => {
new_kts.insert(l.clone(), t.clone());
@@ -504,45 +504,22 @@ pub fn typecheck_operation(
selection_val
}
With(record, labels, expr) => {
- use crate::syntax::Label;
- use std::iter::once;
-
- let mut current_nir: Option<Nir> =
- Some(record.ty().as_nir().clone());
- let mut visited: Vec<(&Label, HashMap<Label, Nir>)> = Vec::new();
- let mut to_create = Vec::new();
-
+ let mut record_ty = record.into_ty().into_nir();
+ let mut current = &mut record_ty;
+ // We dig through the current record type with the provided labels.
for label in labels {
- match current_nir {
- None => to_create.push(label),
- Some(nir) => {
- let kts = (match nir.kind() {
- NirKind::RecordType(kts) => Ok(kts.clone()),
- _ => mk_span_err(span.clone(), "WithMustBeRecord"), // TODO better error
- })?;
-
- current_nir = kts.get(label).cloned();
- visited.push((label, kts));
- }
+ if let RecordType(kts) = current.kind_mut() {
+ // Get existing entry or insert empty record type into it.
+ current = kts.entry(label).or_insert_with(|| {
+ Nir::from_kind(RecordType(HashMap::new()))
+ });
+ } else {
+ return mk_span_err(span.clone(), "WithMustBeRecord");
}
}
+ *current = expr.into_ty().into_nir();
- // Create Nir for record type bottom up
- let mut nir = expr.ty().as_nir().clone();
-
- while let Some(label) = to_create.pop() {
- let rec = RecordType(once((label.clone(), nir)).collect());
- nir = Nir::from_kind(rec);
- }
-
- // Update visited records
- while let Some((label, mut kts)) = visited.pop() {
- kts.insert(label.clone(), nir);
- let rec = RecordType(kts);
- nir = Nir::from_kind(rec);
- }
-
- Type::new_infer_universe(env, nir)?
+ Type::new_infer_universe(env, record_ty)?
}
Completion(..) => {
unreachable!("This case should have been handled in resolution")
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index ec15a1f..f34802c 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -117,6 +117,9 @@ impl<'hir> Tir<'hir> {
pub fn ty(&self) -> &Type {
&self.ty
}
+ pub fn into_ty(self) -> Type {
+ self.ty
+ }
pub fn to_hir(&self) -> Hir {
self.as_hir().clone()
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index d21c7ce..498bd76 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -35,7 +35,7 @@ fn type_one_layer(
) -> Result<Type, TypeError> {
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
- Ok(match &ekind {
+ Ok(match ekind {
ExprKind::Import(..) => {
unreachable!("This case should have been handled in resolution")
}
@@ -57,7 +57,7 @@ fn type_one_layer(
NumKind::Double(_) => Builtin::Double,
}),
ExprKind::Builtin(b) => {
- let t_hir = type_of_builtin(*b);
+ let t_hir = type_of_builtin(b);
typecheck(&t_hir)?.eval_to_type(env)?
}
ExprKind::TextLit(interpolated) => {