21 "App _ _ = dummy_term" |
21 "App _ _ = dummy_term" |
22 |
22 |
23 code_datatype Const App |
23 code_datatype Const App |
24 |
24 |
25 class term_of = typerep + |
25 class term_of = typerep + |
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 {* |
31 ML {* |
65 |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) |
65 |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) |
66 |> snd |
66 |> snd |
67 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
67 |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |
68 |> LocalTheory.exit_global |
68 |> LocalTheory.exit_global |
69 end; |
69 end; |
70 fun interpretator (tyco, (raw_vs, _)) thy = |
70 fun interpretator ("prop", (raw_vs, _)) thy = thy |
71 let |
71 | interpretator (tyco, (raw_vs, _)) thy = |
72 val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
72 let |
73 val constrain_sort = |
73 val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; |
74 curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
74 val constrain_sort = |
75 val vs = (map o apsnd) constrain_sort raw_vs; |
75 curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
76 val ty = Type (tyco, map TFree vs); |
76 val vs = (map o apsnd) constrain_sort raw_vs; |
77 in |
77 val ty = Type (tyco, map TFree vs); |
78 thy |
78 in |
79 |> Typerep.perhaps_add_def tyco |
79 thy |
80 |> not has_inst ? add_term_of_def ty vs tyco |
80 |> Typerep.perhaps_add_def tyco |
81 end; |
81 |> not has_inst ? add_term_of_def ty vs tyco |
|
82 end; |
82 in |
83 in |
83 Code.type_interpretation interpretator |
84 Code.type_interpretation interpretator |
84 end |
85 end |
85 *} |
86 *} |
86 |
87 |
103 |> Thm.varifyT; |
104 |> Thm.varifyT; |
104 in |
105 in |
105 thy |
106 thy |
106 |> Code.add_eqn thm |
107 |> Code.add_eqn thm |
107 end; |
108 end; |
108 fun interpretator (tyco, (raw_vs, raw_cs)) thy = |
109 fun interpretator ("prop", (raw_vs, _)) thy = thy |
109 let |
110 | interpretator (tyco, (raw_vs, raw_cs)) thy = |
110 val constrain_sort = |
111 let |
111 curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
112 val constrain_sort = |
112 val vs = (map o apsnd) constrain_sort raw_vs; |
113 curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; |
113 val cs = (map o apsnd o map o map_atyps) |
114 val vs = (map o apsnd) constrain_sort raw_vs; |
114 (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs; |
115 val cs = (map o apsnd o map o map_atyps) |
115 val ty = Type (tyco, map TFree vs); |
116 (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs; |
116 val eqs = map (mk_term_of_eq ty vs tyco) cs; |
117 val ty = Type (tyco, map TFree vs); |
117 val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); |
118 val eqs = map (mk_term_of_eq ty vs tyco) cs; |
118 in |
119 val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); |
119 thy |
120 in |
120 |> Code.del_eqns const |
121 thy |
121 |> fold (prove_term_of_eq ty) eqs |
122 |> Code.del_eqns const |
122 end; |
123 |> fold (prove_term_of_eq ty) eqs |
|
124 end; |
123 in |
125 in |
124 Code.type_interpretation interpretator |
126 Code.type_interpretation interpretator |
125 end |
127 end |
126 *} |
128 *} |
127 |
129 |
144 in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char))) |
146 in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char))) |
145 (Code_Eval.term_of n)) (Code_Eval.term_of m))" |
147 (Code_Eval.term_of n)) (Code_Eval.term_of m))" |
146 by (subst term_of_anything) rule |
148 by (subst term_of_anything) rule |
147 |
149 |
148 code_type "term" |
150 code_type "term" |
149 (SML "Term.term") |
151 (Eval "Term.term") |
150 |
152 |
151 code_const Const and App |
153 code_const Const and App |
152 (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)") |
154 (Eval "Term.Const/ (_, _)" and "Term.$/ (_, _)") |
153 |
155 |
154 code_const "term_of \<Colon> message_string \<Rightarrow> term" |
156 code_const "term_of \<Colon> message_string \<Rightarrow> term" |
155 (SML "Message'_String.mk") |
157 (Eval "Message'_String.mk") |
156 |
158 |
157 |
159 |
158 subsection {* Evaluation setup *} |
160 subsection {* Evaluation setup *} |
159 |
161 |
160 ML {* |
162 ML {* |