From d4f2d4c1a4784f84aa27e1bb96b8b377a6553c65 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 5 Nov 2010 10:42:10 +0000 Subject: [PATCH] - refreshing of uris in NotationPt.terms implemented --- matita/components/content/notationUtil.ml | 17 +++++++- matita/components/content/notationUtil.mli | 5 ++- .../content_pres/cicNotationParser.ml | 7 +++- .../content_pres/cicNotationParser.mli | 5 ++- .../grafite_engine/grafiteEngine.ml | 39 +++++++++++-------- .../grafite_engine/nCicCoercDeclaration.ml | 8 ++-- matita/components/ng_library/nCicLibrary.ml | 12 ++++-- matita/components/ng_library/nCicLibrary.mli | 1 + 8 files changed, 66 insertions(+), 28 deletions(-) diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml index a2ab34833..3d80e8fd5 100644 --- 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 f1c96c536..ac291a2ce 100644 --- 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 1f83a64d5..7379dd693 100644 --- 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 1cbef668d..1b6a0cf7d 100644 --- 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 30c176fd2..855b1f708 100644 --- 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 7cc5644d9..4522a0a1a 100644 --- 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 70be8ae57..ad8084692 100644 --- 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 b2015a952..9f641d1ca 100644 --- 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) > -- 2.39.2