Codegen update (#75)

this breaks all our tools, we just need to go and fix them now

* update codegen to produce full function definition for javascript and python

* change function name

* add currentState to the inputs and outputs of updateState

src/TSL/HOA/Arduino.hs

@@ -41,5 +41,6 @@ config =
       impAssign = \x y -> x ++ " = " ++ y ++ ";",
       impIndent = \n -> replicate (2 * n) ' ',
       impBlockStart = " {",
-      impBlockEnd = "}"
+      impBlockEnd = "}",
+      impInitialIndent = 0
     }

src/TSL/HOA/Codegen.hs

@@ -2,6 +2,7 @@
 
 module TSL.HOA.Codegen
   ( codegen,
+    splitInputsCellsOutputs,
     Program (..),
     StateTrans (..),
     Trans (..),
@@ -67,6 +68,37 @@ data Term
   | App String [Term]
   deriving (Show)
 
+-- | SPLIT INPUTS, CELLS, OUTPUTS
+splitInputsCellsOutputs :: Program -> (Set.Set String, Set.Set String, Set.Set String)
+splitInputsCellsOutputs p =
+  let (is, os) = ioFromProgram p
+   in splitSets is os
+  where
+    splitSets :: Set.Set String -> Set.Set String -> (Set.Set String, Set.Set String, Set.Set String)
+    splitSets is os = (is', cs, os')
+      where
+        cs = Set.intersection is os -- Elements common to both is and os
+        is' = is `Set.difference` os -- Elements in is not in os
+        os' = os `Set.difference` is -- Elements in os not in is
+    ioFromProgram :: Program -> (Set.Set String, Set.Set String)
+    ioFromProgram (Program stateTransList) = foldr ((\(ps, us) (ps', us') -> (Set.union ps ps', Set.union us us')) . ioFromStateTrans) (Set.empty, Set.empty) stateTransList
+    ioFromStateTrans :: StateTrans -> (Set.Set String, Set.Set String)
+    ioFromStateTrans (StateTrans _ transList) = foldr ((\(ps, us) (ps', us') -> (Set.union ps ps', Set.union us us')) . ioFromTrans) (Set.empty, Set.empty) transList
+    ioFromTrans :: Trans -> (Set.Set String, Set.Set String)
+    ioFromTrans (Trans ps us _) = (Set.unions (map varsFromPredicate ps) `Set.union` Set.unions (map varsFromUpdateRHS us), Set.fromList (map varsFromUpdateLHS us))
+    varsFromPredicate :: Predicate -> Set.Set String
+    varsFromPredicate PTrue = Set.empty
+    varsFromPredicate PFalse = Set.empty
+    varsFromPredicate (PNot p) = varsFromPredicate p
+    varsFromPredicate (PTerm t) = varsFromTerm t
+    varsFromTerm :: Term -> Set.Set String
+    varsFromTerm (Var x) = Set.singleton x
+    varsFromTerm (App _ ts) = Set.unions (map varsFromTerm ts)
+    varsFromUpdateLHS :: Update -> String
+    varsFromUpdateLHS (Update x _) = x
+    varsFromUpdateRHS :: Update -> Set.Set String
+    varsFromUpdateRHS (Update _ t) = varsFromTerm t
+
 -- | CODEGEN MONAD
 type Gen a = Reader GenCtx a
 

src/TSL/HOA/Imp.hs

@@ -15,6 +15,12 @@ import Data.List
 import qualified Hanoi as H
 import qualified TSL.HOA.Codegen as CG
 
+functionName :: String
+functionName = "updateState"
+
+cellOutputNextPrefix :: String
+cellOutputNextPrefix = "_next_"
+
 data ImpConfig = ImpConfig
   { -- binary functions
     impAdd :: String,
@@ -41,21 +47,27 @@ data ImpConfig = ImpConfig
     impAssign :: String -> String -> String,
     impIndent :: Int -> String,
     impBlockStart :: String,
-    impBlockEnd :: String
+    impBlockEnd :: String,
+    impInitialIndent :: Int
   }
 
 withConfig :: ImpConfig -> Bool -> H.HOA -> String
 withConfig config isCounterStrat hoa =
   let prog = CG.codegen hoa in Reader.runReader (writeProgram isCounterStrat prog) config -- TODO: make the False a flag for indicating counterstrategy
 
+withConfig' :: ImpConfig -> Bool -> CG.Program -> String
+withConfig' config isCounterStrat prog =
+  Reader.runReader (writeProgram isCounterStrat prog) config -- TODO: make the False a flag for indicating counterstrategy
+
 -- | WRITE PROGRAM TO STRING
 type Imp a = Reader ImpConfig a
 
 writeProgram :: Bool -> CG.Program -> Imp String
 writeProgram isCounterStrat (CG.Program stateTransList) = do
+  ImpConfig {..} <- Reader.ask
   lines <-
     concat <$> zipWithM (writeStateTrans isCounterStrat) (False : repeat True) stateTransList
-  return $ intercalate "\n" $ discardEmptyLines lines
+  return $ impIndent impInitialIndent ++ intercalate ("\n" ++ impIndent impInitialIndent) (discardEmptyLines lines)
   where
     discardEmptyLines lines =
       filter (\l -> not (null l) && not (all isSpace l)) lines
@@ -114,7 +126,7 @@ writePredicate p = do
 writeUpdate :: CG.Update -> Imp String
 writeUpdate (CG.Update var term) = do
   ImpConfig {..} <- Reader.ask
-  impAssign var <$> writeTermNoParens term
+  impAssign (cellOutputNextPrefix ++ var) <$> writeTermNoParens term
 
 writeTerm :: CG.Term -> Imp String
 writeTerm term = do

src/TSL/HOA/JavaScript.hs

@@ -5,14 +5,54 @@ module TSL.HOA.JavaScript
 where
 
 import Data.List (intercalate)
+import qualified Data.Set as Set
 import qualified Hanoi as H
+import TSL.HOA.Codegen (codegen, splitInputsCellsOutputs)
 import TSL.HOA.Imp
   ( ImpConfig (..),
-    withConfig,
+    cellOutputNextPrefix,
+    functionName,
+    withConfig',
   )
 
 implement :: Bool -> H.HOA -> String
-implement = withConfig config
+implement isCounterStrat hoa =
+  let prog = codegen hoa
+      controller = withConfig' config isCounterStrat prog
+      (is', cs', os') = splitInputsCellsOutputs prog
+      is = Set.toList is'
+      cs = Set.toList cs'
+      os = Set.toList os'
+   in "function "
+        ++ functionName
+        ++ "({"
+        -- inputs and cells (using JS object destructuring)
+        ++ commas ("currentState" : is ++ cs)
+        ++ "}) {\n"
+        -- instantiate next cells (using let)
+        ++ ( if not (null cs)
+               then
+                 indent 1
+                   ++ "let "
+                   ++ commas (map (cellOutputNextPrefix ++) (cs ++ os))
+                   ++ "\n\n"
+               else ""
+           )
+        -- controller logic
+        ++ controller
+        ++ "\n\n"
+        -- return next cells and outputs (using JS object)
+        ++ indent 1
+        ++ "return {"
+        ++ commas ("currentState" : map cellToNext (cs ++ os))
+        ++ "}\n"
+        ++ "}"
+  where
+    commas = intercalate ", "
+    cellToNext c = c ++ ": " ++ cellOutputNextPrefix ++ c
+
+indent :: Int -> String
+indent n = replicate (2 * n) ' '
 
 config :: ImpConfig
 config =
@@ -40,7 +80,8 @@ config =
       impCondition = \c -> "(" ++ c ++ ")",
       impFuncApp = \f args -> f ++ "(" ++ intercalate ", " args ++ ")",
       impAssign = \x y -> x ++ " = " ++ y,
-      impIndent = \n -> replicate (2 * n) ' ',
+      impIndent = indent,
       impBlockStart = " {",
-      impBlockEnd = "}"
+      impBlockEnd = "}",
+      impInitialIndent = 1
     }

src/TSL/HOA/Python.hs

@@ -5,14 +5,54 @@ module TSL.HOA.Python
 where
 
 import Data.List (intercalate)
+import qualified Data.Set as Set
 import qualified Hanoi as H
+import TSL.HOA.Codegen (codegen, splitInputsCellsOutputs)
 import TSL.HOA.Imp
   ( ImpConfig (..),
-    withConfig,
+    cellOutputNextPrefix,
+    functionName,
+    withConfig',
   )
 
 implement :: Bool -> H.HOA -> String
-implement = withConfig config
+implement isCounterStrat hoa =
+  let prog = codegen hoa
+      controller = withConfig' config isCounterStrat prog
+      (is', cs', os') = splitInputsCellsOutputs prog
+      is = Set.toList is'
+      cs = Set.toList cs'
+      os = Set.toList os'
+   in "def "
+        ++ functionName
+        ++ "(_inputs_and_cells):\n"
+        -- inputs and cells
+        ++ ( if not (null (is ++ cs))
+               then
+                 indent 1
+                   ++ commas ("currentState" : is ++ cs)
+                   ++ " = itemgetter("
+                   ++ commas ("currentState" : map wrapQuotes (is ++ cs))
+                   ++ ")(_inputs_and_cells)"
+                   ++ "\n\n"
+               else ""
+           )
+        -- controller logic
+        ++ controller
+        ++ "\n\n"
+        -- return next cells and outputs (using JS object)
+        ++ indent 1
+        ++ "return {"
+        ++ commas ("\"currentState\": currentState" : map cellToNext (cs ++ os))
+        ++ "}\n"
+        ++ "}"
+  where
+    wrapQuotes s = "\"" ++ s ++ "\""
+    commas = intercalate ", "
+    cellToNext c = wrapQuotes c ++ ": " ++ cellOutputNextPrefix ++ c
+
+indent :: Int -> String
+indent n = replicate (2 * n) ' '
 
 config :: ImpConfig
 config =
@@ -40,7 +80,8 @@ config =
       impCondition = id,
       impFuncApp = \f args -> f ++ "(" ++ intercalate ", " args ++ ")",
       impAssign = \x y -> x ++ " = " ++ y,
-      impIndent = \n -> replicate (2 * n) ' ',
+      impIndent = indent,
       impBlockStart = ":",
-      impBlockEnd = ""
+      impBlockEnd = "",
+      impInitialIndent = 1
     }

src/TSL/HOA/Verilog.hs

@@ -42,5 +42,6 @@ config =
       impAssign = \x y -> x ++ " <= " ++ y ++ ";",
       impIndent = \n -> replicate (2 * n) ' ',
       impBlockStart = " begin",
-      impBlockEnd = "end "
+      impBlockEnd = "end ",
+      impInitialIndent = 0
     }