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,'m) test_result =
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 ~env ~uri ~is_path ast
178 (* create_dummy_ids shouldbe used only for interpretating patterns *)
180 let rec aux ~localize loc context = 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 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))
666 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
669 let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
670 interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
675 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
676 | Ast.AttributedTerm (`Loc loc, term) ->
677 domain_of_term ~loc ~context term
678 | Ast.AttributedTerm (_, term) ->
679 domain_of_term ~loc ~context term
680 | Ast.Symbol (symbol, instance) ->
681 [ Node ([loc], Symbol (symbol, instance), []) ]
682 (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
683 | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
684 | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
688 (fun term acc -> domain_of_term ~loc ~context term @ acc)
692 Ast.AttributedTerm (`Loc loc,_) -> loc
695 [ Node ([loc], Symbol (symbol, instance), args_dom) ]
696 | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
697 | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
700 (fun term acc -> domain_of_term ~loc ~context term @ acc)
704 Ast.AttributedTerm (`Loc loc,_) -> loc
708 (* the next line can raise Not_found *)
709 ignore(find_in_context name context);
710 if subst <> None then
711 Ast.fail loc "Explicit substitutions not allowed here"
716 | None -> [ Node ([loc], Id name, args_dom) ]
720 (fun dom (_, term) ->
721 let dom' = domain_of_term ~loc ~context term in
724 [ Node ([loc], Id name, terms @ args_dom) ]))
727 (fun term acc -> domain_of_term ~loc ~context term @ acc)
729 | Ast.Binder (kind, (var, typ), body) ->
730 let type_dom = domain_of_term_option ~loc ~context typ in
733 ~context:(CicNotationUtil.cic_name_of_name var :: context) body in
735 | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
736 | _ -> type_dom @ body_dom)
737 | Ast.Case (term, indty_ident, outtype, branches) ->
738 let term_dom = domain_of_term ~loc ~context term in
739 let outtype_dom = domain_of_term_option ~loc ~context outtype in
740 let rec get_first_constructor = function
742 | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
743 | _ :: tl -> get_first_constructor tl in
746 Ast.Pattern (head, _, args), term ->
747 let (term_context, args_domain) =
749 (fun (cont, dom) (name, typ) ->
750 (CicNotationUtil.cic_name_of_name name :: cont,
753 | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
756 domain_of_term ~loc ~context:term_context term @ args_domain
757 | Ast.Wildcard, term ->
758 domain_of_term ~loc ~context term
761 List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
762 (match indty_ident with
763 | None -> get_first_constructor branches
764 | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
765 @ term_dom @ outtype_dom @ branches_dom
766 | Ast.Cast (term, ty) ->
767 let term_dom = domain_of_term ~loc ~context term in
768 let ty_dom = domain_of_term ~loc ~context ty in
770 | Ast.LetIn ((var, typ), body, where) ->
771 let body_dom = domain_of_term ~loc ~context body in
772 let type_dom = domain_of_term_option ~loc ~context typ in
775 ~context:(CicNotationUtil.cic_name_of_name var :: context) where in
776 body_dom @ type_dom @ where_dom
777 | Ast.LetRec (kind, defs, where) ->
778 let add_defs context =
780 (fun acc (_, (var, _), _, _) ->
781 CicNotationUtil.cic_name_of_name var :: acc
783 let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
786 (fun dom (params, (_, typ), body, _) ->
790 (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
796 (fun (context,res) (var,ty) ->
797 CicNotationUtil.cic_name_of_name var :: context,
798 domain_of_term_option ~loc ~context ty @ res)
799 (add_defs context,[]) params))
801 @ domain_of_term_option ~loc ~context:context' typ
802 @ domain_of_term ~loc ~context:context' body
806 | Ast.Ident (name, subst) ->
808 (* the next line can raise Not_found *)
809 ignore(find_in_context name context);
810 if subst <> None then
811 Ast.fail loc "Explicit substitutions not allowed here"
816 | None -> [ Node ([loc], Id name, []) ]
820 (fun dom (_, term) ->
821 let dom' = domain_of_term ~loc ~context term in
824 [ Node ([loc], Id name, terms) ]))
827 | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
828 | Ast.Meta (index, local_context) ->
830 (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
837 | Ast.Variable _ -> assert false
839 and domain_of_term_option ~loc ~context = function
841 | Some t -> domain_of_term ~loc ~context t
843 let domain_of_term ~context term =
844 uniq_domain (domain_of_term ~context term)
846 let domain_of_obj ~context ast =
847 let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
848 assert (context = []);
850 | Ast.Theorem (_,_,ty,bo) ->
854 | Some bo -> domain_of_term [] bo)
855 | Ast.Inductive (params,tyl) ->
858 (fun (context, dom) (var, ty) ->
859 let context' = CicNotationUtil.cic_name_of_name var :: context in
861 None -> context', dom
862 | Some ty -> context', dom @ domain_of_term context ty
864 let context_w_types =
866 (fun (var, _, _, _) -> Cic.Name var) tyl
872 domain_of_term context ty
875 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
877 | CicNotationPt.Record (params,var,ty,fields) ->
880 (fun (context, dom) (var, ty) ->
881 let context' = CicNotationUtil.cic_name_of_name var :: context in
883 None -> context', dom
884 | Some ty -> context', dom @ domain_of_term context ty
886 let context_w_types = Cic.Name var :: context in
888 @ domain_of_term context ty
891 (fun (context,res) (name,ty,_,_) ->
892 Cic.Name name::context, res @ domain_of_term context ty
893 ) (context_w_types,[]) fields)
895 let domain_of_obj ~context obj =
896 uniq_domain (domain_of_obj ~context obj)
898 let domain_of_ast_term = domain_of_term;;
900 let domain_of_term ~context term =
902 List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
904 domain_of_term ~context term
907 let domain_diff dom1 dom2 =
908 (* let domain_diff = Domain.diff *)
912 | Symbol (symb, 0) ->
914 Symbol (symb',_) when symb = symb' -> true
926 | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
927 | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
931 module type Disambiguator =
933 val disambiguate_thing:
936 metasenv:'metasenv ->
937 initial_ugraph:'ugraph ->
938 hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
939 (('refined_thing,'metasenv) test_result -> 'ugraph ->
940 ('refined_thing,'metasenv) test_result * 'ugraph) ->
941 aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
942 universe:DisambiguateTypes.codomain_item list
943 DisambiguateTypes.Environment.t option ->
945 pp_thing:('ast_thing -> string) ->
946 domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
947 interpretate_thing:(context:'context ->
948 env:DisambiguateTypes.codomain_item
949 DisambiguateTypes.Environment.t ->
951 is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
952 refine_thing:('metasenv ->
956 'ugraph -> localization_tbl:'cichash -> ('refined_thing,
957 'metasenv) test_result * 'ugraph) ->
958 localization_tbl:'cichash ->
959 string * int * 'ast_thing ->
960 ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
961 list * 'metasenv * 'refined_thing * 'ugraph)
964 val disambiguate_term :
965 ?fresh_instances:bool ->
967 context:Cic.context ->
968 metasenv:Cic.metasenv -> ?goal:int ->
969 ?initial_ugraph:CicUniv.universe_graph ->
970 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
971 universe:DisambiguateTypes.multiple_environment option ->
972 CicNotationPt.term disambiguator_input ->
973 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
974 Cic.metasenv * (* new metasenv *)
976 CicUniv.universe_graph) list * (* disambiguated term *)
979 val disambiguate_obj :
980 ?fresh_instances:bool ->
982 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
983 universe:DisambiguateTypes.multiple_environment option ->
984 uri:UriManager.uri option -> (* required only for inductive types *)
985 CicNotationPt.term CicNotationPt.obj disambiguator_input ->
986 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
987 Cic.metasenv * (* new metasenv *)
989 CicUniv.universe_graph) list * (* disambiguated obj *)
993 module Make (C: Callbacks) =
995 let choices_of_id dbd id =
996 let uris = Whelp.locate ~dbd id in
1001 (C.input_or_locate_uri
1002 ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())
1005 | Some uri -> [uri])
1008 C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
1009 ~ok:"Try selected." ~enable_button_for_non_vars:true
1010 ~title:"Ambiguous input." ~id
1011 ~msg: ("Ambiguous input \"" ^ id ^
1012 "\". Please, choose one or more interpretations:")
1017 (UriManager.string_of_uri uri,
1020 CicUtil.term_of_uri uri
1022 debug_print (lazy (UriManager.string_of_uri uri));
1023 debug_print (lazy (Printexc.to_string exn));
1029 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
1031 let disambiguate_thing ~dbd ~context ~metasenv
1032 ~initial_ugraph ~hint
1034 ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
1036 (thing_txt,thing_txt_prefix_len,thing)
1038 debug_print (lazy "DISAMBIGUATE INPUT");
1039 debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
1040 let thing_dom = domain_of_thing ~context thing in
1042 (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
1044 debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
1045 (DisambiguatePp.pp_environment aliases)));
1046 debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
1047 (match universe with None -> "None" | Some _ -> "Some _")));
1050 Environment.fold (fun item _ dom -> item :: dom) aliases [] in
1051 let todo_dom = domain_diff thing_dom current_dom in
1053 (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
1054 (* (2) lookup function for any item (Id/Symbol/Num) *)
1055 let lookup_choices =
1058 let lookup_in_library () =
1060 | Id id -> choices_of_id dbd id
1061 | Symbol (symb, _) ->
1063 List.map DisambiguateChoices.mk_choice
1064 (TermAcicContent.lookup_interpretations symb)
1066 TermAcicContent.Interpretation_not_found -> [])
1068 DisambiguateChoices.lookup_num_choices ()
1071 | None -> lookup_in_library ()
1076 | Symbol (symb, _) -> Symbol (symb, 0)
1079 Environment.find item e
1080 with Not_found -> lookup_in_library ())
1087 if benchmark then begin
1088 let per_item_choices =
1092 let len = List.length (lookup_choices dom_item) in
1093 debug_print (lazy (sprintf "BENCHMARK %s: %d"
1094 (string_of_domain_item dom_item) len));
1096 with No_choices _ -> 0)
1099 max_refinements := List.fold_left ( * ) 1 per_item_choices;
1100 actual_refinements := 0;
1101 domain_size := List.length thing_dom;
1103 (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
1109 (* (3) test an interpretation filling with meta uninterpreted identifiers
1111 let test_env aliases todo_dom ugraph =
1112 let rec aux env = function
1114 | Node (_, item, l) :: tl ->
1116 Environment.add item
1120 (fun _ _ _ -> Cic.Implicit (Some `Closed))
1121 | Symbol _ -> (fun _ _ _ -> Cic.Implicit None)))
1123 aux (aux env l) tl in
1124 let filled_env = aux aliases todo_dom in
1127 interpretate_thing ~context ~env:filled_env
1128 ~uri ~is_path:false thing ~localization_tbl
1130 let cic_thing = (fst hint) metasenv cic_thing in
1133 refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
1135 let k, ugraph1 = (snd hint) k ugraph1 in
1137 in refine_profiler.HExtlib.profile foo ()
1139 | Try_again msg -> Uncertain (None,msg), ugraph
1140 | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph
1142 (* (4) build all possible interpretations *)
1143 let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
1144 (* aux returns triples Ok/Uncertain/Ko *)
1145 (* rem_dom is the concatenation of all the remainin domains *)
1146 let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ =
1147 debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
1150 assert (lookup_in_todo_dom = None);
1151 (match test_env aliases rem_dom base_univ with
1152 | Ok (thing, metasenv),new_univ ->
1153 [ aliases, diff, metasenv, thing, new_univ ], [], []
1154 | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true]
1155 | Uncertain (loc,msg),new_univ ->
1156 [],[aliases,diff,loc,msg,new_univ],[])
1157 | Node (locs,item,inner_dom) :: remaining_dom ->
1158 debug_print (lazy (sprintf "CHOOSED ITEM: %s"
1159 (string_of_domain_item item)));
1161 match lookup_in_todo_dom with
1162 None -> lookup_choices item
1163 | Some choices -> choices in
1167 [aliases, diff, Some (List.hd locs),
1168 lazy ("No choices for " ^ string_of_domain_item item),
1171 | [codomain_item] ->
1172 (* just one choice. We perform a one-step look-up and
1173 if the next set of choices is also a singleton we
1174 skip this refinement step *)
1175 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1176 let new_env = Environment.add item codomain_item aliases in
1177 let new_diff = (item,codomain_item)::diff in
1178 let lookup_in_todo_dom,next_choice_is_single =
1179 match remaining_dom with
1182 let choices = lookup_choices he in
1183 Some choices,List.length choices = 1
1185 if next_choice_is_single then
1186 aux new_env new_diff lookup_in_todo_dom remaining_dom
1189 (match test_env new_env remaining_dom base_univ with
1190 | Ok (thing, metasenv),new_univ ->
1191 (match remaining_dom with
1193 [ new_env, new_diff, metasenv, thing, new_univ ], []
1195 aux new_env new_diff lookup_in_todo_dom
1196 remaining_dom new_univ)
1197 | Uncertain (loc,msg),new_univ ->
1198 (match remaining_dom with
1199 | [] -> [], [new_env,new_diff,loc,msg,true]
1201 aux new_env new_diff lookup_in_todo_dom
1202 remaining_dom new_univ)
1203 | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
1206 let mark_not_significant failures =
1208 (fun (env, diff, loc, msg, _b) ->
1209 env, diff, loc, msg, false)
1211 let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
1212 if ok_l <> [] || uncertain_l <> [] then
1213 ok_l,uncertain_l,mark_not_significant error_l
1216 let rec filter univ = function
1218 | codomain_item :: tl ->
1219 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1220 let new_env = Environment.add item codomain_item aliases in
1221 let new_diff = (item,codomain_item)::diff in
1223 test_env new_env (inner_dom@remaining_dom@rem_dom) univ
1225 | Ok (thing, metasenv),new_univ ->
1227 (match inner_dom with
1229 [new_env,new_diff,metasenv,thing,new_univ], [], []
1231 aux new_env new_diff None inner_dom
1232 (remaining_dom@rem_dom) new_univ
1235 res @@ filter univ tl
1236 | Uncertain (loc,msg),new_univ ->
1238 (match inner_dom with
1239 | [] -> [],[new_env,new_diff,loc,msg,new_univ],[]
1241 aux new_env new_diff None inner_dom
1242 (remaining_dom@rem_dom) new_univ
1245 res @@ filter univ tl
1247 let res = [],[],[new_env,new_diff,loc,msg,true] in
1248 res @@ filter univ tl)
1250 let ok_l,uncertain_l,error_l =
1251 classify_errors (filter base_univ choices)
1253 let res_after_ok_l =
1255 (fun (env,diff,_,_,univ) res ->
1256 aux env diff None remaining_dom rem_dom univ @@ res
1257 ) ok_l ([],[],error_l)
1260 (fun (env,diff,_,_,univ) res ->
1261 aux env diff None remaining_dom rem_dom univ @@ res
1262 ) uncertain_l res_after_ok_l
1264 let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
1265 match test_env aliases todo_dom base_univ with
1268 aux aliases diff lookup_in_todo_dom todo_dom [] base_univ
1269 | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in
1270 let base_univ = initial_ugraph in
1273 match aux' aliases [] None todo_dom base_univ with
1274 | [],uncertain,errors ->
1277 (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true)
1278 ) uncertain @ errors
1282 (fun (env,diff,loc,msg,significant) ->
1285 (fun locs domain_item ->
1288 fst (Environment.find domain_item env)
1290 Some (locs,descr_of_domain_item domain_item,description)
1295 env',diff,loc,msg,significant
1298 raise (NoWellTypedInterpretation (0,errors))
1299 | [_,diff,metasenv,t,ugraph],_,_ ->
1300 debug_print (lazy "SINGLE INTERPRETATION");
1301 [diff,metasenv,t,ugraph], false
1304 (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
1307 (fun (env, _, _, _, _) ->
1309 (fun locs domain_item ->
1311 fst (Environment.find domain_item env)
1313 locs,descr_of_domain_item domain_item, description)
1318 C.interactive_interpretation_choice
1319 thing_txt thing_txt_prefix_len choices
1321 (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
1326 CicEnvironment.CircularDependency s ->
1327 failwith "Disambiguate: circular dependency"
1329 let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
1331 ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
1332 (text,prefix_len,term)
1335 if fresh_instances then CicNotationUtil.freshen_term term else term
1337 let hint = match goal with
1338 | None -> (fun _ x -> x), fun k u -> k, u
1341 let _,c,ty = CicUtil.lookup_meta i metasenv in
1345 | Ok (t,m) -> fun ug ->
1347 | Cic.Cast(t,_) -> Ok (t,m), ug
1348 | _ -> assert false)
1349 | k -> fun ug -> k, ug
1351 let localization_tbl = Cic.CicHash.create 503 in
1352 disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
1353 ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
1354 ~domain_of_thing:domain_of_term
1355 ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
1356 ~refine_thing:refine_term (text,prefix_len,term)
1360 let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
1361 (text,prefix_len,obj)
1364 if fresh_instances then CicNotationUtil.freshen_obj obj else obj
1370 let localization_tbl = Cic.CicHash.create 503 in
1371 disambiguate_thing ~dbd ~context:[] ~metasenv:[]
1372 ~aliases ~universe ~uri
1373 ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
1374 ~initial_ugraph:CicUniv.empty_ugraph
1375 ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
1378 (text,prefix_len,obj)