copilot-theorem 3.8 → 3.9
raw patch · 33 files changed
+437/−670 lines, 33 filesdep ~copilot-corePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: copilot-core
API changes (from Hackage documentation)
Files
- CHANGELOG +4/−0
- copilot-theorem.cabal +2/−2
- src/Copilot/Theorem.hs +0/−4
- src/Copilot/Theorem/IL.hs +0/−4
- src/Copilot/Theorem/IL/PrettyPrint.hs +3/−8
- src/Copilot/Theorem/IL/Spec.hs +4/−18
- src/Copilot/Theorem/IL/Transform.hs +1/−2
- src/Copilot/Theorem/IL/Translate.hs +54/−54
- src/Copilot/Theorem/Kind2.hs +0/−4
- src/Copilot/Theorem/Kind2/AST.hs +0/−6
- src/Copilot/Theorem/Kind2/Output.hs +1/−7
- src/Copilot/Theorem/Kind2/PrettyPrint.hs +4/−13
- src/Copilot/Theorem/Kind2/Prover.hs +2/−12
- src/Copilot/Theorem/Kind2/Translate.hs +21/−37
- src/Copilot/Theorem/Misc/Error.hs +0/−6
- src/Copilot/Theorem/Misc/SExpr.hs +18/−27
- src/Copilot/Theorem/Misc/Utils.hs +0/−10
- src/Copilot/Theorem/Prove.hs +5/−10
- src/Copilot/Theorem/Prover/Backend.hs +1/−1
- src/Copilot/Theorem/Prover/SMT.hs +21/−26
- src/Copilot/Theorem/Prover/SMTIO.hs +5/−15
- src/Copilot/Theorem/Prover/SMTLib.hs +3/−12
- src/Copilot/Theorem/Prover/TPTP.hs +3/−12
- src/Copilot/Theorem/TransSys.hs +0/−4
- src/Copilot/Theorem/TransSys/Cast.hs +4/−12
- src/Copilot/Theorem/TransSys/Operators.hs +6/−18
- src/Copilot/Theorem/TransSys/PrettyPrint.hs +19/−24
- src/Copilot/Theorem/TransSys/Renaming.hs +0/−8
- src/Copilot/Theorem/TransSys/Spec.hs +8/−24
- src/Copilot/Theorem/TransSys/Transform.hs +1/−19
- src/Copilot/Theorem/TransSys/Translate.hs +7/−30
- src/Copilot/Theorem/TransSys/Type.hs +3/−12
- src/Copilot/Theorem/What4.hs +237/−229
CHANGELOG view
@@ -1,3 +1,7 @@+2022-05-06+ * Version bump (3.9). (#320)+ * Compliance with style guide (partial). (#316)+ 2022-03-07 * Version bump (3.8). (#298) * Mark package as uncurated to avoid modification. (#288)
copilot-theorem.cabal view
@@ -14,7 +14,7 @@ <https://copilot-language.github.io>. -version : 3.8+version : 3.9 license : BSD3 license-file : LICENSE maintainer : Ivan Perez <ivan.perezdominguez@nasa.gov>@@ -74,7 +74,7 @@ , xml >= 1.3 && < 1.4 , what4 >= 1.1 && < 1.3 - , copilot-core >= 3.8 && < 3.9+ , copilot-core >= 3.9 && < 3.10 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove
src/Copilot/Theorem.hs view
@@ -1,5 +1,3 @@---------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} -- | Highly automated proof techniques are a necessary step for the widespread@@ -22,5 +20,3 @@ import Copilot.Theorem.Tactics as X import Copilot.Theorem.Prove----------------------------------------------------------------------------------
src/Copilot/Theorem/IL.hs view
@@ -1,5 +1,3 @@---------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} -- | Each prover first translates the Copilot specification into an@@ -16,5 +14,3 @@ import Copilot.Theorem.IL.Translate as X import Copilot.Theorem.IL.Transform as X import Copilot.Theorem.IL.PrettyPrint as X----------------------------------------------------------------------------------
src/Copilot/Theorem/IL/PrettyPrint.hs view
@@ -1,7 +1,6 @@------------------------------------------------------------------------------------{-# LANGUAGE NamedFieldPuns, GADTs #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE Safe #-} -- | This module implements a pretty printer for the IL format, an intermediate -- representation used in copilot-theorem to facilitate model checking.@@ -13,8 +12,6 @@ import Prelude hiding ((<>)) ---------------------------------------------------------------------------------- -- | Pretty print an IL specification. prettyPrint :: IL -> String prettyPrint = render . ppSpec@@ -87,5 +84,3 @@ ppOp2 :: Op2 -> Doc ppOp2 = text . show----------------------------------------------------------------------------------
src/Copilot/Theorem/IL/Spec.hs view
@@ -1,7 +1,7 @@-----------------------------------------------------------------------------------{-# LANGUAGE ExistentialQuantification, GADTs, LambdaCase #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE Safe #-} -- | This module implements the specification language for the IL format, an -- intermediate representation used in copilot-theorem to facilitate model@@ -35,8 +35,6 @@ import Data.Map (Map) import Data.Function (on) ---------------------------------------------------------------------------------- -- | Identifier of a sequence. type SeqId = String @@ -77,8 +75,6 @@ | FunApp Type String [Expr] -- ^ Function application. deriving (Eq, Ord, Show) ---------------------------------------------------------------------------------- -- | A description of a variable (or function) together with its type. data VarDescr = VarDescr { varName :: String@@ -92,8 +88,6 @@ instance Ord VarDescr where compare = compare `on` varName ---------------------------------------------------------------------------------- -- | Identifier for a property. type PropId = String @@ -111,8 +105,6 @@ , inductive :: Bool } ---------------------------------------------------------------------------------- -- | Unary operators. data Op1 = Not | Neg | Abs | Exp | Sqrt | Log | Sin | Tan | Cos | Asin | Atan | Acos | Sinh | Tanh | Cosh | Asinh | Atanh | Acosh@@ -122,8 +114,6 @@ data Op2 = Eq | And | Or | Le | Lt | Ge | Gt | Add | Sub | Mul | Mod | Fdiv | Pow deriving (Eq, Ord) --------------------------------------------------------------------------------- instance Show Op1 where show op = case op of Neg -> "-"@@ -167,8 +157,6 @@ Lt -> "<" Gt -> ">" --------------------------------------------------------------------------------- -- | Return the type of an expression. typeOf :: Expr -> Type typeOf e = case e of@@ -202,5 +190,3 @@ evalAt _ e@(SVal _ _ (Fixed _)) = e evalAt (Fixed n) (SVal t s (Var d)) = SVal t s (Fixed $ n + d) evalAt (Var k) (SVal t s (Var d)) = SVal t s (Var $ k + d)----------------------------------------------------------------------------------
src/Copilot/Theorem/IL/Transform.hs view
@@ -1,5 +1,5 @@ {-# LANGUAGE LambdaCase #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE Safe #-} -- | Simplify IL expressions by partly evaluating operations on booleans. module Copilot.Theorem.IL.Transform ( bsimpl ) where@@ -45,4 +45,3 @@ FunApp t f args -> FunApp t f (map bsimpl' args) e -> e-
src/Copilot/Theorem/IL/Translate.hs view
@@ -1,8 +1,9 @@-----------------------------------------------------------------------------------{-# LANGUAGE RankNTypes, NamedFieldPuns, ScopedTypeVariables, GADTs,- LambdaCase #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-} -- | Translate Copilot specifications into IL specifications. module Copilot.Theorem.IL.Translate ( translate, translateWithBounds ) where@@ -24,8 +25,6 @@ import Data.Typeable (Typeable) ---------------------------------------------------------------------------------- -- 'nc' stands for naming convention. ncSeq :: C.Id -> SeqId ncSeq = printf "s%d"@@ -43,8 +42,6 @@ ncMux :: Integer -> SeqId ncMux n = "mux" ++ show n ---------------------------------------------------------------------------------- -- | Translate a Copilot specification to an IL specification. translate :: C.Spec -> IL translate = translate' False@@ -88,22 +85,24 @@ C.Word32 -> bound' C.Word32 C.Word64 -> bound' C.Word64 _ -> return ()- where bound' :: (Bounded a, Integral a) => C.Type a -> Trans ()- bound' t = do- b <- addBounds <$> get- when b $ localConstraint (Op2 Bool And- (Op2 Bool Le (trConst t minBound) s)- (Op2 Bool Ge (trConst t maxBound) s))+ where+ bound' :: (Bounded a, Integral a) => C.Type a -> Trans ()+ bound' t = do+ b <- addBounds <$> get+ when b $ localConstraint (Op2 Bool And+ (Op2 Bool Le (trConst t minBound) s)+ (Op2 Bool Ge (trConst t maxBound) s)) streamInit :: C.Stream -> [Expr] streamInit (C.Stream { C.streamId = id , C.streamBuffer = b :: [val] , C.streamExprType = t }) = zipWith initConstraint [0..] b- where initConstraint :: Integer -> val -> Expr- initConstraint p v = Op2 Bool Eq- (SVal (trType t) (ncSeq id) (Fixed p))- $ trConst t v+ where+ initConstraint :: Integer -> val -> Expr+ initConstraint p v = Op2 Bool Eq+ (SVal (trType t) (ncSeq id) (Fixed p))+ $ trConst t v streamRec :: C.Stream -> Trans Expr streamRec (C.Stream { C.streamId = id@@ -116,8 +115,6 @@ e' <- expr e return $ Op2 Bool Eq s e' ---------------------------------------------------------------------------------- expr :: Typeable a => C.Expr a -> Trans Expr expr (C.Const t v) = return $ trConst t v@@ -134,7 +131,8 @@ expr (C.Var t name) = return $ SVal (trType t) (ncLocal name) _n_ expr (C.ExternVar t name _) = bound s t >> return s- where s = SVal (trType t) (ncExternVar name) _n_+ where+ s = SVal (trType t) (ncExternVar name) _n_ expr (C.Op1 (C.Sign ta) e) = case ta of C.Int8 -> trSign ta e@@ -144,15 +142,16 @@ C.Float -> trSign ta e C.Double -> trSign ta e _ -> expr $ C.Const ta 1- where trSign :: (Typeable a, Ord a, Num a) => C.Type a -> C.Expr a -> Trans Expr- trSign ta e =- expr (C.Op3 (C.Mux ta)- (C.Op2 (C.Lt ta) e (C.Const ta 0))- (C.Const ta (-1))- (C.Op3 (C.Mux ta)- (C.Op2 (C.Gt ta) e (C.Const ta 0))- (C.Const ta 1)- (C.Const ta 0)))+ where+ trSign :: (Typeable a, Ord a, Num a) => C.Type a -> C.Expr a -> Trans Expr+ trSign ta e =+ expr (C.Op3 (C.Mux ta)+ (C.Op2 (C.Lt ta) e (C.Const ta 0))+ (C.Const ta (-1))+ (C.Op3 (C.Mux ta)+ (C.Op2 (C.Gt ta) e (C.Const ta 0))+ (C.Const ta 1)+ (C.Const ta 0))) expr (C.Op1 (C.Sqrt _) e) = do e' <- expr e return $ Op2 Real Pow e' (ConstR 0.5)@@ -160,19 +159,22 @@ expr (C.Op1 op e) = do e' <- expr e return $ Op1 t' op' e'- where (op', t') = trOp1 op+ where+ (op', t') = trOp1 op expr (C.Op2 (C.Ne t) e1 e2) = do e1' <- expr e1 e2' <- expr e2 return $ Op1 Bool Not (Op2 t' Eq e1' e2')- where t' = trType t+ where+ t' = trType t expr (C.Op2 op e1 e2) = do e1' <- expr e1 e2' <- expr e2 return $ Op2 t' op' e1' e2'- where (op', t') = trOp2 op+ where+ (op', t') = trOp2 op expr (C.Op3 (C.Mux t) cond e1 e2) = do cond' <- expr cond@@ -193,14 +195,15 @@ t@C.Word16 -> negifyI v (trType t) t@C.Word32 -> negifyI v (trType t) t@C.Word64 -> negifyI v (trType t)- where negifyR :: Double -> Expr- negifyR v- | v >= 0 = ConstR v- | otherwise = Op1 Real Neg $ ConstR $ negate $ v- negifyI :: Integral a => a -> Type -> Expr- negifyI v t- | v >= 0 = ConstI t $ toInteger v- | otherwise = Op1 t Neg $ ConstI t $ negate $ toInteger v+ where+ negifyR :: Double -> Expr+ negifyR v+ | v >= 0 = ConstR v+ | otherwise = Op1 Real Neg $ ConstR $ negate $ v+ negifyI :: Integral a => a -> Type -> Expr+ negifyI v t+ | v >= 0 = ConstI t $ toInteger v+ | otherwise = Op1 t Neg $ ConstI t $ negate $ toInteger v trOp1 :: C.Op1 a b -> (Op1, Type) trOp1 = \case@@ -225,7 +228,7 @@ C.Acosh t -> (Acosh, trType t) -- C.BwNot t -> -- C.Cast t ->- _ -> error "Unsupported unary operator in input." -- TODO(chathhorn)+ _ -> error "Unsupported unary operator in input." trOp2 :: C.Op2 a b c -> (Op2, Type) trOp2 = \case@@ -258,7 +261,7 @@ -- C.BwShiftL t _ -> -- C.BwShiftR t _ -> - _ -> error "Unsupported binary operator in input." -- TODO(chathhorn)+ _ -> error "Unsupported binary operator in input." trType :: C.Type a -> Type trType = \case@@ -274,8 +277,6 @@ C.Float -> Real C.Double -> Real ---------------------------------------------------------------------------------- -- | Translation state. data TransST = TransST { localConstraints :: [Expr]@@ -294,14 +295,16 @@ modify $ \st -> st { muxes = (v, mux) : ms } return v Just (v, _) -> return v- where mux = (c, t, e1, e2)+ where+ mux = (c, t, e1, e2) getMuxes :: Trans [Expr] getMuxes = muxes <$> get >>= return . concat . (map toConstraints)- where toConstraints (v, (c, _, e1, e2)) =- [ Op2 Bool Or (Op1 Bool Not c) (Op2 Bool Eq v e1)- , Op2 Bool Or c (Op2 Bool Eq v e2)- ]+ where+ toConstraints (v, (c, _, e1, e2)) =+ [ Op2 Bool Or (Op1 Bool Not c) (Op2 Bool Eq v e1)+ , Op2 Bool Or c (Op2 Bool Eq v e2)+ ] -- | A state monad over the translation state ('TransST'). type Trans = State TransST@@ -321,6 +324,3 @@ runTrans :: Bool -> Trans a -> a runTrans b m = evalState m $ TransST [] [] 0 b-----------------------------------------------------------------------------------
src/Copilot/Theorem/Kind2.hs view
@@ -1,5 +1,3 @@---------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} -- | Copilot backend for the <https://kind2-mc.github.io/kind2/ Kind 2> SMT@@ -11,5 +9,3 @@ import Copilot.Theorem.Kind2.Translate as X import Copilot.Theorem.Kind2.PrettyPrint as X import Copilot.Theorem.Kind2.Prover as X----------------------------------------------------------------------------------
src/Copilot/Theorem/Kind2/AST.hs view
@@ -1,12 +1,8 @@---------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} -- | Abstract syntax tree of Kind2 files. module Copilot.Theorem.Kind2.AST where ---------------------------------------------------------------------------------- -- | A file is a sequence of predicates and propositions. data File = File { filePreds :: [PredDef]@@ -54,5 +50,3 @@ | StateVar String | FunApp String [Term] | PredApp String PredType [Term]----------------------------------------------------------------------------------
src/Copilot/Theorem/Kind2/Output.hs view
@@ -1,7 +1,5 @@---------------------------------------------------------------------------------- {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE Safe #-} -- | Parse output of Kind2. module Copilot.Theorem.Kind2.Output (parseOutput) where@@ -12,8 +10,6 @@ import qualified Copilot.Theorem.Misc.Error as Err ---------------------------------------------------------------------------------- simpleName s = QName s Nothing Nothing -- | Parse output of Kind2.@@ -52,5 +48,3 @@ err msg = Err.fatal $ "Parse error while reading the Kind2 XML output : \n" ++ msg ++ "\n\n" ++ xml----------------------------------------------------------------------------------
src/Copilot/Theorem/Kind2/PrettyPrint.hs view
@@ -1,5 +1,3 @@---------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} -- | Pretty print a Kind2 file defining predicates and propositions.@@ -11,16 +9,12 @@ import Data.List (intercalate) ---------------------------------------------------------------------------------- -- | A tree of expressions, in which the leafs are strings. type SSExpr = SExpr String -- | Reserved keyword prime. kwPrime = "prime" ---------------------------------------------------------------------------------- -- | Pretty print a Kind2 file. prettyPrint :: File -> String prettyPrint =@@ -34,8 +28,6 @@ shouldIndent (List [Atom a, Atom _]) = a `notElem` [kwPrime] shouldIndent _ = True ---------------------------------------------------------------------------------- -- | Convert a file into a sequence of expressions. ppFile :: File -> [SSExpr] ppFile (File preds props) = map ppPredDef preds ++ ppProps props@@ -75,8 +67,7 @@ ppTerm (StateVar v) = atom v ppTerm (FunApp f args) = node f $ map ppTerm args ppTerm (PredApp p t args) = node (p ++ "." ++ ext) $ map ppTerm args- where ext = case t of- Init -> "init"- Trans -> "trans"----------------------------------------------------------------------------------+ where+ ext = case t of+ Init -> "init"+ Trans -> "trans"
src/Copilot/Theorem/Kind2/Prover.hs view
@@ -1,6 +1,4 @@-----------------------------------------------------------------------------------{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE Trustworthy #-} -- | A prover backend based on Kind2.@@ -26,8 +24,6 @@ import qualified Copilot.Theorem.TransSys as TS ---------------------------------------------------------------------------------- -- | Options for Kind2 data Options = Options { bmcMax :: Int -- ^ Upper bound on the number of unrolling that base and@@ -52,13 +48,9 @@ , askProver = askKind2 , closeProver = const $ return () } ---------------------------------------------------------------------------------- kind2Prog = "kind2" kind2BaseOptions = ["--input-format", "native", "-xml"] ---------------------------------------------------------------------------------- askKind2 :: ProverST -> [PropId] -> [PropId] -> IO Output askKind2 (ProverST opts spec) assumptions toCheck = do @@ -76,6 +68,4 @@ putStrLn kind2Input removeFile tempName- return $ parseOutput (head toCheck) output -- TODO support multiple toCheck props----------------------------------------------------------------------------------+ return $ parseOutput (head toCheck) output
src/Copilot/Theorem/Kind2/Translate.hs view
@@ -1,7 +1,8 @@-----------------------------------------------------------------------------------{-# LANGUAGE RankNTypes, ViewPatterns, NamedFieldPuns, GADTs #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ViewPatterns #-} -- | Convert modular transition systems ('TransSys') into Kind2 file -- specifications.@@ -24,20 +25,14 @@ import qualified Data.Map as Map import qualified Data.Bimap as Bimap ---------------------------------------------------------------------------------- -- The following properties MUST hold for the given transition system : -- * Nodes are sorted by topological order -- * Nodes are `completed`, which means the dependency graph is transitive -- and each node imports all the local variables of its dependencies -- ---------------------------------------------------------------------------------- type DepGraph = Map NodeId [NodeId] ---------------------------------------------------------------------------------- -- | Style of the Kind2 files produced: modular (with multiple separate nodes), -- or all inlined (with only one node). --@@ -58,17 +53,19 @@ toKind2 style assumptions checkedProps spec = addAssumptions spec assumptions $ trSpec (complete spec') predCallsGraph assumptions checkedProps- where predCallsGraph = specDependenciesGraph spec'- spec' = case style of- Inlined -> inline spec- Modular -> removeCycles spec+ where+ predCallsGraph = specDependenciesGraph spec'+ spec' = case style of+ Inlined -> inline spec+ Modular -> removeCycles spec trSpec :: TransSys -> DepGraph -> [PropId] -> [PropId] -> K.File trSpec spec predCallsGraph _assumptions checkedProps = K.File preds props- where preds = map (trNode spec predCallsGraph) (specNodes spec)- props = map trProp $- filter ((`elem` checkedProps) . fst) $- Map.toList (specProps spec)+ where+ preds = map (trNode spec predCallsGraph) (specNodes spec)+ props = map trProp $+ filter ((`elem` checkedProps) . fst) $+ Map.toList (specProps spec) trProp :: (PropId, ExtVar) -> K.Prop trProp (pId, var) = K.Prop pId (trVar . extVarLocalPart $ var)@@ -86,7 +83,6 @@ ++ map (trExpr True) (nodeConstrs node) ++ predCalls False spec predCallsGraph node - addAssumptions :: TransSys -> [PropId] -> K.File -> K.File addAssumptions spec assumptions (K.File {K.filePreds, K.fileProps}) = K.File (changeTail aux filePreds) fileProps@@ -106,15 +102,12 @@ toTopVar (ExtVar nId v) = assert (nId == specTopNodeId spec) v in map (varName . toTopVar . toExtVar) assumptions -----------------------------------------------------------------------------------{- The ordering really matters here because the variables- have to be given in this order in a pred call- Our convention :- * First the local variables, sorted by alphabetical order- * Then the imported variables, by alphabetical order on- the father node then by alphabetical order on the variable name--}+-- The ordering really matters here because the variables+-- have to be given in this order in a pred call+-- Our convention :+-- * First the local variables, sorted by alphabetical order+-- * Then the imported variables, by alphabetical order on+-- the father node then by alphabetical order on the variable name gatherPredStateVars :: TransSys -> Node -> [K.StateVarDef] gatherPredStateVars spec node = locals ++ imported@@ -136,8 +129,6 @@ map (\(v, ev) -> K.StateVarDef (varName v) (extVarType ev) []) . sortBy (compare `on` snd) . Bimap.toList $ nodeImportedVars node ---------------------------------------------------------------------------------- mkConj :: [K.Term] -> K.Term mkConj [] = trConst Bool True mkConj [x] = x@@ -158,8 +149,6 @@ trConst Bool True = K.ValueLiteral "true" trConst Bool False = K.ValueLiteral "false" ---------------------------------------------------------------------------------- initLocals :: Node -> [K.Term] initLocals node = concatMap f (Map.toList $ nodeLocalVars node)@@ -170,7 +159,6 @@ Expr e -> [mkEquality (trVar v) (trExpr False e)] Constrs cs -> map (trExpr False) cs - transLocals :: Node -> [K.Term] transLocals node = concatMap f (Map.toList $ nodeLocalVars node)@@ -214,8 +202,6 @@ argsSeq trVarF = map (localAlias trVarF) (calleeLocals ++ calleeImported) ---------------------------------------------------------------------------------- trExpr :: Bool -> Expr t -> K.Term trExpr primed = tr where@@ -225,5 +211,3 @@ tr (Op1 _ op e) = K.FunApp (show op) [tr e] tr (Op2 _ op e1 e2) = K.FunApp (show op) [tr e1, tr e2] tr (VarE _ v) = if primed then trPrimedVar v else trVar v----------------------------------------------------------------------------------
src/Copilot/Theorem/Misc/Error.hs view
@@ -1,5 +1,3 @@---------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} -- | Custom functions to report error messages to users.@@ -10,8 +8,6 @@ , fatal ) where ---------------------------------------------------------------------------------- -- | Tag used with error messages to help users locate the component that -- failed or reports the error. errorHeader :: String@@ -34,5 +30,3 @@ -- | Report an unrecoverable error (e.g., incorrect format). fatal :: String -> a fatal = error----------------------------------------------------------------------------------
src/Copilot/Theorem/Misc/SExpr.hs view
@@ -1,7 +1,5 @@---------------------------------------------------------------------------------- {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE Safe #-} -- | A representation for structured expression trees, with support for pretty -- printing and for parsing.@@ -12,8 +10,6 @@ import Control.Monad ---------------------------------------------------------------------------------- -- | A structured expression is either an atom, or a sequence of expressions, -- where the first in the sequence denotes the tag or label of the tree. data SExpr a = Atom a@@ -38,8 +34,6 @@ -- additional expressions or arguments.. node a l = List (Atom a : l) -- (s ss) ---------------------------------------------------------------------------------- -- A straightforward string representation for 'SExpr's of Strings that -- parenthesizes lists of expressions. instance Show (SExpr String) where@@ -48,7 +42,6 @@ show' (Atom s) = text s show' (List ts) = parens . hsep . map show' $ ts - -- More advanced printing with some basic indentation -- | Indent by a given number.@@ -71,13 +64,12 @@ Atom a -> text (printAtom a) List l -> parens (foldl renderItem empty l) - where renderItem doc s- | shouldIndent s =- doc $$ indent (toDoc shouldIndent printAtom s)- | otherwise =- doc <+> toDoc shouldIndent printAtom s----------------------------------------------------------------------------------+ where+ renderItem doc s+ | shouldIndent s =+ doc $$ indent (toDoc shouldIndent printAtom s)+ | otherwise =+ doc <+> toDoc shouldIndent printAtom s -- | Parser for strings of characters separated by spaces into a structured -- tree.@@ -88,19 +80,20 @@ parser = choice [try unitP, nodeP, leafP] - where symbol = oneOf "!#$%&|*+-/:<=>?@^_~."- lonelyStr = many1 (alphaNum <|> symbol)+ where+ symbol = oneOf "!#$%&|*+-/:<=>?@^_~."+ lonelyStr = many1 (alphaNum <|> symbol) - unitP = string "()" >> return unit+ unitP = string "()" >> return unit - leafP = atom <$> lonelyStr+ leafP = atom <$> lonelyStr - nodeP = do void $ char '('- spaces- st <- sepBy parser spaces- spaces- void $ char ')'- return $ List st+ nodeP = do void $ char '('+ spaces+ st <- sepBy parser spaces+ spaces+ void $ char ')'+ return $ List st -- | Parser for strings of characters separated by spaces into a structured -- tree.@@ -111,5 +104,3 @@ parseSExpr str = case parse parser "" str of Left s -> error (show s) -- Nothing Right t -> Just t----------------------------------------------------------------------------------
src/Copilot/Theorem/Misc/Utils.hs view
@@ -1,5 +1,3 @@---------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} -- | Utility / auxiliary functions.@@ -8,8 +6,6 @@ , openTempFile ) where ---------------------------------------------------------------------------------- import Data.Function (on) import Data.List (groupBy, sortBy, group, sort) @@ -22,8 +18,6 @@ import System.Random import System.Directory ---------------------------------------------------------------------------------- -- | True if the given list is a subset of the second list, when both are -- considered as sets. isSublistOf :: Ord a => [a] -> [a] -> Bool@@ -46,8 +40,6 @@ nubBy' :: (a -> a -> Ordering) -> [a] -> [a] nubBy' f = map head . groupBy (\x y -> f x y == EQ) . sortBy f ---------------------------------------------------------------------------------- -- | Create a temporary file and open it for writing. openTempFile :: String -- ^ Directory where the file should be created. -> String -- ^ Base name for the file (prefix).@@ -72,5 +64,3 @@ pathFromSuff :: String -> FilePath pathFromSuff suf = loc ++ "/" ++ baseName ++ suf ++ "." ++ extension----------------------------------------------------------------------------------
src/Copilot/Theorem/Prove.hs view
@@ -1,7 +1,8 @@-----------------------------------------------------------------------------------{-# LANGUAGE NamedFieldPuns, ViewPatterns, ExistentialQuantification, GADTs #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ViewPatterns #-} -- | Connection to theorem provers. module Copilot.Theorem.Prove@@ -23,8 +24,6 @@ import Control.Applicative (liftA2) import Control.Monad.Writer ---------------------------------------------------------------------------------- -- | Output produced by a prover, containing the 'Status' of the proof and -- additional information. data Output = Output Status [String]@@ -92,8 +91,6 @@ Assume :: PropId -> Action Admit :: Action ---------------------------------------------------------------------------------- -- | Record a requirement for satisfiability checking. check :: Prover -> Proof a check prover = Proof $ tell [Check prover]@@ -214,5 +211,3 @@ ++ msgL ++ [decoName nameR] ++ msgR----------------------------------------------------------------------------------
src/Copilot/Theorem/Prover/Backend.hs view
@@ -1,5 +1,5 @@ {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE Safe #-} -- | Backend to SMT solvers and theorem provers. --
src/Copilot/Theorem/Prover/SMT.hs view
@@ -1,7 +1,9 @@-----------------------------------------------------------------------------------{-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs #-}-{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Trustworthy #-} -- | Connections to various SMT solvers and theorem provers. module Copilot.Theorem.Prover.SMT@@ -50,8 +52,6 @@ import System.IO (hClose) ---------------------------------------------------------------------------------- -- * Tactics -- | Options to configure the provers.@@ -115,8 +115,6 @@ , P.closeProver = const $ return () } --------------------------------------------------------------------------------- -- * Backends -- | Backend to the Yices 2 SMT solver.@@ -238,8 +236,6 @@ , interpret = TPTP.interpret } --------------------------------------------------------------------------------- -- | Checks the Copilot specification with k-induction type ProofScript b = MaybeT (StateT (ProofState b) IO)@@ -331,18 +327,19 @@ getVars :: [Expr] -> [VarDescr] getVars = nubBy' (compare `on` varName) . concatMap getVars'- where getVars' :: Expr -> [VarDescr]- getVars' = \case- ConstB _ -> []- ConstI _ _ -> []- ConstR _ -> []- Ite _ e1 e2 e3 -> getVars' e1 ++ getVars' e2 ++ getVars' e3- Op1 _ _ e -> getVars' e- Op2 _ _ e1 e2 -> getVars' e1 ++ getVars' e2- SVal t seq (Fixed i) -> [VarDescr (seq ++ "_" ++ show i) t []]- SVal t seq (Var i) -> [VarDescr (seq ++ "_n" ++ show i) t []]- FunApp t name args -> [VarDescr name t (map typeOf args)]- ++ concatMap getVars' args+ where+ getVars' :: Expr -> [VarDescr]+ getVars' = \case+ ConstB _ -> []+ ConstI _ _ -> []+ ConstR _ -> []+ Ite _ e1 e2 e3 -> getVars' e1 ++ getVars' e2 ++ getVars' e3+ Op1 _ _ e -> getVars' e+ Op2 _ _ e1 e2 -> getVars' e1 ++ getVars' e2+ SVal t seq (Fixed i) -> [VarDescr (seq ++ "_" ++ show i) t []]+ SVal t seq (Var i) -> [VarDescr (seq ++ "_n" ++ show i) t []]+ FunApp t name args -> [VarDescr name t (map typeOf args)]+ ++ concatMap getVars' args unknown :: ProofScript b a unknown = mzero@@ -383,7 +380,6 @@ Unknown -> unknown Unsat -> valid $ "proved with " ++ proofKind k - onlySat' :: SmtFormat b => ProofState b -> [PropId] -> [PropId] -> IO Output onlySat' s as ps = (fromJust . fst) <$> runPS (script <* stopSolvers) s where@@ -419,6 +415,5 @@ selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr]) selectProps propIds properties = (squash . unzip) [(as, p) | (id, (as, p)) <- Map.toList properties, id `elem` propIds]- where squash (a, b) = (concat a, b)----------------------------------------------------------------------------------+ where+ squash (a, b) = (concat a, b)
src/Copilot/Theorem/Prover/SMTIO.hs view
@@ -1,7 +1,8 @@-----------------------------------------------------------------------------------{-# LANGUAGE LambdaCase, NamedFieldPuns, RankNTypes, ViewPatterns #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ViewPatterns #-} -- | Communication with SMT solvers or theorem provers. --@@ -23,8 +24,6 @@ import Data.Maybe import Data.Set ((\\), fromList, Set, union, empty, elems) ---------------------------------------------------------------------------------- -- | A connection with a running SMT solver or theorem prover. data Solver a = Solver { solverName :: String@@ -37,8 +36,6 @@ , backend :: Backend a } ---------------------------------------------------------------------------------- -- | Output a debugging message if debugging is enabled for the solver. debug :: Bool -> Solver a -> String -> IO () debug printName s str = when (debugMode s) $@@ -64,8 +61,6 @@ liftIO $ debug True s $ "[received: " ++ ln ++ "]" MaybeT $ return $ (interpret $ backend s) ln ---------------------------------------------------------------------------------- -- | Create a new solver implemented by the backend specified. -- -- The error handle from the backend handle is immediately closed/discarded,@@ -86,8 +81,6 @@ hClose $ outh s terminateProcess $ process s ---------------------------------------------------------------------------------- -- | Register the given expressions as assumptions or axioms with the solver. assume :: SmtFormat a => Solver a -> [Expr] -> IO (Solver a) assume s@(Solver { model }) cs = do@@ -119,6 +112,3 @@ forM_ newVars $ \(VarDescr {varName, varType, args}) -> send s $ declFun varName varType args return s { vars = vars `union` fromList newVars }-----------------------------------------------------------------------------------
src/Copilot/Theorem/Prover/SMTLib.hs view
@@ -1,7 +1,6 @@-----------------------------------------------------------------------------------{-# LANGUAGE GADTs, FlexibleInstances #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE Safe #-} -- | A backend to the SMT-Lib format, enabling to produce commands for SMT-Lib -- implementing solvers, and parse results.@@ -14,8 +13,6 @@ import Text.Printf ---------------------------------------------------------------------------------- -- | Type used to represent SMT-lib commands. -- -- Use the interface in 'SmtFormat' to create such commands.@@ -29,8 +26,6 @@ smtTy Real = "Real" smtTy _ = "Int" ---------------------------------------------------------------------------------- -- | Interface for SMT-Lib conforming backends. instance SmtFormat SmtLib where push = SmtLib $ node "push" [atom "1"]@@ -48,8 +43,6 @@ interpret "unsat" = Just Unsat interpret _ = Just Unknown ---------------------------------------------------------------------------------- expr :: Expr -> SExpr String expr (ConstB v) = atom $ if v then "true" else "false"@@ -104,5 +97,3 @@ expr (SVal _ f ix) = atom $ case ix of Fixed i -> f ++ "_" ++ show i Var off -> f ++ "_n" ++ show off----------------------------------------------------------------------------------
src/Copilot/Theorem/Prover/TPTP.hs view
@@ -1,7 +1,6 @@-----------------------------------------------------------------------------------{-# LANGUAGE GADTs, LambdaCase #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE Safe #-} -- | A backend to <http://www.tptp.org/ TPTP>, enabling to produce assertions -- and to parse the results from TPTP.@@ -12,8 +11,6 @@ import Data.List ---------------------------------------------------------------------------------- -- | Type used to represent TPTP expressions. -- -- Although this type implements the 'SmtFormat' interface, only 'assert' is@@ -33,8 +30,6 @@ show (Atom atom) = atom show (Fun name args) = name ++ "(" ++ intercalate ", " (map show args) ++ ")" ---------------------------------------------------------------------------------- instance SmtFormat Tptp where push = Null pop = Null@@ -50,8 +45,6 @@ | "SZS status" `isPrefixOf` str = Just Unknown | otherwise = Nothing ---------------------------------------------------------------------------------- expr :: Expr -> TptpExpr expr = \case ConstB v -> Atom $ if v then "$true" else "$false"@@ -109,5 +102,3 @@ Mod -> "mod" Fdiv -> "/" Pow -> "^"----------------------------------------------------------------------------------
src/Copilot/Theorem/TransSys.hs view
@@ -1,5 +1,3 @@---------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} -- | Each prover first translates the Copilot specification into an@@ -17,5 +15,3 @@ import Copilot.Theorem.TransSys.PrettyPrint as X import Copilot.Theorem.TransSys.Translate as X import Copilot.Theorem.TransSys.Transform as X----------------------------------------------------------------------------------
src/Copilot/Theorem/TransSys/Cast.hs view
@@ -1,7 +1,7 @@-----------------------------------------------------------------------------------{-# LANGUAGE RankNTypes, ScopedTypeVariables, GADTs #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-} -- | Casting of values with dynamic types and translating from Copilot core -- types to Copilot theorem types.@@ -14,8 +14,6 @@ , casting ) where ---------------------------------------------------------------------------------- import Copilot.Core as C import Data.Dynamic (Dynamic(..), fromDynamic, toDyn)@@ -23,8 +21,6 @@ import qualified Copilot.Theorem.TransSys.Type as K ---------------------------------------------------------------------------------- -- | Synonym for a dynamic type in Copilot core. type Dyn = Dynamic @@ -60,8 +56,6 @@ K.U K.Integer -> f K.Integer K.U K.Real -> f K.Real ---------------------------------------------------------------------------------- class Casted b where _cast :: Dyn -> Maybe b @@ -87,5 +81,3 @@ | Just (v :: Float) <- fromDynamic d = Just $ float2Double v | Just (v :: Double) <- fromDynamic d = Just v | otherwise = Nothing----------------------------------------------------------------------------------
src/Copilot/Theorem/TransSys/Operators.hs view
@@ -1,8 +1,9 @@-----------------------------------------------------------------------------------{-# LANGUAGE GADTs, ExistentialQuantification, LambdaCase, ScopedTypeVariables,- RankNTypes #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-} -- | Operators in modular transition systems and their translation. module Copilot.Theorem.TransSys.Operators where@@ -13,8 +14,6 @@ import Copilot.Theorem.Misc.Error as Err ---------------------------------------------------------------------------------- -- | Unary operators. data Op1 a where Not :: Op1 Bool@@ -55,8 +54,6 @@ Pow :: (Num a) => Op2 a a --------------------------------------------------------------------------------- instance Show (Op1 a) where show op = case op of Neg -> "-"@@ -94,8 +91,6 @@ Fdiv -> "/" Pow -> "^" --------------------------------------------------------------------------------- -- | Unhandled unary operator. -- -- Unhandled operators are monomorphic, and their names are labeled so that@@ -195,8 +190,6 @@ notHandled ta s = casting ta $ \ta' -> notHandledF $ UnhandledOp1 s ta' resT ---------------------------------------------------------------------------------- -- | Translate an Op2. -- -- This function is parameterized so that it can be used to translate@@ -228,7 +221,6 @@ -> m (expr resT) - handleOp2 resT (op, e1, e2) handleExpr notHandledF mkOp notOp = case op of C.And -> boolConnector And@@ -328,10 +320,6 @@ notHandled ta s = casting ta $ \ta' -> notHandledF (UnhandledOp2 s ta' ta' ta') ---------------------------------------------------------------------------------- -- | Error message for unexpected behavior / internal errors. typeErrMsg :: String typeErrMsg = "Unexpected type error in 'Misc.CoreOperators'"----------------------------------------------------------------------------------
src/Copilot/Theorem/TransSys/PrettyPrint.hs view
@@ -1,7 +1,6 @@-----------------------------------------------------------------------------------{-# LANGUAGE NamedFieldPuns, GADTs #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE Safe #-} -- | Pretty print a TransSys specification as a Kind2/Lustre specification. module Copilot.Theorem.TransSys.PrettyPrint ( prettyPrint ) where@@ -15,8 +14,6 @@ import Prelude hiding ((<>)) ---------------------------------------------------------------------------------- indent = nest 4 emptyLine = text "" @@ -82,24 +79,24 @@ pLVar :: Var -> VarDescr -> Doc pLVar l (VarDescr {varType, varDef}) = header $$ indent body- where header =- text (varName l)- <+> text ":"- <+> pType varType- <+> text "="-- body = case varDef of- Pre val var ->- pConst varType val- <+> text "->" <+> text "pre"- <+> text (varName var)- Expr e -> pExpr e+ where+ header =+ text (varName l)+ <+> text ":"+ <+> pType varType+ <+> text "=" - Constrs cs ->- text "{"- <+> (hsep . punctuate (space <> text ";" <> space)) (map pExpr cs)- <+> text "}"+ body = case varDef of+ Pre val var ->+ pConst varType val+ <+> text "->" <+> text "pre"+ <+> text (varName var)+ Expr e -> pExpr e + Constrs cs ->+ text "{"+ <+> (hsep . punctuate (space <> text ";" <> space)) (map pExpr cs)+ <+> text "}" pExpr :: Expr t -> Doc @@ -122,5 +119,3 @@ pOp2 :: Op2 a b -> Doc pOp2 = text . show----------------------------------------------------------------------------------
src/Copilot/Theorem/TransSys/Renaming.hs view
@@ -1,5 +1,3 @@---------------------------------------------------------------------------------- {-# LANGUAGE Safe #-} -- | A monad capable of keeping track of variable renames and of providing@@ -25,8 +23,6 @@ import qualified Data.Set as Set import qualified Data.List as List ---------------------------------------------------------------------------------- -- | A monad capable of keeping track of variable renames and of providing -- fresh names for variables. type Renaming = State RenamingST@@ -36,8 +32,6 @@ { _reservedNames :: Set Var , _renaming :: Map ExtVar Var } ---------------------------------------------------------------------------------- -- | Register a name as reserved or used. addReservedName :: Var -> Renaming () addReservedName v = modify $ \st ->@@ -86,5 +80,3 @@ r <- m f <- getRenamingF return (r, f)----------------------------------------------------------------------------------
src/Copilot/Theorem/TransSys/Spec.hs view
@@ -1,7 +1,7 @@-----------------------------------------------------------------------------------{-# LANGUAGE ExistentialQuantification, GADTs, RankNTypes #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-} -- | Specification of Copilot streams as modular transition systems. module Copilot.Theorem.TransSys.Spec@@ -44,8 +44,6 @@ import qualified Data.Set as Set import qualified Data.Bimap as Bimap ---------------------------------------------------------------------------------- -- | Unique name that identifies a node. type NodeId = String @@ -76,7 +74,6 @@ -- its local name. , nodeConstrs :: [Expr Bool] } - -- | Identifer of a variable in the local (within one node) namespace. data Var = Var {varName :: String} deriving (Eq, Show, Ord)@@ -103,8 +100,6 @@ Op2 :: Type t -> Op2 a t -> Expr a -> Expr a -> Expr t VarE :: Type t -> Var -> Expr t ---------------------------------------------------------------------------------- -- | Constructor for variables identifiers in the global namespace. mkExtVar node name = ExtVar node (Var name) @@ -130,8 +125,6 @@ tre (Op2 t op e1 e2) = f (Op2 t op (tre e1) (tre e2)) tre e = f e ---------------------------------------------------------------------------------- -- | The set of variables related to a node (union of the local variables and -- the imported variables after deferencing them). nodeVarsSet :: Node -> Set Var@@ -160,8 +153,6 @@ nodeExportedExtVarsSet :: Node -> Set ExtVar nodeExportedExtVarsSet n = Set.map (ExtVar $ nodeId n) (nodeLocalVarsSet n) ---------------------------------------------------------------------------------- instance HasInvariants Node where invariants n =@@ -178,8 +169,6 @@ in preVars `isSubsetOf` nodeLocalVarsSet n ] ---------------------------------------------------------------------------------- specNodesIds :: TransSys -> Set NodeId specNodesIds s = Set.fromList . map nodeId $ specNodes s @@ -195,8 +184,6 @@ ((== specTopNodeId spec) . nodeId) (specNodes spec) ---------------------------------------------------------------------------------- instance HasInvariants TransSys where invariants s =@@ -218,14 +205,11 @@ isTopologicallySorted :: TransSys -> Bool isTopologicallySorted spec = isJust $ foldM inspect Set.empty (specNodes spec)- where inspect acc n = do- guard $ Set.fromList (nodeDependencies n) `isSubsetOf` acc- return . Set.insert (nodeId n) $ acc----------------------------------------------------------------------------------+ where+ inspect acc n = do+ guard $ Set.fromList (nodeDependencies n) `isSubsetOf` acc+ return . Set.insert (nodeId n) $ acc -- For debugging purposes instance Show ExtVar where show (ExtVar n v) = "(" ++ n ++ " : " ++ show v ++ ")"----------------------------------------------------------------------------------
src/Copilot/Theorem/TransSys/Transform.hs view
@@ -1,7 +1,5 @@---------------------------------------------------------------------------------- {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE Safe #-} -- | Helper module to manipulate and simplify TransSys graphs. module Copilot.Theorem.TransSys.Transform@@ -31,15 +29,11 @@ import qualified Data.Graph as Graph import qualified Data.Bimap as Bimap ---------------------------------------------------------------------------------- prefix :: String -> Var -> Var prefix s1 (Var s2) = Var $ s1 ++ "." ++ s2 ncNodeIdSep = "-" ---------------------------------------------------------------------------------- -- | Merge all the given nodes, replacing all references to the given node Ids -- with a reference to a fresh node id (unless the nodes given as argument -- contain the top node), in which case its ID is chosen instead.@@ -92,7 +86,6 @@ constrs = mergeConstrs toMerge renamingF - updateOtherNode :: NodeId -> [NodeId] -> (ExtVar -> ExtVar) -> Node -> Node updateOtherNode newNodeId mergedNodesIds renamingF n = n { nodeDependencies =@@ -105,8 +98,6 @@ | (lv, gv) <- Bimap.toList $ nodeImportedVars n ] } -- updateExpr :: NodeId -> (ExtVar -> Var) -> Expr t -> Expr t updateExpr nId renamingF = transformExpr aux where@@ -114,7 +105,6 @@ aux (VarE t v) = VarE t (renamingF (ExtVar nId v)) aux e = e - mergeVarsDescrs :: [Node] -> (ExtVar -> Var) -> Map Var VarDescr mergeVarsDescrs toMerge renamingF = Map.fromList $ do n <- toMerge@@ -169,8 +159,6 @@ then Bimap.insert v' (ExtVar nId v) acc else acc -- redirectLocalImports :: [Node] -> Renaming () redirectLocalImports toMerge = do renamingF <- getRenamingF@@ -186,8 +174,6 @@ guard $ n' `member` mergedNodesSet return (nId, alias, n', v) ---------------------------------------------------------------------------------- -- | Discard all the structure of a /modular transition system/ and turn it -- into a /non-modular transition system/ with only one node. inline :: TransSys -> TransSys@@ -224,8 +210,6 @@ topoSort s = s { specNodes = map (\(Graph.AcyclicSCC n) -> n) $ buildScc id (specNodes s) } ---------------------------------------------------------------------------------- -- | Completes each node of a specification with imported variables such that -- each node contains a copy of all its dependencies. --@@ -289,5 +273,3 @@ return $ Bimap.tryInsert alias ev acc foldM tryImport (nodeImportedVars n) toImportVars----------------------------------------------------------------------------------
src/Copilot/Theorem/TransSys/Translate.hs view
@@ -1,8 +1,10 @@-----------------------------------------------------------------------------------{-# LANGUAGE RankNTypes, NamedFieldPuns, ViewPatterns,- ScopedTypeVariables, GADTs, FlexibleContexts #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns #-} -- | Translate Copilot specifications into a modular transition system. --@@ -57,8 +59,6 @@ import qualified Data.Map as Map import qualified Data.Bimap as Bimap ---------------------------------------------------------------------------------- -- Naming conventions -- These are important in order to avoid name conflicts @@ -80,8 +80,6 @@ | d == 0 = s | otherwise = s ++ ncSep ++ show d ---------------------------------------------------------------------------------- -- | Translate Copilot specifications into a modular transition system. translate :: C.Spec -> TransSys translate cspec =@@ -108,9 +106,6 @@ topNode = mkTopNode topNodeId (map nodeId propNodes) cprops extVarNodes = map mkExtVarNode extvarNodesNames ----------------------------------------------------------------------------------- mkTopNode :: String -> [NodeId] -> [C.Property] -> Node mkTopNode topNodeId dependencies cprops = Node { nodeId = topNodeId@@ -123,8 +118,6 @@ [ (Var cp, mkExtVar (ncPropNode cp) ncMain) | cp <- C.propertyName <$> cprops ] -- mkExtVarNode (name, U t) = Node { nodeId = name , nodeDependencies = []@@ -132,7 +125,6 @@ , nodeImportedVars = Bimap.empty , nodeConstrs = []} - mkPropNodes :: [C.Property] -> Trans [Node] mkPropNodes = mapM propNode where@@ -149,8 +141,6 @@ , C.streamExpr = C.propertyExpr prop , C.streamExprType = C.Bool } ---------------------------------------------------------------------------------- stream :: C.Stream -> Trans Node stream (C.Stream { C.streamId , C.streamBuffer@@ -180,8 +170,6 @@ { nodeId, nodeDependencies, nodeLocalVars , nodeImportedVars, nodeConstrs = [] } ---------------------------------------------------------------------------------- expr :: Type t -> C.Expr t' -> Trans (Expr t) expr t (C.Const _ v) = return $ Const t (cast t $ toDyn v)@@ -219,12 +207,6 @@ newImportedVar localAlias (ExtVar nodeName (Var ncMain)) return $ VarE t localAlias --- TODO : Use uninterpreted functions to handle--- * Unhandled operators--- * Extern functions--- * Extern arrays--- For now, the result of these operations is a new unconstrained variable- expr t (C.Op1 op e) = handleOp1 t (op, e) expr notHandled Op1 where@@ -244,8 +226,6 @@ newDep newNode return $ VarE t (Var newNode) ---------------------------------------------------------------------------------- runTrans :: Trans a -> (a, [(NodeId, U Type)]) runTrans mx = (x, nubBy' (compare `on` fst) $ _extVarsNodes st)@@ -293,7 +273,6 @@ , _dependencies = [] } return (lvs, ivs, nub' dps) - getUid :: Trans Int getUid = do uid <- _nextUid <$> get@@ -312,5 +291,3 @@ newExtVarNode id t = modify $ \st -> st { _extVarsNodes = (id, t) : _extVarsNodes st }----------------------------------------------------------------------------------
src/Copilot/Theorem/TransSys/Type.hs view
@@ -1,7 +1,6 @@-----------------------------------------------------------------------------------{-# LANGUAGE ExistentialQuantification, GADTs #-}-{-# LANGUAGE Safe #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE Safe #-} -- | Types suported by the modular transition systems. module Copilot.Theorem.TransSys.Type@@ -11,8 +10,6 @@ import Copilot.Core.Type.Equality ---------------------------------------------------------------------------------- -- | A type at both value and type level. -- -- Real numbers are mapped to 'Double's.@@ -28,18 +25,12 @@ Real =~= Real = Just Refl _ =~= _ = Nothing ---------------------------------------------------------------------------------- -- | Unknown types. -- -- For instance, 'U Expr' is the type of an expression of unknown type data U f = forall t . U (f t) ---------------------------------------------------------------------------------- instance Show (Type t) where show Integer = "Int" show Bool = "Bool" show Real = "Real"----------------------------------------------------------------------------------
src/Copilot/Theorem/What4.hs view
@@ -1,18 +1,18 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE MultiWayIf #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-} -- | -- Module : Copilot.Theorem.What4@@ -98,7 +98,6 @@ import GHC.TypeNats (KnownNat) import qualified Panic as Panic --------------------------------------------------------------------------------- -- 'prove' function -- -- To prove properties of a spec, we translate them into What4 using the TransM@@ -185,7 +184,6 @@ (res, _) <- runStateT (unTransM proveProperties) st return res --------------------------------------------------------------------------------- -- What4 translation -- | the state for translating Copilot expressions into What4 expressions. As we@@ -303,8 +301,9 @@ XDouble e -> Some . CopilotValue CT.Double . fst . bfToDouble NearEven <$> WG.groundEval ge e _ -> error "valFromExpr unhandled case"- where fromBV :: forall a w . Num a => BV.BV w -> a- fromBV = fromInteger . BV.asUnsigned+ where+ fromBV :: forall a w . Num a => BV.BV w -> a+ fromBV = fromInteger . BV.asUnsigned -- | A view of an XExpr as a bitvector expression, a natrepr for its width, its -- signed/unsigned status, and the constructor used to reconstruct an XExpr from@@ -519,7 +518,8 @@ if k' < length buf then liftIO $ translateConstExpr sym tp (buf !! k') else translateExprAt sym (k' - length buf) e- where k' = k + fromIntegral ix+ where+ k' = k + fromIntegral ix CE.Local _ _ _ _ _ -> error "translateExpr: Local unimplemented" CE.Var _ _ -> error "translateExpr: Var unimplemented" CE.ExternVar tp nm _prefix -> getExternConstantAt sym tp nm k@@ -558,37 +558,40 @@ (CE.Not, XBool e) -> XBool <$> WI.notPred sym e (CE.Not, _) -> panic (CE.Abs _, xe) -> numOp bvAbs fpAbs xe- where bvAbs :: BVOp1 w t- bvAbs e = do zero <- WI.bvLit sym knownNat (BV.zero knownNat)- e_neg <- WI.bvSlt sym e zero- neg_e <- WI.bvSub sym zero e- WI.bvIte sym e_neg neg_e e- fpAbs :: FPOp1 fpp t- fpAbs e = do zero <- WI.floatLit sym knownRepr bfPosZero- e_neg <- WI.floatLt sym e zero- neg_e <- WI.floatSub sym fpRM zero e- WI.floatIte sym e_neg neg_e e+ where+ bvAbs :: BVOp1 w t+ bvAbs e = do zero <- WI.bvLit sym knownNat (BV.zero knownNat)+ e_neg <- WI.bvSlt sym e zero+ neg_e <- WI.bvSub sym zero e+ WI.bvIte sym e_neg neg_e e+ fpAbs :: FPOp1 fpp t+ fpAbs e = do zero <- WI.floatLit sym knownRepr bfPosZero+ e_neg <- WI.floatLt sym e zero+ neg_e <- WI.floatSub sym fpRM zero e+ WI.floatIte sym e_neg neg_e e (CE.Sign _, xe) -> numOp bvSign fpSign xe- where bvSign :: BVOp1 w t- bvSign e = do zero <- WI.bvLit sym knownRepr (BV.zero knownNat)- neg_one <- WI.bvLit sym knownNat (BV.mkBV knownNat (-1))- pos_one <- WI.bvLit sym knownNat (BV.mkBV knownNat 1)- e_zero <- WI.bvEq sym e zero- e_neg <- WI.bvSlt sym e zero- t <- WI.bvIte sym e_neg neg_one pos_one- WI.bvIte sym e_zero zero t- fpSign :: FPOp1 fpp t- fpSign e = do zero <- WI.floatLit sym knownRepr bfPosZero- neg_one <- WI.floatLit sym knownRepr (bfFromDouble (-1.0))- pos_one <- WI.floatLit sym knownRepr (bfFromDouble 1.0)- e_zero <- WI.floatEq sym e zero- e_neg <- WI.floatLt sym e zero- t <- WI.floatIte sym e_neg neg_one pos_one- WI.floatIte sym e_zero zero t+ where+ bvSign :: BVOp1 w t+ bvSign e = do zero <- WI.bvLit sym knownRepr (BV.zero knownNat)+ neg_one <- WI.bvLit sym knownNat (BV.mkBV knownNat (-1))+ pos_one <- WI.bvLit sym knownNat (BV.mkBV knownNat 1)+ e_zero <- WI.bvEq sym e zero+ e_neg <- WI.bvSlt sym e zero+ t <- WI.bvIte sym e_neg neg_one pos_one+ WI.bvIte sym e_zero zero t+ fpSign :: FPOp1 fpp t+ fpSign e = do zero <- WI.floatLit sym knownRepr bfPosZero+ neg_one <- WI.floatLit sym knownRepr (bfFromDouble (-1.0))+ pos_one <- WI.floatLit sym knownRepr (bfFromDouble 1.0)+ e_zero <- WI.floatEq sym e zero+ e_neg <- WI.floatLt sym e zero+ t <- WI.floatIte sym e_neg neg_one pos_one+ WI.floatIte sym e_zero zero t (CE.Recip _, xe) -> fpOp recip xe- where recip :: FPOp1 fpp t- recip e = do one <- WI.floatLit sym knownRepr (bfFromDouble 1.0)- WI.floatDiv sym fpRM one e+ where+ recip :: FPOp1 fpp t+ recip e = do one <- WI.floatLit sym knownRepr (bfFromDouble 1.0)+ WI.floatDiv sym fpRM one e (CE.Exp _, xe) -> realOp (WI.realExp sym) xe (CE.Sqrt _, xe) -> fpOp (WI.floatSqrt sym fpRM) xe (CE.Log _, xe) -> realOp (WI.realLog sym) xe@@ -652,51 +655,53 @@ Just ix -> return $ xes !! ix Nothing -> panic _ -> panic- where numOp :: (forall w . BVOp1 w t)- -> (forall fpp . FPOp1 fpp t)- -> XExpr t- -> IO (XExpr t)- numOp bvOp fpOp xe = case xe of- XInt8 e -> XInt8 <$> bvOp e- XInt16 e -> XInt16 <$> bvOp e- XInt32 e -> XInt32 <$> bvOp e- XInt64 e -> XInt64 <$> bvOp e- XWord8 e -> XWord8 <$> bvOp e- XWord16 e -> XWord16 <$> bvOp e- XWord32 e -> XWord32 <$> bvOp e- XWord64 e -> XWord64 <$> bvOp e- XFloat e -> XFloat <$> fpOp e- XDouble e -> XDouble <$> fpOp e- _ -> panic+ where+ numOp :: (forall w . BVOp1 w t)+ -> (forall fpp . FPOp1 fpp t)+ -> XExpr t+ -> IO (XExpr t)+ numOp bvOp fpOp xe = case xe of+ XInt8 e -> XInt8 <$> bvOp e+ XInt16 e -> XInt16 <$> bvOp e+ XInt32 e -> XInt32 <$> bvOp e+ XInt64 e -> XInt64 <$> bvOp e+ XWord8 e -> XWord8 <$> bvOp e+ XWord16 e -> XWord16 <$> bvOp e+ XWord32 e -> XWord32 <$> bvOp e+ XWord64 e -> XWord64 <$> bvOp e+ XFloat e -> XFloat <$> fpOp e+ XDouble e -> XDouble <$> fpOp e+ _ -> panic - bvOp :: (forall w . BVOp1 w t) -> XExpr t -> IO (XExpr t)- bvOp f xe = case xe of- XInt8 e -> XInt8 <$> f e- XInt16 e -> XInt16 <$> f e- XInt32 e -> XInt32 <$> f e- XInt64 e -> XInt64 <$> f e- XWord8 e -> XWord8 <$> f e- XWord16 e -> XWord16 <$> f e- XWord32 e -> XWord32 <$> f e- XWord64 e -> XWord64 <$> f e- _ -> panic+ bvOp :: (forall w . BVOp1 w t) -> XExpr t -> IO (XExpr t)+ bvOp f xe = case xe of+ XInt8 e -> XInt8 <$> f e+ XInt16 e -> XInt16 <$> f e+ XInt32 e -> XInt32 <$> f e+ XInt64 e -> XInt64 <$> f e+ XWord8 e -> XWord8 <$> f e+ XWord16 e -> XWord16 <$> f e+ XWord32 e -> XWord32 <$> f e+ XWord64 e -> XWord64 <$> f e+ _ -> panic - fpOp :: (forall fpp . FPOp1 fpp t) -> XExpr t -> IO (XExpr t)- fpOp g xe = case xe of- XFloat e -> XFloat <$> g e- XDouble e -> XDouble <$> g e- _ -> panic+ fpOp :: (forall fpp . FPOp1 fpp t) -> XExpr t -> IO (XExpr t)+ fpOp g xe = case xe of+ XFloat e -> XFloat <$> g e+ XDouble e -> XDouble <$> g e+ _ -> panic - realOp :: RealOp1 t -> XExpr t -> IO (XExpr t)- realOp h xe = fpOp hf xe- where hf :: (forall fpp . FPOp1 fpp t)- hf e = do re <- WI.floatToReal sym e- hre <- h re- WI.realToFloat sym knownRepr fpRM hre+ realOp :: RealOp1 t -> XExpr t -> IO (XExpr t)+ realOp h xe = fpOp hf xe+ where+ hf :: (forall fpp . FPOp1 fpp t)+ hf e = do re <- WI.floatToReal sym e+ hre <- h re+ WI.realToFloat sym knownRepr fpRM hre - realRecip :: RealOp1 t- realRecip e = do one <- WI.realLit sym 1- WI.realDiv sym one e+ realRecip :: RealOp1 t+ realRecip e = do one <- WI.realLit sym 1+ WI.realDiv sym one e type BVOp2 w t = (KnownNat w, 1 <= w) => WB.BVExpr t w -> WB.BVExpr t w -> IO (WB.BVExpr t w) @@ -734,30 +739,33 @@ (CE.Div _, xe1, xe2) -> bvOp (WI.bvSdiv sym) (WI.bvUdiv sym) xe1 xe2 (CE.Fdiv _, xe1, xe2) -> fpOp (WI.floatDiv sym fpRM) xe1 xe2 (CE.Pow _, xe1, xe2) -> fpOp powFn' xe1 xe2- where powFn' :: FPOp2 fpp t- powFn' e1 e2 = do re1 <- WI.floatToReal sym e1- re2 <- WI.floatToReal sym e2- let args = (Empty :> re1 :> re2)- rpow <- WI.applySymFn sym powFn args- WI.realToFloat sym knownRepr fpRM rpow+ where+ powFn' :: FPOp2 fpp t+ powFn' e1 e2 = do re1 <- WI.floatToReal sym e1+ re2 <- WI.floatToReal sym e2+ let args = (Empty :> re1 :> re2)+ rpow <- WI.applySymFn sym powFn args+ WI.realToFloat sym knownRepr fpRM rpow (CE.Logb _, xe1, xe2) -> fpOp logbFn' xe1 xe2- where logbFn' :: FPOp2 fpp t- logbFn' e1 e2 = do re1 <- WI.floatToReal sym e1- re2 <- WI.floatToReal sym e2- let args = (Empty :> re1 :> re2)- rpow <- WI.applySymFn sym logbFn args- WI.realToFloat sym knownRepr fpRM rpow+ where+ logbFn' :: FPOp2 fpp t+ logbFn' e1 e2 = do re1 <- WI.floatToReal sym e1+ re2 <- WI.floatToReal sym e2+ let args = (Empty :> re1 :> re2)+ rpow <- WI.applySymFn sym logbFn args+ WI.realToFloat sym knownRepr fpRM rpow (CE.Eq _, xe1, xe2) -> cmp (WI.eqPred sym) (WI.bvEq sym) (WI.floatEq sym) xe1 xe2 (CE.Ne _, xe1, xe2) -> cmp neqPred bvNeq fpNeq xe1 xe2- where neqPred :: BoolCmp2 t- neqPred e1 e2 = do e <- WI.eqPred sym e1 e2- WI.notPred sym e- bvNeq :: forall w . BVCmp2 w t- bvNeq e1 e2 = do e <- WI.bvEq sym e1 e2- WI.notPred sym e- fpNeq :: forall fpp . FPCmp2 fpp t- fpNeq e1 e2 = do e <- WI.floatEq sym e1 e2- WI.notPred sym e+ where+ neqPred :: BoolCmp2 t+ neqPred e1 e2 = do e <- WI.eqPred sym e1 e2+ WI.notPred sym e+ bvNeq :: forall w . BVCmp2 w t+ bvNeq e1 e2 = do e <- WI.bvEq sym e1 e2+ WI.notPred sym e+ fpNeq :: forall fpp . FPCmp2 fpp t+ fpNeq e1 e2 = do e <- WI.floatEq sym e1 e2+ WI.notPred sym e (CE.Le _, xe1, xe2) -> numCmp (WI.bvSle sym) (WI.bvUle sym) (WI.floatLe sym) xe1 xe2 (CE.Ge _, xe1, xe2) -> numCmp (WI.bvSge sym) (WI.bvUge sym) (WI.floatGe sym) xe1 xe2 (CE.Lt _, xe1, xe2) -> numCmp (WI.bvSlt sym) (WI.bvUlt sym) (WI.floatLt sym) xe1 xe2@@ -797,131 +805,131 @@ (XArray xes, XWord32 ix) -> buildIndexExpr sym 0 ix xes _ -> panic _ -> panic- where numOp :: (forall w . BVOp2 w t)- -> (forall fpp . FPOp2 fpp t)- -> XExpr t- -> XExpr t- -> IO (XExpr t)- numOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of- (XInt8 e1, XInt8 e2) -> XInt8 <$> bvOp e1 e2- (XInt16 e1, XInt16 e2) -> XInt16 <$> bvOp e1 e2- (XInt32 e1, XInt32 e2)-> XInt32 <$> bvOp e1 e2- (XInt64 e1, XInt64 e2)-> XInt64 <$> bvOp e1 e2- (XWord8 e1, XWord8 e2)-> XWord8 <$> bvOp e1 e2- (XWord16 e1, XWord16 e2)-> XWord16 <$> bvOp e1 e2- (XWord32 e1, XWord32 e2)-> XWord32 <$> bvOp e1 e2- (XWord64 e1, XWord64 e2)-> XWord64 <$> bvOp e1 e2- (XFloat e1, XFloat e2)-> XFloat <$> fpOp e1 e2- (XDouble e1, XDouble e2)-> XDouble <$> fpOp e1 e2- _ -> panic-- bvOp :: (forall w . BVOp2 w t)- -> (forall w . BVOp2 w t)- -> XExpr t- -> XExpr t- -> IO (XExpr t)- bvOp opS opU xe1 xe2 = case (xe1, xe2) of- (XInt8 e1, XInt8 e2) -> XInt8 <$> opS e1 e2- (XInt16 e1, XInt16 e2) -> XInt16 <$> opS e1 e2- (XInt32 e1, XInt32 e2) -> XInt32 <$> opS e1 e2- (XInt64 e1, XInt64 e2) -> XInt64 <$> opS e1 e2- (XWord8 e1, XWord8 e2) -> XWord8 <$> opU e1 e2- (XWord16 e1, XWord16 e2) -> XWord16 <$> opU e1 e2- (XWord32 e1, XWord32 e2) -> XWord32 <$> opU e1 e2- (XWord64 e1, XWord64 e2) -> XWord64 <$> opU e1 e2- _ -> panic+ where+ numOp :: (forall w . BVOp2 w t)+ -> (forall fpp . FPOp2 fpp t)+ -> XExpr t+ -> XExpr t+ -> IO (XExpr t)+ numOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of+ (XInt8 e1, XInt8 e2) -> XInt8 <$> bvOp e1 e2+ (XInt16 e1, XInt16 e2) -> XInt16 <$> bvOp e1 e2+ (XInt32 e1, XInt32 e2)-> XInt32 <$> bvOp e1 e2+ (XInt64 e1, XInt64 e2)-> XInt64 <$> bvOp e1 e2+ (XWord8 e1, XWord8 e2)-> XWord8 <$> bvOp e1 e2+ (XWord16 e1, XWord16 e2)-> XWord16 <$> bvOp e1 e2+ (XWord32 e1, XWord32 e2)-> XWord32 <$> bvOp e1 e2+ (XWord64 e1, XWord64 e2)-> XWord64 <$> bvOp e1 e2+ (XFloat e1, XFloat e2)-> XFloat <$> fpOp e1 e2+ (XDouble e1, XDouble e2)-> XDouble <$> fpOp e1 e2+ _ -> panic - fpOp :: (forall fpp . FPOp2 fpp t)- -> XExpr t- -> XExpr t- -> IO (XExpr t)- fpOp op xe1 xe2 = case (xe1, xe2) of- (XFloat e1, XFloat e2) -> XFloat <$> op e1 e2- (XDouble e1, XDouble e2) -> XDouble <$> op e1 e2- _ -> panic+ bvOp :: (forall w . BVOp2 w t)+ -> (forall w . BVOp2 w t)+ -> XExpr t+ -> XExpr t+ -> IO (XExpr t)+ bvOp opS opU xe1 xe2 = case (xe1, xe2) of+ (XInt8 e1, XInt8 e2) -> XInt8 <$> opS e1 e2+ (XInt16 e1, XInt16 e2) -> XInt16 <$> opS e1 e2+ (XInt32 e1, XInt32 e2) -> XInt32 <$> opS e1 e2+ (XInt64 e1, XInt64 e2) -> XInt64 <$> opS e1 e2+ (XWord8 e1, XWord8 e2) -> XWord8 <$> opU e1 e2+ (XWord16 e1, XWord16 e2) -> XWord16 <$> opU e1 e2+ (XWord32 e1, XWord32 e2) -> XWord32 <$> opU e1 e2+ (XWord64 e1, XWord64 e2) -> XWord64 <$> opU e1 e2+ _ -> panic - cmp :: BoolCmp2 t- -> (forall w . BVCmp2 w t)- -> (forall fpp . FPCmp2 fpp t)- -> XExpr t- -> XExpr t- -> IO (XExpr t)- cmp boolOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of- (XBool e1, XBool e2) -> XBool <$> boolOp e1 e2- (XInt8 e1, XInt8 e2) -> XBool <$> bvOp e1 e2- (XInt16 e1, XInt16 e2) -> XBool <$> bvOp e1 e2- (XInt32 e1, XInt32 e2)-> XBool <$> bvOp e1 e2- (XInt64 e1, XInt64 e2)-> XBool <$> bvOp e1 e2- (XWord8 e1, XWord8 e2)-> XBool <$> bvOp e1 e2- (XWord16 e1, XWord16 e2)-> XBool <$> bvOp e1 e2- (XWord32 e1, XWord32 e2)-> XBool <$> bvOp e1 e2- (XWord64 e1, XWord64 e2)-> XBool <$> bvOp e1 e2- (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2- (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2- _ -> panic+ fpOp :: (forall fpp . FPOp2 fpp t)+ -> XExpr t+ -> XExpr t+ -> IO (XExpr t)+ fpOp op xe1 xe2 = case (xe1, xe2) of+ (XFloat e1, XFloat e2) -> XFloat <$> op e1 e2+ (XDouble e1, XDouble e2) -> XDouble <$> op e1 e2+ _ -> panic - numCmp :: (forall w . BVCmp2 w t)- -> (forall w . BVCmp2 w t)- -> (forall fpp . FPCmp2 fpp t)- -> XExpr t- -> XExpr t- -> IO (XExpr t)- numCmp bvSOp bvUOp fpOp xe1 xe2 = case (xe1, xe2) of- (XInt8 e1, XInt8 e2) -> XBool <$> bvSOp e1 e2- (XInt16 e1, XInt16 e2) -> XBool <$> bvSOp e1 e2- (XInt32 e1, XInt32 e2)-> XBool <$> bvSOp e1 e2- (XInt64 e1, XInt64 e2)-> XBool <$> bvSOp e1 e2- (XWord8 e1, XWord8 e2)-> XBool <$> bvUOp e1 e2- (XWord16 e1, XWord16 e2)-> XBool <$> bvUOp e1 e2- (XWord32 e1, XWord32 e2)-> XBool <$> bvUOp e1 e2- (XWord64 e1, XWord64 e2)-> XBool <$> bvUOp e1 e2- (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2- (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2- _ -> panic+ cmp :: BoolCmp2 t+ -> (forall w . BVCmp2 w t)+ -> (forall fpp . FPCmp2 fpp t)+ -> XExpr t+ -> XExpr t+ -> IO (XExpr t)+ cmp boolOp bvOp fpOp xe1 xe2 = case (xe1, xe2) of+ (XBool e1, XBool e2) -> XBool <$> boolOp e1 e2+ (XInt8 e1, XInt8 e2) -> XBool <$> bvOp e1 e2+ (XInt16 e1, XInt16 e2) -> XBool <$> bvOp e1 e2+ (XInt32 e1, XInt32 e2)-> XBool <$> bvOp e1 e2+ (XInt64 e1, XInt64 e2)-> XBool <$> bvOp e1 e2+ (XWord8 e1, XWord8 e2)-> XBool <$> bvOp e1 e2+ (XWord16 e1, XWord16 e2)-> XBool <$> bvOp e1 e2+ (XWord32 e1, XWord32 e2)-> XBool <$> bvOp e1 e2+ (XWord64 e1, XWord64 e2)-> XBool <$> bvOp e1 e2+ (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2+ (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2+ _ -> panic - buildIndexExpr :: 1 <= n- => WB.ExprBuilder t st fs- -> Word32- -- ^ Index- -> WB.Expr t (WT.BaseBVType 32)- -- ^ Index- -> V.Vector n (XExpr t)- -- ^ Elements- -> IO (XExpr t)- buildIndexExpr sym curIx ix xelts = case V.uncons xelts of- (xe, Left Refl) -> return xe- (xe, Right xelts') -> do- LeqProof <- return $ V.nonEmpty xelts'- rstExpr <- buildIndexExpr sym (curIx+1) ix xelts'- curIxExpr <- WI.bvLit sym knownNat (BV.word32 curIx)- ixEq <- WI.bvEq sym curIxExpr ix- mkIte sym ixEq xe rstExpr+ numCmp :: (forall w . BVCmp2 w t)+ -> (forall w . BVCmp2 w t)+ -> (forall fpp . FPCmp2 fpp t)+ -> XExpr t+ -> XExpr t+ -> IO (XExpr t)+ numCmp bvSOp bvUOp fpOp xe1 xe2 = case (xe1, xe2) of+ (XInt8 e1, XInt8 e2) -> XBool <$> bvSOp e1 e2+ (XInt16 e1, XInt16 e2) -> XBool <$> bvSOp e1 e2+ (XInt32 e1, XInt32 e2)-> XBool <$> bvSOp e1 e2+ (XInt64 e1, XInt64 e2)-> XBool <$> bvSOp e1 e2+ (XWord8 e1, XWord8 e2)-> XBool <$> bvUOp e1 e2+ (XWord16 e1, XWord16 e2)-> XBool <$> bvUOp e1 e2+ (XWord32 e1, XWord32 e2)-> XBool <$> bvUOp e1 e2+ (XWord64 e1, XWord64 e2)-> XBool <$> bvUOp e1 e2+ (XFloat e1, XFloat e2)-> XBool <$> fpOp e1 e2+ (XDouble e1, XDouble e2)-> XBool <$> fpOp e1 e2+ _ -> panic - mkIte :: WB.ExprBuilder t st fs- -> WB.Expr t WT.BaseBoolType- -> XExpr t- -> XExpr t- -> IO (XExpr t)- mkIte sym pred xe1 xe2 = case (xe1, xe2) of- (XBool e1, XBool e2) -> XBool <$> WI.itePred sym pred e1 e2- (XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym pred e1 e2- (XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym pred e1 e2- (XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym pred e1 e2- (XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym pred e1 e2- (XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym pred e1 e2- (XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym pred e1 e2- (XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym pred e1 e2- (XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym pred e1 e2- (XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym pred e1 e2- (XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym pred e1 e2- (XStruct xes1, XStruct xes2) ->- XStruct <$> zipWithM (mkIte sym pred) xes1 xes2- (XArray xes1, XArray xes2) ->- case V.length xes1 `testEquality` V.length xes2 of- Just Refl -> XArray <$> V.zipWithM (mkIte sym pred) xes1 xes2- Nothing -> panic- _ -> panic+ buildIndexExpr :: 1 <= n+ => WB.ExprBuilder t st fs+ -> Word32+ -- ^ Index+ -> WB.Expr t (WT.BaseBVType 32)+ -- ^ Index+ -> V.Vector n (XExpr t)+ -- ^ Elements+ -> IO (XExpr t)+ buildIndexExpr sym curIx ix xelts = case V.uncons xelts of+ (xe, Left Refl) -> return xe+ (xe, Right xelts') -> do+ LeqProof <- return $ V.nonEmpty xelts'+ rstExpr <- buildIndexExpr sym (curIx+1) ix xelts'+ curIxExpr <- WI.bvLit sym knownNat (BV.word32 curIx)+ ixEq <- WI.bvEq sym curIxExpr ix+ mkIte sym ixEq xe rstExpr + mkIte :: WB.ExprBuilder t st fs+ -> WB.Expr t WT.BaseBoolType+ -> XExpr t+ -> XExpr t+ -> IO (XExpr t)+ mkIte sym pred xe1 xe2 = case (xe1, xe2) of+ (XBool e1, XBool e2) -> XBool <$> WI.itePred sym pred e1 e2+ (XInt8 e1, XInt8 e2) -> XInt8 <$> WI.bvIte sym pred e1 e2+ (XInt16 e1, XInt16 e2) -> XInt16 <$> WI.bvIte sym pred e1 e2+ (XInt32 e1, XInt32 e2) -> XInt32 <$> WI.bvIte sym pred e1 e2+ (XInt64 e1, XInt64 e2) -> XInt64 <$> WI.bvIte sym pred e1 e2+ (XWord8 e1, XWord8 e2) -> XWord8 <$> WI.bvIte sym pred e1 e2+ (XWord16 e1, XWord16 e2) -> XWord16 <$> WI.bvIte sym pred e1 e2+ (XWord32 e1, XWord32 e2) -> XWord32 <$> WI.bvIte sym pred e1 e2+ (XWord64 e1, XWord64 e2) -> XWord64 <$> WI.bvIte sym pred e1 e2+ (XFloat e1, XFloat e2) -> XFloat <$> WI.floatIte sym pred e1 e2+ (XDouble e1, XDouble e2) -> XDouble <$> WI.floatIte sym pred e1 e2+ (XStruct xes1, XStruct xes2) ->+ XStruct <$> zipWithM (mkIte sym pred) xes1 xes2+ (XArray xes1, XArray xes2) ->+ case V.length xes1 `testEquality` V.length xes2 of+ Just Refl -> XArray <$> V.zipWithM (mkIte sym pred) xes1 xes2+ Nothing -> panic+ _ -> panic translateOp3 :: forall t st fs a b c d . WB.ExprBuilder t st fs