- changed moo representation in MatitaTypes.status, no longer a string list, but...

- fixed redundancy in moo: aliases, interpretation, and default commands are always present only once in a single moo
- added MatitaTypes.add_moo_content: from now on it must be then only function used to add content to moo objects

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 19944417f048e440b7c5ac0ace0967fcef6cad7b..89481b287434a12284dedd67c24e76c08acee8e5 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -24,6 +24,7 @@
  *)
 
 open Printf
+
 open MatitaTypes
 
 exception Drop;;
@@ -353,7 +354,7 @@ module MatitaStatus =
   let set_goals (status,_) goals = status,goals
 
   let id_tac status =
-    apply_tactic (GrafiteAst.IdTac Disambiguate.dummy_floc) status
+    apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc) status
 
   let mk_tactic tac = tac
 
@@ -451,21 +452,18 @@ let eval_coercion status coercion =
    List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
     status new_coercions in
   let statement_of name =
-    GrafiteAstPp.pp_statement 
-      (GrafiteAst.Executable (Disambiguate.dummy_floc,
-        (GrafiteAst.Command (Disambiguate.dummy_floc,
-          (GrafiteAst.Coercion (Disambiguate.dummy_floc, 
-            (CicNotationPt.Ident (name, None)))))))) ^ "\n"
+    GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, 
+      (CicNotationPt.Ident (name, None)))
   in
-  let moo_content_rev =
-    [statement_of (UriManager.name_of_uri coer_uri)] @ 
+  let moo_content = 
+    statement_of (UriManager.name_of_uri coer_uri) ::
     (List.map 
       (fun (uri, _, _) -> 
         statement_of (UriManager.name_of_uri uri))
-    new_coercions) @ status.moo_content_rev 
+    new_coercions)
   in
-  let status =  {status with moo_content_rev = moo_content_rev} in
-  {status with proof_status = No_proof}
+  let status = add_moo_content moo_content status in
+  { status with proof_status = No_proof }
 
 let generate_elimination_principles uri status =
  let elim sort status =
@@ -571,8 +569,7 @@ let eval_command opts status cmd =
   match cmd with
   | GrafiteAst.Default (loc, what, uris) as cmd ->
      LibraryObjects.set_default what uris;
