From f62eb86a47b0320e2e107efd1d9a587d6c7d26ff Mon Sep 17 00:00:00 2001 From: "Feitong (Leo) Qiao" Date: Fri, 19 Apr 2024 18:21:47 -0400 Subject: [PATCH] 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 | 3 ++- src/TSL/HOA/Codegen.hs | 32 +++++++++++++++++++++++++ src/TSL/HOA/Imp.hs | 18 +++++++++++--- src/TSL/HOA/JavaScript.hs | 49 +++++++++++++++++++++++++++++++++++---- src/TSL/HOA/Python.hs | 49 +++++++++++++++++++++++++++++++++++---- src/TSL/HOA/Verilog.hs | 3 ++- 6 files changed, 141 insertions(+), 13 deletions(-) diff --git a/src/TSL/HOA/Arduino.hs b/src/TSL/HOA/Arduino.hs index ea4923a..2590e65 100644 --- a/src/TSL/HOA/Arduino.hs +++ b/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 } diff --git a/src/TSL/HOA/Codegen.hs b/src/TSL/HOA/Codegen.hs index c70d10e..b994ecb 100644 --- a/src/TSL/HOA/Codegen.hs +++ b/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 diff --git a/src/TSL/HOA/Imp.hs b/src/TSL/HOA/Imp.hs index a28eb0e..039183e 100644 --- a/src/TSL/HOA/Imp.hs +++ b/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 diff --git a/src/TSL/HOA/JavaScript.hs b/src/TSL/HOA/JavaScript.hs index 8f2db4c..6c0a37e 100644 --- a/src/TSL/HOA/JavaScript.hs +++ b/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 } diff --git a/src/TSL/HOA/Python.hs b/src/TSL/HOA/Python.hs index a413cfa..029edf6 100644 --- a/src/TSL/HOA/Python.hs +++ b/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 } diff --git a/src/TSL/HOA/Verilog.hs b/src/TSL/HOA/Verilog.hs index 5b39943..7d86374 100644 --- a/src/TSL/HOA/Verilog.hs +++ b/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 }