|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
-- This file:
-- http://anggtwu.net/LEAN/feline1.lean.html
-- http://anggtwu.net/LEAN/feline1.lean
-- (find-angg "LEAN/feline1.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LEAN/feline1.lean"))
-- (find-fplean4page 72 "the result is pure ()")
-- (find-fplean4text 72 "the result is pure ()")
-- (find-fplean4page 79 "Worked Example: cat")
-- (find-fplean4text 79 "Worked Example: cat")
-- import Init.System.FilePath
-- open System.FilePath
-- open System
-- (find-lean4prefile "Init/System/FilePath.lean" "namespace FilePath\n")
-- (find-lean4prefile "Init/System/FilePath.lean" "def mkFilePath")
-- (find-lean4pregrep "grep --color=auto -nRH --null -e 'mkFilePath' *")
-- System.mkFilePath
#check System.mkFilePath
#check System.mkFilePath ["/tmp/o"]
#eval System.mkFilePath ["/tmp/o"]
#check IO.FS.readFile
#check IO.FS.readFile (System.mkFilePath ["/tmp/o"])
#eval IO.FS.readFile (System.mkFilePath ["/tmp/o"])
#check IO.FS.writeFile
def mkfilepath (fname : String) : System.FilePath :=
System.mkFilePath [fname]
def readfile (fname : String) : IO String :=
IO.FS.readFile (mkfilepath fname)
def writefile (fname content : String) : IO Unit :=
IO.FS.writeFile (mkfilepath fname) content
#check mkfilepath "/tmp/o"
#eval mkfilepath "/tmp/o"
#check readfile "/tmp/o"
#eval readfile "/tmp/o"
#check writefile "/tmp/o2" "bar\n"
#eval writefile "/tmp/o2" "bar\n"
-- (find-angg "LEAN/ioprocess1.lean")
-- import IO.Process
def main : IO Unit :=
writefile "/tmp/o2" "bar\n"
#check pure
#check pure ()
#check ()
#check IO
#check IO.FS.Stream
/-
structure Stream where
flush : IO Unit
read : USize → IO ByteArray
write : ByteArray → IO Unit
getLine : IO String
putStr : String → IO Unit
-/
/-
The Lean compiler contains IO actions (such as IO.getStdout , which is called in dump ) to
get streams that represent standard input, standard output, and standard error. These are
IO actions rather than ordinary definitions because Lean allows these standard POSIX
streams to be replaced in a process, which makes it easier to do things like capturing the
output from a program into a string by writing a custom IO.FS.Stream .
The control flow in dump is essentially a while loop. When dump is called, if the stream has
reached the end of the file, pure () terminates the function by returning the constructor
for Unit . If the stream has not yet reached the end of the file, one block is read, and its
contents are written to stdout , after which dump calls itself directly. The recursive calls
continue until stream.read returns an empty byte array, which indicates that the end of the
file has been reached.
When an if expression occurs as a statement in a do , as in dump , each branch of the if
is implicitly provided with a do . In other words, the sequence of steps following the else
are treated as a sequence of IO actions to be executed, just as if they had a do at the
beginning. Names introduced with let in the branches of the if are visible only in their
own branches, and are not in scope outside of the if .
There is no danger of running out of stack space while calling dump because the recursive
call happens as the very last step in the function, and its result is returned directly rather
than being manipulated or computed with. This kind of recursion is called tail recursion, and
it is described in more detail later in this book. Because the compiled code does not need to
retain any state, the Lean compiler can compile the recursive call to a jump.
If feline only redirected standard input to standard output, then dump would be
sufficient. However, it also needs to be able to open files that are provided as command-line
arguments and emit their contents. When its argument is the name of a file that exists,
fileStream returns a stream that reads the file's contents. When the argument is not a file,
fileStream emits an error and returns none .
-/
#check IO.FS.readFile
#check IO.FS.writeFile
-- import IO.System.FilePath
-- import IO.FilePath
-- (find-lean4prefile "Init/System/FilePath.lean")
def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
let fileExists ← filename.pathExists
if not fileExists then
let stderr ← IO.getStderr
stderr.putStrLn s!"File not found: {filename}"
pure none
else
let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
pure (some (IO.FS.Stream.ofHandle handle))
/-
Opening a file as a stream takes two steps. First, a file handle is created by opening the file
in read mode. A Lean file handle tracks an underlying file descriptor. When there are no
references to the file handle value, a finalizer closes the file descriptor. Second, the file
handle is given the same interface as a POSIX stream using IO.FS.Stream.ofHandle , which
fills each field of the Stream structure with the corresponding IO action that works on file
handles.
Handling Input
The main loop of feline is another tail-recursive function, called process . In order to
return a non-zero exit code if any of the inputs could not be read, process takes an
argument exitCode that represents the current exit code for the whole program.
Additionally, it takes a list of input files to be processed.
-/
def process (exitCode : UInt32) (args : List String) : IO UInt32 := do
match args with
| [] => pure exitCode
| "-" :: args =>
let stdin ← IO.getStdin
dump stdin
process exitCode args
| filename :: args =>
let stream ← fileStream ⟨filename⟩
match stream with
| none =>
process 1 args
| some stream =>
dump stream
process exitCode args
/-
Just as with if , each branch of a match that is used as a statement in a do is implicitly
provided with its own do .
There are three possibilities. One is that no more files remain to be processed, in which case
process returns the error code unchanged. Another is that the specified filename is "-" ,
in which case process dumps the contents of the standard input and then processes the
remaining filenames. The final possibility is that an actual filename was specified. In this
case, fileStream is used to attempt to open the file as a POSIX stream. Its argument is
encased in ⟨ ... ⟩ because a FilePath is a single-field structure that contains a string. If
the file could not be opened, it is skipped, and the recursive call to process sets the exit
code to 1 . If it could, then it is dumped, and the recursive call to process leaves the exit
code unchanged.
process does not need to be marked partial because it is structurally recursive. Each
recursive call is provided with the tail of the input list, and all Lean lists are finite. Thus,
process does not introduce any non-termination.
Main
The final step is to write the main action. Unlike prior examples, main in feline is a
function. In Lean, main can have one of three types:
main : IO Unit corresponds to programs that cannot read their command-line
arguments and always indicate success with an exit code of 0 ,
main : IO UInt32 corresponds to int main(void) in C, for programs without
arguments that return exit codes, and
main : List String → IO UInt32 corresponds to int main(int argc, char
**argv) in C, for programs that take arguments and signal success or failure.
If no arguments were provided, feline should read from standard input as if it were called
with a single "-" argument. Otherwise, the arguments should be processed one after the
other.
-/
def main (args : List String) : IO UInt32 :=
match args with
| [] => process 0 ["-"]
| _ => process 0 args
/-
Meow!
To check whether feline works, the first step is to build it with lake build . First off, when
called without arguments, it should emit what it receives from standard input. Check that
echo "It works!" | ./build/bin/feline
emits It works! .
Secondly, when called with files as arguments, it should print them. If the file test1.txt
contains
It's time to find a warm spot
https://leanprover.github.io/functional_programming_in_lean/print.html 83/432
02/06/2023, 22:33 Functional Programming in Lean
and test2.txt contains
and curl up!
then the command
./build/bin/feline test1.txt test2.txt
should emit
It's time to find a warm spot
and curl up!
Finally, the - argument should be handled appropriately.
echo "and purr" | ./build/bin/feline test1.txt - test2.txt
should yield
It's time to find a warm spot
and purr
and curl up!
Exercise
Extend feline with support for usage information. The extended version should accept a
command-line argument --help that causes documentation about the available command-
line options to be written to standard output.
Additional Conveniences
Nested Actions
Many of the functions in feline exhibit a repetitive pattern in which an IO action's result
is given a name, and then used immediately and only once. For instance, in dump :
-/
partial def dump (stream : IO.FS.Stream) : IO Unit := do
let buf ← stream.read bufsize
if buf.isEmpty then
pure ()
else
let stdout ← IO.getStdout
stdout.write buf
dump stream
/-
the pattern occurs for stdout :
-/
let stdout ← IO.getStdout
stdout.write buf
/-
Similarly, fileStream contains the following snippet:
-/
let fileExists ← filename.pathExists
if not fileExists then
/-
When Lean is compiling a do block, expressions that consist of a left arrow immediately
under parentheses are lifted to the nearest enclosing do , and their results are bound to a
unique name. This unique name replaces the origin of the expression. This means that
dump can also be written as follows:
-/
partial def dump (stream : IO.FS.Stream) : IO Unit := do
let buf ← stream.read bufsize
if buf.isEmpty then
pure ()
else
(← IO.getStdout).write buf
dump stream
/-
This version of dump avoids introducing names that are used only once, which can greatly
simplify a program. IO actions that Lean lifts from a nested expression context are called
nested actions.
fileStream can be simplified using the same technique:
-/
def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
if not (← filename.pathExists) then
(← IO.getStderr).putStrLn s!"File not found: {filename}"
pure none
else
let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
pure (some (IO.FS.Stream.ofHandle handle))
/-
In this case, the local name of handle could also have been eliminated using nested
actions, but the resulting expression would have been long and complicated. Even though
it's often good style to use nested actions, it can still sometimes be helpful to name
intermediate results.
It is important to remember, however, that nested actions are only a shorter notation for
IO actions that occur in a surrounding do block. The side effects that are involved in
executing them still occur in the same order, and execution of side effects is not
interspersed with the evaluation of expressions. For an example of where this might be
confusing, consider the following helper definitions that return data after announcing to the
world that they have been executed:
-/
def getNumA : IO Nat := do
(← IO.getStdout).putStrLn "A"
pure 5
def getNumB : IO Nat := do
(← IO.getStdout).putStrLn "B"
pure 7
/-
These definitions are intended to stand in for more complicated IO code that might
validate user input, read a database, or open a file.
A program that prints 0 when number A is five, or number B otherwise, can be written as
follows:
-/
def test : IO Unit := do
let a : Nat := if (← getNumA) == 5 then 0 else (← getNumB)
(← IO.getStdout).putStrLn s!"The answer is {a}"
/-
However, this program probably has more side effects (such as prompting for user input or
reading a database) than was intended. The definition of getNumA makes it clear that it will
always return 5 , and thus the program should not read number B. However, running the
program results in the following output:
A
B
The answer is 0
getNumB was executed because test is equivalent to this definition:
-/
def test : IO Unit := do
let x ← getNumA
let y ← getNumB
let a : Nat := if x == 5 then 0 else y
(← IO.getStdout).putStrLn s!"The answer is {a}"
/-
This is due to the rule that nested actions are lifted to the closest enclosing do block. The
branches of the if were not implicitly wrapped in do blocks because the if is not itself a
statement in the do block—the statement is the let that defines a . Indeed, they could
not be wrapped this way, because the type of the conditional expression is Nat , not IO
Nat .
Flexible Layouts for do
In Lean, do expressions are whitespace-sensitive. Each IO action or local binding in the do
is expected to start on its own line, and they should all have the same indentation. Almost
all uses of do should be written this way. In some rare contexts, however, manual control
over whitespace and indentation may be necessary, or it may be convenient to have
multiple small actions on a single line. In these cases, newlines can be replaced with a
semicolon and indentation can be replaced with curly braces.
For instance, all of the following programs are equivalent:
-- This version uses only whitespace-sensitive layout
def main : IO Unit := do
let stdin ← IO.getStdin
let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let name := (← stdin.getLine).trim
stdout.putStrLn s!"Hello, {name}!"
-- This version is as explicit as possible
def main : IO Unit := do {
let stdin ← IO.getStdin;
let stdout ← IO.getStdout;
stdout.putStrLn "How would you like to be addressed?";
let name := (← stdin.getLine).trim;
stdout.putStrLn s!"Hello, {name}!"
}
-- This version uses a semicolon to put two actions on the same line
def main : IO Unit := do
let stdin ← IO.getStdin; let stdout ← IO.getStdout
stdout.putStrLn "How would you like to be addressed?"
let name := (← stdin.getLine).trim
stdout.putStrLn s!"Hello, {name}!"
Idiomatic Lean code uses curly braces with do very rarely.
Running IO Actions With #eval
Lean's #eval command can be used to execute IO actions, rather than just evaluating
them. Normally, adding a #eval command to a Lean file causes Lean to evaluate the
provided expression, convert the resulting value to a string, and provide that string as a
tooltip and in the info window. Rather than failing because IO actions can't be converted to
strings, #eval executes them, carrying out their side effects. If the result of execution is the
Unit value () , then no result string is shown, but if it is a type that can be converted to a
string, then Lean displays the resulting value.
This means that, given the prior definitions of countdown and runActions ,
#eval runActions (countdown 3)
displays
3
2
1
Blast off!
https://leanprover.github.io/functional_programming_in_lean/print.html 88/432
02/06/2023, 22:33 Functional Programming in Lean
This is the output produced by running the IO action, rather than some opaque
representation of the action itself. In other words, for IO actions, #eval both evaluates the
provided expression and executes the resulting action value.
Quickly testing IO actions with #eval can be much more convenient that compiling and
running whole programs. However, there are some limitations. For instance, reading from
standard input simply returns empty input. Additionally, the IO action is re-executed
whenever Lean needs to update the diagnostic information that it provides to users, and
this can happen at unpredictable times. An action that reads and writes files, for instance,
may do so at inconvenient times.
https://leanprover.github.io/functional_programming_in_lean/print.html 89/432
02/06/2023, 22:33 Functional Programming in Lean
Summary
Evaluation vs Execution
Side effects are aspects of program execution that go beyond the evaluation of
mathematical expressions, such as reading files, throwing exceptions, or triggering
industrial machinery. While most languages allow side effects to occur during evaluation,
Lean does not. Instead, Lean has a type called IO that represents descriptions of programs
that use side effects. These descriptions are then executed by the language's run-time
system, which invokes the Lean expression evaluator to carry out specific computations.
Values of type IO α are called IO actions. The simplest is pure , which returns its argument
and has no actual side effects.
IO actions can also be understood as functions that take the whole world as an argument
and return a new world in which the side effect has occurred. Behind the scenes, the IO
library ensures that the world is never duplicated, created, or destroyed. While this model of
side effects cannot actually be implemented, as the whole universe is too big to fit in
memory, the real world can be represented by a token that is passed around through the
program.
An IO action main is executed when the program starts. main can have one of three
types:
main : IO Unit is used for simple programs that cannot read their command-line
arguments and always return exit code 0 ,
main : IO UInt32 is used for programs without arguments that may signal success or
failure, and
main : List String → IO UInt32 is used for programs that take command-line
arguments and signal success or failure.
-/
/-
| (find-elan4leanfile "Lean/")
| (find-lean4file "doc/")
| (find-lean4file "doc/tour.md")
| (find-angg ".emacs.papers" "fplean4")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "/tmp/feline/")
rm -Rv /tmp/feline/
mkdir /tmp/feline/
cd /tmp/feline/
lake new feline
laf
find
lean --run feline1.lean
-/
-- Local Variables:
-- coding: utf-8-unix
-- End: