From 1cd385f3b354a78ae8d02333f40cd065073c9b19 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 21 Dec 2013 17:00:43 +0000
Subject: Support "default" cases in the middle of a "switch", not just at the
 end.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2383 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Csharpminor.v | 32 +++++++++++++++++++++++---------
 1 file changed, 23 insertions(+), 9 deletions(-)

(limited to 'cfrontend/Csharpminor.v')

diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 718daa18..6ae33a69 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -72,8 +72,8 @@ Inductive stmt : Type :=
   | Sgoto: label -> stmt
 
 with lbl_stmt : Type :=
-  | LSdefault: stmt -> lbl_stmt
-  | LScase: int -> stmt -> lbl_stmt -> lbl_stmt.
+  | LSnil: lbl_stmt
+  | LScons: option int -> stmt -> lbl_stmt -> lbl_stmt.
 
 (** Functions are composed of a return type, a list of parameter names,
   a list of local variables with their sizes, a list of temporary variables,
@@ -183,16 +183,30 @@ Definition is_call_cont (k: cont) : Prop :=
 
 (** Resolve [switch] statements. *)
 
-Fixpoint select_switch (n: int) (sl: lbl_stmt) {struct sl} : lbl_stmt :=
+Fixpoint select_switch_default (sl: lbl_stmt): lbl_stmt :=
   match sl with
-  | LSdefault _ => sl
-  | LScase c s sl' => if Int.eq c n then sl else select_switch n sl'
+  | LSnil => sl
+  | LScons None s sl' => sl
+  | LScons (Some i) s sl' => select_switch_default sl'
+  end.
+
+Fixpoint select_switch_case (n: int) (sl: lbl_stmt): option lbl_stmt :=
+  match sl with
+  | LSnil => None
+  | LScons None s sl' => select_switch_case n sl'
+  | LScons (Some c) s sl' => if Int.eq c n then Some sl else select_switch_case n sl'
+  end.
+
+Definition select_switch (n: int) (sl: lbl_stmt): lbl_stmt :=
+  match select_switch_case n sl with
+  | Some sl' => sl'
+  | None => select_switch_default sl
   end.
 
 Fixpoint seq_of_lbl_stmt (sl: lbl_stmt) : stmt :=
   match sl with
-  | LSdefault s => s
-  | LScase c s sl' => Sseq s (seq_of_lbl_stmt sl')
+  | LSnil => Sskip
+  | LScons c s sl' => Sseq s (seq_of_lbl_stmt sl')
   end.
 
 (** Find the statement and manufacture the continuation 
@@ -225,8 +239,8 @@ Fixpoint find_label (lbl: label) (s: stmt) (k: cont)
 with find_label_ls (lbl: label) (sl: lbl_stmt) (k: cont) 
                    {struct sl}: option (stmt * cont) :=
   match sl with
-  | LSdefault s => find_label lbl s k
-  | LScase _ s sl' =>
+  | LSnil => None
+  | LScons _ s sl' =>
       match find_label lbl s (Kseq (seq_of_lbl_stmt sl') k) with
       | Some sk => Some sk
       | None => find_label_ls lbl sl' k
-- 
cgit