From: Enrico Tassi Date: Thu, 19 Jul 2007 10:03:42 +0000 (+0000) Subject: COERCIONS: tentative addition of an equivalence relation over coercion source X-Git-Tag: make_still_working~6154 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4f2e7eacea9e8b3089a575d7bf529fd5e70e8453;p=helm.git COERCIONS: tentative addition of an equivalence relation over coercion source carriers (convertibility) for the moment used only in the FunClass case. --- diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 840a955cb..856c9a586 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -454,6 +454,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in (match boh with | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ | CoercGraph.NotHandled _ -> enrich localization_tbl t (RefineFailure @@ -526,6 +527,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in match boh with | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ | CoercGraph.NotHandled _ -> enrich localization_tbl s' (RefineFailure @@ -1363,6 +1365,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | CoercGraph.NoCoercion | CoercGraph.NotMetaClosed | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.SomeCoercionToTgt candidates | CoercGraph.SomeCoercion candidates -> match HExtlib.list_findopt @@ -1447,6 +1450,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il in (match coer with | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ | CoercGraph.NotHandled _ -> enrich localization_tbl hete exn ~f:(fun _ -> diff --git a/helm/software/components/cic_unification/coercGraph.ml b/helm/software/components/cic_unification/coercGraph.ml index 37ded8ee0..cb33d9e32 100644 --- a/helm/software/components/cic_unification/coercGraph.ml +++ b/helm/software/components/cic_unification/coercGraph.ml @@ -32,6 +32,7 @@ type coercion_search_result = (* to apply the coercion it is sufficient to unify the last coercion argument (that is a Meta) with the term to be coerced *) | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list + | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list | NoCoercion | NotMetaClosed | NotHandled of string Lazy.t @@ -65,30 +66,38 @@ let saturate_coercion ul metasenv subst context = (* searches a coercion fron src to tgt in the !coercions list *) let look_for_coercion' metasenv subst context src tgt = + let pp_l s l = + match l with + | [] -> + debug_print + (lazy + (sprintf ":-( coercion non trovata[%s] da %s a %s" s + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt))); + | _::_ -> + debug_print (lazy ( + sprintf ":-) TROVATE[%s] %d coercion(s) da %s a %s" s + (List.length l) + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt))); + in try let l = CoercDb.find_coercion - (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in - let uri = - match l with - | [] -> - debug_print - (lazy - (sprintf ":-( coercion non trovata da %s a %s" - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt))); - None - | _::_ -> - debug_print (lazy ( - sprintf ":-) TROVATE %d coercion(s) da %s a %s" - (List.length l) - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt))); - Some l + (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in - (match uri with - None -> NoCoercion - | Some ul -> SomeCoercion (saturate_coercion ul metasenv subst context)) + pp_l "precise" l; + (match l with + | [] -> + let l = + CoercDb.find_coercion + (fun (_,t) -> CoercDb.eq_carr t tgt) + in + pp_l "approx" l; + (match l with + | [] -> NoCoercion + | ul -> SomeCoercionToTgt (saturate_coercion ul metasenv subst context)) + | ul -> SomeCoercion (saturate_coercion ul metasenv subst context)) with | CoercDb.EqCarrNotImplemented s -> NotHandled s | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed diff --git a/helm/software/components/cic_unification/coercGraph.mli b/helm/software/components/cic_unification/coercGraph.mli index ae2bd9233..711a1527d 100644 --- a/helm/software/components/cic_unification/coercGraph.mli +++ b/helm/software/components/cic_unification/coercGraph.mli @@ -32,6 +32,7 @@ type coercion_search_result = (* to apply the coercion it is sufficient to unify the last coercion argument (that is a Meta) with the term to be coerced *) | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list + | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list | NoCoercion | NotMetaClosed | NotHandled of string Lazy.t diff --git a/helm/software/components/library/coercDb.ml b/helm/software/components/library/coercDb.ml index 2e93efa0e..aec6dd579 100644 --- a/helm/software/components/library/coercDb.ml +++ b/helm/software/components/library/coercDb.ml @@ -66,9 +66,20 @@ let rec name_of_carr = function | Fun i -> "FunClass_" ^ string_of_int i ;; -let eq_carr src tgt = +let eq_carr ?(exact=false) src tgt = match src, tgt with - | Uri src, Uri tgt -> UriManager.eq src tgt + | 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 -> diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli index 5f455c2af..e6d7e46b3 100644 --- a/helm/software/components/library/coercDb.mli +++ b/helm/software/components/library/coercDb.mli @@ -41,7 +41,7 @@ type coerc_carr = exception EqCarrNotImplemented of string Lazy.t exception EqCarrOnNonMetaClosed -val eq_carr: coerc_carr -> coerc_carr -> bool +val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool val coerc_carr_of_term: Cic.term -> coerc_carr val name_of_carr: coerc_carr -> string val uri_of_carr: coerc_carr -> UriManager.uri option diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index d9dc679b3..2cff9c608 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -52,15 +52,20 @@ let get_closure_coercions src tgt uri coercions = coercions in (HExtlib.flatten_map - (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @ + (fun (_,t,ul) -> + if CoercDb.eq_carr ~exact:true src t then [] else + List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @ (HExtlib.flatten_map - (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @ + (fun (s,_,ul) -> + if CoercDb.eq_carr ~exact:true s tgt then [] else + List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @ (HExtlib.flatten_map (fun (s,_,u1l) -> HExtlib.flatten_map (fun (_,t,u2l) -> HExtlib.flatten_map (fun u1 -> + if CoercDb.eq_carr ~exact:true s t then [] else List.map (fun u2 -> (s,[u1;uri;u2],t)) u2l)