--- a/src/HOL/Eisbach/Eisbach.thy Wed Dec 23 14:36:45 2015 +0100
+++ b/src/HOL/Eisbach/Eisbach.thy Wed Dec 23 16:43:31 2015 +0100
@@ -19,7 +19,6 @@
ML_file "method_closure.ML"
ML_file "eisbach_rule_insts.ML"
ML_file "match_method.ML"
-ML_file "eisbach_antiquotations.ML"
method solves methods m = (m; fail)
--- a/src/HOL/Eisbach/eisbach_antiquotations.ML Wed Dec 23 14:36:45 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-(* Title: HOL/Eisbach/eisbach_antiquotations.ML
- Author: Daniel Matichuk, NICTA/UNSW
-
-ML antiquotations for Eisbach.
-*)
-
-structure Eisbach_Antiquotations: sig end =
-struct
-
-(** evaluate Eisbach method from ML **)
-
-val _ =
- Theory.setup
- (ML_Antiquotation.inline @{binding method} (* FIXME ML_Antiquotation.value (!?) *)
- (Args.context -- Scan.lift (Args.mode "drop_cases") -- Scan.lift (Parse.position Parse.name)
- >> (fn ((ctxt, drop_cases), nameref) =>
- let
- val ((targs, (factargs, margs)), _) = Method_Closure.get_method ctxt nameref;
-
- val has_factargs = not (null factargs);
-
- val (targnms, ctxt') =
- fold_map (fn (Var ((x, _), _)) => ML_Context.variant x) targs ctxt;
- val (margnms, ctxt'') = fold_map ML_Context.variant margs ctxt';
- val (factsnm, _) = ML_Context.variant "facts" ctxt'';
-
- val fn_header =
- margnms
- |> has_factargs ? append [factsnm]
- |> append targnms
- |> map (fn nm => "fn " ^ nm ^ " => ")
- |> implode;
-
- val ML_context = ML_Context.struct_name ctxt ^ ".ML_context";
- val ml_inner =
- ML_Syntax.atomic
- ("Method_Closure.get_method " ^ ML_context ^
- ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position nameref ^
- "|> (fn ((targs, (_, margs)), text) => Method_Closure.eval_method " ^
- ML_context ^ " ((targs, margs), text))");
-
- val drop_cases_suffix =
- if drop_cases then "#> (fn f => (fn ctxt => fn thms => f ctxt thms |> Seq.map snd))"
- else "";
-
- val factsnm = if has_factargs then factsnm else "[]";
- in
- ML_Syntax.atomic
- (fn_header ^ ml_inner ^ " " ^ ML_Syntax.print_list I targnms ^ " " ^
- factsnm ^ " " ^
- ML_Syntax.print_list I margnms ^ drop_cases_suffix)
- end)));
-
-end;
--- a/src/HOL/Eisbach/method_closure.ML Wed Dec 23 14:36:45 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML Wed Dec 23 16:43:31 2015 +0100
@@ -10,16 +10,16 @@
signature METHOD_CLOSURE =
sig
+ val get_method: Proof.context -> string * Position.T ->
+ (term list * (string list * string list)) * Method.text
+ val eval_method: Proof.context -> (term list * string list) * Method.text ->
+ term list -> (string * thm list) list -> (Proof.context -> Method.method) list ->
+ Proof.context -> Method.method
val read: Proof.context -> Token.src -> Method.text
val read_closure: Proof.context -> Token.src -> Method.text * Token.src
val read_closure_input: Proof.context -> Input.source -> Method.text * Token.src
val method_text: Method.text context_parser
val method_evaluate: Method.text -> Proof.context -> Method.method
- val get_method: Proof.context -> string * Position.T ->
- (term list * (string list * string list)) * Method.text
- val eval_method: Proof.context -> (term list * string list) * Method.text ->
- term list -> (string * thm list) list -> (Proof.context -> Method.method) list ->
- Proof.context -> Method.method
val method: binding -> (binding * typ option * mixfix) list -> binding list ->
binding list -> binding list -> Token.src -> local_theory -> string * local_theory
val method_cmd: binding -> (binding * string option * mixfix) list -> binding list ->
@@ -29,7 +29,7 @@
structure Method_Closure: METHOD_CLOSURE =
struct
-(* context data *)
+(* context data for ML antiquotation *)
structure Data = Generic_Data
(
@@ -39,9 +39,30 @@
fun merge data : T = Symtab.merge (K true) data;
);
-val get_methods = Data.get o Context.Proof;
-val map_methods = Data.map;
+fun get_method ctxt (xname, pos) =
+ let
+ val name = Method.check_name ctxt (xname, pos);
+ in
+ (case Symtab.lookup (Data.get (Context.Proof ctxt)) name of
+ SOME entry => entry
+ | NONE => error ("Unknown Eisbach method: " ^ quote name ^ Position.here pos))
+ end;
+(* FIXME redundant!? -- base name of binding is not changed by usual morphisms*)
+fun Morphism_name phi name =
+ Morphism.binding phi (Binding.make (name, Position.none)) |> Binding.name_of;
+
+fun add_method binding ((fixes, declares, methods), text) lthy =
+ lthy |>
+ Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+ Data.map
+ (Symtab.update (Local_Theory.full_name lthy binding,
+ (((map (Morphism.term phi) fixes),
+ (map (Morphism_name phi) declares, map (Morphism_name phi) methods)),
+ (Method.map_source o map) (Token.transform phi) text))));
+
+
+(* context data for method definition *)
structure Local_Data = Proof_Data
(
@@ -65,16 +86,12 @@
(* read method text *)
fun read ctxt src =
- let
- val parser =
- Parse.!!! (Method.parser 0 --| Scan.ahead Parse.eof)
- >> apfst (Method.check_text ctxt);
- in
- (case Scan.read Token.stopper parser src of
- SOME (text, range) => (Method.report (text, range); text)
- | NONE =>
- error ("Failed to parse method" ^ Position.here (Position.set_range (Token.range_of src))))
- end;
+ (case Scan.read Token.stopper (Parse.!!! (Method.parser 0 --| Scan.ahead Parse.eof)) src of
+ SOME (text, range) =>
+ if Method.checked_text text then text
+ else (Method.report (text, range); Method.check_text ctxt text)
+ | NONE =>
+ error ("Failed to parse method" ^ Position.here (Position.set_range (Token.range_of src))));
fun read_closure ctxt src0 =
let
@@ -88,7 +105,6 @@
Token.read_no_commands (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof) #>
read_closure ctxt;
-
val method_text =
Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
(case Token.get_value tok of
@@ -100,6 +116,57 @@
in text end));
+(* evaluate method text *)
+
+fun method_evaluate text ctxt =
+ let
+ val text' =
+ text |> (Method.map_source o map o Token.map_facts)
+ (fn SOME name =>
+ (case Proof_Context.lookup_fact ctxt name of
+ SOME (false, ths) => K ths
+ | _ => I)
+ | NONE => I);
+ val ctxt' = Config.put Method.closure false ctxt;
+ in fn facts => Method.RUNTIME (fn st => Method.evaluate text' ctxt' facts st) end;
+
+fun method_instantiate env text =
+ let
+ val morphism = Morphism.term_morphism "method_instantiate" (Envir.norm_term env);
+ val text' = (Method.map_source o map) (Token.transform morphism) text;
+ in method_evaluate text' end;
+
+
+
+(** Isar command **)
+
+local
+
+fun setup_local_method binding lthy =
+ let
+ val full_name = Local_Theory.full_name lthy binding;
+ fun get_method ctxt = lookup_dynamic_method ctxt full_name ctxt;
+ in
+ lthy
+ |> update_dynamic_method (full_name, K Method.fail)
+ |> Method.local_setup binding (Scan.succeed get_method) "(internal)"
+ end;
+
+fun check_attrib ctxt attrib =
+ let
+ val name = Binding.name_of attrib;
+ val pos = Binding.pos_of attrib;
+ val named_thm = Named_Theorems.check ctxt (name, pos);
+ val parser: Method.modifier parser =
+ Args.$$$ name -- Args.colon >>
+ K {init = I, attribute = Named_Theorems.add named_thm, pos = pos};
+ in (named_thm, parser) end;
+
+fun dummy_named_thm named_thm =
+ Context.proof_map
+ (Named_Theorems.clear named_thm
+ #> Named_Theorems.add_thm named_thm Drule.free_dummy_thm);
+
fun parse_term_args args =
Args.context :|-- (fn ctxt =>
let
@@ -136,50 +203,6 @@
(map Term.dest_Var args ~~ ts) Vartab.empty;
in Envir.Envir {maxidx = ~1, tenv = tenv, tyenv = tyenv} end;
-fun check_attrib ctxt attrib =
- let
- val name = Binding.name_of attrib;
- val pos = Binding.pos_of attrib;
- val named_thm = Named_Theorems.check ctxt (name, pos);
- val parser: Method.modifier parser =
- Args.$$$ name -- Args.colon >>
- K {init = I, attribute = Named_Theorems.add named_thm, pos = pos};
- in (named_thm, parser) end;
-
-
-fun method_evaluate text ctxt =
- let
- val text' =
- text |> (Method.map_source o map o Token.map_facts)
- (fn SOME name =>
- (case Proof_Context.lookup_fact ctxt name of
- SOME (false, ths) => K ths
- | _ => I)
- | NONE => I);
- val ctxt' = Config.put Method.closure false ctxt;
- in fn facts => Method.RUNTIME (fn st => Method.evaluate text' ctxt' facts st) end;
-
-fun method_instantiate env text =
- let
- val morphism = Morphism.term_morphism "method_instantiate" (Envir.norm_term env);
- val text' = (Method.map_source o map) (Token.transform morphism) text;
- in method_evaluate text' end;
-
-fun setup_local_method binding lthy =
- let
- val full_name = Local_Theory.full_name lthy binding;
- fun get_method ctxt = lookup_dynamic_method ctxt full_name ctxt;
- in
- lthy
- |> update_dynamic_method (full_name, K Method.fail)
- |> Method.local_setup binding (Scan.succeed get_method) "(internal)"
- end;
-
-fun dummy_named_thm named_thm =
- Context.proof_map
- (Named_Theorems.clear named_thm
- #> Named_Theorems.add_thm named_thm Drule.free_dummy_thm);
-
fun parse_method_args method_names =
let
fun bind_method (name, text) ctxt =
@@ -192,54 +215,6 @@
| rep (t :: ts) x = ((method_text >> pair t) ::: rep ts) x;
in rep method_names >> fold bind_method end;
-
-(* FIXME redundant!? -- base name of binding is not changed by usual morphisms*)
-fun Morphism_name phi name =
- Morphism.binding phi (Binding.make (name, Position.none)) |> Binding.name_of;
-
-fun add_method binding ((fixes, declares, methods), text) lthy =
- lthy |>
- Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
- map_methods
- (Symtab.update (Local_Theory.full_name lthy binding,
- (((map (Morphism.term phi) fixes),
- (map (Morphism_name phi) declares, map (Morphism_name phi) methods)),
- (Method.map_source o map) (Token.transform phi) text))));
-
-fun get_method ctxt (xname, pos) =
- let
- val name = Method.check_name ctxt (xname, pos);
- in
- (case Symtab.lookup (get_methods ctxt) name of
- SOME entry => entry
- | NONE => error ("Unknown Eisbach method: " ^ quote name ^ Position.here pos))
- end;
-
-fun eval_method ctxt0 header fixes attribs methods =
- let
- val ((term_args, hmethods), text) = header;
-
- fun match fixes = (* FIXME proper context!? *)
- (case Seq.pull (Unify.matchers (Context.Proof ctxt0) (term_args ~~ fixes)) of
- SOME (env, _) => env
- | NONE => error "Couldn't match term arguments");
-
- fun add_thms (name, thms) =
- fold (Context.proof_map o Named_Theorems.add_thm name) thms;
-
- val setup_ctxt = fold add_thms attribs
- #> fold update_dynamic_method (hmethods ~~ methods)
- #> put_recursive_method (fn xs => method_instantiate (match xs) text);
- in
- fn ctxt => method_instantiate (match fixes) text (setup_ctxt ctxt)
- end;
-
-
-
-(** Isar command **)
-
-local
-
fun gen_method add_fixes name vars uses declares methods source lthy =
let
val (uses_internal, lthy1) = lthy
@@ -313,4 +288,69 @@
(fn ((((name, vars), (methods, uses)), declares), src) =>
#2 o method_cmd name vars uses declares methods src));
+
+
+(** ML antiquotation **)
+
+fun eval_method ctxt0 header fixes attribs methods =
+ let
+ val ((term_args, hmethods), text) = header;
+
+ fun match fixes = (* FIXME proper context!? *)
+ (case Seq.pull (Unify.matchers (Context.Proof ctxt0) (term_args ~~ fixes)) of
+ SOME (env, _) => env
+ | NONE => error "Couldn't match term arguments");
+
+ fun add_thms (name, thms) =
+ fold (Context.proof_map o Named_Theorems.add_thm name) thms;
+
+ val setup_ctxt = fold add_thms attribs
+ #> fold update_dynamic_method (hmethods ~~ methods)
+ #> put_recursive_method (fn xs => method_instantiate (match xs) text);
+ in
+ fn ctxt => method_instantiate (match fixes) text (setup_ctxt ctxt)
+ end;
+
+val _ =
+ Theory.setup
+ (ML_Antiquotation.inline @{binding method} (* FIXME ML_Antiquotation.value (!?) *)
+ (Args.context -- Scan.lift (Args.mode "drop_cases") -- Scan.lift (Parse.position Parse.name)
+ >> (fn ((ctxt, drop_cases), nameref) =>
+ let
+ val ((targs, (factargs, margs)), _) = get_method ctxt nameref;
+
+ val has_factargs = not (null factargs);
+
+ val (targnms, ctxt') =
+ fold_map (fn (Var ((x, _), _)) => ML_Context.variant x) targs ctxt;
+ val (margnms, ctxt'') = fold_map ML_Context.variant margs ctxt';
+ val (factsnm, _) = ML_Context.variant "facts" ctxt'';
+
+ val fn_header =
+ margnms
+ |> has_factargs ? append [factsnm]
+ |> append targnms
+ |> map (fn nm => "fn " ^ nm ^ " => ")
+ |> implode;
+
+ val ML_context = ML_Context.struct_name ctxt ^ ".ML_context";
+ val ml_inner =
+ ML_Syntax.atomic
+ ("Method_Closure.get_method " ^ ML_context ^
+ ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position nameref ^
+ "|> (fn ((targs, (_, margs)), text) => Method_Closure.eval_method " ^
+ ML_context ^ " ((targs, margs), text))");
+
+ val drop_cases_suffix =
+ if drop_cases then "#> (fn f => (fn ctxt => fn thms => f ctxt thms |> Seq.map snd))"
+ else "";
+
+ val factsnm = if has_factargs then factsnm else "[]";
+ in
+ ML_Syntax.atomic
+ (fn_header ^ ml_inner ^ " " ^ ML_Syntax.print_list I targnms ^ " " ^
+ factsnm ^ " " ^
+ ML_Syntax.print_list I margnms ^ drop_cases_suffix)
+ end)));
+
end;
--- a/src/Pure/Isar/method.ML Wed Dec 23 14:36:45 2015 +0100
+++ b/src/Pure/Isar/method.ML Wed Dec 23 16:43:31 2015 +0100
@@ -73,6 +73,7 @@
val check_name: Proof.context -> xstring * Position.T -> string
val check_src: Proof.context -> Token.src -> Token.src
val check_text: Proof.context -> text -> text
+ val checked_text: text -> bool
val method_syntax: (Proof.context -> method) context_parser ->
Token.src -> Proof.context -> method
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
@@ -439,6 +440,10 @@
| check_text _ (Basic m) = Basic m
| check_text ctxt (Combinator (x, y, body)) = Combinator (x, y, map (check_text ctxt) body);
+fun checked_text (Source src) = Token.checked_src src
+ | checked_text (Basic _) = true
+ | checked_text (Combinator (_, _, body)) = forall checked_text body;
+
(* method setup *)