X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicCoercion.ml;h=b45599ceb5efd3ca6893365a78c107bf4a25223f;hb=4693f3b9de6d867921b51f61e9a7dc36c3da1b77;hp=7e36ac1aa5000d5c7ff2bb7dbc7627aa3d496e70;hpb=a8e20a3995f4f90b742049dd682b25d831840d73;p=helm.git diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml index 7e36ac1aa..b45599ceb 100644 --- a/helm/software/components/library/cicCoercion.ml +++ b/helm/software/components/library/cicCoercion.ml @@ -25,203 +25,16 @@ (* $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 -> - aux (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 +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 * int) list) ;; -(* 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 set_close_coercion_graph f = close_coercion_graph_ref := f;; -(* 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 +let close_coercion_graph c1 c2 u sat s = + !close_coercion_graph_ref c1 c2 u sat s ;; -