2 Declaration of Cic.name * Cic.term
3 | Definition of Cic.name * Cic.term
6 type metasenv = (int * Cic.term) list;;
8 type named_context = binder_type list;;
10 type sequent = named_context * Cic.term;;
13 ref (None : (UriManager.uri * metasenv * Cic.term * Cic.term) option)
15 (*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *)
16 (* Note: the sequent is redundant: it can be computed from the type of the *)
17 (* metavariable and its context in the proof. We keep it just for efficiency *)
18 (* because computing the context of a term may be quite expensive. *)
19 let goal = ref (None : (int * sequent) option);;
21 exception NotImplemented
23 let cic_context_of_named_context =
26 Declaration (_,t) -> Cic.Decl t
27 | Definition (_,t) -> Cic.Def t
31 let refine_meta_with_brand_new_metasenv meta term newmetasenv =
35 | Some (uri,_,bo,ty) -> uri,bo,ty
38 ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
40 let bo' = subst_in bo in
41 let metasenv' = List.remove_assoc meta newmetasenv in
42 proof := Some (uri,metasenv',bo',ty)
45 let refine_meta meta term newmetasenv =
46 let (uri,metasenv,bo,ty) =
49 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
52 ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
54 let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
55 let metasenv'' = List.map (function i,ty -> i,(subst_in ty)) metasenv' in
56 let bo' = subst_in bo in
57 proof := Some (uri,metasenv'',bo',ty)
60 (* Returns the first meta whose number is above the *)
61 (* number of the higher meta. *)
66 | Some (_,metasenv,_,_) -> metasenv
72 | None,(n,_)::tl -> aux (Some n,tl)
73 | Some m,(n,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
75 1 + aux (None,metasenv)
78 (* metas_in_term term *)
79 (* Returns the ordered list of the metas that occur in [term]. *)
80 (* Duplicates are removed. The implementation is not very efficient. *)
81 let metas_in_term term =
90 | C.Cast (te,ty) -> (aux te) @ (aux ty)
91 | C.Prod (_,s,t) -> (aux s) @ (aux t)
92 | C.Lambda (_,s,t) -> (aux s) @ (aux t)
93 | C.LetIn (_,s,t) -> (aux s) @ (aux t)
94 | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
98 | C.MutConstruct _ -> []
99 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
100 (aux outt) @ (aux t) @
101 (List.fold_left (fun i t -> i @ (aux t)) [] pl)
103 List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
105 List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
107 let metas = aux term in
108 let rec elim_duplicates =
112 he::(elim_duplicates (List.filter (function el -> he <> el) tl))
114 elim_duplicates metas
117 (* perforate context term ty *)
118 (* replaces the term [term] in the proof with a new metavariable whose type *)
119 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
120 (* could be easily computed; so the only reasons to have it as an argument *)
121 (* are efficiency reasons. *)
122 let perforate context term ty =
123 let module C = Cic in
124 let newmeta = new_meta () in
127 | Some (uri,metasenv,bo,gty) ->
128 (* We push the new meta at the end of the list for pretty-printing *)
129 (* purposes: in this way metas are ordered. *)
130 let metasenv' = metasenv@[newmeta,ty] in
131 let bo' = ProofEngineReduction.replace term (C.Meta newmeta) bo in
132 (* It may be possible that some metavariables occurred only in *)
133 (* the term we are perforating and they now occurs no more. We *)
134 (* get rid of them, collecting the really useful metavariables *)
136 let newmetas = metas_in_term bo' in
138 List.filter (function (n,_) -> List.mem n newmetas) metasenv'
140 proof := Some (uri,metasenv'',bo',gty) ;
141 goal := Some (newmeta,(context,ty)) ;
145 (************************************************************)
146 (* Some easy tactics. *)
147 (************************************************************)
149 exception Fail of string;;
152 let module C = Cic in
153 let module R = CicReduction in
157 | Some (_,metasenv,_,_) -> metasenv
159 let (metano,context,ty) =
162 | Some (metano,(context,ty)) -> metano,context,ty
164 let newmeta = new_meta () in
165 let rec collect_context =
167 C.Cast (te,_) -> collect_context te
169 let (ctx,ty,bo) = collect_context t in
173 (*CSC: generatore di nomi? Chiedere il nome? *)
174 | C.Anonimous -> C.Name "fresh_name"
176 ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
178 let (ctx,ty,bo) = collect_context t in
179 ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo))
180 | _ as t -> [], t, (C.Meta newmeta)
182 let revcontext',ty',bo' = collect_context ty in
183 let context'' = (List.rev revcontext') @ context in
184 refine_meta metano bo' [newmeta,ty'] ;
185 goal := Some (newmeta,(context'',ty'))
188 (* The term bo must be closed in the current context *)
190 let module T = CicTypeChecker in
191 let module R = CicReduction in
195 | Some (_,metasenv,_,_) -> metasenv
197 let (metano,context,ty) =
200 | Some (metano,(context,ty)) ->
201 assert (ty = List.assoc metano metasenv) ;
202 (* Invariant: context is the actual context of the meta in the proof *)
205 let context = cic_context_of_named_context context in
206 if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
208 refine_meta metano bo [] ;
212 raise (Fail "The type of the provided term is not the one expected.")
215 (* Auxiliary function for apply: given a type (a backbone), it returns its *)
216 (* head, a META environment in which there is a META for each hypothesis and *)
217 (* the indexes of the first and last new METAs introduced. *)
218 let new_metasenv_for_apply ty =
219 let module C = Cic in
220 let module S = CicSubstitution in
221 let rec aux newmeta =
223 C.Cast (he,_) -> aux newmeta he
225 let (res,newmetasenv,lastmeta) =
226 aux (newmeta + 1) (S.subst (C.Meta newmeta) t)
228 res,(newmeta,s)::newmetasenv,lastmeta
231 let newmeta = new_meta () in
232 (* WARNING: here we are using the invariant that above the most *)
233 (* recente new_meta() there are no used metas. *)
234 let (res,newmetasenv,lastmeta) = aux newmeta ty in
235 res,newmetasenv,newmeta,lastmeta
238 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
239 let classify_metas newmeta in_subst_domain apply_subst =
241 (fun (old_uninst,new_uninst) (i,ty) ->
242 if in_subst_domain i then
243 old_uninst,new_uninst
245 let ty' = apply_subst ty in
247 ((i,ty')::old_uninst),new_uninst
249 old_uninst,((i,ty')::new_uninst)
253 (* The term bo must be closed in the current context *)
255 let module T = CicTypeChecker in
256 let module R = CicReduction in
257 let module C = Cic in
261 | Some (_,metasenv,_,_) -> metasenv
263 let (metano,context,ty) =
266 | Some (metano,(context,ty)) ->
267 assert (ty = List.assoc metano metasenv) ;
268 (* Invariant: context is the actual context of the meta in the proof *)
271 let ciccontext = cic_context_of_named_context context in
272 let termty = CicTypeChecker.type_of_aux' metasenv ciccontext term in
273 (* newmeta is the lowest index of the new metas introduced *)
274 let (consthead,newmetas,newmeta,_) = new_metasenv_for_apply termty in
275 let newmetasenv = newmetas@metasenv in
276 let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in
277 let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
278 let apply_subst = CicUnification.apply_subst subst in
279 let old_uninstantiatedmetas,new_uninstantiatedmetas =
280 classify_metas newmeta in_subst_domain apply_subst newmetasenv
283 if List.length newmetas = 0 then
288 (List.map (function (i,_) -> C.Meta i) newmetas)
290 Cic.Appl (term::arguments)
292 refine_meta_with_brand_new_metasenv metano bo'
293 (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
294 match new_uninstantiatedmetas with
296 | (i,ty)::_ -> goal := Some (i,(context,ty))
299 let eta_expand metasenv ciccontext t arg =
300 let module T = CicTypeChecker in
301 let module S = CicSubstitution in
302 let module C = Cic in
305 t' when t' = S.lift n arg -> C.Rel (1 + n)
306 | C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1)
310 | C.Implicit as t -> t
311 | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
312 | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
313 | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
314 | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
315 | C.Appl l -> C.Appl (List.map (aux n) l)
316 | C.Const _ as t -> t
317 | C.Abst _ -> assert false
319 | C.MutConstruct _ as t -> t
320 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
321 C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
324 let tylen = List.length fl in
327 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
330 C.Fix (i, substitutedfl)
332 let tylen = List.length fl in
335 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
338 C.CoFix (i, substitutedfl)
341 T.type_of_aux' metasenv ciccontext arg
343 (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
346 exception NotAnInductiveTypeToEliminate;;
347 exception NotTheRightEliminatorShape;;
348 exception NoHypothesesFound;;
351 let module T = CicTypeChecker in
352 let module U = UriManager in
353 let module R = CicReduction in
354 let module C = Cic in
358 | Some (curi,metasenv,_,_) -> curi,metasenv
360 let (metano,context,ty) =
363 | Some (metano,(context,ty)) ->
364 assert (ty = List.assoc metano metasenv) ;
365 (* Invariant: context is the actual context of the meta in the proof *)
368 let ciccontext = cic_context_of_named_context context in
369 let termty = T.type_of_aux' metasenv ciccontext term in
370 let uri,cookingno,typeno,args =
372 C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
373 | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
374 (uri,cookingno,typeno,args)
375 | _ -> raise NotAnInductiveTypeToEliminate
378 let buri = U.buri_of_uri uri in
380 match CicEnvironment.get_cooked_obj uri cookingno with
381 C.InductiveDefinition (tys,_,_) ->
382 let (name,_,_,_) = List.nth tys typeno in
387 match T.type_of_aux' metasenv ciccontext ty with
388 C.Sort C.Prop -> "_ind"
389 | C.Sort C.Set -> "_rec"
390 | C.Sort C.Type -> "_rect"
393 U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
395 let eliminator_cookingno =
396 UriManager.relative_depth curi eliminator_uri 0
398 let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
400 T.type_of_aux' [] [] eliminator_ref
402 let (econclusion,newmetas,newmeta,lastmeta) =
403 new_metasenv_for_apply ety
405 (* Here we assume that we have only one inductive hypothesis to *)
406 (* eliminate and that it is the last hypothesis of the theorem. *)
407 (* A better approach would be fingering the hypotheses in some *)
409 let meta_of_corpse = Cic.Meta (lastmeta - 1) in
410 let newmetasenv = newmetas @ metasenv in
411 prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ;
414 CicUnification.fo_unif newmetasenv ciccontext term meta_of_corpse
416 let ueconclusion = CicUnification.apply_subst subst1 econclusion in
417 prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ;
419 (* The conclusion of our elimination principle is *)
420 (* (?i farg1 ... fargn) *)
421 (* The conclusion of our goal is ty. So, we can *)
422 (* eta-expand ty w.r.t. farg1 .... fargn to get *)
423 (* a new ty equal to (P farg1 ... fargn). Now *)
424 (* ?i can be instantiated with P and we are ready *)
425 (* to refine the term. *)
427 match ueconclusion with
428 C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
429 | _ -> raise NotTheRightEliminatorShape
431 let ty' = CicUnification.apply_subst subst1 ty in
432 let eta_expanded_ty =
433 List.fold_left (eta_expand metasenv ciccontext) ty' fargs
435 prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ;
437 (*CSC: passo newmetasenv, ma alcune variabili sono gia' state sostituite
438 da subst1!!!! Dovrei rimuoverle o sono innocue?*)
439 CicUnification.fo_unif
440 newmetasenv ciccontext ueconclusion eta_expanded_ty
442 prerr_endline "Dopo la seconda unificazione" ; flush stdout ;
443 prerr_endline "unwind"; flush stderr;
444 let in_subst_domain i =
445 let eq_to_i = function (j,_) -> i=j in
446 List.exists eq_to_i subst1 ||
447 List.exists eq_to_i subst2
449 (* When unwinding the META that corresponds to the elimination *)
450 (* predicate (which is emeta), we must also perform one-step *)
451 (* beta-reduction. *)
454 let t' = CicUnification.apply_subst subst1 t in
455 CicUnification.apply_subst_reducing
456 subst2 (Some (emeta,List.length fargs)) t'
459 List.map (function (i,ty) -> i, apply_subst ty) newmetasenv
461 let old_uninstantiatedmetas,new_uninstantiatedmetas =
462 classify_metas newmeta in_subst_domain apply_subst newmetasenv
466 (List.map (function (i,_) -> C.Meta i) newmetas)
468 let bo' = Cic.Appl (eliminator_ref::arguments) in
469 prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
470 List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ;
471 refine_meta_with_brand_new_metasenv metano bo'
472 (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
473 match new_uninstantiatedmetas with
475 | (i,ty)::_ -> goal := Some (i,(context,ty))
478 let elim_intros term =
483 let reduction_tactic reduction_function term =
484 let curi,metasenv,pbo,pty =
487 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
489 let (metano,context,ty) =
492 | Some (metano,(context,ty)) -> metano,context,ty
494 let term' = reduction_function term in
495 (* We don't know if [term] is a subterm of [ty] or a subterm of *)
496 (* the type of one metavariable. So we replace it everywhere. *)
497 (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
498 (*CSC: che si guadagni nulla in fatto di efficienza. *)
499 let replace = ProofEngineReduction.replace ~what:term ~with_what:term' in
500 let ty' = replace ty in
504 Definition (n,t) -> Definition (n,replace t)
505 | Declaration (n,t) -> Declaration (n,replace t)
511 (n,_) when n = metano -> (metano,ty')
515 proof := Some (curi,metasenv',pbo,pty) ;
516 goal := Some (metano,(context',ty'))
519 let reduction_tactic_in_scratch reduction_function ty term =
523 | Some (_,metasenv,_,_) -> metasenv
528 | Some (_,(context,_)) -> context
530 let term' = reduction_function term in
531 ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
534 let whd = reduction_tactic CicReduction.whd;;
535 let reduce = reduction_tactic ProofEngineReduction.reduce;;
536 let simpl = reduction_tactic ProofEngineReduction.simpl;;
538 let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd;;
539 let reduce_in_scratch =
540 reduction_tactic_in_scratch ProofEngineReduction.reduce;;
541 let simpl_in_scratch =
542 reduction_tactic_in_scratch ProofEngineReduction.simpl;;
544 (* It is just the opposite of whd. The code should probably be merged. *)
546 let curi,metasenv,pbo,pty =
549 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
551 let (metano,context,ty) =
554 | Some (metano,(context,ty)) -> metano,context,ty
556 let term' = CicReduction.whd term in
557 (* We don't know if [term] is a subterm of [ty] or a subterm of *)
558 (* the type of one metavariable. So we replace it everywhere. *)
559 (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
560 (*CSC: che si guadagni nulla in fatto di efficienza. *)
561 let replace = ProofEngineReduction.replace ~what:term' ~with_what:term in
562 let ty' = replace ty in
566 Declaration (n,t) -> Declaration (n,replace t)
567 | Definition (n,t) -> Definition (n,replace t)
573 (n,_) when n = metano -> (metano,ty')
577 proof := Some (curi,metasenv',pbo,pty) ;
578 goal := Some (metano,(context',ty'))
582 let module C = Cic in
583 let curi,metasenv,pbo,pty =
586 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
588 let (metano,context,ty) =
591 | Some (metano,(context,ty)) -> metano,context,ty
593 let newmeta1 = new_meta () in
594 let newmeta2 = newmeta1 + 1 in
595 let newmeta1ty = CicSubstitution.lift 1 ty in
598 [C.Lambda (C.Name "dummy_for_cut",term,C.Meta newmeta1) ;
601 prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ;
602 refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty];
605 (newmeta1,((Declaration (C.Name "dummy_for_cut", term))::context,
610 let module C = Cic in
611 let curi,metasenv,pbo,pty =
614 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
616 let (metano,context,ty) =
619 | Some (metano,(context,ty)) -> metano,context,ty
621 let ciccontext = cic_context_of_named_context context in
622 let _ = CicTypeChecker.type_of_aux' metasenv ciccontext term in
623 let newmeta = new_meta () in
624 let newmetaty = CicSubstitution.lift 1 ty in
625 let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta newmeta) in
626 refine_meta metano bo' [newmeta,newmetaty];
630 ((Definition (C.Name "dummy_for_letin", term))::context, newmetaty))
633 exception NotConvertible;;
635 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *)
636 (*CSC: while [goal_input] can have a richer context (because of binders) *)
637 (*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
638 (*CSC: Is that evident? Is that right? Or should it be changed? *)
639 let change ~goal_input ~input =
640 let curi,metasenv,pbo,pty =
643 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
645 let (metano,context,ty) =
648 | Some (metano,(context,ty)) -> metano,context,ty
650 let ciccontext = cic_context_of_named_context context in
651 (* are_convertible works only on well-typed terms *)
652 ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
653 if CicReduction.are_convertible goal_input input then
655 let ty' = ProofEngineReduction.replace goal_input input ty in
659 (n,_) when n = metano -> (metano,ty')
663 proof := Some (curi,metasenv',pbo,pty) ;
664 goal := Some (metano,(context,ty'))