(* $Id$ *)
-open ProofEngineTypes
+module PET = ProofEngineTypes
+module C = Cic
let clearbody ~hyp =
- let clearbody ~hyp (proof, goal) =
- let module C = Cic in
- let curi,metasenv,pbo,pty = proof in
+ let clearbody (proof, goal) =
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,_,_ = CicUtil.lookup_meta goal metasenv in
let string_of_name =
function
with
_ ->
raise
- (Fail
+ (PET.Fail
(lazy ("The correctness of hypothesis " ^
string_of_name n ^
" relies on the body of " ^ hyp)
with
_ ->
raise
- (Fail
+ (PET.Fail
(lazy ("The correctness of the goal relies on the body of " ^
hyp)))
in
| t -> t
) metasenv
in
- (curi,metasenv',pbo,pty), [goal]
+ (curi,metasenv',_subst,pbo,pty, attrs), [goal]
in
- mk_tactic (clearbody ~hyp)
+ PET.mk_tactic clearbody
-let clear ~hyp =
- let clear ~hyp (proof, goal) =
- let module C = Cic in
- let curi,metasenv,pbo,pty = proof in
+let clear_one ~hyp =
+ let clear_one (proof, goal) =
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty =
CicUtil.lookup_meta goal metasenv
in
CicUniv.empty_ugraph
with _ ->
raise
- (Fail
+ (PET.Fail
(lazy ("Hypothesis " ^ string_of_name n ^
" uses hypothesis " ^ hyp)))
in
) canonical_context (false, [])
in
if not context_changed then
- raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
+ raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist")));
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
CicUniv.empty_ugraph
with _ ->
- raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
+ raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
in
m,canonical_context',ty
| t -> t
) metasenv
in
- (curi,metasenv',pbo,pty), [goal]
+ (curi,metasenv',_subst,pbo,pty, attrs), [goal]
in
- mk_tactic (clear ~hyp)
+ PET.mk_tactic clear_one
+
+let clear ~hyps =
+ let clear status =
+ let aux status hyp =
+ match PET.apply_tactic (clear_one ~hyp) status with
+ | proof, [g] -> proof, g
+ | _ -> raise (PET.Fail (lazy "clear: internal error"))
+ in
+ let proof, g = List.fold_left aux status hyps in
+ proof, [g]
+ in
+ PET.mk_tactic clear
(* 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) ->
- let (_, metasenv, _, _) = proof in
- if CicUtil.exists_meta n metasenv then
- (proof, [n])
- else
- raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n))))
+let rename ~froms ~tos =
+ let rename (proof, goal) =
+ let error = "rename: lists of different length" in
+ let assocs =
+ try List.combine froms tos
+ with Invalid_argument _ -> raise (PET.Fail (lazy error))
+ in
+ let curi, metasenv, _subst, pbo, pty, attrs = proof in
+ let metano, _, _ = CicUtil.lookup_meta goal metasenv in
+ let rename_map = function
+ | Some (Cic.Name hyp, decl_or_def) as entry ->
+ begin try Some (Cic.Name (List.assoc hyp assocs), decl_or_def)
+ with Not_found -> entry end
+ | entry -> entry
+ in
+ let map = function
+ | m, canonical_context, ty when m = metano ->
+ let canonical_context = List.map rename_map canonical_context in
+ m, canonical_context, ty
+ | conjecture -> conjecture
+ in
+ let metasenv = List.map map metasenv in
+ (curi, metasenv, _subst, pbo, pty, attrs), [goal]
+ in
+ PET.mk_tactic rename