open DisambiguateTypes
open UriManager
-exception NoWellTypedInterpretation of string Lazy.t list
+exception NoWellTypedInterpretation of
+ (Token.flocation option * string Lazy.t) list
exception PathNotWellFormed
(** raised when an environment is not enough informative to decide *)
type 'a test_result =
| Ok of 'a * Cic.metasenv
- | Ko of string Lazy.t
- | Uncertain of string Lazy.t
+ | Ko of Token.flocation option * string Lazy.t
+ | Uncertain of Token.flocation option * string Lazy.t
-let refine_term metasenv context uri term ugraph =
+let refine_term metasenv context uri term ugraph ~localization_tbl =
(* if benchmark then incr actual_refinements; *)
assert (uri=None);
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
try
let term', _, metasenv',ugraph1 =
- CicRefine.type_of_aux' metasenv context term ugraph in
+ CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
(Ok (term', metasenv')),ugraph1
with
- | CicRefine.Uncertain msg ->
- debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
- Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph
- | CicRefine.RefineFailure msg ->
- debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
- (CicPp.ppterm term) (Lazy.force msg)));
- Ko (msg (*lazy ("Error trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph
+ exn ->
+ let rec process_exn loc =
+ function
+ HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
+ | CicRefine.Uncertain msg ->
+ debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
+ Uncertain (loc,msg),ugraph
+ | CicRefine.RefineFailure msg ->
+ debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+ (CicPp.ppterm term) (Lazy.force msg)));
+ Ko (loc,msg),ugraph
+ | exn -> raise exn
+ in
+ process_exn None exn
-let refine_obj metasenv context uri obj ugraph =
+let refine_obj metasenv context uri obj ugraph ~localization_tbl =
assert (context = []);
debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
try
- let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
+ let obj', metasenv,ugraph =
+ CicRefine.typecheck metasenv uri obj ~localization_tbl
+ in
(Ok (obj', metasenv)),ugraph
with
- | CicRefine.Uncertain msg ->
- debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
- Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph
- | CicRefine.RefineFailure msg ->
- debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
- (CicPp.ppobj obj) (Lazy.force msg))) ;
- Ko (msg (*lazy ("Error trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph
+ exn ->
+ let rec process_exn loc =
+ function
+ HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
+ | CicRefine.Uncertain msg ->
+ debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
+ Uncertain (loc,msg),ugraph
+ | CicRefine.RefineFailure msg ->
+ debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+ (CicPp.ppobj obj) (Lazy.force msg))) ;
+ Ko (loc,msg),ugraph
+ | exn -> raise exn
+ in
+ process_exn None exn
let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
try
in
aux 1 context
-let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
+let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
+ ~localization_tbl
+=
assert (uri = None);
let rec aux loc (context: Cic.name list) = function
| CicNotationPt.AttributedTerm (`Loc loc, term) ->
- aux loc context term
+ let res = aux loc context term in
+ Cic.CicHash.add localization_tbl res loc;
+ res
| CicNotationPt.AttributedTerm (_, term) -> aux loc context term
| CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
let cic_args = List.map (aux loc context) args in
| None -> Cic.Implicit annotation
| Some term -> aux loc context term
in
- match ast with
- | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term
- | term -> aux dummy_floc context term
+ aux dummy_floc context ast
let interpretate_path ~context path =
- interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true path
+ let localization_tbl = Cic.CicHash.create 23 in
+ (* here we are throwing away useful localization informations!!! *)
+ fst (
+ interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true
+ path ~localization_tbl, localization_tbl)
-let interpretate_obj ~context ~env ~uri ~is_path obj =
+let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
assert (context = []);
assert (is_path = false);
+ let interpretate_term = interpretate_term ~localization_tbl in
match obj with
| CicNotationPt.Inductive (params,tyl) ->
let uri = match uri with Some uri -> uri | None -> assert false in
aliases todo_dom
in
try
+ let localization_tbl = Cic.CicHash.create 503 in
let cic_thing =
interpretate_thing ~context:disambiguate_context ~env:filled_env
- ~uri ~is_path:false thing
+ ~uri ~is_path:false thing ~localization_tbl
in
let foo () =
- let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
+ let k,ugraph1 =
+ refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
+ in
(k , ugraph1 )
in refine_profiler.HExtlib.profile foo ()
with
- | Try_again msg -> Uncertain msg, ugraph
- | Invalid_choice msg -> Ko msg, ugraph
+ | Try_again msg -> Uncertain (None,msg), ugraph
+ | Invalid_choice msg -> Ko (None,msg), ugraph
in
(* (4) build all possible interpretations *)
let (@@) (l1,l2) (l1',l2') = l1@l1', l2@l2' in
(match test_env aliases [] base_univ with
| Ok (thing, metasenv),new_univ ->
[ aliases, diff, metasenv, thing, new_univ ], []
- | Ko msg,_ | Uncertain msg,_ -> [],[msg])
+ | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg])
| item :: remaining_dom ->
debug_print (lazy (sprintf "CHOOSED ITEM: %s"
(string_of_domain_item item)));
None -> lookup_choices item
| Some choices -> choices in
match choices with
- [] -> [], [lazy ("No choices for " ^ string_of_domain_item item)]
+ [] ->
+ [], [None,lazy ("No choices for " ^ string_of_domain_item item)]
| [codomain_item] ->
(* just one choice. We perform a one-step look-up and
if the next set of choices is also a singleton we
| _ ->
aux new_env new_diff lookup_in_todo_dom
remaining_dom new_univ)
- | Uncertain msg,new_univ ->
+ | Uncertain (loc,msg),new_univ ->
(match remaining_dom with
- | [] -> [], [msg]
+ | [] -> [], [loc,msg]
| _ ->
aux new_env new_diff lookup_in_todo_dom
remaining_dom new_univ)
- | Ko msg,_ -> [], [msg])
+ | Ko (loc,msg),_ -> [], [loc,msg])
| _::_ ->
let rec filter univ = function
| [] -> [],[]
| _ -> aux new_env new_diff None remaining_dom new_univ
) @@
filter univ tl
- | Uncertain msg,new_univ ->
+ | Uncertain (loc,msg),new_univ ->
(match remaining_dom with
- | [] -> [],[msg]
+ | [] -> [],[loc,msg]
| _ -> aux new_env new_diff None remaining_dom new_univ
) @@
filter univ tl
- | Ko msg,_ -> ([],[msg]) @@ filter univ tl)
+ | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl)
in
filter base_univ choices
in
projects / helm.git / blobdiff