(* Copyright (C) 2000, 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/.
 *)

(* $Id$ *)

open Printf;;

type coercion_search_result = 
     (* metasenv, last coercion argument, fully saturated coercion *)
     (* to apply the coercion it is sufficient to unify the last coercion
        argument (that is a Meta) with the term to be coerced *)
  | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
  | NoCoercion
  | NotMetaClosed
  | NotHandled of string Lazy.t

let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()

(* searches a coercion fron src to tgt in the !coercions list *)
let look_for_coercion' metasenv subst context src tgt =
  try 
    let l = 
      CoercDb.find_coercion 
        (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in
    let uri =
     match l with
     | [] -> 
         debug_print 
           (lazy 
             (sprintf ":-( coercion non trovata da %s a %s" 
               (CoercDb.name_of_carr src) 
               (CoercDb.name_of_carr tgt)));
         None
     | _::_ -> 
         debug_print (lazy (
           sprintf ":-) TROVATE %d coercion(s) da %s a %s" 
             (List.length l)
             (CoercDb.name_of_carr src) 
             (CoercDb.name_of_carr tgt)));
         Some l
    in
     (match uri with
         None -> NoCoercion
       | Some ul ->
          let cl = List.map CicUtil.term_of_uri ul in
          let funclass_arityl = 
            let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
            List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
          in
          let freshmeta = CicMkImplicit.new_meta metasenv subst in
          let newtl =
           List.map2
            (fun arity c -> 
              let ty,_ =
               CicTypeChecker.type_of_aux' ~subst metasenv context c
                CicUniv.empty_ugraph in
              let _,metasenv,args,lastmeta =
               TermUtil.saturate_term freshmeta metasenv context ty arity in
              let irl =
               CicMkImplicit.identity_relocation_list_for_metavariable context
              in
               metasenv, Cic.Meta (lastmeta-1,irl),
                match args with
                   [] -> c
                 | _ -> Cic.Appl (c::args)
            ) funclass_arityl cl
          in
           SomeCoercion newtl)
  with
    | CoercDb.EqCarrNotImplemented s -> NotHandled s
    | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
;;

let look_for_coercion metasenv subst context src tgt = 
  let src_uri = CoercDb.coerc_carr_of_term src in
  let tgt_uri = CoercDb.coerc_carr_of_term tgt in
  look_for_coercion' metasenv subst context src_uri tgt_uri

let source_of t = 
  try
    let uri = CicUtil.uri_of_term t in
    CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
  with Invalid_argument _ -> assert false (* t must be a coercion *)

let generate_dot_file () =
  let module Pp = GraphvizPp.Dot in
  let buf = Buffer.create 10240 in
  let fmt = Format.formatter_of_buffer buf in
  Pp.header ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
    ~edge_attrs:["fontsize", "10"] fmt;
  let l = CoercDb.to_list () in
  let pp_description carr =
    match CoercDb.uri_of_carr carr with
    | None -> ()
    | Some uri ->
        Pp.node (CoercDb.name_of_carr carr)
          ~attrs:["href", UriManager.string_of_uri uri] fmt in
  List.iter
    (fun (src, tgt, cl) ->
      let src_name = CoercDb.name_of_carr src in
      let tgt_name = CoercDb.name_of_carr tgt in
      pp_description src;
      pp_description tgt;
      List.iter
        (fun c ->
          Pp.edge src_name tgt_name
            ~attrs:[ "label", UriManager.name_of_uri c;
              "href", UriManager.string_of_uri c ]
            fmt)
        cl)
    l;
  Pp.trailer fmt;
  Buffer.contents buf
;;
    
let is_composite t =
  try
    let uri = 
      match t with 
      | Cic.Appl (he::_) -> CicUtil.uri_of_term he
      | _ -> CicUtil.uri_of_term t
    in
    match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
    | Cic.Constant (_,_, _, _, attrs),_  ->
        List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
    | _ -> false
  with Invalid_argument _ -> false
;;

let uniq = HExtlib.list_uniq ~eq:(fun (a,_) (b,_) -> CoercDb.eq_carr a b);;

let splat e l = List.map (fun x -> e, x) l;;

let get_coercions_to carr = 
  let l = CoercDb.to_list () in
  List.flatten 
    (HExtlib.filter_map 
      (fun (src,tgt,cl) -> 
        if CoercDb.eq_carr tgt carr then Some (splat src cl) else None) 
      l)
;;

let get_coercions_from carr = 
  let l = CoercDb.to_list () in
  List.flatten 
    (HExtlib.filter_map 
      (fun (src,tgt,cl) -> 
        if CoercDb.eq_carr src carr then Some (splat tgt cl) else None) 
      l)
;;

let intersect l1 l2 = 
  let is_in_l1 (x,_) = List.exists (fun (src,_) -> CoercDb.eq_carr x src) l1 in
  uniq (List.filter is_in_l1 l2)
;;

let grow s = 
  uniq (List.flatten (List.map (fun (x,_) -> get_coercions_to x) s) @ s)
;;

let lb c = 
  let l = get_coercions_from c in
  function x -> List.exists (fun (y,_) -> CoercDb.eq_carr x y) l
;;

let rec min acc = function
  | c::tl -> 
    if List.exists (lb c) (tl@acc) then min acc tl else min (c::acc) tl
  | [] -> acc
;;

let meets left right =
  let u = UriManager.uri_of_string "cic:/foo.con" in
  min [] (List.map fst (intersect (grow [left,u]) (grow [right,u])))
;;

(* EOF *)