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

chore(library/init/meta/base_tactic): exception takes 'options'

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-07 09:54:50 -07:00
parent d68b7eafd7
commit 36046072a4
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/init/meta/base_tactic.lean
View file

@ -6,12 +6,14 @@ Authors: Leonardo de Moura
prelude
import init.monad init.meta.format
/-
Remark: we use a thunk that produces a format object as the exception information.
Motivation: the formatting object may be big.
Remark: we use a function that produces a format object as the exception information.
Motivation: the formatting object may be big, and we may create it on demand.
Remark: We use base_tactic_result to define base_tactic (a monad that combines the state an exceptional monads).
We "merge" them for performance reasons.
-/
inductive base_tactic_result (S : Type) (A : Type) :=
| success : A → S → base_tactic_result S A
| exception : (unit → format) → base_tactic_result S A
| exception : (options → format) → base_tactic_result S A
section
open base_tactic_result
@ -20,7 +22,7 @@ variables [has_to_string A]
protected meta_definition base_tactic_result.to_string : base_tactic_result S A → string
| (success a s) := to_string a
| (exception S A e) := "Exception: " + to_string (e unit.star)
| (exception S A e) := "Exception: " + to_string (e options.mk)
protected meta_definition base_tactic_result.has_to_string [instance] : has_to_string (base_tactic_result S A) :=
has_to_string.mk base_tactic_result.to_string