* For details, see the HELM World-Wide-Web page,
* http://cs.unibo.it/helm/.
*)
+
+(* $Id$ *)
-let rewrite_tac ~direction ~pattern equality =
- let rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
+let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality =
+ let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status
=
let module C = Cic in
let module U = UriManager in
let module PEH = ProofEngineHelpers in
let module PT = PrimitiveTactics in
assert (wanted = None); (* this should be checked syntactically *)
- (*assert (hyps_pat = []); (*CSC: not implemented yet! *)*)
let proof,goal = status in
let curi, metasenv, pbo, pty = proof in
- let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in
+ let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
+ match hyps_pat with
+ he::(_::_ as tl) ->
+ PET.apply_tactic
+ (Tacticals.then_
+ (rewrite_tac ~direction
+ ~pattern:(None,[he],None) equality)
+ (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) equality)
+ ) status
+ | [_] as hyps_pat when concl_pat <> None ->
+ PET.apply_tactic
+ (Tacticals.then_
+ (rewrite_tac ~direction
+ ~pattern:(None,hyps_pat,None) equality)
+ (rewrite_tac ~direction ~pattern:(None,[],concl_pat) equality)
+ ) status
+ | _ ->
let arg,dir2,tac,concl_pat,gty =
match hyps_pat with
- [] -> None,true,PT.exact_tac,concl_pat,gty
+ [] -> None,true,(fun ~term _ -> PT.exact_tac term),concl_pat,gty
| [name,pat] ->
- (*CSC: bug here; I am ignoring the concl_pat *)
let rec find_hyp n =
function
[] -> assert false
| Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
Cic.Rel n, CicSubstitution.lift n ty
- | Some (Cic.Name s,Cic.Def _)::_ -> assert false (*CSC: not implemented yet!*)
+ | Some (Cic.Name s,Cic.Def _)::_ -> assert false (*CSC: not implemented yet! But does this make any sense?*)
| _::tl -> find_hyp (n+1) tl
in
let arg,gty = find_hyp 1 context in
- let last_hyp_name_of_status (proof,goal) =
- let curi, metasenv, pbo, pty = proof in
- let metano,context,gty = CicUtil.lookup_meta goal metasenv in
- match context with
- (Some (Cic.Name s,_))::_ -> s
- | _ -> assert false
- in
+ let dummy = "dummy" in
Some arg,false,
- (fun ~term ->
+ (fun ~term typ ->
Tacticals.seq
~tactics:
- [PT.letin_tac term;
- PET.mk_tactic (fun status ->
- PET.apply_tactic
- (ProofEngineStructuralRules.clearbody
- (last_hyp_name_of_status status)) status);
- PET.mk_tactic (fun status ->
- let hyp = last_hyp_name_of_status status in
- PET.apply_tactic
- (ReductionTactics.simpl_tac
- ~pattern:
- (None,[hyp,Cic.Implicit (Some `Hole)],Cic.Implicit None))
- status);
- ProofEngineStructuralRules.clear name;
- PET.mk_tactic (fun status ->
- let hyp = last_hyp_name_of_status status in
- PET.apply_tactic
- (ProofEngineStructuralRules.rename hyp name) status)
+ [ProofEngineStructuralRules.rename name dummy;
+ PT.letin_tac
+ ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term;
+ ProofEngineStructuralRules.clearbody name;
+ ReductionTactics.change_tac
+ ~pattern:
+ (None,[name,Cic.Implicit (Some `Hole)], None)
+ (ProofEngineTypes.const_lazy_term typ);
+ ProofEngineStructuralRules.clear dummy
]),
- pat,gty
- | _ -> assert false (*CSC: not implemented yet!*)
+ Some pat,gty
+ | _::_ -> assert false
in
let if_right_to_left do_not_change a b =
match direction with
let lifted_conjecture =
metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in
let lifted_pattern =
- Some (fun _ m u -> lifted_t1, m, u),[],CicSubstitution.lift 1 concl_pat
+ let lifted_concl_pat =
+ match concl_pat with
+ | None -> None
+ | Some term -> Some (CicSubstitution.lift 1 term) in
+ Some (fun _ m u -> lifted_t1, m, u),[],lifted_concl_pat
in
let subst,metasenv',ugraph,_,selected_terms_with_context =
ProofEngineHelpers.select
let pred = C.Lambda (fresh_name, ty, abstr_gty) in
(* The argument is either a meta if we are rewriting in the conclusion
or the hypothesis if we are rewriting in an hypothesis *)
- let metasenv',arg =
+ let metasenv',arg,newtyp =
match arg with
None ->
let gty' = CicSubstitution.subst t2 abstr_gty in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,gty')::metasenv' in
- metasenv', C.Meta (fresh_meta,irl)
+ metasenv', C.Meta (fresh_meta,irl), Cic.Rel (-1) (* dummy term, never used *)
| Some arg ->
- metasenv,arg
+ let gty' = CicSubstitution.subst t1 abstr_gty in
+ metasenv,arg,gty'
in
let exact_proof =
C.Appl [eq_ind ; ty ; t2 ; pred ; arg ; t1 ;equality]
in
let (proof',goals) =
PET.apply_tactic
- (tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal)
+ (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty),goal)
in
let goals =
goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
in
(proof',goals)
in
- ProofEngineTypes.mk_tactic (rewrite_tac ~direction ~pattern equality)
+ ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality)
let rewrite_simpl_tac ~direction ~pattern equality =
ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~direction ~pattern equality)
;;
-let replace_tac ~pattern ~with_what =
- let replace_tac ~pattern:(wanted,hyps_pat,concl_pat) ~with_what status =
+let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
+ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status =
+ let _wanted, hyps_pat, concl_pat = pattern in
let (proof, goal) = status in
let module C = Cic in
let module U = UriManager in
ty_of_with_what ty_of_t_in_context u in
if b then
let concl_pat_for_t = ProofEngineHelpers.pattern_of ~term:ty [t] in
- let pattern_for_t = None,[],concl_pat_for_t in
+ let pattern_for_t = None,[],Some concl_pat_for_t in
t_in_context,pattern_for_t
else
raise
let rec aux n whats status =
match whats with
[] -> ProofEngineTypes.apply_tactic T.id_tac status
- | (what,pattern)::tl ->
+ | (what,lazy_pattern)::tl ->
let what = CicSubstitution.lift n what in
let with_what = CicSubstitution.lift n with_what in
let ty_of_with_what = CicSubstitution.lift n ty_of_with_what in
~continuations:[
T.then_
~start:(
- rewrite_tac ~direction:`LeftToRight ~pattern (C.Rel 1))
+ rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1))
~continuation:(
T.then_
~start:(