(* Copyright (C) 2005, 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://helm.cs.unibo.it/
 *)

(* $Id$ *)

type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
exception EqCarrNotImplemented of string Lazy.t
exception EqCarrOnNonMetaClosed

let db = ref []

let coerc_carr_of_term t =
 try
  match t with
     Cic.Sort s -> Sort s
   | Cic.Appl (t::_)
   | t -> Uri (CicUtil.uri_of_term t)
 with Invalid_argument _ ->
  Term t
;;

let uri_of_carr = function
  | Uri u -> Some u
  | _ -> None

let rec name_of_carr = function
  | Uri u -> UriManager.name_of_uri u
  | Sort s -> CicPp.ppsort s
  | Term (Cic.Appl ((Cic.Const (uri, _))::_)) 
  | Term (Cic.Appl ((Cic.MutInd (uri, _, _))::_)) 
  | Term (Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_)) -> 
        UriManager.name_of_uri uri
  | Term (Cic.Prod (_,_,t)) -> name_of_carr (Term t)
  | Term t -> 
      prerr_endline ("CoercDb.name_of_carr:" ^ CicPp.ppterm t); 
      "FixTheNameMangler"

let eq_carr src tgt =
  match src, tgt with
  | Uri src, Uri tgt -> UriManager.eq src tgt
  | Sort (Cic.Type _), Sort (Cic.Type _) -> true
  | Sort src, Sort tgt when src = tgt -> true
  | Term t1, Term t2 ->
      if t1 = t2 then true
      else
        if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then
          raise 
          (EqCarrNotImplemented 
          (lazy ("Unsupported carr for coercions: " ^ 
          CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
      else raise EqCarrOnNonMetaClosed
  | _, _ -> false

let to_list () =
  !db

let rec myfilter p = function
  | [] -> []
  | (s,t,l)::tl ->
      let l = List.filter (fun u -> not (p (s,t,u))) l in
      if l = [] then myfilter p tl else (s,t,l)::myfilter p tl
;;
  
let remove_coercion p = db := myfilter p !db;;

let find_coercion f =
  List.flatten 
    (List.map 
      (fun (_,_,x) -> x) 
      (List.filter (fun (s,t,_) -> f (s,t)) !db))
;;

let is_a_coercion u = 
  List.exists (fun (_,_,xl) -> List.exists (UriManager.eq u) xl) !db
;;

let get_carr uri =
  try
    let src, tgt, _ = 
      List.find (fun (_,_,xl) -> List.exists (UriManager.eq uri) xl) !db 
    in
    src, tgt
  with Not_found -> assert false (* uri must be a coercion *)
;;

let term_of_carr = function
  | Uri u -> CicUtil.term_of_uri u
  | Sort s -> Cic.Sort s
  | Term _ -> assert false
;;
  
let add_coercion (src,tgt,u) =
  let f s t = eq_carr s src && eq_carr t tgt in
  let where = List.filter (fun (s,t,_) -> f s t) !db in
  let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in
  match where with
  | [] -> db := (src,tgt,[u]) :: !db
  | (src,tgt,l)::tl ->
      assert (tl = []); (* not sure, this may be a feature *)
      db := (src,tgt,u::l)::tl @ rest
;;