--- /dev/null
+module dsl
+
+import StdEnv
+
+import Data.Func => qualified app
+import Data.Functor
+import Data.Either
+import Data.GenEq
+import Data.Functor.Identity
+import Control.Applicative
+import Control.Monad => qualified join
+import Text
+
+import Text.Parsers.Simple.Core
+
+class Symantics v where
+ int :: Int -> v Int
+ bool :: Bool -> v Bool
+ lam :: ((v a) -> v b) -> v (a -> b)
+ app :: (v (a -> b)) (v a) -> v b
+ Fix :: ((v a) -> (v a)) -> v a
+ add :: (v a) (v a) -> v a | + a
+ mul :: (v a) (v a) -> v a | * a
+ leq :: (v a) (v a) -> v Bool | Ord a
+ If :: (v Bool) (v a) (v a) -> v a
+
+//Run the object
+:: Run a = Run a
+runRun (Run a) = a
+instance Functor Run where fmap f a = Run $ f $ runRun a
+instance pure Run where pure a = Run a
+instance <*> Run where <*> a b = Run $ runRun a $ runRun b
+instance Symantics Run where
+ int a = pure a
+ bool a = pure a
+ lam f = pure $ runRun o f o Run
+ app f a = f <*> a
+ Fix f = pure $ let x = runRun $ f $ pure x in x
+ add a b = (+) <$> a <*> b
+ mul a b = (*) <$> a <*> b
+ leq a b = (<=) <$> a <*> b
+ If i t e = if` <$> i <*> t <*> e
+
+//Length of the object
+:: Length a = Length Int
+runLength (Length i) = i
+(+.) infixl 6
+(+.) (Length a) (Length b) = Length $ a + b
+instance one (Length a) where one = Length 1
+instance zero (Length a) where zero = Length 0
+instance Symantics Length where
+ int _ = one
+ bool _ = one
+ lam f = f zero +. one
+ app f a = f +. a +. one
+ Fix f = f zero +. one
+ add a b = a +. b +. one
+ mul a b = a +. b +. one
+ leq a b = a +. b +. one
+ If i t e = i +. t +. e +. one
+
+//Print the object
+:: Print a = Print (Int [String] -> [String])
+runPrint (Print a) = a
+print a = concat $ runPrint a 0 []
+var i = "v" +++ toString i
+show a = Print \_ c->[toString a:c]
+binop op (Print a) (Print b) = Print \i c->["(":a i [op: b i [")":c]]]
+instance Symantics Print where
+ int a = show a
+ bool a = show a
+ lam f = Print \i c->["(\\", var i, ".":runPrint (f $ show $ var i) (i+1) [")":c]]
+ app f a = Print \i c->["(":runPrint f i [" ":runPrint a i [")":c]]]
+ Fix f = Print \i c->["fix (\\","self.":runPrint (f $ show "self") (i+1) [")":c]]
+ add a b = binop "+" a b
+ mul a b = binop "*" a b
+ leq a b = binop "<=" a b
+ If p t e = Print \i c->["if ":runPrint p i [" then ":runPrint t i [" else ":runPrint e i c]]]
+
+//Parsing
+:: Token = IntToken Int | BoolToken Bool | BrackOpenToken | BrackCloseToken | LeqToken | AddToken | MulToken | IfToken
+derive gEq Token
+instance == Token where == a b = a === b
+
+lex :: [Char] -> Either [String] [Token]
+lex [] = Right []
+lex [')':cs] = clex cs BrackCloseToken
+lex ['(':cs] = clex cs BrackOpenToken
+lex ['<=':cs] = clex cs LeqToken
+lex ['+':cs] = clex cs AddToken
+lex ['*':cs] = clex cs MulToken
+lex ['True':cs] = clex cs $ BoolToken True
+lex ['False':cs] = clex cs $ BoolToken False
+lex ['-',c:cs]
+ | isDigit c = lex [c:cs] >>= \v->case v of
+ [IntToken i:rest] = Right [IntToken (~i):rest]
+ x = pure x
+lex [c:cs]
+ | isSpace c = lex cs
+ | isDigit c
+ # (d, cs) = span isDigit [c:cs]
+ = clex cs $ IntToken $ toInt $ toString d
+ = Left ["Unexpected: " +++ toString c +++ " ord: " +++ toString (toInt c)]
+
+clex :: [Char] Token -> Either [String] [Token]
+clex cs t = (\ts->[t:ts]) <$> lex cs
+
+class parseSym a where
+ parseSym :: Parser Token (v a) | Symantics v
+instance parseSym Int where
+ parseSym
+ = flip pChainl1 (add <$ pToken AddToken)
+ $ flip pChainl1 (mul <$ pToken MulToken)
+ $ pToken BrackOpenToken *> parseSym <* pToken BrackCloseToken
+ <|> If <$ pToken IfToken <*> parseSym <*> parseSym <*> parseSym
+ <|> int <$> pInt
+ where
+ pInt = pSatisfy (\t->t=:(IntToken _)) >>= \(IntToken i)->pure i
+instance parseSym Bool where
+ parseSym
+ = leq <$> parseSymInt <* pToken LeqToken <*> parseSymInt
+ <|> If <$ pToken IfToken <*> parseSym <*> parseSym <*> parseSym
+ <|> pToken BrackOpenToken *> parseSym <* pToken BrackCloseToken
+ <|> bool <$> pBool
+ where
+ pBool = pSatisfy (\t->t=:(BoolToken _)) >>= \(BoolToken b)->pure b
+
+ parseSymInt :: Parser Token (v Int) | Symantics v
+ parseSymInt = parseSym
+
+Start = print <$> exp
+where
+ exp :: Either [String] (v Bool) | Symantics v
+ exp = lex (fromString inp) >>= parse parseSym
+
+ inp = "1+2*3 <= 42*42"
+//Start =
+// [ toString $ runRun fourtytwo
+// , print fourtytwo
+// , toString $ runRun true
+// , print true
+// , toString $ runRun powfix33
+// , print powfix33
+// , toString $ runRun factfix5
+// , print factfix5
+// ]
+
+fourtytwo :: v Int | Symantics v
+fourtytwo = add (int 38) (int 4)
+
+true :: v Bool | Symantics v
+true = app (lam (\x->x)) (bool True)
+
+powfix = lam \x->Fix \self->lam \n->
+ If (leq n (int 0)) (int 1)
+ (mul x (app self (add n (int -1))))
+
+powfix33 = app (app powfix (int 3)) (int 3)
+
+factfix = Fix \self->lam \n->
+ If (leq n (int 0)) (int 1)
+ (mul n (app self (add n (int -1))))
+
+factfix5 = app factfix (int 5)
repositories / clean-tests.git / blobdiff