55 |
55 |
56 (* evaluation into target language values *) |
56 (* evaluation into target language values *) |
57 |
57 |
58 type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string; |
58 type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string; |
59 |
59 |
60 fun base_evaluator cookie thy some_target naming program ((_, (vs, ty)), t) deps args = |
60 fun base_evaluator cookie thy some_target naming program ((vs, ty), t) deps args = |
61 let |
61 let |
62 val ctxt = ProofContext.init_global thy; |
62 val ctxt = ProofContext.init_global thy; |
63 val _ = if Code_Thingol.contains_dictvar t then |
63 val _ = if Code_Thingol.contains_dictvar t then |
64 error "Term to be evaluated contains free dictionaries" else (); |
64 error "Term to be evaluated contains free dictionaries" else (); |
65 val v' = Name.variant (map fst vs) "a"; |
65 val v' = Name.variant (map fst vs) "a"; |
81 | General.Bind => NONE |
81 | General.Bind => NONE |
82 | General.Fail _ => NONE; |
82 | General.Fail _ => NONE; |
83 |
83 |
84 fun dynamic_value_exn cookie thy some_target postproc t args = |
84 fun dynamic_value_exn cookie thy some_target postproc t args = |
85 let |
85 let |
86 fun evaluator naming program expr deps = |
86 fun evaluator naming program ((_, vs_ty), t) deps = |
87 base_evaluator cookie thy some_target naming program expr deps args; |
87 base_evaluator cookie thy some_target naming program (vs_ty, t) deps args; |
88 in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end; |
88 in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end; |
89 |
89 |
90 fun dynamic_value_strict cookie thy some_target postproc t args = |
90 fun dynamic_value_strict cookie thy some_target postproc t args = |
91 Exn.release (dynamic_value_exn cookie thy some_target postproc t args); |
91 Exn.release (dynamic_value_exn cookie thy some_target postproc t args); |
92 |
92 |
93 fun dynamic_value cookie thy some_target postproc t args = |
93 fun dynamic_value cookie thy some_target postproc t args = |
94 partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args); |
94 partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args); |
95 |
95 |
96 fun static_value_exn cookie thy some_target postproc consts = |
96 fun static_value_exn cookie thy some_target postproc consts = |
97 let |
97 let |
98 fun evaluator naming program thy expr deps = |
98 fun evaluator naming program thy ((_, vs_ty), t) deps = |
99 base_evaluator cookie thy some_target naming program expr deps []; |
99 base_evaluator cookie thy some_target naming program (vs_ty, t) deps []; |
100 in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end; |
100 in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end; |
101 |
101 |
102 fun static_value_strict cookie thy some_target postproc consts t = |
102 fun static_value_strict cookie thy some_target postproc consts t = |
103 Exn.release (static_value_exn cookie thy some_target postproc consts t); |
103 Exn.release (static_value_exn cookie thy some_target postproc consts t); |
104 |
104 |
113 fun init _ () = error "Truth_Result" |
113 fun init _ () = error "Truth_Result" |
114 ); |
114 ); |
115 val put_truth = Truth_Result.put; |
115 val put_truth = Truth_Result.put; |
116 val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth"); |
116 val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth"); |
117 |
117 |
118 fun check_holds thy naming program expr deps ct = |
118 fun check_holds thy naming program vs_t deps ct = |
119 let |
119 let |
120 val t = Thm.term_of ct; |
120 val t = Thm.term_of ct; |
121 val _ = if fastype_of t <> propT |
121 val _ = if fastype_of t <> propT |
122 then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t) |
122 then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t) |
123 else (); |
123 else (); |
124 val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT)); |
124 val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT)); |
125 val result = case partiality_as_none (base_evaluator truth_cookie thy NONE naming program expr deps []) |
125 val result = case partiality_as_none (base_evaluator truth_cookie thy NONE naming program vs_t deps []) |
126 of SOME Holds => true |
126 of SOME Holds => true |
127 | _ => false; |
127 | _ => false; |
128 in |
128 in |
129 Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct) |
129 Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct) |
130 end; |
130 end; |
131 |
131 |
132 val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result |
132 val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result |
133 (Thm.add_oracle (Binding.name "holds_by_evaluation", |
133 (Thm.add_oracle (Binding.name "holds_by_evaluation", |
134 fn (thy, naming, program, expr, deps, ct) => check_holds thy naming program expr deps ct))); |
134 fn (thy, naming, program, vs_t, deps, ct) => check_holds thy naming program vs_t deps ct))); |
135 |
135 |
136 fun check_holds_oracle thy naming program expr deps ct = |
136 fun check_holds_oracle thy naming program ((_, vs_ty), t) deps ct = |
137 raw_check_holds_oracle (thy, naming, program, expr, deps, ct); |
137 raw_check_holds_oracle (thy, naming, program, (vs_ty, t), deps, ct); |
138 |
138 |
139 val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy (check_holds_oracle thy)); |
139 val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy (check_holds_oracle thy)); |
140 |
140 |
141 fun static_holds_conv thy consts = Code_Thingol.static_eval_conv thy consts |
141 fun static_holds_conv thy consts = Code_Thingol.static_eval_conv thy consts |
142 (fn naming => fn program => fn thy => check_holds_oracle thy naming program); |
142 (fn naming => fn program => fn thy => check_holds_oracle thy naming program); |