1.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Thu Dec 17 11:45:12 2020 +0100
     1.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Thu Dec 17 18:00:27 2020 +0100
     1.3 @@ -27,8 +27,10 @@
     1.4    from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C2
     1.5      by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
     1.6  qed
     1.7 +
     1.8 +subsection \<open>observing interaction on the proof\<close>
     1.9  text \<open>
    1.10 -  general notes:
    1.11 +  :
    1.12  # Clicks on different positions give different traces.
    1.13  # There are blocks with equal traces (separated by \n or |)
    1.14      proof
    1.15 @@ -44,7 +46,7 @@
    1.16    but both NOT by ...                                      by (rule pos_mod_sign)
    1.17  # Private_Output.report seems to have "" as argument frequently
    1.18  # Output.report provided semantic annotations in Naproche;
    1.19 -  thus ALL calls of Output.report (in src/pure) are traced:
    1.20 +  thus ALL calls of Output.report (in src/Pure) are traced an show up at these elements:
    1.21      proof                                        x  x  .  .  .  
    1.22      from \<open>0 < d\<close>                                 x  .  x  x  x  
    1.23      have "0 \<le> c mod d"                           x  .  x  x  .  
    1.24 @@ -63,7 +65,7 @@
    1.25                                                   Private_Output.report
    1.26  \<close>
    1.27  
    1.28 -subsection \<open>tracing calls of \<close>
    1.29 +subsection \<open>tracing calls of Output.report\<close>
    1.30  text \<open>
    1.31  (*--------- click on "proof -" --------
    1.32  ### Private_Output.report keyword1
    1.33 @@ -74,8 +76,132 @@
    1.34  ### Private_Output.report 
    1.35  ### Token.syntax_generic, Scan.error
    1.36  \<close>
    1.37 +text \<open>
    1.38 +(*--------- click on "from \<open>0 < d\<close>" --------
    1.39 +### Private_Output.report keyword1
    1.40 +### Private_Output.report cartouch
    1.41 +### Private_Output.report delimite
    1.42 +### Private_Output.report entityo
    1.43 +### Syntax_Phases.check_typs
    1.44 +### Private_Output.report 
    1.45 +### Syntax_Phases.check_typs
    1.46 +### Private_Output.report 
    1.47 +### Syntax_Phases.check_terms
    1.48 +### Private_Output.report typingo          =====
    1.49 +### Context_Position.report_generic           //--- different to subsequent part below
    1.50 +### Private_Output.report entityo
    1.51 +\<close>
    1.52 +text \<open>
    1.53 +(*--------- click on "have "0 \<le> c mod d"" --------
    1.54 +### Private_Output.report keyword1
    1.55 +### Private_Output.report 
    1.56 +### Private_Output.report cartouch
    1.57 +### Private_Output.report delimite
    1.58 +### Private_Output.report entityo
    1.59 +### Syntax_Phases.check_typs
    1.60 +### Private_Output.report 
    1.61 +### Syntax_Phases.check_typs
    1.62 +### Private_Output.report 
    1.63 +### Syntax_Phases.check_terms
    1.64 +### Private_Output.report typingo          =====
    1.65 +### Syntax_Phases.check_typs                  //--- different to previous part above
    1.66 +### Private_Output.report 
    1.67 +### Syntax_Phases.check_terms
    1.68 +### Private_Output.report 
    1.69 +\<close>
    1.70 +
    1.71 +subsection \<open>signatures of the traced callers of Private_Output.report\<close>
    1.72 +ML \<open>
    1.73 +\<close> ML \<open>
    1.74 +Private_Output.report          : string(*= markup*) list                   -> unit; 
    1.75 +Context_Position.report_generic: Context.generic -> Position.T -> Markup.T -> unit;
    1.76 +Token.syntax_generic           : 'a Token.context_parser -> Token.src -> Context.generic ->
    1.77 +                                   'a * Context.generic;
    1.78 +(*Syntax_Phases.check_typs     : Proof.context -> typ list -> typ list;    ..local*)
    1.79 +(*Syntax_Phases.check_terms    : Proof.context -> term list -> term list;  ..local*)
    1.80 +\<close> ML \<open>
    1.81 +\<close>
    1.82 +
    1.83 +subsection \<open>lookup calls of Syntax_Phases.check_terms\<close>
    1.84 +text \<open>
    1.85 +  focus are    "from \<open>0 < d\<close>"   and   have "0 \<le> c mod d".
    1.86 +
    1.87 +  encapsulation?:
    1.88 +    Syntax_Phases.check_terms NOwhere in src/Pure,
    1.89 +    check_terms occurs in Theory.setup (Syntax.install_operations {..check_terms = check_terms..}
    1.90 +    and nowhere else (except fun check_props)
    1.91 +  so the calls are Syntax.check_terms ? -- NO: calls.1..4 --vv pop up in NONE of the 3 traces above.
    1.92 +                                           ^^^^^^^^^^^^^^^     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    1.93 +  but they seem to be identical:
    1.94 +    Syntax_Phases.check_terms: Proof.context -> term list -> term list;
    1.95 +           Syntax.check_terms: Proof.context -> term list -> term list;
    1.96 +    ?! there are 3-times structure Syntax:
    1.97 +      Pure/Syntax/lexicon.ML                      /NO check_terms/
    1.98 +        signature LEXICON = sig structure Syntax: sig val const: string -> term ..
    1.99 +      Pure/Syntax/syntax.ML 
   1.100 +        type operations = {..., ..., check_terms: Proof.context -> term list -> term list, ..
   1.101 +        val check_terms = operation #check_terms;
   1.102 +      Pure/Syntax/syntax_trans.ML                 /NO check_terms/
   1.103 +        
   1.104 +  the ASSUMED callers of Syntax.check_terms:
   1.105 +//  Pure/Isar/expression.ML
   1.106 +//    1,val inst_morphism: (string * typ) list -> (string * bool) * term list -> Proof.context ->
   1.107 +//        morphism * Proof.context
   1.108 +//    2.val check_autofix:
   1.109 +//        ('a * ('b * term list)) list ->
   1.110 +//          ('c * term) list list ->
   1.111 +//            (typ, term, 'd) ctxt list ->
   1.112 +//              ('e * (term * term list) list) list -> Proof.context ->
   1.113 +//        (('a * ('b * term list)) list * ('c * term) list list * (typ, term, 'd) ctxt list *
   1.114 +//          ('e * (term * term list) list) list) * Proof.context
   1.115 +//        val check: (term * term list) list -> Proof.context ->
   1.116 +//          (term * term list) list * Proof.context
   1.117 +//  Pure/Isar/obtain.ML
   1.118 +//    3.val Obtain.read_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list 
   1.119 +//  Pure/Isar/proof.ML
   1.120 +//    4.val let_bind: (term list * term) list -> state -> state
   1.121 +//    5.val let_bind_cmd: (string list * string) list -> state -> state
   1.122 +//        val read_terms: context -> typ -> string list -> term list
   1.123 +//  Pure/Isar/proof_context.ML
   1.124 +//    6.val infer_type: Proof.context -> string * typ -> typ
   1.125 +//  Pure/simplifier.ML
   1.126 +//    7.val Simplifier.define_simproc: binding -> term Simplifier.simproc_spec ->
   1.127 +//        local_theory -> local_theory
   1.128 +//  Pure/Tools/rule_insts.ML
   1.129 +//    8.val Rule_Insts.read_term: string -> Proof.context -> term * Proof.context
   1.130 +//    :
   1.131 +//    1.. looked up in the sequel
   1.132 +\<close>
   1.133 +subsection \<open>lookup Syntax.check_terms -> *1..4\<close>
   1.134 +text \<open>\<close>
   1.135 +
   1.136 +subsubsection \<open>lookup 1* -> Expression.inst_morphism\<close>
   1.137 +text \<open>\<close>
   1.138 +
   1.139 +subsubsection \<open>lookup 2* -> Expression.check_autofix\<close>
   1.140 +text \<open>
   1.141 +\<close> 
   1.142 +subsubsection \<open>lookup 3* -> Obtain.read_obtains\<close>
   1.143 +text \<open>\<close>
   1.144 +
   1.145 +subsubsection \<open>lookup 4* -> Proof.let_bind\<close>
   1.146 +text \<open>\<close>
   1.147 +
   1.148 +subsubsection \<open>lookup 5* -> Proof.let_bind_cmd\<close>
   1.149 +text \<open>\<close>
   1.150 +
   1.151 +subsubsection \<open>lookup 6* -> Proof_Context.infer_type\<close>
   1.152 +text \<open>\<close>
   1.153 +
   1.154 +subsubsection \<open>lookup 7* -> Simplifier.define_simproc\<close>
   1.155 +text \<open>\<close>
   1.156 +
   1.157 +subsubsection \<open>lookup 8* -> Rule_Insts.read_term\<close>
   1.158 +text \<open>\<close>
   1.159 +
   1.160  
   1.161  section \<open>example 2\<close>
   1.162 +
   1.163  spark_vc procedure_g_c_d_11 (*..select 2nd VC for proof: *)
   1.164  proof -
   1.165    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	Thu Dec 17 11:45:12 2020 +0100
     2.2 +++ b/src/Pure/General/output.ML	Thu Dec 17 18:00:27 2020 +0100
     2.3 @@ -159,7 +159,7 @@
     2.4  fun report ss = ! report_fn (map output ss);
     2.5  fun report ss =
     2.6  ((** )@{print} {a = "### Private_Output.report"};( *..not yet available*)
     2.7 - (**)writeln ("### Private_Output.report " (**)^ (ss |> cat_lines |> cut_string 10)(**));
     2.8 + (** )writeln ("### Private_Output.report " (**)^ (ss |> cat_lines |> cut_string 10));( **)
     2.9   (* HOL build fails with greater length ----------------------------------------^^ *)
    2.10    ! report_fn (map output ss)
    2.11  );

     3.1 --- a/src/Pure/Isar/expression.ML	Thu Dec 17 11:45:12 2020 +0100
     3.2 +++ b/src/Pure/Isar/expression.ML	Thu Dec 17 18:00:27 2020 +0100
     3.3 @@ -44,7 +44,7 @@
     3.4      (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context
     3.5  end;
     3.6  
     3.7 -structure Expression : EXPRESSION =
     3.8 +structure Expression (**): EXPRESSION(**) =
     3.9  struct
    3.10  
    3.11  datatype ctxt = datatype Element.ctxt;
    3.12 @@ -166,10 +166,13 @@
    3.13  
    3.14  (* Instantiation morphism *)
    3.15  
    3.16 +(*val inst_morphism: (string * typ) list -> (string * bool) * term list -> Proof.context ->
    3.17 +        morphism * Proof.context*)
    3.18  fun inst_morphism params ((prfx, mandatory), insts') ctxt =
    3.19    let
    3.20 +    val _ = writeln "#### Expression.inst_morphism";
    3.21      (* parameters *)
    3.22 -    val parm_types = map #2 params;
    3.23 +    val parm_types = map #2 (params: (string * typ) list);
    3.24      val type_parms = fold Term.add_tfreesT parm_types [];
    3.25  
    3.26      (* type inference *)
    3.27 @@ -226,7 +229,7 @@
    3.28  
    3.29  (** Simultaneous type inference: instantiations + elements + statement **)
    3.30  
    3.31 -local
    3.32 +(**)local(**)
    3.33  
    3.34  fun mk_type T = (Logic.mk_type T, []);
    3.35  fun mk_term t = (t, []);
    3.36 @@ -269,6 +272,11 @@
    3.37        (ctxt', ts))
    3.38    end;
    3.39  
    3.40 +(*WN*)
    3.41 +
    3.42 +(*WN*)
    3.43 +(* val check: (term * term list) list -> Proof.context ->
    3.44 +      (term * term list) list * Proof.context *)
    3.45  fun check cs ctxt =
    3.46    let
    3.47      val (cs', (ctxt', _)) = fold_map prep cs
    3.48 @@ -276,10 +284,11 @@
    3.49          (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs));
    3.50    in (cs', ctxt') end;
    3.51  
    3.52 -in
    3.53 +(**)in(**)
    3.54  
    3.55  fun check_autofix insts eqnss elems concl ctxt =
    3.56    let
    3.57 +    val _ = writeln "#### Expression.check_autofix";
    3.58      val inst_cs = map extract_inst insts;
    3.59      val eqns_cs = map extract_eqns eqnss;
    3.60      val elem_css = map extract_elem elems;
    3.61 @@ -295,7 +304,7 @@
    3.62        map fst concl ~~ concl_cs'), ctxt')
    3.63    end;
    3.64  
    3.65 -end;
    3.66 +(**)end;(**)
    3.67  
    3.68  
    3.69  (** Prepare locale elements **)

     4.1 --- a/src/Pure/Isar/obtain.ML	Thu Dec 17 11:45:12 2020 +0100
     4.2 +++ b/src/Pure/Isar/obtain.ML	Thu Dec 17 18:00:27 2020 +0100
     4.3 @@ -131,9 +131,11 @@
     4.4  val parse_clause = prepare_clause Proof_Context.read_var Syntax.parse_prop mk_all_external;
     4.5  val cert_clause = prepare_clause Proof_Context.cert_var (K I) mk_all_internal;
     4.6  
     4.7 -in
     4.8 +in                              
     4.9  
    4.10 -val read_obtains = prepare_obtains parse_clause Syntax.check_terms;
    4.11 +val read_obtains =
    4.12 +  (writeln "#### Obtain.read_obtains";
    4.13 +    prepare_obtains parse_clause Syntax.check_terms);
    4.14  val cert_obtains = prepare_obtains cert_clause (K I);
    4.15  val parse_obtains = prepare_obtains parse_clause (K I);
    4.16  

     5.1 --- a/src/Pure/Isar/proof.ML	Thu Dec 17 11:45:12 2020 +0100
     5.2 +++ b/src/Pure/Isar/proof.ML	Thu Dec 17 18:00:27 2020 +0100
     5.3 @@ -146,7 +146,7 @@
     5.4    val global_future_terminal_proof: Method.text_range * Method.text_range option -> state -> context
     5.5  end;
     5.6  
     5.7 -structure Proof: PROOF =
     5.8 +structure Proof(**): PROOF(**) =
     5.9  struct
    5.10  
    5.11  type context = Proof.context;
    5.12 @@ -557,7 +557,7 @@
    5.13  
    5.14  (* let bindings *)
    5.15  
    5.16 -local
    5.17 +(**)local(**)
    5.18  
    5.19  fun gen_bind prep_terms raw_binds =
    5.20    assert_forward #> map_context (fn ctxt =>
    5.21 @@ -582,15 +582,22 @@
    5.22      in ctxt'' end)
    5.23    #> reset_facts;
    5.24  
    5.25 +(*val read_terms: context -> typ -> string list -> term list*)
    5.26  fun read_terms ctxt T =
    5.27    map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt;
    5.28  
    5.29 -in
    5.30 +(**)in(**)
    5.31  
    5.32 -val let_bind = gen_bind (fn ctxt => fn _ => map (Proof_Context.cert_term ctxt));
    5.33 -val let_bind_cmd = gen_bind read_terms;
    5.34 +(*val let_bind: (term list * term) list -> state -> state*)
    5.35 +val let_bind =
    5.36 +  (writeln "#### Proof.let_bind";
    5.37 +    gen_bind (fn ctxt => fn _ => map (Proof_Context.cert_term ctxt)));
    5.38 +(*val let_bind_cmd: (string list * string) list -> state -> state*)
    5.39 +val let_bind_cmd =
    5.40 +  (writeln "#### Proof.let_bind_cmd";
    5.41 +    gen_bind read_terms);
    5.42  
    5.43 -end;
    5.44 +(**)end;(**)
    5.45  
    5.46  
    5.47  (* concrete syntax *)

     6.1 --- a/src/Pure/Isar/proof_context.ML	Thu Dec 17 11:45:12 2020 +0100
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Dec 17 18:00:27 2020 +0100
     6.3 @@ -504,7 +504,8 @@
     6.4  (* inferred types of parameters *)
     6.5  
     6.6  fun infer_type ctxt x =
     6.7 -  Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x));
     6.8 +  (writeln "#### Proof_Context.infer_type";
     6.9 +    Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x)));
    6.10  
    6.11  fun inferred_param x ctxt =
    6.12    let val p = (x, infer_type ctxt (x, dummyT))

     7.1 --- a/src/Pure/ROOT.ML	Thu Dec 17 11:45:12 2020 +0100
     7.2 +++ b/src/Pure/ROOT.ML	Thu Dec 17 18:00:27 2020 +0100
     7.3 @@ -355,3 +355,10 @@
     7.4  ML_file "Tools/jedit.ML";
     7.5  ML_file "Tools/ghc.ML";
     7.6  ML_file "Tools/generated_files.ML"
     7.7 +(* NOT during bootstrap -----------------------\\
     7.8 +ML \<open>
     7.9 +\<close> ML \<open>
    7.10 +\<close> ML \<open>
    7.11 +\<close> ML \<open>
    7.12 +\<close>
    7.13 +\\---------------------------------------------//*)
    7.14 \ No newline at end of file

     8.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Dec 17 11:45:12 2020 +0100
     8.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Dec 17 18:00:27 2020 +0100
     8.3 @@ -37,7 +37,7 @@
     8.4      Context.generic -> Context.generic
     8.5  end
     8.6  
     8.7 -structure Syntax_Phases: SYNTAX_PHASES =
     8.8 +structure Syntax_Phases(**): SYNTAX_PHASES(**) =
     8.9  struct
    8.10  
    8.11  (** markup logical entities **)
    8.12 @@ -972,6 +972,7 @@
    8.13      |> Term_Sharing.typs (Proof_Context.theory_of ctxt)
    8.14    end;
    8.15  
    8.16 +(*  Syntax_Phases.check_terms: Proof.context -> term list -> term list*)
    8.17  fun check_terms ctxt raw_ts =
    8.18    let
    8.19      val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts;
    8.20 @@ -992,7 +993,7 @@
    8.21        if Context_Position.is_visible ctxt
    8.22        then
    8.23          ((** )@{print} {a = "### Syntax_Phases.check_terms"};( *..NOT yet available 2 *)
    8.24 -         (**) writeln "### Syntax_Phases.check_terms";(**)
    8.25 +         (**)writeln "### Syntax_Phases.check_terms";(**)
    8.26            Output.report (sorting_report @ typing_report))
    8.27        else ();
    8.28    in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;

     9.1 --- a/src/Pure/Tools/rule_insts.ML	Thu Dec 17 11:45:12 2020 +0100
     9.2 +++ b/src/Pure/Tools/rule_insts.ML	Thu Dec 17 18:00:27 2020 +0100
     9.3 @@ -42,12 +42,12 @@
     9.4      (Proof.context -> Proof.method) context_parser
     9.5  end;
     9.6  
     9.7 -structure Rule_Insts: RULE_INSTS =
     9.8 +structure Rule_Insts(**): RULE_INSTS(**) =
     9.9  struct
    9.10  
    9.11  (** read instantiations **)
    9.12  
    9.13 -local
    9.14 +(**)local(**)
    9.15  
    9.16  fun error_var msg (xi, pos) =
    9.17    error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos);
    9.18 @@ -83,8 +83,11 @@
    9.19      val t' = f t;
    9.20    in if t aconv t' then NONE else SOME (v, t') end;
    9.21  
    9.22 +(*   read_terms: string list -> typ list -> Proof.context ->
    9.23 +        (term list * ((Vartab.key * sort) * typ) list) * Proof.context*)
    9.24  fun read_terms ss Ts ctxt =
    9.25    let
    9.26 +    val _ = writeln "#### Rule_Insts.read_terms";
    9.27      fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
    9.28      val (ts, ctxt') = fold_map Variable.fix_dummy_patterns (map2 parse Ts ss) ctxt;
    9.29      val ts' =
    9.30 @@ -96,10 +99,12 @@
    9.31      val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
    9.32    in ((ts', tyenv'), ctxt') end;
    9.33  
    9.34 -in
    9.35 +(**)in(**)
    9.36  
    9.37 +(*  read_term: string -> Proof.context -> term * Proof.context*)
    9.38  fun read_term s ctxt =
    9.39    let
    9.40 +    val _ = writeln "#### Rule_Insts.read_term";
    9.41      val (t, ctxt') = Variable.fix_dummy_patterns (Syntax.parse_term ctxt s) ctxt;
    9.42      val t' = Syntax.check_term ctxt' t;
    9.43    in (t', ctxt') end;
    9.44 @@ -138,7 +143,7 @@
    9.45      val inst_vars = map_filter (make_inst inst2) vars2;
    9.46    in ((inst_tvars, inst_vars), ctxt2) end;
    9.47  
    9.48 -end;
    9.49 +(**)end;(**)
    9.50  
    9.51  
    9.52  

    10.1 --- a/src/Pure/simplifier.ML	Thu Dec 17 11:45:12 2020 +0100
    10.2 +++ b/src/Pure/simplifier.ML	Thu Dec 17 18:00:27 2020 +0100
    10.3 @@ -152,7 +152,9 @@
    10.4  
    10.5  in
    10.6  
    10.7 -val define_simproc = def_simproc Syntax.check_terms;
    10.8 +val define_simproc =
    10.9 +  (writeln "#### Simplifier.define_simproc";
   10.10 +    def_simproc Syntax.check_terms);
   10.11  val define_simproc_cmd = def_simproc Syntax.read_terms;
   10.12  
   10.13  end;