Generic monadic indentation + specifically ext-lib / Compcert + doc.

This a generalization of PR#451 proposed by @Chobbes.

Since these syntax are not completely universal (and not builtin in
coq), the idea is to make the syntax customizable, especially to make
it possible to disable it.

NOTE: to make the Compcert syntax supported I had to refine the smie
lexer so that the ";" token was emitted as a fllback instead of ";
tactic".

NOTE2: I had to make the coq-user-token and coq-monadic-tokens be
tested ON THE RESULT of smie-coq-backward-token.

2 files changed, 68 insertions, 0 deletions

diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 43fcd9ac..e93616c8 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -5,6 +5,30 @@ Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
 
 Require Import Arith.
 
+Definition arith1:
+  1 + 3 *
+      4.
+
+Definition arith2 :=
+  1 * 3 +
+  4.
+
+Definition logic1 :=
+  True \/ False /\
+          False.
+
+Definition logic2 :=
+  True /\ False \/
+  False.
+
+Definition logic3 :=
+  let x := True /\ False in True \/
+                            False .
+Definition logic4 :=
+  (let x := True /\ False in True) \/
+  False .
+
+
 Record a : Type := make_a {
                        aa : nat
                      }.
diff --git a/coq/ex/indent_monadic.v b/coq/ex/indent_monadic.v
new file mode 100644
index 00000000..3a3961fd
--- /dev/null
+++ b/coq/ex/indent_monadic.v
@@ -0,0 +1,44 @@
+(* Needs ext-lib library to compile. *)
+
+Require Import Coq.ZArith.ZArith_base Coq.Strings.Ascii Coq.Strings.String.
+Require Import ExtLib.Data.Monads.StateMonad ExtLib.Structures.Monads.
+Import StringSyntax.
+Open Scope string_scope.
+Section StateGame.
+  
+  Check Ascii.Space.
+
+  Import MonadNotation.
+  Local Open Scope Z_scope.
+  Local Open Scope char_scope.
+  Local Open Scope monad_scope.
+
+  Definition GameValue : Type := Z.
+  Definition GameState : Type := (prod bool Z).
+
+  Variable m : Type -> Type.
+  Context {Monad_m: Monad m}.
+  Context {State_m: MonadState GameState m}.
+
+  Print Grammar constr.
+
+  Fixpoint playGame (s: string) m' {struct s}: m GameValue :=
+    match s with
+    |  EmptyString =>
+       v <- (if true then m' else get) ;;
+       let '(on, score) := v in ret score
+    |  String x xs =>
+       v <- get ;;
+       let '(on, score) := v in
+       match x, on with
+       | "a"%char, true =>  put (on, score + 1)
+       | "b"%char, true => put (on, score - 1)
+       | "c"%char, _ =>   put (negb on, score)
+       |  _, _  =>    put (on, score)
+       end ;;
+       playGame xs m'
+    end.
+
+  Definition startState: GameState := (false, 0).
+
+End StateGame.