1 (* Copyright (C) 2004, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 open DisambiguateTypes
32 module Ast = NotationPt
34 (* the integer is an offset to be added to each location *)
35 exception Ambiguous_input
36 (* the integer is an offset to be added to each location *)
37 exception NoWellTypedInterpretation of
39 ((Stdpp.location list * string * string) list *
40 (DisambiguateTypes.domain_item * string) list *
41 (Stdpp.location * string) Lazy.t * bool) list
42 exception PathNotWellFormed
44 (** raised when an environment is not enough informative to decide *)
45 exception Try_again of string Lazy.t
47 type ('alias,'term) aliases =
48 bool * 'term DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t
49 type 'a disambiguator_input = string * int * 'a
51 type domain = domain_tree list
52 and domain_tree = Node of Stdpp.location list * domain_item * domain
54 let mono_uris_callback ~selection_mode ?ok
55 ?(enable_button_for_non_vars = true) ~title ~msg ~id =
56 if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
57 "matita.auto_disambiguation"
63 let mono_interp_callback _ _ _ = raise Ambiguous_input
65 let _choose_uris_callback = ref mono_uris_callback
66 let _choose_interp_callback = ref mono_interp_callback
67 let set_choose_uris_callback f = _choose_uris_callback := f
68 let set_choose_interp_callback f = _choose_interp_callback := f
70 let interactive_user_uri_choice = !_choose_uris_callback
71 let interactive_interpretation_choice interp = !_choose_interp_callback interp
72 let input_or_locate_uri ~(title:string) ?id () = None
73 (* Zack: I try to avoid using this callback. I therefore assume that
74 * the presence of an identifier that can't be resolved via "locate"
75 * query is a syntax error *)
78 let rec string_of_domain =
81 | Node (_,domain_item,l)::tl ->
82 DisambiguateTypes.string_of_domain_item domain_item ^
83 " [ " ^ string_of_domain l ^ " ] " ^ string_of_domain tl
85 let rec filter_map_domain f =
88 | Node (locs,domain_item,l)::tl ->
89 match f locs domain_item with
90 None -> filter_map_domain f l @ filter_map_domain f tl
91 | Some res -> res :: filter_map_domain f l @ filter_map_domain f tl
93 let rec map_domain f =
96 | Node (locs,domain_item,l)::tl ->
97 f locs domain_item :: map_domain f l @ map_domain f tl
103 | Node (locs,domain_item,l)::tl ->
104 if List.mem domain_item seen then
105 let seen,l = aux seen l in
106 let seen,tl = aux seen tl in
109 let seen,l = aux (domain_item::seen) l in
110 let seen,tl = aux seen tl in
111 seen, Node (locs,domain_item,l)::tl
116 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
119 (** print benchmark information *)
121 let max_refinements = ref 0 (* benchmarking is not thread safe *)
122 let actual_refinements = ref 0
123 let domain_size = ref 0
124 let choices_avg = ref 0.
127 let descr_of_domain_item = function
130 | Num i -> string_of_int i
132 type ('term,'metasenv,'subst,'graph) test_result =
133 | Ok of 'term * 'metasenv * 'subst * 'graph
134 | Ko of (Stdpp.location * string) Lazy.t
135 | Uncertain of (Stdpp.location * string) Lazy.t
137 let resolve ~env ~mk_choice (item: domain_item) arg =
139 match snd (mk_choice (Environment.find item env)), arg with
140 `Num_interp f, `Num_arg n -> f n
141 | `Sym_interp f, `Args l -> f l
142 | `Sym_interp f, `Num_arg n -> (* Implicit number! *) f []
143 | _,_ -> assert false
145 failwith ("Domain item not found: " ^
146 (DisambiguateTypes.string_of_domain_item item))
148 (* TODO move it to Cic *)
149 let find_in_context name context =
150 let rec aux acc = function
151 | [] -> raise Not_found
152 | Some hd :: tl when hd = name -> acc
153 | _ :: tl -> aux (acc + 1) tl
159 | Ast.Ident (n, None) -> Some n
163 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
164 | Ast.AttributedTerm (`Loc loc, term) ->
165 domain_of_term ~loc ~context term
166 | Ast.AttributedTerm (_, term) ->
167 domain_of_term ~loc ~context term
168 | Ast.Symbol (symbol, instance) ->
169 [ Node ([loc], Symbol (symbol, instance), []) ]
170 (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
171 | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
172 | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
176 (fun term acc -> domain_of_term ~loc ~context term @ acc)
180 Ast.AttributedTerm (`Loc loc,_) -> loc
183 [ Node ([loc], Symbol (symbol, instance), args_dom) ]
184 | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
185 | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
188 (fun term acc -> domain_of_term ~loc ~context term @ acc)
192 Ast.AttributedTerm (`Loc loc,_) -> loc
196 (* the next line can raise Not_found *)
197 ignore(find_in_context name context);
198 if subst <> None then
199 Ast.fail loc "Explicit substitutions not allowed here"
204 | None -> [ Node ([loc], Id name, args_dom) ]
208 (fun dom (_, term) ->
209 let dom' = domain_of_term ~loc ~context term in
212 [ Node ([loc], Id name, terms @ args_dom) ]))
215 (fun term acc -> domain_of_term ~loc ~context term @ acc)
217 | Ast.Binder (kind, (var, typ), body) ->
218 let type_dom = domain_of_term_option ~loc ~context typ in
221 ~context:(string_of_name var :: context) body in
223 | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
224 | _ -> type_dom @ body_dom)
225 | Ast.Case (term, indty_ident, outtype, branches) ->
226 let term_dom = domain_of_term ~loc ~context term in
227 let outtype_dom = domain_of_term_option ~loc ~context outtype in
228 let rec get_first_constructor = function
230 | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
231 | _ :: tl -> get_first_constructor tl in
234 Ast.Pattern (head, _, args), term ->
235 let (term_context, args_domain) =
237 (fun (cont, dom) (name, typ) ->
238 (string_of_name name :: cont,
241 | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
244 domain_of_term ~loc ~context:term_context term @ args_domain
245 | Ast.Wildcard, term ->
246 domain_of_term ~loc ~context term
249 List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
250 (match indty_ident with
251 | None -> get_first_constructor branches
252 | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
253 @ term_dom @ outtype_dom @ branches_dom
254 | Ast.Cast (term, ty) ->
255 let term_dom = domain_of_term ~loc ~context term in
256 let ty_dom = domain_of_term ~loc ~context ty in
258 | Ast.LetIn ((var, typ), body, where) ->
259 let body_dom = domain_of_term ~loc ~context body in
260 let type_dom = domain_of_term_option ~loc ~context typ in
262 domain_of_term ~loc ~context:(string_of_name var :: context) where in
263 body_dom @ type_dom @ where_dom
264 | Ast.LetRec (kind, defs, where) ->
265 let add_defs context =
267 (fun acc (_, (var, _), _, _) -> string_of_name var :: acc
269 let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
272 (fun dom (params, (_, typ), body, _) ->
276 (fun acc (var,_) -> string_of_name var :: acc)
282 (fun (context,res) (var,ty) ->
283 string_of_name var :: context,
284 domain_of_term_option ~loc ~context ty @ res)
285 (add_defs context,[]) params))
287 @ domain_of_term_option ~loc ~context:context' typ
288 @ domain_of_term ~loc ~context:context' body
292 | Ast.Ident (name, subst) ->
294 (* the next line can raise Not_found *)
295 ignore(find_in_context name context);
296 if subst <> None then
297 Ast.fail loc "Explicit substitutions not allowed here"
302 | None -> [ Node ([loc], Id name, []) ]
306 (fun dom (_, term) ->
307 let dom' = domain_of_term ~loc ~context term in
310 [ Node ([loc], Id name, terms) ]))
314 | Ast.Implicit _ -> []
315 | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
316 | Ast.Meta (index, local_context) ->
318 (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
325 | Ast.Variable _ -> assert false
327 and domain_of_term_option ~loc ~context = function
329 | Some t -> domain_of_term ~loc ~context t
331 let domain_of_term ~context term =
332 uniq_domain (domain_of_term ~context term)
334 let domain_of_obj ~context ast =
335 assert (context = []);
337 | Ast.Theorem (_,_,ty,bo,_) ->
341 | Some bo -> domain_of_term [] bo)
342 | Ast.Inductive (params,tyl) ->
345 (fun (context, dom) (var, ty) ->
346 let context' = string_of_name var :: context in
348 None -> context', dom
349 | Some ty -> context', dom @ domain_of_term context ty
351 let context_w_types =
352 List.rev_map (fun (var, _, _, _) -> Some var) tyl @ context in
357 domain_of_term context ty
360 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
362 | Ast.Record (params,var,ty,fields) ->
365 (fun (context, dom) (var, ty) ->
366 let context' = string_of_name var :: context in
368 None -> context', dom
369 | Some ty -> context', dom @ domain_of_term context ty
371 let context_w_types = Some var :: context in
373 @ domain_of_term context ty
376 (fun (context,res) (name,ty,_,_) ->
377 Some name::context, res @ domain_of_term context ty
378 ) (context_w_types,[]) fields)
380 let domain_of_obj ~context obj =
381 uniq_domain (domain_of_obj ~context obj)
384 let domain_diff dom1 dom2 =
385 (* let domain_diff = Domain.diff *)
389 | Symbol (symb, 0) ->
391 Symbol (symb',_) when symb = symb' -> true
403 | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
404 | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
408 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
411 | Ident_alias of string * string (* identifier, uri *)
412 | Symbol_alias of string * int * string (* name, instance no, description *)
413 | Number_alias of int * string (* instance no, description *)
415 let disambiguate_thing
416 ~context ~metasenv ~subst ~use_coercions
417 ~string_context_of_context
418 ~initial_ugraph:base_univ ~expty
419 ~mk_implicit ~description_of_alias ~fix_instance
420 ~aliases ~universe ~lookup_in_library
421 ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
423 (thing_txt,thing_txt_prefix_len,thing)
425 debug_print (lazy "DISAMBIGUATE INPUT");
426 debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
428 domain_of_thing ~context:(string_context_of_context context) thing in
430 (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
432 Environment.fold (fun item _ dom -> item :: dom) aliases [] in
433 let todo_dom = domain_diff thing_dom current_dom in
435 (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
436 (* (2) lookup function for any item (Id/Symbol/Num) *)
442 interactive_user_uri_choice
443 input_or_locate_uri item
446 fix_instance item (Environment.find item e)
447 with Not_found -> [])
450 (* items with 1 choice are interpreted ASAP *)
451 let aliases, todo_dom =
452 let rec aux (aliases,acc) = function
454 | (Node (_, item,extra) as node) :: tl ->
455 let choices = lookup_choices item in
456 if List.length choices <> 1 then aux (aliases, acc@[node]) tl
458 let tl = tl @ extra in
459 if Environment.mem item aliases then aux (aliases, acc) tl
460 else aux (Environment.add item (List.hd choices) aliases, acc) tl
462 aux (aliases,[]) todo_dom
468 if benchmark then begin
469 let per_item_choices =
473 let len = List.length (lookup_choices dom_item) in
474 debug_print (lazy (sprintf "BENCHMARK %s: %d"
475 (string_of_domain_item dom_item) len));
477 with No_choices _ -> 0)
480 max_refinements := List.fold_left ( * ) 1 per_item_choices;
481 actual_refinements := 0;
482 domain_size := List.length thing_dom;
484 (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
490 (* (3) test an interpretation filling with meta uninterpreted identifiers
492 let test_env aliases todo_dom ugraph =
494 let rec aux env = function
496 | Node (_, item, l) :: tl ->
500 (match item with | Id _ | Num _ -> true | Symbol _ -> false))
502 aux (aux env l) tl in
503 let filled_env = aux aliases todo_dom in
504 let localization_tbl = mk_localization_tbl 503 in
506 interpretate_thing ~context ~env:filled_env
507 ~uri ~is_path:false thing ~localization_tbl
510 refine_thing metasenv subst context uri
511 ~use_coercions cic_thing expty ugraph ~localization_tbl
512 in refine_profiler.HExtlib.profile foo ()
514 | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
515 | Invalid_choice loc_msg -> Ko loc_msg
517 (* (4) build all possible interpretations *)
518 let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
519 (* aux returns triples Ok/Uncertain/Ko *)
520 (* rem_dom is the concatenation of all the remainin domains *)
521 let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom =
522 debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
525 assert (lookup_in_todo_dom = None);
526 (match test_env aliases rem_dom base_univ with
527 | Ok (thing, metasenv,subst,new_univ) ->
528 [ aliases, diff, metasenv, subst, thing, new_univ ], [], []
529 | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true]
530 | Uncertain loc_msg ->
531 [],[aliases,diff,loc_msg],[])
532 | Node (locs,item,inner_dom) :: remaining_dom ->
533 debug_print (lazy (sprintf "CHOOSED ITEM: %s"
534 (string_of_domain_item item)));
536 match lookup_in_todo_dom with
537 None -> lookup_choices item
538 | Some choices -> choices in
544 "No choices for " ^ string_of_domain_item item)),
548 (* just one choice. We perform a one-step look-up and
549 if the next set of choices is also a singleton we
550 skip this refinement step *)
551 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
552 let new_env = Environment.add item codomain_item aliases in
553 let new_diff = (item,codomain_item)::diff in
554 let lookup_in_todo_dom,next_choice_is_single =
555 match remaining_dom with
558 let choices = lookup_choices he in
559 Some choices,List.length choices = 1
561 if next_choice_is_single then
562 aux new_env new_diff lookup_in_todo_dom remaining_dom
565 (match test_env new_env remaining_dom base_univ with
566 | Ok (thing, metasenv),new_univ ->
567 (match remaining_dom with
569 [ new_env, new_diff, metasenv, thing, new_univ ], []
571 aux new_env new_diff lookup_in_todo_dom
572 remaining_dom new_univ)
573 | Uncertain (loc,msg),new_univ ->
574 (match remaining_dom with
575 | [] -> [], [new_env,new_diff,loc,msg,true]
577 aux new_env new_diff lookup_in_todo_dom
578 remaining_dom new_univ)
579 | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
582 let mark_not_significant failures =
584 (fun (env, diff, loc_msg, _b) ->
585 env, diff, loc_msg, false)
587 let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
588 if ok_l <> [] || uncertain_l <> [] then
589 ok_l,uncertain_l,mark_not_significant error_l
592 let rec filter = function
594 | codomain_item :: tl ->
595 (*debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));*)
596 let new_env = Environment.add item codomain_item aliases in
597 let new_diff = (item,codomain_item)::diff in
600 (inner_dom@remaining_dom@rem_dom) base_univ
602 | Ok (thing, metasenv,subst,new_univ) ->
603 (* prerr_endline "OK"; *)
605 (match inner_dom with
607 [new_env,new_diff,metasenv,subst,thing,new_univ],
610 aux new_env new_diff None inner_dom
611 (remaining_dom@rem_dom)
615 | Uncertain loc_msg ->
616 (* prerr_endline ("UNCERTAIN"); *)
618 (match inner_dom with
619 | [] -> [],[new_env,new_diff,loc_msg],[]
621 aux new_env new_diff None inner_dom
622 (remaining_dom@rem_dom)
627 (* prerr_endline "KO"; *)
628 let res = [],[],[new_env,new_diff,loc_msg,true] in
631 let ok_l,uncertain_l,error_l =
632 classify_errors (filter choices)
636 (fun (env,diff,_,_,_,_) res ->
637 aux env diff None remaining_dom rem_dom @@ res
638 ) ok_l ([],[],error_l)
641 (fun (env,diff,_) res ->
642 aux env diff None remaining_dom rem_dom @@ res
643 ) uncertain_l res_after_ok_l
645 let aux' aliases diff lookup_in_todo_dom todo_dom =
646 if todo_dom = [] then
647 aux aliases diff lookup_in_todo_dom todo_dom []
649 match test_env aliases todo_dom base_univ with
652 aux aliases diff lookup_in_todo_dom todo_dom []
653 | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true]
656 match aux' aliases [] None todo_dom with
657 | [],uncertain,errors ->
660 (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)
665 (fun (env,diff,loc_msg,significant) ->
668 (fun locs domain_item ->
671 description_of_alias (Environment.find domain_item env)
673 Some (locs,descr_of_domain_item domain_item,description)
678 let diff= List.map (fun a,b -> a,description_of_alias b) diff in
679 env',diff,loc_msg,significant
682 raise (NoWellTypedInterpretation (0,errors))
683 | [_,diff,metasenv,subst,t,ugraph],_,_ ->
684 debug_print (lazy "SINGLE INTERPRETATION");
685 [diff,metasenv,subst,t,ugraph], false
688 (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
691 (fun (env, _, _, _, _, _) ->
693 (fun locs domain_item ->
695 description_of_alias (Environment.find domain_item env)
697 locs,descr_of_domain_item domain_item, description)
702 interactive_interpretation_choice
703 thing_txt thing_txt_prefix_len choices
705 (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u)