From e5d9aee00b0c775df1d8e2d8819aeb80dffa73c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 1 Mar 2019 17:28:19 +0100 Subject: Split abnf_to_pest and dhall into their own crates --- dhall/src/core.rs | 1056 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1056 insertions(+) create mode 100644 dhall/src/core.rs (limited to 'dhall/src/core.rs') diff --git a/dhall/src/core.rs b/dhall/src/core.rs new file mode 100644 index 0000000..473a6a6 --- /dev/null +++ b/dhall/src/core.rs @@ -0,0 +1,1056 @@ +#![allow(non_snake_case)] +use std::collections::BTreeMap; +use std::fmt::{self, Display}; +use std::path::PathBuf; + +/* +module Dhall.Core ( + -- * Syntax + Const(..) + , Path(..) + , Var(..) + , Expr(..) + + -- * Normalization + , normalize + , subst + , shift + + -- * Pretty-printing + , pretty + + -- * Miscellaneous + , internalError + ) where +*/ + +/// Constants for a pure type system +/// +/// The only axiom is: +/// +/// ```c +/// ⊦ Type : Kind +/// ``` +/// +/// ... and the valid rule pairs are: +/// +/// ```c +/// ⊦ Type ↝ Type : Type -- Functions from terms to terms (ordinary functions) +/// ⊦ Kind ↝ Type : Type -- Functions from types to terms (polymorphic functions) +/// ⊦ Kind ↝ Kind : Kind -- Functions from types to types (type constructors) +/// ``` +/// +/// These are the same rule pairs as System Fω +/// +/// Note that Dhall does not support functions from terms to types and therefore +/// Dhall is not a dependently typed language +/// +#[derive(Debug, Copy, Clone, PartialEq, Eq)] // (Show, Bounded, Enum) +pub enum Const { + Type, + Kind, +} + + +/// Path to an external resource +#[derive(Debug, Clone, PartialEq, Eq)] // (Eq, Ord, Show) +pub enum Path { + File(PathBuf), + URL(String), +} + +/// Label for a bound variable +/// +/// The `String` field is the variable's name (i.e. \"`x`\"). +/// +/// The `Int` field disambiguates variables with the same name if there are +/// multiple bound variables of the same name in scope. Zero refers to the +/// nearest bound variable and the index increases by one for each bound +/// variable of the same name going outward. The following diagram may help: +/// +/// ```c +/// +---refers to--+ +/// | | +/// v | +/// \(x : Type) -> \(y : Type) -> \(x : Type) -> x@0 +/// +/// +------------------refers to-----------------+ +/// | | +/// v | +/// \(x : Type) -> \(y : Type) -> \(x : Type) -> x@1 +/// ``` +/// +/// This `Int` behaves like a De Bruijn index in the special case where all +/// variables have the same name. +/// +/// You can optionally omit the index if it is `0`: +/// +/// ```c +/// +refers to+ +/// | | +/// v | +/// \(x : *) -> \(y : *) -> \(x : *) -> x +/// ``` +/// +/// Zero indices are omitted when pretty-printing `Var`s and non-zero indices +/// appear as a numeric suffix. +/// +#[derive(Debug, Copy, Clone, PartialEq, Eq)] // (Eq, Show) +pub struct V<'i>(pub &'i str, pub usize); + +/* +instance IsString Var where + fromString str = V (fromString str) 0 + +instance Buildable Var where + build = buildVar +*/ + +/// Syntax tree for expressions +#[derive(Debug, Clone, PartialEq)] // (Functor, Foldable, Traversable, Show) +pub enum Expr<'i, S, A> { + /// `Const c ~ c` + Const(Const), + /// `Var (V x 0) ~ x`
+ /// `Var (V x n) ~ x@n` + Var(V<'i>), + /// `Lam x A b ~ λ(x : A) -> b` + Lam(&'i str, Box>, Box>), + /// `Pi "_" A B ~ A -> B` + /// `Pi x A B ~ ∀(x : A) -> B` + Pi(&'i str, Box>, Box>), + /// `App f A ~ f A` + App(Box>, Box>), + /// `Let x Nothing r e ~ let x = r in e` + /// `Let x (Just t) r e ~ let x : t = r in e` + Let(&'i str, Option>>, Box>, Box>), + /// `Annot x t ~ x : t` + Annot(Box>, Box>), + /// Built-in types + BuiltinType(BuiltinType), + /// Built-in function values + BuiltinValue(BuiltinValue), + /// `BoolLit b ~ b` + BoolLit(bool), + /// `BoolAnd x y ~ x && y` + BoolAnd(Box>, Box>), + /// `BoolOr x y ~ x || y` + BoolOr(Box>, Box>), + /// `BoolEQ x y ~ x == y` + BoolEQ(Box>, Box>), + /// `BoolNE x y ~ x != y` + BoolNE(Box>, Box>), + /// `BoolIf x y z ~ if x then y else z` + BoolIf(Box>, Box>, Box>), + /// `NaturalLit n ~ +n` + NaturalLit(Natural), + /// `NaturalPlus x y ~ x + y` + NaturalPlus(Box>, Box>), + /// `NaturalTimes x y ~ x * y` + NaturalTimes(Box>, Box>), + /// `IntegerLit n ~ n` + IntegerLit(Integer), + /// `DoubleLit n ~ n` + DoubleLit(Double), + /// `TextLit t ~ t` + TextLit(Builder), + /// `TextAppend x y ~ x ++ y` + TextAppend(Box>, Box>), + /// `ListLit t [x, y, z] ~ [x, y, z] : List t` + ListLit(Box>, Vec>), + /// `OptionalLit t [e] ~ [e] : Optional t` + /// `OptionalLit t [] ~ [] : Optional t` + OptionalLit(Box>, Vec>), + /// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }` + Record(BTreeMap<&'i str, Expr<'i, S, A>>), + /// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }` + RecordLit(BTreeMap<&'i str, Expr<'i, S, A>>), + /// `Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >` + Union(BTreeMap<&'i str, Expr<'i, S, A>>), + /// `UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 >` + UnionLit(&'i str, Box>, BTreeMap<&'i str, Expr<'i, S, A>>), + /// `Combine x y ~ x ∧ y` + Combine(Box>, Box>), + /// `Merge x y t ~ merge x y : t` + Merge(Box>, Box>, Box>), + /// `Field e x ~ e.x` + Field(Box>, &'i str), + /// `Note S x ~ e` + Note(S, Box>), + /// `Embed path ~ path` + Embed(A), +} + +/// Built-in types +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum BuiltinType { + /// `Bool ~ Bool` + Bool, + /// `Natural ~ Natural` + Natural, + /// `Integer ~ Integer` + Integer, + /// `Double ~ Double` + Double, + /// `Text ~ Text` + Text, + /// `List ~ List` + List, + /// `Optional ~ Optional` + Optional, +} + +/// Built-in function values +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum BuiltinValue { + /// `NaturalFold ~ Natural/fold` + NaturalFold, + /// `NaturalBuild ~ Natural/build` + NaturalBuild, + /// `NaturalIsZero ~ Natural/isZero` + NaturalIsZero, + /// `NaturalEven ~ Natural/even` + NaturalEven, + /// `NaturalOdd ~ Natural/odd` + NaturalOdd, + NaturalShow, + /// `ListBuild ~ List/build` + ListBuild, + /// `ListFold ~ List/fold` + ListFold, + /// `ListLength ~ List/length` + ListLength, + /// `ListHead ~ List/head` + ListHead, + /// `ListLast ~ List/last` + ListLast, + /// `ListIndexed ~ List/indexed` + ListIndexed, + /// `ListReverse ~ List/reverse` + ListReverse, + /// `OptionalFold ~ Optional/fold` + OptionalFold, +} + +impl<'i> From<&'i str> for V<'i> { + fn from(s: &'i str) -> Self { + V(s, 0) + } +} + +impl<'i, S, A> From<&'i str> for Expr<'i, S, A> { + fn from(s: &'i str) -> Self { + Expr::Var(s.into()) + } +} + +impl<'i, S, A> From for Expr<'i, S, A> { + fn from(t: BuiltinType) -> Self { + Expr::BuiltinType(t) + } +} + +impl<'i, S, A> From for Expr<'i, S, A> { + fn from(t: BuiltinValue) -> Self { + Expr::BuiltinValue(t) + } +} + +impl<'i, S, A> Expr<'i, S, A> { + fn bool_lit(&self) -> Option { + match *self { + Expr::BoolLit(v) => Some(v), + _ => None, + } + } + + fn natural_lit(&self) -> Option { + match *self { + Expr::NaturalLit(v) => Some(v), + _ => None, + } + } + + fn text_lit(&self) -> Option { + match *self { + Expr::TextLit(ref t) => Some(t.clone()), // FIXME? + _ => None, + } + } +} + +// There is a one-to-one correspondence between the formatters in this section +// and the grammar in grammar.lalrpop. Each formatter is named after the +// corresponding grammar rule and the relationship between formatters exactly matches +// the relationship between grammar rules. This leads to the nice emergent property +// of automatically getting all the parentheses and precedences right. +// +// This approach has one major disadvantage: you can get an infinite loop if +// you add a new constructor to the syntax tree without adding a matching +// case the corresponding builder. + +impl<'i, S, A: Display> Display for Expr<'i, S, A> { + fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { // buildExprA + use crate::Expr::*; + match self { + &Annot(ref a, ref b) => { a.fmt_b(f)?; write!(f, " : ")?; b.fmt(f) } + &Note(_, ref b) => b.fmt(f), + a => a.fmt_b(f), + } + } +} + +impl<'i, S, A: Display> Expr<'i, S, A> { + fn fmt_b(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + use crate::Expr::*; + match self { + &Lam(a, ref b, ref c) => { + write!(f, "λ({} : ", a)?; + b.fmt(f)?; + write!(f, ") → ")?; + c.fmt_b(f) + } + &BoolIf(ref a, ref b, ref c) => { + write!(f, "if ")?; + a.fmt(f)?; + write!(f, " then ")?; + b.fmt_b(f)?; + write!(f, " else ")?; + c.fmt_c(f) + } + &Pi("_", ref b, ref c) => { + b.fmt_c(f)?; + write!(f, " → ")?; + c.fmt_b(f) + } + &Pi(a, ref b, ref c) => { + write!(f, "∀({} : ", a)?; + b.fmt(f)?; + write!(f, ") → ")?; + c.fmt_b(f) + } + &Let(a, None, ref c, ref d) => { + write!(f, "let {} = ", a)?; + c.fmt(f)?; + write!(f, ") → ")?; + d.fmt_b(f) + } + &Let(a, Some(ref b), ref c, ref d) => { + write!(f, "let {} : ", a)?; + b.fmt(f)?; + write!(f, " = ")?; + c.fmt(f)?; + write!(f, ") → ")?; + d.fmt_b(f) + } + &ListLit(ref t, ref es) => { + fmt_list("[", "] : List ", es, f, |e, f| e.fmt(f))?; + t.fmt_e(f) + } + &OptionalLit(ref t, ref es) => { + fmt_list("[", "] : Optional ", es, f, |e, f| e.fmt(f))?; + t.fmt_e(f) + } + &Merge(ref a, ref b, ref c) => { + write!(f, "merge ")?; + a.fmt_e(f)?; + write!(f, " ")?; + b.fmt_e(f)?; + write!(f, " : ")?; + c.fmt_d(f) + } + &Note(_, ref b) => b.fmt_b(f), + a => a.fmt_c(f), + } + } + + fn fmt_c(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + use crate::Expr::*; + match self { + // FIXME precedence + &BoolOr(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" || ")?; b.fmt_c(f) } + &TextAppend(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" ++ ")?; b.fmt_c(f) } + &NaturalPlus(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" + ")?; b.fmt_c(f) } + &BoolAnd(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" && ")?; b.fmt_c(f) } + &Combine(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" ^ ")?; b.fmt_c(f) } + &NaturalTimes(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" * ")?; b.fmt_c(f) } + &BoolEQ(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" == ")?; b.fmt_c(f) } + &BoolNE(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" != ")?; b.fmt_c(f) } + &Note(_, ref b) => b.fmt_c(f), + a => a.fmt_d(f), + } + } + + fn fmt_d(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + use crate::Expr::*; + match self { + &App(ref a, ref b) => { a.fmt_d(f)?; f.write_str(" ")?; b.fmt_e(f) } + &Note(_, ref b) => b.fmt_d(f), + a => a.fmt_e(f) + } + } + + fn fmt_e(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + use crate::Expr::*; + match self { + &Field(ref a, b) => { a.fmt_e(f)?; write!(f, ".{}", b) } + &Note(_, ref b) => b.fmt_e(f), + a => a.fmt_f(f) + } + } + + fn fmt_f(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + use crate::Expr::*; + match self { + &Var(a) => a.fmt(f), + &Const(k) => k.fmt(f), + &BuiltinType(t) => t.fmt(f), + &BuiltinValue(v) => v.fmt(f), + &BoolLit(true) => f.write_str("True"), + &BoolLit(false) => f.write_str("False"), + &IntegerLit(a) => a.fmt(f), + &NaturalLit(a) => { + f.write_str("+")?; + a.fmt(f) + } + &DoubleLit(a) => a.fmt(f), + &TextLit(ref a) => ::fmt(a, f), // FIXME Format with Haskell escapes + &Record(ref a) if a.is_empty() => f.write_str("{}"), + &Record(ref a) => { + fmt_list("{ ", " }", a, f, |(k, t), f| write!(f, "{} : {}", k, t)) + } + &RecordLit(ref a) if a.is_empty() => f.write_str("{=}"), + &RecordLit(ref a) => { + fmt_list("{ ", " }", a, f, |(k, v), f| write!(f, "{} = {}", k, v)) + } + &Union(ref _a) => f.write_str("Union"), + &UnionLit(_a, ref _b, ref _c) => f.write_str("UnionLit"), + &Embed(ref a) => a.fmt(f), + &Note(_, ref b) => b.fmt_f(f), + a => write!(f, "({})", a), + } + } +} + +fn fmt_list(open: &str, + close: &str, + it: I, + f: &mut fmt::Formatter, + func: F) + -> Result<(), fmt::Error> + where I: IntoIterator, + F: Fn(T, &mut fmt::Formatter) -> Result<(), fmt::Error> +{ + f.write_str(open)?; + for (i, x) in it.into_iter().enumerate() { + if i > 0 { + f.write_str(", ")?; + } + func(x, f)?; + } + f.write_str(close) +} + +impl Display for Const { + fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + ::fmt(self, f) + } +} + +impl Display for BuiltinType { + fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + ::fmt(self, f) + } +} + +impl Display for BuiltinValue { + fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + use crate::BuiltinValue::*; + f.write_str(match *self { + ListBuild => "List/build", + ListFold => "List/fold", + ListHead => "List/head", + ListIndexed => "List/indexed", + ListLast => "List/last", + ListLength => "List/length", + ListReverse => "List/reverse", + NaturalBuild => "Natural/build", + NaturalEven => "Natural/even", + NaturalFold => "Natural/fold", + NaturalIsZero => "Natural/isZero", + NaturalOdd => "Natural/odd", + NaturalShow => "Natural/show", + OptionalFold => "Optional/fold", + }) + } +} + +impl<'i> Display for V<'i> { + fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + let V(x, n) = *self; + f.write_str(x)?; + if n != 0 { + write!(f, "@{}", n)?; + } + Ok(()) + } +} + +pub fn pi<'i, S, A, Name, Et, Ev>(var: Name, ty: Et, value: Ev) -> Expr<'i, S, A> + where Name: Into<&'i str>, + Et: Into>, + Ev: Into> +{ + Expr::Pi(var.into(), bx(ty.into()), bx(value.into())) +} + +pub fn app<'i, S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<'i, S, A> + where Ef: Into>, + Ex: Into> +{ + Expr::App(bx(f.into()), bx(x.into())) +} + +pub type Builder = String; +pub type Double = f64; +pub type Int = isize; +pub type Integer = isize; +pub type Natural = usize; + +/// A void type +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum X {} + +impl Display for X { + fn fmt(&self, _: &mut fmt::Formatter) -> Result<(), fmt::Error> { + match *self {} + } +} + +pub fn bx(x: T) -> Box { + Box::new(x) +} + +fn add_ui(u: usize, i: isize) -> usize { + if i < 0 { + u.checked_sub(i.checked_neg().unwrap() as usize).unwrap() + } else { + u.checked_add(i as usize).unwrap() + } +} + +fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap + where I: IntoIterator, + K: Eq + Ord + Copy + 'a, + V: 'a, + F: Fn(&V) -> U +{ + it.into_iter().map(|(&k, v)| (k, f(v))).collect() +} + +fn map_op2(f: F, g: G, a: T, b: T) -> V + where F: FnOnce(U, U) -> V, + G: Fn(T) -> U, +{ + f(g(a), g(b)) +} + +/// `shift` is used by both normalization and type-checking to avoid variable +/// capture by shifting variable indices +/// +/// For example, suppose that you were to normalize the following expression: +/// +/// ```c +/// λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x +/// ``` +/// +/// If you were to substitute `y` with `x` without shifting any variable +/// indices, then you would get the following incorrect result: +/// +/// ```c +/// λ(a : Type) → λ(x : a) → λ(x : a) → x -- Incorrect normalized form +/// ``` +/// +/// In order to substitute `x` in place of `y` we need to `shift` `x` by `1` in +/// order to avoid being misinterpreted as the `x` bound by the innermost +/// lambda. If we perform that `shift` then we get the correct result: +/// +/// ```c +/// λ(a : Type) → λ(x : a) → λ(x : a) → x@1 +/// ``` +/// +/// As a more worked example, suppose that you were to normalize the following +/// expression: +/// +/// ```c +/// λ(a : Type) +/// → λ(f : a → a → a) +/// → λ(x : a) +/// → λ(x : a) +/// → (λ(x : a) → f x x@1) x@1 +/// ``` +/// +/// The correct normalized result would be: +/// +/// ```c +/// λ(a : Type) +/// → λ(f : a → a → a) +/// → λ(x : a) +/// → λ(x : a) +/// → f x@1 x +/// ``` +/// +/// The above example illustrates how we need to both increase and decrease +/// variable indices as part of substitution: +/// +/// * We need to increase the index of the outer `x\@1` to `x\@2` before we +/// substitute it into the body of the innermost lambda expression in order +/// to avoid variable capture. This substitution changes the body of the +/// lambda expression to `(f x\@2 x\@1)` +/// +/// * We then remove the innermost lambda and therefore decrease the indices of +/// both `x`s in `(f x\@2 x\@1)` to `(f x\@1 x)` in order to reflect that one +/// less `x` variable is now bound within that scope +/// +/// Formally, `(shift d (V x n) e)` modifies the expression `e` by adding `d` to +/// the indices of all variables named `x` whose indices are greater than +/// `(n + m)`, where `m` is the number of bound variables of the same name +/// within that scope +/// +/// In practice, `d` is always `1` or `-1` because we either: +/// +/// * increment variables by `1` to avoid variable capture during substitution +/// * decrement variables by `1` when deleting lambdas after substitution +/// +/// `n` starts off at `0` when substitution begins and increments every time we +/// descend into a lambda or let expression that binds a variable of the same +/// name in order to avoid shifting the bound variables by mistake. +/// +pub fn shift<'i, S, T, A: Clone>(d: isize, v: V, e: &Expr<'i, S, A>) -> Expr<'i, T, A> { + use crate::Expr::*; + let V(x, n) = v; + match *e { + Const(a) => Const(a), + Var(V(x2, n2)) => { + let n3 = if x == x2 && n <= n2 { add_ui(n2, d) } else { n2 }; + Var(V(x2, n3)) + } + Lam(x2, ref tA, ref b) => { + let n2 = if x == x2 { n + 1 } else { n }; + let tA2 = shift(d, V(x, n ), tA); + let b2 = shift(d, V(x, n2), b); + Lam(x2, bx(tA2), bx(b2)) + } + Pi(x2, ref tA, ref tB) => { + let n2 = if x == x2 { n + 1 } else { n }; + let tA2 = shift(d, V(x, n ), tA); + let tB2 = shift(d, V(x, n2), tB); + pi(x2, tA2, tB2) + } + App(ref f, ref a) => app(shift(d, v, f), shift(d, v, a)), + Let(f, ref mt, ref r, ref e) => { + let n2 = if x == f { n + 1 } else { n }; + let e2 = shift(d, V(x, n2), e); + let mt2 = mt.as_ref().map(|t| bx(shift(d, V(x, n), t))); + let r2 = shift(d, V(x, n), r); + Let(f, mt2, bx(r2), bx(e2)) + } + Annot(ref a, ref b) => shift_op2(Annot, d, v, a, b), + BuiltinType(t) => BuiltinType(t), + BuiltinValue(v) => BuiltinValue(v), + BoolLit(a) => BoolLit(a), + BoolAnd(ref a, ref b) => shift_op2(BoolAnd, d, v, a, b), + BoolOr(ref a, ref b) => shift_op2(BoolOr, d, v, a, b), + BoolEQ(ref a, ref b) => shift_op2(BoolEQ, d, v, a, b), + BoolNE(ref a, ref b) => shift_op2(BoolNE, d, v, a, b), + BoolIf(ref a, ref b, ref c) => { + BoolIf(bx(shift(d, v, a)), bx(shift(d, v, b)), bx(shift(d, v, c))) + } + NaturalLit(a) => NaturalLit(a), + NaturalPlus(ref a, ref b) => NaturalPlus(bx(shift(d, v, a)), bx(shift(d, v, b))), + NaturalTimes(ref a, ref b) => shift_op2(NaturalTimes, d, v, a, b), + IntegerLit(a) => IntegerLit(a), + DoubleLit(a) => DoubleLit(a), + TextLit(ref a) => TextLit(a.clone()), + TextAppend(ref a, ref b) => shift_op2(TextAppend, d, v, a, b), + ListLit(ref t, ref es) => { + ListLit(bx(shift(d, v, t)), + es.iter().map(|e| shift(d, v, e)).collect()) + } + OptionalLit(ref t, ref es) => { + OptionalLit(bx(shift(d, v, t)), + es.iter().map(|e| shift(d, v, e)).collect()) + } + Record(ref a) => Record(map_record_value(a, |val| shift(d, v, val))), + RecordLit(ref a) => RecordLit(map_record_value(a, |val| shift(d, v, val))), + Union(ref a) => Union(map_record_value(a, |val| shift(d, v, val))), + UnionLit(k, ref uv, ref a) => { + UnionLit(k, + bx(shift(d, v, uv)), + map_record_value(a, |val| shift(d, v, val))) + } + Combine(ref a, ref b) => shift_op2(Combine, d, v, a, b), + Merge(ref a, ref b, ref c) => { + Merge(bx(shift(d, v, a)), bx(shift(d, v, b)), bx(shift(d, v, c))) + } + Field(ref a, b) => Field(bx(shift(d, v, a)), b), + Note(_, ref b) => shift(d, v, b), + // The Dhall compiler enforces that all embedded values are closed expressions + // and `shift` does nothing to a closed expression + Embed(ref p) => Embed(p.clone()), + } +} + +fn shift_op2<'i, S, T, A, F>(f: F, + d: isize, + v: V, + a: &Expr<'i, S, A>, + b: &Expr<'i, S, A>) + -> Expr<'i, T, A> + where F: FnOnce(Box>, Box>) -> Expr<'i, T, A>, + A: Clone +{ + map_op2(f, |x| bx(shift(d, v, x)), a, b) +} + +/// Substitute all occurrences of a variable with an expression +/// +/// ```c +/// subst x C B ~ B[x := C] +/// ``` +/// +pub fn subst<'i, S, T, A>(v: V<'i>, e: &Expr<'i, S, A>, b: &Expr<'i, T, A>) -> Expr<'i, S, A> + where S: Clone, + A: Clone +{ + use crate::Expr::*; + let V(x, n) = v; + match *b { + Const(a) => Const(a), + Lam(y, ref tA, ref b) => { + let n2 = if x == y { n + 1 } else { n }; + let b2 = subst(V(x, n2), &shift(1, V(y, 0), e), b); + let tA2 = subst(V(x, n), e, tA); + Lam(y, bx(tA2), bx(b2)) + } + Pi(y, ref tA, ref tB) => { + let n2 = if x == y { n + 1 } else { n }; + let tB2 = subst(V(x, n2), &shift(1, V(y, 0), e), tB); + let tA2 = subst(V(x, n), e, tA); + pi(y, tA2, tB2) + } + App(ref f, ref a) => { + let f2 = subst(v, e, f); + let a2 = subst(v, e, a); + app(f2, a2) + } + Var(v2) => if v == v2 { e.clone() } else { Var(v2) }, + Let(f, ref mt, ref r, ref b) => { + let n2 = if x == f { n + 1 } else { n }; + let b2 = subst(V(x, n2), &shift(1, V(f, 0), e), b); + let mt2 = mt.as_ref().map(|t| bx(subst(V(x, n), e, t))); + let r2 = subst(V(x, n), e, r); + Let(f, mt2, bx(r2), bx(b2)) + } + Annot(ref a, ref b) => subst_op2(Annot, v, e, a, b), + BuiltinType(t) => BuiltinType(t), + BuiltinValue(v) => BuiltinValue(v), + BoolLit(a) => BoolLit(a), + BoolAnd(ref a, ref b) => subst_op2(BoolAnd, v, e, a, b), + BoolOr(ref a, ref b) => subst_op2(BoolOr, v, e, a, b), + BoolEQ(ref a, ref b) => subst_op2(BoolEQ, v, e, a, b), + BoolNE(ref a, ref b) => subst_op2(BoolNE, v, e, a, b), + BoolIf(ref a, ref b, ref c) => { + BoolIf(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c))) + } + NaturalLit(a) => NaturalLit(a), + NaturalPlus(ref a, ref b) => subst_op2(NaturalPlus, v, e, a, b), + NaturalTimes(ref a, ref b) => subst_op2(NaturalTimes, v, e, a, b), + IntegerLit(a) => IntegerLit(a), + DoubleLit(a) => DoubleLit(a), + TextLit(ref a) => TextLit(a.clone()), + TextAppend(ref a, ref b) => subst_op2(TextAppend, v, e, a, b), + ListLit(ref a, ref b) => { + let a2 = subst(v, e, a); + let b2 = b.iter().map(|be| subst(v, e, be)).collect(); + ListLit(bx(a2), b2) + } + OptionalLit(ref a, ref b) => { + let a2 = subst(v, e, a); + let b2 = b.iter().map(|be| subst(v, e, be)).collect(); + OptionalLit(bx(a2), b2) + } + Record(ref kts) => Record(map_record_value(kts, |t| subst(v, e, t))), + RecordLit(ref kvs) => RecordLit(map_record_value(kvs, |val| subst(v, e, val))), + Union(ref kts) => Union(map_record_value(kts, |t| subst(v, e, t))), + UnionLit(k, ref uv, ref kvs) => { + UnionLit(k, + bx(subst(v, e, uv)), + map_record_value(kvs, |val| subst(v, e, val))) + } + Combine(ref a, ref b) => subst_op2(Combine, v, e, a, b), + Merge(ref a, ref b, ref c) => { + Merge(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c))) + } + Field(ref a, b) => Field(bx(subst(v, e, a)), b), + Note(_, ref b) => subst(v, e, b), + Embed(ref p) => Embed(p.clone()), + } +} + +fn subst_op2<'i, S, T, A, F>(f: F, + v: V<'i>, + e: &Expr<'i, S, A>, + a: &Expr<'i, T, A>, + b: &Expr<'i, T, A>) + -> Expr<'i, S, A> + where F: FnOnce(Box>, Box>) -> Expr<'i, S, A>, + S: Clone, + A: Clone +{ + map_op2(f, |x| bx(subst(v, e, x)), a, b) +} + +/// 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<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A> + where S: Clone + fmt::Debug, + T: Clone + fmt::Debug, + A: Clone + fmt::Debug, +{ + use crate::BuiltinValue::*; + use crate::Expr::*; + match *e { + Const(k) => Const(k), + Var(v) => Var(v), + Lam(x, ref tA, ref b) => { + let tA2 = normalize(tA); + let b2 = normalize(b); + Lam(x, bx(tA2), bx(b2)) + } + Pi(x, ref tA, ref tB) => { + let tA2 = normalize(tA); + let tB2 = normalize(tB); + pi(x, tA2, tB2) + } + App(ref f, ref a) => match normalize::(f) { + Lam(x, _A, b) => { // Beta reduce + let vx0 = V(x, 0); + let a2 = shift::( 1, vx0, a); + let b2 = subst::(vx0, &a2, &b); + let b3 = shift::(-1, vx0, &b2); + normalize(&b3) + } + f2 => match (f2, normalize::(a)) { + // fold/build fusion for `List` + (App(box BuiltinValue(ListBuild), _), App(box App(box BuiltinValue(ListFold), _), box e2)) | + (App(box BuiltinValue(ListFold), _), App(box App(box BuiltinValue(ListBuild), _), box e2)) | + + // fold/build fusion for `Natural` + (BuiltinValue(NaturalBuild), App(box BuiltinValue(NaturalFold), box e2)) | + (BuiltinValue(NaturalFold), App(box BuiltinValue(NaturalBuild), box e2)) => normalize(&e2), + + /* + App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero -> + normalize (go n0) + where + go !0 = zero + go !n = App succ' (go (n - 1)) + App NaturalBuild k + | check -> NaturalLit n + | otherwise -> App f' a' + where + labeled = + normalize (App (App (App k Natural) "Succ") "Zero") + + n = go 0 labeled + where + go !m (App (Var "Succ") e') = go (m + 1) e' + go !m (Var "Zero") = m + go !_ _ = internalError text + check = go labeled + where + go (App (Var "Succ") e') = go e' + go (Var "Zero") = True + go _ = False + */ + (BuiltinValue(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0), + (BuiltinValue(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0), + (BuiltinValue(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0), + (BuiltinValue(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()), + (App(f@box BuiltinValue(ListBuild), box t), k) => { + let labeled = + normalize::<_, T, _>(&app(app(app(k.clone(), app( + BuiltinType(self::BuiltinType::List), t.clone())), "Cons"), "Nil")); + + fn list_to_vector<'i, S, A>(v: &mut Vec>, e: Expr<'i, S, A>) + where S: Clone, A: Clone + { + match e { + App(box App(box Var(V("Cons", _)), box x), box e2) => { + v.push(x); + list_to_vector(v, e2) + } + Var(V("Nil", _)) => {} + _ => panic!("internalError list_to_vector"), + } + } + fn check(e: &Expr) -> bool { + match *e { + App(box App(box Var(V("Cons", _)), _), ref e2) => check(e2), + Var(V("Nil", _)) => true, + _ => false, + } + } + + if check(&labeled) { + let mut v = vec![]; + list_to_vector(&mut v, labeled); + ListLit(bx(t), v) + } else { + app(App(f, bx(t)), k) + } + } + (App(box App(box App(box App(box BuiltinValue(ListFold), _), box ListLit(_, xs)), _), cons), nil) => { + let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| // foldr + App(bx(App(cons.clone(), bx(y))), bx(ys)) + ); + normalize(&e2) + } + (App(f, x_), ListLit(t, ys)) => match *f { + BuiltinValue(ListLength) => + NaturalLit(ys.len()), + BuiltinValue(ListHead) => + normalize(&OptionalLit(t, ys.into_iter().take(1).collect())), + BuiltinValue(ListLast) => + normalize(&OptionalLit(t, ys.into_iter().last().into_iter().collect())), + BuiltinValue(ListReverse) => { + let mut xs = ys; + xs.reverse(); + normalize(&ListLit(t, xs)) + } + _ => app(App(f, x_), ListLit(t, ys)), + }, + /* + App (App ListIndexed _) (ListLit t xs) -> + normalize (ListLit t' (fmap adapt (Data.Vector.indexed xs))) + where + t' = Record (Data.Map.fromList kts) + where + kts = [ ("index", Natural) + , ("value", t) + ] + adapt (n, x) = RecordLit (Data.Map.fromList kvs) + where + kvs = [ ("index", NaturalLit (fromIntegral n)) + , ("value", x) + ] + App (App (App (App (App OptionalFold _) (OptionalLit _ xs)) _) just) nothing -> + normalize (maybe nothing just' (toMaybe xs)) + where + just' y = App just y + toMaybe = Data.Maybe.listToMaybe . Data.Vector.toList + */ + (f2, a2) => app(f2, a2), + } + }, + Let(f, _, ref r, ref b) => { + let r2 = shift::<_, S, _>( 1, V(f, 0), r); + let b2 = subst(V(f, 0), &r2, b); + let b3 = shift::<_, T, _>(-1, V(f, 0), &b2); + normalize(&b3) + } + Annot(ref x, _) => normalize(x), + BuiltinType(t) => BuiltinType(t), + BuiltinValue(v) => BuiltinValue(v), + BoolLit(b) => BoolLit(b), + BoolAnd(ref x, ref y) => { + with_binop(BoolAnd, Expr::bool_lit, + |xn, yn| BoolLit(xn && yn), + normalize(x), normalize(y)) + } + BoolOr(ref x, ref y) => { + with_binop(BoolOr, Expr::bool_lit, + |xn, yn| BoolLit(xn || yn), + normalize(x), normalize(y)) + } + BoolEQ(ref x, ref y) => { + with_binop(BoolEQ, Expr::bool_lit, + |xn, yn| BoolLit(xn == yn), + normalize(x), normalize(y)) + } + BoolNE(ref x, ref y) => { + with_binop(BoolNE, Expr::bool_lit, + |xn, yn| BoolLit(xn != yn), + normalize(x), normalize(y)) + } + BoolIf(ref b, ref t, ref f) => match normalize(b) { + BoolLit(true) => normalize(t), + BoolLit(false) => normalize(f), + b2 => BoolIf(bx(b2), bx(normalize(t)), bx(normalize(f))), + }, + NaturalLit(n) => NaturalLit(n), + NaturalPlus(ref x, ref y) => { + with_binop(NaturalPlus, Expr::natural_lit, + |xn, yn| NaturalLit(xn + yn), + normalize(x), normalize(y)) + } + NaturalTimes(ref x, ref y) => { + with_binop(NaturalTimes, Expr::natural_lit, + |xn, yn| NaturalLit(xn * yn), + normalize(x), normalize(y)) + } + IntegerLit(n) => IntegerLit(n), + DoubleLit(n) => DoubleLit(n), + TextLit(ref t) => TextLit(t.clone()), + TextAppend(ref x, ref y) => { + with_binop(TextAppend, Expr::text_lit, + |xt, yt| TextLit(xt + &yt), + normalize(x), normalize(y)) + } + ListLit(ref t, ref es) => { + let t2 = normalize(t); + let es2 = es.iter().map(normalize).collect(); + ListLit(bx(t2), es2) + } + OptionalLit(ref t, ref es) => { + let t2 = normalize(t); + let es2 = es.iter().map(normalize).collect(); + OptionalLit(bx(t2), es2) + } + Record(ref kts) => Record(map_record_value(kts, normalize)), + RecordLit(ref kvs) => RecordLit(map_record_value(kvs, normalize)), + Union(ref kts) => Union(map_record_value(kts, normalize)), + UnionLit(k, ref v, ref kvs) => UnionLit(k, bx(normalize(v)), map_record_value(kvs, normalize)), + Combine(ref _x0, ref _y0) => unimplemented!(), + Merge(ref _x, ref _y, ref _t) => unimplemented!(), + Field(ref r, x) => match normalize(r) { + RecordLit(kvs) => match kvs.get(x) { + Some(r2) => normalize(r2), + None => Field(bx(RecordLit(map_record_value(&kvs, normalize))), x), + }, + r2 => Field(bx(r2), x), + }, + Note(_, ref e) => normalize(e), + Embed(ref a) => Embed(a.clone()), + } +} + +fn with_binop(op: Op, get: Get, set: Set, x: T, y: T) -> T + where Get: Fn(&T) -> Option, + Set: FnOnce(U, U) -> T, + Op: FnOnce(Box, Box) -> T, +{ + if let (Some(xv), Some(yv)) = (get(&x), get(&y)) { + set(xv, yv) + } else { + op(bx(x), bx(y)) + } +} -- cgit v1.2.3