diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 00:24:37 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2012-02-08 00:24:37 +0000 |
| commit | 9e135cc00931717c9186f188db8324b858aa785a (patch) | |
| tree | 9d5bdb387612bd9b094a3944ec9006387e99706f /hol-light | |
| parent | bc513d5ec50c0cb59c1cbd3ce76dcc86ed0f401e (diff) | |
Adjust global state idea, it is supposed to count down as well as up...
Diffstat (limited to 'hol-light')
| -rw-r--r-- | hol-light/pg_tactics.ml | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/hol-light/pg_tactics.ml b/hol-light/pg_tactics.ml index 45e8591e..c96c5cdc 100644 --- a/hol-light/pg_tactics.ml +++ b/hol-light/pg_tactics.ml @@ -134,7 +134,7 @@ let (print_xgoalstack:goalstack->unit) = x ^ if (can (rev_assoc v) theta) then " using" else " open" in let xs = map foo vs in (print_newline(); - print_string "(dependent evars: "; + print_string "(dependent evars:"; print_string_seplist ", " xs; print_string ")"; print_newline ())));; @@ -203,7 +203,7 @@ let (mk_xgoalstate:goal->xgoalstate) = else failwith "mk_goalstate: Non-boolean goal";; (* ------------------------------------------------------------------------- *) -(* The Prooftree global state is an ever increasing counter. *) +(* The global state counts the total number of undoable proof steps. *) (* ------------------------------------------------------------------------- *) let the_pt_global_state = ref 1;; @@ -211,10 +211,13 @@ let the_pt_global_state = ref 1;; let inc_pt_global_state () = (the_pt_global_state := !the_pt_global_state + 1);; +let dec_pt_global_state () = + (the_pt_global_state := !the_pt_global_state - 1);; + let pt_global_state () = !the_pt_global_state;; (* ------------------------------------------------------------------------- *) -(* The Prooftree proof state is the length of the goal stack. *) +(* The proof state number is the length of the current goal stack. *) (* ------------------------------------------------------------------------- *) let the_current_xgoalstack = ref ([] : goalstack);; @@ -272,9 +275,11 @@ let g t = let b() = let l = !the_current_xgoalstack in - if length l = 1 then failwith "Can't back up any more" else - (inc_pt_global_state (); - the_current_xgoalstack := tl l; + (* FIXME: this is wrong wrt "global" state, we might try to keep + a stack of proof states to be closer. + if length l = 1 then failwith "Can't back up any more" *) + (dec_pt_global_state (); + the_current_xgoalstack := if length l > 1 then tl l else l; !the_current_xgoalstack);; let p() = !the_current_xgoalstack;; |