src/Pure/ML/ml_antiquote.ML
author wenzelm
Thu Mar 06 13:44:01 2014 +0100 (2014-03-06)
changeset 55954 a29aefc88c8d
parent 55951 c07d184aebe9
child 55955 e8f1bf005661
permissions -rw-r--r--
more uniform check_const/read_const;
     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.add_antiq name
    41     (Scan.depend (fn context => Scan.pass context scan >> (fn s => (context, K ("", s)))));
    42 
    43 fun value name scan =
    44   ML_Context.add_antiq name
    45     (Scan.depend (fn context => Scan.pass context scan >> (fn s =>
    46       let
    47         val ctxt = Context.the_proof context;
    48         val (a, ctxt') = variant (Binding.name_of name) ctxt;
    49         val env = "val " ^ a ^ " = " ^ s ^ ";\n";
    50         val body = "Isabelle." ^ a;
    51       in (Context.Proof ctxt', (K (env, body))) end)));
    52 
    53 
    54 
    55 (** misc antiquotations **)
    56 
    57 val _ = Theory.setup
    58  (inline (Binding.name "assert")
    59     (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
    60 
    61   inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
    62 
    63   value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
    64     (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
    65      ML_Syntax.print_string name))) #>
    66 
    67   value (Binding.name "binding")
    68     (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
    69 
    70   value (Binding.name "theory")
    71     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    72       (Context_Position.report ctxt pos
    73         (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
    74        "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
    75     || Scan.succeed "Proof_Context.theory_of ML_context") #>
    76 
    77   value (Binding.name "theory_context")
    78     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    79       (Context_Position.report ctxt pos
    80         (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
    81        "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
    82         ML_Syntax.print_string name))) #>
    83 
    84   inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
    85 
    86   inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
    87   inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    88   inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    89 
    90   value (Binding.name "ctyp") (Args.typ >> (fn T =>
    91     "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^
    92       ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
    93 
    94   value (Binding.name "cterm") (Args.term >> (fn t =>
    95     "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
    96      ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    97 
    98   value (Binding.name "cprop") (Args.prop >> (fn t =>
    99     "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   100      ML_Syntax.atomic (ML_Syntax.print_term t))) #>
   101 
   102   value (Binding.name "cpat")
   103     (Args.context --
   104       Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
   105         "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
   106           ML_Syntax.atomic (ML_Syntax.print_term t))));
   107 
   108 
   109 (* type classes *)
   110 
   111 fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
   112   Proof_Context.read_class ctxt s
   113   |> syn ? Lexicon.mark_class
   114   |> ML_Syntax.print_string);
   115 
   116 val _ = Theory.setup
   117  (inline (Binding.name "class") (class false) #>
   118   inline (Binding.name "class_syntax") (class true) #>
   119 
   120   inline (Binding.name "sort")
   121     (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
   122       ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
   123 
   124 
   125 (* type constructors *)
   126 
   127 fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   128   >> (fn (ctxt, (s, pos)) =>
   129     let
   130       val Type (c, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s;
   131       val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
   132       val res =
   133         (case try check (c, decl) of
   134           SOME res => res
   135         | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
   136     in ML_Syntax.print_string res end);
   137 
   138 val _ = Theory.setup
   139  (inline (Binding.name "type_name")
   140     (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
   141   inline (Binding.name "type_abbrev")
   142     (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
   143   inline (Binding.name "nonterminal")
   144     (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
   145   inline (Binding.name "type_syntax")
   146     (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
   147 
   148 
   149 (* constants *)
   150 
   151 fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
   152   >> (fn (ctxt, (s, pos)) =>
   153     let
   154       val Const (c, _) = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT s;
   155       val res = check (Proof_Context.consts_of ctxt, c)
   156         handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   157     in ML_Syntax.print_string res end);
   158 
   159 val _ = Theory.setup
   160  (inline (Binding.name "const_name")
   161     (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
   162   inline (Binding.name "const_abbrev")
   163     (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
   164   inline (Binding.name "const_syntax")
   165     (const_name (fn (_, c) => Lexicon.mark_const c)) #>
   166 
   167   inline (Binding.name "syntax_const")
   168     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
   169       if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
   170       then ML_Syntax.print_string c
   171       else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
   172 
   173   inline (Binding.name "const")
   174     (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
   175         (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   176       >> (fn ((ctxt, raw_c), Ts) =>
   177         let
   178           val Const (c, _) =
   179             Proof_Context.read_const ctxt {proper = true, strict = true} dummyT 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), pos)
   194       handle ERROR msg => error (msg ^ Position.here pos)));
   195 
   196 val _ = Theory.setup
   197  (value (Binding.name "keyword")
   198     (with_keyword
   199       (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name
   200         | ((name, SOME _), pos) =>
   201             error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #>
   202   value (Binding.name "command_spec")
   203     (with_keyword
   204       (fn ((name, SOME kind), pos) =>
   205           "Keyword.command_spec " ^ ML_Syntax.atomic
   206             ((ML_Syntax.print_pair
   207               (ML_Syntax.print_pair ML_Syntax.print_string
   208                 (ML_Syntax.print_pair
   209                   (ML_Syntax.print_pair ML_Syntax.print_string
   210                     (ML_Syntax.print_list ML_Syntax.print_string))
   211                   (ML_Syntax.print_list ML_Syntax.print_string)))
   212               ML_Syntax.print_position) ((name, kind), pos))
   213         | ((name, NONE), pos) =>
   214             error ("Expected command keyword " ^ quote name ^ Position.here pos))));
   215 
   216 end;
   217