Moved

3 files changed, 257 insertions, 0 deletions

diff --git a/obsolete/lclam/README b/obsolete/lclam/README
new file mode 100644
index 00000000..39db25c1
--- /dev/null
+++ b/obsolete/lclam/README
@@ -0,0 +1,15 @@
+Lambda-CLAM Proof General
+
+Written by James Brotherston <jjb@dai.ed.ac.uk>.
+
+
+Status:			supported
+Maintainer:		James Brotherston <jjb@dai.ed.ac.uk>
+Lambda-CLAM version:    ??
+Lambda-CLAM homepage:   http://dream.dai.ed.ac.uk/software/systems/lambda-clam/
+
+========================================
+
+$Id$
+
+
diff --git a/obsolete/lclam/example.lcm b/obsolete/lclam/example.lcm
new file mode 100644
index 00000000..5b275814
--- /dev/null
+++ b/obsolete/lclam/example.lcm
@@ -0,0 +1,34 @@
+/* File name:      example.lcm                            */
+/* Description:    Tutorial walkthrough from LClam manual */
+/* Author:         James Brotherston                      */
+/* Last modified:  20th August 2001                       */
+
+query_top_goal X assp.
+
+set_spypoint (induction_top normal_ind).
+set_spypoint sym_eval.
+
+silent_output on.
+
+pds_plan (induction_top normal_ind) assp.
+continue.
+continue.
+continue.
+
+add_theory_to_induction_scheme_list arithmetic.
+add_theory_to_sym_eval_list arithmetic.
+set_wave_rule_to_sym_eval.
+add_to_sym_eval_list [idty].
+set_wave_rule_to_sym_eval.
+remove_spypoint (induction_top normal_ind).
+remove_spypoint sym_eval.
+pds_plan (induction_top normal_ind) assp.
+
+step_by_step on.
+pds_plan (induction_top normal_ind) assp.
+continue.
+backtrack.
+try ind_strat.
+continue.
+plan_node (2::1::nil).
+abandon.
diff --git a/obsolete/lclam/lclam.el b/obsolete/lclam/lclam.el
new file mode 100644
index 00000000..ae171aa0
--- /dev/null
+++ b/obsolete/lclam/lclam.el
@@ -0,0 +1,208 @@
+;; File name:      lclam.el        
+;; Description:    Proof General instance for Lambda-CLAM
+;; Author:         James Brotherston <jjb@dai.ed.ac.uk>
+;; Last modified:  23 October 2001
+;;
+;; $Id$
+
+(require 'proof)            ; load generic parts
+(require 'proof-syntax)     
+
+;;
+;; =========== User settings for Lambda-CLAM ============
+;;
+
+(defcustom lclam-prog-name ; "~/lambda-clam-teyjus/bin/lclam"
+			   "lclam"
+  "*Name of program to run Lambda-CLAM"
+  :type 'file
+  :group 'lclam)
+
+(defcustom lclam-web-page
+  "http://dream.dai.ed.ac.uk/software/systems/lambda-clam/"
+  "URL of web page for Lambda-CLAM"
+  :type 'string
+  :group 'lclam-config)
+
+
+;;
+;; =========== Configuration of generic modes ============
+;;
+
+(defun lclam-config ()
+  "Configure Proof General scripting for Lambda-CLAM."
+  (setq 
+   proof-terminal-char             ?\.
+   proof-comment-start             "/*"
+   proof-comment-end               "*/"
+   proof-goal-command-regexp       "^pds_plan"
+   proof-save-command-regexp       nil
+   proof-goal-with-hole-regexp     nil
+   proof-save-with-hole-regexp     nil
+   proof-non-undoables-regexp      nil
+   proof-undo-n-times-cmd          nil
+   proof-showproof-command         nil 
+   proof-goal-command              "^pds_plan %s."
+   proof-save-command              nil
+   proof-kill-goal-command         nil
+   proof-assistant-homepage        lclam-web-page
+   proof-auto-multiple-files       nil 
+   ))
+
+(defun lclam-shell-config ()
+  "Configure Proof General shell for Lambda-CLAM"
+  (setq
+   proof-shell-annotated-prompt-regexp "^lclam:" 
+   proof-shell-cd-cmd                  nil
+   proof-shell-prompt-pattern          nil
+   proof-shell-interrupt-regexp        nil
+   proof-shell-error-regexp            nil
+   proof-shell-start-goals-regexp      nil
+   proof-shell-end-goals-regexp        nil
+   proof-shell-proof-completed-regexp  "^Plan Succeeded"
+   proof-shell-init-cmd                nil
+   proof-shell-quit-cmd                "halt."
+   proof-shell-eager-annotation-start  nil
+    ))
+
+;;
+;; =========== Defining the derived modes ================
+;;
+
+(define-derived-mode lclam-proofscript-mode proof-mode
+  "Lambda-CLAM script" nil
+  (lclam-config)
+  (proof-config-done))
+
+(define-derived-mode lclam-shell-mode proof-shell-mode
+  "Lambda-CLAM shell" nil
+  (lclam-shell-config)
+  (proof-shell-config-done))
+
+(define-derived-mode lclam-response-mode proof-response-mode
+  "Lambda-CLAM response" nil
+  (proof-response-config-done))
+
+(define-derived-mode lclam-goals-mode proof-goals-mode
+  "Lambda-CLAM goals" nil
+  (proof-goals-config-done))
+
+;; Automatic selection of theory file or proof script mode
+;; .lcm -> proof script mode
+;; .def -> theory file mode
+
+(defun lclam-mode ()
+(interactive)
+(cond
+    ((proof-string-match "\\.def$" (buffer-file-name))
+    (thy-mode))
+    (t
+    (lclam-proofscript-mode)))
+)
+
+;; Hook which configures settings to get the proof shell running 
+
+(add-hook 'proof-pre-shell-start-hook 'lclam-pre-shell-start)
+
+(defun lclam-pre-shell-start ()
+  (setq proof-prog-name         lclam-prog-name)
+  (setq proof-mode-for-shell    'lclam-shell-mode)
+  (setq proof-mode-for-response 'lclam-response-mode)
+  (setq proof-mode-for-goals    'lclam-goals-mode)
+  (setq proof-shell-process-connection-type t))
+
+
+;;
+;; ============ Extra bits and pieces - JB ============
+;;
+
+;; Open .def files in theory mode from now on
+
+(setq auto-mode-alist
+      (cons '("\\.def$" . thy-mode) auto-mode-alist))
+
+;; Remove redundant toolbar buttons
+
+(setq lclam-toolbar-entries
+      (remassoc 'state lclam-toolbar-entries))
+(setq lclam-toolbar-entries
+      (remassoc 'context lclam-toolbar-entries))
+(setq lclam-toolbar-entries
+      (remassoc 'undo lclam-toolbar-entries))
+(setq lclam-toolbar-entries
+      (remassoc 'retract lclam-toolbar-entries))
+(setq lclam-toolbar-entries
+      (remassoc 'qed lclam-toolbar-entries))
+
+;;
+;; ============ Theory file mode ==============
+;;
+
+(define-derived-mode thy-mode fundamental-mode "Lambda-CLAM theory file mode"
+  (thy-add-menus))
+
+(defvar thy-mode-map nil)
+
+(defun thy-add-menus ()
+  "Add Lambda-CLAM menu to current menu bar."  
+  (require 'proof-script)    
+  (require 'proof-x-symbol)
+  (easy-menu-define thy-mode-pg-menu
+                    thy-mode-map
+                    "PG Menu for Lambda-CLAM Proof General"
+                    (cons proof-general-name
+                          (append
+                           (list
+                           ;; A couple from the toolbar that make sense here
+                           ;; (also in proof-universal-keys)
+                            ["Issue command" proof-minibuffer-cmd t]
+                            ["Interrupt prover" proof-interrupt-process t])
+			   (list proof-buffer-menu)
+                           (list proof-help-menu))))
+
+  (easy-menu-define thy-mode-lclam-menu
+                    thy-mode-map
+                    "Menu for Lambda-CLAM Proof General, theory file mode."
+                    (cons "Theory"
+                          (list
+                           ["Next section" thy-goto-next-section t]
+                           ["Prev section" thy-goto-prev-section t]
+                           ["Insert template" thy-insert-template t]
+; da: commented out this, function is incomplete
+;                           ["Include definitions" match-and-assert-defs
+;                            :active (proof-locked-region-empty-p)]
+                           ["Process theory" process-thy-file
+                            :active (proof-locked-region-empty-p)]
+; da: commented out this, there's no retract function provided
+;                           ["Retract theory" isa-retract-thy-file
+;                            :active (proof-locked-region-full-p)]
+                           ["Next error" proof-next-error t]
+                           ["Switch to script" thy-find-other-file t])))
+
+  (easy-menu-add thy-mode-pg-menu thy-mode-map)
+  (easy-menu-add thy-mode-lclam-menu thy-mode-map)
+)
+
+(defun process-thy-file (file)
+  "Process the theory file FILE.  If interactive, use buffer-file-name."
+  (interactive (list buffer-file-name))
+  (save-some-buffers)
+  (update-thy-only file nil nil))
+
+(defun update-thy-only (file try wait)
+  "Process the theory file FILE."
+  ;; First make sure we're in the right directory to take care of
+  ;; relative "files" paths inside theory file.
+  (proof-cd-sync)
+  (proof-shell-invisible-command
+   (proof-format-filename
+    ;; %r parameter means relative (don't expand) path
+    (format "use_thy \"%%r\"." (if try "try_" ""))
+    (file-name-nondirectory file))
+   wait))
+
+;(defun match-and-assert-defs
+;  "Interactively process and assert definitions in theory file"
+;)
+
+(provide 'lclam)