- components: composed coercions mus be generated with current base uri

- transcript: fixed to handle coercions from constructors
- CoRN-Decl: regenerated. CoRN.ma now compiles!

diff --git a/helm/software/components/binaries/transcript/CoRN.conf.xml b/helm/software/components/binaries/transcript/CoRN.conf.xml
index ad576e986226e7672db29a9b8a4406dad1582e96..e904b4d4e7a3a45ea3b4413f514ca6ecff58913b 100644 (file)
--- a/helm/software/components/binaries/transcript/CoRN.conf.xml
+++ b/helm/software/components/binaries/transcript/CoRN.conf.xml
@@ -8,6 +8,8 @@
     <key name="input_path">/projects/helm/exportation/CoRN</key>
     <key name="output_path">$(transcript.helm_dir)/matita/contribs/CoRN-Decl</key>
     <key name="script_type">.v</key>
-    <key name="coercion">Z_of_nat cic:/Coq/ZArith/BinInt</key>
+    <key name="coercion">Z_of_nat cic:/Coq/ZArith/BinInt/Z_of_nat.con</key>
+    <key name="coercion">Zpos cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2)</key>
+    <key name="coercion">nat_of_P cic:/Coq/NArith/BinPos/nat_of_P.con</key>
   </section>
 </helm_registry>

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index 9824426daf5497dceb4c62ec5590b3323a65cf1c..61787318b430edc46b92c71df2aa9547cf93ddea 100644 (file)
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/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/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index f95829797a3c91ea75be791f83fac86d0f16ab03..a747223c7dea4136e5a54a6b69f59eed4d0bc427 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/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/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index 10dfef58aa0d18a74195f8d2f85bf7e72012c439..fecdde3c6a8321edcadec528908ff138222e611f 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/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/helm/software/components/grafite_engine/grafiteSync.mli b/helm/software/components/grafite_engine/grafiteSync.mli
index 8453dd64559c994627348c13389d957698e88c99..571b7a91a1da7d29044f6257ba95f3cca7052629 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteSync.mli
+++ b/helm/software/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/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml
index d7ad886b2c8fa33a07213faf7ea8b98bb9e974b4..6f2443e98a45798f511279a0c5dd74e0a7e5bd07 100644 (file)
--- a/helm/software/components/library/cicCoercion.ml
+++ b/helm/software/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/helm/software/components/library/cicCoercion.mli b/helm/software/components/library/cicCoercion.mli
index 7e4f03ab8607bb9dc6d94d453f3f189360875191..e3ee8dbfc8d46ed2418d1d988cc13da57d9a048e 100644 (file)
--- a/helm/software/components/library/cicCoercion.mli
+++ b/helm/software/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/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 5e8ddaf6d5db898229d0cd7aec7b1eb72bda2bcf..4dc20f77fa968ed961361a7449c69646d06b8037 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/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/helm/software/components/library/librarySync.mli b/helm/software/components/library/librarySync.mli
index 06b1010ab500e05cd43aa0bbe1a8c08e6724de3e..a836dfd5788df205ac27ffd35ef539bd80dc05f0 100644 (file)
--- a/helm/software/components/library/librarySync.mli
+++ b/helm/software/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/helm/software/matita/contribs/CoRN-Decl/CoRN.ma b/helm/software/matita/contribs/CoRN-Decl/CoRN.ma
index 6a0b5b4f3691d38b32b8ef226169ab77d49e6bd5..e75ca07486cdc79fc1a13516eb1164508b09436d 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/CoRN.ma
+++ b/helm/software/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/helm/software/matita/contribs/CoRN-Decl/model/structures/Zsec.ma b/helm/software/matita/contribs/CoRN-Decl/model/structures/Zsec.ma
index 7251b8f066adba0434cbfb64ce64f6ee6f9eb200..b7aa226b1e3cf59977007a73a1d124a0fb99f70a 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/model/structures/Zsec.ma
+++ b/helm/software/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/helm/software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma b/helm/software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma
index f9fca0040875a146281e0dbe8415de7c03da8631..1a7f26cf17375e752343bfe88f6671b1772cecb4 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma
+++ b/helm/software/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 *)