0 | ||| The content of this module is based on the MSc Thesis
 1 | ||| Coinductive Formalization of SECD Machine in Agda
 2 | ||| by Adam Krupička
 3 |
 4 | module Language.IntrinsicTyping.STLCR
 5 |
 6 | import Data.List.Elem
 7 | import Language.IntrinsicTyping.SECD
 8 |
 9 | %default total
10 |
11 | public export
12 | data STLCR : List (Ty, Ty) -> List Ty -> Ty -> Type where
13 |   Var : Elem ty g -> STLCR r g ty
14 |   Lam : STLCR ((a, b) :: r) (a :: g) b -> STLCR r g (TyFun a b)
15 |   App : {a : _} -> STLCR r g (TyFun a b) -> STLCR r g a -> STLCR r g b
16 |   Rec : Elem (a,b) r -> STLCR r g (TyFun a b)
17 |   If  : STLCR r g TyBool -> (t, f : STLCR r g a) -> STLCR r g a
18 |   Eqb : {a : _} -> STLCR r g a -> STLCR r g a -> STLCR r g TyBool
19 |   Lit : Const ty -> STLCR r g ty
20 |   Add, Sub, Mul : (m, n : STLCR r g TyInt) -> STLCR r g TyInt
21 |
22 | public export
23 | fromInteger : Integer -> STLCR r g TyInt
24 | fromInteger n = Lit (AnInt (cast n))
25 |
26 | factorial : STLCR [] [] (TyFun TyInt TyInt)
27 | factorial
28 |   = Lam $ If (Eqb (Var Here) 0)
29 |       1
30 |       (Mul (Var Here) (App (Rec Here) (Sub (Var Here) 1)))
31 |
32 | public export
33 | compile : {ty : _} -> STLCR r g ty -> MkState s g r `Steps` MkState (ty :: s) g r
34 |
35 | public export
36 | compileT : {b : _} -> STLCR ((a, b) :: r) (a :: g) b ->
37 |            MkState [] (a :: g) ((a, b) :: r) `Steps` MkState [b] (a :: g) ((a, b) :: r)
38 |
39 | public export
40 | compileAcc : {ty : _} -> init `Stepz` MkState s g r -> STLCR r g ty -> init `Stepz` MkState (ty :: s) g r
41 | compileAcc acc (Var v) = acc :< LDA v
42 | compileAcc acc (Lam b) = acc :< LDF (compileT b)
43 | compileAcc acc (App f t) = compileAcc (compileAcc acc f) t :< APP
44 | compileAcc acc (Rec v) = acc :< LDR v
45 | compileAcc acc (If b t f) = compileAcc acc b :< BCH (compile t) (compile f)
46 | compileAcc acc (Eqb x y) = compileAcc (compileAcc acc y) x :< EQB
47 | compileAcc acc (Lit c) = acc :< LDC c
48 | compileAcc acc (Add m n) = compileAcc (compileAcc acc n) m :< ADD
49 | compileAcc acc (Sub m n) = compileAcc (compileAcc acc n) m :< SUB
50 | compileAcc acc (Mul m n) = compileAcc (compileAcc acc n) m :< MUL
51 |
52 | compile t = compileAcc [<] t <>> []
53 |
54 | compileT (Lam b) = [LDF (compileT b)]
55 | compileT (App f t) = compileAcc (compileAcc [<] f) t <>> [TAP]
56 | compileT (If b t f) = compileAcc [<] b <>> [BCH (compileT t) (compileT f)]
57 | compileT (Lit c) = [LDC c]
58 | compileT t = compileAcc [<] t <>> [RTN]
59 |
60 |
61 | testPLS : compile (Lam (Lam (Add (Var (There Here)) (Var Here))))
62 |       === [LDF [LDF [LDA Here, LDA (There Here), ADD, RTN]]]
63 | testPLS = Refl
64 |
65 | testFAC : run (compile (App STLCR.factorial 5)) 12 === Just 120
66 | testFAC = Refl
67 |