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 (* refine_meta_with_brand_new_metasenv meta term apply_subst_replacing *)
33 (* This (heavy) function must be called when a tactic can instantiate old *)
34 (* metavariables (i.e. existential variables). It substitues the metasenv *)
35 (* of the proof with the result of removing [meta] from the domain of *)
36 (* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
37 (* in the current proof. Finally it applies [apply_subst_replacing] to *)
39 (*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
40 (*CSC: ci ripasso sopra apply_subst!!! *)
41 (*CSC: Inoltre, potrebbe essere questa funzione ad applicare apply_subst a *)
42 (*CSC: newmetasenv!!! *)
43 let refine_meta_with_brand_new_metasenv meta term apply_subst_replacing
49 | Some (uri,_,bo,ty) -> uri,bo,ty
52 ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
54 let bo' = apply_subst_replacing (subst_in bo) in
55 let metasenv' = List.remove_assoc meta newmetasenv in
56 proof := Some (uri,metasenv',bo',ty)
59 let refine_meta meta term newmetasenv =
60 let (uri,metasenv,bo,ty) =
63 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
66 ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
68 let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
69 let metasenv'' = List.map (function i,ty -> i,(subst_in ty)) metasenv' in
70 let bo' = subst_in bo in
71 proof := Some (uri,metasenv'',bo',ty)
74 (* Returns the first meta whose number is above the *)
75 (* number of the higher meta. *)
80 | Some (_,metasenv,_,_) -> metasenv
86 | None,(n,_)::tl -> aux (Some n,tl)
87 | Some m,(n,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
89 1 + aux (None,metasenv)
92 (* metas_in_term term *)
93 (* Returns the ordered list of the metas that occur in [term]. *)
94 (* Duplicates are removed. The implementation is not very efficient. *)
95 let metas_in_term term =
104 | C.Cast (te,ty) -> (aux te) @ (aux ty)
105 | C.Prod (_,s,t) -> (aux s) @ (aux t)
106 | C.Lambda (_,s,t) -> (aux s) @ (aux t)
107 | C.LetIn (_,s,t) -> (aux s) @ (aux t)
108 | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
112 | C.MutConstruct _ -> []
113 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
114 (aux outt) @ (aux t) @
115 (List.fold_left (fun i t -> i @ (aux t)) [] pl)
117 List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
119 List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
121 let metas = aux term in
122 let rec elim_duplicates =
126 he::(elim_duplicates (List.filter (function el -> he <> el) tl))
128 elim_duplicates metas
131 (* perforate context term ty *)
132 (* replaces the term [term] in the proof with a new metavariable whose type *)
133 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
134 (* could be easily computed; so the only reasons to have it as an argument *)
135 (* are efficiency reasons. *)
136 let perforate context term ty =
137 let module C = Cic in
138 let newmeta = new_meta () in
141 | Some (uri,metasenv,bo,gty) ->
142 (* We push the new meta at the end of the list for pretty-printing *)
143 (* purposes: in this way metas are ordered. *)
144 let metasenv' = metasenv@[newmeta,ty] in
145 let bo' = ProofEngineReduction.replace term (C.Meta newmeta) bo in
146 (* It may be possible that some metavariables occurred only in *)
147 (* the term we are perforating and they now occurs no more. We *)
148 (* get rid of them, collecting the really useful metavariables *)
150 let newmetas = metas_in_term bo' in
152 List.filter (function (n,_) -> List.mem n newmetas) metasenv'
154 proof := Some (uri,metasenv'',bo',gty) ;
155 goal := Some (newmeta,(context,ty)) ;
159 (************************************************************)
160 (* Some easy tactics. *)
161 (************************************************************)
163 exception Fail of string;;
166 let module C = Cic in
167 let module R = CicReduction in
171 | Some (_,metasenv,_,_) -> metasenv
173 let (metano,context,ty) =
176 | Some (metano,(context,ty)) -> metano,context,ty
178 let newmeta = new_meta () in
179 let rec collect_context =
181 C.Cast (te,_) -> collect_context te
183 let (ctx,ty,bo) = collect_context t in
187 (*CSC: generatore di nomi? Chiedere il nome? *)
188 | C.Anonimous -> C.Name "fresh_name"
190 ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
192 let (ctx,ty,bo) = collect_context t in
193 ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo))
194 | _ as t -> [], t, (C.Meta newmeta)
196 let revcontext',ty',bo' = collect_context ty in
197 let context'' = (List.rev revcontext') @ context in
198 refine_meta metano bo' [newmeta,ty'] ;
199 goal := Some (newmeta,(context'',ty'))
202 (* The term bo must be closed in the current context *)
204 let module T = CicTypeChecker in
205 let module R = CicReduction in
209 | Some (_,metasenv,_,_) -> metasenv
211 let (metano,context,ty) =
214 | Some (metano,(context,ty)) ->
215 assert (ty = List.assoc metano metasenv) ;
216 (* Invariant: context is the actual context of the meta in the proof *)
219 let context = cic_context_of_named_context context in
220 if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
222 refine_meta metano bo [] ;
226 raise (Fail "The type of the provided term is not the one expected.")
229 (* Auxiliary function for apply: given a type (a backbone), it returns its *)
230 (* head, a META environment in which there is a META for each hypothesis and *)
231 (* the indexes of the first and last new METAs introduced. *)
232 let new_metasenv_for_apply ty =
233 let module C = Cic in
234 let module S = CicSubstitution in
235 let rec aux newmeta =
237 C.Cast (he,_) -> aux newmeta he
239 let (res,newmetasenv,lastmeta) =
240 aux (newmeta + 1) (S.subst (C.Meta newmeta) t)
242 res,(newmeta,s)::newmetasenv,lastmeta
245 let newmeta = new_meta () in
246 (* WARNING: here we are using the invariant that above the most *)
247 (* recente new_meta() there are no used metas. *)
248 let (res,newmetasenv,lastmeta) = aux newmeta ty in
249 res,newmetasenv,newmeta,lastmeta
252 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
253 let classify_metas newmeta in_subst_domain apply_subst metasenv =
255 (fun (i,ty) (old_uninst,new_uninst) ->
256 if in_subst_domain i then
257 old_uninst,new_uninst
259 let ty' = apply_subst ty in
261 ((i,ty')::old_uninst),new_uninst
263 old_uninst,((i,ty')::new_uninst)
267 (* The term bo must be closed in the current context *)
269 let module T = CicTypeChecker in
270 let module R = CicReduction in
271 let module C = Cic in
275 | Some (_,metasenv,_,_) -> metasenv
277 let (metano,context,ty) =
280 | Some (metano,(context,ty)) ->
281 assert (ty = List.assoc metano metasenv) ;
282 (* Invariant: context is the actual context of the meta in the proof *)
285 let ciccontext = cic_context_of_named_context context in
286 let termty = CicTypeChecker.type_of_aux' metasenv ciccontext term in
287 (* newmeta is the lowest index of the new metas introduced *)
288 let (consthead,newmetas,newmeta,_) = new_metasenv_for_apply termty in
289 let newmetasenv = newmetas@metasenv in
290 let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in
291 let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
292 let apply_subst = CicUnification.apply_subst subst in
293 (*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
294 let apply_subst_replacing t =
297 ProofEngineReduction.replace
298 ~what:(Cic.Meta i) ~with_what:bo ~where:t)
301 let old_uninstantiatedmetas,new_uninstantiatedmetas =
302 classify_metas newmeta in_subst_domain apply_subst newmetasenv
305 if List.length newmetas = 0 then
310 (List.map (function (i,_) -> C.Meta i) newmetas)
312 Cic.Appl (term::arguments)
314 refine_meta_with_brand_new_metasenv metano bo' apply_subst_replacing
315 (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
316 prerr_endline "QUI4" ; flush stderr ; (
317 match new_uninstantiatedmetas with
319 | (i,ty)::_ -> goal := Some (i,(context,ty))
321 List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (new_uninstantiatedmetas@old_uninstantiatedmetas)
322 ; prerr_endline "FATTO" ; flush stderr ;
323 List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (match !proof with Some (_,m,_,_) -> m) ;
324 prerr_endline ("PROVA: " ^ CicPp.ppterm (match !proof with Some (_,_,b,_) -> b))
325 ; prerr_endline "FATTO2" ; flush stderr
328 let eta_expand metasenv ciccontext t arg =
329 let module T = CicTypeChecker in
330 let module S = CicSubstitution in
331 let module C = Cic in
334 t' when t' = S.lift n arg -> C.Rel (1 + n)
335 | C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1)
339 | C.Implicit as t -> t
340 | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
341 | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
342 | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
343 | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
344 | C.Appl l -> C.Appl (List.map (aux n) l)
345 | C.Const _ as t -> t
346 | C.Abst _ -> assert false
348 | C.MutConstruct _ as t -> t
349 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
350 C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
353 let tylen = List.length fl in
356 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
359 C.Fix (i, substitutedfl)
361 let tylen = List.length fl in
364 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
367 C.CoFix (i, substitutedfl)
370 T.type_of_aux' metasenv ciccontext arg
372 (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
375 exception NotAnInductiveTypeToEliminate;;
376 exception NotTheRightEliminatorShape;;
377 exception NoHypothesesFound;;
380 let module T = CicTypeChecker in
381 let module U = UriManager in
382 let module R = CicReduction in
383 let module C = Cic in
387 | Some (curi,metasenv,_,_) -> curi,metasenv
389 let (metano,context,ty) =
392 | Some (metano,(context,ty)) ->
393 assert (ty = List.assoc metano metasenv) ;
394 (* Invariant: context is the actual context of the meta in the proof *)
397 let ciccontext = cic_context_of_named_context context in
398 let termty = T.type_of_aux' metasenv ciccontext term in
399 let uri,cookingno,typeno,args =
401 C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
402 | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
403 (uri,cookingno,typeno,args)
404 | _ -> raise NotAnInductiveTypeToEliminate
407 let buri = U.buri_of_uri uri in
409 match CicEnvironment.get_cooked_obj uri cookingno with
410 C.InductiveDefinition (tys,_,_) ->
411 let (name,_,_,_) = List.nth tys typeno in
416 match T.type_of_aux' metasenv ciccontext ty with
417 C.Sort C.Prop -> "_ind"
418 | C.Sort C.Set -> "_rec"
419 | C.Sort C.Type -> "_rect"
422 U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
424 let eliminator_cookingno =
425 UriManager.relative_depth curi eliminator_uri 0
427 let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
429 T.type_of_aux' [] [] eliminator_ref
431 let (econclusion,newmetas,newmeta,lastmeta) =
432 new_metasenv_for_apply ety
434 (* Here we assume that we have only one inductive hypothesis to *)
435 (* eliminate and that it is the last hypothesis of the theorem. *)
436 (* A better approach would be fingering the hypotheses in some *)
438 let meta_of_corpse = Cic.Meta (lastmeta - 1) in
439 let newmetasenv = newmetas @ metasenv in
440 prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ;
443 CicUnification.fo_unif newmetasenv ciccontext term meta_of_corpse
445 let ueconclusion = CicUnification.apply_subst subst1 econclusion in
446 prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ;
448 (* The conclusion of our elimination principle is *)
449 (* (?i farg1 ... fargn) *)
450 (* The conclusion of our goal is ty. So, we can *)
451 (* eta-expand ty w.r.t. farg1 .... fargn to get *)
452 (* a new ty equal to (P farg1 ... fargn). Now *)
453 (* ?i can be instantiated with P and we are ready *)
454 (* to refine the term. *)
456 match ueconclusion with
457 C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
458 | _ -> raise NotTheRightEliminatorShape
460 let ty' = CicUnification.apply_subst subst1 ty in
461 let eta_expanded_ty =
462 List.fold_left (eta_expand metasenv ciccontext) ty' fargs
464 prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ;
466 (*CSC: passo newmetasenv, ma alcune variabili sono gia' state sostituite
467 da subst1!!!! Dovrei rimuoverle o sono innocue?*)
468 CicUnification.fo_unif
469 newmetasenv ciccontext ueconclusion eta_expanded_ty
471 prerr_endline "Dopo la seconda unificazione" ; flush stdout ;
472 prerr_endline "unwind"; flush stderr;
473 let in_subst_domain i =
474 let eq_to_i = function (j,_) -> i=j in
475 List.exists eq_to_i subst1 ||
476 List.exists eq_to_i subst2
478 (* When unwinding the META that corresponds to the elimination *)
479 (* predicate (which is emeta), we must also perform one-step *)
480 (* beta-reduction. *)
482 let t' = CicUnification.apply_subst subst1 t in
483 CicUnification.apply_subst_reducing
484 subst2 (Some (emeta,List.length fargs)) t'
486 (*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
487 let apply_subst_replacing t =
491 ProofEngineReduction.replace
492 ~what:(Cic.Meta i) ~with_what:bo ~where:t)
497 ProofEngineReduction.replace
498 ~what:(Cic.Meta i) ~with_what:bo ~where:t)
502 List.map (function (i,ty) -> i, apply_subst ty) newmetasenv
504 let old_uninstantiatedmetas,new_uninstantiatedmetas =
505 classify_metas newmeta in_subst_domain apply_subst newmetasenv
509 (List.map (function (i,_) -> C.Meta i) newmetas)
511 let bo' = Cic.Appl (eliminator_ref::arguments) in
512 prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
513 List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ;
514 refine_meta_with_brand_new_metasenv metano bo'
515 apply_subst_replacing
516 (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
517 match new_uninstantiatedmetas with
519 | (i,ty)::_ -> goal := Some (i,(context,ty))
522 let elim_intros term =
527 let reduction_tactic reduction_function term =
528 let curi,metasenv,pbo,pty =
531 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
533 let (metano,context,ty) =
536 | Some (metano,(context,ty)) -> metano,context,ty
538 let term' = reduction_function term in
539 (* We don't know if [term] is a subterm of [ty] or a subterm of *)
540 (* the type of one metavariable. So we replace it everywhere. *)
541 (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
542 (*CSC: che si guadagni nulla in fatto di efficienza. *)
543 let replace = ProofEngineReduction.replace ~what:term ~with_what:term' in
544 let ty' = replace ty in
548 Definition (n,t) -> Definition (n,replace t)
549 | Declaration (n,t) -> Declaration (n,replace t)
555 (n,_) when n = metano -> (metano,ty')
559 proof := Some (curi,metasenv',pbo,pty) ;
560 goal := Some (metano,(context',ty'))
563 let reduction_tactic_in_scratch reduction_function ty term =
567 | Some (_,metasenv,_,_) -> metasenv
572 | Some (_,(context,_)) -> context
574 let term' = reduction_function term in
575 ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
578 let whd = reduction_tactic CicReduction.whd;;
579 let reduce = reduction_tactic ProofEngineReduction.reduce;;
580 let simpl = reduction_tactic ProofEngineReduction.simpl;;
582 let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd;;
583 let reduce_in_scratch =
584 reduction_tactic_in_scratch ProofEngineReduction.reduce;;
585 let simpl_in_scratch =
586 reduction_tactic_in_scratch ProofEngineReduction.simpl;;
588 (* It is just the opposite of whd. The code should probably be merged. *)
590 let curi,metasenv,pbo,pty =
593 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
595 let (metano,context,ty) =
598 | Some (metano,(context,ty)) -> metano,context,ty
600 let term' = CicReduction.whd term in
601 (* We don't know if [term] is a subterm of [ty] or a subterm of *)
602 (* the type of one metavariable. So we replace it everywhere. *)
603 (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
604 (*CSC: che si guadagni nulla in fatto di efficienza. *)
605 let replace = ProofEngineReduction.replace ~what:term' ~with_what:term in
606 let ty' = replace ty in
610 Declaration (n,t) -> Declaration (n,replace t)
611 | Definition (n,t) -> Definition (n,replace t)
617 (n,_) when n = metano -> (metano,ty')
621 proof := Some (curi,metasenv',pbo,pty) ;
622 goal := Some (metano,(context',ty'))
626 let module C = Cic in
627 let curi,metasenv,pbo,pty =
630 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
632 let (metano,context,ty) =
635 | Some (metano,(context,ty)) -> metano,context,ty
637 let newmeta1 = new_meta () in
638 let newmeta2 = newmeta1 + 1 in
639 let newmeta1ty = CicSubstitution.lift 1 ty in
642 [C.Lambda (C.Name "dummy_for_cut",term,C.Meta newmeta1) ;
645 prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ;
646 refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty];
649 (newmeta1,((Declaration (C.Name "dummy_for_cut", term))::context,
654 let module C = Cic in
655 let curi,metasenv,pbo,pty =
658 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
660 let (metano,context,ty) =
663 | Some (metano,(context,ty)) -> metano,context,ty
665 let ciccontext = cic_context_of_named_context context in
666 let _ = CicTypeChecker.type_of_aux' metasenv ciccontext term in
667 let newmeta = new_meta () in
668 let newmetaty = CicSubstitution.lift 1 ty in
669 let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta newmeta) in
670 refine_meta metano bo' [newmeta,newmetaty];
674 ((Definition (C.Name "dummy_for_letin", term))::context, newmetaty))
677 exception NotConvertible;;
679 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *)
680 (*CSC: while [goal_input] can have a richer context (because of binders) *)
681 (*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
682 (*CSC: Is that evident? Is that right? Or should it be changed? *)
683 let change ~goal_input ~input =
684 let curi,metasenv,pbo,pty =
687 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
689 let (metano,context,ty) =
692 | Some (metano,(context,ty)) -> metano,context,ty
694 let ciccontext = cic_context_of_named_context context in
695 (* are_convertible works only on well-typed terms *)
696 ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
697 if CicReduction.are_convertible goal_input input then
699 let ty' = ProofEngineReduction.replace goal_input input ty in
703 (n,_) when n = metano -> (metano,ty')
707 proof := Some (curi,metasenv',pbo,pty) ;
708 goal := Some (metano,(context,ty'))