From: Enrico Tassi Date: Tue, 7 Jun 2005 16:41:18 +0000 (+0000) Subject: added support for coercions X-Git-Tag: PRE_INDEX_1~53 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6376b9d56df8c0151a4cd5f35f2646d9922b5858;p=helm.git added support for coercions --- diff --git a/helm/ocaml/cic_unification/.depend b/helm/ocaml/cic_unification/.depend index bf364009e..e31ec55a9 100644 --- a/helm/ocaml/cic_unification/.depend +++ b/helm/ocaml/cic_unification/.depend @@ -8,6 +8,8 @@ cicUnification.cmo: freshNamesGenerator.cmi cicMetaSubst.cmi \ cicUnification.cmi cicUnification.cmx: freshNamesGenerator.cmx cicMetaSubst.cmx \ cicUnification.cmi +coercDb.cmo: coercDb.cmi +coercDb.cmx: coercDb.cmi coercGraph.cmo: freshNamesGenerator.cmi coercGraph.cmi coercGraph.cmx: freshNamesGenerator.cmx coercGraph.cmi cicRefine.cmo: freshNamesGenerator.cmi cicUnification.cmi cicMkImplicit.cmi \ diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile index 0002887aa..f5699c025 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 \ + coercDb.mli \ coercGraph.mli \ cicRefine.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index eda04d36e..1e655b352 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -833,9 +833,9 @@ and type_of_aux' metasenv context t ugraph = hete,subst,metasenv,ugraph1 with exn -> (* we search a coercion from hety to s *) - let coer = None (* CoercGraph.look_for_coercion + let coer = CoercGraph.look_for_coercion (CicMetaSubst.apply_subst subst hety) - (CicMetaSubst.apply_subst subst s) *) + (CicMetaSubst.apply_subst subst s) in match coer with | None -> raise exn diff --git a/helm/ocaml/cic_unification/coercDb.ml b/helm/ocaml/cic_unification/coercDb.ml new file mode 100644 index 000000000..149f3a4ab --- /dev/null +++ b/helm/ocaml/cic_unification/coercDb.ml @@ -0,0 +1,14 @@ +let db = ref [] + +let to_list () = + !db + +let add_coercion c = + db := c :: !db + +let remove_coercion p = + db := List.filter p !db + +let find_coercion f = + List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db) + diff --git a/helm/ocaml/cic_unification/coercDb.mli b/helm/ocaml/cic_unification/coercDb.mli new file mode 100644 index 000000000..1d56132ea --- /dev/null +++ b/helm/ocaml/cic_unification/coercDb.mli @@ -0,0 +1,38 @@ +(* 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 to_list: + unit -> + (UriManager.uri * UriManager.uri * UriManager.uri) list + +val add_coercion: + UriManager.uri * UriManager.uri * UriManager.uri -> unit + +val remove_coercion: + (UriManager.uri * UriManager.uri * UriManager.uri -> bool) -> unit + +val find_coercion: + (UriManager.uri * UriManager.uri -> bool) -> UriManager.uri list + diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index 00cfa90da..d7454925a 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -25,49 +25,30 @@ open Printf;; -let debug_print = fun _ -> () - -type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list - -(* 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" - - ); - -] -;; +let debug = true +let debug_print = if debug then prerr_endline else ignore (* 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 - debug_print (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 -> - debug_print (sprintf ":( NON TROVATA la coercion %s %s" - (UriManager.name_of_uri src) (UriManager.name_of_uri 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 ;; @@ -75,17 +56,9 @@ let look_for_coercion src tgt = * 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 +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 ( @@ -136,13 +109,13 @@ let generate_composite_closure c1 c2 univ = ;; (* removes from l the coercions that are in !coercions *) -let filter_duplicates l = +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) - !coercions)) + coercions)) l (* given a new coercion uri from src to tgt returns @@ -150,8 +123,9 @@ let filter_duplicates l = *) 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 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 ( @@ -190,12 +164,8 @@ let close_coercion_graph src tgt uri = ((src,tgt,c_uri),(c_uri,named_obj,u)) ) todo_list) in - coercions := !coercions @ new_coercions @ [src,tgt,uri]; + List.iter CoercDb.add_coercion (new_coercions @ [src,tgt,uri]); new_coercions_obj ;; -let get_coercions_list () = - !coercions - - (* EOF *) diff --git a/helm/ocaml/cic_unification/coercGraph.mli b/helm/ocaml/cic_unification/coercGraph.mli index cb0e51ca6..03acb4a6d 100644 --- a/helm/ocaml/cic_unification/coercGraph.mli +++ b/helm/ocaml/cic_unification/coercGraph.mli @@ -23,15 +23,11 @@ * http://cs.unibo.it/helm/. *) -type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list - val look_for_coercion : - UriManager.uri -> UriManager.uri -> Cic.term option + Cic.term -> Cic.term -> Cic.term option +(* also adds them to the Db *) val close_coercion_graph: UriManager.uri -> UriManager.uri -> UriManager.uri -> (UriManager.uri * Cic.obj * CicUniv.universe_graph) list -val get_coercions_list: - unit -> (UriManager.uri * UriManager.uri * UriManager.uri) list -