108 |
108 |
109 code_reserved SML Fail |
109 code_reserved SML Fail |
110 code_reserved Haskell error |
110 code_reserved Haskell error |
111 |
111 |
112 |
112 |
113 subsection {* normalization by evaluation *} |
113 subsection {* Evaluation oracle *} |
|
114 |
|
115 ML {* |
|
116 signature HOL_EVAL = |
|
117 sig |
|
118 val eval_ref: bool option ref |
|
119 val oracle: string * (theory * exn -> term) |
|
120 val tac: int -> tactic |
|
121 val method: Method.src -> Proof.context -> Method.method |
|
122 end; |
|
123 |
|
124 structure HOLEval : HOL_EVAL = |
|
125 struct |
|
126 |
|
127 val eval_ref : bool option ref = ref NONE; |
|
128 |
|
129 fun eval_prop thy t = |
|
130 CodegenPackage.eval_term |
|
131 thy (("HOLEval.eval_ref", eval_ref), t); |
|
132 |
|
133 exception Eval of term; |
|
134 |
|
135 val oracle = ("Eval", fn (thy, Eval t) => |
|
136 Logic.mk_equals (t, if eval_prop thy t then HOLogic.true_const else HOLogic.false_const)); |
|
137 |
|
138 val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle]; |
|
139 |
|
140 fun conv ct = |
|
141 let |
|
142 val {thy, t, ...} = rep_cterm ct; |
|
143 in Thm.invoke_oracle_i thy oracle_name (thy, Eval t) end; |
|
144 |
|
145 fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule |
|
146 (Drule.goals_conv (equal i) (HOL.Trueprop_conv conv))); |
|
147 |
|
148 val method = |
|
149 Method.no_args (Method.METHOD (fn _ => |
|
150 tac 1 THEN rtac TrueI 1)); |
|
151 |
|
152 end; |
|
153 *} |
|
154 |
|
155 setup {* |
|
156 Theory.add_oracle HOLEval.oracle |
|
157 #> Method.add_method ("eval", HOLEval.method, "solve goal by evaluation") |
|
158 *} |
|
159 |
|
160 |
|
161 subsection {* Normalization by evaluation *} |
114 |
162 |
115 setup {* |
163 setup {* |
116 let |
164 let |
117 fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule |
165 fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule |
118 (Drule.goals_conv (equal i) (HOL.Trueprop_conv |
166 (Drule.goals_conv (equal i) (HOL.Trueprop_conv |