copilot-theorem 3.0 → 3.1

raw patch · 4 files changed

+6/−15 lines, 4 filesdep ~copilot-corenew-uploaderPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot-core

API changes (from Hackage documentation)

Files

• CHANGELOG +3/−0
• copilot-theorem.cabal +3/−2
• src/Copilot/Theorem/IL/Translate.hs +0/−10
• src/Copilot/Theorem/TransSys/Translate.hs +0/−3

@@ -0,0 +1,3 @@+2019-11-22 Ivan Perez <ivan.perez@nianet.org>+        * Version bump (3.1).+        * Remove ExternFun (#6).

@@ -6,7 +6,7 @@   Some tools to prove properties on Copilot programs with k-induction model   checking. -version                   : 3.0+version                   : 3.1 license                   : BSD3 license-file              : LICENSE maintainer                : jonathan.laurent@ens.fr@@ -14,6 +14,7 @@ category                  : Language, Embedded build-type                : Simple extra-source-files        : README.md+                          , CHANGELOG  author                    : Jonathan Laurent @@ -55,7 +56,7 @@                           , transformers  >= 0.5 && < 0.6                           , xml           >= 1.3 && < 1.4 -                          , copilot-core  >= 3.0 && < 3.1+                          , copilot-core  >= 3.1 && < 3.2    exposed-modules         : Copilot.Theorem                           , Copilot.Theorem.Prove

@@ -36,9 +36,6 @@ ncExternVar :: C.Name -> SeqId ncExternVar n = "ext_" ++ n -ncExternFun :: C.Name -> SeqId-ncExternFun n = "_" ++ n- ncUnhandledOp :: String -> String ncUnhandledOp = id @@ -135,13 +132,6 @@  expr (C.ExternVar t name _) = bound s t >> return s   where s = SVal (trType t) (ncExternVar name) _n_--expr (C.ExternFun t name args _ _) = do-  args' <- mapM trArg args-  let s = FunApp (trType t) (ncExternFun name) args'-  bound s t-  return s-  where trArg (C.UExpr {C.uExprExpr}) = expr uExprExpr  expr (C.Op1 (C.Sign ta) e) = case ta of   C.Int8   -> trSign ta e

@@ -36,7 +36,6 @@ ncLocal s     = "l" ++ dropWhile (not . isNumber) s  ncExternVarNode name = "ext-" ++ name-ncExternFunNode name = "fun-" ++ name  ncImported :: NodeId -> String -> String ncImported n s = n ++ ncSep ++ s@@ -201,8 +200,6 @@   where     notHandled (UnhandledOp2 _opName _ta _tb _tc) =       newUnconstrainedVar t--expr t (C.ExternFun _ _ _ _ _) = newUnconstrainedVar t  newUnconstrainedVar :: Type t -> Trans (Expr t) newUnconstrainedVar t = do