Skip to content

Instantly share code, notes, and snippets.

@tmcdonell

tmcdonell/temp_Down-convert-feldspar_2020739063107554536.hs

Created July 3, 2015 00:49
Show Gist options
  • Save tmcdonell/c5e07cf2348bfba03b10 to your computer and use it in GitHub Desktop.
Save tmcdonell/c5e07cf2348bfba03b10 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
temp_Down-convert-feldspar_2020739063107554536.hs
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- {-# OPTIONS_GHC -fdefer-type-errors #-}
{-# OPTIONS_GHC -fno-warn-unused-binds #-}
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
{-# OPTIONS_GHC -fno-warn-unused-matches #-}
module Ghostbuster where
import Prelude hiding ({- Int, -} Maybe(..), Bool(..))
data TypeDict a where
ExistentialDict :: TypeDict any
ArrowTyDict :: !(TypeDict a) -> !(TypeDict b) -> TypeDict (a -> b)
IntDict :: TypeDict Int
Tup2Dict :: !(TypeDict a) -> !(TypeDict b) -> TypeDict (Tup2 a b)
UnitDict :: TypeDict Unit
data TyEquality a b where
Refl :: TyEquality a a
data Typ arr where
Int :: Typ Int
Arr :: Typ v -> Typ w -> Typ (v -> w)
data Var env ans where
Zro :: Var (Tup2 e1 a) a
Suc :: Var e2 x -> Var (Tup2 e2 y) x
data Exp env ans where
Con :: Int -> Exp e1 Int
Add :: Exp e2 Int -> Exp e2 Int -> Exp e2 Int
Mul :: Exp e3 Int -> Exp e3 Int -> Exp e3 Int
Var :: Var e4 u -> Exp e4 u
Abs :: Typ r -> Exp (Tup2 e5 r) s -> Exp e5 (r -> s)
App :: Exp e6 (x -> y) -> Exp e6 x -> Exp e6 y
data Typ' where
Int' :: Typ'
Arr' :: !Typ' -> !Typ' -> Typ'
deriving Show
data SealedTyp where
SealedTyp :: TypeDict arr -> Typ arr -> SealedTyp
data Var' where
Zro' :: Var'
Suc' :: !Var' -> Var'
deriving Show
data SealedVar env where
SealedVar :: TypeDict ans -> Var env ans -> SealedVar env
data Exp' where
Con' :: !Int -> Exp'
Add' :: !Exp' -> !Exp' -> Exp'
Mul' :: !Exp' -> !Exp' -> Exp'
Var' :: !Var' -> Exp'
Abs' :: !Typ' -> !Exp' -> Exp'
App' :: !Exp' -> !Exp' -> Exp'
deriving Show
data SealedExp env where
SealedExp :: TypeDict ans -> Exp env ans -> SealedExp env
data ArrowTy a b where
-- data Int where
-- One :: Int
-- Two :: Int
-- Three :: Int
-- deriving Show
data Maybe a where
Just :: !a -> Maybe a
Nothing :: Maybe a
deriving Show
data Bool where
True :: Bool
False :: Bool
deriving Show
data Unit where
Unit :: Unit
deriving Show
data Tup2 a b where
Tup2 :: !a -> !b -> Tup2 a b
deriving Show
checkTEQ :: TypeDict t -> TypeDict u -> Maybe (TyEquality t u)
checkTEQ x y
= case x of
ArrowTyDict a1 b1 -> case y of
ArrowTyDict a2 b2 -> case checkTEQ a1 a2 of
Just Refl -> case checkTEQ b1 b2 of
Just Refl -> Just Refl
Nothing -> Nothing
Nothing -> Nothing
IntDict -> Nothing
UnitDict -> Nothing
Tup2Dict a2 b2 -> Nothing
IntDict -> case y of
ArrowTyDict a2 b2 -> Nothing
IntDict -> Just Refl
UnitDict -> Nothing
Tup2Dict a2 b2 -> Nothing
UnitDict -> case y of
ArrowTyDict a2 b2 -> Nothing
IntDict -> Nothing
UnitDict -> Just Refl
Tup2Dict a2 b2 -> Nothing
Tup2Dict a1 b1 -> case y of
ArrowTyDict a2 b2 -> Nothing
IntDict -> Nothing
UnitDict -> Nothing
Tup2Dict a2 b2 -> case checkTEQ a1 a2 of
Just Refl -> case checkTEQ b1 b2 of
Just Refl -> Just Refl
Nothing -> Nothing
Nothing -> Nothing
downTyp :: forall arr . TypeDict arr -> Typ arr -> Typ'
downTyp !arr_dict !orig
= case orig of
Int -> Int'
Arr a b -> Arr'
(downTyp
(case arr_dict of
ArrowTyDict left right -> left
-- IntDict -> ExistentialDict
-- UnitDict -> ExistentialDict
-- Tup2Dict a b -> ExistentialDict)
)
a)
(downTyp
(case arr_dict of
ArrowTyDict left right -> right
-- IntDict -> ExistentialDict
-- UnitDict -> ExistentialDict
-- Tup2Dict a b -> ExistentialDict)
)
b)
downVar ::
forall env ans .
TypeDict env -> TypeDict ans -> Var env ans -> Var'
downVar !env_dict !ans_dict !orig
= case orig of
Zro -> Zro'
Suc a -> Suc'
(downVar
(case env_dict of
ExistentialDict -> ExistentialDict
Tup2Dict a b -> a
-- ArrowTyDict a b -> ExistentialDict
-- IntDict -> ExistentialDict
-- UnitDict -> ExistentialDict)
)
(let
x_dict :: TypeDict ans
x_dict = ans_dict
in x_dict)
a)
downExp ::
forall env ans .
TypeDict env -> TypeDict ans -> Exp env ans -> Exp'
downExp !env_dict !ans_dict !orig
= case orig of
Con a -> Con' a
Add a b -> Add'
(downExp
(let
e2_dict :: TypeDict env
e2_dict = env_dict
in e2_dict)
IntDict
a)
(downExp
(let
e2_dict :: TypeDict env
e2_dict = env_dict
in e2_dict)
IntDict
b)
Mul a b -> Mul'
(downExp
(let
e3_dict :: TypeDict env
e3_dict = env_dict
in e3_dict)
IntDict
a)
(downExp
(let
e3_dict :: TypeDict env
e3_dict = env_dict
in e3_dict)
IntDict
b)
Var a -> Var'
(downVar
(let
e4_dict :: TypeDict env
e4_dict = env_dict
in e4_dict)
(let
u_dict :: TypeDict ans
u_dict = ans_dict
in u_dict)
a)
Abs a b -> Abs'
(downTyp
(case ans_dict of
ExistentialDict -> ExistentialDict
ArrowTyDict left right -> left
-- IntDict -> ExistentialDict
-- UnitDict -> ExistentialDict
-- Tup2Dict a b -> ExistentialDict)
)
a)
(downExp
(let
e5_dict :: TypeDict env
e5_dict = env_dict
in
case ans_dict of
ExistentialDict -> ExistentialDict
-- ArrowTyDict left right -> left
-- IntDict -> ExistentialDict
-- UnitDict -> ExistentialDict
-- Tup2Dict a b -> ExistentialDict)
)
(case ans_dict of
ExistentialDict -> ExistentialDict
ArrowTyDict left right -> right
-- IntDict -> ExistentialDict
-- UnitDict -> ExistentialDict
-- Tup2Dict a b -> ExistentialDict)
)
b)
App a b -> App'
(downExp
(let
e6_dict :: TypeDict env
e6_dict = env_dict
in e6_dict)
ExistentialDict
a)
(downExp
(let
e6_dict :: TypeDict env
e6_dict = env_dict
in e6_dict)
ExistentialDict
b)
ghostbuster :: Exp'
-- ghostbuster = downExp UnitDict IntDict (Con Three)
ghostbuster = downExp UnitDict IntDict fib3
fib3 :: Exp Unit Int
fib3 = App
(Abs Int (App (Abs Int (Add (Var Zro) (Var (Suc Zro)))) (Con 1)))
(App
(Abs Int (App (Abs Int (Add (Var Zro) (Var (Suc Zro)))) (Con 0)))
(Con 1))
fib4 :: Exp Unit Int
fib4 = App
(Abs
Int
(App
(Abs Int (Add (Var Zro) (Var (Suc Zro))))
(App
(Abs Int (App (Abs Int (Add (Var Zro) (Var (Suc Zro)))) (Con 0)))
(Con 1))))
(App
(Abs Int (App (Abs Int (Add (Var Zro) (Var (Suc Zro)))) (Con 1)))
(App
(Abs Int (App (Abs Int (Add (Var Zro) (Var (Suc Zro)))) (Con 0)))
(Con 1)))
bin52 :: Exp Unit Int
bin52 =
App
(Abs
Int
(App
(Abs Int (Add (Var Zro) (Var (Suc Zro))))
(App
(Abs Int (App (Abs Int (Add (Var Zro) (Var (Suc Zro)))) (Con 1)))
(App
(Abs Int (App (Abs Int (Add (Var Zro) (Var (Suc Zro)))) (Con 1)))
(App
(Abs Int (App (Abs Int (Add (Var Zro) (Var (Suc Zro)))) (Con 1)))
(Con 1))))))
(App
(Abs
Int
(App
(Abs Int (Add (Var Zro) (Var (Suc Zro))))
(App
(Abs Int (App (Abs Int (Add (Var Zro) (Var (Suc Zro)))) (Con 1)))
(App
(Abs Int (App (Abs Int (Add (Var Zro) (Var (Suc Zro)))) (Con 1)))
(Con 1)))))
(App
(Abs
Int
(App
(Abs Int (Add (Var Zro) (Var (Suc Zro))))
(App
(Abs Int (App (Abs Int (Add (Var Zro) (Var (Suc Zro)))) (Con 1)))
(Con 1))))
(Con 1)))
main :: IO ()
main = print ghostbuster
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment