--- /dev/null
+(* Copyright (C) 2005, 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://helm.cs.unibo.it/
+ *)
+
+(* $Id$ *)
+
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
+
+(* 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 (Printf.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
+
+(* 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 =
+ List.map (
+ fun (src, l , tgt) ->
+ match l with
+ | [] -> assert false
+ | he :: tl ->
+ let first_step =
+ Cic.Constant ("",
+ Some (CoercDb.term_of_carr (CoercDb.Uri he)),
+ Cic.Sort Cic.Prop, [], obj_attrs)
+ in
+ let o,_ =
+ List.fold_left (fun (o,univ) coer ->
+ match o with
+ | Cic.Constant (_,Some c,_,[],_) ->
+ generate_composite_closure c (CoercDb.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,named_obj))
+ ) todo_list
+ in
+ new_coercions
+;;
+
projects / helm.git / blobdiff