From 82d50e8734e0caad0b34ae32493ab831e7ec7fae Mon Sep 17 00:00:00 2001 From: NanoTech Date: Thu, 8 Dec 2016 14:59:02 -0600 Subject: Seperate built-in types and functions from Expr --- src/core.rs | 166 ++++++++++++++++++++++++++++-------------------------------- 1 file changed, 76 insertions(+), 90 deletions(-) (limited to 'src/core.rs') diff --git a/src/core.rs b/src/core.rs index 0bc42d4..8b0156c 100644 --- a/src/core.rs +++ b/src/core.rs @@ -125,8 +125,10 @@ pub enum Expr<'i, S, A> { Let(&'i str, Option>>, Box>, Box>), /// `Annot x t ~ x : t` Annot(Box>, Box>), - /// `Bool ~ Bool` - Bool, + /// Built-in types + BuiltinType(BuiltinType), + /// Built-in function values + BuiltinValue(BuiltinValue), /// `BoolLit b ~ b` BoolLit(bool), /// `BoolAnd x y ~ x && y` @@ -139,63 +141,25 @@ pub enum Expr<'i, S, A> { BoolNE(Box>, Box>), /// `BoolIf x y z ~ if x then y else z` BoolIf(Box>, Box>, Box>), - /// `Natural ~ Natural` - Natural, /// `NaturalLit n ~ +n` NaturalLit(Natural), - /// `NaturalFold ~ Natural/fold` - NaturalFold, - /// `NaturalBuild ~ Natural/build` - NaturalBuild, - /// `NaturalIsZero ~ Natural/isZero` - NaturalIsZero, - /// `NaturalEven ~ Natural/even` - NaturalEven, - /// `NaturalOdd ~ Natural/odd` - NaturalOdd, /// `NaturalPlus x y ~ x + y` NaturalPlus(Box>, Box>), /// `NaturalTimes x y ~ x * y` NaturalTimes(Box>, Box>), - /// `Integer ~ Integer` - Integer, /// `IntegerLit n ~ n` IntegerLit(Integer), - /// `Double ~ Double` - Double, /// `DoubleLit n ~ n` DoubleLit(Double), - /// `Text ~ Text` - Text, /// `TextLit t ~ t` TextLit(Builder), /// `TextAppend x y ~ x ++ y` TextAppend(Box>, Box>), - /// `List ~ List` - List, /// `ListLit t [x, y, z] ~ [x, y, z] : List t` ListLit(Box>, Vec>), - /// `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, - /// `Optional ~ Optional` - Optional, /// `OptionalLit t [e] ~ [e] : Optional t` /// `OptionalLit t [] ~ [] : Optional t` OptionalLit(Box>, Vec>), - /// `OptionalFold ~ Optional/fold` - OptionalFold, /// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }` Record(HashMap<&'i str, Expr<'i, S, A>>), /// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }` @@ -216,39 +180,54 @@ pub enum Expr<'i, S, A> { Embed(A), } -impl<'i, S, A> Expr<'i, S, A> { - /// Clones the expression if it is a unit constructor - fn clone_unit(&self) -> Option> { - use Expr::*; - match self { - &Bool => Some(Bool), - &Natural => Some(Natural), - &NaturalFold => Some(NaturalFold), - &NaturalBuild => Some(NaturalBuild), - &NaturalIsZero => Some(NaturalIsZero), - &NaturalEven => Some(NaturalEven), - &NaturalOdd => Some(NaturalOdd), - &Integer => Some(Integer), - &Double => Some(Double), - &Text => Some(Text), - &List => Some(List), - &ListBuild => Some(ListBuild), - &ListFold => Some(ListFold), - &ListLength => Some(ListLength), - &ListHead => Some(ListHead), - &ListLast => Some(ListLast), - &ListIndexed => Some(ListIndexed), - &ListReverse => Some(ListReverse), - &Optional => Some(Optional), - &OptionalFold => Some(OptionalFold), - _ => None, - } - } +/// 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, +} - /// Returns true if the expression is a unit constructor - pub fn is_unit(&self) -> bool { - self.clone_unit::().is_some() - } +/// 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, + /// `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> { @@ -263,6 +242,18 @@ impl<'i, S, A> From<&'i str> for Expr<'i, S, A> { } } +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) + } +} + 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>, @@ -509,11 +500,9 @@ shift d v (Note _ b) = b' -- and `shift` does nothing to a closed expression shift _ _ (Embed p) = Embed p */ - e => if let Some(e2) = e.clone_unit() { - e2 - } else { - panic!("Unimplemented shift case: {:?}", (d, v, e)) - }, + BuiltinType(t) => BuiltinType(t), + BuiltinValue(v) => BuiltinValue(v), + e => panic!("Unimplemented shift case: {:?}", (d, v, e)), } } @@ -556,11 +545,9 @@ pub fn subst<'i, S, T, A>(v: V<'i>, a: Expr<'i, S, A>, b: Expr<'i, T, A>) -> Exp let a2 = subst(v, e, *a); ListLit(bx(a2), b2) } - (a, b) => if let Some(e2) = b.clone_unit() { - e2 - } else { - panic!("Unimplemented subst case: {:?}", (v, a, b)) - } + (_, BuiltinType(t)) => BuiltinType(t), + (_, BuiltinValue(v)) => BuiltinValue(v), + (a, b) => panic!("Unimplemented subst case: {:?}", (v, a, b)), } } @@ -578,6 +565,7 @@ pub fn normalize(e: Expr) -> Expr T: Clone + ::std::fmt::Debug, A: Clone + ::std::fmt::Debug, { + use BuiltinValue::*; use Expr::*; match e { Const(k) => Const(k), @@ -633,9 +621,9 @@ pub fn normalize(e: Expr) -> Expr go (Var "Zero") = True go _ = False */ - (NaturalIsZero, NaturalLit(n)) => BoolLit(n == 0), - (NaturalEven, NaturalLit(n)) => BoolLit(n % 2 == 0), - (NaturalOdd, NaturalLit(n)) => BoolLit(n % 2 != 0), + (BuiltinValue(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0), + (BuiltinValue(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0), + (BuiltinValue(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0), /* App (App ListBuild t) k | check -> ListLit t (buildVector k') @@ -697,10 +685,8 @@ pub fn normalize(e: Expr) -> Expr let es2 = es.into_iter().map(normalize).collect(); ListLit(bx(t2), es2) } - _ => if let Some(e2) = e.clone_unit() { - e2 - } else { - panic!("Unimplemented normalize case: {:?}", e) - } + BuiltinType(t) => BuiltinType(t), + BuiltinValue(v) => BuiltinValue(v), + _ => panic!("Unimplemented normalize case: {:?}", e), } } -- cgit v1.2.3