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

open CicReduction
open PrimitiveTactics
open ProofEngineTypes
open UriManager

open HelmLibraryObjects

(** DEBUGGING *)

  (** perform debugging output? *)
let debug = false

  (** debugging print *)
let warn s =
  if debug then
    prerr_endline ("RING WARNING: " ^ s)

(** CIC URIS *)

(**
  Note: For constructors URIs aren't really URIs but rather triples of
  the form (uri, typeno, consno).  This discrepancy is to preserver an
  uniformity of invocation of "mkXXX" functions.
*)

let equality_is_a_congruence_A =
 uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var"
let equality_is_a_congruence_x =
 uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var"
let equality_is_a_congruence_y =
 uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var"

let apolynomial_uri =
  uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"
let apvar_uri = (apolynomial_uri, 0, 1)
let ap0_uri = (apolynomial_uri, 0, 2)
let ap1_uri = (apolynomial_uri, 0, 3)
let applus_uri = (apolynomial_uri, 0, 4)
let apmult_uri = (apolynomial_uri, 0, 5)
let apopp_uri = (apolynomial_uri, 0, 6)

let quote_varmap_A_uri = uri_of_string "cic:/Coq/ring/Quote/variables_map/A.var"
let varmap_uri = uri_of_string "cic:/Coq/ring/Quote/varmap.ind"
let empty_vm_uri = (varmap_uri, 0, 1)
let node_vm_uri = (varmap_uri, 0, 2)
let varmap_find_uri = uri_of_string "cic:/Coq/ring/Quote/varmap_find.con"
let index_uri = uri_of_string "cic:/Coq/ring/Quote/index.ind"
let left_idx_uri = (index_uri, 0, 1)
let right_idx_uri = (index_uri, 0, 2)
let end_idx_uri = (index_uri, 0, 3)

let abstract_rings_A_uri =
 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/A.var"
let abstract_rings_Aplus_uri =
 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aplus.var"
let abstract_rings_Amult_uri =
 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Amult.var"
let abstract_rings_Aone_uri =
 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aone.var"
let abstract_rings_Azero_uri =
 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Azero.var"
let abstract_rings_Aopp_uri =
 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aopp.var"
let abstract_rings_Aeq_uri =
 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aeq.var"
let abstract_rings_vm_uri =
 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/vm.var"
let abstract_rings_T_uri =
 uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/T.var"
let interp_ap_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/interp_ap.con"
let interp_sacs_uri =
  uri_of_string "cic:/Coq/ring/Ring_abstract/interp_sacs.con"
let apolynomial_normalize_uri =
  uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con"
let apolynomial_normalize_ok_uri =
  uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con"

(** CIC PREDICATES *)

  (**
    check whether a term is a constant or not, if argument "uri" is given and is
    not "None" also check if the constant correspond to the given one or not
  *)
let cic_is_const ?(uri: uri option = None) term =
  match uri with
  | None ->
      (match term with
        | Cic.Const _ -> true
        | _ -> false)
  | Some realuri ->
      (match term with
        | Cic.Const (u, _) when (eq u realuri) -> true
        | _ -> false)

(** PROOF AND GOAL ACCESSORS *)

  (**
    @param proof a proof
    @return the uri of a given proof
  *)
let uri_of_proof ~proof:(uri, _, _, _) = uri

  (**
    @param status current proof engine status
    @raise Failure if proof is None
    @return current goal's metasenv
  *)
let metasenv_of_status ((_,m,_,_), _) = m

  (**
    @param status a proof engine status
    @raise Failure when proof or goal are None
    @return context corresponding to current goal
  *)
let context_of_status status =
  let (proof, goal) = status in
  let metasenv = metasenv_of_status status in
  let _, context, _ = CicUtil.lookup_meta goal metasenv in
   context

(** CIC TERM CONSTRUCTORS *)

  (**
    Create a Cic term consisting of a constant
    @param uri URI of the constant
    @proof current proof
    @exp_named_subst explicit named substitution
  *)
