X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcicCoercion.ml;h=638c0ce64a81d037749048c9a698362bde6b0916;hb=65662e7d8de61a338b636f208d04e85eb59e6b8e;hp=33309f109e6c48d2b9f11b5885170ac4d65bab8c;hpb=2499f5fdcf4dbfecc6f4fafe925b24ae76f14be8;p=helm.git diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index 33309f109..638c0ce64 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -25,331 +25,15 @@ (* $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,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*)) - coercions - in - let c_to_src = - List.filter - (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) - coercions - in - (HExtlib.flatten_map - (fun (_,t,ul) -> List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @ - (HExtlib.flatten_map - (fun (s,_,ul) -> List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @ - (HExtlib.flatten_map - (fun (s,_,u1l) -> - HExtlib.flatten_map - (fun (_,t,u2l) -> - HExtlib.flatten_map - (fun u1 -> - List.map - (fun u2 -> (s,[u1;uri;u2],t)) - u2l) - u1l) - c_from_tgt) - c_to_src) - | _ -> [] (* do not close in case source or target is not an indty ?? *) -;; - -let obj_attrs n = [`Class (`Coercion n); `Generated] - -exception UnableToCompose - -(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) -let generate_composite_closure rt c1 c2 univ arity = - 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 = function - | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1) - in - let rec mk_lambda_spline c namer = function - | 0 -> c - | n -> - Cic.Lambda - (namer n, - (Cic.Implicit None), - mk_lambda_spline c namer (n-1)) - in - let count_saturations_needed t arity = - let rec aux acc n = function - | Cic.Prod (name,src, ((Cic.Prod _) as t)) -> - aux (acc@[name]) (n+1) t - | _ -> n,acc - in - let len,names = aux [] 0 t in - let len = len - arity in - List.fold_left - (fun (n,l) x -> if n <= len then n+1,l@[x] else n,l) (0,[]) - names - 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 = - let module OT = struct type t = int let compare = Pervasives.compare end in - let module S = HTopoSort.Make (OT) in - let dep i = - let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in - let metas = List.map fst (CicUtil.metas_of_term ty) in - HExtlib.list_uniq (List.sort Pervasives.compare metas) - in - let om = - S.topological_sort (List.map (fun (i,_,_) -> i) metasenv) dep - in - List.map (fun i -> List.find (fun (j,_,_) -> i=j) metasenv) om - 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 -> - aux (CicSubstitution.subst (Cic.Rel ~-100) t) - | Cic.Lambda (name, s, t) -> - Cic.Lambda (name, s, aux t) - | t -> t - in - aux t - in - let order_body_menv term body_metasenv = - let rec purge_lambdas = function - | Cic.Lambda (_,_,t) -> purge_lambdas t - | t -> t - in - let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in - let metas_that_saturate l = - List.fold_left - (fun (acc,n) t -> - let metas = CicUtil.metas_of_term t in - let metas = List.map fst metas in - let metas = - List.filter - (fun i -> List.for_all (fun (j,_) -> j<>i) acc) - metas - in - let metas = List.map (fun i -> i,n) metas in - metas @ acc, n+1) - ([],0) l - in - let l_c2 = skip_appl (purge_lambdas term) in - let l_c1 = - match HExtlib.list_last l_c2 with - | Cic.Appl l -> List.tl l - | _ -> assert false - in - (* i should cut off the laet elem of l_c2 *) - let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in - List.sort - (fun (i,ctx1,ty1) (j,ctx1,ty1) -> - try List.assoc i meta2no - List.assoc j meta2no - with Not_found -> assert false) - body_metasenv - in - let namer l n = - let l = List.map (function Cic.Name s -> s | _ -> "A") l in - let l = List.fold_left - (fun acc s -> - let rec add' s = - if List.exists ((=) s) acc then add' (s^"'") else s - in - acc@[add' s]) - [] l - in - let l = List.rev l in - Cic.Name (List.nth l (n-1)) - 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, names_c1 = count_saturations_needed c1_ty arity in - let saturations_for_c2, names_c2 = count_saturations_needed c2_ty 0 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 (namer (names_c1 @ names_c2)) 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 body_metasenv = order_body_menv term body_metasenv in - debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_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 arity) in - obj,univ +let close_coercion_graph_ref = ref + (fun _ _ _ _ _ -> [] : + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> + string (* baseuri *) -> + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * int) list) ;; -(* removes from l the coercions that are in !coercions *) -let filter_duplicates l coercions = - List.filter ( - fun (src,l1,tgt) -> - not (List.exists (fun (s,t,l2) -> - CoercDb.eq_carr s src && - CoercDb.eq_carr t tgt && - try - List.for_all2 (fun u1 u2 -> UriManager.eq u1 u2) l1 l2 - with - | Invalid_argument "List.for_all2" -> false) - coercions)) - l +let set_close_coercion_graph f = close_coercion_graph_ref := f;; -let mangle s t l = - (*List.fold_left - (fun s x -> s ^ "_" ^ x) - (s ^ "_OF_" ^ t ^ "_BY" ^ string_of_int (List.length l)) l*) - s ^ "_OF_" ^ t +let close_coercion_graph c1 c2 u sat s = + !close_coercion_graph_ref c1 c2 u sat s ;; - -exception ManglingFailed of string - -let number_if_already_defined buri name l = - let err () = - raise - (ManglingFailed - ("Unable to give an altenative name to " ^ buri ^ "/" ^ name ^ ".con")) - in - let rec aux n = - let suffix = if n > 0 then string_of_int n else "" in - let suri = buri ^ "/" ^ name ^ suffix ^ ".con" in - let uri = UriManager.uri_of_string suri in - let retry () = - if n < 100 then - begin - HLog.warn ("Uri " ^ suri ^ " already exists."); - aux (n+1) - end - else - err () - in - if List.exists (UriManager.eq uri) l then retry () - else - try - let _ = Http_getter.resolve' ~writable:true uri in - if Http_getter.exists' uri then retry () else uri - with - | Http_getter_types.Key_not_found _ -> uri - | Http_getter_types.Unresolvable_URI _ -> assert false - in - aux 0 -;; - -(* 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 - try - let new_coercions = - List.fold_left ( - fun acc (src, l , tgt) -> - try - (match l with - | [] -> assert false - | he :: tl -> - let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in - let first_step = - Cic.Constant ("", - Some (CoercDb.term_of_carr (CoercDb.Uri he)), - Cic.Sort Cic.Prop, [], obj_attrs arity) - 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 arity - | _ -> 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 by = List.map UriManager.name_of_uri l in - let name = mangle name_tgt name_src by in - let buri = UriManager.buri_of_uri uri in - let c_uri = - number_if_already_defined buri name - (List.map (fun (_,_,u,_) -> u) acc) - 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))::acc - with UnableToCompose -> acc - ) [] todo_list - in - new_coercions - with ManglingFailed s -> HLog.error s; [] -;; -