From 655f67fb29ca847f86c3e19338757e7b031d4f50 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 11:09:39 +0000
Subject: Move builtins-related code to its own module

---
 dhall/src/semantics/phase/typecheck.rs | 177 ---------------------------------
 1 file changed, 177 deletions(-)

(limited to 'dhall/src/semantics/phase/typecheck.rs')

diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 2e22ad2..8b13789 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -1,178 +1 @@
-use crate::semantics::{NzEnv, Value, ValueKind};
-use crate::syntax;
-use crate::syntax::{
-    Builtin, Const, Expr, ExprKind, Label, Span, UnspannedExpr,
-};
 
-pub(crate) fn const_to_value(c: Const) -> Value {
-    let v = ValueKind::Const(c);
-    match c {
-        Const::Type => {
-            Value::from_kind_and_type(v, const_to_value(Const::Kind))
-        }
-        Const::Kind => {
-            Value::from_kind_and_type(v, const_to_value(Const::Sort))
-        }
-        Const::Sort => Value::const_sort(),
-    }
-}
-
-pub fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
-    Expr::new(x, Span::Artificial)
-}
-
-// Ad-hoc macro to help construct the types of builtins
-macro_rules! make_type {
-    (Type) => { ExprKind::Const(Const::Type) };
-    (Bool) => { ExprKind::Builtin(Builtin::Bool) };
-    (Natural) => { ExprKind::Builtin(Builtin::Natural) };
-    (Integer) => { ExprKind::Builtin(Builtin::Integer) };
-    (Double) => { ExprKind::Builtin(Builtin::Double) };
-    (Text) => { ExprKind::Builtin(Builtin::Text) };
-    ($var:ident) => {
-        ExprKind::Var(syntax::V(stringify!($var).into(), 0))
-    };
-    (Optional $ty:ident) => {
-        ExprKind::App(
-            rc(ExprKind::Builtin(Builtin::Optional)),
-            rc(make_type!($ty))
-        )
-    };
-    (List $($rest:tt)*) => {
-        ExprKind::App(
-            rc(ExprKind::Builtin(Builtin::List)),
-            rc(make_type!($($rest)*))
-        )
-    };
-    ({ $($label:ident : $ty:ident),* }) => {{
-        let mut kts = syntax::map::DupTreeMap::new();
-        $(
-            kts.insert(
-                Label::from(stringify!($label)),
-                rc(make_type!($ty)),
-            );
-        )*
-        ExprKind::RecordType(kts)
-    }};
-    ($ty:ident -> $($rest:tt)*) => {
-        ExprKind::Pi(
-            "_".into(),
-            rc(make_type!($ty)),
-            rc(make_type!($($rest)*))
-        )
-    };
-    (($($arg:tt)*) -> $($rest:tt)*) => {
-        ExprKind::Pi(
-            "_".into(),
-            rc(make_type!($($arg)*)),
-            rc(make_type!($($rest)*))
-        )
-    };
-    (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
-        ExprKind::Pi(
-            stringify!($var).into(),
-            rc(make_type!($($ty)*)),
-            rc(make_type!($($rest)*))
-        )
-    };
-}
-
-pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
-    use 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),
-        IntegerNegate => make_type!(Integer -> Integer),
-        IntegerClamp => make_type!(Integer -> Natural),
-
-        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 {
-    builtin_to_value_env(b, &NzEnv::new())
-}
-pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value {
-    Value::from_kind_and_type(
-        ValueKind::from_builtin_env(b, env.clone()),
-        crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b))
-            .unwrap()
-            .normalize_whnf_noenv(),
-    )
-}
-- 
cgit v1.2.3