118 val _ = if ! trace |
118 val _ = if ! trace |
119 then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t)) |
119 then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t)) |
120 else () |
120 else () |
121 fun evaluator naming program ((_, vs_ty), t) deps = |
121 fun evaluator naming program ((_, vs_ty), t) deps = |
122 base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args; |
122 base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args; |
123 in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end; |
123 in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end; |
124 |
124 |
125 fun dynamic_value_strict cookie thy some_target postproc t args = |
125 fun dynamic_value_strict cookie thy some_target postproc t args = |
126 Exn.release (dynamic_value_exn cookie thy some_target postproc t args); |
126 Exn.release (dynamic_value_exn cookie thy some_target postproc t args); |
127 |
127 |
128 fun dynamic_value cookie thy some_target postproc t args = |
128 fun dynamic_value cookie thy some_target postproc t args = |
131 fun static_value_exn cookie thy some_target postproc consts = |
131 fun static_value_exn cookie thy some_target postproc consts = |
132 let |
132 let |
133 val serializer = obtain_serializer thy some_target; |
133 val serializer = obtain_serializer thy some_target; |
134 fun evaluator naming program thy ((_, vs_ty), t) deps = |
134 fun evaluator naming program thy ((_, vs_ty), t) deps = |
135 base_evaluator cookie serializer naming thy program (vs_ty, t) deps []; |
135 base_evaluator cookie serializer naming thy program (vs_ty, t) deps []; |
136 in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end; |
136 in Code_Thingol.static_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end; |
137 |
137 |
138 fun static_value_strict cookie thy some_target postproc consts t = |
138 fun static_value_strict cookie thy some_target postproc consts t = |
139 Exn.release (static_value_exn cookie thy some_target postproc consts t); |
139 Exn.release (static_value_exn cookie thy some_target postproc consts t); |
140 |
140 |
141 fun static_value cookie thy some_target postproc consts t = |
141 fun static_value cookie thy some_target postproc consts t = |
173 fn (serializer, naming, thy, program, vs_t, deps, ct) => check_holds serializer naming thy program vs_t deps ct))); |
173 fn (serializer, naming, thy, program, vs_t, deps, ct) => check_holds serializer naming thy program vs_t deps ct))); |
174 |
174 |
175 fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct = |
175 fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct = |
176 raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct); |
176 raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct); |
177 |
177 |
178 val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy |
178 val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy |
179 (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy) |
179 (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy) |
180 o reject_vars thy); |
180 o reject_vars thy); |
181 |
181 |
182 fun static_holds_conv thy consts = |
182 fun static_holds_conv thy consts = |
183 let |
183 let |
184 val serializer = obtain_serializer thy NONE; |
184 val serializer = obtain_serializer thy NONE; |
185 in |
185 in |
186 Code_Thingol.static_eval_conv thy consts |
186 Code_Thingol.static_conv thy consts |
187 (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program) |
187 (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program) |
188 o reject_vars thy |
188 o reject_vars thy |
189 end; |
189 end; |
190 |
190 |
191 |
191 |