added ML antiquotation @{print};
authorwenzelm
Fri Apr 04 12:07:48 2014 +0200 (2014-04-04)
changeset 56399386e4cb7ad68
parent 56398 15d0821c8667
child 56400 f0bd809b5d35
added ML antiquotation @{print};
NEWS
src/Doc/IsarImplementation/ML.thy
src/Pure/ML/ml_antiquotations.ML
     1.1 --- a/NEWS	Fri Apr 04 10:41:53 2014 +0200
     1.2 +++ b/NEWS	Fri Apr 04 12:07:48 2014 +0200
     1.3 @@ -642,6 +642,10 @@
     1.4  well-defined master directory, so an absolute symbolic path
     1.5  specification is usually required, e.g. "~~/src/HOL".
     1.6  
     1.7 +* ML antiquotation @{print} inlines a function to print an arbitrary
     1.8 +ML value, which is occasionally useful for diagnostic or demonstration
     1.9 +purposes.
    1.10 +
    1.11  
    1.12  *** System ***
    1.13  
     2.1 --- a/src/Doc/IsarImplementation/ML.thy	Fri Apr 04 10:41:53 2014 +0200
     2.2 +++ b/src/Doc/IsarImplementation/ML.thy	Fri Apr 04 12:07:48 2014 +0200
     2.3 @@ -690,38 +690,52 @@
     2.4  text {* The ML compiler knows about the structure of values according
     2.5    to their static type, and can print them in the manner of the
     2.6    toplevel loop, although the details are non-portable.  The
     2.7 -  antiquotation @{ML_antiquotation_def "make_string"} provides a
     2.8 -  quasi-portable way to refer to this potential capability of the
     2.9 -  underlying ML system in generic Isabelle/ML sources.  *}
    2.10 +  antiquotations @{ML_antiquotation_def "make_string"} and
    2.11 +  @{ML_antiquotation_def "print"} provide a quasi-portable way to
    2.12 +  refer to this potential capability of the underlying ML system in
    2.13 +  generic Isabelle/ML sources.
    2.14 +
    2.15 +  This is occasionally useful for diagnostic or demonstration
    2.16 +  purposes.  Note that production-quality tools require proper
    2.17 +  user-level error messages. *}
    2.18  
    2.19  text %mlantiq {*
    2.20    \begin{matharray}{rcl}
    2.21    @{ML_antiquotation_def "make_string"} & : & @{text ML_antiquotation} \\
    2.22 +  @{ML_antiquotation_def "print"} & : & @{text ML_antiquotation} \\
    2.23    \end{matharray}
    2.24  
    2.25    @{rail \<open>
    2.26    @@{ML_antiquotation make_string}
    2.27 +  ;
    2.28 +  @@{ML_antiquotation print} @{syntax name}?
    2.29    \<close>}
    2.30  
    2.31    \begin{description}
    2.32  
    2.33    \item @{text "@{make_string}"} inlines a function to print arbitrary
    2.34 -values similar to the ML toplevel.  The result is compiler dependent
    2.35 -and may fall back on "?" in certain situations.
    2.36 +  values similar to the ML toplevel.  The result is compiler dependent
    2.37 +  and may fall back on "?" in certain situations.
    2.38 +
    2.39 +  \item @{text "@{print f}"} uses the ML function @{text "f: string ->
    2.40 +  unit"} to output the result of @{text "@{make_string}"} above,
    2.41 +  together with the source position of the antiquotation.  The default
    2.42 +  output function is @{ML writeln}.
    2.43  
    2.44    \end{description}
    2.45  *}
    2.46  
    2.47 -text %mlex {* The following artificial example shows how to produce
    2.48 -  ad-hoc output of ML values for debugging purposes.  This should not
    2.49 -  be done in production code, and not persist in regular Isabelle/ML
    2.50 -  sources.  *}
    2.51 +text %mlex {* The following artificial examples show how to produce
    2.52 +  adhoc output of ML values for debugging purposes. *}
    2.53  
    2.54  ML {*
    2.55    val x = 42;
    2.56    val y = true;
    2.57  
    2.58    writeln (@{make_string} {x = x, y = y});
    2.59 +
    2.60 +  @{print} {x = x, y = y};
    2.61 +  @{print tracing} {x = x, y = y};
    2.62  *}
    2.63  
    2.64  
     3.1 --- a/src/Pure/ML/ml_antiquotations.ML	Fri Apr 04 10:41:53 2014 +0200
     3.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Fri Apr 04 12:07:48 2014 +0200
     3.3 @@ -8,12 +8,7 @@
     3.4  struct
     3.5  
     3.6  val _ = Theory.setup
     3.7 - (ML_Antiquotation.inline @{binding assert}
     3.8 -    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
     3.9 -
    3.10 -  ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
    3.11 -
    3.12 -  ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
    3.13 + (ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
    3.14      (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
    3.15       ML_Syntax.print_string name))) #>
    3.16  
    3.17 @@ -56,6 +51,30 @@
    3.18            ML_Syntax.atomic (ML_Syntax.print_term t))));
    3.19  
    3.20  
    3.21 +(* ML support *)
    3.22 +
    3.23 +val _ = Theory.setup
    3.24 + (ML_Antiquotation.inline @{binding assert}
    3.25 +    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
    3.26 +
    3.27 +  ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
    3.28 +
    3.29 +  ML_Antiquotation.declaration @{binding print}
    3.30 +    (Scan.lift (Scan.optional Args.name "Output.writeln"))
    3.31 +      (fn src => fn output => fn ctxt =>
    3.32 +        let
    3.33 +          val (_, pos) = Args.name_of_src src;
    3.34 +          val (a, ctxt') = ML_Antiquotation.variant "output" ctxt;
    3.35 +          val env =
    3.36 +            "val " ^ a ^ ": string -> unit =\n\
    3.37 +            \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
    3.38 +            ML_Syntax.print_position pos ^ "));\n";
    3.39 +          val body =
    3.40 +            "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))";
    3.41 +        in (K (env, body), ctxt') end));
    3.42 +
    3.43 +  
    3.44 +
    3.45  (* type classes *)
    3.46  
    3.47  fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>