equal
deleted
inserted
replaced
149 end |
149 end |
150 |
150 |
151 fun all_input_of T = |
151 fun all_input_of T = |
152 let |
152 let |
153 val (Ts, U) = strip_type T |
153 val (Ts, U) = strip_type T |
154 fun input_of (Type (@{type_name Product_Type.prod}, [T1, T2])) = Pair (input_of T1, input_of T2) |
154 fun input_of (Type (\<^type_name>\<open>Product_Type.prod\<close>, [T1, T2])) = Pair (input_of T1, input_of T2) |
155 | input_of _ = Input |
155 | input_of _ = Input |
156 in |
156 in |
157 if U = HOLogic.boolT then |
157 if U = HOLogic.boolT then |
158 fold_rev (curry Fun) (map input_of Ts) Bool |
158 fold_rev (curry Fun) (map input_of Ts) Bool |
159 else |
159 else |
221 |
221 |
222 fun is_constructable vs t = forall (member (op =) vs) (term_vs t) |
222 fun is_constructable vs t = forall (member (op =) vs) (term_vs t) |
223 |
223 |
224 fun missing_vars vs t = subtract (op =) vs (term_vs t) |
224 fun missing_vars vs t = subtract (op =) vs (term_vs t) |
225 |
225 |
226 fun output_terms (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) = |
226 fun output_terms (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2, Mode_Pair (d1, d2)) = |
227 output_terms (t1, d1) @ output_terms (t2, d2) |
227 output_terms (t1, d1) @ output_terms (t2, d2) |
228 | output_terms (t1 $ t2, Mode_App (d1, d2)) = |
228 | output_terms (t1 $ t2, Mode_App (d1, d2)) = |
229 output_terms (t1, d1) @ output_terms (t2, d2) |
229 output_terms (t1, d1) @ output_terms (t2, d2) |
230 | output_terms (t, Term Output) = [t] |
230 | output_terms (t, Term Output) = [t] |
231 | output_terms _ = [] |
231 | output_terms _ = [] |
237 | lookup_mode modes (Free (x, _)) = |
237 | lookup_mode modes (Free (x, _)) = |
238 (case (AList.lookup (op =) modes x) of |
238 (case (AList.lookup (op =) modes x) of |
239 SOME ms => SOME (map (fn m => (Context m , [])) ms) |
239 SOME ms => SOME (map (fn m => (Context m , [])) ms) |
240 | NONE => NONE) |
240 | NONE => NONE) |
241 |
241 |
242 fun derivations_of (ctxt : Proof.context) modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) (Pair (m1, m2)) = |
242 fun derivations_of (ctxt : Proof.context) modes vs (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2) (Pair (m1, m2)) = |
243 map_product |
243 map_product |
244 (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2)) |
244 (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2)) |
245 (derivations_of ctxt modes vs t1 m1) (derivations_of ctxt modes vs t2 m2) |
245 (derivations_of ctxt modes vs t1 m1) (derivations_of ctxt modes vs t2 m2) |
246 | derivations_of ctxt modes vs t (m as Fun _) = |
246 | derivations_of ctxt modes vs t (m as Fun _) = |
247 (case try (all_derivations_of ctxt modes vs) t of |
247 (case try (all_derivations_of ctxt modes vs) t of |
252 if eq_mode (m, Input) then |
252 if eq_mode (m, Input) then |
253 [(Term Input, missing_vars vs t)] |
253 [(Term Input, missing_vars vs t)] |
254 else if eq_mode (m, Output) then |
254 else if eq_mode (m, Output) then |
255 (if is_possible_output ctxt vs t then [(Term Output, [])] else []) |
255 (if is_possible_output ctxt vs t then [(Term Output, [])] else []) |
256 else [] |
256 else [] |
257 and all_derivations_of ctxt modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) = |
257 and all_derivations_of ctxt modes vs (Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2) = |
258 let |
258 let |
259 val derivs1 = all_derivations_of ctxt modes vs t1 |
259 val derivs1 = all_derivations_of ctxt modes vs t1 |
260 val derivs2 = all_derivations_of ctxt modes vs t2 |
260 val derivs2 = all_derivations_of ctxt modes vs t2 |
261 in |
261 in |
262 map_product |
262 map_product |