2 Copyright (C) 1999-2006, HELM Team.
4 This file is part of HELM, an Hypertextual, Electronic
5 Library of Mathematics, developed at the Computer Science
6 Department, University of Bologna, Italy.
8 HELM is free software; you can redistribute it and/or
9 modify it under the terms of the GNU General Public License
10 as published by the Free Software Foundation; either version 2
11 of the License, or (at your option) any later version.
13 HELM is distributed in the hope that it will be useful,
14 but WITHOUT ANY WARRANTY; without even the implied warranty of
15 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16 GNU General Public License for more details.
18 You should have received a copy of the GNU General Public License
19 along with this program; if not, write to the Free Software
20 Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
23 For details, see the HELM web site: http://helm.cs.unibo.it/
27 module Ast = CicNotationPt
30 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
32 let rec string_context_of_context =
35 | Cic.Name n -> Some n
36 | Cic.Anonymous -> Some "_")
39 let refine_term metasenv subst context uri ~use_coercions
40 term ugraph ~localization_tbl =
41 (* if benchmark then incr actual_refinements; *)
43 debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
44 let saved_use_coercions = !CicRefine.insert_coercions in
46 CicRefine.insert_coercions := use_coercions;
47 let term', _, metasenv',ugraph1 =
48 CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl
50 CicRefine.insert_coercions := saved_use_coercions;
51 (Disambiguate.Ok (term', metasenv',[],ugraph1))
54 CicRefine.insert_coercions := saved_use_coercions;
55 let rec process_exn loc =
57 HExtlib.Localized (loc,exn) -> process_exn loc exn
58 | CicRefine.Uncertain msg ->
59 debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
60 Disambiguate.Uncertain (lazy (loc,Lazy.force msg))
61 | CicRefine.RefineFailure msg ->
62 debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
63 (CicPp.ppterm term) (Lazy.force msg)));
64 Disambiguate.Ko (lazy (loc,Lazy.force msg))
67 process_exn Stdpp.dummy_loc exn
69 let refine_obj metasenv subst context uri ~use_coercions obj ugraph
71 assert (context = []);
72 assert (metasenv = []);
74 debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
75 let saved_use_coercions = !CicRefine.insert_coercions in
77 CicRefine.insert_coercions := use_coercions;
78 let obj', metasenv,ugraph =
79 CicRefine.typecheck metasenv uri obj ~localization_tbl
81 CicRefine.insert_coercions := saved_use_coercions;
82 (Disambiguate.Ok (obj', metasenv,[],ugraph))
85 CicRefine.insert_coercions := saved_use_coercions;
86 let rec process_exn loc =
88 HExtlib.Localized (loc,exn) -> process_exn loc exn
89 | CicRefine.Uncertain msg ->
90 debug_print (lazy ("UNCERTAIN!!! [" ^
91 (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
92 Disambiguate.Uncertain (lazy (loc,Lazy.force msg))
93 | CicRefine.RefineFailure msg ->
94 debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
95 (CicPp.ppobj obj) (Lazy.force msg))) ;
96 Disambiguate.Ko (lazy (loc,Lazy.force msg))
99 process_exn Stdpp.dummy_loc exn
102 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
105 (* create_dummy_ids shouldbe used only for interpretating patterns *)
107 let rec aux ~localize loc context = function
108 | CicNotationPt.AttributedTerm (`Loc loc, term) ->
109 let res = aux ~localize loc context term in
110 if localize then Cic.CicHash.add localization_tbl res loc;
112 | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
113 | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
114 let cic_args = List.map (aux ~localize loc context) args in
115 Disambiguate.resolve env
116 (DisambiguateTypes.Symbol (symb, i)) ~args:cic_args ()
117 | CicNotationPt.Appl terms ->
118 Cic.Appl (List.map (aux ~localize loc context) terms)
119 | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
120 let cic_type = aux_option ~localize loc context (Some `Type) typ in
121 let cic_name = CicNotationUtil.cic_name_of_name var in
122 let cic_body = aux ~localize loc (cic_name :: context) body in
123 (match binder_kind with
124 | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
126 | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
128 Disambiguate.resolve env (DisambiguateTypes.Symbol ("exists", 0))
129 ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ())
130 | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
131 let cic_term = aux ~localize loc context term in
132 let cic_outtype = aux_option ~localize loc context None outtype in
133 let do_branch ((head, _, args), term) =
134 let rec do_branch' context = function
135 | [] -> aux ~localize loc context term
136 | (name, typ) :: tl ->
137 let cic_name = CicNotationUtil.cic_name_of_name name in
138 let cic_body = do_branch' (cic_name :: context) tl in
141 | None -> Cic.Implicit (Some `Type)
142 | Some typ -> aux ~localize loc context typ
144 Cic.Lambda (cic_name, typ, cic_body)
146 do_branch' context args
148 let indtype_uri, indtype_no =
149 if create_dummy_ids then
150 (UriManager.uri_of_string "cic:/fake_indty.con", 0)
152 match indty_ident with
153 | Some (indty_ident, _) ->
155 Disambiguate.resolve env
156 (DisambiguateTypes.Id indty_ident) ()
158 | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
160 raise (Disambiguate.Try_again
161 (lazy "The type of the term to be matched
164 raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
166 let rec fst_constructor =
168 (Ast.Pattern (head, _, _), _) :: _ -> head
169 | (Ast.Wildcard, _) :: tl -> fst_constructor tl
170 | [] -> raise (DisambiguateTypes.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")))
172 (match Disambiguate.resolve env
173 (DisambiguateTypes.Id (fst_constructor branches)) () with
174 | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
175 (indtype_uri, indtype_no)
177 raise (Disambiguate.Try_again (lazy "The type of the term to be matched
180 raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
183 if create_dummy_ids then
186 Ast.Wildcard,term -> ("wildcard",None,[]), term
188 raise (DisambiguateTypes.Invalid_choice (lazy (loc, "Syntax error: the left hand side of a branch patterns must be \"_\"")))
191 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
192 Cic.InductiveDefinition (il,_,leftsno,_) ->
195 List.nth il indtype_no
196 with _ -> assert false
198 let rec count_prod t =
199 match CicReduction.whd [] t with
200 Cic.Prod (_, _, t) -> 1 + (count_prod t)
203 let rec sort branches cl =
206 let rec analyze unused unrecognized useless =
209 if unrecognized != [] then
210 raise (DisambiguateTypes.Invalid_choice
212 ("Unrecognized constructors: " ^
213 String.concat " " unrecognized))))
214 else if useless > 0 then
215 raise (DisambiguateTypes.Invalid_choice
217 ("The last " ^ string_of_int useless ^
218 "case" ^ if useless > 1 then "s are" else " is" ^
222 | (Ast.Wildcard,_)::tl when not unused ->
223 analyze true unrecognized useless tl
224 | (Ast.Pattern (head,_,_),_)::tl when not unused ->
225 analyze unused (head::unrecognized) useless tl
226 | _::tl -> analyze unused unrecognized (useless + 1) tl
228 analyze false [] 0 branches
230 let rec find_and_remove =
234 (DisambiguateTypes.Invalid_choice
235 (lazy (loc, ("Missing case: " ^ name))))
236 | ((Ast.Wildcard, _) as branch :: _) as branches ->
238 | (Ast.Pattern (name',_,_),_) as branch :: tl
242 let found,rest = find_and_remove tl in
245 let branch,tl = find_and_remove branches in
247 Ast.Pattern (name,y,args),term ->
248 if List.length args = count_prod ty - leftsno then
249 ((name,y,args),term)::sort tl cltl
252 (DisambiguateTypes.Invalid_choice
253 (lazy (loc,"Wrong number of arguments for " ^
255 | Ast.Wildcard,term ->
261 (`Lambda, (CicNotationPt.Ident ("_", None), None),
264 (("wildcard",None,[]),
265 mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
270 Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
271 (List.map do_branch branches))
272 | CicNotationPt.Cast (t1, t2) ->
273 let cic_t1 = aux ~localize loc context t1 in
274 let cic_t2 = aux ~localize loc context t2 in
275 Cic.Cast (cic_t1, cic_t2)
276 | CicNotationPt.LetIn ((name, typ), def, body) ->
277 let cic_def = aux ~localize loc context def in
278 let cic_name = CicNotationUtil.cic_name_of_name name in
281 | None -> Cic.Implicit (Some `Type)
282 | Some t -> aux ~localize loc context t
284 let cic_body = aux ~localize loc (cic_name :: context) body in
285 Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
286 | CicNotationPt.LetRec (kind, defs, body) ->
289 (fun acc (_, (name, _), _, _) ->
290 CicNotationUtil.cic_name_of_name name :: acc)
294 let unlocalized_body = aux ~localize:false loc context' body in
295 match unlocalized_body with
296 Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
297 | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
302 let t',subst,metasenv =
303 CicMetaSubst.delift_rels [] [] (List.length defs) t
306 assert (metasenv=[]);
309 (* We can avoid the LetIn. But maybe we need to recompute l'
310 so that it is localized *)
313 CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
314 (* since we avoid the letin, the context has no
316 let l' = List.map (aux ~localize loc context) l in
322 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
324 `AddLetIn (aux ~localize loc context' body)
326 `AddLetIn unlocalized_body)
329 `AddLetIn (aux ~localize loc context' body)
331 `AddLetIn unlocalized_body
335 (fun (params, (name, typ), body, decr_idx) ->
336 let add_binders kind t =
338 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
341 aux ~localize loc context' (add_binders `Lambda body) in
343 aux_option ~localize loc context (Some `Type)
344 (HExtlib.map_option (add_binders `Pi) typ) in
346 match CicNotationUtil.cic_name_of_name name with
348 CicNotationPt.fail loc
349 "Recursive functions cannot be anonymous"
350 | Cic.Name name -> name
352 (name, decr_idx, cic_type, cic_body))
357 `Inductive -> Cic.Fix (n,inductiveFuns)
359 let coinductiveFuns =
361 (fun (name, _, typ, body) -> name, typ, body)
364 Cic.CoFix (n,coinductiveFuns)
366 let counter = ref ~-1 in
367 let build_term funs (var,_,ty,_) t =
369 Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
372 `AvoidLetInNoAppl n ->
373 let n' = List.length inductiveFuns - n in
375 | `AvoidLetIn (n,l) ->
376 let n' = List.length inductiveFuns - n in
377 Cic.Appl (fix_or_cofix n'::l)
378 | `AddLetIn cic_body ->
379 List.fold_right (build_term inductiveFuns) inductiveFuns
381 | CicNotationPt.Ident _
382 | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
383 | CicNotationPt.Ident (name, subst)
384 | CicNotationPt.Uri (name, subst) as ast ->
385 let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
387 if is_uri ast then raise Not_found;(* don't search the env for URIs *)
389 Disambiguate.find_in_context name (string_context_of_context context)
391 if subst <> None then
392 CicNotationPt.fail loc "Explicit substitutions not allowed here";
396 if is_uri ast then (* we have the URI, build the term out of it *)
398 CicUtil.term_of_uri (UriManager.uri_of_string name)
399 with UriManager.IllFormedUri _ ->
400 CicNotationPt.fail loc "Ill formed URI"
402 Disambiguate.resolve env (DisambiguateTypes.Id name) ()
406 List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
413 List.assoc s ids_to_uris, aux ~localize loc context term
415 raise (DisambiguateTypes.Invalid_choice (lazy (loc, "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))))
417 | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
421 | Cic.Const (uri, []) ->
422 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
423 let uris = CicUtil.params_of_obj o in
424 Cic.Const (uri, mk_subst uris)
425 | Cic.Var (uri, []) ->
426 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
427 let uris = CicUtil.params_of_obj o in
428 Cic.Var (uri, mk_subst uris)
429 | Cic.MutInd (uri, i, []) ->
431 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
432 let uris = CicUtil.params_of_obj o in
433 Cic.MutInd (uri, i, mk_subst uris)
435 CicEnvironment.Object_not_found _ ->
436 (* if we are here it is probably the case that during the
437 definition of a mutual inductive type we have met an
438 occurrence of the type in one of its constructors.
439 However, the inductive type is not yet in the environment
441 (*here the explicit_named_substituion is assumed to be of length 0 *)
442 Cic.MutInd (uri,i,[]))
443 | Cic.MutConstruct (uri, i, j, []) ->
444 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
445 let uris = CicUtil.params_of_obj o in
446 Cic.MutConstruct (uri, i, j, mk_subst uris)
447 | Cic.Meta _ | Cic.Implicit _ as t ->
449 debug_print (lazy (sprintf
450 "Warning: %s must be instantiated with _[%s] but we do not enforce it"
454 (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
459 raise (DisambiguateTypes.Invalid_choice (lazy (loc, "??? Can this happen?")))
461 CicEnvironment.CircularDependency _ ->
462 raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
463 | CicNotationPt.Implicit -> Cic.Implicit None
464 | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
465 | CicNotationPt.Num (num, i) -> Disambiguate.resolve env (DisambiguateTypes.Num i) ~num ()
466 | CicNotationPt.Meta (index, subst) ->
471 | Some term -> Some (aux ~localize loc context term))
474 Cic.Meta (index, cic_subst)
475 | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
476 | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
477 | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
478 | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
479 | CicNotationPt.Symbol (symbol, instance) ->
480 Disambiguate.resolve env (DisambiguateTypes.Symbol (symbol, instance)) ()
481 | _ -> assert false (* god bless Bologna *)
482 and aux_option ~localize loc context annotation = function
483 | None -> Cic.Implicit annotation
484 | Some term -> aux ~localize loc context term
486 aux ~localize:true HExtlib.dummy_floc context ast
488 let interpretate_path ~context path =
489 let localization_tbl = Cic.CicHash.create 23 in
490 (* here we are throwing away useful localization informations!!! *)
492 interpretate_term ~create_dummy_ids:true
493 ~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true
494 path ~localization_tbl, localization_tbl)
496 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
497 assert (context = []);
498 assert (is_path = false);
499 let interpretate_term = interpretate_term ~localization_tbl in
501 | CicNotationPt.Inductive (params,tyl) ->
502 let uri = match uri with Some uri -> uri | None -> assert false in
506 (fun (context,res) (name,t) ->
509 None -> CicNotationPt.Implicit
511 let name = CicNotationUtil.cic_name_of_name name in
512 name::context,(name, interpretate_term context env None false t)::res
515 context,List.rev res in
517 List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
521 (*here the explicit_named_substituion is assumed to be of length 0 *)
522 (fun (i,res) (name,_,_,_) ->
523 i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
525 let con_env = DisambiguateTypes.env_of_list name_to_uris env in
528 (fun (name,b,ty,cl) ->
529 let ty' = add_params (interpretate_term context env None false ty) in
534 add_params (interpretate_term context con_env None false ty)
542 Cic.InductiveDefinition (tyl,[],List.length params,[])
543 | CicNotationPt.Record (params,name,ty,fields) ->
544 let uri = match uri with Some uri -> uri | None -> assert false in
548 (fun (context,res) (name,t) ->
551 None -> CicNotationPt.Implicit
553 let name = CicNotationUtil.cic_name_of_name name in
554 name::context,(name, interpretate_term context env None false t)::res
557 context,List.rev res in
560 (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
561 let ty' = add_params (interpretate_term context env None false ty) in
565 (fun (context,res) (name,ty,_coercion,arity) ->
566 let context' = Cic.Name name :: context in
567 context',(name,interpretate_term context env None false ty)::res
568 ) (context,[]) fields) in
570 (*here the explicit_named_substituion is assumed to be of length 0 *)
571 let mutind = Cic.MutInd (uri,0,[]) in
572 if params = [] then mutind
575 (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
578 (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
580 let con' = add_params con in
581 let tyl = [name,true,ty',["mk_" ^ name,con']] in
582 let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
583 Cic.InductiveDefinition
584 (tyl,[],List.length params,[`Class (`Record field_names)])
585 | CicNotationPt.Theorem (flavour, name, ty, bo) ->
586 let attrs = [`Flavour flavour] in
587 let ty' = interpretate_term [] env None false ty in
588 (match bo,flavour with
590 Cic.Constant (name,None,ty',[],attrs)
591 | Some bo,`Axiom -> assert false
593 Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
595 let bo' = Some (interpretate_term [] env None false bo) in
596 Cic.Constant (name,bo',ty',[],attrs))
599 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
602 let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
603 interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
608 function true -> Cic.Implicit (Some `Closed)
609 | _ -> Cic.Implicit None
612 let string_context_of_context =
613 List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some
614 (Cic.Anonymous,_) -> Some "_");;
616 let disambiguate_term ~context ~metasenv ~subst ?goal
617 ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
619 (text,prefix_len,term)
621 let hint = match goal with
622 | None -> (fun _ x -> x), fun k -> k
625 let _,c,ty = CicUtil.lookup_meta i metasenv in
629 | Disambiguate.Ok (t,m,s,ug) ->
631 | Cic.Cast(t,_) -> Disambiguate.Ok (t,m,s,ug)
635 let localization_tbl = Cic.CicHash.create 503 in
636 MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
637 ~initial_ugraph ~aliases ~mk_implicit ~string_context_of_context
638 ~universe ~lookup_in_library
639 ~uri:None ~pp_thing:CicNotationPp.pp_term
640 ~domain_of_thing:Disambiguate.domain_of_term
641 ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))
642 ~refine_thing:refine_term (text,prefix_len,term)
645 ~freshen_thing:CicNotationUtil.freshen_term
646 ~passes:(MultiPassDisambiguator.passes ())
648 let disambiguate_obj ~aliases ~universe ~uri ~lookup_in_library
649 (text,prefix_len,obj)
651 let hint = (fun _ x -> x), fun k -> k in
652 let localization_tbl = Cic.CicHash.create 503 in
653 MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
654 ~aliases ~universe ~uri ~mk_implicit ~string_context_of_context
655 ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
656 ~domain_of_thing:Disambiguate.domain_of_obj
658 ~initial_ugraph:CicUniv.empty_ugraph
659 ~interpretate_thing:interpretate_obj
660 ~refine_thing:refine_obj
663 ~passes:(MultiPassDisambiguator.passes ())
664 ~freshen_thing:CicNotationUtil.freshen_obj
665 (text,prefix_len,obj)