(*
    ||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 $ *)

let debug s = prerr_endline (Lazy.force s);;
let debug _ = ();;

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 empty_db = DB.empty,DB.empty

class status =
 object
  val db = empty_db
  method coerc_db = db
  method set_coerc_db v = {< db = v >}
  method set_coercion_status
   : 'status. < coerc_db : db; .. > as 'status -> 'self
   = fun o -> {< db = o#coerc_db >}
 end

let index_coercion status c src tgt arity arg =
  let db_src,db_tgt = status#coerc_db in
  let data = (c,arity,arg) in

  debug (lazy ("INDEX:" ^ 
    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
    NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^ 
    string_of_int arg ^ " " ^ string_of_int arity));

  let db_src = DB.index db_src src data in
  let db_tgt = DB.index db_tgt tgt data in
  status#set_coerc_db (db_src, db_tgt)
;;

let index_old_db odb (status : #status) =
  List.fold_left 
    (fun status (_,tgt,clist) -> 
       List.fold_left 
         (fun status (uri,_,arg) ->
           try
            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
(*
            debug (lazy (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 -> 
                  debug (lazy (
                    NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t));
                  assert false
            in
            index_coercion status c src tgt arity arg
           with 
           | NCicEnvironment.BadDependency _ 
           | NCicTypeChecker.TypeCheckerFailure _ -> status)
         status clist)
    status (CoercDb.to_list odb)
;;

let look_for_coercion status metasenv subst context infty expty =
 let db_src,db_tgt = status#coerc_db in
  match infty, expty with
  | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), 
    (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] 
  | _ ->

    debug (lazy ("LOOK FOR COERCIONS: " ^ 
      NCicPp.ppterm ~metasenv ~subst ~context infty ^ "  |===> " ^
      NCicPp.ppterm ~metasenv ~subst ~context 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

    debug (lazy ("CANDIDATES: " ^ 
      String.concat "," (List.map (fun (t,_,_) ->
        NCicPp.ppterm ~metasenv ~subst ~context t) 
      (CoercionSet.elements candidates))));

    List.map
      (fun (t,arity,arg) ->
          let ty =
            try NCicTypeChecker.typeof ~metasenv:[] ~subst:[] [] t 
            with NCicTypeChecker.TypeCheckerFailure s ->
             prerr_endline ("illtyped coercion: "^Lazy.force s);
             prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
             assert false
          in
          let ty, metasenv, args = 
           NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty arity
          in

          debug (lazy (
            NCicPp.ppterm ~metasenv ~subst:[] ~context:[] ty ^ " --- " ^ 
            NCicPp.ppterm ~metasenv ~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)
;;