From b5334adddde4e222b58288e66096724026e74d24 Mon Sep 17 00:00:00 2001
From: Zhicheng HUI <huizhicheng123@gmail.com>
Date: Tue, 13 Aug 2024 15:40:16 +0200
Subject: [PATCH] allow nicer symbols to be parsed

---
 src/annot/spec.ml          | 24 ++++++++++++------------
 src/parser/text_parser.mly |  2 +-
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/annot/spec.ml b/src/annot/spec.ml
index 78dd50966..870b142f3 100644
--- a/src/annot/spec.ml
+++ b/src/annot/spec.ml
@@ -307,7 +307,7 @@ let rec parse_prop =
   | Atom "true" -> ok @@ Const true
   | Atom "false" -> ok @@ Const false
   (* BinPred *)
-  | List [ Atom ">="; tm1; tm2 ] ->
+  | List [ Atom (">=" | "≥"); tm1; tm2 ] ->
     let* tm1 = parse_term tm1 in
     let+ tm2 = parse_term tm2 in
     BinPred (Ge, tm1, tm2)
@@ -315,7 +315,7 @@ let rec parse_prop =
     let* tm1 = parse_term tm1 in
     let+ tm2 = parse_term tm2 in
     BinPred (Gt, tm1, tm2)
-  | List [ Atom "<="; tm1; tm2 ] ->
+  | List [ Atom ("<=" | "≤"); tm1; tm2 ] ->
     let* tm1 = parse_term tm1 in
     let+ tm2 = parse_term tm2 in
     BinPred (Le, tm1, tm2)
@@ -327,46 +327,46 @@ let rec parse_prop =
     let* tm1 = parse_term tm1 in
     let+ tm2 = parse_term tm2 in
     BinPred (Eq, tm1, tm2)
-  | List [ Atom "!="; tm1; tm2 ] ->
+  | List [ Atom ("!=" | "≠"); tm1; tm2 ] ->
     let* tm1 = parse_term tm1 in
     let+ tm2 = parse_term tm2 in
     BinPred (Neq, tm1, tm2)
   (* UnConnect *)
-  | List [ Atom "!"; pr1 ] ->
+  | List [ Atom ("!" | "¬"); pr1 ] ->
     let+ pr1 = parse_prop pr1 in
     UnConnect (Not, pr1)
   (* BinConnect *)
-  | List [ Atom "&&"; pr1; pr2 ] ->
+  | List [ Atom ("&&" | "∧"); pr1; pr2 ] ->
     let* pr1 = parse_prop pr1 in
     let+ pr2 = parse_prop pr2 in
     BinConnect (And, pr1, pr2)
-  | List [ Atom "||"; pr1; pr2 ] ->
+  | List [ Atom ("||" | "∨"); pr1; pr2 ] ->
     let* pr1 = parse_prop pr1 in
     let+ pr2 = parse_prop pr2 in
     BinConnect (Or, pr1, pr2)
-  | List [ Atom "==>"; pr1; pr2 ] ->
+  | List [ Atom ("==>" | "⇒"); pr1; pr2 ] ->
     let* pr1 = parse_prop pr1 in
     let+ pr2 = parse_prop pr2 in
     BinConnect (Imply, pr1, pr2)
-  | List [ Atom "<==>"; pr1; pr2 ] ->
+  | List [ Atom ("<==>" | "⇔"); pr1; pr2 ] ->
     let* pr1 = parse_prop pr1 in
     let+ pr2 = parse_prop pr2 in
     BinConnect (Equiv, pr1, pr2)
   (* Binder *)
-  | List [ Atom "forall"; bt; pr1 ] ->
+  | List [ Atom ("forall" | "∀"); bt; pr1 ] ->
     let* bt = parse_binder_type bt in
     let+ pr1 = parse_prop pr1 in
     Binder (Forall, bt, None, pr1)
-  | List [ Atom "forall"; bt; Atom ind; pr1 ] ->
+  | List [ Atom ("forall" | "∀"); bt; Atom ind; pr1 ] ->
     let* bt = parse_binder_type bt in
     let* ind = parse_text_id_result ind in
     let+ pr1 = parse_prop pr1 in
     Binder (Forall, bt, Some ind, pr1)
-  | List [ Atom "exists"; bt; pr1 ] ->
+  | List [ Atom ("exists" | "∃"); bt; pr1 ] ->
     let* bt = parse_binder_type bt in
     let+ pr1 = parse_prop pr1 in
     Binder (Exists, bt, None, pr1)
-  | List [ Atom "exists"; bt; Atom ind; pr1 ] ->
+  | List [ Atom ("exists" | "∃"); bt; Atom ind; pr1 ] ->
     let* bt = parse_binder_type bt in
     let* ind = parse_text_id_result ind in
     let+ pr1 = parse_prop pr1 in
diff --git a/src/parser/text_parser.mly b/src/parser/text_parser.mly
index 8110d1e92..228b0d6be 100644
--- a/src/parser/text_parser.mly
+++ b/src/parser/text_parser.mly
@@ -1008,7 +1008,7 @@ let inline_module_inner ==
       | Ok annots -> annots
       | _ -> []
     in
-    let () = Fmt.(pr "%a\n" (list pp_annot) annots) in
+    let () = Fmt.(pr "%a" (list pp_annot) annots) in
     { id; fields; annots }
   }