src/Pure/ML/ml_antiquote.ML
author wenzelm
Fri Apr 27 22:47:30 2012 +0200 (2012-04-27 ago)
changeset 47815 43f677b3ae91
parent 46987 15ce93dfe6da
child 48646 91281e9472d8
permissions -rw-r--r--
clarified signature;
wenzelm@27340
     1
(*  Title:      Pure/ML/ml_antiquote.ML
wenzelm@27340
     2
    Author:     Makarius
wenzelm@27340
     3
wenzelm@27340
     4
Common ML antiquotations.
wenzelm@27340
     5
*)
wenzelm@27340
     6
wenzelm@27340
     7
signature ML_ANTIQUOTE =
wenzelm@27340
     8
sig
wenzelm@27340
     9
  val variant: string -> Proof.context -> string * Proof.context
wenzelm@43560
    10
  val macro: binding -> Proof.context context_parser -> theory -> theory
wenzelm@43560
    11
  val inline: binding -> string context_parser -> theory -> theory
wenzelm@43560
    12
  val declaration: string -> binding -> string context_parser -> theory -> theory
wenzelm@43560
    13
  val value: binding -> string context_parser -> theory -> theory
wenzelm@27340
    14
end;
wenzelm@27340
    15
wenzelm@27340
    16
structure ML_Antiquote: ML_ANTIQUOTE =
wenzelm@27340
    17
struct
wenzelm@27340
    18
wenzelm@27340
    19
(** generic tools **)
wenzelm@27340
    20
wenzelm@27340
    21
(* ML names *)
wenzelm@27340
    22
wenzelm@37216
    23
structure Names = Proof_Data
wenzelm@27340
    24
(
wenzelm@27340
    25
  type T = Name.context;
wenzelm@27340
    26
  fun init _ = ML_Syntax.reserved;
wenzelm@27340
    27
);
wenzelm@27340
    28
wenzelm@27340
    29
fun variant a ctxt =
wenzelm@27340
    30
  let
wenzelm@37216
    31
    val names = Names.get ctxt;
wenzelm@43326
    32
    val (b, names') = Name.variant a names;
wenzelm@37216
    33
    val ctxt' = Names.put names' ctxt;
wenzelm@27340
    34
  in (b, ctxt') end;
wenzelm@27340
    35
wenzelm@27340
    36
wenzelm@27340
    37
(* specific antiquotations *)
wenzelm@27340
    38
wenzelm@27379
    39
fun macro name scan = ML_Context.add_antiq name
wenzelm@27868
    40
  (fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
wenzelm@35019
    41
    (Context.Proof ctxt, fn background => (K ("", ""), background)))));
wenzelm@27379
    42
wenzelm@27340
    43
fun inline name scan = ML_Context.add_antiq name
wenzelm@35019
    44
  (fn _ => scan >> (fn s => fn background => (K ("", s), background)));
wenzelm@27340
    45
wenzelm@27340
    46
