almost done

diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nDisambiguate.ml
index 5313ee20f809433c6278bc37cec2da074772d72b..f4213bc3086b0c83603d1389b92ffe455c70eb44 100644 (file)
--- 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 a61d37653990b25f82039e8af7d254a4c28dfc33..ae1b16f59560e745145d36009e0b22641f3e687f 100644 (file)
--- 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 328856a0f0565bcb3d71d2863e37af60826228fe..b8cadbcbf53c738835acec46dfd7148bee4bcaf1 100644 (file)
--- 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 2e47b4ffb829b412ba3afb299d4a660ca9d3935c..db9671cc4d10b7c34f27b1f1897d53eb33ad5b88 100644 (file)
--- 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