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 --- src/core.rs | 1056 ----------------------------------------------------------- 1 file changed, 1056 deletions(-) delete mode 100644 src/core.rs (limited to 'src/core.rs') diff --git a/src/core.rs b/src/core.rs deleted file mode 100644 index 473a6a6..0000000 --- a/src/core.rs +++ /dev/null @@ -1,1056 +0,0 @@ -#![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