--- /dev/null
+(* 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
+
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
;;
* 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 (
;;
(* 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
*)
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 (
((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 *)
projects / helm.git / commitdiff