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

feat: use trick to inform compiler that a builtin doesn't throw exceptions

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-20 11:05:11 -07:00
parent e153f245d7
commit 4e736bcca0
1 changed files with 23 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -327,18 +327,35 @@ def Ref (α : Type) : Type := (RefPointed α).type
instance (α : Type) : Inhabited (Ref α) := ⟨(RefPointed α).val⟩
namespace Prim
@[inline] unsafe def exceptionFreeUnsafe {α} (x : IO α) : IO α :=
fun s => match x s with
| r@(EStateM.Result.error _ _) => False.elim lcProof
| r => r
/- TODO: add a exceptionFreeBuiltin macro that creates an unsafe definition `using exceptionFreeUnsafe`
and then seals it using `implementedBy`. Then, we can remove the not so safe constant `exceptionFree`. -/
@[implementedBy exceptionFreeUnsafe] private constant exceptionFree {α} (x : IO α) : IO α :=
x
@[extern "lean_io_mk_ref"]
constant mkRef {α : Type} (a : α) : IO (Ref α) := arbitrary _
constant mkRefCore {α : Type} (a : α) : IO (Ref α) := arbitrary _
@[inline] def mkRef {α : Type} (a : α) : IO (Ref α) := exceptionFree $ mkRefCore a
@[extern "lean_io_ref_get"]
constant Ref.get {α : Type} (r : @& Ref α) : IO α := arbitrary _
constant Ref.getCore {α : Type} (r : @& Ref α) : IO α := arbitrary _
@[inline] def Ref.get {α : Type} (r : Ref α) : IO α := exceptionFree $ Ref.getCore r
@[extern "lean_io_ref_set"]
constant Ref.set {α : Type} (r : @& Ref α) (a : α) : IO Unit := arbitrary _
constant Ref.setCore {α : Type} (r : @& Ref α) (a : α) : IO Unit := arbitrary _
@[inline] def Ref.set {α : Type} (r : Ref α) (a : α) : IO Unit := exceptionFree $ Ref.setCore r a
@[extern "lean_io_ref_swap"]
constant Ref.swap {α : Type} (r : @& Ref α) (a : α) : IO α := arbitrary _
constant Ref.swapCore {α : Type} (r : @& Ref α) (a : α) : IO α := arbitrary _
@[inline] def Ref.swap {α : Type} (r : Ref α) (a : α) : IO α := exceptionFree $ Ref.swapCore r a
@[extern "lean_io_ref_take"]
unsafe constant Ref.take {α : Type} (r : @& Ref α) : IO α := arbitrary _
unsafe constant Ref.takeCore {α : Type} (r : @& Ref α) : IO α := arbitrary _
@[inline] unsafe def Ref.take {α : Type} (r : Ref α) : IO α := exceptionFree $ Ref.takeCore r
@[extern "lean_io_ref_ptr_eq"]
constant Ref.ptrEq {α : Type} (r1 r2 : @& Ref α) : IO Bool := arbitrary _
constant Ref.ptrEqCore {α : Type} (r1 r2 : @& Ref α) : IO Bool := arbitrary _
@[inline] def Ref.ptrEq {α : Type} (r1 r2 : Ref α) : IO Bool := exceptionFree $ Ref.ptrEqCore r1 r2
end Prim
section