Skip to content

GitLab

Commit 8cc6655e authored by Michael Hanus 's avatar Michael Hanus
Browse files

Tools updated

parent 2e8bbbb9
Hide whitespace changes
Inline Side-by-side
.gitignore
View file @ 8cc6655e
......@@ -13,10 +13,12 @@ optimize/.cpm/packages/currypath-0.0.1
optimize/.cpm/packages/flatcurry-2.0.0
optimize/.cpm/packages/frontend-exec-0.0.1
optimize/.cpm/packages/propertyfile-0.0.1
optimize/.cpm/packages/queue-0.0.1
optimize/.cpm/packages/random-0.0.1
optimize/.cpm/packages/redblacktree-0.0.1
optimize/.cpm/packages/scc-0.0.1
optimize/.cpm/packages/socket-0.0.1
optimize/.cpm/packages/wl-pprint-0.0.1
optimize/.cpm/packages/xml-2.0.0
# executables
......
cpm/vendor/queue/LICENSE 0 → 100644
View file @ 8cc6655e
Copyright (c) 2018, Michael Hanus
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
3. Neither the names of the copyright holders nor the names of its
contributors may be used to endorse or promote products derived from
this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
cpm/vendor/queue/README.md 0 → 100644
View file @ 8cc6655e
queue
=====
This package contains a library implementing
double-ended queues supporting access at both
ends in constant amortized time.
cpm/vendor/queue/package.json 0 → 100644
View file @ 8cc6655e
{
"name": "queue",
"version": "0.0.1",
"author": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "Library with double-ended queues supporting access at both ends in constant amortized time",
"category": [ "Data" ],
"license": "BSD-3-Clause",
"licenseFile": "LICENSE",
"dependencies": {
"base" : ">= 1.0.0, < 2.0.0",
"random" : ">= 0.0.1"
},
"compilerCompatibility": {
"pakcs": ">= 2.0.0",
"kics2": ">= 2.0.0"
},
"exportedModules": [ "Data.Queue" ],
"testsuite": {
"src-dir": "test",
"modules": [ "TestQueue" ]
},
"source": {
"git": "https://git.ps.informatik.uni-kiel.de/curry-packages/queue.git",
"tag": "$version"
}
}
cpm/vendor/queue/src/Data/Queue.curry 0 → 100644
View file @ 8cc6655e
------------------------------------------------------------------------------
--- An implementation of double-ended queues supporting access at both
--- ends in constant amortized time.
---
--- @author Bernd Brassel, Olaf Chitil, Michael Hanus, Sebastian Fischer,
--- Bjoern Peemoeller
--- @version December 2018
------------------------------------------------------------------------------
module Data.Queue
( -- Abstract data type, constructors and queries
Queue, empty, cons, snoc, isEmpty, deqLength
-- Selectors
, deqHead, deqTail, deqLast, deqInit, deqReverse, rotate, matchHead, matchLast
-- conversion from and to lists
, listToDeq, deqToList
) where
--- The datatype of a queue.
data Queue a = S Int [a] Int [a]
--- The empty queue.
empty :: Queue _
empty = S 0 [] 0 []
--- Inserts an element at the front of the queue.
cons :: a -> Queue a -> Queue a
cons x (S lenf f lenr r) = check (lenf + 1) (x : f) lenr r
--- Inserts an element at the end of the queue.
snoc :: a -> Queue a -> Queue a
snoc x (S lenf f lenr r) = deqReverse (check (lenr + 1) (x : r) lenf f)
--- Is the queue empty?
isEmpty :: Queue _ -> Bool
isEmpty (S lenf _ lenr _) = lenf + lenr == 0
--- Returns the number of elements in the queue.
deqLength :: Queue _ -> Int
deqLength (S lenf _ lenr _) = lenf + lenr
--- The first element of the queue.
deqHead :: Queue a -> a
deqHead (S lenf f _ r) = head (if lenf == 0 then r else f)
--- Removes an element at the front of the queue.
deqTail :: Queue a -> Queue a
deqTail (S _ [] _ _) = empty
deqTail (S lenf (_:fs) lenr r) = deqReverse (check lenr r (lenf - 1) fs)
--- The last element of the queue.
deqLast :: Queue a -> a
deqLast (S _ f lenr r) = head (if lenr == 0 then f else r)
--- Removes an element at the end of the queue.
deqInit :: Queue a -> Queue a
deqInit (S _ _ _ [] ) = empty
deqInit (S lenf f lenr (_:rs)) = check lenf f (lenr - 1) rs
--- Reverses a double ended queue.
deqReverse :: Queue a -> Queue a
deqReverse (S lenf f lenr r) = S lenr r lenf f
--- Moves the first element to the end of the queue.
rotate :: Queue a -> Queue a
rotate q = snoc (deqHead q) (deqTail q)
--- Matches the front of a queue.
--- `matchHead q` is equivalent to
--- `if isEmpty q then Nothing else Just (deqHead q, deqTail q)`
--- but more efficient.
matchHead :: Queue a -> Maybe (a, Queue a)
matchHead (S _ [] _ [] ) = Nothing
matchHead (S _ [] _ [x] ) = Just (x, empty)
matchHead (S _ [] _ (_:_:_))
= error $ "Data.Queue.matchHead: illegal queue"
matchHead (S lenf (x:xs) lenr r )
= Just (x, deqReverse (check lenr r (lenf - 1) xs))
--- Matches the end of a queue.
--- `matchLast q` is equivalent to
--- `if isEmpty q then Nothing else Just (deqLast q,deqInit q)`
--- but more efficient.
matchLast :: Queue a -> Maybe (a,Queue a)
matchLast (S _ [] _ [] ) = Nothing
matchLast (S _ [x] _ [] ) = Just (x, empty)
matchLast (S _ (_:_:_) _ [] )
= error $ "Data.Queue.matchLast: illegal queue"
matchLast (S lenf f lenr (x:xs)) = Just (x, check lenf f (lenr - 1) xs)
--- Transforms a list to a double ended queue.
listToDeq :: [a] -> Queue a
listToDeq xs = check (length xs) xs 0 []
--- Transforms a double ended queue to a list.
deqToList :: Queue a -> [a]
deqToList (S _ xs _ ys) = xs ++ reverse ys
--- Check for invariant: The length of the first list is smaller than
--- three times the length of the second plus 1.
check :: Int -> [a] -> Int -> [a] -> Queue a
check lenf f lenr r
| lenf <= 3 * lenr + 1 = S lenf f lenr r
| otherwise = S lenf' f' lenr' r'
where
len = lenf + lenr
lenf' = len `div` 2
lenr' = len - lenf'
(f', rf') = splitAt lenf' f
r' = r ++ reverse rf'
cpm/vendor/queue/test/RandomTest.curry 0 → 100644
View file @ 8cc6655e
-- A few auxiliary functions to formulate tests with random numbers.
module RandomTest ( test, eq ) where
import List ( nub )
import Test.EasyCheck
import System.Random
--- Tests a given predicate on a list of distinct random numbers.
--- In case of a failure, the list of random numbers is returned
--- in order to see the test cases in the CurryTest tool.
test :: ([Int] -> Bool) -> PropIO
test f = (rndList lenRnds >>= \xs -> return (if f xs then Nothing else Just xs))
`returns` Nothing
--- Tests whether two operations return equal results
--- on a list of distinct random numbers.
--- In case of a failure, the list of random numbers is returned
--- in order to see the test cases in the CurryTest tool.
eq :: Eq a => ([Int] -> a) -> ([Int] -> a) -> PropIO
eq f g = test (\x -> (f x)==(g x))
--- generate a list of at most n random numbers (without duplicated elements)
rndList :: Int -> IO [Int]
rndList n = getRandomSeed >>= return . nub . take n . (flip nextIntRange 100000)
--- maximal length of test lists
lenRnds :: Int
lenRnds = 1000
cpm/vendor/queue/test/TestQueue.curry 0 → 100644
View file @ 8cc6655e
import List
import Data.Queue
import RandomTest
deq f = f . listToDeq
deqs f = deqToList . f . listToDeq
testHead = eq (deq deqHead) head
testLast = eq (deq deqLast) last
testCons = eq (deqs (cons 73)) (73:)
testTail = eq (deqs (deqTail)) tail
testSnoc = eq (deqs (snoc 73)) (++[73])
testInit = eq (deqs deqInit) init
where
init [x] = []
init (x:y:ys) = x : init (y:ys)
testReverse = eq (deqs deqReverse) reverse
testLength = eq (deq deqLength) length
testRotate = eq (deqs rotate) (\ (x:xs) -> xs ++ [x])
cpm/vendor/redblacktree/README.md
View file @ 8cc6655e
redblacktree
============
This package contains library implementing
This package contains libraries implementing
red-black trees and efficient access structures,
like tables and sets, using red-black trees.
cpm/vendor/wl-pprint/package.json
View file @ 8cc6655e
......@@ -8,7 +8,8 @@
"license": "BSD-3-Clause",
"licenseFile": "LICENSE",
"dependencies": {
"base": ">= 1.0.0, < 2.0.0"
"base" : ">= 1.0.0, < 2.0.0",
"queue": ">= 0.0.1"
},
"compilerCompatibility": {
"pakcs": ">= 2.0.0",
......
cpm/vendor/wl-pprint/src/Text/PrettyImpl.curry
View file @ 8cc6655e
......@@ -3,13 +3,12 @@
--- by Olaf Chitil.
---
--- @author Sebastian Fischer, Bjoern Peemoeller, Jan Tikovsky
--- @version October 2017
--- @category general
--- @version December 2018
------------------------------------------------------------------------------
module Text.PrettyImpl where
import qualified Dequeue as Q (Queue, cons, empty, matchHead, matchLast)
import qualified Data.Queue as Q (Queue, cons, empty, matchHead, matchLast)
-- The abstract data type Doc represents pretty documents.
data Doc = Doc (Tokens -> Tokens)
......
download_tools.sh
View file @ 8cc6655e
......@@ -64,6 +64,9 @@ cd .cpm/packages
PKGV=`ls -d propertyfile-*`
mv $PKGV propertyfile
ln -s propertyfile $PKGV
PKGV=`ls -d queue-*`
mv $PKGV queue
ln -s queue $PKGV
PKGV=`ls -d random-*`
mv $PKGV random
ln -s random $PKGV
......@@ -76,6 +79,9 @@ cd .cpm/packages
PKGV=`ls -d socket-*`
mv $PKGV socket
ln -s socket $PKGV
PKGV=`ls -d wl-pprint-*`
mv $PKGV wl-pprint
ln -s wl-pprint $PKGV
PKGV=`ls -d frontend-exec-*`
mv $PKGV frontend-exec
ln -s frontend-exec $PKGV
......
optimize/.cpm/packages/queue/LICENSE 0 → 100644
View file @ 8cc6655e
Copyright (c) 2018, Michael Hanus
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
3. Neither the names of the copyright holders nor the names of its
contributors may be used to endorse or promote products derived from
this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
optimize/.cpm/packages/queue/README.md 0 → 100644
View file @ 8cc6655e
queue
=====
This package contains a library implementing
double-ended queues supporting access at both
ends in constant amortized time.
optimize/.cpm/packages/queue/package.json 0 → 100644
View file @ 8cc6655e
{
"name": "queue",
"version": "0.0.1",
"author": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "Library with double-ended queues supporting access at both ends in constant amortized time",
"category": [ "Data" ],
"license": "BSD-3-Clause",
"licenseFile": "LICENSE",
"dependencies": {
"base" : ">= 1.0.0, < 2.0.0",
"random" : ">= 0.0.1"
},
"compilerCompatibility": {
"pakcs": ">= 2.0.0",
"kics2": ">= 2.0.0"
},
"exportedModules": [ "Data.Queue" ],
"testsuite": {
"src-dir": "test",
"modules": [ "TestQueue" ]
},
"source": {
"git": "https://git.ps.informatik.uni-kiel.de/curry-packages/queue.git",
"tag": "$version"
}
}
optimize/.cpm/packages/queue/src/Data/Queue.curry 0 → 100644
View file @ 8cc6655e
------------------------------------------------------------------------------
--- An implementation of double-ended queues supporting access at both
--- ends in constant amortized time.
---
--- @author Bernd Brassel, Olaf Chitil, Michael Hanus, Sebastian Fischer,
--- Bjoern Peemoeller
--- @version December 2018
------------------------------------------------------------------------------
module Data.Queue
( -- Abstract data type, constructors and queries
Queue, empty, cons, snoc, isEmpty, deqLength
-- Selectors
, deqHead, deqTail, deqLast, deqInit, deqReverse, rotate, matchHead, matchLast
-- conversion from and to lists
, listToDeq, deqToList
) where
--- The datatype of a queue.
data Queue a = S Int [a] Int [a]
--- The empty queue.
empty :: Queue _
empty = S 0 [] 0 []
--- Inserts an element at the front of the queue.
cons :: a -> Queue a -> Queue a
cons x (S lenf f lenr r) = check (lenf + 1) (x : f) lenr r
--- Inserts an element at the end of the queue.
snoc :: a -> Queue a -> Queue a
snoc x (S lenf f lenr r) = deqReverse (check (lenr + 1) (x : r) lenf f)
--- Is the queue empty?
isEmpty :: Queue _ -> Bool
isEmpty (S lenf _ lenr _) = lenf + lenr == 0
--- Returns the number of elements in the queue.
deqLength :: Queue _ -> Int
deqLength (S lenf _ lenr _) = lenf + lenr
--- The first element of the queue.
deqHead :: Queue a -> a
deqHead (S lenf f _ r) = head (if lenf == 0 then r else f)
--- Removes an element at the front of the queue.
deqTail :: Queue a -> Queue a
deqTail (S _ [] _ _) = empty
deqTail (S lenf (_:fs) lenr r) = deqReverse (check lenr r (lenf - 1) fs)
--- The last element of the queue.
deqLast :: Queue a -> a
deqLast (S _ f lenr r) = head (if lenr == 0 then f else r)
--- Removes an element at the end of the queue.
deqInit :: Queue a -> Queue a
deqInit (S _ _ _ [] ) = empty
deqInit (S lenf f lenr (_:rs)) = check lenf f (lenr - 1) rs
--- Reverses a double ended queue.
deqReverse :: Queue a -> Queue a
deqReverse (S lenf f lenr r) = S lenr r lenf f
--- Moves the first element to the end of the queue.
rotate :: Queue a -> Queue a
rotate q = snoc (deqHead q) (deqTail q)
--- Matches the front of a queue.
--- `matchHead q` is equivalent to
--- `if isEmpty q then Nothing else Just (deqHead q, deqTail q)`
--- but more efficient.
matchHead :: Queue a -> Maybe (a, Queue a)
matchHead (S _ [] _ [] ) = Nothing
matchHead (S _ [] _ [x] ) = Just (x, empty)
matchHead (S _ [] _ (_:_:_))
= error $ "Data.Queue.matchHead: illegal queue"
matchHead (S lenf (x:xs) lenr r )
= Just (x, deqReverse (check lenr r (lenf - 1) xs))
--- Matches the end of a queue.
--- `matchLast q` is equivalent to
--- `if isEmpty q then Nothing else Just (deqLast q,deqInit q)`
--- but more efficient.
matchLast :: Queue a -> Maybe (a,Queue a)
matchLast (S _ [] _ [] ) = Nothing
matchLast (S _ [x] _ [] ) = Just (x, empty)
matchLast (S _ (_:_:_) _ [] )
= error $ "Data.Queue.matchLast: illegal queue"
matchLast (S lenf f lenr (x:xs)) = Just (x, check lenf f (lenr - 1) xs)
--- Transforms a list to a double ended queue.
listToDeq :: [a] -> Queue a
listToDeq xs = check (length xs) xs 0 []
--- Transforms a double ended queue to a list.
deqToList :: Queue a -> [a]
deqToList (S _ xs _ ys) = xs ++ reverse ys
--- Check for invariant: The length of the first list is smaller than
--- three times the length of the second plus 1.
check :: Int -> [a] -> Int -> [a] -> Queue a
check lenf f lenr r
| lenf <= 3 * lenr + 1 = S lenf f lenr r
| otherwise = S lenf' f' lenr' r'
where
len = lenf + lenr
lenf' = len `div` 2
lenr' = len - lenf'
(f', rf') = splitAt lenf' f
r' = r ++ reverse rf'
optimize/.cpm/packages/queue/test/RandomTest.curry 0 → 100644
View file @ 8cc6655e
-- A few auxiliary functions to formulate tests with random numbers.
module RandomTest ( test, eq ) where
import List ( nub )
import Test.EasyCheck
import System.Random
--- Tests a given predicate on a list of distinct random numbers.
--- In case of a failure, the list of random numbers is returned
--- in order to see the test cases in the CurryTest tool.
test :: ([Int] -> Bool) -> PropIO
test f = (rndList lenRnds >>= \xs -> return (if f xs then Nothing else Just xs))
`returns` Nothing
--- Tests whether two operations return equal results
--- on a list of distinct random numbers.
--- In case of a failure, the list of random numbers is returned
--- in order to see the test cases in the CurryTest tool.
eq :: Eq a => ([Int] -> a) -> ([Int] -> a) -> PropIO
eq f g = test (\x -> (f x)==(g x))
--- generate a list of at most n random numbers (without duplicated elements)
rndList :: Int -> IO [Int]
rndList n = getRandomSeed >>= return . nub . take n . (flip nextIntRange 100000)
--- maximal length of test lists
lenRnds :: Int
lenRnds = 1000
optimize/.cpm/packages/queue/test/TestQueue.curry 0 → 100644
View file @ 8cc6655e
import List
import Data.Queue
import RandomTest
deq f = f . listToDeq
deqs f = deqToList . f . listToDeq
testHead = eq (deq deqHead) head
testLast = eq (deq deqLast) last
testCons = eq (deqs (cons 73)) (73:)
testTail = eq (deqs (deqTail)) tail
testSnoc = eq (deqs (snoc 73)) (++[73])
testInit = eq (deqs deqInit) init
where
init [x] = []
init (x:y:ys) = x : init (y:ys)
testReverse = eq (deqs deqReverse) reverse
testLength = eq (deq deqLength) length
testRotate = eq (deqs rotate) (\ (x:xs) -> xs ++ [x])
optimize/.cpm/packages/redblacktree/README.md
View file @ 8cc6655e
redblacktree
============
This package contains library implementing
This package contains libraries implementing
red-black trees and efficient access structures,
like tables and sets, using red-black trees.
optimize/.cpm/packages/wl-pprint/LICENSE 0 → 100644
View file @ 8cc6655e
Copyright (c) 2017, <AUTHOR NAME>
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
3. Neither the names of the copyright holders nor the names of its
contributors may be used to endorse or promote products derived from
this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
optimize/.cpm/packages/wl-pprint/README.md 0 → 100644
View file @ 8cc6655e
wl-pprint
=========
This package provides pretty printing combinators for Curry.
It uses the interface of Daan Leijen's library for Haskell
(http://www.cs.uu.nl/~daan/download/pprint/pprint.html).
The linear-time bounded implementation is based on an approach by Olaf Chitil
(http://www.cs.kent.ac.uk/pubs/2006/2381/index.html).
Note that the implementation of `fill` and `fillBreak` is not linear-time bounded
Besides well-known pretty printing combinators, this library also supports ANSI
escape codes for formatting and colorisation of documents in text terminals
(see https://en.wikipedia.org/wiki/ANSI_escape_code).
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