fun declaration kind name scan = ML_Context.add_antiq name
wenzelm@35019
    47
  (fn _ => scan >> (fn s => fn background =>
wenzelm@27340
    48
    let
wenzelm@43560
    49
      val (a, background') =
wenzelm@43560
    50
        variant (translate_string (fn "." => "_" | c => c) (Binding.name_of name)) background;
wenzelm@27340
    51
      val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
wenzelm@41486
    52
      val body = "Isabelle." ^ a;
wenzelm@27340
    53
    in (K (env, body), background') end));
wenzelm@27340
    54
wenzelm@27340
    55
val value = declaration "val";
wenzelm@27340
    56
wenzelm@27340
    57
wenzelm@27340
    58
wenzelm@30231
    59
(** misc antiquotations **)
wenzelm@27340
    60
wenzelm@43560
    61
val _ = Context.>> (Context.map_theory
wenzelm@43560
    62
wenzelm@43560
    63
 (inline (Binding.name "assert")
wenzelm@43560
    64
    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
wenzelm@40110
    65
wenzelm@43560
    66
  inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
wenzelm@36162
    67
wenzelm@43560
    68
  value (Binding.name "binding")
wenzelm@46961
    69
    (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
wenzelm@27340
    70
wenzelm@43560
    71
  value (Binding.name "theory")
wenzelm@43560
    72
    (Scan.lift Args.name >> (fn name =>
wenzelm@43560
    73
      "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
wenzelm@43560
    74
    || Scan.succeed "ML_Context.the_global_context ()") #>
wenzelm@27340
    75
wenzelm@43560
    76
  value (Binding.name "context") (Scan.succeed "ML_Context.the_local_context ()") #>
wenzelm@27340
    77
wenzelm@43560
    78
  inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
wenzelm@43560
    79
  inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
wenzelm@43560
    80
  inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
wenzelm@27340
    81
wenzelm@43560
    82
  macro (Binding.name "let")
wenzelm@43560
    83
    (Args.context --
wenzelm@43560
    84
      Scan.lift
wenzelm@43560
    85
        (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
wenzelm@43560
    86
        >> (fn (ctxt, args) => #2 (Proof_Context.match_bind true args ctxt))) #>
wenzelm@27379
    87
wenzelm@43560
    88
  macro (Binding.name "note")
wenzelm@43560
    89
    (Args.context :|-- (fn ctxt =>
wenzelm@43560
    90
      Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms
wenzelm@47815
    91
        >> (fn ((a, srcs), ths) => ((a, map (Attrib.attribute_cmd ctxt) srcs), [(ths, [])])))
wenzelm@43560
    92
      >> (fn args => #2 (Proof_Context.note_thmss "" args ctxt)))) #>
wenzelm@27379
    93
wenzelm@43560
    94
  value (Binding.name "ctyp") (Args.typ >> (fn T =>
wenzelm@43560
    95
    "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
wenzelm@27340
    96
wenzelm@43560
    97
  value (Binding.name "cterm") (Args.term >> (fn t =>
wenzelm@46961
    98
    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
wenzelm@27340
    99
wenzelm@43560
   100
  value (Binding.name "cprop") (Args.prop >> (fn t =>
wenzelm@46961
   101
    "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
wenzelm@27340
   102
wenzelm@43560
   103
  value (Binding.name "cpat")
wenzelm@43560
   104
    (Args.context --
wenzelm@43560
   105
      Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
wenzelm@43560
   106
        "Thm.cterm_of (ML_Context.the_global_context ()) " ^
wenzelm@43560
   107
          ML_Syntax.atomic (ML_Syntax.print_term t)))));
wenzelm@27340
   108
wenzelm@27340
   109
wenzelm@35396
   110
(* type classes *)
wenzelm@35396
   111
wenzelm@35670
   112
fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
wenzelm@42360
   113
  Proof_Context.read_class ctxt s
wenzelm@42290
   114
  |> syn ? Lexicon.mark_class
wenzelm@35396
   115
  |> ML_Syntax.print_string);
wenzelm@35396
   116
wenzelm@43560
   117
val _ = Context.>> (Context.map_theory
wenzelm@43560
   118
 (inline (Binding.name "class") (class false) #>
wenzelm@43560
   119
  inline (Binding.name "class_syntax") (class true) #>
wenzelm@35396
   120
wenzelm@43560
   121
  inline (Binding.name "sort")
wenzelm@43560
   122
    (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
wenzelm@43560
   123
      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))));
wenzelm@35396
   124
wenzelm@35396
   125
wenzelm@35361
   126
(* type constructors *)
wenzelm@27340
   127
wenzelm@36950
   128
fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
wenzelm@35401
   129
  >> (fn (ctxt, (s, pos)) =>
wenzelm@35401
   130
    let
wenzelm@42360
   131
      val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
wenzelm@42468
   132
      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
wenzelm@35401
   133
      val res =
wenzelm@35401
   134
        (case try check (c, decl) of
wenzelm@35401
   135
          SOME res => res
wenzelm@35401
   136
        | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.str_of pos));
wenzelm@35401
   137
    in ML_Syntax.print_string res end);
wenzelm@27340
   138
wenzelm@43560
   139
val _ = Context.>> (Context.map_theory
wenzelm@43560
   140
 (inline (Binding.name "type_name")
wenzelm@43560
   141
    (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
wenzelm@43560
   142
  inline (Binding.name "type_abbrev")
wenzelm@43560
   143
    (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
wenzelm@43560
   144
  inline (Binding.name "nonterminal")
wenzelm@43560
   145
    (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
wenzelm@43560
   146
  inline (Binding.name "type_syntax")
wenzelm@43560
   147
    (type_name "type" (fn (c, _) => Lexicon.mark_type c))));
wenzelm@35361
   148
wenzelm@35361
   149
wenzelm@35361
   150
(* constants *)
wenzelm@27340
   151
wenzelm@36950
   152
fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
wenzelm@35401
   153
  >> (fn (ctxt, (s, pos)) =>
wenzelm@35401
   154
    let
wenzelm@42360
   155
      val Const (c, _) = Proof_Context.read_const_proper ctxt false s;
wenzelm@42360
   156
      val res = check (Proof_Context.consts_of ctxt, c)
wenzelm@35401
   157
        handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
wenzelm@35401
   158
    in ML_Syntax.print_string res end);
wenzelm@27340
   159
wenzelm@43560
   160
val _ = Context.>> (Context.map_theory
wenzelm@43560
   161
 (inline (Binding.name "const_name")
wenzelm@43794
   162
    (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
wenzelm@43560
   163
  inline (Binding.name "const_abbrev")
wenzelm@43560
   164
    (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
wenzelm@43560
   165
  inline (Binding.name "const_syntax")
wenzelm@43560
   166
    (const_name (fn (_, c) => Lexicon.mark_const c)) #>
wenzelm@35401
   167
wenzelm@43560
   168
  inline (Binding.name "syntax_const")
wenzelm@43560
   169
    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
wenzelm@43560
   170
      if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
wenzelm@43560
   171
      then ML_Syntax.print_string c
wenzelm@43560
   172
      else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos))) #>
wenzelm@27340
   173
wenzelm@43560
   174
  inline (Binding.name "const")
wenzelm@43560
   175
    (Args.context -- Scan.lift Args.name_source -- Scan.optional
wenzelm@43560
   176
        (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
wenzelm@43560
   177
      >> (fn ((ctxt, raw_c), Ts) =>
wenzelm@43560
   178
        let
wenzelm@43560
   179
          val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
wenzelm@46987
   180
          val consts = Proof_Context.consts_of ctxt;
wenzelm@46987
   181
          val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
wenzelm@46987
   182
          val _ = length Ts <> n andalso
wenzelm@46987
   183
            error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
wenzelm@46987
   184
              quote c ^ enclose "(" ")" (commas (replicate n "_")));
wenzelm@46987
   185
          val const = Const (c, Consts.instance consts (c, Ts));
wenzelm@43560
   186
        in ML_Syntax.atomic (ML_Syntax.print_term const) end))));
wenzelm@27340
   187
wenzelm@46948
   188
wenzelm@46948
   189
(* outer syntax *)
wenzelm@46948
   190
wenzelm@46961
   191
fun with_keyword f =
wenzelm@46961
   192
  Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
wenzelm@46961
   193
    (f (name, Thy_Header.the_keyword thy name)
wenzelm@46961
   194
      handle ERROR msg => error (msg ^ Position.str_of pos)));
wenzelm@46961
   195
wenzelm@46948
   196
val _ = Context.>> (Context.map_theory
wenzelm@46961
   197
 (value (Binding.name "keyword")
wenzelm@46961
   198
    (with_keyword
wenzelm@46961
   199
      (fn (name, NONE) => "Parse.$$$ " ^ ML_Syntax.print_string name
wenzelm@46961
   200
        | (name, SOME _) => error ("Expected minor keyword " ^ quote name))) #>
wenzelm@46961
   201
  value (Binding.name "command_spec")
wenzelm@46961
   202
    (with_keyword
wenzelm@46961
   203
      (fn (name, SOME kind) =>
wenzelm@46961
   204
          "Keyword.command_spec " ^ ML_Syntax.atomic
wenzelm@46961
   205
            (ML_Syntax.print_pair ML_Syntax.print_string
wenzelm@46961
   206
              (ML_Syntax.print_pair ML_Syntax.print_string
wenzelm@46961
   207
                (ML_Syntax.print_list ML_Syntax.print_string)) (name, kind))
wenzelm@46961
   208
        | (name, NONE) => error ("Expected command keyword " ^ quote name)))));
wenzelm@46948
   209
wenzelm@27340
   210
end;
wenzelm@27340
   211