equal
deleted
inserted
replaced
58 |
58 |
59 (* evaluation into target language values *) |
59 (* evaluation into target language values *) |
60 |
60 |
61 type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string; |
61 type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string; |
62 |
62 |
|
63 fun reject_vars thy t = |
|
64 let |
|
65 val ctxt = ProofContext.init_global thy; |
|
66 in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end; |
|
67 |
63 fun obtain_serializer thy some_target = Code_Target.produce_code_for thy |
68 fun obtain_serializer thy some_target = Code_Target.produce_code_for thy |
64 (the_default target some_target) NONE "Code" []; |
69 (the_default target some_target) NONE "Code" []; |
65 |
70 |
66 fun base_evaluator cookie serializer (naming : Code_Thingol.naming) thy program ((vs, ty), t) deps args = |
71 fun base_evaluator cookie serializer (naming : Code_Thingol.naming) thy program ((vs, ty), t) deps args = |
67 let |
72 let |
86 | General.Bind => NONE |
91 | General.Bind => NONE |
87 | General.Fail _ => NONE; |
92 | General.Fail _ => NONE; |
88 |
93 |
89 fun dynamic_value_exn cookie thy some_target postproc t args = |
94 fun dynamic_value_exn cookie thy some_target postproc t args = |
90 let |
95 let |
|
96 val _ = reject_vars thy t; |
91 fun evaluator naming program ((_, vs_ty), t) deps = |
97 fun evaluator naming program ((_, vs_ty), t) deps = |
92 base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args; |
98 base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args; |
93 in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end; |
99 in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end; |
94 |
100 |
95 fun dynamic_value_strict cookie thy some_target postproc t args = |
101 fun dynamic_value_strict cookie thy some_target postproc t args = |
101 fun static_value_exn cookie thy some_target postproc consts = |
107 fun static_value_exn cookie thy some_target postproc consts = |
102 let |
108 let |
103 val serializer = obtain_serializer thy some_target; |
109 val serializer = obtain_serializer thy some_target; |
104 fun evaluator naming program thy ((_, vs_ty), t) deps = |
110 fun evaluator naming program thy ((_, vs_ty), t) deps = |
105 base_evaluator cookie serializer naming thy program (vs_ty, t) deps []; |
111 base_evaluator cookie serializer naming thy program (vs_ty, t) deps []; |
106 in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end; |
112 in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end; |
107 |
113 |
108 fun static_value_strict cookie thy some_target postproc consts t = |
114 fun static_value_strict cookie thy some_target postproc consts t = |
109 Exn.release (static_value_exn cookie thy some_target postproc consts t); |
115 Exn.release (static_value_exn cookie thy some_target postproc consts t); |
110 |
116 |
111 fun static_value cookie thy some_target postproc consts t = |
117 fun static_value cookie thy some_target postproc consts t = |
118 type T = unit -> truth |
124 type T = unit -> truth |
119 fun init _ () = error "Truth_Result" |
125 fun init _ () = error "Truth_Result" |
120 ); |
126 ); |
121 val put_truth = Truth_Result.put; |
127 val put_truth = Truth_Result.put; |
122 val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth"); |
128 val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth"); |
|
129 |
|
130 val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of); |
123 |
131 |
124 fun check_holds serializer naming thy program vs_t deps ct = |
132 fun check_holds serializer naming thy program vs_t deps ct = |
125 let |
133 let |
126 val t = Thm.term_of ct; |
134 val t = Thm.term_of ct; |
127 val _ = if fastype_of t <> propT |
135 val _ = if fastype_of t <> propT |
141 |
149 |
142 fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct = |
150 fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct = |
143 raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct); |
151 raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct); |
144 |
152 |
145 val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy |
153 val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy |
146 (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)); |
154 (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy) |
|
155 o reject_vars thy); |
147 |
156 |
148 fun static_holds_conv thy consts = |
157 fun static_holds_conv thy consts = |
149 let |
158 let |
150 val serializer = obtain_serializer thy NONE; |
159 val serializer = obtain_serializer thy NONE; |
151 in |
160 in |
152 Code_Thingol.static_eval_conv thy consts |
161 Code_Thingol.static_eval_conv thy consts |
153 (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program) |
162 (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program) |
|
163 o reject_vars thy |
154 end; |
164 end; |
155 |
165 |
156 |
166 |
157 (** instrumentalization **) |
167 (** instrumentalization **) |
158 |
168 |