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 NoWellTypedInterpretation of
32 (Token.flocation option * string Lazy.t) list
33 exception PathNotWellFormed
35 (** raised when an environment is not enough informative to decide *)
36 exception Try_again of string Lazy.t
38 type aliases = bool * DisambiguateTypes.environment
41 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
44 (** print benchmark information *)
46 let max_refinements = ref 0 (* benchmarking is not thread safe *)
47 let actual_refinements = ref 0
48 let domain_size = ref 0
49 let choices_avg = ref 0.
52 let descr_of_domain_item = function
55 | Num i -> string_of_int i
58 | Ok of 'a * Cic.metasenv
59 | Ko of Token.flocation option * string Lazy.t
60 | Uncertain of Token.flocation option * string Lazy.t
62 let refine_term metasenv context uri term ugraph ~localization_tbl =
63 (* if benchmark then incr actual_refinements; *)
65 debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
67 let term', _, metasenv',ugraph1 =
68 CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
69 (Ok (term', metasenv')),ugraph1
72 let rec process_exn loc =
74 HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
75 | CicRefine.Uncertain msg ->
76 debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
77 Uncertain (loc,msg),ugraph
78 | CicRefine.RefineFailure msg ->
79 debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
80 (CicPp.ppterm term) (Lazy.force msg)));
86 let refine_obj metasenv context uri obj ugraph ~localization_tbl =
87 assert (context = []);
88 debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
90 let obj', metasenv,ugraph =
91 CicRefine.typecheck metasenv uri obj ~localization_tbl
93 (Ok (obj', metasenv)),ugraph
96 let rec process_exn loc =
98 HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
99 | CicRefine.Uncertain msg ->
100 debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
101 Uncertain (loc,msg),ugraph
102 | CicRefine.RefineFailure msg ->
103 debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
104 (CicPp.ppobj obj) (Lazy.force msg))) ;
110 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
112 snd (Environment.find item env) env num args
114 failwith ("Domain item not found: " ^
115 (DisambiguateTypes.string_of_domain_item item))
117 (* TODO move it to Cic *)
118 let find_in_context name (context: Cic.name list) =
119 let rec aux acc = function
120 | [] -> raise Not_found
121 | Cic.Name hd :: tl when hd = name -> acc
122 | _ :: tl -> aux (acc + 1) tl
126 let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
130 let rec aux ~localize loc (context: Cic.name list) = function
131 | CicNotationPt.AttributedTerm (`Loc loc, term) ->
132 let res = aux ~localize loc context term in
133 if localize then Cic.CicHash.add localization_tbl res loc;
135 | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
136 | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
137 let cic_args = List.map (aux ~localize loc context) args in
138 resolve env (Symbol (symb, i)) ~args:cic_args ()
139 | CicNotationPt.Appl terms ->
140 Cic.Appl (List.map (aux ~localize loc context) terms)
141 | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
142 let cic_type = aux_option ~localize loc context (Some `Type) typ in
143 let cic_name = CicNotationUtil.cic_name_of_name var in
144 let cic_body = aux ~localize loc (cic_name :: context) body in
145 (match binder_kind with
146 | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
148 | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
150 resolve env (Symbol ("exists", 0))
151 ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
152 | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
153 let cic_term = aux ~localize loc context term in
154 let cic_outtype = aux_option ~localize loc context None outtype in
155 let do_branch ((head, _, args), term) =
156 let rec do_branch' context = function
157 | [] -> aux ~localize loc context term
158 | (name, typ) :: tl ->
159 let cic_name = CicNotationUtil.cic_name_of_name name in
160 let cic_body = do_branch' (cic_name :: context) tl in
163 | None -> Cic.Implicit (Some `Type)
164 | Some typ -> aux ~localize loc context typ
166 Cic.Lambda (cic_name, typ, cic_body)
168 do_branch' context args
170 let (indtype_uri, indtype_no) =
171 match indty_ident with
172 | Some (indty_ident, _) ->
173 (match resolve env (Id indty_ident) () with
174 | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
176 raise (Try_again (lazy "The type of the term to be matched
179 raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!")))
181 let fst_constructor =
183 | ((head, _, _), _) :: _ -> head
184 | [] -> raise (Invalid_choice (lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined"))
186 (match resolve env (Id fst_constructor) () with
187 | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
188 (indtype_uri, indtype_no)
190 raise (Try_again (lazy "The type of the term to be matched
193 raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!")))
195 Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
196 (List.map do_branch branches))
197 | CicNotationPt.Cast (t1, t2) ->
198 let cic_t1 = aux ~localize loc context t1 in
199 let cic_t2 = aux ~localize loc context t2 in
200 Cic.Cast (cic_t1, cic_t2)
201 | CicNotationPt.LetIn ((name, typ), def, body) ->
202 let cic_def = aux ~localize loc context def in
203 let cic_name = CicNotationUtil.cic_name_of_name name in
207 | Some t -> Cic.Cast (cic_def, aux ~localize loc context t)
209 let cic_body = aux ~localize loc (cic_name :: context) body in
210 Cic.LetIn (cic_name, cic_def, cic_body)
211 | CicNotationPt.LetRec (kind, defs, body) ->
214 (fun acc ((name, _), _, _) ->
215 CicNotationUtil.cic_name_of_name name :: acc)
219 let unlocalized_body = aux ~localize:false loc context' body in
220 match unlocalized_body with
221 Cic.Rel 1 -> `AvoidLetInNoAppl
222 | Cic.Appl (Cic.Rel 1::l) ->
227 let t',subst,metasenv =
228 CicMetaSubst.delift_rels [] [] 1 t
231 assert (metasenv=[]);
234 (* We can avoid the LetIn. But maybe we need to recompute l'
235 so that it is localized *)
238 CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
239 let l' = List.map (aux ~localize loc context) l in
245 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
247 `AddLetIn (aux ~localize loc context' body)
249 `AddLetIn unlocalized_body)
252 `AddLetIn (aux ~localize loc context' body)
254 `AddLetIn unlocalized_body
258 (fun ((name, typ), body, decr_idx) ->
259 let cic_body = aux ~localize loc context' body in
261 aux_option ~localize loc context (Some `Type) typ in
263 match CicNotationUtil.cic_name_of_name name with
265 CicNotationPt.fail loc
266 "Recursive functions cannot be anonymous"
267 | Cic.Name name -> name
269 (name, decr_idx, cic_type, cic_body))
272 let counter = ref ~-1 in
273 let build_term funs =
274 (* this is the body of the fold_right function below. Rationale: Fix
275 * and CoFix cases differs only in an additional index in the
276 * inductiveFun list, see Cic.term *)
279 (fun (var, _, _, _) cic ->
281 let fix = Cic.Fix (!counter,funs) in
283 `Recipe (`AddLetIn cic) ->
284 `Term (Cic.LetIn (Cic.Name var, fix, cic))
285 | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (fix::l))
286 | `Recipe `AvoidLetInNoAppl -> `Term fix
287 | `Term t -> `Term (Cic.LetIn (Cic.Name var, fix, t)))
290 List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
292 (fun (var, _, _, _) cic ->
294 let cofix = Cic.CoFix (!counter,funs) in
296 `Recipe (`AddLetIn cic) ->
297 `Term (Cic.LetIn (Cic.Name var, cofix, cic))
298 | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (cofix::l))
299 | `Recipe `AvoidLetInNoAppl -> `Term cofix
300 | `Term t -> `Term (Cic.LetIn (Cic.Name var, cofix, t)))
303 List.fold_right (build_term inductiveFuns) inductiveFuns
306 `Recipe _ -> assert false
308 | CicNotationPt.Ident _
309 | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
310 | CicNotationPt.Ident (name, subst)
311 | CicNotationPt.Uri (name, subst) as ast ->
312 let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
314 if is_uri ast then raise Not_found;(* don't search the env for URIs *)
315 let index = find_in_context name context in
316 if subst <> None then
317 CicNotationPt.fail loc "Explicit substitutions not allowed here";
321 if is_uri ast then (* we have the URI, build the term out of it *)
323 CicUtil.term_of_uri (UriManager.uri_of_string name)
324 with UriManager.IllFormedUri _ ->
325 CicNotationPt.fail loc "Ill formed URI"
327 resolve env (Id name) ()
331 List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
338 List.assoc s ids_to_uris, aux ~localize loc context term
340 raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
342 | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
346 | Cic.Const (uri, []) ->
347 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
348 let uris = CicUtil.params_of_obj o in
349 Cic.Const (uri, mk_subst uris)
350 | Cic.Var (uri, []) ->
351 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
352 let uris = CicUtil.params_of_obj o in
353 Cic.Var (uri, mk_subst uris)
354 | Cic.MutInd (uri, i, []) ->
356 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
357 let uris = CicUtil.params_of_obj o in
358 Cic.MutInd (uri, i, mk_subst uris)
360 CicEnvironment.Object_not_found _ ->
361 (* if we are here it is probably the case that during the
362 definition of a mutual inductive type we have met an
363 occurrence of the type in one of its constructors.
364 However, the inductive type is not yet in the environment
366 (*here the explicit_named_substituion is assumed to be of length 0 *)
367 Cic.MutInd (uri,i,[]))
368 | Cic.MutConstruct (uri, i, j, []) ->
369 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
370 let uris = CicUtil.params_of_obj o in
371 Cic.MutConstruct (uri, i, j, mk_subst uris)
372 | Cic.Meta _ | Cic.Implicit _ as t ->
374 debug_print (lazy (sprintf
375 "Warning: %s must be instantiated with _[%s] but we do not enforce it"
379 (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
384 raise (Invalid_choice (lazy "??? Can this happen?"))
386 CicEnvironment.CircularDependency _ ->
387 raise (Invalid_choice (lazy "Circular dependency in the environment"))))
388 | CicNotationPt.Implicit -> Cic.Implicit None
389 | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
390 | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
391 | CicNotationPt.Meta (index, subst) ->
396 | Some term -> Some (aux ~localize loc context term))
399 Cic.Meta (index, cic_subst)
400 | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
401 | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
402 | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
403 | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
404 | CicNotationPt.Symbol (symbol, instance) ->
405 resolve env (Symbol (symbol, instance)) ()
406 | _ -> assert false (* god bless Bologna *)
407 and aux_option ~localize loc (context: Cic.name list) annotation = function
408 | None -> Cic.Implicit annotation
409 | Some term -> aux ~localize loc context term
411 aux ~localize:true dummy_floc context ast
413 let interpretate_path ~context path =
414 let localization_tbl = Cic.CicHash.create 23 in
415 (* here we are throwing away useful localization informations!!! *)
417 interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true
418 path ~localization_tbl, localization_tbl)
420 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
421 assert (context = []);
422 assert (is_path = false);
423 let interpretate_term = interpretate_term ~localization_tbl in
425 | CicNotationPt.Inductive (params,tyl) ->
426 let uri = match uri with Some uri -> uri | None -> assert false in
430 (fun (context,res) (name,t) ->
431 Cic.Name name :: context,
432 (name, interpretate_term context env None false t)::res
435 context,List.rev res in
438 (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
442 (*here the explicit_named_substituion is assumed to be of length 0 *)
443 (fun (i,res) (name,_,_,_) ->
444 i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
446 let con_env = DisambiguateTypes.env_of_list name_to_uris env in
450 (fun (name,_,_,_) (i,t) ->
451 (*here the explicit_named_substituion is assumed to be of length 0 *)
452 let t' = Cic.MutInd (uri,i,[]) in
453 let t = CicSubstitution.subst t' t in
455 ) tyl (List.length tyl - 1,t)) in
458 (fun (name,b,ty,cl) ->
459 let ty' = add_params (interpretate_term context env None false ty) in
464 add_params (interpretate_term context con_env None false ty)
472 Cic.InductiveDefinition (tyl,[],List.length params,[])
473 | CicNotationPt.Record (params,name,ty,fields) ->
474 let uri = match uri with Some uri -> uri | None -> assert false in
478 (fun (context,res) (name,t) ->
479 (Cic.Name name :: context),
480 (name, interpretate_term context env None false t)::res
483 context,List.rev res in
486 (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in
487 let ty' = add_params (interpretate_term context env None false ty) in
491 (fun (context,res) (name,ty) ->
492 let context' = Cic.Name name :: context in
493 context',(name,interpretate_term context env None false ty)::res
494 ) (context,[]) fields) in
496 (*here the explicit_named_substituion is assumed to be of length 0 *)
497 let mutind = Cic.MutInd (uri,0,[]) in
498 if params = [] then mutind
501 (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
504 (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
506 let con' = add_params con in
507 let tyl = [name,true,ty',["mk_" ^ name,con']] in
508 let field_names = List.map fst fields in
509 Cic.InductiveDefinition
510 (tyl,[],List.length params,[`Class (`Record field_names)])
511 | CicNotationPt.Theorem (flavour, name, ty, bo) ->
512 let attrs = [`Flavour flavour] in
513 let ty' = interpretate_term [] env None false ty in
516 Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
518 let bo' = Some (interpretate_term [] env None false bo) in
519 Cic.Constant (name,bo',ty',[],attrs))
522 (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
524 let module SortedItem =
526 type t = DisambiguateTypes.domain_item
527 let compare = Pervasives.compare
530 let module Set = Set.Make (SortedItem) in
532 let rev_l = List.rev l in
533 let (_, uniq_rev_l) =
535 (fun (members, rev_l) elt ->
536 if Set.mem elt members then
539 Set.add elt members, elt :: rev_l)
540 (Set.empty, []) rev_l
544 (* "aux" keeps domain in reverse order and doesn't care about duplicates.
545 * Domain item more in deep in the list will be processed first.
547 let rec domain_rev_of_term ?(loc = dummy_floc) context = function
548 | CicNotationPt.AttributedTerm (`Loc loc, term) ->
549 domain_rev_of_term ~loc context term
550 | CicNotationPt.AttributedTerm (_, term) ->
551 domain_rev_of_term ~loc context term
552 | CicNotationPt.Appl terms ->
554 (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms
555 | CicNotationPt.Binder (kind, (var, typ), body) ->
558 | `Exists -> [ Symbol ("exists", 0) ]
561 let type_dom = domain_rev_of_term_option loc context typ in
563 domain_rev_of_term ~loc
564 (CicNotationUtil.cic_name_of_name var :: context) body
566 body_dom @ type_dom @ kind_dom
567 | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
568 let term_dom = domain_rev_of_term ~loc context term in
569 let outtype_dom = domain_rev_of_term_option loc context outtype in
570 let get_first_constructor = function
572 | ((head, _, _), _) :: _ -> [ Id head ]
574 let do_branch ((head, _, args), term) =
575 let (term_context, args_domain) =
577 (fun (cont, dom) (name, typ) ->
578 (CicNotationUtil.cic_name_of_name name :: cont,
581 | Some typ -> domain_rev_of_term ~loc cont typ @ dom)))
584 args_domain @ domain_rev_of_term ~loc term_context term
587 List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches
589 branches_dom @ outtype_dom @ term_dom @
590 (match indty_ident with
591 | None -> get_first_constructor branches
592 | Some (ident, _) -> [ Id ident ])
593 | CicNotationPt.Cast (term, ty) ->
594 let term_dom = domain_rev_of_term ~loc context term in
595 let ty_dom = domain_rev_of_term ~loc context ty in
597 | CicNotationPt.LetIn ((var, typ), body, where) ->
598 let body_dom = domain_rev_of_term ~loc context body in
599 let type_dom = domain_rev_of_term_option loc context typ in
601 domain_rev_of_term ~loc
602 (CicNotationUtil.cic_name_of_name var :: context) where
604 where_dom @ type_dom @ body_dom
605 | CicNotationPt.LetRec (kind, defs, where) ->
608 (fun acc ((var, typ), _, _) ->
609 CicNotationUtil.cic_name_of_name var :: acc)
612 let where_dom = domain_rev_of_term ~loc context' where in
615 (fun dom ((_, typ), body, _) ->
616 domain_rev_of_term ~loc context' body @
617 domain_rev_of_term_option loc context typ)
621 | CicNotationPt.Ident (name, subst) ->
623 let index = find_in_context name context in
624 if subst <> None then
625 CicNotationPt.fail loc "Explicit substitutions not allowed here"
633 (fun dom (_, term) ->
634 let dom' = domain_rev_of_term ~loc context term in
637 | CicNotationPt.Uri _ -> []
638 | CicNotationPt.Implicit -> []
639 | CicNotationPt.Num (num, i) -> [ Num i ]
640 | CicNotationPt.Meta (index, local_context) ->
642 (fun dom term -> domain_rev_of_term_option loc context term @ dom) []
644 | CicNotationPt.Sort _ -> []
645 | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
646 | CicNotationPt.UserInput
647 | CicNotationPt.Literal _
648 | CicNotationPt.Layout _
649 | CicNotationPt.Magic _
650 | CicNotationPt.Variable _ -> assert false
652 and domain_rev_of_term_option loc context = function
654 | Some t -> domain_rev_of_term ~loc context t
656 let domain_of_term ~context ast = rev_uniq (domain_rev_of_term context ast)
658 let domain_of_obj ~context ast =
659 assert (context = []);
662 | CicNotationPt.Theorem (_,_,ty,bo) ->
665 | Some bo -> domain_rev_of_term [] bo) @
667 | CicNotationPt.Inductive (params,tyl) ->
674 (fun (_,ty) -> domain_rev_of_term [] ty) cl) @
675 domain_rev_of_term [] ty) tyl) in
679 domain_rev_of_term [] ty @ dom
684 not ( List.exists (fun (name',_) -> name = Id name') params
685 || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
687 | CicNotationPt.Record (params,_,ty,fields) ->
690 (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
694 not ( List.exists (fun (name',_) -> name = Id name') params
695 || List.exists (fun (name',_) -> name = Id name') fields)
700 domain_rev_of_term [] ty @ dom
701 ) (dom @ domain_rev_of_term [] ty) params
706 let domain_diff dom1 dom2 =
707 (* let domain_diff = Domain.diff *)
709 List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
710 (fun _ -> false) dom2
712 List.filter (fun elt -> not (is_in_dom2 elt)) dom1
714 module type Disambiguator =
716 val disambiguate_term :
717 ?fresh_instances:bool ->
719 context:Cic.context ->
720 metasenv:Cic.metasenv ->
721 ?initial_ugraph:CicUniv.universe_graph ->
722 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
723 universe:DisambiguateTypes.multiple_environment option ->
724 CicNotationPt.term ->
725 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
726 Cic.metasenv * (* new metasenv *)
728 CicUniv.universe_graph) list * (* disambiguated term *)
731 val disambiguate_obj :
732 ?fresh_instances:bool ->
734 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
735 universe:DisambiguateTypes.multiple_environment option ->
736 uri:UriManager.uri option -> (* required only for inductive types *)
738 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
739 Cic.metasenv * (* new metasenv *)
741 CicUniv.universe_graph) list * (* disambiguated obj *)
745 module Make (C: Callbacks) =
747 let choices_of_id dbd id =
748 let uris = Whelp.locate ~dbd id in
752 [(C.input_or_locate_uri
753 ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
756 C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
757 ~ok:"Try selected." ~enable_button_for_non_vars:true
758 ~title:"Ambiguous input." ~id
759 ~msg: ("Ambiguous input \"" ^ id ^
760 "\". Please, choose one or more interpretations:")
765 (UriManager.string_of_uri uri,
768 CicUtil.term_of_uri uri
770 debug_print (lazy (UriManager.string_of_uri uri));
771 debug_print (lazy (Printexc.to_string exn));
777 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
779 let disambiguate_thing ~dbd ~context ~metasenv
780 ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
781 ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
783 debug_print (lazy "DISAMBIGUATE INPUT");
784 let disambiguate_context = (* cic context -> disambiguate context *)
786 (function None -> Cic.Anonymous | Some (name, _) -> name)
789 debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
790 let thing_dom = domain_of_thing ~context:disambiguate_context thing in
791 debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"
792 (string_of_domain thing_dom)));
794 debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
795 (DisambiguatePp.pp_environment aliases)));
796 debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
797 (match universe with None -> "None" | Some _ -> "Some _")));
800 Environment.fold (fun item _ dom -> item :: dom) aliases []
802 let todo_dom = domain_diff thing_dom current_dom in
803 (* (2) lookup function for any item (Id/Symbol/Num) *)
807 let lookup_in_library () =
809 | Id id -> choices_of_id dbd id
810 | Symbol (symb, _) ->
811 List.map DisambiguateChoices.mk_choice
812 (TermAcicContent.lookup_interpretations symb)
814 DisambiguateChoices.lookup_num_choices ()
817 | None -> lookup_in_library ()
822 | Symbol (symb, _) -> Symbol (symb, 0)
825 Environment.find item e
826 with Not_found -> [])
833 if benchmark then begin
834 let per_item_choices =
838 let len = List.length (lookup_choices dom_item) in
839 debug_print (lazy (sprintf "BENCHMARK %s: %d"
840 (string_of_domain_item dom_item) len));
842 with No_choices _ -> 0)
845 max_refinements := List.fold_left ( * ) 1 per_item_choices;
846 actual_refinements := 0;
847 domain_size := List.length thing_dom;
849 (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
855 (* (3) test an interpretation filling with meta uninterpreted identifiers
857 let test_env aliases todo_dom ugraph =
864 | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
865 | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
869 let localization_tbl = Cic.CicHash.create 503 in
871 interpretate_thing ~context:disambiguate_context ~env:filled_env
872 ~uri ~is_path:false thing ~localization_tbl
876 refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
879 in refine_profiler.HExtlib.profile foo ()
881 | Try_again msg -> Uncertain (None,msg), ugraph
882 | Invalid_choice msg -> Ko (None,msg), ugraph
884 (* (4) build all possible interpretations *)
885 let (@@) (l1,l2) (l1',l2') = l1@l1', l2@l2' in
886 let rec aux aliases diff lookup_in_todo_dom todo_dom base_univ =
889 assert (lookup_in_todo_dom = None);
890 (match test_env aliases [] base_univ with
891 | Ok (thing, metasenv),new_univ ->
892 [ aliases, diff, metasenv, thing, new_univ ], []
893 | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg])
894 | item :: remaining_dom ->
895 debug_print (lazy (sprintf "CHOOSED ITEM: %s"
896 (string_of_domain_item item)));
898 match lookup_in_todo_dom with
899 None -> lookup_choices item
900 | Some choices -> choices in
903 [], [None,lazy ("No choices for " ^ string_of_domain_item item)]
905 (* just one choice. We perform a one-step look-up and
906 if the next set of choices is also a singleton we
907 skip this refinement step *)
908 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
909 let new_env = Environment.add item codomain_item aliases in
910 let new_diff = (item,codomain_item)::diff in
911 let lookup_in_todo_dom,next_choice_is_single =
912 match remaining_dom with
915 let choices = lookup_choices he in
916 Some choices,List.length choices = 1
918 if next_choice_is_single then
919 aux new_env new_diff lookup_in_todo_dom remaining_dom
922 (match test_env new_env remaining_dom base_univ with
923 | Ok (thing, metasenv),new_univ ->
924 (match remaining_dom with
926 [ new_env, new_diff, metasenv, thing, new_univ ], []
928 aux new_env new_diff lookup_in_todo_dom
929 remaining_dom new_univ)
930 | Uncertain (loc,msg),new_univ ->
931 (match remaining_dom with
932 | [] -> [], [loc,msg]
934 aux new_env new_diff lookup_in_todo_dom
935 remaining_dom new_univ)
936 | Ko (loc,msg),_ -> [], [loc,msg])
938 let rec filter univ = function
940 | codomain_item :: tl ->
941 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
942 let new_env = Environment.add item codomain_item aliases in
943 let new_diff = (item,codomain_item)::diff in
944 (match test_env new_env remaining_dom univ with
945 | Ok (thing, metasenv),new_univ ->
946 (match remaining_dom with
947 | [] -> [ new_env, new_diff, metasenv, thing, new_univ ], []
948 | _ -> aux new_env new_diff None remaining_dom new_univ
951 | Uncertain (loc,msg),new_univ ->
952 (match remaining_dom with
954 | _ -> aux new_env new_diff None remaining_dom new_univ
957 | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl)
959 filter base_univ choices
961 let base_univ = initial_ugraph in
964 match aux aliases [] None todo_dom base_univ with
965 | [],errors -> raise (NoWellTypedInterpretation errors)
966 | [_,diff,metasenv,t,ugraph],_ ->
967 debug_print (lazy "SINGLE INTERPRETATION");
968 [diff,metasenv,t,ugraph], false
970 debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
973 (fun (env, _, _, _, _) ->
977 fst (Environment.find domain_item env)
979 (descr_of_domain_item domain_item, description))
983 let choosed = C.interactive_interpretation_choice choices in
984 (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
989 CicEnvironment.CircularDependency s ->
990 failwith "Disambiguate: circular dependency"
992 let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
993 ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe term
996 if fresh_instances then CicNotationUtil.freshen_term term else term
998 disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
999 ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
1000 ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term
1001 ~refine_thing:refine_term term
1003 let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
1007 if fresh_instances then CicNotationUtil.freshen_obj obj else obj
1009 disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
1010 ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj
1011 ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj