From d7227b93729c13636d297b959b7d8c178dfe3aaf Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 5 Dec 2006 15:44:54 +0000 Subject: [PATCH] - components: composed coercions mus be generated with current base uri - transcript: fixed to handle coercions from constructors - CoRN-Decl: regenerated. CoRN.ma now compiles! --- components/binaries/transcript/CoRN.conf.xml | 4 +++- components/binaries/transcript/engine.ml | 6 ++---- components/grafite_engine/grafiteEngine.ml | 4 +++- components/grafite_engine/grafiteSync.ml | 4 ++-- components/grafite_engine/grafiteSync.mli | 1 + components/library/cicCoercion.ml | 5 ++--- components/library/cicCoercion.mli | 1 + components/library/librarySync.ml | 4 +++- components/library/librarySync.mli | 1 + matita/contribs/CoRN-Decl/CoRN.ma | 4 ++-- matita/contribs/CoRN-Decl/model/structures/Zsec.ma | 2 +- matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma | 2 +- 12 files changed, 22 insertions(+), 16 deletions(-) diff --git a/components/binaries/transcript/CoRN.conf.xml b/components/binaries/transcript/CoRN.conf.xml index ad576e986..e904b4d4e 100644 --- a/components/binaries/transcript/CoRN.conf.xml +++ b/components/binaries/transcript/CoRN.conf.xml @@ -8,6 +8,8 @@ /projects/helm/exportation/CoRN $(transcript.helm_dir)/matita/contribs/CoRN-Decl .v - Z_of_nat cic:/Coq/ZArith/BinInt + Z_of_nat cic:/Coq/ZArith/BinInt/Z_of_nat.con + Zpos cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2) + nat_of_P cic:/Coq/NArith/BinPos/nat_of_P.con diff --git a/components/binaries/transcript/engine.ml b/components/binaries/transcript/engine.ml index 9824426da..61787318b 100644 --- a/components/binaries/transcript/engine.ml +++ b/components/binaries/transcript/engine.ml @@ -186,10 +186,8 @@ let produce st = end | T.Coercion (b, obj) -> let str = get_coercion st obj in - let base_uri = - if str <> "" then str else - if b then out_base_uri else in_base_uri - in + if str <> "" then path, Some (T.Coercion (b, str)) else + let base_uri = if b then out_base_uri else in_base_uri in let s = obj ^ G.string_of_inline_kind T.Con in path, Some (T.Coercion (b, Filename.concat base_uri s)) | T.Section (b, id, _) as item -> diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index f95829797..a747223c7 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -444,9 +444,10 @@ let refinement_toolkit = { RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj; } -let eval_coercion status ~add_composites uri arity = +let eval_coercion status ~add_composites uri arity baseuri = let status,compounds = GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity + baseuri in let moo_content = List.map (coercion_moo_statement_of arity) (uri::compounds) @@ -643,6 +644,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status,[] | GrafiteAst.Coercion (loc, uri, add_composites, arity) -> eval_coercion status ~add_composites uri arity + (GrafiteTypes.get_string_option status "baseuri") | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,[] diff --git a/components/grafite_engine/grafiteSync.ml b/components/grafite_engine/grafiteSync.ml index 10dfef58a..fecdde3c6 100644 --- a/components/grafite_engine/grafiteSync.ml +++ b/components/grafite_engine/grafiteSync.ml @@ -99,9 +99,9 @@ let add_obj refinement_toolkit uri obj status = GrafiteTypes.universe = universe}, lemmas -let add_coercion refinement_toolkit ~add_composites status uri arity = +let add_coercion refinement_toolkit ~add_composites status uri arity baseuri = let compounds = - LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity in + LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity 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 8453dd645..571b7a91a 100644 --- a/components/grafite_engine/grafiteSync.mli +++ b/components/grafite_engine/grafiteSync.mli @@ -32,6 +32,7 @@ val add_coercion: RefinementTool.kit -> add_composites:bool -> GrafiteTypes.status -> UriManager.uri -> int -> + string (* baseuri *) -> GrafiteTypes.status * UriManager.uri list val time_travel: diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index d7ad886b2..6f2443e98 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -302,7 +302,7 @@ 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 rt src tgt uri = +let close_coercion_graph rt src tgt uri baseuri = (* check if the coercion already exists *) let coercions = CoercDb.to_list () in let todo_list = get_closure_coercions src tgt uri coercions in @@ -334,9 +334,8 @@ let close_coercion_graph rt src tgt uri = 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 + number_if_already_defined baseuri name (List.map (fun (_,_,u,_) -> u) acc) in let named_obj = diff --git a/components/library/cicCoercion.mli b/components/library/cicCoercion.mli index 7e4f03ab8..e3ee8dbfc 100644 --- a/components/library/cicCoercion.mli +++ b/components/library/cicCoercion.mli @@ -28,5 +28,6 @@ val close_coercion_graph: RefinementTool.kit -> CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> + string (* baseuri *) -> (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 5e8ddaf6d..4dc20f77f 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -211,7 +211,7 @@ let remove_all_coercions () = UriManager.UriHashtbl.clear coercion_hashtbl; CoercDb.remove_coercion (fun (_,_,u1) -> true) -let add_coercion ~add_composites refinement_toolkit uri arity = +let add_coercion ~add_composites refinement_toolkit uri arity baseuri = let coer_ty,_ = let coer = CicUtil.term_of_uri uri in CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph @@ -270,6 +270,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity = else let new_coercions = CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri + baseuri in let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in if already_in then @@ -359,6 +360,7 @@ let generate_projections refinement_toolkit uri fields = (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*) let x = add_coercion ~add_composites:true refinement_toolkit uri arity + (UriManager.buri_of_uri uri) in (*prerr_endline ("are: "); List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x; diff --git a/components/library/librarySync.mli b/components/library/librarySync.mli index 06b1010ab..a836dfd57 100644 --- a/components/library/librarySync.mli +++ b/components/library/librarySync.mli @@ -48,6 +48,7 @@ val remove_obj: UriManager.uri -> unit val add_coercion: add_composites:bool -> RefinementTool.kit -> UriManager.uri -> int (* arity *) -> + string (* baseuri *) -> UriManager.uri list (* inverse of add_coercion, removes both the eventually created composite *) diff --git a/matita/contribs/CoRN-Decl/CoRN.ma b/matita/contribs/CoRN-Decl/CoRN.ma index 6a0b5b4f3..e75ca0748 100644 --- a/matita/contribs/CoRN-Decl/CoRN.ma +++ b/matita/contribs/CoRN-Decl/CoRN.ma @@ -619,7 +619,7 @@ coercion cic:/CoRN/model/structures/Qsec/inject_Z.con 0 (* compounds *). Infix "{#Z}" := ap_Z (no associativity, at level 90). *) -coercion cic:/CoRN/model/structures/Zsec/Zpos.con 0 (* compounds *). +coercion cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2) 0 (* compounds *). (* From reals/Bridges_LUB *************************************************) @@ -689,7 +689,7 @@ Notation "( A , B )" := (pairT A B). (* From reals/Q_in_CReals *************************************************) -coercion cic:/CoRN/reals/Q_in_CReals/nat_of_P.con 0 (* compounds *). +coercion cic:/Coq/NArith/BinPos/nat_of_P.con 0 (* compounds *). (* From reals/R_morphism **************************************************) diff --git a/matita/contribs/CoRN-Decl/model/structures/Zsec.ma b/matita/contribs/CoRN-Decl/model/structures/Zsec.ma index 7251b8f06..b7aa226b1 100644 --- a/matita/contribs/CoRN-Decl/model/structures/Zsec.ma +++ b/matita/contribs/CoRN-Decl/model/structures/Zsec.ma @@ -74,7 +74,7 @@ inline "cic:/CoRN/model/structures/Zsec/Zpos.con". (* begin hide *) -coercion cic:/matita/CoRN-Decl/model/structures/Zsec/Zpos.con 0 (* compounds *). +coercion cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2) 0 (* compounds *). (* end hide *) diff --git a/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma b/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma index f9fca0040..1a7f26cf1 100644 --- a/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma +++ b/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma @@ -59,7 +59,7 @@ inline "cic:/CoRN/reals/Q_in_CReals/Archimedes'.con". (*#**************************************) -coercion cic:/matita/CoRN-Decl/reals/Q_in_CReals/nat_of_P.con 0 (* compounds *). +coercion cic:/Coq/NArith/BinPos/nat_of_P.con 0 (* compounds *). (* end hide *) -- 2.39.2