Commit c587a684 authored by Michael Hanus 's avatar Michael Hanus

Fix for using default rules and contracts, examples moved into example directory

parent 9e0c6581
--------------------------------------------------------------
A translater from Curry with Integrated Code to standard Curry
--------------------------------------------------------------
The Curry Preprocessor
======================
Authors: Max Deppert - made@informatik.uni-kiel.de
Jasper Sikorra - jsi@informatik.uni-kiel.de
This repository contains the implementation of the
Curry preprocessor `currypp` which supports some
extensions for Curry programs, like
* Integrated code, i.e., the integration of code
written in some other language into Curry programs,
like regular expressions, format specifications (`printf`),
HTML and XML code,
* default rules,
* contracts.
Details about the usage can be found in the manual.
Here is a short summary of the usage of integrated code.
General usage of the code integrator:
-------------------------------------
If the pre-processor is installed (see Makefile) as the binary `currypp`,
If the pre-processor is installed as the binary `currypp`,
Curry source files containing integrated code can be translated
by running `currypp` as follows:
......
......@@ -715,6 +715,20 @@ queens :: Int -> [Int]
queens n = safe (permute [1..n])
\end{curry}
\paragraph{Important note:}
The implementation of default rules is based on set functions
(implemented by the module \code{Control.SetFunctions}).
Therefore, the package \code{setfunctions} should be installed
as a dependency.
This can easily done by executing
%
\begin{curry}
> cypm add setfunctions
\end{curry}
%
before compiling a program containing default rules with the
Curry preprocessor.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Contracts}
......@@ -778,6 +792,22 @@ Postcondition of 'sort' (module Quicksort, line 27) violated for:
ERROR: Execution aborted due to contract violation!
\end{curry}
\paragraph{Important note:}
The implementation of default rules is based on set functions
(implemented by the module \code{Control.SetFunctions}) and
the auxiliary package to check contracts at run time.
Therefore, the packages \code{setfunctions} and \code{contracts}
should be installed as dependencies.
This can easily done by executing
%
\begin{curry}
> cypm add setfunctions
> cypm add contracts
\end{curry}
%
before compiling a program containing contracts with the
Curry preprocessor.
% LocalWords: preprocessor
......
......@@ -3,12 +3,16 @@
-- Defining factorial numbers:
-- Specification: the usual recursive definition
fac'spec :: Int -> Int
fac'spec n = if n==0 then 1 else n * fac'spec (n-1)
-- The input should be non-negative:
fac'pre :: Int -> Bool
fac'pre n = n>=0
-- The result should be positive:
fac'post :: Int -> Int -> Bool
fac'post _ v = v>0
-- An implementation using Prelude operations:
fac :: Int -> Int
fac n = foldr (*) 1 [1..n]
{
"name": "currypp",
"version": "2.0.0",
"version": "2.1.0",
"author": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "The standard preprocessor of Curry",
"category": [ "Programming", "Analysis" ],
......@@ -16,6 +16,7 @@
"finite-map" : ">= 0.0.1",
"fl-parser" : ">= 1.0.0",
"flatcurry" : ">= 2.0.0",
"frontend-exec" : ">= 0.0.1",
"html" : ">= 2.0.0",
"printf" : ">= 0.0.1",
"regexp" : ">= 1.1.0",
......@@ -30,12 +31,11 @@
"pakcs": ">= 2.0.0",
"kics2": ">= 2.0.0"
},
"sourceDirs": [ "src", "src/IntegratedCode",
"sourceDirs": [ "src",
"src/IntegratedCode",
"src/IntegratedCode/Parser",
"src/IntegratedCode/Parser/ML",
"src/IntegratedCode/Parser/SQL",
"src/DefaultRules",
"src/ContractWrapper"
"src/IntegratedCode/Parser/SQL"
],
"exportedModules": [ "Main" ],
"executable": {
......@@ -43,19 +43,27 @@
"main": "Main"
},
"testsuite": [
{ "src-dir": "src/IntegratedCode/Examples",
{ "src-dir": "examples/IntegratedCode",
"modules": [ "testFormat", "testHtml", "testRegExps" ]
},
{ "src-dir": "src/IntegratedCode/ExamplesSQL",
{ "src-dir": "examples/IntegratedSQLCode",
"options": "-v",
"script" : "test.sh"
},
{ "src-dir": "src/DefaultRules/Examples",
{ "src-dir": "examples/Contracts",
"options": "--nospec --nodet --deftype=Int",
"modules": [ "BubbleSort", "BubbleSortFormat", "Coin",
"FibInfinite", "Quicksort" ]
},
{ "src-dir": "examples/DefaultRules",
"options": "-m40",
"modules": [ "BreakWhere", "BubbleSort", "ColorMap", "DutchFlag",
"FixInt", "FloatString", "Guards", "ListFuns", "Lookup",
"Nim", "ParOr", "Queens", "Rev2", "WorldCup",
"ParOrDet", "BubbleSortDet", "DutchFlagDet" ]
"Nim", "ParOr", "Queens", "Rev2", "WorldCup" ]
},
{ "src-dir": "examples/DeterministicOperations",
"options": "-m40",
"modules": [ "BubbleSortDet", "DutchFlagDet", "ParOrDet" ]
}
],
"documentation": {
......
{
"name": "currypp",
"version": "2.0.0",
"author": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "The standard preprocessor of Curry",
"category": [ "Programming", "Analysis" ],
"dependencies": {
"base" : ">= 1.0.0, < 2.0.0",
"abstract-curry": ">= 2.0.0",
"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",
"searchtree" : ">= 0.0.1",
"setfunctions" : ">= 0.0.1",
"wl-pprint" : ">= 0.0.1",
"xml" : ">= 2.0.0",
"easycheck" : ">= 0.0.1"
},
"compilerCompatibility": {
"pakcs": ">= 2.0.0",
"kics2": ">= 2.0.0"
},
"sourceDirs": [ "src", "src/IntegratedCode",
"src/IntegratedCode/Parser",
"src/IntegratedCode/Parser/ML",
"src/IntegratedCode/Parser/SQL",
"src/DefaultRules",
"src/ContractWrapper"
],
"exportedModules": [ "Main" ],
"executable": {
"name": "currypp",
"main": "Main"
},
"testsuite": [
{ "src-dir": "src/IntegratedCode/Examples",
"modules": [ "testFormat", "testHtml", "testRegExps" ]
},
{ "src-dir": "src/IntegratedCode/ExamplesSQL",
"options": "-v",
"script" : "test.sh"
},
{ "src-dir": "src/DefaultRules/Examples",
"options": "-m40",
"modules": [ "BreakWhere", "BubbleSort", "ColorMap", "DutchFlag",
"FixInt", "FloatString", "Guards", "ListFuns", "Lookup",
"Nim", "ParOr", "Queens", "Rev2", "WorldCup",
"ParOrDet", "BubbleSortDet", "DutchFlagDet" ]
},
{ "src-dir": "src/ContractWrapper/Examples",
"options": "--nospec --nodet --deftype=Int",
"modules": [ "BubbleSort", "BubbleSortFormat", "Coin",
"FibInfinite", "Quicksort" ]
}
],
"documentation": {
"src-dir": "docs",
"main": "main.tex"
},
"source": {
"git": "https://git.ps.informatik.uni-kiel.de/curry-packages/currypp.git",
"tag": "$version"
}
}
------------------------------------------------------------------------------
--- Auxiliary operations to compile additionally imported modules
--- with the front end.
module CPP.CompileWithFrontend
where
import Distribution ( curryCompiler )
import System.FrontendExec
------------------------------------------------------------------------------
--- If a module is added as a new import to the transformed program,
--- we have to compile it in order to avoid a compilation error
--- of the front end, since the front end assumes,
-- if the preprocessor is called, that all imported modules are
-- already compiled.
compileImportedModule :: Int -> String -> IO ()
compileImportedModule verb modname = do
mapM (compileModuleTo verb modname) [ACY, UACY]
compileSetFunctions2Flat
where
compileSetFunctions2Flat
| curryCompiler == "kics2"
= compileModuleTo verb modname TFCY
| curryCompiler == "pakcs"
= compileModuleTo verb modname FCY
| otherwise
= error $ "compileSetFunctions: unknown Curry compiler '" ++
curryCompiler ++ "'!"
compileModuleTo :: Int -> String -> FrontendTarget -> IO ()
compileModuleTo verb modname target = do
when (verb > 2) $ putStrLn $
"Compiling '" ++ modname ++ "' to '" ++ showFrontendTarget target ++ "'..."
callFrontendWithParams target (setQuiet True defaultParams) modname
------------------------------------------------------------------------------
......@@ -14,7 +14,8 @@
--- @version April 2019
------------------------------------------------------------------------
module TransContracts( main, transContracts ) where
module CPP.Contracts ( main, translateContracts )
where
import Char
import Directory
......@@ -45,12 +46,14 @@ import CASS.Server ( analyzeGeneric )
import SimplifyPostConds
import TheoremUsage
import CPP.CompileWithFrontend ( compileImportedModule )
------------------------------------------------------------------------
banner :: String
banner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText = "Contract Transformation Tool (Version of 30/04/19)"
bannerText = "Contract Transformation Tool (Version of 11/10/19)"
bannerLine = take (length bannerText) (repeat '=')
------------------------------------------------------------------------
......@@ -60,9 +63,9 @@ 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 -> String -> CurryProg
-> IO (Maybe CurryProg)
transContracts verb moreopts modname srcprog inputProg = do
translateContracts :: Int -> [String] -> String -> String -> CurryProg
-> IO (Maybe CurryProg)
translateContracts verb moreopts modname srcprog inputProg = do
when (verb>1) $ putStr banner
opts <- processOpts defaultOptions moreopts
transformCProg verb opts modname srcprog inputProg (progName inputProg)
......@@ -198,8 +201,8 @@ transformCProg verb opts modname srctxt orgprog outmodname = do
putStrLn $ "Adding contract checking to: " ++ unwords checkfuns
detinfo <- analyzeGeneric nondetAnalysis (progName prog)
>>= return . either id error
let newprog = transformProgram opts funposs fdecls detinfo
funspecs preconds postconds prog
newprog <- transformProgram verb opts funposs fdecls detinfo
funspecs preconds postconds prog
return (Just (renameCurryModule outmodname newprog))
-- Get functions from a Curry module with a name satisfying the predicate:
......@@ -208,33 +211,35 @@ getFunDeclsWith pred prog = filter (pred . snd . funcName) (functions prog)
------------------------------------------------------------------------
-- Transform a given program w.r.t. given specifications and pre/postconditions
transformProgram :: Options -> [(QName,Int)]-> [CFuncDecl]
transformProgram :: Int -> Options -> [(QName,Int)]-> [CFuncDecl]
-> ProgInfo Deterministic -> [CFuncDecl]
-> [CFuncDecl] -> [CFuncDecl] -> CurryProg -> CurryProg
transformProgram opts funposs allfdecls detinfo specdecls predecls postdecls
(CurryProg mname imps dfltdecl clsdecls instdecls tdecls orgfdecls opdecls) =
let -- replace in program old postconditions by new simplified postconditions:
fdecls = filter (\fd -> funcName fd `notElem` map funcName postdecls)
orgfdecls ++ postdecls
newpostconds = concatMap
(genPostCond4Spec opts allfdecls detinfo postdecls)
specdecls
newfunnames = map (snd . funcName) newpostconds
-- remove old postconditions which are transformed into postconditions
-- with specification checking:
wonewfuns = filter (\fd -> snd (funcName fd) `notElem` newfunnames)
fdecls
-- compute postconditions actually used for contract checking:
contractpcs = postdecls++newpostconds
in CurryProg mname
(nub ("Test.Contract":"Control.SetFunctions":imps))
dfltdecl clsdecls instdecls tdecls
(map deleteCmtIfEmpty
(concatMap
(addContract opts funposs allfdecls predecls contractpcs)
wonewfuns ++
newpostconds))
opdecls
-> [CFuncDecl] -> [CFuncDecl] -> CurryProg -> IO CurryProg
transformProgram verb opts funposs allfdecls detinfo
specdecls predecls postdecls
(CurryProg mname imps dfltdecl clsdecls instdecls tdecls
orgfdecls opdecls) = do
let -- replace in program old postconditions by new simplified postconditions:
fdecls = filter (\fd -> funcName fd `notElem` map funcName postdecls)
orgfdecls ++ postdecls
newpostconds = concatMap
(genPostCond4Spec opts allfdecls detinfo postdecls)
specdecls
newfunnames = map (snd . funcName) newpostconds
-- remove old postconditions which are transformed into postconditions
-- with specification checking:
wonewfuns = filter (\fd -> snd (funcName fd) `notElem` newfunnames)
fdecls
-- compute postconditions actually used for contract checking:
contractpcs = postdecls++newpostconds
unless (contractMod `elem` imps) $ compileImportedModule verb contractMod
unless (setFunMod `elem` imps) $ compileImportedModule verb setFunMod
return $ CurryProg
mname (nub (contractMod : setFunMod : imps))
dfltdecl clsdecls instdecls tdecls
(map deleteCmtIfEmpty
(concatMap (addContract opts funposs allfdecls predecls contractpcs)
wonewfuns ++ newpostconds))
opdecls
-- Add an empty comment to each function which has no comment
addCmtFuncInProg :: CurryProg -> CurryProg
......@@ -530,4 +535,12 @@ propModule = "Test.Prop"
easyCheckModule :: String
easyCheckModule = "Test.EasyCheck"
--- Name of the set functions module.
setFunMod :: String
setFunMod = "Control.SetFunctions"
--- Name of the contract module.
contractMod :: String
contractMod = "Test.Contract"
------------------------------------------------------------------------
-----------------------------------------------------------------------------
--- Translator for Curry programs to implement default rules
--- and deterministic functions.
--- Default Rules Preprocessor
--- ==========================
---
--- This module contains the implementation of a preprocessor
--- for Curry programs in order to implement default rules
--- and deterministic operations.
---
--- A default rule for a function `f` processed by this preprocessor
--- must be defined as a rule defining the operation `f'default`, e.g.,
---
--- nlookup key (_ ++ [(key,value)] ++ _) = Just value
--- nlookup'default _ _ = Nothing
---
--- The concept of default rules and their implementation are described in
---
--- Sergio Antoy, Michael Hanus: Default Rules for Curry
--- Theory and Practice of Logic Programming,
--- Vol. 17, No. 2, pp. 121-147, 2017
---
--- An operation can be marked as deterministic by decorating the
--- result type with `DET`, e.g.,
---
--- psort :: [Int] -> DET [Int]
---
--- The concept of deterministic operations and their implementation
--- are described in
---
--- Sergio Antoy, Michael Hanus:
--- Eliminating Irrelevant Non-determinism in Functional Logic Programs
--- Proc. 19th Int. Symp. on Practical Aspects of Declarative Languages,
--- Springer LNCS 10137, pp. 1-18, 2017
---
--- This preprocessor can be invoked by the Curry preprocessor `currypp`
--- with the option `defaultrules` (provided as a CYMAKE option,
--- see the example programs in the directory `examples/DefaultRules`).
---
--- @author Michael Hanus
--- @version December 2018
--- @version October 2019
-----------------------------------------------------------------------------
module CPP.DefaultRules ( translateDefaultRulesAndDetOps )
where
import Distribution ( curryCompiler )
import FilePath ( takeDirectory )
import List ( partition )
......@@ -20,6 +56,7 @@ import System.CurryPath ( modNameToPath )
import TheoremUsage ( determinismTheoremFor, existsProofFor
, getModuleProofFiles, isProofFileNameFor )
import CPP.CompileWithFrontend ( compileImportedModule )
--------------------------------------------------------------------
......@@ -27,7 +64,7 @@ banner :: String
banner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText =
"Transformation Tool for Curry with Default Rules (Version of 31/10/18)"
"Transformation Tool for Curry with Default Rules (Version of 11/10/19)"
bannerLine = take (length bannerText) (repeat '=')
------------------------------------------------------------------------
......@@ -44,16 +81,18 @@ defaultTransScheme = if curryCompiler == "kics2"
else SpecScheme -- NoDupScheme
------------------------------------------------------------------------
-- Start default rules transformation in "preprocessor mode".
-- The Curry program must be read with readUntypedCurry in order to
-- process DET annotations!
transDefaultRules :: Int -> [String] -> String -> CurryProg
-> IO (Maybe CurryProg)
transDefaultRules verb moreopts _ prog = do
--- Start default rules/deterministic operations transformation
--- in "preprocessor mode".
--- It is assumed that the Curry program passed as the last argument
--- was read with `readUntypedCurry` which is important to
--- process DET annotations!
translateDefaultRulesAndDetOps :: Int -> [String] -> String -> CurryProg
-> IO (Maybe CurryProg)
translateDefaultRulesAndDetOps verb moreopts _ prog = do
when (verb>1) $ putStr banner
trscm <- processOpts moreopts
when (verb>1) $ putStrLn ("Translation scheme: " ++ show trscm)
mbtransprog <- translateProg trscm prog
mbtransprog <- translateProg verb trscm prog
maybe (return Nothing)
(\ (detfuncnames,newprog) -> do
-- check whether we have files with determinism proofs:
......@@ -115,8 +154,9 @@ showQName (qn,fn) = "'" ++ qn ++ "." ++ fn ++ "'"
-- transformation).
-- If the program was not transformed, `Nothing` is returned.
translateProg :: TransScheme -> CurryProg -> IO (Maybe ([QName],CurryProg))
translateProg trscm
translateProg :: Int -> TransScheme -> CurryProg
-> IO (Maybe ([QName],CurryProg))
translateProg verb trscm
prog@(CurryProg mn imps dfltdecl clsdecls instdecls tdecls fdecls ops) = do
let usageerrors = checkDefaultRules prog
unless (null usageerrors) $ do
......@@ -125,10 +165,13 @@ translateProg trscm
usageerrors)
error "Transformation aborted"
-- now we do not have to check the correct usage of default rules...
unless (setFunMod `elem` imps) $
compileImportedModule verb setFunMod
return $ if null deffuncs && null detfuncnames
then Nothing
else Just (detfuncnames, CurryProg mn newimports dfltdecl clsdecls
instdecls tdecls newfdecls ops)
then Nothing
else Just (detfuncnames,
CurryProg mn newimports dfltdecl clsdecls
instdecls tdecls newfdecls ops)
where
newimports = if setFunMod `elem` imps then imps else setFunMod:imps
detfuncnames = map funcName (filter isDetFun fdecls)
......
------------------------------------------------------------------------
A transformation tool to generate a Curry module with
assertion checking from pre/postconditions and specifications.
The preprocessor contains a transformation tool to generate
a Curry module with assertion checking from pre/postconditions
and specifications.
Sergio Antoy, Michael Hanus
August 12, 2016
The tool is implemented in the module `CPP.Contracts`.
------------------------------------------------------------------------
How to use the tool:
......@@ -17,7 +16,7 @@ beginning of your Curry module:
If postconditions or specifications are nondeterministic,
it is better that they will be evaluated via encapsulated search
(see Examples/NDAssertion.curry for a discussion).
(see `examples/Contracts/NDAssertion.curry` for a discussion).
For this purpose use the option "-e" as follows:
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts --optF=-e #-}
......@@ -69,7 +68,7 @@ Assumptions:
------------------------------------------------------------------------
Examples:
See programs in the directory Examples
See programs in the directory `examples/Contracts`.
------------------------------------------------------------------------
Known problems:
......
Default Rules Preprocessor
==========================
This directory contains the implementation of a preprocessor
for Curry programs in order to implement default rules.
A default rule for a function `f` processed by this preprocessor
must be defined as a rule defining the operation `f'default`.
The preprocessor can be called by the Curry preprocessor `currypp`
with the option `defaultrules` (provided as a CYMAKE option,
see the example programs in the directory Examples).
--------------------------------------------------------------
A translater from Curry with Integrated Code to standard Curry
--------------------------------------------------------------
Authors: Max Deppert - made@informatik.uni-kiel.de
Jasper Sikorra - jsi@informatik.uni-kiel.de
General usage of the code integrator:
-------------------------------------
If the pre-processor is installed as the binary `currypp`,
Curry source files containing integrated code can be translated
by running `currypp` as follows:
currypp <org-filename> <input-file> <output-file> foreigncode [-o]
The parameters are:
* The name of the original Curry source file.
* The name of the file containing the input to be translated.
* The name of the output file where the translated code should be stored.
* If the optional parameter `-o` is given, a copy of the translated code
is stored in the file `org-filename.CURRYPP`.
* To preprocess SQL: --model:<modelname>_SQLCode.info
Writing files with integrated code:
-----------------------------------
The basic syntax of integrated code in Curry program looks like
``langtag expression''
Here, `langtag` is a tag indicating the kind of integrated language,
and `expression` is an expression of this language.
If `` or '' are used in the expression itself, the enclosing accents
need to be of higher number than the inner graves, i.e., the following
integrated code expression is also allowed:
````langtag expression''''
The number of opening and closing accents must always be identical.
Currently, the following `langtag` values are supported:
format - `printf` Syntax
printf - same as above (but with an implicit `putStr` call)
regex - Polymorphic regex expressions
html - Standard HTML
xml - Standard XML
sql - SQL syntax
See the examples and source file comments for further details.
......@@ -7,29 +7,29 @@
--- is supported (option `foreigncode`, see module `Translator`).
---
--- @author Michael Hanus
--- @version December 2018
--- @version October 2019
------------------------------------------------------------------------------
import AbstractCurry.Types
import AbstractCurry.Files
import AbstractCurry.Pretty(showCProg)
import AbstractCurry.Select(progName)
import Char(isDigit,digitToInt,isSpace)