equal
deleted
inserted
replaced
4 Setup for Transfer for types that are BNF. |
4 Setup for Transfer for types that are BNF. |
5 *) |
5 *) |
6 |
6 |
7 signature TRANSFER_BNF = |
7 signature TRANSFER_BNF = |
8 sig |
8 sig |
|
9 exception NO_PRED_DATA of unit |
|
10 |
9 val transfer_plugin: string |
11 val transfer_plugin: string |
10 val base_name_of_bnf: BNF_Def.bnf -> binding |
12 val base_name_of_bnf: BNF_Def.bnf -> binding |
11 val type_name_of_bnf: BNF_Def.bnf -> string |
13 val type_name_of_bnf: BNF_Def.bnf -> string |
12 val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data |
14 val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data |
13 val bnf_only_type_ctr: (BNF_Def.bnf -> 'a -> 'a) -> BNF_Def.bnf -> 'a -> 'a |
15 val bnf_only_type_ctr: (BNF_Def.bnf -> 'a -> 'a) -> BNF_Def.bnf -> 'a -> 'a |
18 |
20 |
19 open BNF_Util |
21 open BNF_Util |
20 open BNF_Def |
22 open BNF_Def |
21 open BNF_FP_Util |
23 open BNF_FP_Util |
22 open BNF_FP_Def_Sugar |
24 open BNF_FP_Def_Sugar |
|
25 |
|
26 exception NO_PRED_DATA of unit |
23 |
27 |
24 val transfer_plugin = Plugin_Name.declare_setup @{binding transfer} |
28 val transfer_plugin = Plugin_Name.declare_setup @{binding transfer} |
25 |
29 |
26 (* util functions *) |
30 (* util functions *) |
27 |
31 |
316 (bnf_interpretation transfer_plugin (bnf_only_type_ctr transfer_bnf_interpretation)) |
320 (bnf_interpretation transfer_plugin (bnf_only_type_ctr transfer_bnf_interpretation)) |
317 |
321 |
318 (* simplification rules for the predicator *) |
322 (* simplification rules for the predicator *) |
319 |
323 |
320 fun lookup_defined_pred_data lthy name = |
324 fun lookup_defined_pred_data lthy name = |
321 case (Transfer.lookup_pred_data lthy name) of |
325 case Transfer.lookup_pred_data lthy name of |
322 SOME data => data |
326 SOME data => data |
323 | NONE => (error "lookup_pred_data: something went utterly wrong") |
327 | NONE => raise NO_PRED_DATA () |
324 |
328 |
325 fun lives_of_fp (fp_sugar: fp_sugar) = |
329 fun lives_of_fp (fp_sugar: fp_sugar) = |
326 let |
330 let |
327 val As = snd (dest_Type (#T fp_sugar)) |
331 val As = snd (dest_Type (#T fp_sugar)) |
328 val liveness = liveness_of_fp_bnf (length As) (hd (#bnfs (#fp_res fp_sugar))); |
332 val liveness = liveness_of_fp_bnf (length As) (hd (#bnfs (#fp_res fp_sugar))); |
375 |> map (Local_Defs.unfold lthy [@{thm conj_assoc}]) |
379 |> map (Local_Defs.unfold lthy [@{thm conj_assoc}]) |
376 |> map rel2pred_massage |
380 |> map rel2pred_massage |
377 |> Variable.export lthy old_lthy |
381 |> Variable.export lthy old_lthy |
378 |> map Drule.zero_var_indexes |
382 |> map Drule.zero_var_indexes |
379 end |
383 end |
|
384 handle NO_PRED_DATA () => [] |
380 |
385 |
381 |
386 |
382 (* fp_sugar interpretation *) |
387 (* fp_sugar interpretation *) |
383 |
388 |
384 fun fp_sugar_transfer_rules (fp_sugar:fp_sugar) = |
389 fun fp_sugar_transfer_rules (fp_sugar:fp_sugar) = |