Commit 9e0c6581 authored by Michael Hanus 's avatar Michael Hanus

Update w.r.t. package contracts

parent 1b3cefc5
......@@ -10,10 +10,12 @@
"cass-analysis" : ">= 2.0.0",
"cass" : ">= 2.0.0",
"cdbi" : ">= 2.0.0",
"contracts" : ">= 0.0.1",
"currycheck" : ">= 2.0.0",
"currypath" : ">= 0.0.1",
"finite-map" : ">= 0.0.1",
"fl-parser" : ">= 1.0.0",
"flatcurry" : ">= 2.0.0",
"html" : ">= 2.0.0",
"printf" : ">= 0.0.1",
"regexp" : ">= 1.1.0",
......@@ -22,7 +24,6 @@
"wl-pprint" : ">= 0.0.1",
"xml" : ">= 2.0.0",
"contracts" : ">= 0.0.1",
"easycheck" : ">= 0.0.1"
},
"compilerCompatibility": {
......
......@@ -10,9 +10,12 @@
"cass-analysis" : ">= 2.0.0",
"cass" : ">= 2.0.0",
"cdbi" : ">= 2.0.0",
"contracts" : ">= 0.0.1",
"currycheck" : ">= 2.0.0",
"currypath" : ">= 0.0.1",
"finite-map" : ">= 0.0.1",
"fl-parser" : ">= 1.0.0",
"flatcurry" : ">= 2.0.0",
"html" : ">= 2.0.0",
"printf" : ">= 0.0.1",
"regexp" : ">= 1.1.0",
......@@ -21,7 +24,6 @@
"wl-pprint" : ">= 0.0.1",
"xml" : ">= 2.0.0",
"contracts" : ">= 0.0.1",
"easycheck" : ">= 0.0.1"
},
"compilerCompatibility": {
......
......@@ -8,9 +8,11 @@ sort (xs++[x,y]++ys) | x>y = sort (xs++[y,x]++ys)
sort'default xs = xs
-- Precondition: we don't like to sort empty lists...
sort'pre :: [Int] -> Bool
sort'pre xs = length xs > 0
-- Postcondition: input and output lists should have the same length
sort'post :: [Int] -> [Int] -> Bool
sort'post xs ys = length xs == length ys
sort7 = sort [7,1,6,3,5,4,2] -=- [1..7]
......
......@@ -15,9 +15,11 @@ sort (xs++[x,y]++ys) | x>y = sort (xs++[y,x]++ys)
sort'default xs = xs
-- Precondition: we don't like to sort empty lists...
sort'pre :: (Ord a, Show a) => [a] -> Bool
sort'pre xs = length xs > 0
-- Postcondition: input and output lists should have the same length
sort'post :: (Ord a, Show a) => [a] -> [a] -> Bool
sort'post xs ys = length xs == length ys
sort7 = sort (map showInt [7,1,6,3,5,4,2]) -=- map (\d -> "+00"++show d) [1..7]
......
......@@ -16,9 +16,11 @@ sorted [_] = True
sorted (x:y:ys) = x<=y && sorted (y:ys)
-- Trivial precondition, just for testing
sort'pre :: [Int] -> Bool
sort'pre xs = length xs >= 0
-- Postcondition: input and output lists should have the same length
sort'post :: [Int] -> [Int] -> Bool
sort'post xs ys = length xs == length ys
-- Specification of sort:
......
......@@ -11,10 +11,10 @@
--- > Declarative Languages (PADL 2012), pp. 33-47, Springer LNCS 7149, 2012
---
--- @author Michael Hanus
--- @version December 2018
--- @version April 2019
------------------------------------------------------------------------
module TransContracts(main,transContracts) where
module TransContracts( main, transContracts ) where
import Char
import Directory
......@@ -30,7 +30,10 @@ import AbstractCurry.Pretty
import AbstractCurry.Build
import AbstractCurry.Select
import AbstractCurry.Transform
import ContractUsage
import Contract.Names
import Contract.Usage ( checkContractUsage )
import FlatCurry.Files ( readFlatCurry )
import qualified FlatCurry.Goodies as FCG
import System.CurryPath ( lookupModuleSourceInLoadPath, modNameToPath
, stripCurrySuffix)
......@@ -47,7 +50,7 @@ import TheoremUsage
banner :: String
banner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText = "Contract Transformation Tool (Version of 12/08/16)"
bannerText = "Contract Transformation Tool (Version of 30/04/19)"
bannerLine = take (length bannerText) (repeat '=')
------------------------------------------------------------------------
......@@ -57,11 +60,12 @@ banner = unlines [bannerLine,bannerText,bannerLine]
--- based on function types!
--- The result is `Nothing` if no transformation was applied or `Just` the
--- transformed program.
transContracts :: Int -> [String] -> String -> CurryProg -> IO (Maybe CurryProg)
transContracts verb moreopts srcprog inputProg = do
transContracts :: Int -> [String] -> String -> String -> CurryProg
-> IO (Maybe CurryProg)
transContracts verb moreopts modname srcprog inputProg = do
when (verb>1) $ putStr banner
opts <- processOpts defaultOptions moreopts
transformCProg verb opts srcprog inputProg (progName inputProg)
transformCProg verb opts modname srcprog inputProg (progName inputProg)
where
processOpts opts ppopts = case ppopts of
[] -> return opts
......@@ -131,7 +135,7 @@ transformStandalone opts modname outfile = do
doesFileExist acyfile >>= \b -> if b then done
else error "Source program incorrect"
let outmodname = transformedModName modname
newprog <- transformCProg 1 opts srcprog prog outmodname
newprog <- transformCProg 1 opts modname srcprog prog outmodname
writeFile outfile (showCProg (maybe prog id newprog) ++ "\n")
when (executeProg opts) $ loadIntoCurry outmodname
......@@ -151,23 +155,27 @@ loadIntoCurry m = do
--- The main transformation operation with parameters:
--- * verbosity level
--- * options
--- * module name
--- * source text of the module
--- * AbstractCurry representation of the module
--- * name of the output module (if it should be renamed)
--- The result is Nothing if no transformation was applied or Just the
--- transformed program.
transformCProg :: Int -> Options -> String -> CurryProg -> String
transformCProg :: Int -> Options -> String -> String -> CurryProg -> String
-> IO (Maybe CurryProg)
transformCProg verb opts srctxt orgprog outmodname = do
let -- to avoid constructor CFunc and references to Test.Prop
prog = addCmtFuncInProg (renameProp2EasyCheck orgprog)
usageerrors = checkContractUse prog
transformCProg verb opts modname srctxt orgprog outmodname = do
fcyprog <- readFlatCurry modname
let usageerrors = checkContractUsage modname
(map (\fd -> (snd (FCG.funcName fd), FCG.funcType fd))
(FCG.progFuncs fcyprog))
unless (null usageerrors) $ do
putStr (unlines $ "ERROR: ILLEGAL USE OF CONTRACTS:" :
map (\ ((mn,fn),err) -> fn ++ " (module " ++ mn ++ "): " ++ err)
usageerrors)
error "Contract transformation aborted"
let funposs = linesOfFDecls srctxt prog
let -- to avoid constructor CFunc and references to Test.Prop
prog = addCmtFuncInProg (renameProp2EasyCheck orgprog)
funposs = linesOfFDecls srctxt prog
fdecls = functions prog
funspecs = getFunDeclsWith isSpecName prog
specnames = map (fromSpecName . snd . funcName) funspecs
......
......@@ -226,11 +226,11 @@ callPreprocessors opts optlines modname srcprog orgfile
maybe done
(\defprog -> writeFile orgfile (optlines ++ showCProg defprog))
mbdefprog
readCurry modname >>= transContracts verb contopts srcprog
readCurry modname >>= transContracts verb contopts modname srcprog
>>= return . maybe newsrcprog showCProg
else return newsrcprog
| Contracts `elem` pptargets
= readCurry modname >>= transContracts verb contopts srcprog
= readCurry modname >>= transContracts verb contopts modname srcprog
>>= return . maybe srcprog showCProg
| otherwise
= error "currypp internal error during dispatching"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment