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