                 "effect" "new_effect" "sub_effect")
               'symbols))
 
+(defconst fstar-syntax-types
+  (regexp-opt '("Type")
+              'symbols))
+
 (defconst fstar-syntax-constants
   (regexp-opt '("False" "True")
               'symbols))
 
+(defface fstar-structure-face
+  '((((background light)) (:bold t))
+    (t :bold t :foreground "salmon"))
+  "Face used to highlight structural keywords."
+  :group 'fstar)
+
 (defface fstar-subtype-face
+  '((t :inherit font-lock-type-face :italic t))
+  "Face used to highlight subtyping clauses."
+  :group 'fstar)
+
+(defface fstar-attribute-face
   '((t :italic t))
   "Face used to highlight subtyping clauses."
   :group 'fstar)
 
-(defface fstar-subtype-brace-face
-  '((t :bold t))
-  "Face used to highlight braces around subtyping clauses."
+(defface fstar-decreases-face
+  '((t :italic t))
+  "Face used to highlight subtyping clauses."
   :group 'fstar)
 
+(defvar-local should-cancel-match nil)
+
 (defun fstar-group-pre-matcher (prefix-len allowed-newlines)
-  (backward-char prefix-len)
-  (min (save-excursion
-         (forward-sexp)
-         (point))
-       (save-excursion
-         (forward-line allowed-newlines)
-         (point-at-eol))))
+  "Prepare for highlighting.
+
+Go back PREFIX-LEN chars, skip one sexp forward without moving
+point and report that position; point is placed at beginning of
+original match. If ALLOWED-NEWLINES is non-nil, then allow the
+sexp to span at most that many extra lines."
+  (prog1
+      (min (save-excursion
+             (backward-char prefix-len)
+             (forward-sexp)
+             (point))
+           (save-excursion
+             (forward-line (or allowed-newlines 0))
+             (point-at-eol)))
+    (goto-char (match-beginning 0))))
+
+(defun fstar-subexpr-pre-matcher (rewind-to &optional bound-to)
+  (goto-char (match-end rewind-to))
+  (match-end (or bound-to 0)))
+
+(defconst fstar-syntax-id (rx (? (or "#" "'"))
+                              symbol-start
+                              letter (* (or wordchar (syntax symbol)))
+                              (? "." (* (or wordchar (syntax symbol))))
+                              symbol-end))
+
+(defconst fstar-syntax-cs (rx symbol-start
+                              (any "A-Z") (* (or wordchar (syntax symbol)))
+                              (? ".v")
+                              symbol-end))
+
+(defun fstar-find-id-with-type (bound)
+  (let ((start (point)) (found t) (rejected t))
+    (while (and found rejected)
+      (setq found (re-search-forward (concat "\\(" fstar-syntax-id "\\) *:") bound t))
+      (setq rejected (and found (or (eq (char-after) ?:)
+                                    (save-excursion
+                                      (goto-char (match-beginning 0))
+                                      (skip-syntax-backward "-")
+                                      (or (eq (char-before) ?|)
+                                          (save-match-data
+                                            (looking-back "\\_<val" start))))))))
+    found))
+
+(defun fstar-id-with-type-pre-matcher ()
+  (or (save-excursion
+        (ignore-errors
+          (goto-char (match-beginning 0))
+          (skip-syntax-backward "-")
+          (when (eq (char-before) ?\()
+            (up-list)
+            (point))))
+      (save-excursion
+        (forward-sexp)
+        (point))))
+
+(defun fstar-find-fun-and-args (bound)
+  (let ((found))
+    (while (and (not found) (re-search-forward "\\_<fun\\_>" bound t))
+      (-when-let* ((mdata (match-data))
+                   (fnd   (search-forward "->" bound t)))
+        (set-match-data `(,(car mdata) ,(match-end 0)
+                          ,@mdata))
+        (setq found t)))
+    found))
+
+(defun fstar-find-subtype-annotation (bound)
+  (let ((found))
+    (while (and (not found) (re-search-forward "{[^:]" bound t))
+      (setq found
+            (save-excursion
+              (backward-char)
+              (not (looking-at-p "[^ ]+ +with")))))
+    found))
 
 (defconst fstar-syntax-additional
-  '(("{" ("\\({\\)\\(\\(?:.\\|\n\\)+\\)\\(}\\)"
-          (fstar-group-pre-matcher 1 2)
-          nil
-          (1 'fstar-subtype-brace-face append)
-          (2 'fstar-subtype-face append)
-          (3 'fstar-subtype-brace-face append)))
-    ("%\\[" ("\\(%\\[\\)\\(.+\\)\\(\\]\\)"
-            (fstar-group-pre-matcher 2 0)
-            nil
-            (1 'fstar-subtype-brace-face append)
-            (2 'fstar-subtype-face append)
-            (3 'fstar-subtype-brace-face append)))))
+  (let ((id fstar-syntax-id))
+    `((fstar-find-subtype-annotation
+       ("\\({\\)\\(\\(?:.\\|\n\\)+\\)\\(}\\)"
+        (fstar-group-pre-matcher 2 2) nil
+        (1 'font-lock-type-face append)
+        (2 'fstar-subtype-face append)
+        (3 'font-lock-type-face append)))
+      ("{:" (,(concat "\\({\\)\\(:" id "\\)\\(\\(?: +.+\\)?\\)\\(}\\)")
+             (fstar-group-pre-matcher 2 2) nil
+             (2 'font-lock-function-name-face append)
+             (3 'fstar-attribute-face append)))
+      ("%\\[" ("%\\[\\([^]]+\\)\\]"
+              (fstar-group-pre-matcher 1 0) nil
+              (1 'fstar-decreases-face append)))
+      (,(concat "\\_<\\(let\\(?: +rec\\)?\\)\\(\\(?: +" id "\\)?\\) +[^=]+=")
+       (1 'fstar-structure-face)
+       (2 'font-lock-function-name-face)
+       (,id (fstar-subexpr-pre-matcher 2) nil
+            (0 'font-lock-variable-name-face)))
+      (,(concat "\\_<\\(type\\|kind\\)\\( +" id "\\)[^=]+=")
+       (1 'fstar-structure-face)
+       (2 'font-lock-function-name-face)
+       (,id (fstar-subexpr-pre-matcher 2) nil
+            (0 'font-lock-variable-name-face)))
+      (fstar-find-id-with-type
+       (1 'font-lock-variable-name-face)
+       (,id (fstar-id-with-type-pre-matcher) nil
+            (0 'font-lock-type-face prepend)))
+      ("\\(forall\\|exists\\) [^.]+\."
+       (0 'font-lock-keyword-face)
+       (,id (fstar-subexpr-pre-matcher 1) nil
+            (0 'font-lock-variable-name-face)))
+      (fstar-find-fun-and-args
+       (1 'font-lock-keyword-face)
+       (,id (fstar-subexpr-pre-matcher 1) nil
+            (0 'font-lock-variable-name-face)))
+      (,(concat "\\_<\\(val\\) +\\(" id "\\) *:")
+       (1 'fstar-structure-face)
+       (2 'font-lock-function-name-face)
+       (,id nil nil
+            (0 'font-lock-type-face)))
+      (,fstar-syntax-cs (0 'font-lock-constant-face)))))
+
+;;; Syntax table
+
+(defvar fstar-syntax-table
+  (let ((table (make-syntax-table)))
+    (modify-syntax-entry ?# "_" table)
+    (modify-syntax-entry ?_ "_" table)
+    (modify-syntax-entry ?' "_" table)
+    (modify-syntax-entry ?\\ "\\" table)
+    (modify-syntax-entry ?\" "\"" table)
+    (modify-syntax-entry ?*  ". 23" table)
+    (modify-syntax-entry ?/  ". 12b" table)
+    (modify-syntax-entry ?\n "> b" table)
+    (modify-syntax-entry ?\( "()1n" table)
+    (modify-syntax-entry ?\) ")(4n" table)
+    table)
+  "Syntax table for F*.")
+
+;;; Indentation
+
+(defun fstar-indentation-points ()
+  "Find reasonable indentation points on the current line."
+  (let ((points)) ;; FIXME first line?
+    (save-excursion
+      (forward-line -1)
+      (while (re-search-forward "\\s-+" (point-at-eol) t)
+        (push (current-column) points)))
+    (when points
+      (push (+ 2 (apply #'min points)) points))
+    (push 0 points)
+    (push 2 points)
+    (-distinct (sort points #'<))))
+
+(defun fstar-indent ()
+  "Cycle between vaguely relevant indentation points."
+  (interactive)
+  (let* ((current-ind (current-indentation))
+         (points      (fstar-indentation-points))
+         (remaining   (-filter (lambda (x) (> x current-ind)) points))
+         (target      (car (or remaining points))))
+    (if (> (current-column) current-ind)
+        (save-excursion (indent-line-to target))
+      (indent-line-to target))))
 
 ;;; fstar-mode
 


;; Copyright (C) 2015 Clément Pit--Claudel
;; Author: Clément Pit--Claudel <clement.pitclaudel@live.com>
;; URL: https://github.com/boogie-org/boogie-friends/

;; Keywords: convenience, languages

;; This file is not part of GNU Emacs.

;; Permission is hereby granted, free of charge, to any person obtaining a copy
;; of this software and associated documentation files (the "Software"), to deal
;; in the Software without restriction, including without limitation the rights
;; to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
;; copies of the Software, and to permit persons to whom the Software is
;; furnished to do so, subject to the following conditions:

;; The above copyright notice and this permission notice shall be included in all
;; copies or substantial portions of the Software.

;; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
;; IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
;; FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
;; AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
;; LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
;; OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
;; SOFTWARE.

;;; Commentary:



(add-to-list 'flycheck-checkers 'fstar)

;;; Prettify symbols

(defconst fstar-symbols-alist '(("exists" . ?∃) ("forall" . ?∀) ("fun" . ?λ)
                                ("nat" . ?ℕ) ("int" . ?ℤ)
                                ("True" . ?⊤) ("False" . ?⊥)
                                ("*" . ?×) ("~>" . ?↝)
                                ("<=" . ?≤) (">=" . ?≥) ("::" . ?⸬)
                                ("/\\" . ?∧) ("\\/" . ?∨) ("=!=" . ?≠)
                                ("&&" . ?∧) ("||" . ?∨) ("<>" . ?≠)
                                ("<==>" . ?⟺) ("==>" . ?⟹)
                                ("=>" . ?⇒) ("->" . ?→)
                                ("'a" . ?α) ("'b" . ?β) ("'c" . ?γ)
                                ("'d" . ?δ) ("'e" . ?η))
  "Fstar symbols.")

;;; font-lock
