From 366ff018d7ad21abb2148c79d7a3baa03d4f2961 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 25 Aug 2010 15:14:25 +0000 Subject: Moved --- obsolete/lclam/README | 15 ++++ obsolete/lclam/example.lcm | 34 ++++++++ obsolete/lclam/lclam.el | 208 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 257 insertions(+) create mode 100644 obsolete/lclam/README create mode 100644 obsolete/lclam/example.lcm create mode 100644 obsolete/lclam/lclam.el (limited to 'obsolete/lclam') 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 . + + +Status: supported +Maintainer: James Brotherston +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 +;; 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) -- cgit v1.2.3