fixed precedence of \to

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 8e02154ab994c1fcffb0626fdd6e9a93a06f135f..431b15ae83d807617aeef459fbec3d9e621ac068 100644 (file)
--- 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 f0a91418d3f64c24a3861a23a14eaa5e68a071d9..cd7186fcf6a3ace26de12020692f93bf5b024d9a 100644 (file)
--- 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 31bcdad054e19763f646e09527a5455c63ee80f5..3b30e59001dd35aba70508c6ecdf4ce2b5adebe3 100644 (file)
--- 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