From: Enrico Tassi Date: Wed, 12 Nov 2008 12:09:52 +0000 (+0000) Subject: exported disambiguate_thing X-Git-Tag: make_still_working~4570 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=1f3e810634367e2ce4b929a935ac6f3553870632;p=helm.git exported disambiguate_thing --- diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 68afd810b..e11927d7d 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -103,8 +103,8 @@ let descr_of_domain_item = function | Symbol (s, _) -> s | Num i -> string_of_int i -type 'a test_result = - | Ok of 'a * Cic.metasenv +type ('a,'m) test_result = + | Ok of 'a * 'm | Ko of Stdpp.location option * string Lazy.t | Uncertain of Stdpp.location option * string Lazy.t @@ -172,12 +172,12 @@ let find_in_context name context = in aux 1 context -let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~uri ~is_path ast +let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast ~localization_tbl = (* create_dummy_ids shouldbe used only for interpretating patterns *) assert (uri = None); - let rec aux ~localize loc (context: Cic.name list) = function + let rec aux ~localize loc context = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> let res = aux ~localize loc context term in if localize then Cic.CicHash.add localization_tbl res loc; @@ -546,7 +546,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ | CicNotationPt.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () | _ -> assert false (* god bless Bologna *) - and aux_option ~localize loc (context: Cic.name list) annotation = function + and aux_option ~localize loc context annotation = function | None -> Cic.Implicit annotation | Some term -> aux ~localize loc context term in @@ -661,6 +661,16 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl = | Some bo,_ -> let bo' = Some (interpretate_term [] env None false bo) in Cic.Constant (name,bo',ty',[],attrs)) +;; + +let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast + ~localization_tbl += + let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in +interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast +~localization_tbl +;; + let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function | Ast.AttributedTerm (`Loc loc, term) -> @@ -834,6 +844,7 @@ let domain_of_term ~context term = uniq_domain (domain_of_term ~context term) let domain_of_obj ~context ast = + let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in assert (context = []); match ast with | Ast.Theorem (_,_,ty,bo) -> @@ -884,6 +895,12 @@ let domain_of_obj ~context ast = let domain_of_obj ~context obj = uniq_domain (domain_of_obj ~context obj) +let domain_of_term ~context term = + let context = + List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context + in + domain_of_term ~context term + (* dom1 \ dom2 *) let domain_diff dom1 dom2 = (* let domain_diff = Domain.diff *) @@ -911,6 +928,33 @@ let domain_diff dom1 dom2 = module type Disambiguator = sig + val disambiguate_thing: + dbd:HSql.dbd -> + context:'context -> + metasenv:'metasenv -> + initial_ugraph:'ugraph -> + aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t -> + universe:DisambiguateTypes.codomain_item list + DisambiguateTypes.Environment.t option -> + uri:'uri -> + pp_thing:('ast_thing -> string) -> + domain_of_thing:(context:'context -> 'ast_thing -> domain) -> + interpretate_thing:(context:'context -> + env:DisambiguateTypes.codomain_item + DisambiguateTypes.Environment.t -> + uri:'uri -> + is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) -> + refine_thing:('metasenv -> + 'context -> + 'uri -> + 'raw_thing -> + 'ugraph -> localization_tbl:'cichash -> ('refined_thing, + 'metasenv) test_result * 'ugraph) -> + localization_tbl:'cichash -> + string * int * 'ast_thing -> + ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item) + list * 'metasenv * 'refined_thing * 'ugraph) + list * bool val disambiguate_term : ?fresh_instances:bool -> dbd:HSql.dbd -> @@ -979,18 +1023,14 @@ module Make (C: Callbacks) = let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let disambiguate_thing ~dbd ~context ~metasenv - ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe + ~initial_ugraph ~aliases ~universe ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing + ~localization_tbl (thing_txt,thing_txt_prefix_len,thing) = debug_print (lazy "DISAMBIGUATE INPUT"); - let disambiguate_context = (* cic context -> disambiguate context *) - List.map - (function None -> Cic.Anonymous | Some (name, _) -> name) - context - in debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); - let thing_dom = domain_of_thing ~context:disambiguate_context thing in + let thing_dom = domain_of_thing ~context thing in debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom))); (* @@ -1076,9 +1116,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" aux (aux env l) tl in let filled_env = aux aliases todo_dom in try - let localization_tbl = Cic.CicHash.create 503 in let cic_thing = - interpretate_thing ~context:disambiguate_context ~env:filled_env + interpretate_thing ~context ~env:filled_env ~uri ~is_path:false thing ~localization_tbl in let foo () = @@ -1285,11 +1324,13 @@ in refine_profiler.HExtlib.profile foo () let term = if fresh_instances then CicNotationUtil.freshen_term term else term in + let localization_tbl = Cic.CicHash.create 503 in disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) ~refine_thing:refine_term (text,prefix_len,term) + ~localization_tbl let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri (text,prefix_len,obj) @@ -1297,9 +1338,14 @@ in refine_profiler.HExtlib.profile foo () let obj = if fresh_instances then CicNotationUtil.freshen_obj obj else obj in + let localization_tbl = Cic.CicHash.create 503 in disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj + ~initial_ugraph:CicUniv.empty_ugraph ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj + ~localization_tbl (text,prefix_len,obj) + end + diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli index 5dc0df28b..99c1e4556 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.mli +++ b/helm/software/components/cic_disambiguation/disambiguate.mli @@ -45,8 +45,46 @@ val interpretate_path : type 'a disambiguator_input = string * int * 'a +type domain = domain_tree list +and domain_tree = + Node of Stdpp.location list * DisambiguateTypes.domain_item * domain +type ('a,'m) test_result = + | Ok of 'a * 'm + | Ko of Stdpp.location option * string Lazy.t + | Uncertain of Stdpp.location option * string Lazy.t + module type Disambiguator = sig + val disambiguate_thing: + dbd:HSql.dbd -> + context:'context -> + metasenv:'metasenv -> + initial_ugraph:'ugraph -> + aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t -> + universe:DisambiguateTypes.codomain_item list + DisambiguateTypes.Environment.t option -> + uri:'uri -> + pp_thing:('ast_thing -> string) -> + domain_of_thing:(context:'context -> 'ast_thing -> domain) -> + interpretate_thing:(context:'context -> + env:DisambiguateTypes.codomain_item + DisambiguateTypes.Environment.t -> + uri:'uri -> + is_path:bool -> + 'ast_thing -> + localization_tbl:'cichash -> 'raw_thing) -> + refine_thing:('metasenv -> + 'context -> + 'uri -> + 'raw_thing -> + 'ugraph -> localization_tbl:'cichash -> ('refined_thing, + 'metasenv) test_result * 'ugraph) -> + localization_tbl:'cichash -> + string * int * 'ast_thing -> + ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item) + list * 'metasenv * 'refined_thing * 'ugraph) + list * bool + (** @param fresh_instances when set to true fresh instances will be generated * for each number _and_ symbol in the disambiguation domain. Instances of the * input AST will be ignored. Defaults to false. *) @@ -78,6 +116,7 @@ sig Cic.obj * CicUniv.universe_graph) list * (* disambiguated obj *) bool (* has interactive_interpretation_choice been invoked? *) + end module Make (C : DisambiguateTypes.Callbacks) : Disambiguator diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml index 8827e709b..ddd655bc4 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml @@ -222,3 +222,5 @@ let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj = let f = Disambiguator.disambiguate_obj ~dbd ~uri in disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff obj + +let disambiguate_thing = assert false