1.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Wed Dec 16 16:25:55 2020 +0100
1.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Thu Dec 17 09:10:30 2020 +0100
1.3 @@ -7,6 +7,7 @@
1.4 imports "HOL-SPARK.SPARK"
1.5 begin
1.6
1.7 +section \<open>spark intro\<close>
1.8 spark_proof_functions
1.9 gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
1.10
1.11 @@ -16,6 +17,7 @@
1.12 ./greatest_common_divisor/g_c_d.siv, *.fdl, *.rls open *.siv and
1.13 find the following 2 open verification conditions (VC): *)
1.14
1.15 +section \<open>example 1\<close>
1.16 spark_vc procedure_g_c_d_4 (*..select 1st VC for proof: *)
1.17 proof -
1.18 from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
1.19 @@ -25,7 +27,55 @@
1.20 from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2
1.21 by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
1.22 qed
1.23 +text \<open>
1.24 + general notes:
1.25 +# Clicks on different positions give different traces.
1.26 +# There are blocks with equal traces (separated by \n or |)
1.27 + proof
1.28 + from \<open>0 < d\<close> | have "0 \<le> c mod d" | by (rule pos_mod_sign)
1.29 + with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> | show ?C1
1.30 + by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
1.31 + next [ONLY ### Private_Output.report keyword1]
1.32 + from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> | show ?C2
1.33 + by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
1.34 + qed [NO TRACE]
1.35 +# Specific traces seem to be extended by the subsequent one,
1.36 + e.g. from \<open>0 < d\<close> extended by have "0 \<le> c mod d"
1.37 + but both NOT by ... by (rule pos_mod_sign)
1.38 +# Private_Output.report seems to have "" as argument frequently
1.39 +# Output.report provided semantic annotations in Naproche;
1.40 + thus ALL calls of Output.report (in src/pure) are traced:
1.41 + proof x x . . .
1.42 + from \<open>0 < d\<close> x . x x x
1.43 + have "0 \<le> c mod d" x . x x .
1.44 + by (rule pos_mod_sign) x x . . .
1.45 + with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> x . x x x
1.46 + show ?C1 x . x x .
1.47 + by (simp add: ...[symmetric]) x x . . .
1.48 + next x . . . .
1.49 + from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> x . x x x
1.50 + show ?C2 x . x x .
1.51 + by (simp add: ...[symmetric] gcd_non_0_int) x x . . .
1.52 + | | | | Context_Position.report_generic
1.53 + | | | Syntax_Phases.check_terms
1.54 + | | Syntax_Phases.check_typs
1.55 + | Token.syntax_generic
1.56 + Private_Output.report
1.57 +\<close>
1.58
1.59 +subsection \<open>tracing calls of \<close>
1.60 +text \<open>
1.61 +(*--------- click on "proof -" --------
1.62 +### Private_Output.report keyword1
1.63 +### Private_Output.report language
1.64 +### Private_Output.report entityo
1.65 +### Private_Output.report operator
1.66 +### Token.syntax_generic, Scan.error
1.67 +### Private_Output.report
1.68 +### Token.syntax_generic, Scan.error
1.69 +\<close>
1.70 +
1.71 +section \<open>example 2\<close>
1.72 spark_vc procedure_g_c_d_11 (*..select 2nd VC for proof: *)
1.73 proof -
1.74 from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d = 0\<close>
2.1 --- a/src/Pure/General/output.ML Wed Dec 16 16:25:55 2020 +0100
2.2 +++ b/src/Pure/General/output.ML Thu Dec 17 09:10:30 2020 +0100
2.3 @@ -62,7 +62,7 @@
2.4 val init_channels: unit -> unit
2.5 end;
2.6
2.7 -structure Private_Output: PRIVATE_OUTPUT =
2.8 +structure Private_Output(**): PRIVATE_OUTPUT(**) =
2.9 struct
2.10
2.11 (** print modes **)
2.12 @@ -154,9 +154,13 @@
2.13 fun error_message s = error_message' (serial (), s);
2.14 fun system_message s = ! system_message_fn [output s];
2.15 fun status ss = ! status_fn (map output ss);
2.16 +(* report: string list -> unit
2.17 + report_fn: (output list -> unit) ref*)
2.18 fun report ss = ! report_fn (map output ss);
2.19 fun report ss =
2.20 -((** )@{print} {};( *..not yet available*)
2.21 +((** )@{print} {a = "### Private_Output.report"};( *..not yet available*)
2.22 + (**)writeln ("### Private_Output.report " (**)^ (ss |> cat_lines |> cut_string 10)(**));
2.23 + (* HOL build fails with greater length ----------------------------------------^^ *)
2.24 ! report_fn (map output ss)
2.25 );
2.26 fun result props ss = ! result_fn props (map output ss);
3.1 --- a/src/Pure/General/position.ML Wed Dec 16 16:25:55 2020 +0100
3.2 +++ b/src/Pure/General/position.ML Thu Dec 17 09:10:30 2020 +0100
3.3 @@ -222,6 +222,7 @@
3.4 fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
3.5 fun report_text pos markup txt =
3.6 ((** )@{print} {a = "### Position.report_text"};( *..NOT yet available*)
3.7 + writeln "### Position.report_text";
3.8 Output.report [reported_text pos markup txt]);
3.9 fun report pos markup = report_text pos markup "";
3.10
4.1 --- a/src/Pure/Isar/outer_syntax.ML Wed Dec 16 16:25:55 2020 +0100
4.2 +++ b/src/Pure/Isar/outer_syntax.ML Thu Dec 17 09:10:30 2020 +0100
4.3 @@ -149,6 +149,7 @@
4.4
4.5 fun command (name, pos) comment parse =
4.6 ((** )@{print} {x = "### Outer_Syntax.command"};( *..NOT yet available*)
4.7 + (**)writeln "### Outer_Syntax.command";(**)
4.8 raw_command (name, pos) comment (Parser parse)
4.9 );
4.10
5.1 --- a/src/Pure/Isar/proof.ML Wed Dec 16 16:25:55 2020 +0100
5.2 +++ b/src/Pure/Isar/proof.ML Thu Dec 17 09:10:30 2020 +0100
5.3 @@ -395,7 +395,8 @@
5.4 else [];
5.5
5.6 val position_markup = Position.markup (Position.thread_data ()) Markup.position;
5.7 -(** )val _ = @{print} {a = "### Proof.pretty_state:"}( *..NOT yet available*)
5.8 +(** )val _ = @{print} {a = "### Proof.pretty_state:"};( *..NOT yet available*)
5.9 +(**)val _ = writeln "### Proof.pretty_state:";(*..NOT yet available*)
5.10 in
5.11 [Pretty.block
5.12 [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @
6.1 --- a/src/Pure/Isar/proof_context.ML Wed Dec 16 16:25:55 2020 +0100
6.2 +++ b/src/Pure/Isar/proof_context.ML Thu Dec 17 09:10:30 2020 +0100
6.3 @@ -801,6 +801,7 @@
6.4 if Context_Position.is_visible ctxt
6.5 then
6.6 ((** )@{print} {a = "### Proof_Context.check_tfree"};( *..NOT yet available 2 *)
6.7 + writeln "### Proof_Context.check_tfree";
6.8 Output.report sorting_report)
6.9 else ();
6.10 in a end;
7.1 --- a/src/Pure/Isar/token.ML Wed Dec 16 16:25:55 2020 +0100
7.2 +++ b/src/Pure/Isar/token.ML Thu Dec 17 09:10:30 2020 +0100
7.3 @@ -771,7 +771,8 @@
7.4 (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of
7.5 (SOME x, (context', [])) =>
7.6 let
7.7 - (** )val _ = @{print} {a = "### Token.syntax_generic, Scan.error"}( *..NOT yet available 2 *)
7.8 + (** )val _ = @{print} {a = "### Token.syntax_generic, Scan.error"};( *..NOT yet available 2 *)
7.9 + (**)val _ = writeln "### Token.syntax_generic, Scan.error";(**)
7.10 val _ = Output.report (reported_text ())
7.11 in (x, context') end
7.12 | (_, (context', args2)) =>
8.1 --- a/src/Pure/ML/ml_compiler.ML Wed Dec 16 16:25:55 2020 +0100
8.2 +++ b/src/Pure/ML/ml_compiler.ML Thu Dec 17 09:10:30 2020 +0100
8.3 @@ -120,6 +120,7 @@
8.4 |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
8.5 |>
8.6 ((** )@{print} {a = "### ML_Compiler.output"};( *..NOT yet available 2 *)
8.7 + (**)writeln "### ML_Compiler.output";(**)
8.8 Output.report);
8.9 val _ =
8.10 if not (null persistent_reports) andalso redirect andalso Future.enabled ()
9.1 --- a/src/Pure/PIDE/execution.ML Wed Dec 16 16:25:55 2020 +0100
9.2 +++ b/src/Pure/PIDE/execution.ML Thu Dec 17 09:10:30 2020 +0100
9.3 @@ -175,6 +175,7 @@
9.4 (status task [Markup.failed];
9.5 status task [Markup.finished];
9.6 ((** )@{print} {a = "### Execution.fork/future"};( *..NOT yet available 2 *)
9.7 + (**) writeln "### Execution.fork/future";(**)
9.8 Output.report [Markup.markup_only (Markup.bad ())]);
9.9 if exec_id = 0 then ()
9.10 else List.app (Future.error_message pos) (Runtime.exn_messages exn))
10.1 --- a/src/Pure/PIDE/resources.ML Wed Dec 16 16:25:55 2020 +0100
10.2 +++ b/src/Pure/PIDE/resources.ML Thu Dec 17 09:10:30 2020 +0100
10.3 @@ -239,6 +239,7 @@
10.4 let
10.5 val fs = files thy;
10.6 (** )val _ = @{print} {a = "### Resources.provide_parse_files", fs = fs}( **)
10.7 + (**)val _ = writeln "### Resources.provide_parse_files";(**)
10.8 val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy;
10.9 in (fs, thy') end);
10.10
11.1 --- a/src/Pure/Pure.thy Wed Dec 16 16:25:55 2020 +0100
11.2 +++ b/src/Pure/Pure.thy Thu Dec 17 09:10:30 2020 +0100
11.3 @@ -1061,7 +1061,8 @@
11.4 Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
11.5 fun report_back () =
11.6 ((**)@{print} {a = "### Pure.thy/report_back: Output.report"};(**)
11.7 - Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"]);
11.8 + (**) writeln "### Pure.thy/report_back: Output.report";(**)
11.9 + Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"]);
11.10
11.11 val _ =
11.12 Outer_Syntax.command \<^command_keyword>\<open>back\<close> "explicit backtracking of proof command"
12.1 --- a/src/Pure/Syntax/syntax_phases.ML Wed Dec 16 16:25:55 2020 +0100
12.2 +++ b/src/Pure/Syntax/syntax_phases.ML Thu Dec 17 09:10:30 2020 +0100
12.3 @@ -963,6 +963,7 @@
12.4 if Context_Position.is_visible ctxt
12.5 then
12.6 ((** )@{print} {a = "### Syntax_Phases.check_typs"};( *..NOT yet available 2 *)
12.7 + (**) writeln "### Syntax_Phases.check_typs";(**)
12.8 Output.report sorting_report)
12.9 else ();
12.10 in
12.11 @@ -991,6 +992,7 @@
12.12 if Context_Position.is_visible ctxt
12.13 then
12.14 ((** )@{print} {a = "### Syntax_Phases.check_terms"};( *..NOT yet available 2 *)
12.15 + (**) writeln "### Syntax_Phases.check_terms";(**)
12.16 Output.report (sorting_report @ typing_report))
12.17 else ();
12.18 in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
13.1 --- a/src/Pure/Thy/document_source.ML Wed Dec 16 16:25:55 2020 +0100
13.2 +++ b/src/Pure/Thy/document_source.ML Thu Dec 17 09:10:30 2020 +0100
13.3 @@ -96,6 +96,7 @@
13.4 (Parse.group (fn () => "document tag scope")
13.5 (Parse.$$$ "(" |-- Parse.!!! (scope --| Parse.$$$ ")"))) toks
13.6 (** )val _ = @{print} {a = "### Document_Source.tag_scope"}( *..NOT yet available*)
13.7 +(**)val _ = writeln "### Document_Source.tag_scope";(**)
13.8 in xxx end;
13.9
13.10 val tag_name =
13.11 @@ -108,7 +109,7 @@
13.12
13.13 val old_tags = Scan.repeat old_tag;
13.14
13.15 -
13.16 +
13.17 (* semantic markers (operation on presentation context) *)
13.18
13.19 val marker = improper |-- Parse.document_marker --| blank_end;
14.1 --- a/src/Pure/context_position.ML Wed Dec 16 16:25:55 2020 +0100
14.2 +++ b/src/Pure/context_position.ML Thu Dec 17 09:10:30 2020 +0100
14.3 @@ -60,6 +60,7 @@
14.4 fun report_generic context pos markup =
14.5 if is_reported_generic context pos then
14.6 ((** )@{print} {a = "### Context_Position.report_generic"};( *..NOT yet available*)
14.7 + (**) writeln "### Context_Position.report_generic";(**)
14.8 Output.report [Position.reported_text pos markup ""])
14.9 else ();
14.10
15.1 --- a/src/Pure/library.ML Wed Dec 16 16:25:55 2020 +0100
15.2 +++ b/src/Pure/library.ML Thu Dec 17 09:10:30 2020 +0100
15.3 @@ -158,6 +158,7 @@
15.4 val decode_lines: string -> string
15.5 val align_right: string -> int -> string -> string
15.6 val match_string: string -> string -> bool
15.7 + val cut_string: int -> string -> string
15.8
15.9 (*reals*)
15.10 val string_of_real: real -> string
15.11 @@ -389,6 +390,10 @@
15.12 ([], _) => []
15.13 | (g, rest) => g :: chop_groups n rest);
15.14
15.15 +fun cut_string n str = str
15.16 + |> Symbol.explode
15.17 + |> take n
15.18 + |> implode
15.19
15.20 (*return nth element of a list, where 0 designates the first element;
15.21 raise Subscript if list too short*)
16.1 --- a/src/Pure/skip_proof.ML Wed Dec 16 16:25:55 2020 +0100
16.2 +++ b/src/Pure/skip_proof.ML Thu Dec 17 09:10:30 2020 +0100
16.3 @@ -24,6 +24,7 @@
16.4 fun report ctxt =
16.5 if Context_Position.is_visible ctxt then
16.6 ((** )@{print} {a = "### Skip_Proof.report"};( *..NOT yet available 2 *)
16.7 + (**) writeln "### Skip_Proof.report";(**)
16.8 Output.report [Markup.markup (Markup.bad ()) "Skipped proof"])
16.9 else ();
16.10
17.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Dec 16 16:25:55 2020 +0100
17.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Thu Dec 17 09:10:30 2020 +0100
17.3 @@ -781,13 +781,22 @@
17.4
17.5 Investigation of Naproche showed, that annotations are ONLY sent bY
17.6 Output.report: string list -> unit, where string holds markup.
17.7 - For Output.report @ {print} is NOT available, so we guard all respective calls.
17.8 - However, NO @ {print} available in src/Pure is reached by "spark_vc procedure_g_c_d_4"
17.9 - [[note: writeln is available earlier then print, e.g. in Pure/Isar/parse.ML]]
17.10 + For Output.report @ {print} is NOT available, so we trace all respective CALLS.
17.11 + However, NO @ {print} available in src/Pure is reached by "spark_vc procedure_g_c_d_4",
17.12 + so tracing is done by writeln (which breaks build between Main and Complex_Main
17.13 + by writing longer strings, see Pure/General/output.ML).
17.14 +
17.15 + Tracing is implemented in (1) Isabelle_Naproche and in (2) isabisac in parallel;
17.16 + (1) requires only Pure, thus is built quicker, but does NOT handle proofs within ML
17.17 + (2) requires HOL.SPARK, there is full proof handling, but this is complex.
17.18 +
17.19 + Tracing the calls of Output.report shows some properties of handling proofs,
17.20 + see text in SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.
17.21 \<close>
17.22
17.23 subsection \<open>notes and testbed for Naproche in preliminary spark_vcs\<close>
17.24 -ML \<open>
17.25 +text \<open>
17.26 + tracing "spark_vc procedure_g_c_d_4" see SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
17.27 \<close> ML \<open>
17.28 \<close> ML \<open>
17.29 \<close> ML \<open>