blob: 79c4428d215e8477473e737a4d95c325b9b49ccd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module Arith.NonBase where
import Data.Kind
import Data.Type.Equality
-- import NonBaseTH
data Typ t where
TInt :: Typ Int
TBool :: Typ Bool
TPair :: Typ a -> Typ b -> Typ (a, b)
TFun :: Typ a -> Typ b -> Typ (a -> b)
deriving instance Show (Typ t)
instance TestEquality Typ where
testEquality TInt TInt = Just Refl
testEquality TBool TBool = Just Refl
testEquality (TPair a b) (TPair a' b')
| Just Refl <- testEquality a a'
, Just Refl <- testEquality b b'
= Just Refl
testEquality (TFun a b) (TFun a' b')
| Just Refl <- testEquality a a'
, Just Refl <- testEquality b b'
= Just Refl
testEquality _ _ = Nothing
data PrimOp a b where
POAddI :: PrimOp (Int, Int) Int
POMulI :: PrimOp (Int, Int) Int
POEqI :: PrimOp (Int, Int) Bool
deriving instance Show (PrimOp a b)
type Arith :: Type -> Type
data Arith t where
A_Var :: Typ t -> String -> Arith t
A_Let :: String -> Typ a -> Arith a -> Arith b -> Arith b
A_Prim :: PrimOp a b -> Arith a -> Arith b
A_Pair :: Arith a -> Arith b -> Arith (a, b)
A_If :: Arith Bool -> Arith a -> Arith a -> Arith a
A_Mono :: Arith Bool -> Arith Bool
|
