equal
deleted
inserted
replaced
6 |
6 |
7 theory Reflection |
7 theory Reflection |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 ML_file "reify_data.ML" |
|
12 ML_file "reflection.ML" |
11 ML_file "reflection.ML" |
13 |
|
14 setup {* Reify_Data.setup *} |
|
15 |
12 |
16 method_setup reify = {* |
13 method_setup reify = {* |
17 Attrib.thms -- |
14 Attrib.thms -- |
18 Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >> |
15 Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >> |
19 (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ fst (Reify_Data.get ctxt)) to)) |
16 (fn (user_eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.default_reify_tac ctxt user_eqs to)) |
20 *} "partial automatic reification" |
17 *} "partial automatic reification" |
21 |
18 |
22 method_setup reflection = {* |
19 method_setup reflection = {* |
23 let |
20 let |
24 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
21 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
26 val rulesN = "rules"; |
23 val rulesN = "rules"; |
27 val any_keyword = keyword onlyN || keyword rulesN; |
24 val any_keyword = keyword onlyN || keyword rulesN; |
28 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
25 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
29 val terms = thms >> map (term_of o Drule.dest_term); |
26 val terms = thms >> map (term_of o Drule.dest_term); |
30 in |
27 in |
31 thms -- |
28 thms -- Scan.optional (keyword rulesN |-- thms) [] -- |
32 Scan.optional (keyword rulesN |-- thms) [] -- |
29 Scan.option (keyword onlyN |-- Args.term) >> |
33 Scan.option (keyword onlyN |-- Args.term) >> |
30 (fn ((user_eqs, user_thms), to) => fn ctxt => |
34 (fn ((eqs, ths), to) => fn ctxt => |
31 SIMPLE_METHOD' (Reflection.default_reflection_tac ctxt user_thms user_eqs to)) |
35 let |
|
36 val (ceqs, cths) = Reify_Data.get ctxt |
|
37 val corr_thms = ths @ cths |
|
38 val raw_eqs = eqs @ ceqs |
|
39 in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end) |
|
40 end |
32 end |
41 *} |
33 *} "partial automatic reflection" |
42 |
34 |
43 end |
35 end |
44 |
36 |