15 -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option |
15 -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option |
16 val dynamic_value_strict: 'a cookie -> Proof.context -> string option |
16 val dynamic_value_strict: 'a cookie -> Proof.context -> string option |
17 -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a |
17 -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a |
18 val dynamic_value_exn: 'a cookie -> Proof.context -> string option |
18 val dynamic_value_exn: 'a cookie -> Proof.context -> string option |
19 -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result |
19 -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result |
20 val static_value: 'a cookie -> { ctxt: Proof.context, target: string option, |
|
21 lift_postproc: (term -> term) -> 'a -> 'a, consts: string list } |
|
22 -> Proof.context -> term -> 'a option |
|
23 val static_value_strict: 'a cookie -> { ctxt: Proof.context, target: string option, |
|
24 lift_postproc: (term -> term) -> 'a -> 'a, consts: string list } |
|
25 -> Proof.context -> term -> 'a |
|
26 val static_value_exn: 'a cookie -> { ctxt: Proof.context, target: string option, |
|
27 lift_postproc: (term -> term) -> 'a -> 'a, consts: string list } |
|
28 -> Proof.context -> term -> 'a Exn.result |
|
29 val dynamic_holds_conv: Proof.context -> conv |
20 val dynamic_holds_conv: Proof.context -> conv |
30 val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv |
|
31 val code_reflect: (string * string list option) list -> string list -> string |
21 val code_reflect: (string * string list option) list -> string list -> string |
32 -> string option -> theory -> theory |
22 -> string option -> theory -> theory |
33 datatype truth = Holds |
23 datatype truth = Holds |
34 val put_truth: (unit -> truth) -> Proof.context -> Proof.context |
24 val put_truth: (unit -> truth) -> Proof.context -> Proof.context |
35 val mount_computation: Proof.context -> (string * typ) list -> typ |
25 val mount_computation: Proof.context -> (string * typ) list -> typ |
128 Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args); |
118 Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args); |
129 |
119 |
130 fun dynamic_value cookie ctxt some_target postproc t args = |
120 fun dynamic_value cookie ctxt some_target postproc t args = |
131 partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args); |
121 partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args); |
132 |
122 |
133 fun static_value_exn cookie { ctxt, target, lift_postproc, consts } = |
|
134 let |
|
135 fun compilation' { program, deps } = |
|
136 let |
|
137 val compilation'' = run_compilation_text cookie ctxt |
|
138 (build_compilation_text ctxt target program (map Constant deps)); |
|
139 in fn _ => fn _ => fn vs_ty_t => fn _ => compilation'' vs_ty_t [] end; |
|
140 val compilation = Code_Thingol.static_value { ctxt = ctxt, |
|
141 lift_postproc = Exn.map_res o lift_postproc, consts = consts } |
|
142 compilation'; |
|
143 in fn ctxt' => compilation ctxt' o reject_vars ctxt' end; |
|
144 |
|
145 fun static_value_strict cookie x = Exn.release oo static_value_exn cookie x; |
|
146 |
|
147 fun static_value cookie x = partiality_as_none oo static_value_exn cookie x; |
|
148 |
|
149 |
123 |
150 (* evaluation for truth or nothing *) |
124 (* evaluation for truth or nothing *) |
151 |
125 |
152 structure Truth_Result = Proof_Data |
126 structure Truth_Result = Proof_Data |
153 ( |
127 ( |
187 |
161 |
188 fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt |
162 fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt |
189 (fn program => fn vs_t => fn deps => |
163 (fn program => fn vs_t => fn deps => |
190 check_holds_oracle ctxt (build_compilation_text ctxt NONE program deps) vs_t) |
164 check_holds_oracle ctxt (build_compilation_text ctxt NONE program deps) vs_t) |
191 o reject_vars ctxt; |
165 o reject_vars ctxt; |
192 |
|
193 fun static_holds_conv (ctxt_consts as { ctxt, ... }) = |
|
194 Code_Thingol.static_conv_thingol ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t => |
|
195 K (check_holds_oracle ctxt' (build_compilation_text ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt')); |
|
196 |
166 |
197 end; (*local*) |
167 end; (*local*) |
198 |
168 |
199 |
169 |
200 (** generator for computations -- partial implementations of the universal morphism from Isabelle to ML terms **) |
170 (** generator for computations -- partial implementations of the universal morphism from Isabelle to ML terms **) |