- refreshing of uris in NotationPt.terms implemented

diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml
index a2ab34833cd098ea72335c56d9242c2ec60498cf..3d80e8fd51427a0d091335a95e186b1b4553d91f 100644 (file)
--- a/matita/components/content/notationUtil.ml
+++ b/matita/components/content/notationUtil.ml
@@ -397,4 +397,19 @@ let freshen_obj obj =
 
 let freshen_term = freshen_term ?index:None
 
-let refresh_uri_in_term t = assert false
+let rec refresh_uri_in_term ~refresh_uri_in_term:refresh_in_cic
+ ~refresh_uri_in_reference
+=
+ function
+    NotationPt.NRef ref -> NotationPt.NRef (refresh_uri_in_reference ref)
+  | NotationPt.NCic t -> NotationPt.NCic (refresh_in_cic t)
+  | t ->
+     visit_ast
+     (refresh_uri_in_term ~refresh_uri_in_term:refresh_in_cic
+       ~refresh_uri_in_reference) t
+      ~special_k:(fun x -> x)
+      ~map_xref_option:(function Some ref -> Some (refresh_uri_in_reference ref)
+                         | x -> x)
+      ~map_case_indty:(function (Some (s,Some ref)) -> Some (s, Some
+                        (refresh_uri_in_reference ref)) | x -> x)
+;;

diff --git a/matita/components/content/notationUtil.mli b/matita/components/content/notationUtil.mli
index f1c96c5364a27c574b70822cd55fa7171925f324..ac291a2cebc72156afa5ffb44c54380a4a158832 100644 (file)
--- a/matita/components/content/notationUtil.mli
+++ b/matita/components/content/notationUtil.mli
@@ -92,4 +92,7 @@ type notation_id
 
 val fresh_id: unit -> notation_id
 
-val refresh_uri_in_term: NotationPt.term -> NotationPt.term
+val refresh_uri_in_term:
+ refresh_uri_in_term:(NCic.term -> NCic.term) ->
+ refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
+  NotationPt.term -> NotationPt.term

diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index 1f83a64d57d9b6ff0bc3e09f46d4156d4f0e4c3d..7379dd693e128b5c480298d7249b704047d322d2 100644 (file)
--- a/matita/components/content_pres/cicNotationParser.ml
+++ b/matita/components/content_pres/cicNotationParser.ml
@@ -48,8 +48,11 @@ type ('a,'b,'c,'d) grammars = {
 
 type checked_l1_pattern = CL1P of NotationPt.term * int
 
-let refresh_uri_in_checked_l1_pattern (CL1P (t,n)) =
- CL1P (NotationUtil.refresh_uri_in_term t, n)
+let refresh_uri_in_checked_l1_pattern ~refresh_uri_in_term
+     ~refresh_uri_in_reference (CL1P (t,n))
+=
+ CL1P (NotationUtil.refresh_uri_in_term ~refresh_uri_in_term
+ ~refresh_uri_in_reference t, n)
 
 type binding =
   | NoBinding

diff --git a/matita/components/content_pres/cicNotationParser.mli b/matita/components/content_pres/cicNotationParser.mli
index 1cbef668d98e1c85254455480297f49642311184..1b6a0cf7dc6ac979e4baed16c804a4032a959e1e 100644 (file)
--- a/matita/components/content_pres/cicNotationParser.mli
+++ b/matita/components/content_pres/cicNotationParser.mli
@@ -42,7 +42,10 @@ class status: keywords:string list ->
 
 type checked_l1_pattern = private CL1P of NotationPt.term * int
 
-val refresh_uri_in_checked_l1_pattern: checked_l1_pattern -> checked_l1_pattern 
+val refresh_uri_in_checked_l1_pattern:
+ refresh_uri_in_term:(NCic.term -> NCic.term) ->
+ refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
+  checked_l1_pattern -> checked_l1_pattern 
 
 (** {2 Parsing functions} *)
 

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 30c176fd2a3cd98188c2aaf8b02955aa4e391c37..855b1f70899b584b7e125d2f5539bce9001b7de2 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -40,8 +40,7 @@ let basic_eval_unification_hint (t,n) status =
 
 let inject_unification_hint =
  let basic_eval_unification_hint (t,n) 
-   ~refresh_uri_in_universe 
-   ~refresh_uri_in_term
+   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
  =
   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
  in
@@ -83,7 +82,7 @@ let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern) status =
 
 let inject_interpretation =
  let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
