diff options
Diffstat (limited to 'parsing/g_cases.ml4')
| -rw-r--r-- | parsing/g_cases.ml4 | 32 |
1 files changed, 18 insertions, 14 deletions
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4 index a6dcbffe7..65248524e 100644 --- a/parsing/g_cases.ml4 +++ b/parsing/g_cases.ml4 @@ -2,14 +2,16 @@ (* $Id$ *) open Pcoq -open Command +open Constr GEXTEND Gram + GLOBAL : constr1 pattern; + +(* pattern_list: [ [ -> [] | p = pattern; pl = pattern_list -> p :: pl ] ] ; -(* lsimple_pattern: [ [ c = simple_pattern2 -> c ] ] ; @@ -18,16 +20,18 @@ GEXTEND Gram [ [ id = ident -> id | "("; p = lsimple_pattern; ")" -> p ] ] ; +(* simple_pattern_list: [ [ -> [] | p = simple_pattern; pl = simple_pattern_list -> p :: pl ] ] ; +*) lsimple_pattern: [ [ id = ident; lp = ne_pattern_list -> <:ast< (PATTCONSTRUCT $id ($LIST $lp)) >> - | p = pattern; "as"; id = ident -> <:ast< (PATTAS $id $p)>> - | c1 = simple_pattern; ","; c2 = simple_pattern -> + | p = lsimple_pattern; "as"; id = ident -> <:ast< (PATTAS $id $p)>> + | c1 = lsimple_pattern; ","; c2 = lsimple_pattern -> <:ast< (PATTCONSTRUCT pair $c1 $c2) >> | "("; p = lsimple_pattern; ")" -> p ] ] ; @@ -41,7 +45,7 @@ GEXTEND Gram | c1 = pattern -> [c1] ] ] ; equation: - [ [ lhs = ne_pattern_list; "=>"; rhs = command -> + [ [ lhs = ne_pattern_list; "=>"; rhs = constr -> <:ast< (EQN $rhs ($LIST $lhs)) >> ] ] ; ne_eqn_list: @@ -49,17 +53,17 @@ GEXTEND Gram | e = equation -> [e] ] ] ; - command1: - [ [ "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of"; + constr1: + [ [ "<"; l1 = lconstr; ">"; "Cases"; lc = ne_constr_list; "of"; OPT "|"; eqs = ne_eqn_list; "end" -> - <:ast< (MULTCASE $l1 (TOMATCH ($LIST $lc)) ($LIST $eqs)) >> - | "Cases"; lc = ne_command_list; "of"; + <:ast< (CASES $l1 (TOMATCH ($LIST $lc)) ($LIST $eqs)) >> + | "Cases"; lc = ne_constr_list; "of"; OPT "|"; eqs = ne_eqn_list; "end" -> - <:ast< (MULTCASE "SYNTH" (TOMATCH ($LIST $lc)) ($LIST $eqs)) >> - | "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of"; + <:ast< (CASES "SYNTH" (TOMATCH ($LIST $lc)) ($LIST $eqs)) >> + | "<"; l1 = lconstr; ">"; "Cases"; lc = ne_constr_list; "of"; "end" -> - <:ast< (MULTCASE $l1 (TOMATCH ($LIST $lc))) >> - | "Cases"; lc = ne_command_list; "of"; "end" -> - <:ast< (MULTCASE "SYNTH" (TOMATCH ($LIST $lc))) >> ] ] + <:ast< (CASES $l1 (TOMATCH ($LIST $lc))) >> + | "Cases"; lc = ne_constr_list; "of"; "end" -> + <:ast< (CASES "SYNTH" (TOMATCH ($LIST $lc))) >> ] ] ; END; |