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 * 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 ('term,'metasenv,'subst,'graph) test_result =
107 | Ok of 'term * 'metasenv * 'subst * 'graph
108 | Ko of (Stdpp.location * string) Lazy.t
109 | Uncertain of (Stdpp.location * string) Lazy.t
111 let refine_term metasenv subst 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 loc exn
124 | CicRefine.Uncertain msg ->
125 debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
126 Uncertain (lazy (loc,Lazy.force msg))
127 | CicRefine.RefineFailure msg ->
128 debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
129 (CicPp.ppterm term) (Lazy.force msg)));
130 Ko (lazy (loc,Lazy.force msg))
133 process_exn Stdpp.dummy_loc exn
135 let refine_obj metasenv subst context uri obj ugraph ~localization_tbl =
136 assert (context = []);
137 assert (metasenv = []);
139 debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
141 let obj', metasenv,ugraph =
142 CicRefine.typecheck metasenv uri obj ~localization_tbl
144 (Ok (obj', metasenv,[],ugraph))
147 let rec process_exn loc =
149 HExtlib.Localized (loc,exn) -> process_exn loc exn
150 | CicRefine.Uncertain msg ->
151 debug_print (lazy ("UNCERTAIN!!! [" ^
152 (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
153 Uncertain (lazy (loc,Lazy.force msg))
154 | CicRefine.RefineFailure msg ->
155 debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
156 (CicPp.ppobj obj) (Lazy.force msg))) ;
157 Ko (lazy (loc,Lazy.force msg))
160 process_exn Stdpp.dummy_loc exn
162 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
164 snd (Environment.find item env) env num args
166 failwith ("Domain item not found: " ^
167 (DisambiguateTypes.string_of_domain_item item))
169 (* TODO move it to Cic *)
170 let find_in_context name context =
171 let rec aux acc = function
172 | [] -> raise Not_found
173 | Cic.Name hd :: tl when hd = name -> acc
174 | _ :: tl -> aux (acc + 1) tl
178 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
181 (* create_dummy_ids shouldbe used only for interpretating patterns *)
183 let rec aux ~localize loc context = function
184 | CicNotationPt.AttributedTerm (`Loc loc, term) ->
185 let res = aux ~localize loc context term in
186 if localize then Cic.CicHash.add localization_tbl res loc;
188 | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
189 | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
190 let cic_args = List.map (aux ~localize loc context) args in
191 resolve env (Symbol (symb, i)) ~args:cic_args ()
192 | CicNotationPt.Appl terms ->
193 Cic.Appl (List.map (aux ~localize loc context) terms)
194 | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
195 let cic_type = aux_option ~localize loc context (Some `Type) typ in
196 let cic_name = CicNotationUtil.cic_name_of_name var in
197 let cic_body = aux ~localize loc (cic_name :: context) body in
198 (match binder_kind with
199 | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
201 | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
203 resolve env (Symbol ("exists", 0))
204 ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
205 | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
206 let cic_term = aux ~localize loc context term in
207 let cic_outtype = aux_option ~localize loc context None outtype in
208 let do_branch ((head, _, args), term) =
209 let rec do_branch' context = function
210 | [] -> aux ~localize loc context term
211 | (name, typ) :: tl ->
212 let cic_name = CicNotationUtil.cic_name_of_name name in
213 let cic_body = do_branch' (cic_name :: context) tl in
216 | None -> Cic.Implicit (Some `Type)
217 | Some typ -> aux ~localize loc context typ
219 Cic.Lambda (cic_name, typ, cic_body)
221 do_branch' context args
223 let indtype_uri, indtype_no =
224 if create_dummy_ids then
225 (UriManager.uri_of_string "cic:/fake_indty.con", 0)
227 match indty_ident with
228 | Some (indty_ident, _) ->
229 (match resolve env (Id indty_ident) () with
230 | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
232 raise (Try_again (lazy "The type of the term to be matched
235 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
237 let rec fst_constructor =
239 (Ast.Pattern (head, _, _), _) :: _ -> head
240 | (Ast.Wildcard, _) :: tl -> fst_constructor tl
241 | [] -> 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"))
243 (match resolve env (Id (fst_constructor branches)) () with
244 | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
245 (indtype_uri, indtype_no)
247 raise (Try_again (lazy "The type of the term to be matched
250 raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
253 if create_dummy_ids then
256 Ast.Wildcard,term -> ("wildcard",None,[]), term
258 raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
261 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
262 Cic.InductiveDefinition (il,_,leftsno,_) ->
265 List.nth il indtype_no
266 with _ -> assert false
268 let rec count_prod t =
269 match CicReduction.whd [] t with
270 Cic.Prod (_, _, t) -> 1 + (count_prod t)
273 let rec sort branches cl =
276 let rec analyze unused unrecognized useless =
279 if unrecognized != [] then
280 raise (Invalid_choice
283 ("Unrecognized constructors: " ^
284 String.concat " " unrecognized)))
285 else if useless > 0 then
286 raise (Invalid_choice
289 ("The last " ^ string_of_int useless ^
290 "case" ^ if useless > 1 then "s are" else " is" ^
294 | (Ast.Wildcard,_)::tl when not unused ->
295 analyze true unrecognized useless tl
296 | (Ast.Pattern (head,_,_),_)::tl when not unused ->
297 analyze unused (head::unrecognized) useless tl
298 | _::tl -> analyze unused unrecognized (useless + 1) tl
300 analyze false [] 0 branches
302 let rec find_and_remove =
307 (Some loc, lazy ("Missing case: " ^ name)))
308 | ((Ast.Wildcard, _) as branch :: _) as branches ->
310 | (Ast.Pattern (name',_,_),_) as branch :: tl
314 let found,rest = find_and_remove tl in
317 let branch,tl = find_and_remove branches in
319 Ast.Pattern (name,y,args),term ->
320 if List.length args = count_prod ty - leftsno then
321 ((name,y,args),term)::sort tl cltl
326 lazy ("Wrong number of arguments for " ^ name)))
327 | Ast.Wildcard,term ->
333 (`Lambda, (CicNotationPt.Ident ("_", None), None),
336 (("wildcard",None,[]),
337 mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
342 Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
343 (List.map do_branch branches))
344 | CicNotationPt.Cast (t1, t2) ->
345 let cic_t1 = aux ~localize loc context t1 in
346 let cic_t2 = aux ~localize loc context t2 in
347 Cic.Cast (cic_t1, cic_t2)
348 | CicNotationPt.LetIn ((name, typ), def, body) ->
349 let cic_def = aux ~localize loc context def in
350 let cic_name = CicNotationUtil.cic_name_of_name name in
353 | None -> Cic.Implicit (Some `Type)
354 | Some t -> aux ~localize loc context t
356 let cic_body = aux ~localize loc (cic_name :: context) body in
357 Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
358 | CicNotationPt.LetRec (kind, defs, body) ->
361 (fun acc (_, (name, _), _, _) ->
362 CicNotationUtil.cic_name_of_name name :: acc)
366 let unlocalized_body = aux ~localize:false loc context' body in
367 match unlocalized_body with
368 Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
369 | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
374 let t',subst,metasenv =
375 CicMetaSubst.delift_rels [] [] (List.length defs) t
378 assert (metasenv=[]);
381 (* We can avoid the LetIn. But maybe we need to recompute l'
382 so that it is localized *)
385 CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
386 (* since we avoid the letin, the context has no
388 let l' = List.map (aux ~localize loc context) l in
394 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
396 `AddLetIn (aux ~localize loc context' body)
398 `AddLetIn unlocalized_body)
401 `AddLetIn (aux ~localize loc context' body)
403 `AddLetIn unlocalized_body
407 (fun (params, (name, typ), body, decr_idx) ->
408 let add_binders kind t =
410 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
413 aux ~localize loc context' (add_binders `Lambda body) in
415 aux_option ~localize loc context (Some `Type)
416 (HExtlib.map_option (add_binders `Pi) typ) in
418 match CicNotationUtil.cic_name_of_name name with
420 CicNotationPt.fail loc
421 "Recursive functions cannot be anonymous"
422 | Cic.Name name -> name
424 (name, decr_idx, cic_type, cic_body))
429 `Inductive -> Cic.Fix (n,inductiveFuns)
431 let coinductiveFuns =
433 (fun (name, _, typ, body) -> name, typ, body)
436 Cic.CoFix (n,coinductiveFuns)
438 let counter = ref ~-1 in
439 let build_term funs (var,_,ty,_) t =
441 Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
444 `AvoidLetInNoAppl n ->
445 let n' = List.length inductiveFuns - n in
447 | `AvoidLetIn (n,l) ->
448 let n' = List.length inductiveFuns - n in
449 Cic.Appl (fix_or_cofix n'::l)
450 | `AddLetIn cic_body ->
451 List.fold_right (build_term inductiveFuns) inductiveFuns
453 | CicNotationPt.Ident _
454 | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
455 | CicNotationPt.Ident (name, subst)
456 | CicNotationPt.Uri (name, subst) as ast ->
457 let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
459 if is_uri ast then raise Not_found;(* don't search the env for URIs *)
460 let index = find_in_context name context in
461 if subst <> None then
462 CicNotationPt.fail loc "Explicit substitutions not allowed here";
466 if is_uri ast then (* we have the URI, build the term out of it *)
468 CicUtil.term_of_uri (UriManager.uri_of_string name)
469 with UriManager.IllFormedUri _ ->
470 CicNotationPt.fail loc "Ill formed URI"
472 resolve env (Id name) ()
476 List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
483 List.assoc s ids_to_uris, aux ~localize loc context term
485 raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
487 | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
491 | Cic.Const (uri, []) ->
492 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
493 let uris = CicUtil.params_of_obj o in
494 Cic.Const (uri, mk_subst uris)
495 | Cic.Var (uri, []) ->
496 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
497 let uris = CicUtil.params_of_obj o in
498 Cic.Var (uri, mk_subst uris)
499 | Cic.MutInd (uri, i, []) ->
501 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
502 let uris = CicUtil.params_of_obj o in
503 Cic.MutInd (uri, i, mk_subst uris)
505 CicEnvironment.Object_not_found _ ->
506 (* if we are here it is probably the case that during the
507 definition of a mutual inductive type we have met an
508 occurrence of the type in one of its constructors.
509 However, the inductive type is not yet in the environment
511 (*here the explicit_named_substituion is assumed to be of length 0 *)
512 Cic.MutInd (uri,i,[]))
513 | Cic.MutConstruct (uri, i, j, []) ->
514 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
515 let uris = CicUtil.params_of_obj o in
516 Cic.MutConstruct (uri, i, j, mk_subst uris)
517 | Cic.Meta _ | Cic.Implicit _ as t ->
519 debug_print (lazy (sprintf
520 "Warning: %s must be instantiated with _[%s] but we do not enforce it"
524 (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
529 raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
531 CicEnvironment.CircularDependency _ ->
532 raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
533 | CicNotationPt.Implicit -> Cic.Implicit None
534 | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
535 | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
536 | CicNotationPt.Meta (index, subst) ->
541 | Some term -> Some (aux ~localize loc context term))
544 Cic.Meta (index, cic_subst)
545 | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
546 | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
547 | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
548 | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
549 | CicNotationPt.Symbol (symbol, instance) ->
550 resolve env (Symbol (symbol, instance)) ()
551 | _ -> assert false (* god bless Bologna *)
552 and aux_option ~localize loc context annotation = function
553 | None -> Cic.Implicit annotation
554 | Some term -> aux ~localize loc context term
556 aux ~localize:true HExtlib.dummy_floc context ast
558 let interpretate_path ~context path =
559 let localization_tbl = Cic.CicHash.create 23 in
560 (* here we are throwing away useful localization informations!!! *)
562 interpretate_term ~create_dummy_ids:true
563 ~context ~env:Environment.empty ~uri:None ~is_path:true
564 path ~localization_tbl, localization_tbl)
566 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
567 assert (context = []);
568 assert (is_path = false);
569 let interpretate_term = interpretate_term ~localization_tbl in
571 | CicNotationPt.Inductive (params,tyl) ->
572 let uri = match uri with Some uri -> uri | None -> assert false in
576 (fun (context,res) (name,t) ->
579 None -> CicNotationPt.Implicit
581 let name = CicNotationUtil.cic_name_of_name name in
582 name::context,(name, interpretate_term context env None false t)::res
585 context,List.rev res in
587 List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
591 (*here the explicit_named_substituion is assumed to be of length 0 *)
592 (fun (i,res) (name,_,_,_) ->
593 i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
595 let con_env = DisambiguateTypes.env_of_list name_to_uris env in
598 (fun (name,b,ty,cl) ->
599 let ty' = add_params (interpretate_term context env None false ty) in
604 add_params (interpretate_term context con_env None false ty)
612 Cic.InductiveDefinition (tyl,[],List.length params,[])
613 | CicNotationPt.Record (params,name,ty,fields) ->
614 let uri = match uri with Some uri -> uri | None -> assert false in
618 (fun (context,res) (name,t) ->
621 None -> CicNotationPt.Implicit
623 let name = CicNotationUtil.cic_name_of_name name in
624 name::context,(name, interpretate_term context env None false t)::res
627 context,List.rev res in
630 (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
631 let ty' = add_params (interpretate_term context env None false ty) in
635 (fun (context,res) (name,ty,_coercion,arity) ->
636 let context' = Cic.Name name :: context in
637 context',(name,interpretate_term context env None false ty)::res
638 ) (context,[]) fields) in
640 (*here the explicit_named_substituion is assumed to be of length 0 *)
641 let mutind = Cic.MutInd (uri,0,[]) in
642 if params = [] then mutind
645 (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
648 (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
650 let con' = add_params con in
651 let tyl = [name,true,ty',["mk_" ^ name,con']] in
652 let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
653 Cic.InductiveDefinition
654 (tyl,[],List.length params,[`Class (`Record field_names)])
655 | CicNotationPt.Theorem (flavour, name, ty, bo) ->
656 let attrs = [`Flavour flavour] in
657 let ty' = interpretate_term [] env None false ty in
658 (match bo,flavour with
660 Cic.Constant (name,None,ty',[],attrs)
661 | Some bo,`Axiom -> assert false
663 Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
665 let bo' = Some (interpretate_term [] env None false bo) in
666 Cic.Constant (name,bo',ty',[],attrs))
669 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
672 let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
673 interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
678 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
679 | Ast.AttributedTerm (`Loc loc, term) ->
680 domain_of_term ~loc ~context term
681 | Ast.AttributedTerm (_, term) ->
682 domain_of_term ~loc ~context term
683 | Ast.Symbol (symbol, instance) ->
684 [ Node ([loc], Symbol (symbol, instance), []) ]
685 (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
686 | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
687 | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
691 (fun term acc -> domain_of_term ~loc ~context term @ acc)
695 Ast.AttributedTerm (`Loc loc,_) -> loc
698 [ Node ([loc], Symbol (symbol, instance), args_dom) ]
699 | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
700 | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
703 (fun term acc -> domain_of_term ~loc ~context term @ acc)
707 Ast.AttributedTerm (`Loc loc,_) -> loc
711 (* the next line can raise Not_found *)
712 ignore(find_in_context name context);
713 if subst <> None then
714 Ast.fail loc "Explicit substitutions not allowed here"
719 | None -> [ Node ([loc], Id name, args_dom) ]
723 (fun dom (_, term) ->
724 let dom' = domain_of_term ~loc ~context term in
727 [ Node ([loc], Id name, terms @ args_dom) ]))
730 (fun term acc -> domain_of_term ~loc ~context term @ acc)
732 | Ast.Binder (kind, (var, typ), body) ->
733 let type_dom = domain_of_term_option ~loc ~context typ in
736 ~context:(CicNotationUtil.cic_name_of_name var :: context) body in
738 | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
739 | _ -> type_dom @ body_dom)
740 | Ast.Case (term, indty_ident, outtype, branches) ->
741 let term_dom = domain_of_term ~loc ~context term in
742 let outtype_dom = domain_of_term_option ~loc ~context outtype in
743 let rec get_first_constructor = function
745 | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
746 | _ :: tl -> get_first_constructor tl in
749 Ast.Pattern (head, _, args), term ->
750 let (term_context, args_domain) =
752 (fun (cont, dom) (name, typ) ->
753 (CicNotationUtil.cic_name_of_name name :: cont,
756 | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
759 domain_of_term ~loc ~context:term_context term @ args_domain
760 | Ast.Wildcard, term ->
761 domain_of_term ~loc ~context term
764 List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
765 (match indty_ident with
766 | None -> get_first_constructor branches
767 | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
768 @ term_dom @ outtype_dom @ branches_dom
769 | Ast.Cast (term, ty) ->
770 let term_dom = domain_of_term ~loc ~context term in
771 let ty_dom = domain_of_term ~loc ~context ty in
773 | Ast.LetIn ((var, typ), body, where) ->
774 let body_dom = domain_of_term ~loc ~context body in
775 let type_dom = domain_of_term_option ~loc ~context typ in
778 ~context:(CicNotationUtil.cic_name_of_name var :: context) where in
779 body_dom @ type_dom @ where_dom
780 | Ast.LetRec (kind, defs, where) ->
781 let add_defs context =
783 (fun acc (_, (var, _), _, _) ->
784 CicNotationUtil.cic_name_of_name var :: acc
786 let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
789 (fun dom (params, (_, typ), body, _) ->
793 (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
799 (fun (context,res) (var,ty) ->
800 CicNotationUtil.cic_name_of_name var :: context,
801 domain_of_term_option ~loc ~context ty @ res)
802 (add_defs context,[]) params))
804 @ domain_of_term_option ~loc ~context:context' typ
805 @ domain_of_term ~loc ~context:context' body
809 | Ast.Ident (name, subst) ->
811 (* the next line can raise Not_found *)
812 ignore(find_in_context name context);
813 if subst <> None then
814 Ast.fail loc "Explicit substitutions not allowed here"
819 | None -> [ Node ([loc], Id name, []) ]
823 (fun dom (_, term) ->
824 let dom' = domain_of_term ~loc ~context term in
827 [ Node ([loc], Id name, terms) ]))
830 | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
831 | Ast.Meta (index, local_context) ->
833 (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
840 | Ast.Variable _ -> assert false
842 and domain_of_term_option ~loc ~context = function
844 | Some t -> domain_of_term ~loc ~context t
846 let domain_of_term ~context term =
847 uniq_domain (domain_of_term ~context term)
849 let domain_of_obj ~context ast =
850 let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
851 assert (context = []);
853 | Ast.Theorem (_,_,ty,bo) ->
857 | Some bo -> domain_of_term [] bo)
858 | Ast.Inductive (params,tyl) ->
861 (fun (context, dom) (var, ty) ->
862 let context' = CicNotationUtil.cic_name_of_name var :: context in
864 None -> context', dom
865 | Some ty -> context', dom @ domain_of_term context ty
867 let context_w_types =
869 (fun (var, _, _, _) -> Cic.Name var) tyl
875 domain_of_term context ty
878 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
880 | CicNotationPt.Record (params,var,ty,fields) ->
883 (fun (context, dom) (var, ty) ->
884 let context' = CicNotationUtil.cic_name_of_name var :: context in
886 None -> context', dom
887 | Some ty -> context', dom @ domain_of_term context ty
889 let context_w_types = Cic.Name var :: context in
891 @ domain_of_term context ty
894 (fun (context,res) (name,ty,_,_) ->
895 Cic.Name name::context, res @ domain_of_term context ty
896 ) (context_w_types,[]) fields)
898 let domain_of_obj ~context obj =
899 uniq_domain (domain_of_obj ~context obj)
901 let domain_of_ast_term = domain_of_term;;
903 let domain_of_term ~context term =
905 List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
907 domain_of_term ~context term
910 let domain_diff dom1 dom2 =
911 (* let domain_diff = Domain.diff *)
915 | Symbol (symb, 0) ->
917 Symbol (symb',_) when symb = symb' -> true
929 | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
930 | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
934 module type Disambiguator =
936 val disambiguate_thing:
939 metasenv:'metasenv ->
941 initial_ugraph:'ugraph ->
942 hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
943 (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
944 ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
945 aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
946 universe:DisambiguateTypes.codomain_item list
947 DisambiguateTypes.Environment.t option ->
949 pp_thing:('ast_thing -> string) ->
950 domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
951 interpretate_thing:(context:'context ->
952 env:DisambiguateTypes.codomain_item
953 DisambiguateTypes.Environment.t ->
955 is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
956 refine_thing:('metasenv ->
961 'ugraph -> localization_tbl:'cichash ->
962 ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
963 localization_tbl:'cichash ->
964 string * int * 'ast_thing ->
965 ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
966 list * 'metasenv * 'subst * 'refined_thing * 'ugraph)
969 val disambiguate_term :
970 ?fresh_instances:bool ->
972 context:Cic.context ->
973 metasenv:Cic.metasenv ->
974 subst:Cic.substitution ->
976 ?initial_ugraph:CicUniv.universe_graph ->
977 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
978 universe:DisambiguateTypes.multiple_environment option ->
979 CicNotationPt.term disambiguator_input ->
980 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
981 Cic.metasenv * (* new metasenv *)
984 CicUniv.universe_graph) list * (* disambiguated term *)
987 val disambiguate_obj :
988 ?fresh_instances:bool ->
990 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
991 universe:DisambiguateTypes.multiple_environment option ->
992 uri:UriManager.uri option -> (* required only for inductive types *)
993 CicNotationPt.term CicNotationPt.obj disambiguator_input ->
994 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
995 Cic.metasenv * (* new metasenv *)
998 CicUniv.universe_graph) list * (* disambiguated obj *)
1002 module Make (C: Callbacks) =
1004 let choices_of_id dbd id =
1005 let uris = Whelp.locate ~dbd id in
1010 (C.input_or_locate_uri
1011 ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())
1014 | Some uri -> [uri])
1017 C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
1018 ~ok:"Try selected." ~enable_button_for_non_vars:true
1019 ~title:"Ambiguous input." ~id
1020 ~msg: ("Ambiguous input \"" ^ id ^
1021 "\". Please, choose one or more interpretations:")
1026 (UriManager.string_of_uri uri,
1029 CicUtil.term_of_uri uri
1031 debug_print (lazy (UriManager.string_of_uri uri));
1032 debug_print (lazy (Printexc.to_string exn));
1038 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
1040 let disambiguate_thing ~dbd ~context ~metasenv ~subst
1041 ~initial_ugraph:base_univ ~hint
1043 ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
1045 (thing_txt,thing_txt_prefix_len,thing)
1047 debug_print (lazy "DISAMBIGUATE INPUT");
1048 debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
1049 let thing_dom = domain_of_thing ~context thing in
1051 (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
1053 debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
1054 (DisambiguatePp.pp_environment aliases)));
1055 debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
1056 (match universe with None -> "None" | Some _ -> "Some _")));
1059 Environment.fold (fun item _ dom -> item :: dom) aliases [] in
1060 let todo_dom = domain_diff thing_dom current_dom in
1062 (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
1063 (* (2) lookup function for any item (Id/Symbol/Num) *)
1064 let lookup_choices =
1067 let lookup_in_library () =
1069 | Id id -> choices_of_id dbd id
1070 | Symbol (symb, _) ->
1072 List.map DisambiguateChoices.mk_choice
1073 (TermAcicContent.lookup_interpretations symb)
1075 TermAcicContent.Interpretation_not_found -> [])
1077 DisambiguateChoices.lookup_num_choices ()
1080 | None -> lookup_in_library ()
1085 | Symbol (symb, _) -> Symbol (symb, 0)
1088 Environment.find item e
1089 with Not_found -> lookup_in_library ())
1096 if benchmark then begin
1097 let per_item_choices =
1101 let len = List.length (lookup_choices dom_item) in
1102 debug_print (lazy (sprintf "BENCHMARK %s: %d"
1103 (string_of_domain_item dom_item) len));
1105 with No_choices _ -> 0)
1108 max_refinements := List.fold_left ( * ) 1 per_item_choices;
1109 actual_refinements := 0;
1110 domain_size := List.length thing_dom;
1112 (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
1118 (* (3) test an interpretation filling with meta uninterpreted identifiers
1120 let test_env aliases todo_dom ugraph =
1121 let rec aux env = function
1123 | Node (_, item, l) :: tl ->
1125 Environment.add item
1129 (fun _ _ _ -> Cic.Implicit (Some `Closed))
1130 | Symbol _ -> (fun _ _ _ -> Cic.Implicit None)))
1132 aux (aux env l) tl in
1133 let filled_env = aux aliases todo_dom in
1136 interpretate_thing ~context ~env:filled_env
1137 ~uri ~is_path:false thing ~localization_tbl
1139 let cic_thing = (fst hint) metasenv cic_thing in
1142 refine_thing metasenv subst
1143 context uri cic_thing ugraph ~localization_tbl
1145 let k = (snd hint) k in
1147 in refine_profiler.HExtlib.profile foo ()
1149 | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
1150 | Invalid_choice (None,msg) -> Ko(lazy (Stdpp.dummy_loc,Lazy.force msg))
1151 | Invalid_choice (Some loc,msg) -> Ko (lazy (loc,Lazy.force msg))
1153 (* (4) build all possible interpretations *)
1154 let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
1155 (* aux returns triples Ok/Uncertain/Ko *)
1156 (* rem_dom is the concatenation of all the remainin domains *)
1157 let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom =
1158 debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
1161 assert (lookup_in_todo_dom = None);
1162 (match test_env aliases rem_dom base_univ with
1163 | Ok (thing, metasenv,subst,new_univ) ->
1164 [ aliases, diff, metasenv, subst, thing, new_univ ], [], []
1165 | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true]
1166 | Uncertain loc_msg ->
1167 [],[aliases,diff,loc_msg],[])
1168 | Node (locs,item,inner_dom) :: remaining_dom ->
1169 debug_print (lazy (sprintf "CHOOSED ITEM: %s"
1170 (string_of_domain_item item)));
1172 match lookup_in_todo_dom with
1173 None -> lookup_choices item
1174 | Some choices -> choices in
1179 (lazy (List.hd locs,
1180 "No choices for " ^ string_of_domain_item item)),
1183 | [codomain_item] ->
1184 (* just one choice. We perform a one-step look-up and
1185 if the next set of choices is also a singleton we
1186 skip this refinement step *)
1187 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1188 let new_env = Environment.add item codomain_item aliases in
1189 let new_diff = (item,codomain_item)::diff in
1190 let lookup_in_todo_dom,next_choice_is_single =
1191 match remaining_dom with
1194 let choices = lookup_choices he in
1195 Some choices,List.length choices = 1
1197 if next_choice_is_single then
1198 aux new_env new_diff lookup_in_todo_dom remaining_dom
1201 (match test_env new_env remaining_dom base_univ with
1202 | Ok (thing, metasenv),new_univ ->
1203 (match remaining_dom with
1205 [ new_env, new_diff, metasenv, thing, new_univ ], []
1207 aux new_env new_diff lookup_in_todo_dom
1208 remaining_dom new_univ)
1209 | Uncertain (loc,msg),new_univ ->
1210 (match remaining_dom with
1211 | [] -> [], [new_env,new_diff,loc,msg,true]
1213 aux new_env new_diff lookup_in_todo_dom
1214 remaining_dom new_univ)
1215 | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
1218 let mark_not_significant failures =
1220 (fun (env, diff, loc_msg, _b) ->
1221 env, diff, loc_msg, false)
1223 let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
1224 if ok_l <> [] || uncertain_l <> [] then
1225 ok_l,uncertain_l,mark_not_significant error_l
1228 let rec filter = function
1230 | codomain_item :: tl ->
1231 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1232 let new_env = Environment.add item codomain_item aliases in
1233 let new_diff = (item,codomain_item)::diff in
1236 (inner_dom@remaining_dom@rem_dom) base_univ
1238 | Ok (thing, metasenv,subst,new_univ) ->
1240 (match inner_dom with
1242 [new_env,new_diff,metasenv,subst,thing,new_univ],
1245 aux new_env new_diff None inner_dom
1246 (remaining_dom@rem_dom)
1250 | Uncertain loc_msg ->
1252 (match inner_dom with
1253 | [] -> [],[new_env,new_diff,loc_msg],[]
1255 aux new_env new_diff None inner_dom
1256 (remaining_dom@rem_dom)
1261 let res = [],[],[new_env,new_diff,loc_msg,true] in
1264 let ok_l,uncertain_l,error_l =
1265 classify_errors (filter choices)
1267 let res_after_ok_l =
1269 (fun (env,diff,_,_,_,_) res ->
1270 aux env diff None remaining_dom rem_dom @@ res
1271 ) ok_l ([],[],error_l)
1274 (fun (env,diff,_) res ->
1275 aux env diff None remaining_dom rem_dom @@ res
1276 ) uncertain_l res_after_ok_l
1278 let aux' aliases diff lookup_in_todo_dom todo_dom =
1279 match test_env aliases todo_dom base_univ with
1282 aux aliases diff lookup_in_todo_dom todo_dom []
1283 | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in
1286 match aux' aliases [] None todo_dom with
1287 | [],uncertain,errors ->
1290 (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)
1291 ) uncertain @ errors
1295 (fun (env,diff,loc_msg,significant) ->
1298 (fun locs domain_item ->
1301 fst (Environment.find domain_item env)
1303 Some (locs,descr_of_domain_item domain_item,description)
1308 env',diff,loc_msg,significant
1311 raise (NoWellTypedInterpretation (0,errors))
1312 | [_,diff,metasenv,subst,t,ugraph],_,_ ->
1313 debug_print (lazy "SINGLE INTERPRETATION");
1314 [diff,metasenv,subst,t,ugraph], false
1317 (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
1320 (fun (env, _, _, _, _, _) ->
1322 (fun locs domain_item ->
1324 fst (Environment.find domain_item env)
1326 locs,descr_of_domain_item domain_item, description)
1331 C.interactive_interpretation_choice
1332 thing_txt thing_txt_prefix_len choices
1334 (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u)
1340 CicEnvironment.CircularDependency s ->
1341 failwith "Disambiguate: circular dependency"
1343 let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
1345 ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
1346 (text,prefix_len,term)
1349 if fresh_instances then CicNotationUtil.freshen_term term else term
1351 let hint = match goal with
1352 | None -> (fun _ x -> x), fun k -> k
1355 let _,c,ty = CicUtil.lookup_meta i metasenv in
1361 | Cic.Cast(t,_) -> Ok (t,m,s,ug)
1362 | _ -> assert false)
1365 let localization_tbl = Cic.CicHash.create 503 in
1366 disambiguate_thing ~dbd ~context ~metasenv ~subst
1367 ~initial_ugraph ~aliases
1368 ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
1369 ~domain_of_thing:domain_of_term
1370 ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
1371 ~refine_thing:refine_term (text,prefix_len,term)
1375 let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
1376 (text,prefix_len,obj)
1379 if fresh_instances then CicNotationUtil.freshen_obj obj else obj
1385 let localization_tbl = Cic.CicHash.create 503 in
1386 disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~subst:[]
1387 ~aliases ~universe ~uri
1388 ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
1389 ~initial_ugraph:CicUniv.empty_ugraph
1390 ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
1393 (text,prefix_len,obj)