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
cicMetaSubst.mli \
cicMkImplicit.mli \
cicUnification.mli \
- coercGraph.mli \
cicRefine.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
+++ /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/.
- *)
-
-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 *)
+++ /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/.
- *)
-
-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
-
+coercGraph.cmi: coercDb.cmi
cicElim.cmo: cicElim.cmi
cicElim.cmx: cicElim.cmi
cicRecord.cmo: cicRecord.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 \
libraryMisc.mli \
libraryDb.mli \
coercDb.mli \
+ coercGraph.mli \
librarySync.mli \
libraryClean.mli \
$(NULL)
--- /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/.
+ *)
+
+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 *)
--- /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/.
+ *)
+
+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
+
projects / helm.git / commitdiff