From f2551cc0cc563b34b88a70a6bb0ef5e352a5d542 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 13 Sep 2005 13:27:53 +0000 Subject: [PATCH] - changed moo representation in MatitaTypes.status, no longer a string list, but a command (in AST format) list - 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 --- helm/matita/matitaEngine.ml | 33 ++++++++++++--------------------- helm/matita/matitaSync.ml | 11 ++++------- helm/matita/matitaTypes.ml | 32 +++++++++++++++++++++++++++----- helm/matita/matitaTypes.mli | 7 ++++++- helm/matita/matitacLib.ml | 4 +++- helm/matita/matitacLib.mli | 5 ++++- 6 files changed, 56 insertions(+), 36 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 19944417f..89481b287 100644 --- 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 a77c24761..55cb4a45c 100644 --- 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 3bc105628..4ac480cf1 100644 --- 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 053f05be6..c0946c89f 100644 --- 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 e7d3f18e6..9cc063271 100644 --- 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 b19ff5b90..7c07402d8 100644 --- 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 -- 2.39.2