* http://cs.unibo.it/helm/.
*)
+open ProofEngineTypes
+
(*
-let reduction_tac ~reduction ~status:(proof,goal) =
+let reduction_tac ~reduction (proof,goal) =
let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let new_ty = reduction context ty in
let new_metasenv =
List.map
*)
(* The default of term is the thesis of the goal to be prooved *)
-let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
+let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) =
let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let terms =
match terms with None -> [ty] | Some l -> l
in
(curi,metasenv',pbo,pty), [metano]
;;
-let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;;
-let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;;
-let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;
+let simpl_tac ~also_in_hypotheses ~terms =
+ mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.simpl
+ ~also_in_hypotheses ~terms);;
-let fold_tac ~reduction ~also_in_hypotheses ~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' = reduction context term 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: ma si potrebbe ovviare al problema. Ma non credo *)
- (*CSC: che si guadagni nulla in fatto di efficienza. *)
- let replace =
- ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term]
- in
- let ty' = replace ty in
- let metasenv' =
- let context' =
- if also_in_hypotheses then
+let reduce_tac ~also_in_hypotheses ~terms =
+ mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.reduce
+ ~also_in_hypotheses ~terms);;
+
+let whd_tac ~also_in_hypotheses ~terms =
+ mk_tactic ( reduction_tac ~reduction:CicReduction.whd
+ ~also_in_hypotheses ~terms);;
+
+let fold_tac ~reduction ~also_in_hypotheses ~term =
+ let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let term' = reduction context term 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: ma si potrebbe ovviare al problema. Ma non credo *)
+ (*CSC: che si guadagni nulla in fatto di efficienza. *)
+ let replace =
+ ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term]
+ in
+ let ty' = replace ty in
+ let metasenv' =
+ let context' =
+ if also_in_hypotheses then
+ List.map
+ (function
+ Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
+ | Some (n,Cic.Def (t,None)) -> Some (n,Cic.Def ((replace t),None))
+ | None -> None
+ | Some (_,Cic.Def (_,Some _)) -> assert false
+ ) context
+ else
+ context
+ in
List.map
(function
- Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
- | Some (n,Cic.Def (t,None)) -> Some (n,Cic.Def ((replace t),None))
- | None -> None
- | Some (_,Cic.Def (_,Some _)) -> assert false
- ) context
- else
- context
+ (n,_,_) when n = metano -> (metano,context',ty')
+ | _ as t -> t
+ ) metasenv
+
in
- List.map
- (function
- (n,_,_) when n = metano -> (metano,context',ty')
- | _ as t -> t
- ) metasenv
-
- in
- (curi,metasenv',pbo,pty), [metano]
+ (curi,metasenv',pbo,pty), [metano]
+ in
+ mk_tactic (fold_tac ~reduction ~also_in_hypotheses ~term)
;;