src/Pure/ML/ml_antiquote.ML
author wenzelm
Wed Mar 12 22:44:55 2014 +0100 (2014-03-12)
changeset 56071 2ffdedb0c044
parent 56069 451d5b73f8cf
permissions -rw-r--r--
added ML antiquotation @{here};
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 inline: binding -> string context_parser -> theory -> theory
wenzelm@43560
    11
  val value: binding -> string context_parser -> theory -> theory
wenzelm@27340
    12
end;
wenzelm@27340
    13
wenzelm@27340
    14
structure ML_Antiquote: ML_ANTIQUOTE =
wenzelm@27340
    15
struct
wenzelm@27340
    16
wenzelm@27340
    17
(** generic tools **)
wenzelm@27340
    18
wenzelm@27340
    19
(* ML names *)
wenzelm@27340
    20
wenzelm@48776
    21
val init_context = ML_Syntax.reserved |> Name.declare "ML_context";
wenzelm@48776
    22
wenzelm@37216
    23
structure Names = Proof_Data
wenzelm@27340
    24
(
wenzelm@27340
    25
  type T = Name.context;
wenzelm@48776
    26
  fun init _ = init_context;
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@53170
    32
    val (b, names') = Name.variant (Name.desymbolize false 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@53169
    39
fun inline name scan =
wenzelm@56069
    40
  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
wenzelm@27340
    41
wenzelm@53169
    42
fun value name scan =
wenzelm@56069
    43
  ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt =>
wenzelm@56069
    44
    let
wenzelm@56069
    45
      val (a, ctxt') = variant (Binding.name_of name) ctxt;
wenzelm@56069
    46
      val env = "val " ^ a ^ " = " ^ s ^ ";\n";
wenzelm@56069
    47
      val body = "Isabelle." ^ a;
wenzelm@56069
    48
    in (K (env, body), ctxt') end);
wenzelm@27340
    49
wenzelm@27340
    50
wenzelm@27340
    51
wenzelm@30231
    52
(** misc antiquotations **)
wenzelm@27340
    53
wenzelm@53171
    54
val _ = Theory.setup
wenzelm@56071
    55
 (ML_Context.antiquotation (Binding.name "here") (Scan.succeed ())
wenzelm@56071
    56
    (fn src => fn () => fn ctxt =>
wenzelm@56071
    57
      let
wenzelm@56071
    58
        val (a, ctxt') = variant "position" ctxt;
wenzelm@56071
    59
        val (_, pos) = Args.name_of_src src;
wenzelm@56071
    60
        val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n";
wenzelm@56071
    61
        val body = "Isabelle." ^ a;
wenzelm@56071
    62
      in (K (env, body), ctxt') end) #>
wenzelm@56071
    63
wenzelm@56071
    64
  inline (Binding.name "assert")
wenzelm@43560
    65
    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
wenzelm@40110
    66
wenzelm@43560
    67
  inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
wenzelm@36162
    68
wenzelm@51979
    69
  value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
wenzelm@51979
    70
    (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
wenzelm@51979
    71
     ML_Syntax.print_string name))) #>
wenzelm@51942
    72
wenzelm@43560
    73
  value (Binding.name "binding")
wenzelm@46961
    74
    (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
wenzelm@27340
    75
wenzelm@43560
    76
  value (Binding.name "theory")
wenzelm@55614
    77
    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
wenzelm@55614
    78
      (Context_Position.report ctxt pos
wenzelm@55614
    79
        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
wenzelm@55614
    80
       "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
wenzelm@48781
    81
    || Scan.succeed "Proof_Context.theory_of ML_context") #>
wenzelm@27340
    82
wenzelm@51686
    83
  value (Binding.name "theory_context")
wenzelm@55614
    84
    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
wenzelm@55614
    85
      (Context_Position.report ctxt pos
wenzelm@55614
    86
        (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
wenzelm@55614
    87
       "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
wenzelm@51686
    88
        ML_Syntax.print_string name))) #>
wenzelm@51686
    89
wenzelm@48781
    90
  inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
wenzelm@27340
    91
wenzelm@43560
    92
  inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
wenzelm@43560
    93
  inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
wenzelm@43560
    94
  inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
wenzelm@27340
    95
wenzelm@43560
    96
  value (Binding.name "ctyp") (Args.typ >> (fn T =>
wenzelm@48781
    97
    "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
wenzelm@48781
    98
      ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
wenzelm@27340
    99
wenzelm@43560
   100
  value (Binding.name "cterm") (Args.term >> (fn t =>
wenzelm@48781
   101
    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
wenzelm@48781
   102
     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
wenzelm@27340
   103
wenzelm@43560
   104
  value (Binding.name "cprop") (Args.prop >> (fn t =>
wenzelm@48781
   105
    "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
wenzelm@48781
   106
     ML_Syntax.atomic (ML_Syntax.print_term t))) #>
wenzelm@27340
   107
wenzelm@43560
   108
  value (Binding.name "cpat")
wenzelm@43560
   109
    (Args.context --
wenzelm@55111
   110
      Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
wenzelm@48781
   111
        "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
wenzelm@53171
   112
          ML_Syntax.atomic (ML_Syntax.print_term t))));
wenzelm@27340
   113
wenzelm@27340
   114
wenzelm@35396
   115
(* type classes *)
wenzelm@35396
   116
wenzelm@55111
   117
fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
wenzelm@42360
   118
  Proof_Context.read_class ctxt s
wenzelm@42290
   119
  |> syn ? Lexicon.mark_class
wenzelm@35396
   120
  |> ML_Syntax.print_string);
wenzelm@35396
   121
wenzelm@53171
   122
val _ = Theory.setup
wenzelm@43560
   123
 (inline (Binding.name "class") (class false) #>
wenzelm@43560
   124
  inline (Binding.name "class_syntax") (class true) #>
wenzelm@35396
   125
wenzelm@43560
   126
  inline (Binding.name "sort")
wenzelm@55111
   127
    (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
wenzelm@53171
   128
      ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
wenzelm@35396
   129
wenzelm@35396
   130
wenzelm@35361
   131
(* type constructors *)
wenzelm@27340
   132
wenzelm@55111
   133
fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
wenzelm@35401
   134
  >> (fn (ctxt, (s, pos)) =>
wenzelm@35401
   135
    let
wenzelm@56002
   136
      val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
wenzelm@42468
   137
      val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
wenzelm@35401
   138
      val res =
wenzelm@35401
   139
        (case try check (c, decl) of
wenzelm@35401
   140
          SOME res => res
wenzelm@48992
   141
        | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
wenzelm@35401
   142
    in ML_Syntax.print_string res end);
wenzelm@27340
   143
wenzelm@53171
   144
val _ = Theory.setup
wenzelm@43560
   145
 (inline (Binding.name "type_name")
wenzelm@43560
   146
    (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
wenzelm@43560
   147
  inline (Binding.name "type_abbrev")
wenzelm@43560
   148
    (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
wenzelm@43560
   149
  inline (Binding.name "nonterminal")
wenzelm@43560
   150
    (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
wenzelm@43560
   151
  inline (Binding.name "type_syntax")
wenzelm@53171
   152
    (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
wenzelm@35361
   153
wenzelm@35361
   154
wenzelm@35361
   155
(* constants *)
wenzelm@27340
   156
wenzelm@55111
   157
fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
wenzelm@35401
   158
  >> (fn (ctxt, (s, pos)) =>
wenzelm@35401
   159
    let
wenzelm@56002
   160
      val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
wenzelm@42360
   161
      val res = check (Proof_Context.consts_of ctxt, c)
wenzelm@48992
   162
        handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
wenzelm@35401
   163
    in ML_Syntax.print_string res end);
wenzelm@27340
   164
wenzelm@53171
   165
val _ = Theory.setup
wenzelm@43560
   166
 (inline (Binding.name "const_name")
wenzelm@43794
   167
    (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
wenzelm@43560
   168
  inline (Binding.name "const_abbrev")
wenzelm@43560
   169
    (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
wenzelm@43560
   170
  inline (Binding.name "const_syntax")
wenzelm@43560
   171
    (const_name (fn (_, c) => Lexicon.mark_const c)) #>
wenzelm@35401
   172
wenzelm@43560
   173
  inline (Binding.name "syntax_const")
wenzelm@43560
   174
    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
wenzelm@43560
   175
      if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
wenzelm@43560
   176
      then ML_Syntax.print_string c
wenzelm@48992
   177
      else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
wenzelm@27340
   178
wenzelm@43560
   179
  inline (Binding.name "const")
wenzelm@55111
   180
    (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
wenzelm@43560
   181
        (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
wenzelm@43560
   182
      >> (fn ((ctxt, raw_c), Ts) =>
wenzelm@43560
   183
        let
wenzelm@55954
   184
          val Const (c, _) =
wenzelm@56002
   185
            Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
wenzelm@46987
   186
          val consts = Proof_Context.consts_of ctxt;
wenzelm@46987
   187
          val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
wenzelm@46987
   188
          val _ = length Ts <> n andalso
wenzelm@46987
   189
            error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
wenzelm@46987
   190
              quote c ^ enclose "(" ")" (commas (replicate n "_")));
wenzelm@46987
   191
          val const = Const (c, Consts.instance consts (c, Ts));
wenzelm@53171
   192
        in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
wenzelm@27340
   193
wenzelm@46948
   194
wenzelm@46948
   195
(* outer syntax *)
wenzelm@46948
   196
wenzelm@46961
   197
fun with_keyword f =
wenzelm@46961
   198
  Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
wenzelm@48646
   199
    (f ((name, Thy_Header.the_keyword thy name), pos)
wenzelm@48992
   200
      handle ERROR msg => error (msg ^ Position.here pos)));
wenzelm@46961
   201
wenzelm@53171
   202
val _ = Theory.setup
wenzelm@46961
   203
 (value (Binding.name "keyword")
wenzelm@46961
   204
    (with_keyword
wenzelm@48646
   205
      (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
wenzelm@48646
   206
        | ((name, SOME _), pos) =>
wenzelm@48992
   207
            error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
wenzelm@46961
   208
  value (Binding.name "command_spec")
wenzelm@46961
   209
    (with_keyword
wenzelm@48646
   210
      (fn ((name, SOME kind), pos) =>
wenzelm@46961
   211
          "Keyword.command_spec " ^ ML_Syntax.atomic
wenzelm@48646
   212
            ((ML_Syntax.print_pair
wenzelm@46961
   213
              (ML_Syntax.print_pair ML_Syntax.print_string
wenzelm@48864
   214
                (ML_Syntax.print_pair
wenzelm@48864
   215
                  (ML_Syntax.print_pair ML_Syntax.print_string
wenzelm@48864
   216
                    (ML_Syntax.print_list ML_Syntax.print_string))
wenzelm@48646
   217
                  (ML_Syntax.print_list ML_Syntax.print_string)))
wenzelm@48646
   218
              ML_Syntax.print_position) ((name, kind), pos))
wenzelm@48646
   219
        | ((name, NONE), pos) =>
wenzelm@53171
   220
            error ("Expected command keyword " ^ quote name ^ Position.here pos))));
wenzelm@46948
   221
wenzelm@27340
   222
end;
wenzelm@27340
   223