(* Copyright (C) 2000, 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/.
 *)

open ProofEngineHelpers
open ProofEngineTypes

  (* proof assistant status *)

let proof = ref (None : proof option)
let goal = ref (None : goal option)

let apply_or_can_apply_tactic ~try_only ~tactic =
 match !proof,!goal with
    None,_
  | _,None -> assert false
  | Some proof', Some goal' ->
     let (newproof, newgoals) = tactic ~status:(proof', goal') in
      if not try_only then
       begin
        proof := Some newproof;
        goal :=
         (match newgoals, newproof with
             goal::_, _ -> Some goal
           | [], (_,(goal,_,_)::_,_,_) ->
           (* the tactic left no open goal ; let's choose the first open goal *)
(*CSC: here we could implement and use a proof-tree like notion... *)
              Some goal
           | _, _ -> None)
       end
;;

let apply_tactic = apply_or_can_apply_tactic ~try_only:false;;

let can_apply_tactic ~tactic =
 try
  apply_or_can_apply_tactic ~try_only:true ~tactic ;
  true
 with
  Fail _ -> false
;;

(* metas_in_term term                                                *)
(* Returns the ordered list of the metas that occur in [term].       *)
(* Duplicates are removed. The implementation is not very efficient. *)
let metas_in_term term =
 let module C = Cic in
  let rec aux =
   function
      C.Rel _ -> []
    | C.Meta (n,_) -> [n]
    | C.Sort _
    | C.Implicit -> []
    | C.Cast (te,ty) -> (aux te) @ (aux ty)
    | C.Prod (_,s,t) -> (aux s) @ (aux t)
    | C.Lambda (_,s,t) -> (aux s) @ (aux t)
    | C.LetIn (_,s,t) -> (aux s) @ (aux t)
    | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
    | C.Var (_,exp_named_subst)
    | C.Const (_,exp_named_subst)
    | C.MutInd (_,_,exp_named_subst)
    | C.MutConstruct (_,_,_,exp_named_subst) ->
       List.fold_left (fun i (_,t) -> i @ (aux t)) [] exp_named_subst
    | C.MutCase (_,_,outt,t,pl) ->
       (aux outt) @ (aux t) @
        (List.fold_left (fun i t -> i @ (aux t)) [] pl)
    | C.Fix (_,fl) ->
        List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
    | C.CoFix (_,fl) ->
        List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
  in
   let metas = aux term in
    let rec elim_duplicates =
     function
        [] -> []
      | he::tl ->
         he::(elim_duplicates (List.filter (function el -> he <> el) tl))
    in
     elim_duplicates metas

(* perforate context term ty                                                 *)
(* replaces the term [term] in the proof with a new metavariable whose type  *)
(* is [ty]. [context] must be the context of [term] in the whole proof. This *)
(* could be easily computed; so the only reasons to have it as an argument   *)
(* are efficiency reasons.                                                   *)
let perforate context term ty =
 let module C = Cic in
  match !proof with
     None -> assert false
   | Some (uri,metasenv,bo,gty as proof') ->
      let newmeta = new_meta proof' in
       (* We push the new meta at the end of the list for pretty-printing *)
       (* purposes: in this way metas are ordered.                        *)
       let metasenv' = metasenv@[newmeta,context,ty] in
        let irl = identity_relocation_list_for_metavariable context in
(*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
        let bo' =
         ProofEngineReduction.replace (==) term (C.Meta (newmeta,irl)) bo
        in
        (* It may be possible that some metavariables occurred only in *)
        (* the term we are perforating and they now occurs no more. We *)
        (* get rid of them, collecting the really useful metavariables *)
        (* in metasenv''.                                              *)
(*CSC: Bug: una meta potrebbe non comparire in bo', ma comparire nel tipo *)
(*CSC: di una metavariabile che compare in bo'!!!!!!!                     *)
         let newmetas = metas_in_term bo' in
          let metasenv'' =
           List.filter (function (n,_,_) -> List.mem n newmetas) metasenv'
          in
           proof := Some (uri,metasenv'',bo',gty) ;
           goal := Some newmeta


(************************************************************)
(*                  Some easy tactics.                      *)
(************************************************************)

(* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
let reduction_tactic_in_scratch reduction_function term ty =
 let metasenv =
  match !proof with
     None -> []
   | Some (_,metasenv,_,_) -> metasenv
 in
 let metano,context,_ =
  match !goal with
     None -> assert false
   | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 in
  let term' = reduction_function context term in
   ProofEngineReduction.replace
    ~equality:(==) ~what:term ~with_what:term' ~where:ty
;;

let whd_in_scratch    = reduction_tactic_in_scratch CicReduction.whd
let reduce_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.reduce
let simpl_in_scratch  = reduction_tactic_in_scratch ProofEngineReduction.simpl

(************************************************************)
(*              Tactics defined elsewhere                   *)
(************************************************************)

  (* primitive tactics *)

let can_apply term = can_apply_tactic (PrimitiveTactics.apply_tac ~term)
let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
let intros () = apply_tactic PrimitiveTactics.intros_tac
let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term)
let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
let elim_intros_simpl term =
  apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
let change ~goal_input:what ~input:with_what =
  apply_tactic (PrimitiveTactics.change_tac ~what ~with_what)

  (* structural tactics *)

let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp)
let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)

  (* 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_whd term =
 apply_tactic
  (ReductionTactics.fold_tac ~reduction:CicReduction.whd
    ~also_in_hypotheses:true ~term)
let fold_reduce term =
 apply_tactic
  (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.reduce
    ~also_in_hypotheses:true ~term)
let fold_simpl term =
 apply_tactic
  (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.simpl
    ~also_in_hypotheses:true ~term)

  (* other tactics *)

let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term)
let ring () = apply_tactic Ring.ring_tac
let fourier () = apply_tactic FourierR.fourier_tac

let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)
let replace ~goal_input:what ~input:with_what = 
  apply_tactic (EqualityTactics.replace_tac ~what ~with_what)

let reflexivity () = apply_tactic EqualityTactics.reflexivity_tac
let symmetry () = apply_tactic EqualityTactics.symmetry_tac
let transitivity term = apply_tactic (EqualityTactics.transitivity_tac ~term)

let exists () = apply_tactic IntroductionTactics.exists_tac
let split () = apply_tactic IntroductionTactics.split_tac 
let left () = apply_tactic IntroductionTactics.left_tac
let right () = apply_tactic IntroductionTactics.right_tac

let assumption () = apply_tactic VariousTactics.assumption_tac

let generalize term = apply_tactic (VariousTactics.generalize_tac ~term)

let absurd term = apply_tactic (NegationTactics.absurd_tac ~term)
let contradiction () = apply_tactic NegationTactics.contradiction_tac

let decompose ~uris_choice_callback term =
 apply_tactic (EliminationTactics.decompose_tac ~term ~uris_choice_callback)

(*
let decide_equality () = apply_tactic VariousTactics.decide_equality_tac
let compare term1 term2 = apply_tactic (VariousTactics.compare_tac ~term1 ~term2)
*)

(*
let prova_tatticali () = apply_tactic Tacticals.prova_tac
*)