(* 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 *)