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

(******************************************************************************)
(*                                                                            *)
(*                               PROJECT HELM                                 *)
(*                                                                            *)
(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
(*                                 29/01/2003                                 *)
(*                                                                            *)
(*                                                                            *)
(******************************************************************************)

exception RefreshSequentException of exn;;
exception RefreshProofException of exn;;

module type Callbacks =
  sig
    val sequent_viewer : unit -> TermViewer.sequent_viewer
    val term_editor : unit -> TermEditor.term_editor
    val get_current_scratch_infos :
     unit ->
      (Cic.term *
       (Cic.id, Cic.term) Hashtbl.t *
       (Cic.id, Cic.id option) Hashtbl.t *
       (string, Cic.hypothesis) Hashtbl.t
      ) option
    val set_current_scratch_infos :
     (Cic.term *
      (Cic.id, Cic.term) Hashtbl.t *
      (Cic.id, Cic.id option) Hashtbl.t *
      (string, Cic.hypothesis) Hashtbl.t
     ) option -> unit
    val refresh_proof : unit -> unit
    val refresh_goals : unit -> unit
    val decompose_uris_choice_callback :
      (UriManager.uri * int * 'a) list ->
      (UriManager.uri * int * 'b list) list
    val mk_fresh_name_callback :
      Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
    val output_html : string -> unit
  end
;;

module Make(C:Callbacks) =
  struct

   let call_tactic tactic () =
    let savedproof = !ProofEngine.proof in
    let savedgoal  = !ProofEngine.goal in
     begin
      try
       tactic () ;
       C.refresh_goals () ;
       C.refresh_proof ()
      with
         RefreshSequentException e ->
          C.output_html
           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
            "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
          ProofEngine.proof := savedproof ;
          ProofEngine.goal := savedgoal ;
          C.refresh_goals ()
       | RefreshProofException e ->
          C.output_html
           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
            "proof: " ^ Printexc.to_string e ^ "</h1>") ;
          ProofEngine.proof := savedproof ;
          ProofEngine.goal := savedgoal ;
          C.refresh_goals () ;
          C.refresh_proof ()
       | e ->
          C.output_html
           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
          ProofEngine.proof := savedproof ;
          ProofEngine.goal := savedgoal
     end

   let call_tactic_with_input tactic () =
    let savedproof = !ProofEngine.proof in
    let savedgoal  = !ProofEngine.goal in
     let uri,metasenv,bo,ty =
      match !ProofEngine.proof with
         None -> assert false
       | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
     in
      let canonical_context =
       match !ProofEngine.goal with
          None -> assert false
        | Some metano ->
           let (_,canonical_context,_) =
            List.find (function (m,_,_) -> m=metano) metasenv
           in
            canonical_context
      in
       try
        let metasenv',expr =
         (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
        in
         ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
         tactic expr ;
         C.refresh_goals () ;
         C.refresh_proof () ;
         (C.term_editor ())#reset
       with
          RefreshSequentException e ->
           C.output_html
            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
             "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
           ProofEngine.proof := savedproof ;
           ProofEngine.goal := savedgoal ;
           C.refresh_goals ()
        | RefreshProofException e ->
           C.output_html
            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
             "proof: " ^ Printexc.to_string e ^ "</h1>") ;
           ProofEngine.proof := savedproof ;
           ProofEngine.goal := savedgoal ;
           C.refresh_goals () ;
           C.refresh_proof ()
        | e ->
           C.output_html
            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
           ProofEngine.proof := savedproof ;
           ProofEngine.goal := savedgoal

  let call_tactic_with_goal_input tactic () =
   let module L = LogicalOperations in
   let module G = Gdome in
    let savedproof = !ProofEngine.proof in
    let savedgoal  = !ProofEngine.goal in
     match (C.sequent_viewer ())#get_selected_terms with
       [term] ->
         begin
          try
           tactic term ;
           C.refresh_goals () ;
           C.refresh_proof ()
          with
             RefreshSequentException e ->
              C.output_html
               ("<h1 color=\"red\">Exception raised during the refresh of " ^
                "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
              C.refresh_goals ()
           | RefreshProofException e ->
              C.output_html
               ("<h1 color=\"red\">Exception raised during the refresh of " ^
                "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
              C.refresh_goals () ;
              C.refresh_proof ()
           | e ->
              C.output_html
               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
         end
     | [] ->
        C.output_html
         ("<h1 color=\"red\">No term selected</h1>")
     | _ ->
        C.output_html
         ("<h1 color=\"red\">Many terms selected</h1>")

  let call_tactic_with_goal_inputs tactic () =
   let module L = LogicalOperations in
   let module G = Gdome in
    let savedproof = !ProofEngine.proof in
    let savedgoal  = !ProofEngine.goal in
     try
      match (C.sequent_viewer ())#get_selected_terms with
         [] ->
          C.output_html
           ("<h1 color=\"red\">No term selected</h1>")
       | terms ->
          tactic terms ;
          C.refresh_goals () ;
          C.refresh_proof ()
     with
        RefreshSequentException e ->
         C.output_html
          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
         ProofEngine.proof := savedproof ;
         ProofEngine.goal := savedgoal ;
         C.refresh_goals ()
      | RefreshProofException e ->
         C.output_html
          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
         ProofEngine.proof := savedproof ;
         ProofEngine.goal := savedgoal ;
         C.refresh_goals () ;
         C.refresh_proof ()
      | e ->
         C.output_html
          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
         ProofEngine.proof := savedproof ;
         ProofEngine.goal := savedgoal

  let call_tactic_with_input_and_goal_input tactic () =
   let module L = LogicalOperations in
   let module G = Gdome in
    let savedproof = !ProofEngine.proof in
    let savedgoal  = !ProofEngine.goal in
     match (C.sequent_viewer ())#get_selected_terms with
       [term] ->
         begin
          try
           let uri,metasenv,bo,ty =
            match !ProofEngine.proof with
               None -> assert false
             | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
           in
            let canonical_context =
             match !ProofEngine.goal with
                None -> assert false
              | Some metano ->
                 let (_,canonical_context,_) =
                  List.find (function (m,_,_) -> m=metano) metasenv
                 in
                  canonical_context in
            let (metasenv',expr) =
             (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
            in
             ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
             tactic ~goal_input:term ~input:expr ;
             C.refresh_goals () ;
             C.refresh_proof () ;
             (C.term_editor ())#reset
          with
             RefreshSequentException e ->
              C.output_html
               ("<h1 color=\"red\">Exception raised during the refresh of " ^
                "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
              C.refresh_goals ()
           | RefreshProofException e ->
              C.output_html
               ("<h1 color=\"red\">Exception raised during the refresh of " ^
                "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
              C.refresh_goals () ;
              C.refresh_proof ()
           | e ->
              C.output_html
               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
         end
     | [] ->
        C.output_html
         ("<h1 color=\"red\">No term selected</h1>")
     | _ ->
        C.output_html
         ("<h1 color=\"red\">Many terms selected</h1>")

  let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
   let module L = LogicalOperations in
   let module G = Gdome in
    let mmlwidget =
     (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
    let savedproof = !ProofEngine.proof in
    let savedgoal  = !ProofEngine.goal in
     match mmlwidget#get_selections with
       [node] ->
        let xpath =
         ((node : Gdome.element)#getAttributeNS
           ~namespaceURI:Misc.helmns
           ~localName:(G.domString "xref"))#to_string
        in
         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
         else
          begin
           try
            match C.get_current_scratch_infos () with
               (* term is the whole goal in the scratch_area *)
               Some (term,ids_to_terms, ids_to_father_ids,_) ->
                let id = xpath in
                 let expr = tactic term (Hashtbl.find ids_to_terms id) in
                  let mml,scratch_infos =
                   ApplyStylesheets.mml_of_cic_term 111 expr
                  in
                   C.set_current_scratch_infos (Some scratch_infos) ;
                   scratch_window#show () ;
                   scratch_window#mmlwidget#load_doc ~dom:mml
             | None -> assert false (* "ERROR: No current term!!!" *)
           with
            e ->
             C.output_html
              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
          end
     | [] ->
        C.output_html
         ("<h1 color=\"red\">No term selected</h1>")
     | _ ->
        C.output_html
         ("<h1 color=\"red\">Many terms selected</h1>")

  let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
   let module L = LogicalOperations in
   let module G = Gdome in
    let mmlwidget =
     (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
    let savedproof = !ProofEngine.proof in
    let savedgoal  = !ProofEngine.goal in
     match mmlwidget#get_selections with
        [] ->
         C.output_html
          ("<h1 color=\"red\">No term selected</h1>")
      | l ->
         try
          match C.get_current_scratch_infos () with
             (* term is the whole goal in the scratch_area *)
             Some (term,ids_to_terms, ids_to_father_ids,_) ->
              let term_of_node node =
               let xpath =
                ((node : Gdome.element)#getAttributeNS
                  ~namespaceURI:Misc.helmns
                  ~localName:(G.domString "xref"))#to_string
               in
                if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
                else
                 let id = xpath in
                  Hashtbl.find ids_to_terms id
              in
               let terms = List.map term_of_node l in
                let expr = tactic terms term in
                 let mml,scratch_infos =
                  ApplyStylesheets.mml_of_cic_term 111 expr
                 in
                  C.set_current_scratch_infos (Some scratch_infos) ;
                  scratch_window#show () ;
                  scratch_window#mmlwidget#load_doc ~dom:mml
           | None -> assert false (* "ERROR: No current term!!!" *)
         with
          e ->
           C.output_html
            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")

  let call_tactic_with_hypothesis_input tactic () =
   let module L = LogicalOperations in
   let module G = Gdome in
    let savedproof = !ProofEngine.proof in
    let savedgoal  = !ProofEngine.goal in
     match (C.sequent_viewer ())#get_selected_hypotheses with
       [hypothesis] ->
         begin
          try
           tactic hypothesis ;
           C.refresh_goals () ;
           C.refresh_proof ()
          with
             RefreshSequentException e ->
              C.output_html
               ("<h1 color=\"red\">Exception raised during the refresh of " ^
                "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
              C.refresh_goals ()
           | RefreshProofException e ->
              C.output_html
               ("<h1 color=\"red\">Exception raised during the refresh of " ^
                "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
              C.refresh_goals () ;
              C.refresh_proof ()
           | e ->
              C.output_html
               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
         end
     | [] ->
        C.output_html
         ("<h1 color=\"red\">No hypothesis selected</h1>")
     | _ ->
        C.output_html
         ("<h1 color=\"red\">Many hypothesis selected</h1>")


  let intros =
   call_tactic
    (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
  let exact = call_tactic_with_input ProofEngine.exact
  let apply = call_tactic_with_input ProofEngine.apply
  let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
  let elimtype = call_tactic_with_input ProofEngine.elim_type
  let whd = call_tactic_with_goal_inputs ProofEngine.whd
  let reduce = call_tactic_with_goal_inputs ProofEngine.reduce
  let simpl = call_tactic_with_goal_inputs ProofEngine.simpl
  let fold_whd = call_tactic_with_input ProofEngine.fold_whd
  let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce
  let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl
  let cut =
   call_tactic_with_input
    (ProofEngine.cut ~mk_fresh_name_callback:C.mk_fresh_name_callback)
  let change = call_tactic_with_input_and_goal_input ProofEngine.change
  let letin =
   call_tactic_with_input
    (ProofEngine.letin ~mk_fresh_name_callback:C.mk_fresh_name_callback)
  let ring = call_tactic ProofEngine.ring
  let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody
  let clear = call_tactic_with_hypothesis_input ProofEngine.clear
  let fourier = call_tactic ProofEngine.fourier
  let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl
  let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl
  let replace = call_tactic_with_input_and_goal_input ProofEngine.replace
  let reflexivity = call_tactic ProofEngine.reflexivity
  let symmetry = call_tactic ProofEngine.symmetry
  let transitivity = call_tactic_with_input ProofEngine.transitivity
  let exists = call_tactic ProofEngine.exists
  let split = call_tactic ProofEngine.split
  let left = call_tactic ProofEngine.left
  let right = call_tactic ProofEngine.right
  let assumption = call_tactic ProofEngine.assumption
  let generalize =
   call_tactic_with_goal_inputs
    (ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)
  let absurd = call_tactic_with_input ProofEngine.absurd
  let contradiction = call_tactic ProofEngine.contradiction
  let decompose =
   call_tactic_with_input
    (ProofEngine.decompose
      ~uris_choice_callback:C.decompose_uris_choice_callback)
  let whd_in_scratch scratch_window =
   call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
    scratch_window
  let reduce_in_scratch scratch_window =
   call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
    scratch_window
  let simpl_in_scratch scratch_window =
   call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
    scratch_window
  
end
;;