X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcicCoercion.ml;h=40def823834c65c256f4b6b0752d465aecaba343;hb=9393a9f9370014c904244358abe4ec6e11a9d158;hp=fe636ee351dc0a66240ece88cf7b494829097fab;hpb=4ab6b4054730b9ed419f0c4296f9deda9ab321b2;p=helm.git diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index fe636ee35..40def8238 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -60,35 +60,104 @@ let get_closure_coercions src tgt uri coercions = 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 purge_unused_lambdas metasenv t = + let rec aux = function + | Cic.Lambda (_, Cic.Meta (i,_), t) when + List.exists (fun (j,_,_) -> j = i) metasenv -> + CicSubstitution.subst (Cic.Rel ~-100) t + | Cic.Lambda (name, s, t) -> + Cic.Lambda (name, s, aux t) + | t -> t + in + aux t in - let c = compose 0 c1_ty 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 @@ -110,45 +179,47 @@ let filter_duplicates l coercions = (* 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 ( + HExtlib.filter_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 + 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 - ) (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)) + in + Some ((src,tgt,c_uri,named_obj))) + with UnableToCompose -> None ) todo_list in new_coercions