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/
28 open DisambiguateTypes
31 exception No_choices of domain_item
32 exception NoWellTypedInterpretation
33 exception PathNotWellFormed
35 (** raised when an environment is not enough informative to decide *)
39 let debug_print = if debug then prerr_endline else ignore
42 (** print benchmark information *)
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.
50 let floc_of_loc (loc_begin, loc_end) =
52 { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
53 Lexing.pos_cnum = loc_begin }
55 let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in
56 (floc_begin, floc_end)
58 let dummy_floc = floc_of_loc (-1, -1)
60 let descr_of_domain_item = function
63 | Num i -> string_of_int i
66 | Ok of 'a * Cic.metasenv
70 let refine_term metasenv context uri term ugraph =
71 (* if benchmark then incr actual_refinements; *)
74 CicMkImplicit.expand_implicits metasenv [] context term in
75 debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
77 let term', _, metasenv',ugraph1 =
78 CicRefine.type_of_aux' metasenv context term ugraph in
79 (Ok (term', metasenv')),ugraph1
81 | CicRefine.Uncertain s ->
82 debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term) ;
84 | CicRefine.RefineFailure msg ->
85 debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
86 (CicPp.ppterm term) msg);
89 let refine_obj metasenv context uri obj ugraph =
90 assert (context = []);
91 let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in
92 debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj));
94 let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
95 (Ok (obj', metasenv)),ugraph
97 | CicRefine.Uncertain s ->
98 debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj) ;
100 | CicRefine.RefineFailure msg ->
101 debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
102 (CicPp.ppobj obj) msg);
105 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
107 snd (Environment.find item env) env num args
109 failwith ("Domain item not found: " ^
110 (DisambiguateTypes.string_of_domain_item item))
112 (* TODO move it to Cic *)
113 let find_in_environment name (context: Cic.name list) =
114 let rec aux acc = function
115 | [] -> raise Not_found
116 | Cic.Name hd :: tl when hd = name -> acc
117 | _ :: tl -> aux (acc + 1) tl
121 let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
123 let rec aux loc (context: Cic.name list) = function
124 | CicNotationPt.AttributedTerm (`Loc loc, term) ->
126 | CicNotationPt.AttributedTerm (_, term) -> aux loc context term
127 | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
128 let cic_args = List.map (aux loc context) args in
129 resolve env (Symbol (symb, i)) ~args:cic_args ()
130 | CicNotationPt.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
131 | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
132 let cic_type = aux_option loc context (Some `Type) typ in
133 let cic_name = CicNotationUtil.cic_name_of_name var in
134 let cic_body = aux loc (cic_name :: context) body in
135 (match binder_kind with
136 | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
138 | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
140 resolve env (Symbol ("exists", 0))
141 ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
142 | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
143 let cic_term = aux loc context term in
144 let cic_outtype = aux_option loc context None outtype in
145 let do_branch ((head, args), term) =
146 let rec do_branch' context = function
147 | [] -> aux loc context term
148 | (name, typ) :: tl ->
149 let cic_name = CicNotationUtil.cic_name_of_name name in
150 let cic_body = do_branch' (cic_name :: context) tl in
153 | None -> Cic.Implicit (Some `Type)
154 | Some typ -> aux loc context typ
156 Cic.Lambda (cic_name, typ, cic_body)
158 do_branch' context args
160 let (indtype_uri, indtype_no) =
161 match indty_ident with
162 | Some indty_ident ->
163 (match resolve env (Id indty_ident) () with
164 | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
165 | Cic.Implicit _ -> raise Try_again
166 | _ -> raise Invalid_choice)
168 let fst_constructor =
170 | ((head, _), _) :: _ -> head
171 | [] -> raise Invalid_choice
173 (match resolve env (Id fst_constructor) () with
174 | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
175 (indtype_uri, indtype_no)
176 | Cic.Implicit _ -> raise Try_again
177 | _ -> raise Invalid_choice)
179 Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
180 (List.map do_branch branches))
181 | CicNotationPt.Cast (t1, t2) ->
182 let cic_t1 = aux loc context t1 in
183 let cic_t2 = aux loc context t2 in
184 Cic.Cast (cic_t1, cic_t2)
185 | CicNotationPt.LetIn ((name, typ), def, body) ->
186 let cic_def = aux loc context def in
187 let cic_name = CicNotationUtil.cic_name_of_name name in
191 | Some t -> Cic.Cast (cic_def, aux loc context t)
193 let cic_body = aux loc (cic_name :: context) body in
194 Cic.LetIn (cic_name, cic_def, cic_body)
195 | CicNotationPt.LetRec (kind, defs, body) ->
198 (fun acc ((name, _), _, _) ->
199 CicNotationUtil.cic_name_of_name name :: acc)
202 let cic_body = aux loc context' body in
205 (fun ((name, typ), body, decr_idx) ->
206 let cic_body = aux loc context' body in
207 let cic_type = aux_option loc context (Some `Type) typ in
209 match CicNotationUtil.cic_name_of_name name with
211 CicNotationPt.fail loc
212 "Recursive functions cannot be anonymous"
213 | Cic.Name name -> name
215 (name, decr_idx, cic_type, cic_body))
218 let counter = ref ~-1 in
219 let build_term funs =
220 (* this is the body of the fold_right function below. Rationale: Fix
221 * and CoFix cases differs only in an additional index in the
222 * inductiveFun list, see Cic.term *)
225 (fun (var, _, _, _) cic ->
227 Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
230 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
232 (fun (var, _, _, _) cic ->
234 Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
236 List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
237 | CicNotationPt.Ident _
238 | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
239 | CicNotationPt.Ident (name, subst)
240 | CicNotationPt.Uri (name, subst) as ast ->
241 let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
243 if is_uri ast then raise Not_found;(* don't search the env for URIs *)
244 let index = find_in_environment name context in
245 if subst <> None then
246 CicNotationPt.fail loc "Explicit substitutions not allowed here";
250 if is_uri ast then (* we have the URI, build the term out of it *)
252 CicUtil.term_of_uri (UriManager.uri_of_string name)
253 with UriManager.IllFormedUri _ ->
254 CicNotationPt.fail loc "Ill formed URI"
256 resolve env (Id name) ()
260 List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
267 List.assoc s ids_to_uris, aux loc context term
269 raise Invalid_choice))
271 | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
275 | Cic.Const (uri, []) ->
276 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
277 let uris = CicUtil.params_of_obj o in
278 Cic.Const (uri, mk_subst uris)
279 | Cic.Var (uri, []) ->
280 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
281 let uris = CicUtil.params_of_obj o in
282 Cic.Var (uri, mk_subst uris)
283 | Cic.MutInd (uri, i, []) ->
285 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
286 let uris = CicUtil.params_of_obj o in
287 Cic.MutInd (uri, i, mk_subst uris)
289 CicEnvironment.Object_not_found _ ->
290 (* if we are here it is probably the case that during the
291 definition of a mutual inductive type we have met an
292 occurrence of the type in one of its constructors.
293 However, the inductive type is not yet in the environment
295 (*here the explicit_named_substituion is assumed to be of length 0 *)
296 Cic.MutInd (uri,i,[]))
297 | Cic.MutConstruct (uri, i, j, []) ->
298 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
299 let uris = CicUtil.params_of_obj o in
300 Cic.MutConstruct (uri, i, j, mk_subst uris)
301 | Cic.Meta _ | Cic.Implicit _ as t ->
304 "Warning: %s must be instantiated with _[%s] but we do not enforce it"
308 (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
315 CicEnvironment.CircularDependency _ ->
316 raise Invalid_choice))
317 | CicNotationPt.Implicit -> Cic.Implicit None
318 | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
319 | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
320 | CicNotationPt.Meta (index, subst) ->
323 (function None -> None | Some term -> Some (aux loc context term))
326 Cic.Meta (index, cic_subst)
327 | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
328 | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
329 | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
330 | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
331 | CicNotationPt.Symbol (symbol, instance) ->
332 resolve env (Symbol (symbol, instance)) ()
333 | _ -> assert false (* god bless Bologna *)
334 and aux_option loc (context: Cic.name list) annotation = function
335 | None -> Cic.Implicit annotation
336 | Some term -> aux loc context term
339 | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term
340 | term -> aux dummy_floc context term
342 let interpretate_path ~context ~env path =
343 interpretate_term ~context ~env ~uri:None ~is_path:true path
345 let interpretate_obj ~context ~env ~uri ~is_path obj =
346 assert (context = []);
347 assert (is_path = false);
349 | GrafiteAst.Inductive (params,tyl) ->
350 let uri = match uri with Some uri -> uri | None -> assert false in
354 (fun (context,res) (name,t) ->
355 Cic.Name name :: context,
356 (name, interpretate_term context env None false t)::res
359 context,List.rev res in
362 (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
366 (*here the explicit_named_substituion is assumed to be of length 0 *)
367 (fun (i,res) (name,_,_,_) ->
368 i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
370 let con_env = DisambiguateTypes.env_of_list name_to_uris env in
374 (fun (name,_,_,_) (i,t) ->
375 (*here the explicit_named_substituion is assumed to be of length 0 *)
376 let t' = Cic.MutInd (uri,i,[]) in
377 let t = CicSubstitution.subst t' t in
379 ) tyl (List.length tyl - 1,t)) in
382 (fun (name,b,ty,cl) ->
383 let ty' = add_params (interpretate_term context env None false ty) in
388 add_params (interpretate_term context con_env None false ty)
396 Cic.InductiveDefinition (tyl,[],List.length params,[])
397 | GrafiteAst.Record (params,name,ty,fields) ->
398 let uri = match uri with Some uri -> uri | None -> assert false in
402 (fun (context,res) (name,t) ->
403 (Cic.Name name :: context),
404 (name, interpretate_term context env None false t)::res
407 context,List.rev res in
410 (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
411 let ty' = add_params (interpretate_term context env None false ty) in
415 (fun (context,res) (name,ty) ->
416 let context' = Cic.Name name :: context in
417 context',(name,interpretate_term context env None false ty)::res
418 ) (context,[]) fields) in
420 (*here the explicit_named_substituion is assumed to be of length 0 *)
421 let mutind = Cic.MutInd (uri,0,[]) in
422 if params = [] then mutind
425 (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
428 (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
430 let con' = add_params con in
431 let tyl = [name,true,ty',["mk_" ^ name,con']] in
432 let field_names = List.map fst fields in
433 Cic.InductiveDefinition
434 (tyl,[],List.length params,[`Class (`Record field_names)])
435 | GrafiteAst.Theorem (flavour, name, ty, bo) ->
436 let attrs = [`Flavour flavour] in
437 let ty' = interpretate_term [] env None false ty in
440 Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
442 let bo' = Some (interpretate_term [] env None false bo) in
443 Cic.Constant (name,bo',ty',[],attrs))
446 (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
448 let module SortedItem =
450 type t = DisambiguateTypes.domain_item
451 let compare = Pervasives.compare
454 let module Set = Set.Make (SortedItem) in
456 let rev_l = List.rev l in
457 let (_, uniq_rev_l) =
459 (fun (members, rev_l) elt ->
460 if Set.mem elt members then
463 Set.add elt members, elt :: rev_l)
464 (Set.empty, []) rev_l
468 (* "aux" keeps domain in reverse order and doesn't care about duplicates.
469 * Domain item more in deep in the list will be processed first.
471 let rec domain_rev_of_term ?(loc = dummy_floc) context = function
472 | CicNotationPt.AttributedTerm (`Loc loc, term) ->
473 domain_rev_of_term ~loc context term
474 | CicNotationPt.AttributedTerm (_, term) ->
475 domain_rev_of_term ~loc context term
476 | CicNotationPt.Appl terms ->
478 (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms
479 | CicNotationPt.Binder (kind, (var, typ), body) ->
482 | `Exists -> [ Symbol ("exists", 0) ]
485 let type_dom = domain_rev_of_term_option loc context typ in
487 domain_rev_of_term ~loc
488 (CicNotationUtil.cic_name_of_name var :: context) body
490 body_dom @ type_dom @ kind_dom
491 | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
492 let term_dom = domain_rev_of_term ~loc context term in
493 let outtype_dom = domain_rev_of_term_option loc context outtype in
494 let get_first_constructor = function
496 | ((head, _), _) :: _ -> [ Id head ]
498 let do_branch ((head, args), term) =
499 let (term_context, args_domain) =
501 (fun (cont, dom) (name, typ) ->
502 (CicNotationUtil.cic_name_of_name name :: cont,
505 | Some typ -> domain_rev_of_term ~loc cont typ @ dom)))
508 args_domain @ domain_rev_of_term ~loc term_context term
511 List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
513 branches_dom @ outtype_dom @ term_dom @
514 (match indty_ident with
515 | None -> get_first_constructor branches
516 | Some ident -> [ Id ident ])
517 | CicNotationPt.Cast (term, ty) ->
518 let term_dom = domain_rev_of_term ~loc context term in
519 let ty_dom = domain_rev_of_term ~loc context ty in
521 | CicNotationPt.LetIn ((var, typ), body, where) ->
522 let body_dom = domain_rev_of_term ~loc context body in
523 let type_dom = domain_rev_of_term_option loc context typ in
525 domain_rev_of_term ~loc
526 (CicNotationUtil.cic_name_of_name var :: context) where
528 where_dom @ type_dom @ body_dom
529 | CicNotationPt.LetRec (kind, defs, where) ->
532 (fun acc ((var, typ), _, _) ->
533 CicNotationUtil.cic_name_of_name var :: acc)
536 let where_dom = domain_rev_of_term ~loc context' where in
539 (fun dom ((_, typ), body, _) ->
540 domain_rev_of_term ~loc context' body @
541 domain_rev_of_term_option loc context typ)
545 | CicNotationPt.Ident (name, subst) ->
547 let index = find_in_environment name context in
548 if subst <> None then
549 CicNotationPt.fail loc "Explicit substitutions not allowed here"
557 (fun dom (_, term) ->
558 let dom' = domain_rev_of_term ~loc context term in
561 | CicNotationPt.Uri _ -> []
562 | CicNotationPt.Implicit -> []
563 | CicNotationPt.Num (num, i) -> [ Num i ]
564 | CicNotationPt.Meta (index, local_context) ->
566 (fun dom term -> domain_rev_of_term_option loc context term @ dom) []
568 | CicNotationPt.Sort _ -> []
569 | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
570 | CicNotationPt.UserInput
571 | CicNotationPt.Literal _
572 | CicNotationPt.Layout _
573 | CicNotationPt.Magic _
574 | CicNotationPt.Variable _ -> assert false
576 and domain_rev_of_term_option loc context = function
578 | Some t -> domain_rev_of_term ~loc context t
580 let domain_of_term ~context ast =
581 rev_uniq (domain_rev_of_term context ast)
583 let domain_of_obj ~context ast =
584 assert (context = []);
587 | GrafiteAst.Theorem (_,_,ty,bo) ->
590 | Some bo -> domain_rev_of_term [] bo) @
592 | GrafiteAst.Inductive (params,tyl) ->
599 (fun (_,ty) -> domain_rev_of_term [] ty) cl) @
600 domain_rev_of_term [] ty) tyl) in
604 domain_rev_of_term [] ty @ dom
609 not ( List.exists (fun (name',_) -> name = Id name') params
610 || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
612 | GrafiteAst.Record (params,_,ty,fields) ->
615 (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
619 not ( List.exists (fun (name',_) -> name = Id name') params
620 || List.exists (fun (name',_) -> name = Id name') fields)
625 domain_rev_of_term [] ty @ dom
626 ) (dom @ domain_rev_of_term [] ty) params
631 let domain_diff dom1 dom2 =
632 (* let domain_diff = Domain.diff *)
634 List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
635 (fun _ -> false) dom2
637 List.filter (fun elt -> not (is_in_dom2 elt)) dom1
639 module type Disambiguator =
641 val disambiguate_term :
643 context:Cic.context ->
644 metasenv:Cic.metasenv ->
645 ?initial_ugraph:CicUniv.universe_graph ->
646 aliases:environment -> (* previous interpretation status *)
647 CicNotationPt.term ->
648 (environment * (* new interpretation status *)
649 Cic.metasenv * (* new metasenv *)
651 CicUniv.universe_graph) list (* disambiguated term *)
653 val disambiguate_obj :
655 aliases:environment -> (* previous interpretation status *)
656 uri:UriManager.uri option -> (* required only for inductive types *)
658 (environment * (* new interpretation status *)
659 Cic.metasenv * (* new metasenv *)
661 CicUniv.universe_graph) list (* disambiguated obj *)
664 module Make (C: Callbacks) =
666 let choices_of_id dbd id =
667 let uris = MetadataQuery.locate ~dbd id in
671 [(C.input_or_locate_uri
672 ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
675 C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
676 ~ok:"Try selected." ~enable_button_for_non_vars:true
677 ~title:"Ambiguous input." ~id
678 ~msg: ("Ambiguous input \"" ^ id ^
679 "\". Please, choose one or more interpretations:")
684 (UriManager.string_of_uri uri,
687 CicUtil.term_of_uri uri
689 debug_print (UriManager.string_of_uri uri);
690 debug_print (Printexc.to_string exn);
696 let disambiguate_thing ~dbd ~context ~metasenv
697 ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
698 ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
700 debug_print "NEW DISAMBIGUATE INPUT";
701 let disambiguate_context = (* cic context -> disambiguate context *)
703 (function None -> Cic.Anonymous | Some (name, _) -> name)
706 debug_print ("TERM IS: " ^ (pp_thing thing));
707 let thing_dom = domain_of_thing ~context:disambiguate_context thing in
708 debug_print (sprintf "DISAMBIGUATION DOMAIN: %s"
709 (string_of_domain thing_dom));
711 Environment.fold (fun item _ dom -> item :: dom) current_env []
713 let todo_dom = domain_diff thing_dom current_dom in
714 (* (2) lookup function for any item (Id/Symbol/Num) *)
716 let id_choices = Hashtbl.create 1023 in
722 Hashtbl.find id_choices id
724 let choices = choices_of_id dbd id in
725 Hashtbl.add id_choices id choices;
727 | Symbol (symb, _) ->
728 List.map DisambiguateChoices.mk_choice
729 (CicNotationRew.lookup_interpretations symb)
730 (* DisambiguateChoices.lookup_symbol_choices symb *)
731 | Num instance -> DisambiguateChoices.lookup_num_choices ()
733 if choices = [] then raise (No_choices item);
740 if benchmark then begin
741 let per_item_choices =
745 let len = List.length (lookup_choices dom_item) in
746 debug_print (sprintf "BENCHMARK %s: %d"
747 (string_of_domain_item dom_item) len);
749 with No_choices _ -> 0)
752 max_refinements := List.fold_left ( * ) 1 per_item_choices;
753 actual_refinements := 0;
754 domain_size := List.length thing_dom;
756 (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
762 (* (3) test an interpretation filling with meta uninterpreted identifiers
764 let test_env current_env todo_dom ugraph =
771 | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
772 | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
777 interpretate_thing ~context:disambiguate_context ~env:filled_env
778 ~uri ~is_path:false thing
780 let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
783 | Try_again -> Uncertain, ugraph
784 | Invalid_choice -> Ko, ugraph
786 (* (4) build all possible interpretations *)
787 let rec aux current_env todo_dom base_univ =
790 (match test_env current_env [] base_univ with
791 | Ok (thing, metasenv),new_univ ->
792 [ current_env, metasenv, thing, new_univ ]
793 | Ko,_ | Uncertain,_ -> [])
794 | item :: remaining_dom ->
795 debug_print (sprintf "CHOOSED ITEM: %s"
796 (string_of_domain_item item));
797 let choices = lookup_choices item in
798 let rec filter univ = function
800 | codomain_item :: tl ->
801 debug_print (sprintf "%s CHOSEN" (fst codomain_item)) ;
803 Environment.add item codomain_item current_env
805 (match test_env new_env remaining_dom univ with
806 | Ok (thing, metasenv),new_univ ->
807 (match remaining_dom with
808 | [] -> [ new_env, metasenv, thing, new_univ ]
809 | _ -> aux new_env remaining_dom new_univ )@
811 | Uncertain,new_univ ->
812 (match remaining_dom with
814 | _ -> aux new_env remaining_dom new_univ )@
816 | Ko,_ -> filter univ tl)
818 filter base_univ choices
820 let base_univ = initial_ugraph in
823 match aux current_env todo_dom base_univ with
824 | [] -> raise NoWellTypedInterpretation
826 debug_print "UNA SOLA SCELTA";
827 (* Experimental: we forget the environment [e] since we are able
828 to recompute it. In this way we are forced to do more work
829 later (since we have less aliases), but we have more freedom
830 (since we have less aliases) in the future disambiguations. *)
831 [ current_env,me,t,u]
833 debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
836 (fun (env, _, _, _) ->
840 fst (Environment.find domain_item env)
842 (descr_of_domain_item domain_item, description))
846 let choosed = C.interactive_interpretation_choice choices in
847 List.map (List.nth l) choosed
851 let res_size = List.length res in
853 ("BENCHMARK: %d/%d refinements performed, domain size %d, interps %d, k %.2f\n" ^^
854 "BENCHMARK: estimated %.2f")
855 !actual_refinements !max_refinements !domain_size res_size
857 (float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg)));
861 CicEnvironment.CircularDependency s ->
862 failwith "Disambiguate: circular dependency"
864 let disambiguate_term ~dbd ~context ~metasenv
865 ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term
867 disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
868 ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term
869 ~interpretate_thing:interpretate_term ~refine_thing:refine_term term
871 let disambiguate_obj ~dbd ~aliases ~uri obj =
872 disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri
873 ~pp_thing:GrafiteAstPp.pp_obj ~domain_of_thing:domain_of_obj
874 ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
880 exception Ambiguous_term of string
884 let interactive_user_uri_choice ~selection_mode ?ok
885 ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
887 let interactive_interpretation_choice interp = raise Exit
888 let input_or_locate_uri ~(title:string) ?id = raise Exit
890 module Disambiguator = Make (Callbacks)
891 let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
892 ?(aliases = DisambiguateTypes.Environment.empty) term
894 let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in
896 Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
897 ?initial_ugraph ~aliases
898 with Exit -> raise (Ambiguous_term term)