Fusion des modifications faites sur les branches "tailcalls" et "smallstep".

En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

9 files changed, 342 insertions, 238 deletions

diff --git a/caml/CMlexer.mll b/caml/CMlexer.mll
index 49d0dbd..ae71e0c 100644
--- a/caml/CMlexer.mll
+++ b/caml/CMlexer.mll
@@ -30,8 +30,10 @@ rule token = parse
   | "|"     { BAR }
   | "||"    { BARBAR }
   | "^"     { CARET }
+  | "case"  { CASE }
   | ":"    { COLON }
   | ","    { COMMA }
+  | "default" { DEFAULT }
   | "$"    { DOLLAR }
   | "else"    { ELSE }
   | "="    { EQUAL }
@@ -75,6 +77,7 @@ rule token = parse
   | "let"     { LET }
   | "loop"    { LOOP }
   | "("    { LPAREN }
+  | "match" { MATCH }
   | "-"    { MINUS }
   | "->"    { MINUSGREATER }
   | "-f"    { MINUSF }
diff --git a/caml/CMparser.mly b/caml/CMparser.mly
index d9a8187..0db0af2 100644
--- a/caml/CMparser.mly
+++ b/caml/CMparser.mly
@@ -8,16 +8,67 @@ open BinPos
 open BinInt
 open Integers
 open AST
-open Op
 open Cminor
 
 let intconst n =
-  Eop(Ointconst(coqint_of_camlint n), Enil)
+  Econst(Ointconst(coqint_of_camlint n))
 
 let andbool e1 e2 =
-  Cmconstr.conditionalexpr e1 e2 (intconst 0l)
+  Econdition(e1, e2, intconst 0l)
 let orbool e1 e2 =
-  Cmconstr.conditionalexpr e1 (intconst 1l) e2
+  Econdition(e1, intconst 1l, e2)
+
+let exitnum n = nat_of_camlint(Int32.pred n)
+
+let mkswitch expr (cases, dfl) =
+  let rec mktable = function
+  | [] -> Coq_nil
+  | (key, exit) :: rem ->
+      Coq_cons(Coq_pair(coqint_of_camlint key, exitnum exit), mktable rem) in
+  Sswitch(expr, mktable cases, exitnum dfl)
+
+(***
+   match (a) { case 0: s0; case 1: s1; case 2: s2; }  --->
+
+   block {
+   block {
+   block {
+   block {
+     switch(a) { case 0: exit 0; case 1: exit 1; default: exit 2; }
+   }; s0; exit 2;
+   }; s1; exit 1;
+   }; s2;
+   }
+
+   Note that matches are assumed to be exhaustive
+***)
+
+let mkmatch_aux expr cases =
+  let ncases = Int32.of_int (List.length cases) in
+  let rec mktable n = function
+    | [] -> assert false
+    | [key, action] -> Coq_nil
+    | (key, action) :: rem ->
+        Coq_cons(Coq_pair(coqint_of_camlint key, nat_of_camlint n),
+                 mktable (Int32.succ n) rem) in
+  let sw =
+    Sswitch(expr, mktable 0l cases, nat_of_camlint (Int32.pred ncases)) in
+  let rec mkblocks body n = function
+    | [] -> assert false
+    | [key, action] ->
+        Sblock(Sseq(body, action))
+    | (key, action) :: rem ->
+        mkblocks
+          (Sblock(Sseq(body, Sseq(action, Sexit (nat_of_camlint n)))))
+          (Int32.pred n)
+          rem in
+  mkblocks (Sblock sw) (Int32.pred ncases) cases
+
+let mkmatch expr cases =
+  match cases with
+  | [] -> Sskip (* ??? *)
+  | [key, action] -> action
+  | _ -> mkmatch_aux expr cases
 
 %}
 
@@ -32,8 +83,10 @@ let orbool e1 e2 =
 %token BAR
 %token BARBAR
 %token CARET
+%token CASE
 %token COLON
 %token COMMA
+%token DEFAULT
 %token DOLLAR
 %token ELSE
 %token EQUAL
@@ -81,6 +134,7 @@ let orbool e1 e2 =
 %token LET
 %token LOOP
 %token LPAREN
+%token MATCH
 %token MINUS
 %token MINUSF
 %token MINUSGREATER
@@ -200,7 +254,7 @@ parameter_list:
 
 stack_declaration:
     /* empty */                                 { Z0 }
-  | STACK INTLIT                                { z_of_camlint $2 }
+  | STACK INTLIT SEMICOLON                      { z_of_camlint $2 }
 ;
 
 var_declarations:
@@ -217,14 +271,18 @@ var_declaration:
 stmt:
     expr SEMICOLON                              { Sexpr $1 }
   | IDENT EQUAL expr SEMICOLON                  { Sassign($1, $3) }
-  | IF LPAREN expr RPAREN stmts ELSE stmts      { Cmconstr.ifthenelse $3 $5 $7 }
-  | IF LPAREN expr RPAREN stmts                 { Cmconstr.ifthenelse $3 $5 Sskip }
+  | IF LPAREN expr RPAREN stmts ELSE stmts      { Sifthenelse($3, $5, $7) }
+  | IF LPAREN expr RPAREN stmts                 { Sifthenelse($3, $5, Sskip) }
   | LOOP stmts                                  { Sloop($2) }
   | LBRACELBRACE stmt_list RBRACERBRACE         { Sblock($2) }
   | EXIT SEMICOLON                              { Sexit O }
