(* Copyright (C) 2005, 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 Utils;;

let debug_print s = ();;(*prerr_endline (Lazy.force s);;*)

type auto_type = 
  int ->
  AutoTypes.flags ->
  ProofEngineTypes.proof -> 
  Cic.context -> 
  AutoCache.cache -> 
  ProofEngineTypes.goal list ->
    Cic.substitution list * AutoCache.cache * int

let is_var_free (_,term,_ty) =
  let rec is_var_free = function
    | Cic.Var _ -> false
    | Cic.Appl l -> List.for_all is_var_free l
    | Cic.Prod (_, s, t) 
    | Cic.Lambda (_, s, t)
    | Cic.LetIn (_, s, t) 
    | Cic.Cast (s, t) -> (is_var_free s) && (is_var_free t)
    | _ -> true
 in
 is_var_free term
;;

let rec is_an_equality = function
  | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] 
    when (LibraryObjects.is_eq_URI uri) -> true
  | Cic.Prod (name, s, t) -> is_an_equality t
  | _ -> false
;;

let build_equality_of_hypothesis bag index head args newmetas maxmeta = 
  match head with
  | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
      let p =
        if args = [] then Cic.Rel index else Cic.Appl ((Cic.Rel index)::args)
      in 
      debug_print
        (lazy
           (Printf.sprintf "OK: %s" (CicPp.ppterm p)));
      let o = !Utils.compare_terms t1 t2 in
      let stat = (ty,t1,t2,o) in
      (* let w = compute_equality_weight stat in *)
      let w = 0 in 
      let proof = Equality.Exact p in
      let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
      (* to clean the local context of metas *)
      Equality.fix_metas bag maxmeta e
  | _ -> assert false
;;
 
let build_equality bag ty t1 t2 proof menv maxmeta =
  let o = !Utils.compare_terms t1 t2 in
  let stat = (ty,t1,t2,o) in
  let w = compute_equality_weight stat in
  let proof = Equality.Exact proof in
  let e = Equality.mk_equality bag (w, proof, stat, menv) in
  (* to clean the local context of metas *)
  Equality.fix_metas bag maxmeta e
;;

let tty_of_u u = 
  let t = CicUtil.term_of_uri u in
  let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
  t, ty
;;

let utty_of_u u =
  let t,ty = tty_of_u u in
  u, t, ty
;;
 
let is_monomorphic_eq (_,term,termty) = 
  let rec last = function
    | Cic.Prod(_,_,t) -> last t
    | t -> t
  in
  match last termty with
  | Cic.Appl [Cic.MutInd (_, _, []); Cic.Rel _; _; _] -> false
  | Cic.Appl [Cic.MutInd (_, _, []); _; _; _] -> true
  | _ -> false
;;

(*
let equations_blacklist =
 let blacklist = [
  "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
  "cic:/Coq/Init/Logic/trans_eq.con"; "cic:/Coq/Init/Logic/f_equal.con";
  "cic:/Coq/Init/Logic/f_equal2.con"; "cic:/Coq/Init/Logic/f_equal3.con";
  "cic:/Coq/Init/Logic/f_equal4.con"; "cic:/Coq/Init/Logic/f_equal5.con";
  "cic:/Coq/Init/Logic/sym_eq.con"; "cic:/Coq/Init/Logic/eq_ind.con";
  "cic:/Coq/Init/Logic/eq_ind_r.con"; "cic:/Coq/Init/Logic/eq_rec.con";
  "cic:/Coq/Init/Logic/eq_rec_r.con"; "cic:/Coq/Init/Logic/eq_rect.con";
  "cic:/Coq/Init/Logic/eq_rect_r.con"; "cic:/Coq/Logic/Eqdep/UIP.con";
  "cic:/Coq/Logic/Eqdep/UIP_refl.con";"cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
  "cic:/Coq/ZArith/Zcompare/rename.con";
  "cic:/Rocq/SUBST/comparith/mult_n_2.con";
  "cic:/matita/logic/equality/eq_f.con";"cic:/matita/logic/equality/eq_f2.con";
  "cic:/matita/logic/equality/eq_rec.con";
  "cic:/matita/logic/equality/eq_rect.con"; ]
 in
  List.fold_left
    (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
    UriManager.UriSet.empty blacklist
;;
*)
let equations_blacklist = UriManager.UriSet.empty;;

(* {{{ ****************** SATURATION STUFF ***************************)
exception UnableToSaturate of AutoCache.cache * int

let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;;

let saturate_term context metasenv oldnewmeta term cache auto fast = 
  let head, metasenv, args, newmeta =
    ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
  in
  let args_for_auto = 
    HExtlib.filter_map
      (function 
      | Cic.Meta(i,_) -> 
          let _,_,mt = CicUtil.lookup_meta i metasenv in
          let sort,u = 
            CicTypeChecker.type_of_aux' metasenv context mt 
              CicUniv.empty_ugraph
          in
          let b, _ = 
            CicReduction.are_convertible ~metasenv context 
              sort (Cic.Sort Cic.Prop) u
          in
          if b then Some i else None 
          (* maybe unif or conv should be used instead of = *)
      | _ -> assert false)
    args
  in
  let results,cache,newmeta = 
    if args_for_auto = [] then 
      let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
      [args,metasenv,newmetas,head,newmeta],cache,newmeta
    else
      let proof = 
        None,metasenv,term,term (* term non e' significativo *)
      in
      let flags = 
        if fast then
          {AutoTypes.default_flags() with 
           AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
           maxwidth = 2;maxdepth = 2;
           use_paramod=true;use_only_paramod=false}
        else
          {AutoTypes.default_flags() with
           AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
           maxwidth = 2;maxdepth = 4;
           use_paramod=true;use_only_paramod=false} 
      in
      match auto newmeta flags proof context cache args_for_auto with
      | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta))
      | substs,cache,newmeta ->
          List.map 
            (fun subst ->
              let metasenv = 
                CicMetaSubst.apply_subst_metasenv subst metasenv
              in
              let head = CicMetaSubst.apply_subst subst head in
              let newmetas = 
                List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv 
              in
              let args = List.map (CicMetaSubst.apply_subst subst) args in
              let newm = CicMkImplicit.new_meta metasenv subst in
              args,metasenv,newmetas,head,max newm newmeta)
            substs, cache, newmeta
  in
  results,cache,newmeta
;;
(* }}} ***************************************************************)

