(* The default of term is the thesis of the goal to be prooved *)
let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) =
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let terms =
- match terms with None -> [ty] | Some l -> l
+ match terms with None -> [ty] | Some l -> l
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: 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 lift 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 terms = List.fold_left
- (fun acc t ->
- try
- (CicSubstitution.delift lift t) :: acc
- with Failure _ -> acc
- ) [] terms
- in
- let terms' = List.map (reduction context) terms in
- ProofEngineReduction.replace
- ~equality:(=) ~what:terms ~with_what:terms' ~where:where
- with
- _ -> where
+ 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 terms' = List.map (reduction context) terms in
+ ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
+ ~where:where
+ with
+ _ -> where
in
- let ty' = replace 0 context ty in
- let context', _ =
+ let ty' = replace context ty in
+ let context' =
if also_in_hypotheses then
List.fold_right
- (fun entry (context,i) ->
+ (fun entry context ->
match entry with
- | Some (name,Cic.Def (t,None)) ->
- (Some (name,Cic.Def ((replace i context t),None)))::context, i-1
+ Some (name,Cic.Def (t,None)) ->
+ (Some (name,Cic.Def ((replace context t),None)))::context
| Some (name,Cic.Decl t) ->
- (Some (name,Cic.Decl (replace i context t)))::context, i-1
- | None -> None::context, i-1
+ (Some (name,Cic.Decl (replace context t)))::context
+ | None -> None::context
| Some (_,Cic.Def (_,Some _)) -> assert false
- ) context ([],(List.length context))
+ ) context []
else
- context, 0
+ context
in
let metasenv' =
List.map