-  | EXIT INTLIT SEMICOLON                       { Sexit (nat_of_camlint(Int32.pred $2)) }
+  | EXIT INTLIT SEMICOLON                       { Sexit (exitnum $2) }
   | RETURN SEMICOLON                            { Sreturn None }
   | RETURN expr SEMICOLON                       { Sreturn (Some $2) }
+  | SWITCH LPAREN expr RPAREN LBRACE switch_cases RBRACE
+                                                { mkswitch $3 $6 }
+  | MATCH LPAREN expr RPAREN LBRACE match_cases RBRACE
+                                                { mkmatch $3 $6 }
 ;
 
 stmts:
@@ -237,72 +295,84 @@ stmt_list:
   | stmt stmt_list                              { Sseq($1, $2) }
 ;
 
+switch_cases:
+    DEFAULT COLON EXIT INTLIT SEMICOLON
+           { ([], $4) }
+  | CASE INTLIT COLON EXIT INTLIT SEMICOLON switch_cases
+           { let (cases, dfl) = $7 in (($2, $5) :: cases, dfl) }
+;
+
+match_cases:
+    /* empty */                                 { [] }
+  | CASE INTLIT COLON stmt_list match_cases     { ($2, $4) :: $5 }
+;
+
 /* Expressions */
 
 expr:
     LPAREN expr RPAREN                          { $2 }
   | IDENT                                       { Evar $1 }
   | INTLIT                                      { intconst $1 }
-  | FLOATLIT                                    { Eop(Ofloatconst $1, Enil) }
-  | STRINGLIT                                   { Eop(Oaddrsymbol($1, Int.zero), Enil) }
-  | AMPERSAND INTLIT                            { Eop(Oaddrstack(coqint_of_camlint $2), Enil) }
-  | MINUS expr    %prec p_uminus                { Cmconstr.negint $2 }
-  | MINUSF expr   %prec p_uminus                { Cmconstr.negfloat $2 }
-  | ABSF expr                                   { Cmconstr.absfloat $2 }
-  | INTOFFLOAT expr                             { Cmconstr.intoffloat $2 }
-  | FLOATOFINT expr                             { Cmconstr.floatofint $2 }
-  | FLOATOFINTU expr                            { Cmconstr.floatofintu $2 }
-  | TILDE expr                                  { Cmconstr.notint $2 }
-  | BANG expr                                   { Cmconstr.notbool $2 }
-  | INT8S expr                                  { Cmconstr.cast8signed $2 }
-  | INT8U expr                                  { Cmconstr.cast8unsigned $2 }
-  | INT16S expr                                 { Cmconstr.cast16signed $2 }
-  | INT16U expr                                 { Cmconstr.cast16unsigned $2 }
-  | FLOAT32 expr                                { Cmconstr.singleoffloat $2 }
+  | FLOATLIT                                    { Econst(Ofloatconst $1) }
+  | STRINGLIT                                   { Econst(Oaddrsymbol($1, Int.zero)) }
+  | AMPERSAND INTLIT                            { Econst(Oaddrstack(coqint_of_camlint $2)) }
+  | MINUS expr    %prec p_uminus                { Eunop(Onegint, $2) }
+  | MINUSF expr   %prec p_uminus                { Eunop(Onegf, $2) }
+  | ABSF expr                                   { Eunop(Oabsf, $2) }
+  | INTOFFLOAT expr                             { Eunop(Ointoffloat, $2) }
+  | FLOATOFINT expr                             { Eunop(Ofloatofint, $2) }
+  | FLOATOFINTU expr                            { Eunop(Ofloatofintu, $2) }
+  | TILDE expr                                  { Eunop(Onotint, $2) }
+  | BANG expr                                   { Eunop(Onotbool, $2) }
+  | INT8S expr                                  { Eunop(Ocast8signed, $2) }
+  | INT8U expr                                  { Eunop(Ocast8unsigned, $2) }
+  | INT16S expr                                 { Eunop(Ocast16signed, $2) }
+  | INT16U expr                                 { Eunop(Ocast16unsigned, $2) }
+  | FLOAT32 expr                                { Eunop(Osingleoffloat, $2) }
   | ALLOC expr                                  { Ealloc $2 }
