From c785b7c0c6cd8b3b1cc15eb79caf982a757020ba Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 6 Dec 2020 23:55:21 +0000 Subject: Thread cx through normalization --- dhall/src/operations/normalization.rs | 6 +-- dhall/src/operations/typecheck.rs | 72 +++++++++++++++++++---------------- 2 files changed, 43 insertions(+), 35 deletions(-) (limited to 'dhall/src/operations') diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs index 28375b2..6c68e7c 100644 --- a/dhall/src/operations/normalization.rs +++ b/dhall/src/operations/normalization.rs @@ -8,7 +8,7 @@ use crate::semantics::{ }; use crate::syntax::{ExprKind, Label, NumKind}; -fn normalize_binop(o: BinOp, x: Nir, y: Nir) -> Ret { +fn normalize_binop<'cx>(o: BinOp, x: Nir<'cx>, y: Nir<'cx>) -> Ret<'cx> { use BinOp::*; use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType}; use NumKind::{Bool, Natural}; @@ -119,7 +119,7 @@ fn normalize_binop(o: BinOp, x: Nir, y: Nir) -> Ret { } } -fn normalize_field(v: &Nir, field: &Label) -> Ret { +fn normalize_field<'cx>(v: &Nir<'cx>, field: &Label) -> Ret<'cx> { use self::BinOp::{RecursiveRecordMerge, RightBiasedRecordMerge}; use NirKind::{Op, RecordLit, UnionConstructor, UnionType}; use OpKind::{BinOp, Field, Projection}; @@ -187,7 +187,7 @@ fn normalize_field(v: &Nir, field: &Label) -> Ret { } } -pub fn normalize_operation(opkind: OpKind) -> Ret { +pub fn normalize_operation<'cx>(opkind: OpKind>) -> Ret<'cx> { use self::BinOp::RightBiasedRecordMerge; use NirKind::{ EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, Op, diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs index 5718114..9b19c84 100644 --- a/dhall/src/operations/typecheck.rs +++ b/dhall/src/operations/typecheck.rs @@ -14,8 +14,8 @@ use crate::syntax::{Const, ExprKind, Span}; fn check_rectymerge( span: &Span, env: &TyEnv<'_>, - x: Nir, - y: Nir, + x: Nir<'_>, + y: Nir<'_>, ) -> Result<(), TypeError> { let kts_x = match x.kind() { NirKind::RecordType(kts) => kts, @@ -44,13 +44,14 @@ fn check_rectymerge( Ok(()) } -fn typecheck_binop( - env: &TyEnv<'_>, +fn typecheck_binop<'cx>( + env: &TyEnv<'cx>, span: Span, op: BinOp, - l: Tir<'_>, - r: Tir<'_>, -) -> Result { + l: Tir<'cx, '_>, + r: Tir<'cx, '_>, +) -> Result, TypeError> { + let cx = env.cx(); let span_err = |msg: &str| mk_span_err(span.clone(), msg); use BinOp::*; use NirKind::{ListType, RecordType}; @@ -124,17 +125,20 @@ fn typecheck_binop( Type::from_const(Const::Type) } op => { - let t = Type::from_builtin(match op { - BoolAnd | BoolOr | BoolEQ | BoolNE => Builtin::Bool, - NaturalPlus | NaturalTimes => Builtin::Natural, - TextAppend => Builtin::Text, - ListAppend - | RightBiasedRecordMerge - | RecursiveRecordMerge - | RecursiveRecordTypeMerge - | Equivalence => unreachable!(), - ImportAlt => unreachable!("ImportAlt leftover in tck"), - }); + let t = Type::from_builtin( + cx, + match op { + BoolAnd | BoolOr | BoolEQ | BoolNE => Builtin::Bool, + NaturalPlus | NaturalTimes => Builtin::Natural, + TextAppend => Builtin::Text, + ListAppend + | RightBiasedRecordMerge + | RecursiveRecordMerge + | RecursiveRecordTypeMerge + | Equivalence => unreachable!(), + ImportAlt => unreachable!("ImportAlt leftover in tck"), + }, + ); if *l.ty() != t { return span_err("BinOpTypeMismatch"); @@ -149,13 +153,13 @@ fn typecheck_binop( }) } -fn typecheck_merge( - env: &TyEnv<'_>, +fn typecheck_merge<'cx>( + env: &TyEnv<'cx>, span: Span, - record: &Tir<'_>, - scrut: &Tir<'_>, - type_annot: Option<&Tir<'_>>, -) -> Result { + record: &Tir<'cx, '_>, + scrut: &Tir<'cx, '_>, + type_annot: Option<&Tir<'cx, '_>>, +) -> Result, TypeError> { let span_err = |msg: &str| mk_span_err(span.clone(), msg); use NirKind::{OptionalType, PiClosure, RecordType, UnionType}; @@ -287,11 +291,12 @@ fn typecheck_merge( }) } -pub fn typecheck_operation( - env: &TyEnv<'_>, +pub fn typecheck_operation<'cx>( + env: &TyEnv<'cx>, span: Span, - opkind: OpKind>, -) -> Result { + opkind: OpKind>, +) -> Result, TypeError> { + let cx = env.cx(); let span_err = |msg: &str| mk_span_err(span.clone(), msg); use NirKind::{ListType, PiClosure, RecordType, UnionType}; use OpKind::*; @@ -347,7 +352,7 @@ pub fn typecheck_operation( } BinOp(o, l, r) => typecheck_binop(env, span, o, l, r)?, BoolIf(x, y, z) => { - if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) { + if *x.ty().kind() != NirKind::from_builtin(cx, Builtin::Bool) { return span_err("InvalidPredicate"); } if y.ty().ty().as_const().is_none() { @@ -399,7 +404,7 @@ pub fn typecheck_operation( return span_err(err_msg); } match kts.get("mapKey") { - Some(t) if *t == Nir::from_builtin(Builtin::Text) => {} + Some(t) if *t == Nir::from_builtin(cx, Builtin::Text) => {} _ => return span_err(err_msg), } match kts.get("mapValue") { @@ -418,9 +423,12 @@ pub fn typecheck_operation( } let mut kts = HashMap::new(); - kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text)); + kts.insert( + "mapKey".into(), + Nir::from_builtin(cx, Builtin::Text), + ); kts.insert("mapValue".into(), entry_type); - let output_type: Type = Nir::from_builtin(Builtin::List) + let output_type: Type = Nir::from_builtin(cx, Builtin::List) .app(Nir::from_kind(RecordType(kts))) .to_type(Const::Type); if let Some(annot) = annot { -- cgit v1.2.3