From dee621d7243248654cef6309eee3998bd7e21a39 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 8 Feb 2012 08:49:25 +0000 Subject: Improve handling of undo, implementing pg_kill and pg_undo. --- hol-light/hol-light.el | 13 ++++++------ hol-light/pg_tactics.ml | 53 ++++++++++++++++++++++++------------------------- 2 files changed, 33 insertions(+), 33 deletions(-) (limited to 'hol-light') diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index f773eb6e..05f1ab98 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -51,14 +51,15 @@ You need to restart Emacs if you change this setting." "#use \"hol.ml\"") (if hol-light-use-custom-toplevel (list (format "#use \"%shol-light/pg_tactics.ml\"" - proof-home-directory))) - (list - "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1));;")) + proof-home-directory)) + (list + "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1));;" + "let pg_undo n = (pg_repeat n (fun ()->let _ = b() in ()); p());;" + "let pg_kill () = current_goalstack:=[];;"))) "*Commands used to start up a running HOL Light session." :type '(list string) :group 'hol-light) - ;; ;; Regular expressions for matching output with ;; standard or custom top levels @@ -161,9 +162,9 @@ You need to restart Emacs if you change this setting." proof-non-undoables-regexp "b()" ; and others.. proof-goal-command "g `%s`;;" proof-save-command "val %s = top_thm();;" - proof-kill-goal-command "current_goalstack:=[];;" ; for cleanliness + proof-kill-goal-command "pg_kill();;" + proof-undo-n-times-cmd "pg_undo %s;;" proof-showproof-command "p()" - proof-undo-n-times-cmd "(pg_repeat b %s; p());;" proof-auto-multiple-files t proof-shell-cd-cmd "#cd \"%s\";;" proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) diff --git a/hol-light/pg_tactics.ml b/hol-light/pg_tactics.ml index c96c5cdc..6cbf6784 100644 --- a/hol-light/pg_tactics.ml +++ b/hol-light/pg_tactics.ml @@ -203,18 +203,18 @@ let (mk_xgoalstate:goal->xgoalstate) = else failwith "mk_goalstate: Non-boolean goal";; (* ------------------------------------------------------------------------- *) -(* The global state counts the total number of undoable proof steps. *) +(* The global state counts the total number of proof steps taken. *) (* ------------------------------------------------------------------------- *) -let the_pt_global_state = ref 1;; +let the_pg_global_state = ref 1;; -let inc_pt_global_state () = - (the_pt_global_state := !the_pt_global_state + 1);; +let inc_pg_global_state () = + (the_pg_global_state := !the_pg_global_state + 1);; -let dec_pt_global_state () = - (the_pt_global_state := !the_pt_global_state - 1);; +let dec_pg_global_state n = + (the_pg_global_state := !the_pg_global_state - n);; -let pt_global_state () = !the_pt_global_state;; +let pg_global_state () = !the_pg_global_state;; (* ------------------------------------------------------------------------- *) (* The proof state number is the length of the current goal stack. *) @@ -222,15 +222,7 @@ let pt_global_state () = !the_pt_global_state;; let the_current_xgoalstack = ref ([] : goalstack);; -let pt_proof_state () = length !the_current_xgoalstack;; - -let pt_back_to_proof_state n : goalstack = - let pst = pt_proof_state () in - if (0 <= n) & (n <= pst) - then (the_current_xgoalstack := - snd (chop_list (pst-n) !the_current_xgoalstack); - !the_current_xgoalstack) - else failwith "Not a valid Prooftree state number";; +let pg_proof_state () = length !the_current_xgoalstack;; (* ------------------------------------------------------------------------- *) (* Subgoal package but for xgoals. These overwrite the existing commands. *) @@ -250,17 +242,17 @@ let flush_goalstack() = let e tac = let result = xrefine(xby(VALID tac)) in - (inc_pt_global_state (); + (inc_pg_global_state (); the_tactic_flag := true; result);; let r n = - (inc_pt_global_state (); + (inc_pg_global_state (); xrefine(xrotate n));; let set_goal(asl,w) = let aths = map ASSUME asl in - (inc_pt_global_state (); + (inc_pg_global_state (); the_current_xgoalstack := [mk_xgoalstate(map (fun th -> "",th) aths,w)]; !the_current_xgoalstack);; @@ -273,16 +265,23 @@ let g t = else ()); set_goal([],t);; +let p() = !the_current_xgoalstack;; + let b() = + failwith "Undo with b() is not available in Proof General top level";; + +let pg_undo n = let l = !the_current_xgoalstack in - (* 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);; + if length l < n then failwith "pg_undo: called with too many steps" + else (dec_pg_global_state n; + the_current_xgoalstack := snd (chop_list n l); + p());; -let p() = !the_current_xgoalstack;; +let pg_kill () = + let n = length (!the_current_xgoalstack) in + (dec_pg_global_state n; + the_current_xgoalstack := []; + p());; let top_realgoal() = let (_,(((asl,w),id)::_),_)::_ = !the_current_xgoalstack in @@ -302,7 +301,7 @@ let top_thm() = pg_prompt_info := fun () -> - let pst = pt_proof_state () and gst = pt_global_state () in + let pst = pg_proof_state () and gst = pg_global_state () in string_of_int gst ^ "|" ^ string_of_int pst;; (* ------------------------------------------------------------------------- *) -- cgit v1.2.3