Import EasyCrypt PG mode

5 files changed, 678 insertions, 0 deletions

diff --git a/easycrypt/easycrypt-abbrev.el b/easycrypt/easycrypt-abbrev.el
new file mode 100644
index 00000000..6d87367f
--- /dev/null
+++ b/easycrypt/easycrypt-abbrev.el
@@ -0,0 +1,18 @@
+(require 'proof)
+(require 'easycrypt-syntax)
+
+(defpgdefault menu-entries
+  '(
+    ["Use Three Panes" proof-three-window-toggle
+      :style    toggle
+      :active   (not proof-multiple-frames-enable)
+      :selected proof-three-window-enable
+      :help     "Use three panes"]
+
+    ["Weak-check mode" easycrypt-proof-weak-mode-toggle
+     :style    toggle
+     :selected easycrypt-proof-weak-mode
+     :help     "Toggles EasyCrypt check mode."]
+))
+
+(provide 'easycrypt-abbrev)
diff --git a/easycrypt/easycrypt-hooks.el b/easycrypt/easycrypt-hooks.el
new file mode 100644
index 00000000..22669c3a
--- /dev/null
+++ b/easycrypt/easycrypt-hooks.el
@@ -0,0 +1,63 @@
+(require 'span)
+(require 'proof)
+
+(defvar easycrypt-last-but-one-statenum 0)
+(defvar easycrypt-proof-weak-mode nil)
+
+;; Proof mode
+(defun easycrypt-proof-weak-mode-toggle ()
+  "Toggle EasyCrypt check mode."
+  (interactive)
+  (cond
+     (easycrypt-proof-weak-mode
+        (proof-shell-invisible-cmd-get-result "pragma Proofs:check"))
+     (t (proof-shell-invisible-cmd-get-result "pragma Proofs:weak")))
+  (if
+      (eq 'error proof-shell-last-output-kind)
+      (message "Failed to set proof mode")))
+
+;; Function for set or get the information in the span
+(defsubst easycrypt-get-span-statenum (span)
+  "Return the state number of the SPAN."
+  (span-property span 'statenum))
+
+(defsubst easycrypt-set-span-statenum (span val)
+  "Set the state number of the SPAN to VAL."
+  (span-set-property span 'statenum val))
+
+(defsubst proof-last-locked-span ()
+  (with-current-buffer proof-script-buffer
+  (span-at (- (proof-unprocessed-begin) 1) 'type)))
+
+(defun easycrypt-last-prompt-info (s)
+  "Extract the information from prompt."
+  (let ((lastprompt (or s (error "no prompt"))))
+     (when (string-match "\\[\\([0-9]+\\)|\\(\\sw+\\)\\]" lastprompt)
+           (list (string-to-number (match-string 1 lastprompt))
+                 (if (equal (match-string 2 lastprompt) "weakcheck") t nil)))))
+
+(defun easycrypt-last-prompt-info-safe ()
+  "Take from `proof-shell-last-prompt' the last information in the prompt."
+  (easycrypt-last-prompt-info proof-shell-last-prompt))
+
+(defun easycrypt-set-state-infos ()
+  "Set information necessary for backtracking."
+  (if proof-shell-last-prompt
+     ;; infos = prompt infos of the very last prompt
+     ;; sp    = last locked span, which we want to fill with prompt infos
+     (let ((sp    (if proof-script-buffer (proof-last-locked-span)))
+           (infos (or (easycrypt-last-prompt-info-safe) '(0 nil))))
+
+       (unless (or (not sp) (easycrypt-get-span-statenum sp))
+         (easycrypt-set-span-statenum sp easycrypt-last-but-one-statenum))
+       (setq easycrypt-last-but-one-statenum (car infos))
+       (setq easycrypt-proof-weak-mode (car (cdr infos)))
+     )))
+
+(add-hook 'proof-state-change-hook 'easycrypt-set-state-infos)
+
+(defun easycrypt-find-and-forget (span)
+  (let ((span-staten (easycrypt-get-span-statenum span)))
+       (list (format "undo %s." (int-to-string span-staten)))))
+
+(provide 'easycrypt-hooks)
diff --git a/easycrypt/easycrypt-keywords.el b/easycrypt/easycrypt-keywords.el
new file mode 100644
index 00000000..53b695ff
--- /dev/null
+++ b/easycrypt/easycrypt-keywords.el
@@ -0,0 +1,168 @@
+; Generated on Thu Dec 17 16:14:05 2015
+
+(defvar easycrypt-bytac-keywords '(
+  "exact"
+  "assumption"
+  "smt"
+  "by"
+  "reflexivity"
+  "done"
+))
+
+(defvar easycrypt-dangerous-keywords '(
+  "admit"
+  "admitted"
+))
+
+(defvar easycrypt-global-keywords '(
+  "axiom"
+  "axiomatized"
+  "lemma"
+  "realize"
+  "proof"
+  "qed"
+  "abort"
+  "goal"
+  "end"
+  "import"
+  "export"
+  "include"
+  "local"
+  "declare"
+  "hint"
+  "nosmt"
+  "module"
+  "of"
+  "const"
+  "op"
+  "pred"
+  "notation"
+  "abbrev"
+  "require"
+  "theory"
+  "abstract"
+  "section"
+  "type"
+  "class"
+  "instance"
+  "print"
+  "search"
+  "as"
+  "Pr"
+  "clone"
+  "with"
+  "rename"
+  "prover"
+  "timeout"
+  "why3"
+  "dump"
+  "remove"
+  "Top"
+  "Self"
+))
+
+(defvar easycrypt-internal-keywords '(
+  "time"
+  "undo"
+  "debug"
+  "pragma"
+))
+
+(defvar easycrypt-prog-keywords '(
+  "forall"
+  "exists"
+  "fun"
+  "glob"
+  "let"
+  "in"
+  "var"
+  "proc"
+  "if"
+  "then"
+  "else"
+  "elif"
+  "while"
+  "assert"
+  "return"
+  "res"
+  "equiv"
+  "hoare"
+  "phoare"
+  "islossless"
+))
+
+(defvar easycrypt-tactic-keywords '(
+  "beta"
+  "iota"
+  "zeta"
+  "eta"
+  "logic"
+  "delta"
+  "simplify"
+  "congr"
+  "change"
+  "split"
+  "left"
+  "right"
+  "case"
+  "pose"
+  "cut"
+  "have"
+  "suff"
+  "elim"
+  "clear"
+  "apply"
+  "rewrite"
+  "rwnormal"
+  "subst"
+  "progress"
+  "trivial"
+  "auto"
+  "idtac"
+  "move"
+  "modpath"
+  "field"
+  "fieldeq"
+  "ring"
+  "ringeq"
+  "algebra"
+  "transitivity"
+  "symmetry"
+  "seq"
+  "wp"
+  "sp"
+  "sim"
+  "skip"
+  "call"
+  "rcondt"
+  "rcondf"
+  "swap"
+  "cfold"
+  "rnd"
+  "pr_bounded"
+  "bypr"
+  "byphoare"
+  "byequiv"
+  "fel"
+  "conseq"
+  "exfalso"
+  "inline"
+  "alias"
+  "fission"
+  "fusion"
+  "unroll"
+  "splitwhile"
+  "kill"
+  "eager"
+))
+
+(defvar easycrypt-tactical-keywords '(
+  "try"
+  "first"
+  "last"
+  "do"
+  "strict"
+  "expect"
+))
+
+(provide 'easycrypt-keywords)
diff --git a/easycrypt/easycrypt-syntax.el b/easycrypt/easycrypt-syntax.el
new file mode 100644
index 00000000..db1e5342
--- /dev/null
+++ b/easycrypt/easycrypt-syntax.el
@@ -0,0 +1,171 @@
+(require 'proof-syntax)
+(require 'easycrypt-keywords)
+(require 'easycrypt-hooks)
+
+(defconst easycrypt-id "[A-Za-z_]+")
+
+(defconst easycrypt-terminal-string    ".")
+(defconst easycrypt-command-end-regexp "[^\\.]\\.\\(\\s \\|\n\\|$\\)")
+
+(defconst easycrypt-keywords-proof-goal '("lemma" "equiv" "hoare" "realize"))
+(defconst easycrypt-keywords-proof-save '("save" "qed"))
+
+(defconst easycrypt-non-undoables-regexp "^pragma\\b")
+
+(defconst easycrypt-keywords-code-open  '("{"))
+(defconst easycrypt-keywords-code-close '("}")) 
+(defconst easycrypt-keywords-code-end   '(";"))
+
+(defvar easycrypt-other-symbols "\\(\\.\\.\\|\\[\\]\\)")
+
+(defvar easycrypt-operator-char-1 "=\\|<\\|>\\|~")
+(defvar easycrypt-operator-char-2 "\\+\\|\\-")
+(defvar easycrypt-operator-char-3 "\\*\\|/\\|%")
+(defvar easycrypt-operator-char-4 "!\\|\\$\\|&\\|\\?\\|@\\|\\^\\|:\\||\\|#")
+
+(defvar easycrypt-operator-char-1234
+  (concat "\\(" easycrypt-operator-char-1
+          "\\|" easycrypt-operator-char-2
+		  "\\|" easycrypt-operator-char-3
+		  "\\|" easycrypt-operator-char-4
+          "\\)"))
+
+(defconst easycrypt-proof-save-regexp
+  (concat "^\\(" (proof-ids-to-regexp easycrypt-keywords-proof-save) "\\)\\b"))
+
+(defconst easycrypt-goal-command-regexp
+  (concat "^\\(?:local\\s-+\\)?\\(?:" (proof-ids-to-regexp easycrypt-keywords-proof-goal) "\\)"
+          "\\s-+\\(?:nosmt\\s-+\\)?\\(\\sw+\\)"))
+
+(defun easycrypt-save-command-p (span str)
+  "Decide whether argument is a [save|qed] command or not"
+  (let ((txt (or (span-property span 'cmd) "")))
+       (proof-string-match-safe easycrypt-proof-save-regexp txt)))
+
+(defun easycrypt-goal-command-p (span)
+  "Is SPAN a goal start?"
+  (let ((txt (or (span-property span 'cmd) "")))
+       (proof-string-match-safe easycrypt-goal-command-regexp txt)))
+
+(defun easycrypt-init-output-syntax-table ()
+  "Set appropriate values for syntax table for EasyCrypt output."
+  (modify-syntax-entry ?,   " ")
+  (modify-syntax-entry ?\'  "_")
+  (modify-syntax-entry ?_   "_")
+
+  ;; For comments
+  (modify-syntax-entry ?\* ". 23") 
+
+  ;; For blocks
+  (modify-syntax-entry ?\( "()1")
+  (modify-syntax-entry ?\) ")(4")
+  (modify-syntax-entry ?\{ "(}")
+  (modify-syntax-entry ?\} "){")
+  (modify-syntax-entry ?\[ "(]")
+  (modify-syntax-entry ?\] ")["))
+
+;; ----- regular expressions
+
+(defvar easycrypt-error-regexp "^\\[error-[0-9]+-[0-9]+\\]\\|^anomaly"
+  "A regexp indicating that the EasyCrypt process has identified an error.")
+
+(defvar easycrypt-shell-proof-completed-regexp "No more goals"
+  "*Regular expression indicating that the proof has been completed.")
+
+(defconst easycrypt-any-command-regexp
+  ;; allow terminator to be considered as command start:
+  ;; FIXME: really needs change in generic function to take account of this,
+  ;; since the end character of a command is not the start
+  (concat "\\(\\s(\\|\\s)\\|\\sw\\|\\s \\|\\s_\\)*="  ;match assignments
+          "\\|;;\\|;\\|" 
+          (proof-ids-to-regexp easycrypt-global-keywords))
+  "Regexp matching any EasyCrypt command start or the terminator character.")
+
+(defconst easycrypt-keywords-indent-open
+  (append (append '("local") easycrypt-keywords-proof-goal)
+          easycrypt-keywords-code-open))
+
+(defconst easycrypt-keywords-indent-close
+  (append easycrypt-keywords-proof-save
+          easycrypt-keywords-code-close))
+
+(defconst easycrypt-keywords-indent-enclose
+  (append easycrypt-keywords-code-open
+          easycrypt-keywords-code-close
+          easycrypt-keywords-code-end
+          easycrypt-keywords-proof-goal
+          easycrypt-keywords-proof-save))
+
+; Regular expression for indentation
+(defconst easycrypt-indent-any-regexp
+  (proof-regexp-alt easycrypt-any-command-regexp "\\s(" "\\s)"))
+    
+(defconst easycrypt-indent-enclose-regexp
+  (proof-regexp-alt (proof-ids-to-regexp easycrypt-keywords-indent-enclose) "\\s)"))
+
+(defconst easycrypt-indent-open-regexp
+  (proof-regexp-alt (proof-ids-to-regexp easycrypt-keywords-indent-open) "\\s("))
+
+(defconst easycrypt-indent-close-regexp
+  (proof-regexp-alt (proof-ids-to-regexp easycrypt-keywords-indent-close) "\\s)"))
+
+(defface easycrypt-tactics-closing-face
+  (proof-face-specs
+   (:foreground "red")
+   (:foreground "red")
+   ())
+  "Face for names of closing tactics in proof scripts."
+  :group 'proof-faces)
+
+(defface easycrypt-tactics-dangerous-face
+  (proof-face-specs
+   (:background "red")
+   (:background "red")
+   ())
+  "Face for names of dangerous tactics in proof scripts."
+  :group 'proof-faces)
+
+(defface easycrypt-tactics-tacticals-face
+  (proof-face-specs
+   (:foreground "dark green")
+   (:foreground "dark green")
+   ())
+  "Face for names of tacticals in proof scripts."
+  :group 'proof-faces)
+
+(defconst easycrypt-tactics-closing-face   'easycrypt-tactics-closing-face)
+(defconst easycrypt-tactics-dangerous-face 'easycrypt-tactics-dangerous-face)
+(defconst easycrypt-tactics-tacticals-face 'easycrypt-tactics-tacticals-face)
+
+(defvar easycrypt-font-lock-keywords
+  (list
+    (cons (proof-ids-to-regexp easycrypt-global-keywords)    'font-lock-keyword-face)
+    (cons (proof-ids-to-regexp easycrypt-tactic-keywords)    'proof-tactics-name-face)
+    (cons (proof-ids-to-regexp easycrypt-tactical-keywords)  'easycrypt-tactics-tacticals-face)
+    (cons (proof-ids-to-regexp easycrypt-bytac-keywords)     'easycrypt-tactics-closing-face)
+    (cons (proof-ids-to-regexp easycrypt-dangerous-keywords) 'easycrypt-tactics-dangerous-face)
+    (cons (proof-ids-to-regexp easycrypt-prog-keywords)      'font-lock-keyword-face)
+    (cons (concat easycrypt-operator-char-1234 "+")          'font-lock-type-face)
+    (cons easycrypt-other-symbols                            'font-lock-type-face)))
+
+(defun easycrypt-init-syntax-table ()
+  "Set appropriate values for syntax table in current buffer."
+  (modify-syntax-entry ?\$ ".")
+  (modify-syntax-entry ?\/ ".")
+  (modify-syntax-entry ?\\ ".")
+  (modify-syntax-entry ?+  ".")
+  (modify-syntax-entry ?-  ".")
+  (modify-syntax-entry ?=  ".")
+  (modify-syntax-entry ?%  ".")
+  (modify-syntax-entry ?<  ".")
+  (modify-syntax-entry ?>  ".")
+  (modify-syntax-entry ?\& ".")
+  (modify-syntax-entry ?_  "_")
+  (modify-syntax-entry ?\' "_")
+  (modify-syntax-entry ?\| ".")
+  (modify-syntax-entry ?\. ".")
+  (modify-syntax-entry ?\* ". 23n")
+  (modify-syntax-entry ?\( "()1")
+  (modify-syntax-entry ?\) ")(4"))
+
+(provide 'easycrypt-syntax)
diff --git a/easycrypt/easycrypt.el b/easycrypt/easycrypt.el
new file mode 100644
index 00000000..81e3299c
--- /dev/null
+++ b/easycrypt/easycrypt.el
@@ -0,0 +1,258 @@
+(require 'proof)
+(require 'pg-custom)
+(require 'easycrypt-syntax)
+(require 'easycrypt-hooks)
+(require 'easycrypt-abbrev)
+
+(add-to-list 'hs-special-modes-alist
+  '(easycrypt-mode "{" "}" "/[*/]" nil nil))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-load-path-safep (path)
+  (and
+   (listp path)
+   (every (lambda (entry) (stringp entry)) path)))
+
+;; --------------------------------------------------------------------
+(defcustom easycrypt-prog-name "easycrypt"
+  "*Name of program to run EasyCrypt."
+  :type  'file
+  :group 'easycrypt)
+
+(defcustom easycrypt-load-path nil
+  "Non-standard EasyCrypt library load path.
+This list specifies the include path for EasyCrypt. The elements of
+this list are strings."
+  :type  '(repeat (string :tag "simple directory (-I)"))
+  :safe  'easycrypt-load-path-safep
+  :group 'easycrypt)
+
+(defcustom easycrypt-web-page
+  "http://www.easycrypt.info/"
+  "URL of web page for EasyCrypt."
+  :type  'string
+  :group 'easycrypt-config)
+
+;; --------------------------------------------------------------------
+(defun easycrypt-option-of-load-path-entry (entry)
+  (list "-I" (expand-file-name entry)))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-include-options ()
+  (let ((result nil))
+    (when easycrypt-load-path
+      (dolist (entry easycrypt-load-path)
+        (setq result (append result (easycrypt-option-of-load-path-entry entry)))))
+    result))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-build-prog-args ()
+  (delete "-emacs" easycrypt-prog-args)
+  (push "-emacs" easycrypt-prog-args))
+
+(easycrypt-build-prog-args)
+
+;; --------------------------------------------------------------------
+(defun easycrypt-prog-args ()
+  (message "%s" easycrypt-load-path)
+  (append easycrypt-prog-args (easycrypt-include-options)))
+
+;; --------------------------------------------------------------------
+;; Generic mode
+
+(defun easycrypt-config ()
+  "Configure Proof General scripting for EasyCrypt."
+  (easycrypt-init-output-syntax-table)
+  
+  (setq  proof-terminal-string                 easycrypt-terminal-string)
+  (setq  proof-script-command-end-regexp       easycrypt-command-end-regexp)
+
+  (setq  proof-script-comment-start            "(*"
+         proof-script-comment-end              "*)")
+  
+  ;; For undo
+  (setq  proof-find-and-forget-fn              'easycrypt-find-and-forget
+         proof-completed-proof-behaviour       nil
+         proof-non-undoables-regexp            easycrypt-non-undoables-regexp
+         proof-shell-restart-cmd               "pragma restart. ")
+
+  (set (make-local-variable 'comment-quote-nested) nil)
+
+  ;; For func-menu and finding goal...save regions
+  (setq  proof-save-command-regexp             easycrypt-proof-save-regexp
+         proof-really-save-command-p           'easycrypt-save-command-p
+         proof-save-with-hole-regexp           nil
+         proof-goal-command-p                  'easycrypt-goal-command-p
+         proof-goal-with-hole-regexp           easycrypt-goal-command-regexp
+         proof-goal-with-hole-result           1)
+
+  (setq  proof-goal-command                    "lemma %s: ."
+         proof-save-command                    "qed.")
+  
+  (setq  proof-prog-name                       easycrypt-prog-name
+         proof-assistant-home-page             easycrypt-web-page)
+
+  ; Options
+  (setq  proof-three-window-enable             t
+         proof-three-window-mode-policy        (quote hybrid)
+         proof-auto-multiple-files             t)
+
+  ; Setting indents 
+  (set   (make-local-variable 'indent-tabs-mode) nil)
+  (setq  proof-indent-enclose-offset   (- proof-indent)
+         proof-indent-open-offset     0
+         proof-indent-close-offset    0
+         proof-indent-any-regexp      easycrypt-indent-any-regexp
+         proof-indent-enclose-regexp  easycrypt-indent-enclose-regexp
+         proof-indent-open-regexp     easycrypt-indent-open-regexp
+         proof-indent-close-regexp    easycrypt-indent-close-regexp)
+
+  ; Silent/verbose mode for batch processing
+  (setq proof-shell-start-silent-cmd "pragma silent. "
+        proof-shell-stop-silent-cmd  "pragma verbose. ")
+
+  ; Ask for the current goal
+  (setq proof-showproof-command "pragma noop. ")
+
+  (easycrypt-init-syntax-table)
+  ;; we can cope with nested comments
+  (set (make-local-variable 'comment-quote-nested) nil)
+
+  (setq  proof-script-font-lock-keywords
+         easycrypt-font-lock-keywords))
+
+(defun easycrypt-shell-config ()
+  "Configure Proof General shell for EasyCrypt."
+  (easycrypt-init-output-syntax-table)
+  (setq  proof-shell-auto-terminate-commands    easycrypt-terminal-string)
+  (setq  proof-shell-eager-annotation-start
+     (concat "\\(?:^\\[W\\] *\\)\\|\\(?:" easycrypt-shell-proof-completed-regexp "\\)"))
+  (setq  proof-shell-strip-crs-from-input       nil)
+  (setq  proof-shell-annotated-prompt-regexp    "^\\[[0-9]+|\\sw+\\]>")
+  (setq  proof-shell-clear-goals-regexp         easycrypt-shell-proof-completed-regexp)
+  (setq  proof-shell-proof-completed-regexp     easycrypt-shell-proof-completed-regexp)
+  (setq  proof-shell-error-regexp               easycrypt-error-regexp)
+  (setq  proof-shell-truncate-before-error      nil)
+  (setq  proof-shell-start-goals-regexp         "^Current")
+  (setq  proof-shell-end-goals-regexp           nil)  ; up to next prompt
+  (setq  proof-shell-font-lock-keywords         easycrypt-font-lock-keywords))
+
+;; --------------------------------------------------------------------
+;; Derived modes
+
+(define-derived-mode easycrypt-mode proof-mode
+  "EasyCrypt script" nil
+  (easycrypt-config)
+  (proof-config-done))
+
+(define-derived-mode easycrypt-shell-mode proof-shell-mode
+  "EasyCrypt shell" nil
+  (easycrypt-shell-config)
+  (proof-shell-config-done))
+
+(define-derived-mode easycrypt-response-mode proof-response-mode
+  "EasyCrypt response" nil
+  (easycrypt-init-output-syntax-table)
+  (setq  proof-response-font-lock-keywords 
+         easycrypt-font-lock-keywords)
+  (proof-response-config-done))
+
+(define-derived-mode easycrypt-goals-mode proof-goals-mode
+  "EasyCrypt goals" nil
+  (easycrypt-init-output-syntax-table)
+  (setq  proof-goals-font-lock-keywords 
+         easycrypt-font-lock-keywords)
+  (proof-goals-config-done))
+
+(defun easycrypt-get-last-error-location () 
+  "Remove [error] in the error message and extract the position
+  and length of the error "
+  (proof-with-current-buffer-if-exists proof-response-buffer
+
+     (goto-char (point-max))
+     (when (re-search-backward "\\[error-\\([0-9]+\\)-\\([0-9]+\\)\\]" nil t)
+        (let* ((inhibit-read-only t)
+               (pos1 (string-to-number (match-string 1)))
+               (pos2 (string-to-number (match-string 2)))
+               (len (- pos2 pos1)))
+
+              (delete-region (match-beginning 0) (match-end 0))
+              (list pos1 len)))))
+
+(defun easycrypt-advance-until-command ()
+   (while (proof-looking-at "\\s-") (forward-char 1)))
+
+(defun easycrypt-highlight-error ()
+  "Use 'easycrypt-get-last-error-location' to know the position
+  of the error and then highlight in the script buffer"
+  (proof-with-current-buffer-if-exists proof-script-buffer
+    (let ((mtch (easycrypt-get-last-error-location)))
+        (when mtch
+          (let ((pos (car mtch))
+                  (lgth (cadr mtch)))
+          (if (eq (proof-unprocessed-begin) (point-min))
+                (goto-char (proof-unprocessed-begin))
+                (goto-char (+ (proof-unprocessed-begin) 1)))
+            (easycrypt-advance-until-command)
+             (goto-char (+ (point) pos))
+             (span-make-self-removing-span
+               (point) (+ (point) lgth)
+               'face 'proof-script-highlight-error-face))))))
+
+(defun easycrypt-highlight-error-hook ()
+  (easycrypt-highlight-error))
+
+(defun easycrypt-redisplay-hook ()
+  (easycrypt-redisplay))
+
+(add-hook 'proof-shell-handle-error-or-interrupt-hook
+          'easycrypt-highlight-error-hook t)
+
+;; --------------------------------------------------------------------
+;; Check mode related commands
+(defun easycrypt-cmode-check ()
+  "Set EasyCrypt in check mode."
+  (interactive)
+  (proof-shell-invisible-command "pragma Proofs:check."))
+
+(defun easycrypt-cmode-weak-check ()
+  "Set EasyCrypt in weak-check mode."
+  (interactive)
+  (proof-shell-invisible-command "pragma Proofs:weak."))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-ask-do (do)
+  (let* ((cmd))
+    (setq cmd (read-string (format "Term for `%s': " do)))
+    (proof-shell-ready-prover)
+    (proof-shell-invisible-command (format " %s %s . " do cmd))))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-Print ()
+  "Ask for a term and print its type."
+  (interactive)
+  (easycrypt-ask-do "print"))
+
+;; --------------------------------------------------------------------
+(defun easycrypt-Check ()
+  (easycrypt-Print))
+
+;; --------------------------------------------------------------------
+;; Key bindings
+
+(define-key easycrypt-keymap "\C-p" 'easycrypt-Print)
+(define-key easycrypt-goals-mode-map "\C-c\C-a\C-p" 'easycrypt-Print)
+(define-key easycrypt-response-mode-map "\C-c\C-a\C-p" 'easycrypt-Print)
+
+(define-key easycrypt-keymap "\C-c" 'easycrypt-Check)
+(define-key easycrypt-goals-mode-map "\C-c\C-a\C-c" 'easycrypt-Check)
+(define-key easycrypt-response-mode-map "\C-c\C-a\C-c" 'easycrypt-Check)
+
+;; --------------------------------------------------------------------
+;; 3-window pane layout hack
+(add-hook
+  'proof-activate-scripting-hook
+  '(lambda () (when proof-three-window-enable (proof-layout-windows))))
+
+;; --------------------------------------------------------------------
+(provide 'easycrypt)