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 expty 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;
50 | Some ty -> Cic.Cast(term,ty)
52 let term', _, metasenv',ugraph1 =
53 CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl
56 match expty, term' with
58 | Some _,Cic.Cast (term',_) -> term'
61 CicRefine.insert_coercions := saved_use_coercions;
62 (Disambiguate.Ok (term', metasenv',[],ugraph1))
65 CicRefine.insert_coercions := saved_use_coercions;
66 let rec process_exn loc =
68 HExtlib.Localized (loc,exn) -> process_exn loc exn
69 | CicRefine.Uncertain msg ->
70 debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
71 Disambiguate.Uncertain (lazy (loc,Lazy.force msg))
72 | CicRefine.RefineFailure msg ->
73 debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
74 (CicPp.ppterm term) (Lazy.force msg)));
75 Disambiguate.Ko (lazy (loc,Lazy.force msg))
78 process_exn Stdpp.dummy_loc exn
80 let refine_obj metasenv subst context uri ~use_coercions obj _ ugraph
82 assert (context = []);
83 assert (metasenv = []);
85 debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
86 let saved_use_coercions = !CicRefine.insert_coercions in
88 CicRefine.insert_coercions := use_coercions;
89 let obj', metasenv,ugraph =
90 CicRefine.typecheck metasenv uri obj ~localization_tbl
92 CicRefine.insert_coercions := saved_use_coercions;
93 (Disambiguate.Ok (obj', metasenv,[],ugraph))
96 CicRefine.insert_coercions := saved_use_coercions;
97 let rec process_exn loc =
99 HExtlib.Localized (loc,exn) -> process_exn loc exn
100 | CicRefine.Uncertain msg ->
101 debug_print (lazy ("UNCERTAIN!!! [" ^
102 (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
103 Disambiguate.Uncertain (lazy (loc,Lazy.force msg))
104 | CicRefine.RefineFailure msg ->
105 debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
106 (CicPp.ppobj obj) (Lazy.force msg))) ;
107 Disambiguate.Ko (lazy (loc,Lazy.force msg))
110 process_exn Stdpp.dummy_loc exn
113 let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
114 ~is_path ast ~localization_tbl ~obj_context
116 (* create_dummy_ids shouldbe used only for interpretating patterns *)
118 let rec aux ~localize loc context = function
119 | CicNotationPt.AttributedTerm (`Loc loc, term) ->
120 let res = aux ~localize loc context term in
121 if localize then Cic.CicHash.add localization_tbl res loc;
123 | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
124 | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
125 let cic_args = List.map (aux ~localize loc context) args in
126 Disambiguate.resolve ~mk_choice ~env
127 (DisambiguateTypes.Symbol (symb, i)) (`Args cic_args)
128 | CicNotationPt.Appl terms ->
129 Cic.Appl (List.map (aux ~localize loc context) terms)
130 | CicNotationPt.Binder (binder_kind, (var, typ), body) ->
131 let cic_type = aux_option ~localize loc context (Some `Type) typ in
132 let cic_name = CicNotationUtil.cic_name_of_name var in
133 let cic_body = aux ~localize loc (cic_name :: context) body in
134 (match binder_kind with
135 | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body)
137 | `Forall -> Cic.Prod (cic_name, cic_type, cic_body)
139 Disambiguate.resolve ~mk_choice ~env
140 (DisambiguateTypes.Symbol ("exists", 0))
141 (`Args [ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ]))
142 | CicNotationPt.Case (term, indty_ident, outtype, branches) ->
143 let cic_term = aux ~localize loc context term in
144 let cic_outtype = aux_option ~localize loc context None outtype in
145 let do_branch ((head, _, args), term) =
146 let rec do_branch' context = function
147 | [] -> aux ~localize loc context term
148 | (name, typ) :: tl ->
149 let cic_name = CicNotationUtil.cic_name_of_name name in
150 let cic_body = do_branch' (cic_name :: context) tl in
153 | None -> Cic.Implicit (Some `Type)
154 | Some typ -> aux ~localize loc context typ
156 Cic.Lambda (cic_name, typ, cic_body)
158 do_branch' context args
160 let indtype_uri, indtype_no =
161 if create_dummy_ids then
162 (UriManager.uri_of_string "cic:/fake_indty.con", 0)
164 match indty_ident with
165 | Some (indty_ident, _) ->
167 Disambiguate.resolve ~mk_choice ~env
168 (DisambiguateTypes.Id indty_ident) (`Args [])
170 | Cic.MutInd (uri, tyno, _) -> (uri, tyno)
172 raise (Disambiguate.Try_again
173 (lazy "The type of the term to be matched
176 raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
178 let rec fst_constructor =
180 (Ast.Pattern (head, _, _), _) :: _ -> head
181 | (Ast.Wildcard, _) :: tl -> fst_constructor tl
182 | [] -> 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")))
184 (match Disambiguate.resolve ~mk_choice ~env
185 (DisambiguateTypes.Id (fst_constructor branches))
187 | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
188 (indtype_uri, indtype_no)
190 raise (Disambiguate.Try_again (lazy "The type of the term to be matched
193 raise (DisambiguateTypes.Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
196 if create_dummy_ids then
199 Ast.Wildcard,term -> ("wildcard",None,[]), term
201 raise (DisambiguateTypes.Invalid_choice (lazy (loc, "Syntax error: the left hand side of a branch patterns must be \"_\"")))
204 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
205 Cic.InductiveDefinition (il,_,leftsno,_) ->
208 List.nth il indtype_no
209 with _ -> assert false
211 let rec count_prod t =
212 match CicReduction.whd [] t with
213 Cic.Prod (_, _, t) -> 1 + (count_prod t)
216 let rec sort branches cl =
219 let rec analyze unused unrecognized useless =
222 if unrecognized != [] then
223 raise (DisambiguateTypes.Invalid_choice
225 ("Unrecognized constructors: " ^
226 String.concat " " unrecognized))))
227 else if useless > 0 then
228 raise (DisambiguateTypes.Invalid_choice
230 ("The last " ^ string_of_int useless ^
231 "case" ^ if useless > 1 then "s are" else " is" ^
235 | (Ast.Wildcard,_)::tl when not unused ->
236 analyze true unrecognized useless tl
237 | (Ast.Pattern (head,_,_),_)::tl when not unused ->
238 analyze unused (head::unrecognized) useless tl
239 | _::tl -> analyze unused unrecognized (useless + 1) tl
241 analyze false [] 0 branches
243 let rec find_and_remove =
247 (DisambiguateTypes.Invalid_choice
248 (lazy (loc, ("Missing case: " ^ name))))
249 | ((Ast.Wildcard, _) as branch :: _) as branches ->
251 | (Ast.Pattern (name',_,_),_) as branch :: tl
255 let found,rest = find_and_remove tl in
258 let branch,tl = find_and_remove branches in
260 Ast.Pattern (name,y,args),term ->
261 if List.length args = count_prod ty - leftsno then
262 ((name,y,args),term)::sort tl cltl
265 (DisambiguateTypes.Invalid_choice
266 (lazy (loc,"Wrong number of arguments for " ^
268 | Ast.Wildcard,term ->
274 (`Lambda, (CicNotationPt.Ident ("_", None), None),
277 (("wildcard",None,[]),
278 mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
283 Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
284 (List.map do_branch branches))
285 | CicNotationPt.Cast (t1, t2) ->
286 let cic_t1 = aux ~localize loc context t1 in
287 let cic_t2 = aux ~localize loc context t2 in
288 Cic.Cast (cic_t1, cic_t2)
289 | CicNotationPt.LetIn ((name, typ), def, body) ->
290 let cic_def = aux ~localize loc context def in
291 let cic_name = CicNotationUtil.cic_name_of_name name in
294 | None -> Cic.Implicit (Some `Type)
295 | Some t -> aux ~localize loc context t
297 let cic_body = aux ~localize loc (cic_name :: context) body in
298 Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
299 | CicNotationPt.LetRec (kind, defs, body) ->
302 (fun acc (_, (name, _), _, _) ->
303 CicNotationUtil.cic_name_of_name name :: acc)
307 let unlocalized_body = aux ~localize:false loc context' body in
308 match unlocalized_body with
309 Cic.Rel n when n <= List.length defs -> `AvoidLetInNoAppl n
310 | Cic.Appl (Cic.Rel n::l) when n <= List.length defs ->
315 let t',subst,metasenv =
316 CicMetaSubst.delift_rels [] [] (List.length defs) t
319 assert (metasenv=[]);
322 (* We can avoid the LetIn. But maybe we need to recompute l'
323 so that it is localized *)
326 CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
327 (* since we avoid the letin, the context has no
329 let l' = List.map (aux ~localize loc context) l in
335 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
337 `AddLetIn (aux ~localize loc context' body)
339 `AddLetIn unlocalized_body)
342 `AddLetIn (aux ~localize loc context' body)
344 `AddLetIn unlocalized_body
348 (fun (params, (name, typ), body, decr_idx) ->
349 let add_binders kind t =
351 (fun var t -> CicNotationPt.Binder (kind, var, t)) params t
354 aux ~localize loc context' (add_binders `Lambda body) in
356 match typ with Some typ -> typ | None-> CicNotationPt.Implicit in
358 aux_option ~localize loc context (Some `Type)
359 (Some (add_binders `Pi typ)) in
361 match CicNotationUtil.cic_name_of_name name with
363 CicNotationPt.fail loc
364 "Recursive functions cannot be anonymous"
365 | Cic.Name name -> name
367 (name, decr_idx, cic_type, cic_body))
372 `Inductive -> Cic.Fix (n,inductiveFuns)
374 let coinductiveFuns =
376 (fun (name, _, typ, body) -> name, typ, body)
379 Cic.CoFix (n,coinductiveFuns)
381 let counter = ref ~-1 in
382 let build_term funs (var,_,ty,_) t =
384 Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
387 `AvoidLetInNoAppl n ->
388 let n' = List.length inductiveFuns - n in
390 | `AvoidLetIn (n,l) ->
391 let n' = List.length inductiveFuns - n in
392 Cic.Appl (fix_or_cofix n'::l)
393 | `AddLetIn cic_body ->
394 List.fold_right (build_term inductiveFuns) inductiveFuns
396 | CicNotationPt.Ident _
397 | CicNotationPt.Uri _
398 | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
399 | CicNotationPt.NRef _ -> assert false
400 | CicNotationPt.Ident (name,subst)
401 | CicNotationPt.Uri (name, subst) as ast ->
402 let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
404 if is_uri ast then raise Not_found;(* don't search the env for URIs *)
406 Disambiguate.find_in_context name (string_context_of_context context)
408 if subst <> None then
409 CicNotationPt.fail loc "Explicit substitutions not allowed here";
413 if is_uri ast then (* we have the URI, build the term out of it *)
415 CicUtil.term_of_uri (UriManager.uri_of_string name)
416 with UriManager.IllFormedUri _ ->
417 CicNotationPt.fail loc "Ill formed URI"
420 List.assoc name obj_context
423 Disambiguate.resolve ~mk_choice ~env
424 (DisambiguateTypes.Id name) (`Args [])
428 List.map (fun uri -> UriManager.name_of_uri uri, uri) uris
435 List.assoc s ids_to_uris, aux ~localize loc context term
437 raise (DisambiguateTypes.Invalid_choice (lazy (loc, "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))))
439 | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
443 | Cic.Const (uri, []) ->
444 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
445 let uris = CicUtil.params_of_obj o in
446 Cic.Const (uri, mk_subst uris)
447 | Cic.Var (uri, []) ->
448 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
449 let uris = CicUtil.params_of_obj o in
450 Cic.Var (uri, mk_subst uris)
451 | Cic.MutInd (uri, i, []) ->
453 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
454 let uris = CicUtil.params_of_obj o in
455 Cic.MutInd (uri, i, mk_subst uris)
457 CicEnvironment.Object_not_found _ ->
458 (* if we are here it is probably the case that during the
459 definition of a mutual inductive type we have met an
460 occurrence of the type in one of its constructors.
461 However, the inductive type is not yet in the environment
463 (*here the explicit_named_substituion is assumed to be of length 0 *)
464 Cic.MutInd (uri,i,[]))
465 | Cic.MutConstruct (uri, i, j, []) ->
466 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
467 let uris = CicUtil.params_of_obj o in
468 Cic.MutConstruct (uri, i, j, mk_subst uris)
469 | Cic.Meta _ | Cic.Implicit _ as t ->
471 debug_print (lazy (sprintf
472 "Warning: %s must be instantiated with _[%s] but we do not enforce it"
476 (fun (s, term) -> s ^ " := " ^ CicNotationPtPp.pp_term term)
481 raise (DisambiguateTypes.Invalid_choice (lazy (loc, "??? Can this happen?")))
483 CicEnvironment.CircularDependency _ ->
484 raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
485 | CicNotationPt.Implicit -> Cic.Implicit None
486 | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
487 | CicNotationPt.Num (num, i) ->
488 Disambiguate.resolve ~mk_choice ~env
489 (DisambiguateTypes.Num i) (`Num_arg num)
490 | CicNotationPt.Meta (index, subst) ->
495 | Some term -> Some (aux ~localize loc context term))
498 Cic.Meta (index, cic_subst)
499 | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
500 | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
501 | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
502 | CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
503 | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
504 | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
505 | CicNotationPt.Symbol (symbol, instance) ->
506 Disambiguate.resolve ~mk_choice ~env
507 (DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
508 | CicNotationPt.Variable _
509 | CicNotationPt.Magic _
510 | CicNotationPt.Layout _
511 | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
512 and aux_option ~localize loc context annotation = function
513 | None -> Cic.Implicit annotation
514 | Some term -> aux ~localize loc context term
516 aux ~localize:true HExtlib.dummy_floc context ast
518 let interpretate_path ~context path =
519 let localization_tbl = Cic.CicHash.create 23 in
520 (* here we are throwing away useful localization informations!!! *)
522 interpretate_term ~mk_choice:(fun _ -> assert false) ~create_dummy_ids:true
523 ~context ~env:DisambiguateTypes.Environment.empty ~uri:None ~is_path:true
524 path ~localization_tbl ~obj_context:[], localization_tbl)
526 let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
529 assert (context = []);
530 assert (is_path = false);
531 let interpretate_term ?(obj_context=[]) =
532 interpretate_term ~mk_choice ~localization_tbl ~obj_context in
534 | CicNotationPt.Inductive (params,tyl) ->
535 let uri = match uri with Some uri -> uri | None -> assert false in
539 (fun (context,res) (name,t) ->
542 None -> CicNotationPt.Implicit
544 let name = CicNotationUtil.cic_name_of_name name in
545 name::context,(name, interpretate_term context env None false t)::res
548 context,List.rev res in
550 List.fold_right (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
554 (*here the explicit_named_substituion is assumed to be of length 0 *)
555 (fun (i,res) (name,_,_,_) -> i + 1,(name,Cic.MutInd (uri,i,[]))::res)
559 (fun (name,b,ty,cl) ->
560 let ty' = add_params (interpretate_term context env None false ty) in
566 (interpretate_term ~obj_context ~context ~env ~uri:None
575 Cic.InductiveDefinition (tyl,[],List.length params,[])
576 | CicNotationPt.Record (params,name,ty,fields) ->
577 let uri = match uri with Some uri -> uri | None -> assert false in
581 (fun (context,res) (name,t) ->
584 None -> CicNotationPt.Implicit
586 let name = CicNotationUtil.cic_name_of_name name in
587 name::context,(name, interpretate_term context env None false t)::res
590 context,List.rev res in
593 (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in
594 let ty' = add_params (interpretate_term context env None false ty) in
598 (fun (context,res) (name,ty,_coercion,arity) ->
599 let context' = Cic.Name name :: context in
600 context',(name,interpretate_term context env None false ty)::res
601 ) (context,[]) fields) in
603 (*here the explicit_named_substituion is assumed to be of length 0 *)
604 let mutind = Cic.MutInd (uri,0,[]) in
605 if params = [] then mutind
608 (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
611 (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
613 let con' = add_params con in
614 let tyl = [name,true,ty',["mk_" ^ name,con']] in
615 let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
616 Cic.InductiveDefinition
617 (tyl,[],List.length params,[`Class (`Record field_names)])
618 | CicNotationPt.Theorem (flavour, name, ty, bo) ->
619 let attrs = [`Flavour flavour] in
620 let ty' = interpretate_term [] env None false ty in
621 (match bo,flavour with
623 Cic.Constant (name,None,ty',[],attrs)
624 | Some bo,`Axiom -> assert false
626 Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
628 let bo' = Some (interpretate_term [] env None false bo) in
629 Cic.Constant (name,bo',ty',[],attrs))
632 let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
633 ~is_path ast ~localization_tbl
636 List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context
638 interpretate_term ~mk_choice ~create_dummy_ids ~context ~env ~uri ~is_path
639 ast ~localization_tbl ~obj_context:[]
642 let string_context_of_context =
643 List.map (function None -> None | Some (Cic.Name n,_) -> Some n | Some
644 (Cic.Anonymous,_) -> Some "_");;
646 let disambiguate_term ~context ~metasenv ~subst ~expty
647 ?(initial_ugraph = CicUniv.oblivion_ugraph)
648 ~mk_implicit ~description_of_alias ~mk_choice
649 ~aliases ~universe ~lookup_in_library (text,prefix_len,term)
651 let mk_localization_tbl x = Cic.CicHash.create x in
652 MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
653 ~initial_ugraph ~aliases ~string_context_of_context
654 ~universe ~lookup_in_library ~mk_implicit ~description_of_alias
655 ~uri:None ~pp_thing:CicNotationPp.pp_term
656 ~domain_of_thing:Disambiguate.domain_of_term
657 ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
658 ~refine_thing:refine_term (text,prefix_len,term)
661 ~freshen_thing:CicNotationUtil.freshen_term
662 ~passes:(MultiPassDisambiguator.passes ())
664 let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
665 ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
667 let mk_localization_tbl x = Cic.CicHash.create x in
668 MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[]
669 ~aliases ~universe ~uri ~string_context_of_context
670 ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
671 ~domain_of_thing:Disambiguate.domain_of_obj
672 ~lookup_in_library ~mk_implicit ~description_of_alias
673 ~initial_ugraph:CicUniv.empty_ugraph
674 ~interpretate_thing:(interpretate_obj ~mk_choice)
675 ~refine_thing:refine_obj
678 ~passes:(MultiPassDisambiguator.passes ())
679 ~freshen_thing:CicNotationUtil.freshen_obj
680 (text,prefix_len,obj)