From 3b4ce4f34c41a0a588cbb02e69a728d296b75359 Mon Sep 17 00:00:00 2001 From: Enrico Tassi 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> (* → *); 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> (* → *); 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