]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_disambiguation/disambiguate.ml
added Variant theorem flavour
[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 (Some `Type) 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 None 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 (Some `Type) 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 annotation = function
315     | None -> Cic.Implicit annotation
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 (flavour, name, ty, bo) ->
416      let attrs = [`Flavour flavour] in
417      let ty' = interpretate_term [] env None false ty in
418      (match bo with
419         None ->
420          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
421       | Some bo ->
422          let bo' = Some (interpretate_term [] env None false bo) in
423           Cic.Constant (name,bo',ty',[],attrs))
424           
425
426   (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
427 let rev_uniq =
428   let module SortedItem =
429     struct
430       type t = DisambiguateTypes.domain_item
431       let compare = Pervasives.compare
432     end
433   in
434   let module Set = Set.Make (SortedItem) in
435   fun l ->
436     let rev_l = List.rev l in
437     let (_, uniq_rev_l) =
438       List.fold_left
439         (fun (members, rev_l) elt ->
440           if Set.mem elt members then
441             (members, rev_l)
442           else
443             Set.add elt members, elt :: rev_l)
444         (Set.empty, []) rev_l
445     in
446     List.rev uniq_rev_l
447
448 (* "aux" keeps domain in reverse order and doesn't care about duplicates.
449  * Domain item more in deep in the list will be processed first.
450  *)
451 let rec domain_rev_of_term ?(loc = CicAst.dummy_floc) context = function
452   | CicAst.AttributedTerm (`Loc loc, term) ->
453      domain_rev_of_term ~loc context term
454   | CicAst.AttributedTerm (_, term) -> domain_rev_of_term ~loc context term
455   | CicAst.Appl terms ->
456       List.fold_left
457        (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms
458   | CicAst.Binder (kind, (var, typ), body) ->
459       let kind_dom =
460         match kind with
461         | `Exists -> [ Symbol ("exists", 0) ]
462         | _ -> []
463       in
464       let type_dom = domain_rev_of_term_option loc context typ in
465       let body_dom = domain_rev_of_term ~loc (var :: context) body in
466       body_dom @ type_dom @ kind_dom
467   | CicAst.Case (term, indty_ident, outtype, branches) ->
468       let term_dom = domain_rev_of_term ~loc context term in
469       let outtype_dom = domain_rev_of_term_option loc context outtype in
470       let get_first_constructor = function
471         | [] -> []
472         | ((head, _), _) :: _ -> [ Id head ]
473       in
474       let do_branch ((head, args), term) =
475         let (term_context, args_domain) =
476           List.fold_left
477             (fun (cont, dom) (name, typ) ->
478               (name :: cont,
479                (match typ with
480                | None -> dom
481                | Some typ -> domain_rev_of_term ~loc cont typ @ dom)))
482             (context, []) args
483         in
484         args_domain @ domain_rev_of_term ~loc term_context term
485       in
486       let branches_dom =
487         List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
488       in
489       branches_dom @ outtype_dom @ term_dom @
490       (match indty_ident with
491        | None -> get_first_constructor branches
492        | Some ident -> [ Id ident ])
493   | CicAst.LetIn ((var, typ), body, where) ->
494       let body_dom = domain_rev_of_term ~loc context body in
495       let type_dom = domain_rev_of_term_option loc context typ in
496       let where_dom = domain_rev_of_term ~loc (var :: context) where in
497       where_dom @ type_dom @ body_dom
498   | CicAst.LetRec (kind, defs, where) ->
499       let context' =
500         List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
501           context defs
502       in
503       let where_dom = domain_rev_of_term ~loc context' where in
504       let defs_dom =
505         List.fold_left
506           (fun dom ((_, typ), body, _) ->
507             domain_rev_of_term ~loc context' body @
508             domain_rev_of_term_option loc context typ)
509           [] defs
510       in
511       where_dom @ defs_dom
512   | CicAst.Ident (name, subst) ->
513       (try
514         let index = find_in_environment name context in
515         if subst <> None then
516           CicTextualParser2.fail loc
517             "Explicit substitutions not allowed here"
518         else
519           []
520       with Not_found ->
521         (match subst with
522         | None -> [Id name]
523         | Some subst ->
524             List.fold_left
525               (fun dom (_, term) ->
526                 let dom' = domain_rev_of_term ~loc context term in
527                 dom' @ dom)
528               [Id name] subst))
529   | CicAst.Uri _ -> []
530   | CicAst.Implicit -> []
531   | CicAst.Num (num, i) -> [ Num i ]
532   | CicAst.Meta (index, local_context) ->
533       List.fold_left
534        (fun dom term -> domain_rev_of_term_option loc context term @ dom) []
535         local_context
536   | CicAst.Sort _ -> []
537   | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
538   | CicAst.UserInput -> assert false
539
540 and domain_rev_of_term_option loc context = function
541   | None -> []
542   | Some t -> domain_rev_of_term ~loc context t
543
544 let domain_of_term ~context ast =
545  rev_uniq (domain_rev_of_term context ast)
546
547 let domain_of_obj ~context ast =
548  assert (context = []);
549  let domain_rev =
550   match ast with
551    | TacticAst.Theorem (_,_,ty,bo) ->
552       (match bo with
553           None -> []
554         | Some bo -> domain_rev_of_term [] bo) @
555       domain_of_term [] ty
556    | TacticAst.Inductive (params,tyl) ->
557       let dom =
558        List.flatten (
559         List.rev_map
560          (fun (_,_,ty,cl) ->
561            List.flatten (
562             List.rev_map
563              (fun (_,ty) -> domain_rev_of_term [] ty) cl) @
564             domain_rev_of_term [] ty) tyl)
565       in
566        List.filter
567         (fun name ->
568           not (  List.exists (fun (name',_) -> name = Id name') params
569               || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
570         ) dom
571    | TacticAst.Record (params,_,ty,fields) ->
572       let dom =
573        List.flatten
574         (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
575       let dom' =
576        List.filter
577         (fun name->
578           not (  List.exists (fun (name',_) -> name = Id name') params
579               || List.exists (fun (name',_) -> name = Id name') fields)
580         ) dom
581       in
582        dom' @ domain_rev_of_term [] ty
583  in
584   rev_uniq domain_rev
585
586   (* dom1 \ dom2 *)
587 let domain_diff dom1 dom2 =
588 (* let domain_diff = Domain.diff *)
589   let is_in_dom2 =
590     List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
591       (fun _ -> false) dom2
592   in
593   List.filter (fun elt -> not (is_in_dom2 elt)) dom1
594
595 module type Disambiguator =
596 sig
597   val disambiguate_term :
598     dbd:Mysql.dbd ->
599     context:Cic.context ->
600     metasenv:Cic.metasenv ->
601     ?initial_ugraph:CicUniv.universe_graph -> 
602     aliases:environment ->  (* previous interpretation status *)
603     CicAst.term ->
604     (environment *                   (* new interpretation status *)
605      Cic.metasenv *                  (* new metasenv *)
606      Cic.term*
607      CicUniv.universe_graph) list    (* disambiguated term *)
608
609   val disambiguate_obj :
610     dbd:Mysql.dbd ->
611     aliases:environment ->           (* previous interpretation status *)
612     uri:UriManager.uri option ->     (* required only for inductive types *)
613     TacticAst.obj ->
614     (environment *                   (* new interpretation status *)
615      Cic.metasenv *                  (* new metasenv *)
616      Cic.obj *
617      CicUniv.universe_graph) list    (* disambiguated obj *)
618 end
619
620 module Make (C: Callbacks) =
621   struct
622     let choices_of_id dbd id =
623       let uris = MetadataQuery.locate ~dbd id in
624       let uris =
625        match uris with
626         | [] ->
627            [(C.input_or_locate_uri
628             ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
629         | [uri] -> [uri]
630         | _ ->
631             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
632              ~ok:"Try selected." ~enable_button_for_non_vars:true
633              ~title:"Ambiguous input." ~id
634              ~msg: ("Ambiguous input \"" ^ id ^
635                 "\". Please, choose one or more interpretations:")
636              uris
637       in
638       List.map
639         (fun uri ->
640           (UriManager.string_of_uri uri,
641            let term =
642              try
643                CicUtil.term_of_uri uri
644              with exn ->
645                debug_print (UriManager.string_of_uri uri);
646                debug_print (Printexc.to_string exn);
647                assert false
648             in
649            fun _ _ _ -> term))
650         uris
651
652     let disambiguate_thing ~dbd ~context ~metasenv
653       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
654       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
655     =
656       debug_print "NEW DISAMBIGUATE INPUT";
657       let disambiguate_context =  (* cic context -> disambiguate context *)
658         List.map
659           (function None -> Cic.Anonymous | Some (name, _) -> name)
660           context
661       in
662       debug_print ("TERM IS: " ^ (pp_thing thing));
663       let thing_dom = domain_of_thing ~context:disambiguate_context thing in
664       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
665         (string_of_domain thing_dom));
666       let current_dom =
667         Environment.fold (fun item _ dom -> item :: dom) current_env []
668       in
669       let todo_dom = domain_diff thing_dom current_dom in
670       (* (2) lookup function for any item (Id/Symbol/Num) *)
671       let lookup_choices =
672         let id_choices = Hashtbl.create 1023 in
673         fun item ->
674         let choices =
675           match item with
676           | Id id ->
677               (try
678                 Hashtbl.find id_choices id
679               with Not_found ->
680                 let choices = choices_of_id dbd id in
681                 Hashtbl.add id_choices id choices;
682                 choices)
683           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
684           | Num instance -> DisambiguateChoices.lookup_num_choices ()
685         in
686         if choices = [] then raise (No_choices item);
687         choices
688       in
689
690 (*
691       (* <benchmark> *)
692       let _ =
693         if benchmark then begin
694           let per_item_choices =
695             List.map
696               (fun dom_item ->
697                 try
698                   let len = List.length (lookup_choices dom_item) in
699                   debug_print (sprintf "BENCHMARK %s: %d"
700                     (string_of_domain_item dom_item) len);
701                   len
702                 with No_choices _ -> 0)
703               thing_dom
704           in
705           max_refinements := List.fold_left ( * ) 1 per_item_choices;
706           actual_refinements := 0;
707           domain_size := List.length thing_dom;
708           choices_avg :=
709             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
710         end
711       in
712       (* </benchmark> *)
713 *)
714
715       (* (3) test an interpretation filling with meta uninterpreted identifiers
716        *)
717       let test_env current_env todo_dom ugraph = 
718         let filled_env =
719           List.fold_left
720             (fun env item ->
721                Environment.add item
722                ("Implicit",
723                  (match item with
724                     | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
725                     | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
726             current_env todo_dom 
727         in
728         try
729           let cic_thing =
730             interpretate_thing ~context:disambiguate_context ~env:filled_env
731              ~uri ~is_path:false thing
732           in
733           let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
734             (k , ugraph1 )
735         with
736         | Try_again -> Uncertain,ugraph
737         | DisambiguateChoices.Invalid_choice -> Ko,ugraph
738       in
739       (* (4) build all possible interpretations *)
740       let rec aux current_env todo_dom base_univ =
741         match todo_dom with
742         | [] ->
743             (match test_env current_env [] base_univ with
744             | Ok (thing, metasenv),new_univ -> 
745                [ current_env, metasenv, thing, new_univ ]
746             | Ko,_ | Uncertain,_ -> [])
747         | item :: remaining_dom ->
748             debug_print (sprintf "CHOOSED ITEM: %s"
749              (string_of_domain_item item));
750             let choices = lookup_choices item in
751             let rec filter univ = function 
752               | [] -> []
753               | codomain_item :: tl ->
754                   debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
755                   let new_env =
756                     Environment.add item codomain_item current_env
757                   in
758                   (match test_env new_env remaining_dom univ with
759                   | Ok (thing, metasenv),new_univ ->
760                       (match remaining_dom with
761                       | [] -> [ new_env, metasenv, thing, new_univ ]
762                       | _ -> aux new_env remaining_dom new_univ )@ 
763                         filter univ tl
764                   | Uncertain,new_univ ->
765                       (match remaining_dom with
766                       | [] -> []
767                       | _ -> aux new_env remaining_dom new_univ )@ 
768                         filter univ tl
769                   | Ko,_ -> filter univ tl)
770             in
771             filter base_univ choices 
772       in
773       let base_univ = initial_ugraph in
774       try
775         let res =
776          match aux current_env todo_dom base_univ with
777          | [] -> raise NoWellTypedInterpretation
778          | [ e,me,t,u ] as l ->
779              debug_print "UNA SOLA SCELTA";
780              [ e,me,t,u]
781          | l ->
782              debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
783              let choices =
784                List.map
785                  (fun (env, _, _, _) ->
786                    List.map
787                      (fun domain_item ->
788                        let description =
789                          fst (Environment.find domain_item env)
790                        in
791                        (descr_of_domain_item domain_item, description))
792                      thing_dom)
793                  l
794              in
795              let choosed = C.interactive_interpretation_choice choices in
796              List.map (List.nth l) choosed
797         in
798 (*
799         (if benchmark then
800           let res_size = List.length res in
801           debug_print (sprintf
802             ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
803             "BENCHMARK:   estimated %.2f")
804             !actual_refinements !max_refinements !domain_size res_size
805             !choices_avg
806             (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)));
807 *)
808         res
809      with
810       CicEnvironment.CircularDependency s -> 
811         failwith "Disambiguate: circular dependency"
812
813     let disambiguate_term ~dbd ~context ~metasenv
814       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term
815     =
816      disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
817       ~uri:None ~pp_thing:CicAstPp.pp_term ~domain_of_thing:domain_of_term
818       ~interpretate_thing:interpretate_term ~refine_thing:refine_term term
819
820     let disambiguate_obj ~dbd ~aliases ~uri obj =
821      disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
822       ~pp_thing:TacticAstPp.pp_obj ~domain_of_thing:domain_of_obj
823       ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
824       obj
825   end
826
827 module Trivial =
828 struct
829   exception Ambiguous_term of string
830   exception Exit
831   module Callbacks =
832   struct
833     let interactive_user_uri_choice ~selection_mode ?ok
834           ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
835               raise Exit
836     let interactive_interpretation_choice interp = raise Exit
837     let input_or_locate_uri ~(title:string) ?id = raise Exit
838   end
839   module Disambiguator = Make (Callbacks)
840   let disambiguate_string ~dbd ?(context=[]) ?(metasenv=[]) ?initial_ugraph
841         ?(aliases=DisambiguateTypes.Environment.empty) term =
842     let ast = CicTextualParser2.parse_term (Stream.of_string term) in
843     try
844       Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
845         ?initial_ugraph ~aliases
846     with Exit -> raise (Ambiguous_term term)
847 end
848