(* 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
  | Fun of int 
;;

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.Prod _ -> Fun 0 
     (* BUG: this should be the real arity. The computation
      requires menv, context etc.., but since carrs are compared discharging Fun
      arity... it works *)
   | 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"
  | Fun i -> "FunClass_" ^ string_of_int i   
;;

let eq_carr ?(exact=false) src tgt =
  match src, tgt with
  | Uri src, Uri tgt -> 
      let coarse_eq = UriManager.eq src tgt in
      let t = CicUtil.term_of_uri src in
      let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
      (match ty, exact with
      | Cic.Prod _, true -> false
      | Cic.Prod _, false -> coarse_eq
      | _ -> coarse_eq) 
  | 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
  | Fun _,Fun _ -> true (* only one Funclass? *)
(*   | Fun i,Fun j when i=j -> true *)
  | Term t, _
  | _, Term t when not (CicUtil.is_meta_closed t) -> raise EqCarrOnNonMetaClosed
  | _, _ -> false
;;

let to_list () =
  List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b -> a,b) l) !db
;;

let rec myfilter p = function
  | [] -> []
  | (s,t,l)::tl ->
      let l = 
        HExtlib.filter_map 
          (fun (u,n,saturations) -> 
            if p (s,t,u,saturations) then
              if n = 1 then
                None
              else
                Some (u,n-1,saturations)
            else
              Some (u,n,saturations)) 
          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.map
    (fun uri,_,saturations -> uri,saturations)
    (List.flatten
    (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db))
;;

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

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

let is_a_coercion' t = 
  try
    let uri = CicUtil.uri_of_term t in
     is_a_coercion uri
  with Invalid_argument _ -> false
;;

let is_a_coercion_to_funclass t =
  try
    let uri = CicUtil.uri_of_term t in
    match snd (get_carr uri) with
    | Fun i -> Some i
    | _ -> None
  with Invalid_argument _ -> None
  

let term_of_carr = function
  | Uri u -> CicUtil.term_of_uri u
  | Sort s -> Cic.Sort s
  | Fun _ -> assert false
  | Term _ -> assert false
;;
  
let add_coercion (src,tgt,u,saturations) =
  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,1,saturations]) :: !db
  | (src,tgt,l)::tl ->
      assert (tl = []); (* not sure, this may be a feature *)
      if List.exists (fun (x,_,_) -> UriManager.eq u x) l then
        let l' = List.map
          (fun (x,n,saturations') ->
            if UriManager.eq u x then
             (x,n+1,saturations)
            else
             (x,n,saturations))
          l
        in
        db := (src,tgt,l')::tl @ rest
      else
        db := (src,tgt,(u,1,saturations)::l)::tl @ rest
      
;;

type coerc_db = (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list 
let dump () = !db 
let restore coerc_db = db := coerc_db