Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Tim Steenvoorden
clean-base
Commits
df67f0c9
Commit
df67f0c9
authored
Mar 03, 2016
by
Tim Steenvoorden
Browse files
add first IO implementation
parent
41608b8e
Changes
18
Hide whitespace changes
Inline
Side-by-side
src/Clean/Core.dcl
View file @
df67f0c9
...
...
@@ -20,7 +20,3 @@ import Algebra.Ring
import
Algebra
.
Lattice
import
Text
.
Show
// import System.Console
// import System.File
// import System.Process
src/Clean/Core.icl
View file @
df67f0c9
...
...
@@ -2,16 +2,37 @@ implementation module Clean.Core
import
Clean
.
Core
a
::
{#
Char
}
a
=
{
'a'
,
'b'
}
b
::
{#
Char
}
b
=
{
'a'
,
'b'
}
c
::
{#
Int
}
c
=
{
1
,
2
}
d
::
{#
Int
}
d
=
{
1
,
2
}
d
=
{
3
,
4
}
// e :: {#Nat}
// e = {nat 1, nat 2}
::
NewInt
=
{
n
::
Int
}
instance
Semigroup
{#
NewInt
}
where
(+)
xs
ys
=
concatUnboxedArray
xs
ys
// concatUnboxedArray :: {#a} {#a} -> {#a}
concatUnboxedArray
xs
ys
#
// new = array (size xs + size ys) neutral
new
=
unsafeArray
(
size
xs
+
size
ys
)
new
=
{
new
&
[
i
]
=
xs
.[
i
]
\\
i
<-
[
0
..
pred
(
size
xs
)]
}
new
=
{
new
&
[
i
+
size
xs
]
=
ys
.[
i
]
\\
i
<-
[
0
..
pred
(
size
ys
)]
}
:==
new
f
::
{#
NewInt
}
f
=
{{
n
=
5
},
{
n
=
6
}}
g
::
{#
NewInt
}
g
=
{{
n
=
7
},
{
n
=
8
}}
n0
=
nat
0
n1
=
nat
1
n2
=
nat
2
n_
=
nat
-1
Start
=
((
show
a
,
show
4
),
(
a
,
c
))
Start
=
[
n2
.-
n1
,
n1
.-
n0
,
n1
.-
n2
,
n_
]
src/Clean/Prim.icl
View file @
df67f0c9
...
...
@@ -102,176 +102,3 @@ prim_sliceString s a b = code inline {
jsr
sliceAC
.o
1
0
}
/// # Files
/// ## Opening and Closing
/// 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.
prim_openFile
::
!
String
!
Int
->
(!
Bool
,!*
File
)
prim_openFile
s
i
=
code inline {
.d
1
1
i
jsr
openF
.o
0
3
b
f
}
/// Closes a file.
/// The boolean output parameter reports whether the file was successfully closed.
prim_closeFile
::
!*
File
->
Bool
prim_closeFile
f
=
code inline {
.d
0
2
f
jsr
closeF
.o
0
1
b
}
/// Re-opens an open file in a possibly different mode.
/// The boolean indicates whether the file was successfully closed before reopening.
prim_reopenFile
::
!*
File
!
Int
->
(!
Bool
,!*
File
)
prim_reopenFile
f
m
=
code inline {
.d
0
3
f
i
jsr
reopenF
.o
0
3
b
f
}
/// ## Standard IO
/// Open the 'Console' for reading and writing.
prim_stdio
::
*
File
prim_stdio
=
code inline {
.d
0
0
jsr
stdioF
.o
0
2
f
}
/// Open the 'Errors' file for writing only. May be opened more than once.
prim_stderr
::
*
File
prim_stderr
=
code inline {
.d
0
0
jsr
stderrF
.o
0
2
f
}
/// ## Seeking
/// Returns the current position of the file pointer as an integer.
/// This position can be used later on for the fseek function.
prim_positionFile
::
!*
File
->
(!
Int
,!*
File
)
prim_positionFile
f
=
code inline {
.d
0
2
f
jsr
positionF
.o
0
3
i
f
}
/// 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.
prim_seekFile
::
!*
File
!
Int
!
Int
->
(!
Bool
,!*
File
)
prim_seekFile
f
p
m
=
code inline {
.d
0
4
f
i
i
jsr
seekF
.o
0
3
b
f
}
/// ## Tests
/// Tests for end-of-file.
prim_isEndFile
::
!*
File
->
(!
Bool
,!*
File
)
prim_isEndFile
f
=
code inline {
.d
0
2
f
jsr
endF
.o
0
3
b
f
}
/// Has an error occurred during previous file I/O operations?
prim_isErrorFile
::
!*
File
->
(!
Bool
,!*
File
)
prim_isErrorFile
f
=
code inline {
.d
0
2
f
jsr
errorF
.o
0
3
b
f
}
/// ## Reading
/// Reads a character from a text file or a byte from a datafile.
prim_readCharFile
::
!*
File
->
(!
Bool
,!
Char
,!*
File
)
prim_readCharFile
f
=
code inline {
.d
0
2
f
jsr
readFC
.o
0
4
b
c
f
}
/// 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).
prim_readIntFile
::
!*
File
->
(!
Bool
,!
Int
,!*
File
)
prim_readIntFile
f
=
code inline {
.d
0
2
f
jsr
readFI
.o
0
4
b
i
f
}
/// 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).
prim_readRealFile
::!*
File
->
(!
Bool
,!
Real
,!*
File
)
prim_readRealFile
f
=
code inline {
.d
0
2
f
jsr
readFR
.o
0
5
b
r
f
}
/// 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.
prim_readStringFile
::
!*
File
!
Int
->
(!*
String
,!*
File
)
prim_readStringFile
f
l
=
code inline {
.d
0
3
f
i
jsr
readFS
.o
1
2
f
}
/// Reads a line from a textfile. (including a newline character, except for the last
/// line) freadline cannot be used on data files.
prim_readLineFile
::
!*
File
->
(!*
String
,!*
File
)
prim_readLineFile
f
=
code inline {
.d
0
2
f
jsr
readLineF
.o
1
2
f
}
/// ## Writing
/// Writes a character to a textfile.
/// To a datafile fwritec writes one byte (a Clean Char).
prim_writeCharFile
::
!
Char
!*
File
->
*
File
prim_writeCharFile
c
f
=
code inline {
.d
0
3
c
f
jsr
writeFC
.o
0
2
f
}
/// Writes an integer (its textual representation) to a text file.
/// To a datafile fwritec writes four bytes (a Clean Int).
prim_writeIntFile
::
!
Int
!*
File
->
*
File
prim_writeIntFile
i
f
=
code inline {
.d
0
3
i
f
jsr
writeFI
.o
0
2
f
}
/// Writes a real (its textual representation) to a text file.
/// To a datafile fwriter writes eight bytes (a Clean Real).
prim_writeRealFile
::
!
Real
!*
File
->
*
File
prim_writeRealFile
r
f
=
code inline {
.d
0
4
r
f
jsr
writeFR
.o
0
2
f
}
/// Writes a String to a text or data file.
prim_writeStringFile
::
!
String
!*
File
->
*
File
prim_writeStringFile
s
f
=
code inline {
.d
1
2
f
jsr
writeFS
.o
0
2
f
}
src/Data/Error.dcl
View file @
df67f0c9
...
...
@@ -16,3 +16,27 @@ from Text.Show import class Show
instance
Show
Error
/* Add or not?
/// # Helpers
Error e :== Left e
Ok r :== Right r
/// Return True when the argument is an Ok value and return False otherwise.
isOk r :== isRight r
/// Return True when the argument is an Error value and return False otherwise.
isError e :== isLeft e
/// Return the contents of an Ok value and abort at run-time otherwise.
fromOk r :== fromRight r
/// Return the contents of an Error value and abort at run-time otherwise.
fromError e :== fromLeft e
mapOk f r :== mapRight f r
mapError f r :== mapLeft f r
wrap r :== Ok r
rewrap f r :== mapOk f r
throw e :== Error e
rethrow f e :== mapError f e
*/
src/Data/File.icl
0 → 100644
View file @
df67f0c9
implementation
module
Data
.
File
//TODO change `prim_` prefix to just `_` and move to internal module.
/// ## Opening and Closing
/// 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.
prim_openFile
::
!
String
!
Int
->
(!
Bool
,!*
File
)
prim_openFile
s
i
=
code inline {
.d
1
1
i
jsr
openF
.o
0
3
b
f
}
/// Closes a file.
/// The boolean output parameter reports whether the file was successfully closed.
prim_closeFile
::
!*
File
->
Bool
prim_closeFile
f
=
code inline {
.d
0
2
f
jsr
closeF
.o
0
1
b
}
/// Re-opens an open file in a possibly different mode.
/// The boolean indicates whether the file was successfully closed before reopening.
prim_reopenFile
::
!*
File
!
Int
->
(!
Bool
,!*
File
)
prim_reopenFile
f
m
=
code inline {
.d
0
3
f
i
jsr
reopenF
.o
0
3
b
f
}
/// ## Standard IO
/// Open the 'Console' for reading and writing.
prim_stdio
::
*
File
prim_stdio
=
code inline {
.d
0
0
jsr
stdioF
.o
0
2
f
}
/// Open the 'Errors' file for writing only. May be opened more than once.
prim_stderr
::
*
File
prim_stderr
=
code inline {
.d
0
0
jsr
stderrF
.o
0
2
f
}
/// ## Seeking
/// Returns the current position of the file pointer as an integer.
/// This position can be used later on for the fseek function.
prim_positionFile
::
!*
File
->
(!
Int
,!*
File
)
prim_positionFile
f
=
code inline {
.d
0
2
f
jsr
positionF
.o
0
3
i
f
}
/// 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.
prim_seekFile
::
!*
File
!
Int
!
Int
->
(!
Bool
,!*
File
)
prim_seekFile
f
p
m
=
code inline {
.d
0
4
f
i
i
jsr
seekF
.o
0
3
b
f
}
/// ## Tests
/// Tests for end-of-file.
prim_isEndOfFile
::
!*
File
->
(!
Bool
,!*
File
)
prim_isEndOfFile
f
=
code inline {
.d
0
2
f
jsr
endF
.o
0
3
b
f
}
/// Has an error occurred during previous file I/O operations?
prim_isErrorFile
::
!*
File
->
(!
Bool
,!*
File
)
prim_isErrorFile
f
=
code inline {
.d
0
2
f
jsr
errorF
.o
0
3
b
f
}
/// ## Reading
/// Reads a character from a text file or a byte from a datafile.
prim_readCharFile
::
!*
File
->
(!
Bool
,!
Char
,!*
File
)
prim_readCharFile
f
=
code inline {
.d
0
2
f
jsr
readFC
.o
0
4
b
c
f
}
/// 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).
prim_readIntFile
::
!*
File
->
(!
Bool
,!
Int
,!*
File
)
prim_readIntFile
f
=
code inline {
.d
0
2
f
jsr
readFI
.o
0
4
b
i
f
}
/// 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).
prim_readRealFile
::!*
File
->
(!
Bool
,!
Real
,!*
File
)
prim_readRealFile
f
=
code inline {
.d
0
2
f
jsr
readFR
.o
0
5
b
r
f
}
/// 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.
prim_readStringFile
::
!*
File
!
Int
->
(!*
String
,!*
File
)
prim_readStringFile
f
l
=
code inline {
.d
0
3
f
i
jsr
readFS
.o
1
2
f
}
/// Reads a line from a textfile. (including a newline character, except for the last
/// line) freadline cannot be used on data files.
prim_readLineFile
::
!*
File
->
(!*
String
,!*
File
)
prim_readLineFile
f
=
code inline {
.d
0
2
f
jsr
readLineF
.o
1
2
f
}
/// ## Writing
/// Writes a character to a textfile.
/// To a datafile fwritec writes one byte (a Clean Char).
prim_writeCharFile
::
!
Char
!*
File
->
*
File
prim_writeCharFile
c
f
=
code inline {
.d
0
3
c
f
jsr
writeFC
.o
0
2
f
}
/// Writes an integer (its textual representation) to a text file.
/// To a datafile fwritec writes four bytes (a Clean Int).
prim_writeIntFile
::
!
Int
!*
File
->
*
File
prim_writeIntFile
i
f
=
code inline {
.d
0
3
i
f
jsr
writeFI
.o
0
2
f
}
/// Writes a real (its textual representation) to a text file.
/// To a datafile fwriter writes eight bytes (a Clean Real).
prim_writeRealFile
::
!
Real
!*
File
->
*
File
prim_writeRealFile
r
f
=
code inline {
.d
0
4
r
f
jsr
writeFR
.o
0
2
f
}
/// Writes a String to a text or data file.
prim_writeStringFile
::
!
String
!*
File
->
*
File
prim_writeStringFile
s
f
=
code inline {
.d
1
2
f
jsr
writeFS
.o
0
2
f
}
src/Data/List.icl
View file @
df67f0c9
...
...
@@ -128,7 +128,7 @@ instance % [a]
instance toString [x] | toChar x
where
// toString::![x] -> {#Char} | toChar x
toString xs = ltosacc 0 xs (
createA
rray l ' ')
toString xs = ltosacc 0 xs (
a
rray l ' ')
where
l = length xs
ltosacc i [h:t] arr = ltosacc (inc i) t {arr & [i]=toChar h}
...
...
src/Overview.dcl
View file @
df67f0c9
...
...
@@ -88,8 +88,6 @@ instance Sliceable Slice
/// # Literals
module
Data
.
Int
class
IsInt
a
where
fromInt
::
Int
->
a
...
...
src/System/Console.dcl
View file @
df67f0c9
definition
module
System
.
Console
src/System/Directory.dcl
0 → 100644
View file @
df67f0c9
definition
module
System
.
Console
src/System/Environment.dcl
0 → 100644
View file @
df67f0c9
definition
module
System
.
Console
src/System/Exit.dcl
0 → 100644
View file @
df67f0c9
src/System/File.dcl
View file @
df67f0c9
definition
module
System
.
File
definition
module
System
.
IO
from
Data
.
Error
import
::
Error
,
::
Usually
from
Data
.
Either
import
::
Either
...
...
@@ -8,28 +8,49 @@ from Data.Either import :: Either
// :: File
// BUILTIN
::
Path
:==
String
/// # IOModes
::
IOMode
(:==
Int
)
ReadMode
,
WriteMode
,
AppendMode
::
IOMode
ReadMode
=
0
WriteMode
=
1
AppendMode
=
2
ReadWriteMode
=
undefined
::
SeekMode
(:==
Int
)
AbsoluteSeek
,
RelativeSeek
,
SeekFromEnd
::
SeekMode
AbsoluteSeek
=
0
RelativeSeek
=
1
SeekFromEnd
=
2
::
FilePath
:==
String
::
Error
|
DoesNotExist
|
FileDoesNotExist
|
AlreadyExists
|
FileAlreadyExists
|
Permission
|
FilePermission
Denied
|
EOFError
|
FileIs
EOF
|
FullError
|
FileFull
|
Illegal
OperationError
|
FileIllegal
Operation
|
UserError
[
Char
]
|
FileUserError
|
FileDoesNotExist
|
FileAlreadyExists
|
PermissionDenied
|
FileIs
AtEnd
|
File
Is
Full
|
Illegal
File
Operation
|
User
File
Error
[
Char
]
/// # Opening and Closing
openFile
::
!
Path
!
FileMode
!*
World
->
*(
Usually
*
File
,
*
World
)
withFile
::
!
FilePath
!
IOMode
(!*
File
->
*(
Usually
a
,
*
File
))
->
*(
Usually
a
,
*
File
)
openFile
::
!
FilePath
!
IOMode
!*
World
->
*(
Usually
*
File
,
*
World
)
openBinaryFile
::
!
FilePath
!
IOMode
!*
World
->
*(
Usually
*
File
,
*
World
)
closeFile
::
!*
File
!*
World
->
*(
Usually
(),
*
World
)
/// ## Standard Input and Output
stdio
::
*
File
stdin
::
*
File
stdout
::
*
File
stderr
::
*
File
/// ## Reading and Writing
readFile
::
!
Path
!*
World
->
*(
Usually
String
,
*
World
)
writeFile
::
!
Path
!
String
!*
World
->
*(
Usually
(),
*
World
)
appendFile
::
!
Path
!
String
!*
World
->
*(
Usually
(),
*
World
)
readFile
::
!
FilePath
!*
World
->
*(
Usually
String
,
*
World
)
writeFile
::
!
FilePath
!
String
!*
World
->
*(
Usually
(),
*
World
)
appendFile
::
!
FilePath
!
String
!*
World
->
*(
Usually
(),
*
World
)
src/System/File.icl
View file @
df67f0c9
implementation
module
System
.
File
implementation
module
System
.
IO
import
Data
.
Error
import
Data
.
Either
import
Data
.
File
import
Data
.
Function
/// # Opening and Closing
BINARY_MODE_OFFSET
:==
3
withFile
::
!
FilePath
!
IOMode
(!*
File
->
*(
Usually
a
,
*
World
))
!*
World
->
*(
Usually
a
,
!*
World
)
withFile
name
mode
operation
world
#
(
opened
,
world
)
=
openFile
name
mode
world
|
isLeft
opened
=
(
opened
,
world
)
#
(
edited
,
world
)
=
operation
file
|
isLeft
edited
=
(
edited
,
world
)
#
(
closed
,
world
)
=
closeFile
name
world
|
isLeft
closed
=
(
closed
,
world
)
=
(
mapRight
id
edited
,
world
)
openFile
::
!
FilePath
!
IOMode
!*
World
->
*(
Usually
*
File
,
*
World
)
openFile
name
mode
world
#
(
ok
,
file
)
=
prim_openFile
name
mode
|
not
ok
=
(
Left
FileDoesNotExist
,
world
)
=
(
Right
file
,
world
)
openBinaryFile
::
!
FilePath
!
IOMode
!*
World
->
*(
Usually
*
File
,
*
World
)
openBinaryFile
name
mode
world
=
openFile
name
(
mode
+
BINARY_MODE_OFFSET
)
world
closeFile
::
!*
File
!*
World
->
*(
Usually
(),
*
World
)
closeFile
file
word
#
ok
=
prim_closeFile
file
|
not
ok
=
(
Left
FileIsFull
,
world
)
=
(
Right
(),
world
)
/// ## Standard Input and Output
//FIXME inline these here?
stdin
::
File
stdin
=
undefined
stdin
::
*
File
stdin
=
prim_stdio
stdout
::
File
stdout
=
undefined
stdout
::
*
File
stdout
=
prim_stderr
stderr
::
File
stderr
=
undefined
stderr
::
*
File
stderr
=
prim_stderr
/// ## Reading and Writing
readFile
::
!
Path
!*
World
->
*(
Usually
String
,
*
World
)
readFile
p
w
=
undefined
writeFile
::
!
Path
!
String
!*
World
->
*(
Usually
(),
*
World
)
writeFile
p
s
w
=
undefined
readFile
::
!
FilePath
!*
World
->
*(
Usually
String
,
*
World
)
readFile
name
world
=
withFile
name
ReadMode
readAllLines
world