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 (lazy (loc,"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 (lazy (loc,"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 (lazy (loc,"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 (lazy (loc, "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
282 ("Unrecognized constructors: " ^
283 String.concat " " unrecognized))))
284 else if useless > 0 then
285 raise (Invalid_choice
287 ("The last " ^ string_of_int useless ^
288 "case" ^ if useless > 1 then "s are" else " is" ^
292 | (Ast.Wildcard,_)::tl when not unused ->
293 analyze true unrecognized useless tl
294 | (Ast.Pattern (head,_,_),_)::tl when not unused ->
295 analyze unused (head::unrecognized) useless tl
296 | _::tl -> analyze unused unrecognized (useless + 1) tl
298 analyze false [] 0 branches
300 let rec find_and_remove =
305 (lazy (loc, ("Missing case: " ^ name))))
306 | ((Ast.Wildcard, _) as branch :: _) as branches ->
308 | (Ast.Pattern (name',_,_),_) as branch :: tl
312 let found,rest = find_and_remove tl in
315 let branch,tl = find_and_remove branches in
317 Ast.Pattern (name,y,args),term ->
318 if List.length args = count_prod ty - leftsno then
319 ((name,y,args),term)::sort tl cltl
323 (lazy (loc,"Wrong number of arguments for " ^
325 | Ast.Wildcard,term ->
331 (`Lambda, (CicNotationPt.Ident ("_", None), None),
334 (("wildcard",None,[]),
335 mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
340 Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
341 (List.map do_branch branches))
342 | CicNotationPt.Cast (t1, t2) ->
343 let cic_t1 = aux ~localize loc context t1 in
344 let cic_t2 = aux ~localize loc context t2 in
345 Cic.Cast (cic_t1, cic_t2)
346 | CicNotationPt.LetIn ((name, typ), def, body) ->
347 let cic_def = aux ~localize loc context def in
348 let cic_name = CicNotationUtil.cic_name_of_name name in
351 | None -> Cic.Implicit (Some `Type)
352 | Some t -> aux ~localize loc context t
354 let cic_body = aux ~localize loc (cic_name :: context) body in
355 Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
356 | CicNotationPt.LetRec (kind, defs, body) ->
359 (fun acc (_, (name, _), _, _) ->
360 CicNotationUtil.cic_name_of_name name :: acc)
364 let unlocalized_body = aux ~localize:false loc context' body in
365 match unlocalized_body with
366 Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
367 | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
372 let t',subst,metasenv =
373 CicMetaSubst.delift_rels [] [] (List.length defs) t
376 assert (metasenv=[]);
379 (* We can avoid the LetIn. But maybe we need to recompute l'
380 so that it is localized *)
383 CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
384 (* since we avoid the letin, the context has no
386 let l' = List.map (aux ~localize loc context) l in
392 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
394 `AddLetIn (aux ~localize loc context' body)
396 `AddLetIn unlocalized_body)
399 `AddLetIn (aux ~localize loc context' body)
401 `AddLetIn unlocalized_body
405 (fun (params, (name, typ), body, decr_idx) ->
406 let add_binders kind t =
408 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
411 aux ~localize loc context' (add_binders `Lambda body) in
413 aux_option ~localize loc context (Some `Type)
414 (HExtlib.map_option (add_binders `Pi) typ) in
416 match CicNotationUtil.cic_name_of_name name with
418 CicNotationPt.fail loc
419 "Recursive functions cannot be anonymous"
420 | Cic.Name name -> name
422 (name, decr_idx, cic_type, cic_body))
427 `Inductive -> Cic.Fix (n,inductiveFuns)
429 let coinductiveFuns =
431 (fun (name, _, typ, body) -> name, typ, body)
434 Cic.CoFix (n,coinductiveFuns)
436 let counter = ref ~-1 in
437 let build_term funs (var,_,ty,_) t =
439 Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
442 `AvoidLetInNoAppl n ->
443 let n' = List.length inductiveFuns - n in
445 | `AvoidLetIn (n,l) ->
446 let n' = List.length inductiveFuns - n in
447 Cic.Appl (fix_or_cofix n'::l)
448 | `AddLetIn cic_body ->
449 List.fold_right (build_term inductiveFuns) inductiveFuns
451 | CicNotationPt.Ident _
452 | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed
453 | CicNotationPt.Ident (name, subst)
454 | CicNotationPt.Uri (name, subst) as ast ->
455 let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
457 if is_uri ast then raise Not_found;(* don't search the env for URIs *)
458 let index = find_in_context name context in
459 if subst <> None then
460 CicNotationPt.fail loc "Explicit substitutions not allowed here";
464 if is_uri ast then (* we have the URI, build the term out of it *)
466 CicUtil.term_of_uri (UriManager.uri_of_string name)
467 with UriManager.IllFormedUri _ ->
468 CicNotationPt.fail loc "Ill formed URI"
470 resolve env (Id name) ()
474 List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
481 List.assoc s ids_to_uris, aux ~localize loc context term
483 raise (Invalid_choice (lazy (loc, "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))))
485 | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
489 | Cic.Const (uri, []) ->
490 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
491 let uris = CicUtil.params_of_obj o in
492 Cic.Const (uri, mk_subst uris)
493 | Cic.Var (uri, []) ->
494 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
495 let uris = CicUtil.params_of_obj o in
496 Cic.Var (uri, mk_subst uris)
497 | Cic.MutInd (uri, i, []) ->
499 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
500 let uris = CicUtil.params_of_obj o in
501 Cic.MutInd (uri, i, mk_subst uris)
503 CicEnvironment.Object_not_found _ ->
504 (* if we are here it is probably the case that during the
505 definition of a mutual inductive type we have met an
506 occurrence of the type in one of its constructors.
507 However, the inductive type is not yet in the environment
509 (*here the explicit_named_substituion is assumed to be of length 0 *)
510 Cic.MutInd (uri,i,[]))
511 | Cic.MutConstruct (uri, i, j, []) ->
512 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
513 let uris = CicUtil.params_of_obj o in
514 Cic.MutConstruct (uri, i, j, mk_subst uris)
515 | Cic.Meta _ | Cic.Implicit _ as t ->
517 debug_print (lazy (sprintf
518 "Warning: %s must be instantiated with _[%s] but we do not enforce it"
522 (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
527 raise (Invalid_choice (lazy (loc, "??? Can this happen?")))
529 CicEnvironment.CircularDependency _ ->
530 raise (Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
531 | CicNotationPt.Implicit -> Cic.Implicit None
532 | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
533 | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
534 | CicNotationPt.Meta (index, subst) ->
539 | Some term -> Some (aux ~localize loc context term))
542 Cic.Meta (index, cic_subst)
543 | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
544 | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
545 | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
546 | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
547 | CicNotationPt.Symbol (symbol, instance) ->
548 resolve env (Symbol (symbol, instance)) ()
549 | _ -> assert false (* god bless Bologna *)
550 and aux_option ~localize loc context annotation = function
551 | None -> Cic.Implicit annotation
552 | Some term -> aux ~localize loc context term
554 aux ~localize:true HExtlib.dummy_floc context ast
556 let interpretate_path ~context path =
557 let localization_tbl = Cic.CicHash.create 23 in
558 (* here we are throwing away useful localization informations!!! *)
560 interpretate_term ~create_dummy_ids:true
561 ~context ~env:Environment.empty ~uri:None ~is_path:true
562 path ~localization_tbl, localization_tbl)
564 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
565 assert (context = []);
566 assert (is_path = false);
567 let interpretate_term = interpretate_term ~localization_tbl in
569 | CicNotationPt.Inductive (params,tyl) ->
570 let uri = match uri with Some uri -> uri | None -> assert false in
574 (fun (context,res) (name,t) ->
577 None -> CicNotationPt.Implicit
579 let name = CicNotationUtil.cic_name_of_name name in
580 name::context,(name, interpretate_term context env None false t)::res
583 context,List.rev res in
585 List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
589 (*here the explicit_named_substituion is assumed to be of length 0 *)
590 (fun (i,res) (name,_,_,_) ->
591 i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
593 let con_env = DisambiguateTypes.env_of_list name_to_uris env in
596 (fun (name,b,ty,cl) ->
597 let ty' = add_params (interpretate_term context env None false ty) in
602 add_params (interpretate_term context con_env None false ty)
610 Cic.InductiveDefinition (tyl,[],List.length params,[])
611 | CicNotationPt.Record (params,name,ty,fields) ->
612 let uri = match uri with Some uri -> uri | None -> assert false in
616 (fun (context,res) (name,t) ->
619 None -> CicNotationPt.Implicit
621 let name = CicNotationUtil.cic_name_of_name name in
622 name::context,(name, interpretate_term context env None false t)::res
625 context,List.rev res in
628 (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
629 let ty' = add_params (interpretate_term context env None false ty) in
633 (fun (context,res) (name,ty,_coercion,arity) ->
634 let context' = Cic.Name name :: context in
635 context',(name,interpretate_term context env None false ty)::res
636 ) (context,[]) fields) in
638 (*here the explicit_named_substituion is assumed to be of length 0 *)
639 let mutind = Cic.MutInd (uri,0,[]) in
640 if params = [] then mutind
643 (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
646 (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
648 let con' = add_params con in
649 let tyl = [name,true,ty',["mk_" ^ name,con']] in
650 let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
651 Cic.InductiveDefinition
652 (tyl,[],List.length params,[`Class (`Record field_names)])
653 | CicNotationPt.Theorem (flavour, name, ty, bo) ->
654 let attrs = [`Flavour flavour] in
655 let ty' = interpretate_term [] env None false ty in
656 (match bo,flavour with
658 Cic.Constant (name,None,ty',[],attrs)
659 | Some bo,`Axiom -> assert false
661 Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
663 let bo' = Some (interpretate_term [] env None false bo) in
664 Cic.Constant (name,bo',ty',[],attrs))
667 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
670 let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
671 interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
676 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
677 | Ast.AttributedTerm (`Loc loc, term) ->
678 domain_of_term ~loc ~context term
679 | Ast.AttributedTerm (_, term) ->
680 domain_of_term ~loc ~context term
681 | Ast.Symbol (symbol, instance) ->
682 [ Node ([loc], Symbol (symbol, instance), []) ]
683 (* to be kept in sync with Ast.Appl (Ast.Symbol ...) *)
684 | Ast.Appl (Ast.Symbol (symbol, instance) as hd :: args)
685 | Ast.Appl (Ast.AttributedTerm (_,Ast.Symbol (symbol, instance)) as hd :: args)
689 (fun term acc -> domain_of_term ~loc ~context term @ acc)
693 Ast.AttributedTerm (`Loc loc,_) -> loc
696 [ Node ([loc], Symbol (symbol, instance), args_dom) ]
697 | Ast.Appl (Ast.Ident (name, subst) as hd :: args)
698 | Ast.Appl (Ast.AttributedTerm (_,Ast.Ident (name, subst)) as hd :: args) ->
701 (fun term acc -> domain_of_term ~loc ~context term @ acc)
705 Ast.AttributedTerm (`Loc loc,_) -> loc
709 (* the next line can raise Not_found *)
710 ignore(find_in_context name context);
711 if subst <> None then
712 Ast.fail loc "Explicit substitutions not allowed here"
717 | None -> [ Node ([loc], Id name, args_dom) ]
721 (fun dom (_, term) ->
722 let dom' = domain_of_term ~loc ~context term in
725 [ Node ([loc], Id name, terms @ args_dom) ]))
728 (fun term acc -> domain_of_term ~loc ~context term @ acc)
730 | Ast.Binder (kind, (var, typ), body) ->
731 let type_dom = domain_of_term_option ~loc ~context typ in
734 ~context:(CicNotationUtil.cic_name_of_name var :: context) body in
736 | `Exists -> [ Node ([loc], Symbol ("exists", 0), (type_dom @ body_dom)) ]
737 | _ -> type_dom @ body_dom)
738 | Ast.Case (term, indty_ident, outtype, branches) ->
739 let term_dom = domain_of_term ~loc ~context term in
740 let outtype_dom = domain_of_term_option ~loc ~context outtype in
741 let rec get_first_constructor = function
743 | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
744 | _ :: tl -> get_first_constructor tl in
747 Ast.Pattern (head, _, args), term ->
748 let (term_context, args_domain) =
750 (fun (cont, dom) (name, typ) ->
751 (CicNotationUtil.cic_name_of_name name :: cont,
754 | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
757 domain_of_term ~loc ~context:term_context term @ args_domain
758 | Ast.Wildcard, term ->
759 domain_of_term ~loc ~context term
762 List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
763 (match indty_ident with
764 | None -> get_first_constructor branches
765 | Some (ident, _) -> [ Node ([loc], Id ident, []) ])
766 @ term_dom @ outtype_dom @ branches_dom
767 | Ast.Cast (term, ty) ->
768 let term_dom = domain_of_term ~loc ~context term in
769 let ty_dom = domain_of_term ~loc ~context ty in
771 | Ast.LetIn ((var, typ), body, where) ->
772 let body_dom = domain_of_term ~loc ~context body in
773 let type_dom = domain_of_term_option ~loc ~context typ in
776 ~context:(CicNotationUtil.cic_name_of_name var :: context) where in
777 body_dom @ type_dom @ where_dom
778 | Ast.LetRec (kind, defs, where) ->
779 let add_defs context =
781 (fun acc (_, (var, _), _, _) ->
782 CicNotationUtil.cic_name_of_name var :: acc
784 let where_dom = domain_of_term ~loc ~context:(add_defs context) where in
787 (fun dom (params, (_, typ), body, _) ->
791 (fun acc (var,_) -> CicNotationUtil.cic_name_of_name var :: acc)
797 (fun (context,res) (var,ty) ->
798 CicNotationUtil.cic_name_of_name var :: context,
799 domain_of_term_option ~loc ~context ty @ res)
800 (add_defs context,[]) params))
802 @ domain_of_term_option ~loc ~context:context' typ
803 @ domain_of_term ~loc ~context:context' body
807 | Ast.Ident (name, subst) ->
809 (* the next line can raise Not_found *)
810 ignore(find_in_context name context);
811 if subst <> None then
812 Ast.fail loc "Explicit substitutions not allowed here"
817 | None -> [ Node ([loc], Id name, []) ]
821 (fun dom (_, term) ->
822 let dom' = domain_of_term ~loc ~context term in
825 [ Node ([loc], Id name, terms) ]))
828 | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
829 | Ast.Meta (index, local_context) ->
831 (fun dom term -> dom @ domain_of_term_option ~loc ~context term)
838 | Ast.Variable _ -> assert false
840 and domain_of_term_option ~loc ~context = function
842 | Some t -> domain_of_term ~loc ~context t
844 let domain_of_term ~context term =
845 uniq_domain (domain_of_term ~context term)
847 let domain_of_obj ~context ast =
848 let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
849 assert (context = []);
851 | Ast.Theorem (_,_,ty,bo) ->
855 | Some bo -> domain_of_term [] bo)
856 | Ast.Inductive (params,tyl) ->
859 (fun (context, dom) (var, ty) ->
860 let context' = CicNotationUtil.cic_name_of_name var :: context in
862 None -> context', dom
863 | Some ty -> context', dom @ domain_of_term context ty
865 let context_w_types =
867 (fun (var, _, _, _) -> Cic.Name var) tyl
873 domain_of_term context ty
876 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
878 | CicNotationPt.Record (params,var,ty,fields) ->
881 (fun (context, dom) (var, ty) ->
882 let context' = CicNotationUtil.cic_name_of_name var :: context in
884 None -> context', dom
885 | Some ty -> context', dom @ domain_of_term context ty
887 let context_w_types = Cic.Name var :: context in
889 @ domain_of_term context ty
892 (fun (context,res) (name,ty,_,_) ->
893 Cic.Name name::context, res @ domain_of_term context ty
894 ) (context_w_types,[]) fields)
896 let domain_of_obj ~context obj =
897 uniq_domain (domain_of_obj ~context obj)
899 let domain_of_ast_term = domain_of_term;;
901 let domain_of_term ~context term =
903 List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
905 domain_of_term ~context term
908 let domain_diff dom1 dom2 =
909 (* let domain_diff = Domain.diff *)
913 | Symbol (symb, 0) ->
915 Symbol (symb',_) when symb = symb' -> true
927 | Node (_,elt,l)::tl when is_in_dom2 elt -> aux (l @ tl)
928 | Node (loc,elt,l)::tl -> Node (loc,elt,aux l)::(aux tl)
932 module type Disambiguator =
934 val disambiguate_thing:
937 metasenv:'metasenv ->
939 initial_ugraph:'ugraph ->
940 hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
941 (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
942 ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
943 aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
944 universe:DisambiguateTypes.codomain_item list
945 DisambiguateTypes.Environment.t option ->
947 pp_thing:('ast_thing -> string) ->
948 domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
949 interpretate_thing:(context:'context ->
950 env:DisambiguateTypes.codomain_item
951 DisambiguateTypes.Environment.t ->
953 is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
954 refine_thing:('metasenv ->
959 'ugraph -> localization_tbl:'cichash ->
960 ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
961 localization_tbl:'cichash ->
962 string * int * 'ast_thing ->
963 ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
964 list * 'metasenv * 'subst * 'refined_thing * 'ugraph)
967 val disambiguate_term :
968 ?fresh_instances:bool ->
970 context:Cic.context ->
971 metasenv:Cic.metasenv ->
972 subst:Cic.substitution ->
974 ?initial_ugraph:CicUniv.universe_graph ->
975 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
976 universe:DisambiguateTypes.multiple_environment option ->
977 CicNotationPt.term disambiguator_input ->
978 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
979 Cic.metasenv * (* new metasenv *)
982 CicUniv.universe_graph) list * (* disambiguated term *)
985 val disambiguate_obj :
986 ?fresh_instances:bool ->
988 aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
989 universe:DisambiguateTypes.multiple_environment option ->
990 uri:UriManager.uri option -> (* required only for inductive types *)
991 CicNotationPt.term CicNotationPt.obj disambiguator_input ->
992 ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
993 Cic.metasenv * (* new metasenv *)
996 CicUniv.universe_graph) list * (* disambiguated obj *)
1000 module Make (C: Callbacks) =
1002 let choices_of_id dbd id =
1003 let uris = Whelp.locate ~dbd id in
1008 (C.input_or_locate_uri
1009 ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())
1012 | Some uri -> [uri])
1015 C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
1016 ~ok:"Try selected." ~enable_button_for_non_vars:true
1017 ~title:"Ambiguous input." ~id
1018 ~msg: ("Ambiguous input \"" ^ id ^
1019 "\". Please, choose one or more interpretations:")
1024 (UriManager.string_of_uri uri,
1027 CicUtil.term_of_uri uri
1029 debug_print (lazy (UriManager.string_of_uri uri));
1030 debug_print (lazy (Printexc.to_string exn));
1036 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
1038 let disambiguate_thing ~dbd ~context ~metasenv ~subst
1039 ~initial_ugraph:base_univ ~hint
1041 ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
1043 (thing_txt,thing_txt_prefix_len,thing)
1045 debug_print (lazy "DISAMBIGUATE INPUT");
1046 debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
1047 let thing_dom = domain_of_thing ~context thing in
1049 (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
1051 debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
1052 (DisambiguatePp.pp_environment aliases)));
1053 debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
1054 (match universe with None -> "None" | Some _ -> "Some _")));
1057 Environment.fold (fun item _ dom -> item :: dom) aliases [] in
1058 let todo_dom = domain_diff thing_dom current_dom in
1060 (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
1061 (* (2) lookup function for any item (Id/Symbol/Num) *)
1062 let lookup_choices =
1065 let lookup_in_library () =
1067 | Id id -> choices_of_id dbd id
1068 | Symbol (symb, _) ->
1070 List.map DisambiguateChoices.mk_choice
1071 (TermAcicContent.lookup_interpretations symb)
1073 TermAcicContent.Interpretation_not_found -> [])
1075 DisambiguateChoices.lookup_num_choices ()
1078 | None -> lookup_in_library ()
1083 | Symbol (symb, _) -> Symbol (symb, 0)
1086 Environment.find item e
1087 with Not_found -> lookup_in_library ())
1094 if benchmark then begin
1095 let per_item_choices =
1099 let len = List.length (lookup_choices dom_item) in
1100 debug_print (lazy (sprintf "BENCHMARK %s: %d"
1101 (string_of_domain_item dom_item) len));
1103 with No_choices _ -> 0)
1106 max_refinements := List.fold_left ( * ) 1 per_item_choices;
1107 actual_refinements := 0;
1108 domain_size := List.length thing_dom;
1110 (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size)
1116 (* (3) test an interpretation filling with meta uninterpreted identifiers
1118 let test_env aliases todo_dom ugraph =
1119 let rec aux env = function
1121 | Node (_, item, l) :: tl ->
1123 Environment.add item
1127 (fun _ _ _ -> Cic.Implicit (Some `Closed))
1128 | Symbol _ -> (fun _ _ _ -> Cic.Implicit None)))
1130 aux (aux env l) tl in
1131 let filled_env = aux aliases todo_dom in
1134 interpretate_thing ~context ~env:filled_env
1135 ~uri ~is_path:false thing ~localization_tbl
1137 let cic_thing = (fst hint) metasenv cic_thing in
1140 refine_thing metasenv subst
1141 context uri cic_thing ugraph ~localization_tbl
1143 let k = (snd hint) k in
1145 in refine_profiler.HExtlib.profile foo ()
1147 | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
1148 | Invalid_choice loc_msg -> Ko loc_msg
1150 (* (4) build all possible interpretations *)
1151 let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
1152 (* aux returns triples Ok/Uncertain/Ko *)
1153 (* rem_dom is the concatenation of all the remainin domains *)
1154 let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom =
1155 debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
1158 assert (lookup_in_todo_dom = None);
1159 (match test_env aliases rem_dom base_univ with
1160 | Ok (thing, metasenv,subst,new_univ) ->
1161 [ aliases, diff, metasenv, subst, thing, new_univ ], [], []
1162 | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true]
1163 | Uncertain loc_msg ->
1164 [],[aliases,diff,loc_msg],[])
1165 | Node (locs,item,inner_dom) :: remaining_dom ->
1166 debug_print (lazy (sprintf "CHOOSED ITEM: %s"
1167 (string_of_domain_item item)));
1169 match lookup_in_todo_dom with
1170 None -> lookup_choices item
1171 | Some choices -> choices in
1176 (lazy (List.hd locs,
1177 "No choices for " ^ string_of_domain_item item)),
1180 | [codomain_item] ->
1181 (* just one choice. We perform a one-step look-up and
1182 if the next set of choices is also a singleton we
1183 skip this refinement step *)
1184 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1185 let new_env = Environment.add item codomain_item aliases in
1186 let new_diff = (item,codomain_item)::diff in
1187 let lookup_in_todo_dom,next_choice_is_single =
1188 match remaining_dom with
1191 let choices = lookup_choices he in
1192 Some choices,List.length choices = 1
1194 if next_choice_is_single then
1195 aux new_env new_diff lookup_in_todo_dom remaining_dom
1198 (match test_env new_env remaining_dom base_univ with
1199 | Ok (thing, metasenv),new_univ ->
1200 (match remaining_dom with
1202 [ new_env, new_diff, metasenv, thing, new_univ ], []
1204 aux new_env new_diff lookup_in_todo_dom
1205 remaining_dom new_univ)
1206 | Uncertain (loc,msg),new_univ ->
1207 (match remaining_dom with
1208 | [] -> [], [new_env,new_diff,loc,msg,true]
1210 aux new_env new_diff lookup_in_todo_dom
1211 remaining_dom new_univ)
1212 | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
1215 let mark_not_significant failures =
1217 (fun (env, diff, loc_msg, _b) ->
1218 env, diff, loc_msg, false)
1220 let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
1221 if ok_l <> [] || uncertain_l <> [] then
1222 ok_l,uncertain_l,mark_not_significant error_l
1225 let rec filter = function
1227 | codomain_item :: tl ->
1228 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
1229 let new_env = Environment.add item codomain_item aliases in
1230 let new_diff = (item,codomain_item)::diff in
1233 (inner_dom@remaining_dom@rem_dom) base_univ
1235 | Ok (thing, metasenv,subst,new_univ) ->
1237 (match inner_dom with
1239 [new_env,new_diff,metasenv,subst,thing,new_univ],
1242 aux new_env new_diff None inner_dom
1243 (remaining_dom@rem_dom)
1247 | Uncertain loc_msg ->
1249 (match inner_dom with
1250 | [] -> [],[new_env,new_diff,loc_msg],[]
1252 aux new_env new_diff None inner_dom
1253 (remaining_dom@rem_dom)
1258 let res = [],[],[new_env,new_diff,loc_msg,true] in
1261 let ok_l,uncertain_l,error_l =
1262 classify_errors (filter choices)
1264 let res_after_ok_l =
1266 (fun (env,diff,_,_,_,_) res ->
1267 aux env diff None remaining_dom rem_dom @@ res
1268 ) ok_l ([],[],error_l)
1271 (fun (env,diff,_) res ->
1272 aux env diff None remaining_dom rem_dom @@ res
1273 ) uncertain_l res_after_ok_l
1275 let aux' aliases diff lookup_in_todo_dom todo_dom =
1276 match test_env aliases todo_dom base_univ with
1279 aux aliases diff lookup_in_todo_dom todo_dom []
1280 | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in
1283 match aux' aliases [] None todo_dom with
1284 | [],uncertain,errors ->
1287 (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)
1288 ) uncertain @ errors
1292 (fun (env,diff,loc_msg,significant) ->
1295 (fun locs domain_item ->
1298 fst (Environment.find domain_item env)
1300 Some (locs,descr_of_domain_item domain_item,description)
1305 env',diff,loc_msg,significant
1308 raise (NoWellTypedInterpretation (0,errors))
1309 | [_,diff,metasenv,subst,t,ugraph],_,_ ->
1310 debug_print (lazy "SINGLE INTERPRETATION");
1311 [diff,metasenv,subst,t,ugraph], false
1314 (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
1317 (fun (env, _, _, _, _, _) ->
1319 (fun locs domain_item ->
1321 fst (Environment.find domain_item env)
1323 locs,descr_of_domain_item domain_item, description)
1328 C.interactive_interpretation_choice
1329 thing_txt thing_txt_prefix_len choices
1331 (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u)
1337 CicEnvironment.CircularDependency s ->
1338 failwith "Disambiguate: circular dependency"
1340 let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
1342 ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
1343 (text,prefix_len,term)
1346 if fresh_instances then CicNotationUtil.freshen_term term else term
1348 let hint = match goal with
1349 | None -> (fun _ x -> x), fun k -> k
1352 let _,c,ty = CicUtil.lookup_meta i metasenv in
1358 | Cic.Cast(t,_) -> Ok (t,m,s,ug)
1359 | _ -> assert false)
1362 let localization_tbl = Cic.CicHash.create 503 in
1363 disambiguate_thing ~dbd ~context ~metasenv ~subst
1364 ~initial_ugraph ~aliases
1365 ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
1366 ~domain_of_thing:domain_of_term
1367 ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
1368 ~refine_thing:refine_term (text,prefix_len,term)
1372 let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
1373 (text,prefix_len,obj)
1376 if fresh_instances then CicNotationUtil.freshen_obj obj else obj
1382 let localization_tbl = Cic.CicHash.create 503 in
1383 disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~subst:[]
1384 ~aliases ~universe ~uri
1385 ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
1386 ~initial_ugraph:CicUniv.empty_ugraph
1387 ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
1390 (text,prefix_len,obj)