-   ~refresh_uri_in_universe ~refresh_uri_in_term
+   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
  =
   let rec refresh =
    function
@@ -112,7 +111,8 @@ let basic_eval_alias (mode,diff) status =
 ;;
 
 let inject_alias =
- let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term=
+ let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term
+   ~refresh_uri_in_reference =
    basic_eval_alias (mode,diff)
  in
   GrafiteTypes.Serializer.register#run "alias" basic_eval_alias
@@ -133,10 +133,14 @@ let basic_eval_input_notation (l1,l2) status =
 
 let inject_input_notation =
  let basic_eval_input_notation (l1,l2)
-  ~refresh_uri_in_universe ~refresh_uri_in_term
+  ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
  =
-   let l1 = CicNotationParser.refresh_uri_in_checked_l1_pattern l1 in
-   let l2 = NotationUtil.refresh_uri_in_term l2 in
+   let l1 =
+    CicNotationParser.refresh_uri_in_checked_l1_pattern
+     ~refresh_uri_in_term ~refresh_uri_in_reference l1 in
+   let l2 = NotationUtil.refresh_uri_in_term
+     ~refresh_uri_in_term ~refresh_uri_in_reference l2
+   in
     basic_eval_input_notation (l1,l2)
  in
   GrafiteTypes.Serializer.register#run "input_notation"
@@ -155,10 +159,14 @@ let basic_eval_output_notation (l1,l2) status =
 
 let inject_output_notation =
  let basic_eval_output_notation (l1,l2)
-  ~refresh_uri_in_universe ~refresh_uri_in_term
+  ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
  =
-  let l1 = CicNotationParser.refresh_uri_in_checked_l1_pattern l1 in
-  let l2 = NotationUtil.refresh_uri_in_term l2 in
+  let l1 =
+   CicNotationParser.refresh_uri_in_checked_l1_pattern
+    ~refresh_uri_in_term ~refresh_uri_in_reference l1 in
+  let l2 = NotationUtil.refresh_uri_in_term
+    ~refresh_uri_in_term ~refresh_uri_in_reference l2
+  in
    basic_eval_output_notation (l1,l2)
  in
   GrafiteTypes.Serializer.register#run "output_notation"
@@ -172,9 +180,8 @@ let eval_output_notation status data=
 ;;
 
 let record_index_obj = 
