--- a/src/HOL/Eisbach/eisbach_antiquotations.ML Wed Dec 23 14:40:18 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:40:18 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML Wed Dec 23 16:33:15 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 ->
@@ -39,8 +39,27 @@
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))));
structure Local_Data = Proof_Data
@@ -84,7 +103,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
@@ -96,42 +114,6 @@
in text end));
-fun parse_term_args args =
- Args.context :|-- (fn ctxt =>
- let
- val ctxt' = Proof_Context.set_mode (Proof_Context.mode_schematic) ctxt;
-
- fun parse T =
- (if T = propT then Syntax.parse_prop ctxt' else Syntax.parse_term ctxt')
- #> Type.constraint (Type_Infer.paramify_vars T);
-
- fun do_parse' T =
- Parse_Tools.name_term >> Parse_Tools.parse_val_cases (parse T);
-
- fun do_parse (Var (_, T)) = do_parse' T
- | do_parse (Free (_, T)) = do_parse' T
- | do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt' t);
-
- fun rep [] x = Scan.succeed [] x
- | rep (t :: ts) x = (do_parse t ::: rep ts) x;
-
- fun check ts =
- let
- val (ts, fs) = split_list ts;
- val ts' = Syntax.check_terms ctxt' ts |> Variable.polymorphic ctxt';
- val _ = ListPair.app (fn (f, t) => f t) (fs, ts');
- in ts' end;
- in Scan.lift (rep args) >> check end);
-
-fun match_term_args ctxt args ts =
- let
- val match_types = Sign.typ_match (Proof_Context.theory_of ctxt) o apply2 Term.fastype_of;
- val tyenv = fold match_types (args ~~ ts) Vartab.empty;
- val tenv =
- fold (fn ((xi, T), t) => Vartab.update_new (xi, (T, t)))
- (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;
@@ -189,53 +171,47 @@
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 parse_term_args args =
+ Args.context :|-- (fn ctxt =>
+ let
+ val ctxt' = Proof_Context.set_mode (Proof_Context.mode_schematic) ctxt;
+
+ fun parse T =
+ (if T = propT then Syntax.parse_prop ctxt' else Syntax.parse_term ctxt')
+ #> Type.constraint (Type_Infer.paramify_vars T);
+
+ fun do_parse' T =
+ Parse_Tools.name_term >> Parse_Tools.parse_val_cases (parse T);
+
+ fun do_parse (Var (_, T)) = do_parse' T
+ | do_parse (Free (_, T)) = do_parse' T
+ | do_parse t = error ("Unexpected method parameter: " ^ Syntax.string_of_term ctxt' t);
+
+ fun rep [] x = Scan.succeed [] x
+ | rep (t :: ts) x = (do_parse t ::: rep ts) x;
+
+ fun check ts =
+ let
+ val (ts, fs) = split_list ts;
+ val ts' = Syntax.check_terms ctxt' ts |> Variable.polymorphic ctxt';
+ val _ = ListPair.app (fn (f, t) => f t) (fs, ts');
+ in ts' end;
+ in Scan.lift (rep args) >> check end);
+
+fun match_term_args ctxt args ts =
+ let
+ val match_types = Sign.typ_match (Proof_Context.theory_of ctxt) o apply2 Term.fastype_of;
+ val tyenv = fold match_types (args ~~ ts) Vartab.empty;
+ val tenv =
+ fold (fn ((xi, T), t) => Vartab.update_new (xi, (T, t)))
+ (map Term.dest_Var args ~~ ts) Vartab.empty;
+ in Envir.Envir {maxidx = ~1, tenv = tenv, tyenv = tyenv} end;
+
fun gen_method add_fixes name vars uses declares methods source lthy =
let
val (uses_internal, lthy1) = lthy
@@ -309,4 +285,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;