max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: file IO using handles

Browse source
This commit is contained in:
Simon Hudon 2019-12-17 04:05:01 -08:00 • committed by Leonardo de Moura
parent 354678a5e4
commit 92c8773137
28 changed files with 814 additions and 122 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Init/Data/Char/Basic.lean
View file

@ -5,6 +5,7 @@ Author: Leonardo de Moura
-/
prelude
import Init.Data.UInt
@[inline, reducible] def isValidChar (n : UInt32) : Prop :=
n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
@ -19,14 +20,10 @@ instance : HasSizeof Char :=
namespace Char
def utf8Size (c : Char) : UInt32 :=
let v := c.val;
if UInt32.land v 0x80 = 0 then 1
else if UInt32.land v 0xE0 = 0xC0 then 2
else if UInt32.land v 0xF0 = 0xE0 then 3
else if UInt32.land v 0xF8 = 0xF0 then 4
else if UInt32.land v 0xFC = 0xF8 then 5
else if UInt32.land v 0xFE = 0xFC then 6
else if v = 0xFF then 1
else 0
if v < 0x7F then 1
else if v < 0x7FF then 2
else if v < 0xFFFF then 3
else 4
protected def Less (a b : Char) : Prop := a.val < b.val
protected def LessEq (a b : Char) : Prop := a.val ≤ b.val

5
src/Init/Data/UInt.lean
View file