- let aux l 
-   ~refresh_uri_in_universe 
-   ~refresh_uri_in_term
+ let aux l ~refresh_uri_in_universe 
+   ~refresh_uri_in_term ~refresh_uri_in_reference
  =
     basic_index_obj
       (List.map 
@@ -258,8 +265,7 @@ let index_eq uri status =
 
 let record_index_eq =
  let basic_index_eq uri
-   ~refresh_uri_in_universe 
-   ~refresh_uri_in_term 
+   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference 
    = index_eq (NCicLibrary.refresh_uri uri) 
  in
   GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
@@ -284,8 +290,7 @@ let basic_eval_add_constraint (u1,u2) status =
 
 let inject_constraint =
  let basic_eval_add_constraint (u1,u2) 
-       ~refresh_uri_in_universe 
-       ~refresh_uri_in_term
+       ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
  =
   let u1 = refresh_uri_in_universe u1 in 
   let u2 = refresh_uri_in_universe u2 in 

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index 7cc5644d99c54ea74e0b041cbd4963cae07daf4e..4522a0a1a917855a8aed045d35b1eaa52d753e94 100644 (file)
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -282,14 +282,16 @@ let basic_eval_ncoercion (name,t,s,d,p,a) status =
 ;;
 
 let record_ncoercion =
- let aux (name,t,s,d,p,a) ~refresh_uri_in_universe ~refresh_uri_in_term =
+ let aux (name,t,s,d,p,a) ~refresh_uri_in_term =
   let t = refresh_uri_in_term t in
   let s = refresh_uri_in_term s in
   let d = refresh_uri_in_term d in
    basic_index_ncoercion (name,t,s,d,p,a)
  in
- let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term =
-   List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l
+ let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
+  ~refresh_uri_in_reference
+ =
+   List.fold_right (aux ~refresh_uri_in_term) l
  in
   GrafiteTypes.Serializer.register#run "ncoercion" aux_l 
 ;;

diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index 70be8ae5768c31cf13bdc2c7e75a63dda843cf7c..ad8084692fd11f3951546183b36d65083da22b7b 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -22,13 +22,15 @@ let refresh_uri_in_universe =
  List.map (fun (x,u) -> x, refresh_uri u)
 ;;
 
+let refresh_uri_in_reference (NReference.Ref (uri,spec)) =
+ NReference.reference_of_spec (refresh_uri uri) spec
+
 let rec refresh_uri_in_term =
  function
   | NCic.Meta (i,(n,NCic.Ctx l)) ->
      NCic.Meta (i,(n,NCic.Ctx (List.map refresh_uri_in_term l)))
   | NCic.Meta _ as t -> t
-  | NCic.Const (NReference.Ref (u,spec)) ->
-     NCic.Const (NReference.reference_of_spec (refresh_uri u) spec)
+  | NCic.Const ref -> NCic.Const (refresh_uri_in_reference ref)
   | NCic.Sort (NCic.Type l) -> NCic.Sort (NCic.Type (refresh_uri_in_universe l))
   | NCic.Match (NReference.Ref (uri,spec),outtype,term,pl) ->
      let r = NReference.reference_of_spec (refresh_uri uri) spec in
@@ -196,6 +198,7 @@ module type SerializerType =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
     refresh_uri_in_term:(NCic.term -> NCic.term) ->
+    refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
      dumpable_status -> dumpable_status
 
   val register: < run: 'a.  string -> 'a register_type -> ('a -> obj) >
@@ -211,6 +214,7 @@ module Serializer(D: sig type dumpable_status end) =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
     refresh_uri_in_term:(NCic.term -> NCic.term) ->
+    refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
      dumpable_status -> dumpable_status
 
   let require1 = ref (fun _ -> assert false) (* unknown data*)
@@ -227,6 +231,7 @@ module Serializer(D: sig type dumpable_status end) =
       (fun ((tag',data) as x) ->
         if tag=tag' then
          require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
+          ~refresh_uri_in_reference
         else
          old_require1 x);
      (fun x -> tag,Obj.repr x)
@@ -244,7 +249,8 @@ module Serializer(D: sig type dumpable_status end) =
      raise (IncludedFileNotCompiled(path_of_baseuri baseuri,NUri.string_of_uri baseuri))
 
   let record_include =
-   let aux baseuri ~refresh_uri_in_universe ~refresh_uri_in_term =
+   let aux baseuri ~refresh_uri_in_universe ~refresh_uri_in_term
+   ~refresh_uri_in_reference =
      (* memorizzo baseuri in una tabella; *)
      require2 ~baseuri
    in

diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli
index b2015a9528f1def60d0f8dc869021dcd9a565520..9f641d1cafc52c758acaaf9a813d42e360650b7c 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.mli
+++ b/matita/components/ng_library/nCicLibrary.mli
@@ -48,6 +48,7 @@ module type SerializerType =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
     refresh_uri_in_term:(NCic.term -> NCic.term) ->
+    refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
      dumpable_status -> dumpable_status
 
   val register: < run: 'a.  string -> 'a register_type -> ('a -> obj) >