diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2010-08-25 15:09:34 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-25 15:09:34 +0000 |
commit | d354c17e240a5adde788e326e0a67363fee5b1e7 (patch) | |
tree | cbcbe72aa68d426284348b3f7f2f61e1e8ad3206 /obsolete/plastic/plastic-syntax.el | |
parent | 33b8947b98461acdc2d7b88d3002a14d0492b3e6 (diff) |
Renamed file obsolete/plastic/plastic-syntax.el, formerly plastic/plastic-syntax.el
Diffstat (limited to 'obsolete/plastic/plastic-syntax.el')
-rw-r--r-- | obsolete/plastic/plastic-syntax.el | 119 |
1 files changed, 119 insertions, 0 deletions
diff --git a/obsolete/plastic/plastic-syntax.el b/obsolete/plastic/plastic-syntax.el new file mode 100644 index 00000000..c259a3b7 --- /dev/null +++ b/obsolete/plastic/plastic-syntax.el @@ -0,0 +1,119 @@ +;; plastic-syntax.el - Syntax of Plastic +;; Author: Paul Callaghan <P.C.Callaghan@durham.ac.uk> +;; Maintainer: <author> +;; plastic-syntax.el,v 6.0 2001/09/03 12:11:56 da Exp + +;; adapted from the following, by Paul Callaghan +;; ;; lego-syntax.el Syntax of LEGO +;; ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; ;; Author: Thomas Kleymann and Dilip Sequeira +;; ;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk> +;; ;; lego-syntax.el,v 2.10 1998/11/06 16:18:55 tms Exp + + +(require 'proof-syntax) + +;; ----- keywords for font-lock. + +(defconst plastic-keywords-goal '("$?Goal")) + +(defconst plastic-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen")) + +(defconst plastic-commands + (append plastic-keywords-goal plastic-keywords-save + '("allE" "allI" "andE" "andI" "Assumption" "Claim" "Coercion" + "Cut" "Discharge" "DischargeKeep" + "echo" "exE" "exI" "Expand" "ExpAll" + "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed" + "impE" "impI" "Induction" "Inductive" + "Invert" "Init" "intros" "Intros" "Module" "Next" + "Normal" "notE" "notI" "orE" "orIL" "orIR" "qnify" "Qnify" + "Qrepl" "Record" "Refine" "Repeat" "Return" "ReturnAll" + "Try" "Unfreeze")) + "Subset of Plastic keywords and tacticals which are terminated by a \?;") + +(defconst plastic-keywords + (append plastic-commands + '("Constructors" "Double" "ElimOver" "Fields" "Import" "Inversion" + "NoReductions" "Parameters" "Relation" "Theorems"))) + +(defconst plastic-tacticals '("Then" "Else" "Try" "Repeat" "For")) + +;; ----- regular expressions for font-lock +(defconst plastic-error-regexp "^\\(FAIL\\)" + "A regular expression indicating that the Plastic process has identified an error.") + +(defvar plastic-id proof-id) + +(defvar plastic-ids (concat plastic-id "\\(\\s *,\\s *" plastic-id "\\)*") + "*For font-lock, we treat \",\" separated identifiers as one identifier + and refontify commata using \\{plastic-fixup-change}.") + +(defconst plastic-arg-list-regexp "\\s *\\(\\[[^]]+\\]\\s *\\)*" + "Regular expression maching a list of arguments.") + +(defun plastic-decl-defn-regexp (char) + (concat "\\[\\s *\\(" plastic-ids "\\)" plastic-arg-list-regexp char)) +; Examples +; ^ ^^^^ ^^^^^^^^^^^^^^^^^^^^^^^ ^^^^ +; [ sort = +; [ sort [n:nat] = +; [ sort [abbrev=...][n:nat] = + +(defconst plastic-definiendum-alternative-regexp + (concat "\\(" plastic-id "\\)" plastic-arg-list-regexp "\\s * ==") + "Regular expression where the first match identifies the definiendum.") + +(defvar plastic-font-lock-terms + (list + + ; lambda binders + (list (plastic-decl-defn-regexp "[:|?]") 1 + 'proof-declaration-name-face) + + ; let binders + (list plastic-definiendum-alternative-regexp 1 'font-lock-function-name-face) + (list (plastic-decl-defn-regexp "=") 1 'font-lock-function-name-face) + + ; Pi and Sigma binders + (list (concat "[{<]\\s *\\(" plastic-ids "\\)") 1 + 'proof-declaration-name-face) + + ;; Kinds + (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\((" + plastic-id ")\\)?") 'font-lock-type-face)) + "*Font-lock table for Plastic terms.") + +;; Instead of "[^:]+", it may be better to use "plastic-id". Furthermore, +;; it might be safer to append "\\s-*:". +(defconst plastic-goal-with-hole-regexp + (concat "\\(" (proof-ids-to-regexp plastic-keywords-goal) "\\)\\s-+\\([^:]+\\)") + "Regular expression which matches an entry in `plastic-keywords-goal' + and the name of the goal.") + +(defconst plastic-save-with-hole-regexp + (concat "\\(" (proof-ids-to-regexp plastic-keywords-save) "\\)\\s-+\\([^;]+\\)") + "Regular expression which matches an entry in + `plastic-keywords-save' and the name of the goal.") + +(defvar plastic-font-lock-keywords-1 + (append + plastic-font-lock-terms + (list + (cons (proof-ids-to-regexp plastic-keywords) 'font-lock-keyword-face) + (cons (proof-ids-to-regexp plastic-tacticals) 'proof-tacticals-name-face) + (list plastic-goal-with-hole-regexp 2 'font-lock-function-name-face) + (list plastic-save-with-hole-regexp 2 'font-lock-function-name-face)))) + +(defun plastic-init-syntax-table () + "Set appropriate values for syntax table in current buffer." + + (modify-syntax-entry ?_ "_") + (modify-syntax-entry ?\' "_") + (modify-syntax-entry ?\| ".") + (modify-syntax-entry ?\* ". 23") + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4")) + + +(provide 'plastic-syntax) |