diff options
| -rw-r--r-- | parsing/g_cases.ml4 | 62 | ||||
| -rw-r--r-- | parsing/g_multiple_case.ml4 | 74 |
2 files changed, 62 insertions, 74 deletions
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4 new file mode 100644 index 0000000000..0b45dd3e47 --- /dev/null +++ b/parsing/g_cases.ml4 @@ -0,0 +1,62 @@ + +(* $Id$ *) + +open Pcoq +open Command + +GEXTEND Gram + pattern_list: + [ [ -> [] + | p = pattern; pl = pattern_list -> p :: pl ] ] + ; + lsimple_pattern: + [ [ c = simple_pattern2 -> c ] ] + ; + simple_pattern: + [ [ id = ident -> id + | "("; p = lsimple_pattern; ")" -> p ] ] + ; + simple_pattern_list: + [ [ -> [] + | p = simple_pattern; pl = simple_pattern_list -> + p :: pl ] ] + ; + (* The XTRA"!" means we want to override the implicit arg mecanism of bdize, + since params are not given in patterns *) + simple_pattern2: + [ [ p = simple_pattern; lp = pattern_list -> + <:ast< (PATTCONSTRUCT $p ($LIST $lp)) >> + | p = simple_pattern; "as"; id = ident -> <:ast< (PATTAS $id $p) >> + | c1 = simple_pattern; ","; c2 = simple_pattern -> + <:ast< (PATTCONSTRUCT pair $c1 $c2) >> ] ] + ; + pattern: + [ [ p = simple_pattern -> p ] ] + ; + ne_pattern_list: + [ [ c1 = pattern; cl = ne_pattern_list -> c1 :: cl + | c1 = pattern -> [c1] ] ] + ; + equation: + [ [ lhs = ne_pattern_list; "=>"; rhs = command -> + <:ast< (EQN $rhs ($LIST $lhs)) >> ] ] + ; + ne_eqn_list: + [ [ e = equation; "|"; leqn = ne_eqn_list -> e :: leqn + | e = equation -> [e] ] ] + ; + + command1: + [ [ "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of"; + OPT "|"; eqs = ne_eqn_list; "end" -> + <:ast< (MULTCASE $l1 (TOMATCH ($LIST $lc)) ($LIST $eqs)) >> + | "Cases"; lc = ne_command_list; "of"; + OPT "|"; eqs = ne_eqn_list; "end" -> + <:ast< (MULTCASE "SYNTH" (TOMATCH ($LIST $lc)) ($LIST $eqs)) >> + | "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of"; + "end" -> + <:ast< (MULTCASE $l1 (TOMATCH ($LIST $lc))) >> + | "Cases"; lc = ne_command_list; "of"; "end" -> + <:ast< (MULTCASE "SYNTH" (TOMATCH ($LIST $lc))) >> ] ] + ; +END; diff --git a/parsing/g_multiple_case.ml4 b/parsing/g_multiple_case.ml4 deleted file mode 100644 index 6611911cad..0000000000 --- a/parsing/g_multiple_case.ml4 +++ /dev/null @@ -1,74 +0,0 @@ - -(* $Id$ *) - -open Pcoq - -open Command - -GEXTEND Gram - pattern_list: - [ [ -> ([],[]) - | (id1,p) = pattern; (id2,pl) = pattern_list -> (id1@id2, p::pl) ] ] - ; - lsimple_pattern: - [ [ c = simple_pattern2 -> c ] ] - ; - simple_pattern: - [ [ id = ident -> ([Ast.nvar_of_ast id], id) - | "("; p = lsimple_pattern; ")" -> p ] ] - ; - simple_pattern_list: - [ [ -> ([],[]) - | (id1,p) = simple_pattern; (id2,pl) = simple_pattern_list -> - (id1@id2, p::pl) ] ] - ; - (* The XTRA"!" means we want to override the implicit arg mecanism of bdize, - since params are not given in patterns *) - simple_pattern2: - [ [ (id1,p) = simple_pattern; (id2,lp) = pattern_list -> - (id1@id2, <:ast< (APPLIST (XTRA "!" $p) ($LIST $lp)) >>) - | (id1,p) = simple_pattern; "as"; id = ident -> - ((Ast.nvar_of_ast id)::id1, <:ast< (XTRA"AS" $id $p) >>) - | (id1,c1) = simple_pattern; ","; (id2,c2) = simple_pattern -> - (id1@id2, <:ast< (APPLIST (XTRA "!" pair) $c1 $c2) >>) ] ] - ; - pattern: - [ [ p = simple_pattern -> p ] ] - ; - ne_pattern_list: - [ [ (id1,c1) = pattern; (id2,cl) = ne_pattern_list -> - (id1@id2, c1::cl) - | (id1,c1) = pattern -> (id1,[c1]) ] ] - ; - equation: - [ [ (ids,lhs) = ne_pattern_list; "=>"; rhs = command -> - let br = - List.fold_right (fun s ast -> Coqast.Slam loc (Some s) ast) - ids - <:ast< (XTRA"EQN" $rhs ($LIST $lhs)) >> in - let lid = List.map (fun s -> Coqast.Id loc s) ids in - <:ast< (XTRA"LAMEQN"($LIST $lid) $br) >> ] ] - ; - ne_eqn_list: - [ [ e = equation; "|"; leqn = ne_eqn_list -> e :: leqn - | e = equation -> [e] ] ] - ; - - command1: - [ [ "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of"; - OPT "|"; eqs = ne_eqn_list; "end" -> - <:ast< (XTRA"MULTCASE" $l1 (XTRA"TOMATCH" ($LIST $lc)) - ($LIST $eqs)) >> - | "Cases"; lc = ne_command_list; "of"; - OPT "|"; eqs = ne_eqn_list; "end" -> - <:ast< (XTRA"MULTCASE" (XTRA"SYNTH") - (XTRA"TOMATCH"($LIST $lc)) ($LIST $eqs)) >> - | "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of"; - "end" -> - <:ast< (XTRA"MULTCASE" $l1 (XTRA"TOMATCH" ($LIST $lc))) >> - | "Cases"; lc = ne_command_list; "of"; "end" -> - <:ast< (XTRA"MULTCASE" (XTRA"SYNTH") - (XTRA"TOMATCH"($LIST $lc))) >> ] ] - ; - END - |