module Copilot.Compile.SBV.Common
( mkTmpStVar
, mkUpdateStFn
, mkQueueVar
, mkQueuePtrVar
, mkExtTmpVar
, mkExtTmpTag
, mkExtArrFn
, mkExtFunArgFn
, mkObserverFn
, mkTriggerGuardFn
, mkTriggerArgFn
, mkArgIdx
, tagExtract
) where
import Copilot.Core (Id, Tag, impossible)
import Prelude hiding (id)
mkVar :: String -> Id -> String
mkVar str id = str ++ show id
mkTmpStVar :: Id -> String
mkTmpStVar = mkVar "tmp_"
mkUpdateStFn :: Id -> String
mkUpdateStFn = mkVar "update_state_"
mkQueueVar :: Id -> String
mkQueueVar = mkVar "queue_"
mkQueuePtrVar :: Id -> String
mkQueuePtrVar = mkVar "ptr_"
mkExtTmpVar :: String -> String
mkExtTmpVar = ("ext_" ++)
mkExtTmpTag :: String -> Maybe Tag -> String
mkExtTmpTag name tag = "ext_" ++ name ++ "_" ++ show (tagExtract tag)
mkExtArrFn :: String -> String
mkExtArrFn = (++) "ext_arr_"
mkExtFunArgFn :: Int -> String -> Maybe Tag -> String
mkExtFunArgFn i nm tag =
"ext_" ++ nm ++ "_" ++ show (tagExtract tag) ++ "_arg" ++ show i
mkObserverFn :: String -> String
mkObserverFn = ("observer_" ++)
mkTriggerGuardFn :: String -> String
mkTriggerGuardFn = ("trigger_guard_" ++)
mkTriggerArgFn :: Int -> String -> String
mkTriggerArgFn i nm = "trigger_" ++ nm ++ "_arg_" ++ show i
mkArgIdx :: [a] -> [(Int, a)]
mkArgIdx args = zip [0,1 ..] args
tagExtract :: Maybe Tag -> Tag
tagExtract Nothing = impossible "tagExtract" "copilot-sbv"
tagExtract (Just tag) = tag