From 934164a914831ae5c8e7a4d7bbecd624d2dd5e14 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 7 Feb 2012 10:57:54 +0000 Subject: Start support for both plain and custom top levels (work in progress). --- hol-light/hol-light.el | 178 +++++++++++++++++++++++++-------- hol-light/pg_prompt.ml | 41 ++++++++ hol-light/pg_tactics.ml | 260 ++++++++++++++++++++++++++++-------------------- 3 files changed, 329 insertions(+), 150 deletions(-) create mode 100644 hol-light/pg_prompt.ml diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index 001779ca..1fdafcde 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.el @@ -13,36 +13,130 @@ (require 'proof-easy-config) ; easy configure mechanism (require 'proof-syntax) ; functions for making regexps -(defcustom hol-light-home "/home/da/hol_light" +(defcustom hol-light-home + (or (getenv "HOLLIGHT_HOME") + (concat (getenv "HOME") "/hol_light")) "*Directory holding the local installation of HOL Light." :type 'string :group 'hol-light) +(defcustom hol-light-use-custom-toplevel t + "*If non-nil, we use a custom toplevel for Proof General. +This configures extra annotations inside HOL Light to help +recognise portions of output from the proof assistant. + +If this is incompatible with your usage of HOL Light for +some reason, you can change this setting to run in a +degraded (less robust) way which interfaces with the +standard top level. + +You need to restart Emacs if you change this setting.") + +(defconst hol-light-pre-sync-cmd + (format "#use \"%spg_prompt.ml\";; " proof-home-directory) + "Command used to configure prompt annotations for Proof General.") + (defcustom hol-light-startup-cmds (list (format "#cd \"%s\"" hol-light-home) - "#use \"hol.ml\"" - (format "#cd \"%s\"" proof-home-directory) - "#use \"pg_tactics.ml\"") + "#use \"hol.ml\"") "*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 +;; + +(defconst hol-light-plain-start-goals-regexp + (concat + "^\\(val it : x?goalstack = \\)" + "\\(?:.+\n\\)*" + "\\(?:[0-9]*[0-9] subgoals? ([0-9]+ total)\\|No subgoals\\)") + "Value for `proof-shell-start-goals-regexp' with standard top level.") + +(defconst hol-light-annotated-start-goals-regexp + hol-light-plain-start-goals-regexp + "Value for `proof-shell-start-goals-regexp' with custom top level.") + +(defconst hol-light-plain-interrupt-regexp + "Interrupted" + "Value for `proof-shell-interrupt-regexp' with standard top level.") + +(defconst hol-light-annotated-interrupt-regexp + hol-light-plain-interrupt-regexp ;; TODO + "Value for `proof-shell-interrupt-regexp' with custom top level.") + +(defconst hol-light-plain-prompt-regexp + "^# " + "Value for `proof-shell-annotated-prompt-regexp' with standard top level.") + +(defconst hol-light-annotated-prompt-regexp + ".+" + "Value for `proof-shell-annotated-prompt-regexp' with custom top level.") + +(defconst hol-light-plain-error-regexp + (proof-regexp-alt "Characters [0-9]+-[0-9]+:" + "Exception: Failure" + "Parse error: " + ;; TODO: more here, file not found, etc. + ) + "Value for `proof-shell-error-regexp' with standard top level.") + +(defconst hol-light-annotated-error-regexp + ".+" ;; FIXME: include new lines + "Value for `proof-shell-error-regexp' with custom top level.") + +(defconst hol-light-plain-proof-completed-regexp + "Initial goal proved" + "Value for `proof-shell-proof-completed-regexp' with standard top level.") + +(defconst hol-light-annotated-proof-completed-regexp + hol-light-plain-proof-completed-regexp ;; TODO + "Value for `proof-shell-proof-completed-regexp' with standard top level.") + +(defconst hol-light-plain-message-start + nil ;; TODO + "Value for `proof-shell-eager-annotation-start' with standard top level.") + +(defconst hol-light-annotated-message-start + nil ;; TODO + "Value for `proof-shell-eager-annotation-start' with custom top level.") + +(defconst hol-light-plain-message-end + nil ;; TODO + "Value for `proof-shell-eager-annotation-start' with standard top level.") + +(defconst hol-light-annotated-message-end + nil ;; TODO + "Value for `proof-shell-eager-annotation-start' with custom top level.") + + +;;; +;;; State +;;; + (defvar hol-light-keywords nil) (defvar hol-light-rules nil) (defvar hol-light-tactics nil) (defvar hol-light-tacticals nil) + +;;; +;;; Main configuration +;;; + (proof-easy-config 'hol-light "HOL Light" proof-assistant-home-page "https://www.cl.cam.ac.uk/~jrh13/hol-light/" proof-prog-name "ocaml" proof-terminal-string ";;" - proof-script-comment-start "(*" - proof-script-comment-end "*)" + proof-shell-pre-sync-init-cmd hol-light-pre-sync-cmd + proof-shell-startup-cmds hol-light-startup-cmds - ;; These are all approximations, of course. + ;; Regexps for matching tactic script inputs: all approximations, of course. proof-goal-command-regexp "^g[ `]" - proof-save-command-regexp "pg_top_thm_and_drop" + proof-save-command-regexp "top_thm()" proof-goal-with-hole-regexp "let \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*prove" proof-save-with-hole-regexp "let \\(\\([^ \t=]*\\)\\)[ \t]*=[ \t]*top_thm()" proof-non-undoables-regexp "b()" ; and others.. @@ -50,32 +144,44 @@ proof-save-command "val %s = top_thm();;" proof-kill-goal-command "current_goalstack:=[];;" ; for cleanliness proof-showproof-command "p()" - proof-undo-n-times-cmd "(pg_repeat b %s; p());;" + proof-undo-n-times-cmd "(funpow %s b %s; p());;" proof-auto-multiple-files t proof-shell-cd-cmd "#cd \"%s\";;" proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) - proof-shell-interrupt-regexp "Interrupted" - proof-shell-start-goals-regexp -(setq proof-shell-start-goals-regexp - (concat - "^\\(val it : x?goalstack = \\)" - "\\(?:.+\n\\)*" - "\\(?:[0-9]*[0-9] subgoals? ([0-9]+ total)\\|No subgoals\\)") - ) - proof-shell-annotated-prompt-regexp "^# " - proof-shell-error-regexp - (proof-regexp-alt "Characters [0-9]+-[0-9]+:" - "Exception: Failure" - "Parse error: ") - proof-shell-init-cmd - (append hol-light-startup-cmds - '("let rec pg_repeat f n = match n with 0 -> () | _ -> (f(); pg_repeat f (n-1))" - "let pg_top_thm_and_drop () = let t = top_thm() in ((let _ = b() in ()); t)")) + proof-shell-annotated-prompt-regexp (if hol-light-use-custom-toplevel + hol-light-annotated-prompt-regexp + hol-light-plain-prompt-regexp) + + proof-shell-interrupt-regexp (if hol-light-use-custom-toplevel + hol-light-annotated-interrupt-regexp + hol-light-plain-interrupt-regexp) + + proof-shell-start-goals-regexp (if hol-light-use-custom-toplevel + hol-light-annotated-start-goals-regexp + hol-light-plain-start-goals-regexp) + + proof-shell-error-regexp (if hol-light-use-custom-toplevel + hol-light-annotated-error-regexp + hol-light-plain-error-regexp) + proof-shell-proof-completed-regexp (if hol-light-use-custom-toplevel + hol-light-annotated-proof-completed-regexp + hol-light-plain-proof-completed-regexp) + + proof-shell-eager-annotation-start (if hol-light-use-custom-toplevel + hol-light-annotated-message-start + hol-light-plain-message-start) + + proof-shell-eager-annotation-end (if hol-light-use-custom-toplevel + hol-light-annotated-message-end + hol-light-plain-message-end) + + ;; FIXME: add optional help topic parameter to help command. proof-info-command "help \"hol\"" - proof-shell-proof-completed-regexp "Initial goal proved" + proof-shell-proof-completed-regexp + ;; FIXME: next one needs setting so that "urgent" messages are displayed ;; eagerly from HOL. ;; proof-shell-eager-annotation-start @@ -83,13 +189,11 @@ proof-forget-id-command "();;" ;; candidate for making nil, change generic - ;; We must force this to use ptys since mosml doesn't flush its output - ;; (on Linux, presumably on Solaris too). - proof-shell-process-connection-type t - ;; - ;; Syntax table entries for proof scripts + ;; Syntax and syntax table entries for proof scripts ;; + proof-script-comment-start "(*" + proof-script-comment-end "*)" proof-script-syntax-table-entries '(?\` "\"" ?\$ "." @@ -221,8 +325,9 @@ ) +;;; ;;; Prooftree configuration (experimental, ongoing) -;; +;;; ;; regexps for recognising additional markup in output @@ -333,11 +438,4 @@ The not yet delayed output is in the region (add-hook 'proof-tree-urgent-action-hook 'hol-light-proof-tree-get-new-subgoals) - - - - -(warn "Hol Light Proof General is incomplete! Please help improve it! -Read the manual, make improvements, upload at http://proofgeneral.inf.ed.ac.uk/trac") - (provide 'hol-light) diff --git a/hol-light/pg_prompt.ml b/hol-light/pg_prompt.ml new file mode 100644 index 00000000..f52dc76e --- /dev/null +++ b/hol-light/pg_prompt.ml @@ -0,0 +1,41 @@ +(* ========================================================================= *) +(* HOL Light tweaks for Proof General. *) +(* *) +(* Mark Adams, David Aspinall. *) +(* LFCS, School of Informatics, University of Edinburgh *) +(* *) +(* (c) Copyright University of Edinburgh and authors, 2012. *) +(* *) +(* This file adjust the OCaml prompt to help Proof General synchronization. *) +(* It is loaded before HOL Light. *) +(* ========================================================================= *) + + +(* ------------------------------------------------------------------------- *) +(* Proof General mode, providing extra annotations in output *) +(* ------------------------------------------------------------------------- *) + +let pg_mode = ref (true : bool);; + +let pg_mode_on () = (pg_mode := true);; +let pg_mode_off () = (pg_mode := false);; + +let pg_prompt_info = ref (fun () -> "");; + + +(* ------------------------------------------------------------------------- *) +(* Adjust the OCaml prompt to carry information for Proof General. *) +(* ------------------------------------------------------------------------- *) + +let original_prompt_fn = !Toploop.read_interactive_input in +(Toploop.read_interactive_input := + fun prompt buffer len -> + let prompt' = + if (!pg_mode) + then "" ^ + (!pg_prompt_info()) ^ + "" + else prompt in + original_prompt_fn prompt' buffer len);; + + diff --git a/hol-light/pg_tactics.ml b/hol-light/pg_tactics.ml index ece7a22a..45e8591e 100644 --- a/hol-light/pg_tactics.ml +++ b/hol-light/pg_tactics.ml @@ -1,23 +1,30 @@ -(* - Modified HOL Light goalstack to support Hendrik Tew's Prooftree - application via Proof General. - - Mark Adams, David Aspinall - January 2012. - - This file contains some functions that are modified from the - original HOL Light code, and is therefore subject to the HOL Light - copyright, see the file LICENSE-HOL-LIGHT in this directory. - - TODO: - 1) rebind top-level identifiers for g, e, r, b and add a flag - to turn on/off extended behaviour +(* ========================================================================= *) +(* HOL Light subgoal package amended for Proof General and Prooftree. *) +(* *) +(* Mark Adams, David Aspinall. *) +(* LFCS, School of Informatics, University of Edinburgh *) +(* *) +(* (c) Copyright University of Edinburgh and authors, 2012. *) +(* *) +(* This file contains some functions that are modified from the *) +(* original HOL Light code, and is therefore subject to the HOL Light *) +(* copyright, see the file LICENSE-HOL-LIGHT in this directory. *) +(* *) +(* ========================================================================= *) +(* *) +(* This file overwrites HOL Light's subgoal package commands with variants *) +(* that output additional annotations specifically for Prooftree. These get *) +(* intercepted by Proof General, which removes them from the output *) +(* displayed to the Proof General user. *) + +(* TODO: + 1. add urgent message annotations for errors and strings output during + long-running tactics + 2. fix on/off: don't turn off prompt annotation, support Prooftree on/off. *) - - (* ------------------------------------------------------------------------- *) -(* Goal counter for providing goad ids. *) +(* Goal counter for providing goal ids. *) (* ------------------------------------------------------------------------- *) type goal_id = int;; @@ -27,8 +34,7 @@ let string_of_goal_id id = string_of_int id;; let the_goal_counter = ref (0 : goal_id);; let inc_goal_counter () = - (the_goal_counter := !the_goal_counter + 1; - !the_goal_counter);; + (the_goal_counter := !the_goal_counter + 1);; let reset_goal_counter () = (the_goal_counter := 0; @@ -49,10 +55,10 @@ let dest_xgoal (gx : xgoal) = gx;; type xgoalstate = (term list * instantiation) * xgoal list * justification;; (* ------------------------------------------------------------------------- *) -(* A goalstack but for xgoals. *) +(* A goalstack but for xgoals. Overwrites original HL datatype. *) (* ------------------------------------------------------------------------- *) -type xgoalstack = xgoalstate list;; +type goalstack = xgoalstate list;; (* ------------------------------------------------------------------------- *) (* A refinement but for xgoals. *) @@ -61,7 +67,7 @@ type xgoalstack = xgoalstate list;; type xrefinement = xgoalstate -> xgoalstate;; (* ------------------------------------------------------------------------- *) -(* Apply instantiation to a goal. *) +(* Instantiation of xgoals. *) (* ------------------------------------------------------------------------- *) let (inst_xgoal:instantiation->xgoal->xgoal) = @@ -69,19 +75,26 @@ let (inst_xgoal:instantiation->xgoal->xgoal) = (map (I F_F INSTANTIATE_ALL p) thms,instantiate p w),id;; (* ------------------------------------------------------------------------- *) -(* A printer for xgoals etc. *) +(* A printer for xgoals and xgoalstacks. *) (* ------------------------------------------------------------------------- *) let the_new_goal_ids = ref ([] : goal_id list);; let the_tactic_flag = ref false;; +let print_string_seplist sep xs = + if (xs = []) + then () + else (print_string (hd xs); + do_list (fun x -> print_string sep; print_string x) (tl xs));; + let print_xgoal ((g,id) : xgoal) : unit = - (print_string ("[Goal ID " ^ string_of_goal_id id ^ "]"); - print_newline (); + ((if (!pg_mode) + then (print_string ("[Goal ID " ^ string_of_goal_id id ^ "]"); + print_newline ())); print_goal g);; -let (print_xgoalstack:xgoalstack->unit) = +let (print_xgoalstack:goalstack->unit) = let print_xgoalstate k gs = let (_,gl,_) = gs in let n = length gl in @@ -91,35 +104,48 @@ let (print_xgoalstack:xgoalstack->unit) = print_string s; print_newline(); if gl = [] then () else (do_list (print_xgoal o C el gl) (rev(1--(k-1))); - print_string "[*]"; + (if (!pg_mode) then print_string "[*]"); print_xgoal (el 0 gl)) in fun l -> - (print_string ("[State Counter " ^ string_of_int (length l) ^ "]"); - (if (!the_tactic_flag) + ((if (!pg_mode) & (!the_tactic_flag) then let xs = map string_of_int (!the_new_goal_ids) in - the_tactic_flag := false; - if (length xs > 0) then - print_string - ("[New Goal IDs: " ^ - end_itlist (fun x1 x2 -> x1 ^ " " ^ x2) xs ^ "]")); - print_newline (); - if l = [] then print_string "Empty goalstack" - else if tl l = [] then - let (_,gl,_ as gs) = hd l in - print_xgoalstate 1 gs - else - let (_,gl,_ as gs) = hd l - and (_,gl0,_) = hd(tl l) in - let p = length gl - length gl0 in - let p' = if p < 1 then 1 else p + 1 in - print_xgoalstate p' gs);; + (the_tactic_flag := false; + print_string "[New Goal IDs: "; + print_string_seplist " " xs; + print_string "]"; + print_newline ())); + (if l = [] then print_string "Empty goalstack" + else if tl l = [] then + let (_,gl,_ as gs) = hd l in + print_xgoalstate 1 gs + else + let (_,gl,_ as gs) = hd l + and (_,gl0,_) = hd(tl l) in + let p = length gl - length gl0 in + let p' = if p < 1 then 1 else p + 1 in + print_xgoalstate p' gs); + (if (!pg_mode) then + let (vs,theta) = + if (l = []) then ([],[]) + else let ((vs,(_,theta,_)),_,_) = hd l in + (vs,theta) in + let foo v = + let (x,_) = dest_var v in + 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_seplist ", " xs; + print_string ")"; + print_newline ())));; (* ------------------------------------------------------------------------- *) (* Goal labelling, for fresh xgoals. *) (* ------------------------------------------------------------------------- *) let label_goals (gs : goal list) : xgoal list = - let gxs = map (fun g -> (g, inc_goal_counter ())) gs in + let gxs = map (fun g -> inc_goal_counter (); (g, !the_goal_counter)) + gs in (the_new_goal_ids := map snd gxs; gxs);; @@ -146,7 +172,7 @@ let (xby:tactic->xrefinement) = (mvs',inst'),glsx',just';; (* ------------------------------------------------------------------------- *) -(* Rotate but for xgoalstate. Completely trivial redefinition. *) +(* Rotate but for xgoalstate. Only change is different ML datatype. *) (* ------------------------------------------------------------------------- *) let (xrotate:int->xrefinement) = @@ -177,102 +203,116 @@ let (mk_xgoalstate:goal->xgoalstate) = else failwith "mk_goalstate: Non-boolean goal";; (* ------------------------------------------------------------------------- *) -(* Subgoal package but for xgoals. *) +(* The Prooftree global state is an ever increasing counter. *) (* ------------------------------------------------------------------------- *) -let current_xgoalstack = ref ([] :xgoalstack);; +let the_pt_global_state = ref 1;; -let (xrefine:xrefinement->xgoalstack) = - fun r -> - let l = !current_xgoalstack in - let h = hd l in - let res = r h :: l in - current_xgoalstack := res; - !current_xgoalstack;; +let inc_pt_global_state () = + (the_pt_global_state := !the_pt_global_state + 1);; -let flush_xgoalstack() = - let l = !current_xgoalstack in - current_xgoalstack := [hd l];; +let pt_global_state () = !the_pt_global_state;; -let xe tac = - the_tactic_flag := true; - xrefine(xby(VALID tac));; +(* ------------------------------------------------------------------------- *) +(* The Prooftree proof state is the length of the goal stack. *) +(* ------------------------------------------------------------------------- *) -let xr n = xrefine(xrotate n);; +let the_current_xgoalstack = ref ([] : goalstack);; -let set_xgoal(asl,w) = - current_xgoalstack := - [mk_xgoalstate(map (fun t -> "",ASSUME t) asl,w)]; - !current_xgoalstack;; +let pt_proof_state () = length !the_current_xgoalstack;; -let xg t = +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";; + +(* ------------------------------------------------------------------------- *) +(* Subgoal package but for xgoals. These overwrite the existing commands. *) +(* ------------------------------------------------------------------------- *) + +let (xrefine:xrefinement->goalstack) = + fun r -> + let l = !the_current_xgoalstack in + let h = hd l in + let res = r h :: l in + the_current_xgoalstack := res; + !the_current_xgoalstack;; + +let flush_goalstack() = + let l = !the_current_xgoalstack in + the_current_xgoalstack := [hd l];; + +let e tac = + let result = xrefine(xby(VALID tac)) in + (inc_pt_global_state (); + the_tactic_flag := true; + result);; + +let r n = + (inc_pt_global_state (); + xrefine(xrotate n));; + +let set_goal(asl,w) = + let aths = map ASSUME asl in + (inc_pt_global_state (); + the_current_xgoalstack := + [mk_xgoalstate(map (fun th -> "",th) aths,w)]; + !the_current_xgoalstack);; + +let g t = let fvs = sort (<) (map (fst o dest_var) (frees t)) in (if fvs <> [] then let errmsg = end_itlist (fun s t -> s^", "^t) fvs in warn true ("Free variables in goal: "^errmsg) else ()); - set_xgoal([],t);; + set_goal([],t);; -let xb() = - let l = !current_xgoalstack in +let b() = + let l = !the_current_xgoalstack in if length l = 1 then failwith "Can't back up any more" else - current_xgoalstack := tl l; - !current_xgoalstack;; + (inc_pt_global_state (); + the_current_xgoalstack := tl l; + !the_current_xgoalstack);; -let xp() = - !current_xgoalstack;; +let p() = !the_current_xgoalstack;; -let xtop_realgoal() = - let (_,(((asl,w),id)::_),_)::_ = !current_xgoalstack in +let top_realgoal() = + let (_,(((asl,w),id)::_),_)::_ = !the_current_xgoalstack in asl,w;; -let xtop_goal() = - let asl,w = xtop_realgoal() in +let top_goal() = + let asl,w = top_realgoal() in map (concl o snd) asl,w;; -let xtop_thm() = - let (_,[],f)::_ = !current_xgoalstack in +let top_thm() = + let (_,[],f)::_ = !the_current_xgoalstack in f null_inst [];; (* ------------------------------------------------------------------------- *) -(* Goal id to goal lookup function. *) +(* Configure the annotated prompt. *) (* ------------------------------------------------------------------------- *) -let print_xgoal_of_id (id:goal_id) : unit = - let gsts = !current_xgoalstack in - let find_goal (_,xgs,_) = find (fun (g,id0) -> id0 = id) xgs in - let xg = tryfind find_goal gsts in - print_xgoal xg;; +pg_prompt_info := + fun () -> + let pst = pt_proof_state () and gst = pt_global_state () in + string_of_int gst ^ "|" ^ string_of_int pst;; (* ------------------------------------------------------------------------- *) -(* Jumping back to a previous state. *) +(* Printing the goal of a given Prooftree goal id. *) (* ------------------------------------------------------------------------- *) -let jump_back_to_state n : xgoalstack = - let l = length !current_xgoalstack in - if (0 <= n) & (n <= l) - then (current_xgoalstack := snd (chop_list (l-n) !current_xgoalstack); - !current_xgoalstack) - else failwith "Not a valid state number";; +let print_xgoal_of_id (id:goal_id) : unit = + let gsts = !the_current_xgoalstack in + let find_goal (_,xgs,_) = find (fun (g,id0) -> id0 = id) xgs in + let xg = tryfind find_goal gsts in + print_xgoal xg;; (* ------------------------------------------------------------------------- *) -(* Install the goal-related printers. *) +(* Install the new goal-related printers. *) (* ------------------------------------------------------------------------- *) #install_printer print_xgoal;; #install_printer print_xgoalstack;; - -(* ------------------------------------------------------------------------- *) -(* Replace the top-level prompt *) -(* ------------------------------------------------------------------------- *) - -(* TODO: something like this - -let prompt () => - "[State Counter " ^ string_of_int (length (!current_xgoalstack)) ^ "]# "); - -Toploop.read_interactive_input := - let old = !Toploop.read_interactive_input in fun prompt buffer len -> - old (prompt()) buffer len ;; - -*) -- cgit v1.2.3