From 3b72a5ad0218a0df14913b6631f13e880a1983f5 Mon Sep 17 00:00:00 2001 From: Hiroki Tokunaga Date: Sat, 12 Aug 2023 21:43:25 +0900 Subject: [PATCH 1/5] Move a test into a new directory --- test/coq_files/match/or-pattern/{ => whole_branch}/in.v | 0 test/coq_files/match/or-pattern/{ => whole_branch}/out.v | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename test/coq_files/match/or-pattern/{ => whole_branch}/in.v (100%) rename test/coq_files/match/or-pattern/{ => whole_branch}/out.v (100%) diff --git a/test/coq_files/match/or-pattern/in.v b/test/coq_files/match/or-pattern/whole_branch/in.v similarity index 100% rename from test/coq_files/match/or-pattern/in.v rename to test/coq_files/match/or-pattern/whole_branch/in.v diff --git a/test/coq_files/match/or-pattern/out.v b/test/coq_files/match/or-pattern/whole_branch/out.v similarity index 100% rename from test/coq_files/match/or-pattern/out.v rename to test/coq_files/match/or-pattern/whole_branch/out.v From 93a51ba14a42833bef66c907173c9bad33cd4f8b Mon Sep 17 00:00:00 2001 From: Hiroki Tokunaga Date: Sat, 12 Aug 2023 21:43:53 +0900 Subject: [PATCH 2/5] Add a test --- test/coq_files/match/or-pattern/inside_tuple/in.v | 1 + test/coq_files/match/or-pattern/inside_tuple/out.v | 5 +++++ 2 files changed, 6 insertions(+) create mode 100644 test/coq_files/match/or-pattern/inside_tuple/in.v create mode 100644 test/coq_files/match/or-pattern/inside_tuple/out.v diff --git a/test/coq_files/match/or-pattern/inside_tuple/in.v b/test/coq_files/match/or-pattern/inside_tuple/in.v new file mode 100644 index 00000000..fe01b249 --- /dev/null +++ b/test/coq_files/match/or-pattern/inside_tuple/in.v @@ -0,0 +1 @@ +Definition foo(x y:nat):bool:=match x,y with 0,(0|1|2)=>true|_,_=>false end. diff --git a/test/coq_files/match/or-pattern/inside_tuple/out.v b/test/coq_files/match/or-pattern/inside_tuple/out.v new file mode 100644 index 00000000..af38c20f --- /dev/null +++ b/test/coq_files/match/or-pattern/inside_tuple/out.v @@ -0,0 +1,5 @@ +Definition foo (x y : nat) : bool := + match x, y with + | 0, (0 | 1 | 2) => true + | _, _ => false + end. From 3a6e73168b2d97ac8f76425b1554d2f3a2f45774 Mon Sep 17 00:00:00 2001 From: Hiroki Tokunaga Date: Sat, 12 Aug 2023 21:58:50 +0900 Subject: [PATCH 3/5] Pass the test --- lib/ppast.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/lib/ppast.ml b/lib/ppast.ml index 98ef33c9..b471bf94 100644 --- a/lib/ppast.ml +++ b/lib/ppast.ml @@ -67,6 +67,8 @@ and pp_cases_pattern_expr_r printer = function (pp_cases_pattern_expr printer) exprs; write printer suffix + | Constrexpr.CPatPrim _ -> write printer "0" + | Constrexpr.CPatOr _ -> write printer "(0 | 1 | 2)" | _ -> raise (NotImplemented (contents printer)) let rec pp_constr_expr printer CAst.{ v; loc = _ } = pp_constr_expr_r printer v From e286b7f52605c0e8f9cc417dc621702955ca88da Mon Sep 17 00:00:00 2001 From: Hiroki Tokunaga Date: Sat, 12 Aug 2023 21:59:16 +0900 Subject: [PATCH 4/5] Replace a wildcard --- lib/ppast.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ppast.ml b/lib/ppast.ml index b471bf94..6b6e4c7c 100644 --- a/lib/ppast.ml +++ b/lib/ppast.ml @@ -67,7 +67,7 @@ and pp_cases_pattern_expr_r printer = function (pp_cases_pattern_expr printer) exprs; write printer suffix - | Constrexpr.CPatPrim _ -> write printer "0" + | Constrexpr.CPatPrim token -> pp_prim_token printer token | Constrexpr.CPatOr _ -> write printer "(0 | 1 | 2)" | _ -> raise (NotImplemented (contents printer)) From a81c4abb4a40d6137066e83483f446057137b08d Mon Sep 17 00:00:00 2001 From: Hiroki Tokunaga Date: Sat, 12 Aug 2023 22:00:58 +0900 Subject: [PATCH 5/5] Replace a wildcard --- lib/ppast.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/lib/ppast.ml b/lib/ppast.ml index 6b6e4c7c..3ed558ad 100644 --- a/lib/ppast.ml +++ b/lib/ppast.ml @@ -68,7 +68,12 @@ and pp_cases_pattern_expr_r printer = function exprs; write printer suffix | Constrexpr.CPatPrim token -> pp_prim_token printer token - | Constrexpr.CPatOr _ -> write printer "(0 | 1 | 2)" + | Constrexpr.CPatOr xs -> + parens printer (fun () -> + with_seps + ~sep:(fun () -> write printer " | ") + (pp_cases_pattern_expr printer) + xs) | _ -> raise (NotImplemented (contents printer)) let rec pp_constr_expr printer CAst.{ v; loc = _ } = pp_constr_expr_r printer v