-     {status with moo_content_rev =
-        (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
+     add_moo_content [cmd] status
   | GrafiteAst.Include (loc, path) ->
      let absolute_path = make_absolute opts.include_paths path in
      let moopath = MatitaMisc.obj_file_of_script absolute_path in
@@ -649,11 +646,7 @@ let eval_command opts status cmd =
   | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
   | GrafiteAst.Dump _ -> assert false   (* ZACK: to be removed *)
   | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
-      let status' =
-        { status with
-            moo_content_rev =
-              (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev }
-      in
+      let status' = add_moo_content [stm] status in
       let aliases' =
         DisambiguateTypes.Environment.cons
           (DisambiguateTypes.Symbol (symbol, 0))
@@ -661,9 +654,7 @@ let eval_command opts status cmd =
           status.aliases
       in
       MatitaSync.set_proof_aliases status' aliases'
-  | GrafiteAst.Notation _ as stm ->
-      { status with moo_content_rev =
-        (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev }
+  | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status
   | GrafiteAst.Obj (loc,obj) ->
      let ext,name =
       match obj with

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index a77c2476101f5546acf3cb2445bb6e54f6921f04..55cb4a45c09d45c887e07c26602934283bc61679 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -53,13 +53,10 @@ let alias_diff ~from status =
 let set_proof_aliases status aliases =
  let new_status = { status with aliases = aliases } in
  let diff = alias_diff ~from:status new_status in
- let textual_diff =
-  if DisambiguateTypes.Environment.is_empty diff then
-   ""
-  else
-   DisambiguatePp.pp_environment diff ^ "\n" in
- let moo_content_rev = textual_diff :: status.moo_content_rev in
- {new_status with moo_content_rev = moo_content_rev}
+ if DisambiguateTypes.Environment.is_empty diff then
+   new_status
+ else
+   add_moo_content (DisambiguatePp.commands_of_environment diff) new_status
   
 (** given a uri and a type list (the contructors types) builds a list of pairs
  *  (name,uri) that is used to generate authomatic aliases **)

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 3bc1056283d05740630b2d042a859f4d08e2177a..4ac480cf1761b5fed5fbcbcac80d313f995185d0 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -57,12 +57,14 @@ type option_value =
 type options = option_value StringMap.t
 let no_options = StringMap.empty
 
+type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+
 type status = {
-  aliases : DisambiguateTypes.environment;
-  moo_content_rev : string list;
-  proof_status : proof_status;
-  options : options;
-  objects : (UriManager.uri * string) list;
+  aliases: DisambiguateTypes.environment;
+  moo_content_rev: ast_command list;
+  proof_status: proof_status;
+  options: options;
+  objects: (UriManager.uri * string) list;
   notation_ids: CicNotation.notation_id list;
 }
 
@@ -77,6 +79,26 @@ let set_metasenv metasenv status =
   in
   { status with proof_status = proof_status }
 
+let add_moo_content cmds status =
+  let content = status.moo_content_rev in
+  let content' =
+    List.fold_right
+      (fun cmd acc ->
+(*         prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
+        match cmd with
+        | GrafiteAst.Interpretation _
+        | GrafiteAst.Default _ ->
+            if List.mem cmd content then acc
+            else cmd :: acc
+        | GrafiteAst.Alias _ -> (* move Alias as the last inserted one *)
+            cmd :: (List.filter ((<>) cmd) acc)
+        | _ -> cmd :: acc)
+      cmds content
+  in
+(*   prerr_endline ("new moo content: " ^ String.concat " " (List.map
+    GrafiteAstPp.pp_command content')); *)
+  { status with moo_content_rev = content' }
+
 let dump_status status = 
   MatitaLog.message "status.aliases:\n";
   MatitaLog.message

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 053f05be6b2b6a70a9e98ff4461030135c2d2087..c0946c89f8a0c8990d073ff489a3afa8b1be7c32 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -47,9 +47,11 @@ type option_value =
 type options = option_value StringMap.t
 val no_options : 'a StringMap.t
 
+type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+
 type status = {
   aliases: DisambiguateTypes.environment;   (** disambiguation aliases *)
-  moo_content_rev: string list;(*CSC: GrafiteAst.command list would be better *)
+  moo_content_rev: ast_command list;
   proof_status: proof_status;
   options: options;
   objects: (UriManager.uri * string) list;  (** in-scope objects, with paths *)
@@ -58,6 +60,9 @@ type status = {
 
 val set_metasenv: Cic.metasenv -> status -> status
 
+  (** list is not reversed, head command will be the first emitted *)
+val add_moo_content: ast_command list -> status -> status
+
 val dump_status : status -> unit
 val get_option : status -> StringMap.key -> option_value
 val get_string_option : status -> StringMap.key -> string

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index e7d3f18e6c7f9599cc02455454d13fcad72772a2..9cc063271d801902cd5375661e5a850458fe9424 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -149,7 +149,9 @@ let dump_moo_to_file file moo =
  let os = open_out (MatitaMisc.obj_file_of_script file) in
  let output s = output_string os s in
  output "(* GENERATED FILE: DO NOT EDIT! *)\n\n";
- List.iter output (List.rev moo);
+ List.iter
+  (fun cmd -> output (GrafiteAstPp.pp_command cmd ^ "\n"))
+  (List.rev moo);
  close_out os
   
 let main ~mode = 

diff --git a/helm/matita/matitacLib.mli b/helm/matita/matitacLib.mli
index b19ff5b90c4ef0ef72ef09bc3d494452565960d3..7c07402d875f144ef99c9adfd182c2015f336353 100644 (file)
--- a/helm/matita/matitacLib.mli
+++ b/helm/matita/matitacLib.mli
@@ -30,7 +30,10 @@ val go : unit -> unit
 val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit
 
 (** fname is the .ma *)
-val dump_moo_to_file: string -> string list -> unit
+val dump_moo_to_file:
+  string ->
+  (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command list ->
+    unit
 
 (** clean_exit n
   if n = Some n it performs an exit [n] after a complete clean-up of what was