X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcicCoercion.ml;h=9a9ddb62bd6e797a89eed53de5e96997a5b76a8a;hb=27ebdab06ba308c431669b58a46fc0bb12c8c72e;hp=fe636ee351dc0a66240ece88cf7b494829097fab;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index fe636ee35..9a9ddb62b 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -42,53 +42,134 @@ let get_closure_coercions src tgt uri coercions = match src,tgt with | CoercDb.Uri _, CoercDb.Uri _ -> let c_from_tgt = - List.filter (fun (f,_,_) -> eq_carr f tgt) coercions + List.filter + (fun (f,t,_) -> eq_carr f tgt && not (eq_carr t src)) + coercions in let c_to_src = - List.filter (fun (_,t,_) -> eq_carr t src) coercions + List.filter + (fun (f,t,_) -> eq_carr t src && not (eq_carr f tgt)) + 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) + (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 = [`Class `Coercion; `Generated] +exception UnableToCompose + (* generate_composite_closure (c2 (c1 s)) in the universe graph univ *) -let generate_composite_closure c1 c2 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 rec mk_rels n = + let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in + let rec mk_implicits n = match n with | 0 -> [] - | _ -> (Cic.Rel n) :: (mk_rels (n-1)) + | _ -> (Cic.Implicit None) :: mk_implicits (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)) ]) + 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 c = compose 0 c1_ty 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 as exn -> + with CicTypeChecker.TypeCheckerFailure s -> debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s" (CicPp.ppterm c) (Lazy.force s))); - raise exn + raise UnableToCompose in let cleaned_ty = FreshNamesGenerator.clean_dummy_dependent_types c_ty @@ -100,57 +181,97 @@ let generate_composite_closure c1 c2 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) -> + fun (src,l1,tgt) -> + not (List.exists (fun (s,t,l2) -> CoercDb.eq_carr s src && - CoercDb.eq_carr t tgt) + 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 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 +;; + +exception ManglingFailed of string + +let number_if_already_defined buri name = + let rec aux n = + let suffix = if n > 0 then string_of_int n else "" in + let uri = buri ^ "/" ^ name ^ suffix ^ ".con" in + try + let _ = Http_getter.resolve ~writable:true uri in + if Http_getter.exists uri then + begin + HLog.warn ("Uri " ^ uri ^ " already exists."); + if n < 10 then aux (n+1) else + raise + (ManglingFailed + ("Unable to give an altenative name to " ^ + buri ^ "/" ^ name ^ ".con")) + end + else + UriManager.uri_of_string uri + with + | Http_getter_types.Key_not_found _ -> UriManager.uri_of_string 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 src tgt uri = +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 = - 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 + try + 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 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 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 + with ManglingFailed s -> HLog.error s; [] ;;