]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_disambiguation/disambiguate.ml
6b5e3f8332c60e21283486461032d020f12ac60d
[helm.git] / helm / ocaml / 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 open Printf
27
28 open DisambiguateTypes
29 open UriManager
30
31 exception No_choices of domain_item
32 exception NoWellTypedInterpretation
33 exception PathNotWellFormed
34
35   (** raised when an environment is not enough informative to decide *)
36 exception Try_again
37
38 let debug = false
39 let debug_print = if debug then prerr_endline else ignore
40
41 (*
42   (** print benchmark information *)
43 let benchmark = true
44 let max_refinements = ref 0       (* benchmarking is not thread safe *)
45 let actual_refinements = ref 0
46 let domain_size = ref 0
47 let choices_avg = ref 0.
48 *)
49
50 let descr_of_domain_item = function
51  | Id s -> s
52  | Symbol (s, _) -> s
53  | Num i -> string_of_int i
54
55 type 'a test_result =
56   | Ok of 'a * Cic.metasenv
57   | Ko
58   | Uncertain
59
60 let refine_term metasenv context uri term ugraph =
61 (*   if benchmark then incr actual_refinements; *)
62   assert (uri=None);
63   let metasenv, term = 
64     CicMkImplicit.expand_implicits metasenv [] context term in
65     debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
66     try
67       let term', _, metasenv',ugraph1 = 
68         CicRefine.type_of_aux' metasenv context term ugraph in
69         (Ok (term', metasenv')),ugraph1
70     with
71       | CicRefine.Uncertain s ->
72           debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term) ;
73           Uncertain,ugraph
74       | CicRefine.RefineFailure msg ->
75           debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
76             (CicPp.ppterm term) msg);
77           Ko,ugraph
78
79 let refine_obj metasenv context uri obj ugraph =
80  assert (context = []);
81  let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in
82    debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj));
83    try
84      let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
85        (Ok (obj', metasenv)),ugraph
86    with
87      | CicRefine.Uncertain s ->
88          debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj) ;
89          Uncertain,ugraph
90      | CicRefine.RefineFailure msg ->
91          debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
92            (CicPp.ppobj obj) msg);
93          Ko,ugraph
94
95 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
96   try
97     snd (Environment.find item env) env num args
98   with Not_found -> 
99     failwith ("Domain item not found: " ^ 
100       (DisambiguateTypes.string_of_domain_item item))
101
102   (* TODO move it to Cic *)
103 let find_in_environment name context =
104   let rec aux acc = function
105     | [] -> raise Not_found
106     | Cic.Name hd :: tl when hd = name -> acc
107     | _ :: tl ->  aux (acc + 1) tl
108   in
109   aux 1 context
110
111 let interpretate_term ~context ~env ~uri ~is_path ast =
112   assert (uri = None);
113   let rec aux loc context = function
114     | CicAst.AttributedTerm (`Loc loc, term) ->
115         aux loc context term
116     | CicAst.AttributedTerm (_, term) -> aux loc context term
117     | CicAst.Appl (CicAst.Symbol (symb, i) :: args) ->
118         let cic_args = List.map (aux loc context) args in
119         resolve env (Symbol (symb, i)) ~args:cic_args ()
120     | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
121     | CicAst.Binder (binder_kind, (var, typ), body) ->
122         let cic_type = aux_option loc context typ in
123         let cic_body = aux loc (var :: context) body in
124         (match binder_kind with
125         | `Lambda -> Cic.Lambda (var, cic_type, cic_body)
126         | `Pi | `Forall -> Cic.Prod (var, cic_type, cic_body)
127         | `Exists ->
128             resolve env (Symbol ("exists", 0))
129               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
130     | CicAst.Case (term, indty_ident, outtype, branches) ->
131         let cic_term = aux loc context term in
132         let cic_outtype = aux_option loc context outtype in
133         let do_branch ((head, args), term) =
134           let rec do_branch' context = function
135             | [] -> aux loc context term
136             | (name, typ) :: tl ->
137                 let cic_body = do_branch' (name :: context) tl in
138                 let typ =
139                   match typ with
140                   | None -> Cic.Implicit (Some `Type)
141                   | Some typ -> aux loc context typ
142                 in
143                 Cic.Lambda (name, typ, cic_body)
144           in
145           do_branch' context args
146         in
147         let (indtype_uri, indtype_no) =
148           match indty_ident with
149           | Some indty_ident ->
150               (match resolve env (Id indty_ident) () with
151               | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
152               | Cic.Implicit _ -> raise Try_again
153               | _ -> raise DisambiguateChoices.Invalid_choice)
154           | None ->
155               let fst_constructor =
156                 match branches with
157                 | ((head, _), _) :: _ -> head
158                 | [] -> raise DisambiguateChoices.Invalid_choice
159               in
160               (match resolve env (Id fst_constructor) () with
161               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
162                   (indtype_uri, indtype_no)
163               | Cic.Implicit _ -> raise Try_again
164               | _ -> raise DisambiguateChoices.Invalid_choice)
165         in
166         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
167           (List.map do_branch branches))
168     | CicAst.LetIn ((name, typ), def, body) ->
169         let cic_def = aux loc context def in
170         let cic_def =
171           match typ with
172           | None -> cic_def
173           | Some t -> Cic.Cast (cic_def, aux loc context t)
174         in
175         let cic_body = aux loc (name :: context) body in
176         Cic.LetIn (name, cic_def, cic_body)
177     | CicAst.LetRec (kind, defs, body) ->
178         let context' =
179           List.fold_left (fun acc ((name, _), _, _) -> name :: acc)
180             context defs
181         in
182         let cic_body = aux loc context' body in
183         let inductiveFuns =
184           List.map
185             (fun ((name, typ), body, decr_idx) ->
186               let cic_body = aux loc context' body in
187               let cic_type = aux_option loc context typ in
188               let name =
189                 match name with
190                 | Cic.Anonymous ->
191                     CicTextualParser2.fail loc
192                       "Recursive functions cannot be anonymous"
193                 | Cic.Name name -> name
194               in
195               (name, decr_idx, cic_type, cic_body))
196             defs
197         in
198         let counter = ref ~-1 in
199         let build_term funs =
200           (* this is the body of the fold_right function below. Rationale: Fix
201            * and CoFix cases differs only in an additional index in the
202            * inductiveFun list, see Cic.term *)
203           match kind with
204           | `Inductive ->
205               (fun (var, _, _, _) cic ->
206                 incr counter;
207                 Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
208           | `CoInductive ->
209               let funs =
210                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
211               in
212               (fun (var, _, _, _) cic ->
213                 incr counter;
214                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
215         in
216         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
217     | CicAst.Ident _
218     | CicAst.Uri _ when is_path -> raise PathNotWellFormed
219     | CicAst.Ident (name, subst)
220     | CicAst.Uri (name, subst) as ast ->
221         let is_uri = function CicAst.Uri _ -> true | _ -> false in
222         (try
223           if is_uri ast then raise Not_found;(* don't search the env for URIs *)
224           let index = find_in_environment name context in
225           if subst <> None then
226             CicTextualParser2.fail loc
227               "Explicit substitutions not allowed here";
228           Cic.Rel index
229         with Not_found ->
230           let cic =
231             if is_uri ast then  (* we have the URI, build the term out of it *)
232               try
233                 CicUtil.term_of_uri (UriManager.uri_of_string name)
234               with UriManager.IllFormedUri _ ->
235                 CicTextualParser2.fail loc "Ill formed URI"
236             else
237               resolve env (Id name) ()
238           in
239           let mk_subst uris =
240             let ids_to_uris =
241               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
242             in
243             (match subst with
244             | Some subst ->
245                 List.map
246                   (fun (s, term) ->
247                     (try
248                       List.assoc s ids_to_uris, aux loc context term
249                      with Not_found ->
250                        raise DisambiguateChoices.Invalid_choice))
251                   subst
252             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
253           in
254           (try 
255             match cic with
256             | Cic.Const (uri, []) ->
257                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
258                 let uris = CicUtil.params_of_obj o in
259                 Cic.Const (uri, mk_subst uris)
260             | Cic.Var (uri, []) ->
261                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
262                 let uris = CicUtil.params_of_obj o in
263                 Cic.Var (uri, mk_subst uris)
264             | Cic.MutInd (uri, i, []) ->
265                (try
266                  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
267                  let uris = CicUtil.params_of_obj o in
268                  Cic.MutInd (uri, i, mk_subst uris)
269                 with
270                  CicEnvironment.Object_not_found _ ->
271                   (* if we are here it is probably the case that during the
272                      definition of a mutual inductive type we have met an
273                      occurrence of the type in one of its constructors.
274                      However, the inductive type is not yet in the environment
275                   *)
276                   (*here the explicit_named_substituion is assumed to be of length 0 *)
277                   Cic.MutInd (uri,i,[]))
278             | Cic.MutConstruct (uri, i, j, []) ->
279                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
280                 let uris = CicUtil.params_of_obj o in
281                 Cic.MutConstruct (uri, i, j, mk_subst uris)
282             | Cic.Meta _ | Cic.Implicit _ as t ->
283 (*
284                 debug_print (sprintf
285                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
286                   (CicPp.ppterm t)
287                   (String.concat "; "
288                     (List.map
289                       (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term)
290                       subst)));
291 *)
292                 t
293             | _ ->
294               raise DisambiguateChoices.Invalid_choice
295            with 
296              CicEnvironment.CircularDependency _ -> 
297                raise DisambiguateChoices.Invalid_choice))
298     | CicAst.Implicit -> Cic.Implicit None
299     | CicAst.UserInput -> Cic.Implicit (Some `Hole)
300     | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
301     | CicAst.Meta (index, subst) ->
302         let cic_subst =
303           List.map
304             (function None -> None | Some term -> Some (aux loc context term))
305             subst
306         in
307         Cic.Meta (index, cic_subst)
308     | CicAst.Sort `Prop -> Cic.Sort Cic.Prop
309     | CicAst.Sort `Set -> Cic.Sort Cic.Set
310     | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
311     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
312     | CicAst.Symbol (symbol, instance) ->
313         resolve env (Symbol (symbol, instance)) ()
314   and aux_option loc context = function
315     | None -> Cic.Implicit (Some `Type)
316     | Some term -> aux loc context term
317   in
318   match ast with
319   | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
320   | term -> aux CicAst.dummy_floc context term
321
322 let interpretate_path ~context ~env path =
323  interpretate_term ~context ~env ~uri:None ~is_path:true path
324
325 let interpretate_obj ~context ~env ~uri ~is_path obj =
326  assert (context = []);
327  assert (is_path = false);
328  match obj with
329   | TacticAst.Inductive (params,tyl) ->
330      let uri = match uri with Some uri -> uri | None -> assert false in
331      let context,params =
332       let context,res =
333        List.fold_left
334         (fun (context,res) (name,t) ->
335           (Cic.Name name)::context,
336           (name, interpretate_term context env None false t)::res
337         ) ([],[]) params
338       in
339        context,List.rev res in
340      let add_params =
341       List.fold_right
342        (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
343      let name_to_uris =
344       snd (
345        List.fold_left
346         (*here the explicit_named_substituion is assumed to be of length 0 *)
347         (fun (i,res) (name,_,_,_) ->
348           i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
349         ) (0,[]) tyl) in
350      let con_env = DisambiguateTypes.env_of_list name_to_uris env in
351      let undebrujin t =
352       snd
353        (List.fold_right
354          (fun (name,_,_,_) (i,t) ->
355            (*here the explicit_named_substituion is assumed to be of length 0 *)
356            let t' = Cic.MutInd (uri,i,[])  in
357            let t = CicSubstitution.subst t' t in
358             i - 1,t
359          ) tyl (List.length tyl - 1,t)) in
360      let tyl =
361       List.map
362        (fun (name,b,ty,cl) ->
363          let ty' = add_params (interpretate_term context env None false ty) in
364          let cl' =
365           List.map
366            (fun (name,ty) ->
367              let ty' =
368               add_params (interpretate_term context con_env None false ty)
369              in
370               name,undebrujin ty'
371            ) cl
372          in
373           name,b,ty',cl'
374        ) tyl
375      in
376       Cic.InductiveDefinition (tyl,[],List.length params,[])
377   | TacticAst.Record (params,name,ty,fields) ->
378      let uri = match uri with Some uri -> uri | None -> assert false in
379      let context,params =
380       let context,res =
381        List.fold_left
382         (fun (context,res) (name,t) ->
383           (Cic.Name name)::context,
384           (name, interpretate_term context env None false t)::res
385         ) ([],[]) params
386       in
387        context,List.rev res in
388      let add_params =
389       List.fold_right
390        (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
391      let ty' = add_params (interpretate_term context env None false ty) in
392      let fields' =
393       snd (
394        List.fold_left
395         (fun (context,res) (name,ty) ->
396           let context' = (Cic.Name name)::context in
397            context',(name,interpretate_term context env None false ty)::res
398         ) (context,[]) fields) in
399      let concl =
400       (*here the explicit_named_substituion is assumed to be of length 0 *)
401       let mutind = Cic.MutInd (uri,0,[]) in
402       if params = [] then mutind
403       else
404        Cic.Appl
405         (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
406      let con =
407       List.fold_left
408        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
409        concl fields' in
410      let con' = add_params con in
411      let tyl = [name,true,ty',["mk_" ^ name,con']] in
412      let field_names = List.map fst fields in
413       Cic.InductiveDefinition
414        (tyl,[],List.length params,[`Class (`Record field_names)])
415   | TacticAst.Theorem (_,name,ty,bo) ->
416      let ty' = interpretate_term [] env None false ty in
417      match bo with
418         None ->
419          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],[])
420       | Some bo ->
421          let bo' = Some (interpretate_term [] env None false bo) in
422           Cic.Constant (name,bo',ty',[],[])
423
424   (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
425 let rev_uniq =
426   let module SortedItem =
427     struct
428       type t = DisambiguateTypes.domain_item
429       let compare = Pervasives.compare
430     end
431   in
432   let module Set = Set.Make (SortedItem) in
433   fun l ->
434     let rev_l = List.rev l in
435     let (_, uniq_rev_l) =
436       List.fold_left
437         (fun (members, rev_l) elt ->
438           if Set.mem elt members then
439             (members, rev_l)
440           else
441             Set.add elt members, elt :: rev_l)
442         (Set.empty, []) rev_l
443     in
444     List.rev uniq_rev_l
445
446 (* "aux" keeps domain in reverse order and doesn't care about duplicates.
447  * Domain item more in deep in the list will be processed first.
448  *)
449 let rec domain_rev_of_term ?(loc = CicAst.dummy_floc) context = function
450   | CicAst.AttributedTerm (`Loc loc, term) ->
451      domain_rev_of_term ~loc context term
452   | CicAst.AttributedTerm (_, term) -> domain_rev_of_term ~loc context term
453   | CicAst.Appl terms ->
454       List.fold_left
455        (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms
456   | CicAst.Binder (kind, (var, typ), body) ->
457       let kind_dom =
458         match kind with
459         | `Exists -> [ Symbol ("exists", 0) ]
460         | _ -> []
461       in
462       let type_dom = domain_rev_of_term_option loc context typ in
463       let body_dom = domain_rev_of_term ~loc (var :: context) body in
464       body_dom @ type_dom @ kind_dom
465   | CicAst.Case (term, indty_ident, outtype, branches) ->
466       let term_dom = domain_rev_of_term ~loc context term in
467       let outtype_dom = domain_rev_of_term_option loc context outtype in
468       let get_first_constructor = function
469         | [] -> []
470         | ((head, _), _) :: _ -> [ Id head ]
471       in
472       let do_branch ((head, args), term) =
473         let (term_context, args_domain) =
474           List.fold_left
475             (fun (cont, dom) (name, typ) ->
476               (name :: cont,
477                (match typ with
478                | None -> dom
479                | Some typ -> domain_rev_of_term ~loc cont typ @ dom)))
480             (context, []) args
481         in
482         args_domain @ domain_rev_of_term ~loc term_context term
483       in
484       let branches_dom =
485         List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
486       in
487       branches_dom @ outtype_dom @ term_dom @
488       (match indty_ident with
489        | None -> get_first_constructor branches
490        | Some ident -> [ Id ident ])
491   | CicAst.LetIn ((var, typ), body, where) ->
492       let body_dom = domain_rev_of_term ~loc context body in
493       let type_dom = domain_rev_of_term_option loc context typ in
494       let where_dom = domain_rev_of_term ~loc (var :: context) where in
495       where_dom @ type_dom @ body_dom
496   | CicAst.LetRec (kind, defs, where) ->
497       let context' =
498         List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
499           context defs
500       in
501       let where_dom = domain_rev_of_term ~loc context' where in
502       let defs_dom =
503         List.fold_left
504           (fun dom ((_, typ), body, _) ->
505             domain_rev_of_term ~loc context' body @
506             domain_rev_of_term_option loc context typ)
507           [] defs
508       in
509       where_dom @ defs_dom
510   | CicAst.Ident (name, subst) ->
511       (try
512         let index = find_in_environment name context in
513         if subst <> None then
514           CicTextualParser2.fail loc
515             "Explicit substitutions not allowed here"
516         else
517           []
518       with Not_found ->
519         (match subst with
520         | None -> [Id name]
521         | Some subst ->
522             List.fold_left
523               (fun dom (_, term) ->
524                 let dom' = domain_rev_of_term ~loc context term in
525                 dom' @ dom)
526               [Id name] subst))
527   | CicAst.Uri _ -> []
528   | CicAst.Implicit -> []
529   | CicAst.Num (num, i) -> [ Num i ]
530   | CicAst.Meta (index, local_context) ->
531       List.fold_left
532        (fun dom term -> domain_rev_of_term_option loc context term @ dom) []
533         local_context
534   | CicAst.Sort _ -> []
535   | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
536   | CicAst.UserInput -> assert false
537
538 and domain_rev_of_term_option loc context = function
539   | None -> []
540   | Some t -> domain_rev_of_term ~loc context t
541
542 let domain_of_term ~context ast =
543  rev_uniq (domain_rev_of_term context ast)
544
545 let domain_of_obj ~context ast =
546  assert (context = []);
547  let domain_rev =
548   match ast with
549    | TacticAst.Theorem (_,_,ty,bo) ->
550       (match bo with
551           None -> []
552         | Some bo -> domain_rev_of_term [] bo) @
553       domain_of_term [] ty
554    | TacticAst.Inductive (params,tyl) ->
555       let dom =
556        List.flatten (
557         List.rev_map
558          (fun (_,_,ty,cl) ->
559            List.flatten (
560             List.rev_map
561              (fun (_,ty) -> domain_rev_of_term [] ty) cl) @
562             domain_rev_of_term [] ty) tyl)
563       in
564        List.filter
565         (fun name ->
566           not (  List.exists (fun (name',_) -> name = Id name') params
567               || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
568         ) dom
569    | TacticAst.Record (params,_,ty,fields) ->
570       let dom =
571        List.flatten
572         (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
573       let dom' =
574        List.filter
575         (fun name->
576           not (  List.exists (fun (name',_) -> name = Id name') params
577               || List.exists (fun (name',_) -> name = Id name') fields)
578         ) dom
579       in
580        dom' @ domain_rev_of_term [] ty
581  in
582   rev_uniq domain_rev
583
584   (* dom1 \ dom2 *)
585 let domain_diff dom1 dom2 =
586 (* let domain_diff = Domain.diff *)
587   let is_in_dom2 =
588     List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
589       (fun _ -> false) dom2
590   in
591   List.filter (fun elt -> not (is_in_dom2 elt)) dom1
592
593 module type Disambiguator =
594 sig
595   val disambiguate_term :
596     dbd:Mysql.dbd ->
597     context:Cic.context ->
598     metasenv:Cic.metasenv ->
599     ?initial_ugraph:CicUniv.universe_graph -> 
600     aliases:environment ->  (* previous interpretation status *)
601     CicAst.term ->
602     (environment *                   (* new interpretation status *)
603      Cic.metasenv *                  (* new metasenv *)
604      Cic.term*
605      CicUniv.universe_graph) list    (* disambiguated term *)
606
607   val disambiguate_obj :
608     dbd:Mysql.dbd ->
609     aliases:environment ->           (* previous interpretation status *)
610     uri:UriManager.uri option ->     (* required only for inductive types *)
611     TacticAst.obj ->
612     (environment *                   (* new interpretation status *)
613      Cic.metasenv *                  (* new metasenv *)
614      Cic.obj *
615      CicUniv.universe_graph) list    (* disambiguated obj *)
616 end
617
618 module Make (C: Callbacks) =
619   struct
620     let choices_of_id dbd id =
621       let uris = MetadataQuery.locate ~dbd id in
622       let uris =
623        match uris with
624         | [] ->
625            [(C.input_or_locate_uri
626             ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
627         | [uri] -> [uri]
628         | _ ->
629             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
630              ~ok:"Try selected." ~enable_button_for_non_vars:true
631              ~title:"Ambiguous input." ~id
632              ~msg: ("Ambiguous input \"" ^ id ^
633                 "\". Please, choose one or more interpretations:")
634              uris
635       in
636       List.map
637         (fun uri ->
638           (UriManager.string_of_uri uri,
639            let term =
640              try
641                CicUtil.term_of_uri uri
642              with exn ->
643                debug_print (UriManager.string_of_uri uri);
644                debug_print (Printexc.to_string exn);
645                assert false
646             in
647            fun _ _ _ -> term))
648         uris
649
650     let disambiguate_thing ~dbd ~context ~metasenv
651       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
652       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
653     =
654       debug_print "NEW DISAMBIGUATE INPUT";
655       let disambiguate_context =  (* cic context -> disambiguate context *)
656         List.map
657           (function None -> Cic.Anonymous | Some (name, _) -> name)
658           context
659       in
660       debug_print ("TERM IS: " ^ (pp_thing thing));
661       let thing_dom = domain_of_thing ~context:disambiguate_context thing in
662       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
663         (string_of_domain thing_dom));
664       let current_dom =
665         Environment.fold (fun item _ dom -> item :: dom) current_env []
666       in
667       let todo_dom = domain_diff thing_dom current_dom in
668       (* (2) lookup function for any item (Id/Symbol/Num) *)
669       let lookup_choices =
670         let id_choices = Hashtbl.create 1023 in
671         fun item ->
672         let choices =
673           match item with
674           | Id id ->
675               (try
676                 Hashtbl.find id_choices id
677               with Not_found ->
678                 let choices = choices_of_id dbd id in
679                 Hashtbl.add id_choices id choices;
680                 choices)
681           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
682           | Num instance -> DisambiguateChoices.lookup_num_choices ()
683         in
684         if choices = [] then raise (No_choices item);
685         choices
686       in
687
688 (*
689       (* <benchmark> *)
690       let _ =
691         if benchmark then begin
692           let per_item_choices =
693             List.map
694               (fun dom_item ->
695                 try
696                   let len = List.length (lookup_choices dom_item) in
697                   debug_print (sprintf "BENCHMARK %s: %d"
698                     (string_of_domain_item dom_item) len);
699                   len
700                 with No_choices _ -> 0)
701               thing_dom
702           in
703           max_refinements := List.fold_left ( * ) 1 per_item_choices;
704           actual_refinements := 0;
705           domain_size := List.length thing_dom;
706           choices_avg :=
707             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
708         end
709       in
710       (* </benchmark> *)
711 *)
712
713       (* (3) test an interpretation filling with meta uninterpreted identifiers
714        *)
715       let test_env current_env todo_dom ugraph = 
716         let filled_env =
717           List.fold_left
718             (fun env item ->
719                Environment.add item
720                ("Implicit",
721                  (match item with
722                     | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
723                     | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
724             current_env todo_dom 
725         in
726         try
727           let cic_thing =
728             interpretate_thing ~context:disambiguate_context ~env:filled_env
729              ~uri ~is_path:false thing
730           in
731           let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
732             (k , ugraph1 )
733         with
734         | Try_again -> Uncertain,ugraph
735         | DisambiguateChoices.Invalid_choice -> Ko,ugraph
736       in
737       (* (4) build all possible interpretations *)
738       let rec aux current_env todo_dom base_univ =
739         match todo_dom with
740         | [] ->
741             (match test_env current_env [] base_univ with
742             | Ok (thing, metasenv),new_univ -> 
743                [ current_env, metasenv, thing, new_univ ]
744             | Ko,_ | Uncertain,_ -> [])
745         | item :: remaining_dom ->
746             debug_print (sprintf "CHOOSED ITEM: %s"
747              (string_of_domain_item item));
748             let choices = lookup_choices item in
749             let rec filter univ = function 
750               | [] -> []
751               | codomain_item :: tl ->
752                   debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
753                   let new_env =
754                     Environment.add item codomain_item current_env
755                   in
756                   (match test_env new_env remaining_dom univ with
757                   | Ok (thing, metasenv),new_univ ->
758                       (match remaining_dom with
759                       | [] -> [ new_env, metasenv, thing, new_univ ]
760                       | _ -> aux new_env remaining_dom new_univ )@ 
761                         filter univ tl
762                   | Uncertain,new_univ ->
763                       (match remaining_dom with
764                       | [] -> []
765                       | _ -> aux new_env remaining_dom new_univ )@ 
766                         filter univ tl
767                   | Ko,_ -> filter univ tl)
768             in
769             filter base_univ choices 
770       in
771       let base_univ = initial_ugraph in
772       try
773         let res =
774          match aux current_env todo_dom base_univ with
775          | [] -> raise NoWellTypedInterpretation
776          | [ e,me,t,u ] as l ->
777              debug_print "UNA SOLA SCELTA";
778              [ e,me,t,u]
779          | l ->
780              debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
781              let choices =
782                List.map
783                  (fun (env, _, _, _) ->
784                    List.map
785                      (fun domain_item ->
786                        let description =
787                          fst (Environment.find domain_item env)
788                        in
789                        (descr_of_domain_item domain_item, description))
790                      thing_dom)
791                  l
792              in
793              let choosed = C.interactive_interpretation_choice choices in
794              List.map (List.nth l) choosed
795         in
796 (*
797         (if benchmark then
798           let res_size = List.length res in
799           debug_print (sprintf
800             ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
801             "BENCHMARK:   estimated %.2f")
802             !actual_refinements !max_refinements !domain_size res_size
803             !choices_avg
804             (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)));
805 *)
806         res
807      with
808       CicEnvironment.CircularDependency s -> 
809         failwith "Disambiguate: circular dependency"
810
811     let disambiguate_term ~dbd ~context ~metasenv
812       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term
813     =
814      disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
815       ~uri:None ~pp_thing:CicAstPp.pp_term ~domain_of_thing:domain_of_term
816       ~interpretate_thing:interpretate_term ~refine_thing:refine_term term
817
818     let disambiguate_obj ~dbd ~aliases ~uri obj =
819      disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
820       ~pp_thing:TacticAstPp.pp_obj ~domain_of_thing:domain_of_obj
821       ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
822       obj
823   end
824
825 module Trivial =
826 struct
827   exception Ambiguous_term of string
828   exception Exit
829   module Callbacks =
830   struct
831     let interactive_user_uri_choice ~selection_mode ?ok
832           ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
833               raise Exit
834     let interactive_interpretation_choice interp = raise Exit
835     let input_or_locate_uri ~(title:string) ?id = raise Exit
836   end
837   module Disambiguator = Make (Callbacks)
838   let disambiguate_string ~dbd ?(context=[]) ?(metasenv=[]) ?initial_ugraph
839         ?(aliases=DisambiguateTypes.Environment.empty) term =
840     let ast = CicTextualParser2.parse_term (Stream.of_string term) in
841     try
842       Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
843         ?initial_ugraph ~aliases
844     with Exit -> raise (Ambiguous_term term)
845 end
846