]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_disambiguation/disambiguate.ml
...
[helm.git] / helm / software / components / cic_disambiguation / 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,'m) test_result =
107   | Ok of 'a * 'm
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 ~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 = 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                      (* since we avoid the letin, the context has no
384                       * recfuns in it *)
385                      let l' = List.map (aux ~localize loc context) l in
386                       `AvoidLetIn (n,l')
387                   | _ -> assert false
388                 else
389                  `AvoidLetIn (n,l')
390               with
391                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
392                 if localize then
393                  `AddLetIn (aux ~localize loc context' body)
394                 else
395                  `AddLetIn unlocalized_body)
396           | _ ->
397              if localize then
398               `AddLetIn (aux ~localize loc context' body)
399              else
400               `AddLetIn unlocalized_body
401         in
402         let inductiveFuns =
403           List.map
404             (fun (params, (name, typ), body, decr_idx) ->
405               let add_binders kind t =
406                List.fold_right
407                 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
408               in
409               let cic_body =
410                aux ~localize loc context' (add_binders `Lambda body) in
411               let cic_type =
412                aux_option ~localize loc context (Some `Type)
413                 (HExtlib.map_option (add_binders `Pi) typ) in
414               let name =
415                 match CicNotationUtil.cic_name_of_name name with
416                 | Cic.Anonymous ->
417                     CicNotationPt.fail loc
418                       "Recursive functions cannot be anonymous"
419                 | Cic.Name name -> name
420               in
421               (name, decr_idx, cic_type, cic_body))
422             defs
423         in
424         let fix_or_cofix n =
425          match kind with
426             `Inductive -> Cic.Fix (n,inductiveFuns)
427           | `CoInductive ->
428               let coinductiveFuns =
429                 List.map
430                  (fun (name, _, typ, body) -> name, typ, body)
431                  inductiveFuns
432               in
433                Cic.CoFix (n,coinductiveFuns)
434         in
435          let counter = ref ~-1 in
436          let build_term funs (var,_,ty,_) t =
437           incr counter;
438           Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
439          in
440           (match cic_body with
441               `AvoidLetInNoAppl n ->
442                 let n' = List.length inductiveFuns - n in
443                  fix_or_cofix n'
444             | `AvoidLetIn (n,l) ->
445                 let n' = List.length inductiveFuns - n in
446                  Cic.Appl (fix_or_cofix n'::l)
447             | `AddLetIn cic_body ->         
448                 List.fold_right (build_term inductiveFuns) inductiveFuns
449                  cic_body)
450     | CicNotationPt.Ident _
451     | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
452     | CicNotationPt.Ident (name, subst)
453     | CicNotationPt.Uri (name, subst) as ast ->
454         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
455         (try
456           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
457           let index = find_in_context name context in
458           if subst <> None then
459             CicNotationPt.fail loc "Explicit substitutions not allowed here";
460           Cic.Rel index
461         with Not_found ->
462           let cic =
463             if is_uri ast then  (* we have the URI, build the term out of it *)
464               try
465                 CicUtil.term_of_uri (UriManager.uri_of_string name)
466               with UriManager.IllFormedUri _ ->
467                 CicNotationPt.fail loc "Ill formed URI"
468             else
469               resolve env (Id name) ()
470           in
471           let mk_subst uris =
472             let ids_to_uris =
473               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
474             in
475             (match subst with
476             | Some subst ->
477                 List.map
478                   (fun (s, term) ->
479                     (try
480                       List.assoc s ids_to_uris, aux ~localize loc context term
481                      with Not_found ->
482                        raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
483                   subst
484             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
485           in
486           (try 
487             match cic with
488             | Cic.Const (uri, []) ->
489                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
490                 let uris = CicUtil.params_of_obj o in
491                 Cic.Const (uri, mk_subst uris)
492             | Cic.Var (uri, []) ->
493                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
494                 let uris = CicUtil.params_of_obj o in
495                 Cic.Var (uri, mk_subst uris)
496             | Cic.MutInd (uri, i, []) ->
497                (try
498                  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
499                  let uris = CicUtil.params_of_obj o in
500                  Cic.MutInd (uri, i, mk_subst uris)
501                 with
502                  CicEnvironment.Object_not_found _ ->
503                   (* if we are here it is probably the case that during the
504                      definition of a mutual inductive type we have met an
505                      occurrence of the type in one of its constructors.
506                      However, the inductive type is not yet in the environment
507                   *)
508                   (*here the explicit_named_substituion is assumed to be of length 0 *)
509                   Cic.MutInd (uri,i,[]))
510             | Cic.MutConstruct (uri, i, j, []) ->
511                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
512                 let uris = CicUtil.params_of_obj o in
513                 Cic.MutConstruct (uri, i, j, mk_subst uris)
514             | Cic.Meta _ | Cic.Implicit _ as t ->
515 (*
516                 debug_print (lazy (sprintf
517                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
518                   (CicPp.ppterm t)
519                   (String.concat "; "
520                     (List.map
521                       (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
522                       subst))));
523 *)
524                 t
525             | _ ->
526               raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
527            with 
528              CicEnvironment.CircularDependency _ -> 
529                raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
530     | CicNotationPt.Implicit -> Cic.Implicit None
531     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
532     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
533     | CicNotationPt.Meta (index, subst) ->
534         let cic_subst =
535           List.map
536             (function
537                 None -> None
538               | Some term -> Some (aux ~localize loc context term))
539             subst
540         in
541         Cic.Meta (index, cic_subst)
542     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
543     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
544     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
545     | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
546     | CicNotationPt.Symbol (symbol, instance) ->
547         resolve env (Symbol (symbol, instance)) ()
548     | _ -> assert false (* god bless Bologna *)
549   and aux_option ~localize loc context annotation = function
550     | None -> Cic.Implicit annotation
551     | Some term -> aux ~localize loc context term
552   in
553    aux ~localize:true HExtlib.dummy_floc context ast
554
555 let interpretate_path ~context path =
556  let localization_tbl = Cic.CicHash.create 23 in
557   (* here we are throwing away useful localization informations!!! *)
558   fst (
559    interpretate_term ~create_dummy_ids:true 
560     ~context ~env:Environment.empty ~uri:None ~is_path:true
561     path ~localization_tbl, localization_tbl)
562
563 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
564  assert (context = []);
565  assert (is_path = false);
566  let interpretate_term = interpretate_term ~localization_tbl in
567  match obj with
568   | CicNotationPt.Inductive (params,tyl) ->
569      let uri = match uri with Some uri -> uri | None -> assert false in
570      let context,params =
571       let context,res =
572        List.fold_left
573         (fun (context,res) (name,t) ->
574           let t =
575            match t with
576               None -> CicNotationPt.Implicit
577             | Some t -> t in
578           let name = CicNotationUtil.cic_name_of_name name in
579            name::context,(name, interpretate_term context env None false t)::res
580         ) ([],[]) params
581       in
582        context,List.rev res in
583      let add_params =
584       List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
585      let name_to_uris =
586       snd (
587        List.fold_left
588         (*here the explicit_named_substituion is assumed to be of length 0 *)
589         (fun (i,res) (name,_,_,_) ->
590           i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
591         ) (0,[]) tyl) in
592      let con_env = DisambiguateTypes.env_of_list name_to_uris env in
593      let tyl =
594       List.map
595        (fun (name,b,ty,cl) ->
596          let ty' = add_params (interpretate_term context env None false ty) in
597          let cl' =
598           List.map
599            (fun (name,ty) ->
600              let ty' =
601               add_params (interpretate_term context con_env None false ty)
602              in
603               name,ty'
604            ) cl
605          in
606           name,b,ty',cl'
607        ) tyl
608      in
609       Cic.InductiveDefinition (tyl,[],List.length params,[])
610   | CicNotationPt.Record (params,name,ty,fields) ->
611      let uri = match uri with Some uri -> uri | None -> assert false in
612      let context,params =
613       let context,res =
614        List.fold_left
615         (fun (context,res) (name,t) ->
616           let t =
617            match t with
618               None -> CicNotationPt.Implicit
619             | Some t -> t in
620           let name = CicNotationUtil.cic_name_of_name name in
621            name::context,(name, interpretate_term context env None false t)::res
622         ) ([],[]) params
623       in
624        context,List.rev res in
625      let add_params =
626       List.fold_right
627        (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
628      let ty' = add_params (interpretate_term context env None false ty) in
629      let fields' =
630       snd (
631        List.fold_left
632         (fun (context,res) (name,ty,_coercion,arity) ->
633           let context' = Cic.Name name :: context in
634            context',(name,interpretate_term context env None false ty)::res
635         ) (context,[]) fields) in
636      let concl =
637       (*here the explicit_named_substituion is assumed to be of length 0 *)
638       let mutind = Cic.MutInd (uri,0,[]) in
639       if params = [] then mutind
640       else
641        Cic.Appl
642         (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
643      let con =
644       List.fold_left
645        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
646        concl fields' in
647      let con' = add_params con in
648      let tyl = [name,true,ty',["mk_" ^ name,con']] in
649      let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
650       Cic.InductiveDefinition
651        (tyl,[],List.length params,[`Class (`Record field_names)])
652   | CicNotationPt.Theorem (flavour, name, ty, bo) ->
653      let attrs = [`Flavour flavour] in
654      let ty' = interpretate_term [] env None false ty in
655      (match bo,flavour with
656         None,`Axiom ->
657          Cic.Constant (name,None,ty',[],attrs)
658       | Some bo,`Axiom -> assert false
659       | None,_ ->
660          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
661       | Some bo,_ ->
662          let bo' = Some (interpretate_term [] env None false bo) in
663           Cic.Constant (name,bo',ty',[],attrs))
664 ;;
665
666 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
667      ~localization_tbl
668 =
669   let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
670 interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
671 ~localization_tbl
672 ;;
673
674           
675 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
676   | Ast.AttributedTerm (`Loc loc, term) ->
677      domain_of_term ~loc ~context term
678   | Ast.AttributedTerm (_, term) ->
679       domain_of_term ~loc ~context term
680   | Ast.Symbol (symbol, instance) ->
681       [ Node ([loc], Symbol (symbol, instance), []) ]
682       (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
683   | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
684   | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
685      ->
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        [ Node ([loc], Symbol (symbol, instance), args_dom) ]
696   | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
697   | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
698       let args_dom =
699         List.fold_right
700           (fun term acc -> domain_of_term ~loc ~context term @ acc)
701           args [] in
702       let loc =
703        match hd with
704           Ast.AttributedTerm (`Loc loc,_)  -> loc
705         | _ -> loc
706       in
707       (try
708         (* the next line can raise Not_found *)
709         ignore(find_in_context name context);
710         if subst <> None then
711           Ast.fail loc "Explicit substitutions not allowed here"
712         else
713           args_dom
714       with Not_found ->
715         (match subst with
716         | None -> [ Node ([loc], Id name, args_dom) ]
717         | Some subst ->
718             let terms =
719               List.fold_left
720                 (fun dom (_, term) ->
721                   let dom' = domain_of_term ~loc ~context term in
722                   dom @ dom')
723                 [] subst in
724             [ Node ([loc], Id name, terms @ args_dom) ]))
725   | Ast.Appl terms ->
726       List.fold_right
727         (fun term acc -> domain_of_term ~loc ~context term @ acc)
728         terms []
729   | Ast.Binder (kind, (var, typ), body) ->
730       let type_dom = domain_of_term_option ~loc ~context typ in
731       let body_dom =
732         domain_of_term ~loc
733           ~context:(CicNotationUtil.cic_name_of_name var :: context) body in
734       (match kind with
735       | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
736       | _ -> type_dom @ body_dom)
737   | Ast.Case (term, indty_ident, outtype, branches) ->
738       let term_dom = domain_of_term ~loc ~context term in
739       let outtype_dom = domain_of_term_option ~loc ~context outtype in
740       let rec get_first_constructor = function
741         | [] -> []
742         | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
743         | _ :: tl -> get_first_constructor tl in
744       let do_branch =
745        function
746           Ast.Pattern (head, _, args), term ->
747            let (term_context, args_domain) =
748              List.fold_left
749                (fun (cont, dom) (name, typ) ->
750                  (CicNotationUtil.cic_name_of_name name :: cont,
751                   (match typ with
752                   | None -> dom
753                   | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
754                (context, []) args
755            in
756             domain_of_term ~loc ~context:term_context term @ args_domain
757         | Ast.Wildcard, term ->
758             domain_of_term ~loc ~context term
759       in
760       let branches_dom =
761         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
762       (match indty_ident with
763        | None -> get_first_constructor branches
764        | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
765       @ term_dom @ outtype_dom @ branches_dom
766   | Ast.Cast (term, ty) ->
767       let term_dom = domain_of_term ~loc ~context term in
768       let ty_dom = domain_of_term ~loc ~context ty in
769       term_dom @ ty_dom
770   | Ast.LetIn ((var, typ), body, where) ->
771       let body_dom = domain_of_term ~loc ~context body in
772       let type_dom = domain_of_term_option ~loc ~context typ in
773       let where_dom =
774         domain_of_term ~loc
775           ~context:(CicNotationUtil.cic_name_of_name var :: context) where in
776       body_dom @ type_dom @ where_dom
777   | Ast.LetRec (kind, defs, where) ->
778       let add_defs context =
779         List.fold_left
780           (fun acc (_, (var, _), _, _) ->
781             CicNotationUtil.cic_name_of_name var :: acc
782           ) context defs in
783       let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
784       let defs_dom =
785         List.fold_left
786           (fun dom (params, (_, typ), body, _) ->
787             let context' =
788              add_defs
789               (List.fold_left
790                 (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
791                 context params)
792             in
793             List.rev
794              (snd
795                (List.fold_left
796                 (fun (context,res) (var,ty) ->
797                   CicNotationUtil.cic_name_of_name var :: context,
798                   domain_of_term_option ~loc ~context ty @ res)
799                 (add_defs context,[]) params))
800             @ dom
801             @ domain_of_term_option ~loc ~context:context' typ
802             @ domain_of_term ~loc ~context:context' body
803           ) [] defs
804       in
805       defs_dom @ where_dom
806   | Ast.Ident (name, subst) ->
807       (try
808         (* the next line can raise Not_found *)
809         ignore(find_in_context name context);
810         if subst <> None then
811           Ast.fail loc "Explicit substitutions not allowed here"
812         else
813           []
814       with Not_found ->
815         (match subst with
816         | None -> [ Node ([loc], Id name, []) ]
817         | Some subst ->
818             let terms =
819               List.fold_left
820                 (fun dom (_, term) ->
821                   let dom' = domain_of_term ~loc ~context term in
822                   dom @ dom')
823                 [] subst in
824             [ Node ([loc], Id name, terms) ]))
825   | Ast.Uri _ -> []
826   | Ast.Implicit -> []
827   | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
828   | Ast.Meta (index, local_context) ->
829       List.fold_left
830        (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
831        [] local_context
832   | Ast.Sort _ -> []
833   | Ast.UserInput
834   | Ast.Literal _
835   | Ast.Layout _
836   | Ast.Magic _
837   | Ast.Variable _ -> assert false
838
839 and domain_of_term_option ~loc ~context = function
840   | None -> []
841   | Some t -> domain_of_term ~loc ~context t
842
843 let domain_of_term ~context term = 
844  uniq_domain (domain_of_term ~context term)
845
846 let domain_of_obj ~context ast =
847  let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
848  assert (context = []);
849   match ast with
850    | Ast.Theorem (_,_,ty,bo) ->
851       domain_of_term [] ty
852       @ (match bo with
853           None -> []
854         | Some bo -> domain_of_term [] bo)
855    | Ast.Inductive (params,tyl) ->
856       let context, dom = 
857        List.fold_left
858         (fun (context, dom) (var, ty) ->
859           let context' = CicNotationUtil.cic_name_of_name var :: context in
860           match ty with
861              None -> context', dom
862            | Some ty -> context', dom @ domain_of_term context ty
863         ) ([], []) params in
864       let context_w_types =
865         List.rev_map
866           (fun (var, _, _, _) -> Cic.Name var) tyl
867         @ context in
868       dom
869       @ List.flatten (
870          List.map
871           (fun (_,_,ty,cl) ->
872             domain_of_term context ty
873             @ List.flatten (
874                List.map
875                 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
876                 tyl)
877    | CicNotationPt.Record (params,var,ty,fields) ->
878       let context, dom = 
879        List.fold_left
880         (fun (context, dom) (var, ty) ->
881           let context' = CicNotationUtil.cic_name_of_name var :: context in
882           match ty with
883              None -> context', dom
884            | Some ty -> context', dom @ domain_of_term context ty
885         ) ([], []) params in
886       let context_w_types = Cic.Name var :: context in
887       dom
888       @ domain_of_term context ty
889       @ snd
890          (List.fold_left
891           (fun (context,res) (name,ty,_,_) ->
892             Cic.Name name::context, res @ domain_of_term context ty
893           ) (context_w_types,[]) fields)
894
895 let domain_of_obj ~context obj = 
896  uniq_domain (domain_of_obj ~context obj)
897
898 let domain_of_ast_term = domain_of_term;;
899
900 let domain_of_term ~context term = 
901  let context = 
902    List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context 
903  in
904  domain_of_term ~context term
905
906   (* dom1 \ dom2 *)
907 let domain_diff dom1 dom2 =
908 (* let domain_diff = Domain.diff *)
909   let is_in_dom2 elt =
910     List.exists
911      (function
912        | Symbol (symb, 0) ->
913           (match elt with
914               Symbol (symb',_) when symb = symb' -> true
915             | _ -> false)
916        | Num i ->
917           (match elt with
918               Num _ -> true
919             | _ -> false)
920        | item -> elt = item
921      ) dom2
922   in
923    let rec aux =
924     function
925        [] -> []
926      | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
927      | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
928    in
929     aux dom1
930
931 module type Disambiguator =
932 sig
933   val disambiguate_thing:
934     dbd:HSql.dbd ->
935     context:'context ->
936     metasenv:'metasenv ->
937     initial_ugraph:'ugraph ->
938     aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
939     universe:DisambiguateTypes.codomain_item list
940              DisambiguateTypes.Environment.t option ->
941     uri:'uri ->
942     pp_thing:('ast_thing -> string) ->
943     domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
944     interpretate_thing:(context:'context ->
945                         env:DisambiguateTypes.codomain_item
946                             DisambiguateTypes.Environment.t ->
947                         uri:'uri ->
948                         is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
949     refine_thing:('metasenv ->
950                   'context ->
951                   'uri ->
952                   'raw_thing ->
953                   'ugraph -> localization_tbl:'cichash -> ('refined_thing,
954                   'metasenv) test_result * 'ugraph) ->
955     localization_tbl:'cichash ->
956     string * int * 'ast_thing ->
957     ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
958      list * 'metasenv * 'refined_thing * 'ugraph)
959     list * bool
960   val disambiguate_term :
961     ?fresh_instances:bool ->
962     dbd:HSql.dbd ->
963     context:Cic.context ->
964     metasenv:Cic.metasenv ->
965     ?initial_ugraph:CicUniv.universe_graph -> 
966     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
967     universe:DisambiguateTypes.multiple_environment option ->
968     CicNotationPt.term disambiguator_input ->
969     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
970      Cic.metasenv *                  (* new metasenv *)
971      Cic.term*
972      CicUniv.universe_graph) list *  (* disambiguated term *)
973     bool
974
975   val disambiguate_obj :
976     ?fresh_instances:bool ->
977     dbd:HSql.dbd ->
978     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
979     universe:DisambiguateTypes.multiple_environment option ->
980     uri:UriManager.uri option ->     (* required only for inductive types *)
981     CicNotationPt.term CicNotationPt.obj disambiguator_input ->
982     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
983      Cic.metasenv *                  (* new metasenv *)
984      Cic.obj *
985      CicUniv.universe_graph) list *  (* disambiguated obj *)
986     bool
987 end
988
989 module Make (C: Callbacks) =
990   struct
991     let choices_of_id dbd id =
992       let uris = Whelp.locate ~dbd id in
993       let uris =
994        match uris with
995         | [] ->
996            (match 
997              (C.input_or_locate_uri 
998                ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ()) 
999            with
1000            | None -> []
1001            | Some uri -> [uri])
1002         | [uri] -> [uri]
1003         | _ ->
1004             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
1005              ~ok:"Try selected." ~enable_button_for_non_vars:true
1006              ~title:"Ambiguous input." ~id
1007              ~msg: ("Ambiguous input \"" ^ id ^
1008                 "\". Please, choose one or more interpretations:")
1009              uris
1010       in
1011       List.map
1012         (fun uri ->
1013           (UriManager.string_of_uri uri,
1014            let term =
1015              try
1016                CicUtil.term_of_uri uri
1017              with exn ->
1018                debug_print (lazy (UriManager.string_of_uri uri));
1019                debug_print (lazy (Printexc.to_string exn));
1020                assert false
1021             in
1022            fun _ _ _ -> term))
1023         uris
1024
1025 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
1026
1027     let disambiguate_thing ~dbd ~context ~metasenv
1028       ~initial_ugraph ~aliases ~universe
1029       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
1030       ~localization_tbl
1031       (thing_txt,thing_txt_prefix_len,thing)
1032     =
1033       debug_print (lazy "DISAMBIGUATE INPUT");
1034       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
1035       let thing_dom = domain_of_thing ~context thing in
1036       debug_print
1037        (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
1038 (*
1039       debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
1040         (DisambiguatePp.pp_environment aliases)));
1041       debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
1042         (match universe with None -> "None" | Some _ -> "Some _")));
1043 *)
1044       let current_dom =
1045         Environment.fold (fun item _ dom -> item :: dom) aliases [] in
1046       let todo_dom = domain_diff thing_dom current_dom in
1047       debug_print
1048        (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
1049       (* (2) lookup function for any item (Id/Symbol/Num) *)
1050       let lookup_choices =
1051         fun item ->
1052           let choices =
1053             let lookup_in_library () =
1054               match item with
1055               | Id id -> choices_of_id dbd id
1056               | Symbol (symb, _) ->
1057                  (try
1058                    List.map DisambiguateChoices.mk_choice
1059                     (TermAcicContent.lookup_interpretations symb)
1060                   with
1061                    TermAcicContent.Interpretation_not_found -> [])
1062               | Num instance ->
1063                   DisambiguateChoices.lookup_num_choices ()
1064             in
1065             match universe with
1066             | None -> lookup_in_library ()
1067             | Some e ->
1068                 (try
1069                   let item =
1070                     match item with
1071                     | Symbol (symb, _) -> Symbol (symb, 0)
1072                     | item -> item
1073                   in
1074                   Environment.find item e
1075                 with Not_found -> lookup_in_library ())
1076           in
1077           choices
1078       in
1079 (*
1080       (* <benchmark> *)
1081       let _ =
1082         if benchmark then begin
1083           let per_item_choices =
1084             List.map
1085               (fun dom_item ->
1086                 try
1087                   let len = List.length (lookup_choices dom_item) in
1088                   debug_print (lazy (sprintf "BENCHMARK %s: %d"
1089                     (string_of_domain_item dom_item) len));
1090                   len
1091                 with No_choices _ -> 0)
1092               thing_dom
1093           in
1094           max_refinements := List.fold_left ( * ) 1 per_item_choices;
1095           actual_refinements := 0;
1096           domain_size := List.length thing_dom;
1097           choices_avg :=
1098             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
1099         end
1100       in
1101       (* </benchmark> *)
1102 *)
1103
1104       (* (3) test an interpretation filling with meta uninterpreted identifiers
1105        *)
1106       let test_env aliases todo_dom ugraph = 
1107         let rec aux env = function
1108           | [] -> env
1109           | Node (_, item, l) :: tl ->
1110               let env =
1111                 Environment.add item
1112                  ("Implicit",
1113                    (match item with
1114                       | Id _ | Num _ ->
1115                           (fun _ _ _ -> Cic.Implicit (Some `Closed))
1116                       | Symbol _ -> (fun _ _ _ -> Cic.Implicit None)))
1117                  env in
1118               aux (aux env l) tl in
1119         let filled_env = aux aliases todo_dom in
1120         try
1121           let cic_thing =
1122             interpretate_thing ~context ~env:filled_env
1123              ~uri ~is_path:false thing ~localization_tbl
1124           in
1125 let foo () =
1126           let k,ugraph1 =
1127            refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
1128           in
1129             (k , ugraph1 )
1130 in refine_profiler.HExtlib.profile foo ()
1131         with
1132         | Try_again msg -> Uncertain (None,msg), ugraph
1133         | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph
1134       in
1135       (* (4) build all possible interpretations *)
1136       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
1137       (* aux returns triples Ok/Uncertain/Ko *)
1138       (* rem_dom is the concatenation of all the remainin domains *)
1139       let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ =
1140         debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
1141         match todo_dom with
1142         | [] ->
1143             assert (lookup_in_todo_dom = None);
1144             (match test_env aliases rem_dom base_univ with
1145             | Ok (thing, metasenv),new_univ -> 
1146                [ aliases, diff, metasenv, thing, new_univ ], [], []
1147             | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true]
1148             | Uncertain (loc,msg),new_univ ->
1149                [],[aliases,diff,loc,msg,new_univ],[])
1150         | Node (locs,item,inner_dom) :: remaining_dom ->
1151             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
1152              (string_of_domain_item item)));
1153             let choices =
1154              match lookup_in_todo_dom with
1155                 None -> lookup_choices item
1156               | Some choices -> choices in
1157             match choices with
1158                [] ->
1159                 [], [],
1160                  [aliases, diff, Some (List.hd locs),
1161                   lazy ("No choices for " ^ string_of_domain_item item),
1162                   true]
1163 (*
1164              | [codomain_item] ->
1165                  (* just one choice. We perform a one-step look-up and
1166                     if the next set of choices is also a singleton we
1167                     skip this refinement step *)
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                  let lookup_in_todo_dom,next_choice_is_single =
1172                   match remaining_dom with
1173                      [] -> None,false
1174                    | (_,he)::_ ->
1175                       let choices = lookup_choices he in
1176                        Some choices,List.length choices = 1
1177                  in
1178                   if next_choice_is_single then
1179                    aux new_env new_diff lookup_in_todo_dom remaining_dom
1180                     base_univ
1181                   else
1182                     (match test_env new_env remaining_dom base_univ with
1183                     | Ok (thing, metasenv),new_univ ->
1184                         (match remaining_dom with
1185                         | [] ->
1186                            [ new_env, new_diff, metasenv, thing, new_univ ], []
1187                         | _ ->
1188                            aux new_env new_diff lookup_in_todo_dom
1189                             remaining_dom new_univ)
1190                     | Uncertain (loc,msg),new_univ ->
1191                         (match remaining_dom with
1192                         | [] -> [], [new_env,new_diff,loc,msg,true]
1193                         | _ ->
1194                            aux new_env new_diff lookup_in_todo_dom
1195                             remaining_dom new_univ)
1196                     | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
1197 *)
1198              | _::_ ->
1199                  let mark_not_significant failures =
1200                    List.map
1201                     (fun (env, diff, loc, msg, _b) ->
1202                       env, diff, loc, msg, false)
1203                     failures in
1204                  let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
1205                   if ok_l <> [] || uncertain_l <> [] then
1206                    ok_l,uncertain_l,mark_not_significant error_l
1207                   else
1208                    outcome in
1209                let rec filter univ = function 
1210                 | [] -> [],[],[]
1211                 | codomain_item :: tl ->
1212                     debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1213                     let new_env = Environment.add item codomain_item aliases in
1214                     let new_diff = (item,codomain_item)::diff in
1215                     (match
1216                       test_env new_env (inner_dom@remaining_dom@rem_dom) univ
1217                      with
1218                     | Ok (thing, metasenv),new_univ ->
1219                         let res = 
1220                           (match inner_dom with
1221                           | [] ->
1222                              [new_env,new_diff,metasenv,thing,new_univ], [], []
1223                           | _ ->
1224                              aux new_env new_diff None inner_dom
1225                               (remaining_dom@rem_dom) new_univ
1226                           ) 
1227                         in
1228                          res @@ filter univ tl
1229                     | Uncertain (loc,msg),new_univ ->
1230                         let res =
1231                           (match inner_dom with
1232                           | [] -> [],[new_env,new_diff,loc,msg,new_univ],[]
1233                           | _ ->
1234                              aux new_env new_diff None inner_dom
1235                               (remaining_dom@rem_dom) new_univ
1236                           )
1237                         in
1238                          res @@ filter univ tl
1239                     | Ko (loc,msg),_ ->
1240                         let res = [],[],[new_env,new_diff,loc,msg,true] in
1241                          res @@ filter univ tl)
1242                in
1243                 let ok_l,uncertain_l,error_l =
1244                  classify_errors (filter base_univ choices)
1245                 in
1246                  let res_after_ok_l =
1247                   List.fold_right
1248                    (fun (env,diff,_,_,univ) res ->
1249                      aux env diff None remaining_dom rem_dom univ @@ res
1250                    ) ok_l ([],[],error_l)
1251                 in
1252                  List.fold_right
1253                   (fun (env,diff,_,_,univ) res ->
1254                     aux env diff None remaining_dom rem_dom univ @@ res
1255                   ) uncertain_l res_after_ok_l
1256       in
1257       let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
1258        match test_env aliases todo_dom base_univ with
1259         | Ok _,_
1260         | Uncertain _,_ ->
1261            aux aliases diff lookup_in_todo_dom todo_dom [] base_univ
1262         | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in
1263       let base_univ = initial_ugraph in
1264       try
1265         let res =
1266          match aux' aliases [] None todo_dom base_univ with
1267          | [],uncertain,errors ->
1268             let errors =
1269              List.map
1270               (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true)
1271               ) uncertain @ errors
1272             in
1273             let errors =
1274              List.map
1275               (fun (env,diff,loc,msg,significant) ->
1276                 let env' =
1277                  filter_map_domain
1278                    (fun locs domain_item ->
1279                      try
1280                       let description =
1281                        fst (Environment.find domain_item env)
1282                       in
1283                        Some (locs,descr_of_domain_item domain_item,description)
1284                      with
1285                       Not_found -> None)
1286                    thing_dom
1287                 in
1288                  env',diff,loc,msg,significant
1289               ) errors
1290             in
1291              raise (NoWellTypedInterpretation (0,errors))
1292          | [_,diff,metasenv,t,ugraph],_,_ ->
1293              debug_print (lazy "SINGLE INTERPRETATION");
1294              [diff,metasenv,t,ugraph], false
1295          | l,_,_ ->
1296              debug_print 
1297                (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
1298              let choices =
1299                List.map
1300                  (fun (env, _, _, _, _) ->
1301                    map_domain
1302                      (fun locs domain_item ->
1303                        let description =
1304                          fst (Environment.find domain_item env)
1305                        in
1306                        locs,descr_of_domain_item domain_item, description)
1307                      thing_dom)
1308                  l
1309              in
1310              let choosed = 
1311                C.interactive_interpretation_choice 
1312                  thing_txt thing_txt_prefix_len choices 
1313              in
1314              (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
1315               true
1316         in
1317          res
1318      with
1319       CicEnvironment.CircularDependency s -> 
1320         failwith "Disambiguate: circular dependency"
1321
1322     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
1323       ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe 
1324       (text,prefix_len,term)
1325     =
1326       let term =
1327         if fresh_instances then CicNotationUtil.freshen_term term else term
1328       in
1329       let localization_tbl = Cic.CicHash.create 503 in
1330       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
1331         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
1332         ~domain_of_thing:domain_of_term
1333         ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
1334         ~refine_thing:refine_term (text,prefix_len,term)
1335         ~localization_tbl
1336
1337     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
1338      (text,prefix_len,obj)
1339     =
1340       let obj =
1341         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
1342       in
1343       let localization_tbl = Cic.CicHash.create 503 in
1344       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
1345         ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
1346         ~initial_ugraph:CicUniv.empty_ugraph
1347         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
1348         ~localization_tbl
1349         (text,prefix_len,obj)
1350
1351   end
1352
1353