X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=ce26f935131f418f26963c4e8121ba7948a74e15;hb=a56837c8e421a9d1e71566bde12ea8cc1518cfba;hp=f8fa77dc67b894f6bc5a77f2a820ac65942f2f75;hpb=f5b76bf5f55bbd2f2053e36d4b251548f3ed8623;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index f8fa77dc6..ce26f9351 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -28,8 +28,8 @@ open Printf open DisambiguateTypes open UriManager -exception No_choices of domain_item -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 *) @@ -56,40 +56,56 @@ let descr_of_domain_item = function 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 (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 (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 (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 (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 @@ -107,11 +123,15 @@ let find_in_context name (context: Cic.name list) = 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 @@ -353,18 +373,21 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | 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 - | GrafiteAst.Inductive (params,tyl) -> + | CicNotationPt.Inductive (params,tyl) -> let uri = match uri with Some uri -> uri | None -> assert false in let context,params = let context,res = @@ -412,7 +435,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = ) tyl in Cic.InductiveDefinition (tyl,[],List.length params,[]) - | GrafiteAst.Record (params,name,ty,fields) -> + | CicNotationPt.Record (params,name,ty,fields) -> let uri = match uri with Some uri -> uri | None -> assert false in let context,params = let context,res = @@ -450,7 +473,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj = let field_names = List.map fst fields in Cic.InductiveDefinition (tyl,[],List.length params,[`Class (`Record field_names)]) - | GrafiteAst.Theorem (flavour, name, ty, bo) -> + | CicNotationPt.Theorem (flavour, name, ty, bo) -> let attrs = [`Flavour flavour] in let ty' = interpretate_term [] env None false ty in (match bo with @@ -601,12 +624,12 @@ let domain_of_obj ~context ast = assert (context = []); let domain_rev = match ast with - | GrafiteAst.Theorem (_,_,ty,bo) -> + | CicNotationPt.Theorem (_,_,ty,bo) -> (match bo with None -> [] | Some bo -> domain_rev_of_term [] bo) @ domain_of_term [] ty - | GrafiteAst.Inductive (params,tyl) -> + | CicNotationPt.Inductive (params,tyl) -> let dom = List.flatten ( List.rev_map @@ -626,7 +649,7 @@ let domain_of_obj ~context ast = not ( List.exists (fun (name',_) -> name = Id name') params || List.exists (fun (name',_,_,_) -> name = Id name') tyl) ) dom - | GrafiteAst.Record (params,_,ty,fields) -> + | CicNotationPt.Record (params,_,ty,fields) -> let dom = List.flatten (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in @@ -676,7 +699,7 @@ sig aliases:DisambiguateTypes.environment ->(* previous interpretation status *) universe:DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) - GrafiteAst.obj -> + CicNotationPt.obj -> ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.obj * @@ -687,7 +710,7 @@ end module Make (C: Callbacks) = struct let choices_of_id dbd id = - let uris = MetadataQuery.locate ~dbd id in + let uris = Whelp.locate ~dbd id in let uris = match uris with | [] -> @@ -752,7 +775,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" | Id id -> choices_of_id dbd id | Symbol (symb, _) -> List.map DisambiguateChoices.mk_choice - (CicNotationRew.lookup_interpretations symb) + (TermAcicContent.lookup_interpretations symb) | Num instance -> DisambiguateChoices.lookup_num_choices () in @@ -760,10 +783,14 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" | None -> lookup_in_library () | Some e -> (try + let item = + match item with + | Symbol (symb, _) -> Symbol (symb, 0) + | item -> item + in Environment.find item e - with Not_found -> lookup_in_library ()) + with Not_found -> []) in - if choices = [] then raise (No_choices item); choices in (* @@ -805,17 +832,20 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" 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 @@ -826,7 +856,7 @@ in refine_profiler.HExtlib.profile foo () (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))); @@ -835,7 +865,8 @@ in refine_profiler.HExtlib.profile foo () None -> lookup_choices item | Some choices -> choices in match choices with - [] -> [], [lazy "No choices"] + [] -> + [], [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 @@ -862,13 +893,13 @@ in refine_profiler.HExtlib.profile foo () | _ -> 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 | [] -> [],[] @@ -883,13 +914,13 @@ in refine_profiler.HExtlib.profile foo () | _ -> 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 @@ -942,33 +973,8 @@ in refine_profiler.HExtlib.profile foo () if fresh_instances then CicNotationUtil.freshen_obj obj else obj in disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri - ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj + ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj obj end -module Trivial = -struct - exception Ambiguous_term of string Lazy.t - exception Exit - module Callbacks = - struct - let interactive_user_uri_choice ~selection_mode ?ok - ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = - raise Exit - let interactive_interpretation_choice interp = raise Exit - let input_or_locate_uri ~(title:string) ?id = raise Exit - end - module Disambiguator = Make (Callbacks) - let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph - ?(aliases = DisambiguateTypes.Environment.empty) term - = - let ast = - CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term) - in - try - fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast - ?initial_ugraph ~aliases ~universe:None) - with Exit -> raise (Ambiguous_term (lazy term)) -end -