468 |
468 |
469 fun parents_wrt_facts facts fact_graph = |
469 fun parents_wrt_facts facts fact_graph = |
470 let |
470 let |
471 val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts |
471 val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts |
472 val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts |
472 val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts |
473 fun insert_not_parent parents name = |
473 fun insert_not_seen seen name = |
474 not (member (op =) parents name) ? insert (op =) name |
474 not (member (op =) seen name) ? insert (op =) name |
475 fun parents_of parents [] = parents |
475 fun parents_of seen parents [] = parents |
476 | parents_of parents (name :: names) = |
476 | parents_of seen parents (name :: names) = |
477 if Symtab.defined tab name then |
477 if Symtab.defined tab name then |
478 parents_of (name :: parents) names |
478 parents_of (name :: seen) (name :: parents) names |
479 else |
479 else |
480 parents_of parents (Graph.Keys.fold (insert_not_parent parents) |
480 parents_of (name :: seen) parents |
481 (Graph.imm_preds fact_graph name) names) |
481 (Graph.Keys.fold (insert_not_seen seen) |
482 in parents_of [] (Graph.maximals fact_graph) end |
482 (Graph.imm_preds fact_graph name) names) |
|
483 in parents_of [] [] (Graph.maximals fact_graph) end |
483 |
484 |
484 (* Generate more suggestions than requested, because some might be thrown out |
485 (* Generate more suggestions than requested, because some might be thrown out |
485 later for various reasons and "meshing" gives better results with some |
486 later for various reasons and "meshing" gives better results with some |
486 slack. *) |
487 slack. *) |
487 fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts) |
488 fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts) |