Big change:

 - new command "include alias" to include only the aliases
 - "include" now always includes the aliases and it includes everything else
   only if the file has not been already included

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 32a29c2158a98e8f1dda73f10191a6a6f6fe3d54..1175d3cc131c7fc9a6083f5ea072c59ad4c1fef4 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -92,7 +92,7 @@ type alias_spec =
   | Symbol_alias of string * int * string (* name, instance no, description *)
   | Number_alias of int * string          (* instance no, description *)
 
-type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *)
+type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* aka aliases *)
 
 type command =
   | Include of loc * inclusion_mode * string (* _,buri,_,path *)

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 79391193dd1f0699de8913b03cd136e0903aff28..5997297cd765b2491551e91ba726e2372119f87a 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -41,8 +41,12 @@ 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_reference
+   ~alias_only status
  =
-  let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
+  if not alias_only then
+   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "unification_hints"
    basic_eval_unification_hint
@@ -69,9 +73,12 @@ let basic_index_obj l status =
     status#auto_cache l) 
 ;;     
 
-let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern) status =
+let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern) status =
  let status =
-  Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern
+  if not alias_only then
+   Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern
+  else
+   status
  in
  let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *)
  let diff =
@@ -83,6 +90,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_reference
+   ~alias_only
  =
   let rec refresh =
    function
@@ -94,14 +102,14 @@ let inject_interpretation =
     | NotationPt.ApplPattern l -> NotationPt.ApplPattern (List.map refresh l)
   in
   let cic_appl_pattern = refresh cic_appl_pattern in
-   basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
+   basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern)
  in
   GrafiteTypes.Serializer.register#run "interpretation"
    basic_eval_interpretation
 ;;
 
 let eval_interpretation status data= 
- let status = basic_eval_interpretation data status in
+ let status = basic_eval_interpretation ~alias_only:false data status in
  let dump = inject_interpretation data::status#dump in
   status#set_dump dump
 ;;
@@ -112,7 +120,7 @@ let basic_eval_alias (mode,diff) status =
 
 let inject_alias =
  let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term
-   ~refresh_uri_in_reference =
+   ~refresh_uri_in_reference ~alias_only =
    basic_eval_alias (mode,diff)
  in
   GrafiteTypes.Serializer.register#run "alias" basic_eval_alias
@@ -134,14 +142,18 @@ 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_reference
+  ~alias_only status
  =
-   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)
+   if not alias_only then
+    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) status
+   else
+    status
  in
   GrafiteTypes.Serializer.register#run "input_notation"
    basic_eval_input_notation
@@ -160,14 +172,18 @@ 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_reference
+  ~alias_only status
  =
-  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)
+  if not alias_only then
+   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) status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "output_notation"
    basic_eval_output_notation
@@ -181,12 +197,15 @@ let eval_output_notation status data=
 
 let record_index_obj = 
  let aux l ~refresh_uri_in_universe 
-   ~refresh_uri_in_term ~refresh_uri_in_reference
+   ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status
  =
+  if not alias_only then
     basic_index_obj
       (List.map 
         (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v) 
-      l)
+      l) status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "index_obj" aux
 ;;
@@ -266,7 +285,9 @@ 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_reference 
-   = index_eq (NCicLibrary.refresh_uri uri) 
+   ~alias_only status
+   = if not alias_only then index_eq (NCicLibrary.refresh_uri uri) status else
+     status
  in
   GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
 ;;
@@ -290,11 +311,15 @@ 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_reference
+     ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
+     ~alias_only status
  =
-  let u1 = refresh_uri_in_universe u1 in 
-  let u2 = refresh_uri_in_universe u2 in 
-  basic_eval_add_constraint (u1,u2)
+  if not alias_only then
+   let u1 = refresh_uri_in_universe u1 in 
+   let u2 = refresh_uri_in_universe u2 in 
+    basic_eval_add_constraint (u1,u2) status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint 
 ;;
@@ -458,13 +483,13 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
   | GrafiteAst.Include (loc, mode, fname) ->
           let _root, baseuri, _fullpath, _rrelpath = 
        Librarian.baseuri_of_script ~include_paths fname in
+     let baseuri = NUri.uri_of_string baseuri in
+     (* MATITA 1.0: keep WithoutPreferences? *)
+     let alias_only = (mode = GrafiteAst.OnlyPreferences) in
      let status,obj =
-       GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
-        status in
+      GrafiteTypes.Serializer.require ~alias_only ~baseuri status in
      let status = status#set_dump (obj::status#dump) in
      let status = status#set_dependencies (fname::status#dependencies) in
-     (*assert false;*) (*  MATITA 1.0mode must be passed to GrafiteTypes.Serializer.require
-     somehow *)
        status
   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
   | GrafiteAst.NCoercion (loc, name, t, ty, source, target) ->

diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.ml b/matita/components/grafite_engine/nCicCoercDeclaration.ml
index 4522a0a1a917855a8aed045d35b1eaa52d753e94..e370975d798fabd79384c536d357d55381c1e501 100644 (file)
--- a/matita/components/grafite_engine/nCicCoercDeclaration.ml
+++ b/matita/components/grafite_engine/nCicCoercDeclaration.ml
@@ -289,9 +289,12 @@ let record_ncoercion =
    basic_index_ncoercion (name,t,s,d,p,a)
  in
  let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term
