(*
    ||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 * int * int = 
  struct
        type t = NCic.term * int * int
        let compare = Pervasives.compare
  end

module CoercionSet = Set.Make(COT)

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

type db = DB.t * DB.t

let index_coercion (db_src,db_tgt) c src tgt arity arg =
  let data = (c,arity,arg) in
  let db_src = DB.index db_src src data in
  let db_tgt = DB.index db_tgt tgt data in
  db_src, db_tgt
;;

let 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
              match NCicMetaSubst.saturate ~delta:max_int [] [] cty (arity+1) 
              with
              | NCic.Prod (_, src, tgt),_,_ -> 
                src, NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) tgt 
              | t,metasenv,_ -> 
                  prerr_endline (
                    NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
                  assert false
            in
(*
            prerr_endline (Printf.sprintf "indicizzo %s %d %d" 
              (UriManager.string_of_uri uri) arity arg);
*)
            index_coercion db c src tgt arity arg)
         db clist)
    (DB.empty,DB.empty) (CoercDb.to_list ())
;;

(* XXX saturate takes no subst!!!! *)
let look_for_coercion (db_src,db_tgt) metasenv _subst context infty expty =
  let set_src = DB.retrieve_unifiables db_src infty in
  let set_tgt = DB.retrieve_unifiables db_tgt expty in
  let candidates = CoercionSet.inter set_src set_tgt in
  prerr_endline "aaaaaaaaaaaaa";
  List.map
    (fun (t,arity,arg) ->
        let ty = NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t in
        let ty, metasenv, args = 
          NCicMetaSubst.saturate ~delta:max_int metasenv context ty arity
        in
        prerr_endline (
          NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ 
          NCicPp.ppterm ~metasenv ~subst:_subst ~context
          (NCicUntrusted.mk_appl t args) ^ " --- " ^ 
            string_of_int (List.length args) ^ " == " ^ string_of_int arg);
        metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg)
    (CoercionSet.elements candidates)
;;