From 30bbf22fbfaead80322888eba7b7acdf908c3f3e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 17 Dec 2019 15:00:44 +0000 Subject: Rename ValueF to ValueKind --- dhall/src/semantics/phase/typecheck.rs | 72 +++++++++++++++++----------------- 1 file changed, 36 insertions(+), 36 deletions(-) (limited to 'dhall/src/semantics/phase/typecheck.rs') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 59380a3..96a0b4b 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -3,7 +3,7 @@ use std::collections::HashMap; use crate::semantics::core::context::TypecheckContext; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{Shift, Subst}; use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::merge_maps; @@ -39,8 +39,8 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(Value::from_valuef_and_type( - ValueF::Pi(x.into(), tx, te), + Ok(Value::from_kind_and_type( + ValueKind::Pi(x.into(), tx, te), Value::from_const(k), )) } @@ -71,8 +71,8 @@ fn tck_record_type( }; } - Ok(Value::from_valuef_and_type( - ValueF::RecordType(new_kts), + Ok(Value::from_kind_and_type( + ValueKind::RecordType(new_kts), Value::from_const(k), )) } @@ -116,8 +116,8 @@ where // an union type with only unary variants also has type Type let k = k.unwrap_or(Const::Type); - Ok(Value::from_valuef_and_type( - ValueF::UnionType(new_kts), + Ok(Value::from_kind_and_type( + ValueKind::UnionType(new_kts), Value::from_const(k), )) } @@ -131,13 +131,13 @@ fn function_check(a: Const, b: Const) -> Const { } pub(crate) fn const_to_value(c: Const) -> Value { - let v = ValueF::Const(c); + let v = ValueKind::Const(c); match c { Const::Type => { - Value::from_valuef_and_type(v, const_to_value(Const::Kind)) + Value::from_kind_and_type(v, const_to_value(Const::Kind)) } Const::Kind => { - Value::from_valuef_and_type(v, const_to_value(Const::Sort)) + Value::from_kind_and_type(v, const_to_value(Const::Sort)) } Const::Sort => Value::const_sort(), } @@ -290,8 +290,8 @@ fn type_of_builtin(b: Builtin) -> Expr { pub(crate) fn builtin_to_value(b: Builtin) -> Value { let ctx = TypecheckContext::new(); - Value::from_valuef_and_type( - ValueF::from_builtin(b), + Value::from_kind_and_type( + ValueKind::from_builtin(b), type_with(&ctx, type_of_builtin(b)).unwrap(), ) } @@ -313,8 +313,8 @@ fn type_with( let ctx2 = ctx.insert_type(var, annot.clone()); let body = type_with(&ctx2, body.clone())?; let body_type = body.get_type()?; - Value::from_valuef_and_type( - ValueF::Lam(var.clone().into(), annot.clone(), body), + Value::from_kind_and_type( + ValueKind::Lam(var.clone().into(), annot.clone(), body), tck_pi_type(ctx, var.clone(), annot, body_type)?, ) } @@ -389,7 +389,7 @@ fn type_last_layer( let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); let (x, tx, tb) = match &*tf_borrow { - ValueF::Pi(x, tx, tb) => (x, tx, tb), + ValueKind::Pi(x, tx, tb) => (x, tx, tb), _ => return mkerr(NotAFunction(f.clone())), }; if &a.get_type()? != tx { @@ -406,8 +406,8 @@ fn type_last_layer( } Assert(t) => { match &*t.as_whnf() { - ValueF::Equivalence(x, y) if x == y => {} - ValueF::Equivalence(x, y) => { + ValueKind::Equivalence(x, y) if x == y => {} + ValueKind::Equivalence(x, y) => { return mkerr(AssertMismatch(x.clone(), y.clone())) } _ => return mkerr(AssertMustTakeEquivalence), @@ -415,7 +415,7 @@ fn type_last_layer( RetTypeOnly(t.clone()) } BoolIf(x, y, z) => { - if *x.get_type()?.as_whnf() != ValueF::from_builtin(Bool) { + if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) { return mkerr(InvalidPredicate(x.clone())); } @@ -435,7 +435,7 @@ fn type_last_layer( } EmptyListLit(t) => { match &*t.as_whnf() { - ValueF::AppliedBuiltin(syntax::Builtin::List, args) + ValueKind::AppliedBuiltin(syntax::Builtin::List, args) if args.len() == 1 => {} _ => return mkerr(InvalidListType(t.clone())), } @@ -482,7 +482,7 @@ fn type_last_layer( )?), Field(r, x) => { match &*r.get_type()?.as_whnf() { - ValueF::RecordType(kts) => match kts.get(&x) { + ValueKind::RecordType(kts) => match kts.get(&x) { Some(tth) => { RetTypeOnly(tth.clone()) }, @@ -492,7 +492,7 @@ fn type_last_layer( // TODO: branch here only when r.get_type() is a Const _ => { match &*r.as_whnf() { - ValueF::UnionType(kts) => match kts.get(&x) { + ValueKind::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { RetTypeOnly( @@ -553,14 +553,14 @@ fn type_last_layer( // Extract the LHS record type let l_type_borrow = l_type.as_whnf(); let kts_x = match &*l_type_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(MustCombineRecord(l.clone())), }; // Extract the RHS record type let r_type_borrow = r_type.as_whnf(); let kts_y = match &*r_type_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(MustCombineRecord(r.clone())), }; @@ -589,7 +589,7 @@ fn type_last_layer( // Extract the LHS record type let borrow_l = l.as_whnf(); let kts_x = match &*borrow_l { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => { return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) } @@ -598,7 +598,7 @@ fn type_last_layer( // Extract the RHS record type let borrow_r = r.as_whnf(); let kts_y = match &*borrow_r { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => { return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) } @@ -626,7 +626,7 @@ fn type_last_layer( } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { - ValueF::AppliedBuiltin(List, _) => {} + ValueKind::AppliedBuiltin(List, _) => {} _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), } @@ -648,8 +648,8 @@ fn type_last_layer( return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone())); } - RetWhole(Value::from_valuef_and_type( - ValueF::Equivalence(l.clone(), r.clone()), + RetWhole(Value::from_kind_and_type( + ValueKind::Equivalence(l.clone(), r.clone()), Value::from_const(Type), )) } @@ -684,14 +684,14 @@ fn type_last_layer( let record_type = record.get_type()?; let record_borrow = record_type.as_whnf(); let handlers = match &*record_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(Merge1ArgMustBeRecord(record.clone())), }; let union_type = union.get_type()?; let union_borrow = union_type.as_whnf(); let variants = match &*union_borrow { - ValueF::UnionType(kts) => kts, + ValueKind::UnionType(kts) => kts, _ => return mkerr(Merge2ArgMustBeUnion(union.clone())), }; @@ -703,7 +703,7 @@ fn type_last_layer( Some(Some(variant_type)) => { let handler_type_borrow = handler_type.as_whnf(); let (x, tx, tb) = match &*handler_type_borrow { - ValueF::Pi(x, tx, tb) => (x, tx, tb), + ValueKind::Pi(x, tx, tb) => (x, tx, tb), _ => { return mkerr(NotAFunction( handler_type.clone(), @@ -765,7 +765,7 @@ fn type_last_layer( let record_type = record.get_type()?; let record_type_borrow = record_type.as_whnf(); let kts = match &*record_type_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(ProjectionMustBeRecord), }; @@ -777,8 +777,8 @@ fn type_last_layer( }; } - RetTypeOnly(Value::from_valuef_and_type( - ValueF::RecordType(new_kts), + RetTypeOnly(Value::from_kind_and_type( + ValueKind::RecordType(new_kts), record_type.get_type()?, )) } @@ -786,8 +786,8 @@ fn type_last_layer( }; Ok(match ret { - RetTypeOnly(typ) => Value::from_valuef_and_type_and_span( - ValueF::PartialExpr(e), + RetTypeOnly(typ) => Value::from_kind_and_type_and_span( + ValueKind::PartialExpr(e), typ, span, ), -- cgit v1.2.3 From 78d066a44c5598794602effa4c10a09f80ed1e72 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 17:57:49 +0000 Subject: Move error module to root of crate --- dhall/src/semantics/phase/typecheck.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/phase/typecheck.rs') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 96a0b4b..5041235 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -1,11 +1,11 @@ use std::cmp::max; use std::collections::HashMap; +use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TypecheckContext; use crate::semantics::core::value::Value; use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{Shift, Subst}; -use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; use crate::syntax; -- cgit v1.2.3 From e355984c3c83f8288eac36023c361db869643367 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 18:12:10 +0000 Subject: s/ExprF/ExprKind/ --- dhall/src/semantics/phase/typecheck.rs | 45 +++++++++++++++++----------------- 1 file changed, 23 insertions(+), 22 deletions(-) (limited to 'dhall/src/semantics/phase/typecheck.rs') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 5041235..f83bb94 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -10,7 +10,8 @@ use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; use crate::syntax; use crate::syntax::{ - Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span, + Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, RawExpr, + Span, }; fn tck_pi_type( @@ -149,24 +150,24 @@ pub fn rc(x: RawExpr) -> Expr { // Ad-hoc macro to help construct the types of builtins macro_rules! make_type { - (Type) => { ExprF::Const(Const::Type) }; - (Bool) => { ExprF::Builtin(Builtin::Bool) }; - (Natural) => { ExprF::Builtin(Builtin::Natural) }; - (Integer) => { ExprF::Builtin(Builtin::Integer) }; - (Double) => { ExprF::Builtin(Builtin::Double) }; - (Text) => { ExprF::Builtin(Builtin::Text) }; + (Type) => { ExprKind::Const(Const::Type) }; + (Bool) => { ExprKind::Builtin(Builtin::Bool) }; + (Natural) => { ExprKind::Builtin(Builtin::Natural) }; + (Integer) => { ExprKind::Builtin(Builtin::Integer) }; + (Double) => { ExprKind::Builtin(Builtin::Double) }; + (Text) => { ExprKind::Builtin(Builtin::Text) }; ($var:ident) => { - ExprF::Var(syntax::V(stringify!($var).into(), 0)) + ExprKind::Var(syntax::V(stringify!($var).into(), 0)) }; (Optional $ty:ident) => { - ExprF::App( - rc(ExprF::Builtin(Builtin::Optional)), + ExprKind::App( + rc(ExprKind::Builtin(Builtin::Optional)), rc(make_type!($ty)) ) }; (List $($rest:tt)*) => { - ExprF::App( - rc(ExprF::Builtin(Builtin::List)), + ExprKind::App( + rc(ExprKind::Builtin(Builtin::List)), rc(make_type!($($rest)*)) ) }; @@ -178,24 +179,24 @@ macro_rules! make_type { rc(make_type!($ty)), ); )* - ExprF::RecordType(kts) + ExprKind::RecordType(kts) }}; ($ty:ident -> $($rest:tt)*) => { - ExprF::Pi( + ExprKind::Pi( "_".into(), rc(make_type!($ty)), rc(make_type!($($rest)*)) ) }; (($($arg:tt)*) -> $($rest:tt)*) => { - ExprF::Pi( + ExprKind::Pi( "_".into(), rc(make_type!($($arg)*)), rc(make_type!($($rest)*)) ) }; (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - ExprF::Pi( + ExprKind::Pi( stringify!($var).into(), rc(make_type!($($ty)*)), rc(make_type!($($rest)*)) @@ -304,7 +305,7 @@ fn type_with( ctx: &TypecheckContext, e: Expr, ) -> Result { - use syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; + use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var}; let span = e.span(); Ok(match e.as_ref() { @@ -359,13 +360,13 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: ExprF, + e: ExprKind, span: Span, ) -> Result { use syntax::BinOp::*; use syntax::Builtin::*; use syntax::Const::Type; - use syntax::ExprF::*; + use syntax::ExprKind::*; use TypeMessage::*; let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg)); @@ -578,7 +579,7 @@ fn type_last_layer( } BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer( ctx, - ExprF::BinOp( + ExprKind::BinOp( RecursiveRecordTypeMerge, l.get_type()?, r.get_type()?, @@ -612,7 +613,7 @@ fn type_last_layer( |_, l: &Value, r: &Value| { type_last_layer( ctx, - ExprF::BinOp( + ExprKind::BinOp( RecursiveRecordTypeMerge, l.clone(), r.clone(), @@ -806,5 +807,5 @@ pub(crate) fn typecheck_with( expr: Expr, ty: Expr, ) -> Result { - typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty))) + typecheck(expr.rewrap(ExprKind::Annot(expr.clone(), ty))) } -- cgit v1.2.3 From 980e50f33a88559edcf8b12cdec91fd9bee84ca9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 19:01:07 +0000 Subject: s/RawExpr/UnspannedExpr/ --- dhall/src/semantics/phase/typecheck.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics/phase/typecheck.rs') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index f83bb94..cf928d8 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -10,8 +10,8 @@ use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; use crate::syntax; use crate::syntax::{ - Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, RawExpr, - Span, + Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, + UnspannedExpr, }; fn tck_pi_type( @@ -144,7 +144,7 @@ pub(crate) fn const_to_value(c: Const) -> Value { } } -pub fn rc(x: RawExpr) -> Expr { +pub fn rc(x: UnspannedExpr) -> Expr { Expr::new(x, Span::Artificial) } -- cgit v1.2.3 From 64cca1837cc97b7679c4e2ffd54a22ad50f05cfd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 19:26:08 +0000 Subject: Move ValueKind into value.rs --- dhall/src/semantics/phase/typecheck.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/phase/typecheck.rs') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index cf928d8..c439f74 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -4,7 +4,7 @@ use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TypecheckContext; use crate::semantics::core::value::Value; -use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{Shift, Subst}; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; -- cgit v1.2.3