diff options
Diffstat (limited to 'dhall/src/phase')
| -rw-r--r-- | dhall/src/phase/binary.rs | 748 | ||||
| -rw-r--r-- | dhall/src/phase/mod.rs | 254 | ||||
| -rw-r--r-- | dhall/src/phase/normalize.rs | 794 | ||||
| -rw-r--r-- | dhall/src/phase/parse.rs | 37 | ||||
| -rw-r--r-- | dhall/src/phase/resolve.rs | 180 | ||||
| -rw-r--r-- | dhall/src/phase/typecheck.rs | 815 |
6 files changed, 0 insertions, 2828 deletions
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs deleted file mode 100644 index b1e7638..0000000 --- a/dhall/src/phase/binary.rs +++ /dev/null @@ -1,748 +0,0 @@ -use itertools::Itertools; -use serde_cbor::value::value as cbor; -use std::iter::FromIterator; -use std::vec; - -use crate::syntax::map::DupTreeMap; -use crate::syntax::{ - Expr, ExprF, FilePath, FilePrefix, Hash, Import, ImportLocation, - ImportMode, Integer, InterpolatedText, Label, Natural, RawExpr, Scheme, - Span, URL, V, -}; - -use crate::error::{DecodeError, EncodeError}; -use crate::phase::DecodedExpr; - -pub(crate) fn decode(data: &[u8]) -> Result<DecodedExpr, DecodeError> { - match serde_cbor::de::from_slice(data) { - Ok(v) => cbor_value_to_dhall(&v), - Err(e) => Err(DecodeError::CBORError(e)), - } -} - -pub(crate) fn encode<E>(expr: &Expr<E>) -> Result<Vec<u8>, EncodeError> { - serde_cbor::ser::to_vec(&Serialize::Expr(expr)) - .map_err(|e| EncodeError::CBORError(e)) -} - -// Should probably rename this -pub fn rc<E>(x: RawExpr<E>) -> Expr<E> { - Expr::new(x, Span::Decoded) -} - -fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { - use cbor::Value::*; - use crate::syntax::{BinOp, Builtin, Const}; - use ExprF::*; - Ok(rc(match data { - String(s) => match Builtin::parse(s) { - Some(b) => ExprF::Builtin(b), - None => match s.as_str() { - "True" => BoolLit(true), - "False" => BoolLit(false), - "Type" => Const(Const::Type), - "Kind" => Const(Const::Kind), - "Sort" => Const(Const::Sort), - _ => Err(DecodeError::WrongFormatError("builtin".to_owned()))?, - }, - }, - U64(n) => Var(V(Label::from("_"), *n as usize)), - F64(x) => DoubleLit((*x).into()), - Bool(b) => BoolLit(*b), - Array(vec) => match vec.as_slice() { - [String(l), U64(n)] => { - if l.as_str() == "_" { - Err(DecodeError::WrongFormatError( - "`_` variable was encoded incorrectly".to_owned(), - ))? - } - let l = Label::from(l.as_str()); - Var(V(l, *n as usize)) - } - [U64(0), f, args @ ..] => { - if args.is_empty() { - Err(DecodeError::WrongFormatError( - "Function application must have at least one argument" - .to_owned(), - ))? - } - let mut f = cbor_value_to_dhall(&f)?; - for a in args { - let a = cbor_value_to_dhall(&a)?; - f = rc(App(f, a)) - } - return Ok(f); - } - [U64(1), x, y] => { - let x = cbor_value_to_dhall(&x)?; - let y = cbor_value_to_dhall(&y)?; - Lam(Label::from("_"), x, y) - } - [U64(1), String(l), x, y] => { - if l.as_str() == "_" { - Err(DecodeError::WrongFormatError( - "`_` variable was encoded incorrectly".to_owned(), - ))? - } - let x = cbor_value_to_dhall(&x)?; - let y = cbor_value_to_dhall(&y)?; - let l = Label::from(l.as_str()); - Lam(l, x, y) - } - [U64(2), x, y] => { - let x = cbor_value_to_dhall(&x)?; - let y = cbor_value_to_dhall(&y)?; - Pi(Label::from("_"), x, y) - } - [U64(2), String(l), x, y] => { - if l.as_str() == "_" { - Err(DecodeError::WrongFormatError( - "`_` variable was encoded incorrectly".to_owned(), - ))? - } - let x = cbor_value_to_dhall(&x)?; - let y = cbor_value_to_dhall(&y)?; - let l = Label::from(l.as_str()); - Pi(l, x, y) - } - [U64(3), U64(n), x, y] => { - let x = cbor_value_to_dhall(&x)?; - let y = cbor_value_to_dhall(&y)?; - use BinOp::*; - let op = match n { - 0 => BoolOr, - 1 => BoolAnd, - 2 => BoolEQ, - 3 => BoolNE, - 4 => NaturalPlus, - 5 => NaturalTimes, - 6 => TextAppend, - 7 => ListAppend, - 8 => RecursiveRecordMerge, - 9 => RightBiasedRecordMerge, - 10 => RecursiveRecordTypeMerge, - 11 => ImportAlt, - 12 => Equivalence, - _ => { - Err(DecodeError::WrongFormatError("binop".to_owned()))? - } - }; - BinOp(op, x, y) - } - [U64(4), t] => { - let t = cbor_value_to_dhall(&t)?; - EmptyListLit(rc(App(rc(ExprF::Builtin(Builtin::List)), t))) - } - [U64(4), Null, rest @ ..] => { - let rest = rest - .iter() - .map(cbor_value_to_dhall) - .collect::<Result<Vec<_>, _>>()?; - NEListLit(rest) - } - [U64(5), Null, x] => { - let x = cbor_value_to_dhall(&x)?; - SomeLit(x) - } - // Old-style optional literals - [U64(5), t] => { - let t = cbor_value_to_dhall(&t)?; - App(rc(ExprF::Builtin(Builtin::OptionalNone)), t) - } - [U64(5), t, x] => { - let x = cbor_value_to_dhall(&x)?; - let t = cbor_value_to_dhall(&t)?; - Annot( - rc(SomeLit(x)), - rc(App(rc(ExprF::Builtin(Builtin::Optional)), t)), - ) - } - [U64(6), x, y] => { - let x = cbor_value_to_dhall(&x)?; - let y = cbor_value_to_dhall(&y)?; - Merge(x, y, None) - } - [U64(6), x, y, z] => { - let x = cbor_value_to_dhall(&x)?; - let y = cbor_value_to_dhall(&y)?; - let z = cbor_value_to_dhall(&z)?; - Merge(x, y, Some(z)) - } - [U64(7), Object(map)] => { - let map = cbor_map_to_dhall_map(map)?; - RecordType(map) - } - [U64(8), Object(map)] => { - let map = cbor_map_to_dhall_map(map)?; - RecordLit(map) - } - [U64(9), x, String(l)] => { - let x = cbor_value_to_dhall(&x)?; - let l = Label::from(l.as_str()); - Field(x, l) - } - [U64(10), x, Array(arr)] => { - let x = cbor_value_to_dhall(&x)?; - if let [y] = arr.as_slice() { - let y = cbor_value_to_dhall(&y)?; - ProjectionByExpr(x, y) - } else { - Err(DecodeError::WrongFormatError( - "projection-by-expr".to_owned(), - ))? - } - } - [U64(10), x, rest @ ..] => { - let x = cbor_value_to_dhall(&x)?; - let labels = rest - .iter() - .map(|s| match s { - String(s) => Ok(Label::from(s.as_str())), - _ => Err(DecodeError::WrongFormatError( - "projection".to_owned(), - )), - }) - .collect::<Result<_, _>>()?; - Projection(x, labels) - } - [U64(11), Object(map)] => { - let map = cbor_map_to_dhall_opt_map(map)?; - UnionType(map) - } - [U64(12), ..] => Err(DecodeError::WrongFormatError( - "Union literals are not supported anymore".to_owned(), - ))?, - [U64(14), x, y, z] => { - let x = cbor_value_to_dhall(&x)?; - let y = cbor_value_to_dhall(&y)?; - let z = cbor_value_to_dhall(&z)?; - BoolIf(x, y, z) - } - [U64(15), U64(x)] => NaturalLit(*x as Natural), - [U64(16), U64(x)] => IntegerLit(*x as Integer), - [U64(16), I64(x)] => IntegerLit(*x as Integer), - [U64(18), String(first), rest @ ..] => { - TextLit(InterpolatedText::from(( - first.clone(), - rest.iter() - .tuples() - .map(|(x, y)| { - let x = cbor_value_to_dhall(&x)?; - let y = match y { - String(s) => s.clone(), - _ => Err(DecodeError::WrongFormatError( - "text".to_owned(), - ))?, - }; - Ok((x, y)) - }) - .collect::<Result<_, _>>()?, - ))) - } - [U64(19), t] => { - let t = cbor_value_to_dhall(&t)?; - Assert(t) - } - [U64(24), hash, U64(mode), U64(scheme), rest @ ..] => { - let mode = match mode { - 0 => ImportMode::Code, - 1 => ImportMode::RawText, - 2 => ImportMode::Location, - _ => Err(DecodeError::WrongFormatError(format!( - "import/mode/unknown_mode: {:?}", - mode - )))?, - }; - let hash = match hash { - Null => None, - Bytes(bytes) => match bytes.as_slice() { - [18, 32, rest @ ..] => { - Some(Hash::SHA256(rest.to_vec())) - } - _ => Err(DecodeError::WrongFormatError(format!( - "import/hash/unknown_multihash: {:?}", - bytes - )))?, - }, - _ => Err(DecodeError::WrongFormatError( - "import/hash/should_be_bytes".to_owned(), - ))?, - }; - let mut rest = rest.iter(); - let location = match scheme { - 0 | 1 => { - let scheme = match scheme { - 0 => Scheme::HTTP, - _ => Scheme::HTTPS, - }; - let headers = match rest.next() { - Some(Null) => None, - Some(x) => { - let x = cbor_value_to_dhall(&x)?; - Some(x) - } - _ => Err(DecodeError::WrongFormatError( - "import/remote/headers".to_owned(), - ))?, - }; - let authority = match rest.next() { - Some(String(s)) => s.to_owned(), - _ => Err(DecodeError::WrongFormatError( - "import/remote/authority".to_owned(), - ))?, - }; - let query = match rest.next_back() { - Some(Null) => None, - Some(String(s)) => Some(s.to_owned()), - _ => Err(DecodeError::WrongFormatError( - "import/remote/query".to_owned(), - ))?, - }; - let file_path = rest - .map(|s| match s.as_string() { - Some(s) => Ok(s.clone()), - None => Err(DecodeError::WrongFormatError( - "import/remote/path".to_owned(), - )), - }) - .collect::<Result<_, _>>()?; - let path = FilePath { file_path }; - ImportLocation::Remote(URL { - scheme, - authority, - path, - query, - headers, - }) - } - 2 | 3 | 4 | 5 => { - let prefix = match scheme { - 2 => FilePrefix::Absolute, - 3 => FilePrefix::Here, - 4 => FilePrefix::Parent, - 5 => FilePrefix::Home, - _ => Err(DecodeError::WrongFormatError( - "import/local/prefix".to_owned(), - ))?, - }; - let file_path = rest - .map(|s| match s.as_string() { - Some(s) => Ok(s.clone()), - None => Err(DecodeError::WrongFormatError( - "import/local/path".to_owned(), - )), - }) - .collect::<Result<_, _>>()?; - let path = FilePath { file_path }; - ImportLocation::Local(prefix, path) - } - 6 => { - let env = match rest.next() { - Some(String(s)) => s.to_owned(), - _ => Err(DecodeError::WrongFormatError( - "import/env".to_owned(), - ))?, - }; - ImportLocation::Env(env) - } - 7 => ImportLocation::Missing, - _ => Err(DecodeError::WrongFormatError( - "import/type".to_owned(), - ))?, - }; - Import(crate::syntax::Import { - mode, - hash, - location, - }) - } - [U64(25), bindings @ ..] => { - let mut tuples = bindings.iter().tuples(); - let bindings = (&mut tuples) - .map(|(x, t, v)| { - let x = x.as_string().ok_or_else(|| { - DecodeError::WrongFormatError( - "let/label".to_owned(), - ) - })?; - let x = Label::from(x.as_str()); - let t = match t { - Null => None, - t => Some(cbor_value_to_dhall(&t)?), - }; - let v = cbor_value_to_dhall(&v)?; - Ok((x, t, v)) - }) - .collect::<Result<Vec<_>, _>>()?; - let expr = tuples.into_buffer().next().ok_or_else(|| { - DecodeError::WrongFormatError("let/expr".to_owned()) - })?; - let expr = cbor_value_to_dhall(expr)?; - return Ok(bindings - .into_iter() - .rev() - .fold(expr, |acc, (x, t, v)| rc(Let(x, t, v, acc)))); - } - [U64(26), x, y] => { - let x = cbor_value_to_dhall(&x)?; - let y = cbor_value_to_dhall(&y)?; - Annot(x, y) - } - [U64(27), x] => { - let x = cbor_value_to_dhall(&x)?; - ToMap(x, None) - } - [U64(27), x, y] => { - let x = cbor_value_to_dhall(&x)?; - let y = cbor_value_to_dhall(&y)?; - ToMap(x, Some(y)) - } - [U64(28), x] => { - let x = cbor_value_to_dhall(&x)?; - EmptyListLit(x) - } - _ => Err(DecodeError::WrongFormatError(format!("{:?}", data)))?, - }, - _ => Err(DecodeError::WrongFormatError(format!("{:?}", data)))?, - })) -} - -fn cbor_map_to_dhall_map<'a, T>( - map: impl IntoIterator<Item = (&'a cbor::ObjectKey, &'a cbor::Value)>, -) -> Result<T, DecodeError> -where - T: FromIterator<(Label, DecodedExpr)>, -{ - map.into_iter() - .map(|(k, v)| -> Result<(_, _), _> { - let k = k.as_string().ok_or_else(|| { - DecodeError::WrongFormatError("map/key".to_owned()) - })?; - let v = cbor_value_to_dhall(v)?; - Ok((Label::from(k.as_ref()), v)) - }) - .collect::<Result<_, _>>() -} - -fn cbor_map_to_dhall_opt_map<'a, T>( - map: impl IntoIterator<Item = (&'a cbor::ObjectKey, &'a cbor::Value)>, -) -> Result<T, DecodeError> -where - T: FromIterator<(Label, Option<DecodedExpr>)>, -{ - map.into_iter() - .map(|(k, v)| -> Result<(_, _), _> { - let k = k.as_string().ok_or_else(|| { - DecodeError::WrongFormatError("map/key".to_owned()) - })?; - let v = match v { - cbor::Value::Null => None, - _ => Some(cbor_value_to_dhall(v)?), - }; - Ok((Label::from(k.as_ref()), v)) - }) - .collect::<Result<_, _>>() -} - -enum Serialize<'a, E> { - Expr(&'a Expr<E>), - CBOR(cbor::Value), - RecordMap(&'a DupTreeMap<Label, Expr<E>>), - UnionMap(&'a DupTreeMap<Label, Option<Expr<E>>>), -} - -macro_rules! count { - (@replace_with $_t:tt $sub:expr) => { $sub }; - ($($tts:tt)*) => {0usize $(+ count!(@replace_with $tts 1usize))*}; -} - -macro_rules! ser_seq { - ($ser:expr; $($elt:expr),* $(,)?) => {{ - use serde::ser::SerializeSeq; - let count = count!($($elt)*); - let mut ser_seq = $ser.serialize_seq(Some(count))?; - $( - ser_seq.serialize_element(&$elt)?; - )* - ser_seq.end() - }}; -} - -fn serialize_subexpr<S, E>(ser: S, e: &Expr<E>) -> Result<S::Ok, S::Error> -where - S: serde::ser::Serializer, -{ - use cbor::Value::{String, I64, U64}; - use crate::syntax::Builtin; - use crate::syntax::ExprF::*; - use std::iter::once; - - use self::Serialize::{RecordMap, UnionMap}; - fn expr<E>(x: &Expr<E>) -> self::Serialize<'_, E> { - self::Serialize::Expr(x) - } - let cbor = - |v: cbor::Value| -> self::Serialize<'_, E> { self::Serialize::CBOR(v) }; - let tag = |x: u64| cbor(U64(x)); - let null = || cbor(cbor::Value::Null); - let label = |l: &Label| cbor(cbor::Value::String(l.into())); - - match e.as_ref() { - Const(c) => ser.serialize_str(&c.to_string()), - Builtin(b) => ser.serialize_str(&b.to_string()), - BoolLit(b) => ser.serialize_bool(*b), - NaturalLit(n) => ser_seq!(ser; tag(15), U64(*n as u64)), - IntegerLit(n) => ser_seq!(ser; tag(16), I64(*n as i64)), - DoubleLit(n) => { - let n: f64 = (*n).into(); - ser.serialize_f64(n) - } - BoolIf(x, y, z) => ser_seq!(ser; tag(14), expr(x), expr(y), expr(z)), - Var(V(l, n)) if l == &"_".into() => ser.serialize_u64(*n as u64), - Var(V(l, n)) => ser_seq!(ser; label(l), U64(*n as u64)), - Lam(l, x, y) if l == &"_".into() => { - ser_seq!(ser; tag(1), expr(x), expr(y)) - } - Lam(l, x, y) => ser_seq!(ser; tag(1), label(l), expr(x), expr(y)), - Pi(l, x, y) if l == &"_".into() => { - ser_seq!(ser; tag(2), expr(x), expr(y)) - } - Pi(l, x, y) => ser_seq!(ser; tag(2), label(l), expr(x), expr(y)), - Let(_, _, _, _) => { - let (bound_e, bindings) = collect_nested_lets(e); - let count = 1 + 3 * bindings.len() + 1; - - use serde::ser::SerializeSeq; - let mut ser_seq = ser.serialize_seq(Some(count))?; - ser_seq.serialize_element(&tag(25))?; - for (l, t, v) in bindings { - ser_seq.serialize_element(&label(l))?; - match t { - Some(t) => ser_seq.serialize_element(&expr(t))?, - None => ser_seq.serialize_element(&null())?, - } - ser_seq.serialize_element(&expr(v))?; - } - ser_seq.serialize_element(&expr(bound_e))?; - ser_seq.end() - } - App(_, _) => { - let (f, args) = collect_nested_applications(e); - ser.collect_seq( - once(tag(0)) - .chain(once(expr(f))) - .chain(args.into_iter().rev().map(expr)), - ) - } - Annot(x, y) => ser_seq!(ser; tag(26), expr(x), expr(y)), - Assert(x) => ser_seq!(ser; tag(19), expr(x)), - SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)), - EmptyListLit(x) => match x.as_ref() { - App(f, a) => match f.as_ref() { - ExprF::Builtin(Builtin::List) => ser_seq!(ser; tag(4), expr(a)), - _ => ser_seq!(ser; tag(28), expr(x)), - }, - _ => ser_seq!(ser; tag(28), expr(x)), - }, - NEListLit(xs) => ser.collect_seq( - once(tag(4)).chain(once(null())).chain(xs.iter().map(expr)), - ), - TextLit(xs) => { - use crate::syntax::InterpolatedTextContents::{Expr, Text}; - ser.collect_seq(once(tag(18)).chain(xs.iter().map(|x| match x { - Expr(x) => expr(x), - Text(x) => cbor(String(x.clone())), - }))) - } - RecordType(map) => ser_seq!(ser; tag(7), RecordMap(map)), - RecordLit(map) => ser_seq!(ser; tag(8), RecordMap(map)), - UnionType(map) => ser_seq!(ser; tag(11), UnionMap(map)), - Field(x, l) => ser_seq!(ser; tag(9), expr(x), label(l)), - BinOp(op, x, y) => { - use crate::syntax::BinOp::*; - let op = match op { - BoolOr => 0, - BoolAnd => 1, - BoolEQ => 2, - BoolNE => 3, - NaturalPlus => 4, - NaturalTimes => 5, - TextAppend => 6, - ListAppend => 7, - RecursiveRecordMerge => 8, - RightBiasedRecordMerge => 9, - RecursiveRecordTypeMerge => 10, - ImportAlt => 11, - Equivalence => 12, - }; - ser_seq!(ser; tag(3), U64(op), expr(x), expr(y)) - } - Merge(x, y, None) => ser_seq!(ser; tag(6), expr(x), expr(y)), - Merge(x, y, Some(z)) => { - ser_seq!(ser; tag(6), expr(x), expr(y), expr(z)) - } - ToMap(x, None) => ser_seq!(ser; tag(27), expr(x)), - ToMap(x, Some(y)) => ser_seq!(ser; tag(27), expr(x), expr(y)), - Projection(x, ls) => ser.collect_seq( - once(tag(10)) - .chain(once(expr(x))) - .chain(ls.iter().map(label)), - ), - ProjectionByExpr(x, y) => { - ser_seq!(ser; tag(10), expr(x), vec![expr(y)]) - } - Import(import) => serialize_import(ser, import), - Embed(_) => unimplemented!( - "An expression with resolved imports cannot be binary-encoded" - ), - } -} - -fn serialize_import<S, E>( - ser: S, - import: &Import<Expr<E>>, -) -> Result<S::Ok, S::Error> -where - S: serde::ser::Serializer, -{ - use cbor::Value::{Bytes, Null, U64}; - use serde::ser::SerializeSeq; - - let count = 4 + match &import.location { - ImportLocation::Remote(url) => 3 + url.path.file_path.len(), - ImportLocation::Local(_, path) => path.file_path.len(), - ImportLocation::Env(_) => 1, - ImportLocation::Missing => 0, - }; - let mut ser_seq = ser.serialize_seq(Some(count))?; - - ser_seq.serialize_element(&U64(24))?; - - let hash = match &import.hash { - None => Null, - Some(Hash::SHA256(h)) => { - let mut bytes = vec![18, 32]; - bytes.extend_from_slice(h); - Bytes(bytes) - } - }; - ser_seq.serialize_element(&hash)?; - - let mode = match import.mode { - ImportMode::Code => 0, - ImportMode::RawText => 1, - ImportMode::Location => 2, - }; - ser_seq.serialize_element(&U64(mode))?; - - let scheme = match &import.location { - ImportLocation::Remote(url) => match url.scheme { - Scheme::HTTP => 0, - Scheme::HTTPS => 1, - }, - ImportLocation::Local(prefix, _) => match prefix { - FilePrefix::Absolute => 2, - FilePrefix::Here => 3, - FilePrefix::Parent => 4, - FilePrefix::Home => 5, - }, - ImportLocation::Env(_) => 6, - ImportLocation::Missing => 7, - }; - ser_seq.serialize_element(&U64(scheme))?; - - match &import.location { - ImportLocation::Remote(url) => { - match &url.headers { - None => ser_seq.serialize_element(&Null)?, - Some(e) => { - ser_seq.serialize_element(&self::Serialize::Expr(e))? - } - }; - ser_seq.serialize_element(&url.authority)?; - for p in url.path.file_path.iter() { - ser_seq.serialize_element(&p)?; - } - match &url.query { - None => ser_seq.serialize_element(&Null)?, - Some(x) => ser_seq.serialize_element(x)?, - }; - } - ImportLocation::Local(_, path) => { - for p in path.file_path.iter() { - ser_seq.serialize_element(&p)?; - } - } - ImportLocation::Env(env) => { - ser_seq.serialize_element(env)?; - } - ImportLocation::Missing => {} - } - - ser_seq.end() -} - -impl<'a, E> serde::ser::Serialize for Serialize<'a, E> { - fn serialize<S>(&self, ser: S) -> Result<S::Ok, S::Error> - where - S: serde::ser::Serializer, - { - match self { - Serialize::Expr(e) => serialize_subexpr(ser, e), - Serialize::CBOR(v) => v.serialize(ser), - Serialize::RecordMap(map) => { - ser.collect_map(map.iter().map(|(k, v)| { - (cbor::Value::String(k.into()), Serialize::Expr(v)) - })) - } - Serialize::UnionMap(map) => { - ser.collect_map(map.iter().map(|(k, v)| { - let v = match v { - Some(x) => Serialize::Expr(x), - None => Serialize::CBOR(cbor::Value::Null), - }; - (cbor::Value::String(k.into()), v) - })) - } - } - } -} - -fn collect_nested_applications<'a, E>( - e: &'a Expr<E>, -) -> (&'a Expr<E>, Vec<&'a Expr<E>>) { - fn go<'a, E>(e: &'a Expr<E>, vec: &mut Vec<&'a Expr<E>>) -> &'a Expr<E> { - match e.as_ref() { - ExprF::App(f, a) => { - vec.push(a); - go(f, vec) - } - _ => e, - } - } - let mut vec = vec![]; - let e = go(e, &mut vec); - (e, vec) -} - -type LetBinding<'a, E> = (&'a Label, &'a Option<Expr<E>>, &'a Expr<E>); - -fn collect_nested_lets<'a, E>( - e: &'a Expr<E>, -) -> (&'a Expr<E>, Vec<LetBinding<'a, E>>) { - fn go<'a, E>( - e: &'a Expr<E>, - vec: &mut Vec<LetBinding<'a, E>>, - ) -> &'a Expr<E> { - match e.as_ref() { - ExprF::Let(l, t, v, e) => { - vec.push((l, t, v)); - go(e, vec) - } - _ => e, - } - } - let mut vec = vec![]; - let e = go(e, &mut vec); - (e, vec) -} diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs deleted file mode 100644 index 918c4d0..0000000 --- a/dhall/src/phase/mod.rs +++ /dev/null @@ -1,254 +0,0 @@ -use std::fmt::Display; -use std::path::Path; - -use crate::syntax::{Builtin, Const, Expr}; - -use crate::core::value::{ToExprOptions, Value}; -use crate::core::valuef::ValueF; -use crate::core::var::{AlphaVar, Shift, Subst}; -use crate::error::{EncodeError, Error, ImportError, TypeError}; - -use resolve::ImportRoot; - -pub(crate) mod binary; -pub(crate) mod normalize; -pub(crate) mod parse; -pub(crate) mod resolve; -pub(crate) mod typecheck; - -pub type ParsedExpr = Expr<Normalized>; -pub type DecodedExpr = Expr<Normalized>; -pub type ResolvedExpr = Expr<Normalized>; -pub type NormalizedExpr = Expr<Normalized>; - -#[derive(Debug, Clone)] -pub struct Parsed(ParsedExpr, ImportRoot); - -/// An expression where all imports have been resolved -/// -/// Invariant: there must be no `Import` nodes or `ImportAlt` operations left. -#[derive(Debug, Clone)] -pub struct Resolved(ResolvedExpr); - -/// A typed expression -#[derive(Debug, Clone)] -pub struct Typed(Value); - -/// A normalized expression. -/// -/// Invariant: the contained Typed expression must be in normal form, -#[derive(Debug, Clone)] -pub struct Normalized(Typed); - -impl Parsed { - pub fn parse_file(f: &Path) -> Result<Parsed, Error> { - parse::parse_file(f) - } - pub fn parse_str(s: &str) -> Result<Parsed, Error> { - parse::parse_str(s) - } - pub fn parse_binary_file(f: &Path) -> Result<Parsed, Error> { - parse::parse_binary_file(f) - } - pub fn parse_binary(data: &[u8]) -> Result<Parsed, Error> { - parse::parse_binary(data) - } - - pub fn resolve(self) -> Result<Resolved, ImportError> { - resolve::resolve(self) - } - pub fn skip_resolve(self) -> Result<Resolved, ImportError> { - resolve::skip_resolve_expr(self) - } - - pub fn encode(&self) -> Result<Vec<u8>, EncodeError> { - crate::phase::binary::encode(&self.0) - } -} - -impl Resolved { - pub fn typecheck(self) -> Result<Typed, TypeError> { - Ok(typecheck::typecheck(self.0)?.into_typed()) - } - pub fn typecheck_with(self, ty: &Typed) -> Result<Typed, TypeError> { - Ok(typecheck::typecheck_with(self.0, ty.normalize_to_expr())? - .into_typed()) - } -} - -impl Typed { - /// Reduce an expression to its normal form, performing beta reduction - /// - /// `normalize` does not type-check the expression. You may want to type-check - /// expressions before normalizing them since normalization can convert an - /// ill-typed expression into a well-typed expression. - /// - /// However, `normalize` will not fail if the expression is ill-typed and will - /// leave ill-typed sub-expressions unevaluated. - pub fn normalize(mut self) -> Normalized { - self.normalize_mut(); - Normalized(self) - } - - pub(crate) fn from_const(c: Const) -> Self { - Typed(Value::from_const(c)) - } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Typed) -> Self { - Typed(Value::from_valuef_and_type(v, t.into_value())) - } - pub(crate) fn from_value(th: Value) -> Self { - Typed(th) - } - pub(crate) fn const_type() -> Self { - Typed::from_const(Const::Type) - } - - pub(crate) fn to_expr(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: false, - }) - } - pub fn normalize_to_expr(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: true, - }) - } - pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: true, - normalize: true, - }) - } - pub(crate) fn to_value(&self) -> Value { - self.0.clone() - } - pub(crate) fn into_value(self) -> Value { - self.0 - } - - pub(crate) fn normalize_mut(&mut self) { - self.0.normalize_mut() - } - - pub(crate) fn get_type(&self) -> Result<Typed, TypeError> { - Ok(self.0.get_type()?.into_typed()) - } - - pub fn make_builtin_type(b: Builtin) -> Self { - Typed::from_value(Value::from_builtin(b)) - } - pub fn make_optional_type(t: Typed) -> Self { - Typed::from_value( - Value::from_builtin(Builtin::Optional).app(t.to_value()), - ) - } - pub fn make_list_type(t: Typed) -> Self { - Typed::from_value(Value::from_builtin(Builtin::List).app(t.to_value())) - } - pub fn make_record_type( - kts: impl Iterator<Item = (String, Typed)>, - ) -> Self { - Typed::from_valuef_and_type( - ValueF::RecordType( - kts.map(|(k, t)| (k.into(), t.into_value())).collect(), - ), - Typed::const_type(), - ) - } - pub fn make_union_type( - kts: impl Iterator<Item = (String, Option<Typed>)>, - ) -> Self { - Typed::from_valuef_and_type( - ValueF::UnionType( - kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) - .collect(), - ), - Typed::const_type(), - ) - } -} - -impl Normalized { - pub fn encode(&self) -> Result<Vec<u8>, EncodeError> { - crate::phase::binary::encode(&self.to_expr()) - } - - pub(crate) fn to_expr(&self) -> NormalizedExpr { - self.0.normalize_to_expr() - } - pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { - self.0.normalize_to_expr_alpha() - } - pub(crate) fn into_typed(self) -> Typed { - self.0 - } -} - -impl Shift for Typed { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Typed(self.0.shift(delta, var)?)) - } -} - -impl Shift for Normalized { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(Normalized(self.0.shift(delta, var)?)) - } -} - -impl Subst<Value> for Typed { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - Typed(self.0.subst_shift(var, val)) - } -} - -macro_rules! derive_traits_for_wrapper_struct { - ($ty:ident) => { - impl std::cmp::PartialEq for $ty { - fn eq(&self, other: &Self) -> bool { - self.0 == other.0 - } - } - - impl std::cmp::Eq for $ty {} - - impl std::fmt::Display for $ty { - fn fmt( - &self, - f: &mut std::fmt::Formatter, - ) -> Result<(), std::fmt::Error> { - self.0.fmt(f) - } - } - }; -} - -derive_traits_for_wrapper_struct!(Parsed); -derive_traits_for_wrapper_struct!(Resolved); -derive_traits_for_wrapper_struct!(Normalized); - -impl std::hash::Hash for Normalized { - fn hash<H>(&self, state: &mut H) - where - H: std::hash::Hasher, - { - if let Ok(vec) = self.encode() { - vec.hash(state) - } - } -} - -impl Eq for Typed {} -impl PartialEq for Typed { - fn eq(&self, other: &Self) -> bool { - self.0 == other.0 - } -} - -impl Display for Typed { - fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { - self.to_expr().fmt(f) - } -} diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs deleted file mode 100644 index 3ed53f4..0000000 --- a/dhall/src/phase/normalize.rs +++ /dev/null @@ -1,794 +0,0 @@ -use std::collections::HashMap; - -use crate::syntax::Const::Type; -use crate::syntax::{ - BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label, - NaiveDouble, -}; - -use crate::core::value::Value; -use crate::core::valuef::ValueF; -use crate::core::var::{AlphaLabel, Shift, Subst}; -use crate::phase::Normalized; - -// Ad-hoc macro to help construct closures -macro_rules! make_closure { - (#$var:ident) => { $var.clone() }; - (var($var:ident, $n:expr, $($ty:tt)*)) => {{ - let var = crate::core::var::AlphaVar::from_var_and_alpha( - Label::from(stringify!($var)).into(), - $n - ); - ValueF::Var(var) - .into_value_with_type(make_closure!($($ty)*)) - }}; - // Warning: assumes that $ty, as a dhall value, has type `Type` - (λ($var:ident : $($ty:tt)*) -> $($body:tt)*) => {{ - let var: AlphaLabel = Label::from(stringify!($var)).into(); - let ty = make_closure!($($ty)*); - let body = make_closure!($($body)*); - let body_ty = body.get_type_not_sort(); - let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty) - .into_value_with_type(Value::from_const(Type)); - ValueF::Lam(var, ty, body).into_value_with_type(lam_ty) - }}; - (Natural) => { - Value::from_builtin(Builtin::Natural) - }; - (List $($rest:tt)*) => { - Value::from_builtin(Builtin::List) - .app(make_closure!($($rest)*)) - }; - (Some($($rest:tt)*)) => {{ - let v = make_closure!($($rest)*); - let v_type = v.get_type_not_sort(); - let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type); - ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type) - }}; - (1 + $($rest:tt)*) => { - ValueF::PartialExpr(ExprF::BinOp( - crate::syntax::BinOp::NaturalPlus, - make_closure!($($rest)*), - Value::from_valuef_and_type( - ValueF::NaturalLit(1), - make_closure!(Natural) - ), - )).into_value_with_type( - make_closure!(Natural) - ) - }; - ([ $($head:tt)* ] # $($tail:tt)*) => {{ - let head = make_closure!($($head)*); - let tail = make_closure!($($tail)*); - let list_type = tail.get_type_not_sort(); - ValueF::PartialExpr(ExprF::BinOp( - crate::syntax::BinOp::ListAppend, - ValueF::NEListLit(vec![head]) - .into_value_with_type(list_type.clone()), - tail, - )).into_value_with_type(list_type) - }}; -} - -#[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin( - b: Builtin, - args: Vec<Value>, - ty: &Value, -) -> ValueF { - use crate::syntax::Builtin::*; - use ValueF::*; - - // Small helper enum - enum Ret<'a> { - ValueF(ValueF), - Value(Value), - // For applications that can return a function, it's important to keep the remaining - // arguments to apply them to the resulting function. - ValueWithRemainingArgs(&'a [Value], Value), - DoneAsIs, - } - - let ret = match (b, args.as_slice()) { - (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())), - (NaturalIsZero, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)), - _ => Ret::DoneAsIs, - }, - (NaturalEven, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)), - _ => Ret::DoneAsIs, - }, - (NaturalOdd, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)), - _ => Ret::DoneAsIs, - }, - (NaturalToInteger, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)), - _ => Ret::DoneAsIs, - }, - (NaturalShow, [n]) => match &*n.as_whnf() { - NaturalLit(n) => { - Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text( - n.to_string(), - )])) - } - _ => Ret::DoneAsIs, - }, - (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) { - (NaturalLit(a), NaturalLit(b)) => { - Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 })) - } - (NaturalLit(0), _) => Ret::Value(b.clone()), - (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)), - _ if a == b => Ret::ValueF(NaturalLit(0)), - _ => Ret::DoneAsIs, - }, - (IntegerShow, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - let s = if *n < 0 { - n.to_string() - } else { - format!("+{}", n) - }; - Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)])) - } - _ => Ret::DoneAsIs, - }, - (IntegerToDouble, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64))) - } - _ => Ret::DoneAsIs, - }, - (DoubleShow, [n]) => match &*n.as_whnf() { - DoubleLit(n) => { - Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text( - n.to_string(), - )])) - } - _ => Ret::DoneAsIs, - }, - (TextShow, [v]) => match &*v.as_whnf() { - TextLit(elts) => { - match elts.as_slice() { - // Empty string literal. - [] => { - // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText<Normalized> = - std::iter::empty().collect(); - let s = txt.to_string(); - Ret::ValueF(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])) - } - // If there are no interpolations (invariants ensure that when there are no - // interpolations, there is a single Text item) in the literal. - [InterpolatedTextContents::Text(s)] => { - // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText<Normalized> = - std::iter::once(InterpolatedTextContents::Text( - s.clone(), - )) - .collect(); - let s = txt.to_string(); - Ret::ValueF(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])) - } - _ => Ret::DoneAsIs, - } - } - _ => Ret::DoneAsIs, - }, - (ListLength, [_, l]) => match &*l.as_whnf() { - EmptyListLit(_) => Ret::ValueF(NaturalLit(0)), - NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())), - _ => Ret::DoneAsIs, - }, - (ListHead, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())), - NEListLit(xs) => { - Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone())) - } - _ => Ret::DoneAsIs, - }, - (ListLast, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())), - NEListLit(xs) => Ret::ValueF(NEOptionalLit( - xs.iter().rev().next().unwrap().clone(), - )), - _ => Ret::DoneAsIs, - }, - (ListReverse, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())), - NEListLit(xs) => { - Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect())) - } - _ => Ret::DoneAsIs, - }, - (ListIndexed, [_, l]) => { - let l_whnf = l.as_whnf(); - match &*l_whnf { - EmptyListLit(_) | NEListLit(_) => { - // Extract the type of the list elements - let t = match &*l_whnf { - EmptyListLit(t) => t.clone(), - NEListLit(xs) => xs[0].get_type_not_sort(), - _ => unreachable!(), - }; - - // Construct the returned record type: { index: Natural, value: t } - let mut kts = HashMap::new(); - kts.insert("index".into(), Value::from_builtin(Natural)); - kts.insert("value".into(), t.clone()); - let t = Value::from_valuef_and_type( - RecordType(kts), - Value::from_const(Type), - ); - - // Construct the new list, with added indices - let list = match &*l_whnf { - EmptyListLit(_) => EmptyListLit(t), - NEListLit(xs) => NEListLit( - xs.iter() - .enumerate() - .map(|(i, e)| { - let mut kvs = HashMap::new(); - kvs.insert( - "index".into(), - Value::from_valuef_and_type( - NaturalLit(i), - Value::from_builtin( - Builtin::Natural, - ), - ), - ); - kvs.insert("value".into(), e.clone()); - Value::from_valuef_and_type( - RecordLit(kvs), - t.clone(), - ) - }) - .collect(), - ), - _ => unreachable!(), - }; - Ret::ValueF(list) - } - _ => Ret::DoneAsIs, - } - } - (ListBuild, [t, f]) => match &*f.as_whnf() { - // fold/build fusion - ValueF::AppliedBuiltin(ListFold, args) => { - if args.len() >= 2 { - Ret::Value(args[1].clone()) - } else { - // Do we really need to handle this case ? - unimplemented!() - } - } - _ => { - let list_t = Value::from_builtin(List).app(t.clone()); - Ret::Value( - f.app(list_t.clone()) - .app({ - // Move `t` under new variables - let t1 = t.under_binder(Label::from("x")); - let t2 = t1.under_binder(Label::from("xs")); - make_closure!( - λ(x : #t) -> - λ(xs : List #t1) -> - [ var(x, 1, #t2) ] # var(xs, 0, List #t2) - ) - }) - .app( - EmptyListLit(t.clone()) - .into_value_with_type(list_t), - ), - ) - } - }, - (ListFold, [_, l, _, cons, nil, r @ ..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()), - NEListLit(xs) => { - let mut v = nil.clone(); - for x in xs.iter().cloned().rev() { - v = cons.app(x).app(v); - } - Ret::ValueWithRemainingArgs(r, v) - } - _ => Ret::DoneAsIs, - }, - (OptionalBuild, [t, f]) => match &*f.as_whnf() { - // fold/build fusion - ValueF::AppliedBuiltin(OptionalFold, args) => { - if args.len() >= 2 { - Ret::Value(args[1].clone()) - } else { - // Do we really need to handle this case ? - unimplemented!() - } - } - _ => { - let optional_t = Value::from_builtin(Optional).app(t.clone()); - Ret::Value( - f.app(optional_t.clone()) - .app({ - let t1 = t.under_binder(Label::from("x")); - make_closure!(λ(x: #t) -> Some(var(x, 0, #t1))) - }) - .app( - EmptyOptionalLit(t.clone()) - .into_value_with_type(optional_t), - ), - ) - } - }, - (OptionalFold, [_, v, _, just, nothing, r @ ..]) => match &*v.as_whnf() - { - EmptyOptionalLit(_) => { - Ret::ValueWithRemainingArgs(r, nothing.clone()) - } - NEOptionalLit(x) => { - Ret::ValueWithRemainingArgs(r, just.app(x.clone())) - } - _ => Ret::DoneAsIs, - }, - (NaturalBuild, [f]) => match &*f.as_whnf() { - // fold/build fusion - ValueF::AppliedBuiltin(NaturalFold, args) => { - if !args.is_empty() { - Ret::Value(args[0].clone()) - } else { - // Do we really need to handle this case ? - unimplemented!() - } - } - _ => Ret::Value( - f.app(Value::from_builtin(Natural)) - .app(make_closure!( - λ(x : Natural) -> 1 + var(x, 0, Natural) - )) - .app( - NaturalLit(0) - .into_value_with_type(Value::from_builtin(Natural)), - ), - ), - }, - (NaturalFold, [n, t, succ, zero, r @ ..]) => match &*n.as_whnf() { - NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()), - NaturalLit(n) => { - let fold = Value::from_builtin(NaturalFold) - .app( - NaturalLit(n - 1) - .into_value_with_type(Value::from_builtin(Natural)), - ) - .app(t.clone()) - .app(succ.clone()) - .app(zero.clone()); - Ret::ValueWithRemainingArgs(r, succ.app(fold)) - } - _ => Ret::DoneAsIs, - }, - _ => Ret::DoneAsIs, - }; - match ret { - Ret::ValueF(v) => v, - Ret::Value(v) => v.to_whnf_check_type(ty), - Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => { - let n_consumed_args = args.len() - unconsumed_args.len(); - for x in args.into_iter().skip(n_consumed_args) { - v = v.app(x); - } - v.to_whnf_check_type(ty) - } - Ret::DoneAsIs => AppliedBuiltin(b, args), - } -} - -pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF { - let f_borrow = f.as_whnf(); - match &*f_borrow { - ValueF::Lam(x, _, e) => { - e.subst_shift(&x.into(), &a).to_whnf_check_type(ty) - } - ValueF::AppliedBuiltin(b, args) => { - use std::iter::once; - let args = args.iter().cloned().chain(once(a.clone())).collect(); - apply_builtin(*b, args, ty) - } - ValueF::UnionConstructor(l, kts) => { - ValueF::UnionLit(l.clone(), a, kts.clone()) - } - _ => { - drop(f_borrow); - ValueF::PartialExpr(ExprF::App(f, a)) - } - } -} - -pub(crate) fn squash_textlit( - elts: impl Iterator<Item = InterpolatedTextContents<Value>>, -) -> Vec<InterpolatedTextContents<Value>> { - use std::mem::replace; - use InterpolatedTextContents::{Expr, Text}; - - fn inner( - elts: impl Iterator<Item = InterpolatedTextContents<Value>>, - crnt_str: &mut String, - ret: &mut Vec<InterpolatedTextContents<Value>>, - ) { - for contents in elts { - match contents { - Text(s) => crnt_str.push_str(&s), - Expr(e) => { - let e_borrow = e.as_whnf(); - match &*e_borrow { - ValueF::TextLit(elts2) => { - inner(elts2.iter().cloned(), crnt_str, ret) - } - _ => { - drop(e_borrow); - if !crnt_str.is_empty() { - ret.push(Text(replace(crnt_str, String::new()))) - } - ret.push(Expr(e.clone())) - } - } - } - } - } - } - - let mut crnt_str = String::new(); - let mut ret = Vec::new(); - inner(elts, &mut crnt_str, &mut ret); - if !crnt_str.is_empty() { - ret.push(Text(replace(&mut crnt_str, String::new()))) - } - ret -} - -pub(crate) fn merge_maps<K, V, F, Err>( - map1: &HashMap<K, V>, - map2: &HashMap<K, V>, - mut f: F, -) -> Result<HashMap<K, V>, Err> -where - F: FnMut(&K, &V, &V) -> Result<V, Err>, - K: std::hash::Hash + Eq + Clone, - V: Clone, -{ - let mut kvs = HashMap::new(); - for (x, v2) in map2 { - let newv = if let Some(v1) = map1.get(x) { - f(x, v1, v2)? - } else { - v2.clone() - }; - kvs.insert(x.clone(), newv); - } - for (x, v1) in map1 { - // Insert only if key not already present - kvs.entry(x.clone()).or_insert_with(|| v1.clone()); - } - Ok(kvs) -} - -// Small helper enum to avoid repetition -enum Ret<'a> { - ValueF(ValueF), - Value(Value), - ValueRef(&'a Value), - Expr(ExprF<Value, Normalized>), -} - -fn apply_binop<'a>( - o: BinOp, - x: &'a Value, - y: &'a Value, - ty: &Value, -) -> Option<Ret<'a>> { - use BinOp::{ - BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, - NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, - RightBiasedRecordMerge, TextAppend, - }; - use ValueF::{ - BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, - TextLit, - }; - let x_borrow = x.as_whnf(); - let y_borrow = y.as_whnf(); - Some(match (o, &*x_borrow, &*y_borrow) { - (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y), - (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x), - (BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)), - (BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)), - (BoolAnd, _, _) if x == y => Ret::ValueRef(x), - (BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)), - (BoolOr, _, BoolLit(true)) => Ret::ValueF(BoolLit(true)), - (BoolOr, BoolLit(false), _) => Ret::ValueRef(y), - (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x), - (BoolOr, _, _) if x == y => Ret::ValueRef(x), - (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y), - (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x), - (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x == y)), - (BoolEQ, _, _) if x == y => Ret::ValueF(BoolLit(true)), - (BoolNE, BoolLit(false), _) => Ret::ValueRef(y), - (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x), - (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x != y)), - (BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)), - - (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y), - (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), - (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueF(NaturalLit(x + y)) - } - (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)), - (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)), - (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y), - (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x), - (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueF(NaturalLit(x * y)) - } - - (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y), - (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueF(NEListLit( - xs.iter().chain(ys.iter()).cloned().collect(), - )), - - (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y), - (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x), - (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueF(TextLit( - squash_textlit(x.iter().chain(y.iter()).cloned()), - )), - (TextAppend, TextLit(x), _) => { - use std::iter::once; - let y = InterpolatedTextContents::Expr(y.clone()); - Ret::ValueF(TextLit(squash_textlit( - x.iter().cloned().chain(once(y)), - ))) - } - (TextAppend, _, TextLit(y)) => { - use std::iter::once; - let x = InterpolatedTextContents::Expr(x.clone()); - Ret::ValueF(TextLit(squash_textlit( - once(x).chain(y.iter().cloned()), - ))) - } - - (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ValueRef(x) - } - (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ValueRef(y) - } - (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let mut kvs = kvs2.clone(); - for (x, v) in kvs1 { - // Insert only if key not already present - kvs.entry(x.clone()).or_insert_with(|| v.clone()); - } - Ret::ValueF(RecordLit(kvs)) - } - - (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ValueRef(x) - } - (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ValueRef(y) - } - (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let ty_borrow = ty.as_whnf(); - let kts = match &*ty_borrow { - RecordType(kts) => kts, - _ => unreachable!("Internal type error"), - }; - let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { - Ok(Value::from_valuef_and_type( - ValueF::PartialExpr(ExprF::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), - )), - kts.get(k).expect("Internal type error").clone(), - )) - })?; - Ret::ValueF(RecordLit(kvs)) - } - - (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => { - unreachable!("This case should have been handled in typecheck") - } - - _ => return None, - }) -} - -pub(crate) fn normalize_one_layer( - expr: ExprF<Value, Normalized>, - ty: &Value, -) -> ValueF { - use ValueF::{ - AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, - NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, - UnionConstructor, UnionLit, UnionType, - }; - - let ret = match expr { - ExprF::Import(_) => unreachable!( - "There should remain no imports in a resolved expression" - ), - // Those cases have already been completely handled in the typechecking phase (using - // `RetWhole`), so they won't appear here. - ExprF::Lam(_, _, _) - | ExprF::Pi(_, _, _) - | ExprF::Let(_, _, _, _) - | ExprF::Embed(_) - | ExprF::Const(_) - | ExprF::Builtin(_) - | ExprF::Var(_) - | ExprF::Annot(_, _) - | ExprF::RecordType(_) - | ExprF::UnionType(_) => { - unreachable!("This case should have been handled in typecheck") - } - ExprF::Assert(_) => Ret::Expr(expr), - ExprF::App(v, a) => Ret::Value(v.app(a)), - ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)), - ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)), - ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)), - ExprF::DoubleLit(n) => Ret::ValueF(DoubleLit(n)), - ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)), - ExprF::EmptyListLit(ref t) => { - // Check if the type is of the form `List x` - let t_borrow = t.as_whnf(); - match &*t_borrow { - AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::ValueF(EmptyListLit(args[0].clone())) - } - _ => { - drop(t_borrow); - Ret::Expr(expr) - } - } - } - ExprF::NEListLit(elts) => { - Ret::ValueF(NEListLit(elts.into_iter().collect())) - } - ExprF::RecordLit(kvs) => { - Ret::ValueF(RecordLit(kvs.into_iter().collect())) - } - ExprF::TextLit(elts) => { - use InterpolatedTextContents::Expr; - let elts: Vec<_> = squash_textlit(elts.into_iter()); - // Simplify bare interpolation - if let [Expr(th)] = elts.as_slice() { - Ret::Value(th.clone()) - } else { - Ret::ValueF(TextLit(elts)) - } - } - ExprF::BoolIf(ref b, ref e1, ref e2) => { - let b_borrow = b.as_whnf(); - match &*b_borrow { - BoolLit(true) => Ret::ValueRef(e1), - BoolLit(false) => Ret::ValueRef(e2), - _ => { - let e1_borrow = e1.as_whnf(); - let e2_borrow = e2.as_whnf(); - match (&*e1_borrow, &*e2_borrow) { - // Simplify `if b then True else False` - (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b), - _ if e1 == e2 => Ret::ValueRef(e1), - _ => { - drop(b_borrow); - drop(e1_borrow); - drop(e2_borrow); - Ret::Expr(expr) - } - } - } - } - } - ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { - Some(ret) => ret, - None => Ret::Expr(expr), - }, - - ExprF::Projection(_, ref ls) if ls.is_empty() => { - Ret::ValueF(RecordLit(HashMap::new())) - } - ExprF::Projection(ref v, ref ls) => { - let v_borrow = v.as_whnf(); - match &*v_borrow { - RecordLit(kvs) => Ret::ValueF(RecordLit( - ls.iter() - .filter_map(|l| { - kvs.get(l).map(|x| (l.clone(), x.clone())) - }) - .collect(), - )), - _ => { - drop(v_borrow); - Ret::Expr(expr) - } - } - } - ExprF::Field(ref v, ref l) => { - let v_borrow = v.as_whnf(); - match &*v_borrow { - RecordLit(kvs) => match kvs.get(l) { - Some(r) => Ret::Value(r.clone()), - None => { - drop(v_borrow); - Ret::Expr(expr) - } - }, - UnionType(kts) => { - Ret::ValueF(UnionConstructor(l.clone(), kts.clone())) - } - _ => { - drop(v_borrow); - Ret::Expr(expr) - } - } - } - ExprF::ProjectionByExpr(_, _) => { - unimplemented!("selection by expression") - } - - ExprF::Merge(ref handlers, ref variant, _) => { - 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) { - Some(h) => Ret::Value(h.clone()), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - }, - (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { - Some(h) => Ret::Value(h.app(v.clone())), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - }, - _ => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - } - } - ExprF::ToMap(_, _) => unimplemented!("toMap"), - }; - - match ret { - Ret::ValueF(v) => v, - Ret::Value(v) => v.to_whnf_check_type(ty), - Ret::ValueRef(v) => v.to_whnf_check_type(ty), - Ret::Expr(expr) => ValueF::PartialExpr(expr), - } -} - -/// Normalize a ValueF into WHNF -pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF { - match v { - ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), - ValueF::PartialExpr(e) => normalize_one_layer(e, ty), - ValueF::TextLit(elts) => { - ValueF::TextLit(squash_textlit(elts.into_iter())) - } - // All other cases are already in WHNF - v => v, - } -} diff --git a/dhall/src/phase/parse.rs b/dhall/src/phase/parse.rs deleted file mode 100644 index e277e54..0000000 --- a/dhall/src/phase/parse.rs +++ /dev/null @@ -1,37 +0,0 @@ -use std::fs::File; -use std::io::Read; -use std::path::Path; - -use crate::syntax::parse_expr; - -use crate::error::Error; -use crate::phase::resolve::ImportRoot; -use crate::phase::Parsed; - -pub(crate) fn parse_file(f: &Path) -> Result<Parsed, Error> { - let mut buffer = String::new(); - File::open(f)?.read_to_string(&mut buffer)?; - let expr = parse_expr(&*buffer)?; - let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned()); - Ok(Parsed(expr, root)) -} - -pub(crate) fn parse_str(s: &str) -> Result<Parsed, Error> { - let expr = parse_expr(s)?; - let root = ImportRoot::LocalDir(std::env::current_dir()?); - Ok(Parsed(expr, root)) -} - -pub(crate) fn parse_binary(data: &[u8]) -> Result<Parsed, Error> { - let expr = crate::phase::binary::decode(data)?; - let root = ImportRoot::LocalDir(std::env::current_dir()?); - Ok(Parsed(expr, root)) -} - -pub(crate) fn parse_binary_file(f: &Path) -> Result<Parsed, Error> { - let mut buffer = Vec::new(); - File::open(f)?.read_to_end(&mut buffer)?; - let expr = crate::phase::binary::decode(&buffer)?; - let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned()); - Ok(Parsed(expr, root)) -} diff --git a/dhall/src/phase/resolve.rs b/dhall/src/phase/resolve.rs deleted file mode 100644 index 5920f82..0000000 --- a/dhall/src/phase/resolve.rs +++ /dev/null @@ -1,180 +0,0 @@ -use std::collections::HashMap; -use std::path::{Path, PathBuf}; - -use crate::error::{Error, ImportError}; -use crate::phase::{Normalized, NormalizedExpr, Parsed, Resolved}; -use crate::syntax::{FilePath, ImportLocation, URL}; - -type Import = crate::syntax::Import<NormalizedExpr>; - -/// A root from which to resolve relative imports. -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ImportRoot { - LocalDir(PathBuf), -} - -type ImportCache = HashMap<Import, Normalized>; - -pub(crate) type ImportStack = Vec<Import>; - -fn resolve_import( - import: &Import, - root: &ImportRoot, - import_cache: &mut ImportCache, - import_stack: &ImportStack, -) -> Result<Normalized, ImportError> { - use self::ImportRoot::*; - use crate::syntax::FilePrefix::*; - use crate::syntax::ImportLocation::*; - let cwd = match root { - LocalDir(cwd) => cwd, - }; - match &import.location { - Local(prefix, path) => { - let path_buf: PathBuf = path.file_path.iter().collect(); - let path_buf = match prefix { - // TODO: fail gracefully - Parent => cwd.parent().unwrap().join(path_buf), - Here => cwd.join(path_buf), - _ => unimplemented!("{:?}", import), - }; - Ok(load_import(&path_buf, import_cache, import_stack).map_err( - |e| ImportError::Recursive(import.clone(), Box::new(e)), - )?) - } - _ => unimplemented!("{:?}", import), - } -} - -fn load_import( - f: &Path, - import_cache: &mut ImportCache, - import_stack: &ImportStack, -) -> Result<Normalized, Error> { - Ok( - do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)? - .typecheck()? - .normalize(), - ) -} - -fn do_resolve_expr( - parsed: Parsed, - import_cache: &mut ImportCache, - import_stack: &ImportStack, -) -> Result<Resolved, ImportError> { - let Parsed(mut expr, root) = parsed; - let mut resolve = |import: Import| -> Result<Normalized, ImportError> { - if import_stack.contains(&import) { - return Err(ImportError::ImportCycle(import_stack.clone(), import)); - } - match import_cache.get(&import) { - Some(expr) => Ok(expr.clone()), - None => { - // Copy the import stack and push the current import - let mut import_stack = import_stack.clone(); - import_stack.push(import.clone()); - - // Resolve the import recursively - let expr = resolve_import( - &import, - &root, - import_cache, - &import_stack, - )?; - - // Add the import to the cache - import_cache.insert(import, expr.clone()); - Ok(expr) - } - } - }; - expr.traverse_resolve_mut(&mut resolve)?; - Ok(Resolved(expr)) -} - -pub(crate) fn resolve(e: Parsed) -> Result<Resolved, ImportError> { - do_resolve_expr(e, &mut HashMap::new(), &Vec::new()) -} - -pub(crate) fn skip_resolve_expr( - parsed: Parsed, -) -> Result<Resolved, ImportError> { - let mut expr = parsed.0; - let mut resolve = |import: Import| -> Result<Normalized, ImportError> { - Err(ImportError::UnexpectedImport(import)) - }; - expr.traverse_resolve_mut(&mut resolve)?; - Ok(Resolved(expr)) -} - -pub trait Canonicalize { - fn canonicalize(&self) -> Self; -} - -impl Canonicalize for FilePath { - fn canonicalize(&self) -> FilePath { - let mut file_path = Vec::new(); - let mut file_path_components = self.file_path.clone().into_iter(); - - loop { - let component = file_path_components.next(); - match component.as_ref() { - // ─────────────────── - // canonicalize(ε) = ε - None => break, - - // canonicalize(directory₀) = directory₁ - // ─────────────────────────────────────── - // canonicalize(directory₀/.) = directory₁ - Some(c) if c == "." => continue, - - Some(c) if c == ".." => match file_path_components.next() { - // canonicalize(directory₀) = ε - // ──────────────────────────── - // canonicalize(directory₀/..) = /.. - None => file_path.push("..".to_string()), - - // canonicalize(directory₀) = directory₁/.. - // ────────────────────────────────────────────── - // canonicalize(directory₀/..) = directory₁/../.. - Some(ref c) if c == ".." => { - file_path.push("..".to_string()); - file_path.push("..".to_string()); - } - - // canonicalize(directory₀) = directory₁/component - // ─────────────────────────────────────────────── ; If "component" is not - // canonicalize(directory₀/..) = directory₁ ; ".." - Some(_) => continue, - }, - - // canonicalize(directory₀) = directory₁ - // ───────────────────────────────────────────────────────── ; If no other - // canonicalize(directory₀/component) = directory₁/component ; rule matches - Some(c) => file_path.push(c.clone()), - } - } - - FilePath { file_path } - } -} - -impl<SE: Copy> Canonicalize for ImportLocation<SE> { - fn canonicalize(&self) -> ImportLocation<SE> { - match self { - ImportLocation::Local(prefix, file) => { - ImportLocation::Local(*prefix, file.canonicalize()) - } - ImportLocation::Remote(url) => ImportLocation::Remote(URL { - scheme: url.scheme, - authority: url.authority.clone(), - path: url.path.canonicalize(), - query: url.query.clone(), - headers: url.headers.clone(), - }), - ImportLocation::Env(name) => ImportLocation::Env(name.to_string()), - ImportLocation::Missing => ImportLocation::Missing, - } - } -} diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs deleted file mode 100644 index 9a41be9..0000000 --- a/dhall/src/phase/typecheck.rs +++ /dev/null @@ -1,815 +0,0 @@ -use std::cmp::max; -use std::collections::HashMap; - -use crate::syntax::{ - Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span, -}; - -use crate::core::context::TypecheckContext; -use crate::core::value::Value; -use crate::core::valuef::ValueF; -use crate::core::var::{Shift, Subst}; -use crate::error::{TypeError, TypeMessage}; -use crate::phase::Normalized; - -fn tck_pi_type( - ctx: &TypecheckContext, - x: Label, - tx: Value, - te: Value, -) -> Result<Value, TypeError> { - use crate::error::TypeMessage::*; - let ctx2 = ctx.insert_type(&x, tx.clone()); - - let ka = match tx.get_type()?.as_const() { - Some(k) => k, - _ => return Err(TypeError::new(ctx, InvalidInputType(tx))), - }; - - let kb = match te.get_type()?.as_const() { - Some(k) => k, - _ => { - return Err(TypeError::new( - &ctx2, - InvalidOutputType(te.get_type()?), - )) - } - }; - - let k = function_check(ka, kb); - - Ok(Value::from_valuef_and_type( - ValueF::Pi(x.into(), tx, te), - Value::from_const(k), - )) -} - -fn tck_record_type( - ctx: &TypecheckContext, - kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>, -) -> Result<Value, TypeError> { - use crate::error::TypeMessage::*; - use std::collections::hash_map::Entry; - let mut new_kts = HashMap::new(); - // An empty record type has type Type - let mut k = Const::Type; - for e in kts { - let (x, t) = e?; - // Construct the union of the contained `Const`s - match t.get_type()?.as_const() { - Some(k2) => k = max(k, k2), - None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))), - } - // Check for duplicated entries - let entry = new_kts.entry(x); - match &entry { - Entry::Occupied(_) => { - return Err(TypeError::new(ctx, RecordTypeDuplicateField)) - } - Entry::Vacant(_) => entry.or_insert_with(|| t), - }; - } - - Ok(Value::from_valuef_and_type( - ValueF::RecordType(new_kts), - Value::from_const(k), - )) -} - -fn tck_union_type<Iter>( - ctx: &TypecheckContext, - kts: Iter, -) -> Result<Value, TypeError> -where - Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>, -{ - use crate::error::TypeMessage::*; - use std::collections::hash_map::Entry; - let mut new_kts = HashMap::new(); - // Check that all types are the same const - let mut k = None; - for e in kts { - let (x, t) = e?; - if let Some(t) = &t { - match (k, t.get_type()?.as_const()) { - (None, Some(k2)) => k = Some(k2), - (Some(k1), Some(k2)) if k1 == k2 => {} - _ => { - return Err(TypeError::new( - ctx, - InvalidFieldType(x, t.clone()), - )) - } - } - } - let entry = new_kts.entry(x); - match &entry { - Entry::Occupied(_) => { - return Err(TypeError::new(ctx, UnionTypeDuplicateField)) - } - Entry::Vacant(_) => entry.or_insert_with(|| t), - }; - } - - // An empty union type has type Type; - // 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), - Value::from_const(k), - )) -} - -fn function_check(a: Const, b: Const) -> Const { - if b == Const::Type { - Const::Type - } else { - max(a, b) - } -} - -pub(crate) fn const_to_value(c: Const) -> Value { - let v = ValueF::Const(c); - match c { - Const::Type => { - Value::from_valuef_and_type(v, const_to_value(Const::Kind)) - } - Const::Kind => { - Value::from_valuef_and_type(v, const_to_value(Const::Sort)) - } - Const::Sort => Value::const_sort(), - } -} - -pub fn rc<E>(x: RawExpr<E>) -> Expr<E> { - Expr::new(x, Span::Artificial) -} - -// 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) }; - ($var:ident) => { - ExprF::Var(crate::syntax::V(stringify!($var).into(), 0)) - }; - (Optional $ty:ident) => { - ExprF::App( - rc(ExprF::Builtin(Builtin::Optional)), - rc(make_type!($ty)) - ) - }; - (List $($rest:tt)*) => { - ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - rc(make_type!($($rest)*)) - ) - }; - ({ $($label:ident : $ty:ident),* }) => {{ - let mut kts = crate::syntax::map::DupTreeMap::new(); - $( - kts.insert( - Label::from(stringify!($label)), - rc(make_type!($ty)), - ); - )* - ExprF::RecordType(kts) - }}; - ($ty:ident -> $($rest:tt)*) => { - ExprF::Pi( - "_".into(), - rc(make_type!($ty)), - rc(make_type!($($rest)*)) - ) - }; - (($($arg:tt)*) -> $($rest:tt)*) => { - ExprF::Pi( - "_".into(), - rc(make_type!($($arg)*)), - rc(make_type!($($rest)*)) - ) - }; - (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - ExprF::Pi( - stringify!($var).into(), - rc(make_type!($($ty)*)), - rc(make_type!($($rest)*)) - ) - }; -} - -fn type_of_builtin<E>(b: Builtin) -> Expr<E> { - use crate::syntax::Builtin::*; - rc(match b { - Bool | Natural | Integer | Double | Text => make_type!(Type), - List | Optional => make_type!( - Type -> Type - ), - - NaturalFold => make_type!( - Natural -> - forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural - ), - NaturalBuild => make_type!( - (forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural) -> - Natural - ), - NaturalIsZero | NaturalEven | NaturalOdd => make_type!( - Natural -> Bool - ), - NaturalToInteger => make_type!(Natural -> Integer), - NaturalShow => make_type!(Natural -> Text), - NaturalSubtract => make_type!(Natural -> Natural -> Natural), - - IntegerToDouble => make_type!(Integer -> Double), - IntegerShow => make_type!(Integer -> Text), - DoubleShow => make_type!(Double -> Text), - TextShow => make_type!(Text -> Text), - - ListBuild => make_type!( - forall (a: Type) -> - (forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list) -> - List a - ), - ListFold => make_type!( - forall (a: Type) -> - (List a) -> - forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list - ), - ListLength => make_type!(forall (a: Type) -> (List a) -> Natural), - ListHead | ListLast => { - make_type!(forall (a: Type) -> (List a) -> Optional a) - } - ListIndexed => make_type!( - forall (a: Type) -> - (List a) -> - List { index: Natural, value: a } - ), - ListReverse => make_type!( - forall (a: Type) -> (List a) -> List a - ), - - OptionalBuild => make_type!( - forall (a: Type) -> - (forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional) -> - Optional a - ), - OptionalFold => make_type!( - forall (a: Type) -> - (Optional a) -> - forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional - ), - OptionalNone => make_type!( - forall (a: Type) -> Optional a - ), - }) -} - -pub(crate) fn builtin_to_value(b: Builtin) -> Value { - let ctx = TypecheckContext::new(); - Value::from_valuef_and_type( - ValueF::from_builtin(b), - type_with(&ctx, type_of_builtin(b)).unwrap(), - ) -} - -/// Type-check an expression and return the expression alongside its type if type-checking -/// succeeded, or an error if type-checking failed. -/// Some normalization is done while typechecking, so the returned expression might be partially -/// normalized as well. -fn type_with( - ctx: &TypecheckContext, - e: Expr<Normalized>, -) -> Result<Value, TypeError> { - use crate::syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; - let span = e.span(); - - Ok(match e.as_ref() { - Lam(var, annot, body) => { - let annot = type_with(ctx, annot.clone())?; - 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), - tck_pi_type(ctx, var.clone(), annot, body_type)?, - ) - } - Pi(x, ta, tb) => { - let ta = type_with(ctx, ta.clone())?; - let ctx2 = ctx.insert_type(x, ta.clone()); - let tb = type_with(&ctx2, tb.clone())?; - return tck_pi_type(ctx, x.clone(), ta, tb); - } - Let(x, t, v, e) => { - let v = if let Some(t) = t { - t.rewrap(Annot(v.clone(), t.clone())) - } else { - v.clone() - }; - - let v = type_with(ctx, v)?; - return type_with(&ctx.insert_value(x, v.clone())?, e.clone()); - } - Embed(p) => p.clone().into_typed().into_value(), - Var(var) => match ctx.lookup(&var) { - Some(typed) => typed.clone(), - None => { - return Err(TypeError::new( - ctx, - TypeMessage::UnboundVariable(span), - )) - } - }, - e => { - // Typecheck recursively all subexpressions - let expr = e.traverse_ref_with_special_handling_of_binders( - |e| type_with(ctx, e.clone()), - |_, _| unreachable!(), - )?; - type_last_layer(ctx, expr, span)? - } - }) -} - -/// When all sub-expressions have been typed, check the remaining toplevel -/// layer. -fn type_last_layer( - ctx: &TypecheckContext, - e: ExprF<Value, Normalized>, - span: Span, -) -> Result<Value, TypeError> { - use crate::error::TypeMessage::*; - use crate::syntax::BinOp::*; - use crate::syntax::Builtin::*; - use crate::syntax::Const::Type; - use crate::syntax::ExprF::*; - let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg)); - - /// Intermediary return type - enum Ret { - /// Returns the contained value as is - RetWhole(Value), - /// Returns the input expression `e` with the contained value as its type - RetTypeOnly(Value), - } - use Ret::*; - - let ret = match &e { - Import(_) => unreachable!( - "There should remain no imports in a resolved expression" - ), - Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => { - unreachable!() - } - App(f, a) => { - 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), - _ => return mkerr(NotAFunction(f.clone())), - }; - if &a.get_type()? != tx { - return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone())); - } - - RetTypeOnly(tb.subst_shift(&x.into(), a)) - } - Annot(x, t) => { - if &x.get_type()? != t { - return mkerr(AnnotMismatch(x.clone(), t.clone())); - } - RetWhole(x.clone()) - } - Assert(t) => { - match &*t.as_whnf() { - ValueF::Equivalence(x, y) if x == y => {} - ValueF::Equivalence(x, y) => { - return mkerr(AssertMismatch(x.clone(), y.clone())) - } - _ => return mkerr(AssertMustTakeEquivalence), - } - RetTypeOnly(t.clone()) - } - BoolIf(x, y, z) => { - if *x.get_type()?.as_whnf() != ValueF::from_builtin(Bool) { - return mkerr(InvalidPredicate(x.clone())); - } - - if y.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(IfBranchMustBeTerm(true, y.clone())); - } - - if z.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(IfBranchMustBeTerm(false, z.clone())); - } - - if y.get_type()? != z.get_type()? { - return mkerr(IfBranchMismatch(y.clone(), z.clone())); - } - - RetTypeOnly(y.get_type()?) - } - EmptyListLit(t) => { - match &*t.as_whnf() { - ValueF::AppliedBuiltin(crate::syntax::Builtin::List, args) - if args.len() == 1 => {} - _ => return mkerr(InvalidListType(t.clone())), - } - RetTypeOnly(t.clone()) - } - NEListLit(xs) => { - let mut iter = xs.iter().enumerate(); - let (_, x) = iter.next().unwrap(); - for (i, y) in iter { - if x.get_type()? != y.get_type()? { - return mkerr(InvalidListElement( - i, - x.get_type()?, - y.clone(), - )); - } - } - let t = x.get_type()?; - if t.get_type()?.as_const() != Some(Type) { - return mkerr(InvalidListType(t)); - } - - RetTypeOnly(Value::from_builtin(crate::syntax::Builtin::List).app(t)) - } - SomeLit(x) => { - let t = x.get_type()?; - if t.get_type()?.as_const() != Some(Type) { - return mkerr(InvalidOptionalType(t)); - } - - RetTypeOnly( - Value::from_builtin(crate::syntax::Builtin::Optional).app(t), - ) - } - RecordType(kts) => RetWhole(tck_record_type( - ctx, - kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), - )?), - UnionType(kts) => RetWhole(tck_union_type( - ctx, - kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))), - )?), - RecordLit(kvs) => RetTypeOnly(tck_record_type( - ctx, - kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))), - )?), - Field(r, x) => { - match &*r.get_type()?.as_whnf() { - ValueF::RecordType(kts) => match kts.get(&x) { - Some(tth) => { - RetTypeOnly(tth.clone()) - }, - None => return mkerr(MissingRecordField(x.clone(), - r.clone())), - }, - // TODO: branch here only when r.get_type() is a Const - _ => { - match &*r.as_whnf() { - ValueF::UnionType(kts) => match kts.get(&x) { - // Constructor has type T -> < x: T, ... > - Some(Some(t)) => { - RetTypeOnly( - tck_pi_type( - ctx, - "_".into(), - t.clone(), - r.under_binder(Label::from("_")), - )? - ) - }, - Some(None) => { - RetTypeOnly(r.clone()) - }, - None => { - return mkerr(MissingUnionField( - x.clone(), - r.clone(), - )) - }, - }, - _ => { - return mkerr(NotARecord( - x.clone(), - r.clone() - )) - }, - } - } - // _ => mkerr(NotARecord( - // x, - // r?, - // )), - } - } - Const(c) => RetWhole(const_to_value(*c)), - Builtin(b) => RetWhole(builtin_to_value(*b)), - BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)), - NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)), - IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)), - DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)), - TextLit(interpolated) => { - let text_type = builtin_to_value(Text); - for contents in interpolated.iter() { - use InterpolatedTextContents::Expr; - if let Expr(x) = contents { - if x.get_type()? != text_type { - return mkerr(InvalidTextInterpolation(x.clone())); - } - } - } - RetTypeOnly(text_type) - } - BinOp(RightBiasedRecordMerge, l, r) => { - use crate::phase::normalize::merge_maps; - - let l_type = l.get_type()?; - let r_type = r.get_type()?; - - // Extract the LHS record type - let l_type_borrow = l_type.as_whnf(); - let kts_x = match &*l_type_borrow { - ValueF::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, - _ => return mkerr(MustCombineRecord(r.clone())), - }; - - // Union the two records, prefering - // the values found in the RHS. - let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| { - Ok(r_t.clone()) - })?; - - // Construct the final record type from the union - RetTypeOnly(tck_record_type( - ctx, - kts.into_iter().map(|(x, v)| Ok((x.clone(), v))), - )?) - } - BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer( - ctx, - ExprF::BinOp( - RecursiveRecordTypeMerge, - l.get_type()?, - r.get_type()?, - ), - Span::Artificial, - )?), - BinOp(RecursiveRecordTypeMerge, l, r) => { - use crate::phase::normalize::merge_maps; - - // Extract the LHS record type - let borrow_l = l.as_whnf(); - let kts_x = match &*borrow_l { - ValueF::RecordType(kts) => kts, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) - } - }; - - // Extract the RHS record type - let borrow_r = r.as_whnf(); - let kts_y = match &*borrow_r { - ValueF::RecordType(kts) => kts, - _ => { - return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) - } - }; - - // Ensure that the records combine without a type error - let kts = merge_maps( - kts_x, - kts_y, - // If the Label exists for both records, then we hit the recursive case. - |_, l: &Value, r: &Value| { - type_last_layer( - ctx, - ExprF::BinOp( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - ), - Span::Artificial, - ) - }, - )?; - - RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?) - } - BinOp(o @ ListAppend, l, r) => { - match &*l.get_type()?.as_whnf() { - ValueF::AppliedBuiltin(List, _) => {} - _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), - } - - if l.get_type()? != r.get_type()? { - return mkerr(BinOpTypeMismatch(*o, r.clone())); - } - - RetTypeOnly(l.get_type()?) - } - BinOp(Equivalence, l, r) => { - if l.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone())); - } - if r.get_type()?.get_type()?.as_const() != Some(Type) { - return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone())); - } - - if l.get_type()? != r.get_type()? { - return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone())); - } - - RetWhole(Value::from_valuef_and_type( - ValueF::Equivalence(l.clone(), r.clone()), - Value::from_const(Type), - )) - } - BinOp(o, l, r) => { - let t = builtin_to_value(match o { - BoolAnd => Bool, - BoolOr => Bool, - BoolEQ => Bool, - BoolNE => Bool, - NaturalPlus => Natural, - NaturalTimes => Natural, - TextAppend => Text, - ListAppend => unreachable!(), - RightBiasedRecordMerge => unreachable!(), - RecursiveRecordMerge => unreachable!(), - RecursiveRecordTypeMerge => unreachable!(), - ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"), - Equivalence => unreachable!(), - }); - - if l.get_type()? != t { - return mkerr(BinOpTypeMismatch(*o, l.clone())); - } - - if r.get_type()? != t { - return mkerr(BinOpTypeMismatch(*o, r.clone())); - } - - RetTypeOnly(t) - } - Merge(record, union, type_annot) => { - let record_type = record.get_type()?; - let record_borrow = record_type.as_whnf(); - let handlers = match &*record_borrow { - ValueF::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, - _ => return mkerr(Merge2ArgMustBeUnion(union.clone())), - }; - - let mut inferred_type = None; - for (x, handler_type) in handlers { - let handler_return_type = - match variants.get(x) { - // Union alternative with type - 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), - _ => { - return mkerr(NotAFunction( - handler_type.clone(), - )) - } - }; - - if variant_type != tx { - return mkerr(TypeMismatch( - handler_type.clone(), - tx.clone(), - variant_type.clone(), - )); - } - - // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`. - match tb.over_binder(x) { - Some(x) => x, - None => return mkerr( - MergeHandlerReturnTypeMustNotBeDependent, - ), - } - } - // Union alternative without type - Some(None) => handler_type.clone(), - None => { - return mkerr(MergeHandlerMissingVariant(x.clone())) - } - }; - match &inferred_type { - None => inferred_type = Some(handler_return_type), - Some(t) => { - if t != &handler_return_type { - return mkerr(MergeHandlerTypeMismatch); - } - } - } - } - for x in variants.keys() { - if !handlers.contains_key(x) { - return mkerr(MergeVariantMissingHandler(x.clone())); - } - } - - match (inferred_type, type_annot) { - (Some(ref t1), Some(t2)) => { - if t1 != t2 { - return mkerr(MergeAnnotMismatch); - } - RetTypeOnly(t2.clone()) - } - (Some(t), None) => RetTypeOnly(t), - (None, Some(t)) => RetTypeOnly(t.clone()), - (None, None) => return mkerr(MergeEmptyNeedsAnnotation), - } - } - ToMap(_, _) => unimplemented!("toMap"), - Projection(record, labels) => { - let record_type = record.get_type()?; - let record_type_borrow = record_type.as_whnf(); - let kts = match &*record_type_borrow { - ValueF::RecordType(kts) => kts, - _ => return mkerr(ProjectionMustBeRecord), - }; - - let mut new_kts = HashMap::new(); - for l in labels { - match kts.get(l) { - None => return mkerr(ProjectionMissingEntry), - Some(t) => new_kts.insert(l.clone(), t.clone()), - }; - } - - RetTypeOnly(Value::from_valuef_and_type( - ValueF::RecordType(new_kts), - record_type.get_type()?, - )) - } - ProjectionByExpr(_, _) => unimplemented!("selection by expression"), - }; - - Ok(match ret { - RetTypeOnly(typ) => Value::from_valuef_and_type_and_span( - ValueF::PartialExpr(e), - typ, - span, - ), - RetWhole(v) => v.with_span(span), - }) -} - -/// `type_of` is the same as `type_with` with an empty context, meaning that the -/// expression must be closed (i.e. no free variables), otherwise type-checking -/// will fail. -pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<Value, TypeError> { - type_with(&TypecheckContext::new(), e) -} - -pub(crate) fn typecheck_with( - expr: Expr<Normalized>, - ty: Expr<Normalized>, -) -> Result<Value, TypeError> { - typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty))) -} |