1(* Title: Pure/ML/ml_context.ML 2 Author: Makarius 3 4ML context and antiquotations. 5*) 6 7signature ML_CONTEXT = 8sig 9 val check_antiquotation: Proof.context -> xstring * Position.T -> string 10 val struct_name: Proof.context -> string 11 val variant: string -> Proof.context -> string * Proof.context 12 type decl = Proof.context -> string * string 13 val value_decl: string -> string -> Proof.context -> decl * Proof.context 14 val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) -> 15 theory -> theory 16 val print_antiquotations: bool -> Proof.context -> unit 17 val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit 18 val eval_file: ML_Compiler.flags -> Path.T -> unit 19 val eval_source: ML_Compiler.flags -> Input.source -> unit 20 val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T -> 21 ML_Lex.token Antiquote.antiquote list -> unit 22 val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit 23 val exec: (unit -> unit) -> Context.generic -> Context.generic 24 val expression: Position.range -> string -> string -> string -> 25 ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic 26end 27 28structure ML_Context: ML_CONTEXT = 29struct 30 31(** ML antiquotations **) 32 33(* names for generated environment *) 34 35structure Names = Proof_Data 36( 37 type T = string * Name.context; 38 val init_names = ML_Syntax.reserved |> Name.declare "ML_context"; 39 fun init _ = ("Isabelle0", init_names); 40); 41 42fun struct_name ctxt = #1 (Names.get ctxt); 43val struct_begin = (Names.map o apfst) (fn _ => "Isabelle" ^ serial_string ()); 44 45fun variant a ctxt = 46 let 47 val names = #2 (Names.get ctxt); 48 val (b, names') = Name.variant (Name.desymbolize (SOME false) a) names; 49 val ctxt' = (Names.map o apsnd) (K names') ctxt; 50 in (b, ctxt') end; 51 52 53(* decl *) 54 55type decl = Proof.context -> string * string; (*final context -> ML env, ML body*) 56 57fun value_decl a s ctxt = 58 let 59 val (b, ctxt') = variant a ctxt; 60 val env = "val " ^ b ^ " = " ^ s ^ ";\n"; 61 val body = struct_name ctxt ^ "." ^ b; 62 fun decl (_: Proof.context) = (env, body); 63 in (decl, ctxt') end; 64 65 66(* theory data *) 67 68structure Antiquotations = Theory_Data 69( 70 type T = (Token.src -> Proof.context -> decl * Proof.context) Name_Space.table; 71 val empty : T = Name_Space.empty_table Markup.ML_antiquotationN; 72 val extend = I; 73 fun merge data : T = Name_Space.merge_tables data; 74); 75 76val get_antiquotations = Antiquotations.get o Proof_Context.theory_of; 77 78fun check_antiquotation ctxt = 79 #1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt); 80 81fun add_antiquotation name f thy = thy 82 |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd); 83 84fun print_antiquotations verbose ctxt = 85 Pretty.big_list "ML antiquotations:" 86 (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_antiquotations ctxt))) 87 |> Pretty.writeln; 88 89fun apply_antiquotation src ctxt = 90 let val (src', f) = Token.check_src ctxt get_antiquotations src 91 in f src' ctxt end; 92 93 94(* parsing and evaluation *) 95 96local 97 98val antiq = 99 Parse.!!! ((Parse.token Parse.liberal_name ::: Parse.args) --| Scan.ahead Parse.eof); 100 101fun make_env name visible = 102 (ML_Lex.tokenize 103 ("structure " ^ name ^ " =\nstruct\n\ 104 \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^ 105 " (Context.the_local_context ());\n"), 106 ML_Lex.tokenize "end;"); 107 108fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end"); 109 110fun eval_antiquotes (ants, pos) opt_context = 111 let 112 val visible = 113 (case opt_context of 114 SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt 115 | _ => true); 116 val opt_ctxt = Option.map Context.proof_of opt_context; 117 118 val ((ml_env, ml_body), opt_ctxt') = 119 if forall (fn Antiquote.Text _ => true | _ => false) ants 120 then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt) 121 else 122 let 123 fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range)); 124 125 fun expand_src range src ctxt = 126 let val (decl, ctxt') = apply_antiquotation src ctxt 127 in (decl #> tokenize range, ctxt') end; 128 129 fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt) 130 | expand (Antiquote.Control {name, range, body}) ctxt = 131 expand_src range 132 (Token.make_src name (if null body then [] else [Token.read_cartouche body])) ctxt 133 | expand (Antiquote.Antiq {range, body, ...}) ctxt = 134 expand_src range 135 (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)) ctxt; 136 137 val ctxt = 138 (case opt_ctxt of 139 NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos) 140 | SOME ctxt => struct_begin ctxt); 141 142 val (begin_env, end_env) = make_env (struct_name ctxt) visible; 143 val (decls, ctxt') = fold_map expand ants ctxt; 144 val (ml_env, ml_body) = 145 decls |> map (fn decl => decl ctxt') |> split_list |> apply2 flat; 146 in ((begin_env @ ml_env @ end_env, ml_body), SOME ctxt') end; 147 in ((ml_env, ml_body), opt_ctxt') end; 148 149in 150 151fun eval flags pos ants = 152 let 153 val non_verbose = ML_Compiler.verbose false flags; 154 155 (*prepare source text*) 156 val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.get_generic_context ()); 157 val _ = 158 (case env_ctxt of 159 SOME ctxt => 160 if Config.get ctxt ML_Options.source_trace andalso Context_Position.is_visible ctxt 161 then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body]) 162 else () 163 | NONE => ()); 164 165 (*prepare environment*) 166 val _ = 167 Context.setmp_generic_context 168 (Option.map (Context.Proof o Context_Position.set_visible false) env_ctxt) 169 (fn () => 170 (ML_Compiler.eval non_verbose Position.none env; Context.get_generic_context ())) () 171 |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context')); 172 173 (*eval body*) 174 val _ = ML_Compiler.eval flags pos body; 175 176 (*clear environment*) 177 val _ = 178 (case (env_ctxt, is_some (Context.get_generic_context ())) of 179 (SOME ctxt, true) => 180 let 181 val name = struct_name ctxt; 182 val _ = ML_Compiler.eval non_verbose Position.none (reset_env name); 183 val _ = Context.>> (ML_Env.forget_structure name); 184 in () end 185 | _ => ()); 186 in () end; 187 188end; 189 190 191(* derived versions *) 192 193fun eval_file flags path = 194 let val pos = Path.position path 195 in eval flags pos (ML_Lex.read_pos pos (File.read path)) end; 196 197fun eval_source flags source = 198 eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source); 199 200fun eval_in ctxt flags pos ants = 201 Context.setmp_generic_context (Option.map Context.Proof ctxt) 202 (fn () => eval flags pos ants) (); 203 204fun eval_source_in ctxt flags source = 205 Context.setmp_generic_context (Option.map Context.Proof ctxt) 206 (fn () => eval_source flags source) (); 207 208fun exec (e: unit -> unit) context = 209 (case Context.setmp_generic_context (SOME context) 210 (fn () => (e (); Context.get_generic_context ())) () of 211 SOME context' => context' 212 | NONE => error "Missing context after execution"); 213 214fun expression range name constraint body ants = 215 exec (fn () => 216 eval ML_Compiler.flags (#1 range) 217 (ML_Lex.read "Context.put_generic_context (SOME (let val " @ ML_Lex.read_set_range range name @ 218 ML_Lex.read (": " ^ constraint ^ " =") @ ants @ 219 ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));"))); 220 221end; 222 223val ML = ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags); 224