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/core/context.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/core/context.rs') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index d150e56..8861378 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::rc::Rc; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::error::TypeError; use crate::syntax::{Label, V}; @@ -39,7 +39,7 @@ impl TypecheckContext { let i = i.under_multiple_binders(&shift_map); return Some(match i { CtxItem::Kept(newvar, t) => { - Value::from_valuef_and_type(ValueF::Var(newvar), t) + Value::from_kind_and_type(ValueKind::Var(newvar), t) } CtxItem::Replaced(v) => v, }); -- cgit v1.3.1 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/error/mod.rs | 178 +++++++++++++++++++++++++++++++++ dhall/src/lib.rs | 1 + dhall/src/semantics/core/context.rs | 2 +- dhall/src/semantics/core/value.rs | 2 +- dhall/src/semantics/error/mod.rs | 178 --------------------------------- dhall/src/semantics/mod.rs | 1 - dhall/src/semantics/phase/mod.rs | 2 +- dhall/src/semantics/phase/parse.rs | 2 +- dhall/src/semantics/phase/resolve.rs | 2 +- dhall/src/semantics/phase/typecheck.rs | 2 +- dhall/src/syntax/binary/decode.rs | 2 +- dhall/src/syntax/binary/encode.rs | 2 +- dhall/src/tests.rs | 2 +- serde_dhall/src/lib.rs | 4 +- 14 files changed, 190 insertions(+), 190 deletions(-) create mode 100644 dhall/src/error/mod.rs delete mode 100644 dhall/src/semantics/error/mod.rs (limited to 'dhall/src/semantics/core/context.rs') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs new file mode 100644 index 0000000..1288c12 --- /dev/null +++ b/dhall/src/error/mod.rs @@ -0,0 +1,178 @@ +use std::io::Error as IOError; + +use crate::semantics::core::context::TypecheckContext; +use crate::semantics::core::value::Value; +use crate::semantics::phase::resolve::ImportStack; +use crate::semantics::phase::NormalizedExpr; +use crate::syntax::{BinOp, Import, Label, ParseError, Span}; + +pub type Result = std::result::Result; + +#[derive(Debug)] +#[non_exhaustive] +pub enum Error { + IO(IOError), + Parse(ParseError), + Decode(DecodeError), + Encode(EncodeError), + Resolve(ImportError), + Typecheck(TypeError), +} + +#[derive(Debug)] +pub enum ImportError { + Recursive(Import, Box), + UnexpectedImport(Import), + ImportCycle(ImportStack, Import), +} + +#[derive(Debug)] +pub enum DecodeError { + CBORError(serde_cbor::error::Error), + WrongFormatError(String), +} + +#[derive(Debug)] +pub enum EncodeError { + CBORError(serde_cbor::error::Error), +} + +/// A structured type error that includes context +#[derive(Debug)] +pub struct TypeError { + message: TypeMessage, + context: TypecheckContext, +} + +/// The specific type error +#[derive(Debug)] +pub(crate) enum TypeMessage { + UnboundVariable(Span), + InvalidInputType(Value), + InvalidOutputType(Value), + NotAFunction(Value), + TypeMismatch(Value, Value, Value), + AnnotMismatch(Value, Value), + InvalidListElement(usize, Value, Value), + InvalidListType(Value), + InvalidOptionalType(Value), + InvalidPredicate(Value), + IfBranchMismatch(Value, Value), + IfBranchMustBeTerm(bool, Value), + InvalidFieldType(Label, Value), + NotARecord(Label, Value), + MustCombineRecord(Value), + MissingRecordField(Label, Value), + MissingUnionField(Label, Value), + BinOpTypeMismatch(BinOp, Value), + InvalidTextInterpolation(Value), + Merge1ArgMustBeRecord(Value), + Merge2ArgMustBeUnion(Value), + MergeEmptyNeedsAnnotation, + MergeHandlerMissingVariant(Label), + MergeVariantMissingHandler(Label), + MergeAnnotMismatch, + MergeHandlerTypeMismatch, + MergeHandlerReturnTypeMustNotBeDependent, + ProjectionMustBeRecord, + ProjectionMissingEntry, + Sort, + RecordTypeDuplicateField, + RecordTypeMergeRequiresRecordType(Value), + UnionTypeDuplicateField, + EquivalenceArgumentMustBeTerm(bool, Value), + EquivalenceTypeMismatch(Value, Value), + AssertMismatch(Value, Value), + AssertMustTakeEquivalence, +} + +impl TypeError { + pub(crate) fn new( + context: &TypecheckContext, + message: TypeMessage, + ) -> Self { + TypeError { + context: context.clone(), + message, + } + } +} + +impl std::fmt::Display for TypeError { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + use TypeMessage::*; + let msg = match &self.message { + UnboundVariable(span) => span.error("Type error: Unbound variable"), + InvalidInputType(v) => { + v.span().error("Type error: Invalid function input") + } + InvalidOutputType(v) => { + v.span().error("Type error: Invalid function output") + } + NotAFunction(v) => v.span().error("Type error: Not a function"), + TypeMismatch(x, y, z) => { + x.span() + .error("Type error: Wrong type of function argument") + + "\n" + + &z.span().error(format!( + "This argument has type {:?}", + z.get_type().unwrap() + )) + + "\n" + + &y.span().error(format!( + "But the function expected an argument of type {:?}", + y + )) + } + _ => "Type error: Unhandled error".to_string(), + }; + write!(f, "{}", msg) + } +} + +impl std::error::Error for TypeError {} + +impl std::fmt::Display for Error { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + match self { + Error::IO(err) => write!(f, "{}", err), + Error::Parse(err) => write!(f, "{}", err), + Error::Decode(err) => write!(f, "{:?}", err), + Error::Encode(err) => write!(f, "{:?}", err), + Error::Resolve(err) => write!(f, "{:?}", err), + Error::Typecheck(err) => write!(f, "{}", err), + } + } +} + +impl std::error::Error for Error {} +impl From for Error { + fn from(err: IOError) -> Error { + Error::IO(err) + } +} +impl From for Error { + fn from(err: ParseError) -> Error { + Error::Parse(err) + } +} +impl From for Error { + fn from(err: DecodeError) -> Error { + Error::Decode(err) + } +} +impl From for Error { + fn from(err: EncodeError) -> Error { + Error::Encode(err) + } +} +impl From for Error { + fn from(err: ImportError) -> Error { + Error::Resolve(err) + } +} +impl From for Error { + fn from(err: TypeError) -> Error { + Error::Typecheck(err) + } +} diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 0991375..12660b4 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -12,5 +12,6 @@ mod tests; +pub mod error; pub mod semantics; pub mod syntax; diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 8861378..9dfd22b 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -1,10 +1,10 @@ use std::collections::HashMap; use std::rc::Rc; +use crate::error::TypeError; use crate::semantics::core::value::Value; use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::TypeError; use crate::syntax::{Label, V}; #[derive(Debug, Clone)] diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index ad0861b..9511cc2 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -1,10 +1,10 @@ use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; +use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TypecheckContext; use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{NormalizedExpr, Typed}; diff --git a/dhall/src/semantics/error/mod.rs b/dhall/src/semantics/error/mod.rs deleted file mode 100644 index 1288c12..0000000 --- a/dhall/src/semantics/error/mod.rs +++ /dev/null @@ -1,178 +0,0 @@ -use std::io::Error as IOError; - -use crate::semantics::core::context::TypecheckContext; -use crate::semantics::core::value::Value; -use crate::semantics::phase::resolve::ImportStack; -use crate::semantics::phase::NormalizedExpr; -use crate::syntax::{BinOp, Import, Label, ParseError, Span}; - -pub type Result = std::result::Result; - -#[derive(Debug)] -#[non_exhaustive] -pub enum Error { - IO(IOError), - Parse(ParseError), - Decode(DecodeError), - Encode(EncodeError), - Resolve(ImportError), - Typecheck(TypeError), -} - -#[derive(Debug)] -pub enum ImportError { - Recursive(Import, Box), - UnexpectedImport(Import), - ImportCycle(ImportStack, Import), -} - -#[derive(Debug)] -pub enum DecodeError { - CBORError(serde_cbor::error::Error), - WrongFormatError(String), -} - -#[derive(Debug)] -pub enum EncodeError { - CBORError(serde_cbor::error::Error), -} - -/// A structured type error that includes context -#[derive(Debug)] -pub struct TypeError { - message: TypeMessage, - context: TypecheckContext, -} - -/// The specific type error -#[derive(Debug)] -pub(crate) enum TypeMessage { - UnboundVariable(Span), - InvalidInputType(Value), - InvalidOutputType(Value), - NotAFunction(Value), - TypeMismatch(Value, Value, Value), - AnnotMismatch(Value, Value), - InvalidListElement(usize, Value, Value), - InvalidListType(Value), - InvalidOptionalType(Value), - InvalidPredicate(Value), - IfBranchMismatch(Value, Value), - IfBranchMustBeTerm(bool, Value), - InvalidFieldType(Label, Value), - NotARecord(Label, Value), - MustCombineRecord(Value), - MissingRecordField(Label, Value), - MissingUnionField(Label, Value), - BinOpTypeMismatch(BinOp, Value), - InvalidTextInterpolation(Value), - Merge1ArgMustBeRecord(Value), - Merge2ArgMustBeUnion(Value), - MergeEmptyNeedsAnnotation, - MergeHandlerMissingVariant(Label), - MergeVariantMissingHandler(Label), - MergeAnnotMismatch, - MergeHandlerTypeMismatch, - MergeHandlerReturnTypeMustNotBeDependent, - ProjectionMustBeRecord, - ProjectionMissingEntry, - Sort, - RecordTypeDuplicateField, - RecordTypeMergeRequiresRecordType(Value), - UnionTypeDuplicateField, - EquivalenceArgumentMustBeTerm(bool, Value), - EquivalenceTypeMismatch(Value, Value), - AssertMismatch(Value, Value), - AssertMustTakeEquivalence, -} - -impl TypeError { - pub(crate) fn new( - context: &TypecheckContext, - message: TypeMessage, - ) -> Self { - TypeError { - context: context.clone(), - message, - } - } -} - -impl std::fmt::Display for TypeError { - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - use TypeMessage::*; - let msg = match &self.message { - UnboundVariable(span) => span.error("Type error: Unbound variable"), - InvalidInputType(v) => { - v.span().error("Type error: Invalid function input") - } - InvalidOutputType(v) => { - v.span().error("Type error: Invalid function output") - } - NotAFunction(v) => v.span().error("Type error: Not a function"), - TypeMismatch(x, y, z) => { - x.span() - .error("Type error: Wrong type of function argument") - + "\n" - + &z.span().error(format!( - "This argument has type {:?}", - z.get_type().unwrap() - )) - + "\n" - + &y.span().error(format!( - "But the function expected an argument of type {:?}", - y - )) - } - _ => "Type error: Unhandled error".to_string(), - }; - write!(f, "{}", msg) - } -} - -impl std::error::Error for TypeError {} - -impl std::fmt::Display for Error { - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - match self { - Error::IO(err) => write!(f, "{}", err), - Error::Parse(err) => write!(f, "{}", err), - Error::Decode(err) => write!(f, "{:?}", err), - Error::Encode(err) => write!(f, "{:?}", err), - Error::Resolve(err) => write!(f, "{:?}", err), - Error::Typecheck(err) => write!(f, "{}", err), - } - } -} - -impl std::error::Error for Error {} -impl From for Error { - fn from(err: IOError) -> Error { - Error::IO(err) - } -} -impl From for Error { - fn from(err: ParseError) -> Error { - Error::Parse(err) - } -} -impl From for Error { - fn from(err: DecodeError) -> Error { - Error::Decode(err) - } -} -impl From for Error { - fn from(err: EncodeError) -> Error { - Error::Encode(err) - } -} -impl From for Error { - fn from(err: ImportError) -> Error { - Error::Resolve(err) - } -} -impl From for Error { - fn from(err: TypeError) -> Error { - Error::Typecheck(err) - } -} diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 6438408..1eeef86 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,4 +1,3 @@ pub mod core; -pub mod error; pub mod phase; pub mod to_expr; diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 6229d15..9359c0b 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -1,10 +1,10 @@ use std::fmt::Display; use std::path::Path; +use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; diff --git a/dhall/src/semantics/phase/parse.rs b/dhall/src/semantics/phase/parse.rs index 4c8ad7b..00db422 100644 --- a/dhall/src/semantics/phase/parse.rs +++ b/dhall/src/semantics/phase/parse.rs @@ -2,7 +2,7 @@ use std::fs::File; use std::io::Read; use std::path::Path; -use crate::semantics::error::Error; +use crate::error::Error; use crate::semantics::phase::resolve::ImportRoot; use crate::semantics::phase::Parsed; use crate::syntax::binary; diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs index 86dc7ae..cc4a024 100644 --- a/dhall/src/semantics/phase/resolve.rs +++ b/dhall/src/semantics/phase/resolve.rs @@ -1,7 +1,7 @@ use std::collections::HashMap; use std::path::{Path, PathBuf}; -use crate::semantics::error::{Error, ImportError}; +use crate::error::{Error, ImportError}; use crate::semantics::phase::{Normalized, NormalizedExpr, Parsed, Resolved}; use crate::syntax; use crate::syntax::{FilePath, ImportLocation, URL}; 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; diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs index 46c9921..f452666 100644 --- a/dhall/src/syntax/binary/decode.rs +++ b/dhall/src/syntax/binary/decode.rs @@ -2,7 +2,7 @@ use itertools::Itertools; use serde_cbor::value::value as cbor; use std::iter::FromIterator; -use crate::semantics::error::DecodeError; +use crate::error::DecodeError; use crate::semantics::phase::DecodedExpr; use crate::syntax; use crate::syntax::{ diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs index 8e13efd..c1e7c4c 100644 --- a/dhall/src/syntax/binary/encode.rs +++ b/dhall/src/syntax/binary/encode.rs @@ -1,7 +1,7 @@ use serde_cbor::value::value as cbor; use std::vec; -use crate::semantics::error::EncodeError; +use crate::error::EncodeError; use crate::syntax; use crate::syntax::map::DupTreeMap; use crate::syntax::{ diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 9e5c744..d73c2d4 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -47,7 +47,7 @@ use std::fs::File; use std::io::{Read, Write}; use std::path::PathBuf; -use crate::semantics::error::{Error, Result}; +use crate::error::{Error, Result}; use crate::semantics::phase::Parsed; #[allow(dead_code)] diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs index 80ebaf8..2863788 100644 --- a/serde_dhall/src/lib.rs +++ b/serde_dhall/src/lib.rs @@ -138,7 +138,7 @@ pub mod value { fn from_str_using_dhall_error_type( s: &str, ty: Option<&Value>, - ) -> dhall::semantics::error::Result { + ) -> dhall::error::Result { let resolved = Parsed::parse_str(s)?.resolve()?; let typed = match ty { None => resolved.typecheck()?, @@ -193,7 +193,7 @@ pub mod de { pub use error::{Error, Result}; mod error { - use dhall::semantics::error::Error as DhallError; + use dhall::error::Error as DhallError; pub type Result = std::result::Result; -- cgit v1.3.1 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/core/context.rs | 2 +- dhall/src/semantics/core/mod.rs | 1 - dhall/src/semantics/core/value.rs | 270 ++++++++++++++++++++++++++++++++- dhall/src/semantics/core/value_kind.rs | 267 -------------------------------- dhall/src/semantics/phase/mod.rs | 2 +- dhall/src/semantics/phase/normalize.rs | 2 +- dhall/src/semantics/phase/typecheck.rs | 2 +- dhall/src/semantics/to_expr.rs | 2 +- 8 files changed, 269 insertions(+), 279 deletions(-) delete mode 100644 dhall/src/semantics/core/value_kind.rs (limited to 'dhall/src/semantics/core/context.rs') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 9dfd22b..f755f72 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -3,7 +3,7 @@ use std::rc::Rc; use crate::error::TypeError; use crate::semantics::core::value::Value; -use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::syntax::{Label, V}; diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs index bf3d390..90d74ea 100644 --- a/dhall/src/semantics/core/mod.rs +++ b/dhall/src/semantics/core/mod.rs @@ -1,4 +1,3 @@ pub mod context; pub mod value; -pub mod value_kind; pub mod var; diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 1e3b965..ca7c4bc 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -1,21 +1,27 @@ use std::cell::{Ref, RefCell, RefMut}; +use std::collections::HashMap; use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TypecheckContext; -use crate::semantics::core::value_kind::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; +use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; -use crate::semantics::phase::{NormalizedExpr, Typed}; +use crate::semantics::phase::{Normalized, NormalizedExpr, Typed}; use crate::semantics::to_expr; -use crate::syntax::{Builtin, Const, Span}; +use crate::syntax::{ + Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, + NaiveDouble, Natural, Span, +}; use self::Form::{Unevaled, NF, WHNF}; -/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, -/// sharing computation automatically. Uses a RefCell to share computation. +/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation +/// automatically. Uses a RefCell to share computation. /// Can optionally store a type from typechecking to preserve type information. +/// If you compare for equality two `Value`s in WHNF, then equality will be up to alpha-equivalence +/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively +/// normalize as needed. #[derive(Clone)] pub(crate) struct Value(Rc>); @@ -45,6 +51,38 @@ pub(crate) enum Form { NF, } +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) enum ValueKind { + /// Closures + Lam(AlphaLabel, Value, Value), + Pi(AlphaLabel, Value, Value), + // Invariant: in whnf, the evaluation must not be able to progress further. + AppliedBuiltin(Builtin, Vec), + + Var(AlphaVar), + Const(Const), + BoolLit(bool), + NaturalLit(Natural), + IntegerLit(Integer), + DoubleLit(NaiveDouble), + EmptyOptionalLit(Value), + NEOptionalLit(Value), + // EmptyListLit(t) means `[] : List t`, not `[] : t` + EmptyListLit(Value), + NEListLit(Vec), + RecordType(HashMap), + RecordLit(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Value, HashMap>), + // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec>), + Equivalence(Value, Value), + // Invariant: in whnf, this must not contain a value captured by one of the variants above. + PartialExpr(ExprKind), +} + impl Value { fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { ValueInternal { @@ -258,6 +296,94 @@ impl ValueInternal { } } +impl ValueKind { + pub(crate) fn into_value_with_type(self, t: Value) -> Value { + Value::from_kind_and_type(self, t) + } + + /// Converts a value back to the corresponding AST expression. + pub(crate) fn to_expr( + &self, + opts: to_expr::ToExprOptions, + ) -> NormalizedExpr { + to_expr::kind_to_expr(self, opts) + } + + pub(crate) fn normalize_mut(&mut self) { + match self { + ValueKind::Var(_) + | ValueKind::Const(_) + | ValueKind::BoolLit(_) + | ValueKind::NaturalLit(_) + | ValueKind::IntegerLit(_) + | ValueKind::DoubleLit(_) => {} + + ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { + tth.normalize_mut(); + } + + ValueKind::NEOptionalLit(th) => { + th.normalize_mut(); + } + ValueKind::Lam(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueKind::Pi(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueKind::AppliedBuiltin(_, args) => { + for x in args.iter_mut() { + x.normalize_mut(); + } + } + ValueKind::NEListLit(elts) => { + for x in elts.iter_mut() { + x.normalize_mut(); + } + } + ValueKind::RecordLit(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueKind::RecordType(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueKind::UnionLit(_, v, kts) => { + v.normalize_mut(); + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueKind::TextLit(elts) => { + for x in elts.iter_mut() { + x.map_mut(Value::normalize_mut); + } + } + ValueKind::Equivalence(x, y) => { + x.normalize_mut(); + y.normalize_mut(); + } + ValueKind::PartialExpr(e) => { + e.map_mut(Value::normalize_mut); + } + } + } + + pub(crate) fn from_builtin(b: Builtin) -> ValueKind { + ValueKind::AppliedBuiltin(b, vec![]) + } +} + impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(Value(self.0.shift(delta, var)?)) @@ -275,6 +401,71 @@ impl Shift for ValueInternal { } } +impl Shift for ValueKind { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(match self { + ValueKind::Lam(x, t, e) => ValueKind::Lam( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueKind::AppliedBuiltin(b, args) => { + ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?) + } + ValueKind::Pi(x, t, e) => ValueKind::Pi( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), + ValueKind::Const(c) => ValueKind::Const(*c), + ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), + ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), + ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), + ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), + ValueKind::EmptyOptionalLit(tth) => { + ValueKind::EmptyOptionalLit(tth.shift(delta, var)?) + } + ValueKind::NEOptionalLit(th) => { + ValueKind::NEOptionalLit(th.shift(delta, var)?) + } + ValueKind::EmptyListLit(tth) => { + ValueKind::EmptyListLit(tth.shift(delta, var)?) + } + ValueKind::NEListLit(elts) => { + ValueKind::NEListLit(elts.shift(delta, var)?) + } + ValueKind::RecordLit(kvs) => { + ValueKind::RecordLit(kvs.shift(delta, var)?) + } + ValueKind::RecordType(kvs) => { + ValueKind::RecordType(kvs.shift(delta, var)?) + } + ValueKind::UnionType(kts) => { + ValueKind::UnionType(kts.shift(delta, var)?) + } + ValueKind::UnionConstructor(x, kts) => { + ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?) + } + ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( + x.clone(), + v.shift(delta, var)?, + kts.shift(delta, var)?, + ), + ValueKind::TextLit(elts) => { + ValueKind::TextLit(elts.shift(delta, var)?) + } + ValueKind::Equivalence(x, y) => ValueKind::Equivalence( + x.shift(delta, var)?, + y.shift(delta, var)?, + ), + ValueKind::PartialExpr(e) => { + ValueKind::PartialExpr(e.shift(delta, var)?) + } + }) + } +} + impl Subst for Value { fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match &*self.as_kind() { @@ -303,6 +494,73 @@ impl Subst for ValueInternal { } } +impl Subst for ValueKind { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + match self { + ValueKind::AppliedBuiltin(b, args) => { + ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val)) + } + ValueKind::PartialExpr(e) => { + ValueKind::PartialExpr(e.subst_shift(var, val)) + } + ValueKind::TextLit(elts) => { + ValueKind::TextLit(elts.subst_shift(var, val)) + } + ValueKind::Lam(x, t, e) => ValueKind::Lam( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueKind::Pi(x, t, e) => ValueKind::Pi( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), + ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), + ValueKind::Const(c) => ValueKind::Const(*c), + ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), + ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), + ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), + ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), + ValueKind::EmptyOptionalLit(tth) => { + ValueKind::EmptyOptionalLit(tth.subst_shift(var, val)) + } + ValueKind::NEOptionalLit(th) => { + ValueKind::NEOptionalLit(th.subst_shift(var, val)) + } + ValueKind::EmptyListLit(tth) => { + ValueKind::EmptyListLit(tth.subst_shift(var, val)) + } + ValueKind::NEListLit(elts) => { + ValueKind::NEListLit(elts.subst_shift(var, val)) + } + ValueKind::RecordLit(kvs) => { + ValueKind::RecordLit(kvs.subst_shift(var, val)) + } + ValueKind::RecordType(kvs) => { + ValueKind::RecordType(kvs.subst_shift(var, val)) + } + ValueKind::UnionType(kts) => { + ValueKind::UnionType(kts.subst_shift(var, val)) + } + ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor( + x.clone(), + kts.subst_shift(var, val), + ), + ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( + x.clone(), + v.subst_shift(var, val), + kts.subst_shift(var, val), + ), + ValueKind::Equivalence(x, y) => ValueKind::Equivalence( + x.subst_shift(var, val), + y.subst_shift(var, val), + ), + } + } +} + // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs deleted file mode 100644 index 35b2b23..0000000 --- a/dhall/src/semantics/core/value_kind.rs +++ /dev/null @@ -1,267 +0,0 @@ -use std::collections::HashMap; - -use crate::semantics::core::value::Value; -use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::semantics::phase::{Normalized, NormalizedExpr}; -use crate::semantics::to_expr; -use crate::syntax::{ - Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, -}; - -/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are -/// normalized on-demand. -/// If you compare for equality two `ValueKind`s in WHNF, then equality will be up to -/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will -/// recursively normalize as needed. -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ValueKind { - /// Closures - Lam(AlphaLabel, Value, Value), - Pi(AlphaLabel, Value, Value), - // Invariant: in whnf, the evaluation must not be able to progress further. - AppliedBuiltin(Builtin, Vec), - - Var(AlphaVar), - Const(Const), - BoolLit(bool), - NaturalLit(Natural), - IntegerLit(Integer), - DoubleLit(NaiveDouble), - EmptyOptionalLit(Value), - NEOptionalLit(Value), - // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(Value), - NEListLit(Vec), - RecordType(HashMap), - RecordLit(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Value, HashMap>), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), - Equivalence(Value, Value), - // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprKind), -} - -impl ValueKind { - pub(crate) fn into_value_with_type(self, t: Value) -> Value { - Value::from_kind_and_type(self, t) - } - - /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr( - &self, - opts: to_expr::ToExprOptions, - ) -> NormalizedExpr { - to_expr::kind_to_expr(self, opts) - } - - pub(crate) fn normalize_mut(&mut self) { - match self { - ValueKind::Var(_) - | ValueKind::Const(_) - | ValueKind::BoolLit(_) - | ValueKind::NaturalLit(_) - | ValueKind::IntegerLit(_) - | ValueKind::DoubleLit(_) => {} - - ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { - tth.normalize_mut(); - } - - ValueKind::NEOptionalLit(th) => { - th.normalize_mut(); - } - ValueKind::Lam(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueKind::Pi(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueKind::AppliedBuiltin(_, args) => { - for x in args.iter_mut() { - x.normalize_mut(); - } - } - ValueKind::NEListLit(elts) => { - for x in elts.iter_mut() { - x.normalize_mut(); - } - } - ValueKind::RecordLit(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueKind::RecordType(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueKind::UnionLit(_, v, kts) => { - v.normalize_mut(); - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueKind::TextLit(elts) => { - for x in elts.iter_mut() { - x.map_mut(Value::normalize_mut); - } - } - ValueKind::Equivalence(x, y) => { - x.normalize_mut(); - y.normalize_mut(); - } - ValueKind::PartialExpr(e) => { - e.map_mut(Value::normalize_mut); - } - } - } - - pub(crate) fn from_builtin(b: Builtin) -> ValueKind { - ValueKind::AppliedBuiltin(b, vec![]) - } -} - -impl Shift for ValueKind { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - ValueKind::Lam(x, t, e) => ValueKind::Lam( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueKind::AppliedBuiltin(b, args) => { - ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?) - } - ValueKind::Pi(x, t, e) => ValueKind::Pi( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), - ValueKind::Const(c) => ValueKind::Const(*c), - ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), - ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), - ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), - ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), - ValueKind::EmptyOptionalLit(tth) => { - ValueKind::EmptyOptionalLit(tth.shift(delta, var)?) - } - ValueKind::NEOptionalLit(th) => { - ValueKind::NEOptionalLit(th.shift(delta, var)?) - } - ValueKind::EmptyListLit(tth) => { - ValueKind::EmptyListLit(tth.shift(delta, var)?) - } - ValueKind::NEListLit(elts) => { - ValueKind::NEListLit(elts.shift(delta, var)?) - } - ValueKind::RecordLit(kvs) => { - ValueKind::RecordLit(kvs.shift(delta, var)?) - } - ValueKind::RecordType(kvs) => { - ValueKind::RecordType(kvs.shift(delta, var)?) - } - ValueKind::UnionType(kts) => { - ValueKind::UnionType(kts.shift(delta, var)?) - } - ValueKind::UnionConstructor(x, kts) => { - ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?) - } - ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( - x.clone(), - v.shift(delta, var)?, - kts.shift(delta, var)?, - ), - ValueKind::TextLit(elts) => { - ValueKind::TextLit(elts.shift(delta, var)?) - } - ValueKind::Equivalence(x, y) => ValueKind::Equivalence( - x.shift(delta, var)?, - y.shift(delta, var)?, - ), - ValueKind::PartialExpr(e) => { - ValueKind::PartialExpr(e.shift(delta, var)?) - } - }) - } -} - -impl Subst for ValueKind { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - ValueKind::AppliedBuiltin(b, args) => { - ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val)) - } - ValueKind::PartialExpr(e) => { - ValueKind::PartialExpr(e.subst_shift(var, val)) - } - ValueKind::TextLit(elts) => { - ValueKind::TextLit(elts.subst_shift(var, val)) - } - ValueKind::Lam(x, t, e) => ValueKind::Lam( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueKind::Pi(x, t, e) => ValueKind::Pi( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), - ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), - ValueKind::Const(c) => ValueKind::Const(*c), - ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), - ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), - ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), - ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), - ValueKind::EmptyOptionalLit(tth) => { - ValueKind::EmptyOptionalLit(tth.subst_shift(var, val)) - } - ValueKind::NEOptionalLit(th) => { - ValueKind::NEOptionalLit(th.subst_shift(var, val)) - } - ValueKind::EmptyListLit(tth) => { - ValueKind::EmptyListLit(tth.subst_shift(var, val)) - } - ValueKind::NEListLit(elts) => { - ValueKind::NEListLit(elts.subst_shift(var, val)) - } - ValueKind::RecordLit(kvs) => { - ValueKind::RecordLit(kvs.subst_shift(var, val)) - } - ValueKind::RecordType(kvs) => { - ValueKind::RecordType(kvs.subst_shift(var, val)) - } - ValueKind::UnionType(kts) => { - ValueKind::UnionType(kts.subst_shift(var, val)) - } - ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor( - x.clone(), - kts.subst_shift(var, val), - ), - ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( - x.clone(), - v.subst_shift(var, val), - kts.subst_shift(var, val), - ), - ValueKind::Equivalence(x, y) => ValueKind::Equivalence( - x.subst_shift(var, val), - y.subst_shift(var, val), - ), - } - } -} diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 7c57c3f..b22120d 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -3,7 +3,7 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; -use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 3e612aa..d81a910 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,7 +1,7 @@ use std::collections::HashMap; use crate::semantics::core::value::Value; -use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::Normalized; use crate::syntax; 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; diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index 6099976..b21fb29 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -1,5 +1,5 @@ use crate::semantics::core::value::Value; -use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::NormalizedExpr; use crate::syntax; -- cgit v1.3.1