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
33 module Ast = CicNotationPt
35 (* the integer is an offset to be added to each location *)
36 exception NoWellTypedInterpretation of
38 ((Stdpp.location list * string * string) list *
39 (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
40 Stdpp.location option * string Lazy.t * bool) list
41 exception PathNotWellFormed
43 (** raised when an environment is not enough informative to decide *)
44 exception Try_again of string Lazy.t
46 type aliases = bool * DisambiguateTypes.environment
47 type 'a disambiguator_input = string * int * 'a
49 type domain = domain_tree list
50 and domain_tree = Node of Stdpp.location list * domain_item * domain
52 let rec string_of_domain =
55 | Node (_,domain_item,l)::tl ->
56 DisambiguateTypes.string_of_domain_item domain_item ^
57 " [ " ^ string_of_domain l ^ " ] " ^ string_of_domain tl
59 let rec filter_map_domain f =
62 | Node (locs,domain_item,l)::tl ->
63 match f locs domain_item with
64 None -> filter_map_domain f l @ filter_map_domain f tl
65 | Some res -> res :: filter_map_domain f l @ filter_map_domain f tl
67 let rec map_domain f =
70 | Node (locs,domain_item,l)::tl ->
71 f locs domain_item :: map_domain f l @ map_domain f tl
77 | Node (locs,domain_item,l)::tl ->
78 if List.mem domain_item seen then
79 let seen,l = aux seen l in
80 let seen,tl = aux seen tl in
83 let seen,l = aux (domain_item::seen) l in
84 let seen,tl = aux seen tl in
85 seen, Node (locs,domain_item,l)::tl
90 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
93 (** print benchmark information *)
95 let max_refinements = ref 0 (* benchmarking is not thread safe *)
96 let actual_refinements = ref 0
97 let domain_size = ref 0
98 let choices_avg = ref 0.
101 let descr_of_domain_item = function
104 | Num i -> string_of_int i
106 type 'a test_result =
107 | Ok of 'a * Cic.metasenv
108 | Ko of Stdpp.location option * string Lazy.t
109 | Uncertain of Stdpp.location option * string Lazy.t
111 let refine_term metasenv context uri term ugraph ~localization_tbl =
112 (* if benchmark then incr actual_refinements; *)
114 debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
116 let term', _, metasenv',ugraph1 =
117 CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
118 (Ok (term', metasenv')),ugraph1
121 let rec process_exn loc =
123 HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
124 | CicRefine.Uncertain msg ->
125 debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
126 Uncertain (loc,msg),ugraph
127 | CicRefine.RefineFailure msg ->
128 debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
129 (CicPp.ppterm term) (Lazy.force msg)));
135 let refine_obj metasenv context uri obj ugraph ~localization_tbl =
136 assert (context = []);
137 debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
139 let obj', metasenv,ugraph =
140 CicRefine.typecheck metasenv uri obj ~localization_tbl
142 (Ok (obj', metasenv)),ugraph
145 let rec process_exn loc =
147 HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
148 | CicRefine.Uncertain msg ->
149 debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
150 Uncertain (loc,msg),ugraph
151 | CicRefine.RefineFailure msg ->
152 debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
153 (CicPp.ppobj obj) (Lazy.force msg))) ;
159 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
161 snd (Environment.find item env) env num args
163 failwith ("Domain item not found: " ^
164 (DisambiguateTypes.string_of_domain_item item))
166 (* TODO move it to Cic *)
167 let find_in_context name context =
168 let rec aux acc = function
169 | [] -> raise Not_found
170 | Cic.Name hd :: tl when hd = name -> acc
171 | _ :: tl -> aux (acc + 1) tl
175 let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~uri ~is_path ast
178 (* create_dummy_ids shouldbe used only for interpretating patterns *)
180 let rec aux ~localize loc (context: Cic.name list) = function
181 | CicNotationPt.AttributedTerm (`Loc loc, term) ->
182 let res = aux ~localize loc context term in
183 if localize then Cic.CicHash.add localization_tbl res loc;
185 | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
186 | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
187 let cic_args = List.map (aux ~localize loc context) args in
188 resolve env (Symbol (symb, i)) ~args:cic_args ()
189 | CicNotationPt.Appl terms ->
190 Cic.Appl (List.map (aux ~localize loc context) terms)
191 | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
192 let cic_type = aux_option ~localize loc context (Some `Type) typ in
193 let cic_name = CicNotationUtil.cic_name_of_name var in
194 let cic_body = aux ~localize loc (cic_name :: context) body in
195 (match binder_kind with
196 | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
198 | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
200 resolve env (Symbol ("exists", 0))
201 ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
202 | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
203 let cic_term = aux ~localize loc context term in
204 let cic_outtype = aux_option ~localize loc context None outtype in
205 let do_branch ((head, _, args), term) =
206 let rec do_branch' context = function
207 | [] -> aux ~localize loc context term
208 | (name, typ) :: tl ->
209 let cic_name = CicNotationUtil.cic_name_of_name name in
210 let cic_body = do_branch' (cic_name :: context) tl in
213 | None -> Cic.Implicit (Some `Type)
214 | Some typ -> aux ~localize loc context typ
216 Cic.Lambda (cic_name, typ, cic_body)
218 do_branch' context args
220 let indtype_uri, indtype_no =
221 if create_dummy_ids then
222 (UriManager.uri_of_string "cic:/fake_indty.con", 0)
224 match indty_ident with
225 | Some (indty_ident, _) ->
226 (match resolve env (Id indty_ident) () with
227 | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
229 raise (Try_again (lazy "The type of the term to be matched
232 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
234 let rec fst_constructor =
236 (Ast.Pattern (head, _, _), _) :: _ -> head
237 | (Ast.Wildcard, _) :: tl -> fst_constructor tl
238 | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))
240 (match resolve env (Id (fst_constructor branches)) () with
241 | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
242 (indtype_uri, indtype_no)
244 raise (Try_again (lazy "The type of the term to be matched
247 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
250 if create_dummy_ids then
253 Ast.Wildcard,term -> ("wildcard",None,[]), term
255 raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
258 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
259 Cic.InductiveDefinition (il,_,leftsno,_) ->
262 List.nth il indtype_no
263 with _ -> assert false
265 let rec count_prod t =
266 match CicReduction.whd [] t with
267 Cic.Prod (_, _, t) -> 1 + (count_prod t)
270 let rec sort branches cl =
273 let rec analyze unused unrecognized useless =
276 if unrecognized != [] then
277 raise (Invalid_choice
280 ("Unrecognized constructors: " ^
281 String.concat " " unrecognized)))
282 else if useless > 0 then
283 raise (Invalid_choice
286 ("The last " ^ string_of_int useless ^
287 "case" ^ if useless > 1 then "s are" else " is" ^
291 | (Ast.Wildcard,_)::tl when not unused ->
292 analyze true unrecognized useless tl
293 | (Ast.Pattern (head,_,_),_)::tl when not unused ->
294 analyze unused (head::unrecognized) useless tl
295 | _::tl -> analyze unused unrecognized (useless + 1) tl
297 analyze false [] 0 branches
299 let rec find_and_remove =
304 (Some loc, lazy ("Missing case: " ^ name)))
305 | ((Ast.Wildcard, _) as branch :: _) as branches ->
307 | (Ast.Pattern (name',_,_),_) as branch :: tl
311 let found,rest = find_and_remove tl in
314 let branch,tl = find_and_remove branches in
316 Ast.Pattern (name,y,args),term ->
317 if List.length args = count_prod ty - leftsno then
318 ((name,y,args),term)::sort tl cltl
323 lazy ("Wrong number of arguments for " ^ name)))
324 | Ast.Wildcard,term ->
330 (`Lambda, (CicNotationPt.Ident ("_", None), None),
333 (("wildcard",None,[]),
334 mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
339 Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
340 (List.map do_branch branches))
341 | CicNotationPt.Cast (t1, t2) ->
342 let cic_t1 = aux ~localize loc context t1 in
343 let cic_t2 = aux ~localize loc context t2 in
344 Cic.Cast (cic_t1, cic_t2)
345 | CicNotationPt.LetIn ((name, typ), def, body) ->
346 let cic_def = aux ~localize loc context def in
347 let cic_name = CicNotationUtil.cic_name_of_name name in
350 | None -> Cic.Implicit (Some `Type)
351 | Some t -> aux ~localize loc context t
353 let cic_body = aux ~localize loc (cic_name :: context) body in
354 Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
355 | CicNotationPt.LetRec (kind, defs, body) ->
358 (fun acc (_, (name, _), _, _) ->
359 CicNotationUtil.cic_name_of_name name :: acc)
363 let unlocalized_body = aux ~localize:false loc context' body in
364 match unlocalized_body with
365 Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
366 | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
371 let t',subst,metasenv =
372 CicMetaSubst.delift_rels [] [] (List.length defs) t
375 assert (metasenv=[]);
378 (* We can avoid the LetIn. But maybe we need to recompute l'
379 so that it is localized *)
382 CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
383 (* since we avoid the letin, the context has no
385 let l' = List.map (aux ~localize loc context) l in
391 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
393 `AddLetIn (aux ~localize loc context' body)
395 `AddLetIn unlocalized_body)
398 `AddLetIn (aux ~localize loc context' body)
400 `AddLetIn unlocalized_body
404 (fun (params, (name, typ), body, decr_idx) ->
405 let add_binders kind t =
407 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
410 aux ~localize loc context' (add_binders `Lambda body) in
412 aux_option ~localize loc context (Some `Type)
413 (HExtlib.map_option (add_binders `Pi) typ) in
415 match CicNotationUtil.cic_name_of_name name with
417 CicNotationPt.fail loc
418 "Recursive functions cannot be anonymous"
419 | Cic.Name name -> name
421 (name, decr_idx, cic_type, cic_body))
426 `Inductive -> Cic.Fix (n,inductiveFuns)
428 let coinductiveFuns =
430 (fun (name, _, typ, body) -> name, typ, body)
433 Cic.CoFix (n,coinductiveFuns)
435 let counter = ref ~-1 in
436 let build_term funs (var,_,ty,_) t =
438 Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
441 `AvoidLetInNoAppl n ->
442 let n' = List.length inductiveFuns - n in
444 | `AvoidLetIn (n,l) ->
445 let n' = List.length inductiveFuns - n in
446 Cic.Appl (fix_or_cofix n'::l)
447 | `AddLetIn cic_body ->
448 List.fold_right (build_term inductiveFuns) inductiveFuns
450 | CicNotationPt.Ident _
451 | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
452 | CicNotationPt.Ident (name, subst)
453 | CicNotationPt.Uri (name, subst) as ast ->
454 let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
456 if is_uri ast then raise Not_found;(* don't search the env for URIs *)
457 let index = find_in_context name context in
458 if subst <> None then
459 CicNotationPt.fail loc "Explicit substitutions not allowed here";
463 if is_uri ast then (* we have the URI, build the term out of it *)
465 CicUtil.term_of_uri (UriManager.uri_of_string name)
466 with UriManager.IllFormedUri _ ->
467 CicNotationPt.fail loc "Ill formed URI"
469 resolve env (Id name) ()
473 List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
480 List.assoc s ids_to_uris, aux ~localize loc context term
482 raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
484 | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
488 | Cic.Const (uri, []) ->
489 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
490 let uris = CicUtil.params_of_obj o in
491 Cic.Const (uri, mk_subst uris)
492 | Cic.Var (uri, []) ->
493 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
494 let uris = CicUtil.params_of_obj o in
495 Cic.Var (uri, mk_subst uris)
496 | Cic.MutInd (uri, i, []) ->
498 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
499 let uris = CicUtil.params_of_obj o in
500 Cic.MutInd (uri, i, mk_subst uris)
502 CicEnvironment.Object_not_found _ ->
503 (* if we are here it is probably the case that during the
504 definition of a mutual inductive type we have met an
505 occurrence of the type in one of its constructors.
506 However, the inductive type is not yet in the environment
508 (*here the explicit_named_substituion is assumed to be of length 0 *)
509 Cic.MutInd (uri,i,[]))
510 | Cic.MutConstruct (uri, i, j, []) ->
511 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
512 let uris = CicUtil.params_of_obj o in
513 Cic.MutConstruct (uri, i, j, mk_subst uris)
514 | Cic.Meta _ | Cic.Implicit _ as t ->
516 debug_print (lazy (sprintf
517 "Warning: %s must be instantiated with _[%s] but we do not enforce it"
521 (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
526 raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
528 CicEnvironment.CircularDependency _ ->
529 raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
530 | CicNotationPt.Implicit -> Cic.Implicit None
531 | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
532 | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
533 | CicNotationPt.Meta (index, subst) ->
538 | Some term -> Some (aux ~localize loc context term))
541 Cic.Meta (index, cic_subst)
542 | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
543 | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
544 | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
545 | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
546 | CicNotationPt.Symbol (symbol, instance) ->
547 resolve env (Symbol (symbol, instance)) ()
548 | _ -> assert false (* god bless Bologna *)
549 and aux_option ~localize loc (context: Cic.name list) annotation = function
550 | None -> Cic.Implicit annotation
551 | Some term -> aux ~localize loc context term
553 aux ~localize:true HExtlib.dummy_floc context ast
555 let interpretate_path ~context path =
556 let localization_tbl = Cic.CicHash.create 23 in
557 (* here we are throwing away useful localization informations!!! *)
559 interpretate_term ~create_dummy_ids:true
560 ~context ~env:Environment.empty ~uri:None ~is_path:true
561 path ~localization_tbl, localization_tbl)
563 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
564 assert (context = []);
565 assert (is_path = false);
566 let interpretate_term = interpretate_term ~localization_tbl in
568 | CicNotationPt.Inductive (params,tyl) ->
569 let uri = match uri with Some uri -> uri | None -> assert false in
573 (fun (context,res) (name,t) ->
576 None -> CicNotationPt.Implicit
578 let name = CicNotationUtil.cic_name_of_name name in
579 name::context,(name, interpretate_term context env None false t)::res
582 context,List.rev res in
584 List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
588 (*here the explicit_named_substituion is assumed to be of length 0 *)
589 (fun (i,res) (name,_,_,_) ->
590 i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
592 let con_env = DisambiguateTypes.env_of_list name_to_uris env in
595 (fun (name,b,ty,cl) ->
596 let ty' = add_params (interpretate_term context env None false ty) in
601 add_params (interpretate_term context con_env None false ty)
609 Cic.InductiveDefinition (tyl,[],List.length params,[])
610 | CicNotationPt.Record (params,name,ty,fields) ->
611 let uri = match uri with Some uri -> uri | None -> assert false in
615 (fun (context,res) (name,t) ->
618 None -> CicNotationPt.Implicit
620 let name = CicNotationUtil.cic_name_of_name name in
621 name::context,(name, interpretate_term context env None false t)::res
624 context,List.rev res in
627 (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
628 let ty' = add_params (interpretate_term context env None false ty) in
632 (fun (context,res) (name,ty,_coercion,arity) ->
633 let context' = Cic.Name name :: context in
634 context',(name,interpretate_term context env None false ty)::res
635 ) (context,[]) fields) in
637 (*here the explicit_named_substituion is assumed to be of length 0 *)
638 let mutind = Cic.MutInd (uri,0,[]) in
639 if params = [] then mutind
642 (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
645 (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
647 let con' = add_params con in
648 let tyl = [name,true,ty',["mk_" ^ name,con']] in
649 let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
650 Cic.InductiveDefinition
651 (tyl,[],List.length params,[`Class (`Record field_names)])
652 | CicNotationPt.Theorem (flavour, name, ty, bo) ->
653 let attrs = [`Flavour flavour] in
654 let ty' = interpretate_term [] env None false ty in
655 (match bo,flavour with
657 Cic.Constant (name,None,ty',[],attrs)
658 | Some bo,`Axiom -> assert false
660 Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
662 let bo' = Some (interpretate_term [] env None false bo) in
663 Cic.Constant (name,bo',ty',[],attrs))
665 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
666 | Ast.AttributedTerm (`Loc loc, term) ->
667 domain_of_term ~loc ~context term
668 | Ast.AttributedTerm (_, term) ->
669 domain_of_term ~loc ~context term
670 | Ast.Symbol (symbol, instance) ->
671 [ Node ([loc], Symbol (symbol, instance), []) ]
672 (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
673 | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
674 | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
678 (fun term acc -> domain_of_term ~loc ~context term @ acc)
682 Ast.AttributedTerm (`Loc loc,_) -> loc
685 [ Node ([loc], Symbol (symbol, instance), args_dom) ]
686 | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
687 | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
690 (fun term acc -> domain_of_term ~loc ~context term @ acc)
694 Ast.AttributedTerm (`Loc loc,_) -> loc
698 (* the next line can raise Not_found *)
699 ignore(find_in_context name context);
700 if subst <> None then
701 Ast.fail loc "Explicit substitutions not allowed here"
706 | None -> [ Node ([loc], Id name, args_dom) ]
710 (fun dom (_, term) ->
711 let dom' = domain_of_term ~loc ~context term in
714 [ Node ([loc], Id name, terms @ args_dom) ]))
717 (fun term acc -> domain_of_term ~loc ~context term @ acc)
719 | Ast.Binder (kind, (var, typ), body) ->
720 let type_dom = domain_of_term_option ~loc ~context typ in
723 ~context:(CicNotationUtil.cic_name_of_name var :: context) body in
725 | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
726 | _ -> type_dom @ body_dom)
727 | Ast.Case (term, indty_ident, outtype, branches) ->
728 let term_dom = domain_of_term ~loc ~context term in
729 let outtype_dom = domain_of_term_option ~loc ~context outtype in
730 let rec get_first_constructor = function
732 | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
733 | _ :: tl -> get_first_constructor tl in
736 Ast.Pattern (head, _, args), term ->
737 let (term_context, args_domain) =
739 (fun (cont, dom) (name, typ) ->
740 (CicNotationUtil.cic_name_of_name name :: cont,
743 | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
746 domain_of_term ~loc ~context:term_context term @ args_domain
747 | Ast.Wildcard, term ->
748 domain_of_term ~loc ~context term
751 List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
752 (match indty_ident with
753 | None -> get_first_constructor branches
754 | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
755 @ term_dom @ outtype_dom @ branches_dom
756 | Ast.Cast (term, ty) ->
757 let term_dom = domain_of_term ~loc ~context term in
758 let ty_dom = domain_of_term ~loc ~context ty in
760 | Ast.LetIn ((var, typ), body, where) ->
761 let body_dom = domain_of_term ~loc ~context body in
762 let type_dom = domain_of_term_option ~loc ~context typ in
765 ~context:(CicNotationUtil.cic_name_of_name var :: context) where in
766 body_dom @ type_dom @ where_dom
767 | Ast.LetRec (kind, defs, where) ->
768 let add_defs context =
770 (fun acc (_, (var, _), _, _) ->
771 CicNotationUtil.cic_name_of_name var :: acc
773 let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
776 (fun dom (params, (_, typ), body, _) ->
780 (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
786 (fun (context,res) (var,ty) ->
787 CicNotationUtil.cic_name_of_name var :: context,
788 domain_of_term_option ~loc ~context ty @ res)
789 (add_defs context,[]) params))
791 @ domain_of_term_option ~loc ~context:context' typ
792 @ domain_of_term ~loc ~context:context' body
796 | Ast.Ident (name, subst) ->
798 (* the next line can raise Not_found *)
799 ignore(find_in_context name context);
800 if subst <> None then
801 Ast.fail loc "Explicit substitutions not allowed here"
806 | None -> [ Node ([loc], Id name, []) ]
810 (fun dom (_, term) ->
811 let dom' = domain_of_term ~loc ~context term in
814 [ Node ([loc], Id name, terms) ]))
817 | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
818 | Ast.Meta (index, local_context) ->
820 (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
827 | Ast.Variable _ -> assert false
829 and domain_of_term_option ~loc ~context = function
831 | Some t -> domain_of_term ~loc ~context t
833 let domain_of_term ~context term =
834 uniq_domain (domain_of_term ~context term)
836 let domain_of_obj ~context ast =
837 assert (context = []);
839 | Ast.Theorem (_,_,ty,bo) ->
843 | Some bo -> domain_of_term [] bo)
844 | Ast.Inductive (params,tyl) ->
847 (fun (context, dom) (var, ty) ->
848 let context' = CicNotationUtil.cic_name_of_name var :: context in
850 None -> context', dom
851 | Some ty -> context', dom @ domain_of_term context ty
853 let context_w_types =
855 (fun (var, _, _, _) -> Cic.Name var) tyl
861 domain_of_term context ty
864 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
866 | CicNotationPt.Record (params,var,ty,fields) ->
869 (fun (context, dom) (var, ty) ->
870 let context' = CicNotationUtil.cic_name_of_name var :: context in
872 None -> context', dom
873 | Some ty -> context', dom @ domain_of_term context ty
875 let context_w_types = Cic.Name var :: context in
877 @ domain_of_term context ty
880 (fun (context,res) (name,ty,_,_) ->
881 Cic.Name name::context, res @ domain_of_term context ty
882 ) (context_w_types,[]) fields)
884 let domain_of_obj ~context obj =
885 uniq_domain (domain_of_obj ~context obj)
888 let domain_diff dom1 dom2 =
889 (* let domain_diff = Domain.diff *)
893 | Symbol (symb, 0) ->
895 Symbol (symb',_) when symb = symb' -> true
907 | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
908 | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
912 module type Disambiguator =
914 val disambiguate_term :
915 ?fresh_instances:bool ->
917 context:Cic.context ->
918 metasenv:Cic.metasenv ->
919 ?initial_ugraph:CicUniv.universe_graph ->
920 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
921 universe:DisambiguateTypes.multiple_environment option ->
922 CicNotationPt.term disambiguator_input ->
923 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
924 Cic.metasenv * (* new metasenv *)
926 CicUniv.universe_graph) list * (* disambiguated term *)
929 val disambiguate_obj :
930 ?fresh_instances:bool ->
932 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
933 universe:DisambiguateTypes.multiple_environment option ->
934 uri:UriManager.uri option -> (* required only for inductive types *)
935 CicNotationPt.term CicNotationPt.obj disambiguator_input ->
936 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
937 Cic.metasenv * (* new metasenv *)
939 CicUniv.universe_graph) list * (* disambiguated obj *)
943 module Make (C: Callbacks) =
945 let choices_of_id dbd id =
946 let uris = Whelp.locate ~dbd id in
951 (C.input_or_locate_uri
952 ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())
958 C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
959 ~ok:"Try selected." ~enable_button_for_non_vars:true
960 ~title:"Ambiguous input." ~id
961 ~msg: ("Ambiguous input \"" ^ id ^
962 "\". Please, choose one or more interpretations:")
967 (UriManager.string_of_uri uri,
970 CicUtil.term_of_uri uri
972 debug_print (lazy (UriManager.string_of_uri uri));
973 debug_print (lazy (Printexc.to_string exn));
979 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
981 let disambiguate_thing ~dbd ~context ~metasenv
982 ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
983 ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
984 (thing_txt,thing_txt_prefix_len,thing)
986 debug_print (lazy "DISAMBIGUATE INPUT");
987 let disambiguate_context = (* cic context -> disambiguate context *)
989 (function None -> Cic.Anonymous | Some (name, _) -> name)
992 debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
993 let thing_dom = domain_of_thing ~context:disambiguate_context thing in
995 (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
997 debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
998 (DisambiguatePp.pp_environment aliases)));
999 debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
1000 (match universe with None -> "None" | Some _ -> "Some _")));
1003 Environment.fold (fun item _ dom -> item :: dom) aliases [] in
1004 let todo_dom = domain_diff thing_dom current_dom in
1006 (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
1007 (* (2) lookup function for any item (Id/Symbol/Num) *)
1008 let lookup_choices =
1011 let lookup_in_library () =
1013 | Id id -> choices_of_id dbd id
1014 | Symbol (symb, _) ->
1016 List.map DisambiguateChoices.mk_choice
1017 (TermAcicContent.lookup_interpretations symb)
1019 TermAcicContent.Interpretation_not_found -> [])
1021 DisambiguateChoices.lookup_num_choices ()
1024 | None -> lookup_in_library ()
1029 | Symbol (symb, _) -> Symbol (symb, 0)
1032 Environment.find item e
1033 with Not_found -> lookup_in_library ())
1040 if benchmark then begin
1041 let per_item_choices =
1045 let len = List.length (lookup_choices dom_item) in
1046 debug_print (lazy (sprintf "BENCHMARK %s: %d"
1047 (string_of_domain_item dom_item) len));
1049 with No_choices _ -> 0)
1052 max_refinements := List.fold_left ( * ) 1 per_item_choices;
1053 actual_refinements := 0;
1054 domain_size := List.length thing_dom;
1056 (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
1062 (* (3) test an interpretation filling with meta uninterpreted identifiers
1064 let test_env aliases todo_dom ugraph =
1065 let rec aux env = function
1067 | Node (_, item, l) :: tl ->
1069 Environment.add item
1073 (fun _ _ _ -> Cic.Implicit (Some `Closed))
1074 | Symbol _ -> (fun _ _ _ -> Cic.Implicit None)))
1076 aux (aux env l) tl in
1077 let filled_env = aux aliases todo_dom in
1079 let localization_tbl = Cic.CicHash.create 503 in
1081 interpretate_thing ~context:disambiguate_context ~env:filled_env
1082 ~uri ~is_path:false thing ~localization_tbl
1086 refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
1089 in refine_profiler.HExtlib.profile foo ()
1091 | Try_again msg -> Uncertain (None,msg), ugraph
1092 | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph
1094 (* (4) build all possible interpretations *)
1095 let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
1096 (* aux returns triples Ok/Uncertain/Ko *)
1097 (* rem_dom is the concatenation of all the remainin domains *)
1098 let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ =
1099 debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
1102 assert (lookup_in_todo_dom = None);
1103 (match test_env aliases rem_dom base_univ with
1104 | Ok (thing, metasenv),new_univ ->
1105 [ aliases, diff, metasenv, thing, new_univ ], [], []
1106 | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true]
1107 | Uncertain (loc,msg),new_univ ->
1108 [],[aliases,diff,loc,msg,new_univ],[])
1109 | Node (locs,item,inner_dom) :: remaining_dom ->
1110 debug_print (lazy (sprintf "CHOOSED ITEM: %s"
1111 (string_of_domain_item item)));
1113 match lookup_in_todo_dom with
1114 None -> lookup_choices item
1115 | Some choices -> choices in
1119 [aliases, diff, Some (List.hd locs),
1120 lazy ("No choices for " ^ string_of_domain_item item),
1123 | [codomain_item] ->
1124 (* just one choice. We perform a one-step look-up and
1125 if the next set of choices is also a singleton we
1126 skip this refinement step *)
1127 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1128 let new_env = Environment.add item codomain_item aliases in
1129 let new_diff = (item,codomain_item)::diff in
1130 let lookup_in_todo_dom,next_choice_is_single =
1131 match remaining_dom with
1134 let choices = lookup_choices he in
1135 Some choices,List.length choices = 1
1137 if next_choice_is_single then
1138 aux new_env new_diff lookup_in_todo_dom remaining_dom
1141 (match test_env new_env remaining_dom base_univ with
1142 | Ok (thing, metasenv),new_univ ->
1143 (match remaining_dom with
1145 [ new_env, new_diff, metasenv, thing, new_univ ], []
1147 aux new_env new_diff lookup_in_todo_dom
1148 remaining_dom new_univ)
1149 | Uncertain (loc,msg),new_univ ->
1150 (match remaining_dom with
1151 | [] -> [], [new_env,new_diff,loc,msg,true]
1153 aux new_env new_diff lookup_in_todo_dom
1154 remaining_dom new_univ)
1155 | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
1158 let mark_not_significant failures =
1160 (fun (env, diff, loc, msg, _b) ->
1161 env, diff, loc, msg, false)
1163 let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
1164 if ok_l <> [] || uncertain_l <> [] then
1165 ok_l,uncertain_l,mark_not_significant error_l
1168 let rec filter univ = function
1170 | codomain_item :: tl ->
1171 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1172 let new_env = Environment.add item codomain_item aliases in
1173 let new_diff = (item,codomain_item)::diff in
1175 test_env new_env (inner_dom@remaining_dom@rem_dom) univ
1177 | Ok (thing, metasenv),new_univ ->
1179 (match inner_dom with
1181 [new_env,new_diff,metasenv,thing,new_univ], [], []
1183 aux new_env new_diff None inner_dom
1184 (remaining_dom@rem_dom) new_univ
1187 res @@ filter univ tl
1188 | Uncertain (loc,msg),new_univ ->
1190 (match inner_dom with
1191 | [] -> [],[new_env,new_diff,loc,msg,new_univ],[]
1193 aux new_env new_diff None inner_dom
1194 (remaining_dom@rem_dom) new_univ
1197 res @@ filter univ tl
1199 let res = [],[],[new_env,new_diff,loc,msg,true] in
1200 res @@ filter univ tl)
1202 let ok_l,uncertain_l,error_l =
1203 classify_errors (filter base_univ choices)
1205 let res_after_ok_l =
1207 (fun (env,diff,_,_,univ) res ->
1208 aux env diff None remaining_dom rem_dom univ @@ res
1209 ) ok_l ([],[],error_l)
1212 (fun (env,diff,_,_,univ) res ->
1213 aux env diff None remaining_dom rem_dom univ @@ res
1214 ) uncertain_l res_after_ok_l
1216 let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
1217 match test_env aliases todo_dom base_univ with
1220 aux aliases diff lookup_in_todo_dom todo_dom [] base_univ
1221 | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in
1222 let base_univ = initial_ugraph in
1225 match aux' aliases [] None todo_dom base_univ with
1226 | [],uncertain,errors ->
1229 (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true)
1230 ) uncertain @ errors
1234 (fun (env,diff,loc,msg,significant) ->
1237 (fun locs domain_item ->
1240 fst (Environment.find domain_item env)
1242 Some (locs,descr_of_domain_item domain_item,description)
1247 env',diff,loc,msg,significant
1250 raise (NoWellTypedInterpretation (0,errors))
1251 | [_,diff,metasenv,t,ugraph],_,_ ->
1252 debug_print (lazy "SINGLE INTERPRETATION");
1253 [diff,metasenv,t,ugraph], false
1256 (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
1259 (fun (env, _, _, _, _) ->
1261 (fun locs domain_item ->
1263 fst (Environment.find domain_item env)
1265 locs,descr_of_domain_item domain_item, description)
1270 C.interactive_interpretation_choice
1271 thing_txt thing_txt_prefix_len choices
1273 (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
1278 CicEnvironment.CircularDependency s ->
1279 failwith "Disambiguate: circular dependency"
1281 let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
1282 ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
1283 (text,prefix_len,term)
1286 if fresh_instances then CicNotationUtil.freshen_term term else term
1288 disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
1289 ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
1290 ~domain_of_thing:domain_of_term
1291 ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
1292 ~refine_thing:refine_term (text,prefix_len,term)
1294 let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
1295 (text,prefix_len,obj)
1298 if fresh_instances then CicNotationUtil.freshen_obj obj else obj
1300 disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
1301 ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
1302 ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
1303 (text,prefix_len,obj)