-  | expr PLUS expr                              { Cmconstr.add $1 $3 }
-  | expr MINUS expr                             { Cmconstr.sub $1 $3 }
-  | expr STAR expr                              { Cmconstr.mul $1 $3 }
-  | expr SLASH expr                             { Cmconstr.divs $1 $3 }
-  | expr PERCENT expr                           { Cmconstr.mods $1 $3 }
-  | expr SLASHU expr                            { Cmconstr.divu $1 $3 }
-  | expr PERCENTU expr                          { Cmconstr.modu $1 $3 }
-  | expr AMPERSAND expr                         { Cmconstr.coq_and $1 $3 }
-  | expr BAR expr                               { Cmconstr.coq_or $1 $3 }
-  | expr CARET expr                             { Cmconstr.xor $1 $3 }
-  | expr LESSLESS expr                          { Cmconstr.shl $1 $3 }
-  | expr GREATERGREATER expr                    { Cmconstr.shr $1 $3 }
-  | expr GREATERGREATERU expr                   { Cmconstr.shru $1 $3 }
-  | expr PLUSF expr                             { Cmconstr.addf $1 $3 }
-  | expr MINUSF expr                            { Cmconstr.subf $1 $3 }
-  | expr STARF expr                             { Cmconstr.mulf $1 $3 }
-  | expr SLASHF expr                            { Cmconstr.divf $1 $3 }
-  | expr EQUALEQUAL expr                        { Cmconstr.cmp Ceq $1 $3 }
-  | expr BANGEQUAL expr                         { Cmconstr.cmp Cne $1 $3 }
-  | expr LESS expr                              { Cmconstr.cmp Clt $1 $3 }
-  | expr LESSEQUAL expr                         { Cmconstr.cmp Cle $1 $3 }
-  | expr GREATER expr                           { Cmconstr.cmp Cgt $1 $3 }
-  | expr GREATEREQUAL expr                      { Cmconstr.cmp Cge $1 $3 }
-  | expr EQUALEQUALU expr                       { Cmconstr.cmpu Ceq $1 $3 }
-  | expr BANGEQUALU expr                        { Cmconstr.cmpu Cne $1 $3 }
-  | expr LESSU expr                             { Cmconstr.cmpu Clt $1 $3 }
-  | expr LESSEQUALU expr                        { Cmconstr.cmpu Cle $1 $3 }
-  | expr GREATERU expr                          { Cmconstr.cmpu Cgt $1 $3 }
-  | expr GREATEREQUALU expr                     { Cmconstr.cmpu Cge $1 $3 }
-  | expr EQUALEQUALF expr                       { Cmconstr.cmpf Ceq $1 $3 }
-  | expr BANGEQUALF expr                        { Cmconstr.cmpf Cne $1 $3 }
-  | expr LESSF expr                             { Cmconstr.cmpf Clt $1 $3 }
-  | expr LESSEQUALF expr                        { Cmconstr.cmpf Cle $1 $3 }
-  | expr GREATERF expr                          { Cmconstr.cmpf Cgt $1 $3 }
-  | expr GREATEREQUALF expr                     { Cmconstr.cmpf Cge $1 $3 }
-  | memory_chunk LBRACKET expr RBRACKET         { Cmconstr.load $1 $3 }
+  | expr PLUS expr                              { Ebinop(Oadd, $1, $3) }
+  | expr MINUS expr                             { Ebinop(Osub, $1, $3) }
+  | expr STAR expr                              { Ebinop(Omul, $1, $3) }
+  | expr SLASH expr                             { Ebinop(Odiv, $1, $3) }
+  | expr PERCENT expr                           { Ebinop(Omod, $1, $3) }
+  | expr SLASHU expr                            { Ebinop(Odivu, $1, $3) }
+  | expr PERCENTU expr                          { Ebinop(Omodu, $1, $3) }
+  | expr AMPERSAND expr                         { Ebinop(Oand, $1, $3) }
+  | expr BAR expr                               { Ebinop(Oor, $1, $3) }
+  | expr CARET expr                             { Ebinop(Oxor, $1, $3) }
+  | expr LESSLESS expr                          { Ebinop(Oshl, $1, $3) }
+  | expr GREATERGREATER expr                    { Ebinop(Oshr, $1, $3) }
+  | expr GREATERGREATERU expr                   { Ebinop(Oshru, $1, $3) }
+  | expr PLUSF expr                             { Ebinop(Oaddf, $1, $3) }
+  | expr MINUSF expr                            { Ebinop(Osubf, $1, $3) }
+  | expr STARF expr                             { Ebinop(Omulf, $1, $3) }
+  | expr SLASHF expr                            { Ebinop(Odivf, $1, $3) }
+  | expr EQUALEQUAL expr                        { Ebinop(Ocmp Ceq, $1, $3) }
+  | expr BANGEQUAL expr                         { Ebinop(Ocmp Cne, $1, $3) }
+  | expr LESS expr                              { Ebinop(Ocmp Clt, $1, $3) }
+  | expr LESSEQUAL expr                         { Ebinop(Ocmp Cle, $1, $3) }
+  | expr GREATER expr                           { Ebinop(Ocmp Cgt, $1, $3) }
+  | expr GREATEREQUAL expr                      { Ebinop(Ocmp Cge, $1, $3) }
+  | expr EQUALEQUALU expr                       { Ebinop(Ocmpu Ceq, $1, $3) }
+  | expr BANGEQUALU expr                        { Ebinop(Ocmpu Cne, $1, $3) }
+  | expr LESSU expr                             { Ebinop(Ocmpu Clt, $1, $3) }
+  | expr LESSEQUALU expr                        { Ebinop(Ocmpu Cle, $1, $3) }
+  | expr GREATERU expr                          { Ebinop(Ocmpu Cgt, $1, $3) }
+  | expr GREATEREQUALU expr                     { Ebinop(Ocmpu Cge, $1, $3) }
+  | expr EQUALEQUALF expr                       { Ebinop(Ocmpf Ceq, $1, $3) }
+  | expr BANGEQUALF expr                        { Ebinop(Ocmpf Cne, $1, $3) }
+  | expr LESSF expr                             { Ebinop(Ocmpf Clt, $1, $3) }
+  | expr LESSEQUALF expr                        { Ebinop(Ocmpf Cle, $1, $3) }
+  | expr GREATERF expr                          { Ebinop(Ocmpf Cgt, $1, $3) }
+  | expr GREATEREQUALF expr                     { Ebinop(Ocmpf Cge, $1, $3) }
+  | memory_chunk LBRACKET expr RBRACKET         { Eload($1, $3) }
   | memory_chunk LBRACKET expr RBRACKET EQUAL expr
