src/Pure/ML/ml_antiquotations.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 64594 4719f13989df
child 67146 909dcdec2122
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Pure/ML/ml_antiquotations.ML
     2     Author:     Makarius
     3 
     4 Miscellaneous ML antiquotations.
     5 *)
     6 
     7 structure ML_Antiquotations: sig end =
     8 struct
     9 
    10 (* ML support *)
    11 
    12 val _ = Theory.setup
    13  (ML_Antiquotation.inline @{binding undefined}
    14     (Scan.succeed "(raise General.Match)") #>
    15 
    16   ML_Antiquotation.inline @{binding assert}
    17     (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
    18 
    19   ML_Antiquotation.declaration @{binding print}
    20     (Scan.lift (Scan.optional Args.embedded "Output.writeln"))
    21       (fn src => fn output => fn ctxt =>
    22         let
    23           val struct_name = ML_Context.struct_name ctxt;
    24           val (_, pos) = Token.name_of_src src;
    25           val (a, ctxt') = ML_Context.variant "output" ctxt;
    26           val env =
    27             "val " ^ a ^ ": string -> unit =\n\
    28             \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
    29             ML_Syntax.print_position pos ^ "));\n";
    30           val body =
    31             "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))";
    32         in (K (env, body), ctxt') end) #>
    33 
    34   ML_Antiquotation.value @{binding rat}
    35     (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat --
    36       Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) =>
    37         "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))))
    38 
    39 
    40 (* formal entities *)
    41 
    42 val _ = Theory.setup
    43  (ML_Antiquotation.value @{binding system_option}
    44     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    45       let
    46         val markup =
    47           Options.default_markup (name, pos) handle ERROR msg =>
    48             let
    49               val completion =
    50                 Completion.make (name, pos) (fn completed =>
    51                     Options.names (Options.default ())
    52                     |> filter completed
    53                     |> map (fn a => (a, ("system_option", a))));
    54               val report = Markup.markup_report (Completion.reported_text completion);
    55             in error (msg ^ report) end;
    56         val _ = Context_Position.report ctxt pos markup;
    57       in ML_Syntax.print_string name end)) #>
    58 
    59   ML_Antiquotation.value @{binding theory}
    60     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    61       (Theory.check ctxt (name, pos);
    62        "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
    63     || Scan.succeed "Proof_Context.theory_of ML_context") #>
    64 
    65   ML_Antiquotation.value @{binding theory_context}
    66     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    67       (Theory.check ctxt (name, pos);
    68        "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
    69         ML_Syntax.print_string name))) #>
    70 
    71   ML_Antiquotation.inline @{binding context}
    72     (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #>
    73 
    74   ML_Antiquotation.inline @{binding typ} (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
    75   ML_Antiquotation.inline @{binding term} (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    76   ML_Antiquotation.inline @{binding prop} (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
    77 
    78   ML_Antiquotation.value @{binding ctyp} (Args.typ >> (fn T =>
    79     "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
    80 
    81   ML_Antiquotation.value @{binding cterm} (Args.term >> (fn t =>
    82     "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    83 
    84   ML_Antiquotation.value @{binding cprop} (Args.prop >> (fn t =>
    85     "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
    86 
    87   ML_Antiquotation.inline @{binding method}
    88     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    89       ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
    90 
    91 
    92 (* locales *)
    93 
    94 val _ = Theory.setup
    95  (ML_Antiquotation.inline @{binding locale}
    96    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
    97       Locale.check (Proof_Context.theory_of ctxt) (name, pos)
    98       |> ML_Syntax.print_string)));
    99 
   100 
   101 (* type classes *)
   102 
   103 fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
   104   Proof_Context.read_class ctxt s
   105   |> syn ? Lexicon.mark_class
   106   |> ML_Syntax.print_string);
   107 
   108 val _ = Theory.setup
   109  (ML_Antiquotation.inline @{binding class} (class false) #>
   110   ML_Antiquotation.inline @{binding class_syntax} (class true) #>
   111 
   112   ML_Antiquotation.inline @{binding sort}
   113     (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
   114       ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
   115 
   116 
   117 (* type constructors *)
   118 
   119 fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
   120   >> (fn (ctxt, (s, pos)) =>
   121     let
   122       val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
   123       val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
   124       val res =
   125         (case try check (c, decl) of
   126           SOME res => res
   127         | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos));
   128     in ML_Syntax.print_string res end);
   129 
   130 val _ = Theory.setup
   131  (ML_Antiquotation.inline @{binding type_name}
   132     (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
   133   ML_Antiquotation.inline @{binding type_abbrev}
   134     (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
   135   ML_Antiquotation.inline @{binding nonterminal}
   136     (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
   137   ML_Antiquotation.inline @{binding type_syntax}
   138     (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
   139 
   140 
   141 (* constants *)
   142 
   143 fun const_name check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
   144   >> (fn (ctxt, (s, pos)) =>
   145     let
   146       val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
   147       val res = check (Proof_Context.consts_of ctxt, c)
   148         handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
   149     in ML_Syntax.print_string res end);
   150 
   151 val _ = Theory.setup
   152  (ML_Antiquotation.inline @{binding const_name}
   153     (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
   154   ML_Antiquotation.inline @{binding const_abbrev}
   155     (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
   156   ML_Antiquotation.inline @{binding const_syntax}
   157     (const_name (fn (_, c) => Lexicon.mark_const c)) #>
   158 
   159   ML_Antiquotation.inline @{binding syntax_const}
   160     (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (c, pos)) =>
   161       if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
   162       then ML_Syntax.print_string c
   163       else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
   164 
   165   ML_Antiquotation.inline @{binding const}
   166     (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional
   167         (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
   168       >> (fn ((ctxt, (raw_c, pos)), Ts) =>
   169         let
   170           val Const (c, _) =
   171             Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
   172           val consts = Proof_Context.consts_of ctxt;
   173           val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
   174           val _ = length Ts <> n andalso
   175             error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
   176               quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos);
   177           val const = Const (c, Consts.instance consts (c, Ts));
   178         in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
   179 
   180 
   181 (* basic combinators *)
   182 
   183 local
   184 
   185 val parameter = Parse.position Parse.nat >> (fn (n, pos) =>
   186   if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos));
   187 
   188 fun indices n = map string_of_int (1 upto n);
   189 
   190 fun empty n = replicate_string n " []";
   191 fun dummy n = replicate_string n " _";
   192 fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n));
   193 fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n));
   194 
   195 val tuple = enclose "(" ")" o commas;
   196 fun tuple_empty n = tuple (replicate n "[]");
   197 fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n));
   198 fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)"
   199 fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n));
   200 
   201 in
   202 
   203 val _ = Theory.setup
   204  (ML_Antiquotation.value @{binding map}
   205     (Scan.lift parameter >> (fn n =>
   206       "fn f =>\n\
   207       \  let\n\
   208       \    fun map _" ^ empty n ^ " = []\n\
   209       \      | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\
   210       \      | map _" ^  dummy n ^ " = raise ListPair.UnequalLengths\n" ^
   211       "  in map f end")) #>
   212   ML_Antiquotation.value @{binding fold}
   213     (Scan.lift parameter >> (fn n =>
   214       "fn f =>\n\
   215       \  let\n\
   216       \    fun fold _" ^ empty n ^ " a = a\n\
   217       \      | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\
   218       \      | fold _" ^  dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
   219       "  in fold f end")) #>
   220   ML_Antiquotation.value @{binding fold_map}
   221     (Scan.lift parameter >> (fn n =>
   222       "fn f =>\n\
   223       \  let\n\
   224       \    fun fold_map _" ^ empty n ^ " a = ([], a)\n\
   225       \      | fold_map f" ^ cons n ^ " a =\n\
   226       \          let\n\
   227       \            val (x, a') = f" ^ vars "x" n ^ " a\n\
   228       \            val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\
   229       \          in (x :: xs, a'') end\n\
   230       \      | fold_map _" ^  dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
   231       "  in fold_map f end")) #>
   232   ML_Antiquotation.value @{binding split_list}
   233     (Scan.lift parameter >> (fn n =>
   234       "fn list =>\n\
   235       \  let\n\
   236       \    fun split_list [] =" ^ tuple_empty n ^ "\n\
   237       \      | split_list" ^ tuple_cons n ^ " =\n\
   238       \          let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\
   239       \          in " ^ cons_tuple n ^ "end\n\
   240       \  in split_list list end")) #>
   241   ML_Antiquotation.value @{binding apply}
   242     (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >>
   243       (fn (n, opt_index) =>
   244         let
   245           val cond =
   246             (case opt_index of
   247               NONE => K true
   248             | SOME (index, index_pos) =>
   249                 if 1 <= index andalso index <= n then equal (string_of_int index)
   250                 else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos));
   251         in
   252           "fn f => fn " ^ tuple_vars "x" n ^ " => " ^
   253             tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n))
   254         end)));
   255 
   256 end;
   257 
   258 
   259 (* outer syntax *)
   260 
   261 val _ = Theory.setup
   262  (ML_Antiquotation.value @{binding keyword}
   263     (Args.context -- Scan.lift (Parse.position (Parse.name || Parse.keyword_with (K true)))
   264       >> (fn (ctxt, (name, pos)) =>
   265         if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then
   266           (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
   267            "Parse.$$$ " ^ ML_Syntax.print_string name)
   268         else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
   269   ML_Antiquotation.value @{binding command_keyword}
   270     (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
   271       (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
   272         SOME markup =>
   273          (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)];
   274           ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos))
   275       | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos)))));
   276 
   277 end;