diff options
| -rw-r--r-- | parsing/termast.ml | 17 | ||||
| -rw-r--r-- | syntax/PPCases.v | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 12 |
3 files changed, 24 insertions, 7 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml index 698536786a..f1ce602fb7 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -224,16 +224,25 @@ let rec ast_of_raw = function let asteqns = List.map ast_of_eqn eqns in ope(tag,pred::asttomatch::asteqns) + | ROrderedCase (_,LetStyle,typopt,tm,[|bv|]) -> + let nvar' = function Anonymous -> nvar wildcard | Name id -> nvar id in + let rec f l = function + | RLambda (_,na,RHole _,c) -> f (nvar' na :: l) c + | RLetIn (_,na,RHole _,c) -> f (nvar' na :: l) c + | c -> List.rev l, ast_of_raw c in + let l,c = f [] bv in + let eqn = ope ("EQN", [c;ope ("PATTCONSTRUCT",(nvar wildcard)::l)]) in + ope ("FORCELET",[(ast_of_rawopt typopt);(ast_of_raw tm);eqn]) + | ROrderedCase (_,st,typopt,tm,bv) -> let tag = match st with | IfStyle -> "FORCEIF" - | LetStyle -> "FORCELET" - | RegularStyle -> "CASES" - | MatchStyle -> "MATCH" + | RegularStyle -> "CASE" + | MatchStyle | LetStyle -> "MATCH" in (* warning "Old Case syntax"; *) - ope("CASE",(ast_of_rawopt typopt) + ope(tag,(ast_of_rawopt typopt) ::(ast_of_raw tm) ::(Array.to_list (Array.map ast_of_raw bv))) | RRec (_,fk,idv,tyv,bv) -> diff --git a/syntax/PPCases.v b/syntax/PPCases.v index f8d80fd1be..b25b17e61a 100644 --- a/syntax/PPCases.v +++ b/syntax/PPCases.v @@ -81,7 +81,7 @@ Syntax constr (* On force les parenthèses autour d'un "if" sous-terme (même si le parsing est lui plus tolérant) *) level 10: - boolean_cases [ << (FORCEIF $pred $tomatch (EQN $c1 $_) (EQN $c2 $_)) >> ] + boolean_cases [ << (FORCEIF $pred $tomatch $c1 $c2) >> ] -> [ [<hov 0> (ELIMPRED $pred) [<hv 0> "if " [<hov 0> $tomatch:L ] [1 0] [<hov 0> "then" [1 1] $c1:L ] diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 6c99d24516..5a4c2fd65e 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -288,7 +288,11 @@ let make_hunks_ast symbols etyps from = add_break (if protect then 1 else 0) (RO (if protect then s^" " else s) :: make CanBreak prods) else - RO s :: make CanBreak prods + if protect then + (if ws = CanBreak then add_break 1 else (fun x -> x)) + (RO (s^" ") :: make CanBreak prods) + else + RO s :: make CanBreak prods | Terminal s :: prods -> RO s :: make NoBreak prods @@ -326,7 +330,11 @@ let make_hunks etyps symbols = add_break (if protect then 1 else 0) (UnpTerminal (if protect then s^" " else s) :: make CanBreak prods) else - UnpTerminal s :: make CanBreak prods + if protect then + (if ws = CanBreak then add_break 1 else (fun x -> x)) + (UnpTerminal (s^" ") :: make CanBreak prods) + else + UnpTerminal s :: make CanBreak prods | Terminal s :: prods -> UnpTerminal s :: make NoBreak prods |