From 3b4ce4f34c41a0a588cbb02e69a728d296b75359 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 24 May 2005 13:57:35 +0000
Subject: [PATCH] fixed precedence of \to

---
 .../cic_disambiguation/cicTextualParser2.ml   |  4 +--
 .../cic_disambiguation/doc/precedence.txt     | 16 ++++++++++++
 helm/ocaml/cic_disambiguation/test_parser.ml  | 26 ++++++++++---------
 3 files changed, 32 insertions(+), 14 deletions(-)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 8e02154ab..431b15ae8 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -250,8 +250,6 @@ EXTEND
         b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
           let binder = mk_binder_ast b typ vars body in
           return_term loc binder
-      | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
-          return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
       ]
     | "logic_add" LEFTA   [ (* nothing here by default *) ]
     | "logic_mult" LEFTA  [ (* nothing here by default *) ]
@@ -277,6 +275,8 @@ EXTEND
         b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
           let binder = mk_binder_ast b typ vars body in
           return_term loc binder
+      | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
+          return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
       ]
     | "simple" NONA
       [ sort = sort -> CicAst.Sort sort
diff --git a/helm/ocaml/cic_disambiguation/doc/precedence.txt b/helm/ocaml/cic_disambiguation/doc/precedence.txt
index f0a91418d..cd7186fcf 100644
--- a/helm/ocaml/cic_disambiguation/doc/precedence.txt
+++ b/helm/ocaml/cic_disambiguation/doc/precedence.txt
@@ -14,3 +14,19 @@ Precedence total order:
 
 where binders are all binders except lambda (i.e. \forall, \pi, \exists)
 
+to test:
+  
+./test_parser term << EOT 
+  \lambda x.x y
+  S x = y
+  \forall x.x=x
+  \lambda x.x \to x
+EOT
+  
+should respond with:
+  
+  (\lambda x.x y)
+  (eq (S x) y)
+  \forall x.(eq x x)
+  \lambda x.(x \to x)
+
diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml
index 31bcdad05..3b30e5900 100644
--- a/helm/ocaml/cic_disambiguation/test_parser.ml
+++ b/helm/ocaml/cic_disambiguation/test_parser.ml
@@ -27,16 +27,17 @@ open Printf
 
 let pp_tactical = TacticAst2Box.tacticalPp
 
+let modes = ("term",`Term) :: ("statement",`Statement) :: []
+
 let mode =
   try
-    match Sys.argv.(1) with
-    | "term" -> prerr_endline "Term"; `Term
-    | "statement" -> prerr_endline "Statement"; `Statement
-(*     | "script" -> prerr_endline "Script"; `Script *)
-    | _ ->
-        prerr_endline "What???????";
-        exit 1
-  with Invalid_argument _ -> prerr_endline "Term"; `Term
+    List.assoc (Sys.argv.(1)) modes
+  with 
+  | _ ->
+      prerr_endline 
+        (sprintf "What? Supported modes are: %s\n" 
+          (String.concat " " (List.map fst modes)));
+      exit 1
 
 let _ =
 (*
@@ -63,10 +64,11 @@ let _ =
               print_endline (BoxPp.pp_term term)
           | `Statement ->
               (match CicTextualParser2.parse_statement istream with
-              | TacticAst.Command (_, cmd) ->
-                  print_endline (TacticAstPp.pp_command cmd)
-              | TacticAst.Tactical (_, tac) ->
-                  print_endline (TacticAstPp.pp_tactical tac))
+              | TacticAst.Executable (_, exe) 
+              | TacticAst.Comment (_,TacticAst.Code (_, exe)) ->
+                  print_endline (TacticAstPp.pp_executable exe)
+              | TacticAst.Comment (_,TacticAst.Note (_, note)) ->
+                  print_endline note)
 (*
           | `Tactical ->
               let tac = CicTextualParser2.parse_tactical istream in
-- 
2.39.2