From: Claudio Sacerdoti Coen Date: Wed, 30 Nov 2005 12:33:06 +0000 (+0000) Subject: coercGraph.ml* moved from cic_unification to library X-Git-Tag: make_still_working~8062 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=727ef55d2a6202a989c274f6caa1b0e1b7307880;p=helm.git coercGraph.ml* moved from cic_unification to library --- diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend index 1fc74e25b..a442c1d4d 100644 --- a/helm/ocaml/cic_unification/.depend +++ b/helm/ocaml/cic_unification/.depend @@ -4,9 +4,7 @@ cicMkImplicit.cmo: cicMkImplicit.cmi cicMkImplicit.cmx: cicMkImplicit.cmi cicUnification.cmo: cicMetaSubst.cmi cicUnification.cmi cicUnification.cmx: cicMetaSubst.cmx cicUnification.cmi -coercGraph.cmo: coercGraph.cmi -coercGraph.cmx: coercGraph.cmi -cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicMkImplicit.cmi \ - cicMetaSubst.cmi cicRefine.cmi -cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicMkImplicit.cmx \ - cicMetaSubst.cmx cicRefine.cmi +cicRefine.cmo: cicUnification.cmi cicMkImplicit.cmi cicMetaSubst.cmi \ + cicRefine.cmi +cicRefine.cmx: cicUnification.cmx cicMkImplicit.cmx cicMetaSubst.cmx \ + cicRefine.cmi diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile index 26e5d4ada..3db00fe5c 100644 --- a/helm/ocaml/cic_unification/Makefile +++ b/helm/ocaml/cic_unification/Makefile @@ -5,7 +5,6 @@ INTERFACE_FILES = \ cicMetaSubst.mli \ cicMkImplicit.mli \ cicUnification.mli \ - coercGraph.mli \ cicRefine.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml deleted file mode 100644 index d99fc6f79..000000000 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ /dev/null @@ -1,210 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -open Printf;; - -type coercion_search_result = - | SomeCoercion of Cic.term - | NoCoercion - | NotMetaClosed - | NotHandled of string Lazy.t - -let debug = false -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 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 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] - -(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) -let generate_composite_closure c1 c2 univ = - let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in - let rec mk_rels n = - match n with - | 0 -> [] - | _ -> (Cic.Rel n) :: (mk_rels (n-1)) - in - let rec compose k = - function - | Cic.Prod (name,src,tgt) -> - let name = - match name with - | Cic.Anonymous -> Cic.Name "x" - | _ -> name - in - Cic.Lambda (name,src,compose (k+1) tgt) - | Cic.Appl (he::tl) -> - Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ]) - | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ]) - in - let c = compose 0 c1_ty in - let c_ty,univ = - try - CicTypeChecker.type_of_aux' [] [] c univ - with CicTypeChecker.TypeCheckerFailure s as exn -> - debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s" - (CicPp.ppterm c) (Lazy.force s))); - raise exn - in - let cleaned_ty = - FreshNamesGenerator.clean_dummy_dependent_types c_ty - in - let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in - obj,univ -;; - -(* removes from l the coercions that are in !coercions *) -let filter_duplicates l coercions = - List.filter ( - fun (src,_,tgt) -> - not (List.exists (fun (s,t,u) -> - 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) - *) -let close_coercion_graph src tgt uri = - (* check if the coercion already exists *) - let coercions = CoercDb.to_list () in - let todo_list = get_closure_coercions src tgt uri coercions in - let todo_list = filter_duplicates todo_list coercions in - let new_coercions, new_coercions_obj = - List.split ( - List.map ( - fun (src, l , tgt) -> - match l with - | [] -> assert false - | he :: tl -> - let first_step = - Cic.Constant ("", - Some (term_of_carr (CoercDb.Uri he)), Cic.Sort Cic.Prop, [], obj_attrs) - in - let o,u = - List.fold_left (fun (o,univ) coer -> - match o with - | Cic.Constant (_,Some c,_,[],_) -> - generate_composite_closure c (term_of_carr (CoercDb.Uri - coer)) univ - | _ -> assert false - ) (first_step, CicUniv.empty_ugraph) tl - 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 = - UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") - in - let named_obj = - match o with - | Cic.Constant (_,bo,ty,vl,attrs) -> - Cic.Constant (name,bo,ty,vl,attrs) - | _ -> assert false - in - ((src,tgt,c_uri),(c_uri,named_obj,u)) - ) todo_list) - in - List.iter CoercDb.add_coercion (new_coercions @ [src,tgt,uri]); - new_coercions_obj -;; - -(* EOF *) diff --git a/helm/ocaml/cic_unification/coercGraph.mli b/helm/ocaml/cic_unification/coercGraph.mli deleted file mode 100644 index fcbed3497..000000000 --- a/helm/ocaml/cic_unification/coercGraph.mli +++ /dev/null @@ -1,39 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -type coercion_search_result = - | SomeCoercion of Cic.term - | NoCoercion - | NotMetaClosed - | NotHandled of string Lazy.t - -val look_for_coercion : - Cic.term -> Cic.term -> coercion_search_result - -(* also adds them to the Db *) -val close_coercion_graph: - CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> - (UriManager.uri * Cic.obj * CicUniv.universe_graph) list - diff --git a/helm/ocaml/library/.depend b/helm/ocaml/library/.depend index 34914e505..1ad51256b 100644 --- a/helm/ocaml/library/.depend +++ b/helm/ocaml/library/.depend @@ -1,3 +1,4 @@ +coercGraph.cmi: coercDb.cmi cicElim.cmo: cicElim.cmi cicElim.cmx: cicElim.cmi cicRecord.cmo: cicRecord.cmi @@ -6,6 +7,8 @@ libraryMisc.cmo: libraryMisc.cmi libraryMisc.cmx: libraryMisc.cmi libraryDb.cmo: libraryDb.cmi libraryDb.cmx: libraryDb.cmi +coercGraph.cmo: coercDb.cmi coercGraph.cmi +coercGraph.cmx: coercDb.cmx coercGraph.cmi coercDb.cmo: coercDb.cmi coercDb.cmx: coercDb.cmi librarySync.cmo: libraryDb.cmi coercDb.cmi cicRecord.cmi cicElim.cmi \ diff --git a/helm/ocaml/library/Makefile b/helm/ocaml/library/Makefile index d64c5020f..224a8d2dd 100644 --- a/helm/ocaml/library/Makefile +++ b/helm/ocaml/library/Makefile @@ -7,6 +7,7 @@ INTERFACE_FILES = \ libraryMisc.mli \ libraryDb.mli \ coercDb.mli \ + coercGraph.mli \ librarySync.mli \ libraryClean.mli \ $(NULL) diff --git a/helm/ocaml/library/coercGraph.ml b/helm/ocaml/library/coercGraph.ml new file mode 100644 index 000000000..d99fc6f79 --- /dev/null +++ b/helm/ocaml/library/coercGraph.ml @@ -0,0 +1,210 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open Printf;; + +type coercion_search_result = + | SomeCoercion of Cic.term + | NoCoercion + | NotMetaClosed + | NotHandled of string Lazy.t + +let debug = false +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 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 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] + +(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) +let generate_composite_closure c1 c2 univ = + let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in + let rec mk_rels n = + match n with + | 0 -> [] + | _ -> (Cic.Rel n) :: (mk_rels (n-1)) + in + let rec compose k = + function + | Cic.Prod (name,src,tgt) -> + let name = + match name with + | Cic.Anonymous -> Cic.Name "x" + | _ -> name + in + Cic.Lambda (name,src,compose (k+1) tgt) + | Cic.Appl (he::tl) -> + Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ]) + | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ]) + in + let c = compose 0 c1_ty in + let c_ty,univ = + try + CicTypeChecker.type_of_aux' [] [] c univ + with CicTypeChecker.TypeCheckerFailure s as exn -> + debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s" + (CicPp.ppterm c) (Lazy.force s))); + raise exn + in + let cleaned_ty = + FreshNamesGenerator.clean_dummy_dependent_types c_ty + in + let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in + obj,univ +;; + +(* removes from l the coercions that are in !coercions *) +let filter_duplicates l coercions = + List.filter ( + fun (src,_,tgt) -> + not (List.exists (fun (s,t,u) -> + 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) + *) +let close_coercion_graph src tgt uri = + (* check if the coercion already exists *) + let coercions = CoercDb.to_list () in + let todo_list = get_closure_coercions src tgt uri coercions in + let todo_list = filter_duplicates todo_list coercions in + let new_coercions, new_coercions_obj = + List.split ( + List.map ( + fun (src, l , tgt) -> + match l with + | [] -> assert false + | he :: tl -> + let first_step = + Cic.Constant ("", + Some (term_of_carr (CoercDb.Uri he)), Cic.Sort Cic.Prop, [], obj_attrs) + in + let o,u = + List.fold_left (fun (o,univ) coer -> + match o with + | Cic.Constant (_,Some c,_,[],_) -> + generate_composite_closure c (term_of_carr (CoercDb.Uri + coer)) univ + | _ -> assert false + ) (first_step, CicUniv.empty_ugraph) tl + 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 = + UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") + in + let named_obj = + match o with + | Cic.Constant (_,bo,ty,vl,attrs) -> + Cic.Constant (name,bo,ty,vl,attrs) + | _ -> assert false + in + ((src,tgt,c_uri),(c_uri,named_obj,u)) + ) todo_list) + in + List.iter CoercDb.add_coercion (new_coercions @ [src,tgt,uri]); + new_coercions_obj +;; + +(* EOF *) diff --git a/helm/ocaml/library/coercGraph.mli b/helm/ocaml/library/coercGraph.mli new file mode 100644 index 000000000..fcbed3497 --- /dev/null +++ b/helm/ocaml/library/coercGraph.mli @@ -0,0 +1,39 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +type coercion_search_result = + | SomeCoercion of Cic.term + | NoCoercion + | NotMetaClosed + | NotHandled of string Lazy.t + +val look_for_coercion : + Cic.term -> Cic.term -> coercion_search_result + +(* also adds them to the Db *) +val close_coercion_graph: + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> + (UriManager.uri * Cic.obj * CicUniv.universe_graph) list +