91 val all_modes_of : theory -> (string * mode list) list |
91 val all_modes_of : theory -> (string * mode list) list |
92 val all_generator_modes_of : theory -> (string * mode list) list |
92 val all_generator_modes_of : theory -> (string * mode list) list |
93 val compile_clause : compilation_funs -> term option -> (term list -> term) -> |
93 val compile_clause : compilation_funs -> term option -> (term list -> term) -> |
94 theory -> string list -> string list -> mode -> term -> moded_clause -> term |
94 theory -> string list -> string list -> mode -> term -> moded_clause -> term |
95 val preprocess_intro : theory -> thm -> thm |
95 val preprocess_intro : theory -> thm -> thm |
|
96 val is_constrt : theory -> term -> bool |
|
97 val is_predT : typ -> bool |
|
98 val guess_nparams : typ -> int |
96 end; |
99 end; |
97 |
100 |
98 structure Predicate_Compile : PREDICATE_COMPILE = |
101 structure Predicate_Compile : PREDICATE_COMPILE = |
99 struct |
102 struct |
100 |
103 |
519 val keys = depending_preds_of thy intros |
521 val keys = depending_preds_of thy intros |
520 in |
522 in |
521 (data, keys) |
523 (data, keys) |
522 end; |
524 end; |
523 *) |
525 *) |
524 |
526 (* guessing number of parameters *) |
525 (* TODO: add_edges - by analysing dependencies *) |
527 fun find_indexes pred xs = |
|
528 let |
|
529 fun find is n [] = is |
|
530 | find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs; |
|
531 in rev (find [] 0 xs) end; |
|
532 |
|
533 fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT) |
|
534 | is_predT _ = false |
|
535 |
|
536 fun guess_nparams T = |
|
537 let |
|
538 val argTs = binder_types T |
|
539 val nparams = fold (curry Int.max) |
|
540 (map (fn x => x + 1) (find_indexes is_predT argTs)) 0 |
|
541 in nparams end; |
|
542 |
526 fun add_intro thm thy = let |
543 fun add_intro thm thy = let |
527 val (name, _) = dest_Const (fst (strip_intro_concl 0 (prop_of thm))) |
544 val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of thm))) |
528 fun cons_intro gr = |
545 fun cons_intro gr = |
529 case try (Graph.get_node gr) name of |
546 case try (Graph.get_node gr) name of |
530 SOME pred_data => Graph.map_node name (map_pred_data |
547 SOME pred_data => Graph.map_node name (map_pred_data |
531 (apfst (fn (intro, elim, nparams) => (thm::intro, elim, nparams)))) gr |
548 (apfst (fn (intro, elim, nparams) => (thm::intro, elim, nparams)))) gr |
532 | NONE => |
549 | NONE => |
533 let |
550 let |
534 val nparams = the_default 0 (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name) |
551 val nparams = the_default (guess_nparams T) (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name) |
535 in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], [], []))) gr end; |
552 in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], [], []))) gr end; |
536 in PredData.map cons_intro thy end |
553 in PredData.map cons_intro thy end |
537 |
554 |
538 fun set_elim thm = let |
555 fun set_elim thm = let |
539 val (name, _) = dest_Const (fst |
556 val (name, _) = dest_Const (fst |
1092 mk_bind compfuns (f_app, match_t)) |
1109 mk_bind compfuns (f_app, match_t)) |
1093 end |
1110 end |
1094 | compile_param_ext _ _ _ _ = error "compile params" |
1111 | compile_param_ext _ _ _ _ = error "compile params" |
1095 *) |
1112 *) |
1096 |
1113 |
1097 fun compile_param thy compfuns (NONE, t) = t |
1114 fun compile_param size thy compfuns (NONE, t) = t |
1098 | compile_param thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) = |
1115 | compile_param size thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) = |
1099 let |
1116 let |
1100 val (f, args) = strip_comb (Envir.eta_contract t) |
1117 val (f, args) = strip_comb (Envir.eta_contract t) |
1101 val (params, args') = chop (length ms) args |
1118 val (params, args') = chop (length ms) args |
1102 val params' = map (compile_param thy compfuns) (ms ~~ params) |
1119 val params' = map (compile_param size thy compfuns) (ms ~~ params) |
|
1120 val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of |
|
1121 val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of |
1103 val f' = |
1122 val f' = |
1104 case f of |
1123 case f of |
1105 Const (name, T) => |
1124 Const (name, T) => |
1106 mk_fun_of compfuns thy (name, T) (iss, is') |
1125 mk_fun_of compfuns thy (name, T) (iss, is') |
1107 | Free (name, T) => Free (name, funT_of compfuns (iss, is') T) |
1126 | Free (name, T) => Free (name, funT_of compfuns (iss, is') T) |
|
1127 | _ => error ("PredicateCompiler: illegal parameter term") |
1108 in list_comb (f', params' @ args') end |
1128 in list_comb (f', params' @ args') end |
1109 |
1129 |
1110 fun compile_expr size thy ((Mode (mode, is, ms)), t) = |
1130 fun compile_expr size thy ((Mode (mode, is, ms)), t) = |
1111 case strip_comb t of |
1131 case strip_comb t of |
1112 (Const (name, T), params) => |
1132 (Const (name, T), params) => |
1113 let |
1133 let |
1114 val params' = map (compile_param thy PredicateCompFuns.compfuns) (ms ~~ params) |
1134 val params' = map (compile_param size thy PredicateCompFuns.compfuns) (ms ~~ params) |
|
1135 val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of |
1115 in |
1136 in |
1116 case size of |
1137 list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params') |
1117 NONE => list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params') |
|
1118 | SOME _ => list_comb (mk_sizelim_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params') |
|
1119 end |
1138 end |
1120 | (Free (name, T), args) => |
1139 | (Free (name, T), args) => |
1121 list_comb (Free (name, funT_of PredicateCompFuns.compfuns ([], is) T), args) |
1140 let |
1122 |
1141 val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of |
1123 fun compile_gen_expr thy compfuns ((Mode (mode, is, ms)), t) = |
1142 in |
|
1143 list_comb (Free (name, funT_of PredicateCompFuns.compfuns ([], is) T), args) |
|
1144 end; |
|
1145 |
|
1146 fun compile_gen_expr size thy compfuns ((Mode (mode, is, ms)), t) = |
1124 case strip_comb t of |
1147 case strip_comb t of |
1125 (Const (name, T), params) => |
1148 (Const (name, T), params) => |
1126 let |
1149 let |
1127 val params' = map (compile_param thy compfuns) (ms ~~ params) |
1150 val params' = map (compile_param size thy compfuns) (ms ~~ params) |
1128 in |
1151 in |
1129 list_comb (mk_generator_of compfuns thy (name, T) mode, params') |
1152 list_comb (mk_generator_of compfuns thy (name, T) mode, params') |
1130 end |
1153 end |
1131 |
1154 |
1132 (** specific rpred functions -- move them to the correct place in this file *) |
1155 (** specific rpred functions -- move them to the correct place in this file *) |
1237 end |
1260 end |
1238 |
1261 |
1239 fun compile_pred compfuns mk_fun_of use_size thy all_vs param_vs s T mode moded_cls = |
1262 fun compile_pred compfuns mk_fun_of use_size thy all_vs param_vs s T mode moded_cls = |
1240 let |
1263 let |
1241 val (Ts1, (Us1, Us2)) = split_mode mode (binder_types T) |
1264 val (Ts1, (Us1, Us2)) = split_mode mode (binder_types T) |
|
1265 val funT_of = if use_size then sizelim_funT_of else funT_of |
1242 val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) (fst mode) Ts1 |
1266 val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) (fst mode) Ts1 |
1243 val xnames = Name.variant_list (all_vs @ param_vs) |
1267 val xnames = Name.variant_list (all_vs @ param_vs) |
1244 (map (fn i => "x" ^ string_of_int i) (snd mode)); |
1268 (map (fn i => "x" ^ string_of_int i) (snd mode)); |
1245 val size_name = Name.variant (all_vs @ param_vs @ xnames) "size" |
1269 val size_name = Name.variant (all_vs @ param_vs @ xnames) "size" |
1246 (* termify code: val xs = map2 (fn s => fn T => Free (s, termifyT T)) xnames Us1; *) |
1270 (* termify code: val xs = map2 (fn s => fn T => Free (s, termifyT T)) xnames Us1; *) |
1317 val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs), |
1341 val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs), |
1318 if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs)) |
1342 if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs)) |
1319 val funpropI = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs), |
1343 val funpropI = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs), |
1320 mk_tuple outargs)) |
1344 mk_tuple outargs)) |
1321 val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI) |
1345 val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI) |
1322 val _ = Output.tracing (Syntax.string_of_term_global thy introtrm) |
|
1323 val simprules = [defthm, @{thm eval_pred}, |
1346 val simprules = [defthm, @{thm eval_pred}, |
1324 @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}] |
1347 @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}] |
1325 val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1 |
1348 val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1 |
1326 val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y"]) [] introtrm (fn {...} => unfolddef_tac) |
1349 val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y"]) [] introtrm (fn {...} => unfolddef_tac) |
1327 val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)); |
1350 val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)); |
1342 (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ (string_of_mode (snd mode)) |
1365 (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ (string_of_mode (snd mode)) |
1343 end; |
1366 end; |
1344 |
1367 |
1345 fun create_definitions preds (name, modes) thy = |
1368 fun create_definitions preds (name, modes) thy = |
1346 let |
1369 let |
1347 val _ = tracing "create definitions" |
|
1348 val compfuns = PredicateCompFuns.compfuns |
1370 val compfuns = PredicateCompFuns.compfuns |
1349 val T = AList.lookup (op =) preds name |> the |
1371 val T = AList.lookup (op =) preds name |> the |
1350 fun create_definition (mode as (iss, is)) thy = let |
1372 fun create_definition (mode as (iss, is)) thy = let |
1351 val mode_cname = create_constname_of_mode thy "" name mode |
1373 val mode_cname = create_constname_of_mode thy "" name mode |
1352 val mode_cbasename = Long_Name.base_name mode_cname |
1374 val mode_cbasename = Long_Name.base_name mode_cname |
1392 let |
1414 let |
1393 val T = AList.lookup (op =) preds name |> the |
1415 val T = AList.lookup (op =) preds name |> the |
1394 fun create_definition mode thy = |
1416 fun create_definition mode thy = |
1395 let |
1417 let |
1396 val mode_cname = create_constname_of_mode thy "sizelim_" name mode |
1418 val mode_cname = create_constname_of_mode thy "sizelim_" name mode |
1397 val (Ts1, (Us1, Us2)) = split_mode mode (binder_types T) |
1419 (* val (Ts1, (Us1, Us2)) = split_mode mode (binder_types T) |
1398 val Ts1' = map2 (fn NONE => I | SOME is => funT_of PredicateCompFuns.compfuns ([], is)) (fst mode) Ts1 |
1420 val Ts1' = map2 (fn NONE => I | SOME is => size_funT_of PredicateCompFuns.compfuns ([], is)) (fst mode) Ts1 |
1399 val funT = (Ts1' @ Us1 @ [@{typ "code_numeral"}]) ---> (PredicateCompFuns.mk_predT (mk_tupleT Us2)) |
1421 (Ts1' @ Us1 @ [@{typ "code_numeral"}]) ---> (PredicateCompFuns.mk_predT (mk_tupleT Us2)) *) |
|
1422 val funT = sizelim_funT_of PredicateCompFuns.compfuns mode T |
1400 in |
1423 in |
1401 thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] |
1424 thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] |
1402 |> set_sizelim_function_name name mode mode_cname |
1425 |> set_sizelim_function_name name mode mode_cname |
1403 end; |
1426 end; |
1404 in |
1427 in |
1445 (* MAJOR FIXME: prove_params should be simple |
1468 (* MAJOR FIXME: prove_params should be simple |
1446 - different form of introrule for parameters ? *) |
1469 - different form of introrule for parameters ? *) |
1447 fun prove_param thy (NONE, t) = TRY (rtac @{thm refl} 1) |
1470 fun prove_param thy (NONE, t) = TRY (rtac @{thm refl} 1) |
1448 | prove_param thy (m as SOME (Mode (mode, is, ms)), t) = |
1471 | prove_param thy (m as SOME (Mode (mode, is, ms)), t) = |
1449 let |
1472 let |
1450 val (f, args) = strip_comb t |
1473 val (f, args) = strip_comb (Envir.eta_contract t) |
1451 val (params, _) = chop (length ms) args |
1474 val (params, _) = chop (length ms) args |
1452 val f_tac = case f of |
1475 val f_tac = case f of |
1453 Const (name, T) => simp_tac (HOL_basic_ss addsimps |
1476 Const (name, T) => simp_tac (HOL_basic_ss addsimps |
1454 (@{thm eval_pred}::(predfun_definition_of thy name mode):: |
1477 (@{thm eval_pred}::(predfun_definition_of thy name mode):: |
1455 @{thm "Product_Type.split_conv"}::[])) 1 |
1478 @{thm "Product_Type.split_conv"}::[])) 1 |
1463 THEN print_tac "after simplification in prove_args" |
1486 THEN print_tac "after simplification in prove_args" |
1464 THEN (EVERY (map (prove_param thy) (ms ~~ params))) |
1487 THEN (EVERY (map (prove_param thy) (ms ~~ params))) |
1465 THEN (REPEAT_DETERM (atac 1)) |
1488 THEN (REPEAT_DETERM (atac 1)) |
1466 end |
1489 end |
1467 |
1490 |
1468 THEN print_tac "after prove_param" |
|
1469 fun prove_expr thy (Mode (mode, is, ms), t, us) (premposition : int) = |
1491 fun prove_expr thy (Mode (mode, is, ms), t, us) (premposition : int) = |
1470 case strip_comb t of |
1492 case strip_comb t of |
1471 (Const (name, T), args) => |
1493 (Const (name, T), args) => |
1472 let |
1494 let |
1473 val introrule = predfun_intro_of thy name mode |
1495 val introrule = predfun_intro_of thy name mode |
1640 *) |
1662 *) |
1641 (* TODO: remove function *) |
1663 (* TODO: remove function *) |
1642 |
1664 |
1643 fun prove_param2 thy (NONE, t) = all_tac |
1665 fun prove_param2 thy (NONE, t) = all_tac |
1644 | prove_param2 thy (m as SOME (Mode (mode, is, ms)), t) = let |
1666 | prove_param2 thy (m as SOME (Mode (mode, is, ms)), t) = let |
1645 val (f, args) = strip_comb t |
1667 val (f, args) = strip_comb (Envir.eta_contract t) |
1646 val (params, _) = chop (length ms) args |
1668 val (params, _) = chop (length ms) args |
1647 val f_tac = case f of |
1669 val f_tac = case f of |
1648 Const (name, T) => full_simp_tac (HOL_basic_ss addsimps |
1670 Const (name, T) => full_simp_tac (HOL_basic_ss addsimps |
1649 (@{thm eval_pred}::(predfun_definition_of thy name mode) |
1671 (@{thm eval_pred}::(predfun_definition_of thy name mode) |
1650 :: @{thm "Product_Type.split_conv"}::[])) 1 |
1672 :: @{thm "Product_Type.split_conv"}::[])) 1 |
1651 | Free _ => all_tac |
1673 | Free _ => all_tac |
|
1674 | _ => error "prove_param2: illegal parameter term" |
1652 in |
1675 in |
1653 print_tac "before simplification in prove_args:" |
1676 print_tac "before simplification in prove_args:" |
1654 THEN f_tac |
1677 THEN f_tac |
1655 THEN print_tac "after simplification in prove_args" |
1678 THEN print_tac "after simplification in prove_args" |
1656 THEN (EVERY (map (prove_param2 thy) (ms ~~ params))) |
1679 THEN (EVERY (map (prove_param2 thy) (ms ~~ params))) |
1868 fun add_equations_of steps prednames thy = |
1891 fun add_equations_of steps prednames thy = |
1869 let |
1892 let |
1870 val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") |
1893 val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") |
1871 val (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) = |
1894 val (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) = |
1872 prepare_intrs thy prednames |
1895 prepare_intrs thy prednames |
1873 val _ = tracing "Infering modes..." |
1896 val _ = Output.tracing "Infering modes..." |
1874 val moded_clauses = #infer_modes steps thy extra_modes arities param_vs clauses |
1897 val moded_clauses = #infer_modes steps thy extra_modes arities param_vs clauses |
1875 val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses |
1898 val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses |
1876 val _ = Output.tracing "Defining executable functions..." |
1899 val _ = Output.tracing "Defining executable functions..." |
1877 val thy' = fold (#create_definitions steps preds) modes thy |
1900 val thy' = fold (#create_definitions steps preds) modes thy |
1878 |> Theory.checkpoint |
1901 |> Theory.checkpoint |
1896 thy'' |
1919 thy'' |
1897 end |
1920 end |
1898 |
1921 |
1899 fun extend' value_of edges_of key (G, visited) = |
1922 fun extend' value_of edges_of key (G, visited) = |
1900 let |
1923 let |
1901 val _ = Output.tracing ("calling extend' with " ^ key) |
|
1902 val (G', v) = case try (Graph.get_node G) key of |
1924 val (G', v) = case try (Graph.get_node G) key of |
1903 SOME v => (G, v) |
1925 SOME v => (G, v) |
1904 | NONE => (Graph.new_node (key, value_of key) G, value_of key) |
1926 | NONE => (Graph.new_node (key, value_of key) G, value_of key) |
1905 val (G'', visited') = fold (extend' value_of edges_of) (edges_of (key, v) \\ visited) |
1927 val (G'', visited') = fold (extend' value_of edges_of) (edges_of (key, v) \\ visited) |
1906 (G', key :: visited) |
1928 (G', key :: visited) |