open Printf;;
+type coercion_search_result =
+ | SomeCoercion of Cic.term
+ | NoCoercion
+ | NotMetaClosed
+ | NotHandled of string Lazy.t
+
let debug = false
-let debug_print = if debug then prerr_endline else ignore
+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 src tgt =
- try
- let src = UriManager.uri_of_string (CicUtil.uri_of_term src) in
- let tgt = UriManager.uri_of_string (CicUtil.uri_of_term tgt) in
- let l =
- CoercDb.find_coercion
- (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt)
- in
- match l with
- | [] -> prerr_endline ":( coercion non trovata"; None
- | u::_ ->
- debug_print (
- sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
- (List.length l)
- (UriManager.name_of_uri src)
- (UriManager.name_of_uri tgt)
- (UriManager.name_of_uri u));
- Some (CicUtil.term_of_uri (UriManager.string_of_uri u))
- with Invalid_argument s ->
- debug_print (":( coercion non trovata (fallita la uri_of_term): " ^ s);
- None
+ try
+ let l =
+ CoercDb.find_coercion
+ (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt)
+ in
+ match l with
+ | [] ->
+ debug_print
+ (lazy
+ (sprintf ":-( coercion non trovata da %s a %s"
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)));
+ NoCoercion
+ | [u] ->
+ debug_print (lazy (
+ sprintf ":-) TROVATA 1 coercion da %s a %s: %s"
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)
+ (UriManager.name_of_uri u)));
+ SomeCoercion (CicUtil.term_of_uri u)
+ | u::_ ->
+ debug_print (lazy (
+ sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s"
+ (List.length l)
+ (CoercDb.name_of_carr src)
+ (CoercDb.name_of_carr tgt)
+ (UriManager.name_of_uri u)));
+ SomeCoercion (CicUtil.term_of_uri u)
+ with
+ | CoercDb.EqCarrNotImplemented s -> NotHandled s
+ | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed
;;
+let look_for_coercion 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 src_uri tgt_uri
+
(* given the new coercion uri from src to tgt returns the list
* of new coercions to create. hte list elements are
* (source, list of coercions to follow, target)
*)
let get_closure_coercions src tgt uri coercions =
- let c_from_tgt = List.filter (fun (f,_,_) -> UriManager.eq f tgt) coercions in
- let c_to_src = List.filter (fun (_,t,_) -> UriManager.eq t src) coercions in
- (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
- (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
- (List.fold_left (
- fun l (s,_,u1) ->
- ((List.map (fun (_,t,u2) ->
- (s,[u1;uri;u2],t)
- )c_from_tgt)@l) )
- [] c_to_src)
+ let eq_carr s t =
+ try
+ CoercDb.eq_carr s t
+ with
+ | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
+ in
+ match src,tgt with
+ | CoercDb.Uri _, CoercDb.Uri _ ->
+ let c_from_tgt =
+ List.filter (fun (f,_,_) -> eq_carr f tgt) coercions
+ in
+ let c_to_src =
+ List.filter (fun (_,t,_) -> eq_carr t src) coercions
+ in
+ (List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
+ (List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
+ (List.fold_left (
+ fun l (s,_,u1) ->
+ ((List.map (fun (_,t,u2) ->
+ (s,[u1;uri;u2],t)
+ )c_from_tgt)@l) )
+ [] c_to_src)
+ | _ -> [] (* do not close in case source or target is not an indty ?? *)
;;
let obj_attrs = [`Class `Coercion; `Generated]
try
CicTypeChecker.type_of_aux' [] [] c univ
with CicTypeChecker.TypeCheckerFailure s as exn ->
- debug_print (sprintf "Generated composite coercion:\n%s\n%s"
- (CicPp.ppterm c) s);
+ debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s"
+ (CicPp.ppterm c) (Lazy.force s)));
raise exn
in
let cleaned_ty =
List.filter (
fun (src,_,tgt) ->
not (List.exists (fun (s,t,u) ->
- UriManager.eq s src &&
- UriManager.eq t tgt)
+ CoercDb.eq_carr s src &&
+ CoercDb.eq_carr t tgt)
coercions))
l
+let term_of_carr = function
+ | CoercDb.Uri u -> CicUtil.term_of_uri u
+ | CoercDb.Sort _ -> assert false
+ | CoercDb.Term _ -> assert false
+
(* given a new coercion uri from src to tgt returns
* a list of (new coercion uri, coercion obj, universe graph)
*)
match l with
| [] -> assert false
| he :: tl ->
- let term_of_uri' uri =
- CicUtil.term_of_uri (UriManager.string_of_uri uri)
- in
let first_step =
- Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [],
- obj_attrs)
+ Cic.Constant ("",
+ Some (term_of_carr (CoercDb.Uri he)), Cic.Sort Cic.Prop, [], obj_attrs)
in
let o,u =
- List.fold_left (fun (o,u) coer ->
+ List.fold_left (fun (o,univ) coer ->
match o with
| Cic.Constant (_,Some c,_,[],_) ->
- generate_composite_closure c (term_of_uri' coer) u
+ generate_composite_closure c (term_of_carr (CoercDb.Uri
+ coer)) univ
| _ -> assert false
) (first_step, CicUniv.empty_ugraph) tl
in
- let name_src = UriManager.name_of_uri src in
- let name_tgt = UriManager.name_of_uri tgt in
+ let name_src = CoercDb.name_of_carr src in
+ let name_tgt = CoercDb.name_of_carr tgt in
let name = name_tgt ^ "_of_" ^ name_src in
let buri = UriManager.buri_of_uri uri in
let c_uri =