diff options
| -rw-r--r-- | parsing/astterm.ml | 8 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 23 | ||||
| -rw-r--r-- | syntax/PPCases.v | 2 | ||||
| -rwxr-xr-x | syntax/PPConstr.v | 41 |
4 files changed, 34 insertions, 40 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index 85bd1a3e5f..45b6b6ae97 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -467,13 +467,13 @@ let ast_to_rawconstr sigma env allow_soapp lvar = List.map (dbrec env) tms, List.map (ast_to_eqn (List.length tms) env) eqns) - | Node(loc,"CASE",Str(_,isrectag)::p::c::cl) -> + | Node(loc,(("CASE"|"IF"|"LET"|"MATCH")as tag), p::c::cl) -> let po = match p with | Str(_,"SYNTH") -> None | _ -> Some(dbrec env p) in - let isrec = match isrectag with - | "REC" -> true | "NOREC" -> false - | _ -> anomaly "ast_to: wrong REC tag in CASE" in + let isrec = match tag with + | "MATCH" -> true | ("LET"|"CASE"|"IF") -> false + | _ -> anomaly "ast_to: wrong tag in old case expression" in ROldCase (loc,isrec,po,dbrec env c, Array.of_list (List.map (dbrec env) cl)) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index ff4a0a7580..56779d71f0 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -92,39 +92,38 @@ GEXTEND Gram [ [ "<"; ":"; IDENT "ast"; ":"; "<"; c = raw_constr; ">>" -> c | "<"; l1 = lconstr; ">"; IDENT "Match"; c = constr; "with"; cl = ne_constr_list; "end" -> - <:ast< (CASE "REC" $l1 $c ($LIST $cl)) >> + <:ast< (MATCH $l1 $c ($LIST $cl)) >> | "<"; l1 = lconstr; ">"; IDENT "Match"; c = constr; "with"; "end" -> - <:ast< (CASE "REC" $l1 $c) >> + <:ast< (MATCH $l1 $c) >> | "<"; l1 = lconstr; ">"; IDENT "Case"; c = constr; "of"; cl = ne_constr_list; "end" -> - <:ast< (CASE "NOREC" $l1 $c ($LIST $cl)) >> + <:ast< (CASE $l1 $c ($LIST $cl)) >> | "<"; l1 = lconstr; ">"; IDENT "Case"; c = constr; "of"; "end" -> - <:ast< (CASE "NOREC" $l1 $c) >> + <:ast< (CASE $l1 $c) >> | IDENT "Case"; c = constr; "of"; cl = ne_constr_list; "end" -> - <:ast< (CASE "NOREC" "SYNTH" $c ($LIST $cl)) >> + <:ast< (CASE "SYNTH" $c ($LIST $cl)) >> | IDENT "Case"; c = constr; "of"; "end" -> - <:ast< (CASE "NOREC" "SYNTH" $c) >> + <:ast< (CASE "SYNTH" $c) >> | IDENT "Match"; c = constr; "with"; cl = ne_constr_list; "end" -> - <:ast< (CASE "REC" "SYNTH" $c ($LIST $cl)) >> + <:ast< (MATCH "SYNTH" $c ($LIST $cl)) >> | IDENT "let"; "("; b = ne_ident_comma_list; ")"; "="; c = constr; "in"; c1 = constr -> - <:ast< (CASE "NOREC" "SYNTH" $c (LAMBDALIST (ISEVAR) - ($SLAM $b $c1))) >> + <:ast< (LET "SYNTH" $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >> | IDENT "let"; id1 = IDENT ; "="; c = constr; "in"; c1 = constr -> <:ast< (LETIN $c [$id1]$c1) >> | IDENT "if"; c1 = constr; IDENT "then"; c2 = constr; IDENT "else"; c3 = constr -> - <:ast< ( CASE "NOREC" "SYNTH" $c1 $c2 $c3) >> + <:ast< ( IF "SYNTH" $c1 $c2 $c3) >> (* EN ATTENTE DE REMPLACER CE QUI EST DANS Program.v ... *) | "<"; l1 = lconstr; ">"; IDENT "let"; "("; b = ne_ident_comma_list; ")"; "="; c = constr; "in"; c1 = constr -> - <:ast< (CASE "NOREC" $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >> + <:ast< (LET $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >> | "<"; l1 = lconstr; ">"; IDENT "if"; c1 = constr; IDENT "then"; c2 = constr; IDENT "else"; c3 = constr -> - <:ast< (CASE "NOREC" $l1 $c1 $c2 $c3) >> + <:ast< (IF $l1 $c1 $c2 $c3) >> | c = constr0 -> c ] ] ; constr2: (* ~ will be here *) diff --git a/syntax/PPCases.v b/syntax/PPCases.v index f8b4eb9475..ff2aca9b39 100644 --- a/syntax/PPCases.v +++ b/syntax/PPCases.v @@ -78,8 +78,6 @@ Syntax constr | let_binder_tail_cons [ << (LETBINDERTAIL $var ($LIST $vars)) >> ] -> [ "," [1 0] $var (LETBINDERTAIL ($LIST $vars)) ] - | elim_pred [ << (ELIMPRED $pred) >> ] -> [ "<" $pred:E ">" [0 2] ] - | elim_pred_xtra [ << (ELIMPRED "SYNTH") >> ] -> [ ] ; (* On force les parenthèses autour d'un "if" sous-terme (même si le diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v index 436b2b8136..f78ef411ea 100755 --- a/syntax/PPConstr.v +++ b/syntax/PPConstr.v @@ -189,37 +189,34 @@ Syntax constr level 8: - recpr [ << (XTRA "REC" ($LIST $RECARGS)) >> ] -> [ (RECTERM ($LIST $RECARGS)) ] - - | recterm [ << (RECTERM $P $c ($LIST $BL)) >> ] -> - [ [<hov 0> [<hov 0> "<" $P:E ">" + recterm [ << (MATCH $P $c ($LIST $BL)) >> ] -> + [ [<hov 0> [<hov 0> (ELIMPRED $P) [0 2] [<hov 0> "Match" [1 1] $c:E [1 0] "with" ]] [1 3] [<hov 0> (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] - | mlcasepr [ << (XTRA "MLCASE" "NOREC" ($LIST $RECARGS)) >> ] - -> [ (MLCASETERM ($LIST $RECARGS)) ] - - | mlcaseterm [ << (MLCASETERM $c ($LIST $BL)) >> ] -> - [ [<hov 0> [<hov 0> "Case" [1 1] $c:E [1 0] "of" ] - [1 3] [<hov 0> (MATCHBRANCHES ($LIST $BL)):E ]"end"] ] - - | mlmatchpr [ << (XTRA "MLCASE" "REC" ($LIST $RECARGS)) >> ] - -> [ (MLMATCHTERM ($LIST $RECARGS)) ] - - | mlmatchterm [ << (MLMATCHTERM $c ($LIST $BL)) >> ] -> - [ [<hov 0> [<hov 0> "Match" [1 1] $c:E [1 0] "with" ] - [1 3] [<hov 0> (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] - - | matchbranchescons [ << (MATCHBRANCHES $B ($LIST $T)) >> ] -> [ [<hov 0> [<hov 0> $B:E ] FNL] (MATCHBRANCHES ($LIST $T)):E ] | matchbranchesnil [ << (MATCHBRANCHES) >> ] -> [ ] - | casepr [ << (MUTCASE ($LIST $MATCHARGS)) >> ] -> [ (CASETERM ($LIST $MATCHARGS)) ] - | caseterm [ << (CASETERM $P $c ($LIST $BL)) >> ] -> - [ [<hov 0> [<hov 0> "<" $P:E ">" + | caseterm [ << (CASE $P $c ($LIST $BL)) >> ] -> + [ [<hov 0> [<hov 0> (ELIMPRED $P) [0 2][<hov 0> "Case" [1 1] $c:E [1 0] "of" ]] [1 3][<hov 0> (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] + + | ifterm [ << (IF $P $c $b1 $b2) >> ] -> + [ (FORCEIF $P $c (EQN $b1 JUNK) (EQN $b2 JUNK)):E ] + + | letterm [ << (LET $P $c (LAMBDALIST $_ $b)) >> ] -> + [ (LETSLAM $P $c $b) ] + | letslamend [ << (LETSLAM $P $c $b ($LIST $IDL))>> ] -> + [ (FORCELET $P $c (EQN $b (PATTCONSTRUCT JUNK ($LIST $IDL)))):E ] + | letslam [ << (LETSLAM $P $c [$ID]$b ($LIST $IDL))>> ] -> + [ (LETSLAM $P $c $b ($LIST $IDL) $ID) ] + | letslamanon [ << (LETSLAM $P $c [<>]$b ($LIST $IDL))>> ] -> + [ (LETSLAM $P $c $b ($LIST $IDL) _) ] + + | elim_pred [ << (ELIMPRED $pred) >> ] -> [ "<" $pred:E ">" [0 2] ] + | elim_pred_xtra [ << (ELIMPRED "SYNTH") >> ] -> [ ] ; level 0: |