(* Copyright (C) 2002, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

(*
let reduction_tac ~reduction ~status:(proof,goal) =
 let curi,metasenv,pbo,pty = proof in
 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
  let new_ty = reduction context ty in
   let new_metasenv = 
    List.map
    (function
      (n,_,_) when n = metano -> (metano,context,new_ty)
      | _ as t -> t
    ) metasenv
   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 ~terms ~status:(proof,goal) =
 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
  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 terms' = List.map (reduction context) terms in
     ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
      ~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,None)) ->
             (Some (name,Cic.Def ((replace context t),None)))::context
          | Some (name,Cic.Decl t) ->
             (Some (name,Cic.Decl (replace context t)))::context
          | None -> None::context
          | Some (_,Cic.Def (_,Some _)) -> assert false
       ) 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 ;;
let whd_tac = reduction_tac ~reduction:CicReduction.whd ;;

let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(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
           (n,_,_) when n = metano -> (metano,context',ty')
         | _ as t -> t
       ) metasenv
     
    in
     (curi,metasenv',pbo,pty), [metano]
;;