From 487fc42595bb43450f2b0b5a49b4edbc22892b9f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 3 Jun 2019 22:26:06 +0200
Subject: rm old select/selectl/selectf/selectfs

---
 backend/Selection.v | 61 -----------------------------------------------------
 1 file changed, 61 deletions(-)

(limited to 'backend/Selection.v')

diff --git a/backend/Selection.v b/backend/Selection.v
index 37a78853..2d407094 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -277,67 +277,6 @@ Definition sel_switch_long :=
     (fun arg ofs => subl arg (longconst (Int64.repr ofs)))
     lowlong.
 
-Definition sel_builtin_default optid ef args :=
-  OK (Sbuiltin (sel_builtin_res optid) ef
-               (sel_builtin_args args
-                                 (Machregs.builtin_constraints ef))).
-
-Definition sel_builtin optid ef args :=
-  match ef with
-    | EF_builtin name sign =>
-      (if String.string_dec name "__builtin_ternary_uint"
-       || String.string_dec name "__builtin_ternary_int"
-       then
-         match optid with
-           | None => OK Sskip
-           | Some id =>
-             match args with
-               | a1::a2::a3::nil =>
-                 OK (Sassign id (select (sel_expr a3) (sel_expr a2) (sel_expr a1)))
-               | _ => Error (msg "__builtin_ternary_(u)int: arguments")
-             end
-         end
-       else
-       if String.string_dec name "__builtin_ternary_ulong"
-       || String.string_dec name "__builtin_ternary_long"  
-       then
-         match optid with
-           | None => OK Sskip
-           | Some id =>
-             match args with
-               | a1::a2::a3::nil =>
-                 OK (Sassign id (selectl (sel_expr a3) (sel_expr a2) (sel_expr a1)))
-               | _ => Error (msg "__builtin_ternary_(u)long: arguments")
-             end
-         end
-       else
-       if String.string_dec name "__builtin_ternary_double"
-       then
-         match optid with
-           | None => OK Sskip
-           | Some id =>
-             match args with
-               | a1::a2::a3::nil =>
-                 OK (Sassign id (selectf (sel_expr a3) (sel_expr a2) (sel_expr a1)))
-               | _ => Error (msg "__builtin_ternary_double: arguments")
-             end
-         end
-       else
-       if String.string_dec name "__builtin_ternary_float"
-       then
-         match optid with
-           | None => OK Sskip
-           | Some id =>
-             match args with
-               | a1::a2::a3::nil =>
-                 OK (Sassign id (selectfs (sel_expr a3) (sel_expr a2) (sel_expr a1)))
-               | _ => Error (msg "__builtin_ternary_float: arguments")
-             end
-         end
-       else
-         sel_builtin_default optid ef args)
-    | _ => sel_builtin_default optid ef args
-
 (** "If conversion": conversion of certain if-then-else statements
   into branchless conditional move instructions. *)
 
-- 
cgit