X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercGraph.ml;h=d99fc6f798f67f72ccbee796adc50b8bd0db1474;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=c1056b6eca8a912c1ba9b0171ebcf368ea514a3a;hpb=405d288cca88e63515164a8d42d60087e305615c;p=helm.git diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index c1056b6ec..d99fc6f79 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -25,48 +25,84 @@ 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 = CicUtil.uri_of_term src in - let tgt = 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 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] @@ -97,8 +133,8 @@ let generate_composite_closure c1 c2 univ = 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 = @@ -113,11 +149,16 @@ let filter_duplicates l coercions = 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) *) @@ -133,21 +174,21 @@ let close_coercion_graph src tgt uri = match l with | [] -> assert false | he :: tl -> - let term_of_uri' uri = CicUtil.term_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 =