(* 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_tactic ~tactic:tactic =
 match !proof,!goal with
    None,_
  | _,None -> assert false
  | Some proof', Some goal' ->
     let (newproof, newgoals) = tactic ~status:(proof', goal') in
     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)

(* 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.Var _ -> []
    | 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.Const _
    | C.MutInd _
    | C.MutConstruct _ -> []
    | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
       (aux outt) @ (aux t) @
        (List.fold_left (fun i t -> i @ (aux t)) [] pl)
    | C.Fix (i,fl) ->
        List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
    | C.CoFix (i,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.                      *)
(************************************************************)

(*CSC: generatore di nomi? Chiedere il nome? *)
let fresh_name =
 let next_fresh_index = ref 0
in
 function () ->
  incr next_fresh_index ;
  "fresh_name" ^ string_of_int !next_fresh_index

let reduction_tactic reduction_function term =
 let curi,metasenv,pbo,pty =
  match !proof with
     None -> assert false
   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 in
 let metano,context,ty =
  match !goal with
     None -> assert false
   | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 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 term' = reduction_function context term in
     ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
      ~where:where
   with
    _ -> where
   in
    let ty' = replace context ty in
    let context' =
     List.fold_right
      (fun entry context ->
        match entry with
           Some (name,Cic.Def  t) ->
            (Some (name,Cic.Def  (replace context t)))::context
         | Some (name,Cic.Decl t) ->
            (Some (name,Cic.Decl (replace context t)))::context
         | None -> None::context
      ) context []
    in
     let metasenv' = 
      List.map
       (function
           (n,_,_) when n = metano -> (metano,context',ty')
         | _ as t -> t
       ) metasenv
     in
      proof := Some (curi,metasenv',pbo,pty) ;
      goal := Some metano

(* 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    = reduction_tactic CicReduction.whd
let reduce = reduction_tactic ProofEngineReduction.reduce
let simpl  = reduction_tactic ProofEngineReduction.simpl

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

(* It is just the opposite of whd. The code should probably be merged. *)
let fold term =
 let curi,metasenv,pbo,pty =
  match !proof with
     None -> assert false
   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 in
 let metano,context,ty =
  match !goal with
     None -> assert false
   | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 in
  let term' = CicReduction.whd 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:(ProofEngineReduction.syntactic_equality)
     ~what:term' ~with_what:term
   in
    let ty' = replace ty in
    let context' =
     List.map
      (function
          Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
        | Some (n,Cic.Def t)  -> Some (n,Cic.Def  (replace t))
        | None -> None
      ) context
    in
     let metasenv' = 
      List.map
       (function
           (n,_,_) when n = metano -> (metano,context',ty')
         | _ as t -> t
       ) metasenv
     in
      proof := Some (curi,metasenv',pbo,pty) ;
      goal := Some metano

exception NotConvertible

(*CSC: Bug (or feature?). [input] is parsed in the context of the goal,  *)
(*CSC: while [goal_input] can have a richer context (because of binders) *)
(*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
(*CSC: Is that evident? Is that right? Or should it be changed?          *)
let change ~goal_input ~input =
 let curi,metasenv,pbo,pty =
  match !proof with
     None -> assert false
   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 in
 let metano,context,ty =
  match !goal with
     None -> assert false
   | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 in
  (* are_convertible works only on well-typed terms *)
  ignore (CicTypeChecker.type_of_aux' metasenv context input) ;
  if CicReduction.are_convertible context goal_input input then
   begin
    let replace =
     ProofEngineReduction.replace
      ~equality:(==) ~what:goal_input ~with_what:input
    in
    let ty' = replace ty in
    let context' =
     List.map
      (function
          Some (name,Cic.Def  t) -> Some (name,Cic.Def  (replace t))
        | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
        | None -> None
      ) context
    in
     let metasenv' = 
      List.map
       (function
           (n,_,_) when n = metano -> (metano,context',ty')
         | _ as t -> t
       ) metasenv
     in
      proof := Some (curi,metasenv',pbo,pty) ;
      goal := Some metano
   end
  else
   raise NotConvertible

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

  (* primitive tactics *)

let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
let intros () =
  apply_tactic (PrimitiveTactics.intros_tac ~name:(fresh_name ()))
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)

  (* structural tactics *)

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

  (* other tactics *)

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