let mkConst ~uri ~exp_named_subst =
  Cic.Const (uri, exp_named_subst)

  (**
    Create a Cic term consisting of a constructor
    @param uri triple <uri, typeno, consno> where uri is the uri of an inductive
    type, typeno is the type number in a mutind structure (0 based), consno is
    the constructor number (1 based)
    @exp_named_subst explicit named substitution
  *)
let mkCtor ~uri:(uri, typeno, consno) ~exp_named_subst =
 Cic.MutConstruct (uri, typeno, consno, exp_named_subst)

  (**
    Create a Cic term consisting of a type member of a mutual induction
    @param uri pair <uri, typeno> where uri is the uri of a mutual inductive
    type and typeno is the type number (0 based) in the mutual induction
    @exp_named_subst explicit named substitution
  *)
let mkMutInd ~uri:(uri, typeno) ~exp_named_subst =
 Cic.MutInd (uri, typeno, exp_named_subst)

(** EXCEPTIONS *)

  (**
    raised when the current goal is not ringable; a goal is ringable when is an
    equality on reals (@see r_uri)
  *)
exception GoalUnringable

(** RING's FUNCTIONS LIBRARY *)

  (**
    Check whether the ring tactic can be applied on a given term (i.e. that is
    an equality on reals)
    @param term to be tested
    @return true if the term is ringable, false otherwise
  *)
let ringable =
  let is_equality = function
    | Cic.MutInd (uri, 0, []) when (eq uri Logic.eq_URI) -> true
    | _ -> false
  in
  let is_real = function
    | Cic.Const (uri, _) when (eq uri Reals.r_URI) -> true
    | _ -> false
  in
  function
    | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) ->
        warn "Goal Ringable!";
        true
    | _ ->
        warn "Goal Not Ringable :-((";
        false

  (**
    split an equality goal of the form "t1 = t2" in its two subterms t1 and t2
    after checking that the goal is ringable
    @param goal the current goal
    @return a pair (t1,t2) that are two sides of the equality goal
    @raise GoalUnringable if the goal isn't ringable
  *)
let split_eq = function
  | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term ->
        warn ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>");
        warn ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>");
        (t1, t2)
  | _ -> raise GoalUnringable

  (**
    @param i an integer index representing a 1 based number of node in a binary
    search tree counted in a fbs manner (i.e.: 1 is the root, 2 is the left
    child of the root (if any), 3 is the right child of the root (if any), 4 is
    the left child of the left child of the root (if any), ....)
    @param proof the current proof
    @return an index representing the same node in a varmap (@see varmap_uri),
    the returned index is as defined in index (@see index_uri)
  *)
let path_of_int n =
  let rec digits_of_int n =
    if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1))
  in
  List.fold_right
    (fun digit path ->
      Cic.Appl [
        mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) [];
        path])
    (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *)
    (mkCtor end_idx_uri [])

  (**
    Build a variable map (@see varmap_uri) from a variables array.
    A variable map is almost a binary tree so this function receiving a var list
    like [v;w;x;y;z] will build a varmap of shape:       v
                                                        / \
                                                       w   x
                                                      / \
                                                     y   z
    @param vars variables array
    @return a cic term representing the variable map containing vars variables
  *)
let btree_of_array ~vars =
  let r = Reals.r in
  let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in
  let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in
  let size = Array.length vars in
  let halfsize = size lsr 1 in
  let rec aux n =   (* build the btree starting from position n *)
      (*
        n is the position in the vars array _1_based_ in order to access
        left and right child using (n*2, n*2+1) trick
      *)
    if n > size then
      empty_vm_r
    else if n > halfsize then  (* no more children *)
      Cic.Appl [node_vm_r; vars.(n-1); empty_vm_r; empty_vm_r]
    else  (* still children *)
      Cic.Appl [node_vm_r; vars.(n-1); aux (n*2); aux (n*2+1)]
  in
  aux 1

  (**
    abstraction function:
    concrete polynoms       ----->      (abstract polynoms, varmap)
    @param terms list of conrete polynoms
    @return a pair <aterms, varmap> where aterms is a list of abstract polynoms
    and varmap is the variable map needed to interpret them
  *)
