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


module Codomain = struct 
  type t = Cic.term 
  let compare = Pervasives.compare 
end
module S = Set.Make(Codomain)
module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
type universe = TI.t

let empty_universe = TI.empty
let get_candidates universe ty = 
  S.elements (TI.retrieve_unifiables universe ty)
;;
let rec head = function 
  | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t)
  | t -> t
;;
let index acc key term =
  match key with
  | Cic.Meta _ -> acc
  | _ -> 
      prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
      TI.index acc key term
;;
let universe_of_goals dbd proof gl universe = 
  let univ = MetadataQuery.universe_of_goals ~dbd proof gl in
  let terms = List.map CicUtil.term_of_uri univ in
  let tyof t = fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)in
  List.fold_left 
    (fun acc term -> 
      let key = head (tyof term) in
      index acc key term)
    universe terms
;;
let universe_of_context ctx metasenv universe =  
  let tail = function [] -> [] | h::tl -> tl in
  let rc,_,_ = 
    List.fold_left 
    (fun (acc,i,ctx) ctxentry ->
      match ctxentry with
      | Some (_,Cic.Decl t) -> 
          let key = CicSubstitution.lift i (head t) in
          let elem = Cic.Rel i in
          index acc key elem, i+1, tail ctx
      | Some (_,Cic.Def (_,Some t)) ->
          let key = CicSubstitution.lift i (head t) in
          let elem = Cic.Rel i in
          index acc key elem, i+1, tail ctx
      | Some (_,Cic.Def (t,None)) ->
          let ctx = tail ctx in 
          let key,_ = 
            CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph
          in
          let elem = Cic.Rel i in
          let key = CicSubstitution.lift i (head key) in
          index acc key elem, i+1, ctx
      |  _ -> universe,i+1,tail ctx)
    (universe,1,ctx) ctx
  in
  rc
;;
let add_to_universe key proof universe =
  index universe key proof
;;

(* (proof,ty) list *)
type cache_key = Cic.term
type cache_elem = 
  | Failed_in of int
  | Succeded of Cic.term
  | UnderInspection
  | Notfound
type cache = (cache_key * cache_elem) list
let cache_examine cache cache_key = 
  try List.assoc cache_key cache with Not_found -> Notfound
;;
let cache_replace cache key v =
  let cache = List.filter (fun (i,_) -> i <> key) cache in
  (key,v)::cache
;;
let cache_add_failure cache cache_key depth =
  match cache_examine cache cache_key with
  | Failed_in i when i > depth -> cache
  | Notfound  
  | Failed_in _ 
  | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
  | Succeded t -> 
      prerr_endline (CicPp.ppterm t);
      assert false (* if succed it can't fail *)
;;
let cache_add_success cache cache_key proof =
  match cache_examine cache cache_key with
  | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
  | UnderInspection -> cache_replace cache cache_key (Succeded proof)
  | Succeded t -> (* we may decide to keep the smallest proof *) cache
  | Notfound -> cache_replace cache cache_key (Succeded proof)
;;
let cache_add_underinspection cache cache_key depth =
  match cache_examine cache cache_key with
  | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
  | Notfound -> (cache_key,UnderInspection)::cache
  | Failed_in _ 
  | UnderInspection 
  | Succeded _ -> assert false (* it must be a new goal *)
;;
let cache_empty = []
let cache_print context cache = 
  let names = List.map (function None -> None | Some (x,_) -> Some x) context in
  String.concat "\n" 
    (HExtlib.filter_map 
      (function 
        | (k,Succeded _) -> Some (CicPp.pp k names)
        | _ -> None)
      cache)
;;
let cache_size cache = 
  List.length (List.filter (function (_,Succeded _) -> true | _ -> false) cache)
;;
let cache_clean cache = 
  List.filter (function (_,Succeded _) -> true | _ -> false) cache
;;

type flags = {
  maxwidth: int;
  maxdepth: int;
  timeout: float;
  use_paramod: bool;
  use_only_paramod : bool;
}

let default_flags _ =
  {maxwidth=3;maxdepth=3;timeout=Unix.gettimeofday() +. 3.0;use_paramod=true;use_only_paramod=false}
;;

(* (metasenv, subst, (metano,depth)list *)
type sort = P | T;;
type and_elem =  Cic.metasenv * Cic.substitution * (int * int * sort) list
type auto_result = 
  | Fail of string 
  | Success of Cic.metasenv * Cic.substitution * and_elem list