src/Pure/ML/ml_antiquote.ML
author wenzelm
Sun Mar 08 17:26:14 2009 +0100 (2009-03-08)
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 30513 1796b8ea88aa
permissions -rw-r--r--
moved basic algebra of long names from structure NameSpace to Long_Name;
     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 macro: string ->
    10     (Context.generic * Args.T list -> Proof.context * (Context.generic * Args.T list)) -> unit
    11   val variant: string -> Proof.context -> string * Proof.context
    12   val inline: string ->
    13     (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
    14   val declaration: string -> string ->
    15     (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
    16   val value: string ->
    17     (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
    18 end;
    19 
    20 structure ML_Antiquote: ML_ANTIQUOTE =
    21 struct
    22 
    23 (** generic tools **)
    24 
    25 (* ML names *)
    26 
    27 structure NamesData = ProofDataFun
    28 (
    29   type T = Name.context;
    30   fun init _ = ML_Syntax.reserved;
    31 );
    32 
    33 fun variant a ctxt =
    34   let
    35     val names = NamesData.get ctxt;
    36     val ([b], names') = Name.variants [a] names;
    37     val ctxt' = NamesData.put names' ctxt;
    38   in (b, ctxt') end;
    39 
    40 
    41 (* specific antiquotations *)
    42 
    43 fun macro name scan = ML_Context.add_antiq name
    44   (fn _ => scan :|-- (fn ctxt => Scan.depend (fn _ => Scan.succeed
    45     (Context.Proof ctxt, fn {background, ...} => (K ("", ""), background)))));
    46 
    47 fun inline name scan = ML_Context.add_antiq name
    48   (fn _ => scan >> (fn s => fn {struct_name, background} => (K ("", s), background)));
    49 
    50 fun declaration kind name scan = ML_Context.add_antiq name
    51   (fn _ => scan >> (fn s => fn {struct_name, background} =>
    52     let
    53       val (a, background') = variant name background;
    54       val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
    55       val body = struct_name ^ "." ^ a;
    56     in (K (env, body), background') end));
    57 
    58 val value = declaration "val";
    59 
    60 
    61 
    62 (** misc antiquotations **)
    63 
    64 structure P = OuterParse;
    65 
    66 val _ = inline "binding" (Scan.lift (P.position Args.name) >> (fn b =>
    67   ML_Syntax.atomic ("Binding.make " ^
    68     ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position b)));
    69 
    70 val _ = value "theory"
    71   (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
    72   || Scan.succeed "ML_Context.the_global_context ()");
    73 
    74 val _ = value "theory_ref"
    75   (Scan.lift Args.name >> (fn name =>
    76     "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")")
    77   || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
    78 
    79 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
    80 
    81 val _ = inline "sort" (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
    82   ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
    83 
    84 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
    85 val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
    86 val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
    87 
    88 val _ = macro "let" (Args.context --
    89   Scan.lift (P.and_list1 (P.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
    90     >> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
    91 
    92 val _ = macro "note" (Args.context :|-- (fn ctxt =>
    93   P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
    94     ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
    95   >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
    96 
    97 val _ = value "ctyp" (Args.typ >> (fn T =>
    98   "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
    99 
   100 val _ = value "cterm" (Args.term >> (fn t =>
   101   "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
   102 
   103 val _ = value "cprop" (Args.prop >> (fn t =>
   104   "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
   105 
   106 val _ = value "cpat"
   107   (Args.context -- Scan.lift Args.name_source >> uncurry ProofContext.read_term_pattern >> (fn t =>
   108     "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
   109 
   110 
   111 fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
   112     #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
   113     |> syn ? Long_Name.base_name
   114     |> ML_Syntax.print_string));
   115 
   116 val _ = inline "type_name" (type_ false);
   117 val _ = inline "type_syntax" (type_ true);
   118 
   119 
   120 fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
   121   #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
   122   |> syn ? ProofContext.const_syntax_name ctxt
   123   |> ML_Syntax.print_string);
   124 
   125 val _ = inline "const_name" (const false);
   126 val _ = inline "const_syntax" (const true);
   127 
   128 val _ = inline "const"
   129   (Args.context -- Scan.lift Args.name_source -- Scan.optional
   130       (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   131     >> (fn ((ctxt, c), Ts) =>
   132       let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
   133       in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
   134 
   135 end;
   136