-                                                { Cmconstr.store $1 $3 $6 }
+                                                { Estore($1, $3, $6) }
   | expr LPAREN expr_list RPAREN COLON signature
                                                 { Ecall($6, $1, $3) }
   | expr AMPERSANDAMPERSAND expr                { andbool $1 $3 }
   | expr BARBAR expr                            { orbool $1 $3 }
-  | expr QUESTION expr COLON expr               { Cmconstr.conditionalexpr $1 $3 $5 }
+  | expr QUESTION expr COLON expr               { Econdition($1, $3, $5) }
   | LET expr IN expr %prec p_let                { Elet($2, $4) }
   | DOLLAR INTLIT                               { Eletvar (nat_of_camlint $2) }
 ;
diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml
index a926039..495ded0 100644
--- a/caml/CMtypecheck.ml
+++ b/caml/CMtypecheck.ml
@@ -6,7 +6,6 @@ open CList
 open Camlcoq
 open AST
 open Integers
-open Op
 open Cminor
 
 exception Error of string
@@ -67,135 +66,91 @@ let name_of_comparison = function
   | Cgt -> "gt"
   | Cge -> "ge"
 
-let type_condition = function
-  | Ccomp _ -> [tint;tint]
-  | Ccompu _ -> [tint;tint]
-  | Ccompimm _ -> [tint]
-  | Ccompuimm _ -> [tint]
-  | Ccompf _ -> [tfloat;tfloat]
-  | Cnotcompf _ -> [tfloat;tfloat]
-  | Cmaskzero _ -> [tint]
-  | Cmasknotzero _ -> [tint]
+let type_constant = function
+  | Ointconst _ -> tint
+  | Ofloatconst _ -> tfloat
+  | Oaddrsymbol _ -> tint
+  | Oaddrstack _ -> tint
 
-let name_of_condition = function
-  | Ccomp c -> sprintf "comp %s" (name_of_comparison c)
-  | Ccompu c ->  sprintf "compu %s" (name_of_comparison c)
-  | Ccompimm(c, n) -> sprintf "compimm %s %ld" (name_of_comparison c) (camlint_of_coqint n)
-  | Ccompuimm(c, n) -> sprintf "compuimm %s %ld" (name_of_comparison c) (camlint_of_coqint n)
-  | Ccompf c -> sprintf "compf %s" (name_of_comparison c)
-  | Cnotcompf c -> sprintf "notcompf %s" (name_of_comparison c)
-  | Cmaskzero n -> sprintf "maskzero %ld" (camlint_of_coqint n)
-  | Cmasknotzero n ->  sprintf "masknotzero %ld" (camlint_of_coqint n)
+let type_unary_operation = function
+  | Ocast8signed -> tint, tint
+  | Ocast16signed -> tint, tint
+  | Ocast8unsigned -> tint, tint
+  | Ocast16unsigned -> tint, tint
+  | Onegint -> tint, tint
+  | Onotbool -> tint, tint
+  | Onotint -> tint, tint
+  | Onegf -> tfloat, tfloat
+  | Oabsf -> tfloat, tfloat
+  | Osingleoffloat -> tfloat, tfloat
+  | Ointoffloat -> tfloat, tint
+  | Ofloatofint -> tint, tfloat
+  | Ofloatofintu -> tint, tfloat
 
