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