99 (string * mode list) list -> (string * mode list) list -> mode -> (term list * indprem list) |
99 (string * mode list) list -> (string * mode list) list -> mode -> (term list * indprem list) |
100 -> (term list * (indprem * tmode) list) option |
100 -> (term list * (indprem * tmode) list) option |
101 val string_of_moded_prem : theory -> (indprem * tmode) -> string |
101 val string_of_moded_prem : theory -> (indprem * tmode) -> string |
102 val all_modes_of : theory -> (string * mode list) list |
102 val all_modes_of : theory -> (string * mode list) list |
103 val all_generator_modes_of : theory -> (string * mode list) list |
103 val all_generator_modes_of : theory -> (string * mode list) list |
104 val compile_clause : compilation_funs -> term option -> (term list -> term) -> |
|
105 theory -> string list -> string list -> mode -> term -> moded_clause -> term |
|
106 val preprocess_intro : theory -> thm -> thm |
104 val preprocess_intro : theory -> thm -> thm |
107 val is_constrt : theory -> term -> bool |
105 val is_constrt : theory -> term -> bool |
108 val is_predT : typ -> bool |
106 val is_predT : typ -> bool |
109 val guess_nparams : typ -> int |
107 val guess_nparams : typ -> int |
110 val cprods_subset : 'a list list -> 'a list list |
108 val cprods_subset : 'a list list -> 'a list list |
1277 val vs = map Free |
1275 val vs = map Free |
1278 (Name.variant_list names (replicate (length Ts) "x") ~~ Ts) |
1276 (Name.variant_list names (replicate (length Ts) "x") ~~ Ts) |
1279 in |
1277 in |
1280 fold_rev lambda vs (f (list_comb (t, vs))) |
1278 fold_rev lambda vs (f (list_comb (t, vs))) |
1281 end; |
1279 end; |
1282 (* |
1280 |
1283 fun compile_param_ext thy compfuns modes (NONE, t) = t |
1281 fun compile_param size thy compfuns (NONE, t) = t |
1284 | compile_param_ext thy compfuns modes (m as SOME (Mode ((iss, is'), is, ms)), t) = |
1282 | compile_param size thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) = |
1285 let |
|
1286 val (vs, u) = strip_abs t |
|
1287 val (ivs, ovs) = split_mode is vs |
|
1288 val (f, args) = strip_comb u |
|
1289 val (params, args') = chop (length ms) args |
|
1290 val (inargs, outargs) = split_mode is' args' |
|
1291 val b = length vs |
|
1292 val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b) |
|
1293 val outp_perm = |
|
1294 snd (split_mode is perm) |
|
1295 |> map (fn i => i - length (filter (fn x => x < i) is')) |
|
1296 val names = [] -- TODO |
|
1297 val out_names = Name.variant_list names (replicate (length outargs) "x") |
|
1298 val f' = case f of |
|
1299 Const (name, T) => |
|
1300 if AList.defined op = modes name then |
|
1301 mk_predfun_of thy compfuns (name, T) (iss, is') |
|
1302 else error "compile param: Not an inductive predicate with correct mode" |
|
1303 | Free (name, T) => Free (name, param_funT_of compfuns T (SOME is')) |
|
1304 val outTs = dest_tupleT (dest_predT compfuns (body_type (fastype_of f'))) |
|
1305 val out_vs = map Free (out_names ~~ outTs) |
|
1306 val params' = map (compile_param thy modes) (ms ~~ params) |
|
1307 val f_app = list_comb (f', params' @ inargs) |
|
1308 val single_t = (mk_single compfuns (mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm))) |
|
1309 val match_t = compile_match thy compfuns [] [] out_vs single_t |
|
1310 in list_abs (ivs, |
|
1311 mk_bind compfuns (f_app, match_t)) |
|
1312 end |
|
1313 | compile_param_ext _ _ _ _ = error "compile params" |
|
1314 *) |
|
1315 |
|
1316 fun compile_param neg_in_sizelim size thy compfuns (NONE, t) = t |
|
1317 | compile_param neg_in_sizelim size thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) = |
|
1318 let |
1283 let |
1319 val (f, args) = strip_comb (Envir.eta_contract t) |
1284 val (f, args) = strip_comb (Envir.eta_contract t) |
1320 val (params, args') = chop (length ms) args |
1285 val (params, args') = chop (length ms) args |
1321 val params' = map (compile_param neg_in_sizelim size thy compfuns) (ms ~~ params) |
1286 val params' = map (compile_param size thy compfuns) (ms ~~ params) |
1322 val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of |
1287 val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of |
1323 val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of |
1288 val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of |
1324 val f' = |
1289 val f' = |
1325 case f of |
1290 case f of |
1326 Const (name, T) => |
1291 Const (name, T) => mk_fun_of compfuns thy (name, T) (iss, is') |
1327 mk_fun_of compfuns thy (name, T) (iss, is') |
1292 | Free (name, T) => Free (name, funT_of compfuns (iss, is') T) |
1328 | Free (name, T) => |
|
1329 case neg_in_sizelim of |
|
1330 SOME _ => Free (name, sizelim_funT_of compfuns (iss, is') T) |
|
1331 | NONE => Free (name, funT_of compfuns (iss, is') T) |
|
1332 |
|
1333 | _ => error ("PredicateCompiler: illegal parameter term") |
1293 | _ => error ("PredicateCompiler: illegal parameter term") |
1334 in |
1294 in |
1335 (case neg_in_sizelim of SOME size_t => |
1295 list_comb (f', params' @ args') |
1336 (fn t => |
|
1337 let |
|
1338 val Ts = fst (split_last (binder_types (fastype_of t))) |
|
1339 val names = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) |
|
1340 in |
|
1341 list_abs (names ~~ Ts, list_comb (t, (map Bound ((length Ts) - 1 downto 0)) @ [size_t])) |
|
1342 end) |
|
1343 | NONE => I) |
|
1344 (list_comb (f', params' @ args')) |
|
1345 end |
1296 end |
1346 |
1297 |
1347 fun compile_expr neg_in_sizelim size thy ((Mode (mode, is, ms)), t) = |
1298 fun compile_expr size thy ((Mode (mode, is, ms)), t) = |
1348 case strip_comb t of |
1299 case strip_comb t of |
1349 (Const (name, T), params) => |
1300 (Const (name, T), params) => |
1350 let |
1301 let |
1351 val params' = map (compile_param neg_in_sizelim size thy PredicateCompFuns.compfuns) (ms ~~ params) |
1302 val params' = map (compile_param size thy PredicateCompFuns.compfuns) (ms ~~ params) |
1352 val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of |
1303 val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of |
1353 in |
1304 in |
1354 list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params') |
1305 list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params') |
1355 end |
1306 end |
1356 | (Free (name, T), args) => |
1307 | (Free (name, T), args) => |
1419 fun tuple args = if null args then [] else [HOLogic.mk_tuple args] |
1370 fun tuple args = if null args then [] else [HOLogic.mk_tuple args] |
1420 in ((tuple inargs, tuple outargs), args) end |
1371 in ((tuple inargs, tuple outargs), args) end |
1421 end |
1372 end |
1422 val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts)) |
1373 val (inoutargs, args) = split_list (map mk_arg (1 upto (length Ts) ~~ Ts)) |
1423 val (inargs, outargs) = pairself flat (split_list inoutargs) |
1374 val (inargs, outargs) = pairself flat (split_list inoutargs) |
1424 val size_t = case size of NONE => [] | SOME size_t => [size_t] |
1375 val size_t = case size of NONE => [] | SOME (polarity, size_t) => [polarity, size_t] |
1425 val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs @ size_t), mk_tuple outargs) |
1376 val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs @ size_t), mk_tuple outargs) |
1426 val t = fold_rev mk_split_lambda args r |
1377 val t = fold_rev mk_split_lambda args r |
1427 in |
1378 in |
1428 (t, names) |
1379 (t, names) |
1429 end; |
1380 end; |
1459 val (out_ts'', (names', eqs')) = |
1410 val (out_ts'', (names', eqs')) = |
1460 fold_map check_constrt out_ts' (names, []); |
1411 fold_map check_constrt out_ts' (names, []); |
1461 val (out_ts''', (names'', constr_vs)) = fold_map distinct_v |
1412 val (out_ts''', (names'', constr_vs)) = fold_map distinct_v |
1462 out_ts'' (names', map (rpair []) vs); |
1413 out_ts'' (names', map (rpair []) vs); |
1463 in |
1414 in |
1464 (* termify code: |
|
1465 compile_match thy compfuns constr_vs (eqs @ eqs') out_ts''' |
1415 compile_match thy compfuns constr_vs (eqs @ eqs') out_ts''' |
1466 (mk_single compfuns (mk_tuple (map mk_valtermify_term out_ts))) |
1416 (mk_single compfuns (mk_tuple out_ts)) |
1467 *) |
|
1468 compile_match thy compfuns constr_vs (eqs @ eqs') out_ts''' |
|
1469 (final_term out_ts) |
|
1470 end |
1417 end |
1471 | compile_prems out_ts vs names ((p, mode as Mode ((_, is), _, _)) :: ps) = |
1418 | compile_prems out_ts vs names ((p, mode as Mode ((_, is), _, _)) :: ps) = |
1472 let |
1419 let |
1473 val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); |
1420 val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); |
1474 val (out_ts', (names', eqs)) = |
1421 val (out_ts', (names', eqs)) = |
1480 let |
1427 let |
1481 val (in_ts, out_ts''') = split_smode is us; |
1428 val (in_ts, out_ts''') = split_smode is us; |
1482 val in_ts = map (compile_arg size thy param_vs iss) in_ts |
1429 val in_ts = map (compile_arg size thy param_vs iss) in_ts |
1483 val args = case size of |
1430 val args = case size of |
1484 NONE => in_ts |
1431 NONE => in_ts |
1485 | SOME size_t => in_ts @ [size_t] |
1432 | SOME (polarity, size_t) => in_ts @ [polarity, size_t] |
1486 val u = lift_pred compfuns |
1433 val u = lift_pred compfuns |
1487 (list_comb (compile_expr NONE size thy (mode, t), args)) |
1434 (list_comb (compile_expr size thy (mode, t), args)) |
1488 val rest = compile_prems out_ts''' vs' names'' ps |
1435 val rest = compile_prems out_ts''' vs' names'' ps |
1489 in |
1436 in |
1490 (u, rest) |
1437 (u, rest) |
1491 end |
1438 end |
1492 | Negprem (us, t) => |
1439 | Negprem (us, t) => |
1493 let |
1440 let |
1494 val (in_ts, out_ts''') = split_smode is us |
1441 val (in_ts, out_ts''') = split_smode is us |
1495 val u = lift_pred compfuns |
1442 val size' = Option.map (apfst HOLogic.mk_not) size |
1496 (mk_not PredicateCompFuns.compfuns (list_comb (compile_expr size NONE thy (mode, t), in_ts))) |
1443 val args = case size' of |
|
1444 NONE => in_ts |
|
1445 | SOME (polarity, size_t) => in_ts @ [polarity, size_t] |
|
1446 val u = lift_pred compfuns (mk_not PredicateCompFuns.compfuns |
|
1447 (list_comb (compile_expr size' thy (mode, t), args))) |
1497 val rest = compile_prems out_ts''' vs' names'' ps |
1448 val rest = compile_prems out_ts''' vs' names'' ps |
1498 in |
1449 in |
1499 (u, rest) |
1450 (u, rest) |
1500 end |
1451 end |
1501 | Sidecond t => |
1452 | Sidecond t => |
1507 | GeneratorPrem (us, t) => |
1458 | GeneratorPrem (us, t) => |
1508 let |
1459 let |
1509 val (in_ts, out_ts''') = split_smode is us; |
1460 val (in_ts, out_ts''') = split_smode is us; |
1510 val args = case size of |
1461 val args = case size of |
1511 NONE => in_ts |
1462 NONE => in_ts |
1512 | SOME size_t => in_ts @ [size_t] |
1463 | SOME (polarity, size_t) => in_ts @ [polarity, size_t] |
1513 val u = compile_gen_expr size thy compfuns (mode, t) args |
1464 val u = compile_gen_expr size thy compfuns (mode, t) args |
1514 val rest = compile_prems out_ts''' vs' names'' ps |
1465 val rest = compile_prems out_ts''' vs' names'' ps |
1515 in |
1466 in |
1516 (u, rest) |
1467 (u, rest) |
1517 end |
1468 end |
1518 | Generator (v, T) => |
1469 | Generator (v, T) => |
1519 let |
1470 let |
1520 val u = lift_random (HOLogic.mk_random T (the size)) |
1471 val u = lift_random (HOLogic.mk_random T (snd (the size))) |
1521 val rest = compile_prems [Free (v, T)] vs' names'' ps; |
1472 val rest = compile_prems [Free (v, T)] vs' names'' ps; |
1522 in |
1473 in |
1523 (u, rest) |
1474 (u, rest) |
1524 end |
1475 end |
1525 in |
1476 in |
1535 let |
1486 let |
1536 val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T) |
1487 val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T) |
1537 val (Us1, Us2) = split_smodeT (snd mode) Ts2 |
1488 val (Us1, Us2) = split_smodeT (snd mode) Ts2 |
1538 val funT_of = if use_size then sizelim_funT_of else funT_of |
1489 val funT_of = if use_size then sizelim_funT_of else funT_of |
1539 val Ts1' = map2 (fn NONE => I | SOME is => funT_of PredicateCompFuns.compfuns ([], is)) (fst mode) Ts1 |
1490 val Ts1' = map2 (fn NONE => I | SOME is => funT_of PredicateCompFuns.compfuns ([], is)) (fst mode) Ts1 |
1540 val size_name = Name.variant (all_vs @ param_vs) "size" |
|
1541 fun mk_input_term (i, NONE) = |
1491 fun mk_input_term (i, NONE) = |
1542 [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))] |
1492 [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))] |
1543 | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of |
1493 | mk_input_term (i, SOME pis) = case HOLogic.strip_tupleT (nth Ts2 (i - 1)) of |
1544 [] => error "strange unit input" |
1494 [] => error "strange unit input" |
1545 | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))] |
1495 | [T] => [Free (Name.variant (all_vs @ param_vs) ("x" ^ string_of_int i), nth Ts2 (i - 1))] |
1549 pis) |
1499 pis) |
1550 in if null pis then [] |
1500 in if null pis then [] |
1551 else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end |
1501 else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end |
1552 val in_ts = maps mk_input_term (snd mode) |
1502 val in_ts = maps mk_input_term (snd mode) |
1553 val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1' |
1503 val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1' |
1554 val size = Free (size_name, @{typ "code_numeral"}) |
1504 val [depth_name, polarity_name] = Name.variant_list (all_vs @ param_vs) ["depth", "polarity"] |
|
1505 val size = Free (depth_name, @{typ "code_numeral"}) |
|
1506 val polarity = Free (polarity_name, @{typ "bool"}) |
1555 val decr_size = |
1507 val decr_size = |
1556 if use_size then |
1508 if use_size then |
1557 SOME (Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"}) |
1509 SOME (polarity, Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"}) |
1558 $ size $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"})) |
1510 $ size $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"})) |
1559 else |
1511 else |
1560 NONE |
1512 NONE |
1561 val cl_ts = |
1513 val cl_ts = |
1562 map (compile_clause compfuns decr_size (fn out_ts => mk_single compfuns (mk_tuple out_ts)) |
1514 map (compile_clause compfuns decr_size |
1563 thy all_vs param_vs mode (mk_tuple in_ts)) moded_cls; |
1515 thy all_vs param_vs mode (mk_tuple in_ts)) moded_cls; |
1564 val t = foldr1 (mk_sup compfuns) cl_ts |
1516 val t = foldr1 (mk_sup compfuns) cl_ts |
1565 val T' = mk_predT compfuns (mk_tupleT Us2) |
1517 val T' = mk_predT compfuns (mk_tupleT Us2) |
1566 val size_t = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T') |
1518 val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T') |
1567 $ HOLogic.mk_eq (size, @{term "0 :: code_numeral"}) |
1519 val full_mode = null Us2 |
1568 $ mk_bot compfuns (dest_predT compfuns T') $ t |
1520 val size_t = |
|
1521 if_const $ HOLogic.mk_eq (size, @{term "0 :: code_numeral"}) |
|
1522 $ (if full_mode then |
|
1523 if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T') $ mk_single compfuns HOLogic.unit |
|
1524 else |
|
1525 mk_bot compfuns (dest_predT compfuns T')) |
|
1526 $ t |
1569 val fun_const = mk_fun_of compfuns thy (s, T) mode |
1527 val fun_const = mk_fun_of compfuns thy (s, T) mode |
1570 val eq = if use_size then |
1528 val eq = if use_size then |
1571 (list_comb (fun_const, params @ in_ts @ [size]), size_t) |
1529 (list_comb (fun_const, params @ in_ts @ [polarity, size]), size_t) |
1572 else |
1530 else |
1573 (list_comb (fun_const, params @ in_ts), t) |
1531 (list_comb (fun_const, params @ in_ts), t) |
1574 in |
1532 in |
1575 HOLogic.mk_Trueprop (HOLogic.mk_eq eq) |
1533 HOLogic.mk_Trueprop (HOLogic.mk_eq eq) |
1576 end; |
1534 end; |
2498 ^ Syntax.string_of_term_global thy t_compr) |
2456 ^ Syntax.string_of_term_global thy t_compr) |
2499 | [m] => m |
2457 | [m] => m |
2500 | m :: _ :: _ => (warning ("Multiple modes possible for comprehension " |
2458 | m :: _ :: _ => (warning ("Multiple modes possible for comprehension " |
2501 ^ Syntax.string_of_term_global thy t_compr); m); |
2459 ^ Syntax.string_of_term_global thy t_compr); m); |
2502 val (inargs, outargs) = split_smode user_mode' args; |
2460 val (inargs, outargs) = split_smode user_mode' args; |
2503 val t_pred = list_comb (compile_expr NONE NONE thy (m, list_comb (pred, params)), inargs); |
2461 val t_pred = list_comb (compile_expr NONE thy (m, list_comb (pred, params)), inargs); |
2504 val t_eval = if null outargs then t_pred else |
2462 val t_eval = if null outargs then t_pred else |
2505 let |
2463 let |
2506 val outargs_bounds = map (fn Bound i => i) outargs; |
2464 val outargs_bounds = map (fn Bound i => i) outargs; |
2507 val outargsTs = map (nth Ts) outargs_bounds; |
2465 val outargsTs = map (nth Ts) outargs_bounds; |
2508 val T_pred = HOLogic.mk_tupleT outargsTs; |
2466 val T_pred = HOLogic.mk_tupleT outargsTs; |