diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-03 20:34:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-12-16 13:15:12 +0100 |
| commit | bff51607cfdda137d7bc55d802895d7f794d5768 (patch) | |
| tree | 1a159136a88ddc6561b814fb4ecbacdf9de0dd70 /pretyping/pretyping.ml | |
| parent | 37ed28dfe253615729763b5d81a533094fb5425e (diff) | |
Getting rid of Exninfo hacks.
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index dfe018c33..07cc36815 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -77,7 +77,9 @@ let search_guard loc env possible_indexes fixdefs = let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with reraise -> - let e = Errors.push reraise in Loc.raise loc e); + let (e, info) = Errors.push reraise in + let info = Loc.add_loc info loc in + iraise (e, info)); indexes else (* we now search recursively amoungst all combinations *) @@ -176,7 +178,7 @@ let apply_heuristics env evdref fail_evar = try evdref := consider_remaining_unif_problems ~ts:(Typeclasses.classes_transparent_state ()) env !evdref with e when Errors.noncritical e -> - let e = Errors.push e in if fail_evar then raise e + let e = Errors.push e in if fail_evar then iraise e let check_typeclasses_instances_are_solved env current_sigma pending = (* Naive way, call resolution again with failure flag *) @@ -542,7 +544,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let cofix = (i,(names,ftys,fdefs)) in (try check_cofix env cofix with reraise -> - let e = Errors.push reraise in Loc.raise loc e); + let (e, info) = Errors.push reraise in + let info = Loc.add_loc info loc in + iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env evdref fixj tycon @@ -672,7 +676,10 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let resj = try judge_of_product env name j j' - with TypeError _ as e -> let e = Errors.push e in Loc.raise loc e in + with TypeError _ as e -> + let (e, info) = Errors.push e in + let info = Loc.add_loc info loc in + iraise (e, info) in inh_conv_coerce_to_tycon loc env evdref resj tycon | GLetIn(loc,name,c1,c2) -> |