copilot-sbv 2.2.0 → 2.2.1
raw patch · 8 files changed
+443/−423 lines, 8 filesdep ~copilot-corenew-uploaderPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: copilot-core
API changes (from Hackage documentation)
Files
- copilot-sbv.cabal +4/−4
- src/Copilot/Compile/SBV.hs +8/−8
- src/Copilot/Compile/SBV/ACSLexpr.hs +23/−27
- src/Copilot/Compile/SBV/ACSLproof.hs +188/−147
- src/Copilot/Compile/SBV/Code.hs +35/−31
- src/Copilot/Compile/SBV/Copilot2SBV.hs +36/−38
- src/Copilot/Compile/SBV/Driver.hs +71/−71
- src/Copilot/Compile/SBV/Transform.hs +78/−97
copilot-sbv.cabal view
@@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-sbv-version : 2.2.0+version : 2.2.1 synopsis : A compiler for CoPilot targeting SBV. description : The Copilot back-end targeting SBV <http://hackage.haskell.org/package/sbv>.@@ -36,12 +36,12 @@ default-language : Haskell2010 hs-source-dirs : src ghc-options : -Wall -fwarn-tabs--- ghc-prof-options : -auto-all -caf-all+ ghc-prof-options : -auto-all -caf-all - build-depends : sbv >= 5.0+ build-depends : sbv >= 5.0 , base >= 4.0 && < 5 , containers >= 0.4- , copilot-core == 2.2.0+ , copilot-core == 2.2.1 , directory >= 1.2.1 , pretty >= 1 , filepath >= 1.1
src/Copilot/Compile/SBV.hs view
@@ -15,11 +15,11 @@ import qualified Copilot.Core.PrettyDot as C import Copilot.Compile.Header.C99 (c99HeaderName, genC99Header) -import qualified Data.SBV as S+import qualified Data.SBV.Tools.CodeGen as S import Copilot.Compile.SBV.Driver (driver, driverName) import Copilot.Compile.SBV.Makefile (makefile, makefileName)-import Copilot.Compile.SBV.Code +import Copilot.Compile.SBV.Code (updateStates, updateObservers, fireTriggers, getExtArrs, getExtFuns) import Copilot.Compile.SBV.MetaTable (allocMetaTable) import Copilot.Compile.SBV.Params@@ -38,7 +38,7 @@ proofACSL :: Params -> C.Spec -> IO () proofACSL p s = do- writeFile "main.gv" (C.prettyPrintDot $ (s))+ writeFile "main.gv" (C.prettyPrintDot s) compileWithSBV p [] (T.transformProofACSL s) compile :: Params -> C.Spec -> IO ()@@ -57,9 +57,9 @@ sbvName $ omitSBVDriver ( updateStates meta spec ++ updateObservers meta spec- ++ fireTriggers meta spec - ++ getExtArrs meta - ++ getExtFuns meta + ++ fireTriggers meta spec+ ++ getExtArrs meta+ ++ getExtFuns meta ++ sbvs ) @@ -88,7 +88,7 @@ -------------------------------------------------------------------------------- readme :: [String]-readme = +readme = [ "These files are automatically generated by Copilot using the SBV code generator backend." , "" , "To build, you will need to ensure that all external variables and triggers are visible."@@ -107,7 +107,7 @@ -------------------------------------------------------------------------------- omitSBVDriver :: [(a, S.SBVCodeGen ())] -> [(a, S.SBVCodeGen ())]-omitSBVDriver = map omit +omitSBVDriver = map omit where omit (a, cg) = (a, S.cgGenerateDriver False >> cg)
src/Copilot/Compile/SBV/ACSLexpr.hs view
@@ -31,41 +31,38 @@ -------------------------------------------------------------------------------- ppExpr :: MT.MetaTable -> Expr a -> Doc-ppExpr meta e0 = parens $ case e0 of+ppExpr meta e0 = case e0 of Const t x -> text (showWithType Haskell t x)- Drop _ 0 id -> + Drop _ 0 id -> let aa = M.lookup id (MT.streamInfoMap meta) in case aa of- Just Stream { streamBuffer = ll } -> - let streamSize = (length ll) in- case streamSize of - 1 -> strmName id <> lbrack <> (text "0") <> rbrack- _ -> strmName id <> lbrack <> (ptrName id) <> rbrack- Drop _ i id -> + Just Stream { streamBuffer = ll } ->+ let streamSize = length ll in+ case streamSize of+ 1 -> strmName id <> lbrack <> text "0" <> rbrack+ _ -> strmName id <> lbrack <> ptrName id <> rbrack+ Drop _ i id -> let aa = M.lookup id (MT.streamInfoMap meta) in case aa of- Just Stream { streamBuffer = ll } -> - let streamSize = (length ll) in- strmName id <> lbrack <> lparen <> ptrName id <> text (" + " ++ show i) <> rparen <> text " % " <> int streamSize <> rbrack + Just Stream { streamBuffer = ll } ->+ let streamSize = length ll in+ strmName id <> lbrack <> lparen <> ptrName id <> text (" + " ++ show i) <> rparen <> text " % " <> int streamSize <> rbrack ExternVar _ name _ -> text $ mkExtTmpVar name- ExternFun _ name _ _ tag -> (text $ mkExtTmpTag name tag)- ExternArray _ _ name - _ _ _ tag -> (text $ mkExtTmpTag name tag)- Local _ _ name e1 e2 -> text "\\let" <+> (text name) <+> equals- <+> (ppExpr meta e1) <+> text ";" <+> (ppExpr meta e2)- Var _ name -> (text name)- Op1 op e -> ppOp1 op (ppExpr meta e)- Op2 op e1 e2 -> ppOp2 op (ppExpr meta e1) (ppExpr meta e2)- Op3 op e1 e2 e3 -> ppOp3 op (ppExpr meta e1) (ppExpr meta e2) (ppExpr meta e3)- Label t s e -> (ppExpr meta e)--ppUExpr :: MT.MetaTable -> UExpr -> Doc-ppUExpr meta UExpr { uExprExpr = e0 } = ppExpr meta e0+ ExternFun _ name _ _ tag -> text $ mkExtTmpTag name tag+ ExternArray _ _ name+ _ _ _ tag -> text $ mkExtTmpTag name tag+ Local _ _ name e1 e2 -> parens $ text "\\let" <+> text name <+> equals+ <+> ppExpr meta e1 <+> text ";" <+> ppExpr meta e2+ Var _ name -> text name+ Op1 op e -> parens $ ppOp1 op (ppExpr meta e)+ Op2 op e1 e2 -> parens $ ppOp2 op (ppExpr meta e1) (ppExpr meta e2)+ Op3 op e1 e2 e3 -> parens $ ppOp3 op (ppExpr meta e1) (ppExpr meta e2) (ppExpr meta e3)+ Label t s e -> ppExpr meta e ppOp1 :: Op1 a b -> Doc -> Doc ppOp1 op = case op of Not -> ppPrefix "!"- Abs _ -> \x -> ((parens $ x <> (text " > 0")) <> text "? " <> x <> text " : -" <> x )+ Abs _ -> ppPrefix "\\abs" Sign _ -> \x -> ((parens $ x <> (text " > 0")) <> text "? 1 : ") <> (parens $ x <> (text " < 0 ? -1 : ") <> x) Recip _ -> ppPrefix "\\recip" Exp _ -> ppPrefix "\\exp"@@ -118,10 +115,9 @@ text ":" <+> doc3 <> text ")" --------------------------------------------------------------------------------- + ppInfix :: String -> Doc -> Doc -> Doc ppInfix cs doc1 doc2 = parens $ doc1 <+> text cs <+> doc2- ppPrefix2 :: String -> Doc -> Doc -> Doc ppPrefix2 cs doc1 doc2 = parens $ text cs <+> doc1 <> text "," <+> doc2
src/Copilot/Compile/SBV/ACSLproof.hs view
@@ -2,11 +2,11 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- -{-# LANGUAGE GADTs, ExistentialQuantification #-}+{-# LANGUAGE GADTs, ExistentialQuantification, LambdaCase #-} module Copilot.Compile.SBV.ACSLproof ( transformProofACSL- ) + ) where import Prelude hiding (id)@@ -82,24 +82,8 @@ , triggerArgs = map transformUExpr uexprl } -------------------------------------------------------------------------------- --- | A property.---data Property = Property--- { propertyName :: Name--- , propertyExpr :: Expr Bool }- --transformProperty :: Property -> Property-transformProperty Property- { propertyName = name- , propertyExpr = bexpr } =- Property- { propertyName = name- , propertyExpr = transformExpr bexpr }----------------------------------------------------------------------------------- -- | A Copilot specification consists of a list of variables bound to anonymous--- streams, a lost of anomymous streams, a list of observers, and a list of+-- streams, a list of anomymous streams, a list of observers, and a list of -- triggers. --data Spec = Spec -- { specStreams :: [Stream]@@ -118,19 +102,20 @@ { specStreams = map transformStream strms , specObservers = map transformObserver obsvs , specTriggers = map transformTrigger trigs- , specProperties = map transformProperty props+ , specProperties = [] } -- -------------------------------------------------------------------------------- --data UExpr = forall a. UExpr -- { uExprType :: Type a -- , uExprExpr :: Expr a } transformUExpr :: UExpr -> UExpr-transformUExpr UExpr { uExprExpr = e, uExprType = t } = +transformUExpr UExpr { uExprExpr = e, uExprType = t } = UExpr { uExprExpr = transformExpr e, uExprType = t } +transformUExpr' :: UExpr -> UExpr+transformUExpr' UExpr { uExprExpr = e, uExprType = t } =+ UExpr { uExprExpr = transformExpr' e, uExprType = t } -------------------------------------------------------------------------------- -- Expr transformation@@ -143,35 +128,37 @@ -- Const :: Type a -> a -> Expr a -- Drop :: Type a -> DropIdx -> Id -> Expr a -- Local :: Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b--- Var :: Type a -> Name -> Expr a --- ExternVar :: Type a -> Name -> Maybe [a] -> Expr a --- ExternFun :: Type a -> Name -> [UExpr] -> Maybe (Expr a) +-- Var :: Type a -> Name -> Expr a+-- ExternVar :: Type a -> Name -> Maybe [a] -> Expr a+-- ExternFun :: Type a -> Name -> [UExpr] -> Maybe (Expr a) -- -> Maybe Tag -> Expr a -- ExternArray :: Integral a => Type a -> Type b -> Name -> Int -> Expr a--- -> Maybe [[b]] -> Maybe Tag -> Expr b --- Op1 :: Op1 a b -> Expr a -> Expr b +-- -> Maybe [[b]] -> Maybe Tag -> Expr b+-- Op1 :: Op1 a b -> Expr a -> Expr b -- Op2 :: Op2 a b c -> Expr a -> Expr b -> Expr c -- Op3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d -transformExpr :: Expr a -> Expr a -transformExpr e0 = case e0 of- Const t x -> Const t x- Drop t k id -> Drop t k id- Local t1 t2 name e1 e2 -> Local t1 t2 name (transformExpr e1) (transformExpr e2) - Var t name -> Var t name- ExternVar t name e -> ExternVar t name e- ExternFun t name args contxt yy-> ExternFun t name (map transformUExpr args) contxt yy- ExternArray t1 t2 name - size idx context yy-> ExternArray t1 t2 name size (transformExpr idx) context yy- Op1 op e -> transformOp1 op e- Op2 op e1 e2 -> transformOp2 op e1 e2- Op3 op e1 e2 e3 -> transformOp3 op e1 e2 e3+transformExpr :: Expr a -> Expr a+transformExpr = simpl . transformExpr' - Label t s e -> case s of - '?':m -> ExternFun t ("ident_"++(showType t)) [UExpr {uExprExpr = transformExpr $ Label t m $ e, uExprType = t}] Nothing Nothing- _ -> Label t s $ transformExpr e- +transformExpr' :: Expr a -> Expr a+transformExpr' e0 = case e0 of+ Const t x -> Const t x+ Drop t k id -> Drop t k id+ Local t1 t2 name e1 e2 -> Local t1 t2 name (transformExpr' e1) (transformExpr e2)+ Var t name -> Var t name+ ExternVar t name e -> ExternVar t name e+ ExternFun t name args contxt yy -> ExternFun t name (map transformUExpr' args) contxt yy+ ExternArray t1 t2 name+ size idx context yy -> ExternArray t1 t2 name size (transformExpr' idx) context yy+ Op1 op e -> transformOp1 op (transformExpr' e)+ Op2 op e1 e2 -> transformOp2 op (transformExpr' e1) (transformExpr' e2)+ Op3 op e1 e2 e3 -> transformOp3 op (transformExpr' e1) (transformExpr' e2) (transformExpr' e3) + Label t s e -> case s of+ '?':m -> ExternFun t ("ident_" ++ showType t) [UExpr {uExprExpr = Label t m $ transformExpr' e, uExprType = t}] Nothing Nothing+ _ -> Label t s $ transformExpr' e+ showType :: Type a -> String showType t = case t of Bool -> "bool"@@ -189,117 +176,171 @@ transformOp1 :: Op1 a b -> Expr a -> Expr b transformOp1 op e = case op of -- Boolean operators.- Not -> Op1 Not $ transformExpr e+ Not -> Op1 Not e -- Numeric operators.- Abs t -> Op2 (Mul t) (transformExpr e) (transformExpr $ Label t "?absolute_value_splitting" $ Op1 (Sign t) $ e)- Sign t -> Op1 (Sign t) $ transformExpr e+-- Abs t -> Op2 (Mul t) e (Label t "?absolute_value_splitting" $ Op1 (Sign t) e)+ Sign t -> Op1 (Sign t) e -- Fractional operators.- Recip a -> Op2 (Fdiv a) (Const a 1.0) (transformExpr e)+ Recip t -> Op2 (Fdiv t) (Const t 1.0) e -- Floating operators.- Exp Float -> ExternFun Float "expf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Exp Double -> ExternFun Double "exp" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Sqrt Float -> ExternFun Float "sqrtf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Sqrt Double -> ExternFun Double "sqrt" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Log Float -> ExternFun Float "logf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Log Double -> ExternFun Double "log" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Sin Float -> ExternFun Float "sinf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Sin Double -> ExternFun Double "sin" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Cos Float -> ExternFun Float "cosf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Cos Double -> ExternFun Double "cos" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Tan Float -> ExternFun Float "tanf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Tan Double -> ExternFun Double "tan" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Asin Float -> ExternFun Float "asinf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Asin Double -> ExternFun Double "asin" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Acos Float -> ExternFun Float "acosf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Acos Double -> ExternFun Double "acos" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Atan Float -> ExternFun Float "atanf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Atan Double -> ExternFun Double "atan" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Sinh Float -> ExternFun Float "sinhf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Sinh Double -> ExternFun Double "sinh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Cosh Float -> ExternFun Float "coshf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Cosh Double -> ExternFun Double "cosh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Tanh Float -> ExternFun Float "tanhf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Tanh Double -> ExternFun Double "tanh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Asinh Float -> ExternFun Float "asinhf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Asinh Double -> ExternFun Double "asinh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Acosh Float -> ExternFun Float "acoshf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Acosh Double -> ExternFun Double "acosh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Atanh Float -> ExternFun Float "atanhf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Atanh Double -> ExternFun Double "atanh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+-- Exp Float -> ExternFun Float "expf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Exp Double -> ExternFun Double "exp"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Sqrt t -> Op2 (Pow t) (Const t 0.5) e+-- Log Float -> ExternFun Float "logf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Log Double -> ExternFun Double "log"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Sin Float -> ExternFun Float "sinf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Sin Double -> ExternFun Double "sin"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Cos Float -> ExternFun Float "cosf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Cos Double -> ExternFun Double "cos"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Tan Float -> ExternFun Float "tanf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Tan Double -> ExternFun Double "tan"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Asin Float -> ExternFun Float "asinf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Asin Double -> ExternFun Double "asin"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Acos Float -> ExternFun Float "acosf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Acos Double -> ExternFun Double "acos"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Atan Float -> ExternFun Float "atanf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Atan Double -> ExternFun Double "atan"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Sinh Float -> ExternFun Float "sinhf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Sinh Double -> ExternFun Double "sinh"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Cosh Float -> ExternFun Float "coshf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Cosh Double -> ExternFun Double "cosh"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Tanh Float -> ExternFun Float "tanhf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Tanh Double -> ExternFun Double "tanh"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Asinh Float -> ExternFun Float "asinhf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Asinh Double -> ExternFun Double "asinh"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Acosh Float -> ExternFun Float "acoshf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Acosh Double -> ExternFun Double "acosh"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing+-- Atanh Float -> ExternFun Float "atanhf"+-- [UExpr { uExprExpr = e, uExprType = Float }] Nothing Nothing+-- Atanh Double -> ExternFun Double "atanh"+-- [UExpr { uExprExpr = e, uExprType = Double }] Nothing Nothing -- Bitwise operators.- BwNot t -> Op1 (BwNot t) $ transformExpr e+ BwNot t -> Op1 (BwNot t) e -- Casting operator.- Cast t s -> Op1 (Cast t s) $ transformExpr e+ Cast t s -> Op1 (Cast t s) e+ op -> Op1 op e transformOp2 :: Op2 a b c -> Expr a -> Expr b -> Expr c transformOp2 op e1 e2 = case op of- -- Boolean operators.- And -> Op2 And (transformExpr e1) (transformExpr e2)- Or -> Op2 Or (transformExpr e1) (transformExpr e2)- -- Numeric operators.- Add t -> Op2 (Add t) (transformExpr e1) (transformExpr e2)- Sub t -> Op2 (Sub t) (transformExpr e1) (transformExpr e2)- Mul t -> Op2 (Mul t) (transformExpr e1) (transformExpr e2)- -- Integral operators.- Mod t -> Op2 (Mod t) (transformExpr e1) (transformExpr e2)- Div t -> Op2 (Div t) (transformExpr e1) (transformExpr e2)- -- Fractional operators.- Fdiv t -> Op2 (Fdiv t) (transformExpr e1) (transformExpr e2) -- Floating operators.- Pow Float -> ExternFun Float "powf" - [UExpr { uExprExpr = transformExpr e1, uExprType = Float } - , UExpr { uExprExpr = transformExpr e2, uExprType = Float }] Nothing Nothing- Pow Double-> ExternFun Double "pow" - [UExpr { uExprExpr = transformExpr e1, uExprType = Double } - , UExpr { uExprExpr = transformExpr e2, uExprType = Double }] Nothing Nothing- Logb t -> Op2 (Fdiv t) (transformExpr $ Op1 (Log t) e1) (transformExpr $ Op1 (Log t) e2)- -- Equality operators.- Eq t -> Op2 (Eq t) (transformExpr e1) (transformExpr e2)- Ne t -> Op2 (Ne t) (transformExpr e1) (transformExpr e2)- -- Relational operators.- Le t -> Op2 (Le t) (transformExpr e1) (transformExpr e2)- Ge t -> Op2 (Ge t) (transformExpr e1) (transformExpr e2)- Lt t -> Op2 (Lt t) (transformExpr e1) (transformExpr e2)- Gt t -> Op2 (Gt t) (transformExpr e1) (transformExpr e2)- -- Bitwise operators.- BwAnd t -> Op2 (BwAnd t) (transformExpr e1) (transformExpr e2)- BwOr t -> Op2 (BwOr t) (transformExpr e1) (transformExpr e2)- BwXor t -> Op2 (BwXor t) (transformExpr e1) (transformExpr e2)- BwShiftL t s -> Op2 (BwShiftL t s) (transformExpr e1) (transformExpr e2)- BwShiftR t s -> Op2 (BwShiftR t s) (transformExpr e1) (transformExpr e2)+ -- Pow Float -> ExternFun Float "powf"+ -- [UExpr { uExprExpr = e1, uExprType = Float }+ -- , UExpr { uExprExpr = e2, uExprType = Float }] Nothing Nothing+ -- Pow Double-> ExternFun Double "pow"+ -- [UExpr { uExprExpr = e1, uExprType = Double }+ -- , UExpr { uExprExpr = e2, uExprType = Double }] Nothing Nothing+ Logb t -> Op2 (Fdiv t) (transformExpr' $ Op1 (Log t) e1) (transformExpr' $ Op1 (Log t) e2)+ op -> Op2 op e1 e2 transformOp3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d-transformOp3 op e1 e2 e3 = case op of - Mux Bool -> Op2 Or (transformExpr $ Op2 And (e2) (e1)) (transformExpr $ Op2 And (e3) (Op1 Not e1))- Mux t -> Op3 (Mux t) (transformExpr e1) (transformExpr e2) (transformExpr e3) +transformOp3 op e1 e2 e3 = case op of+ Mux Bool -> Op2 Or (transformExpr' $ Op2 And e2 e1) (transformExpr' $ Op2 And (e3) (Op1 Not e1))+ Mux t -> Op3 (Mux t) e1 e2 e3++-----------------------------------------++simpl :: Expr a -> Expr a+simpl = \ case+ Op1 op e -> simplOp1 (simpl e) op+ Op2 op e1 e2 -> simplOp2 (simpl e1) (simpl e2) op+ Op3 op e1 e2 e3 -> simplOp3 (simpl e1) (simpl e2) (simpl e3) op+ Local t1 t2 n e1 e2 -> Local t1 t2 n (simpl e1) (simpl e2)+ Label _ _ e -> simpl e+ ExternFun t n args ctx yy -> ExternFun t n (map simplUExpr args) ctx yy++ c -> c++simplUExpr :: UExpr -> UExpr+simplUExpr UExpr { uExprExpr = e, uExprType = t } =+ UExpr { uExprExpr = simpl e, uExprType = t }++simplOp1 :: Expr a -> Op1 a b -> Expr b+simplOp1 e@(Const Bool x) = \ case+ Not -> Const Bool $ not x+ op -> Op1 op e+simplOp1 e@(Const Double x) = \ case+ Abs _ -> Const Double $ abs x+ --Sign _ -> sign x+ --Recip _ ->+ --Exp _ ->+ Sqrt _ -> Const Double $ sqrt x+ --Log _ ->+ Sin _ -> Const Double $ sin x+ Tan _ -> Const Double $ tan x+ Cos _ -> Const Double $ cos x+ Asin _ -> Const Double $ asin x+ Atan _ -> Const Double $ atan x+ Acos _ -> Const Double $ acos x+ Sinh _ -> Const Double $ sinh x+ Tanh _ -> Const Double $ tanh x+ Cosh _ -> Const Double $ cosh x+ Asinh _ -> Const Double $ asinh x+ Atanh _ -> Const Double $ atanh x+ Acosh _ -> Const Double $ acosh x+ --BwNot _ ->+ --Cast _ _ ->+ op -> Op1 op e+simplOp1 e = \ op -> Op1 op e++simplOp2 :: Expr a -> Expr b -> Op2 a b c -> Expr c+simplOp2 e1@(Const Bool x1) e2@(Const Bool x2) = \ case+ And -> Const Bool $ x1 && x2+ Or -> Const Bool $ x1 || x2+ Eq _ -> Const Bool $ x1 == x2+ Ne _ -> Const Bool $ x1 /= x2+ op -> Op2 op e1 e2+simplOp2 e1@(Const t x1) e2@(Const _ x2) = \ case+ Add _ -> Const t $ x1 + x2+ Sub _ -> Const t $ x1 - x2+ Mul _ -> Const t $ x1 * x2+ Div _ -> Const t $ x1 `div` x2+ Mod _ -> Const t $ x1 `mod` x2+ Fdiv _ -> Const t $ x1 / x2+ Pow _ -> Const t $ x1 ** x2+ --Logb _ ->+ Eq _ -> Const Bool $ x1 == x2+ Ne _ -> Const Bool $ x1 /= x2+ Le _ -> Const Bool $ x1 <= x2+ Ge _ -> Const Bool $ x1 >= x2+ Lt _ -> Const Bool $ x1 < x2+ Gt _ -> Const Bool $ x1 > x2+ --BwAnd _ ->+ --BwOr _ ->+ --BwXor _ ->+ --BwShiftL _ _ ->+ --BwShiftR _ _ ->+ op -> Op2 op e1 e2+simplOp2 e1 e2 = \ op -> Op2 op e1 e2++simplOp3 :: Expr a -> Expr b -> Expr c -> Op3 a b c d -> Expr d+-- simplOp3 (Const _ x1) (Const _ x2) (Const _ x3) = \ case+-- Mux _ -> if x1 then x2 else x3+simplOp3 e1 e2 e3 = \ op -> Op3 op e1 e2 e3+
src/Copilot/Compile/SBV/Code.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE LambdaCase #-} module Copilot.Compile.SBV.Code ( updateStates@@ -14,7 +15,7 @@ ) where import Copilot.Compile.SBV.Copilot2SBV-import Copilot.Compile.SBV.MetaTable+import Copilot.Compile.SBV.MetaTable as T import qualified Copilot.Compile.SBV.Witness as W import Copilot.Compile.SBV.Common import Copilot.Compile.SBV.ACSLexpr@@ -22,10 +23,11 @@ import qualified Copilot.Core.PrettyDot as PD import qualified Text.PrettyPrint.HughesPJ as PJ -import qualified Copilot.Core as C+import Copilot.Core as C import Copilot.Core.Type.Equality ((=~=), coerce, cong) -import qualified Data.SBV as S+import qualified Data.SBV as V+import qualified Data.SBV.Tools.CodeGen as S import qualified Data.Map as M import Control.Monad (foldM)@@ -40,6 +42,9 @@ -------------------------------------------------------------------------------- +epsilon :: Double+epsilon = 0.1+ updateStates :: MetaTable -> C.Spec -> [SBVFunc] updateStates meta (C.Spec streams _ _ _) = map updateStreamState streams@@ -47,18 +52,17 @@ where updateStreamState :: C.Stream -> SBVFunc updateStreamState C.Stream { C.streamId = id- , C.streamBuffer = buffer , C.streamExpr = e , C.streamExprType = t1- } + } = mkSBVFunc (mkUpdateStFn id) $ do- S.cgAddDecl [("/*test 001*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta e) ++ ";\n*/")]+ S.cgAddDecl [("/*test 001*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\abs(\\result - " ++ (PJ.render $ ppExpr meta e) ++ ") <= " ++ show epsilon ++ ";\n*/")] inputs <- mkInputs meta (c2Args e) let e' = c2sExpr inputs e- let Just strmInfo = M.lookup id (streamInfoMap meta) + let Just strmInfo = M.lookup id (streamInfoMap meta) updateStreamState1 t1 e' strmInfo - updateStreamState1 :: C.Type a -> S.SBV a -> C.Stream -> S.SBVCodeGen ()+ updateStreamState1 :: C.Type a -> V.SBV a -> C.Stream -> S.SBVCodeGen () updateStreamState1 t1 e1 C.Stream { C.streamExprType = t2 } = do W.SymWordInst <- return (W.symWordInst t2)@@ -82,7 +86,7 @@ where mkSBVExp = do- S.cgAddDecl [("/*test 005*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta e) ++ ";\n*/")]+ S.cgAddDecl [("/*test 005*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\abs(\\result - " ++ (PJ.render $ ppExpr meta e) ++ ") <= " ++ show epsilon ++ ";\n*/")] inputs <- mkInputs meta (c2Args e) let e' = c2sExpr inputs e W.SymWordInst <- return (W.symWordInst t)@@ -105,7 +109,7 @@ where go (i,e) = mkArgCall meta (mkTriggerArgFn i name) e mkSBVExp = do- S.cgAddDecl [("/*test 006*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False guard) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta guard) ++ ";\n*/")]+ S.cgAddDecl [("/*test 006*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta guard) ++ ";\n*/")] inputs <- mkInputs meta (c2Args guard) let e = c2sExpr inputs guard S.cgReturn e@@ -114,12 +118,12 @@ mkArgCall :: MetaTable -> String -> C.UExpr -> SBVFunc mkArgCall meta fnCallName C.UExpr { C.uExprExpr = e- , C.uExprType = t } + , C.uExprType = t } = mkSBVFunc fnCallName mkExpr where mkExpr = do- S.cgAddDecl [("/*test 003*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False e) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta e) ++ ";\n*/")]+ S.cgAddDecl [("/*test 003*/\n/*@\n assigns \\nothing;\n ensures \\abs(\\result - " ++ (PJ.render $ ppExpr meta e) ++ ") <= " ++ show epsilon ++ ";\n*/")] inputs <- mkInputs meta (c2Args e) let e' = c2sExpr inputs e W.SymWordInst <- return (W.symWordInst t)@@ -133,18 +137,18 @@ getExtArrs :: MetaTable -> [SBVFunc] getExtArrs meta@(MetaTable { externArrInfoMap = arrs }) = map mkIdx (M.toList arrs)- + where mkIdx :: (Int, C.ExtArray) -> SBVFunc mkIdx (_, C.ExtArray { C.externArrayName = name , C.externArrayIdx = idx , C.externArrayIdxType = t })- = + = mkSBVFunc (mkExtArrFn name) mkSBVExpr where mkSBVExpr :: S.SBVCodeGen () mkSBVExpr = do- S.cgAddDecl [("/*test 002*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False idx) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\result == " ++ (PJ.render $ ppExpr meta idx) ++ ";\n*/")]+ S.cgAddDecl [("/*test 002*/\n/*DotBegin\n" ++ (PD.prettyPrintExprDot False idx) ++ "\nDotEnd*/\n/*@\n assigns \\nothing;\n ensures \\abs(\\result - " ++ (PJ.render $ ppExpr meta idx) ++ ") <= " ++ show epsilon ++ ";\n*/")] inputs <- mkInputs meta (c2Args idx) W.SymWordInst <- return (W.symWordInst t) W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)@@ -157,13 +161,13 @@ 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@@ -179,42 +183,42 @@ -- (argToCall from MetaTable.hs). mkInputs :: MetaTable -> [Arg] -> S.SBVCodeGen Inputs-mkInputs meta args = - foldM argToInput (Inputs [] [] [] []) args +mkInputs meta args =+ foldM argToInput (Inputs [] [] [] []) args where argToInput :: Inputs -> Arg -> S.SBVCodeGen Inputs ------------------------------------------ + -- External variables- argToInput acc (Extern name) = + argToInput acc (Extern name) = let extInfos = externVarInfoMap meta in let Just extInfo = M.lookup (name) extInfos in mkExtInput extInfo - where + where mkExtInput :: C.ExtVar -> S.SBVCodeGen Inputs mkExtInput (C.ExtVar _ C.UType { C.uTypeType = t }) = do ext <- mkExtInput_ t (mkExtTmpVar name)- return acc { extVars = (name, (ExtInput { extInput = ext + return acc { extVars = (name, (ExtInput { extInput = ext , extType = t }) ) : extVars acc } ----------------------------------------- -- External arrays- argToInput acc (ExternArr name tag) = + argToInput acc (ExternArr name tag) = let extInfos = externArrInfoMap meta in let Just extInfo = M.lookup tag extInfos in mkExtInput extInfo - where + where mkExtInput :: C.ExtArray -> S.SBVCodeGen Inputs mkExtInput C.ExtArray { C.externArrayElemType = t } = do v <- mkExtInput_ t (mkExtTmpTag name (Just tag))- return acc { extArrs = ((mkExtTmpTag name (Just tag)), ExtInput + return acc { extArrs = ((mkExtTmpTag name (Just tag)), ExtInput { extInput = v , extType = t } ) : extArrs acc }@@ -222,7 +226,7 @@ ----------------------------------------- -- External functions- argToInput acc (ExternFun name tag) =+ argToInput acc (T.ExternFun name tag) = let extInfos = externFunInfoMap meta in let Just extInfo = M.lookup tag extInfos in mkExtInput extInfo@@ -232,7 +236,7 @@ mkExtInput C.ExtFun { C.externFunType = t } = do v <- mkExtInput_ t (mkExtTmpTag name (Just tag))- return acc { extFuns = ((mkExtTmpTag name (Just tag)), ExtInput + return acc { extFuns = ((mkExtTmpTag name (Just tag)), ExtInput { extInput = v , extType = t } ) : extFuns acc }@@ -257,8 +261,8 @@ , arrType = t }) ) : extQues acc }- - mkQueInput_ :: C.Type a -> [a] -> S.SBVCodeGen [S.SBV a]++ mkQueInput_ :: C.Type a -> [a] -> S.SBVCodeGen [V.SBV a] mkQueInput_ t que = do W.SymWordInst <- return (W.symWordInst t) W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)@@ -267,7 +271,7 @@ ----------------------------------------- -mkExtInput_ :: C.Type a -> String -> S.SBVCodeGen (S.SBV a)+mkExtInput_ :: C.Type a -> String -> S.SBVCodeGen (V.SBV a) mkExtInput_ t name = do W.SymWordInst <- return (W.symWordInst t) W.HasSignAndSizeInst <- return (W.hasSignAndSizeInst t)
src/Copilot/Compile/SBV/Copilot2SBV.hs view
@@ -12,7 +12,7 @@ , ExtInput(..) , QueInput(..) , QueueIn(..)- ) + ) where import Prelude hiding (id)@@ -46,17 +46,17 @@ , extQues :: [ExtQue] } -- External input -- variables, arrays, and functions-data ExtInput = forall a. ExtInput +data ExtInput = forall a. ExtInput { extInput :: S.SBV a , extType :: C.Type a } -- Stream queues-data QueInput = forall a. QueInput +data QueInput = forall a. QueInput { arrInput :: QueueIn a } data QueueIn a = QueueIn { queue :: [S.SBV a]- , quePtr :: S.SBV Q.QueueSize + , quePtr :: S.SBV Q.QueueSize , arrType :: C.Type a } --------------------------------------------------------------------------------@@ -105,7 +105,7 @@ , arrType = t2 } } = let Just p = t2 =~= t1 in case W.symWordInst t2 of- W.SymWordInst -> + W.SymWordInst -> case W.hasSignAndSizeInst t2 of W.HasSignAndSizeInst -> coerce (cong p) (Q.lookahead i que' qPtr)@@ -120,10 +120,8 @@ ---------------------------------------------------- C.Var t1 name ->- let Just local = M.lookup name env- in- case local of- Local+ case M.lookup name env of+ Just Local { localSBVExpr = e , localType = t2 } ->@@ -132,10 +130,10 @@ ---------------------------------------------------- - C.ExternVar t name _ -> + C.ExternVar t name _ -> getSBV t ext - where + where ext :: ExtInput ext = lookupInput name (extVars inputs) @@ -147,10 +145,10 @@ ---------------------------------------------------- - C.ExternArray _ t name _ _ _ tag -> + C.ExternArray _ t name _ _ _ tag -> getSBV t getExtArr - where + where getExtArr :: ExtInput getExtArr = lookupInput (mkExtTmpTag name (tag)) (extArrs inputs) @@ -172,7 +170,7 @@ , extInput = v } = let Just p = t2 =~= t1 in coerce (cong p) v- + ---------------------------------------------------- C.Op1 op e ->@@ -184,7 +182,7 @@ C.Op2 op e1 e2 -> let res1 = c2sExpr_ e1 env inputs in let res2 = c2sExpr_ e2 env inputs in- c2sOp2 op res1 res2 + c2sOp2 op res1 res2 ---------------------------------------------------- @@ -194,29 +192,29 @@ let res3 = c2sExpr_ e3 env inputs in c2sOp3 op res1 res2 res3 - C.Label t s e -> case W.symWordInst t of + C.Label t s e -> case W.symWordInst t of W.SymWordInst -> S.label s (c2sExpr_ e env inputs) --------------------------------------------------------------------------------- +-------------------------------------------------------------------------------- noFloatOpsErr :: String -> a-noFloatOpsErr op = - badUsage ("The operation you used is not supported by the SBV backend: " +noFloatOpsErr op =+ badUsage ("The operation you used is not supported by the SBV backend: " ++ "operator " ++ op ++ " not supported. Please change it with your math skills to something supported.") --------------------------------------------------------------------------------- +-------------------------------------------------------------------------------- c2sOp1 :: C.Op1 a b -> S.SBV a -> S.SBV b c2sOp1 op = case op of Not -> (S.bnot)- Abs t -> case W.symWordInst t of - W.SymWordInst -> abs - Sign t -> case W.symWordInst t of + Abs t -> case W.symWordInst t of+ W.SymWordInst -> abs+ Sign t -> case W.symWordInst t of W.SymWordInst -> signum- BwNot t -> case W.bitsInst t of + BwNot t -> case W.bitsInst t of W.BitsInst -> (S.complement) - Cast t0 t1 -> case W.castInst t0 t1 of + Cast t0 t1 -> case W.castInst t0 t1 of W.CastInst -> W.sbvCast Recip _ -> noFloatOpsErr "recip"@@ -228,9 +226,9 @@ Log C.Float -> log Log C.Double -> log Sin C.Float -> sin- Sin C.Double -> sin+ Sin C.Double -> S.uninterpret "sin" Cos C.Float -> cos- Cos C.Double -> cos+ Cos C.Double -> S.uninterpret "cos" Tan C.Float -> tan Tan C.Double -> tan Asin C.Float -> asin@@ -269,30 +267,30 @@ Lt t -> case W.ordInst t of W.OrdInst -> (S..<) Gt t -> case W.ordInst t of W.OrdInst -> (S..>) - Div t -> case W.divInst t of W.BVDivisibleInst -> + Div t -> case W.divInst t of W.BVDivisibleInst -> \x y -> fst (S.sQuotRem x y)- Mod t -> case W.divInst t of W.BVDivisibleInst -> + Mod t -> case W.divInst t of W.BVDivisibleInst -> \x y -> snd (S.sQuotRem x y) BwAnd t -> case W.bitsInst t of W.BitsInst -> (S..&.) BwOr t -> case W.bitsInst t of W.BitsInst -> (S..|.) BwXor t -> case W.bitsInst t of W.BitsInst -> (S.xor)- BwShiftL tvec tidx -> - case W.integralInst tvec of - W.IntegralInst -> + BwShiftL tvec tidx ->+ case W.integralInst tvec of+ W.IntegralInst -> \vec idx -> case (W.integralInst tidx) of W.IntegralInst -> S.sShiftLeft vec idx --case S.unliteral idx of -- Nothing -> badUsage "Using the SBV backend, shiftL only supports constant shift indicies" -- Just x -> S.shiftL vec (fromIntegral x)- BwShiftR tvec tidx -> - case W.integralInst tvec of - W.IntegralInst -> + BwShiftR tvec tidx ->+ case W.integralInst tvec of+ W.IntegralInst -> \vec idx -> case (W.integralInst tidx) of W.IntegralInst -> S.sShiftRight vec idx --- case W.bitsInst tvec of --- W.BitsInst -> +-- case W.bitsInst tvec of+-- W.BitsInst -> -- \vec idx -> case W.symWordInst tidx of -- W.SymWordInst -> case S.unliteral idx of -- Nothing -> badUsage "Using the SBV backend, shiftR only supports constant shift indicies"@@ -309,7 +307,7 @@ c2sOp3 :: C.Op3 a b c d -> S.SBV a -> S.SBV b -> S.SBV c -> S.SBV d c2sOp3 op = case op of Mux t ->- case W.mergeableInst t of + case W.mergeableInst t of W.MergeableInst -> \b c1 c2 -> S.ite b c1 c2
src/Copilot/Compile/SBV/Driver.hs view
@@ -81,7 +81,7 @@ wr (text "") wr copilot- + wr (text "/* Idents */\n") wr (text "/*@\n assigns \\nothing;\n */\nSBool ident_bool(SBool a) {return a;}") wr (text "/*@\n assigns \\nothing;\n */\nSWord8 ident_word8(SWord8 a) {return a;}")@@ -117,7 +117,7 @@ testFn :: Doc testFn = mkFunc (withPrefix (prefix params) "testing")- ( text "for(;;) step()"<> semi+ ( text "for(;;)" <> (text (withPrefix (prefix params) "step()")) <> semi ) copilot = vcat $ intersperse (text "")@@ -126,7 +126,7 @@ , updateObservers params meta , updateStates streams , updateBuffers meta- , updatePtrs meta + , updatePtrs meta ] --------------------------------------------------------------------------------@@ -141,12 +141,12 @@ varDecls meta = vcat $ map varDecl (getVars meta) where- getVars :: MetaTable -> [Decl] - getVars MetaTable { streamInfoMap = streams - , externVarInfoMap = externs + getVars :: MetaTable -> [Decl]+ getVars MetaTable { streamInfoMap = streams+ , externVarInfoMap = externs , externArrInfoMap = externArrs , externFunInfoMap = externFuns }- = + = map getTmpStVars strLst ++ map getQueueVars strLst ++ map getQueuePtrVars (map fst strLst)@@ -158,41 +158,41 @@ getTmpStVars :: (C.Id, C.Stream) -> Decl getTmpStVars (id, C.Stream { C.streamExprType = t- , C.streamBuffer = que }) = + , C.streamBuffer = que }) = Decl (retType t) (text $ mkTmpStVar id) getFirst- where + where -- ASSUME queue is nonempty! getFirst = text (cShow $ C.showWithType C.Haskell t (headErr que)) headErr [] = C.impossible "headErr" "copilot-sbv" headErr xs = head xs- + getQueueVars :: (C.Id, C.Stream) -> Decl getQueueVars (id, C.Stream { C.streamExprType = t , C.streamBuffer = que }) =- Decl (retType t) + Decl (retType t) (text (mkQueueVar id) <> lbrack <> int (length que) <> rbrack) getInits- where + where getInits = lbrace <+> vals <+> rbrace- where - vals = hcat $ punctuate (comma <> text " ") - (map (text . cShow . C.showWithType C.Haskell t) + where+ vals = hcat $ punctuate (comma <> text " ")+ (map (text . cShow . C.showWithType C.Haskell t) que) getQueuePtrVars :: C.Id -> Decl- getQueuePtrVars id = + getQueuePtrVars id = Decl (retType queSize) (text $ mkQueuePtrVar id) (int 0)- where + where queSize :: C.Type QueueSize- queSize = C.typeOf + queSize = C.typeOf getExtVars :: (C.Name, C.ExtVar) -> Decl- getExtVars (var, C.ExtVar _ (C.UType { C.uTypeType = t })) = + getExtVars (var, C.ExtVar _ (C.UType { C.uTypeType = t })) = Decl (retType t) (text $ mkExtTmpVar var) (int 0) - getExtArrs :: (Int, C.ExtArray) -> Decl + getExtArrs :: (Int, C.ExtArray) -> Decl getExtArrs (_, C.ExtArray { C.externArrayName = name- , C.externArrayElemType = t + , C.externArrayElemType = t , C.externArrayTag = tag }) = Decl (retType t) (text $ mkExtTmpTag name tag) (int 0)@@ -231,19 +231,19 @@ sampleExts :: MetaTable -> Doc sampleExts MetaTable { externVarInfoMap = extVMap , externArrInfoMap = extAMap- , externFunInfoMap = extFMap } + , 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. The Analyzer.hs -- copilot-core prevents arrays or functions from being used in arrays or -- functions.- --extACSL $$ + --extACSL $$ (mkFunc ("static " ++ sampleExtsF) $ vcat (extVars ++ extArrs ++ extFuns)) where --ll = sampleVExtACSL extVMap ++ sampleAExtACSL extAMap ++ sampleFExtACSL extFMap --extACSL = vcat [text "/*@",--- (case ll of +-- (case ll of -- [] -> text " assigns \\nothing;" -- _ -> vcat $ ll) -- ,text "*/"]@@ -258,17 +258,17 @@ -- Variables --sampleVExtACSL :: M.Map C.Name C.ExtVar -> [Doc]---sampleVExtACSL extVMap = +--sampleVExtACSL extVMap = -- (map sampleVExtACSL1 ((fst . unzip . M.toList) extVMap)) ++ (map sampleVExtACSL2 ((fst . unzip . M.toList) extVMap)) --sampleVExtACSL1 :: C.Name -> Doc---sampleVExtACSL1 name = +--sampleVExtACSL1 name = -- text " assigns" <+> text (mkExtTmpVar name) <> semi --sampleVExtACSL2 :: C.Name -> Doc---sampleVExtACSL2 name = +--sampleVExtACSL2 name = -- text " //ensures" <+> text (mkExtTmpVar name) <+> text "==" <+> text name <> semi sampleVExt :: C.Name -> Doc-sampleVExt name = +sampleVExt name = text (mkExtTmpVar name) <+> equals <+> text name <> semi --------------------------------------------------------------------------------@@ -278,55 +278,55 @@ -- arrays or functions (i.e., an external array can't use another external array -- to compute it's index). --sampleAExtACSL :: M.Map C.Tag C.ExtArray -> [Doc]---sampleAExtACSL extAMap = +--sampleAExtACSL extAMap = -- (map sampleAExtACSL1 (M.toList extAMap)) ++ (map sampleAExtACSL2 (M.toList extAMap)) -- --sampleAExtACSL1 :: (Int, C.ExtArray) -> Doc --sampleAExtACSL1 (_, C.ExtArray { C.externArrayName = name--- , C.externArrayIdx = idx +-- , C.externArrayIdx = idx -- , C.externArrayTag = t })--- = +-- = -- text " assigns" <+> text (mkExtTmpTag name t) <+> semi --sampleAExtACSL2 :: (Int, C.ExtArray) -> Doc --sampleAExtACSL2 (_, C.ExtArray { C.externArrayName = name--- , C.externArrayIdx = idx +-- , C.externArrayIdx = idx -- , C.externArrayTag = t })--- = +-- = -- text " //ensures" <+> text (mkExtTmpTag name t) <+> text "==" <+> text ("tmp_"++(mkExtTmpTag name t)) <> semi --sampleAExt1 :: (Int, C.ExtArray) -> Doc --sampleAExt1 (_, C.ExtArray { C.externArrayName = name--- , C.externArrayIdx = idx --- , C.externArrayElemType = tttt +-- , C.externArrayIdx = idx+-- , C.externArrayElemType = tttt -- , C.externArrayTag = t }) -- = (retType tttt) <+> text ("tmp_"++(mkExtTmpTag name t)) <+> equals <+> arrIdx name idx--- --- where +--+-- where -- arrIdx :: C.Name -> C.Expr a -> Doc -- 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. -- idxFCall :: C.Expr a -> Doc--- idxFCall e = +-- idxFCall e = -- mkFuncCall (mkExtArrFn name) (map text $ collectArgs e) sampleAExt :: (Int, C.ExtArray) -> Doc sampleAExt (_, C.ExtArray { C.externArrayName = name- , C.externArrayIdx = idx - , C.externArrayElemType = tttt + , C.externArrayIdx = idx+ , C.externArrayElemType = tttt , C.externArrayTag = t }) = text (mkExtTmpTag name t) <+> equals <+> arrIdx name idx <> semi- where + where arrIdx :: C.Name -> C.Expr a -> Doc 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. idxFCall :: C.Expr a -> Doc- idxFCall e = + idxFCall e = mkFuncCall (mkExtArrFn name) (map text $ collectArgs e) --------------------------------------------------------------------------------@@ -337,46 +337,46 @@ --sampleFExtACSL1 :: (Int, C.ExtFun) -> Doc --sampleFExtACSL1 (_, C.ExtFun { C.externFunName = name--- , C.externFunArgs = args +-- , C.externFunArgs = args -- , C.externFunTag = tag })--- = +-- = -- text " assigns" <+> text (mkExtTmpTag name tag) <> semi --sampleFExtACSL2 :: (Int, C.ExtFun) -> Doc --sampleFExtACSL2 (_, C.ExtFun { C.externFunName = name--- , C.externFunArgs = args +-- , C.externFunArgs = args -- , C.externFunTag = tag })--- = +-- = -- text " //ensures" <+> text (mkExtTmpTag name tag) <+> text "==" <+> text ("tmp_"++(mkExtTmpTag name tag)) <> semi -- External functions --sampleFExt1 :: (Int, C.ExtFun) -> Doc --sampleFExt1 (_, C.ExtFun { C.externFunName = name--- , C.externFunArgs = args +-- , C.externFunArgs = args -- , C.externFunType = tttt -- , C.externFunTag = tag })--- = +-- = -- (retType tttt) <+> text ("tmp_"++(mkExtTmpTag name tag)) <+> equals <+> text name <> lparen -- <> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args)) -- <> rparen <> semi -- -- where--- mkArgCall :: (Int, C.UExpr) -> Doc --- mkArgCall (i, C.UExpr { C.uExprExpr = e }) = +-- mkArgCall :: (Int, C.UExpr) -> Doc+-- mkArgCall (i, C.UExpr { C.uExprExpr = e }) = -- mkFuncCall (mkExtFunArgFn i name tag) (map text $ collectArgs e) sampleFExt :: (Int, C.ExtFun) -> Doc sampleFExt (_, C.ExtFun { C.externFunName = name- , C.externFunArgs = args + , C.externFunArgs = args , C.externFunType = tttt , C.externFunTag = tag })- = + = text (mkExtTmpTag name tag) <+> equals <+> text name <> lparen <> hsep (punctuate comma $ map mkArgCall (zip [(0 :: Int) ..] args)) <> rparen <> semi where- mkArgCall :: (Int, C.UExpr) -> Doc - mkArgCall (i, C.UExpr { C.uExprExpr = e }) = + mkArgCall :: (Int, C.UExpr) -> Doc+ mkArgCall (i, C.UExpr { C.uExprExpr = e }) = mkFuncCall (mkExtFunArgFn i name tag) (map text $ collectArgs e) --------------------------------------------------------------------------------@@ -412,7 +412,7 @@ -------------------------------------------------------------------------------- updateObservers :: Params -> MetaTable -> Doc-updateObservers params MetaTable { observerInfoMap = observers } +updateObservers params MetaTable { observerInfoMap = observers } = let ll = M.toList observers in (case ll of [] -> text "/*@\n assigns \\nothing;\n */"@@ -432,7 +432,7 @@ -------------------------------------------------------------------------------- fireTriggers :: MetaTable -> Doc-fireTriggers MetaTable { triggerInfoMap = triggers } +fireTriggers MetaTable { triggerInfoMap = triggers } = -- text "/*@\n assigns \\nothing; \n*/" $$ (mkFunc ("static " ++ triggersF) $ vcat $ map fireTrig (M.toList triggers)) @@ -440,14 +440,14 @@ -- if (guard) trigger(args); fireTrig :: (C.Name, TriggerInfo) -> Doc fireTrig (name, TriggerInfo { guardArgs = gArgs- , triggerArgArgs = argArgs }) - = + , triggerArgArgs = argArgs })+ = text "if" <+> lparen <> guardF <> rparen $+$ nest 2 f where- f = text name <> lparen - <> vcat (punctuate comma $ map mkArg (mkArgIdx argArgs)) - <> rparen <> semi + f = text name <> lparen+ <> vcat (punctuate comma $ map mkArg (mkArgIdx argArgs))+ <> rparen <> semi guardF :: Doc guardF = mkFuncCall (mkTriggerGuardFn name) (map text gArgs)@@ -460,14 +460,14 @@ writeACSLqueues :: MetaTable -> Doc writeACSLqueues MetaTable { streamInfoMap = strMap } = let ll = M.toList strMap- in + in vcat $ (text "/*ACSL following*/\n"):(case ll of [] -> [text ""] _ -> (text "/*@" :(map varAndUpdate (ll) ++ [(text "*/")]))- ) + ) - where + where varAndUpdate :: (C.Id, C.Stream) -> Doc varAndUpdate (id, C.Stream { C.streamBuffer = que }) = updateFunc (mkQueueVar id) (fromIntegral $ length que) (mkQueuePtrVar id)@@ -482,7 +482,7 @@ -------------------------------------------------------------------------------- updateBuffers :: MetaTable -> Doc-updateBuffers MetaTable { streamInfoMap = strMap } +updateBuffers MetaTable { streamInfoMap = strMap } = let ll = M.toList strMap in (case ll of [] -> text "/*@\n assigns \\nothing;\n */"@@ -522,7 +522,7 @@ )$$ (mkFunc ("static " ++ updatePtrsF) $ vcat $ map varAndUpdate (ll)) - where + where varAndUpdateACSL :: (C.Id, C.Stream) -> Doc varAndUpdateACSL (id, C.Stream { C.streamBuffer = que }) =@@ -531,8 +531,8 @@ -- idx = (idx + 1) % queueSize; updateFuncACSL :: QueueSize -> String -> Doc updateFuncACSL sz ptr =- text " assigns" <+> text ptr <> semi <> (text "\n ensures" <+> text ptr <+> text "==" - <+> lparen <> text "\\old (" <> text ptr <+> text ") +" <+> int 1 <> rparen + text " assigns" <+> text ptr <> semi <> (text "\n ensures" <+> text ptr <+> text "=="+ <+> lparen <> text "\\old (" <> text ptr <+> text ") +" <+> int 1 <> rparen <+> text "%" <+> int (fromIntegral sz) <> semi <> text "\n") @@ -543,8 +543,8 @@ -- idx = (idx + 1) % queueSize; updateFunc :: QueueSize -> String -> Doc updateFunc sz ptr =- text ptr <+> equals - <+> lparen <> text ptr <+> text "+" <+> int 1 <> rparen + text ptr <+> equals+ <+> lparen <> text ptr <+> text "+" <+> int 1 <> rparen <+> text "%" <+> int (fromIntegral sz) <> semi --------------------------------------------------------------------------------@@ -578,4 +578,4 @@ C.Float -> "SFloat" C.Double -> "SDouble" - _ -> C.badUsage "You've tried to compile a Copilot program to SBV with a type SBV does not support. SBV does not support floats or doubles. To compile programs using these types, use the copilot-c99 (Atom) backend. See README.md for more information."+ _ -> C.badUsage "You've tried to compile a Copilot program to SBV with a type SBV does not support. To compile programs using these types, use the copilot-c99 (Atom) backend. See README.md for more information."
src/Copilot/Compile/SBV/Transform.hs view
@@ -6,7 +6,7 @@ module Copilot.Compile.SBV.Transform ( transform- ) + ) where import Prelude hiding (id)@@ -86,8 +86,8 @@ --data Property = Property -- { propertyName :: Name -- , propertyExpr :: Expr Bool }- + transformProperty :: Property -> Property transformProperty Property { propertyName = name@@ -99,7 +99,7 @@ -------------------------------------------------------------------------------- -- | A Copilot specification consists of a list of variables bound to anonymous--- streams, a lost of anomymous streams, a list of observers, and a list of+-- streams, a list of anomymous streams, a list of observers, and a list of -- triggers. --data Spec = Spec -- { specStreams :: [Stream]@@ -128,14 +128,9 @@ -- { uExprType :: Type a -- , uExprExpr :: Expr a } transformUExpr :: UExpr -> UExpr-transformUExpr UExpr { uExprExpr = e, uExprType = t } = +transformUExpr UExpr { uExprExpr = e, uExprType = t } = UExpr { uExprExpr = transformExpr e, uExprType = t } -transformSExpr :: (Name, UExpr) -> (Name, UExpr)-transformSExpr (name, UExpr { uExprExpr = e, uExprType = t }) =- (name, transformUExpr UExpr { uExprExpr = e, uExprType = t })-- -------------------------------------------------------------------------------- -- Expr transformation --@@ -147,46 +142,32 @@ -- Const :: Type a -> a -> Expr a -- Drop :: Type a -> DropIdx -> Id -> Expr a -- Local :: Type a -> Type b -> Name -> Expr a -> Expr b -> Expr b--- Var :: Type a -> Name -> Expr a --- ExternVar :: Type a -> Name -> Maybe [a] -> Expr a --- ExternFun :: Type a -> Name -> [UExpr] -> Maybe (Expr a) +-- Var :: Type a -> Name -> Expr a+-- ExternVar :: Type a -> Name -> Maybe [a] -> Expr a+-- ExternFun :: Type a -> Name -> [UExpr] -> Maybe (Expr a) -- -> Maybe Tag -> Expr a -- ExternArray :: Integral a => Type a -> Type b -> Name -> Int -> Expr a--- -> Maybe [[b]] -> Maybe Tag -> Expr b --- Op1 :: Op1 a b -> Expr a -> Expr b +-- -> Maybe [[b]] -> Maybe Tag -> Expr b+-- Op1 :: Op1 a b -> Expr a -> Expr b -- Op2 :: Op2 a b c -> Expr a -> Expr b -> Expr c -- Op3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d -transformExpr :: Expr a -> Expr a +transformExpr :: Expr a -> Expr a transformExpr e0 = case e0 of Const t x -> Const t x Drop t k id -> Drop t k id- Local t1 t2 name e1 e2 -> Local t1 t2 name (transformExpr e1) (transformExpr e2) + Local t1 t2 name e1 e2 -> Local t1 t2 name (transformExpr e1) (transformExpr e2) Var t name -> Var t name ExternVar t name e -> ExternVar t name e ExternFun t name args contxt yy-> ExternFun t name (map transformUExpr args) contxt yy- ExternArray t1 t2 name + ExternArray t1 t2 name size idx context yy-> ExternArray t1 t2 name size (transformExpr idx) context yy Op1 op e -> transformOp1 op e Op2 op e1 e2 -> transformOp2 op e1 e2 Op3 op e1 e2 e3 -> transformOp3 op e1 e2 e3 Label t s e -> Label t s $ transformExpr e- -{-showType :: Type a -> String-showType t = case t of- Bool -> "bool"- Int8 -> "int8"- Int16 -> "int16"- Int32 -> "int32"- Int64 -> "int64"- Word8 -> "word8"- Word16-> "word16"- Word32-> "word32"- Word64-> "word64"- Float -> "float"- Double-> "double"-} transformOp1 :: Op1 a b -> Expr a -> Expr b transformOp1 op e = case op of@@ -198,66 +179,66 @@ -- Fractional operators. Recip a -> Op2 (Fdiv a) (Const a 1.0) (transformExpr e) -- Floating operators.- Exp Float -> ExternFun Float "expf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Exp Double -> ExternFun Double "exp" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Sqrt Float -> ExternFun Float "sqrtf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Sqrt Double -> ExternFun Double "sqrt" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Log Float -> ExternFun Float "logf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Log Double -> ExternFun Double "log" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Sin Float -> ExternFun Float "sinf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Sin Double -> ExternFun Double "sin" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Cos Float -> ExternFun Float "cosf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Cos Double -> ExternFun Double "cos" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Tan Float -> ExternFun Float "tanf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Tan Double -> ExternFun Double "tan" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Asin Float -> ExternFun Float "asinf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Asin Double -> ExternFun Double "asin" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Acos Float -> ExternFun Float "acosf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Acos Double -> ExternFun Double "acos" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Atan Float -> ExternFun Float "atanf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Atan Double -> ExternFun Double "atan" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Sinh Float -> ExternFun Float "sinhf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Sinh Double -> ExternFun Double "sinh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Cosh Float -> ExternFun Float "coshf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Cosh Double -> ExternFun Double "cosh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Tanh Float -> ExternFun Float "tanhf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Tanh Double -> ExternFun Double "tanh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Asinh Float -> ExternFun Float "asinhf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Asinh Double -> ExternFun Double "asinh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Acosh Float -> ExternFun Float "acoshf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Acosh Double -> ExternFun Double "acosh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing- Atanh Float -> ExternFun Float "atanhf" - [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing- Atanh Double -> ExternFun Double "atanh" - [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Exp Float -> ExternFun Float "expf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Exp Double -> ExternFun Double "exp"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Sqrt Float -> ExternFun Float "sqrtf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Sqrt Double -> ExternFun Double "sqrt"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Log Float -> ExternFun Float "logf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Log Double -> ExternFun Double "log"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Sin Float -> ExternFun Float "sinf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Sin Double -> ExternFun Double "sin"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Cos Float -> ExternFun Float "cosf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Cos Double -> ExternFun Double "cos"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Tan Float -> ExternFun Float "tanf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Tan Double -> ExternFun Double "tan"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Asin Float -> ExternFun Float "asinf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Asin Double -> ExternFun Double "asin"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Acos Float -> ExternFun Float "acosf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Acos Double -> ExternFun Double "acos"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Atan Float -> ExternFun Float "atanf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Atan Double -> ExternFun Double "atan"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Sinh Float -> ExternFun Float "sinhf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Sinh Double -> ExternFun Double "sinh"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Cosh Float -> ExternFun Float "coshf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Cosh Double -> ExternFun Double "cosh"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Tanh Float -> ExternFun Float "tanhf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Tanh Double -> ExternFun Double "tanh"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Asinh Float -> ExternFun Float "asinhf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Asinh Double -> ExternFun Double "asinh"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Acosh Float -> ExternFun Float "acoshf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Acosh Double -> ExternFun Double "acosh"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing+ -- Atanh Float -> ExternFun Float "atanhf"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Float }] Nothing Nothing+ -- Atanh Double -> ExternFun Double "atanh"+ -- [UExpr { uExprExpr = transformExpr e, uExprType = Double }] Nothing Nothing -- Bitwise operators. BwNot t -> Op1 (BwNot t) $ transformExpr e -- Casting operator.@@ -278,11 +259,11 @@ -- Fractional operators. Fdiv t -> Op2 (Fdiv t) (transformExpr e1) (transformExpr e2) -- Floating operators.- Pow Float -> ExternFun Float "powf" - [UExpr { uExprExpr = transformExpr e1, uExprType = Float } + Pow Float -> ExternFun Float "powf"+ [UExpr { uExprExpr = transformExpr e1, uExprType = Float } , UExpr { uExprExpr = transformExpr e2, uExprType = Float }] Nothing Nothing- Pow Double-> ExternFun Double "pow" - [UExpr { uExprExpr = transformExpr e1, uExprType = Double } + Pow Double-> ExternFun Double "pow"+ [UExpr { uExprExpr = transformExpr e1, uExprType = Double } , UExpr { uExprExpr = transformExpr e2, uExprType = Double }] Nothing Nothing Logb t -> Op2 (Fdiv t) (transformExpr $ Op1 (Log t) e1) (transformExpr $ Op1 (Log t) e2) -- Equality operators.@@ -302,5 +283,5 @@ transformOp3 :: Op3 a b c d -> Expr a -> Expr b -> Expr c -> Expr d-transformOp3 op e1 e2 e3 = case op of - Mux t -> Op3 (Mux t) (transformExpr e1) (transformExpr e2) (transformExpr e3) +transformOp3 op e1 e2 e3 = case op of+ Mux t -> Op3 (Mux t) (transformExpr e1) (transformExpr e2) (transformExpr e3)