(* $Id$ *)
+let debug = false
+let debug_print =
+ if debug then fun x -> prerr_endline (Lazy.force x)
+ else ignore
+;;
+
type coerc_carr =
| Uri of UriManager.uri
| Sort of Cic.sort
- | Term of Cic.term
| Fun of int
+ | Dead
;;
-exception EqCarrNotImplemented of string Lazy.t
-exception EqCarrOnNonMetaClosed
+type saturations = int
+type coerced_pos = int
+type coercion_entry =
+ coerc_carr * coerc_carr * UriManager.uri * saturations * coerced_pos
+
+type coerc_db = (* coercion_entry grouped by carrier with molteplicity *)
+ (coerc_carr * coerc_carr *
+ (UriManager.uri * int * saturations * coerced_pos) list) list
-let db = ref []
+let db = ref ([] : coerc_db)
+let dump () = !db
+let restore coerc_db = db := coerc_db
+let empty_coerc_db = []
-let coerc_carr_of_term t =
+let rec coerc_carr_of_term t a =
try
- match t with
- | Cic.Sort s -> Sort s
- | Cic.Prod _ -> Fun 0
- | Cic.Appl (t::_)
- | t -> Uri (CicUtil.uri_of_term t)
- with Invalid_argument _ ->
- Term t
+ match t, a with
+ | Cic.Sort s, 0 -> Sort s
+ | Cic.Appl (t::_), 0 -> coerc_carr_of_term t a
+ | t, 0 -> Uri (CicUtil.uri_of_term t)
+ | _, n -> Fun n
+ with Invalid_argument _ -> Dead
;;
-let uri_of_carr = function
- | Uri u -> Some u
- | _ -> None
-
-let rec name_of_carr = function
+let string_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
+ | Dead -> "UnsupportedCarrier"
;;
let eq_carr ?(exact=false) src tgt =
match src, tgt with
| Uri src, Uri tgt ->
let coarse_eq = UriManager.eq src tgt in
- let src_noxpointer = UriManager.strip_xpointer src in
- if exact && coarse_eq && UriManager.uri_is_ind src_noxpointer then
- match
- fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph src_noxpointer)
- with
- | Cic.InductiveDefinition (_,[],m,_) when m = 0 -> true
- | Cic.Constant _ -> true
- | _ -> false
- else
- 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
+ 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 _, Sort _ -> true
+ | Fun _,Fun _ when not exact -> true (* only one Funclass *)
+ | Fun i,Fun j when i = j -> true (* only one Funclass *)
| _, _ -> false
;;
-let to_list () =
- List.map (fun (s,t,l) -> s,t,List.map fst l) !db
+let to_list db =
+ List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b,c -> a,b,c) l) db
;;
let rec myfilter p = function
| (s,t,l)::tl ->
let l =
HExtlib.filter_map
- (fun (u,n) ->
- if p (s,t,u) then
- if n = 1 then
- None
- else
- Some (u,n-1)
- else
- Some (u,n))
+ (fun (u,n,saturations,cpos) as e ->
+ if p (s,t,u,saturations,cpos) then
+ if n = 1 then None
+ else Some (u,n-1,saturations,cpos)
+ else Some e)
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
- fst
- (List.flatten
+ 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 =
+let is_a_coercion t =
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 uri = CicUtil.uri_of_term t in
+ match
+ HExtlib.filter_map
+ (fun (src,tgt,xl) ->
+ let xl = List.filter (fun (x,_,_,_) -> UriManager.eq uri x) xl in
+ if xl = [] then None else Some (src,tgt,xl))
+ !db
+ with
+ | [] -> None
+ | (_,_,[])::_ -> assert false
+ | [src,tgt,[u,_,s,p]] -> Some (src,tgt,u,s,p)
+ | (src,tgt,(u,_,s,p)::_)::_ ->
+ debug_print
+ (lazy "coercion has multiple entries, returning the first one");
+ Some (src,tgt,u,s,p)
+ with Invalid_argument _ ->
+ debug_print (lazy "this term is not a constant");
+ None
;;
-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) =
+let add_coercion (src,tgt,u,saturations,cpos) =
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]) :: !db
+ | [] -> db := (src,tgt,[u,1,saturations,cpos]) :: !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) -> if UriManager.eq u x then (x,n+1) else (x,n))
+ if List.exists (fun (x,_,_,_) -> UriManager.eq u x) l then
+ let l =
+ let l =
+ (* this code reorders the list so that adding an already declared
+ * coercion moves it to the begging of the list *)
+ let item = List.find (fun (x,_,_,_) -> UriManager.eq u x) l in
+ let rest=List.filter (fun (x,_,_,_) -> not (UriManager.eq u x)) l in
+ item :: rest
+ in
+ List.map
+ (fun (x,n,x_saturations,x_cpos) as e ->
+ if UriManager.eq u x then
+ (* not sure, this may be a feature *)
+ (assert (x_saturations = saturations && x_cpos = cpos);
+ (x,n+1,saturations,cpos))
+ else e)
l
in
- db := (src,tgt,l')::tl @ rest
+ db := (src,tgt,l)::tl @ rest
else
- db := (src,tgt,(u,1)::l)::tl @ rest
-
+ db := (src,tgt,(u,1,saturations,cpos)::l)::tl @ rest
;;
-
-
+let prefer u =
+ let prefer (s,t,l) =
+ let lb,la = List.partition (fun (uri,_,_,_) -> UriManager.eq uri u) l in
+ s,t,lb@la
+ in
+ db := List.map prefer !db;
+;;