From: Enrico Tassi Date: Wed, 19 Jan 2005 15:23:12 +0000 (+0000) Subject: Added coercion handling module X-Git-Tag: V_0_1_0~125 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93e7f6e653ae9e6e17d054ccd3b9aaf801e13bcf;p=helm.git Added coercion handling module --- diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile index 9762f5936..0002887aa 100644 --- a/helm/ocaml/cic_unification/Makefile +++ b/helm/ocaml/cic_unification/Makefile @@ -7,6 +7,7 @@ INTERFACE_FILES = \ cicMkImplicit.mli \ freshNamesGenerator.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 new file mode 100644 index 000000000..4dd05073b --- /dev/null +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -0,0 +1,214 @@ +(* 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;; + +ignore(Helm_registry.load_from "/home/tassi/helm/gTopLevel/gTopLevel.conf.xml") + +(* the list of known coercions (MUST be transitively closed) *) +let coercions = ref [ + (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)", + UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con", + UriManager.uri_of_string "cic://Coq/Reals/Raxioms/INR.con") ; + + ( + UriManager.uri_of_string "cic:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)", + UriManager.uri_of_string "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)", + UriManager.uri_of_string "cic:/CoRN/algebra/CFields/cf_crr.con" + + ); + ( + UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)", + UriManager.uri_of_string "cic:/CoRN/algebra/CGroups/CGroup.ind#xpointer(1/1)", + UriManager.uri_of_string "cic:/CoRN/algebra/CAbGroups/cag_crr.con" + + ); + +] +;; + +(* searches a coercion fron src to tgt in the !coercions list *) +let look_for_coercion src tgt = + try + let s,t,u = + List.find (fun (s,t,_) -> + UriManager.eq s src && + UriManager.eq t tgt) + !coercions + in + prerr_endline (sprintf ":) TROVATA la coercion %s %s" + (UriManager.name_of_uri src) + (UriManager.name_of_uri tgt)); + Some (CicUtil.term_of_uri (UriManager.string_of_uri u)) + with + Not_found -> + prerr_endline (sprintf ":( NON TROVATA la coercion %s %s" + (UriManager.name_of_uri src) (UriManager.name_of_uri tgt)); + None +;; + +(* 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 = + 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) +;; + + + +(* 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 -> + prerr_endline (sprintf "Generated composite coercion:\n%s\n%s" + (CicPp.ppterm c) s); + raise exn + in + let cleaned_ty = + FreshNamesGenerator.clean_dummy_dependent_types c_ty + in + let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[]) in + obj,univ +;; + +(* removes from l the coercions that are in !coercions *) +let filter_duplicates l = + List.filter ( + fun (src,_,tgt) -> + not (List.exists (fun (s,t,u) -> + UriManager.eq s src && + UriManager.eq t tgt) + !coercions)) + l + +(* 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 todo_list = get_closure_coercions src tgt uri in + let todo_list = filter_duplicates todo_list in + let new_coercions, new_coercions_obj = + List.split ( + List.map ( + fun (src, l , tgt) -> + 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,[])) + in + let o,u = + List.fold_left (fun (o,u) coer -> + match o with + | Cic.Constant (_,Some c,_,[]) -> + generate_composite_closure c (term_of_uri' coer) u + | _ -> 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 = 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) -> Cic.Constant (name,bo,ty,vl) + | _ -> assert false + in + ((src,tgt,c_uri),(c_uri,named_obj,u)) + ) todo_list) + in + coercions := !coercions @ new_coercions; + new_coercions_obj +;; + + + + +(* stupid case *) + +let l = close_coercion_graph + (UriManager.uri_of_string + "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)") + (UriManager.uri_of_string + "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)") + (UriManager.uri_of_string + "cic:/CoRN/algebra/CRings/cr_crr.con") +in + List.iter (fun (u,o,g) -> + prerr_endline (CicPp.ppobj o); + prerr_endline (UriManager.string_of_uri u); + prerr_endline "") + l + + + +(* EOF *) diff --git a/helm/ocaml/cic_unification/coercGraph.mli b/helm/ocaml/cic_unification/coercGraph.mli new file mode 100644 index 000000000..3c03312c7 --- /dev/null +++ b/helm/ocaml/cic_unification/coercGraph.mli @@ -0,0 +1,31 @@ +(* 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/. + *) + +val look_for_coercion : + UriManager.uri -> UriManager.uri -> Cic.term option + +val close_coercion_graph: + UriManager.uri -> UriManager.uri -> UriManager.uri -> + (UriManager.uri * Cic.obj * CicUniv.universe_graph) list