Implement a basic Calculus of Constructions VM / interpreter, to test a linear induction combinator

misc/exe/Coinche.hs

+{-# LANGUAGE FlexibleContexts, LambdaCase #-}
+module Main where
+
+import Definitive
+import Algebra.Monad.Concatenative
+import System.Random.Shuffle
+
+data Hauteur = H7 | H8 | H9 | HValet | HDame | HRoi | H10 | HAs
+             deriving (Eq,Ord,Show,Enum)
+data Couleur = Coeur | Carreau | Pique | Trefle
+             deriving (Eq,Ord,Show,Enum)
+data Carte = Carte Hauteur Couleur
+instance Show Carte where
+  show (Carte h c) = showH h +":"+ showC c
+    where showH H7 = "7" ; showH H8 = "8" ; showH H9 = "9" ; showH H10 = "10"
+          showH HValet = "J"; showH HDame = "Q"; showH HRoi = "K" ; showH HAs = "A"
+          showC Coeur = "co"; showC Carreau = "ca" ; showC Pique = "pi";
+          showC Trefle = "tr"
+
+data CoincheState = CoincheState {
+  _cards :: ([Carte],[Carte],[Carte],[Carte]),
+  _halt :: Bool
+  }
+
+cards :: Lens' CoincheState ([Carte],[Carte],[Carte],[Carte])
+cards = lens _cards (\x y -> x { _cards = y })
+halt :: Lens' CoincheState Bool
+halt = lens _halt (\x y -> x { _halt = y })
+
+nomsHauteurs = c'map $ fromAList [(n,h)
+                                 | (ns,h) <- [(["7","sept","seven"],H7),
+                                              (["8"],H8),
+                                              (["9"],H9),
+                                              (["10"],H10),
+                                              (["V","valet","J"],HValet),
+                                              (["D","Q","dame"],HDame),
+                                              (["R","roi","K"],HRoi),
+                                              (["A","as"],HAs)]
+                                 , n <- ns]
+nomsCouleurs = c'map $ fromAList [(n,h)
+                                 | (ns,h) <- [(["carreau"],Carreau),
+                                              (["coeur"],Coeur),
+                                              (["trefle"],Trefle),
+                                              (["pique"],Pique)]
+                                 , n <- ns]
+
+
+data Builtin = Quit | Hands | Deal | Show | MkCarte
+             deriving Show
+runBuiltin Quit = runExtraState (halt =- True)
+runBuiltin Hands = do
+  (p1,p2,p3,p4) <- runExtraState (getl cards)
+  for_ (zip [1..4] [p1,p2,p3,p4]) $ \(i,pi') -> lift $ do
+    putStrLn $ "Player "+show i+": "+intercalate " " (map show pi')
+runBuiltin Deal = do
+  cs <- lift $ shuffleM deck
+  let (h1,cs1) = splitAt 8 cs
+      (h2,cs2) = splitAt 8 cs1
+      (h3,h4)  = splitAt 8 cs2
+  runExtraState $ do cards =- (h1,h2,h3,h4)
+runBuiltin Show = do
+  st <- runStackState get
+  case st of
+    StackList l:_ -> do
+      lift $ putStrLn $ intercalate " " (map show l)
+      runStackState (modify tail)
+    StackExtra (Opaque c):_ -> do
+      lift $ putStrLn $ show c
+      runStackState (modify tail)
+    _ -> return ()
+runBuiltin MkCarte = runStackState $ modify $ \case
+  StackSymbol c:StackSymbol h:t | Just h' <- lookup h nomsHauteurs
+                                , Just c' <- lookup c nomsCouleurs -> StackExtra (Opaque (Carte h' c')):t
+  st -> st
+
+deck = [Carte h c | h <- [H7 .. HAs], c <- [Coeur .. Trefle]]
+
+main = do
+  str <- words <$> getContents
+  execS (foldr (\sym mr -> do
+                   execSymbol runBuiltin sym
+                   hasQuit <- runExtraState (getl halt)
+                   unless hasQuit mr
+               ) unit str^..concatT) (defaultState (fromAList [(x,StackBuiltin b)
+                                                              | (x,b) <- [("quit",Builtin_Extra Quit),("show",Builtin_Extra Show),("hands",Builtin_Extra Hands),("deal",Builtin_Extra Deal),("def",Builtin_Def),("pop",Builtin_Pop),("$",Builtin_DeRef),("exec",Builtin_Exec)]])
+                                       (CoincheState ([],[],[],[]) False))

misc/misc.cabal

@@ -15,12 +15,29 @@ build-type:          Simple
 extra-source-files:  ChangeLog.md
 cabal-version:       >=1.10
 
+library
+  exposed-modules: Algebra.Monad.Concatenative
+  default-extensions: RebindableSyntax
+  build-depends: base >=4.9 && <4.10,curly-core >=0.7 && <0.8,definitive-base >=2.6 && <2.7, definitive-parser
+  ghc-options: -Wincomplete-patterns -Wname-shadowing -Werror
+  hs-source-dirs: src
+  default-language: Haskell2010
+                     
 executable misc
   main-is:             Misc.hs
   default-extensions:  RebindableSyntax
   -- other-modules:       
   -- other-extensions:    
-  build-depends: base >=4.9 && <4.10,curly-core >=0.7 && <0.8,definitive-base >=2.6 && <2.7
+  build-depends: base >=4.9 && <4.10,curly-core >=0.7 && <0.8,definitive-base >=2.6 && <2.7, definitive-parser, misc
+  ghc-options: -Wincomplete-patterns -Wname-shadowing -Werror
+  hs-source-dirs:      exe
+  default-language:    Haskell2010
+executable coinche
+  main-is:             Coinche.hs
+  default-extensions:  RebindableSyntax
+  -- other-modules:       
+  -- other-extensions:    
+  build-depends: base >=4.9 && <4.10,definitive-base >=2.6 && <2.7, definitive-parser, misc, random, random-shuffle
   ghc-options: -Wincomplete-patterns -Wname-shadowing -Werror
   hs-source-dirs:      exe
   default-language:    Haskell2010

misc/src/Algebra/Monad/Concatenative.hs

+{-# LANGUAGE FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, GeneralizedNewtypeDeriving #-}
+module Algebra.Monad.Concatenative(ConcatT,concatT,MonadStack(..),StackBuiltin(..),StackVal(..),StackState,defaultState,Opaque(..)) where
+
+import Definitive
+
+newtype Opaque a = Opaque a
+instance Show (Opaque a) where show _ = "#<opaque>"
+data StackBuiltin b = Builtin_ListBegin | Builtin_ListEnd
+                    | Builtin_Clear | Builtin_Pop | Builtin_Dup | Builtin_Swap | Builtin_SwapN
+                    | Builtin_If | Builtin_Each
+                    | Builtin_DeRef | Builtin_Def
+                    | Builtin_Exec
+                    | Builtin_Extra b
+                    deriving Show
+data StackVal s b a = StackBuiltin (StackBuiltin b)
+                    | StackInt Int
+                    | StackSymbol s
+                    | StackList [StackVal s b a]
+                    | StackProg [s]
+                    | StackExtra (Opaque a)
+                    deriving Show
+
+data StackState st s b a = StackState {
+  _stack :: [StackVal s b a],
+  _progStack :: [s],
+  _depth :: Int,
+  _dict :: Map s (StackVal s b a),
+  _extraState :: st
+  }
+
+stack :: Lens' (StackState st s b a) [StackVal s b a]
+stack = lens _stack (\x y -> x { _stack = y })
+progStack :: Lens' (StackState st s b a) [s]
+progStack = lens _progStack (\x y -> x { _progStack = y })
+depth :: Lens' (StackState st s b a) Int
+depth = lens _depth (\x y -> x { _depth = y })
+dict :: Lens' (StackState st s b a) (Map s (StackVal s b a))
+dict = lens _dict (\x y -> x { _dict = y })
+extraState :: Lens st st' (StackState st s b a) (StackState st' s b a)
+extraState = lens _extraState (\x y -> x { _extraState = y })
+
+data AtomClass s = OpenBrace | CloseBrace | Quoted s | Other s
+class Ord s => StackSymbol s where atomClass :: s -> AtomClass s
+instance StackSymbol String where
+  atomClass "{" = OpenBrace
+  atomClass "}" = CloseBrace
+  atomClass ('\'':t) = Quoted t
+  atomClass x = Other x
+
+execSymbolImpl :: (StackSymbol s, MonadState (StackState st s b a) m) => (StackBuiltin b -> m ()) -> s -> m ()
+execSymbolImpl execBuiltin' atom = do
+  st <- get
+  case atomClass atom of
+    OpenBrace -> do depth =~ (+1) ; when (st^.depth > 0) (progStack =~ (atom:))
+    CloseBrace -> do
+      depth =~ subtract 1
+      if st^.depth == 1 then do
+        stack =~ (StackProg (reverse $ st^.progStack):)
+        progStack =- []
+        else progStack =~ (atom:)
+    Quoted a | st^.depth==0 -> stack =~ (StackSymbol a:)
+    _ -> case st^.depth of
+           0 -> case st^.dict.at atom of
+             Just v -> exec v
+             Nothing -> stack =~ (StackSymbol atom:)
+           _ -> progStack =~ (atom:)
+  where exec (StackBuiltin b) = execBuiltin' b
+        exec (StackProg p) = traverse_ (execSymbolImpl execBuiltin') p
+        exec x = stack =~ (x:)
+
+execBuiltin :: (StackSymbol s, MonadState (StackState st s b a) m) => (b -> m ()) -> StackBuiltin b -> m ()
+execBuiltin runExtra = go
+  where 
+    go Builtin_Def = get >>= \st -> case st^.stack of
+      (val:StackSymbol var:tl) -> do dict =~ insert var val ; stack =- tl
+      _ -> return ()
+    go Builtin_ListBegin = stack =~ (StackBuiltin Builtin_ListBegin:)
+    go Builtin_ListEnd = stack =~ \st -> let (h,_:t) = break (\x -> case x of
+                                                                               StackBuiltin Builtin_ListBegin -> True
+                                                                               _ -> False) st
+                                                  in StackList (reverse h):t
+    go Builtin_Clear = stack =- []
+    go Builtin_Pop = stack =~ drop 1
+    go Builtin_Swap = stack =~ \st -> case st of x:y:t -> y:x:t ; _ -> st
+    go Builtin_SwapN = stack =~ \st -> case st of
+      StackInt n:st' ->
+        case splitAt (n+1) st' of
+          (x:tx,y:ty) -> y:tx+(x:ty)
+          _ -> st
+      _ -> st
+    go Builtin_Dup = stack =~ \st -> case st of x:t -> x:x:t ; _ -> st
+    go Builtin_Each = do
+      st <- get
+      case st^.stack of
+        e:StackList l:t -> do
+          stack =- t
+          for_ l $ \x -> do stack =~ (e:) . (x:) ; go Builtin_Exec
+        _ -> return ()
+    go Builtin_DeRef = do
+      st <- get
+      stack =~ \x -> case x of
+                       StackSymbol v:t -> maybe (StackSymbol v) id (st^.dict.at v):t
+                       _ -> x
+    go Builtin_Exec = do
+      st <- get
+      case st^.stack of
+        StackProg p:t -> do stack =- t ; traverse_ (execSymbolImpl go) p
+        StackBuiltin b:t -> do stack =- t ; go b
+        _ -> return ()
+    go Builtin_If = stack =~ \st -> case st of
+      _:y:StackInt 0:t -> y:t
+      x:_:_:t -> x:t
+      _ -> st
+    go (Builtin_Extra x) = runExtra x
+
+
+class (StackSymbol s,Monad m) => MonadStack st s b a m | m -> st s b a where
+  execSymbol :: (b -> m ()) -> s -> m ()
+  runStackState :: State [StackVal s b a] x -> m x
+  runExtraState :: State st x -> m x
+
+newtype ConcatT st b o s m a = ConcatT { _concatT :: StateT (StackState st s b o) m a }
+                          deriving (Functor,SemiApplicative,Unit,Applicative,MonadIO,MonadTrans)
+instance Monad m => Monad (ConcatT st b o s m) where join = coerceJoin ConcatT
+instance (StackSymbol s,Monad m) => MonadStack st s b a (ConcatT st b a s m) where
+  execSymbol x y = ConcatT $ execSymbolImpl (execBuiltin (map _concatT x)) y
+  runStackState st = ConcatT $ (\x -> return (swap $ stack (map swap (st^..state)) x))^.stateT
+  runExtraState st = ConcatT $ (\x -> return (swap $ extraState (map swap (st^..state)) x))^.stateT
+
+defaultState = StackState [] [] 0
+
+concatT :: Iso (ConcatT st b o s m a) (ConcatT st' b' o' s' m' a') (StateT (StackState st s b o) m a) (StateT (StackState st' s' b' o') m' a')
+concatT = iso ConcatT (\(ConcatT x) -> x)

stack.yaml

@@ -46,7 +46,7 @@ packages:
 - curly
 - curly-gateway
 # - grow
-# - misc
+- misc
 # Dependency packages to be pulled from upstream that are not in the resolver
 # (e.g., acme-missiles-0.3)
 extra-deps: [AES-0.2.9,kademlia-1.1.0.0]