* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
open ProofEngineTypes
let clearbody ~hyp =
_ ->
raise
(Fail
- ("The correctness of hypothesis " ^
+ (lazy ("The correctness of hypothesis " ^
string_of_name n ^
" relies on the body of " ^ hyp)
- )
+ ))
in
entry::context
| Some (_,Cic.Def (_,Some _)) -> assert false
_ ->
raise
(Fail
- ("The correctness of the goal relies on the body of " ^
- hyp))
+ (lazy ("The correctness of the goal relies on the body of " ^
+ hyp)))
in
m,canonical_context',ty
| t -> t
Some (Cic.Name hyp',_) when hyp' = hyp ->
(true, None::context)
| None -> (b, None::context)
- | Some (_,Cic.Def (_,Some _)) -> assert false
| Some (n,C.Decl t)
+ | Some (n,Cic.Def (t,Some _))
| Some (n,C.Def (t,None)) ->
if b then
let _,_ =
with _ ->
raise
(Fail
- ("Hypothesis " ^ string_of_name n ^
- " uses hypothesis " ^ hyp))
+ (lazy ("Hypothesis " ^ string_of_name n ^
+ " uses hypothesis " ^ hyp)))
in
(b, entry::context)
else
) canonical_context (false, [])
in
if not context_changed then
- raise (Fail ("Hypothesis " ^ hyp ^ " does not exist"));
+ raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
CicUniv.empty_ugraph
with _ ->
- raise (Fail ("Hypothesis " ^ hyp ^ " occurs in the goal"))
+ raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
in
m,canonical_context',ty
| t -> t
in
mk_tactic (clear ~hyp)
+(* Warning: this tactic has no effect on the proof term.
+ It just changes the name of an hypothesis in the current sequent *)
+let rename ~from ~to_ =
+ let rename ~from ~to_ (proof, goal) =
+ let module C = Cic in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty =
+ CicUtil.lookup_meta goal metasenv
+ in
+ let metasenv' =
+ List.map
+ (function
+ (m,canonical_context,ty) when m = metano ->
+ let canonical_context' =
+ List.map
+ (function
+ Some (Cic.Name hyp,decl_or_def) when hyp = from ->
+ Some (Cic.Name to_,decl_or_def)
+ | item -> item
+ ) canonical_context
+ in
+ m,canonical_context',ty
+ | t -> t
+ ) metasenv
+ in
+ (curi,metasenv',pbo,pty), [goal]
+ in
+ mk_tactic (rename ~from ~to_)
+
let set_goal n =
ProofEngineTypes.mk_tactic
(fun (proof, goal) ->
if CicUtil.exists_meta n metasenv then
(proof, [n])
else
- raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n)))
+ raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n))))