Commit 3b063673 authored by Michael Hanus 's avatar Michael Hanus
Browse files

currypp packaged

parents
*~
.curry
.cpm
--------------------------------------------------------------
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 (see Makefile) 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.
This directory contains some documention for the Curry preprocessor:
manual.tex:
A short description to be included in the main manual of the Curry system.
sqlsyntax.tex:
A specification of the SQL syntax recognized by the code integrator.
This diff is collapsed.
\section{SQL Syntax Supported by CurryPP}
\label{app:sqlsyntax}
This section contains a grammar in EBNF which specifies
the SQL syntax recognized by the Curry preprocessor
in integrated SQL code (see Sect.~\ref{sec:integratedsql}).
%
The grammar satisfies the LL(1) property and is influenced by the
SQLite dialect.\footnote{\url{https://sqlite.org/lang.html}}
\begin{lstlisting}
--------------type of statements--------------------------------
statement ::= queryStatement | transactionStatement
queryStatement ::= ( deleteStatement
| insertStatement
| selectStatement
| updateStatement )
';'
------------- transaction -------------------------------------
transactionStatement ::= (BEGIN
|IN TRANSACTION '(' queryStatement
{ queryStatement }')'
|COMMIT
|ROLLBACK ) ';'
-------------- delete ------------------------------------------
deleteStatement ::= DELETE FROM tableSpecification
[ WHERE condition ]
-------------insert -------------------------------------------
insertStatement ::= INSERT INTO tableSpecification
insertSpecification
insertSpecification ::= ['(' columnNameList ')' ] valuesClause
valuesClause ::= VALUES valueList
------------update--------------------------------------------
updateStatement ::= UPDATE tableSpecification
SET (columnAssignment {',' columnAssignment}
[ WHERE condition ]
| embeddedCurryExpression )
columnAssignment ::= columnName '=' literal
-------------select statement ---------------------------------
selectStatement ::= selectHead { setOperator selectHead }
[ orderByClause ]
[ limitClause ]
selectHead ::= selectClause fromClause
[ WHERE condition ]
[ groupByClause [ havingClause ]]
setOperator ::= UNION | INTERSECT | EXCEPT
selectClause ::= SELECT [( DISTINCT | ALL )]
( selectElementList | '*' )
selectElementList ::= selectElement { ',' selectElement }
selectElement ::= [ tableIdentifier'.' ] columnName
| aggregation
| caseExpression
aggregation ::= function '(' [ DISTINCT ] columnReference ')'
caseExpression ::= CASE WHEN condition THEN operand
ELSE operand END
function ::= COUNT | MIN | MAX | AVG | SUM
fromClause ::= FROM tableReference { ',' tableReference }
groupByClause ::= GROUP BY columnList
havingClause ::= HAVING conditionWithAggregation
orderByClause ::= ORDER BY columnReference [ sortDirection ]
{',' columnReference
[ sortDirection ] }
sortDirection ::= ASC | DESC
limitClause = LIMIT integerExpression
-------------common elements-----------------------------------
columnList ::= columnReference { ',' columnReference }
columnReference ::= [ tableIdentifier'.' ] columnName
columnNameList ::= columnName { ',' columnName}
tableReference ::= tableSpecification [ AS tablePseudonym ]
[ joinSpecification ]
tableSpecification ::= tableName
condition ::= operand operatorExpression
[logicalOperator condition]
| EXISTS subquery [logicalOperator condition]
| NOT condition
| '(' condition ')'
| satConstraint [logicalOperator condition]
operand ::= columnReference
| literal
subquery ::= '(' selectStatement ')'
operatorExpression ::= IS NULL
| NOT NULL
| binaryOperator operand
| IN setSpecification
| BETWEEN operand operand
| LIKE quotes pattern quotes
setSpecification ::= literalList
binaryOperator ::= '>'| '<' | '>=' | '<=' | '=' | '!='
logicalOperator ::= AND | OR
conditionWithAggregation ::=
aggregation [logicalOperator disaggregation]
| '(' conditionWithAggregation ')'
| operand operatorExpression
[logicalOperator conditionWithAggregation]
| NOT conditionWithAggregation
| EXISTS subquery
[logicalOperator conditionWithAggregation]
| satConstraint
[logicalOperator conditionWithAggregation]
aggregation ::= function '('(ALL | DISTINCT) columnReference')'
binaryOperator
operand
satConstraint ::= SATISFIES tablePseudonym
relation
tablePseudonym
joinSpecification ::= joinType tableSpecification
[ AS tablePseudonym ]
[ joinCondition ]
[ joinSpecification ]
joinType ::= CROSS JOIN | INNER JOIN
joinCondition ::= ON condition
-------------identifier and datatypes-------------------------
valueList ::= ( embeddedCurryExpression | literalList )
{',' ( embeddedCurryExpression | literalList )}
literalList ::= '(' literal { ',' literal } ')'
literal ::= numericalLiteral
| quotes alphaNumericalLiteral quotes
| dateLiteral
| booleanLiteral
| embeddedCurryExpression
| NULL
numericalLiteral ::= integerExpression
|floatExpression
integerExpression ::= [ - ] digit { digit }
floatExpression := [ - ] digit { digit } '.' digit { digit }
alphaNumericalLiteral ::= character { character }
character ::= digit | letter
dateLiteral ::= year ':' month ':' day ':'
hours ':' minutes ':' seconds
month ::= digit digit
day ::= digit digit
hours ::= digit digit
minutes ::= digit digit
seconds ::= digit digit
year ::= digit digit digit digit
booleanLiteral ::= TRUE | FALSE
embeddedCurryExpression ::= '{' curryExpression '}'
pattern ::= ( character | specialCharacter )
{( character | specialCharacter )}
specialCharacter ::= '%' | '_'
digit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
letter ::= (a...z) | (A...Z)
tableIdentifier ::= tablePseudonym | tableName
columnName ::= letter [alphanumericalLiteral]
tableName ::= letter [alphanumericalLiteral]
tablePseudonym ::= letter
relation ::= letter [[alphanumericalLiteral] | '_' ]
quotes ::= ('"'|''')
\end{lstlisting}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "../../../docs/src/manual"
%%% End:
{
"name": "currypp",
"version": "0.3.0",
"author": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "The standard preprocessor of Curry",
"category": [ "Analysis" ],
"dependencies": {
"cass-analysis": ">= 0.0.1",
"cass" : ">= 0.0.1",
"currycheck" : ">= 1.0.0",
"verify" : ">= 0.0.1"
},
"sourceDirs": [ "src", "src/IntegratedCode", "src/IntegratedCode/Parser",
"src/IntegratedCode/Parser/ML",
"src/IntegratedCode/Parser/SQL",
"src/SequentialRules", "src/DefaultRules",
"src/ContractWrapper"
],
"exportedModules": [ "Main" ],
"executable": {
"name": "curry-pp",
"main": "Main"
},
"testsuite": [
{ "src-dir": "src/IntegratedCode/Examples",
"modules": [ "testFormat", "testHtml", "testRegExps" ]
},
{ "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" ]
}
],
"source": {
"git": "https://git.ps.informatik.uni-kiel.de/curry-packages/currypp.git",
"tag": "$version"
}
}
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=defaultrules --optF=contracts #-}
import Test.Prop
-- Bubble sort formulation with default rule as deterministic operation:
sort :: [Int] ->DET [Int]
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 xs = length xs > 0
-- Postcondition: input and output lists should have the same length
sort'post xs ys = length xs == length ys
sort7 = sort [7,1,6,3,5,4,2] -=- [1..7]
sortEmpty = toError (sort [])
{-# OPTIONS_CYMAKE -F --pgmF=currypp #-}
{-# OPTIONS_CYMAKE -Wnone #-}
-- Example for using integrated code, default rules, and contracts in one
-- module
import Format
import Test.Prop
showInt i = ``format "%+.3d",i''
-- Bubble sort formulation with default rule as deterministic operation:
sort :: [a] ->DET [a]
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 xs = length xs > 0
-- Postcondition: input and output lists should have the same length
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]
sortEmpty = toError (sort [])
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts #-}
import Test.Prop
-- Examples with nondeterministicm specifications
coin'spec = 0 ? 1
coin = 1 ? 0 --> should be executed without violation
coinCorrect = coin <~> coin'spec
coin3'spec = coin'spec
coin3 = coin ? 2 --> should produce a violation
coin3Violation = toError coin3
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts #-}
-- Defining factorial numbers:
-- Specification: the usual recursive definition
fac'spec n = if n==0 then 1 else n * fac'spec (n-1)
-- The input should be non-negative:
fac'pre n = n>=0
-- The result should be positive:
fac'post _ v = v>0
-- An implementation using Prelude operations:
fac n = foldr (*) 1 [1..n]
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts #-}
-- Fibonacci numbers specified by traditional recursive definition
-- and computed efficiently by an infinite list.
-- Specification of Fibonacci numbers:
fib'pre x = x >= 0
fib'post _ y = (y > 0)
fib'spec x | x == 0 = 0
| x == 1 = 1
| otherwise = fib'spec (x-1) + fib'spec (x-2)
-- Implementation of Fibonacci numbers:
fib n = fiblist 0 1 !! n
where
fiblist x y = x : fiblist y (x+y)
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts #-}
import Test.Prop
-- An infinite list of Fibonacci numbers specified by traditional
-- recursive definition
-- (Deterministic!) specification of all Fibonacci numbers:
fibs'spec = map fib [0..]
where fib n | n == 0 = 0
| n == 1 = 1
| otherwise = fib (n-1) + fib (n-2)
-- In order to check the infinite result list, we define a specific observer:
fibs'post'observe xs = take 10 xs
-- A more efficient (but erroneous) implementation of all Fibonacci numbers:
fibs = fiblist 0 1
where
fiblist x y = x : fiblist (x+y) y
main = take 4 fibs
fibsViolation = toError (take 4 fibs)
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts #-}
-- straight selection sort with specification
import SetFunctions
perm [] = []
perm (x:xs) = insert (perm xs)
where insert ys = x:ys
insert (y:ys) = y : insert ys
sorted [] = True
sorted [_] = True
sorted (x:y:ys) = x<=y && sorted (y:ys)
-- Contract of sort:
sort'pre _ = True
sort'post xs ys = length xs == length ys
-- Specification of sort:
sort'spec :: [Int] -> [Int]
sort'spec x | y =:= perm x & sorted y = y where y free
-- Implementation of sort as minsort:
sort :: [Int] -> [Int]
sort [] = []
sort (x:xs) = min : sort rest
where (min,rest) = minRest (x:xs)
-- Contract of minRest:
-- Precondition: the argument must be a non-empty list
minRest'pre = not . null
-- Postcondition: the result is a pair of the minimum and the remaining
-- elements that must be some permutation of the input list
minRest'post :: [Int] -> (Int,[Int]) -> Bool
minRest'post xs (min,rest) =
(min:rest) `valueOf` (set1 perm xs) && all (>= min) xs
-- Implementations of minRest:
minRest :: [Int] -> (Int,[Int])
minRest xs = minRest2 xs
-- Implementation 1: Find the minimum and then delete it in the list:
minRest1 (x:xs) = let m = min x xs in (m, del m (x:xs))
where
min z [] = z
min z (y:ys) = if z <= y then min z ys else min y ys
del z (y:ys) = if z == y then ys else y : del z ys
-- Implementation 2: Find minimum and delete it in one pass:
minRest2 (x:xs) = mr x [] xs
where mr m r [] = (m,r)
mr m r (y:ys) = if m <= y then mr m (y:r) ys else mr y (m:r) ys
main = sort [26,18,5,4,16,8,22,17]
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts --optF=-e #-}
-- Example for a postcondition with a nondeterministic definition:
por True _ = True
por _ True = True
por False False = False
f'post _ (x,y) = por x y
f :: Bool -> (Bool,Bool)
f x = (x,x)
main = f True
-- The checking of the postcondition might result in a nondeterministic
-- evaluation of the main operation.
-- One can avoid this effect by using the transformation option "-e".
--
-- In general, the transformation option "-e" requires an advanced
-- (lazy!) implementation of set functions. In PAKCS, this works only for
-- violation detection of the values to be considered are finite
-- and there are only finitely many values.
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts #-}
{-# OPTIONS_CYMAKE -Wnone #-}
import Test.Prop
-- A specification of sorting a list and an implementation based
-- on the quicksort algorithm
perm [] = []
perm (x:xs) = insert (perm xs)
where insert ys = x:ys
insert (y:ys) = y : insert ys
sorted [] = True
sorted [_] = True
sorted (x:y:ys) = x<=y && sorted (y:ys)
-- Trivial precondition, just for testing
sort'pre xs = length xs >= 0
-- Postcondition: input and output lists should have the same length
sort'post xs ys = length xs == length ys
-- Specification of sort:
-- A list is a sorted result of an input if it is a permutation and sorted.
sort'spec :: [Int] -> [Int]
sort'spec x | y =:= perm x & sorted y = y where y free
-- A buggy implementation of quicksort:
sort :: [Int] -> [Int]
sort [] = []
sort (x:xs) = sort (filter (<x) xs) ++ [x] ++ sort (filter (>x) xs)
input = [26,18,5,4,16,8,22,17]
-- Buggy implementation ok for different elements:
quickSortCorrect xs = allDifferent xs ==> always (sorted (sort xs))
where
allDifferent [] = True
allDifferent (x:xs) = x `notElem` xs && allDifferent xs
-- In this example, the contract check should produce an error:
quickSortFailure = toError $ sort [1,2,1]
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts --optF=-e #-}
-- Implementation of quicksort with partition
-- Use option "-e" for contract wrapper (see part'post below).
perm [] = []
perm (x:xs) = ndinsert (perm xs)
where ndinsert [] = [x]
ndinsert (y:ys) = (x:y:ys) ? (y:ndinsert ys)
sorted [] = success
sorted [_] = success
sorted (x:y:ys) = (x<=y)=:=True & sorted (y:ys)
-- User contract:
sort'pre _ = True
sort'post xs ys = length xs == length ys
-- Specification of sort:
-- A list is a sorted result of an input if it is a permutation and sorted.
sort'spec :: [Int] -> [Int]
sort'spec x | y =:= perm x & sorted y = y where y free
-- Implementation of sort with quicksort and partition:
sort :: [Int] -> [Int]
sort [] = []
sort (x:xs) = let (low,high) = part x xs in sort low ++ x : sort high
-- Contract for partition: since we put no restriction on the order
-- of the partioned elements, the result can be any permutation
-- (i.e., this is not a precise but a weak specification).
-- Consequence: the postcondition is nondeterministic if the input list
-- contains multiple values. Thus, it should be checked with option "-e".
part'pre _ _ = True
part'post x xs (u,v) | (u++v) =:= perm xs = all (<x) u && all (>=x) v
part :: Int -> [Int] -> ([Int],[Int])
part _ [] = ([],[])
part x (y:ys) = if y<x then (y:u,v) else (u,y:v)
where (u,v) = part x ys
input = [26,18,5,4,16,8,22,17]
main = sort input
------------------------------------------------------------------------