diff --git a/copilot-sbv.cabal b/copilot-sbv.cabal --- a/copilot-sbv.cabal +++ b/copilot-sbv.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-sbv -version : 0.3 +version : 0.4 synopsis : A compiler for CoPilot targeting SBV. description : Blah blah blah... license : BSD3 diff --git a/src/Copilot/Compile/SBV.hs b/src/Copilot/Compile/SBV.hs --- a/src/Copilot/Compile/SBV.hs +++ b/src/Copilot/Compile/SBV.hs @@ -4,6 +4,7 @@ module Copilot.Compile.SBV ( compile + , compileWithSBV , sbvDirName , module Copilot.Compile.SBV.Params ) where @@ -16,7 +17,7 @@ import Copilot.Compile.SBV.Driver (driver, driverName) import Copilot.Compile.SBV.Makefile (makefile, makefileName) import Copilot.Compile.SBV.Code - (updateStates, updateObservers, fireTriggers, getExtArrs) + (updateStates, updateObservers, fireTriggers, getExtArrs, getExtFuns) import Copilot.Compile.SBV.MetaTable (allocMetaTable) import Copilot.Compile.SBV.Params @@ -30,7 +31,11 @@ sbvDirName = "copilot-sbv-codegen" compile :: Params -> C.Spec -> IO () -compile params spec = do +compile p s = compileWithSBV p [] s + +-- | sbvs are optional additional SBVCodeGens to generate. +compileWithSBV :: Params -> [(String, S.SBVCodeGen ())] -> C.Spec -> IO () +compileWithSBV params sbvs spec0 = do let meta = allocMetaTable spec dirName = withPrefix (prefix params) sbvDirName sbvName = withPrefix (prefix params) "internal" @@ -43,6 +48,8 @@ ++ updateObservers meta spec ++ fireTriggers meta spec ++ getExtArrs meta + ++ getExtFuns meta + ++ sbvs ) putStrLn "" @@ -64,6 +71,8 @@ putStrLn "" putStrLn "Done." + + where spec = C.makeTags spec0 -------------------------------------------------------------------------------- diff --git a/src/Copilot/Compile/SBV/Code.hs b/src/Copilot/Compile/SBV/Code.hs --- a/src/Copilot/Compile/SBV/Code.hs +++ b/src/Copilot/Compile/SBV/Code.hs @@ -10,6 +10,7 @@ , updateObservers , fireTriggers , getExtArrs + , getExtFuns ) where import Copilot.Compile.SBV.Copilot2SBV @@ -21,7 +22,6 @@ import Copilot.Core.Type.Equality ((=~=), coerce, cong) import qualified Data.SBV as S ---import qualified Data.SBV.Internals as S import qualified Data.Map as M import Control.Monad (foldM) @@ -94,25 +94,29 @@ , C.triggerGuard = guard , C.triggerArgs = args } = mkSBVFunc (mkTriggerGuardFn name) mkSBVExp - : map (mkTriggerArg name) (mkTriggerArgIdx args) + : map go (mkArgIdx args) where + go (i,e) = mkArgCall meta (mkTriggerArgFn i name) e mkSBVExp = do inputs <- mkInputs meta (c2Args guard) let e = c2sExpr inputs guard S.cgReturn e - mkTriggerArg :: String -> (Int, C.UExpr) -> SBVFunc - mkTriggerArg name (i, C.UExpr { C.uExprExpr = e - , C.uExprType = t } ) = - mkSBVFunc (mkTriggerArgFn i name) mkExpr - where - mkExpr = do - inputs <- mkInputs meta (c2Args e) - let e' = c2sExpr inputs e - W.SymWordInst <- return (W.symWordInst t) - W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t) - S.cgReturn e' +-------------------------------------------------------------------------------- +mkArgCall :: MetaTable -> String -> C.UExpr -> SBVFunc +mkArgCall meta fnCallName C.UExpr { C.uExprExpr = e + , C.uExprType = t } + = + mkSBVFunc fnCallName mkExpr + where + mkExpr = do + inputs <- mkInputs meta (c2Args e) + let e' = c2sExpr inputs e + W.SymWordInst <- return (W.symWordInst t) + W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t) + S.cgReturn e' + -------------------------------------------------------------------------------- -- Generate an SBV function that calculates the Copilot expression to get the @@ -122,9 +126,10 @@ = map mkIdx (M.toList arrs) where - mkIdx :: (C.Name, C.ExtArray) -> SBVFunc - mkIdx (name, C.ExtArray { C.externArrayIdx = idx - , C.externArrayIdxType = t }) + mkIdx :: (Int, C.ExtArray) -> SBVFunc + mkIdx (_, C.ExtArray { C.externArrayName = name + , C.externArrayIdx = idx + , C.externArrayIdxType = t }) = mkSBVFunc (mkExtArrFn name) mkSBVExpr where @@ -137,6 +142,24 @@ -------------------------------------------------------------------------------- +-- Generate an SBV function that calculates the Copilot expression to get the +-- next index to sample an external array. +getExtFuns :: MetaTable -> [SBVFunc] +getExtFuns meta@(MetaTable { externFunInfoMap = exts }) + = concatMap mkExtF (M.toList exts) + + where + mkExtF :: (Int, C.ExtFun) -> [SBVFunc] + mkExtF (_, C.ExtFun { C.externFunName = name + , C.externFunTag = tag + , C.externFunArgs = args }) + = + map go (mkArgIdx args) + where + go (i,e) = mkArgCall meta (mkExtFunArgFn i name tag) e + +-------------------------------------------------------------------------------- + -- mkInputs takes the datatype containing the entire spec (meta) as well as all -- possible arguments to the SBV function generating the expression. From those -- arguments, it then generates in the SBVCodeGen monad---the actual Inputs--- @@ -152,7 +175,7 @@ where argToInput :: Inputs -> Arg -> S.SBVCodeGen Inputs ------------------------------------------ + ----------------------------------------- -- External variables argToInput acc (Extern name) = @@ -168,45 +191,45 @@ , extType = t }) ) : extVars acc } ------------------------------------------ + ----------------------------------------- --- External arrays - argToInput acc (ExternArr name) = + -- External arrays + argToInput acc (ExternArr name tag) = let extInfos = externArrInfoMap meta in - let Just extInfo = M.lookup name extInfos in + let Just extInfo = M.lookup tag extInfos in mkExtInput extInfo where mkExtInput :: C.ExtArray -> S.SBVCodeGen Inputs mkExtInput C.ExtArray { C.externArrayElemType = t } = do - v <- mkExtInput_ t (mkExtTmpVar name) + v <- mkExtInput_ t (mkExtTmpTag name (Just tag)) return acc { extArrs = (name, ExtInput { extInput = v , extType = t } ) : extArrs acc } ------------------------------------------ + ----------------------------------------- --- External functions + -- External functions argToInput acc (ExternFun name tag) = let extInfos = externFunInfoMap meta in - let Just extInfo = M.lookup name extInfos in + let Just extInfo = M.lookup tag extInfos in mkExtInput extInfo where mkExtInput :: C.ExtFun -> S.SBVCodeGen Inputs mkExtInput C.ExtFun { C.externFunType = t } = do - v <- mkExtInput_ t (mkExtTmpFun name tag) + v <- mkExtInput_ t (mkExtTmpTag name (Just tag)) return acc { extFuns = (name, ExtInput { extInput = v , extType = t } ) : extFuns acc } ------------------------------------------ + ----------------------------------------- --- Stream queues + -- Stream queues argToInput acc (Queue id) = let strmInfos = streamInfoMap meta in let Just strmInfo = M.lookup id strmInfos in diff --git a/src/Copilot/Compile/SBV/Common.hs b/src/Copilot/Compile/SBV/Common.hs --- a/src/Copilot/Compile/SBV/Common.hs +++ b/src/Copilot/Compile/SBV/Common.hs @@ -10,15 +10,17 @@ , mkQueueVar , mkQueuePtrVar , mkExtTmpVar - , mkExtTmpFun + , mkExtTmpTag , mkExtArrFn + , mkExtFunArgFn , mkObserverFn , mkTriggerGuardFn , mkTriggerArgFn - , mkTriggerArgIdx + , mkArgIdx + , tagExtract ) where -import Copilot.Core (Id, Tag) +import Copilot.Core (Id, Tag, impossible) import Prelude hiding (id) mkVar :: String -> Id -> String @@ -39,20 +41,28 @@ mkExtTmpVar :: String -> String mkExtTmpVar = ("ext_" ++) -mkExtTmpFun :: String -> Tag -> String -mkExtTmpFun name tag = "ext_" ++ name ++ "_" ++ show tag +mkExtTmpTag :: String -> Maybe Tag -> String +mkExtTmpTag name tag = "ext_" ++ name ++ "_" ++ show (tagExtract tag) mkExtArrFn :: String -> String -mkExtArrFn = (++) "mk_ext_arr_" +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 = ("mk_observer_" ++) +mkObserverFn = ("observer_" ++) mkTriggerGuardFn :: String -> String -mkTriggerGuardFn = ("mk_trigger_guard_" ++) +mkTriggerGuardFn = ("trigger_guard_" ++) mkTriggerArgFn :: Int -> String -> String -mkTriggerArgFn i nm = "mk_trigger_" ++ nm ++ "_arg_" ++ show i +mkTriggerArgFn i nm = "trigger_" ++ nm ++ "_arg_" ++ show i -mkTriggerArgIdx :: [a] -> [(Int, a)] -mkTriggerArgIdx args = zip [0,1 ..] args +mkArgIdx :: [a] -> [(Int, a)] +mkArgIdx args = zip [0,1 ..] args + +tagExtract :: Maybe Tag -> Tag +tagExtract Nothing = impossible "tagExtract" "copilot-sbv" +tagExtract (Just tag) = tag diff --git a/src/Copilot/Compile/SBV/Copilot2SBV.hs b/src/Copilot/Compile/SBV/Copilot2SBV.hs --- a/src/Copilot/Compile/SBV/Copilot2SBV.hs +++ b/src/Copilot/Compile/SBV/Copilot2SBV.hs @@ -8,7 +8,6 @@ ( c2sExpr , Inputs(..) , Ext --- , ExtArr , ExtQue , ExtInput(..) , QueInput(..) @@ -59,11 +58,6 @@ -------------------------------------------------------------------------------- -c2sExpr :: Inputs -> C.Expr a -> S.SBV a -c2sExpr inputs e = c2sExpr_ e M.empty inputs - --------------------------------------------------------------------------------- - data Local = forall a . Local { localSBVExpr :: S.SBV a , localType :: C.Type a } @@ -77,6 +71,11 @@ case lookup id prs of Nothing -> impossible "lookupInput" "copilot-sbv" Just val -> val + +-------------------------------------------------------------------------------- + +c2sExpr :: Inputs -> C.Expr a -> S.SBV a +c2sExpr inputs e = c2sExpr_ e M.empty inputs -------------------------------------------------------------------------------- diff --git a/src/Copilot/Compile/SBV/Driver.hs b/src/Copilot/Compile/SBV/Driver.hs --- a/src/Copilot/Compile/SBV/Driver.hs +++ b/src/Copilot/Compile/SBV/Driver.hs @@ -5,7 +5,9 @@ {-# LANGUAGE ExistentialQuantification, GADTs #-} -- | Generates the code around the SBV functions to hold the state-updates, --- external variables, etc. +-- external variables, etc. Note: this just creates calls to SBV-generated +-- functions, it does not create them! (Use the names from Common.hs to ensure +-- agreement on names.) module Copilot.Compile.SBV.Driver ( driver @@ -24,7 +26,6 @@ import Copilot.Compile.SBV.Params import qualified Copilot.Core as C ---import Copilot.Core.Type.Equality ((=~=), coerce, cong) import qualified Copilot.Core.Type.Show as C (showWithType, ShowType(..)) import Copilot.Compile.Header.C99 (c99HeaderName) @@ -71,9 +72,11 @@ wr (text "#include" <+> doubleQuotes (text $ c99HeaderName (prefix params))) wr (text "") + wr (text "/* Observers */") wr (declObservers (prefix params) observers) wr (text "") + wr (text "/* Variables */") wr (varDecls meta) wr (text "") @@ -89,20 +92,20 @@ driverFn = mkFunc (withPrefix (prefix params) "step") ( mkFuncCall sampleExtsF [] <> semi + $$ mkFuncCall triggersF [] <> semi + $$ mkFuncCall observersF [] <> semi $$ mkFuncCall updateStatesF [] <> semi $$ mkFuncCall updateBuffersF [] <> semi $$ mkFuncCall updatePtrsF [] <> semi - $$ mkFuncCall observersF [] <> semi - $$ mkFuncCall triggersF [] <> semi ) copilot = vcat $ intersperse (text "") [ sampleExts meta + , fireTriggers meta + , updateObservers params meta , updateStates streams , updateBuffers meta , updatePtrs meta - , updateObservers params meta - , fireTriggers meta ] -------------------------------------------------------------------------------- @@ -118,12 +121,19 @@ where getVars :: MetaTable -> [Decl] - getVars MetaTable { streamInfoMap = streams - , externVarInfoMap = externs } = - map getTmpStVars (M.toList streams) - ++ map getQueueVars (M.toList streams) - ++ map getQueuePtrVars (map fst $ M.toList streams) + getVars MetaTable { streamInfoMap = streams + , externVarInfoMap = externs + , externArrInfoMap = externArrs + , externFunInfoMap = externFuns } + = + map getTmpStVars strLst + ++ map getQueueVars strLst + ++ map getQueuePtrVars (map fst strLst) ++ map getExtVars (M.toList externs) + ++ map getExtArrs (M.toList externArrs) + ++ map getExtFuns (M.toList externFuns) + where + strLst = M.toList streams getTmpStVars :: (C.Id, C.Stream) -> Decl getTmpStVars (id, C.Stream { C.streamExprType = t @@ -159,6 +169,20 @@ getExtVars (var, C.ExtVar _ (C.UType { C.uTypeType = t })) = Decl (retType t) (text $ mkExtTmpVar var) (int 0) + getExtArrs :: (Int, C.ExtArray) -> Decl + getExtArrs (_, C.ExtArray { C.externArrayName = name + , C.externArrayElemType = t + , C.externArrayTag = tag }) + = + Decl (retType t) (text $ mkExtTmpTag name tag) (int 0) + + getExtFuns :: (Int, C.ExtFun) -> Decl + getExtFuns (_, C.ExtFun { C.externFunName = name + , C.externFunType = t + , C.externFunTag = tag }) + = + Decl (retType t) (text $ mkExtTmpTag name tag) (int 0) + varDecl :: Decl -> Doc varDecl Decl { retT = t, declVar = v, initVal = i } = t <+> v <+> equals <+> i <> semi @@ -189,9 +213,9 @@ , externFunInfoMap = extFMap } = -- Arrays and functions have to come after vars. This is because we may use - -- the assignment of extVars in the definition of extArrs. We could write it - -- differently, but it's easier. The Analyzer.hs copilot-core prevents arrays - -- or functions from being used in arrays or functions. + -- the assignment of extVars in the definition of extArrs. The Analyzer.hs + -- copilot-core prevents arrays or functions from being used in arrays or + -- functions. mkFunc sampleExtsF $ vcat (extVars ++ extArrs ++ extFuns) where @@ -209,19 +233,19 @@ -------------------------------------------------------------------------------- -- Arrays --- Currenty, Analyze.hs in copilot-language forbids recurssion in --- external arrays or functions (i.e., an external array can't use another --- external array to compute it's index), so a lot of what is below isn't --- currently necessary. -sampleAExt :: (C.Name, C.ExtArray) -> Doc -sampleAExt (name, C.ExtArray { C.externArrayIdx = idx }) +-- Currenty, Analyze.hs in copilot-language forbids recurssion in external +-- arrays or functions (i.e., an external array can't use another external array +-- to compute it's index). +sampleAExt :: (Int, C.ExtArray) -> Doc +sampleAExt (_, C.ExtArray { C.externArrayName = name + , C.externArrayIdx = idx + , C.externArrayTag = t }) = - text (mkExtTmpVar name) <+> equals <+> arrIdx name idx + text (mkExtTmpTag name t) <+> equals <+> arrIdx name idx where arrIdx :: C.Name -> C.Expr a -> Doc - arrIdx name' e = - text name' <> lbrack <> idxFCall e <> rbrack <> semi + arrIdx name' e = text name' <> lbrack <> idxFCall e <> rbrack <> semi -- Ok, because the analyzer disallows arrays or function calls in index -- expressions, and we assign all variables before arrays. @@ -232,15 +256,19 @@ -------------------------------------------------------------------------------- -- External functions -sampleFExt :: (C.Name, C.ExtFun) -> Doc -sampleFExt (name, C.ExtFun { C.externFunArgs = args }) +sampleFExt :: (Int, C.ExtFun) -> Doc +sampleFExt (_, C.ExtFun { C.externFunName = name + , C.externFunArgs = args + , C.externFunTag = tag }) = - text (mkExtTmpVar name) <+> equals <+> text name <> lparen - <+> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args)) + text (mkExtTmpTag name tag) <+> equals <+> text name <> lparen + <> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args)) <> rparen <> semi where - mkArgCall = undefined-- (i, ( C.UType { C.uTypeType = t} + mkArgCall :: (Int, C.UExpr) -> Doc + mkArgCall (i, C.UExpr { C.uExprExpr = e }) = + mkFuncCall (mkExtFunArgFn i name tag) (map text $ collectArgs e) -------------------------------------------------------------------------------- @@ -281,16 +309,18 @@ fireTrig (name, TriggerInfo { guardArgs = gArgs , triggerArgArgs = argArgs }) = - let f = mkFuncCall name (map mkArg (mkTriggerArgIdx argArgs)) <> semi in text "if" <+> lparen <> guardF <> rparen $+$ nest 2 f where + f = text name <> lparen + <> vcat (punctuate comma $ map mkArg (mkArgIdx argArgs)) + <> rparen <> semi + guardF :: Doc guardF = mkFuncCall (mkTriggerGuardFn name) (map text gArgs) mkArg :: (Int, [String]) -> Doc - mkArg (i, args) = - mkFuncCall (mkTriggerArgFn i name) (map text args) + mkArg (i, args) = mkFuncCall (mkTriggerArgFn i name) (map text args) -------------------------------------------------------------------------------- diff --git a/src/Copilot/Compile/SBV/Makefile.hs b/src/Copilot/Compile/SBV/Makefile.hs --- a/src/Copilot/Compile/SBV/Makefile.hs +++ b/src/Copilot/Compile/SBV/Makefile.hs @@ -28,17 +28,19 @@ wr (text "# Makefile rules for the Copilot driver.") wr (text "") wr $ text "driver" <> colon - <+> text (driverName params) <+> text fileName <> text ".h" - <+> text "internal.a" + <+> text (driverName params) <+> text (withPre fileName) <> text ".h" + <+> archive wr $ text "\t" <> (hsep [ text "$" <> braces (text "CC") , text "$" <> braces (text "CCFLAGS") , text "$<" , text "-o" , text "$@" - , text sbvName <> text ".a"]) + , archive]) where + archive = text sbvName <> text ".a" + withPre nm = withPrefix (prefix params) nm mkStyle :: Doc -> String mkStyle = renderStyle (style {lineLength = 80}) diff --git a/src/Copilot/Compile/SBV/MetaTable.hs b/src/Copilot/Compile/SBV/MetaTable.hs --- a/src/Copilot/Compile/SBV/MetaTable.hs +++ b/src/Copilot/Compile/SBV/MetaTable.hs @@ -5,11 +5,9 @@ {-# LANGUAGE ExistentialQuantification, GADTs #-} module Copilot.Compile.SBV.MetaTable - ( --StreamInfo (..) - StreamInfoMap + ( StreamInfoMap , ExternVarInfoMap , ExternArrInfoMap --- , ExternFunInfo (..) , ExternFunInfoMap , TriggerInfo (..) , TriggerInfoMap @@ -27,7 +25,6 @@ import Data.Map (Map) import Data.List (nub) -import Data.Maybe (fromJust) import qualified Data.Map as M import Prelude hiding (id) @@ -35,8 +32,8 @@ type StreamInfoMap = Map C.Id C.Stream type ExternVarInfoMap = Map C.Name C.ExtVar -type ExternArrInfoMap = Map C.Name C.ExtArray -type ExternFunInfoMap = Map C.Name C.ExtFun +type ExternArrInfoMap = Map C.Tag C.ExtArray +type ExternFunInfoMap = Map C.Tag C.ExtFun -------------------------------------------------------------------------------- @@ -67,45 +64,40 @@ allocMetaTable :: C.Spec -> MetaTable allocMetaTable spec = - let - streamInfoMap_ = M.fromList $ map allocStream (C.specStreams spec) - externVarInfoMap_ = M.fromList $ map allocExternVars (C.externVars spec) - externArrInfoMap_ = M.fromList $ map allocExternArrs (C.externArrays spec) - externFunInfoMap_ = M.fromList $ map allocExternFuns (C.externFuns spec) - triggerInfoMap_ = M.fromList $ map allocTrigger (C.specTriggers spec) - observerInfoMap_ = M.fromList $ map allocObserver (C.specObservers spec) - in - MetaTable { streamInfoMap = streamInfoMap_ - , externVarInfoMap = externVarInfoMap_ - , externArrInfoMap = externArrInfoMap_ - , externFunInfoMap = externFunInfoMap_ - , triggerInfoMap = triggerInfoMap_ - , observerInfoMap = observerInfoMap_ - } + MetaTable { streamInfoMap = streamInfoMap_ + , externVarInfoMap = externVarInfoMap_ + , externArrInfoMap = externArrInfoMap_ + , externFunInfoMap = externFunInfoMap_ + , triggerInfoMap = triggerInfoMap_ + , observerInfoMap = observerInfoMap_ } + + where + streamInfoMap_ = M.fromList $ map allocStream (C.specStreams spec) + externVarInfoMap_ = M.fromList $ map allocExternVars (C.externVars spec) + externArrInfoMap_ = M.fromList $ map allocExternArrs (C.externArrays spec) + externFunInfoMap_ = M.fromList $ map allocExternFuns (C.externFuns spec) + triggerInfoMap_ = M.fromList $ map allocTrigger (C.specTriggers spec) + observerInfoMap_ = M.fromList $ map allocObserver (C.specObservers spec) -------------------------------------------------------------------------------- allocStream :: C.Stream -> (C.Id, C.Stream) -allocStream strm = - (C.streamId strm, strm) +allocStream strm = (C.streamId strm, strm) -------------------------------------------------------------------------------- allocExternVars :: C.ExtVar -> (C.Name, C.ExtVar) -allocExternVars var = - (C.externVarName var, var) +allocExternVars var = (C.externVarName var, var) -------------------------------------------------------------------------------- -allocExternArrs :: C.ExtArray -> (C.Name, C.ExtArray) -allocExternArrs arr = - (C.externArrayName arr, arr) +allocExternArrs :: C.ExtArray -> (C.Tag, C.ExtArray) +allocExternArrs arr = (tagExtract $ C.externArrayTag arr, arr) -------------------------------------------------------------------------------- -allocExternFuns :: C.ExtFun -> (C.Name, C.ExtFun) -allocExternFuns fun = - (C.externFunName fun, fun) +allocExternFuns :: C.ExtFun -> (C.Tag, C.ExtFun) +allocExternFuns fun = (tagExtract $ C.externFunTag fun, fun) -------------------------------------------------------------------------------- @@ -135,15 +127,15 @@ -- Kinds of arguments to SBV functions data Arg = Extern C.Name | ExternFun C.Name C.Tag - | ExternArr C.Name + | ExternArr C.Name C.Tag | Queue C.Id deriving Eq -- | Normal argument calls. argToCall :: Arg -> [String] argToCall (Extern name) = [mkExtTmpVar name] -argToCall (ExternArr name) = [mkExtTmpVar name] -argToCall (ExternFun name tag) = [mkExtTmpFun name tag] +argToCall (ExternArr name tag) = [mkExtTmpTag name (Just tag)] +argToCall (ExternFun name tag) = [mkExtTmpTag name (Just tag)] argToCall (Queue id) = [ mkQueueVar id , mkQueuePtrVar id ] @@ -181,12 +173,12 @@ C.ExternVar _ name _ -> [Extern name] C.ExternFun _ name args _ tag -> - (ExternFun name (fromJust tag)) : + (ExternFun name (tagExtract tag)) : concatMap (\C.UExpr { C.uExprExpr = expr } -> c2Args expr) args - C.ExternArray _ _ name _ _ _ _ -> [ExternArr name] + C.ExternArray _ _ name _ _ _ tag -> [ExternArr name (tagExtract tag)] C.Op1 _ e -> c2Args_ e