1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/ML/ml_antiquote.ML Tue Jun 24 19:43:16 2008 +0200
1.3 @@ -0,0 +1,154 @@
1.4 +(* Title: Pure/ML/ml_antiquote.ML
1.5 + ID: $Id$
1.6 + Author: Makarius
1.7 +
1.8 +Common ML antiquotations.
1.9 +*)
1.10 +
1.11 +signature ML_ANTIQUOTE =
1.12 +sig
1.13 + val variant: string -> Proof.context -> string * Proof.context
1.14 + val inline: string ->
1.15 + (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
1.16 + val declaration: string -> string ->
1.17 + (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
1.18 + val value: string ->
1.19 + (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
1.20 + val the_thms: Proof.context -> int -> thm list
1.21 + val the_thm: Proof.context -> int -> thm
1.22 +end;
1.23 +
1.24 +structure ML_Antiquote: ML_ANTIQUOTE =
1.25 +struct
1.26 +
1.27 +(** generic tools **)
1.28 +
1.29 +(* ML names *)
1.30 +
1.31 +structure NamesData = ProofDataFun
1.32 +(
1.33 + type T = Name.context;
1.34 + fun init _ = ML_Syntax.reserved;
1.35 +);
1.36 +
1.37 +fun variant a ctxt =
1.38 + let
1.39 + val names = NamesData.get ctxt;
1.40 + val ([b], names') = Name.variants [a] names;
1.41 + val ctxt' = NamesData.put names' ctxt;
1.42 + in (b, ctxt') end;
1.43 +
1.44 +
1.45 +(* specific antiquotations *)
1.46 +
1.47 +fun inline name scan = ML_Context.add_antiq name
1.48 + (scan >> (fn s => fn {struct_name, background} => ((K ("", s)), background)));
1.49 +
1.50 +fun declaration kind name scan = ML_Context.add_antiq name
1.51 + (scan >> (fn s => fn {struct_name, background} =>
1.52 + let
1.53 + val (a, background') = variant name background;
1.54 + val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
1.55 + val body = struct_name ^ "." ^ a;
1.56 + in (K (env, body), background') end));
1.57 +
1.58 +val value = declaration "val";
1.59 +
1.60 +
1.61 +
1.62 +(** concrete antiquotations **)
1.63 +
1.64 +fun context x = (Scan.state >> Context.proof_of) x;
1.65 +
1.66 +
1.67 +(* misc *)
1.68 +
1.69 +val _ = value "theory"
1.70 + (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
1.71 + || Scan.succeed "ML_Context.the_global_context ()");
1.72 +
1.73 +val _ = value "theory_ref"
1.74 + (Scan.lift Args.name >> (fn name =>
1.75 + "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")")
1.76 + || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
1.77 +
1.78 +val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
1.79 +
1.80 +val _ = inline "sort" (context -- Scan.lift Args.name >> (fn (ctxt, s) =>
1.81 + ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))));
1.82 +
1.83 +val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
1.84 +val _ = inline "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
1.85 +val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
1.86 +
1.87 +val _ = value "ctyp" (Args.typ >> (fn T =>
1.88 + "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
1.89 +
1.90 +val _ = value "cterm" (Args.term >> (fn t =>
1.91 + "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
1.92 +
1.93 +val _ = value "cprop" (Args.prop >> (fn t =>
1.94 + "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
1.95 +
1.96 +val _ = value "cpat"
1.97 + (context -- Scan.lift Args.name >> uncurry ProofContext.read_term_pattern >> (fn t =>
1.98 + "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t)));
1.99 +
1.100 +
1.101 +fun type_ syn = (context -- Scan.lift Args.name >> (fn (ctxt, c) =>
1.102 + #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
1.103 + |> syn ? Sign.base_name
1.104 + |> ML_Syntax.print_string));
1.105 +
1.106 +val _ = inline "type_name" (type_ false);
1.107 +val _ = inline "type_syntax" (type_ true);
1.108 +
1.109 +
1.110 +fun const syn = context -- Scan.lift Args.name >> (fn (ctxt, c) =>
1.111 + #1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
1.112 + |> syn ? ProofContext.const_syntax_name ctxt
1.113 + |> ML_Syntax.print_string);
1.114 +
1.115 +val _ = inline "const_name" (const false);
1.116 +val _ = inline "const_syntax" (const true);
1.117 +
1.118 +val _ = inline "const"
1.119 + (context -- Scan.lift Args.name --
1.120 + Scan.optional (Scan.lift (Args.$$$ "(") |-- Args.enum1 "," Args.typ --| Scan.lift (Args.$$$ ")")) []
1.121 + >> (fn ((ctxt, c), Ts) =>
1.122 + let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
1.123 + in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
1.124 +
1.125 +
1.126 +(* abstract fact values *)
1.127 +
1.128 +val _ = ML_Context.add_keywords ["[", "]", "(", ")", "-", ","]; (* FIXME !? *)
1.129 +
1.130 +structure AuxFacts = ProofDataFun
1.131 +(
1.132 + type T = thm list Inttab.table;
1.133 + fun init _ = Inttab.empty;
1.134 +);
1.135 +
1.136 +fun the_thms ctxt name = the (Inttab.lookup (AuxFacts.get ctxt) name);
1.137 +fun the_thm ctxt name = the_single (the_thms ctxt name);
1.138 +
1.139 +fun put_thms ths ctxt =
1.140 + let val i = serial ()
1.141 + in (i, AuxFacts.map (Inttab.update (i, ths)) ctxt) end;
1.142 +
1.143 +
1.144 +fun thm_antiq kind scan = ML_Context.add_antiq kind
1.145 + (scan >> (fn ths => fn {struct_name, background} =>
1.146 + let
1.147 + val ((a, i), background') = background |> variant kind ||>> put_thms ths;
1.148 + val env = "val " ^ a ^ " = ML_Antiquote.the_" ^ kind ^
1.149 + " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";
1.150 + val body = struct_name ^ "." ^ a;
1.151 + in (K (env, body), background') end));
1.152 +
1.153 +val _ = thm_antiq "thm" (Attrib.thm >> single);
1.154 +val _ = thm_antiq "thms" Attrib.thms;
1.155 +
1.156 +end;
1.157 +