mirror of
https://github.com/KevinMidboe/linguist.git
synced 2026-01-21 08:45:32 +00:00
Adds samples for the clean programming language
This commit is contained in:
99
samples/Clean/sem.icl
Normal file
99
samples/Clean/sem.icl
Normal file
@@ -0,0 +1,99 @@
|
||||
module monadicSemantics
|
||||
|
||||
import StdEnv, StdGeneric, GenMap, GenHylo
|
||||
|
||||
/* For fun I implemented the recursive datastructre Exp and Stm as fixpoints
|
||||
This helps us define recursive functions on them (only a little bit though)
|
||||
However deriving gMap for Fix did not works out of the box
|
||||
I had to remove some uniqueness typing in GenMap and GenHylo */
|
||||
:: Op = Plus | Minus | Times | Rem | Equal | LessThan
|
||||
:: Var :== String
|
||||
|
||||
:: ExpP a = Int Int | Var Var | Op Op a a
|
||||
:: Exp :== Fix ExpP
|
||||
|
||||
:: StmP a = Assign Var Exp | If Exp a a | While Exp a | Seq a a | Cont
|
||||
:: Stm :== Fix StmP
|
||||
|
||||
derive gMap ExpP, StmP, Fix
|
||||
|
||||
// Environment. Semantics is basically Env -> Env
|
||||
:: Env :== Var -> Int
|
||||
:: Sem :== Env -> (Int, Env)
|
||||
empty = \v . 0
|
||||
|
||||
// return
|
||||
rtn :: Int -> Sem
|
||||
rtn i = \e. (i, e)
|
||||
|
||||
// the usual bind
|
||||
(>>=) infixl 1 :: Sem (Int->Sem) -> Sem
|
||||
(>>=) x y = \e. (\(i,e2).y i e2) (x e)
|
||||
(>>|) infixl 1 :: Sem Sem -> Sem
|
||||
(>>|) x y = x >>= \_. y
|
||||
|
||||
// read variable from environment
|
||||
read :: Var -> Sem
|
||||
read v = \e. (e v, e)
|
||||
|
||||
// assign value to give variable in environment
|
||||
write :: Var Int -> Sem
|
||||
write v i = \e. (i, \w. if (w==v) i (e w))
|
||||
|
||||
// semantics
|
||||
class sem a :: a -> Sem
|
||||
|
||||
operator :: Op -> Int -> Int -> Int
|
||||
operator Plus = (+)
|
||||
operator Minus = (-)
|
||||
operator Times = (*)
|
||||
operator Rem = rem
|
||||
operator Equal = \x y . if (x==y) 1 0
|
||||
operator LessThan = \x y . if (x< y) 1 0
|
||||
|
||||
// semantics of expressions
|
||||
instance sem Exp where
|
||||
sem x = cata phi x where
|
||||
phi (Int n) = rtn n
|
||||
phi (Var v) = read v
|
||||
phi (Op op x y) = x >>= \v1. y >>= return o (operator op v1)
|
||||
|
||||
// semantics of statments
|
||||
// NOTE: while will always return 0, as it might not even be executed
|
||||
instance sem Stm where
|
||||
sem x = cata phi x where
|
||||
phi (Assign v e) = sem e >>= write v
|
||||
phi (If e s1 s2) = sem e >>= \b . if (b<>0) s1 s2
|
||||
phi stm=:(While e s) = sem e >>= \b . if (b<>0) (s >>| phi stm) (phi Cont)
|
||||
phi (Seq s1 s2) = s1 >>| s2 // Here the cata *finally* pays off :D
|
||||
phi Cont = rtn 0
|
||||
|
||||
// convenience functions
|
||||
int = In o Int
|
||||
var = In o Var
|
||||
op o = In o2 (Op o)
|
||||
assign = In o2 Assign
|
||||
ifte e = In o2 (If e)
|
||||
while = In o2 While
|
||||
seq = In o2 Seq
|
||||
cont = In Cont
|
||||
|
||||
// test case, also testing the new operator <
|
||||
pEuclides =
|
||||
while (op LessThan (int 0) (var "b"))(
|
||||
seq (assign "r" (op Rem (var "a") (var "b")))
|
||||
(seq (assign "a" (var "b"))
|
||||
( (assign "b" (var "r")))
|
||||
)
|
||||
)
|
||||
|
||||
Start = fst (program start) where
|
||||
program = sem pEuclides >>| read "a"
|
||||
start "a" = 9
|
||||
start "b" = 12
|
||||
start _ = 0
|
||||
|
||||
// Helper
|
||||
(o2) infixr 9
|
||||
(o2) f g x :== f o (g x)
|
||||
|
||||
Reference in New Issue
Block a user