dunhamsteve · September 6, 2022 13:37 · Apr 13, 2022 · Apr 13, 2022 · Mar 13, 2022 · Mar 13, 2022
diff --git a/DTComp2.idr b/DTComp2.idr
@@ -43,7 +43,6 @@ excludedMiddle b with (eval b)
     _ | True = Left Refl
     _ | False = Right Refl
 
-partial
 correct : (e : Exp t) -> (s : Stack ts) -> exec (compile e) s = eval e |> s
 correct (Val x) s = Refl
 correct (Add x y) s = 

diff --git a/DTComp2.idr b/DTComp2.idr
@@ -0,0 +1,59 @@
+-- https://www.cs.nott.ac.uk/~psymp4/files/dependently-typed-compilers.pdf
+data Exp : Type -> Type where
+  Val : t -> Exp t
+  Add : Exp Nat -> Exp Nat -> Exp Nat
+  If  : Eq t => Exp Bool -> Exp t -> Exp t -> Exp t
+
+eval : Exp t -> t
+eval (Val x) = x
+eval (Add x y) = eval x + eval y
+eval (If x y z) = if eval x then eval y else eval z
+
+data Stack : List Type -> Type where
+  Eps : Stack []
+  (|>) : t -> Stack ts -> Stack (t :: ts)
+
+infixr 7 |>
+
+data Code : List Type -> List Type -> Type where
+  PUSH  : t -> Code ts (t :: ts)
+  IF    : Code s s' -> Code s s' -> Code (Bool :: s) s'
+  ADD   : Code (Nat :: Nat :: s) (Nat :: s)
+  (+++) : Code s s' -> Code s' s'' -> Code s s'' 
+
+infixl 7 +++ 
+
+exec : Code s s' -> Stack s -> Stack s'
+exec (PUSH x) s          = x |> s
+exec (IF c1 c2) (b |> s) = if b then exec c1 s else exec c2 s
+exec ADD (m |> n |> s)   = (n + m) |> s
+exec (c1 +++ c2) s       = exec c2 (exec c1 s)
+
+compile : Exp t -> Code s (t :: s)
+compile (Val x)    = PUSH x
+compile (Add x y)  = compile x +++ compile y +++ ADD
+compile (If b x y) = compile b +++ IF (compile x) (compile y)
+
+distributeIf : (b : Bool ) -> (t : ty) -> (e : ty) -> (f : ty -> ty2) -> f (if b then t else e) = if b then f t else f e
+distributeIf False t e f = Refl
+distributeIf True t e f = Refl
+
+excludedMiddle : (b : _) -> Either (eval b === True) (eval b === False)
+excludedMiddle b with (eval b)
+    _ | True = Left Refl
+    _ | False = Right Refl
+
+partial
+correct : (e : Exp t) -> (s : Stack ts) -> exec (compile e) s = eval e |> s
+correct (Val x) s = Refl
+correct (Add x y) s = 
+  rewrite correct x s  in
+  rewrite correct y (eval x |> s) in
+  Refl
+correct (If b x y) s =
+    rewrite correct b s in
+    case excludedMiddle b of
+        Left prf  => rewrite prf in correct x s
+        Right prf => rewrite prf in correct y s
+
+
diff --git a/DTComp.idr b/DTComp.idr
@@ -1,4 +1,5 @@
 -- https://www.cs.nott.ac.uk/~psymp4/files/dependently-typed-compilers.pdf
+
 data Exp : Type -> Type where
   Val : t -> Exp t
   Add : Exp Nat -> Exp Nat -> Exp Nat
@@ -7,7 +8,7 @@ data Exp : Type -> Type where
 eval : Exp t -> t
 eval (Val x) = x
 eval (Add x y) = eval x + eval y
-eval (If x y z) = if eval x then eval y else eval z
+eval (If x y z) = ifThenElse (eval x) (eval y) (eval z)
 
 data Stack : List Type -> Type where
   Eps : Stack []
@@ -25,7 +26,7 @@ infixl 7 +++
 
 exec : Code s s' -> Stack s -> Stack s'
 exec (PUSH x) s          = x |> s
-exec (IF c1 c2) (b |> s) = if b then exec c1 s else exec c2 s
+exec (IF c1 c2) (b |> s) = ifThenElse b (exec c1 s) (exec c2 s)
 exec ADD (m |> n |> s)   = (n + m) |> s
 exec (c1 +++ c2) s       = exec c2 (exec c1 s)
 
@@ -34,11 +35,20 @@ compile (Val x)    = PUSH x
 compile (Add x y)  = compile x +++ compile y +++ ADD
 compile (If b x y) = compile b +++ IF (compile x) (compile y)
 
-correct : (e : Exp t) -> (s : Stack ts) -> exec (compile e) s = eval e |> s
+distributeIf : (f : t1 -> t2) -> (b : Bool) -> (x : t1) -> (y : t1) ->
+               f (ifThenElse b x y) = ifThenElse b (f x) (f y)
+distributeIf _ False x y = Refl
+distributeIf _ True  x y = Refl
+
+correct : (e : Exp t) -> (s : Stack ts) -> exec (compile e) s = eval e |> s 
 correct (Val x) s = Refl
 correct (Add x y) s = 
   rewrite correct x s  in
   rewrite correct y (eval x |> s) in
   Refl
 correct (If b x y) s =
-  rewrite correct b s in ?foo
+  rewrite correct b s in
+  rewrite distributeIf (|> s) (eval b) (eval x) (eval y) in
+  rewrite correct x s in
+  rewrite correct y s in
+  Refl
diff --git a/DTComp.idr b/DTComp.idr
@@ -0,0 +1,44 @@
+-- https://www.cs.nott.ac.uk/~psymp4/files/dependently-typed-compilers.pdf
+data Exp : Type -> Type where
+  Val : t -> Exp t
+  Add : Exp Nat -> Exp Nat -> Exp Nat
+  If  : Eq t => Exp Bool -> Exp t -> Exp t -> Exp t
+
+eval : Exp t -> t
+eval (Val x) = x
+eval (Add x y) = eval x + eval y
+eval (If x y z) = if eval x then eval y else eval z
+
+data Stack : List Type -> Type where
+  Eps : Stack []
+  (|>) : t -> Stack ts -> Stack (t :: ts)
+
+infixr 7 |>
+
+data Code : List Type -> List Type -> Type where
+  PUSH  : t -> Code ts (t :: ts)
+  IF    : Code s s' -> Code s s' -> Code (Bool :: s) s'
+  ADD   : Code (Nat :: Nat :: s) (Nat :: s)
+  (+++) : Code s s' -> Code s' s'' -> Code s s'' 
+
+infixl 7 +++ 
+
+exec : Code s s' -> Stack s -> Stack s'
+exec (PUSH x) s          = x |> s
+exec (IF c1 c2) (b |> s) = if b then exec c1 s else exec c2 s
+exec ADD (m |> n |> s)   = (n + m) |> s
+exec (c1 +++ c2) s       = exec c2 (exec c1 s)
+
+compile : Exp t -> Code s (t :: s)
+compile (Val x)    = PUSH x
+compile (Add x y)  = compile x +++ compile y +++ ADD
+compile (If b x y) = compile b +++ IF (compile x) (compile y)
+
+correct : (e : Exp t) -> (s : Stack ts) -> exec (compile e) s = eval e |> s
+correct (Val x) s = Refl
+correct (Add x y) s = 
+  rewrite correct x s  in
+  rewrite correct y (eval x |> s) in
+  Refl
+correct (If b x y) s =
+  rewrite correct b s in ?foo