-let type_operation = function
-  | Omove -> let v = newvar() in [v], v
-  | Ointconst _ -> [], tint
-  | Ofloatconst _ -> [], tfloat
-  | Oaddrsymbol _ -> [], tint
-  | Oaddrstack _ -> [], tint
-  | Oundef -> [], newvar()
-  | Ocast8signed -> [tint], tint
-  | Ocast16signed -> [tint], tint
-  | Ocast8unsigned -> [tint], tint
-  | Ocast16unsigned -> [tint], tint
-  | Oadd -> [tint;tint], tint
-  | Oaddimm _ -> [tint], tint
-  | Osub -> [tint;tint], tint
-  | Osubimm _ -> [tint], tint
-  | Omul -> [tint;tint], tint
-  | Omulimm _ -> [tint], tint
-  | Odiv -> [tint;tint], tint
-  | Odivu -> [tint;tint], tint
-  | Oand -> [tint;tint], tint
-  | Oandimm _ -> [tint], tint
-  | Oor -> [tint;tint], tint
-  | Oorimm _ -> [tint], tint
-  | Oxor -> [tint;tint], tint
-  | Oxorimm _ -> [tint], tint
-  | Onand -> [tint;tint], tint
-  | Onor -> [tint;tint], tint
-  | Onxor -> [tint;tint], tint
-  | Oshl -> [tint;tint], tint
-  | Oshr -> [tint;tint], tint
-  | Oshrimm _ -> [tint], tint
-  | Oshrximm _ -> [tint], tint
-  | Oshru -> [tint;tint], tint
-  | Orolm _ -> [tint], tint
-  | Onegf -> [tfloat], tfloat
-  | Oabsf -> [tfloat], tfloat
-  | Oaddf -> [tfloat;tfloat], tfloat
-  | Osubf -> [tfloat;tfloat], tfloat
-  | Omulf -> [tfloat;tfloat], tfloat
-  | Odivf -> [tfloat;tfloat], tfloat
-  | Omuladdf -> [tfloat;tfloat;tfloat], tfloat
-  | Omulsubf -> [tfloat;tfloat;tfloat], tfloat
-  | Osingleoffloat -> [tfloat], tfloat
-  | Ointoffloat -> [tfloat], tint
-  | Ofloatofint -> [tint], tfloat
-  | Ofloatofintu -> [tint], tfloat
-  | Ocmp c -> type_condition c, tint
+let type_binary_operation = function
+  | Oadd -> tint, tint, tint
+  | Osub -> tint, tint, tint
+  | Omul -> tint, tint, tint
+  | Odiv -> tint, tint, tint
+  | Odivu -> tint, tint, tint
+  | Omod -> tint, tint, tint
+  | Omodu -> tint, tint, tint
+  | Oand -> tint, tint, tint
+  | Oor -> tint, tint, tint
+  | Oxor -> tint, tint, tint
+  | Oshl -> tint, tint, tint
+  | Oshr -> tint, tint, tint
+  | Oshru -> tint, tint, tint
+  | Oaddf -> tfloat, tfloat, tfloat
+  | Osubf -> tfloat, tfloat, tfloat
+  | Omulf -> tfloat, tfloat, tfloat
+  | Odivf -> tfloat, tfloat, tfloat
+  | Ocmp _ -> tint, tint, tint
+  | Ocmpu _ -> tint, tint, tint
+  | Ocmpf _ -> tfloat, tfloat, tint
 
-let name_of_operation = function
-  | Omove -> "move"
+let name_of_constant = function
   | Ointconst n -> sprintf "intconst %ld" (camlint_of_coqint n)
   | Ofloatconst n -> sprintf "floatconst %g" n
   | Oaddrsymbol (s, ofs) -> sprintf "addrsymbol %s %ld" (extern_atom s) (camlint_of_coqint ofs)
   | Oaddrstack n -> sprintf "addrstack %ld" (camlint_of_coqint n)
-  | Oundef -> "undef"
+
+let name_of_unary_operation = function
   | Ocast8signed -> "cast8signed"
   | Ocast16signed -> "cast16signed"
   | Ocast8unsigned -> "cast8unsigned"
   | Ocast16unsigned -> "cast16unsigned"
+  | Onegint -> "negint"
+  | Onotbool -> "notbool"
+  | Onotint -> "notint"
+  | Onegf -> "negf"
+  | Oabsf -> "absf"
+  | Osingleoffloat -> "singleoffloat"
+  | Ointoffloat -> "intoffloat"
+  | Ofloatofint -> "floatofint"
+  | Ofloatofintu -> "floatofintu"
+
+let name_of_binary_operation = function
   | Oadd -> "add"
-  | Oaddimm n -> sprintf "addimm %ld" (camlint_of_coqint n)
   | Osub -> "sub"
-  | Osubimm n -> sprintf "subimm %ld" (camlint_of_coqint n)
   | Omul -> "mul"
-  | Omulimm n -> sprintf "mulimm %ld" (camlint_of_coqint n)
   | Odiv -> "div"
   | Odivu -> "divu"
+  | Omod -> "mod"
+  | Omodu -> "modu"
   | Oand -> "and"
-  | Oandimm n -> sprintf "andimm %ld" (camlint_of_coqint n)
   | Oor -> "or"
-  | Oorimm n -> sprintf "orimm %ld" (camlint_of_coqint n)
   | Oxor -> "xor"
-  | Oxorimm n -> sprintf "xorimm %ld" (camlint_of_coqint n)
-  | Onand -> "nand"
-  | Onor -> "nor"
-  | Onxor -> "nxor"
   | Oshl -> "shl"
   | Oshr -> "shr"
-  | Oshrimm n -> sprintf "shrimm %ld" (camlint_of_coqint n)
-  | Oshrximm n -> sprintf "shrximm %ld" (camlint_of_coqint n)
   | Oshru -> "shru"
-  | Orolm(n, m) -> sprintf "rolm %ld %ld" (camlint_of_coqint n) (camlint_of_coqint m)
-  | Onegf -> "negf"
-  | Oabsf -> "absf"
   | Oaddf -> "addf"
   | Osubf -> "subf"
   | Omulf -> "mulf"
   | Odivf -> "divf"
