From 925ef7ed385cb92c80762c3e59c5b33d1dcde05b Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 8 Feb 2012 00:25:23 +0000 Subject: More progress with Prooftree. Basic trees produced. Undoing needs work. --- hol-light/hol-light.el | 40 ++++++++++++++++++++++++++++------------ 1 file changed, 28 insertions(+), 12 deletions(-) (limited to 'hol-light') diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index 6fa0d5a8..f773eb6e 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -51,7 +51,9 @@ 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)))) + proof-home-directory))) + (list + "let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1));;")) "*Commands used to start up a running HOL Light session." :type '(list string) :group 'hol-light) @@ -161,7 +163,7 @@ You need to restart Emacs if you change this setting." proof-save-command "val %s = top_thm();;" proof-kill-goal-command "current_goalstack:=[];;" ; for cleanliness proof-showproof-command "p()" - proof-undo-n-times-cmd "(funpow %s (fun ()->let _ = b() in ()); 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 '(("\\\\" . "\\\\") ("\"" . "\\\"")) @@ -353,21 +355,32 @@ You need to restart Emacs if you change this setting." (concat "\\[Goal ID \\([0-9]+\\)\\]" "\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)")) -(defconst hol-light-additional-subgoal-regexp - ;; Group 1 is goal id, 2 is goal text. - (concat - "\\[Goal ID \\([0-9]+\\)\\]" - "\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)")) - (defconst hol-light-current-goal-regexp ;; match final (focused) subgoal. (concat (regexp-quote "[*]") - hol-light-additional-subgoal-regexp)) - -(defvar hol-light-newgoals-match "\\[New Goal IDs: \\([0-9 ]+\\)\\]") + "\\[Goal ID \\([0-9]+\\)\\]" + "\\s-*\n\\(\\(?:.+\n\\)*\\)\\(?:\n\\|$\\)")) + +(defconst hol-light-additional-subgoal-regexp + "\\[New Goal IDs: \\([0-9 ]+\\)\\]" + "HOL Light instance of `proof-tree-additional-subgoal-ID-regexp'.") (defconst hol-light-statenumber-regexp - "\\([0-9]+\\)|\\([0-9]+\\)") + "\\([0-9]+\\)|\\([0-9]+\\)" + "Regular expression to match prompt with state numbers. +The first number is a global state counter which increases with +processed steps. The second number is the number of steps within +the currently open proof.") + +(defconst hol-light-existential-regexp "\\(\\?[0-9]+\\)" + "Regexp for `proof-tree-existential-regexp'.") + +(defconst hol-light-existentials-state-start-regexp "^(dependent evars:" + "HOL Light instance of `proof-tree-existentials-state-start-regexp'.") + +(defconst hol-light-existentials-state-end-regexp ")\n" + "HOL Light instance of `proof-tree-existentials-state-end-regexp'.") + (setq ;; These ones belong in script mode config @@ -385,6 +398,9 @@ You need to restart Emacs if you change this setting." proof-tree-update-goal-regexp hol-light-update-goal-regexp proof-tree-cheating-regexp "CHEAT_TAC" ;; others... + proof-tree-existential-regexp hol-light-existential-regexp + proof-tree-existentials-state-start-regexp hol-light-existentials-state-start-regexp + proof-tree-existentials-state-end-regexp hol-light-existentials-state-end-regexp ) ;; end setq proof tree stuff -- cgit v1.2.3