26 fixes term_of :: "'a \<Rightarrow> term" |
26 fixes term_of :: "'a \<Rightarrow> term" |
27 |
27 |
28 lemma term_of_anything: "term_of x \<equiv> t" |
28 lemma term_of_anything: "term_of x \<equiv> t" |
29 by (rule eq_reflection) (cases "term_of x", cases t, simp) |
29 by (rule eq_reflection) (cases "term_of x", cases t, simp) |
30 |
30 |
31 ML {* |
|
32 structure Eval = |
|
33 struct |
|
34 |
|
35 fun mk_term f g (Const (c, ty)) = |
|
36 @{term Const} $ HOLogic.mk_message_string c $ g ty |
|
37 | mk_term f g (t1 $ t2) = |
|
38 @{term App} $ mk_term f g t1 $ mk_term f g t2 |
|
39 | mk_term f g (Free v) = f v |
|
40 | mk_term f g (Bound i) = Bound i |
|
41 | mk_term f g (Abs (v, _, t)) = Abs (v, @{typ term}, mk_term f g t); |
|
42 |
|
43 fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t; |
|
44 |
|
45 end; |
|
46 *} |
|
47 |
|
48 |
31 |
49 subsubsection {* @{text term_of} instances *} |
32 subsubsection {* @{text term_of} instances *} |
50 |
33 |
51 setup {* |
34 setup {* |
52 let |
35 let |
53 fun add_term_of_def ty vs tyco thy = |
36 fun add_term_of tyco raw_vs thy = |
54 let |
37 let |
|
38 val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; |
|
39 val ty = Type (tyco, map TFree vs); |
55 val lhs = Const (@{const_name term_of}, ty --> @{typ term}) |
40 val lhs = Const (@{const_name term_of}, ty --> @{typ term}) |
56 $ Free ("x", ty); |
41 $ Free ("x", ty); |
57 val rhs = @{term "undefined \<Colon> term"}; |
42 val rhs = @{term "undefined \<Colon> term"}; |
58 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
43 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
59 fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst |
44 fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst |
62 thy |
47 thy |
63 |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of}) |
48 |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of}) |
64 |> `(fn lthy => Syntax.check_term lthy eq) |
49 |> `(fn lthy => Syntax.check_term lthy eq) |
65 |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) |
50 |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) |
66 |> snd |
51 |> snd |
67 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
52 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
68 |> LocalTheory.exit_global |
|
69 end; |
53 end; |
70 fun interpretator ("prop", (raw_vs, _)) thy = thy |
54 fun ensure_term_of (tyco, (raw_vs, _)) thy = |
71 | interpretator (tyco, (raw_vs, _)) thy = |
55 let |
72 let |
56 val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}) |
73 val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
57 andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}; |
74 val constrain_sort = |
58 in |
75 curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
59 thy |
76 val vs = (map o apsnd) constrain_sort raw_vs; |
60 |> need_inst ? add_term_of tyco raw_vs |
77 val ty = Type (tyco, map TFree vs); |
61 end; |
78 in |
|
79 thy |
|
80 |> Typerep.perhaps_add_def tyco |
|
81 |> not has_inst ? add_term_of_def ty vs tyco |
|
82 end; |
|
83 in |
62 in |
84 Code.type_interpretation interpretator |
63 Code.type_interpretation ensure_term_of |
85 end |
64 end |
86 *} |
65 *} |
87 |
66 |
88 setup {* |
67 setup {* |
89 let |
68 let |
90 fun mk_term_of_eq ty vs tyco (c, tys) = |
69 fun mk_term_of_eq thy ty vs tyco (c, tys) = |
91 let |
70 let |
92 val t = list_comb (Const (c, tys ---> ty), |
71 val t = list_comb (Const (c, tys ---> ty), |
93 map Free (Name.names Name.context "a" tys)); |
72 map Free (Name.names Name.context "a" tys)); |
94 in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term |
73 val (arg, rhs) = pairself (Thm.cterm_of thy o map_types Logic.unvarifyT o Logic.varify) |
95 (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty))) |
74 (t, (map_aterms (fn t as Free (v, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t) |
96 (Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort)))) t) |
75 handle TYPE (msg, tys, ts) => (tracing msg; error "") |
|
76 val cty = Thm.ctyp_of thy ty; |
|
77 val _ = tracing (cat_lines [makestring arg, makestring rhs, makestring cty]) |
|
78 in |
|
79 @{thm term_of_anything} |
|
80 |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] |
|
81 |> Thm.varifyT |
97 end; |
82 end; |
98 fun prove_term_of_eq ty eq thy = |
83 fun add_term_of_code tyco raw_vs raw_cs thy = |
99 let |
84 let |
100 val cty = Thm.ctyp_of thy ty; |
85 val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; |
101 val (arg, rhs) = pairself (Thm.cterm_of thy) eq; |
86 val ty = Type (tyco, map TFree vs); |
102 val thm = @{thm term_of_anything} |
87 val cs = (map o apsnd o map o map_atyps) |
103 |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] |
88 (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; |
104 |> Thm.varifyT; |
89 val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); |
|
90 val eqs = map (mk_term_of_eq thy ty vs tyco) cs; |
|
91 in |
|
92 thy |
|
93 |> Code.del_eqns const |
|
94 |> fold Code.add_eqn eqs |
|
95 end; |
|
96 fun ensure_term_of_code (tyco, (raw_vs, cs)) thy = |
|
97 let |
|
98 val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
105 in |
99 in |
106 thy |
100 thy |
107 |> Code.add_eqn thm |
101 |> has_inst ? add_term_of_code tyco raw_vs cs |
108 end; |
102 end; |
109 fun interpretator ("prop", (raw_vs, _)) thy = thy |
|
110 | interpretator (tyco, (raw_vs, raw_cs)) thy = |
|
111 let |
|
112 val constrain_sort = |
|
113 curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
|
114 val vs = (map o apsnd) constrain_sort raw_vs; |
|
115 val cs = (map o apsnd o map o map_atyps) |
|
116 (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs; |
|
117 val ty = Type (tyco, map TFree vs); |
|
118 val eqs = map (mk_term_of_eq ty vs tyco) cs; |
|
119 val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); |
|
120 in |
|
121 thy |
|
122 |> Code.del_eqns const |
|
123 |> fold (prove_term_of_eq ty) eqs |
|
124 end; |
|
125 in |
103 in |
126 Code.type_interpretation interpretator |
104 Code.type_interpretation ensure_term_of_code |
127 end |
105 end |
128 *} |
106 *} |
129 |
107 |
130 |
108 |
131 subsubsection {* Code generator setup *} |
109 subsubsection {* Code generator setup *} |