copilot-theorem 3.18 → 3.18.1

raw patch · 7 files changed

+12/−4 lines, 7 filesdep ~copilot-coredep ~copilot-prettyprinter

Dependency ranges changed: copilot-core, copilot-prettyprinter

Files

CHANGELOG +4/−0
copilot-theorem.cabal +3/−3
src/Copilot/Theorem/IL/Translate.hs +1/−0
src/Copilot/Theorem/Misc/Utils.hs +1/−1
src/Copilot/Theorem/Prove.hs +1/−0
src/Copilot/Theorem/TransSys/Translate.hs +1/−0
src/Copilot/Theorem/What4.hs +1/−0

CHANGELOG view

@@ -1,4 +1,8 @@ 2024-01-07+        * Version bump (3.18.1). (#493)+        * Adjust to work with GHC 9.6. (#491)++2024-01-07         * Version bump (3.18). (#487)         * Introduce testing infrastructure for Copilot.Theorem.What4. (#474)         * Replace uses of forall with forAll. (#470)

copilot-theorem.cabal view

@@ -14,7 +14,7 @@   <https://copilot-language.github.io>.  -version                   : 3.18+version                   : 3.18.1 license                   : BSD3 license-file              : LICENSE maintainer                : Ivan Perez <ivan.perezdominguez@nasa.gov>@@ -63,8 +63,8 @@                           , xml                   >= 1.3 && < 1.4                           , what4                 >= 1.3 && < 1.6 -                          , copilot-core          >= 3.18 && < 3.19-                          , copilot-prettyprinter >= 3.18 && < 3.19+                          , copilot-core          >= 3.18.1 && < 3.19+                          , copilot-prettyprinter >= 3.18.1 && < 3.19    exposed-modules         : Copilot.Theorem                           , Copilot.Theorem.Prove

src/Copilot/Theorem/IL/Translate.hs view

@@ -14,6 +14,7 @@  import qualified Data.Map.Strict as Map +import Control.Monad       (forM, liftM2, when) import Control.Monad.State  import Data.Char

src/Copilot/Theorem/Misc/Utils.hs view

@@ -1,4 +1,4 @@-{-# LANGUAGE Safe #-}+{-# LANGUAGE Trustworthy #-}  -- | Utility / auxiliary functions. module Copilot.Theorem.Misc.Utils

src/Copilot/Theorem/Prove.hs view

@@ -22,6 +22,7 @@  import Data.List (intercalate) import Control.Applicative (liftA2)+import Control.Monad        (ap, liftM) import Control.Monad.Writer  -- | Output produced by a prover, containing the 'Status' of the proof and

src/Copilot/Theorem/TransSys/Translate.hs view

@@ -47,6 +47,7 @@ import Copilot.Theorem.TransSys.Cast import Copilot.Theorem.Misc.Utils +import Control.Monad            (liftM, liftM2, unless) import Control.Monad.State.Lazy  import Data.Char (isNumber)

src/Copilot/Theorem/What4.hs view

@@ -57,6 +57,7 @@ import qualified What4.Solver                   as WS import qualified What4.Solver.DReal             as WS +import Control.Monad (forM) import Control.Monad.State import qualified Data.BitVector.Sized as BV import Data.Foldable (foldrM)