Imp.hs

{-# LANGUAGE DataKinds, GADTs, TypeOperators, TypeFamilies, UndecidableInstances, PartialTypeSignatures #-}

-- Nat

data Zero
data Succ n
data Nat n where
  Zero :: Nat Zero
  Succ :: Nat n -> Nat (Succ n)

infixl 7 *
infixl 6 +, -

type family (+) a b where
  Zero + n = n
  (Succ n) + m = Succ (n + m)

type family (-) a b where
  Zero - m = Zero
  n - Zero = n
  (Succ n) - (Succ m) = n - m

type family (*) a b where
  Zero * n = Zero
  (Succ n) * m = n * m + m

type family EqNat a b where
  EqNat Zero Zero = True
  EqNat (Succ n) (Succ m) = EqNat n m
  EqNat n m = False

type family EqLeq a b where
  EqLeq Zero n = True
  EqLeq (Succ n) (Succ m) = EqLeq n m
  EqLeq n m = False

type N0 = Zero
type N1 = Succ N0
type N2 = Succ N1
type N3 = Succ N2
type N4 = Succ N3
type N5 = Succ N4
type N6 = Succ N5
type N7 = Succ N6
type N8 = Succ N7
type N9 = Succ N8
type N16 = N4 * N4
type N21 = N3 * N7

n0 = Zero
n1 = Succ n0
n2 = Succ n1
n3 = Succ n2
n4 = Succ n3
n5 = Succ n4
n6 = Succ n5
n7 = Succ n6
n8 = Succ n7
n9 = Succ n8

-- State

data Def n
data Update s i n

data State s where
  Def :: Nat n -> State (Def n)
  Update :: State s -> Nat i -> Nat n -> State (Update s i n)

type family Fbool b t f where
  Fbool True t f = t
  Fbool False t f = f

type family Get s j where
  Get (State (Def n)) j = n
  Get (State (Update s' i n)) j = Fbool (EqNat i j) n (Get (State s') j)

-- Aexp

data ANum n
data AVar n
data APlus a1 a2
data AMinus a1 a2
data AMult a1 a2

infix 7 :*
infix 6 :+, :-

type (:+) = APlus
type (:-) = AMinus
type (:*) = AMult

data Aexp a where
  ANum :: Nat n -> Aexp (ANum n)
  AVar :: Nat i -> Aexp (AVar i)
  APlus :: Aexp a1 -> Aexp a2 -> Aexp (a1 :+ a2)
  AMinus :: Aexp a1 -> Aexp a2 -> Aexp (a1 :- a2)
  AMult :: Aexp a1 -> Aexp a2 -> Aexp (a1 :* a2)

data AEval a st e where
  AENum :: Aexp (ANum n) -> st -> AEval (ANum n) st n
  AEVar :: Aexp (AVar i) -> st -> AEval (AVar i) st (Get st i)
  AEPlus :: AEval a0 st n0 -> AEval a1 st n1 -> AEval (a0 :+ a1) st (n0 + n1)
  AEMinus :: AEval a0 st n0 -> AEval a1 st n1 -> AEval (a0 :- a1) st (n0 - n1)
  AEMult :: AEval a0 st n0 -> AEval a1 st n1 -> AEval (a0 :* a1) st (n0 * n1)

aexpExample1 :: Nat n -> AEval (ANum n) (State (Def Zero)) n
aexpExample1 n = AENum (ANum n) (Def Zero)

aexpExample2 :: AEval (AMult (ANum N2) (ANum N3)) (State (Def N0)) N6
aexpExample2 = AEMult l1 l2 where
  l1 :: AEval (ANum N2) (State (Def N0)) N2
  l1 = AENum (ANum n2) (Def n0)
  
  l2 :: AEval (ANum N3) (State (Def N0)) N3
  l2 = AENum (ANum n3) (Def n0)

aexpExample3 :: AEval (APlus (APlus (AVar N0) (ANum N5)) (APlus (ANum N7) (ANum N9))) (State (Def N0)) N21
aexpExample3 = AEPlus l1 l2 where
  l1 :: AEval (APlus (AVar N0) (ANum N5)) (State (Def N0)) N5
  l1 = AEPlus l3 l4
  
  l3 :: AEval (AVar N0) (State (Def N0)) N0
  l3 = AEVar (AVar n0) (Def n0)

  l4 :: AEval (ANum N5) (State (Def N0)) N5
  l4 = AENum (ANum n5) (Def n0)

  l2 :: AEval (APlus (ANum N7) (ANum N9)) (State (Def N0)) N16
  l2 = AEPlus (AENum (ANum n7) (Def n0)) (AENum (ANum n9) (Def n0))

-- Bexp

data BTrue
data BFalse
data BEq a0 a1
data BLeq a0 a1
data BNot b
data BAnd b0 b1
data BOr b0 b1

type (:==) = BEq
type (:/=) b0 b1 = BNot (b0 :== b1)

-- operators
type family (&&) a b where
  BTrue && b = b
  BFalse && b = BFalse

type family (||) a b where
  BTrue || b = BTrue
  BFalse || b = b

data Bexp b where
  BTrue :: Bexp BTrue
  BFalse :: Bexp BFalse
  BEq :: Bexp b0 -> Bexp b1 -> Bexp (BEq b0 b1)
  BLeq :: Bexp b0 -> Bexp b1 -> Bexp (BLeq b0 b1)
  BNot :: Bexp b -> Bexp (BNot b)
  BAnd :: Bexp b0 -> Bexp b1 -> Bexp (BAnd b0 b1)
  BOr :: Bexp b0 -> Bexp b1 -> Bexp (BOr b0 b1)

type family Bbool b where
  Bbool True = BTrue
  Bbool False = BFalse

data BEval b st e where
  BETrue :: Bexp BTrue -> st -> BEval BTrue st BTrue
  BEFalse :: Bexp BFalse -> st -> BEval BFalse st BFalse
  BEEq :: AEval a0 st n0 -> AEval a1 st n1 -> BEval (BEq a0 a1) st (Bbool (EqNat n0 n1))
  BELeq :: AEval a0 st n0 -> AEval a1 st n1 -> BEval (BLeq a0 a1) st (Bbool (EqLeq n0 n1))
  BENot_T :: BEval b st BTrue -> BEval (BNot b) st BFalse
  BENot_F :: BEval b st BFalse -> BEval (BNot b) st BTrue
  BEAnd :: BEval b0 st t0 -> BEval b1 st t1 -> BEval (BAnd b0 b1) st (t0 && t1)
  BEOr :: BEval b0 st t0 -> BEval b1 st t1 -> BEval (BOr b0 b1) st (t0 || t1)

-- Com

data CSkip
data (:&) c0 c1
data (:=) x n
data CIf b c0 c1
data CWhile b c

infix 1 :&
infix 3 :=

data Com c where
  CSkip :: Com CSkip
  CSeq :: Com c0 -> Com c1 -> Com (c0 :& c1)
  CSubst :: AVar i -> Aexp a -> Com (i := a)
  CIf :: Bexp b -> Com c0 -> Com c1 -> Com (CIf b c0 c1)
  CWhile :: Bexp b -> Com c -> Com (CWhile b c)

data CEval c st r where
  CESkip :: CEval CSkip st st
  CESeq :: CEval c0 st st'' -> CEval c1 st'' st' -> CEval (c0 :& c1) st st'
  CESubst :: AEval a (State st) m -> CEval (i := a) (State st) (State (Update st i m))
  CEIf_T :: BEval b st BTrue -> CEval c0 st st' -> CEval (CIf b c0 c1) st st'
  CEIf_F :: BEval b st BFalse -> CEval c1 st st' -> CEval (CIf b c0 c1) st st'
  CEWhile_E :: BEval b st BFalse -> CEval (CWhile b c) st st
  CEWhile_L :: BEval b st BTrue -> CEval c st st'' -> CEval (CWhile b c) st'' st' -> CEval (CWhile b c) st st'

cexpExample1 :: CEval (N1 := ANum N0 :& CWhile (AVar N0 :/= ANum N0) (N1 := AVar N1 :+ AVar N0 :& N0 := AVar N0 :- ANum N1)) (State (Def N2)) (State (Update (Update (Update (Update (Update (Def N2) N1 N0) N1 N2) N0 N1) N1 N3) N0 N0))
cexpExample1 = CESeq c0 c1 where
  c0 :: CEval (N1 := ANum N0) (State (Def N2)) (State (Update (Def N2) N1 N0))
  c0 = CESubst a0 where
    a0 :: AEval (ANum N0) (State (Def N2)) N0
    a0 = AENum (ANum n0) (Def n2)

  s0 = Update (Def n2) n1 n0

  c1 :: CEval (CWhile (AVar N0 :/= ANum N0) (N1 := AVar N1 :+ AVar N0 :& N0 := AVar N0 :- ANum N1)) _ _
  c1 = CEWhile_L b0 c2 c3 where    
    b0 :: BEval (AVar N0 :/= ANum N0) (State (Update (Def N2) N1 N0)) BTrue
    b0 = BENot_F $ BEEq (AEVar (AVar n0) s0) (AENum (ANum n0) (Update (Def n2) n1 n0))

  s1 = Update s0 n1 n2

  c2 :: CEval (N1 := AVar N1 :+ AVar N0 :& N0 := AVar N0 :- ANum N1) _ _
  c2 = CESeq c4 c5 where
    c4 :: CEval (N1 := AVar N1 :+ AVar N0) _ _
    c4 = CESubst (AEPlus (AEVar (AVar n1) s0) (AEVar (AVar n0) s0))

    c5 :: CEval (N0 := AVar N0 :- ANum N1) _ _
    c5 = CESubst (AEMinus (AEVar (AVar n0) s1) (AENum (ANum n1) s1))

  s2 = Update s1 n0 n1
  s3 = Update s2 n1 n3

  c3 :: CEval (CWhile (AVar N0 :/= ANum N0) (N1 := AVar N1 :+ AVar N0 :& N0 := AVar N0 :- ANum N1)) _ _
  c3 = CEWhile_L b0 c6 c7 where
    b0 :: BEval (AVar N0 :/= ANum N0) _ BTrue
    b0 = BENot_F $ BEEq (AEVar (AVar n0) s2) (AENum (ANum n0) s2)

    c6 :: CEval (N1 := AVar N1 :+ AVar N0 :& N0 := AVar N0 :- ANum N1) _ _
    c6 = CESeq (CESubst (AEPlus (AEVar (AVar n1) s2) (AEVar (AVar n0) s2))) (CESubst (AEMinus (AEVar (AVar n0) s3) (AENum (ANum n1) s3)))

  s4 = Update s3 n0 n0

  c7 :: CEval (CWhile (AVar N0 :/= ANum N0) (N1 := AVar N1 :+ AVar N0 :& N0 := AVar N0 :- ANum N1)) _ _
  c7 = CEWhile_E b0 where
    b0 :: BEval (AVar N0 :/= ANum N0) _ BFalse
    b0 = BENot_T $ BEEq (AEVar (AVar n0) s4) (AENum (ANum n0) s4)

main = putStrLn "QED."