let rewrite_simpl_tac ~term ~status =
- Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:ReductionTactics.simpl_tac ~status
+ Tacticals.then_ ~start:(rewrite_tac ~term)
+ ~continuation:
+ (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
+ ~status
;;
(******************** THE FOURIER TACTIC ***********************)
let elim_simpl_intros_tac ~term =
Tacticals.then_ ~start:(elim_tac ~term)
~continuation:
- (Tacticals.then_ ~start:ReductionTactics.simpl_tac
+ (Tacticals.then_
+ ~start:(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
~continuation:(intros_tac ~name:"FOO"))
;;
incr next_fresh_index ;
"fresh_name" ^ string_of_int !next_fresh_index
-let reduction_tactic reduction_function term =
- let curi,metasenv,pbo,pty =
- match !proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,context,ty =
- match !goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
- (* We don't know if [term] is a subterm of [ty] or a subterm of *)
- (* the type of one metavariable. So we replace it everywhere. *)
- (*CSC: Il vero problema e' che non sapendo dove sia il term non *)
- (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *)
- (*CSC: e' meglio prima cercare il termine e scoprirne il *)
- (*CSC: contesto, poi ridurre e infine rimpiazzare. *)
- let replace context where=
-(*CSC: Per il momento se la riduzione fallisce significa solamente che *)
-(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *)
-(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
- try
- let term' = reduction_function context term in
- ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
- ~where:where
- with
- _ -> where
- in
- let ty' = replace context ty in
- let context' =
- List.fold_right
- (fun entry context ->
- match entry with
- Some (name,Cic.Def t) ->
- (Some (name,Cic.Def (replace context t)))::context
- | Some (name,Cic.Decl t) ->
- (Some (name,Cic.Decl (replace context t)))::context
- | None -> None::context
- ) context []
- in
- let metasenv' =
- List.map
- (function
- (n,_,_) when n = metano -> (metano,context',ty')
- | _ as t -> t
- ) metasenv
- in
- proof := Some (curi,metasenv',pbo,pty) ;
- goal := Some metano
-
(* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
let reduction_tactic_in_scratch reduction_function term ty =
let metasenv =
let term' = reduction_function context term in
ProofEngineReduction.replace
~equality:(==) ~what:term ~with_what:term' ~where:ty
-
-let whd = reduction_tactic CicReduction.whd
-let reduce = reduction_tactic ProofEngineReduction.reduce
-let simpl = reduction_tactic ProofEngineReduction.simpl
+;;
let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd
let reduce_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.reduce
(* reduction tactics *)
+let whd term =
+ apply_tactic
+ (ReductionTactics.whd_tac ~also_in_hypotheses:true ~term:(Some term))
+let reduce term =
+ apply_tactic
+ (ReductionTactics.reduce_tac ~also_in_hypotheses:true ~term:(Some term))
+let simpl term =
+ apply_tactic
+ (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~term:(Some term))
+
let fold term =
apply_tactic (ReductionTactics.fold_tac ~also_in_hypotheses:true ~term)
* http://cs.unibo.it/helm/.
*)
+(*
let reduction_tac ~reduction ~status:(proof,goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
in
(curi,new_metasenv,pbo,pty), [metano]
;;
+*)
+
+(* The default of term is the thesis of the goal to be prooved *)
+let reduction_tac ~also_in_hypotheses ~reduction ~term ~status:(proof,goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let term =
+ match term with None -> ty | Some t -> t
+ in
+ (* We don't know if [term] is a subterm of [ty] or a subterm of *)
+ (* the type of one metavariable. So we replace it everywhere. *)
+ (*CSC: Il vero problema e' che non sapendo dove sia il term non *)
+ (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *)
+ (*CSC: e' meglio prima cercare il termine e scoprirne il *)
+ (*CSC: contesto, poi ridurre e infine rimpiazzare. *)
+ let replace context where=
+(*CSC: Per il momento se la riduzione fallisce significa solamente che *)
+(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *)
+(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
+ try
+ let term' = reduction context term in
+ ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
+ ~where:where
+ with
+ _ -> where
+ in
+ let ty' = replace context ty in
+ let context' =
+ if also_in_hypotheses then
+ List.fold_right
+ (fun entry context ->
+ match entry with
+ Some (name,Cic.Def t) ->
+ (Some (name,Cic.Def (replace context t)))::context
+ | Some (name,Cic.Decl t) ->
+ (Some (name,Cic.Decl (replace context t)))::context
+ | None -> None::context
+ ) context []
+ else
+ context
+ in
+ let metasenv' =
+ List.map
+ (function
+ (n,_,_) when n = metano -> (metano,context',ty')
+ | _ as t -> t
+ ) metasenv
+ in
+ (curi,metasenv',pbo,pty), [metano]
+;;
let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;;
let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;;
* http://cs.unibo.it/helm/.
*)
-val simpl_tac: ProofEngineTypes.tactic
-val reduce_tac: ProofEngineTypes.tactic
-val whd_tac: ProofEngineTypes.tactic
+(* The default of term is the thesis of the goal to be prooved *)
+val simpl_tac:
+ also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic
+val reduce_tac:
+ also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic
+val whd_tac:
+ also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic
+
val fold_tac:
also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic
projects / helm.git / commitdiff