1 (* Copyright (C) 2000, 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://cs.unibo.it/helm/.
27 ref (None : (UriManager.uri * Cic.metasenv * Cic.term * Cic.term) option)
29 let goal = ref (None : int option);;
31 (*CSC: commento vecchio *)
32 (* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv *)
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: Attenzione! Ora questa funzione applica anche [subst_in] a *)
42 (*CSC: [newmetasenv]. *)
43 let subst_meta_and_metasenv_in_current_proof meta subst_in newmetasenv =
47 | Some (uri,_,bo,ty) -> uri,bo,ty
49 let bo' = subst_in bo in
52 (fun metasenv_entry i ->
53 match metasenv_entry with
54 (m,canonical_context,ty) when m <> meta ->
55 let canonical_context' =
59 | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
60 | Some (i,Cic.Def t) -> Some (i,Cic.Def (subst_in t))
63 (m,canonical_context',subst_in ty)::i
67 proof := Some (uri,metasenv',bo',ty) ;
71 let subst_meta_in_current_proof meta term newmetasenv =
72 let (uri,metasenv,bo,ty) =
75 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
77 let subst_in = CicUnification.apply_subst [meta,term] in
79 newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
83 (function i,canonical_context,ty ->
84 let canonical_context' =
87 Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
88 | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s))
92 i,canonical_context',(subst_in ty)
95 let bo' = subst_in bo in
96 proof := Some (uri,metasenv'',bo',ty) ;
100 (* Returns the first meta whose number is above the *)
101 (* number of the higher meta. *)
106 | Some (_,metasenv,_,_) -> metasenv
112 | None,(n,_,_)::tl -> aux (Some n,tl)
113 | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
115 1 + aux (None,metasenv)
118 (* metas_in_term term *)
119 (* Returns the ordered list of the metas that occur in [term]. *)
120 (* Duplicates are removed. The implementation is not very efficient. *)
121 let metas_in_term term =
122 let module C = Cic in
127 | C.Meta (n,_) -> [n]
130 | C.Cast (te,ty) -> (aux te) @ (aux ty)
131 | C.Prod (_,s,t) -> (aux s) @ (aux t)
132 | C.Lambda (_,s,t) -> (aux s) @ (aux t)
133 | C.LetIn (_,s,t) -> (aux s) @ (aux t)
134 | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
138 | C.MutConstruct _ -> []
139 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
140 (aux outt) @ (aux t) @
141 (List.fold_left (fun i t -> i @ (aux t)) [] pl)
143 List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
145 List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
147 let metas = aux term in
148 let rec elim_duplicates =
152 he::(elim_duplicates (List.filter (function el -> he <> el) tl))
154 elim_duplicates metas
157 (* identity_relocation_list_for_metavariable i canonical_context *)
158 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
159 (* where n = List.length [canonical_context] *)
160 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
161 let identity_relocation_list_for_metavariable canonical_context =
162 let canonical_context_length = List.length canonical_context in
166 | (n,None::tl) -> None::(aux ((n+1),tl))
167 | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
169 aux (1,canonical_context)
172 (* perforate context term ty *)
173 (* replaces the term [term] in the proof with a new metavariable whose type *)
174 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
175 (* could be easily computed; so the only reasons to have it as an argument *)
176 (* are efficiency reasons. *)
177 let perforate context term ty =
178 let module C = Cic in
179 let newmeta = new_meta () in
182 | Some (uri,metasenv,bo,gty) ->
183 (* We push the new meta at the end of the list for pretty-printing *)
184 (* purposes: in this way metas are ordered. *)
185 let metasenv' = metasenv@[newmeta,context,ty] in
186 let irl = identity_relocation_list_for_metavariable context in
187 (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
189 ProofEngineReduction.replace (==) term (C.Meta (newmeta,irl)) bo
191 (* It may be possible that some metavariables occurred only in *)
192 (* the term we are perforating and they now occurs no more. We *)
193 (* get rid of them, collecting the really useful metavariables *)
195 (*CSC: Bug: una meta potrebbe non comparire in bo', ma comparire nel tipo *)
196 (*CSC: di una metavariabile che compare in bo'!!!!!!! *)
197 let newmetas = metas_in_term bo' in
199 List.filter (function (n,_,_) -> List.mem n newmetas) metasenv'
201 proof := Some (uri,metasenv'',bo',gty) ;
205 (************************************************************)
206 (* Some easy tactics. *)
207 (************************************************************)
209 exception Fail of string;;
211 (*CSC: generatore di nomi? Chiedere il nome? *)
213 let next_fresh_index = ref 0
216 incr next_fresh_index ;
217 "fresh_name" ^ string_of_int !next_fresh_index
220 (* lambda_abstract newmeta ty *)
221 (* returns a triple [bo],[context],[ty'] where *)
222 (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
223 (* and [bo] = Lambda/LetIn [context].(Meta [newmeta]) *)
224 (* So, lambda_abstract is the core of the implementation of *)
225 (* the Intros tactic. *)
226 let lambda_abstract context newmeta ty =
227 let module C = Cic in
228 let rec collect_context context =
230 C.Cast (te,_) -> collect_context context te
235 (*CSC: generatore di nomi? Chiedere il nome? *)
236 | C.Anonimous -> C.Name (fresh_name ())
238 let (context',ty,bo) =
239 collect_context ((Some (n',(C.Decl s)))::context) t
241 (context',ty,C.Lambda(n',s,bo))
243 let (context',ty,bo) =
244 collect_context ((Some (n,(C.Def s)))::context) t
246 (context',ty,C.LetIn(n,s,bo))
248 let irl = identity_relocation_list_for_metavariable context in
249 context, t, (C.Meta (newmeta,irl))
251 collect_context context ty
255 let module C = Cic in
256 let module R = CicReduction in
260 | Some (_,metasenv,_,_) -> metasenv
262 let metano,context,ty =
265 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
267 let newmeta = new_meta () in
268 let (context',ty',bo') = lambda_abstract context newmeta ty in
269 let _ = subst_meta_in_current_proof metano bo' [newmeta,context',ty'] in
273 (* The term bo must be closed in the current context *)
275 let module T = CicTypeChecker in
276 let module R = CicReduction in
280 | Some (_,metasenv,_,_) -> metasenv
282 let metano,context,ty =
285 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
287 if R.are_convertible context (T.type_of_aux' metasenv context bo) ty then
289 let metasenv' = subst_meta_in_current_proof metano bo [] in
293 | (n,_,_)::_ -> Some n
296 raise (Fail "The type of the provided term is not the one expected.")
299 (*CSC: The call to the Intros tactic is embedded inside the code of the *)
300 (*CSC: Elim tactic. Do we already need tacticals? *)
301 (* Auxiliary function for apply: given a type (a backbone), it returns its *)
302 (* head, a META environment in which there is new a META for each hypothesis,*)
303 (* a list of arguments for the new applications and the indexes of the first *)
304 (* and last new METAs introduced. The nth argument in the list of arguments *)
305 (* is the nth new META lambda-abstracted as much as possible. Hence, this *)
306 (* functions already provides the behaviour of Intros on the new goals. *)
307 let new_metasenv_for_apply_intros context ty =
308 let module C = Cic in
309 let module S = CicSubstitution in
310 let rec aux newmeta =
312 C.Cast (he,_) -> aux newmeta he
313 | C.Prod (name,s,t) ->
314 let newcontext,ty',newargument = lambda_abstract context newmeta s in
315 let (res,newmetasenv,arguments,lastmeta) =
316 aux (newmeta + 1) (S.subst newargument t)
318 res,(newmeta,newcontext,ty')::newmetasenv,newargument::arguments,lastmeta
319 | t -> t,[],[],newmeta
321 let newmeta = new_meta () in
322 (* WARNING: here we are using the invariant that above the most *)
323 (* recente new_meta() there are no used metas. *)
324 let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
325 res,newmetasenv,arguments,newmeta,lastmeta
328 (* Auxiliary function for apply: given a type (a backbone), it returns its *)
329 (* head, a META environment in which there is new a META for each hypothesis,*)
330 (* a list of arguments for the new applications and the indexes of the first *)
331 (* and last new METAs introduced. The nth argument in the list of arguments *)
332 (* is just the nth new META. *)
333 let new_metasenv_for_apply context ty =
334 let module C = Cic in
335 let module S = CicSubstitution in
336 let rec aux newmeta =
338 C.Cast (he,_) -> aux newmeta he
339 | C.Prod (name,s,t) ->
340 let irl = identity_relocation_list_for_metavariable context in
341 let newargument = C.Meta (newmeta,irl) in
342 let (res,newmetasenv,arguments,lastmeta) =
343 aux (newmeta + 1) (S.subst newargument t)
345 res,(newmeta,context,s)::newmetasenv,newargument::arguments,lastmeta
346 | t -> t,[],[],newmeta
348 let newmeta = new_meta () in
349 (* WARNING: here we are using the invariant that above the most *)
350 (* recente new_meta() there are no used metas. *)
351 let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
352 res,newmetasenv,arguments,newmeta,lastmeta
356 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
357 let classify_metas newmeta in_subst_domain subst_in metasenv =
359 (fun (i,canonical_context,ty) (old_uninst,new_uninst) ->
360 if in_subst_domain i then
361 old_uninst,new_uninst
363 let ty' = subst_in canonical_context ty in
364 let canonical_context' =
366 (fun entry canonical_context' ->
369 Some (n,Cic.Decl s) ->
370 Some (n,Cic.Decl (subst_in canonical_context' s))
371 | Some (n,Cic.Def s) ->
372 Some (n,Cic.Def (subst_in canonical_context' s))
375 entry'::canonical_context'
376 ) canonical_context []
379 ((i,canonical_context',ty')::old_uninst),new_uninst
381 old_uninst,((i,canonical_context',ty')::new_uninst)
385 (* The term bo must be closed in the current context *)
387 let module T = CicTypeChecker in
388 let module R = CicReduction in
389 let module C = Cic in
393 | Some (_,metasenv,_,_) -> metasenv
395 let metano,context,ty =
399 List.find (function (m,_,_) -> m=metano) metasenv
401 let termty = CicTypeChecker.type_of_aux' metasenv context term in
402 (* newmeta is the lowest index of the new metas introduced *)
403 let (consthead,newmetas,arguments,newmeta,_) =
404 new_metasenv_for_apply context termty
406 let newmetasenv = newmetas@metasenv in
407 let subst,newmetasenv' =
408 CicUnification.fo_unif newmetasenv context consthead ty
410 let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
411 let apply_subst = CicUnification.apply_subst subst in
412 let old_uninstantiatedmetas,new_uninstantiatedmetas =
413 (* subst_in doesn't need the context. Hence the underscore. *)
414 let subst_in _ = CicUnification.apply_subst subst in
415 classify_metas newmeta in_subst_domain subst_in newmetasenv'
418 if List.length newmetas = 0 then
421 let arguments' = List.map apply_subst arguments in
422 Cic.Appl (term::arguments')
424 let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
426 let subst_in = CicUnification.apply_subst ((metano,bo')::subst) in
427 subst_meta_and_metasenv_in_current_proof metano subst_in
430 match newmetasenv''' with
432 | (i,_,_)::_ -> goal := Some i
435 let eta_expand metasenv context t arg =
436 let module T = CicTypeChecker in
437 let module S = CicSubstitution in
438 let module C = Cic in
441 t' when t' = S.lift n arg -> C.Rel (1 + n)
442 | C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1)
446 | C.Implicit as t -> t
447 | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
448 | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
449 | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
450 | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
451 | C.Appl l -> C.Appl (List.map (aux n) l)
452 | C.Const _ as t -> t
453 | C.Abst _ -> assert false
455 | C.MutConstruct _ as t -> t
456 | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
457 C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
460 let tylen = List.length fl in
463 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
466 C.Fix (i, substitutedfl)
468 let tylen = List.length fl in
471 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
474 C.CoFix (i, substitutedfl)
477 T.type_of_aux' metasenv context arg
479 (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
482 exception NotAnInductiveTypeToEliminate;;
483 exception NotTheRightEliminatorShape;;
484 exception NoHypothesesFound;;
486 let elim_intros_simpl term =
487 let module T = CicTypeChecker in
488 let module U = UriManager in
489 let module R = CicReduction in
490 let module C = Cic in
494 | Some (curi,metasenv,_,_) -> curi,metasenv
496 let metano,context,ty =
500 List.find (function (m,_,_) -> m=metano) metasenv
502 let termty = T.type_of_aux' metasenv context term in
503 let uri,cookingno,typeno,args =
505 C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
506 | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
507 (uri,cookingno,typeno,args)
508 | _ -> raise NotAnInductiveTypeToEliminate
511 let buri = U.buri_of_uri uri in
513 match CicEnvironment.get_cooked_obj uri cookingno with
514 C.InductiveDefinition (tys,_,_) ->
515 let (name,_,_,_) = List.nth tys typeno in
520 match T.type_of_aux' metasenv context ty with
521 C.Sort C.Prop -> "_ind"
522 | C.Sort C.Set -> "_rec"
523 | C.Sort C.Type -> "_rect"
526 U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
528 let eliminator_cookingno =
529 UriManager.relative_depth curi eliminator_uri 0
531 let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
533 T.type_of_aux' [] [] eliminator_ref
535 let (econclusion,newmetas,arguments,newmeta,lastmeta) =
537 new_metasenv_for_apply context ety
539 new_metasenv_for_apply_intros context ety
541 (* Here we assume that we have only one inductive hypothesis to *)
542 (* eliminate and that it is the last hypothesis of the theorem. *)
543 (* A better approach would be fingering the hypotheses in some *)
546 let (_,canonical_context,_) =
547 List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas
550 identity_relocation_list_for_metavariable canonical_context
552 Cic.Meta (lastmeta - 1, irl)
554 let newmetasenv = newmetas @ metasenv in
555 let subst1,newmetasenv' =
556 CicUnification.fo_unif newmetasenv context term meta_of_corpse
558 let ueconclusion = CicUnification.apply_subst subst1 econclusion in
559 (* The conclusion of our elimination principle is *)
560 (* (?i farg1 ... fargn) *)
561 (* The conclusion of our goal is ty. So, we can *)
562 (* eta-expand ty w.r.t. farg1 .... fargn to get *)
563 (* a new ty equal to (P farg1 ... fargn). Now *)
564 (* ?i can be instantiated with P and we are ready *)
565 (* to refine the term. *)
567 match ueconclusion with
568 (*CSC: Code to be used for Apply
569 C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs
570 | C.Meta (emeta,_) -> emeta,[]
572 (*CSC: Code to be used for ApplyIntros *)
573 C.Appl (he::fargs) ->
576 C.Meta (emeta,_) -> emeta
577 | C.Lambda (_,_,t) -> find_head t
578 | C.LetIn (_,_,t) -> find_head t
579 | _ ->raise NotTheRightEliminatorShape
583 | _ -> raise NotTheRightEliminatorShape
585 let ty' = CicUnification.apply_subst subst1 ty in
586 let eta_expanded_ty =
587 (*CSC: newmetasenv' era metasenv ??????????? *)
588 List.fold_left (eta_expand newmetasenv' context) ty' fargs
590 let subst2,newmetasenv'' =
591 (*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite
592 da subst1!!!! Dovrei rimuoverle o sono innocue?*)
593 CicUnification.fo_unif
594 newmetasenv' context ueconclusion eta_expanded_ty
596 let in_subst_domain i =
597 let eq_to_i = function (j,_) -> i=j in
598 List.exists eq_to_i subst1 ||
599 List.exists eq_to_i subst2
601 (*CSC: codice per l'elim
602 (* When unwinding the META that corresponds to the elimination *)
603 (* predicate (which is emeta), we must also perform one-step *)
604 (* beta-reduction. apply_subst doesn't need the context. Hence *)
605 (* the underscore. *)
606 let apply_subst _ t =
607 let t' = CicUnification.apply_subst subst1 t in
608 CicUnification.apply_subst_reducing
609 subst2 (Some (emeta,List.length fargs)) t'
612 (*CSC: codice per l'elim_intros_simpl. Non effettua semplificazione. *)
613 let apply_subst context t =
614 let t' = CicUnification.apply_subst (subst1@subst2) t in
615 ProofEngineReduction.simpl context t'
618 let old_uninstantiatedmetas,new_uninstantiatedmetas =
619 classify_metas newmeta in_subst_domain apply_subst
622 let arguments' = List.map (apply_subst context) arguments in
623 let bo' = Cic.Appl (eliminator_ref::arguments') in
625 new_uninstantiatedmetas@old_uninstantiatedmetas
627 let newmetasenv'''' =
628 (* When unwinding the META that corresponds to the *)
629 (* elimination predicate (which is emeta), we must *)
630 (* also perform one-step beta-reduction. *)
631 (* The only difference w.r.t. apply_subst is that *)
632 (* we also substitute metano with bo'. *)
633 (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *)
635 (*CSC: codice per l'elim
637 let t' = CicUnification.apply_subst subst1 t in
638 CicUnification.apply_subst_reducing
639 ((metano,bo')::subst2)
640 (Some (emeta,List.length fargs)) t'
643 (*CSC: codice per l'elim_intros_simpl *)
645 CicUnification.apply_subst
646 ((metano,bo')::(subst1@subst2)) t
649 subst_meta_and_metasenv_in_current_proof metano
650 apply_subst' newmetasenv'''
652 match newmetasenv'''' with
654 | (i,_,_)::_ -> goal := Some i
657 let reduction_tactic reduction_function term =
658 let curi,metasenv,pbo,pty =
661 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
663 let metano,context,ty =
666 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
668 (* We don't know if [term] is a subterm of [ty] or a subterm of *)
669 (* the type of one metavariable. So we replace it everywhere. *)
670 (*CSC: Il vero problema e' che non sapendo dove sia il term non *)
671 (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *)
672 (*CSC: e' meglio prima cercare il termine e scoprirne il *)
673 (*CSC: contesto, poi ridurre e infine rimpiazzare. *)
674 let replace context where=
675 (*CSC: Per il momento se la riduzione fallisce significa solamente che *)
676 (*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *)
677 (*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
679 let term' = reduction_function context term in
680 ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
685 let ty' = replace context ty in
688 (fun entry context ->
690 Some (name,Cic.Def t) ->
691 (Some (name,Cic.Def (replace context t)))::context
692 | Some (name,Cic.Decl t) ->
693 (Some (name,Cic.Decl (replace context t)))::context
694 | None -> None::context
700 (n,_,_) when n = metano -> (metano,context',ty')
704 proof := Some (curi,metasenv',pbo,pty) ;
708 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
709 let reduction_tactic_in_scratch reduction_function term ty =
713 | Some (_,metasenv,_,_) -> metasenv
715 let metano,context,_ =
718 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
720 let term' = reduction_function context term in
721 ProofEngineReduction.replace
722 ~equality:(==) ~what:term ~with_what:term' ~where:ty
725 let whd = reduction_tactic CicReduction.whd;;
726 let reduce = reduction_tactic ProofEngineReduction.reduce;;
727 let simpl = reduction_tactic ProofEngineReduction.simpl;;
729 let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd;;
730 let reduce_in_scratch =
731 reduction_tactic_in_scratch ProofEngineReduction.reduce;;
732 let simpl_in_scratch =
733 reduction_tactic_in_scratch ProofEngineReduction.simpl;;
735 (* It is just the opposite of whd. The code should probably be merged. *)
737 let curi,metasenv,pbo,pty =
740 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
742 let metano,context,ty =
745 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
747 let term' = CicReduction.whd context term in
748 (* We don't know if [term] is a subterm of [ty] or a subterm of *)
749 (* the type of one metavariable. So we replace it everywhere. *)
750 (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
751 (*CSC: che si guadagni nulla in fatto di efficienza. *)
753 ProofEngineReduction.replace
754 ~equality:(ProofEngineReduction.syntactic_equality)
755 ~what:term' ~with_what:term
757 let ty' = replace ty in
761 Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
762 | Some (n,Cic.Def t) -> Some (n,Cic.Def (replace t))
769 (n,_,_) when n = metano -> (metano,context',ty')
773 proof := Some (curi,metasenv',pbo,pty) ;
778 let module C = Cic in
779 let curi,metasenv,pbo,pty =
782 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
784 let metano,context,ty =
787 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
789 let newmeta1 = new_meta () in
790 let newmeta2 = newmeta1 + 1 in
791 let context_for_newmeta1 =
792 (Some (C.Name "dummy_for_cut",C.Decl term))::context in
794 identity_relocation_list_for_metavariable context_for_newmeta1 in
795 let irl2 = identity_relocation_list_for_metavariable context in
796 let newmeta1ty = CicSubstitution.lift 1 ty in
799 [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ;
800 C.Meta (newmeta2,irl2)]
803 subst_meta_in_current_proof metano bo'
804 [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
806 goal := Some newmeta1
810 let module C = Cic in
811 let curi,metasenv,pbo,pty =
814 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
816 let metano,context,ty =
819 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
821 let _ = CicTypeChecker.type_of_aux' metasenv context term in
822 let newmeta = new_meta () in
823 let context_for_newmeta =
824 (Some (C.Name "dummy_for_letin",C.Def term))::context in
826 identity_relocation_list_for_metavariable context_for_newmeta in
827 let newmetaty = CicSubstitution.lift 1 ty in
828 let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta (newmeta,irl)) in
829 let _ = subst_meta_in_current_proof metano bo' [newmeta,context_for_newmeta,newmetaty] in
833 exception NotConvertible;;
835 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *)
836 (*CSC: while [goal_input] can have a richer context (because of binders) *)
837 (*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
838 (*CSC: Is that evident? Is that right? Or should it be changed? *)
839 let change ~goal_input ~input =
840 let curi,metasenv,pbo,pty =
843 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
845 let metano,context,ty =
848 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
850 (* are_convertible works only on well-typed terms *)
851 ignore (CicTypeChecker.type_of_aux' metasenv context input) ;
852 if CicReduction.are_convertible context goal_input input then
855 ProofEngineReduction.replace
856 ~equality:(==) ~what:goal_input ~with_what:input
858 let ty' = replace ty in
862 Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t))
863 | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
870 (n,_,_) when n = metano -> (metano,context',ty')
874 proof := Some (curi,metasenv',pbo,pty) ;
882 let module C = Cic in
885 | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
886 | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
887 let curi,metasenv,pbo,pty =
890 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
895 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
905 (m,canonical_context,ty) when m = metano ->
906 let canonical_context' =
908 (fun entry context ->
910 t when t == hyp_to_clear_body ->
913 CicTypeChecker.type_of_aux' metasenv context term
915 Some (n_to_clear_body, Cic.Decl ty)
917 cleared_entry::context
918 | None -> None::context
920 | Some (n,C.Def t) ->
923 CicTypeChecker.type_of_aux' metasenv context t
928 ("The correctness of hypothesis " ^
930 " relies on the body of " ^
931 string_of_name n_to_clear_body)
935 ) canonical_context []
939 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
944 ("The correctness of the goal relies on the body of " ^
945 string_of_name n_to_clear_body))
947 m,canonical_context',ty
951 proof := Some (curi,metasenv',pbo,pty)
954 let clear hyp_to_clear =
955 let module C = Cic in
956 match hyp_to_clear with
958 | Some (n_to_clear, _) ->
959 let curi,metasenv,pbo,pty =
962 | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
964 let metano,context,ty =
967 | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
977 (m,canonical_context,ty) when m = metano ->
978 let canonical_context' =
980 (fun entry context ->
982 t when t == hyp_to_clear -> None::context
983 | None -> None::context
985 | Some (n,C.Def t) ->
988 CicTypeChecker.type_of_aux' metasenv context t
995 " uses hypothesis " ^
996 string_of_name n_to_clear)
1000 ) canonical_context []
1004 CicTypeChecker.type_of_aux' metasenv canonical_context' ty
1009 ("Hypothesis " ^ string_of_name n_to_clear ^
1010 " occurs in the goal"))
1012 m,canonical_context',ty
1016 proof := Some (curi,metasenv',pbo,pty)