Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
S
StdEnv-doc
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
Operations
Operations
Incidents
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Cloogle
StdEnv-doc
Commits
15f9ab77
Verified
Commit
15f9ab77
authored
Oct 29, 2017
by
Camil Staps
🚀
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
StdClass, StdFile, StdFunc, StdOrdList and _SystemArray
parent
3e1a5743
Changes
5
Show whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
403 additions
and
83 deletions
+403
-83
StdClass.dcl
StdClass.dcl
+61
-0
StdFile.dcl
StdFile.dcl
+212
-69
StdFunc.dcl
StdFunc.dcl
+29
-4
StdOrdList.dcl
StdOrdList.dcl
+42
-10
_SystemArray.dcl
_SystemArray.dcl
+59
-0
No files found.
StdClass.dcl
View file @
15f9ab77
definition
module
StdClass
definition
module
StdClass
/**
* Meta-classes with derived functions.
*/
// ****************************************************************************************
// ****************************************************************************************
// Concurrent Clean Standard Library Module Version 2.0
// Concurrent Clean Standard Library Module Version 2.0
// Copyright 1998 University of Nijmegen
// Copyright 1998 University of Nijmegen
...
@@ -12,40 +16,97 @@ from StdBool import not
...
@@ -12,40 +16,97 @@ from StdBool import not
// For the time-being, macro definitions are used for this purpose
// For the time-being, macro definitions are used for this purpose
// This may cause misleading error messages in case of type errors
// This may cause misleading error messages in case of type errors
/**
* Meta-class describing interval types with an absolute zero.
*/
class
PlusMin
a
|
+
,
-
,
zero
a
class
PlusMin
a
|
+
,
-
,
zero
a
/**
* Meta-class describing ratio types.
*/
class
MultDiv
a
|
*
,
/
,
one
a
class
MultDiv
a
|
*
,
/
,
one
a
/**
* Meta-class describing arithmetical types.
*/
class
Arith
a
|
PlusMin
,
MultDiv
,
abs
,
sign
,
~
a
class
Arith
a
|
PlusMin
,
MultDiv
,
abs
,
sign
,
~
a
/**
* Meta-class describing types that can be incremented and decremented.
*/
class
IncDec
a
|
+
,
-
,
one
,
zero
a
class
IncDec
a
|
+
,
-
,
one
,
zero
a
where
where
/**
* Increment a value by one.
*/
inc
::
!
a
->
a
|
+
,
one
a
inc
::
!
a
->
a
|
+
,
one
a
inc
x
:==
x
+
one
inc
x
:==
x
+
one
/**
* Decrement a value by one.
*/
dec
::
!
a
->
a
|
-
,
one
a
dec
::
!
a
->
a
|
-
,
one
a
dec
x
:==
x
-
one
dec
x
:==
x
-
one
/**
* Meta-class describing types that can be enumerated.
*/
class
Enum
a
|
<
,
IncDec
a
class
Enum
a
|
<
,
IncDec
a
/**
* Equality.
*
* @var The type for which values can be equated
*/
class
Eq
a
|
==
a
class
Eq
a
|
==
a
where
where
/**
* Inequality.
*
* @result True iff the parameters are not equal
*/
(<>)
infix
4
::
!
a
!
a
->
Bool
|
Eq
a
(<>)
infix
4
::
!
a
!
a
->
Bool
|
Eq
a
(<>)
x
y
:==
not
(
x
==
y
)
(<>)
x
y
:==
not
(
x
==
y
)
/**
* Ordering.
*
* @var The type that can be ordered.
*/
class
Ord
a
|
<
a
class
Ord
a
|
<
a
where
where
/**
* Greater than.
*
* @result True iff the first value is strictly greater than the second value.
*/
(>)
infix
4
::
!
a
!
a
->
Bool
|
Ord
a
(>)
infix
4
::
!
a
!
a
->
Bool
|
Ord
a
(>)
x
y
:==
y
<
x
(>)
x
y
:==
y
<
x
/**
* Smaller than or equal to.
*
* @result True iff the first value is smaller than or equal to the second value.
*/
(<=)
infix
4
::
!
a
!
a
->
Bool
|
Ord
a
(<=)
infix
4
::
!
a
!
a
->
Bool
|
Ord
a
(<=)
x
y
:==
not
(
y
<
x
)
(<=)
x
y
:==
not
(
y
<
x
)
/**
* Greater than or equal to.
*
* @result True iff the first value is greater than or equal to the second value.
*/
(>=)
infix
4
::
!
a
!
a
->
Bool
|
Ord
a
(>=)
infix
4
::
!
a
!
a
->
Bool
|
Ord
a
(>=)
x
y
:==
not
(
x
<
y
)
(>=)
x
y
:==
not
(
x
<
y
)
/**
* The minimum of two values.
*/
min
::!
a
!
a
->
a
|
Ord
a
min
::!
a
!
a
->
a
|
Ord
a
min
x
y
:==
case
(
x
<
y
)
of
True
=
x
;
_
=
y
min
x
y
:==
case
(
x
<
y
)
of
True
=
x
;
_
=
y
/**
* The maximum of two values.
*/
max
::!
a
!
a
->
a
|
Ord
a
max
::!
a
!
a
->
a
|
Ord
a
max
x
y
:==
case
(
x
<
y
)
of
True
=
y
;
_
=
x
max
x
y
:==
case
(
x
<
y
)
of
True
=
y
;
_
=
x
StdFile.dcl
View file @
15f9ab77
system
module
StdFile
system
module
StdFile
/**
* Functions to manipulate the file system with the File type.
*/
// ****************************************************************************************
// ****************************************************************************************
// Concurrent Clean Standard Library Module Version 2.0
// Concurrent Clean Standard Library Module Version 2.0
// Copyright 1998 University of Nijmegen
// Copyright 1998 University of Nijmegen
...
@@ -7,110 +11,237 @@ system module StdFile
...
@@ -7,110 +11,237 @@ system module StdFile
// File modes synonyms
// File modes synonyms
FReadText
:==
0
// Read from a text file
/**
FWriteText
:==
1
// Write to a text file
* File mode: read text
FAppendText
:==
2
// Append to an existing text file
* @type Int
FReadData
:==
3
// Read from a data file
*/
FWriteData
:==
4
// Write to a data file
FReadText
:==
0
FAppendData
:==
5
// Append to an existing data file
/**
* File mode: write text
* @type Int
*/
FWriteText
:==
1
/**
* File mode: append text
* @type Int
*/
FAppendText
:==
2
/**
* File mode: read data
* @type Int
*/
FReadData
:==
3
/**
* File mode: write data
* @type Int
*/
FWriteData
:==
4
/**
* File mode: append data
* @type Int
*/
FAppendData
:==
5
// Seek modes synonyms
// Seek modes synonyms
FSeekSet
:==
0
// New position is the seek offset
/**
FSeekCur
:==
1
// New position is the current position plus the seek offset
* Seek mode: the new position is the seek offset
FSeekEnd
:==
2
// New position is the size of the file plus the seek offset
* @type Int
*/
FSeekSet
:==
0
::
*
Files
/**
* Seek mode: the new position is the current position plus the seek offset
* @type Int
*/
FSeekCur
:==
1
// Acces to the FileSystem (Files)
/**
* Seek mode: the new position is the size of the file plus the seek offset
* @type Int
*/
FSeekEnd
:==
2
/**
* The filesystem environment, independent from *World. This type can only be
* used through the FileSystem and FileEnv classes.
*/
::
*
Files
/**
* Access to the filesystem.
*
* @var The unique type that is used to ensure purity.
*/
class
FileSystem
f
where
class
FileSystem
f
where
/**
* Opens a file for the first time in a certain mode.
* @param The filename
* @param The mode (read / write / append; text / data)
* @param The {{`FileSystem`}} (usually {{`World`}})
* @result A boolean indicating success
* @result The {{`File`}}
* @result The new {{`FileSystem`}}
*/
fopen
::
!{#
Char
}
!
Int
!*
f
->
(!
Bool
,!*
File
,!*
f
)
fopen
::
!{#
Char
}
!
Int
!*
f
->
(!
Bool
,!*
File
,!*
f
)
/* Opens a file for the first time in a certain mode (read, write or append, text or data).
The boolean output parameter reports success or failure. */
/**
* Closes a file.
* @param The {{`File`}}
* @param The {{`FileSystem`}}
* @result A boolean indicating success
* @result The new {{`FileSystem`}}
*/
fclose
::
!*
File
!*
f
->
(!
Bool
,!*
f
)
fclose
::
!*
File
!*
f
->
(!
Bool
,!*
f
)
/* Closes a file */
/**
* Open the 'Console' for reading and writing.
*/
stdio
::
!*
f
->
(!*
File
,!*
f
)
stdio
::
!*
f
->
(!*
File
,!*
f
)
/* Open the 'Console' for reading and writing. */
/**
* With `sfopen` a file can be opened for reading more than once. On a file
* opened by `sfopen` only the operations beginning with `sf` can be used.
* The `sf...` operations work just like the corresponding `f...`
* operations. They can't be used for files opened with {{`fopen`} or
* {{`freopen`}}.
*
* @param The filename
* @param The mode (read; text / data)
* @param The {{`FileSystem`}} (usually {{`World`}})
* @result A boolean indicating success
* @result The new {{`File`}}
* @result The new {{`FileSystem`}}
*/
sfopen
::
!{#
Char
}
!
Int
!*
f
->
(!
Bool
,!
File
,!*
f
)
sfopen
::
!{#
Char
}
!
Int
!*
f
->
(!
Bool
,!
File
,!*
f
)
/* With sfopen a file can be opened for reading more than once.
On a file opened by sfopen only the operations beginning with sf can be used.
The sf... operations work just like the corresponding f... operations.
They can't be used for files opened with fopen or freopen. */
instance
FileSystem
Files
instance
FileSystem
Files
instance
FileSystem
World
instance
FileSystem
World
/**
* An environment in which files can be dealt with.
*
* @var The unique type that is used to ensure purity.
*/
class
FileEnv
env
where
class
FileEnv
env
where
accFiles
::
!.(*
Files
->
(.
x
,*
Files
))
!*
env
->
(!.
x
,!*
env
)
accFiles
::
!.(*
Files
->
(.
x
,*
Files
))
!*
env
->
(!.
x
,!*
env
)
appFiles
::
!.(*
Files
->
*
Files
)
!*
env
->
*
env
appFiles
::
!.(*
Files
->
*
Files
)
!*
env
->
*
env
instance
FileEnv
World
instance
FileEnv
World
// openfiles :: !*World -> (!*Files,!*World) // no longer supported
/**
// closefiles :: !*Files !*World -> *World // no longer supported
* Re-opens an open file in a possibly different mode.
* @param The file
* @param The new mode
* @result A boolean indicating successful closing before reopening
* @result The new file
*/
freopen
::
!*
File
!
Int
->
(!
Bool
,!*
File
)
freopen
::
!*
File
!
Int
->
(!
Bool
,!*
File
)
/* Re-opens an open file in a possibly different mode.
The boolean indicates whether the file was successfully closed before reopening. */
// Reading from a File:
// Reading from a File:
/**
* Reads a character from a text file or a byte from a datafile.
* @result A boolean indicating success
* @result The read character
*/
freadc
::
!*
File
->
(!
Bool
,!
Char
,!*
File
)
freadc
::
!*
File
->
(!
Bool
,!
Char
,!*
File
)
/* Reads a character from a text file or a byte from a datafile.
The boolean indicates succes or failure */
/**
* Reads an Integer from a textfile by skipping spaces, tabs and newlines and
* then reading digits, which may be preceeded by a plus or minus sign.
* From a datafile `freadi` will just read four bytes (a Clean Int).
* @result A boolean indicating success
* @result The read integer
*/
freadi
::
!*
File
->
(!
Bool
,!
Int
,!*
File
)
freadi
::
!*
File
->
(!
Bool
,!
Int
,!*
File
)
/* Reads an Integer from a textfile by skipping spaces, tabs and newlines and
then reading digits, which may be preceeded by a plus or minus sign.
From a datafile freadi will just read four bytes (a Clean Int). */
/**
* Reads a Real from a textfile by skipping spaces, tabs and newlines and then
* reading a character representation of a Real number.
* From a datafile `freadr` will just read eight bytes (a Clean Real).
* @result A boolean indicating success
* @result The read real
*/
freadr
::
!*
File
->
(!
Bool
,!
Real
,!*
File
)
freadr
::
!*
File
->
(!
Bool
,!
Real
,!*
File
)
/* Reads a Real from a textfile by skipping spaces, tabs and newlines and then
reading a character representation of a Real number.
From a datafile freadr will just read eight bytes (a Clean Real). */
/**
* Reads n characters from a text or data file, which are returned as a String.
* If the file doesn't contain n characters the file will be read to the end
* of the file. An empty String is returned if no characters can be read.
* @param The file
* @param The amount of characters to read
* @result The read string
* @result The file
*/
freads
::
!
*
File
!
Int
->
(!*{#
Char
},!*
File
)
freads
::
!
*
File
!
Int
->
(!*{#
Char
},!*
File
)
/* Reads n characters from a text or data file, which are returned as a String.
If the file doesn't contain n characters the file will be read to the end
of the file. An empty String is returned if no characters can be read. */
/**
* Reads `n` characters from a text or data file, which are returned in the
* string `arg3` at positions `arg1`..`arg1+arg2-1`. If the file doesn't
* contain `arg2` characters the file will be read to the end of the file, and
* the part of the string `arg3` that could not be read will not be changed.
*
* @param The start of the substring to modify
* @param The length of the substring
* @param The string to modify
* @result The number of characters read
* @result The modified string
*/
freadsubstring
::
!
Int
!
Int
!*{#
Char
}
!*
File
->
(!
Int
,!*{#
Char
},!*
File
)
freadsubstring
::
!
Int
!
Int
!*{#
Char
}
!*
File
->
(!
Int
,!*{#
Char
},!*
File
)
/*
Reads n characters from a text or data file, which are returned in the string
arg3 at positions arg1..arg1+arg2-1. If the file doesn't contain arg2 characters
the file will be read to the end of the file, and the part of the string arg3 that
could not be read will not be changed. The number of characters read, the modified
string and the file are returned.
*/
/**
* Reads a line from a textfile, including a newline character, except for the
* last line. `freadline` cannot be used on data files.
*/
freadline
::
!*
File
->
(!*{#
Char
},!*
File
)
freadline
::
!*
File
->
(!*{#
Char
},!*
File
)
/* Reads a line from a textfile. (including a newline character, except for the last
line) freadline cannot be used on data files. */
// Writing to a File:
// Writing to a File:
/**
* Writes a character to a textfile.
* To a datafile fwritec writes one byte (a Clean Char).
*/
fwritec
::
!
Char
!*
File
->
*
File
fwritec
::
!
Char
!*
File
->
*
File
/* Writes a character to a textfile.
To a datafile fwritec writes one byte (a Clean Char). */
/**
* Writes an Integer (its textual representation) to a text file. To a datafile
* fwritei writes four bytes (a Clean Int).
*/
fwritei
::
!
Int
!*
File
->
*
File
fwritei
::
!
Int
!*
File
->
*
File
/* Writes an Integer (its textual representation) to a text file.
To a datafile fwritei writes four bytes (a Clean Int). */
/**
* Writes a Real (its textual representation) to a text file. To a datafile
* fwriter writes eight bytes (a Clean Real).
*/
fwriter
::
!
Real
!*
File
->
*
File
fwriter
::
!
Real
!*
File
->
*
File
/* Writes a Real (its textual representation) to a text file.
To a datafile fwriter writes eight bytes (a Clean Real). */
/**
* Writes a String to a text or data file.
*/
fwrites
::
!{#
Char
}
!*
File
->
*
File
fwrites
::
!{#
Char
}
!*
File
->
*
File
/* Writes a String to a text or data file. */
/**
* Writes the characters at positions `arg1`..`arg1+arg2-1` of string `arg3` to
* a text or data file.
*/
fwritesubstring
::
!
Int
!
Int
!{#
Char
}
!*
File
->
*
File
fwritesubstring
::
!
Int
!
Int
!{#
Char
}
!*
File
->
*
File
/* Writes the characters at positions arg1..arg1+arg2-1 of string arg3 to
a text or data file. */
/**
* Overloaded write to file. This allows you to chain write operations, like:
* `# f = f <<< "X is: " <<< x <<< "; y is: " <<< y <<< "\n"`
*
* @var The type that can be written to a file
* @param The File
* @param The thing to write
* @result The new File
*/
class
(<<<)
infixl
a
::
!*
File
!
a
->
*
File
class
(<<<)
infixl
a
::
!*
File
!
a
->
*
File
/* Overloaded write to file */
instance
<<<
Int
instance
<<<
Int
instance
<<<
Char
instance
<<<
Char
...
@@ -119,24 +250,37 @@ instance <<< Real
...
@@ -119,24 +250,37 @@ instance <<< Real
// Testing:
// Testing:
/**
* @result Whether end-of-file has been reached
*/
fend
::
!*
File
->
(!
Bool
,!*
File
)
fend
::
!*
File
->
(!
Bool
,!*
File
)
/* Tests for end-of-file. */
/**
* @result Whether an error has occurred during previous file I/O operations
*/
ferror
::
!*
File
->
(!
Bool
,!*
File
)
ferror
::
!*
File
->
(!
Bool
,!*
File
)
/* Has an error occurred during previous file I/O operations? */
/**
* @result The current position of the file pointer as an Integer. This
* position can be used later on for the fseek function.
*/
fposition
::
!*
File
->
(!
Int
,!*
File
)
fposition
::
!*
File
->
(!
Int
,!*
File
)
/* returns the current position of the file poInter as an Integer.
This position can be used later on for the fseek function. */
/**
* Move to a different position in the file
*
* @param The offset
* @param A seek mode ({{`FSeekSet`}}, {{`FSeekCur`}} or {{`FSeekEnd`}})
* @result True iff the seek was successful
*/
fseek
::
!*
File
!
Int
!
Int
->
(!
Bool
,!*
File
)
fseek
::
!*
File
!
Int
!
Int
->
(!
Bool
,!*
File
)
/* Move to a different position in the file, the first Integer argument is the offset,
the second argument is a seek mode. (see above). True is returned if successful. */
// Predefined files.
// Predefined files.
/**
* Open the 'Errors' file for writing only. May be opened more than once.
*/
stderr
::
*
File
stderr
::
*
File
/* Open the 'Errors' file for writing only. May be opened more than once. */
// Opening and reading Shared Files:
// Opening and reading Shared Files:
...
@@ -149,11 +293,10 @@ sfseek :: !File !Int !Int -> (!Bool,!File)
...
@@ -149,11 +293,10 @@ sfseek :: !File !Int !Int -> (!Bool,!File)
sfend
::
!
File
->
Bool
sfend
::
!
File
->
Bool
sfposition
::
!
File
->
Int
sfposition
::
!
File
->
Int
/* The functions sfend and sfposition work like fend and fposition, but don't return a
new file on which other operations can continue. They can be used for files opened
with sfopen or after fshare, and in guards for files opened with fopen or freopen. */
// Convert a *File into:
// Convert a *File into:
/**
* Change a file so that from now it can only be used with `sf...` operations.
*/
fshare
::
!*
File
->
File
fshare
::
!*
File
->
File
/* Change a file so that from now it can only be used with sf... operations. */
StdFunc.dcl
View file @
15f9ab77
...
@@ -85,15 +85,40 @@ iter :: !Int (.a -> .a) .a -> .a
...
@@ -85,15 +85,40 @@ iter :: !Int (.a -> .a) .a -> .a
// Some handy functions for transforming unique states:
// Some handy functions for transforming unique states:
seq
::
![.(.
s
->
.
s
)]
.
s
->
.
s
// fn-1 (..(f1 (f0 x))..)
/**
seqList
::
![
St
.
s
.
a
]
.
s
->
([.
a
],.
s
)
// fn-1 (..(f1 (f0 x))..)
* Iterate a list of state functions.
*
* @param The functions
* @param The initial state
* @result The final state
*/
seq
::
![.(.
s
->
.
s
)]
.
s
->
.
s
/**
* Iterate a list of state functions with result
*
* @param The functions
* @param The initial state
* @result A list of results from the state function and the final state
*/
seqList
::
![
St
.
s
.
a
]
.
s
->
([.
a
],.
s
)
/**
* A function that updates a state and produces a result.
*/
::
St
s
a
:==
s
->
*(
a
,
s
)
::
St
s
a
:==
s
->
*(
a
,
s
)
// monadic style:
// monadic style:
(
`
bind`
)
infix
0
// :: w:(St .s .a) v:(.a -> .(St .s .b)) -> u:(St .s .b), [u <= v, u <= w]
/**
* Monadic bind for the {{`St`}} type.
* @type w:(St .s .a) v:(.a -> .(St .s .b)) -> u:(St .s .b), [u <= v, u <= w]
*/
(
`
bind`
)
infix
0
(
`
bind`
)
f
g
:==
\
st0
->
let
(
r
,
st1
)
=
f
st0
in
g
r
st1
(
`
bind`
)
f
g
:==
\
st0
->
let
(
r
,
st1
)
=
f
st0
in
g
r
st1
// return :: u:a -> u:(St .s u:a)
/**
* Monadic return for the {{`St`}} type.
* @type u:a -> u:(St .s u:a)
*/
return
r
:==
\
s
->
(
r
,
s
)
return
r
:==
\
s
->
(
r
,
s
)
StdOrdList.dcl
View file @
15f9ab77
...
@@ -7,29 +7,61 @@ definition module StdOrdList
...
@@ -7,29 +7,61 @@ definition module StdOrdList
import
StdClass
import
StdClass
sort
::
!
u
:[
a
]
->
u
:[
a
]
|
Ord
a
// Sort the list (mergesort)
/**
* Sort a list (mergesort).
*/
sort
::
!
u
:[
a
]
->
u
:[
a
]
|
Ord
a
special
special
a
=
Char
a
=
Char
a
=
Int
a
=
Int
a
=
Real
a
=
Real
sortBy
::
(
a
a
->
Bool
)
!
u
:[
a
]
->
u
:[
a
]
// Sort the list, arg1 is < function
merge
::
!
u
:[
a
]
!
v
:[
a
]
->
w
:[
a
]
/**
|
Ord
a
,[
u
v
<=
w
]
// Merge two sorted lists giving a sorted list
* Sort a list using a custom ordering.
* @param The custom {{`<`}} function
*/
sortBy
::
(
a
a
->
Bool
)
!
u
:[
a
]
->
u
:[
a
]
/**
* Merge two sorted lists.
*/
merge
::
!
u
:[
a
]
!
v
:[
a
]
->
w
:[
a
]
|
Ord
a
,[
u
v
<=
w
]
special
special
a
=
Char
a
=
Char