]> matita.cs.unibo.it Git - helm.git/blob - disambiguate.ml
ad8028d165a73f4ba5e6923a27cc8daf8cc6e8f1
[helm.git] / disambiguate.ml
1 (* Copyright (C) 2004, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 open Printf
29
30 open DisambiguateTypes
31 open UriManager
32
33 module Ast = CicNotationPt
34
35 (* the integer is an offset to be added to each location *)
36 exception NoWellTypedInterpretation of
37  int *
38  ((Stdpp.location list * string * string) list *
39   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
40   Stdpp.location option * string Lazy.t * bool) list
41 exception PathNotWellFormed
42
43   (** raised when an environment is not enough informative to decide *)
44 exception Try_again of string Lazy.t
45
46 type aliases = bool * DisambiguateTypes.environment
47 type 'a disambiguator_input = string * int * 'a
48
49 type domain = domain_tree list
50 and domain_tree = Node of Stdpp.location list * domain_item * domain
51
52 let rec string_of_domain =
53  function
54     [] -> ""
55   | Node (_,domain_item,l)::tl ->
56      DisambiguateTypes.string_of_domain_item domain_item ^
57       " [ " ^ string_of_domain l ^ " ] " ^ string_of_domain tl
58
59 let rec filter_map_domain f =
60  function
61     [] -> []
62   | Node (locs,domain_item,l)::tl ->
63      match f locs domain_item with
64         None -> filter_map_domain f l @ filter_map_domain f tl
65       | Some res -> res :: filter_map_domain f l @ filter_map_domain f tl
66
67 let rec map_domain f =
68  function
69     [] -> []
70   | Node (locs,domain_item,l)::tl ->
71      f locs domain_item :: map_domain f l @ map_domain f tl
72
73 let uniq_domain dom =
74  let rec aux seen =
75   function
76      [] -> seen,[]
77    | Node (locs,domain_item,l)::tl ->
78       if List.mem domain_item seen then
79        let seen,l = aux seen l in
80        let seen,tl = aux seen tl in
81         seen, l @ tl
82       else
83        let seen,l = aux (domain_item::seen) l in
84        let seen,tl = aux seen tl in
85         seen, Node (locs,domain_item,l)::tl
86  in
87   snd (aux [] dom)
88
89 let debug = false
90 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
91
92 (*
93   (** print benchmark information *)
94 let benchmark = true
95 let max_refinements = ref 0       (* benchmarking is not thread safe *)
96 let actual_refinements = ref 0
97 let domain_size = ref 0
98 let choices_avg = ref 0.
99 *)
100
101 let descr_of_domain_item = function
102  | Id s -> s
103  | Symbol (s, _) -> s
104  | Num i -> string_of_int i
105
106 type 'a test_result =
107   | Ok of 'a * Cic.metasenv
108   | Ko of Stdpp.location option * string Lazy.t
109   | Uncertain of Stdpp.location option * string Lazy.t
110
111 let refine_term metasenv context uri term ugraph ~localization_tbl =
112 (*   if benchmark then incr actual_refinements; *)
113   assert (uri=None);
114     debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
115     try
116       let term', _, metasenv',ugraph1 = 
117         CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
118         (Ok (term', metasenv')),ugraph1
119     with
120      exn ->
121       let rec process_exn loc =
122        function
123           HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
124         | CicRefine.Uncertain msg ->
125             debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
126             Uncertain (loc,msg),ugraph
127         | CicRefine.RefineFailure msg ->
128             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
129               (CicPp.ppterm term) (Lazy.force msg)));
130             Ko (loc,msg),ugraph
131        | exn -> raise exn
132       in
133        process_exn None exn
134
135 let refine_obj metasenv context uri obj ugraph ~localization_tbl =
136  assert (context = []);
137    debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
138    try
139      let obj', metasenv,ugraph =
140       CicRefine.typecheck metasenv uri obj ~localization_tbl
141      in
142        (Ok (obj', metasenv)),ugraph
143    with
144      exn ->
145       let rec process_exn loc =
146        function
147           HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
148         | CicRefine.Uncertain msg ->
149             debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
150             Uncertain (loc,msg),ugraph
151         | CicRefine.RefineFailure msg ->
152             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
153               (CicPp.ppobj obj) (Lazy.force msg))) ;
154             Ko (loc,msg),ugraph
155        | exn -> raise exn
156       in
157        process_exn None exn
158
159 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
160   try
161     snd (Environment.find item env) env num args
162   with Not_found -> 
163     failwith ("Domain item not found: " ^ 
164       (DisambiguateTypes.string_of_domain_item item))
165
166   (* TODO move it to Cic *)
167 let find_in_context name context =
168   let rec aux acc = function
169     | [] -> raise Not_found
170     | Cic.Name hd :: tl when hd = name -> acc
171     | _ :: tl ->  aux (acc + 1) tl
172   in
173   aux 1 context
174
175 let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~uri ~is_path ast
176      ~localization_tbl
177 =
178   (* create_dummy_ids shouldbe used only for interpretating patterns *)
179   assert (uri = None);
180   let rec aux ~localize loc (context: Cic.name list) = function
181     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
182         let res = aux ~localize loc context term in
183          if localize then Cic.CicHash.add localization_tbl res loc;
184          res
185     | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
186     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
187         let cic_args = List.map (aux ~localize loc context) args in
188         resolve env (Symbol (symb, i)) ~args:cic_args ()
189     | CicNotationPt.Appl terms ->
190        Cic.Appl (List.map (aux ~localize loc context) terms)
191     | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
192         let cic_type = aux_option ~localize loc context (Some `Type) typ in
193         let cic_name = CicNotationUtil.cic_name_of_name var in
194         let cic_body = aux ~localize loc (cic_name :: context) body in
195         (match binder_kind with
196         | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
197         | `Pi
198         | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
199         | `Exists ->
200             resolve env (Symbol ("exists", 0))
201               ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
202     | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
203         let cic_term = aux ~localize loc context term in
204         let cic_outtype = aux_option ~localize loc context None outtype in
205         let do_branch ((head, _, args), term) =
206          let rec do_branch' context = function
207            | [] -> aux ~localize loc context term
208            | (name, typ) :: tl ->
209                let cic_name = CicNotationUtil.cic_name_of_name name in
210                let cic_body = do_branch' (cic_name :: context) tl in
211                let typ =
212                  match typ with
213                  | None -> Cic.Implicit (Some `Type)
214                  | Some typ -> aux ~localize loc context typ
215                in
216                Cic.Lambda (cic_name, typ, cic_body)
217          in
218           do_branch' context args
219         in
220         let indtype_uri, indtype_no =
221           if create_dummy_ids then
222             (UriManager.uri_of_string "cic:/fake_indty.con", 0)
223           else
224           match indty_ident with
225           | Some (indty_ident, _) ->
226              (match resolve env (Id indty_ident) () with
227               | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
228               | Cic.Implicit _ ->
229                  raise (Try_again (lazy "The type of the term to be matched
230                   is still unknown"))
231               | _ ->
232                 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
233           | None ->
234               let rec fst_constructor =
235                 function
236                    (Ast.Pattern (head, _, _), _) :: _ -> head
237                  | (Ast.Wildcard, _) :: tl -> fst_constructor tl
238                  | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))
239               in
240               (match resolve env (Id (fst_constructor branches)) () with
241               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
242                   (indtype_uri, indtype_no)
243               | Cic.Implicit _ ->
244                  raise (Try_again (lazy "The type of the term to be matched
245                   is still unknown"))
246               | _ ->
247                 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
248         in
249         let branches =
250          if create_dummy_ids then
251           List.map
252            (function
253                Ast.Wildcard,term -> ("wildcard",None,[]), term
254              | Ast.Pattern _,_ ->
255                 raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
256            ) branches
257          else
258          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
259             Cic.InductiveDefinition (il,_,leftsno,_) ->
260              let _,_,_,cl =
261               try
262                List.nth il indtype_no
263               with _ -> assert false
264              in
265               let rec count_prod t =
266                 match CicReduction.whd [] t with
267                     Cic.Prod (_, _, t) -> 1 + (count_prod t)
268                   | _ -> 0 
269               in 
270               let rec sort branches cl =
271                match cl with
272                   [] ->
273                    let rec analyze unused unrecognized useless =
274                     function
275                        [] ->
276                         if unrecognized != [] then
277                          raise (Invalid_choice
278                           (Some loc,
279                            lazy
280                             ("Unrecognized constructors: " ^
281                              String.concat " " unrecognized)))
282                         else if useless > 0 then
283                          raise (Invalid_choice
284                           (Some loc,
285                            lazy
286                             ("The last " ^ string_of_int useless ^
287                              "case" ^ if useless > 1 then "s are" else " is" ^
288                              " unused")))
289                         else
290                          []
291                      | (Ast.Wildcard,_)::tl when not unused ->
292                          analyze true unrecognized useless tl
293                      | (Ast.Pattern (head,_,_),_)::tl when not unused ->
294                          analyze unused (head::unrecognized) useless tl
295                      | _::tl -> analyze unused unrecognized (useless + 1) tl
296                    in
297                     analyze false [] 0 branches
298                 | (name,ty)::cltl ->
299                    let rec find_and_remove =
300                     function
301                        [] ->
302                         raise
303                          (Invalid_choice
304                           (Some loc, lazy ("Missing case: " ^ name)))
305                      | ((Ast.Wildcard, _) as branch :: _) as branches ->
306                          branch, branches
307                      | (Ast.Pattern (name',_,_),_) as branch :: tl
308                         when name = name' ->
309                          branch,tl
310                      | branch::tl ->
311                         let found,rest = find_and_remove tl in
312                          found, branch::rest
313                    in
314                     let branch,tl = find_and_remove branches in
315                     match branch with
316                        Ast.Pattern (name,y,args),term ->
317                         if List.length args = count_prod ty - leftsno then
318                          ((name,y,args),term)::sort tl cltl
319                         else
320                          raise
321                           (Invalid_choice
322                            (Some loc,
323                              lazy ("Wrong number of arguments for " ^ name)))
324                      | Ast.Wildcard,term ->
325                         let rec mk_lambdas =
326                          function
327                             0 -> term
328                           | n ->
329                              CicNotationPt.Binder
330                               (`Lambda, (CicNotationPt.Ident ("_", None), None),
331                                 mk_lambdas (n - 1))
332                         in
333                          (("wildcard",None,[]),
334                           mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
335               in
336                sort branches cl
337           | _ -> assert false
338         in
339         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
340           (List.map do_branch branches))
341     | CicNotationPt.Cast (t1, t2) ->
342         let cic_t1 = aux ~localize loc context t1 in
343         let cic_t2 = aux ~localize loc context t2 in
344         Cic.Cast (cic_t1, cic_t2)
345     | CicNotationPt.LetIn ((name, typ), def, body) ->
346         let cic_def = aux ~localize loc context def in
347         let cic_name = CicNotationUtil.cic_name_of_name name in
348         let cic_typ =
349           match typ with
350           | None -> Cic.Implicit (Some `Type)
351           | Some t -> aux ~localize loc context t
352         in
353         let cic_body = aux ~localize loc (cic_name :: context) body in
354         Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
355     | CicNotationPt.LetRec (kind, defs, body) ->
356         let context' =
357           List.fold_left
358             (fun acc (_, (name, _), _, _) ->
359               CicNotationUtil.cic_name_of_name name :: acc)
360             context defs
361         in
362         let cic_body =
363          let unlocalized_body = aux ~localize:false loc context' body in
364          match unlocalized_body with
365             Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
366           | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
367              (try
368                let l' =
369                 List.map
370                  (function t ->
371                    let t',subst,metasenv =
372                     CicMetaSubst.delift_rels [] [] (List.length defs) t
373                    in
374                     assert (subst=[]);
375                     assert (metasenv=[]);
376                     t') l
377                in
378                 (* We can avoid the LetIn. But maybe we need to recompute l'
379                    so that it is localized *)
380                 if localize then
381                  match body with
382                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
383                      let l' = List.map (aux ~localize loc context) l in
384                       `AvoidLetIn (n,l')
385                   | _ -> assert false
386                 else
387                  `AvoidLetIn (n,l')
388               with
389                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
390                 if localize then
391                  `AddLetIn (aux ~localize loc context' body)
392                 else
393                  `AddLetIn unlocalized_body)
394           | _ ->
395              if localize then
396               `AddLetIn (aux ~localize loc context' body)
397              else
398               `AddLetIn unlocalized_body
399         in
400         let inductiveFuns =
401           List.map
402             (fun (params, (name, typ), body, decr_idx) ->
403               let add_binders kind t =
404                List.fold_right
405                 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
406               in
407               let cic_body =
408                aux ~localize loc context' (add_binders `Lambda body) in
409               let cic_type =
410                aux_option ~localize loc context (Some `Type)
411                 (HExtlib.map_option (add_binders `Pi) typ) in
412               let name =
413                 match CicNotationUtil.cic_name_of_name name with
414                 | Cic.Anonymous ->
415                     CicNotationPt.fail loc
416                       "Recursive functions cannot be anonymous"
417                 | Cic.Name name -> name
418               in
419               (name, decr_idx, cic_type, cic_body))
420             defs
421         in
422         let fix_or_cofix n =
423          match kind with
424             `Inductive -> Cic.Fix (n,inductiveFuns)
425           | `CoInductive ->
426               let coinductiveFuns =
427                 List.map
428                  (fun (name, _, typ, body) -> name, typ, body)
429                  inductiveFuns
430               in
431                Cic.CoFix (n,coinductiveFuns)
432         in
433          let counter = ref ~-1 in
434          let build_term funs (var,_,ty,_) t =
435           incr counter;
436           Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
437          in
438           (match cic_body with
439               `AvoidLetInNoAppl n ->
440                 let n' = List.length inductiveFuns - n in
441                  fix_or_cofix n'
442             | `AvoidLetIn (n,l) ->
443                 let n' = List.length inductiveFuns - n in
444                  Cic.Appl (fix_or_cofix n'::l)
445             | `AddLetIn cic_body ->         
446                 List.fold_right (build_term inductiveFuns) inductiveFuns
447                  cic_body)
448     | CicNotationPt.Ident _
449     | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
450     | CicNotationPt.Ident (name, subst)
451     | CicNotationPt.Uri (name, subst) as ast ->
452         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
453         (try
454           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
455           let index = find_in_context name context in
456           if subst <> None then
457             CicNotationPt.fail loc "Explicit substitutions not allowed here";
458           Cic.Rel index
459         with Not_found ->
460           let cic =
461             if is_uri ast then  (* we have the URI, build the term out of it *)
462               try
463                 CicUtil.term_of_uri (UriManager.uri_of_string name)
464               with UriManager.IllFormedUri _ ->
465                 CicNotationPt.fail loc "Ill formed URI"
466             else
467               resolve env (Id name) ()
468           in
469           let mk_subst uris =
470             let ids_to_uris =
471               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
472             in
473             (match subst with
474             | Some subst ->
475                 List.map
476                   (fun (s, term) ->
477                     (try
478                       List.assoc s ids_to_uris, aux ~localize loc context term
479                      with Not_found ->
480                        raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
481                   subst
482             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
483           in
484           (try 
485             match cic with
486             | Cic.Const (uri, []) ->
487                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
488                 let uris = CicUtil.params_of_obj o in
489                 Cic.Const (uri, mk_subst uris)
490             | Cic.Var (uri, []) ->
491                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
492                 let uris = CicUtil.params_of_obj o in
493                 Cic.Var (uri, mk_subst uris)
494             | Cic.MutInd (uri, i, []) ->
495                (try
496                  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
497                  let uris = CicUtil.params_of_obj o in
498                  Cic.MutInd (uri, i, mk_subst uris)
499                 with
500                  CicEnvironment.Object_not_found _ ->
501                   (* if we are here it is probably the case that during the
502                      definition of a mutual inductive type we have met an
503                      occurrence of the type in one of its constructors.
504                      However, the inductive type is not yet in the environment
505                   *)
506                   (*here the explicit_named_substituion is assumed to be of length 0 *)
507                   Cic.MutInd (uri,i,[]))
508             | Cic.MutConstruct (uri, i, j, []) ->
509                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
510                 let uris = CicUtil.params_of_obj o in
511                 Cic.MutConstruct (uri, i, j, mk_subst uris)
512             | Cic.Meta _ | Cic.Implicit _ as t ->
513 (*
514                 debug_print (lazy (sprintf
515                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
516                   (CicPp.ppterm t)
517                   (String.concat "; "
518                     (List.map
519                       (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
520                       subst))));
521 *)
522                 t
523             | _ ->
524               raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
525            with 
526              CicEnvironment.CircularDependency _ -> 
527                raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
528     | CicNotationPt.Implicit -> Cic.Implicit None
529     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
530     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
531     | CicNotationPt.Meta (index, subst) ->
532         let cic_subst =
533           List.map
534             (function
535                 None -> None
536               | Some term -> Some (aux ~localize loc context term))
537             subst
538         in
539         Cic.Meta (index, cic_subst)
540     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
541     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
542     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
543     | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
544     | CicNotationPt.Symbol (symbol, instance) ->
545         resolve env (Symbol (symbol, instance)) ()
546     | _ -> assert false (* god bless Bologna *)
547   and aux_option ~localize loc (context: Cic.name list) annotation = function
548     | None -> Cic.Implicit annotation
549     | Some term -> aux ~localize loc context term
550   in
551    aux ~localize:true HExtlib.dummy_floc context ast
552
553 let interpretate_path ~context path =
554  let localization_tbl = Cic.CicHash.create 23 in
555   (* here we are throwing away useful localization informations!!! *)
556   fst (
557    interpretate_term ~create_dummy_ids:true 
558     ~context ~env:Environment.empty ~uri:None ~is_path:true
559     path ~localization_tbl, localization_tbl)
560
561 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
562  assert (context = []);
563  assert (is_path = false);
564  let interpretate_term = interpretate_term ~localization_tbl in
565  match obj with
566   | CicNotationPt.Inductive (params,tyl) ->
567      let uri = match uri with Some uri -> uri | None -> assert false in
568      let context,params =
569       let context,res =
570        List.fold_left
571         (fun (context,res) (name,t) ->
572           let t =
573            match t with
574               None -> CicNotationPt.Implicit
575             | Some t -> t in
576           let name = CicNotationUtil.cic_name_of_name name in
577            name::context,(name, interpretate_term context env None false t)::res
578         ) ([],[]) params
579       in
580        context,List.rev res in
581      let add_params =
582       List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
583      let name_to_uris =
584       snd (
585        List.fold_left
586         (*here the explicit_named_substituion is assumed to be of length 0 *)
587         (fun (i,res) (name,_,_,_) ->
588           i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
589         ) (0,[]) tyl) in
590      let con_env = DisambiguateTypes.env_of_list name_to_uris env in
591      let tyl =
592       List.map
593        (fun (name,b,ty,cl) ->
594          let ty' = add_params (interpretate_term context env None false ty) in
595          let cl' =
596           List.map
597            (fun (name,ty) ->
598              let ty' =
599               add_params (interpretate_term context con_env None false ty)
600              in
601               name,ty'
602            ) cl
603          in
604           name,b,ty',cl'
605        ) tyl
606      in
607       Cic.InductiveDefinition (tyl,[],List.length params,[])
608   | CicNotationPt.Record (params,name,ty,fields) ->
609      let uri = match uri with Some uri -> uri | None -> assert false in
610      let context,params =
611       let context,res =
612        List.fold_left
613         (fun (context,res) (name,t) ->
614           let t =
615            match t with
616               None -> CicNotationPt.Implicit
617             | Some t -> t in
618           let name = CicNotationUtil.cic_name_of_name name in
619            name::context,(name, interpretate_term context env None false t)::res
620         ) ([],[]) params
621       in
622        context,List.rev res in
623      let add_params =
624       List.fold_right
625        (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
626      let ty' = add_params (interpretate_term context env None false ty) in
627      let fields' =
628       snd (
629        List.fold_left
630         (fun (context,res) (name,ty,_coercion,arity) ->
631           let context' = Cic.Name name :: context in
632            context',(name,interpretate_term context env None false ty)::res
633         ) (context,[]) fields) in
634      let concl =
635       (*here the explicit_named_substituion is assumed to be of length 0 *)
636       let mutind = Cic.MutInd (uri,0,[]) in
637       if params = [] then mutind
638       else
639        Cic.Appl
640         (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
641      let con =
642       List.fold_left
643        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
644        concl fields' in
645      let con' = add_params con in
646      let tyl = [name,true,ty',["mk_" ^ name,con']] in
647      let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
648       Cic.InductiveDefinition
649        (tyl,[],List.length params,[`Class (`Record field_names)])
650   | CicNotationPt.Theorem (flavour, name, ty, bo) ->
651      let attrs = [`Flavour flavour] in
652      let ty' = interpretate_term [] env None false ty in
653      (match bo,flavour with
654         None,`Axiom ->
655          Cic.Constant (name,None,ty',[],attrs)
656       | Some bo,`Axiom -> assert false
657       | None,_ ->
658          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
659       | Some bo,_ ->
660          let bo' = Some (interpretate_term [] env None false bo) in
661           Cic.Constant (name,bo',ty',[],attrs))
662           
663 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
664   | Ast.AttributedTerm (`Loc loc, term) ->
665      domain_of_term ~loc ~context term
666   | Ast.AttributedTerm (_, term) ->
667       domain_of_term ~loc ~context term
668   | Ast.Symbol (symbol, instance) ->
669       [ Node ([loc], Symbol (symbol, instance), []) ]
670       (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
671   | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
672   | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
673      ->
674       let args_dom =
675         List.fold_right
676           (fun term acc -> domain_of_term ~loc ~context term @ acc)
677           args [] in
678       let loc =
679        match hd with
680           Ast.AttributedTerm (`Loc loc,_)  -> loc
681         | _ -> loc
682       in
683        [ Node ([loc], Symbol (symbol, instance), args_dom) ]
684   | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
685   | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
686       let args_dom =
687         List.fold_right
688           (fun term acc -> domain_of_term ~loc ~context term @ acc)
689           args [] in
690       let loc =
691        match hd with
692           Ast.AttributedTerm (`Loc loc,_)  -> loc
693         | _ -> loc
694       in
695       (try
696         (* the next line can raise Not_found *)
697         ignore(find_in_context name context);
698         if subst <> None then
699           Ast.fail loc "Explicit substitutions not allowed here"
700         else
701           args_dom
702       with Not_found ->
703         (match subst with
704         | None -> [ Node ([loc], Id name, args_dom) ]
705         | Some subst ->
706             let terms =
707               List.fold_left
708                 (fun dom (_, term) ->
709                   let dom' = domain_of_term ~loc ~context term in
710                   dom @ dom')
711                 [] subst in
712             [ Node ([loc], Id name, terms @ args_dom) ]))
713   | Ast.Appl terms ->
714       List.fold_right
715         (fun term acc -> domain_of_term ~loc ~context term @ acc)
716         terms []
717   | Ast.Binder (kind, (var, typ), body) ->
718       let type_dom = domain_of_term_option ~loc ~context typ in
719       let body_dom =
720         domain_of_term ~loc
721           ~context:(CicNotationUtil.cic_name_of_name var :: context) body in
722       (match kind with
723       | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
724       | _ -> type_dom @ body_dom)
725   | Ast.Case (term, indty_ident, outtype, branches) ->
726       let term_dom = domain_of_term ~loc ~context term in
727       let outtype_dom = domain_of_term_option ~loc ~context outtype in
728       let rec get_first_constructor = function
729         | [] -> []
730         | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
731         | _ :: tl -> get_first_constructor tl in
732       let do_branch =
733        function
734           Ast.Pattern (head, _, args), term ->
735            let (term_context, args_domain) =
736              List.fold_left
737                (fun (cont, dom) (name, typ) ->
738                  (CicNotationUtil.cic_name_of_name name :: cont,
739                   (match typ with
740                   | None -> dom
741                   | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
742                (context, []) args
743            in
744             domain_of_term ~loc ~context:term_context term @ args_domain
745         | Ast.Wildcard, term ->
746             domain_of_term ~loc ~context term
747       in
748       let branches_dom =
749         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
750       (match indty_ident with
751        | None -> get_first_constructor branches
752        | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
753       @ term_dom @ outtype_dom @ branches_dom
754   | Ast.Cast (term, ty) ->
755       let term_dom = domain_of_term ~loc ~context term in
756       let ty_dom = domain_of_term ~loc ~context ty in
757       term_dom @ ty_dom
758   | Ast.LetIn ((var, typ), body, where) ->
759       let body_dom = domain_of_term ~loc ~context body in
760       let type_dom = domain_of_term_option ~loc ~context typ in
761       let where_dom =
762         domain_of_term ~loc
763           ~context:(CicNotationUtil.cic_name_of_name var :: context) where in
764       body_dom @ type_dom @ where_dom
765   | Ast.LetRec (kind, defs, where) ->
766       let add_defs context =
767         List.fold_left
768           (fun acc (_, (var, _), _, _) ->
769             CicNotationUtil.cic_name_of_name var :: acc
770           ) context defs in
771       let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
772       let defs_dom =
773         List.fold_left
774           (fun dom (params, (_, typ), body, _) ->
775             let context' =
776              add_defs
777               (List.fold_left
778                 (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
779                 context params)
780             in
781             List.rev
782              (snd
783                (List.fold_left
784                 (fun (context,res) (var,ty) ->
785                   CicNotationUtil.cic_name_of_name var :: context,
786                   domain_of_term_option ~loc ~context ty @ res)
787                 (add_defs context,[]) params))
788             @ domain_of_term_option ~loc ~context:context' typ
789             @ domain_of_term ~loc ~context:context' body
790           ) [] defs
791       in
792       defs_dom @ where_dom
793   | Ast.Ident (name, subst) ->
794       (try
795         (* the next line can raise Not_found *)
796         ignore(find_in_context name context);
797         if subst <> None then
798           Ast.fail loc "Explicit substitutions not allowed here"
799         else
800           []
801       with Not_found ->
802         (match subst with
803         | None -> [ Node ([loc], Id name, []) ]
804         | Some subst ->
805             let terms =
806               List.fold_left
807                 (fun dom (_, term) ->
808                   let dom' = domain_of_term ~loc ~context term in
809                   dom @ dom')
810                 [] subst in
811             [ Node ([loc], Id name, terms) ]))
812   | Ast.Uri _ -> []
813   | Ast.Implicit -> []
814   | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
815   | Ast.Meta (index, local_context) ->
816       List.fold_left
817        (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
818        [] local_context
819   | Ast.Sort _ -> []
820   | Ast.UserInput
821   | Ast.Literal _
822   | Ast.Layout _
823   | Ast.Magic _
824   | Ast.Variable _ -> assert false
825
826 and domain_of_term_option ~loc ~context = function
827   | None -> []
828   | Some t -> domain_of_term ~loc ~context t
829
830 let domain_of_term ~context term = 
831  uniq_domain (domain_of_term ~context term)
832
833 let domain_of_obj ~context ast =
834  assert (context = []);
835   match ast with
836    | Ast.Theorem (_,_,ty,bo) ->
837       domain_of_term [] ty
838       @ (match bo with
839           None -> []
840         | Some bo -> domain_of_term [] bo)
841    | Ast.Inductive (params,tyl) ->
842       let context, dom = 
843        List.fold_left
844         (fun (context, dom) (var, ty) ->
845           let context' = CicNotationUtil.cic_name_of_name var :: context in
846           match ty with
847              None -> context', dom
848            | Some ty -> context', dom @ domain_of_term context ty
849         ) ([], []) params in
850       let context_w_types =
851         List.rev_map
852           (fun (var, _, _, _) -> Cic.Name var) tyl
853         @ context in
854       dom
855       @ List.flatten (
856          List.map
857           (fun (_,_,ty,cl) ->
858             domain_of_term context ty
859             @ List.flatten (
860                List.map
861                 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
862                 tyl)
863    | CicNotationPt.Record (params,var,ty,fields) ->
864       let context, dom = 
865        List.fold_left
866         (fun (context, dom) (var, ty) ->
867           let context' = CicNotationUtil.cic_name_of_name var :: context in
868           match ty with
869              None -> context', dom
870            | Some ty -> context', dom @ domain_of_term context ty
871         ) ([], []) params in
872       let context_w_types = Cic.Name var :: context in
873       dom
874       @ domain_of_term context ty
875       @ snd
876          (List.fold_left
877           (fun (context,res) (name,ty,_,_) ->
878             Cic.Name name::context, res @ domain_of_term context ty
879           ) (context_w_types,[]) fields)
880
881 let domain_of_obj ~context obj = 
882  uniq_domain (domain_of_obj ~context obj)
883
884   (* dom1 \ dom2 *)
885 let domain_diff dom1 dom2 =
886 (* let domain_diff = Domain.diff *)
887   let is_in_dom2 elt =
888     List.exists
889      (function
890        | Symbol (symb, 0) ->
891           (match elt with
892               Symbol (symb',_) when symb = symb' -> true
893             | _ -> false)
894        | Num i ->
895           (match elt with
896               Num _ -> true
897             | _ -> false)
898        | item -> elt = item
899      ) dom2
900   in
901    let rec aux =
902     function
903        [] -> []
904      | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
905      | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
906    in
907     aux dom1
908
909 module type Disambiguator =
910 sig
911   val disambiguate_term :
912     ?fresh_instances:bool ->
913     dbd:HSql.dbd ->
914     context:Cic.context ->
915     metasenv:Cic.metasenv ->
916     ?initial_ugraph:CicUniv.universe_graph -> 
917     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
918     universe:DisambiguateTypes.multiple_environment option ->
919     CicNotationPt.term disambiguator_input ->
920     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
921      Cic.metasenv *                  (* new metasenv *)
922      Cic.term*
923      CicUniv.universe_graph) list *  (* disambiguated term *)
924     bool
925
926   val disambiguate_obj :
927     ?fresh_instances:bool ->
928     dbd:HSql.dbd ->
929     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
930     universe:DisambiguateTypes.multiple_environment option ->
931     uri:UriManager.uri option ->     (* required only for inductive types *)
932     CicNotationPt.term CicNotationPt.obj disambiguator_input ->
933     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
934      Cic.metasenv *                  (* new metasenv *)
935      Cic.obj *
936      CicUniv.universe_graph) list *  (* disambiguated obj *)
937     bool
938 end
939
940 module Make (C: Callbacks) =
941   struct
942     let choices_of_id dbd id =
943       let uris = Whelp.locate ~dbd id in
944       let uris =
945        match uris with
946         | [] ->
947            (match 
948              (C.input_or_locate_uri 
949                ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ()) 
950            with
951            | None -> []
952            | Some uri -> [uri])
953         | [uri] -> [uri]
954         | _ ->
955             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
956              ~ok:"Try selected." ~enable_button_for_non_vars:true
957              ~title:"Ambiguous input." ~id
958              ~msg: ("Ambiguous input \"" ^ id ^
959                 "\". Please, choose one or more interpretations:")
960              uris
961       in
962       List.map
963         (fun uri ->
964           (UriManager.string_of_uri uri,
965            let term =
966              try
967                CicUtil.term_of_uri uri
968              with exn ->
969                debug_print (lazy (UriManager.string_of_uri uri));
970                debug_print (lazy (Printexc.to_string exn));
971                assert false
972             in
973            fun _ _ _ -> term))
974         uris
975
976 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
977
978     let disambiguate_thing ~dbd ~context ~metasenv
979       ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
980       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
981       (thing_txt,thing_txt_prefix_len,thing)
982     =
983       debug_print (lazy "DISAMBIGUATE INPUT");
984       let disambiguate_context =  (* cic context -> disambiguate context *)
985         List.map
986           (function None -> Cic.Anonymous | Some (name, _) -> name)
987           context
988       in
989       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
990       let thing_dom = domain_of_thing ~context:disambiguate_context thing in
991       debug_print
992        (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
993 (*
994       debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
995         (DisambiguatePp.pp_environment aliases)));
996       debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
997         (match universe with None -> "None" | Some _ -> "Some _")));
998 *)
999       let current_dom =
1000         Environment.fold (fun item _ dom -> item :: dom) aliases [] in
1001       let todo_dom = domain_diff thing_dom current_dom in
1002       debug_print
1003        (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
1004       (* (2) lookup function for any item (Id/Symbol/Num) *)
1005       let lookup_choices =
1006         fun item ->
1007           let choices =
1008             let lookup_in_library () =
1009               match item with
1010               | Id id -> choices_of_id dbd id
1011               | Symbol (symb, _) ->
1012                  (try
1013                    List.map DisambiguateChoices.mk_choice
1014                     (TermAcicContent.lookup_interpretations symb)
1015                   with
1016                    TermAcicContent.Interpretation_not_found -> [])
1017               | Num instance ->
1018                   DisambiguateChoices.lookup_num_choices ()
1019             in
1020             match universe with
1021             | None -> lookup_in_library ()
1022             | Some e ->
1023                 (try
1024                   let item =
1025                     match item with
1026                     | Symbol (symb, _) -> Symbol (symb, 0)
1027                     | item -> item
1028                   in
1029                   Environment.find item e
1030                 with Not_found -> lookup_in_library ())
1031           in
1032           choices
1033       in
1034 (*
1035       (* <benchmark> *)
1036       let _ =
1037         if benchmark then begin
1038           let per_item_choices =
1039             List.map
1040               (fun dom_item ->
1041                 try
1042                   let len = List.length (lookup_choices dom_item) in
1043                   debug_print (lazy (sprintf "BENCHMARK %s: %d"
1044                     (string_of_domain_item dom_item) len));
1045                   len
1046                 with No_choices _ -> 0)
1047               thing_dom
1048           in
1049           max_refinements := List.fold_left ( * ) 1 per_item_choices;
1050           actual_refinements := 0;
1051           domain_size := List.length thing_dom;
1052           choices_avg :=
1053             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
1054         end
1055       in
1056       (* </benchmark> *)
1057 *)
1058
1059       (* (3) test an interpretation filling with meta uninterpreted identifiers
1060        *)
1061       let test_env aliases todo_dom ugraph = 
1062         let rec aux env = function
1063           | [] -> env
1064           | Node (_, item, l) :: tl ->
1065               let env =
1066                 Environment.add item
1067                  ("Implicit",
1068                    (match item with
1069                       | Id _ | Num _ ->
1070                           (fun _ _ _ -> Cic.Implicit (Some `Closed))
1071                       | Symbol _ -> (fun _ _ _ -> Cic.Implicit None)))
1072                  env in
1073               aux (aux env l) tl in
1074         let filled_env = aux aliases todo_dom in
1075         try
1076           let localization_tbl = Cic.CicHash.create 503 in
1077           let cic_thing =
1078             interpretate_thing ~context:disambiguate_context ~env:filled_env
1079              ~uri ~is_path:false thing ~localization_tbl
1080           in
1081 let foo () =
1082           let k,ugraph1 =
1083            refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
1084           in
1085             (k , ugraph1 )
1086 in refine_profiler.HExtlib.profile foo ()
1087         with
1088         | Try_again msg -> Uncertain (None,msg), ugraph
1089         | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph
1090       in
1091       (* (4) build all possible interpretations *)
1092       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
1093       (* aux returns triples Ok/Uncertain/Ko *)
1094       (* rem_dom is the concatenation of all the remainin domains *)
1095       let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ =
1096         debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
1097         match todo_dom with
1098         | [] ->
1099             assert (lookup_in_todo_dom = None);
1100             (match test_env aliases rem_dom base_univ with
1101             | Ok (thing, metasenv),new_univ -> 
1102                [ aliases, diff, metasenv, thing, new_univ ], [], []
1103             | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true]
1104             | Uncertain (loc,msg),new_univ ->
1105                [],[aliases,diff,loc,msg,new_univ],[])
1106         | Node (locs,item,inner_dom) :: remaining_dom ->
1107             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
1108              (string_of_domain_item item)));
1109             let choices =
1110              match lookup_in_todo_dom with
1111                 None -> lookup_choices item
1112               | Some choices -> choices in
1113             match choices with
1114                [] ->
1115                 [], [],
1116                  [aliases, diff, Some (List.hd locs),
1117                   lazy ("No choices for " ^ string_of_domain_item item),
1118                   true]
1119 (*
1120              | [codomain_item] ->
1121                  (* just one choice. We perform a one-step look-up and
1122                     if the next set of choices is also a singleton we
1123                     skip this refinement step *)
1124                  debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1125                  let new_env = Environment.add item codomain_item aliases in
1126                  let new_diff = (item,codomain_item)::diff in
1127                  let lookup_in_todo_dom,next_choice_is_single =
1128                   match remaining_dom with
1129                      [] -> None,false
1130                    | (_,he)::_ ->
1131                       let choices = lookup_choices he in
1132                        Some choices,List.length choices = 1
1133                  in
1134                   if next_choice_is_single then
1135                    aux new_env new_diff lookup_in_todo_dom remaining_dom
1136                     base_univ
1137                   else
1138                     (match test_env new_env remaining_dom base_univ with
1139                     | Ok (thing, metasenv),new_univ ->
1140                         (match remaining_dom with
1141                         | [] ->
1142                            [ new_env, new_diff, metasenv, thing, new_univ ], []
1143                         | _ ->
1144                            aux new_env new_diff lookup_in_todo_dom
1145                             remaining_dom new_univ)
1146                     | Uncertain (loc,msg),new_univ ->
1147                         (match remaining_dom with
1148                         | [] -> [], [new_env,new_diff,loc,msg,true]
1149                         | _ ->
1150                            aux new_env new_diff lookup_in_todo_dom
1151                             remaining_dom new_univ)
1152                     | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
1153 *)
1154              | _::_ ->
1155                  let mark_not_significant failures =
1156                    List.map
1157                     (fun (env, diff, loc, msg, _b) ->
1158                       env, diff, loc, msg, false)
1159                     failures in
1160                  let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
1161                   if ok_l <> [] || uncertain_l <> [] then
1162                    ok_l,uncertain_l,mark_not_significant error_l
1163                   else
1164                    outcome in
1165                let rec filter univ = function 
1166                 | [] -> [],[],[]
1167                 | codomain_item :: tl ->
1168                     debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1169                     let new_env = Environment.add item codomain_item aliases in
1170                     let new_diff = (item,codomain_item)::diff in
1171                     (match
1172                       test_env new_env (inner_dom@remaining_dom@rem_dom) univ
1173                      with
1174                     | Ok (thing, metasenv),new_univ ->
1175                         let res = 
1176                           (match inner_dom with
1177                           | [] ->
1178                              [new_env,new_diff,metasenv,thing,new_univ], [], []
1179                           | _ ->
1180                              aux new_env new_diff None inner_dom
1181                               (remaining_dom@rem_dom) new_univ
1182                           ) 
1183                         in
1184                          res @@ filter univ tl
1185                     | Uncertain (loc,msg),new_univ ->
1186                         let res =
1187                           (match inner_dom with
1188                           | [] -> [],[new_env,new_diff,loc,msg,new_univ],[]
1189                           | _ ->
1190                              aux new_env new_diff None inner_dom
1191                               (remaining_dom@rem_dom) new_univ
1192                           )
1193                         in
1194                          res @@ filter univ tl
1195                     | Ko (loc,msg),_ ->
1196                         let res = [],[],[new_env,new_diff,loc,msg,true] in
1197                          res @@ filter univ tl)
1198                in
1199                 let ok_l,uncertain_l,error_l =
1200                  classify_errors (filter base_univ choices)
1201                 in
1202                  let res_after_ok_l =
1203                   List.fold_right
1204                    (fun (env,diff,_,_,univ) res ->
1205                      aux env diff None remaining_dom rem_dom univ @@ res
1206                    ) ok_l ([],[],error_l)
1207                 in
1208                  List.fold_right
1209                   (fun (env,diff,_,_,univ) res ->
1210                     aux env diff None remaining_dom rem_dom univ @@ res
1211                   ) uncertain_l res_after_ok_l
1212       in
1213       let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
1214        match test_env aliases todo_dom base_univ with
1215         | Ok _,_
1216         | Uncertain _,_ ->
1217            aux aliases diff lookup_in_todo_dom todo_dom [] base_univ
1218         | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in
1219       let base_univ = initial_ugraph in
1220       try
1221         let res =
1222          match aux' aliases [] None todo_dom base_univ with
1223          | [],uncertain,errors ->
1224             let errors =
1225              List.map
1226               (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true)
1227               ) uncertain @ errors
1228             in
1229             let errors =
1230              List.map
1231               (fun (env,diff,loc,msg,significant) ->
1232                 let env' =
1233                  filter_map_domain
1234                    (fun locs domain_item ->
1235                      try
1236                       let description =
1237                        fst (Environment.find domain_item env)
1238                       in
1239                        Some (locs,descr_of_domain_item domain_item,description)
1240                      with
1241                       Not_found -> None)
1242                    thing_dom
1243                 in
1244                  env',diff,loc,msg,significant
1245               ) errors
1246             in
1247              raise (NoWellTypedInterpretation (0,errors))
1248          | [_,diff,metasenv,t,ugraph],_,_ ->
1249              debug_print (lazy "SINGLE INTERPRETATION");
1250              [diff,metasenv,t,ugraph], false
1251          | l,_,_ ->
1252              debug_print 
1253                (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
1254              let choices =
1255                List.map
1256                  (fun (env, _, _, _, _) ->
1257                    map_domain
1258                      (fun locs domain_item ->
1259                        let description =
1260                          fst (Environment.find domain_item env)
1261                        in
1262                        locs,descr_of_domain_item domain_item, description)
1263                      thing_dom)
1264                  l
1265              in
1266              let choosed = 
1267                C.interactive_interpretation_choice 
1268                  thing_txt thing_txt_prefix_len choices 
1269              in
1270              (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
1271               true
1272         in
1273          res
1274      with
1275       CicEnvironment.CircularDependency s -> 
1276         failwith "Disambiguate: circular dependency"
1277
1278     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
1279       ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe 
1280       (text,prefix_len,term)
1281     =
1282       let term =
1283         if fresh_instances then CicNotationUtil.freshen_term term else term
1284       in
1285       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
1286         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
1287         ~domain_of_thing:domain_of_term
1288         ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
1289         ~refine_thing:refine_term (text,prefix_len,term)
1290
1291     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
1292      (text,prefix_len,obj)
1293     =
1294       let obj =
1295         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
1296       in
1297       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
1298         ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
1299         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
1300         (text,prefix_len,obj)
1301   end
1302