(* 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] exception UnableToCompose (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) let generate_composite_closure rt c1 c2 univ = let module RT = RefinementTool in let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in let rec mk_implicits n = match n with | 0 -> [] | _ -> (Cic.Implicit None) :: mk_implicits (n-1) in let rec mk_lambda_spline c = function | 0 -> c | n -> Cic.Lambda (Cic.Name ("A" ^ string_of_int (n-1)), (Cic.Implicit None), mk_lambda_spline c (n-1)) in let rec count_saturations_needed n = function | Cic.Prod (_,src, ((Cic.Prod _) as t)) -> count_saturations_needed (n+1) t | _ -> n in let compose c1 nc1 c2 nc2 = Cic.Lambda (Cic.Name "x", (Cic.Implicit None), Cic.Appl ( c2 :: mk_implicits nc2 @ [ Cic.Appl ( c1 :: mk_implicits nc1 @ [Cic.Rel 1]) ])) in let order_metasenv metasenv = List.sort (fun (_,ctx1,_) (_,ctx2,_) -> List.length ctx1 - List.length ctx2) metasenv in let rec create_subst_from_metas_to_rels n = function | [] -> [] | (metano, ctx, ty)::tl -> (metano,(ctx,Cic.Rel (n+1),ty)) :: create_subst_from_metas_to_rels (n-1) tl in let split_metasenv metasenv n = List.partition (fun (_,ctx,_) -> List.length ctx > n) metasenv in let purge_unused_lambdas metasenv t = let rec aux = function | Cic.Lambda (_, Cic.Meta (i,_), t) when List.exists (fun (j,_,_) -> j = i) metasenv -> CicSubstitution.subst (Cic.Rel ~-100) t | Cic.Lambda (name, s, t) -> Cic.Lambda (name, s, aux t) | t -> t in aux t in debug_print (lazy ("\nCOMPOSING")); debug_print (lazy (" c1= "^CicPp.ppterm c1 ^" : "^ CicPp.ppterm c1_ty)); debug_print (lazy (" c2= "^CicPp.ppterm c2 ^" : "^ CicPp.ppterm c2_ty)); let saturations_for_c1 = count_saturations_needed 0 c1_ty in let saturations_for_c2 = count_saturations_needed 0 c2_ty in let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in let spline_len = saturations_for_c1 + saturations_for_c2 in let c = mk_lambda_spline c spline_len in (* debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); *) let c, univ = match rt.RT.type_of_aux' [] [] c univ with | RT.Success (term, ty, metasenv, ugraph) -> debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term)); let metasenv = order_metasenv metasenv in debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv)); let body_metasenv, lambdas_metasenv = split_metasenv metasenv spline_len in debug_print(lazy("B_MENV: "^rt.RT.ppmetasenv [] body_metasenv)); debug_print(lazy("L_MENV: "^rt.RT.ppmetasenv [] lambdas_metasenv)); let subst = create_subst_from_metas_to_rels spline_len body_metasenv in debug_print (lazy("SUBST: "^rt.RT.ppsubst subst)); let term = rt.RT.apply_subst subst term in debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term)); (match rt.RT.type_of_aux' metasenv [] term ugraph with | RT.Success (term, ty, metasenv, ugraph) -> let body_metasenv, lambdas_metasenv = split_metasenv metasenv spline_len in let term = purge_unused_lambdas lambdas_metasenv term in debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term)); term, ugraph | RT.Exception s -> debug_print s; raise UnableToCompose) | RT.Exception s -> debug_print s; raise UnableToCompose in let c_ty,univ = try CicTypeChecker.type_of_aux' [] [] c univ with CicTypeChecker.TypeCheckerFailure s -> debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s" (CicPp.ppterm c) (Lazy.force s))); raise UnableToCompose 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 rt 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 = HExtlib.filter_map ( fun (src, l , tgt) -> try (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 rt 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 Some ((src,tgt,c_uri,named_obj))) with UnableToCompose -> None ) todo_list in new_coercions ;;