(* 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/.
 *)


(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
let assumption_tac ~status:((proof,goal) as status) =
  let module C = Cic in
  let module R = CicReduction in
  let module S = CicSubstitution in
   let _,metasenv,_,_ = proof in
    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
     let rec find n = function 
        hd::tl -> 
         (match hd with
             (Some (_, C.Decl t)) when
               (R.are_convertible context (S.lift n t) ty) -> n
           | (Some (_, C.Def t)) when
               (R.are_convertible context
                (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n 
           | _ -> find (n+1) tl
         )
      | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
     in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
;;

(* Questa invece era in fourierR.ml 
let assumption_tac ~status:(proof,goal)=
  let curi,metasenv,pbo,pty = proof in
  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  let num = ref 0 in
  let tac_list = List.map
        ( fun x -> num := !num + 1;
                match x with
                  Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
                  | _ -> ("fake",tcl_fail 1)
        )
        context
  in
  Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
;;
*)


(* ANCORA DA DEBUGGARE *)

(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
contesto e si lifta *)
let generalize_tac ~term ~status:((proof,goal) as status) =
  let module C = Cic in
  let module P = PrimitiveTactics in
  let module T = Tacticals in
   let _,metasenv,_,_ = proof in
    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
     T.thens 
      ~start:(P.cut_tac 
       ~term:(
         C.Prod(
          (C.Name "dummy_for_gen"), 
          (CicTypeChecker.type_of_aux' metasenv context term),
          (ProofEngineReduction.replace_lifting_csc 1
            ~equality:(==) 
            ~what:term 
            ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)  
            ~where:ty)
        )))	
      ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
      ~status
;;


(* IN FASE DI IMPLEMENTAZIONE *)

let decide_equality_tac =
  Tacticals.id_tac
;;

(*
let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
  let module C = Cic in
  let module U = UriManager in
  let module P = PrimitiveTactics in
  let module T = Tacticals in
   let _,metasenv,_,_ = proof in
    let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
     if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
       (* controllo che i due termini siano comparabili *)
      then
       T.thens 
         ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
         ~continuations:[split_tac ; P.intros_tac ~name:"FOO"]  
      else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types") 
;;
*)