From: Enrico Tassi Date: Wed, 26 Nov 2008 17:11:00 +0000 (+0000) Subject: almost done X-Git-Tag: make_still_working~4500 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=252b382c0c3c2aec2571d8a4ba563c8a1bad74bb;p=helm.git almost done --- diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nDisambiguate.ml index 5313ee20f..f4213bc30 100644 --- a/helm/software/components/ng_disambiguation/nDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nDisambiguate.ml @@ -50,16 +50,13 @@ let refine_term metasenv subst context uri term _ ~localization_tbl = Disambiguate.Ko loc_msg ;; -let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = +let resolve (env: NCic.term codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = ignore (env,item,num,args); - assert false - (* try snd (Environment.find item env) env num args with Not_found -> failwith ("Domain item not found: " ^ (DisambiguateTypes.string_of_domain_item item)) -*) (* TODO move it to Cic *) let find_in_context name context = @@ -407,8 +404,9 @@ let domain_of_term ~context = module Make (C : DisambiguateTypes.Callbacks) = struct module Disambiguator = Disambiguate.Make(C) - let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv ~subst - ~aliases ~universe ?goal (text,prefix_len,term) + let disambiguate_term ?(fresh_instances=false) ~context ~metasenv ~subst + ~aliases ~universe ~lookup_in_library ?goal + (text,prefix_len,term) = let term = if fresh_instances then CicNotationUtil.freshen_term term else term @@ -430,9 +428,11 @@ module Make (C : DisambiguateTypes.Callbacks) = struct in let res,b = Disambiguator.disambiguate_thing - ~dbd ~context ~metasenv ~initial_ugraph:() ~aliases + ~context ~metasenv ~initial_ugraph:() ~aliases ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term - ~domain_of_thing:domain_of_term + ~mk_implicit:(function None -> NCic.Implicit `Term + | Some `Closed -> NCic.Implicit `Closed) + ~lookup_in_library ~domain_of_thing:domain_of_term ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) ~refine_thing:refine_term (text,prefix_len,term) ~localization_tbl ~hint ~subst diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.mli b/helm/software/components/ng_disambiguation/nDisambiguate.mli index a61d37653..ae1b16f59 100644 --- a/helm/software/components/ng_disambiguation/nDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nDisambiguate.mli @@ -14,15 +14,24 @@ module Make (C : DisambiguateTypes.Callbacks) : sig val disambiguate_term : ?fresh_instances:bool -> - dbd:HSql.dbd -> context:NCic.context -> metasenv:NCic.metasenv -> subst:NCic.substitution -> - aliases:DisambiguateTypes.environment ->(* previous interpretation status *) - universe:DisambiguateTypes.multiple_environment option -> + aliases:NCic.term DisambiguateTypes.environment ->(* previous interpretation status *) + universe:NCic.term DisambiguateTypes.multiple_environment option -> + lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> + msg:string -> + id:string -> + UriManager.uri list -> UriManager.uri list) -> + (title:string -> ?id:string -> unit -> UriManager.uri option) -> + DisambiguateTypes.Environment.key -> + NCic.term DisambiguateTypes.codomain_item list) -> ?goal: int -> CicNotationPt.term Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + ((DisambiguateTypes.domain_item * NCic.term DisambiguateTypes.codomain_item) list * NCic.metasenv * (* new metasenv *) NCic.substitution * NCic.term) list * (* disambiguated term *) diff --git a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml index 328856a0f..b8cadbcbf 100644 --- a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml +++ b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml @@ -11,50 +11,23 @@ (* $Id$ *) -exception Ambiguous_input -exception DisambiguationError of - int * - ((Stdpp.location list * string * string) list * - (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - (Stdpp.location * string) Lazy.t * bool) list list - (** parameters are: option name, error message *) -type choose_uris_callback = id:string -> NUri.uri list -> NUri.uri list -type choose_interp_callback = - string -> int -> (Stdpp.location list * string * string) list list -> - int list - open Printf let debug = false;; let debug_print s = if debug then prerr_endline (Lazy.force s);; -let mono_uris_callback ~id = - if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true - "matita.auto_disambiguation" - then function l -> l - else raise Ambiguous_input - -let mono_interp_callback _ _ _ = raise Ambiguous_input - -let _choose_uris_callback = ref mono_uris_callback -let _choose_interp_callback = ref mono_interp_callback -let set_choose_uris_callback f = _choose_uris_callback := f -let set_choose_interp_callback f = _choose_interp_callback := f - module Callbacks = struct let interactive_user_uri_choice ~selection_mode ?ok ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = - !_choose_uris_callback ~id uris + assert false let interactive_interpretation_choice interp = - !_choose_interp_callback interp + assert false - let input_or_locate_uri ~(title:string) ?id () = None - (* Zack: I try to avoid using this callback. I therefore assume that - * the presence of an identifier that can't be resolved via "locate" - * query is a syntax error *) + let input_or_locate_uri ~(title:string) ?id () = + assert false end module Disambiguator = NDisambiguate.Make (Callbacks) @@ -63,8 +36,8 @@ let only_one_pass = ref false;; let disambiguate_thing ~aliases ~universe ~(f:?fresh_instances:bool -> - aliases:DisambiguateTypes.environment -> - universe:DisambiguateTypes.multiple_environment option -> + aliases:NCic.term DisambiguateTypes.environment -> + universe:NCic.term DisambiguateTypes.multiple_environment option -> 'a -> 'b) ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b) ~(drop_aliases_and_clear_diff: 'b -> 'b) @@ -106,7 +79,7 @@ let disambiguate_thing ~aliases ~universe (try set_aliases pass (try_pass pass) with Disambiguate.NoWellTypedInterpretation (offset,newerrors) -> - raise (DisambiguationError (offset, errors @ [newerrors]))) + raise (GrafiteDisambiguator.DisambiguationError (offset, errors @ [newerrors]))) | hd :: tl -> (try set_aliases hd (try_pass hd) @@ -126,11 +99,11 @@ let disambiguate_thing ~aliases ~universe type disambiguator_thing = { do_it : 'a 'b. - aliases:DisambiguateTypes.environment -> - universe:DisambiguateTypes.multiple_environment option -> + aliases:NCic.term DisambiguateTypes.environment -> + universe:NCic.term DisambiguateTypes.multiple_environment option -> f:(?fresh_instances:bool -> - aliases:DisambiguateTypes.environment -> - universe:DisambiguateTypes.multiple_environment option -> + aliases:NCic.term DisambiguateTypes.environment -> + universe:NCic.term DisambiguateTypes.multiple_environment option -> 'a -> 'b * bool) -> drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) -> drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool @@ -177,27 +150,27 @@ let drop_aliases ?(minimize_instances=false) (choices, user_asked) = in aux d in - (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices), + (List.map (fun (d, a, b, c) -> minimize d, a, b, c) choices), user_asked let drop_aliases_and_clear_diff (choices, user_asked) = - (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices), + (List.map (fun (_, a, b, c) -> [], a, b, c) choices), user_asked -let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph +let disambiguate_term ~context ~metasenv ~subst ?goal ~aliases ~universe term = - assert (fresh_instances = None); let f = - Disambiguator.disambiguate_term ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph + Disambiguator.disambiguate_term ~context ~metasenv ~subst ?goal + ~lookup_in_library:(fun _ _ -> assert false) in disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff term -let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj = +let disambiguate_obj ~aliases ~universe ~uri obj = + assert false (* assert (fresh_instances = None); - let f = Disambiguator.disambiguate_obj ~dbd ~uri in + let f = Disambiguator.disambiguate_obj ~uri ~lookup_in_library:(fun _ _ -> assert false) in disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff obj - -let disambiguate_thing ~dbd = assert false + *) diff --git a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli index 2e47b4ffb..db9671cc4 100644 --- a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli +++ b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli @@ -11,35 +11,17 @@ (* $Id$ *) -exception Ambiguous_input -exception DisambiguationError of - int * - ((Stdpp.location list * string * string) list * - (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - (Stdpp.location * string) Lazy.t * bool) list list - (** parameters are: option name, error message *) -type choose_uris_callback = - id:string -> UriManager.uri list -> UriManager.uri list -type choose_interp_callback = - string -> int -> (Stdpp.location list * string * string) list list -> - int list - -val set_choose_uris_callback: choose_uris_callback -> unit -val set_choose_interp_callback: choose_interp_callback -> unit - val disambiguate_term : - ?fresh_instances:bool -> - dbd:HSql.dbd -> - context:NCic.context -> - metasenv:NCic.metasenv -> - subst:NCic.substitution -> - aliases:DisambiguateTypes.environment ->(* previous interpretation status *) - universe:DisambiguateTypes.multiple_environment option -> - ?goal: int -> - CicNotationPt.term Disambiguate.disambiguator_input -> - ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * - NCic.metasenv * (* new metasenv *) - NCic.substitution * - NCic.term) list * (* disambiguated term *) - bool - + context:NCic.context -> + metasenv:NCic.metasenv -> + subst:NCic.substitution -> + ?goal:int -> + aliases:NCic.term DisambiguateTypes.environment -> + universe:NCic.term DisambiguateTypes.multiple_environment option -> + CicNotationPt.term Disambiguate.disambiguator_input -> + ((DisambiguateTypes.domain_item * + NCic.term DisambiguateTypes.codomain_item) list * + NCic.metasenv * (* new metasenv *) + NCic.substitution * + NCic.term) list * (* disambiguated term *) + bool