module TC = CicTypeChecker
module LO = LibraryObjects
module DTI = DoubleTypeInference
+module HEL = HExtlib
-let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality =
- let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
- =
+let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
+ let _rewrite_tac status =
assert (wanted = None); (* this should be checked syntactically *)
let proof,goal = status in
let curi, metasenv, pbo, pty = proof in
match hyps_pat with
he::(_::_ as tl) ->
PET.apply_tactic
- (Tacticals.then_
+ (T.then_
(rewrite_tac ~direction
~pattern:(None,[he],None) equality)
(rewrite_tac ~direction ~pattern:(None,tl,concl_pat)
) status
| [_] as hyps_pat when concl_pat <> None ->
PET.apply_tactic
- (Tacticals.then_
+ (T.then_
(rewrite_tac ~direction
~pattern:(None,hyps_pat,None) equality)
(rewrite_tac ~direction ~pattern:(None,[],concl_pat)
let dummy = "dummy" in
Some arg,false,
(fun ~term typ ->
- Tacticals.seq
+ T.seq
~tactics:
- [ProofEngineStructuralRules.rename name dummy;
+ [PESR.rename [name] [dummy];
P.letin_tac
~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term;
- ProofEngineStructuralRules.clearbody name;
+ PESR.clearbody name;
ReductionTactics.change_tac
~pattern:
(None,[name,Cic.Implicit (Some `Hole)], None)
(ProofEngineTypes.const_lazy_term typ);
- ProofEngineStructuralRules.clear [dummy]
+ PESR.clear [dummy]
]),
Some pat,gty
| _::_ -> assert false
CicTypeChecker.type_of_aux' metasenv context equality
CicUniv.empty_ugraph in
let (ty_eq,metasenv',arguments,fresh_meta) =
- ProofEngineHelpers.saturate_term
+ TermUtil.saturate_term
(ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in
let equality =
if List.length arguments = 0 then
TC.TypeCheckerFailure _ ->
let msg = lazy "rewrite: nothing to rewrite" in
raise (PET.Fail msg)
- in
- ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality)
-
-
-let rewrite_simpl_tac ~direction ~pattern equality =
- let rewrite_simpl_tac ~direction ~pattern equality status =
- ProofEngineTypes.apply_tactic
- (Tacticals.then_
- ~start:(rewrite_tac ~direction ~pattern equality)
+ in
+ PET.mk_tactic _rewrite_tac
+
+let rewrite_tac ~direction ~pattern equality names =
+ let _, hyps_pat, _ = pattern in
+ let froms = List.map fst hyps_pat in
+ let start = rewrite_tac ~direction ~pattern equality in
+ let continuation = PESR.rename ~froms ~tos:names in
+ if names = [] then start else T.then_ ~start ~continuation
+
+let rewrite_simpl_tac ~direction ~pattern equality names =
+ T.then_
+ ~start:(rewrite_tac ~direction ~pattern equality names)
~continuation:
(ReductionTactics.simpl_tac
- ~pattern:(ProofEngineTypes.conclusion_pattern None)))
- status
- in
- ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~direction ~pattern equality)
-;;
+ ~pattern:(ProofEngineTypes.conclusion_pattern None))
+
let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status =
~continuations:[
T.then_
~start:(
- rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1))
+ rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1) [])
~continuation:(
T.then_
~start:(
with (Failure "hd") -> assert false
in
ProofEngineTypes.apply_tactic
- (ProofEngineStructuralRules.clear ~hyps) status))
+ (PESR.clear ~hyps) status))
~continuation:(aux_tac (n + 1) tl));
T.id_tac])
status
let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
let n = List.length new_context - List.length context in
let equality = if n > 0 then S.lift n equality else equality in
- PET.apply_tactic (rewrite_tac ~direction ~pattern equality) status
+ PET.apply_tactic (rewrite_tac ~direction ~pattern equality []) status
in
PET.mk_tactic lift_rewrite_tac
Some (rewrite (None, [(s, hole)], None))
| _ -> None
in
- let rew_hips = PEH.list_rev_map_filter (map hyp) context in
+ let rew_hips = HEL.list_rev_map_filter (map hyp) context in
let rew_concl = rewrite (None, [], Some hole) in
let clear = PESR.clear ~hyps:[hyp; var] in
let tactics = List.rev_append (rew_concl :: rew_hips) [clear] in
let (proof, goal) = status in
let (_, metasenv, _, _) = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
- let tactics = PEH.list_rev_map_filter map context in
+ let tactics = HEL.list_rev_map_filter map context in
PET.apply_tactic (T.seq ~tactics) status
in
PET.mk_tactic subst_tac