rewrite emacs SMIE grammar

editors/emacs/lambdapi-smie.el

@@ -74,115 +74,122 @@ Indent by `lambdapi-indent-basic' in proofs, and 0 otherwise."
 
 (defconst lambdapi-smie-bnf
   '((ident)
-      (env (ident)
-           (ident ","))
-      (rw-patt)
-      (args (ident)
-            ("{" ident ":" sterm "}")
-            ("(" ident ":" sterm ")"))
-      (sterm ("TYPE")
-             ("_")
-             (ident)
-             ("?" ident "[" env "]")    ; ?M[x;y;z]
-             ("$" ident "[" env "]")    ; $X[x;y;z]
-             ("`" ident args "," sterm) ; quantifier syntax
-             (sterm "→" sterm)
-             ("λ" args "," sterm)
-             ("λ" ident ":" sterm "," sterm)
-             ("Π" args "," sterm)
-             ("Π" ident ":" sterm "," sterm)
-             ("let" ident "≔" sterm "in" sterm)
-             ("let" ident ":" sterm "≔" sterm "in" sterm)
-             ("let" args ":" sterm "≔" sterm "in" sterm)
-             ("let" args "≔" sterm "in" sterm))
-      (tactic ("apply" sterm)
-              ("assume" sterm)
-              ("change" sterm)
-              ("eval" sterm)
-              ("fail")
-              ("focus" ident)
-              ("generalize" ident)
-              ("have" ident ":" sterm)
-              ("induction")
-              ("orelse" tactic)
-              ("refine" sterm)
-              ("reflexivity")
-              ("remove" ident)
-              ("repeat" tactic)
-              ("rewrite" "[" rw-patt "]")
-              ("set" ident "≔" sterm)
-              ("simplify")
-              ("simplify" ident)
-              ("simplify" "rule" "off")
-              ("solve")
-              ("symmetry")
-              ("try" tactic)
-              ("why3"))
-      (query ("assert" args "⊢" sterm ":" sterm)
-             ("assert" args "⊢" sterm "≡" sterm)
-             ("assertnot" args "⊢" sterm ":" sterm)
-             ("assertnot" args "⊢" sterm "≡" sterm)
-             ("compute" sterm)
-             ("print")
-             ("proofterm")
-             ("search" sterm)
-             ("type" sterm))
-      (prfcontent (tactic)
-                  (query))
-      (unif-rule-rhs
-       (sterm "≡" sterm)
-       ("[" unif-rule-rhs "]")
-       (unif-rule-rhs ";"))
-      (symdec ("symbol" args ":" sterm))
-      (indcons (args ":" sterm) ("|" args ":" sterm))
-      (inddec (inddec "with" args ":" sterm "≔" indcons))
-      (rules (rules "with" sterm "↪" sterm))
-      (command
-               ("begin" prfcontent "abort" ";")
-               ("begin" prfcontent "admitted" ";")
-               ("begin" prfcontent "end" ";")
-               ("builtin" ident "≔" sterm ";")
-               ("debug" ident)
-               ("constant" symdec ";")
-               ("flag" ident "off")
-               ("flag" ident "on")
-               ("injective" "inductive" inddec ";")
-               ("injective" symdec ";")
-               ("associative" symdec ";")
-               ("commutative" symdec ";")
-               ("notation" ident "infix" "left" sterm ";")
-               ("notation" ident "infix" "right" sterm ";")
-               ("notation" ident "infix" sterm ";")
-               ("notation" ident "prefix" sterm ";")
-               ("notation" ident "postfix" sterm ";")
-               ("notation" ident "quantifier" ";")
-               ("open" ident ";")
-               ("opaque" "inductive" inddec ";")
-               ("opaque" symdec ";")
-               ("private" "inductive" inddec ";")
-               ("private" symdec ";")
-               ("private" "open" ident ";")
-               ("protected" "inductive" inddec ";")
-               ("protected" symdec ";")
-               ("prover" ident)
-               ("prover_timeout" ident)
-               ("require" ident "as" ident ";")
-               ("require" ident ";")
-               ("rule" rules ";")
-	       ("coerce_rule" sterm "↪" sterm ";")
-               ("verbose" ident)
-               (query ";")
-               ("unif_rule" sterm "≡" sterm "↪" unif-rule-rhs ";")
-               (symdec ";")))
-)
+    (env (ident)
+         (env ";" env))
+    (rw-patt)
+    (args (ident)
+          ("{" ident ":" term "}")
+          ("(" ident ":" term ")"))
+    (term ("TYPE")
+          ("_")
+          (ident)
+          ("?" ident "[" env "]")
+          ("$" ident "[" env "]")
+          ("`" ident args "," term)
+          (term "→" term)
+          ("λ" args "," term)
+          ("λ" ident ":" term "," term)
+          ("Π" args "," term)
+          ("Π" ident ":" term "," term)
+          ("let" ident "≔" term "in" term)
+          ("let" ident ":" term "≔" term "in" term)
+          ("let" args ":" term "≔" term "in" term)
+          ("let" args "≔" term "in" term))
+    (option ("on") ("off"))
+    (equation (term "≡" term))
+    (typing (term ":" term))
+    (assert (equation) (typing))
+    (query ("assert" args "⊢" assert)
+           ("assertnot" args "⊢" assert)
+           ("compute" term)
+           ("debug" ident)
+           ("flag" ident option)
+           ("print")
+           ("proofterm")
+           ("prover" ident)
+           ("prover_timeout" ident)
+           ("search" term)
+           ("type" term)
+           ("verbose" ident))
+    (tactic (query)
+            ("apply" term)
+            ("assume" term)
+            ("change" term)
+            ("eval" term)
+            ("fail")
+            ("focus" ident)
+            ("generalize" ident)
+            ("have" ident ":" term)
+            ("induction")
+            ("orelse" tactic)
+            ("refine" term)
+            ("reflexivity")
+            ("remove" ident)
+            ("repeat" tactic)
+            ("rewrite" "[" rw-patt "]")
+            ("set" ident "≔" term)
+            ("simplify")
+            ("simplify" ident)
+            ("simplify" "rule" "off")
+            ("solve")
+            ("symmetry")
+            ("try" tactic)
+            ("why3"))
+    (proof (tactic) (tactic ";" tactic))
+    (modifier ("associative")
+              ("commutative")
+              ("constant")
+              ("injective")
+              ("opaque")
+              ("private")
+              ("protected")
+              ("sequential"))
+    (modifiers (modifier modifiers))
+    (constructor (args ":" term))
+    (constructors (constructor) (constructors "|" constructors))
+    (inductive (ident args ":" term "≔" constructors))
+    (inductives (inductive) (inductives "with" inductives))
+    (rule (term "↪" term))
+    (rules (rule) (rules "with" rules))
+    (side ("left")
+          ("right"))
+    (notation (infix term)
+              (infix side term)
+              ("prefix" term)
+              ("postfix" term)
+              ("quantifier"))
+    (proofend ("abort") ("admitted") ("end"))
+    (definition ("≔" term)
+                ("≔" term "begin" proof proofend))
+    (unif-rule-rhs (equation) (unif-rule-rhs ";" unif-rule-rhs))
+    (reqopen ("require" ident)
+             ("require" ident "as" iden)
+             ("require" "open" ident)
+             ("require" "private" "open" ident)
+             ("open" ident)
+             ("private" "open" ident))
+    (command (reqopen)
+             (query)
+             (modifiers "symbol" args ":" term)
+             (modifiers "symbol" args ":" term definition)
+             (modifiers "inductive" inductive)
+             ("notation" ident notation)
+             ("builtin" ident "≔" term)
+             ("rule" rules)
+             ("coerce_rule" rule)
+             ("unif_rule" equation "↪" "[" unif-rule-rhs "]"))
+    (commands (command) (commands ";" commands))
+    )
+  )
 
 (defconst lambdapi--smie-prec
   (smie-prec2->grammar
    (smie-bnf->prec2
     lambdapi-smie-bnf
-    '((assoc ";") (assoc "≔"))
-    '((assoc ";") (assoc "↪"))
-    '((assoc "≡") (assoc ",") (assoc "in") (assoc "→")))))
+    '((assoc ";"))
+    '((assoc "with"))
+    '((assoc ","))
+    '((assoc "→")))))
 
 (defun lambdapi--smie-forward-token ()
   "Forward lexer for Dedukti3."