-  | Omuladdf -> "muladdf"
-  | Omulsubf -> "mulsubf"
-  | Osingleoffloat -> "singleoffloat"
-  | Ointoffloat -> "intoffloat"
-  | Ofloatofint -> "floatofint"
-  | Ofloatofintu -> "floatofintu"
-  | Ocmp c -> name_of_condition c
-
-let type_addressing = function
-  | Aindexed _ -> [tint]
-  | Aindexed2 -> [tint;tint]
-  | Aglobal _ -> []
-  | Abased _ -> [tint]
-  | Ainstack _ -> []
-
-let name_of_addressing = function
-  | Aindexed n -> sprintf "indexed %ld" (camlint_of_coqint n)
-  | Aindexed2 -> sprintf "indexed2"
-  | Aglobal(s, ofs) -> sprintf "global %s %ld" (extern_atom s) (camlint_of_coqint ofs)
-  | Abased(s, ofs) -> sprintf "based %s %ld" (extern_atom s) (camlint_of_coqint ofs)
-  | Ainstack n -> sprintf "instack %ld" (camlint_of_coqint n)
+  | Ocmp c -> sprintf "cmp %s" (name_of_comparison c)
+  | Ocmpu c -> sprintf "cmpu %s" (name_of_comparison c)
+  | Ocmpf c -> sprintf "cmpf %s" (name_of_comparison c)
 
 let type_chunk = function
   | Mint8signed -> tint
@@ -219,34 +174,47 @@ let rec type_expr env lenv e =
   match e with
   | Evar id ->
       type_var env id
-  | Eop(op, el) ->
-      let tel = type_exprlist env lenv el in
-      let (targs, tres) = type_operation op in
+  | Econst cst ->
+      type_constant cst
+  | Eunop(op, e1) ->
+      let te1 = type_expr env lenv e1 in
+      let (targ, tres) = type_unary_operation op in
       begin try
-        unify_list targs tel
+        unify targ te1
       with Error s ->
         raise (Error (sprintf "In application of operator %s:\n%s"
-                              (name_of_operation op) s))
+                              (name_of_unary_operation op) s))
       end;
       tres
-  | Eload(chunk, addr, el) ->
-      let tel = type_exprlist env lenv el in
+  | Ebinop(op, e1, e2) ->
+      let te1 = type_expr env lenv e1 in
+      let te2 = type_expr env lenv e2 in
+      let (targ1, targ2, tres) = type_binary_operation op in
       begin try
-        unify_list (type_addressing addr) tel
+        unify targ1 te1; unify targ2 te2
       with Error s ->
-        raise (Error (sprintf "In load %s %s:\n%s"
-                              (name_of_chunk chunk) (name_of_addressing addr) s))
+        raise (Error (sprintf "In application of operator %s:\n%s"
+                              (name_of_binary_operation op) s))
+      end;
+      tres
+  | Eload(chunk, e) ->
+      let te = type_expr env lenv e in
+      begin try
+        unify tint te
+      with Error s ->
+        raise (Error (sprintf "In load %s:\n%s"
+                              (name_of_chunk chunk) s))
       end;
       type_chunk chunk
-  | Estore(chunk, addr, el, e1) ->
-      let tel = type_exprlist env lenv el in
+  | Estore(chunk, e1, e2) ->
       let te1 = type_expr env lenv e1 in
+      let te2 = type_expr env lenv e2 in
       begin try
-        unify_list (type_addressing addr) tel;
-        unify (type_chunk chunk) te1
+        unify tint te1;
+        unify (type_chunk chunk) te2
       with Error s ->
-        raise (Error (sprintf "In store %s %s:\n%s"
-                              (name_of_chunk chunk) (name_of_addressing addr) s))
+        raise (Error (sprintf "In store %s:\n%s"
+                              (name_of_chunk chunk) s))
       end;
       te1
   | Ecall(sg, e1, el) ->
@@ -295,21 +263,13 @@ and type_exprlist env lenv el =
       let tet = type_exprlist env lenv et in
       (te1 :: tet)
 
-and type_condexpr env lenv ce =
-  match ce with
-  | CEtrue -> ()
-  | CEfalse -> ()
-  | CEcond(c, el) ->
-      let tel = type_exprlist env lenv el in
-      begin try
-        unify_list (type_condition c) tel
-      with Error s ->
-        raise (Error (sprintf "In condition %s:\n%s" (name_of_condition c) s))
-      end
-  | CEcondition(ce1, ce2, ce3) ->
-      type_condexpr env lenv ce1;
-      type_condexpr env lenv ce2;
-      type_condexpr env lenv ce3
+and type_condexpr env lenv e =
+  let te = type_expr env lenv e in
+  begin try
+    unify tint te
+  with Error s ->
+    raise (Error (sprintf "In condition:\n%s" s))
+  end
 
 let rec type_stmt env blk ret s =
   match s with
@@ -355,6 +315,15 @@ let rec type_stmt env blk ret s =
             raise (Error (sprintf "In return:\n%s" s))
           end
       end
+  | Stailcall(sg, e1, el) ->
+      let te1 = type_expr env [] e1 in
+      let tel = type_exprlist env [] el in
+      begin try
+        unify tint te1;
+        unify_list (ty_of_sig_args sg.sig_args) tel
+      with Error s ->
+        raise (Error (sprintf "In tail call:\n%s" s))
+      end
 
 let rec env_of_vars idl =
   match idl with
diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml
index c2115df..ec2447f 100644
--- a/caml/Camlcoq.ml
+++ b/caml/Camlcoq.ml
@@ -41,7 +41,7 @@ let z_of_camlint n =
 
 let coqint_of_camlint : int32 -> Integers.int = z_of_camlint
 
-(* Strings *)
+(* Atoms (positive integers representing strings) *)
 
 let atom_of_string = (Hashtbl.create 17 : (string, positive) Hashtbl.t)
 let string_of_atom = (Hashtbl.create 17 : (positive, string) Hashtbl.t)
