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