From c0dd3e6a0100462e79d40e4dca2df7d9b89afe76 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 18 Feb 2004 14:22:49 +0000 Subject: [PATCH] - bugfix in term grammar: lowered precedence level of "let ... in" so that "let x = 1 in x + 2" works as expected - decent grammar for tactics and tacticals: now with precedence levels (no more stackoverflows, hopefully) --- .../cic_disambiguation/cicTextualParser2.ml | 99 ++++++++++--------- 1 file changed, 51 insertions(+), 48 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 349825bf9..cd1de4487 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -119,7 +119,28 @@ EXTEND ]; term0: [ [ t = term; EOI -> return_term loc t ] ]; term: - [ "binder" RIGHTA + [ "letin" NONA + (* actually "in" and "and" are _not_ keywords. Parsing works anyway + * since applications are required to be bound by parens *) + [ "let"; var = typed_name; + SYMBOL "="; (* SYMBOL <:unicode> (* ≝ *); *) + t1 = term; + IDENT "in"; t2 = term -> + return_term loc (CicAst.LetIn (var, t1, t2)) + | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; + defs = LIST1 [ + var = typed_name; + index = OPT [ PAREN "("; index = NUM; PAREN ")" -> + int_of_string index + ]; + SYMBOL "="; (* SYMBOL <:unicode> (* ≝ *); *) + t1 = term -> + (var, t1, (match index with None -> 0 | Some i -> i)) + ] SEP (IDENT "and"); + IDENT "in"; body = term -> + return_term loc (CicAst.LetRec (ind_kind, defs, body)) + ] + | "binder" RIGHTA [ b = binder; (vars, typ) = @@ -167,27 +188,6 @@ EXTEND fail loc ("Invalid meta variable number: " ^ m) in return_term loc (CicAst.Meta (index, substs)) - (* actually "in" and "and" are _not_ keywords. Parsing works anyway - * since applications are required to be bound by parens *) - | "let"; var = typed_name; -(* SYMBOL <:unicode> (* ≝ *); *) - SYMBOL "="; - t1 = term; - IDENT "in"; t2 = term -> - return_term loc (CicAst.LetIn (var, t1, t2)) - | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; - defs = LIST1 [ - var = typed_name; - index = OPT [ PAREN "("; index = NUM; PAREN ")" -> - int_of_string index - ]; -(* SYMBOL <:unicode> (* ≝ *); *) - SYMBOL "="; - t1 = term -> - (var, t1, (match index with None -> 0 | Some i -> i)) - ] SEP (IDENT "and"); - IDENT "in"; body = term -> - return_term loc (CicAst.LetRec (ind_kind, defs, body)) | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ]; "match"; t = term; indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ]; @@ -203,12 +203,8 @@ EXTEND | PAREN "("; t = term; PAREN ")" -> return_term loc t ] ]; - tactic_where: [ - [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] - ]; - tactic_term: [ - [ t = term -> t ] - ]; + tactic_where: [ [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] ]; + tactic_term: [ [ t = term -> t ] ]; ident_list0: [ [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; @@ -269,26 +265,33 @@ EXTEND ] ]; tactical0 : [ [ t = tactical; SYMBOL "." -> t ] ]; - tactical: [ - [ IDENT "fail" -> return_tactical loc TacticAst.Fail - | IDENT "do"; count = int; tac = tactical -> - return_tactical loc (TacticAst.Do (count, tac)) - | IDENT "id" -> return_tactical loc TacticAst.IdTac - | IDENT "repeat"; tac = tactical -> - return_tactical loc (TacticAst.Repeat tac) - | tactics = LIST0 tactical SEP SYMBOL ";" -> - return_tactical loc (TacticAst.Seq tactics) - | tac = tactical; - PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> - return_tactical loc (TacticAst.Then (tac, tacs)) - | IDENT "tries"; - PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> - return_tactical loc (TacticAst.Tries tacs) - | IDENT "try"; tac = tactical -> return_tactical loc (TacticAst.Try tac) - | tac = tactic -> return_tactical loc (TacticAst.Tactic tac) - | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac - ] - ]; + tactical: + [ "sequence" LEFTA + [ tactics = LIST1 NEXT SEP SYMBOL ";" -> + return_tactical loc (TacticAst.Seq tactics) + ] + | "then" NONA + [ tac = tactical; + PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> + return_tactical loc (TacticAst.Then (tac, tacs)) + ] + | "loops" RIGHTA + [ IDENT "do"; count = int; tac = tactical -> + return_tactical loc (TacticAst.Do (count, tac)) + | IDENT "repeat"; tac = tactical -> + return_tactical loc (TacticAst.Repeat tac) + ] + | "simple" NONA + [ IDENT "tries"; + PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> + return_tactical loc (TacticAst.Tries tacs) + | IDENT "try"; tac = NEXT -> return_tactical loc (TacticAst.Try tac) + | IDENT "fail" -> return_tactical loc TacticAst.Fail + | IDENT "id" -> return_tactical loc TacticAst.IdTac + | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac + | tac = tactic -> return_tactical loc (TacticAst.Tactic tac) + ] + ]; END let parse_term stream = -- 2.39.2