diff options
author | mark <> | 2012-02-23 17:12:05 +0000 |
---|---|---|
committer | mark <> | 2012-02-23 17:12:05 +0000 |
commit | 4ed83bcb88f220cc08c3223bd4f274eaa5f31e0c (patch) | |
tree | 7bbf95ed0b561cfdf2e491ca8b6d614b9cdf0e49 /hol-light/TacticRecording/hiproofs.ml | |
parent | f1fdbc36e57c6005aed913830eabe2115dabc7c5 (diff) |
Altered graph .dot export so that nodes are displayed as their tactic.
Diffstat (limited to 'hol-light/TacticRecording/hiproofs.ml')
-rw-r--r-- | hol-light/TacticRecording/hiproofs.ml | 22 |
1 files changed, 19 insertions, 3 deletions
diff --git a/hol-light/TacticRecording/hiproofs.ml b/hol-light/TacticRecording/hiproofs.ml index 4adee607..370e0dc3 100644 --- a/hol-light/TacticRecording/hiproofs.ml +++ b/hol-light/TacticRecording/hiproofs.ml @@ -288,13 +288,24 @@ let thenise_hiproof h = type graph_elem = Box of (label * graph_elem list) | Line of (goalid * goalid) - | Single of goalid;; + | Single of goalid + | Name of (goalid * string);; let is_box ge = match ge with Box _ -> true | _ -> false;; let mk_line id1 id2 = Line (id1,id2);; +let rec graph_elem_nodes ge = + match ge with + Box (_,ges) -> graph_nodes ges + | Line (id1,id2) -> [id1;id2] + | Single id -> [id] + | Name (id,x) -> [id] + +and graph_nodes ges = + foldr (fun ge ids -> union (graph_elem_nodes ge) ids) ges [];; + (* Utils *) @@ -348,8 +359,13 @@ let rec hiproof_graph0 h = let hiproof_graph h = let ges = hiproof_graph0 h in - let (ges1,ges2) = partition is_box ges in - ges1 @ ges2;; + let ids = graph_nodes ges in + let tacname_of_id id = + match ((fst o gtree_tactic1 o get_gtree) id) with + Some x -> x + | None -> "<tactic>" in + let ges' = map (fun id -> Name (id, tacname_of_id id)) ids in + ges' @ ges;; |