src/Pure/ML/ml_antiquotations.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 64594 4719f13989df
child 67146 909dcdec2122
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@56205
     1
(*  Title:      Pure/ML/ml_antiquotations.ML
wenzelm@56205
     2
    Author:     Makarius
wenzelm@56205
     3
wenzelm@56205
     4
Miscellaneous ML antiquotations.
wenzelm@56205
     5
*)
wenzelm@56205
     6
wenzelm@56205
     7
structure ML_Antiquotations: sig end =
wenzelm@56205
     8
struct
wenzelm@56205
     9
wenzelm@58632
    10
(* ML support *)
wenzelm@58632
    11
wenzelm@58632
    12
val _ = Theory.setup
wenzelm@62850
    13
 (ML_Antiquotation.inline @{binding undefined}
wenzelm@61597
    14
    (Scan.succeed "(raise General.Match)") #>
wenzelm@61597
    15
wenzelm@61596
    16
  ML_Antiquotation.inline @{binding assert}
wenzelm@58632
    17
    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
wenzelm@58632
    18
wenzelm@58632
    19
  ML_Antiquotation.declaration @{binding print}
wenzelm@63120
    20
    (Scan.lift (Scan.optional Args.embedded "Output.writeln"))
wenzelm@58632
    21
      (fn src => fn output => fn ctxt =>
wenzelm@58632
    22
        let
wenzelm@59127
    23
          val struct_name = ML_Context.struct_name ctxt;
wenzelm@58632
    24
          val (_, pos) = Token.name_of_src src;
wenzelm@59112
    25
          val (a, ctxt') = ML_Context.variant "output" ctxt;
wenzelm@58632
    26
          val env =
wenzelm@58632
    27
            "val " ^ a ^ ": string -> unit =\n\
wenzelm@58632
    28
            \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
wenzelm@58632
    29
            ML_Syntax.print_position pos ^ "));\n";
wenzelm@58632
    30
          val body =
wenzelm@62900
    31
            "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))";
wenzelm@63204
    32
        in (K (env, body), ctxt') end) #>
wenzelm@63204
    33
wenzelm@63204
    34
  ML_Antiquotation.value @{binding rat}
wenzelm@63204
    35
    (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat --
wenzelm@63204
    36
      Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) =>
wenzelm@63204
    37
        "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))))
wenzelm@58632
    38
wenzelm@58632
    39
wenzelm@58632
    40
(* formal entities *)
wenzelm@58632
    41
wenzelm@56205
    42
val _ = Theory.setup
wenzelm@56467
    43
 (ML_Antiquotation.value @{binding system_option}
wenzelm@56465
    44
    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
wenzelm@59812
    45
      let
wenzelm@59812
    46
        val markup =
wenzelm@59812
    47
          Options.default_markup (name, pos) handle ERROR msg =>
wenzelm@59812
    48
            let
wenzelm@59812
    49
              val completion =
wenzelm@59812
    50
                Completion.make (name, pos) (fn completed =>
wenzelm@59812
    51
                    Options.names (Options.default ())
wenzelm@59812
    52
                    |> filter completed
wenzelm@59812
    53
                    |> map (fn a => (a, ("system_option", a))));
wenzelm@59812
    54
              val report = Markup.markup_report (Completion.reported_text completion);
wenzelm@59878
    55
            in error (msg ^ report) end;
wenzelm@59812
    56
        val _ = Context_Position.report ctxt pos markup;
wenzelm@59812
    57
      in ML_Syntax.print_string name end)) #>
wenzelm@56205
    58
wenzelm@56205
    59
  ML_Antiquotation.value @{binding theory}
wenzelm@56205
    60
    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
wenzelm@60099
    61
      (Theory.check ctxt (name, pos);
wenzelm@56205
    62
       "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
wenzelm@56205
    63
    || Scan.succeed "Proof_Context.theory_of ML_context") #>
wenzelm@56205
    64
wenzelm@56205
    65
  ML_Antiquotation.value @{binding theory_context}
wenzelm@56205
    66
    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
wenzelm@60099
    67
      (Theory.check ctxt (name, pos);
wenzelm@56205
    68
       "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
wenzelm@56205
    69
        ML_Syntax.print_string name))) #>
wenzelm@56205
    70
wenzelm@59127
    71
  ML_Antiquotation.inline @{binding context}
wenzelm@59127
    72
    (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #>
wenzelm@56205
    73
wenzelm@56205
    74
  ML_Antiquotation.inline @{binding typ} (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
wenzelm@56205
    75
  ML_Antiquotation.inline @{binding term} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
wenzelm@56205
    76
  ML_Antiquotation.inline @{binding prop} (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
wenzelm@56205
    77
wenzelm@56205
    78
  ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T =>
wenzelm@59621
    79
    "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
wenzelm@56205
    80
wenzelm@56205
    81
  ML_Antiquotation.value @{binding cterm} (Args.term >> (fn t =>
wenzelm@59621
    82
    "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
wenzelm@56205
    83
wenzelm@56205
    84
  ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t =>
wenzelm@62075
    85
    "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
wenzelm@62075
    86
wenzelm@62075
    87
  ML_Antiquotation.inline @{binding method}
wenzelm@62075
    88
    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
wenzelm@62075
    89
      ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
wenzelm@56205
    90
wenzelm@56205
    91
haftmann@63553
    92
(* locales *)
haftmann@63553
    93
haftmann@63553
    94
val _ = Theory.setup
haftmann@63553
    95
 (ML_Antiquotation.inline @{binding locale}
haftmann@63553
    96
   (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
haftmann@63553
    97
      Locale.check (Proof_Context.theory_of ctxt) (name, pos)
haftmann@63553
    98
      |> ML_Syntax.print_string)));
haftmann@63553
    99
haftmann@63553
   100
wenzelm@56205
   101
(* type classes *)
wenzelm@56205
   102
wenzelm@63120
   103
fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
wenzelm@56205
   104
  Proof_Context.read_class ctxt s
wenzelm@56205
   105
  |> syn ? Lexicon.mark_class
wenzelm@56205
   106
  |> ML_Syntax.print_string);
wenzelm@56205
   107
wenzelm@56205
   108
val _ = Theory.setup
wenzelm@56205
   109
 (ML_Antiquotation.inline @{binding class} (class false) #>
wenzelm@56205
   110
  ML_Antiquotation.inline @{binding class_syntax} (class true) #>
wenzelm@56205
   111
wenzelm@56205
   112
  ML_Antiquotation.inline @{binding sort}
wenzelm@63120
   113
    (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
wenzelm@56205
   114
      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
wenzelm@56205
   115
wenzelm@56205
   116
wenzelm@56205
   117
(* type constructors *)
wenzelm@56205
   118
wenzelm@63120
   119
fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
wenzelm@56205
   120
  >> (fn (ctxt, (s, pos)) =>
wenzelm@56205
   121
    let
wenzelm@56205
   122
      val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
wenzelm@56205
   123
      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
wenzelm@56205
   124
      val res =
wenzelm@56205
   125
        (case try check (c, decl) of
wenzelm@56205
   126
          SOME res => res
wenzelm@56205
   127
        | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
wenzelm@56205
   128
    in ML_Syntax.print_string res end);
wenzelm@56205
   129
wenzelm@56205
   130
val _ = Theory.setup
wenzelm@56205
   131
 (ML_Antiquotation.inline @{binding type_name}
wenzelm@56205
   132
    (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
wenzelm@56205
   133
  ML_Antiquotation.inline @{binding type_abbrev}
wenzelm@56205
   134
    (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
wenzelm@56205
   135
  ML_Antiquotation.inline @{binding nonterminal}
wenzelm@56205
   136
    (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
wenzelm@56205
   137
  ML_Antiquotation.inline @{binding type_syntax}
wenzelm@56205
   138
    (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
wenzelm@56205
   139
wenzelm@56205
   140
wenzelm@56205
   141
(* constants *)
wenzelm@56205
   142
wenzelm@63120
   143
fun const_name check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
wenzelm@56205
   144
  >> (fn (ctxt, (s, pos)) =>
wenzelm@56205
   145
    let
wenzelm@56205
   146
      val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
wenzelm@56205
   147
      val res = check (Proof_Context.consts_of ctxt, c)
wenzelm@56205
   148
        handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
wenzelm@56205
   149
    in ML_Syntax.print_string res end);
wenzelm@56205
   150
wenzelm@56205
   151
val _ = Theory.setup
wenzelm@56205
   152
 (ML_Antiquotation.inline @{binding const_name}
wenzelm@56205
   153
    (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
wenzelm@56205
   154
  ML_Antiquotation.inline @{binding const_abbrev}
wenzelm@56205
   155
    (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
wenzelm@56205
   156
  ML_Antiquotation.inline @{binding const_syntax}
wenzelm@56205
   157
    (const_name (fn (_, c) => Lexicon.mark_const c)) #>
wenzelm@56205
   158
wenzelm@56205
   159
  ML_Antiquotation.inline @{binding syntax_const}
wenzelm@63120
   160
    (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (c, pos)) =>
wenzelm@56205
   161
      if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
wenzelm@56205
   162
      then ML_Syntax.print_string c
wenzelm@56205
   163
      else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
wenzelm@56205
   164
wenzelm@56205
   165
  ML_Antiquotation.inline @{binding const}
wenzelm@63120
   166
    (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional
wenzelm@56205
   167
        (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
wenzelm@56251
   168
      >> (fn ((ctxt, (raw_c, pos)), Ts) =>
wenzelm@56205
   169
        let
wenzelm@56205
   170
          val Const (c, _) =
wenzelm@56205
   171
            Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
wenzelm@56205
   172
          val consts = Proof_Context.consts_of ctxt;
wenzelm@56205
   173
          val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
wenzelm@56205
   174
          val _ = length Ts <> n andalso
wenzelm@56205
   175
            error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
wenzelm@56251
   176
              quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos);
wenzelm@56205
   177
          val const = Const (c, Consts.instance consts (c, Ts));
wenzelm@56205
   178
        in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
wenzelm@56205
   179
wenzelm@56205
   180
wenzelm@58634
   181
(* basic combinators *)
wenzelm@58634
   182
wenzelm@58634
   183
local
wenzelm@58634
   184
wenzelm@58634
   185
val parameter = Parse.position Parse.nat >> (fn (n, pos) =>
wenzelm@58634
   186
  if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos));
wenzelm@58634
   187
wenzelm@58634
   188
fun indices n = map string_of_int (1 upto n);
wenzelm@58634
   189
wenzelm@58634
   190
fun empty n = replicate_string n " []";
wenzelm@58634
   191
fun dummy n = replicate_string n " _";
wenzelm@58634
   192
fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n));
wenzelm@58634
   193
fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n));
wenzelm@58634
   194
wenzelm@58634
   195
val tuple = enclose "(" ")" o commas;
wenzelm@58634
   196
fun tuple_empty n = tuple (replicate n "[]");
wenzelm@58634
   197
fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n));
wenzelm@58634
   198
fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)"
wenzelm@58634
   199
fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n));
wenzelm@58634
   200
wenzelm@58634
   201
in
wenzelm@58634
   202
wenzelm@58634
   203
val _ = Theory.setup
wenzelm@58634
   204
 (ML_Antiquotation.value @{binding map}
wenzelm@58634
   205
    (Scan.lift parameter >> (fn n =>
wenzelm@58634
   206
      "fn f =>\n\
wenzelm@58634
   207
      \  let\n\
wenzelm@58634
   208
      \    fun map _" ^ empty n ^ " = []\n\
wenzelm@58634
   209
      \      | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\
wenzelm@58634
   210
      \      | map _" ^  dummy n ^ " = raise ListPair.UnequalLengths\n" ^
wenzelm@58634
   211
      "  in map f end")) #>
wenzelm@58634
   212
  ML_Antiquotation.value @{binding fold}
wenzelm@58634
   213
    (Scan.lift parameter >> (fn n =>
wenzelm@58634
   214
      "fn f =>\n\
wenzelm@58634
   215
      \  let\n\
wenzelm@58634
   216
      \    fun fold _" ^ empty n ^ " a = a\n\
wenzelm@58634
   217
      \      | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\
wenzelm@58634
   218
      \      | fold _" ^  dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
wenzelm@58634
   219
      "  in fold f end")) #>
wenzelm@58634
   220
  ML_Antiquotation.value @{binding fold_map}
wenzelm@58634
   221
    (Scan.lift parameter >> (fn n =>
wenzelm@58634
   222
      "fn f =>\n\
wenzelm@58634
   223
      \  let\n\
wenzelm@58634
   224
      \    fun fold_map _" ^ empty n ^ " a = ([], a)\n\
wenzelm@58634
   225
      \      | fold_map f" ^ cons n ^ " a =\n\
wenzelm@58634
   226
      \          let\n\
wenzelm@58634
   227
      \            val (x, a') = f" ^ vars "x" n ^ " a\n\
wenzelm@58634
   228
      \            val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\
wenzelm@58634
   229
      \          in (x :: xs, a'') end\n\
wenzelm@58634
   230
      \      | fold_map _" ^  dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
wenzelm@58634
   231
      "  in fold_map f end")) #>
wenzelm@58634
   232
  ML_Antiquotation.value @{binding split_list}
wenzelm@58634
   233
    (Scan.lift parameter >> (fn n =>
wenzelm@58634
   234
      "fn list =>\n\
wenzelm@58634
   235
      \  let\n\
wenzelm@58634
   236
      \    fun split_list [] =" ^ tuple_empty n ^ "\n\
wenzelm@58634
   237
      \      | split_list" ^ tuple_cons n ^ " =\n\
wenzelm@58634
   238
      \          let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\
wenzelm@58634
   239
      \          in " ^ cons_tuple n ^ "end\n\
wenzelm@59057
   240
      \  in split_list list end")) #>
wenzelm@59057
   241
  ML_Antiquotation.value @{binding apply}
wenzelm@59057
   242
    (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >>
wenzelm@59057
   243
      (fn (n, opt_index) =>
wenzelm@59057
   244
        let
wenzelm@59057
   245
          val cond =
wenzelm@59057
   246
            (case opt_index of
wenzelm@59057
   247
              NONE => K true
wenzelm@59057
   248
            | SOME (index, index_pos) =>
wenzelm@59057
   249
                if 1 <= index andalso index <= n then equal (string_of_int index)
wenzelm@59057
   250
                else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos));
wenzelm@59057
   251
        in
wenzelm@59057
   252
          "fn f => fn " ^ tuple_vars "x" n ^ " => " ^
wenzelm@59057
   253
            tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n))
wenzelm@59057
   254
        end)));
wenzelm@58634
   255
wenzelm@58634
   256
end;
wenzelm@58634
   257
wenzelm@58634
   258
wenzelm@56205
   259
(* outer syntax *)
wenzelm@56205
   260
wenzelm@56205
   261
val _ = Theory.setup
wenzelm@56205
   262
 (ML_Antiquotation.value @{binding keyword}
wenzelm@64594
   263
    (Args.context -- Scan.lift (Parse.position (Parse.name || Parse.keyword_with (K true)))
wenzelm@64594
   264
      >> (fn (ctxt, (name, pos)) =>
wenzelm@64594
   265
        if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then
wenzelm@64594
   266
          (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
wenzelm@64594
   267
           "Parse.$$$ " ^ ML_Syntax.print_string name)
wenzelm@64594
   268
        else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
wenzelm@59936
   269
  ML_Antiquotation.value @{binding command_keyword}
wenzelm@59934
   270
    (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
wenzelm@59934
   271
      (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
wenzelm@59934
   272
        SOME markup =>
wenzelm@59934
   273
         (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)];
wenzelm@59934
   274
          ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos))
wenzelm@59934
   275
      | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos)))));
wenzelm@56205
   276
wenzelm@56205
   277
end;