stack-machine/StackMachine3.idr at main · maxbaroi/stack-machine · GitHub

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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
module StackMachine3

import Data.Nat

import Data.List

import Data.Maybe

%hide Prelude.Bool

data Bool = True | False

not : Bool -> Bool
not True = False
not False = True

(&&) : Bool -> Bool -> Bool
True && y = y
False && _ = False

(||) : Bool -> Bool -> Bool
True || _ = True
False || y = y

eqb : Bool -> Bool -> Bool
eqb True True = True
eqb True False = False
eqb False True = False
eqb False False = True

eqn : Nat -> Nat -> Bool
eqn 0 0 = True
eqn 0 (S _) = False
eqn (S _) 0 = False
eqn (S j) (S k) = eqn j k

lte : Nat -> Nat -> Bool
lte 0 _ = True
lte (S _) 0 = False
lte (S j) (S k) = lte j k

eif : Bool -> a -> a -> a
eif True a _ = a
eif False _ b = b

data SType = SNat | SBool

data Uniop : SType -> SType -> Type where
  Not : Uniop SBool SBool
  Succ : Uniop SNat SNat

data Binop : SType -> SType -> SType -> Type where
  Plus : Binop SNat SNat SNat
  Mult : Binop SNat SNat SNat
  And : Binop SBool SBool SBool
  Or : Binop SBool SBool SBool
  LTE : Binop SNat SNat SBool
  Equals : (t : SType) -> Binop t t SBool

data Triop : SType -> SType -> SType -> SType -> Type where
  If : (t : SType) -> Triop SBool t t t

--Type saefty of the expression language is forced by the ambient type setting
data Exp : SType -> Type where
  ENConst : Nat -> Exp SNat
  EBConst : Bool -> Exp SBool
  EUniop : (t , u  : SType) -> Uniop t u -> Exp t -> Exp u
  EBiop : (s , t , u  : SType) -> Binop s t u -> Exp s -> Exp t -> Exp u
  ETriniop : (r, s, t , u  : SType) -> Triop r s t u
    -> Exp r -> Exp s -> Exp t -> Exp u

typeDenote : SType -> Type
typeDenote SNat = Nat
typeDenote SBool = Bool

uniDenote : Uniop t u -> typeDenote t -> typeDenote u
uniDenote Not = not
uniDenote Succ = S

binDenote : Binop s t u -> typeDenote s ->  typeDenote t -> typeDenote u
binDenote Plus = (+)
binDenote Mult = (*)
binDenote And = (&&)
binDenote Or = (||)
binDenote LTE = lte
binDenote (Equals SNat) = eqn
binDenote (Equals SBool) = eqb

--The "right" eif will be selected
triDenote : Triop r s t u -> typeDenote r -> typeDenote s ->  typeDenote t
  -> typeDenote u
triDenote (If _) = eif

expDenote : Exp a -> typeDenote a
expDenote (ENConst k) = k
expDenote (EBConst b) = b
expDenote (EUniop _ _ f e) = (uniDenote f) (expDenote e)
expDenote (EBiop _ _ _ f e1 e2) = (binDenote f) (expDenote e1) (expDenote e2)
expDenote (ETriniop _ _ _ _ f e1 e2 e3) =
  (triDenote f) (expDenote e1) (expDenote e2) (expDenote e3)

TypeStack = List SType
data ValueStack : TypeStack -> Type where
  Empty : ValueStack []
  Cons : {t : SType} -> typeDenote t -> ValueStack vs -> ValueStack (t :: vs)

data Instr : TypeStack -> TypeStack -> Type where
  INConst : (n : Nat) -> (s : TypeStack) -> Instr s (SNat :: s)
  IBConst : (b : Bool) -> (s : TypeStack) -> Instr s (SBool :: s)