X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcicCoercion.ml;h=9a9ddb62bd6e797a89eed53de5e96997a5b76a8a;hb=7f21c77a04c282e789dfbedf202fe90e15a7fde2;hp=40def823834c65c256f4b6b0752d465aecaba343;hpb=9393a9f9370014c904244358abe4ec6e11a9d158;p=helm.git diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index 40def8238..9a9ddb62b 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -42,19 +42,31 @@ 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 ?? *) ;; @@ -109,7 +121,7 @@ let generate_composite_closure rt c1 c2 univ = let rec aux = function | Cic.Lambda (_, Cic.Meta (i,_), t) when List.exists (fun (j,_,_) -> j = i) metasenv -> - CicSubstitution.subst (Cic.Rel ~-100) t + aux (CicSubstitution.subst (Cic.Rel ~-100) t) | Cic.Lambda (name, s, t) -> Cic.Lambda (name, s, aux t) | t -> t @@ -169,13 +181,50 @@ let generate_composite_closure rt 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) *) @@ -184,44 +233,45 @@ let close_coercion_graph rt src tgt uri = 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 + 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 - ) (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 + in + Some ((src,tgt,c_uri,named_obj))) + with UnableToCompose -> None + ) todo_list + in + new_coercions + with ManglingFailed s -> HLog.error s; [] ;;