* 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 use_coercions = ref true
let coerc_carr_of_term t =
try
with Invalid_argument _ ->
match t with
| Cic.Sort s -> Sort s
+ | Cic.Appl ((Cic.Const (uri, _))::_)
+ | Cic.Appl ((Cic.MutInd (uri, _, _))::_)
+ | Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_) -> Uri uri
| t -> Term t
;;
+let 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 t -> (* CicPp.ppterm t *) assert false
+
let eq_carr src tgt =
match src, tgt with
| Uri src, Uri tgt -> UriManager.eq src tgt
else raise EqCarrOnNonMetaClosed
| _, _ -> false
-let name_of_carr = function
- | Uri u -> UriManager.name_of_uri u
- | Sort s -> CicPp.ppsort s
- | Term t -> CicPp.ppterm t
-
-
let to_list () =
!db
db := List.filter (fun u -> not(p u)) !db
let find_coercion f =
- if !use_coercions then
- List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
- else []
+ List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
+
+let is_a_coercion u =
+ List.exists (fun (_,_,x) -> UriManager.eq x u) !db
+
+let get_carr uri =
+ try
+ let src, tgt, _ = List.find (fun (_,_,x) -> UriManager.eq x uri) !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
+
+