X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcicCoercion.ml;h=33309f109e6c48d2b9f11b5885170ac4d65bab8c;hb=2499f5fdcf4dbfecc6f4fafe925b24ae76f14be8;hp=9a9ddb62bd6e797a89eed53de5e96997a5b76a8a;hpb=f764844fa35ab0bb9c10707151340b924060f069;p=helm.git diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index 9a9ddb62b..33309f109 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -43,12 +43,12 @@ let get_closure_coercions src tgt uri coercions = | CoercDb.Uri _, CoercDb.Uri _ -> let c_from_tgt = List.filter - (fun (f,t,_) -> eq_carr f tgt && not (eq_carr t src)) + (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)) + (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*)) coercions in (HExtlib.flatten_map @@ -70,31 +70,37 @@ let get_closure_coercions src tgt uri coercions = | _ -> [] (* do not close in case source or target is not an indty ?? *) ;; -let obj_attrs = [`Class `Coercion; `Generated] +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 = +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 n = - match n with - | 0 -> [] - | _ -> (Cic.Implicit None) :: mk_implicits (n-1) + let rec mk_implicits = function + | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1) in - let rec mk_lambda_spline c = function + let rec mk_lambda_spline c namer = function | 0 -> c | n -> Cic.Lambda - (Cic.Name ("A" ^ string_of_int (n-1)), + (namer n, (Cic.Implicit None), - mk_lambda_spline c (n-1)) + mk_lambda_spline c namer (n-1)) in - let rec count_saturations_needed n = function - | Cic.Prod (_,src, ((Cic.Prod _) as t)) -> count_saturations_needed (n+1) t - | _ -> n + 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 @@ -103,11 +109,21 @@ let generate_composite_closure rt c1 c2 univ = 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 + 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 -> @@ -128,26 +144,77 @@ let generate_composite_closure rt c1 c2 univ = 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 = count_saturations_needed 0 c1_ty in - let saturations_for_c2 = count_saturations_needed 0 c2_ty in + 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 spline_len in - (* debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); *) + 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 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 @@ -174,7 +241,7 @@ let generate_composite_closure rt c1 c2 univ = let cleaned_ty = FreshNamesGenerator.clean_dummy_dependent_types c_ty in - let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in + let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs arity) in obj,univ ;; @@ -201,26 +268,33 @@ let mangle s t l = exception ManglingFailed of string -let number_if_already_defined buri name = +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 uri = buri ^ "/" ^ name ^ suffix ^ ".con" in - try - let _ = Http_getter.resolve ~writable:true uri in - if Http_getter.exists uri then + 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 " ^ uri ^ " already exists."); - if n < 10 then aux (n+1) else - raise - (ManglingFailed - ("Unable to give an altenative name to " ^ - buri ^ "/" ^ name ^ ".con")) + HLog.warn ("Uri " ^ suri ^ " already exists."); + aux (n+1) 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 + 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 ;; @@ -235,23 +309,24 @@ let close_coercion_graph rt src tgt uri = let todo_list = filter_duplicates todo_list coercions in try let new_coercions = - HExtlib.filter_map ( - fun (src, l , tgt) -> + 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) + 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 + generate_composite_closure rt c + (CoercDb.term_of_carr (CoercDb.Uri coer)) univ arity | _ -> assert false ) (first_step, CicUniv.empty_ugraph) tl in @@ -260,16 +335,19 @@ let close_coercion_graph rt src tgt uri = 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 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 - Some ((src,tgt,c_uri,named_obj))) - with UnableToCompose -> None - ) todo_list + (src,tgt,c_uri,named_obj))::acc + with UnableToCompose -> acc + ) [] todo_list in new_coercions with ManglingFailed s -> HLog.error s; []