From aaf1c6a4f2e56d08433e2258da4d4cc51c943e4e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 4 Sep 2007 10:45:18 +0000 Subject: [PATCH] Composition of coercions with arity > 0 is now implemented correctly. --- .../components/library/cicCoercion.ml | 2 +- .../components/library/cicCoercion.mli | 6 +- .../components/library/librarySync.ml | 9 +-- .../components/tactics/closeCoercionGraph.ml | 74 +++++++++++-------- .../components/tactics/closeCoercionGraph.mli | 8 +- helm/software/components/tactics/compose.ml | 16 ++-- 6 files changed, 64 insertions(+), 51 deletions(-) diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml index 85dc9f65b..638c0ce64 100644 --- a/helm/software/components/library/cicCoercion.ml +++ b/helm/software/components/library/cicCoercion.ml @@ -29,7 +29,7 @@ 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) list) + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * int) list) ;; let set_close_coercion_graph f = close_coercion_graph_ref := f;; diff --git a/helm/software/components/library/cicCoercion.mli b/helm/software/components/library/cicCoercion.mli index d86229726..97463b1d6 100644 --- a/helm/software/components/library/cicCoercion.mli +++ b/helm/software/components/library/cicCoercion.mli @@ -28,11 +28,13 @@ val set_close_coercion_graph : (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list) + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * + int (* saturations *) * Cic.obj * int (* arity *)) list) -> unit val close_coercion_graph: CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * + int (* saturations *) * Cic.obj * int (* arity *) ) list diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index 5897d62ba..5189547d3 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -314,13 +314,13 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations baseuri in let new_coercions = - List.filter (fun (s,t,u,saturations,obj) -> not(already_in_obj s t u obj)) + List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj)) new_coercions in - let composite_uris = List.map (fun (_,_,uri,_,_) -> uri) new_coercions in + let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in (* update the DB *) List.iter - (fun (src,tgt,uri,saturations,_) -> + (fun (src,tgt,uri,saturations,_,_) -> CoercDb.add_coercion (src,tgt,uri,saturations)) new_coercions; CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations); @@ -328,9 +328,8 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations let lemmas = if add_composites then List.fold_left - (fun acc (_,tgt,uri,saturations,obj) -> + (fun acc (_,tgt,uri,saturations,obj,arity) -> add_single_obj uri obj refinement_toolkit; - let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in (uri,arity,saturations)::acc) [] new_coercions else diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index 68e4e7cb2..d558c0ef0 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -33,6 +33,11 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else () * (source, list of coercions to follow, target) *) let get_closure_coercions src tgt uri coercions = + let enrich (uri,sat) tgt = + let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in + uri,sat,arity + in + let uri = enrich uri tgt in let eq_carr ?exact s t = try CoercDb.eq_carr ?exact s t @@ -54,13 +59,13 @@ let get_closure_coercions src tgt uri coercions = (HExtlib.flatten_map (fun (_,t,ul) -> if eq_carr ~exact:true src t then [] else - List.map (fun u -> src,[uri; u],t) ul) c_from_tgt) @ + List.map (fun u -> src,[uri; enrich u t],t) ul) c_from_tgt) @ (HExtlib.flatten_map - (fun (s,_,ul) -> + (fun (s,t,ul) -> if eq_carr ~exact:true s tgt then [] else - List.map (fun u -> s,[u; uri],tgt) ul) c_to_src) @ + List.map (fun u -> s,[enrich u t; uri],tgt) ul) c_to_src) @ (HExtlib.flatten_map - (fun (s,_,u1l) -> + (fun (s,t1,u1l) -> HExtlib.flatten_map (fun (_,t,u2l) -> HExtlib.flatten_map @@ -70,7 +75,7 @@ let get_closure_coercions src tgt uri coercions = || eq_carr ~exact:true src t then [] else List.map - (fun u2 -> (s,[u1;uri;u2],t)) + (fun u2 -> (s,[enrich u1 t1;uri;enrich u2 t],t)) u2l) u1l) c_from_tgt) @@ -83,8 +88,14 @@ let obj_attrs n = [`Class (`Coercion n); `Generated] exception UnableToCompose (* generate_composite (c2 (c1 s)) in the universe graph univ - * both living in the same context and metasenv *) -let generate_composite' (c1,sat1) (c2,sat2) context metasenv univ arity = + both living in the same context and metasenv + + c2 ?p2 (c1 ?p1 ?x ?s1) ?s2 + + where: + ?pn + 1 + ?sn = count_pi n - arity n +*) +let generate_composite' (c1,sat1,arity1) (c2,sat2,arity2) context metasenv univ= let original_metasenv = metasenv in let c1_ty,univ = CicTypeChecker.type_of_aux' metasenv context c1 univ in let c2_ty,univ = CicTypeChecker.type_of_aux' metasenv context c2 univ in @@ -210,8 +221,8 @@ let generate_composite' (c1,sat1) (c2,sat2) context metasenv univ arity = 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 c1_pis, names_c1 = count_pis c1_ty 0 in - let c2_pis, names_c2 = count_pis c2_ty arity in + let c1_pis, names_c1 = count_pis c1_ty arity1 in + let c2_pis, names_c2 = count_pis c2_ty arity2 in let c = compose c1 c1_pis c2 c2_pis in let spine_len = c1_pis + c2_pis in let c = mk_lambda_spine c (namer (names_c1 @ names_c2)) spine_len in @@ -278,7 +289,7 @@ let generate_composite' (c1,sat1) (c2,sat2) context metasenv univ arity = CicRefine.insert_coercions := old_insert_coercions; raise exn in - c, metasenv, univ, saturationsres + c, metasenv, univ, saturationsres, arity2 ;; let build_obj c univ arity = @@ -305,7 +316,7 @@ let filter_duplicates l coercions = CoercDb.eq_carr s src && CoercDb.eq_carr t tgt && try - List.for_all2 (fun (u1,_) (u2,_) -> UriManager.eq u1 u2) l1 l2 + List.for_all2 (fun (u1,_,_) (u2,_) -> UriManager.eq u1 u2) l1 l2 with | Invalid_argument "List.for_all2" -> false) coercions)) @@ -366,44 +377,45 @@ let close_coercion_graph src tgt uri saturations baseuri = try (match l with | [] -> assert false - | (he,saturations1) :: tl -> - let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in + | (he,saturations1,arity1) :: tl -> let first_step = Cic.Constant ("", - Some (CoercDb.term_of_carr (CoercDb.Uri he)), - Cic.Sort Cic.Prop, [], obj_attrs arity), saturations1 + Some (CoercDb.term_of_carr (CoercDb.Uri he)), + Cic.Sort Cic.Prop, [], obj_attrs arity1), + saturations1, + arity1 in let o,_ = - List.fold_left (fun (o,univ) (coer,saturations) -> + List.fold_left (fun (o,univ) (coer,saturations2,arity2) -> match o with - | Cic.Constant (_,Some u,_,[],_),saturations1 -> - let t, menv, univ, saturationsres = - generate_composite' (u,saturations1) + | Cic.Constant (_,Some u,_,[],_),saturations1,arity1 -> + let t, menv, univ, saturationsres, arityres = + generate_composite' (u,saturations1,arity1) (CoercDb.term_of_carr (CoercDb.Uri coer), - saturations) [] [] univ arity + saturations2, arity2) [] [] univ in if (menv = []) then HLog.warn "MENV non empty after composing coercions"; - let o,univ = build_obj t univ arity in - (o,saturationsres),univ + let o,univ = build_obj t univ arityres in + (o,saturationsres,arityres),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 (fun u,_ -> UriManager.name_of_uri u) l in + let by = List.map (fun u,_,_ -> UriManager.name_of_uri u) l in let name = mangle name_tgt name_src by in let c_uri = number_if_already_defined baseuri name - (List.map (fun (_,_,u,_,_) -> u) acc) + (List.map (fun (_,_,u,_,_,_) -> u) acc) in - let named_obj,saturations = + let named_obj,saturations,arity = match o with - | Cic.Constant (_,bo,ty,vl,attrs),saturations -> - Cic.Constant (name,bo,ty,vl,attrs),saturations + | Cic.Constant (_,bo,ty,vl,attrs),saturations,arity -> + Cic.Constant (name,bo,ty,vl,attrs),saturations,arity | _ -> assert false in - (src,tgt,c_uri,saturations,named_obj))::acc + (src,tgt,c_uri,saturations,named_obj,arity))::acc with UnableToCompose -> acc ) [] todo_list in @@ -415,9 +427,9 @@ CicCoercion.set_close_coercion_graph close_coercion_graph;; (* generate_composite (c2 (c1 s)) in the universe graph univ * both living in the same context and metasenv *) -let generate_composite c1 c2 context metasenv univ arity = - let a,b,c,_ = - generate_composite' (c1,0) (c2,0) context metasenv univ arity +let generate_composite c1 c2 context metasenv univ sat2 = + let a,b,c,_,_ = + generate_composite' (c1,0,0) (c2,sat2,0) context metasenv univ in a,b,c ;; diff --git a/helm/software/components/tactics/closeCoercionGraph.mli b/helm/software/components/tactics/closeCoercionGraph.mli index baf926ff1..7157e5c2d 100644 --- a/helm/software/components/tactics/closeCoercionGraph.mli +++ b/helm/software/components/tactics/closeCoercionGraph.mli @@ -28,12 +28,12 @@ val close_coercion_graph: CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) - list + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * + int (* saturations *) * Cic.obj * int (* arity *)) list exception UnableToCompose val generate_composite: - Cic.term -> Cic.term -> Cic.context -> - Cic.metasenv -> CicUniv.universe_graph -> int (* arity *) -> + Cic.term -> Cic.term (* t2 *) -> Cic.context -> + Cic.metasenv -> CicUniv.universe_graph -> int (* saturations of t2 *) -> Cic.term * Cic.metasenv * CicUniv.universe_graph diff --git a/helm/software/components/tactics/compose.ml b/helm/software/components/tactics/compose.ml index cd355dc27..317030404 100644 --- a/helm/software/components/tactics/compose.ml +++ b/helm/software/components/tactics/compose.ml @@ -59,27 +59,27 @@ let compose_core t2 t1 (proof, goal) = | CicUnification.Uncertain _ -> false, menv2, m in (* check which "positions" in the input arrow unifies with saturated_ty2 *) - let rec positions menv cur arity = function + let rec positions menv cur saturations = function | Cic.Prod (n,s,t) -> let b, newmenv, sb = unif menv s in if b then - (arity - cur - 1) :: - (positions newmenv (cur + 1) arity (CicSubstitution.subst sb t)) + (saturations - cur - 1) :: + (positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t)) else - positions newmenv (cur + 1) arity (CicSubstitution.subst sb t) + positions newmenv (cur + 1) saturations (CicSubstitution.subst sb t) | _ -> [] in - (* position is a list of arities, that is if t1 : a -> b -> c and arity is + (* position is a list of arities, that is if t1 : a -> b -> c and saturations is * 0 then the computed term will be (t1 ? t2) of type a -> c - * if arity is 1 then (t1 t2 ?) of type b -> c *) + * if saturations is 1 then (t1 t2 ?) of type b -> c *) let rec generate positions menv acc = match positions with | [] -> acc, menv - | arity::tl -> + | saturations::tl -> try let t, menv1, _ = CloseCoercionGraph.generate_composite t2 t1 context menv - CicUniv.oblivion_ugraph arity + CicUniv.oblivion_ugraph saturations in assert (List.length menv1 = List.length menv); generate tl menv (t::acc) -- 2.39.2