let find_context_equalities 
  maxmeta bag ?(auto = default_auto) context proof cache 
=
  prerr_endline "find_equalities";
  let module C = Cic in
  let module S = CicSubstitution in
  let module T = CicTypeChecker in
  let _,metasenv,_,_ = proof in
  let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
  let rec aux cache index newmeta = function
    | [] -> [], newmeta,cache
    | (Some (_, C.Decl (term)))::tl ->
        debug_print
          (lazy
             (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
        let do_find context term =
          match term with
          | C.Prod (name, s, t) when is_an_equality t ->
              (try 
                let term = S.lift index term in
                let saturated,cache,newmeta = 
                  saturate_term context metasenv newmeta term 
                    cache auto false
                in
                let eqs,newmeta = 
                  List.fold_left 
                   (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
                     let newmeta, equality = 
                       build_equality_of_hypothesis 
                         bag index head args newmetas (max newmeta newmeta')
                     in
                     equality::acc, newmeta + 1)
                   ([],newmeta) saturated
                in
                 eqs, newmeta, cache
              with UnableToSaturate (cache,newmeta) ->
                [],newmeta,cache)
          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
              when LibraryObjects.is_eq_URI uri ->
              let term = S.lift index term in
              let newmeta, e = 
                build_equality_of_hypothesis bag index term [] [] newmeta
              in
              [e], (newmeta+1),cache
          | _ -> [], newmeta, cache
        in 
        let eqs, newmeta, cache = do_find context term in
        let rest, newmeta,cache = aux cache (index+1) newmeta tl in
        List.map (fun x -> index,x) eqs @ rest, newmeta, cache
    | _::tl ->
        aux cache (index+1) newmeta tl
  in
  let il, maxm, cache = 
    aux cache 1 newmeta context 
  in
  let indexes, equalities = List.split il in
  indexes, equalities, maxm, cache
;;

let find_library_equalities bag
  ?(auto = default_auto) caso_strano dbd context status maxmeta cache 
= 
  let module C = Cic in
  let module S = CicSubstitution in
  let module T = CicTypeChecker in
  let proof, goalno = status in
  let _,metasenv,_,_ = proof in
  let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
  let signature = 
    if caso_strano then
      begin
        match ty with
        | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] ->
            (let mainl, sigl = MetadataConstraints.signature_of l in
            let mainr, sigr = MetadataConstraints.signature_of r in
            match mainl,mainr with
            | Some (uril,tyl), Some (urir, tyr) 
                when LibraryObjects.is_eq_URI uril && 
                     LibraryObjects.is_eq_URI urir && 
                     tyl = tyr ->
                  Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr)
            | _ -> 
                let u = (UriManager.uri_of_string
                  (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in
                let main = Some (u, []) in
                Some (main,MetadataConstraints.UriManagerSet.union sigl sigr))
        | _ -> assert false
      end
    else
      None
 in
 let eqs = MetadataQuery.equations_for_goal ~dbd ?signature status in
 let candidates = List.map utty_of_u eqs in
 let candidates = List.filter is_monomorphic_eq candidates in
 let candidates = List.filter is_var_free candidates in
 let rec aux cache newmeta = function
    | [] -> [], newmeta, cache
    | (uri, term, termty)::tl ->
        debug_print
          (lazy
             (Printf.sprintf "Examining: %s (%s)"
                (CicPp.ppterm term) (CicPp.ppterm termty)));
        let res, newmeta, cache = 
          match termty with
          | C.Prod (name, s, t) ->
              (try
                let saturated,cache,newmeta = 
                  saturate_term context metasenv newmeta termty 
                    cache auto true
                in
                let eqs,newmeta = 
                  List.fold_left 
                   (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
                     match head with
                     | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
                       when LibraryObjects.is_eq_URI uri ->
                         let proof = C.Appl (term::args) in
                         let maxmeta, equality = 
                           build_equality bag ty t1 t2 proof newmetas 
                             (max newmeta newmeta')
                         in
                         equality::acc,maxmeta + 1
                     | _ -> assert false)
                   ([],newmeta) saturated
                in
                 eqs, newmeta , cache
              with UnableToSaturate (cache,newmeta) ->
                [], newmeta , cache)
          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> 
              let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
              [e], newmeta+1, cache
          | _ -> assert false
        in
        let res = List.map (fun e -> uri, e) res in
        let tl, newmeta, cache = aux cache newmeta tl in
        res @ tl, newmeta, cache
  in
  let found, maxm, cache = 
    aux cache maxmeta candidates 
  in
  let uriset, eqlist = 
    let mceq = Equality.meta_convertibility_eq in
    (List.fold_left
       (fun (s, l) (u, e) ->
          if List.exists (mceq e) (List.map snd l) then (
            debug_print
              (lazy
                 (Printf.sprintf "NO!! %s already there!"
                    (Equality.string_of_equality e)));
            (UriManager.UriSet.add u s, l)
          ) else (UriManager.UriSet.add u s, (u, e)::l))
       (UriManager.UriSet.empty, []) found)
  in
  uriset, eqlist, maxm, cache
;;