]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_disambiguation/disambiguate.ml
Bug fixed in insertion of parametric coercions.
[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 (* the integer is an offset to be added to each location *)
34 exception NoWellTypedInterpretation of
35  int * (Token.flocation option * string Lazy.t) list
36 exception PathNotWellFormed
37
38   (** raised when an environment is not enough informative to decide *)
39 exception Try_again of string Lazy.t
40
41 type aliases = bool * DisambiguateTypes.environment
42
43 let debug = false
44 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
45
46 (*
47   (** print benchmark information *)
48 let benchmark = true
49 let max_refinements = ref 0       (* benchmarking is not thread safe *)
50 let actual_refinements = ref 0
51 let domain_size = ref 0
52 let choices_avg = ref 0.
53 *)
54
55 let descr_of_domain_item = function
56  | Id s -> s
57  | Symbol (s, _) -> s
58  | Num i -> string_of_int i
59
60 type 'a test_result =
61   | Ok of 'a * Cic.metasenv
62   | Ko of Token.flocation option * string Lazy.t
63   | Uncertain of Token.flocation option * string Lazy.t
64
65 let refine_term metasenv context uri term ugraph ~localization_tbl =
66 (*   if benchmark then incr actual_refinements; *)
67   assert (uri=None);
68     debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
69     try
70       let term', _, metasenv',ugraph1 = 
71         CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
72         (Ok (term', metasenv')),ugraph1
73     with
74      exn ->
75       let rec process_exn loc =
76        function
77           HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
78         | CicRefine.Uncertain msg ->
79             debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
80             Uncertain (loc,msg),ugraph
81         | CicRefine.RefineFailure msg ->
82             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
83               (CicPp.ppterm term) (Lazy.force msg)));
84             Ko (loc,msg),ugraph
85        | exn -> raise exn
86       in
87        process_exn None exn
88
89 let refine_obj metasenv context uri obj ugraph ~localization_tbl =
90  assert (context = []);
91    debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
92    try
93      let obj', metasenv,ugraph =
94       CicRefine.typecheck metasenv uri obj ~localization_tbl
95      in
96        (Ok (obj', metasenv)),ugraph
97    with
98      exn ->
99       let rec process_exn loc =
100        function
101           HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
102         | CicRefine.Uncertain msg ->
103             debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
104             Uncertain (loc,msg),ugraph
105         | CicRefine.RefineFailure msg ->
106             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
107               (CicPp.ppobj obj) (Lazy.force msg))) ;
108             Ko (loc,msg),ugraph
109        | exn -> raise exn
110       in
111        process_exn None exn
112
113 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
114   try
115     snd (Environment.find item env) env num args
116   with Not_found -> 
117     failwith ("Domain item not found: " ^ 
118       (DisambiguateTypes.string_of_domain_item item))
119
120   (* TODO move it to Cic *)
121 let find_in_context name context =
122   let rec aux acc = function
123     | [] -> raise Not_found
124     | Cic.Name hd :: tl when hd = name -> acc
125     | _ :: tl ->  aux (acc + 1) tl
126   in
127   aux 1 context
128
129 let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
130      ~localization_tbl
131 =
132   assert (uri = None);
133   let rec aux ~localize loc (context: Cic.name list) = function
134     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
135         let res = aux ~localize loc context term in
136          if localize then Cic.CicHash.add localization_tbl res loc;
137          res
138     | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
139     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
140         let cic_args = List.map (aux ~localize loc context) args in
141         resolve env (Symbol (symb, i)) ~args:cic_args ()
142     | CicNotationPt.Appl terms ->
143        Cic.Appl (List.map (aux ~localize loc context) terms)
144     | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
145         let cic_type = aux_option ~localize loc context (Some `Type) typ in
146         let cic_name = CicNotationUtil.cic_name_of_name var in
147         let cic_body = aux ~localize loc (cic_name :: context) body in
148         (match binder_kind with
149         | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
150         | `Pi
151         | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
152         | `Exists ->
153             resolve env (Symbol ("exists", 0))
154               ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
155     | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
156         let cic_term = aux ~localize loc context term in
157         let cic_outtype = aux_option ~localize loc context None outtype in
158         let do_branch ((head, _, args), term) =
159           let rec do_branch' context = function
160             | [] -> aux ~localize loc context term
161             | (name, typ) :: tl ->
162                 let cic_name = CicNotationUtil.cic_name_of_name name in
163                 let cic_body = do_branch' (cic_name :: context) tl in
164                 let typ =
165                   match typ with
166                   | None -> Cic.Implicit (Some `Type)
167                   | Some typ -> aux ~localize loc context typ
168                 in
169                 Cic.Lambda (cic_name, typ, cic_body)
170           in
171           do_branch' context args
172         in
173         let (indtype_uri, indtype_no) =
174           match indty_ident with
175           | Some (indty_ident, _) ->
176              (match resolve env (Id indty_ident) () with
177               | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
178               | Cic.Implicit _ ->
179                  raise (Try_again (lazy "The type of the term to be matched
180                   is still unknown"))
181               | _ ->
182                 raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!")))
183           | None ->
184               let fst_constructor =
185                 match branches with
186                 | ((head, _, _), _) :: _ -> head
187                 | [] -> raise (Invalid_choice (lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined"))
188               in
189               (match resolve env (Id fst_constructor) () with
190               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
191                   (indtype_uri, indtype_no)
192               | Cic.Implicit _ ->
193                  raise (Try_again (lazy "The type of the term to be matched
194                   is still unknown"))
195               | _ ->
196                 raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!")))
197         in
198         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
199           (List.map do_branch branches))
200     | CicNotationPt.Cast (t1, t2) ->
201         let cic_t1 = aux ~localize loc context t1 in
202         let cic_t2 = aux ~localize loc context t2 in
203         Cic.Cast (cic_t1, cic_t2)
204     | CicNotationPt.LetIn ((name, typ), def, body) ->
205         let cic_def = aux ~localize loc context def in
206         let cic_name = CicNotationUtil.cic_name_of_name name in
207         let cic_def =
208           match typ with
209           | None -> cic_def
210           | Some t -> Cic.Cast (cic_def, aux ~localize loc context t)
211         in
212         let cic_body = aux ~localize loc (cic_name :: context) body in
213         Cic.LetIn (cic_name, cic_def, cic_body)
214     | CicNotationPt.LetRec (kind, defs, body) ->
215         let context' =
216           List.fold_left
217             (fun acc ((name, _), _, _) ->
218               CicNotationUtil.cic_name_of_name name :: acc)
219             context defs
220         in
221         let cic_body =
222          let unlocalized_body = aux ~localize:false loc context' body in
223          match unlocalized_body with
224             Cic.Rel 1 -> `AvoidLetInNoAppl
225           | Cic.Appl (Cic.Rel 1::l) ->
226              (try
227                let l' =
228                 List.map
229                  (function t ->
230                    let t',subst,metasenv =
231                     CicMetaSubst.delift_rels [] [] 1 t
232                    in
233                     assert (subst=[]);
234                     assert (metasenv=[]);
235                     t') l
236                in
237                 (* We can avoid the LetIn. But maybe we need to recompute l'
238                    so that it is localized *)
239                 if localize then
240                  match body with
241                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
242                      let l' = List.map (aux ~localize loc context) l in
243                       `AvoidLetIn l'
244                   | _ -> assert false
245                 else
246                  `AvoidLetIn l'
247               with
248                CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
249                 if localize then
250                  `AddLetIn (aux ~localize loc context' body)
251                 else
252                  `AddLetIn unlocalized_body)
253           | _ ->
254              if localize then
255               `AddLetIn (aux ~localize loc context' body)
256              else
257               `AddLetIn unlocalized_body
258         in
259         let inductiveFuns =
260           List.map
261             (fun ((name, typ), body, decr_idx) ->
262               let cic_body = aux ~localize loc context' body in
263               let cic_type =
264                aux_option ~localize loc context (Some `Type) typ in
265               let name =
266                 match CicNotationUtil.cic_name_of_name name with
267                 | Cic.Anonymous ->
268                     CicNotationPt.fail loc
269                       "Recursive functions cannot be anonymous"
270                 | Cic.Name name -> name
271               in
272               (name, decr_idx, cic_type, cic_body))
273             defs
274         in
275         let counter = ref ~-1 in
276         let build_term funs =
277           (* this is the body of the fold_right function below. Rationale: Fix
278            * and CoFix cases differs only in an additional index in the
279            * inductiveFun list, see Cic.term *)
280           match kind with
281           | `Inductive ->
282               (fun (var, _, _, _) cic ->
283                 incr counter;
284                 let fix = Cic.Fix (!counter,funs) in
285                  match cic with
286                     `Recipe (`AddLetIn cic) ->
287                       `Term (Cic.LetIn (Cic.Name var, fix, cic))
288                   | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (fix::l))
289                   | `Recipe `AvoidLetInNoAppl -> `Term fix
290                   | `Term t -> `Term (Cic.LetIn (Cic.Name var, fix, t)))
291           | `CoInductive ->
292               let funs =
293                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
294               in
295               (fun (var, _, _, _) cic ->
296                 incr counter;
297                 let cofix = Cic.CoFix (!counter,funs) in
298                  match cic with
299                     `Recipe (`AddLetIn cic) ->
300                       `Term (Cic.LetIn (Cic.Name var, cofix, cic))
301                   | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (cofix::l))
302                   | `Recipe `AvoidLetInNoAppl -> `Term cofix
303                   | `Term t -> `Term (Cic.LetIn (Cic.Name var, cofix, t)))
304         in
305          (match
306            List.fold_right (build_term inductiveFuns) inductiveFuns
307             (`Recipe cic_body)
308           with
309              `Recipe _ -> assert false
310            | `Term t -> t)
311     | CicNotationPt.Ident _
312     | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
313     | CicNotationPt.Ident (name, subst)
314     | CicNotationPt.Uri (name, subst) as ast ->
315         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
316         (try
317           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
318           let index = find_in_context name context in
319           if subst <> None then
320             CicNotationPt.fail loc "Explicit substitutions not allowed here";
321           Cic.Rel index
322         with Not_found ->
323           let cic =
324             if is_uri ast then  (* we have the URI, build the term out of it *)
325               try
326                 CicUtil.term_of_uri (UriManager.uri_of_string name)
327               with UriManager.IllFormedUri _ ->
328                 CicNotationPt.fail loc "Ill formed URI"
329             else
330               resolve env (Id name) ()
331           in
332           let mk_subst uris =
333             let ids_to_uris =
334               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
335             in
336             (match subst with
337             | Some subst ->
338                 List.map
339                   (fun (s, term) ->
340                     (try
341                       List.assoc s ids_to_uris, aux ~localize loc context term
342                      with Not_found ->
343                        raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
344                   subst
345             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
346           in
347           (try 
348             match cic with
349             | Cic.Const (uri, []) ->
350                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
351                 let uris = CicUtil.params_of_obj o in
352                 Cic.Const (uri, mk_subst uris)
353             | Cic.Var (uri, []) ->
354                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
355                 let uris = CicUtil.params_of_obj o in
356                 Cic.Var (uri, mk_subst uris)
357             | Cic.MutInd (uri, i, []) ->
358                (try
359                  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
360                  let uris = CicUtil.params_of_obj o in
361                  Cic.MutInd (uri, i, mk_subst uris)
362                 with
363                  CicEnvironment.Object_not_found _ ->
364                   (* if we are here it is probably the case that during the
365                      definition of a mutual inductive type we have met an
366                      occurrence of the type in one of its constructors.
367                      However, the inductive type is not yet in the environment
368                   *)
369                   (*here the explicit_named_substituion is assumed to be of length 0 *)
370                   Cic.MutInd (uri,i,[]))
371             | Cic.MutConstruct (uri, i, j, []) ->
372                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
373                 let uris = CicUtil.params_of_obj o in
374                 Cic.MutConstruct (uri, i, j, mk_subst uris)
375             | Cic.Meta _ | Cic.Implicit _ as t ->
376 (*
377                 debug_print (lazy (sprintf
378                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
379                   (CicPp.ppterm t)
380                   (String.concat "; "
381                     (List.map
382                       (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
383                       subst))));
384 *)
385                 t
386             | _ ->
387               raise (Invalid_choice (lazy "??? Can this happen?"))
388            with 
389              CicEnvironment.CircularDependency _ -> 
390                raise (Invalid_choice (lazy "Circular dependency in the environment"))))
391     | CicNotationPt.Implicit -> Cic.Implicit None
392     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
393     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
394     | CicNotationPt.Meta (index, subst) ->
395         let cic_subst =
396           List.map
397             (function
398                 None -> None
399               | Some term -> Some (aux ~localize loc context term))
400             subst
401         in
402         Cic.Meta (index, cic_subst)
403     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
404     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
405     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
406     | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
407     | CicNotationPt.Symbol (symbol, instance) ->
408         resolve env (Symbol (symbol, instance)) ()
409     | _ -> assert false (* god bless Bologna *)
410   and aux_option ~localize loc (context: Cic.name list) annotation = function
411     | None -> Cic.Implicit annotation
412     | Some term -> aux ~localize loc context term
413   in
414    aux ~localize:true HExtlib.dummy_floc context ast
415
416 let interpretate_path ~context path =
417  let localization_tbl = Cic.CicHash.create 23 in
418   (* here we are throwing away useful localization informations!!! *)
419   fst (
420    interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true
421     path ~localization_tbl, localization_tbl)
422
423 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
424  assert (context = []);
425  assert (is_path = false);
426  let interpretate_term = interpretate_term ~localization_tbl in
427  match obj with
428   | CicNotationPt.Inductive (params,tyl) ->
429      let uri = match uri with Some uri -> uri | None -> assert false in
430      let context,params =
431       let context,res =
432        List.fold_left
433         (fun (context,res) (name,t) ->
434           Cic.Name name :: context,
435           (name, interpretate_term context env None false t)::res
436         ) ([],[]) params
437       in
438        context,List.rev res in
439      let add_params =
440       List.fold_right
441        (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
442      let name_to_uris =
443       snd (
444        List.fold_left
445         (*here the explicit_named_substituion is assumed to be of length 0 *)
446         (fun (i,res) (name,_,_,_) ->
447           i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
448         ) (0,[]) tyl) in
449      let con_env = DisambiguateTypes.env_of_list name_to_uris env in
450      let tyl =
451       List.map
452        (fun (name,b,ty,cl) ->
453          let ty' = add_params (interpretate_term context env None false ty) in
454          let cl' =
455           List.map
456            (fun (name,ty) ->
457              let ty' =
458               add_params (interpretate_term context con_env None false ty)
459              in
460               name,ty'
461            ) cl
462          in
463           name,b,ty',cl'
464        ) tyl
465      in
466       Cic.InductiveDefinition (tyl,[],List.length params,[])
467   | CicNotationPt.Record (params,name,ty,fields) ->
468      let uri = match uri with Some uri -> uri | None -> assert false in
469      let context,params =
470       let context,res =
471        List.fold_left
472         (fun (context,res) (name,t) ->
473           (Cic.Name name :: context),
474           (name, interpretate_term context env None false t)::res
475         ) ([],[]) params
476       in
477        context,List.rev res in
478      let add_params =
479       List.fold_right
480        (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
481      let ty' = add_params (interpretate_term context env None false ty) in
482      let fields' =
483       snd (
484        List.fold_left
485         (fun (context,res) (name,ty,_coercion) ->
486           let context' = Cic.Name name :: context in
487            context',(name,interpretate_term context env None false ty)::res
488         ) (context,[]) fields) in
489      let concl =
490       (*here the explicit_named_substituion is assumed to be of length 0 *)
491       let mutind = Cic.MutInd (uri,0,[]) in
492       if params = [] then mutind
493       else
494        Cic.Appl
495         (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
496      let con =
497       List.fold_left
498        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
499        concl fields' in
500      let con' = add_params con in
501      let tyl = [name,true,ty',["mk_" ^ name,con']] in
502      let field_names = List.map (fun (x,_,y) -> x,y) fields in
503       Cic.InductiveDefinition
504        (tyl,[],List.length params,[`Class (`Record field_names)])
505   | CicNotationPt.Theorem (flavour, name, ty, bo) ->
506      let attrs = [`Flavour flavour] in
507      let ty' = interpretate_term [] env None false ty in
508      (match bo with
509         None ->
510          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
511       | Some bo ->
512          let bo' = Some (interpretate_term [] env None false bo) in
513           Cic.Constant (name,bo',ty',[],attrs))
514           
515
516   (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
517 let rev_uniq =
518   let module SortedItem =
519     struct
520       type t = DisambiguateTypes.domain_item
521       let compare = Pervasives.compare
522     end
523   in
524   let module Set = Set.Make (SortedItem) in
525   fun l ->
526     let rev_l = List.rev l in
527     let (_, uniq_rev_l) =
528       List.fold_left
529         (fun (members, rev_l) elt ->
530           if Set.mem elt members then
531             (members, rev_l)
532           else
533             Set.add elt members, elt :: rev_l)
534         (Set.empty, []) rev_l
535     in
536     List.rev uniq_rev_l
537
538 (* "aux" keeps domain in reverse order and doesn't care about duplicates.
539  * Domain item more in deep in the list will be processed first.
540  *)
541 let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
542   | CicNotationPt.AttributedTerm (`Loc loc, term) ->
543      domain_rev_of_term ~loc context term
544   | CicNotationPt.AttributedTerm (_, term) ->
545       domain_rev_of_term ~loc context term
546   | CicNotationPt.Appl terms ->
547       List.fold_left
548        (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms
549   | CicNotationPt.Binder (kind, (var, typ), body) ->
550       let kind_dom =
551         match kind with
552         | `Exists -> [ Symbol ("exists", 0) ]
553         | _ -> []
554       in
555       let type_dom = domain_rev_of_term_option loc context typ in
556       let body_dom =
557         domain_rev_of_term ~loc
558           (CicNotationUtil.cic_name_of_name var :: context) body
559       in
560       body_dom @ type_dom @ kind_dom
561   | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
562       let term_dom = domain_rev_of_term ~loc context term in
563       let outtype_dom = domain_rev_of_term_option loc context outtype in
564       let get_first_constructor = function
565         | [] -> []
566         | ((head, _, _), _) :: _ -> [ Id head ]
567       in
568       let do_branch ((head, _, args), term) =
569         let (term_context, args_domain) =
570           List.fold_left
571             (fun (cont, dom) (name, typ) ->
572               (CicNotationUtil.cic_name_of_name name :: cont,
573                (match typ with
574                | None -> dom
575                | Some typ -> domain_rev_of_term ~loc cont typ @ dom)))
576             (context, []) args
577         in
578         args_domain @ domain_rev_of_term ~loc term_context term
579       in
580       let branches_dom =
581         List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
582       in
583       branches_dom @ outtype_dom @ term_dom @
584       (match indty_ident with
585        | None -> get_first_constructor branches
586        | Some (ident, _) -> [ Id ident ])
587   | CicNotationPt.Cast (term, ty) ->
588       let term_dom = domain_rev_of_term ~loc context term in
589       let ty_dom = domain_rev_of_term ~loc context ty in
590       ty_dom @ term_dom
591   | CicNotationPt.LetIn ((var, typ), body, where) ->
592       let body_dom = domain_rev_of_term ~loc context body in
593       let type_dom = domain_rev_of_term_option loc context typ in
594       let where_dom =
595         domain_rev_of_term ~loc
596           (CicNotationUtil.cic_name_of_name var :: context) where
597       in
598       where_dom @ type_dom @ body_dom
599   | CicNotationPt.LetRec (kind, defs, where) ->
600       let context' =
601         List.fold_left
602           (fun acc ((var, typ), _, _) ->
603             CicNotationUtil.cic_name_of_name var :: acc)
604           context defs
605       in
606       let where_dom = domain_rev_of_term ~loc context' where in
607       let defs_dom =
608         List.fold_left
609           (fun dom ((_, typ), body, _) ->
610             domain_rev_of_term ~loc context' body @
611             domain_rev_of_term_option loc context typ)
612           [] defs
613       in
614       where_dom @ defs_dom
615   | CicNotationPt.Ident (name, subst) ->
616       (try
617         (* the next line can raise Not_found *)
618         ignore(find_in_context name context);
619         if subst <> None then
620           CicNotationPt.fail loc "Explicit substitutions not allowed here"
621         else
622           []
623       with Not_found ->
624         (match subst with
625         | None -> [Id name]
626         | Some subst ->
627             List.fold_left
628               (fun dom (_, term) ->
629                 let dom' = domain_rev_of_term ~loc context term in
630                 dom' @ dom)
631               [Id name] subst))
632   | CicNotationPt.Uri _ -> []
633   | CicNotationPt.Implicit -> []
634   | CicNotationPt.Num (num, i) -> [ Num i ]
635   | CicNotationPt.Meta (index, local_context) ->
636       List.fold_left
637        (fun dom term -> domain_rev_of_term_option loc context term @ dom) []
638         local_context
639   | CicNotationPt.Sort _ -> []
640   | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
641   | CicNotationPt.UserInput
642   | CicNotationPt.Literal _
643   | CicNotationPt.Layout _
644   | CicNotationPt.Magic _
645   | CicNotationPt.Variable _ -> assert false
646
647 and domain_rev_of_term_option loc context = function
648   | None -> []
649   | Some t -> domain_rev_of_term ~loc context t
650
651 let domain_of_term ~context ast = rev_uniq (domain_rev_of_term context ast)
652
653 let domain_of_obj ~context ast =
654  assert (context = []);
655  let domain_rev =
656   match ast with
657    | CicNotationPt.Theorem (_,_,ty,bo) ->
658       (match bo with
659           None -> []
660         | Some bo -> domain_rev_of_term [] bo) @
661       domain_of_term [] ty
662    | CicNotationPt.Inductive (params,tyl) ->
663       let dom =
664        List.flatten (
665         List.rev_map
666          (fun (_,_,ty,cl) ->
667            List.flatten (
668             List.rev_map
669              (fun (_,ty) -> domain_rev_of_term [] ty) cl) @
670             domain_rev_of_term [] ty) tyl) in
671       let dom = 
672        List.fold_left
673         (fun dom (_,ty) ->
674           domain_rev_of_term [] ty @ dom
675         ) dom params
676       in
677        List.filter
678         (fun name ->
679           not (  List.exists (fun (name',_) -> name = Id name') params
680               || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
681         ) dom
682    | CicNotationPt.Record (params,_,ty,fields) ->
683       let dom =
684        List.flatten
685         (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in
686       let dom =
687        List.fold_left
688         (fun dom (_,ty) ->
689           domain_rev_of_term [] ty @ dom
690         ) (dom @ domain_rev_of_term [] ty) params
691       in
692        List.filter
693         (fun name->
694           not (  List.exists (fun (name',_) -> name = Id name') params
695               || List.exists (fun (name',_,_) -> name = Id name') fields)
696         ) dom
697  in
698   rev_uniq domain_rev
699
700   (* dom1 \ dom2 *)
701 let domain_diff dom1 dom2 =
702 (* let domain_diff = Domain.diff *)
703   let is_in_dom2 =
704     List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
705       (fun _ -> false) dom2
706   in
707   List.filter (fun elt -> not (is_in_dom2 elt)) dom1
708
709 module type Disambiguator =
710 sig
711   val disambiguate_term :
712     ?fresh_instances:bool ->
713     dbd:HMysql.dbd ->
714     context:Cic.context ->
715     metasenv:Cic.metasenv ->
716     ?initial_ugraph:CicUniv.universe_graph -> 
717     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
718     universe:DisambiguateTypes.multiple_environment option ->
719     CicNotationPt.term ->
720     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
721      Cic.metasenv *                  (* new metasenv *)
722      Cic.term*
723      CicUniv.universe_graph) list *  (* disambiguated term *)
724     bool
725
726   val disambiguate_obj :
727     ?fresh_instances:bool ->
728     dbd:HMysql.dbd ->
729     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
730     universe:DisambiguateTypes.multiple_environment option ->
731     uri:UriManager.uri option ->     (* required only for inductive types *)
732     CicNotationPt.obj ->
733     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
734      Cic.metasenv *                  (* new metasenv *)
735      Cic.obj *
736      CicUniv.universe_graph) list *  (* disambiguated obj *)
737     bool
738 end
739
740 module Make (C: Callbacks) =
741   struct
742     let choices_of_id dbd id =
743       let uris = Whelp.locate ~dbd id in
744       let uris =
745        match uris with
746         | [] ->
747            [(C.input_or_locate_uri
748             ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
749         | [uri] -> [uri]
750         | _ ->
751             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
752              ~ok:"Try selected." ~enable_button_for_non_vars:true
753              ~title:"Ambiguous input." ~id
754              ~msg: ("Ambiguous input \"" ^ id ^
755                 "\". Please, choose one or more interpretations:")
756              uris
757       in
758       List.map
759         (fun uri ->
760           (UriManager.string_of_uri uri,
761            let term =
762              try
763                CicUtil.term_of_uri uri
764              with exn ->
765                debug_print (lazy (UriManager.string_of_uri uri));
766                debug_print (lazy (Printexc.to_string exn));
767                assert false
768             in
769            fun _ _ _ -> term))
770         uris
771
772 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
773
774     let disambiguate_thing ~dbd ~context ~metasenv
775       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
776       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
777     =
778       debug_print (lazy "DISAMBIGUATE INPUT");
779       let disambiguate_context =  (* cic context -> disambiguate context *)
780         List.map
781           (function None -> Cic.Anonymous | Some (name, _) -> name)
782           context
783       in
784       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
785       let thing_dom = domain_of_thing ~context:disambiguate_context thing in
786       debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"
787         (string_of_domain thing_dom)));
788 (*
789       debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
790         (DisambiguatePp.pp_environment aliases)));
791       debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
792         (match universe with None -> "None" | Some _ -> "Some _")));
793 *)
794       let current_dom =
795         Environment.fold (fun item _ dom -> item :: dom) aliases []
796       in
797       let todo_dom = domain_diff thing_dom current_dom in
798       (* (2) lookup function for any item (Id/Symbol/Num) *)
799       let lookup_choices =
800         fun item ->
801           let choices =
802             let lookup_in_library () =
803               match item with
804               | Id id -> choices_of_id dbd id
805               | Symbol (symb, _) ->
806                   List.map DisambiguateChoices.mk_choice
807                     (TermAcicContent.lookup_interpretations symb)
808               | Num instance ->
809                   DisambiguateChoices.lookup_num_choices ()
810             in
811             match universe with
812             | None -> lookup_in_library ()
813             | Some e ->
814                 (try
815                   let item =
816                     match item with
817                     | Symbol (symb, _) -> Symbol (symb, 0)
818                     | item -> item
819                   in
820                   Environment.find item e
821                 with Not_found -> [])
822           in
823           choices
824       in
825 (*
826       (* <benchmark> *)
827       let _ =
828         if benchmark then begin
829           let per_item_choices =
830             List.map
831               (fun dom_item ->
832                 try
833                   let len = List.length (lookup_choices dom_item) in
834                   debug_print (lazy (sprintf "BENCHMARK %s: %d"
835                     (string_of_domain_item dom_item) len));
836                   len
837                 with No_choices _ -> 0)
838               thing_dom
839           in
840           max_refinements := List.fold_left ( * ) 1 per_item_choices;
841           actual_refinements := 0;
842           domain_size := List.length thing_dom;
843           choices_avg :=
844             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
845         end
846       in
847       (* </benchmark> *)
848 *)
849
850       (* (3) test an interpretation filling with meta uninterpreted identifiers
851        *)
852       let test_env aliases todo_dom ugraph = 
853         let filled_env =
854           List.fold_left
855             (fun env item ->
856                Environment.add item
857                ("Implicit",
858                  (match item with
859                     | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
860                     | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
861             aliases todo_dom 
862         in
863         try
864           let localization_tbl = Cic.CicHash.create 503 in
865           let cic_thing =
866             interpretate_thing ~context:disambiguate_context ~env:filled_env
867              ~uri ~is_path:false thing ~localization_tbl
868           in
869 let foo () =
870           let k,ugraph1 =
871            refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
872           in
873             (k , ugraph1 )
874 in refine_profiler.HExtlib.profile foo ()
875         with
876         | Try_again msg -> Uncertain (None,msg), ugraph
877         | Invalid_choice msg -> Ko (None,msg), ugraph
878       in
879       (* (4) build all possible interpretations *)
880       let (@@) (l1,l2) (l1',l2') = l1@l1', l2@l2' in
881       let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ =
882         match todo_dom with
883         | [] ->
884             assert (lookup_in_todo_dom = None);
885             (match test_env aliases [] base_univ with
886             | Ok (thing, metasenv),new_univ -> 
887                [ aliases, diff, metasenv, thing, new_univ ], []
888             | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg])
889         | item :: remaining_dom ->
890             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
891              (string_of_domain_item item)));
892             let choices =
893              match lookup_in_todo_dom with
894                 None -> lookup_choices item
895               | Some choices -> choices in
896             match choices with
897                [] ->
898                 [], [None,lazy ("No choices for " ^ string_of_domain_item item)]
899              | [codomain_item] ->
900                  (* just one choice. We perform a one-step look-up and
901                     if the next set of choices is also a singleton we
902                     skip this refinement step *)
903                  debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
904                  let new_env = Environment.add item codomain_item aliases in
905                  let new_diff = (item,codomain_item)::diff in
906                  let lookup_in_todo_dom,next_choice_is_single =
907                   match remaining_dom with
908                      [] -> None,false
909                    | he::_ ->
910                       let choices = lookup_choices he in
911                        Some choices,List.length choices = 1
912                  in
913                   if next_choice_is_single then
914                    aux new_env new_diff lookup_in_todo_dom remaining_dom
915                     base_univ
916                   else
917                     (match test_env new_env remaining_dom base_univ with
918                     | Ok (thing, metasenv),new_univ ->
919                         (match remaining_dom with
920                         | [] ->
921                            [ new_env, new_diff, metasenv, thing, new_univ ], []
922                         | _ ->
923                            aux new_env new_diff lookup_in_todo_dom
924                             remaining_dom new_univ)
925                     | Uncertain (loc,msg),new_univ ->
926                         (match remaining_dom with
927                         | [] -> [], [loc,msg]
928                         | _ ->
929                            aux new_env new_diff lookup_in_todo_dom
930                             remaining_dom new_univ)
931                     | Ko (loc,msg),_ -> [], [loc,msg])
932              | _::_ ->
933                let rec filter univ = function 
934                 | [] -> [],[]
935                 | codomain_item :: tl ->
936                     debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
937                     let new_env = Environment.add item codomain_item aliases in
938                     let new_diff = (item,codomain_item)::diff in
939                     (match test_env new_env remaining_dom univ with
940                     | Ok (thing, metasenv),new_univ ->
941                         (match remaining_dom with
942                         | [] -> [ new_env, new_diff, metasenv, thing, new_univ ], []
943                         | _ -> aux new_env new_diff None remaining_dom new_univ
944                         ) @@ 
945                           filter univ tl
946                     | Uncertain (loc,msg),new_univ ->
947                         (match remaining_dom with
948                         | [] -> [],[loc,msg]
949                         | _ -> aux new_env new_diff None remaining_dom new_univ
950                         ) @@ 
951                           filter univ tl
952                     | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl)
953                in
954                 filter base_univ choices
955       in
956       let base_univ = initial_ugraph in
957       try
958         let res =
959          match aux aliases [] None todo_dom base_univ with
960          | [],errors -> raise (NoWellTypedInterpretation (0,errors))
961          | [_,diff,metasenv,t,ugraph],_ ->
962              debug_print (lazy "SINGLE INTERPRETATION");
963              [diff,metasenv,t,ugraph], false
964          | l,_ ->
965              debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
966              let choices =
967                List.map
968                  (fun (env, _, _, _, _) ->
969                    List.map
970                      (fun domain_item ->
971                        let description =
972                          fst (Environment.find domain_item env)
973                        in
974                        (descr_of_domain_item domain_item, description))
975                      thing_dom)
976                  l
977              in
978              let choosed = C.interactive_interpretation_choice choices in
979              (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
980               true
981         in
982          res
983      with
984       CicEnvironment.CircularDependency s -> 
985         failwith "Disambiguate: circular dependency"
986
987     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
988       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe term
989     =
990       let term =
991         if fresh_instances then CicNotationUtil.freshen_term term else term
992       in
993       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
994         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
995         ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term
996         ~refine_thing:refine_term term
997
998     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
999      obj
1000     =
1001       let obj =
1002         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
1003       in
1004       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
1005         ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj
1006         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
1007         obj
1008   end
1009