@@ -69,24 +69,6 @@ let rec coqlist_iter f = function
     Coq_nil -> ()
   | Coq_cons(a,l) -> f a; coqlist_iter f l
 
-(* Helpers *)
-
-let rec list_iter f = function
-    [] -> ()
-  | a::l -> f a; list_iter f l
-
-let rec list_memq x = function
-    [] -> false
-  | a::l -> a == x || list_memq x l
-
-let rec list_exists p = function
-    [] -> false
-  | a::l -> p a || list_exists p l
-
-let rec list_filter p = function
-    [] -> []
-  | x :: l -> if p x then x :: list_filter p l else list_filter p l
-
 let rec length_coqlist = function
   | Coq_nil -> 0
   | Coq_cons (x, l) -> 1 + length_coqlist l
@@ -100,6 +82,31 @@ let array_of_coqlist = function
         | Coq_cons(hd, tl) -> a.(i) <- hd; fill (i + 1) tl in
       fill 1 tl
 
+(* Strings *)
+
+let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) =
+  Char.chr(  (if a0 then 1 else 0)
+           + (if a1 then 2 else 0)
+           + (if a2 then 4 else 0)
+           + (if a3 then 8 else 0)
+           + (if a4 then 16 else 0)
+           + (if a5 then 32 else 0)
+           + (if a6 then 64 else 0)
+           + (if a7 then 128 else 0))
+
+let coqstring_length s =
+  let rec len accu = function
+  | CString.EmptyString -> accu
+  | CString.CString(_, s) -> len (accu + 1) s
+  in len 0 s
+
+let camlstring_of_coqstring s =
+  let r = String.create (coqstring_length s) in
+  let rec fill pos = function
+  | CString.EmptyString -> r
+  | CString.CString(c, s) -> r.[pos] <- char_of_ascii c; fill (pos + 1) s
+  in fill 0 s
+
 (* Timing facility *)
 
 (*
diff --git a/caml/Coloringaux.ml b/caml/Coloringaux.ml
index a7c8db5..b3f4515 100644
--- a/caml/Coloringaux.ml
+++ b/caml/Coloringaux.ml
@@ -185,8 +185,8 @@ let init() =
 
 let interfere n1 n2 =
   if n1.degree < n2.degree
-  then list_memq n2 n1.adjlist
-  else list_memq n1 n2.adjlist
+  then List.memq n2 n1.adjlist
+  else List.memq n1 n2.adjlist
 
 (* Add an edge to the graph.  Assume edge is not in graph already *)
 
@@ -199,7 +199,7 @@ let addEdge n1 n2 =
 (* Apply the given function to the relevant adjacent nodes of a node *)
 
 let iterAdjacent f n =
-  list_iter
+  List.iter
     (fun n ->
       match n.nstate with
       | SelectStack | CoalescedNodes -> ()
@@ -214,12 +214,12 @@ let moveIsActiveOrWorklist m =
   | _ -> false
 
 let nodeMoves n =
-  list_filter moveIsActiveOrWorklist n.movelist
+  List.filter moveIsActiveOrWorklist n.movelist
 
 (* Determine whether a node is involved in a move *)
 
 let moveRelated n =
-  list_exists moveIsActiveOrWorklist n.movelist
+  List.exists moveIsActiveOrWorklist n.movelist
 
 (*i
 (* Check invariants *)
@@ -361,7 +361,7 @@ let build g typenv spillcosts =
 (* Enable moves that have become low-degree related *)
 
 let enableMoves n =
-  list_iter
+  List.iter
     (fun m ->
       if m.mstate = ActiveMoves
       then DLinkMove.move m activeMoves worklistMoves)
@@ -481,7 +481,7 @@ let freezeMoves u =
     && v.degree < num_available_registers.(v.regclass)
     && v.nstate <> Colored
     then DLinkNode.move v freezeWorklist simplifyWorklist in
-  list_iter freeze (nodeMoves u)
+  List.iter freeze (nodeMoves u)
 
 (* Pick a move and freeze it *)
 
@@ -577,7 +577,7 @@ let find_slot conflicts typ =
 
 let assign_color n =
   let conflicts = ref Locset.empty in
-  list_iter
+  List.iter
     (fun n' ->
       match (getAlias n').color with
       | None -> ()
@@ -607,7 +607,7 @@ let graph_coloring (f: coq_function) (g: graph) (env: regenv) (regs: Regset.t)
   init();
   Array.fill start_points 0 num_register_classes 0;
   let mapping = build g env (spill_costs f) in
-  list_iter assign_color (nodeOrder []);
+  List.iter assign_color (nodeOrder []);
   fun r ->
     try location_of_node (getAlias (Hashtbl.find mapping r))
     with Not_found -> R IT1 (* any location *)
diff --git a/caml/Main2.ml b/caml/Main2.ml
index ff9f350..e3399fb 100644
--- a/caml/Main2.ml
+++ b/caml/Main2.ml
@@ -94,8 +94,8 @@ let process_c_file sourcename =
   (* Convert to PPC *)
   let ppc =
     match Main.transf_c_program csyntax with
-    | Datatypes.Some x -> x
-    | Datatypes.None ->
+    | Errors.OK x -> x
+    | Errors.Error msg ->
         eprintf "Error in translation Csyntax -> PPC\n";
         exit 2 in
   (* Save PPC asm *)
@@ -111,10 +111,10 @@ let process_cminor_file sourcename =
     match Main.transf_cminor_program
             (CMtypecheck.type_program
               (CMparser.prog CMlexer.token lb)) with
-    | Datatypes.None ->
+    | Errors.Error msg ->
         eprintf "Compiler failure\n";
         exit 2
-    | Datatypes.Some p ->
+    | Errors.OK p ->
         let oc = open_out targetname in
         PrintPPC.print_program oc p;
         close_out oc
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml
index 3ee79d1..bf7b2cc 100644
--- a/caml/PrintPPC.ml
+++ b/caml/PrintPPC.ml
@@ -137,6 +137,8 @@ let print_instruction oc labels = function
       fprintf oc "	bf	%a, %a\n" print_crbit bit print_label lbl
   | Pbl s ->
       fprintf oc "	bl	%a\n" print_symb s
+  | Pbs s ->
+      fprintf oc "	b	%a\n" print_symb s
   | Pblr ->
       fprintf oc "	blr\n"
   | Pbt(bit, lbl) ->
@@ -318,10 +320,6 @@ let print_instruction oc labels = function
       fprintf oc "	xoris	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
   | Plabel lbl ->
       if Labelset.mem lbl labels then fprintf oc "%a:\n" print_label lbl
-  | Piundef r ->
-      fprintf oc "	# undef %a\n" ireg r
-  | Pfundef r ->
-      fprintf oc "	# undef %a\n" freg r
 
 let rec labels_of_code = function
   | Coq_nil -> Labelset.empty
diff --git a/caml/RTLgenaux.ml b/caml/RTLgenaux.ml
index 336346a..61abecf 100644
--- a/caml/RTLgenaux.ml
+++ b/caml/RTLgenaux.ml
@@ -1,3 +1,47 @@
-open Cminor
+open Switch
+open CminorSel
 
 let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = false
+
+module IntOrd =
+  struct
+    type t = Integers.int
+    let compare x y =
+      if Integers.Int.eq x y then 0 else
+      if Integers.Int.ltu x y then -1 else 1
+  end
+
+module IntSet = Set.Make(IntOrd)
+
+let normalize_table tbl =
+  let rec norm seen = function
+  | CList.Coq_nil -> []
+  | CList.Coq_cons(Datatypes.Coq_pair(key, act), rem) ->
+      if IntSet.mem key seen
+      then norm seen rem
+      else (key, act) :: norm (IntSet.add key seen) rem
+  in norm IntSet.empty tbl
+
+let compile_switch default table =
+  let sw = Array.of_list (normalize_table table) in
+  Array.stable_sort (fun (n1, _) (n2, _) -> IntOrd.compare n1 n2) sw;
+  let rec build lo hi =
+    match hi - lo with
+    | 0 ->
+       CTaction default
+    | 1 ->
+       CTifeq(fst sw.(lo), snd sw.(lo), CTaction default)
+    | 2 ->
+       CTifeq(fst sw.(lo), snd sw.(lo),
+       CTifeq(fst sw.(lo+1), snd sw.(lo+1),
+       CTaction default))
+    | 3 ->
+       CTifeq(fst sw.(lo), snd sw.(lo),
+       CTifeq(fst sw.(lo+1), snd sw.(lo+1),
+       CTifeq(fst sw.(lo+2), snd sw.(lo+2),
+       CTaction default)))
+    | _ ->
+       let mid = (lo + hi) / 2 in
+       CTiflt(fst sw.(mid), build lo mid, build mid hi)
+  in build 0 (Array.length sw)
+
diff --git a/caml/RTLtypingaux.ml b/caml/RTLtypingaux.ml
index 64f839a..5ed7e6e 100644
--- a/caml/RTLtypingaux.ml
+++ b/caml/RTLtypingaux.ml
@@ -32,10 +32,6 @@ let type_instr retty (Coq_pair(pc, i)) =
       ()
   | Iop(Omove, _, _, _) -> 
       ()
-  | Iop(Oundef, Coq_nil, res, _) ->
-      ()
-  | Iop(Oundef, _, _, _) ->
-      raise (Type_error "wrong Oundef")
   | Iop(op, args, res, _) ->
       let (Coq_pair(targs, tres)) = type_of_operation op in
       set_types args targs; set_type res tres
@@ -61,6 +57,23 @@ let type_instr retty (Coq_pair(pc, i)) =
         raise(Type_error (Printf.sprintf "type mismatch in Icall(%s): %s"
                                          name msg))
       end
+  | Itailcall(sg, ros, args) ->
+      begin try
+        begin match ros with
+        | Coq_inl r -> set_type r Tint
+        | Coq_inr _ -> ()
+        end;
+        set_types args sg.sig_args;
+        if sg.sig_res <> retty then
+          raise (Type_error "mismatch on return type")
+      with Type_error msg ->
+        let name =
+          match ros with
+          | Coq_inl _ -> "<reg>"
+          | Coq_inr id -> extern_atom id in
+        raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s"
+                                         name msg))
+      end
   | Ialloc(arg, res, _) ->
       set_type arg Tint; set_type res Tint
   | Icond(cond, args, _, _) ->