let abstract_poly ~terms =
  let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *)
  let varlist = ref [] in  (* vars list in reverse order *)
  let counter = ref 1 in  (* index of next new variable *)
  let rec aux = function  (* TODO not tail recursive *)
    (* "bop" -> binary operator | "uop" -> unary operator *)
    | Cic.Appl (bop::t1::t2::[])
      when (cic_is_const ~uri:(Some Reals.rplus_URI) bop) -> (* +. *)
        Cic.Appl [mkCtor applus_uri []; aux t1; aux t2]
    | Cic.Appl (bop::t1::t2::[])
      when (cic_is_const ~uri:(Some Reals.rmult_URI) bop) -> (* *. *)
        Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2]
    | Cic.Appl (uop::t::[])
      when (cic_is_const ~uri:(Some Reals.ropp_URI) uop) -> (* ~-. *)
        Cic.Appl [mkCtor apopp_uri []; aux t]
    | t when (cic_is_const ~uri:(Some Reals.r0_URI) t) -> (* 0. *)
        mkCtor ap0_uri []
    | t when (cic_is_const ~uri:(Some Reals.r1_URI) t) -> (* 1. *)
        mkCtor ap1_uri []
    | t ->  (* variable *)
      try
        Hashtbl.find varhash t (* use an old var *)
      with Not_found -> begin (* create a new var *)
        let newvar =
          Cic.Appl [mkCtor apvar_uri []; path_of_int !counter]
        in
        incr counter;
        varlist := t :: !varlist;
        Hashtbl.add varhash t newvar;
        newvar
      end
  in
  let aterms = List.map aux terms in  (* abstract vars *)
  let varmap =  (* build varmap *)
    btree_of_array ~vars:(Array.of_list (List.rev !varlist))
  in
  (aterms, varmap)

  (**
    given a list of abstract terms (i.e. apolynomials) build the ring "segments"
    that is triples like (t', t'', t''') where
          t'    = interp_ap(varmap, at)
          t''   = interp_sacs(varmap, (apolynomial_normalize at))
          t'''  = apolynomial_normalize_ok(varmap, at)
    at is the abstract term built from t, t is a single member of aterms
  *)
let build_segments ~terms =
  let theory_args_subst varmap =
   [abstract_rings_A_uri, Reals.r ;
    abstract_rings_Aplus_uri, Reals.rplus ;
    abstract_rings_Amult_uri, Reals.rmult ;
    abstract_rings_Aone_uri, Reals.r1 ;
    abstract_rings_Azero_uri, Reals.r0 ;
    abstract_rings_Aopp_uri, Reals.ropp ;
    abstract_rings_vm_uri, varmap] in
  let theory_args_subst' eq varmap t =
   [abstract_rings_A_uri, Reals.r ;
    abstract_rings_Aplus_uri, Reals.rplus ;
    abstract_rings_Amult_uri, Reals.rmult ;
    abstract_rings_Aone_uri, Reals.r1 ;
    abstract_rings_Azero_uri, Reals.r0 ;
    abstract_rings_Aopp_uri, Reals.ropp ;
    abstract_rings_Aeq_uri, eq ;
    abstract_rings_vm_uri, varmap ;
    abstract_rings_T_uri, t] in
  let interp_ap varmap =
   mkConst interp_ap_uri (theory_args_subst varmap) in
  let interp_sacs varmap =
   mkConst interp_sacs_uri (theory_args_subst varmap) in
  let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in
  let apolynomial_normalize_ok eq varmap t =
   mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in
  let lxy_false =   (** Cic funcion "fun (x,y):R -> false" *)
    Cic.Lambda (Cic.Anonymous, Reals.r,
      Cic.Lambda (Cic.Anonymous, Reals.r, Datatypes.falseb))
  in
  let (aterms, varmap) = abstract_poly ~terms in  (* abstract polys *)
  List.map    (* build ring segments *)
   (fun t ->
     Cic.Appl [interp_ap varmap ; t],
     Cic.Appl (
       [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]),
     Cic.Appl [apolynomial_normalize_ok lxy_false varmap Reals.rtheory ; t]
   ) aterms


let status_of_single_goal_tactic_result =
 function
    proof,[goal] -> proof,goal
  | _ ->
    raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")

(* Galla: spostata in variousTactics.ml 
  (**
    auxiliary tactic "elim_type"
    @param status current proof engine status
    @param term term to cut
  *)
let elim_type_tac ~term status =
  warn "in Ring.elim_type_tac";
  Tacticals.thens ~start:(cut_tac ~term)
   ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] status
*)

  (**
    auxiliary tactic, use elim_type and try to close 2nd subgoal using proof
    @param status current proof engine status
    @param term term to cut
    @param proof term used to prove second subgoal generated by elim_type
  *)
let elim_type2_tac ~term ~proof =
 let elim_type2_tac ~term ~proof status =
  let module E = EliminationTactics in
  warn "in Ring.elim_type2";
  ProofEngineTypes.apply_tactic 
   (Tacticals.thens ~start:(E.elim_type_tac ~term)
    ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
 in
  ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)

(* Galla: spostata in variousTactics.ml
  (**
    Reflexivity tactic, try to solve current goal using "refl_eqT"
    Warning: this isn't equale to the coq's Reflexivity because this one tries
    only refl_eqT, coq's one also try "refl_equal"
    @param status current proof engine status
  *)
let reflexivity_tac (proof, goal) =
  warn "in Ring.reflexivity_tac";
  let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in
  try
    apply_tac (proof, goal) ~term:refl_eqt
  with (Fail _) as e ->
    let e_str = Printexc.to_string e in
    raise (Fail ("Reflexivity failed with exception: " ^ e_str))
*)

  (** lift an 8-uple of debrujins indexes of n *)
let lift ~n (a,b,c,d,e,f,g,h) =
  match (List.map (CicSubstitution.lift n) [a;b;c;d;e;f;g;h]) with
  | [a;b;c;d;e;f;g;h] -> (a,b,c,d,e,f,g,h)
  | _ -> assert false

  (**
    remove hypothesis from a given status starting from the last one
    @param count number of hypotheses to remove
    @param status current proof engine status
  *)
let purge_hyps_tac ~count =
 let purge_hyps_tac ~count status =
  let module S = ProofEngineStructuralRules in
  let (proof, goal) = status in
  let rec aux n context status =
    assert(n>=0);
    match (n, context) with
    | (0, _) -> status
    | (n, hd::tl) ->
        aux (n-1) tl
         (status_of_single_goal_tactic_result 
	  (ProofEngineTypes.apply_tactic (S.clear ~hyp:hd) status))
    | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
  in
   let (_, metasenv, _, _) = proof in
    let (_, context, _) = CicUtil.lookup_meta goal metasenv in
     let proof',goal' = aux count context status in
      assert (goal = goal') ;
      proof',[goal']
 in
  ProofEngineTypes.mk_tactic (purge_hyps_tac ~count)

(** THE TACTIC! *)

  (**
    Ring tactic, does associative and commutative rewritings in Reals ring
    @param status current proof engine status
  *)
 
let ring_tac status =
  let (proof, goal) = status in
  warn "in Ring tactic";
  let eqt = mkMutInd (Logic.eq_URI, 0) [] in
  let r = Reals.r in
  let metasenv = metasenv_of_status status in
  let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
  let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
  match (build_segments ~terms:[t1; t2]) with
  | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
      List.iter  (* debugging, feel free to remove *)
        (fun (descr, term) ->
          warn (descr ^ " " ^ (CicPp.ppterm term)))
        (List.combine
          ["t1"; "t1'"; "t1''"; "t1'_eq_t1''";
           "t2"; "t2'"; "t2''"; "t2'_eq_t2''"]
          [t1; t1'; t1''; t1'_eq_t1'';
           t2; t2'; t2''; t2'_eq_t2'']);
      try
        let new_hyps = ref 0 in  (* number of new hypotheses created *)
	ProofEngineTypes.apply_tactic 
         (Tacticals.try_tactics
          ~tactics:[
            "reflexivity", EqualityTactics.reflexivity_tac ;
            "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
            "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
            "exact sym_eqt su t1 ...", exact_tac
            ~term:(
              Cic.Appl
               [mkConst Logic.sym_eq_URI
                 [equality_is_a_congruence_A, Reals.r;
                  equality_is_a_congruence_x, t1'' ;
                  equality_is_a_congruence_y, t1
                 ] ;
                t1'_eq_t1''
               ]) ;
            "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
              let status' = (* status after 1st elim_type use *)
                let context = context_of_status status in
		let b,_ = (*TASSI : FIXME*)
		  are_convertible context t1'' t1 CicUniv.empty_ugraph in 
                if not b then begin
                  warn "t1'' and t1 are NOT CONVERTIBLE";
                  let newstatus =
		    ProofEngineTypes.apply_tactic 
                    (elim_type2_tac  (* 1st elim_type use *)
                      ~proof:t1'_eq_t1''
                      ~term:(Cic.Appl [eqt; r; t1''; t1]))
		    status 
                  in
                   incr new_hyps; (* elim_type add an hyp *)
                   match newstatus with
                      (proof,[goal]) -> proof,goal
                    | _ -> assert false
                end else begin
                  warn "t1'' and t1 are CONVERTIBLE";
                  status
                end
              in
              let (t1,t1',t1'',t1'_eq_t1'',t2,t2',t2'',t2'_eq_t2'') =
                lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
              in
              let status'' =
	       ProofEngineTypes.apply_tactic
                (Tacticals.try_tactics (* try to solve 1st subgoal *)
                  ~tactics:[
                    "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
                    "exact sym_eqt su t2 ...",
                      exact_tac
                       ~term:(
                         Cic.Appl
                          [mkConst Logic.sym_eq_URI
                            [equality_is_a_congruence_A, Reals.r;
                             equality_is_a_congruence_x, t2'' ;
                             equality_is_a_congruence_y, t2
                            ] ;
                           t2'_eq_t2''
                          ]) ;
                    "elim_type eqt su t2 ...", 
		     ProofEngineTypes.mk_tactic (fun status ->
                      let status' =
                        let context = context_of_status status in
			let b,_ = (* TASSI:FIXME *)
			  are_convertible context t2'' t2 CicUniv.empty_ugraph 
			in
			  if not b then begin 
                          warn "t2'' and t2 are NOT CONVERTIBLE";
                          let newstatus =
			    ProofEngineTypes.apply_tactic 
                             (elim_type2_tac  (* 2nd elim_type use *)
                              ~proof:t2'_eq_t2''
                              ~term:(Cic.Appl [eqt; r; t2''; t2]))
			     status
                          in
                          incr new_hyps; (* elim_type add an hyp *)
                          match newstatus with
                             (proof,[goal]) -> proof,goal
                           | _ -> assert false
                        end else begin
                          warn "t2'' and t2 are CONVERTIBLE";
                          status
                        end
                      in
                      try (* try to solve main goal *)
                        warn "trying reflexivity ....";
                        ProofEngineTypes.apply_tactic 
			 EqualityTactics.reflexivity_tac status'
                      with (Fail _) ->  (* leave conclusion to the user *)
                        warn "reflexivity failed, solution's left as an ex :-)";
                        ProofEngineTypes.apply_tactic 
			 (purge_hyps_tac ~count:!new_hyps) status')])
		  status'	
              in
              status'')])
	 status      
      with (Fail s) ->
        raise (Fail ("Ring failure: " ^ s))
    end
  | _ -> (* impossible: we are applying ring exacty to 2 terms *)
    assert false

  (* wrap ring_tac catching GoalUnringable and raising Fail *)

let ring_tac status =
  try
    ring_tac status
  with GoalUnringable ->
    raise (Fail "goal unringable")

let ring_tac = ProofEngineTypes.mk_tactic ring_tac