(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id: nCicRefiner.mli 9227 2008-11-21 16:00:06Z tassi $ *)

module COT : Set.OrderedType with type t = NCic.term = 
  struct
        type t = NCic.term
        let compare = Pervasives.compare
  end

module HintSet = Set.Make(COT)

module DB = 
  Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(HintSet)

type db = DB.t

let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;

let index_hint hdb context t1 t2 =
  let pair' = pair t1 t2 in
  let data = 
    List.fold_left 
     (fun t (n,e) -> 
        match e with
        | NCic.Decl ty -> NCic.Prod (n,ty,t)
        | _ -> assert false) 
      pair' context in
  let src = 
    List.fold_left 
     (fun t (_,e) -> 
        match e with
        | NCic.Decl _ -> NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t
        | _ -> assert false) 
     pair' context in
  let _ = prerr_endline ("SONO PASSATO DI QUI") in

(*
  prerr_endline ("INDEX:" ^ 
    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c);
*)
  DB.index hdb src data
;;

let empty_db = DB.empty ;;

let db () = 
  try let _,_,_,x,_,_ = NCicEnvironment.get_checked_def
    (NReference.reference_of_string "cic:/matita/tests/pullback/xxx.def(0)")
  in
    prerr_endline "iiiiiiiiiiiiiiiiii";
  let rec decontextualize ctx = function
    | NCic.Prod (n,s,t) -> decontextualize ((n,NCic.Decl s)::ctx) t
    | t -> ctx, t
  in
    match (decontextualize [] x) with
    | ctx, NCic.Appl [_;_;a;b] -> index_hint empty_db ctx a b
    | _ -> assert false
  with exn -> prerr_endline ("PIPPO" ^ Printexc.to_string exn); empty_db
  
(*  List.fold_left 
    (fun db (_,tgt,clist) -> 
       List.fold_left 
         (fun db (uri,_,arg) ->
            let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
            let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
            let src, tgt = 
              let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in
              let scty, metasenv,_ = 
                NCicMetaSubst.saturate ~delta:max_int [] [] [] cty (arity+1) 
              in
              match scty with
              | NCic.Prod (_, src, tgt) -> 
                 let tgt =
                   NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt
                 in
(*
            prerr_endline (Printf.sprintf "indicizzo %s (%d) : %s ===> %s" 
              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] scty) (arity+1)
              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] src)
              (NCicPp.ppterm ~metasenv ~subst:[] ~context:[] tgt));
*)
                src, tgt
              | t -> 
                  prerr_endline (
                    NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
                  assert false
            in
            index_coercion db c src tgt arity arg)
         db clist)
    (DB.empty,DB.empty) (CoercDb.to_list ())
 *)
;;


let look_for_hint hdb metasenv subst context t1 t2 =

  let candidates = DB.retrieve_unifiables hdb (pair t1 t2) in
  let res = List.map
      (fun ty ->
          let ty, metasenv, _ = 
           NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0 
          in
          match ty with
          | NCic.Appl [_; t1; t2] -> 
          prerr_endline ("candidate1: " ^ NCicPp.ppterm ~metasenv ~subst ~context t1);
          prerr_endline ("candidate2: " ^ NCicPp.ppterm ~metasenv ~subst ~context t2);
              
              metasenv, t1, t2
          | _ -> assert false)
      (HintSet.elements candidates)
  in
  let _ = prerr_endline ("DENTRO RICERCA: " ^ (string_of_int (List.length res))) in
  res
;;