@ -186,6 +186,11 @@ def UInt32.decLe (a b : UInt32) : Decidable (a ≤ b) :=
UInt32.casesOn a $ fun n => UInt32.casesOn b $ fun m =>
inferInstanceAs (Decidable (n <= m))
@[extern c inline "#1 << #2"]
constant UInt32.shiftLeft (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
@[extern c inline "#1 >> #2"]
constant UInt32.shiftRight (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
instance : DecidableEq UInt32 := UInt32.decEq
instance UInt32.hasDecidableLt (a b : UInt32) : Decidable (a < b) := UInt32.decLt a b
instance UInt32.hasDecidableLe (a b : UInt32) : Decidable (a ≤ b) := UInt32.decLe a b

2
src/Init/Lean/Data/Options.lean
View file

@ -64,7 +64,7 @@ pure decl.descr
def setOptionFromString (opts : Options) (entry : String) : IO Options := do
let ps := (entry.splitOn "=").map String.trim;
[key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'";
[key, val] ← pure ps | throw $ IO.userError "invalid configuration option entry, it must be of the form '<key> = <value>'";
defValue ← getOptionDefaulValue key.toName;
match defValue with
| DataValue.ofString v => pure $ opts.setString key val

2
src/Init/Lean/Elab/Command.lean
View file

@ -168,7 +168,7 @@ registerBuiltinAttribute {
unless persistent $ throw (IO.userError ("invalid attribute 'builtinCommandElab', must be persistent"));
kind ← IO.ofExcept $ syntaxNodeKindOfAttrParam env `Lean.Parser.Command arg;
match env.find? declName with
| none => throw "unknown declaration"
| none => throw $ IO.userError "unknown declaration"
| some decl =>
match decl.type with
| Expr.const `Lean.Elab.Command.CommandElab _ _ => declareBuiltinCommandElab env kind declName

2
src/Init/Lean/Elab/Term.lean
View file

@ -203,7 +203,7 @@ registerBuiltinAttribute {
unless persistent $ throw (IO.userError ("invalid attribute 'builtinTermElab', must be persistent"));
kind ← IO.ofExcept $ syntaxNodeKindOfAttrParam env `Lean.Parser.Term arg;
match env.find? declName with
| none => throw "unknown declaration"
| none => throw $ IO.userError "unknown declaration"
| some decl =>
match decl.type with
| Expr.const `Lean.Elab.Term.TermElab _ _ => declareBuiltinTermElab env kind declName

2
src/Init/Lean/Parser/Parser.lean
View file

@ -1639,7 +1639,7 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
when args.hasArgs $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument"));
unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', must be persistent"));
match env.find? declName with
| none => throw "unknown declaration"
| none => throw $ IO.userError "unknown declaration"
| some decl =>
match decl.type with
| Expr.const `Lean.Parser.TrailingParser _ _ =>

142
src/Init/System/IO.lean
View file

@ -6,6 +6,8 @@ Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich
prelude
import Init.Control.EState
import Init.Data.String.Basic
import Init.Data.ByteArray
import Init.System.IOError
import Init.System.FilePath
/-- Like https://hackage.haskell.org/package/ghc-Prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld.
@ -37,22 +39,6 @@ instance (α ε : Type) : HasOrelse (EIO ε α) := ⟨MonadExcept.orelse⟩
instance {ε : Type} {α : Type} [Inhabited ε] : Inhabited (EIO ε α) :=
inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α))
/-
In the future, we may want to give more concrete data
like in https://doc.rust-lang.org/std/IO/enum.ErrorKind.html
-/
def IO.Error := String
instance : HasToString IO.Error := inferInstanceAs (HasToString String)
instance : Inhabited IO.Error := inferInstanceAs (Inhabited String)
def IO.userError (s : String) : IO.Error :=
s
@[export lean_io_error_to_string]
def IO.Error.toString : IO.Error → String :=
id
abbrev IO : Type → Type := EIO IO.Error
section
@ -96,18 +82,29 @@ pure (fn ())
inductive FS.Mode
| read | write | readWrite | append
constant FS.handle : Type := Unit
constant FS.Handle : Type := Unit
namespace Prim
open FS
@[specialize] partial def iterate {α β : Type} : α → (α → IO (Sum α β)) → IO β
| a, f =>
do v ← f a;
| a, f => do
v ← f a;
match v with
| Sum.inl a => iterate a f
| Sum.inr b => pure b
-- @[export lean_fopen_flags]
def fopenFlags (m : FS.Mode) (b : Bool) : String :=
let mode :=
match m with
| FS.Mode.read => "r"
| FS.Mode.write => "w"
| FS.Mode.readWrite => "r+"
| FS.Mode.append => "a" ;
let bin := if b then "b" else "t";
mode ++ bin
@[extern "lean_io_prim_put_str"]
constant putStr (s: @& String) : IO Unit := arbitrary _
@[extern "lean_io_prim_read_text_file"]
@ -115,18 +112,26 @@ constant readTextFile (s : @& String) : IO String := arbitrary _
@[extern "lean_io_prim_get_line"]
constant getLine : IO String := arbitrary _
@[extern "lean_io_prim_handle_mk"]
constant handle.mk (s : @& String) (m : Mode) (bin : Bool := false) : IO handle := arbitrary _
constant Handle.mk (s : @& String) (mode : @& String) : IO Handle := arbitrary _
@[extern "lean_io_prim_handle_is_eof"]
constant handle.isEof (h : @& handle) : IO Bool := arbitrary _
constant Handle.isEof (h : @& Handle) : IO Bool := arbitrary _
@[extern "lean_io_prim_handle_flush"]
constant handle.flush (h : @& handle) : IO Unit := arbitrary _
@[extern "lean_io_prim_handle_close"]
constant handle.close (h : @& handle) : IO Unit := arbitrary _
constant Handle.flush (h : @& Handle) : IO Unit := arbitrary _
-- TODO: replace `String` with byte buffer
-- constant handle.read : handle → Nat → EIO String
-- constant handle.write : handle → String → EIO Unit
@[extern "lean_io_prim_handle_read"]
constant Handle.read (h : @& Handle) (bytes : USize) : IO ByteArray := arbitrary _
@[extern "lean_io_prim_handle_write"]
constant Handle.write (h : @& Handle) (buffer : @& ByteArray) : IO Unit := arbitrary _
@[extern "lean_io_prim_handle_read_byte"]
constant Handle.getByte (h : @& Handle) : IO UInt8 := arbitrary _
@[extern "lean_io_prim_handle_write_byte"]
constant Handle.putByte (h : @& Handle) (c : UInt8) : IO Unit := arbitrary _
@[extern "lean_io_prim_handle_get_line"]
constant handle.getLine (h : @& handle) : IO String := arbitrary _
constant Handle.getLine (h : @& Handle) : IO String := arbitrary _
@[extern "lean_io_prim_handle_put_str"]
constant Handle.putStr (h : @& Handle) (s : @& String) : IO Unit := arbitrary _
@[extern "lean_io_getenv"]
constant getEnv (var : @& String) : IO (Option String) := arbitrary _
@ -167,31 +172,33 @@ end
namespace FS
variables {m : Type → Type} [Monad m] [MonadIO m]
def handle.mk (s : String) (Mode : Mode) (bin : Bool := false) : m handle := Prim.liftIO (Prim.handle.mk s Mode bin)
def handle.isEof : handle → m Bool := Prim.liftIO ∘ Prim.handle.isEof
def handle.flush : handle → m Unit := Prim.liftIO ∘ Prim.handle.flush
def handle.close : handle → m Unit := Prim.liftIO ∘ Prim.handle.flush
-- def handle.read (h : handle) (bytes : Nat) : m String := Prim.liftEIO (Prim.handle.read h bytes)
-- def handle.write (h : handle) (s : String) : m Unit := Prim.liftEIO (Prim.handle.write h s)
def handle.getLine : handle → m String := Prim.liftIO ∘ Prim.handle.getLine
def Handle.mk (s : String) (Mode : Mode) (bin : Bool := false) : m Handle :=
Prim.liftIO (Prim.Handle.mk s (Prim.fopenFlags Mode bin))
/-
def getChar (h : handle) : m Char := do
b ← h.read 1,
if b.isEmpty then fail "getChar failed"
else pure b.mkIterator.curr
@[inline]
def withFile {α} (fn : String) (m : Mode) (f : Handle → IO α) : IO α :=
Handle.mk fn m >>= f
/-- returns whether the end of the file has been reached while reading a file.
`h.isEof` returns true /after/ the first attempt at reading past the end of `h`.
Once `h.isEof` is true, the reading `h` raises `IO.Error.eof`.
-/
def Handle.isEof : Handle → m Bool := Prim.liftIO ∘ Prim.Handle.isEof
def Handle.flush : Handle → m Unit := Prim.liftIO ∘ Prim.Handle.flush
def Handle.read (h : Handle) (bytes : Nat) : m ByteArray := Prim.liftIO (Prim.Handle.read h (USize.ofNat bytes))
def Handle.write (h : Handle) (s : ByteArray) : m Unit := Prim.liftIO (Prim.Handle.write h s)
def Handle.getByte (h : Handle) : m UInt8 := Prim.liftIO (Prim.Handle.getByte h)
def Handle.putByte (h : Handle) (b : UInt8) : m Unit := Prim.liftIO (Prim.Handle.putByte h b)
-- def handle.putChar (h : handle) (c : Char) : m Unit :=
-- h.write (toString c)
def Handle.getLine : Handle → m String := Prim.liftIO ∘ Prim.Handle.getLine
-- def handle.putStr (h : handle) (s : String) : m Unit :=
-- h.write s
def Handle.putStr (h : Handle) (s : String) : m Unit :=
Prim.liftIO $ Prim.Handle.putStr h s
-- def handle.putStrLn (h : handle) (s : String) : m Unit :=
-- h.putStr s *> h.putStr "\n"
def Handle.putStrLn (h : Handle) (s : String) : m Unit :=
h.putStr s *> h.putStr "\n"
def handle.readToEnd (h : handle) : m String :=
def Handle.readToEnd (h : Handle) : m String :=
Prim.liftIO $ Prim.iterate "" $ fun r => do
done ← h.isEof;
if done
@ -202,29 +209,28 @@ Prim.liftIO $ Prim.iterate "" $ fun r => do
pure $ Sum.inl (r ++ c) -- continue
def readFile (fname : String) (bin := false) : m String := do
h ← handle.mk fname Mode.read bin;
h ← Handle.mk fname Mode.read bin;
r ← h.readToEnd;
h.close;
pure r
end FS
-- constant stdin : IO FS.handle
-- constant stderr : IO FS.handle
-- constant stdout : IO FS.handle
-- constant stdin : IO FS.Handle
-- constant stderr : IO FS.Handle
-- constant stdout : IO FS.Handle
/-
namespace Proc
def child : Type :=
MonadIOProcess.child ioCore
def child.stdin : child → handle :=
def child.stdin : child → Handle :=
MonadIOProcess.stdin
def child.stdout : child → handle :=
def child.stdout : child → Handle :=
MonadIOProcess.stdout
def child.stderr : child → handle :=
def child.stderr : child → Handle :=
MonadIOProcess.stderr
def spawn (p : IO.process.spawnArgs) : IO child :=
@ -236,6 +242,34 @@ MonadIOProcess.wait c
end Proc
-/
structure AccessRight :=
(read write execution : Bool := false)
def AccessRight.flags (acc : AccessRight) : UInt32 :=
let r : UInt32 := if acc.read then 0x4 else 0;
let w : UInt32 := if acc.write then 0x2 else 0;
let x : UInt32 := if acc.execution then 0x1 else 0;
r.lor $ w.lor x
structure FileRight :=
(user group other : AccessRight := { })
def FileRight.flags (acc : FileRight) : UInt32 :=
let u : UInt32 := acc.user.flags.shiftLeft 6;
let g : UInt32 := acc.group.flags.shiftLeft 3;
let o : UInt32 := acc.other.flags;
u.lor $ g.lor o
namespace Access
@[extern "lean_chmod"]
constant Prim.setAccessRights (filename : @& String) (mode : UInt32) : IO Unit :=
arbitrary _
def setAccessRights (filename : String) (mode : FileRight) : IO Unit :=
Prim.setAccessRights filename mode.flags
end Access
/- References -/
constant RefPointed (α : Type) : PointedType := arbitrary _

193
src/Init/System/IOError.lean Normal file
View file

@ -0,0 +1,193 @@
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon
-/
prelude
import Init.Core
import Init.Data.UInt
import Init.Data.ToString
import Init.Data.String.Basic
/-
Immitate the structure of IOErrorType in Haskell:
https://hackage.haskell.org/package/base-4.12.0.0/docs/System-IO-Error.html#t:IOErrorType
-/
inductive IO.Error
| alreadyExists (details : String) -- EEXIST, EINPROGRESS, EISCONN
| otherError (details : String) -- EFAULT, default
| resourceBusy (details : String)
-- EADDRINUSE, EBUSY, EDEADLK, ETXTBSY
| resourceVanished (details : String)
-- ECONNRESET, EIDRM, ENETDOWN, ENETRESET,
-- ENOLINK, EPIPE
| unsupportedOperation (details : String)
-- EADDRNOTAVAIL, EAFNOSUPPORT, ENODEV, ENOPROTOOPT
-- ENOSYS, EOPNOTSUPP, ERANGE, ESPIPE, EXDEV
| hardwareFault (details : String) -- EIO
| unsatisfiedConstraints (details : String) -- ENOTEMPTY
| illegalOperation (details : String) -- ENOTTY
| protocolError (details : String)
-- EPROTO, EPROTONOSUPPORT, EPROTOTYPE
| timeExpired (details : String)
-- ETIME, ETIMEDOUT
| interrupted (filename : String) (details : String) -- EINTR
| noFileOrDirectory (filename : String) (details : String) -- ENOENT
| invalidArgument (filename : Option String) (details : String)
-- ELOOP, ENAMETOOLONG, EDESTADDRREQ, EILSEQ, EINVAL, EDOM, EBADF
-- ENOEXEC, ENOSTR, ENOTCONN, ENOTSOCK
| permissionDenied (filename : Option String) (details : String)
-- EACCES, EROFS, ECONNABORTED, EFBIG, EPERM
| resourceExhausted (filename : Option String) (details : String)
-- EMFILE, ENFILE, ENOSPC, E2BIG, EAGAIN, EMLINK:
-- EMSGSIZE, ENOBUFS, ENOLCK, ENOMEM, ENOSR:
| inappropriateType (filename : Option String) (details : String)
-- EISDIR, EBADMSG, ENOTDIR:
| noSuchThing (filename : Option String) (details : String)
-- ENXIO, EHOSTUNREACH, ENETUNREACH, ECHILD, ECONNREFUSED,
-- ENODATA, ENOMSG, ESRCH
-- overflow -- EOVERFLOW
| unexpectedEof
| userError (msg : String)
@[export mk_io_user_error]
def IO.userError (s : String) : IO.Error :=
IO.Error.userError s
namespace IO.Error
@[export lean_mk_io_error_eof]
def mkEofError : IO.Error := unexpectedEof
@[export lean_mk_io_error_inappropriate_type_file]
def mkInappropriateTypeFile : String → String → IO.Error :=
inappropriateType ∘ some
@[export lean_mk_io_error_interrupted]
def mkInterrupted : String → String → IO.Error :=
interrupted
@[export lean_mk_io_error_invalid_argument_file]
def mkInvalidArgumentFile : String → String → IO.Error :=
invalidArgument ∘ some
@[export lean_mk_io_error_no_file_or_directory]
def mkNoFileOrDirectory : String → String → IO.Error :=
noFileOrDirectory
@[export lean_mk_io_error_no_such_thing_file]
def mkNoSuchThingFile : String → String → IO.Error :=
noSuchThing ∘ some
@[export lean_mk_io_error_permission_denied_file]
def mkPermissionDeniedFile : String → String → IO.Error :=
permissionDenied ∘ some
@[export lean_mk_io_error_resource_exhausted_file]
def mkResourceExhaustedFile : String → String → IO.Error :=
resourceExhausted ∘ some
@[export lean_mk_io_error_unsupported_operation]
def mkUnsupportedOperation : String → IO.Error :=
unsupportedOperation
@[export lean_mk_io_error_resource_exhausted]
def mkResourceExhausted : String → IO.Error :=
resourceExhausted none
@[export lean_mk_io_error_already_exists]
def mkAlreadyExists : String → IO.Error :=
alreadyExists
@[export lean_mk_io_error_inappropriate_type]
def mkInappropriateType : String → IO.Error :=
inappropriateType none
@[export lean_mk_io_error_no_such_thing]
def mkNoSuchThing : String → IO.Error :=
noSuchThing none
@[export lean_mk_io_error_resource_vanished]
def mkResourceVanished : String → IO.Error :=
resourceVanished
@[export lean_mk_io_error_resource_busy]
def mkResourceBusy : String → IO.Error :=
resourceBusy
@[export lean_mk_io_error_invalid_argument]
def mkInvalidArgument : String → IO.Error :=
invalidArgument none
@[export lean_mk_io_error_other_error]
def mkOtherError : String → IO.Error :=
otherError
@[export lean_mk_io_error_permission_denied]
def mkPermissionDenied : String → IO.Error :=
permissionDenied none
@[export lean_mk_io_error_hardware_fault]
def mkHardwareFault : String → IO.Error :=
hardwareFault
@[export lean_mk_io_error_unsatisfied_constraints]
def mkUnsatisfiedConstraints : String → IO.Error :=
unsatisfiedConstraints
@[export lean_mk_io_error_illegal_operation]
def mkIllegalOperation : String → IO.Error :=
illegalOperation
@[export lean_mk_io_error_protocol_error]
def mkProtocolError : String → IO.Error :=
protocolError
@[export lean_mk_io_error_time_expired]
def mkTimeExpired : String → IO.Error :=
timeExpired
private def downCaseFirst (s : String) : String := s.set 0 (s.get 0).toLower
def fopenErrorToString (gist fn : String) : Option String → String
| some details => gist ++ ": " ++ downCaseFirst details ++ "\n file: " ++ fn
| none => gist ++ "\n file: " ++ fn
def otherErrorToString (gist : String) : Option String → String
| some details => gist ++ ": " ++ downCaseFirst details
| none => gist
@[export lean_io_error_to_string]
def toString : IO.Error → String
| unexpectedEof => "End of file"
| inappropriateType (some fn) details => fopenErrorToString "Inappropriate type" fn details
| inappropriateType none details => otherErrorToString "Inappropriate type" details
| interrupted fn details => fopenErrorToString "Interrupted system call" fn details
| invalidArgument (some fn) details => fopenErrorToString "Invalid argument" fn details
| invalidArgument none details => otherErrorToString "Invalid argument" details
| noFileOrDirectory fn details => fopenErrorToString "No such file or directory" fn none
| noSuchThing (some fn) details => fopenErrorToString "No such thing" fn details
| noSuchThing none details => otherErrorToString "No such thing" details
| permissionDenied (some fn) details => fopenErrorToString details fn none
| permissionDenied none details => otherErrorToString details none
| resourceExhausted (some fn) details => fopenErrorToString "Resource exhausted" fn details
| resourceExhausted none details => otherErrorToString "Resource exhausted" details
| alreadyExists details => otherErrorToString "Already exists" details
| otherError details => details
| resourceBusy details => otherErrorToString "Resource busy" details
| resourceVanished details => otherErrorToString "Resource vanished" details
| hardwareFault _ => otherErrorToString "Hardware fault" none
| illegalOperation details => otherErrorToString "Illegal operation" details
| protocolError details => otherErrorToString "Protocol error" details
| timeExpired details => otherErrorToString "Time expired" details
| unsatisfiedConstraints details => otherErrorToString "Directory not empty" none
| unsupportedOperation details => otherErrorToString "Unsupported operation" details
| userError msg => msg
instance : HasToString IO.Error := ⟨ IO.Error.toString ⟩
instance : Inhabited IO.Error := ⟨ userError "" ⟩
end IO.Error

69
src/cmake/check_main.sh Normal file
View file

@ -0,0 +1,69 @@
#!/usr/bin/env bash
set -e
if [ $# -ne 3 -a $# -ne 2 ]; then
echo "Usage: test_single.sh [lean-executable-path] [file] [yes/no]?"
exit 1
fi
ulimit -s 8192
LEAN=$1
BIN_DIR=../../../bin
export LEAN_PATH=Init=../../../src/Init:Test=.
if [ $# -ne 3 ]; then
INTERACTIVE=no
else
INTERACTIVE=$3
fi
ff=$2
if [[ "$OSTYPE" == "msys" ]]; then
# Windows running MSYS2
# Replace /c/ with c:, and / with \\
ff=$(echo $ff | sed 's|^/\([a-z]\)/|\1:/|' | sed 's|/|\\\\|g')
fi
DIFF=diff
if diff --color --help >/dev/null 2>&1; then
DIFF="diff --color";
fi
$LEAN --cpp="$ff".cpp "$ff" || echo oh ho!
if [ $? -ne 0 ]; then
echo "Failed to compile $ff into C++ file"
exit 1
fi
$BIN_DIR/leanc -O3 -DNDEBUG -o "$ff.out" $ff.cpp
if [ $? -ne 0 ]; then
echo "Failed to compile C++ file $ff.cpp"
exit 1
fi
"./$ff.out" > "$ff.produced.out" 2>&1 || true
if test -f "$ff.expected.out"; then
if $DIFF -u --ignore-all-space -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then
echo "-- checked"
exit 0
else
echo "ERROR: file $ff.produced.out does not match $ff.expected.out"
if [ $INTERACTIVE == "yes" ]; then
meld "$ff.produced.out" "$ff.expected.out"
if diff -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then
echo "-- mismatch was fixed"
fi
fi
exit 1
fi
else
echo "ERROR: file $ff.expected.out does not exist"
if [ $INTERACTIVE == "yes" ]; then
read -p "copy $ff.produced.out (y/n)? "
if [ $REPLY == "y" ]; then
cp -- "$ff.produced.out" "$ff.expected.out"
echo "-- copied $ff.produced.out --> $ff.expected.out"
fi
fi
exit 1
fi

7
src/frontends/lean/builtin_cmds.cpp
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "runtime/sstream.h"
#include "runtime/compact.h"
#include "util/timeit.h"
#include "util/io.h"
#include "util/option_declarations.h"
#include "kernel/replace_fn.h"
#include "kernel/find_fn.h"
@ -403,8 +404,12 @@ static environment eval_cmd(parser & p) {
out.report();
if (io_result_is_error(r.raw())) {
message_builder msg = p.mk_message(p.cmd_pos(), p.pos(), ERROR);
msg << string_to_std(io_result_get_error(r.raw()));
object * err = io_result_get_error(r.raw());
inc_ref(err);
object * str = lean_io_error_to_string(err);
msg << string_to_std(str);
msg.report();
dec_ref(str);
}
return p.env();
}

308
src/runtime/io.cpp
View file

@ -21,6 +21,8 @@ Author: Leonardo de Moura
#include <cstdlib>
#include <cctype>
#include <sys/stat.h>
#include "util/io.h"
#include "runtime/utf8.h"
#include "runtime/object.h"
#include "runtime/thread.h"
#include "runtime/allocprof.h"
@ -32,8 +34,41 @@ Author: Leonardo de Moura
#endif
namespace lean {
extern "C" lean_object* lean_mk_io_error_permission_denied_file(lean_object*, lean_object*);
extern "C" lean_object* lean_mk_io_error_no_file_or_directory(lean_object*, lean_object*);
extern "C" lean_object* mk_io_user_error(lean_object*);
extern "C" lean_object* lean_string_append(lean_object*, lean_object*);
extern "C" lean_object* lean_mk_io_error_resource_exhausted_file(lean_object*, lean_object*);
extern "C" lean_object* lean_mk_io_error_interrupted(lean_object*, lean_object*);
extern "C" lean_object* lean_mk_io_error_invalid_argument_file(lean_object*, lean_object*);
extern "C" lean_object* lean_mk_io_error_no_such_thing_file(lean_object*, lean_object*);
extern "C" lean_object* lean_mk_io_error_inappropriate_type_file(lean_object*, lean_object*);
extern "C" lean_object* lean_mk_io_error_eof();
extern "C" lean_object* lean_mk_io_error_unsupported_operation(lean_object*);
extern "C" lean_object* lean_mk_io_error_resource_exhausted(lean_object*);
extern "C" lean_object* lean_mk_io_error_already_exists(lean_object*);
extern "C" lean_object* lean_mk_io_error_inappropriate_type(lean_object*);
extern "C" lean_object* lean_mk_io_error_no_such_thing(lean_object*);
extern "C" lean_object* lean_mk_io_error_resource_vanished(lean_object*);
extern "C" lean_object* lean_mk_io_error_resource_busy(lean_object*);
extern "C" lean_object* lean_mk_io_error_invalid_argument(lean_object*);
extern "C" lean_object* lean_mk_io_error_other_error(lean_object*);
extern "C" lean_object* lean_mk_io_error_permission_denied(lean_object*);
extern "C" lean_object* lean_mk_io_error_no_such_thing(lean_object*);
extern "C" lean_object* lean_mk_io_error_unsupported_operation(lean_object*);
extern "C" lean_object* lean_mk_io_error_hardware_fault(lean_object*);
extern "C" lean_object* lean_mk_io_error_unsatisfied_constraints(lean_object*);
extern "C" lean_object* lean_mk_io_error_illegal_operation(lean_object*);
extern "C" lean_object* lean_mk_io_error_protocol_error(lean_object*);
extern "C" lean_object* lean_mk_io_error_time_expired(lean_object*);
extern "C" void lean_io_result_show_error(b_obj_arg r) {
std::cerr << "uncaught exception: " << string_cstr(io_result_get_error(r)) << std::endl;
object * err = io_result_get_error(r);
inc_ref(err);
object * str = lean_io_error_to_string(err);
std::cerr << "uncaught exception: " << string_cstr(str) << std::endl;
dec_ref(str);
}
obj_res set_io_result(obj_arg a) {
@ -50,10 +85,7 @@ obj_res set_io_error(obj_arg e) {
return new_r;
}
object * mk_io_user_error(object * str) {
// TODO(Leo): fix after we expand IO.Error
return str;
}
extern "C" object * mk_io_user_error(object * str);
obj_res set_io_error(char const * msg) {
return set_io_error(mk_io_user_error(mk_string(msg)));
@ -102,37 +134,258 @@ extern "C" obj_res lean_io_prim_get_line(obj_arg /* w */) {
lean_unreachable();
}
/* handle.mk (s : string) (m : mode) (bin : bool := ff) : eio handle */
extern "C" obj_res lean_io_prim_handle_mk(b_obj_arg /* s */, uint8 /* mode */, uint8 /* bin */, obj_arg /* w */) {
// not implemented yet
lean_unreachable();
static lean_external_class * g_io_handle_external_class = nullptr;
static void io_handle_finalizer(void * h) {
fclose(static_cast<FILE *>(h));
}
/* handle.is_eof : handle → eio bool */
extern "C" obj_res lean_io_prim_handle_is_eof(b_obj_arg /* h */, obj_arg /* w */) {
// not implemented yet
lean_unreachable();
static void io_handle_foreach(void * /* mod */, b_obj_arg /* fn */) {
}
/* handle.flush : handle → eio bool */
extern "C" obj_res lean_io_prim_handle_flush(b_obj_arg /* h */, obj_arg /* w */) {
// not implemented yet
lean_unreachable();
static lean_object * io_wrap_handle(FILE *hfile) {
return lean_alloc_external(g_io_handle_external_class, hfile);
}
/* handle.close : handle → eio unit */
extern "C" obj_res lean_io_prim_handle_close(b_obj_arg /* h */, obj_arg /* w */) {
// not implemented yet
lean_unreachable();
static FILE * io_get_handle(lean_object * hfile) {
return static_cast<FILE *>(lean_get_external_data(hfile));
}
/* handle.get_line : handle → eio unit */
extern "C" obj_res lean_io_prim_handle_get_line(b_obj_arg /* h */, obj_arg /* w */) {
// not implemented yet
lean_unreachable();
obj_res decode_io_error(int errnum, b_obj_arg fname) {
object * details = mk_string(strerror(errnum));
switch (errnum) {
case EINTR:
lean_assert(fname != nullptr);
inc_ref(fname);
return lean_mk_io_error_interrupted(fname, details);
case ELOOP: case ENAMETOOLONG: case EDESTADDRREQ:
case EBADF: case EDOM: case EINVAL: case EILSEQ:
case ENOEXEC: case ENOSTR: case ENOTCONN:
case ENOTSOCK:
if (fname == nullptr) {
return lean_mk_io_error_invalid_argument(details);
} else {
inc_ref(fname);
return lean_mk_io_error_invalid_argument_file(fname, details);
}
case ENOENT:
lean_assert(fname != nullptr);
inc_ref(fname);
return lean_mk_io_error_no_file_or_directory(fname, details);
case EACCES: case EROFS: case ECONNABORTED: case EFBIG:
case EPERM:
if (fname == nullptr) {
return lean_mk_io_error_permission_denied(details);
} else {
inc_ref(fname);
return lean_mk_io_error_permission_denied_file(fname, details);
}
case EMFILE: case ENFILE: case ENOSPC:
case E2BIG: case EAGAIN: case EMLINK:
case EMSGSIZE: case ENOBUFS: case ENOLCK:
case ENOMEM: case ENOSR:
if (fname == nullptr) {
return lean_mk_io_error_resource_exhausted(details);
} else {
inc_ref(fname);
return lean_mk_io_error_resource_exhausted_file(fname, details);
}
case EISDIR: case EBADMSG: case ENOTDIR:
if (fname == nullptr) {
return lean_mk_io_error_inappropriate_type(details);
} else {
inc_ref(fname);
return lean_mk_io_error_inappropriate_type_file(fname, details);
}
case ENXIO: case EHOSTUNREACH: case ENETUNREACH:
case ECHILD: case ECONNREFUSED: case ENODATA:
case ENOMSG: case ESRCH:
if (fname == nullptr) {
return lean_mk_io_error_no_such_thing(details);
} else {
inc_ref(fname);
return lean_mk_io_error_no_such_thing_file(fname, details);
}
case EEXIST: case EINPROGRESS: case EISCONN:
lean_assert(fname == nullptr);
return lean_mk_io_error_already_exists(details);
case EIO:
lean_assert(fname == nullptr);
return lean_mk_io_error_hardware_fault(details);
case ENOTEMPTY:
lean_assert(fname == nullptr);
return lean_mk_io_error_unsatisfied_constraints(details);
case ENOTTY:
lean_assert(fname == nullptr);
return lean_mk_io_error_illegal_operation(details);
case ECONNRESET: case EIDRM: case ENETDOWN: case ENETRESET:
case ENOLINK: case EPIPE:
lean_assert(fname == nullptr);
return lean_mk_io_error_resource_vanished(details);
case EPROTO: case EPROTONOSUPPORT: case EPROTOTYPE:
lean_assert(fname == nullptr);
return lean_mk_io_error_protocol_error(details);
case ETIME: case ETIMEDOUT:
lean_assert(fname == nullptr);
return lean_mk_io_error_time_expired(details);
case EADDRINUSE: case EBUSY: case EDEADLK: case ETXTBSY:
lean_assert(fname == nullptr);
return lean_mk_io_error_resource_busy(details);
case EADDRNOTAVAIL: case EAFNOSUPPORT: case ENODEV:
case ENOPROTOOPT: case ENOSYS: case EOPNOTSUPP:
case ERANGE: case ESPIPE: case EXDEV:
lean_assert(fname == nullptr);
return lean_mk_io_error_unsupported_operation(details);
case EFAULT:
default:
lean_assert(fname == nullptr);
return lean_mk_io_error_other_error(details);
}
}
/* timeit {α : Type} (msg : @& string) (fn : io α) : io α */
/* IO.setAccessRights (filename : @& String) (mode : UInt32) : IO Handle */
extern "C" obj_res lean_chmod (b_obj_arg filename, uint32_t mode, obj_arg /* w */) {
if (!chmod(lean_string_cstr(filename), mode)) {
return set_io_result(box(0));
} else {
return set_io_error(decode_io_error(errno, filename));
}
}
/* Handle.mk (filename : @& String) (mode : @& String) : IO Handle */
extern "C" obj_res lean_io_prim_handle_mk(b_obj_arg filename, b_obj_arg modeStr, obj_arg /* w */) {
FILE *fp = fopen(lean_string_cstr(filename), lean_string_cstr(modeStr));
if (!fp) {
return set_io_error(decode_io_error(errno, filename));
} else {
return set_io_result(io_wrap_handle(fp));
}
}
/* Handle.isEof : (@& Handle) → IO Bool */
extern "C" obj_res lean_io_prim_handle_is_eof(b_obj_arg h, obj_arg /* w */) {
FILE * fp = io_get_handle(h);
return set_io_result(box(std::feof(fp) != 0));
}
/* Handle.flush : (@& Handle) → IO Bool */
extern "C" obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /* w */) {
FILE * fp = io_get_handle(h);
if (!std::fflush(fp)) {
return set_io_result(box(0));
} else {
return set_io_error(decode_io_error(errno, nullptr));
}
}
/* Handle.readByte : (@& Handle) → IO UInt8 */
extern "C" obj_res lean_io_prim_handle_read_byte(b_obj_arg h, obj_arg /* w */) {
FILE * fp = io_get_handle(h);
int c = std::fgetc(fp);
if (c != EOF) {
return set_io_result(box(c));
} else {
return set_io_error(decode_io_error(errno, nullptr));
}
}
/* Handle.writeByte : (@& Handle) → UInt8 → IO unit */
extern "C" obj_res lean_io_prim_handle_write_byte(b_obj_arg h, uint8 c, obj_arg /* w */) {
FILE * fp = io_get_handle(h);
if (std::fputc(c, fp) != EOF) {
return set_io_result(box(0));
} else {
return set_io_error(decode_io_error(errno, nullptr));
}
}
/* Handle.read : (@& Handle) → USize → IO ByteArray */
extern "C" obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes, obj_arg /* w */) {
FILE * fp = io_get_handle(h);
if (feof(fp)) {
return set_io_error(lean_mk_io_error_eof());
}
obj_res res = lean_alloc_sarray(1, 0, nbytes);
usize n = std::fread(lean_sarray_cptr(res), 1, nbytes, fp);
if (n > 0) {
lean_sarray_set_size(res, n);
return set_io_result(res);
} else if (feof(fp)) {
dec_ref(res);
return set_io_result(alloc_sarray(1, 0, 0));
} else {
dec_ref(res);
return set_io_error(decode_io_error(errno, nullptr));
}
}
/* Handle.write : (@& Handle) → (@& ByteArray) → IO unit */
extern "C" obj_res lean_io_prim_handle_write(b_obj_arg h, b_obj_arg buf, obj_arg /* w */) {
FILE * fp = io_get_handle(h);
usize n = lean_sarray_size(buf);
usize m = std::fwrite(lean_sarray_cptr(buf), 1, n, fp);
if (m == n) {
return set_io_result(box(0));
} else {
return set_io_error(decode_io_error(errno, nullptr));
}
}
obj_res lean_get_line(FILE * fp) {
const int buf_sz = 64;
lean_string_object * buf_str = lean_to_string(lean_alloc_string(0, buf_sz, 0));
lean_object * res_str = lean_alloc_string(1, buf_sz, 0);
lean_to_string(res_str)->m_data[0] = '\0';
char * out = nullptr;
do {
out = std::fgets(buf_str->m_data, buf_sz, fp);
if (out != nullptr) {
buf_str->m_size = strlen(buf_str->m_data);
buf_str->m_length = buf_str->m_size;
buf_str->m_size++;
res_str = lean_string_append(res_str, reinterpret_cast<object *>(buf_str));
}
} while (out != nullptr && buf_str->m_size == buf_sz);
dec_ref(reinterpret_cast<object *>(buf_str));
lean_to_string(res_str)->m_length = utf8_strlen(lean_to_string(res_str)->m_data);
if (out == nullptr && !feof(fp)) {
dec_ref(res_str);
return nullptr;
} else {
return res_str;
}
}
/* Handle.getLine : (@& Handle) → IO Unit */
/* The line returned by `lean_io_prim_handle_get_line` */
/* is truncated at the first '\0' character and the */
/* rest of the line is discarded. */
extern "C" obj_res lean_io_prim_handle_get_line(b_obj_arg h, obj_arg /* w */) {
FILE * fp = io_get_handle(h);
if (feof(fp)) {
return set_io_error(lean_mk_io_error_eof());
}
object * res = lean_get_line(fp);
if (res != nullptr) {
return set_io_result(res);
} else if (feof(fp)) {
return set_io_result(lean_mk_string(""));
} else {
return set_io_error(decode_io_error(errno, nullptr));
}
}
/* Handle.putStr : (@& Handle) → (@& String) → IO Unit */
extern "C" obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_arg s, obj_arg /* w */) {
FILE * fp = io_get_handle(h);
if (std::fputs(lean_string_cstr(s), fp) != EOF) {
return set_io_result(box(0));
} else {
return set_io_error(decode_io_error(errno, nullptr));
}
}
/* timeit {α : Type} (msg : @& String) (fn : IO α) : IO α */
extern "C" obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn, obj_arg w) {
auto start = std::chrono::steady_clock::now();
w = apply_1(fn, w);
@ -148,7 +401,7 @@ extern "C" obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn, obj_arg w) {
return w;
}
/* allocprof {α : Type} (msg : string) (fn : io α) : io α */
/* allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α */
extern "C" obj_res lean_io_allocprof(b_obj_arg msg, obj_arg fn, obj_arg w) {
std::ostream & out = std::cerr; // TODO(Leo): replace?
allocprof prof(out, string_cstr(msg));
@ -363,6 +616,7 @@ extern "C" obj_res lean_io_ref_ptr_eq(b_obj_arg ref1, b_obj_arg ref2, obj_arg) {
void initialize_io() {
g_io_error_nullptr_read = mk_string("null reference read");
mark_persistent(g_io_error_nullptr_read);
g_io_handle_external_class = lean_register_external_class(io_handle_finalizer, io_handle_foreach);
}
void finalize_io() {

11
src/runtime/lean.h
View file

@ -177,7 +177,7 @@ typedef struct {
typedef struct {
lean_object m_header;
size_t m_size;
size_t m_size; /* byte length including '\0' terminator */
size_t m_capacity;
size_t m_length; /* UTF8 length */
char m_data[0];
@ -951,6 +951,15 @@ static inline lean_obj_res lean_byte_array_size(b_lean_obj_arg a) {
return lean_box(lean_sarray_size(a));
}
/* static inline uint8_t lean_byte_array_uget(b_lean_obj_arg a, size_t i) { */
/* assert(i < lean_sarray_size(a)); */
/* return lean_to_sarray(a)->m_data[i]; */
/* } */
/* static inline uint8_t lean_byte_array_fget(b_lean_obj_arg a, b_lean_obj_arg i) { */
/* return lean_byte_array_uget(a, lean_unbox(i)); */
/* } */
static inline uint8_t lean_byte_array_get(b_lean_obj_arg a, b_lean_obj_arg i) {
if (lean_is_scalar(i)) {
size_t idx = lean_unbox(i);

3
src/shell/CMakeLists.txt
View file

@ -143,6 +143,9 @@ add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash)
# add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z")
add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
add_test(NAME lean_test_main_error
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run"
COMMAND bash "${LEAN_SOURCE_DIR}/cmake/check_main.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "print_error.lean")
if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows"))
# The following test cannot be executed on Windows because of the
# bash script timeout.sh

2
tests/bench/parser.lean
View file

@ -6,4 +6,4 @@ def main : List String → IO Unit
n.toNat.forM $ fun _ =>
Lean.Parser.parseFile env fname *> pure ();
pure ()
| _ => throw "give file"
| _ => throw $ IO.userError "give file"

5
tests/bench/rbmap_checkpoint.lean
View file

@ -82,9 +82,8 @@ def myLen : List Tree → Nat → Nat
| _ :: xs, r => myLen xs r
| [], r => r
def main (xs : List String) : IO UInt32 :=
do
[n, freq] ← pure xs | throw "invalid input";
def main (xs : List String) : IO UInt32 := do
[n, freq] ← pure xs | throw $ IO.userError "invalid input";
let n := n.toNat;
let freq := freq.toNat;
let freq := if freq == 0 then 1 else freq;

5
tests/lean/eval_except.lean Normal file
View file

@ -0,0 +1,5 @@
prelude
import Init.System.IO
#eval (throw $ IO.userError "this is my error" : IO Unit)
#eval (throw $ IO.Error.noFileOrDirectory "file.ext" "and details" : IO Unit)

5
tests/lean/eval_except.lean.expected.out Normal file
View file

@ -0,0 +1,5 @@
eval_except.lean:4:0: error: this is my error
eval_except.lean:5:0: error: No such file or directory
file: file.ext

16
tests/lean/file_not_found.lean Normal file
View file

@ -0,0 +1,16 @@
prelude
import Init.System.IO
open IO.FS
#eval (IO.FS.Handle.mk "non-existant-file.txt" Mode.read *> pure () : IO Unit)
#eval do condM (IO.fileExists "readonly.txt")
(pure ())
(IO.FS.withFile "readonly.txt" Mode.write $ fun _ => pure ());
IO.Access.setAccessRights "readonly.txt" { user := { read := true } };
(pure () : IO Unit)
#eval (IO.FS.Handle.mk "readonly.txt" Mode.write *> pure () : IO Unit)
#eval do h ← IO.FS.Handle.mk "readonly.txt" Mode.read;
h.putStr "foo";
IO.println "foo";
(pure () : IO Unit)

9
tests/lean/file_not_found.lean.expected.out Normal file
View file

@ -0,0 +1,9 @@
file_not_found.lean:6:0: error: No such file or directory
file: non-existant-file.txt
file_not_found.lean:12:0: error: Permission denied
file: readonly.txt
file_not_found.lean:13:0: error: Invalid argument: bad file descriptor

2
tests/lean/mvar1.lean
View file

@ -2,7 +2,7 @@ import Init.Lean.MetavarContext
open Lean
def check (b : Bool) : IO Unit :=
unless b (throw "error")
unless b (throw $ IO.userError "error")
def f := mkConst `f []
def g := mkConst `g []

2
tests/lean/mvar2.lean
View file

@ -2,7 +2,7 @@ import Init.Lean.MetavarContext
open Lean
def check (b : Bool) : IO Unit :=
unless b (throw "error")
unless b (throw $ IO.userError "error")
def f := mkConst `f []
def g := mkConst `g []

2
tests/lean/mvar3.lean
View file

@ -8,7 +8,7 @@ match MetavarContext.mkLambda xs e lctx { mctx := mctx, ngen := ngen } with
| EStateM.Result.error e s => Except.error e
def check (b : Bool) : IO Unit :=
unless b (throw "error")
unless b (throw $ IO.userError "error")
def f := mkConst `f
def g := mkConst `g

82
tests/lean/run/IO_test.lean Normal file
View file

@ -0,0 +1,82 @@
prelude
import Init.System.IO
import Init.Data.List.Control
open IO.FS
instance : HasRepr UInt8 := ⟨ toString ⟩
def check_eq {α} [HasBeq α] [HasRepr α] (tag : String) (expected actual : α) : IO Unit :=
unless (expected == actual) $ throw $ IO.userError $
"assertion failure \"" ++ tag ++
"\":\n expected: " ++ repr expected ++
"\n actual: " ++ repr actual
def test : IO Unit := do
let xs : ByteArray := ⟨#[1,2,3,4]⟩;
let fn := "foo.txt";
withFile fn Mode.write $ fun h => do
{ h.write xs;
h.write xs;
pure () };
ys ← withFile "foo.txt" Mode.read $ fun h => h.read 10;
check_eq "1" (xs.toList ++ xs.toList) ys.toList;
withFile fn Mode.append $ fun h => do
{ h.write ⟨#[5,6,7,8]⟩;
pure () };
withFile "foo.txt" Mode.read $ fun h => do
{ ys ← h.read 10;
check_eq "2" [1,2,3,4,1,2,3,4,5,6] ys.toList;
ys ← h.read 2;
check_eq "3" [7,8] ys.toList;
b ← h.isEof;
unless (!b)
(throw $ IO.userError $ "wrong (4): ");
ys ← h.read 2;
check_eq "5" [] ys.toList;
b ← h.isEof;
unless b
(throw $ IO.userError $ "wrong (6): ") };
pure ()
#eval test
def test2 : IO Unit := do
let fn2 := "foo2.txt";
let xs₀ : String := "⟨[₂,α]⟩";
let xs₁ := "⟨[6,8,@]⟩";
let xs₂ := "/* Handle.getLine : Handle → IO Unit */" ++
"/* The line returned by `lean_io_prim_handle_get_line` */" ++
"/* is truncated at the first \'\\0\' character and the */" ++
"/* rest of the line is discarded. */";
-- multi-buffer line
withFile fn2 Mode.write $ fun h => pure ();
withFile fn2 Mode.write $ fun h => do
{ h.putStr xs₀;
h.putStrLn xs₀;
h.putStrLn xs₂;
h.putStrLn xs₁;
pure () };
ys ← withFile fn2 Mode.read $ fun h => h.getLine;
check_eq "1" (xs₀ ++ xs₀ ++ "\n") ys;
withFile fn2 Mode.append $ fun h => do
{ h.putStrLn xs₁;
pure () };
ys ← withFile fn2 Mode.read $ fun h => do
{ ys ← (List.iota 5).mapM $ fun i => do
{ ln ← h.getLine;
-- IO.println ∘ repr $ ln;
b ← h.isEof;
unless (i == 1 || !b) (throw $ IO.userError "isEof");
pure ln };
b ← h.isEof;
unless b (throw $ IO.userError "not isEof");
pure ys };
let rs := [xs₀ ++ xs₀ ++ "\n", xs₂ ++ "\n", xs₁ ++ "\n", xs₁ ++ "\n", ""];
check_eq "2" rs ys;
ys ← readFile fn2;
check_eq "3" (String.join rs) ys;
pure ()
#eval test2

36
tests/lean/run/expr1.lean
View file

@ -10,7 +10,7 @@ do let f := mkConst `f [];
let as₂ := t.getAppRevArgs;
IO.println as₁;
IO.println as₂;
unless (as₁.reverse == as₂) $ throw "failed";
unless (as₁.reverse == as₂) $ throw $ IO.userError "failed";
pure ()
#eval tst1
@ -20,7 +20,7 @@ do let l1 := mkLevelMax (mkLevelParam `a) (mkLevelParam `b);
let l2 := mkLevelMax (mkLevelParam `b) (mkLevelParam `a);
IO.println l1;
IO.println l2;
unless (Level.isEquiv l1 l2) $ throw "not equiv";
unless (Level.isEquiv l1 l2) $ throw $ IO.userError "not equiv";
pure ()
#eval tst2
@ -49,12 +49,12 @@ do let f := mkConst `f [];
let t2 := mkAppN f #[a, x0];
let t3 := mkLambda `x BinderInfo.default (mkSort levelZero) (mkAppN f #[a, x0]);
let t4 := mkLambda `x BinderInfo.default (mkSort levelZero) (mkAppN f #[a, x1]);
unless (!t1.hasLooseBVar 0) $ throw "failed-1";
unless (t2.hasLooseBVar 0) $ throw "failed-2";
unless (!t3.hasLooseBVar 0) $ throw "failed-3";
unless (t4.hasLooseBVar 0) $ throw "failed-4";
unless (!t4.hasLooseBVar 1) $ throw "failed-5";
unless (!t2.hasLooseBVar 1) $ throw "failed-6";
unless (!t1.hasLooseBVar 0) $ throw $ IO.userError "failed-1";
unless (t2.hasLooseBVar 0) $ throw $ IO.userError "failed-2";
unless (!t3.hasLooseBVar 0) $ throw $ IO.userError "failed-3";
unless (t4.hasLooseBVar 0) $ throw $ IO.userError "failed-4";
unless (!t4.hasLooseBVar 1) $ throw $ IO.userError "failed-5";
unless (!t2.hasLooseBVar 1) $ throw $ IO.userError "failed-6";
pure ()
#eval tst4
@ -68,27 +68,27 @@ do let f := mkConst `f [];
let x2 := mkBVar 2;
let t := mkLambda `x BinderInfo.default nat (mkApp f x0);
IO.println t.etaExpanded?;
unless (t.etaExpanded? == some f) $ throw "failed-1";
unless (t.etaExpanded? == some f) $ throw $ IO.userError "failed-1";
let t := mkLambda `x BinderInfo.default nat (mkApp f x1);
unless (t.etaExpanded? == none) $ throw "failed-2";
unless (t.etaExpanded? == none) $ throw $ IO.userError "failed-2";
let t := mkLambda `x BinderInfo.default nat (mkAppN f #[a, x0]);
unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-3";
unless (t.etaExpanded? == some (mkApp f a)) $ throw $ IO.userError "failed-3";
let t := mkLambda `x BinderInfo.default nat (mkAppN f #[x0, x0]);
unless (t.etaExpanded? == none) $ throw "failed-4";
unless (t.etaExpanded? == none) $ throw $ IO.userError "failed-4";
let t := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkApp f x0));
unless (t.etaExpanded? == none) $ throw "failed-5";
unless (t.etaExpanded? == none) $ throw $ IO.userError "failed-5";
let t := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkAppN f #[x1, x0]));
IO.println t;
unless (t.etaExpanded? == some f) $ throw "failed-6";
unless (t.etaExpanded? == some f) $ throw $ IO.userError "failed-6";
let t := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkLambda `z BinderInfo.default nat (mkAppN f #[x2, x1, x0])));
IO.println t;
unless (t.etaExpanded? == some f) $ throw "failed-7";
unless (t.etaExpanded? == some f) $ throw $ IO.userError "failed-7";
let t := mkLambda `x BinderInfo.default nat (mkLambda `y BinderInfo.default nat (mkLambda `z BinderInfo.default nat (mkAppN f #[a, x2, x1, x0])));
IO.println t;
unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-8";
unless (t.etaExpanded? == some (mkApp f a)) $ throw $ IO.userError "failed-8";
IO.println t.etaExpanded?;
let t := mkApp f a;
unless (t.etaExpanded? == some (mkApp f a)) $ throw "failed-9";
unless (t.etaExpanded? == some (mkApp f a)) $ throw $ IO.userError "failed-9";
pure ()
#eval tst5
@ -102,7 +102,7 @@ IO.println (t1.liftLooseBVars 0 1);
IO.println (t2.liftLooseBVars 0 1);
let t3 := (t2.liftLooseBVars 0 1).lowerLooseBVars 1 1;
IO.println $ t3;
unless (t2 == t3) $ throw "failed-1";
unless (t2 == t3) $ throw $ IO.userError "failed-1";
pure ()
#eval tst6

2
tests/lean/run/expr_maps.lean
View file

@ -18,7 +18,7 @@ def exprT3 := mkLambda `x biDef exprNat (mkApp (mkConst `f []) (mkBVar
def exprT4 := mkLambda `x BinderInfo.implicit exprNat (mkApp (mkConst `f []) (mkBVar 0))
def check (b : Bool) : IO Unit :=
unless b (throw "failed")
unless b (throw $ IO.userError "failed")
def tst1 : IO Unit :=
do IO.println TypeArrowType;

5
tests/lean/run/print_error.lean Normal file
View file

@ -0,0 +1,5 @@
prelude
import Init.System.IO
def main : IO Unit :=
throw $ IO.Error.noFileOrDirectory "file.ext" "this is some context"

2
tests/lean/run/print_error.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
uncaught exception: No such file or directory
file: file.ext

2
tests/plugin/Default.lean
View file

@ -7,7 +7,7 @@ def oh_no : Nat := 0
def snakeLinter : Linter :=
fun env n =>
-- TODO(Sebastian): return actual message with position from syntax tree
if n.toString.contains '_' then throw "SNAKES!!"
if n.toString.contains '_' then throw $ IO.userError "SNAKES!!"
else pure MessageLog.empty
@[init]