From 396a578b680e7fdb9d262822184e52f0d4d5086b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Aug 2007 13:36:44 +0000 Subject: [PATCH] Coercions are now generalized to the general form f: \forall xs:Ts. \forall a:A xs. \forall ys:Ts'. B xs a ys where f is declared as a coercion from A ? to B ? ? ? using the syntax coercion uri arity saturations where: 1. arity and saturations are optional with default 0 2. the saturations option is the number of ys Useful example: it is now possible to declare a coercion from nat to \exists n:nat. 0 \leq n obtaining something extremely close to Russel (the new implementation of the Program tactic of Coq) up to the fact that coercions are not propagated yet under mutcases and fixes. TODO: composition of coercions having saturations <> 0 is not implemented yet (but should be easy to do, at least on paper) --- components/binaries/transcript/grafite.ml | 2 +- components/cic_unification/coercGraph.ml | 26 +++++--- components/grafite/grafiteAst.ml | 5 +- components/grafite/grafiteAstPp.ml | 10 +-- components/grafite/grafiteMarshal.ml | 4 +- components/grafite_engine/grafiteEngine.ml | 22 +++---- components/grafite_engine/grafiteSync.ml | 7 +- components/grafite_engine/grafiteSync.mli | 5 +- components/grafite_parser/grafiteParser.ml | 6 +- components/library/cicCoercion.ml | 10 +-- components/library/cicCoercion.mli | 8 +-- components/library/coercDb.ml | 36 ++++++----- components/library/coercDb.mli | 8 +-- components/library/librarySync.ml | 74 ++++++++++++---------- components/library/librarySync.mli | 4 +- components/tactics/closeCoercionGraph.ml | 70 ++++++++++++-------- components/tactics/closeCoercionGraph.mli | 5 +- matita/matita.ml | 7 +- 18 files changed, 178 insertions(+), 131 deletions(-) diff --git a/components/binaries/transcript/grafite.ml b/components/binaries/transcript/grafite.ml index 93bd922ef..e88406b58 100644 --- a/components/binaries/transcript/grafite.ml +++ b/components/binaries/transcript/grafite.ml @@ -79,7 +79,7 @@ let require value = command_of_obj (G.Include (floc, value ^ ".ma")) let coercion value = - command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0)) + command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0)) let inline (uri, prefix) = command_of_macro (G.Inline (floc, G.Declarative, uri, prefix)) diff --git a/components/cic_unification/coercGraph.ml b/components/cic_unification/coercGraph.ml index cb33d9e32..43e342e70 100644 --- a/components/cic_unification/coercGraph.ml +++ b/components/cic_unification/coercGraph.ml @@ -41,14 +41,15 @@ let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () let saturate_coercion ul metasenv subst context = - let cl = List.map CicUtil.term_of_uri ul in + let cl = + List.map (fun u,saturations -> CicUtil.term_of_uri u,saturations) ul in let funclass_arityl = - let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in + let _,tgtcarl = List.split (List.map (fun u,_ -> CoercDb.get_carr u) ul) in List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl in let freshmeta = CicMkImplicit.new_meta metasenv subst in List.map2 - (fun arity c -> + (fun arity (c,saturations) -> let ty,_ = CicTypeChecker.type_of_aux' ~subst metasenv context c CicUniv.empty_ugraph in @@ -57,7 +58,7 @@ let saturate_coercion ul metasenv subst context = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - metasenv, Cic.Meta (lastmeta-1,irl), + metasenv, Cic.Meta (lastmeta - saturations - 1,irl), match args with [] -> c | _ -> Cic.Appl (c::args) @@ -128,18 +129,23 @@ let generate_dot_file () = Pp.node (CoercDb.name_of_carr carr) ~attrs:["href", UriManager.string_of_uri uri] fmt in List.iter - (fun (src, tgt, cl) -> + (fun (src, tgt, ul) -> let src_name = CoercDb.name_of_carr src in let tgt_name = CoercDb.name_of_carr tgt in pp_description src; pp_description tgt; List.iter - (fun c -> + (fun (u,saturations) -> Pp.edge src_name tgt_name - ~attrs:[ "label", UriManager.name_of_uri c; - "href", UriManager.string_of_uri c ] + ~attrs:[ "label", + (UriManager.name_of_uri u ^ + if saturations = 0 then + "" + else + "(" ^ string_of_int saturations ^ ")"); + "href", UriManager.string_of_uri u ] fmt) - cl) + ul) l; Pp.trailer fmt; Buffer.contents buf @@ -186,7 +192,7 @@ let coerced_arg l = (************************* meet calculation stuff ********************) let eq_uri_opt u1 u2 = match u1,u2 with - | Some u1, Some u2 -> UriManager.eq u1 u2 + | Some (u1,_), Some (u2,_) -> UriManager.eq u1 u2 | None,Some _ | Some _, None -> false | None, None -> true ;; diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index d5eb9c241..b0c25bc1e 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -140,11 +140,12 @@ type 'term macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 11 +let magic = 12 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) - | Coercion of loc * UriManager.uri * bool (* add_obj *) * int (* arity *) + | Coercion of loc * UriManager.uri * bool (* add_obj *) * + int (* arity *) * int (* saturations *) | Default of loc * string * UriManager.uri list | Drop of loc | Include of loc * string diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 14b7d180c..de7af8263 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -263,13 +263,15 @@ let pp_default what uris = Printf.sprintf "default \"%s\" %s" what (String.concat " " (List.map UriManager.string_of_uri uris)) -let pp_coercion uri do_composites arity = - Printf.sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity - (if do_composites then "compounds" else "no compounds") +let pp_coercion uri do_composites arity saturations= + Printf.sprintf "coercion %s %d %d (* %s *)" + (UriManager.string_of_uri uri) arity saturations + (if do_composites then "compounds" else "no compounds") let pp_command ~term_pp ~obj_pp = function | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri - | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i + | Coercion (_, uri, do_composites, i, j) -> + pp_coercion uri do_composites i j | Default (_,what,uris) -> pp_default what uris | Drop _ -> "drop" | Include (_,path) -> "include \"" ^ path ^ "\"" diff --git a/components/grafite/grafiteMarshal.ml b/components/grafite/grafiteMarshal.ml index 056b1225d..7731902b4 100644 --- a/components/grafite/grafiteMarshal.ml +++ b/components/grafite/grafiteMarshal.ml @@ -44,8 +44,8 @@ let rehash_cmd_uris = | GrafiteAst.Default (loc, name, uris) -> let uris = List.map rehash_uri uris in GrafiteAst.Default (loc, name, uris) - | GrafiteAst.Coercion (loc, uri, close, arity) -> - GrafiteAst.Coercion (loc, rehash_uri uri, close, arity) + | GrafiteAst.Coercion (loc, uri, close, arity, saturations) -> + GrafiteAst.Coercion (loc, rehash_uri uri, close, arity, saturations) | GrafiteAst.Index (loc, key, uri) -> GrafiteAst.Index (loc, HExtlib.map_option CicUtil.rehash_term key, rehash_uri uri) | cmd -> diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index a31f3990e..7cf1520ab 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -456,8 +456,8 @@ type 'a eval_executable = type 'a eval_from_moo = { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status } -let coercion_moo_statement_of (uri,arity) = - GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity) +let coercion_moo_statement_of (uri,arity, saturations) = + GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity, saturations) let refinement_toolkit = { RefinementTool.type_of_aux' = @@ -482,17 +482,17 @@ let refinement_toolkit = { RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj; } -let eval_coercion status ~add_composites uri arity baseuri = +let eval_coercion status ~add_composites uri arity saturations baseuri = let status,compounds = - GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity - baseuri + GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity + saturations baseuri in let moo_content = - List.map coercion_moo_statement_of ((uri,arity)::compounds) + List.map coercion_moo_statement_of ((uri,arity,saturations)::compounds) in let status = GrafiteTypes.add_moo_content moo_content status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, - List.map fst compounds + List.map (fun u,_,_ -> u) compounds module MatitaStatus = struct @@ -603,9 +603,9 @@ let add_coercions_of_record_to_moo obj lemmas status = in let is_a_coercion, arity_coercion = is_a_coercion uri in if is_a_coercion then - Some (uri, coercion_moo_statement_of (uri,arity_coercion)) + Some (uri, coercion_moo_statement_of (uri,arity_coercion,0)) else if is_a_wanted_coercion then - Some (uri, coercion_moo_statement_of (uri,arity_wanted)) + Some (uri, coercion_moo_statement_of (uri,arity_wanted,0)) else None) lemmas) @@ -648,8 +648,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status *) let status = GrafiteTypes.add_moo_content [cmd] status in status,[] - | GrafiteAst.Coercion (loc, uri, add_composites, arity) -> - eval_coercion status ~add_composites uri arity + | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) -> + eval_coercion status ~add_composites uri arity saturations (GrafiteTypes.get_string_option status "baseuri") | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; diff --git a/components/grafite_engine/grafiteSync.ml b/components/grafite_engine/grafiteSync.ml index fecdde3c6..067fe9b59 100644 --- a/components/grafite_engine/grafiteSync.ml +++ b/components/grafite_engine/grafiteSync.ml @@ -99,9 +99,12 @@ let add_obj refinement_toolkit uri obj status = GrafiteTypes.universe = universe}, lemmas -let add_coercion refinement_toolkit ~add_composites status uri arity baseuri = +let add_coercion refinement_toolkit ~add_composites status uri arity + saturations baseuri += let compounds = - LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity baseuri in + LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity + saturations baseuri in {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions}, compounds diff --git a/components/grafite_engine/grafiteSync.mli b/components/grafite_engine/grafiteSync.mli index 42b29a9fa..0a2595430 100644 --- a/components/grafite_engine/grafiteSync.mli +++ b/components/grafite_engine/grafiteSync.mli @@ -31,9 +31,10 @@ val add_obj: val add_coercion: RefinementTool.kit -> add_composites:bool -> GrafiteTypes.status -> - UriManager.uri -> int -> + UriManager.uri -> int -> int -> string (* baseuri *) -> - GrafiteTypes.status * (UriManager.uri * int) list (* URI and arity *) + GrafiteTypes.status * (UriManager.uri * int * int) list + (* URI, arity, saturations *) val time_travel: present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index e21083812..081055ce8 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -639,9 +639,11 @@ EXTEND ind_types in GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) - | IDENT "coercion" ; suri = URI ; arity = OPT int -> + | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int -> let arity = match arity with None -> 0 | Some x -> x in - GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity) + let saturations = match saturations with None -> 0 | Some x -> x in + GrafiteAst.Coercion + (loc, UriManager.uri_of_string suri, true, arity, saturations) | IDENT "record" ; (params,name,ty,fields) = record_spec -> GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index 42a19bcf9..85dc9f65b 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -26,14 +26,14 @@ (* $Id$ *) let close_coercion_graph_ref = ref - (fun _ _ _ _ -> [] : - CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> + (fun _ _ _ _ _ -> [] : + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list) + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list) ;; let set_close_coercion_graph f = close_coercion_graph_ref := f;; -let close_coercion_graph c1 c2 u s = - !close_coercion_graph_ref c1 c2 u s +let close_coercion_graph c1 c2 u sat s = + !close_coercion_graph_ref c1 c2 u sat s ;; diff --git a/components/library/cicCoercion.mli b/components/library/cicCoercion.mli index 5dc086ec4..d86229726 100644 --- a/components/library/cicCoercion.mli +++ b/components/library/cicCoercion.mli @@ -26,13 +26,13 @@ (* This module implements the Coercions transitive closure *) val set_close_coercion_graph : - (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> + (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list) + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list) -> unit val close_coercion_graph: - CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) list diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml index 1f3874912..e0dc18d05 100644 --- a/components/library/coercDb.ml +++ b/components/library/coercDb.ml @@ -99,7 +99,7 @@ let eq_carr ?(exact=false) src tgt = ;; let to_list () = - List.map (fun (s,t,l) -> s,t,List.map fst l) !db + List.map (fun (s,t,l) -> s,t,List.map (fun a,_,b -> a,b) l) !db ;; let rec myfilter p = function @@ -107,14 +107,14 @@ let rec myfilter p = function | (s,t,l)::tl -> let l = HExtlib.filter_map - (fun (u,n) -> - if p (s,t,u) then + (fun (u,n,saturations) -> + if p (s,t,u,saturations) then if n = 1 then None else - Some (u,n-1) + Some (u,n-1,saturations) else - Some (u,n)) + Some (u,n,saturations)) l in if l = [] then myfilter p tl else (s,t,l)::myfilter p tl @@ -124,7 +124,7 @@ let remove_coercion p = db := myfilter p !db;; let find_coercion f = List.map - fst + (fun uri,_,saturations -> uri,saturations) (List.flatten (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db)) ;; @@ -133,7 +133,7 @@ let get_carr uri = try let src, tgt, _ = List.find - (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq uri x) xl) + (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq uri x) xl) !db in src, tgt @@ -142,7 +142,7 @@ let get_carr uri = let is_a_coercion u = List.exists - (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq u x) xl) + (fun (_,_,xl) -> List.exists (fun (x,_,_) -> UriManager.eq u x) xl) !db ;; @@ -169,24 +169,26 @@ let term_of_carr = function | Term _ -> assert false ;; -let add_coercion (src,tgt,u) = +let add_coercion (src,tgt,u,saturations) = let f s t = eq_carr s src && eq_carr t tgt in let where = List.filter (fun (s,t,_) -> f s t) !db in let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in match where with - | [] -> db := (src,tgt,[u,1]) :: !db + | [] -> db := (src,tgt,[u,1,saturations]) :: !db | (src,tgt,l)::tl -> assert (tl = []); (* not sure, this may be a feature *) - if List.exists (fun (x,_) -> UriManager.eq u x) l then - let l' = List.map - (fun (x,n) -> if UriManager.eq u x then (x,n+1) else (x,n)) + if List.exists (fun (x,_,_) -> UriManager.eq u x) l then + let l' = List.map + (fun (x,n,saturations') -> + assert (saturations=saturations'); + if UriManager.eq u x then + (x,n+1,saturations) + else + (x,n,saturations)) l in db := (src,tgt,l')::tl @ rest else - db := (src,tgt,(u,1)::l)::tl @ rest + db := (src,tgt,(u,1,saturations)::l)::tl @ rest ;; - - - diff --git a/components/library/coercDb.mli b/components/library/coercDb.mli index e6d7e46b3..e1afd61aa 100644 --- a/components/library/coercDb.mli +++ b/components/library/coercDb.mli @@ -48,16 +48,16 @@ val uri_of_carr: coerc_carr -> UriManager.uri option val to_list: unit -> - (coerc_carr * coerc_carr * UriManager.uri list) list + (coerc_carr * coerc_carr * (UriManager.uri * int) list) list val add_coercion: - coerc_carr * coerc_carr * UriManager.uri -> unit + coerc_carr * coerc_carr * UriManager.uri * int -> unit val remove_coercion: - (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit + (coerc_carr * coerc_carr * UriManager.uri * int -> bool) -> unit val find_coercion: - (coerc_carr * coerc_carr -> bool) -> UriManager.uri list + (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list val is_a_coercion: UriManager.uri -> bool val is_a_coercion': Cic.term -> bool diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 64f037922..cbc45e6a9 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -230,9 +230,11 @@ let generate_elimination_principles uri refinement_toolkit = let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; - CoercDb.remove_coercion (fun (_,_,u1) -> true) + CoercDb.remove_coercion (fun (_,_,_,_) -> true) -let add_coercion ~add_composites refinement_toolkit uri arity baseuri = +let add_coercion ~add_composites refinement_toolkit uri arity saturations + baseuri += let coer_ty,_ = let coer = CicUtil.term_of_uri uri in CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph @@ -248,7 +250,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri = * should we saturate it with metas in case we insert it? * *) - let spline2list ty = + let spine2list ty = let rec aux = function | Cic.Prod( _, src, tgt) -> src::aux tgt | t -> [t] @@ -256,30 +258,34 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri = aux ty in let src_carr, tgt_carr = - let list_remove_from_tail n l = - let rec aux n = function - | hd::tl when n > 0 -> aux (n-1) tl - | l when n = 0 -> l - | _ -> assert false + let get_classes arity saturations l = + let rec aux target = function + 0,0,tgt::src::_ when target = None -> src,Some (`Class tgt) + | 0,0,src::_ when target <> None -> src,target + | 0,saturations,tgt::tl when target = None -> + aux (Some (`Class tgt)) (0,saturations,tl) + | 0,saturations,_::tl -> + aux target (0,saturations - 1,tl) + | arity,saturations,_::tl -> + aux (Some `Funclass) (arity - 1, saturations, tl) + | _,_,_ -> assert false in - aux n (List.rev l) + aux None (arity,saturations,List.rev l) in - let types = spline2list coer_ty in - match arity, list_remove_from_tail arity types with - | 0,tgt::src::_ -> - (* if ~delta is true, it is impossible to define an identity coercion *) - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src), - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) - | n,_::src::_ -> - CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src), - CoercDb.Fun arity - | _ -> assert false + let types = spine2list coer_ty in + let src,tgt = get_classes arity saturations types in + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src), + match tgt with + None -> assert false + | Some `Funclass -> CoercDb.Fun arity + | Some (`Class tgt) -> + CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt) in let already_in_obj src_carr tgt_carr uri obj = List.exists (fun (s,t,ul) -> List.exists - (fun u -> + (fun u,_ -> let bo = match obj with | Cic.Constant (_, Some bo, _, _, _) -> bo @@ -294,36 +300,37 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri = ("Coercions " ^ UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri uri^" are not convertible, but are between the same nodes.\n"^ - "From now on nification can fail randomly."); + "From now on unification can fail randomly."); false)) ul) (CoercDb.to_list ()) in if not add_composites then - (CoercDb.add_coercion (src_carr, tgt_carr, uri);[]) + (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[]) else let new_coercions = - CicCoercion.close_coercion_graph src_carr tgt_carr uri + CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations baseuri in let new_coercions = - List.filter (fun (s,t,u,obj) -> not(already_in_obj s t u obj)) + List.filter (fun (s,t,u,saturations,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,_) -> CoercDb.add_coercion (src,tgt,uri)) + (fun (src,tgt,uri,saturations,_) -> + CoercDb.add_coercion (src,tgt,uri,saturations)) new_coercions; - CoercDb.add_coercion (src_carr, tgt_carr, uri); + CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations); (* add the composites obj and they eventual lemmas *) let lemmas = if add_composites then List.fold_left - (fun acc (_,tgt,uri,obj) -> + (fun acc (_,tgt,uri,saturations,obj) -> add_single_obj uri obj refinement_toolkit; let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in - (uri,arity)::acc) + (uri,arity,saturations)::acc) [] new_coercions else [] @@ -355,10 +362,10 @@ let remove_coercion uri = List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) composites_in_db;*) UriManager.UriHashtbl.remove coercion_hashtbl uri; - CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u); + CoercDb.remove_coercion (fun (_,_,u,_) -> UriManager.eq uri u); (* remove from the DB *) List.iter - (fun u -> CoercDb.remove_coercion (fun (_,_,u1) -> UriManager.eq u u1)) + (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1)) composites_in_db; (* remove composites from the lib *) List.iter remove_single_obj composites_in_lib @@ -375,6 +382,7 @@ let generate_projections refinement_toolkit uri fields = try List.iter2 (fun (uri, name, bo) (_name, coercion, arity) -> + let saturations = 0 in try let ty, ugraph = CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in @@ -390,14 +398,14 @@ let generate_projections refinement_toolkit uri fields = every time. Right? *) let x = add_coercion ~add_composites:true refinement_toolkit uri arity - (UriManager.buri_of_uri uri) + saturations (UriManager.buri_of_uri uri) in (*prerr_endline ("are: "); List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x; prerr_endline "---"; *) (*CSC: I throw the arity away. See comment above *) - List.map fst x + List.map (fun u,_,_ -> u) x end else [] diff --git a/components/library/librarySync.mli b/components/library/librarySync.mli index 96e923100..980e4724a 100644 --- a/components/library/librarySync.mli +++ b/components/library/librarySync.mli @@ -48,8 +48,8 @@ val remove_obj: UriManager.uri -> unit val add_coercion: add_composites:bool -> RefinementTool.kit -> UriManager.uri -> int (* arity *) -> - string (* baseuri *) -> - (UriManager.uri * int) list (* URI and arity *) + int (* saturations *) -> string (* baseuri *) -> + (UriManager.uri * int * int) list (* URI, arity, saturations *) (* inverse of add_coercion, removes both the eventually created composite *) (* coercions and the information that [uri] and the composites are coercion *) diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml index 6c253df9f..0ab937ace 100644 --- a/components/tactics/closeCoercionGraph.ml +++ b/components/tactics/closeCoercionGraph.ml @@ -81,20 +81,25 @@ exception UnableToCompose (* 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 last_lam_with_inn_arg = +let generate_composite' (c1,sat1) (c2,sat2) context metasenv univ arity + last_lam_with_inn_arg += +assert (sat1 = 0); +assert (sat2 = 0); +let saturationsres = 0 in 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 let rec mk_implicits = function | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1) in - let rec mk_lambda_spline c namer = function + let rec mk_lambda_spine c namer = function | 0 -> c | n -> Cic.Lambda (namer n, (Cic.Implicit None), - mk_lambda_spline (CicSubstitution.lift 1 c) namer (n-1)) + mk_lambda_spine (CicSubstitution.lift 1 c) namer (n-1)) in let count_saturations_needed t arity = let rec aux acc n = function @@ -177,7 +182,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = | Cic.Appl l -> List.tl l | _ -> assert false in - (* i should cut off the laet elem of l_c2 *) + (* i should cut off the last elem of l_c2 *) let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in List.sort (fun (i,ctx1,ty1) (j,ctx1,ty1) -> @@ -204,8 +209,8 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = let saturations_for_c1, names_c1 = count_saturations_needed c1_ty 0 in let saturations_for_c2, names_c2 = count_saturations_needed c2_ty arity 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 (namer (names_c1 @ names_c2)) spline_len in + let spine_len = saturations_for_c1 + saturations_for_c2 in + let c = mk_lambda_spine c (namer (names_c1 @ names_c2)) spine_len in debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); let old_insert_coercions = !CicRefine.insert_coercions in let c, metasenv, univ = @@ -218,13 +223,13 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = (* let metasenv = order_metasenv metasenv in *) (* debug_print(lazy("ORDERED MENV: "^CicMetaSubst.ppmetasenv [] metasenv)); *) let body_metasenv, lambdas_metasenv = - split_metasenv metasenv (spline_len + List.length context) + split_metasenv metasenv (spine_len + List.length context) in debug_print(lazy("B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv)); debug_print(lazy("L_MENV: "^CicMetaSubst.ppmetasenv [] lambdas_metasenv)); let body_metasenv = order_body_menv term body_metasenv in debug_print(lazy("ORDERED_B_MENV: "^CicMetaSubst.ppmetasenv [] body_metasenv)); - let subst = create_subst_from_metas_to_rels spline_len body_metasenv in + let subst = create_subst_from_metas_to_rels spine_len body_metasenv in debug_print (lazy("SUBST: "^CicMetaSubst.ppsubst body_metasenv subst)); let term = CicMetaSubst.apply_subst subst term in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in @@ -233,7 +238,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = CicRefine.type_of_aux' metasenv context term ugraph in let body_metasenv, lambdas_metasenv = - split_metasenv metasenv (spline_len + List.length context) + split_metasenv metasenv (spine_len + List.length context) in let lambdas_metasenv = List.filter @@ -264,7 +269,7 @@ let generate_composite c1 c2 context metasenv univ arity last_lam_with_inn_arg = CicRefine.insert_coercions := old_insert_coercions; raise exn in - c, metasenv, univ + c, metasenv, univ, saturationsres ;; let build_obj c univ arity = @@ -291,7 +296,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)) @@ -340,10 +345,10 @@ let number_if_already_defined buri name l = (* 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 baseuri = +let close_coercion_graph src tgt uri saturations baseuri = (* 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 = get_closure_coercions src tgt (uri,saturations) coercions in let todo_list = filter_duplicates todo_list coercions in try let new_coercions = @@ -352,43 +357,45 @@ let close_coercion_graph src tgt uri baseuri = try (match l with | [] -> assert false - | he :: tl -> + | (he,saturations1) :: 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 arity) + Cic.Sort Cic.Prop, [], obj_attrs arity), saturations1 in let o,_ = - List.fold_left (fun (o,univ) coer -> + List.fold_left (fun (o,univ) (coer,saturations) -> match o with - | Cic.Constant (_,Some c,_,[],_) -> - let t, menv, univ = - generate_composite c - (CoercDb.term_of_carr (CoercDb.Uri coer)) + | Cic.Constant (_,Some u,_,[],_),saturations1 -> + let t, menv, univ, saturationsres = + generate_composite' (u,saturations1) + (CoercDb.term_of_carr (CoercDb.Uri coer), + saturations) [] [] univ arity true in if (menv = []) then HLog.warn "MENV non empty after composing coercions"; - build_obj t univ arity + let o,univ = build_obj t univ arity in + (o,saturationsres),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 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 = + let named_obj,saturations = match o with - | Cic.Constant (_,bo,ty,vl,attrs) -> - Cic.Constant (name,bo,ty,vl,attrs) + | Cic.Constant (_,bo,ty,vl,attrs),saturations -> + Cic.Constant (name,bo,ty,vl,attrs),saturations | _ -> assert false in - (src,tgt,c_uri,named_obj))::acc + (src,tgt,c_uri,saturations,named_obj))::acc with UnableToCompose -> acc ) [] todo_list in @@ -397,3 +404,12 @@ let close_coercion_graph src tgt uri baseuri = ;; 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 b = + let a,b,c,_ = + generate_composite' (c1,0) (c2,0) context metasenv univ arity b + in + a,b,c +;; diff --git a/components/tactics/closeCoercionGraph.mli b/components/tactics/closeCoercionGraph.mli index 8750ce0f7..1acea0eeb 100644 --- a/components/tactics/closeCoercionGraph.mli +++ b/components/tactics/closeCoercionGraph.mli @@ -26,9 +26,10 @@ (* This module implements the Coercions transitive closure *) val close_coercion_graph: - CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj) + list exception UnableToCompose diff --git a/matita/matita.ml b/matita/matita.ml index 58d404888..a326754dc 100644 --- a/matita/matita.ml +++ b/matita/matita.ml @@ -250,7 +250,12 @@ let _ = List.iter (fun (s,t,ul) -> HLog.debug - ((String.concat "," (List.map UriManager.name_of_uri ul)) ^ ":" + ((String.concat "," + (List.map + (fun u,saturations -> + UriManager.name_of_uri u ^ + "(" ^ string_of_int saturations ^ ")") + ul)) ^ ":" ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t)) (CoercDb.to_list ())); addDebugSeparator (); -- 2.39.2