{-# LANGUAGE GADTs, PolyKinds, TypeOperators, TemplateHaskell,
DataKinds, TypeFamilies, UndecidableInstances,
FlexibleContexts, RankNTypes, ScopedTypeVariables #-}
module Part5 where
import Prelude ( Bool(..), undefined, return )
import GHC.TypeLits ( type (-) )
import Data.Singletons
import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Type.Equality
$(singletons [d|
data Nat :: * where
Zero :: Nat
Succ :: Nat -> Nat
(+) :: Nat -> Nat -> Nat
Zero + m = m
Succ n + m = Succ (n + m)
data Ty :: * where
Bool :: Ty
Nat :: Ty
|])
infixl 6 +
type family U n where
U 0 = Zero
U n = Succ (U (n-1))
type family El (ty :: Ty) :: * where
El 'Bool = Bool
El 'Nat = Nat
data Expr :: Ty -> * where
Val :: El t -> Expr t
Plus :: Expr 'Nat -> Expr 'Nat -> Expr 'Nat
If :: Expr 'Bool -> Expr t -> Expr t -> Expr t
eval :: Expr t -> El t
eval (Val n) = n
eval (e1 `Plus` e2) = eval e1 + eval e2
eval (If e0 e1 e2) = if eval e0 then eval e1 else eval e2
type Rel i = i -> i -> *
data List (x :: Rel i) :: Rel i where
Nil :: List x i i
(:::) :: x i j -> List x j k -> List x i k
infixr 5 :::
(++) :: List x i j -> List x j k -> List x i k
Nil ++ ys = ys
(x ::: xs) ++ ys = x ::: (xs ++ ys)
infixr 5 ++
type SC = [Ty]
data Elt :: Rel SC where
E :: El t -> Elt (t ': ts) ts
type Stk i = List Elt i '[]
$(genDefunSymbols [ ''Stk, ''El ])
$(return [])
-- a b ~ c d ===> (a ~ c, b ~ d)
type Pi = Sing
-- data Sg (s :: *) (t :: s -> *) :: * where ...
data Sg (s :: *) (t :: TyFun s * -> *) :: * where
(:&) :: -- forall (s :: *) (t :: TyFun s * -> *) (fst :: s).
Pi (fst :: s) -> t @@ fst -> Sg s t
data Inst :: Rel (Sg SC StkSym0) where
PUSH :: forall (t :: Ty) (st :: Sing t) (ts :: [Ty]) (sts :: Sing ts)
(v :: El t) (vs :: Stk ts).
Sing v -> Inst (sts :& vs) ((st `SCons` sts) :& (E v ::: vs))
ADD :: Inst (('SNat `SCons` 'SNat `SCons` ts) :& (E y ::: E x ::: vs))
(('SNat `SCons` ts) :& (E (x :+ y) ::: vs))
IFPOP :: List Inst (sts :& vs) (sts' :& vst)
-> List Inst (sts :& vs) (sts' :& vsf)
-> Inst (('SBool `SCons` sts) :& (E b ::: vs))
(sts' :& If b vst vsf)
fact :: forall (ty :: Ty) (sc :: SC) (b :: Bool) (t :: El ty) (f :: El ty) (s :: Stk sc).
Sing b -> Sing t -> Sing f
-> (E (If b t f) ::: s) :~: (If b (E t ::: s) (E f ::: s))
fact = undefined
{-
fact STrue = Refl
fact SFalse = Refl
compile :: forall (t :: Ty) (st :: Sing t) (e :: Expr t) (ts :: [Ty]) (sts :: Sing ts)
(vs :: Stk ts).
Sing e -> List Inst (sts :& vs) ((st `SCons` sts) :& (E (Eval e) ::: vs))
compile (SVal y) = PUSH y ::: Nil
compile (e1 `SPlus` e2) = compile e1 ++ compile e2 ++ ADD ::: Nil
compile (SIf e0 e1 e2) = case fact e0 e1 e2 of
Refl -> compile e0 ++ IFPOP (compile e1) (compile e2) ::: Nil
-}
The following loops: