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)