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 let l' = List.map (aux ~localize loc context') l in
389 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
391 `AddLetIn (aux ~localize loc context' body)
393 `AddLetIn unlocalized_body)
396 `AddLetIn (aux ~localize loc context' body)
398 `AddLetIn unlocalized_body
402 (fun (params, (name, typ), body, decr_idx) ->
403 let add_binders kind t =
405 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
408 aux ~localize loc context' (add_binders `Lambda body) in
410 aux_option ~localize loc context (Some `Type)
411 (HExtlib.map_option (add_binders `Pi) typ) in
413 match CicNotationUtil.cic_name_of_name name with
415 CicNotationPt.fail loc
416 "Recursive functions cannot be anonymous"
417 | Cic.Name name -> name
419 (name, decr_idx, cic_type, cic_body))
424 `Inductive -> Cic.Fix (n,inductiveFuns)
426 let coinductiveFuns =
428 (fun (name, _, typ, body) -> name, typ, body)
431 Cic.CoFix (n,coinductiveFuns)
433 let counter = ref ~-1 in
434 let build_term funs (var,_,ty,_) t =
436 Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
439 `AvoidLetInNoAppl n ->
440 let n' = List.length inductiveFuns - n in
442 | `AvoidLetIn (n,l) ->
443 let n' = List.length inductiveFuns - n in
444 Cic.Appl (fix_or_cofix n'::l)
445 | `AddLetIn cic_body ->
446 List.fold_right (build_term inductiveFuns) inductiveFuns
448 | CicNotationPt.Ident _
449 | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
450 | CicNotationPt.Ident (name, subst)
451 | CicNotationPt.Uri (name, subst) as ast ->
452 let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
454 if is_uri ast then raise Not_found;(* don't search the env for URIs *)
455 let index = find_in_context name context in
456 if subst <> None then
457 CicNotationPt.fail loc "Explicit substitutions not allowed here";
461 if is_uri ast then (* we have the URI, build the term out of it *)
463 CicUtil.term_of_uri (UriManager.uri_of_string name)
464 with UriManager.IllFormedUri _ ->
465 CicNotationPt.fail loc "Ill formed URI"
467 resolve env (Id name) ()
471 List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
478 List.assoc s ids_to_uris, aux ~localize loc context term
480 raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
482 | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
486 | Cic.Const (uri, []) ->
487 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
488 let uris = CicUtil.params_of_obj o in
489 Cic.Const (uri, mk_subst uris)
490 | Cic.Var (uri, []) ->
491 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
492 let uris = CicUtil.params_of_obj o in
493 Cic.Var (uri, mk_subst uris)
494 | Cic.MutInd (uri, i, []) ->
496 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
497 let uris = CicUtil.params_of_obj o in
498 Cic.MutInd (uri, i, mk_subst uris)
500 CicEnvironment.Object_not_found _ ->
501 (* if we are here it is probably the case that during the
502 definition of a mutual inductive type we have met an
503 occurrence of the type in one of its constructors.
504 However, the inductive type is not yet in the environment
506 (*here the explicit_named_substituion is assumed to be of length 0 *)
507 Cic.MutInd (uri,i,[]))
508 | Cic.MutConstruct (uri, i, j, []) ->
509 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
510 let uris = CicUtil.params_of_obj o in
511 Cic.MutConstruct (uri, i, j, mk_subst uris)
512 | Cic.Meta _ | Cic.Implicit _ as t ->
514 debug_print (lazy (sprintf
515 "Warning: %s must be instantiated with _[%s] but we do not enforce it"
519 (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
524 raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
526 CicEnvironment.CircularDependency _ ->
527 raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
528 | CicNotationPt.Implicit -> Cic.Implicit None
529 | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
530 | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
531 | CicNotationPt.Meta (index, subst) ->
536 | Some term -> Some (aux ~localize loc context term))
539 Cic.Meta (index, cic_subst)
540 | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
541 | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
542 | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
543 | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
544 | CicNotationPt.Symbol (symbol, instance) ->
545 resolve env (Symbol (symbol, instance)) ()
546 | _ -> assert false (* god bless Bologna *)
547 and aux_option ~localize loc (context: Cic.name list) annotation = function
548 | None -> Cic.Implicit annotation
549 | Some term -> aux ~localize loc context term
551 aux ~localize:true HExtlib.dummy_floc context ast
553 let interpretate_path ~context path =
554 let localization_tbl = Cic.CicHash.create 23 in
555 (* here we are throwing away useful localization informations!!! *)
557 interpretate_term ~create_dummy_ids:true
558 ~context ~env:Environment.empty ~uri:None ~is_path:true
559 path ~localization_tbl, localization_tbl)
561 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
562 assert (context = []);
563 assert (is_path = false);
564 let interpretate_term = interpretate_term ~localization_tbl in
566 | CicNotationPt.Inductive (params,tyl) ->
567 let uri = match uri with Some uri -> uri | None -> assert false in
571 (fun (context,res) (name,t) ->
574 None -> CicNotationPt.Implicit
576 let name = CicNotationUtil.cic_name_of_name name in
577 name::context,(name, interpretate_term context env None false t)::res
580 context,List.rev res in
582 List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
586 (*here the explicit_named_substituion is assumed to be of length 0 *)
587 (fun (i,res) (name,_,_,_) ->
588 i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
590 let con_env = DisambiguateTypes.env_of_list name_to_uris env in
593 (fun (name,b,ty,cl) ->
594 let ty' = add_params (interpretate_term context env None false ty) in
599 add_params (interpretate_term context con_env None false ty)
607 Cic.InductiveDefinition (tyl,[],List.length params,[])
608 | CicNotationPt.Record (params,name,ty,fields) ->
609 let uri = match uri with Some uri -> uri | None -> assert false in
613 (fun (context,res) (name,t) ->
616 None -> CicNotationPt.Implicit
618 let name = CicNotationUtil.cic_name_of_name name in
619 name::context,(name, interpretate_term context env None false t)::res
622 context,List.rev res in
625 (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
626 let ty' = add_params (interpretate_term context env None false ty) in
630 (fun (context,res) (name,ty,_coercion,arity) ->
631 let context' = Cic.Name name :: context in
632 context',(name,interpretate_term context env None false ty)::res
633 ) (context,[]) fields) in
635 (*here the explicit_named_substituion is assumed to be of length 0 *)
636 let mutind = Cic.MutInd (uri,0,[]) in
637 if params = [] then mutind
640 (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
643 (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
645 let con' = add_params con in
646 let tyl = [name,true,ty',["mk_" ^ name,con']] in
647 let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
648 Cic.InductiveDefinition
649 (tyl,[],List.length params,[`Class (`Record field_names)])
650 | CicNotationPt.Theorem (flavour, name, ty, bo) ->
651 let attrs = [`Flavour flavour] in
652 let ty' = interpretate_term [] env None false ty in
653 (match bo,flavour with
655 Cic.Constant (name,None,ty',[],attrs)
656 | Some bo,`Axiom -> assert false
658 Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
660 let bo' = Some (interpretate_term [] env None false bo) in
661 Cic.Constant (name,bo',ty',[],attrs))
663 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
664 | Ast.AttributedTerm (`Loc loc, term) ->
665 domain_of_term ~loc ~context term
666 | Ast.AttributedTerm (_, term) ->
667 domain_of_term ~loc ~context term
668 | Ast.Symbol (symbol, instance) ->
669 [ Node ([loc], Symbol (symbol, instance), []) ]
670 (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
671 | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
672 | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
676 (fun term acc -> domain_of_term ~loc ~context term @ acc)
680 Ast.AttributedTerm (`Loc loc,_) -> loc
683 [ Node ([loc], Symbol (symbol, instance), args_dom) ]
684 | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
685 | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
688 (fun term acc -> domain_of_term ~loc ~context term @ acc)
692 Ast.AttributedTerm (`Loc loc,_) -> loc
696 (* the next line can raise Not_found *)
697 ignore(find_in_context name context);
698 if subst <> None then
699 Ast.fail loc "Explicit substitutions not allowed here"
704 | None -> [ Node ([loc], Id name, args_dom) ]
708 (fun dom (_, term) ->
709 let dom' = domain_of_term ~loc ~context term in
712 [ Node ([loc], Id name, terms @ args_dom) ]))
715 (fun term acc -> domain_of_term ~loc ~context term @ acc)
717 | Ast.Binder (kind, (var, typ), body) ->
718 let type_dom = domain_of_term_option ~loc ~context typ in
721 ~context:(CicNotationUtil.cic_name_of_name var :: context) body in
723 | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
724 | _ -> type_dom @ body_dom)
725 | Ast.Case (term, indty_ident, outtype, branches) ->
726 let term_dom = domain_of_term ~loc ~context term in
727 let outtype_dom = domain_of_term_option ~loc ~context outtype in
728 let rec get_first_constructor = function
730 | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
731 | _ :: tl -> get_first_constructor tl in
734 Ast.Pattern (head, _, args), term ->
735 let (term_context, args_domain) =
737 (fun (cont, dom) (name, typ) ->
738 (CicNotationUtil.cic_name_of_name name :: cont,
741 | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
744 domain_of_term ~loc ~context:term_context term @ args_domain
745 | Ast.Wildcard, term ->
746 domain_of_term ~loc ~context term
749 List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
750 (match indty_ident with
751 | None -> get_first_constructor branches
752 | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
753 @ term_dom @ outtype_dom @ branches_dom
754 | Ast.Cast (term, ty) ->
755 let term_dom = domain_of_term ~loc ~context term in
756 let ty_dom = domain_of_term ~loc ~context ty in
758 | Ast.LetIn ((var, typ), body, where) ->
759 let body_dom = domain_of_term ~loc ~context body in
760 let type_dom = domain_of_term_option ~loc ~context typ in
763 ~context:(CicNotationUtil.cic_name_of_name var :: context) where in
764 body_dom @ type_dom @ where_dom
765 | Ast.LetRec (kind, defs, where) ->
766 let add_defs context =
768 (fun acc (_, (var, _), _, _) ->
769 CicNotationUtil.cic_name_of_name var :: acc
771 let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
774 (fun dom (params, (_, typ), body, _) ->
778 (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
784 (fun (context,res) (var,ty) ->
785 CicNotationUtil.cic_name_of_name var :: context,
786 domain_of_term_option ~loc ~context ty @ res)
787 (add_defs context,[]) params))
789 @ domain_of_term_option ~loc ~context:context' typ
790 @ domain_of_term ~loc ~context:context' body
794 | Ast.Ident (name, subst) ->
796 (* the next line can raise Not_found *)
797 ignore(find_in_context name context);
798 if subst <> None then
799 Ast.fail loc "Explicit substitutions not allowed here"
804 | None -> [ Node ([loc], Id name, []) ]
808 (fun dom (_, term) ->
809 let dom' = domain_of_term ~loc ~context term in
812 [ Node ([loc], Id name, terms) ]))
815 | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
816 | Ast.Meta (index, local_context) ->
818 (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
825 | Ast.Variable _ -> assert false
827 and domain_of_term_option ~loc ~context = function
829 | Some t -> domain_of_term ~loc ~context t
831 let domain_of_term ~context term =
832 uniq_domain (domain_of_term ~context term)
834 let domain_of_obj ~context ast =
835 assert (context = []);
837 | Ast.Theorem (_,_,ty,bo) ->
841 | Some bo -> domain_of_term [] bo)
842 | Ast.Inductive (params,tyl) ->
845 (fun (context, dom) (var, ty) ->
846 let context' = CicNotationUtil.cic_name_of_name var :: context in
848 None -> context', dom
849 | Some ty -> context', dom @ domain_of_term context ty
851 let context_w_types =
853 (fun (var, _, _, _) -> Cic.Name var) tyl
859 domain_of_term context ty
862 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
864 | CicNotationPt.Record (params,var,ty,fields) ->
867 (fun (context, dom) (var, ty) ->
868 let context' = CicNotationUtil.cic_name_of_name var :: context in
870 None -> context', dom
871 | Some ty -> context', dom @ domain_of_term context ty
873 let context_w_types = Cic.Name var :: context in
875 @ domain_of_term context ty
878 (fun (context,res) (name,ty,_,_) ->
879 Cic.Name name::context, res @ domain_of_term context ty
880 ) (context_w_types,[]) fields)
882 let domain_of_obj ~context obj =
883 uniq_domain (domain_of_obj ~context obj)
886 let domain_diff dom1 dom2 =
887 (* let domain_diff = Domain.diff *)
891 | Symbol (symb, 0) ->
893 Symbol (symb',_) when symb = symb' -> true
905 | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
906 | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
910 module type Disambiguator =
912 val disambiguate_term :
913 ?fresh_instances:bool ->
915 context:Cic.context ->
916 metasenv:Cic.metasenv ->
917 ?initial_ugraph:CicUniv.universe_graph ->
918 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
919 universe:DisambiguateTypes.multiple_environment option ->
920 CicNotationPt.term disambiguator_input ->
921 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
922 Cic.metasenv * (* new metasenv *)
924 CicUniv.universe_graph) list * (* disambiguated term *)
927 val disambiguate_obj :
928 ?fresh_instances:bool ->
930 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
931 universe:DisambiguateTypes.multiple_environment option ->
932 uri:UriManager.uri option -> (* required only for inductive types *)
933 CicNotationPt.term CicNotationPt.obj disambiguator_input ->
934 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
935 Cic.metasenv * (* new metasenv *)
937 CicUniv.universe_graph) list * (* disambiguated obj *)
941 module Make (C: Callbacks) =
943 let choices_of_id dbd id =
944 let uris = Whelp.locate ~dbd id in
949 (C.input_or_locate_uri
950 ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())
956 C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
957 ~ok:"Try selected." ~enable_button_for_non_vars:true
958 ~title:"Ambiguous input." ~id
959 ~msg: ("Ambiguous input \"" ^ id ^
960 "\". Please, choose one or more interpretations:")
965 (UriManager.string_of_uri uri,
968 CicUtil.term_of_uri uri
970 debug_print (lazy (UriManager.string_of_uri uri));
971 debug_print (lazy (Printexc.to_string exn));
977 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
979 let disambiguate_thing ~dbd ~context ~metasenv
980 ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
981 ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
982 (thing_txt,thing_txt_prefix_len,thing)
984 debug_print (lazy "DISAMBIGUATE INPUT");
985 let disambiguate_context = (* cic context -> disambiguate context *)
987 (function None -> Cic.Anonymous | Some (name, _) -> name)
990 debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
991 let thing_dom = domain_of_thing ~context:disambiguate_context thing in
993 (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
995 debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
996 (DisambiguatePp.pp_environment aliases)));
997 debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
998 (match universe with None -> "None" | Some _ -> "Some _")));
1001 Environment.fold (fun item _ dom -> item :: dom) aliases [] in
1002 let todo_dom = domain_diff thing_dom current_dom in
1004 (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
1005 (* (2) lookup function for any item (Id/Symbol/Num) *)
1006 let lookup_choices =
1009 let lookup_in_library () =
1011 | Id id -> choices_of_id dbd id
1012 | Symbol (symb, _) ->
1014 List.map DisambiguateChoices.mk_choice
1015 (TermAcicContent.lookup_interpretations symb)
1017 TermAcicContent.Interpretation_not_found -> [])
1019 DisambiguateChoices.lookup_num_choices ()
1022 | None -> lookup_in_library ()
1027 | Symbol (symb, _) -> Symbol (symb, 0)
1030 Environment.find item e
1031 with Not_found -> lookup_in_library ())
1038 if benchmark then begin
1039 let per_item_choices =
1043 let len = List.length (lookup_choices dom_item) in
1044 debug_print (lazy (sprintf "BENCHMARK %s: %d"
1045 (string_of_domain_item dom_item) len));
1047 with No_choices _ -> 0)
1050 max_refinements := List.fold_left ( * ) 1 per_item_choices;
1051 actual_refinements := 0;
1052 domain_size := List.length thing_dom;
1054 (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
1060 (* (3) test an interpretation filling with meta uninterpreted identifiers
1062 let test_env aliases todo_dom ugraph =
1063 let rec aux env = function
1065 | Node (_, item, l) :: tl ->
1067 Environment.add item
1071 (fun _ _ _ -> Cic.Implicit (Some `Closed))
1072 | Symbol _ -> (fun _ _ _ -> Cic.Implicit None)))
1074 aux (aux env l) tl in
1075 let filled_env = aux aliases todo_dom in
1077 let localization_tbl = Cic.CicHash.create 503 in
1079 interpretate_thing ~context:disambiguate_context ~env:filled_env
1080 ~uri ~is_path:false thing ~localization_tbl
1084 refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
1087 in refine_profiler.HExtlib.profile foo ()
1089 | Try_again msg -> Uncertain (None,msg), ugraph
1090 | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph
1092 (* (4) build all possible interpretations *)
1093 let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
1094 (* aux returns triples Ok/Uncertain/Ko *)
1095 (* rem_dom is the concatenation of all the remainin domains *)
1096 let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ =
1097 debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
1100 assert (lookup_in_todo_dom = None);
1101 (match test_env aliases rem_dom base_univ with
1102 | Ok (thing, metasenv),new_univ ->
1103 [ aliases, diff, metasenv, thing, new_univ ], [], []
1104 | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true]
1105 | Uncertain (loc,msg),new_univ ->
1106 [],[aliases,diff,loc,msg,new_univ],[])
1107 | Node (locs,item,inner_dom) :: remaining_dom ->
1108 debug_print (lazy (sprintf "CHOOSED ITEM: %s"
1109 (string_of_domain_item item)));
1111 match lookup_in_todo_dom with
1112 None -> lookup_choices item
1113 | Some choices -> choices in
1117 [aliases, diff, Some (List.hd locs),
1118 lazy ("No choices for " ^ string_of_domain_item item),
1121 | [codomain_item] ->
1122 (* just one choice. We perform a one-step look-up and
1123 if the next set of choices is also a singleton we
1124 skip this refinement step *)
1125 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1126 let new_env = Environment.add item codomain_item aliases in
1127 let new_diff = (item,codomain_item)::diff in
1128 let lookup_in_todo_dom,next_choice_is_single =
1129 match remaining_dom with
1132 let choices = lookup_choices he in
1133 Some choices,List.length choices = 1
1135 if next_choice_is_single then
1136 aux new_env new_diff lookup_in_todo_dom remaining_dom
1139 (match test_env new_env remaining_dom base_univ with
1140 | Ok (thing, metasenv),new_univ ->
1141 (match remaining_dom with
1143 [ new_env, new_diff, metasenv, thing, new_univ ], []
1145 aux new_env new_diff lookup_in_todo_dom
1146 remaining_dom new_univ)
1147 | Uncertain (loc,msg),new_univ ->
1148 (match remaining_dom with
1149 | [] -> [], [new_env,new_diff,loc,msg,true]
1151 aux new_env new_diff lookup_in_todo_dom
1152 remaining_dom new_univ)
1153 | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
1156 let mark_not_significant failures =
1158 (fun (env, diff, loc, msg, _b) ->
1159 env, diff, loc, msg, false)
1161 let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
1162 if ok_l <> [] || uncertain_l <> [] then
1163 ok_l,uncertain_l,mark_not_significant error_l
1166 let rec filter univ = function
1168 | codomain_item :: tl ->
1169 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1170 let new_env = Environment.add item codomain_item aliases in
1171 let new_diff = (item,codomain_item)::diff in
1173 test_env new_env (inner_dom@remaining_dom@rem_dom) univ
1175 | Ok (thing, metasenv),new_univ ->
1177 (match inner_dom with
1179 [new_env,new_diff,metasenv,thing,new_univ], [], []
1181 aux new_env new_diff None inner_dom
1182 (remaining_dom@rem_dom) new_univ
1185 res @@ filter univ tl
1186 | Uncertain (loc,msg),new_univ ->
1188 (match inner_dom with
1189 | [] -> [],[new_env,new_diff,loc,msg,new_univ],[]
1191 aux new_env new_diff None inner_dom
1192 (remaining_dom@rem_dom) new_univ
1195 res @@ filter univ tl
1197 let res = [],[],[new_env,new_diff,loc,msg,true] in
1198 res @@ filter univ tl)
1200 let ok_l,uncertain_l,error_l =
1201 classify_errors (filter base_univ choices)
1203 let res_after_ok_l =
1205 (fun (env,diff,_,_,univ) res ->
1206 aux env diff None remaining_dom rem_dom univ @@ res
1207 ) ok_l ([],[],error_l)
1210 (fun (env,diff,_,_,univ) res ->
1211 aux env diff None remaining_dom rem_dom univ @@ res
1212 ) uncertain_l res_after_ok_l
1214 let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
1215 match test_env aliases todo_dom base_univ with
1218 aux aliases diff lookup_in_todo_dom todo_dom [] base_univ
1219 | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in
1220 let base_univ = initial_ugraph in
1223 match aux' aliases [] None todo_dom base_univ with
1224 | [],uncertain,errors ->
1227 (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true)
1228 ) uncertain @ errors
1232 (fun (env,diff,loc,msg,significant) ->
1235 (fun locs domain_item ->
1238 fst (Environment.find domain_item env)
1240 Some (locs,descr_of_domain_item domain_item,description)
1245 env',diff,loc,msg,significant
1248 raise (NoWellTypedInterpretation (0,errors))
1249 | [_,diff,metasenv,t,ugraph],_,_ ->
1250 debug_print (lazy "SINGLE INTERPRETATION");
1251 [diff,metasenv,t,ugraph], false
1254 (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
1257 (fun (env, _, _, _, _) ->
1259 (fun locs domain_item ->
1261 fst (Environment.find domain_item env)
1263 locs,descr_of_domain_item domain_item, description)
1268 C.interactive_interpretation_choice
1269 thing_txt thing_txt_prefix_len choices
1271 (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
1276 CicEnvironment.CircularDependency s ->
1277 failwith "Disambiguate: circular dependency"
1279 let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
1280 ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
1281 (text,prefix_len,term)
1284 if fresh_instances then CicNotationUtil.freshen_term term else term
1286 disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
1287 ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
1288 ~domain_of_thing:domain_of_term
1289 ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
1290 ~refine_thing:refine_term (text,prefix_len,term)
1292 let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
1293 (text,prefix_len,obj)
1296 if fresh_instances then CicNotationUtil.freshen_obj obj else obj
1298 disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
1299 ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
1300 ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
1301 (text,prefix_len,obj)