-  ~refresh_uri_in_reference
+  ~refresh_uri_in_reference ~alias_only status
  =
-   List.fold_right (aux ~refresh_uri_in_term) l
+  if not alias_only then
+   List.fold_right (aux ~refresh_uri_in_term) l status
+  else
+   status
  in
   GrafiteTypes.Serializer.register#run "ncoercion" aux_l 
 ;;

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 5873d29c7a1ddbfeb2ccc45599c2e376772cf132..dd4075a8a5f70fb5b87ccdc364dac0c7f58ad1a1 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -518,6 +518,8 @@ EXTEND
     include_command: [ [
         IDENT "include" ; path = QSTRING -> 
           loc,path,G.WithPreferences
+      | IDENT "include" ; IDENT "alias"; path = QSTRING -> 
+          loc,path,G.OnlyPreferences
       | IDENT "include'" ; path = QSTRING -> 
           loc,path,G.WithoutPreferences
      ]];

diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index ae6666be581fbae322e84226e43708be8cbc54b9..e40d3e05c10071bb9a416f473b4a4ef48c38694f 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -198,12 +198,14 @@ module type SerializerType =
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
     refresh_uri_in_term:(NCic.term -> NCic.term) ->
     refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
+    alias_only:bool ->
      dumpable_status -> dumpable_status
 
   val register: < run: 'a.  string -> 'a register_type -> ('a -> obj) >
   val serialize: baseuri:NUri.uri -> dependencies:string list -> obj list -> unit
    (* the obj is the "include" command to be added to the dump list *)
-  val require: baseuri:NUri.uri -> dumpable_status -> dumpable_status * obj
+  val require: baseuri:
+   NUri.uri -> alias_only:bool -> dumpable_status -> dumpable_status * obj
   val dependencies_of: baseuri:NUri.uri -> string list
  end
 
@@ -215,9 +217,10 @@ module Serializer(D: sig type dumpable_status end) =
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
     refresh_uri_in_term:(NCic.term -> NCic.term) ->
     refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
+    alias_only:bool ->
      dumpable_status -> dumpable_status
 
-  let require1 = ref (fun _ -> assert false) (* unknown data*)
+  let require1 = ref (fun ~alias_only:_ _ -> assert false) (* unknown data*)
   let already_registered = ref []
 
   let register =
@@ -228,22 +231,22 @@ module Serializer(D: sig type dumpable_status end) =
      already_registered := tag :: !already_registered;
      let old_require1 = !require1 in
      require1 :=
-      (fun ((tag',data) as x) ->
+      (fun ~alias_only ((tag',data) as x) ->
         if tag=tag' then
          require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
-          ~refresh_uri_in_reference
+          ~refresh_uri_in_reference ~alias_only
         else
-         old_require1 x);
+         old_require1 ~alias_only x);
      (fun x -> tag,Obj.repr x)
    end
 
   let serialize = serialize
 
-  let require2 ~baseuri status =
+  let require2 ~baseuri ~alias_only status =
    try
     includes := baseuri::!includes;
     let _dependencies,dump = require0 ~baseuri in
-     List.fold_right !require1 dump status
+     List.fold_right (!require1 ~alias_only) dump status
    with
     Sys_error _ ->
      raise (IncludedFileNotCompiled(ng_path_of_baseuri baseuri,NUri.string_of_uri baseuri))
@@ -251,15 +254,19 @@ module Serializer(D: sig type dumpable_status end) =
   let dependencies_of ~baseuri = fst (require0 ~baseuri)
 
   let record_include =
-   let aux baseuri ~refresh_uri_in_universe ~refresh_uri_in_term
-   ~refresh_uri_in_reference =
-     (* memorizzo baseuri in una tabella; *)
-     require2 ~baseuri
+   let aux baseuri ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_
+   ~refresh_uri_in_reference:_ ~alias_only =
+     let alias_only =
+      alias_only || List.mem baseuri (get_already_included ())
+     in
+      require2 ~baseuri ~alias_only
    in
     register#run "include" aux
 
-  let require ~baseuri status =
-   let status = require2 ~baseuri status in
+  let require ~baseuri ~alias_only status =
+   let alias_only =
+    alias_only || List.mem baseuri (get_already_included ()) in
+   let status = require2 ~baseuri ~alias_only status in
     status,record_include baseuri
 end
 

diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli
index 4e080e8c2920c54136b15c0dd744be4a4aa42e5d..aff1473c18bdea540949853c36d2d70cf6670b83 100644 (file)
--- a/matita/components/ng_library/nCicLibrary.mli
+++ b/matita/components/ng_library/nCicLibrary.mli
@@ -49,13 +49,15 @@ module type SerializerType =
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
     refresh_uri_in_term:(NCic.term -> NCic.term) ->
     refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
+    alias_only:bool ->
      dumpable_status -> dumpable_status
 
   val register: < run: 'a.  string -> 'a register_type -> ('a -> obj) >
   val serialize: baseuri:NUri.uri -> dependencies:string list -> obj list ->
        unit
    (* the obj is the "include" command to be added to the dump list *)
-  val require: baseuri:NUri.uri -> dumpable_status -> dumpable_status * obj
+  val require: baseuri:
+   NUri.uri -> alias_only:bool -> dumpable_status -> dumpable_status * obj
   val dependencies_of: baseuri:NUri.uri -> string list
  end