498 List.app (add_th 1) deps; |
498 List.app (add_th 1) deps; |
499 List.app add_sym feats |
499 List.app add_sym feats |
500 end |
500 end |
501 |
501 |
502 fun for i = |
502 fun for i = |
503 if i = num_facts then |
503 if i = num_facts then () |
504 () |
504 else (learn_one i (Vector.sub (featss, i)) (Vector.sub (depss, i)); for (i + 1)) |
505 else |
505 in |
506 (learn_one (num_facts0 + i) (Vector.sub (featss, i)) (Vector.sub (depss, i)); |
506 for num_facts0; |
507 for (i + 1)) |
|
508 in |
|
509 for 0; |
|
510 (Array.vector tfreq, Array.vector sfreq, Array.vector dffreq) |
507 (Array.vector tfreq, Array.vector sfreq, Array.vector dffreq) |
511 end |
508 end |
512 |
509 |
513 fun naive_bayes (tfreq, sfreq, dffreq) num_facts max_suggs visible_facts goal_feats = |
510 fun naive_bayes (tfreq, sfreq, dffreq) num_facts max_suggs visible_facts goal_feats = |
514 let |
511 let |
655 |
652 |
656 fun add_node kind name parents feats deps (access_G, (fact_xtab, feat_xtab), learns) = |
653 fun add_node kind name parents feats deps (access_G, (fact_xtab, feat_xtab), learns) = |
657 ((Graph.new_node (name, (kind, feats, deps)) access_G |
654 ((Graph.new_node (name, (kind, feats, deps)) access_G |
658 handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G) |
655 handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G) |
659 |> fold (add_edge_to name) parents, |
656 |> fold (add_edge_to name) parents, |
660 (maybe_add_to_xtab name fact_xtab, |
657 (add_to_xtab name fact_xtab, fold maybe_add_to_xtab feats feat_xtab), |
661 fold maybe_add_to_xtab feats feat_xtab), |
|
662 (name, feats, deps) :: learns) |
658 (name, feats, deps) :: learns) |
663 |
659 |
664 fun try_graph ctxt when def f = |
660 fun try_graph ctxt when def f = |
665 f () |
661 f () |
666 handle |
662 handle |
1418 |
1414 |
1419 val access_G = access_G |> Graph.default_node (name, (Isar_Proof, feats, deps)) |
1415 val access_G = access_G |> Graph.default_node (name, (Isar_Proof, feats, deps)) |
1420 val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents |
1416 val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents |
1421 val (deps, _) = ([], access_G) |> fold maybe_learn_from deps |
1417 val (deps, _) = ([], access_G) |> fold maybe_learn_from deps |
1422 |
1418 |
1423 val fact_xtab = maybe_add_to_xtab name fact_xtab |
1419 val fact_xtab = add_to_xtab name fact_xtab |
1424 val feat_xtab = fold maybe_add_to_xtab feats feat_xtab |
1420 val feat_xtab = fold maybe_add_to_xtab feats feat_xtab |
1425 in |
1421 in |
1426 ((name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab))) |
1422 ((name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab))) |
1427 end |
1423 end |
1428 |
1424 |