]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_disambiguation/disambiguate.ml
added dummy entry in CicAst: UserInput
[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
34   (** raised when an environment is not enough informative to decide *)
35 exception Try_again
36
37 let debug = false
38 let debug_print = if debug then prerr_endline else ignore
39
40 (*
41   (** print benchmark information *)
42 let benchmark = true
43 let max_refinements = ref 0       (* benchmarking is not thread safe *)
44 let actual_refinements = ref 0
45 let domain_size = ref 0
46 let choices_avg = ref 0.
47 *)
48
49 let descr_of_domain_item = function
50  | Id s -> s
51  | Symbol (s, _) -> s
52  | Num i -> string_of_int i
53
54 type test_result =
55   | Ok of Cic.term * Cic.metasenv
56   | Ko
57   | Uncertain
58
59 let refine metasenv context term =
60 (*   if benchmark then incr actual_refinements; *)
61   let metasenv, term = CicMkImplicit.expand_implicits metasenv [] context term in
62   debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
63   try
64     let term', _, metasenv' = CicRefine.type_of_aux' metasenv context term in
65     Ok (term', metasenv')
66   with
67     | CicRefine.Uncertain _ ->
68         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
69         Uncertain
70     | CicRefine.RefineFailure _ ->
71         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
72         Ko
73
74 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
75   try
76     snd (Environment.find item env) env num args
77   with Not_found -> assert false
78
79   (* TODO move it to Cic *)
80 let find_in_environment name context =
81   let rec aux acc = function
82     | [] -> raise Not_found
83     | Cic.Name hd :: tl when hd = name -> acc
84     | _ :: tl ->  aux (acc + 1) tl
85   in
86   aux 1 context
87
88 let interpretate ~context ~env ast =
89   let rec aux loc context = function
90     | CicAst.AttributedTerm (`Loc loc, term) ->
91         aux loc context term
92     | CicAst.AttributedTerm (_, term) -> aux loc context term
93     | CicAst.Appl (CicAst.Symbol (symb, i) :: args) ->
94         let cic_args = List.map (aux loc context) args in
95         resolve env (Symbol (symb, i)) ~args:cic_args ()
96     | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
97     | CicAst.Binder (binder_kind, (var, typ), body) ->
98         let cic_type = aux_option loc context typ in
99         let cic_body = aux loc (var :: context) body in
100         (match binder_kind with
101         | `Lambda -> Cic.Lambda (var, cic_type, cic_body)
102         | `Pi | `Forall -> Cic.Prod (var, cic_type, cic_body)
103         | `Exists ->
104             resolve env (Symbol ("exists", 0))
105               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
106     | CicAst.Case (term, indty_ident, outtype, branches) ->
107         let cic_term = aux loc context term in
108         let cic_outtype = aux_option loc context outtype in
109         let do_branch ((head, args), term) =
110           let rec do_branch' context = function
111             | [] -> aux loc context term
112             | (name, typ) :: tl ->
113                 let cic_body = do_branch' (name :: context) tl in
114                 let typ =
115                   match typ with
116                   | None -> Cic.Implicit (Some `Type)
117                   | Some typ -> aux loc context typ
118                 in
119                 Cic.Lambda (name, typ, cic_body)
120           in
121           do_branch' context args
122         in
123         let (indtype_uri, indtype_no) =
124           match indty_ident with
125           | Some indty_ident ->
126               (match resolve env (Id indty_ident) () with
127               | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
128               | Cic.Implicit _ -> raise Try_again
129               | _ -> raise DisambiguateChoices.Invalid_choice)
130           | None ->
131               let fst_constructor =
132                 match branches with
133                 | ((head, _), _) :: _ -> head
134                 | [] -> raise DisambiguateChoices.Invalid_choice
135               in
136               (match resolve env (Id fst_constructor) () with
137               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
138                   (indtype_uri, indtype_no)
139               | Cic.Implicit _ -> raise Try_again
140               | _ -> raise DisambiguateChoices.Invalid_choice)
141         in
142         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
143           (List.map do_branch branches))
144     | CicAst.LetIn ((name, typ), def, body) ->
145         let cic_def = aux loc context def in
146         let cic_def =
147           match typ with
148           | None -> cic_def
149           | Some t -> Cic.Cast (cic_def, aux loc context t)
150         in
151         let cic_body = aux loc (name :: context) body in
152         Cic.LetIn (name, cic_def, cic_body)
153     | CicAst.LetRec (kind, defs, body) ->
154         let context' =
155           List.fold_left (fun acc ((name, _), _, _) -> name :: acc)
156             context defs
157         in
158         let cic_body = aux loc context' body in
159         let inductiveFuns =
160           List.map
161             (fun ((name, typ), body, decr_idx) ->
162               let cic_body = aux loc context' body in
163               let cic_type = aux_option loc context typ in
164               let name =
165                 match name with
166                 | Cic.Anonymous ->
167                     CicTextualParser2.fail loc
168                       "Recursive functions cannot be anonymous"
169                 | Cic.Name name -> name
170               in
171               (name, decr_idx, cic_type, cic_body))
172             defs
173         in
174         let counter = ref ~-1 in
175         let build_term funs =
176           (* this is the body of the fold_right function below. Rationale: Fix
177            * and CoFix cases differs only in an additional index in the
178            * inductiveFun list, see Cic.term *)
179           match kind with
180           | `Inductive ->
181               (fun (var, _, _, _) cic ->
182                 incr counter;
183                 Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
184           | `CoInductive ->
185               let funs =
186                 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
187               in
188               (fun (var, _, _, _) cic ->
189                 incr counter;
190                 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
191         in
192         List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
193     | CicAst.Ident (name, subst) ->
194         (try
195           let index = find_in_environment name context in
196           if subst <> None then
197             CicTextualParser2.fail loc
198               "Explicit substitutions not allowed here";
199           Cic.Rel index
200         with Not_found ->
201           let cic = resolve env (Id name) () in
202           let mk_subst uris =
203             let ids_to_uris =
204               List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
205             in
206             (match subst with
207             | Some subst ->
208                 List.map
209                   (fun (s, term) ->
210                     (try
211                       List.assoc s ids_to_uris, aux loc context term
212                      with Not_found ->
213                        raise DisambiguateChoices.Invalid_choice))
214                   subst
215             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
216           in
217           (* the try is for CicTypeChecker.typecheck *)
218           (try 
219             match cic with
220             | Cic.Const (uri, []) ->
221                 let uris =
222                   match CicEnvironment.get_obj uri with
223                   (*match CicTypeChecker.typecheck uri with*)
224                   | Cic.Constant (_, _, _, uris) -> uris
225                   | _ -> assert false
226                 in
227                 Cic.Const (uri, mk_subst uris)
228             | Cic.Var (uri, []) ->
229                 let uris =
230                   match CicEnvironment.get_obj uri with
231                   (*match CicTypeChecker.typecheck uri with*)
232                   | Cic.Variable (_, _, _, uris) -> uris
233                   | _ -> assert false
234                 in
235                 Cic.Var (uri, mk_subst uris)
236             | Cic.MutInd (uri, i, []) ->
237                 let uris =
238                   match CicEnvironment.get_obj uri with
239                   (*match CicTypeChecker.typecheck uri with*)
240                   | Cic.InductiveDefinition (_, uris, _) -> uris
241                   | _ -> assert false
242                 in
243                 Cic.MutInd (uri, i, mk_subst uris)
244             | Cic.MutConstruct (uri, i, j, []) ->
245                 let uris =
246                   match CicEnvironment.get_obj uri with
247                   (*match CicTypeChecker.typecheck uri with*)
248                   | Cic.InductiveDefinition (_, uris, _) -> uris
249                   | _ -> assert false
250                 in
251                 Cic.MutConstruct (uri, i, j, mk_subst uris)
252             | Cic.Meta _ | Cic.Implicit _ as t ->
253 (*
254                 prerr_endline (sprintf
255                   "Warning: %s must be instantiated with _[%s] but we do not enforce it"
256                   (CicPp.ppterm t)
257                   (String.concat "; "
258                     (List.map
259                       (fun (s, term) -> s ^ " := " ^ CicAstPp.pp_term term)
260                       subst)));
261 *)
262                 t
263             | _ ->
264               raise DisambiguateChoices.Invalid_choice
265            with 
266              CicEnvironment.CircularDependency _ -> 
267                raise DisambiguateChoices.Invalid_choice))
268     | CicAst.Implicit -> Cic.Implicit None
269     | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
270     | CicAst.Meta (index, subst) ->
271         let cic_subst =
272           List.map
273             (function None -> None | Some term -> Some (aux loc context term))
274             subst
275         in
276         Cic.Meta (index, cic_subst)
277     | CicAst.Sort `Prop -> Cic.Sort Cic.Prop
278     | CicAst.Sort `Set -> Cic.Sort Cic.Set
279     | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
280     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
281     | CicAst.Symbol (symbol, instance) ->
282         resolve env (Symbol (symbol, instance)) ()
283     | CicAst.UserInput -> assert false
284   and aux_option loc context = function
285     | None -> Cic.Implicit (Some `Type)
286     | Some term -> aux loc context term
287   in
288   match ast with
289   | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
290   | term -> aux CicAst.dummy_floc context term
291
292 let domain_of_term ~context ast =
293     (* "aux" keeps domain in reverse order and doesn't care about duplicates.
294      * Domain item more in deep in the list will be processed first.
295      *)
296   let rec aux loc context = function
297     | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
298     | CicAst.AttributedTerm (_, term) -> aux loc context term
299     | CicAst.Appl terms ->
300         List.fold_left (fun dom term -> aux loc context term @ dom) [] terms
301     | CicAst.Binder (kind, (var, typ), body) ->
302         let kind_dom =
303           match kind with
304           | `Exists -> [ Symbol ("exists", 0) ]
305           | _ -> []
306         in
307         let type_dom = aux_option loc context typ in
308         let body_dom = aux loc (var :: context) body in
309         body_dom @ type_dom @ kind_dom
310     | CicAst.Case (term, indty_ident, outtype, branches) ->
311         let term_dom = aux loc context term in
312         let outtype_dom = aux_option loc context outtype in
313         let do_branch ((head, args), term) =
314           let (term_context, args_domain) =
315             List.fold_left
316               (fun (cont, dom) (name, typ) ->
317                 (name :: cont,
318                  (match typ with
319                  | None -> dom
320                  | Some typ -> aux loc cont typ @ dom)))
321               (context, []) args
322           in
323           args_domain @ aux loc term_context term
324         in
325         let branches_dom =
326           List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
327         in
328         branches_dom @ outtype_dom @ term_dom @
329         (match indty_ident with None -> [] | Some ident -> [ Id ident ])
330     | CicAst.LetIn ((var, typ), body, where) ->
331         let body_dom = aux loc context body in
332         let type_dom = aux_option loc context typ in
333         let where_dom = aux loc (var :: context) where in
334         where_dom @ type_dom @ body_dom
335     | CicAst.LetRec (kind, defs, where) ->
336         let context' =
337           List.fold_left (fun acc ((var, typ), _, _) -> var :: acc)
338             context defs
339         in
340         let where_dom = aux loc context' where in
341         let defs_dom =
342           List.fold_left
343             (fun dom ((_, typ), body, _) ->
344               aux loc context' body @ aux_option loc context typ)
345             [] defs
346         in
347         where_dom @ defs_dom
348     | CicAst.Ident (name, subst) ->
349         (try
350           let index = find_in_environment name context in
351           if subst <> None then
352             CicTextualParser2.fail loc
353               "Explicit substitutions not allowed here"
354           else
355             []
356         with Not_found ->
357           (match subst with
358           | None -> [Id name]
359           | Some subst ->
360               List.fold_left
361                 (fun dom (_, term) ->
362                   let dom' = aux loc context term in
363                   dom' @ dom)
364                 [Id name] subst))
365     | CicAst.Implicit -> []
366     | CicAst.Num (num, i) -> [ Num i ]
367     | CicAst.Meta (index, local_context) ->
368         List.fold_left (fun dom term -> aux_option loc context term @ dom) []
369           local_context
370     | CicAst.Sort _ -> []
371     | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
372     | CicAst.UserInput -> assert false
373
374   and aux_option loc context = function
375     | None -> []
376     | Some t -> aux loc context t
377   in
378
379     (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
380   let rev_uniq =
381     let module SortedItem =
382       struct
383         type t = DisambiguateTypes.domain_item
384         let compare = Pervasives.compare
385       end
386     in
387     let module Set = Set.Make (SortedItem) in
388     fun l ->
389       let rev_l = List.rev l in
390       let (_, uniq_rev_l) =
391         List.fold_left
392           (fun (members, rev_l) elt ->
393             if Set.mem elt members then
394               (members, rev_l)
395             else
396               Set.add elt members, elt :: rev_l)
397           (Set.empty, []) rev_l
398       in
399       List.rev uniq_rev_l
400   in
401             
402   rev_uniq
403     (match ast with
404     | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
405     | term -> aux CicAst.dummy_floc context term)
406
407   (* dom1 \ dom2 *)
408 let domain_diff dom1 dom2 =
409 (* let domain_diff = Domain.diff *)
410   let is_in_dom2 =
411     List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
412       (fun _ -> false) dom2
413   in
414   List.filter (fun elt -> not (is_in_dom2 elt)) dom1
415
416 module Make (C: Callbacks) =
417   struct
418     let choices_of_id dbd id =
419       let uris = MetadataQuery.locate ~dbd id in
420       let uris =
421        match uris with
422         | [] ->
423            [UriManager.string_of_uri (C.input_or_locate_uri
424             ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
425         | [uri] -> [uri]
426         | _ ->
427             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
428              ~ok:"Try selected." ~enable_button_for_non_vars:true
429              ~title:"Ambiguous input." ~id
430              ~msg: ("Ambiguous input \"" ^ id ^
431                 "\". Please, choose one or more interpretations:")
432              uris
433       in
434       List.map
435         (fun uri ->
436           (uri,
437            let term =
438              try
439                CicUtil.term_of_uri uri
440              with exn ->
441                prerr_endline uri;
442                prerr_endline (Printexc.to_string exn);
443                assert false
444             in
445            fun _ _ _ -> term))
446         uris
447
448     let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
449       ~aliases:current_env
450     =
451       debug_print "NEW DISAMBIGUATE INPUT";
452       let disambiguate_context =  (* cic context -> disambiguate context *)
453         List.map
454           (function None -> Cic.Anonymous | Some (name, _) -> name)
455           context
456       in
457       let term_dom = domain_of_term ~context:disambiguate_context term in
458       debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
459         (string_of_domain term_dom));
460       let current_dom =
461         Environment.fold (fun item _ dom -> item :: dom) current_env []
462       in
463       let todo_dom = domain_diff term_dom current_dom in
464       (* (2) lookup function for any item (Id/Symbol/Num) *)
465       let lookup_choices =
466         let id_choices = Hashtbl.create 1023 in
467         fun item ->
468         let choices =
469           match item with
470           | Id id ->
471               (try
472                 Hashtbl.find id_choices id
473               with Not_found ->
474                 let choices = choices_of_id dbd id in
475                 Hashtbl.add id_choices id choices;
476                 choices)
477           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb
478           | Num instance -> DisambiguateChoices.lookup_num_choices ()
479         in
480         if choices = [] then raise (No_choices item);
481         choices
482       in
483
484 (*
485       (* <benchmark> *)
486       let _ =
487         if benchmark then begin
488           let per_item_choices =
489             List.map
490               (fun dom_item ->
491                 try
492                   let len = List.length (lookup_choices dom_item) in
493                   prerr_endline (sprintf "BENCHMARK %s: %d"
494                     (string_of_domain_item dom_item) len);
495                   len
496                 with No_choices _ -> 0)
497               term_dom
498           in
499           max_refinements := List.fold_left ( * ) 1 per_item_choices;
500           actual_refinements := 0;
501           domain_size := List.length term_dom;
502           choices_avg :=
503             (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
504         end
505       in
506       (* </benchmark> *)
507 *)
508
509       (* (3) test an interpretation filling with meta uninterpreted identifiers
510        *)
511       let test_env current_env todo_dom univ = 
512         let filled_env =
513           List.fold_left
514             (fun env item ->
515               Environment.add item
516                 ("Implicit",
517                  (match item with
518                  | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
519                  | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
520             current_env todo_dom 
521         in
522         try
523           CicUniv.set_working univ; 
524           let cic_term =
525             interpretate ~context:disambiguate_context ~env:filled_env term
526           in
527            let k = refine metasenv context cic_term in
528            let new_univ = CicUniv.get_working () in
529             (k , new_univ )
530         with
531         | Try_again -> Uncertain,univ 
532         | DisambiguateChoices.Invalid_choice -> Ko,univ 
533       in
534       (* (4) build all possible interpretations *)
535       let rec aux current_env todo_dom base_univ =
536         match todo_dom with
537         | [] ->
538             (match test_env current_env [] base_univ with
539             | Ok (term, metasenv),new_univ -> 
540                                [ current_env, metasenv, term, new_univ ]
541             | Ko,_ | Uncertain,_ -> [])
542         | item :: remaining_dom ->
543             debug_print (sprintf "CHOOSED ITEM: %s"
544              (string_of_domain_item item));
545             let choices = lookup_choices item in
546             let rec filter univ = function 
547               | [] -> []
548               | codomain_item :: tl ->
549                   debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
550                   let new_env =
551                     Environment.add item codomain_item current_env
552                   in
553                   (match test_env new_env remaining_dom univ with
554                   | Ok (term, metasenv),new_univ ->
555                       (match remaining_dom with
556                       | [] -> [ new_env, metasenv, term, new_univ ]
557                       | _ -> aux new_env remaining_dom new_univ )@ 
558                         filter univ tl
559                   | Uncertain,new_univ ->
560                       (match remaining_dom with
561                       | [] -> []
562                       | _ -> aux new_env remaining_dom new_univ )@ 
563                         filter univ tl
564                   | Ko,_ -> filter univ tl)
565             in
566             filter base_univ choices 
567       in
568        let base_univ = CicUniv.get_working () in
569       try
570         let res =
571          match aux current_env todo_dom base_univ with
572          | [] -> raise NoWellTypedInterpretation
573          | [ e,me,t,u ] as l ->
574              debug_print "UNA SOLA SCELTA";
575              CicUniv.set_working u;
576              [ e,me,t ]
577          | l ->
578              debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
579              let choices =
580                List.map
581                  (fun (env, _, _, _) ->
582                    List.map
583                      (fun domain_item ->
584                        let description =
585                          fst (Environment.find domain_item env)
586                        in
587                        (descr_of_domain_item domain_item, description))
588                      term_dom)
589                  l
590              in
591              let choosed = C.interactive_interpretation_choice choices in
592              let l' = List.map (List.nth l) choosed in
593              match l' with
594                [] -> assert false
595              | [e,me,t,u] -> 
596                  CicUniv.set_working u;
597                  (*CicUniv.print_working_graph ();*)
598                  [e,me,t]
599              | hd::tl -> (* ok, testlibrary... cosi' stampa MANY... bah *)
600                  List.map (fun (e,me,t,u) -> (e,me,t)) l'
601         in
602 (*
603         (if benchmark then
604           let res_size = List.length res in
605           prerr_endline (sprintf
606             ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
607             "BENCHMARK:   estimated %.2f")
608             !actual_refinements !max_refinements !domain_size res_size
609             !choices_avg
610             (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)));
611 *)
612         res
613      with
614       CicEnvironment.CircularDependency s -> 
615         raise (Failure "e chi la becca sta CircularDependency?");
616   end
617