Imported Upstream version 0.2

[pkg-cerco/acc-trusted.git] / extracted / switchRemoval.ml

diff --git a/extracted/switchRemoval.ml b/extracted/switchRemoval.ml
index 3a873f716e9589180701189cb81ae442b8cf3166..c018da29d5b627768edebfc747e66d33f3d154e8 100644 (file)
--- a/extracted/switchRemoval.ml
+++ b/extracted/switchRemoval.ml
@@ -173,10 +173,10 @@ let rec produce_cond e switch_cases u exit =
     { Types.fst = { Types.fst = (Csyntax.Slabel (lab, st')); Types.snd =
     lab }; Types.snd = u1 }
   | Csyntax.LScase (sz, tag, st, other_cases) ->
-    let { Types.fst = eta2108; Types.snd = u1 } =
+    let { Types.fst = eta2130; Types.snd = u1 } =
       produce_cond e other_cases u exit
     in
-    let { Types.fst = sub_statements; Types.snd = sub_label } = eta2108 in
+    let { Types.fst = sub_statements; Types.snd = sub_label } = eta2130 in
     let st' = convert_break_to_goto st exit in
     let { Types.fst = lab; Types.snd = u2 } =
       Identifiers.fresh PreIdentifiers.SymbolTag u1
@@ -198,10 +198,10 @@ let simplify_switch e switch_cases uv =
   let { Types.fst = exit_label; Types.snd = uv1 } =
     Identifiers.fresh PreIdentifiers.SymbolTag uv
   in
-  let { Types.fst = eta2109; Types.snd = uv2 } =
+  let { Types.fst = eta2131; Types.snd = uv2 } =
     produce_cond e switch_cases uv1 exit_label
   in
-  let { Types.fst = result; Types.snd = useless_label } = eta2109 in
+  let { Types.fst = result; Types.snd = useless_label } = eta2131 in
   { Types.fst = (Csyntax.Ssequence (result, (Csyntax.Slabel (exit_label,
   Csyntax.Sskip)))); Types.snd = uv2 }
 
@@ -218,36 +218,36 @@ let rec switch_removal st u =
   | Csyntax.Scall (x, x0, x1) ->
     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
   | Csyntax.Ssequence (s1, s2) ->
-    let { Types.fst = eta2123; Types.snd = u' } = switch_removal s1 u in
-    let { Types.fst = s1'; Types.snd = acc1 } = eta2123 in
-    let { Types.fst = eta2122; Types.snd = u'' } = switch_removal s2 u' in
-    let { Types.fst = s2'; Types.snd = acc2 } = eta2122 in
+    let { Types.fst = eta2145; Types.snd = u' } = switch_removal s1 u in
+    let { Types.fst = s1'; Types.snd = acc1 } = eta2145 in
+    let { Types.fst = eta2144; Types.snd = u'' } = switch_removal s2 u' in
+    let { Types.fst = s2'; Types.snd = acc2 } = eta2144 in
     { Types.fst = { Types.fst = (Csyntax.Ssequence (s1', s2')); Types.snd =
     (List.append acc1 acc2) }; Types.snd = u'' }
   | Csyntax.Sifthenelse (e, s1, s2) ->
-    let { Types.fst = eta2125; Types.snd = u' } = switch_removal s1 u in
-    let { Types.fst = s1'; Types.snd = acc1 } = eta2125 in
-    let { Types.fst = eta2124; Types.snd = u'' } = switch_removal s2 u' in
-    let { Types.fst = s2'; Types.snd = acc2 } = eta2124 in
+    let { Types.fst = eta2147; Types.snd = u' } = switch_removal s1 u in
+    let { Types.fst = s1'; Types.snd = acc1 } = eta2147 in
+    let { Types.fst = eta2146; Types.snd = u'' } = switch_removal s2 u' in
+    let { Types.fst = s2'; Types.snd = acc2 } = eta2146 in
     { Types.fst = { Types.fst = (Csyntax.Sifthenelse (e, s1', s2'));
     Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
   | Csyntax.Swhile (e, body) ->
-    let { Types.fst = eta2126; Types.snd = u' } = switch_removal body u in
-    let { Types.fst = body'; Types.snd = acc } = eta2126 in
+    let { Types.fst = eta2148; Types.snd = u' } = switch_removal body u in
+    let { Types.fst = body'; Types.snd = acc } = eta2148 in
     { Types.fst = { Types.fst = (Csyntax.Swhile (e, body')); Types.snd =
     acc }; Types.snd = u' }
   | Csyntax.Sdowhile (e, body) ->
-    let { Types.fst = eta2127; Types.snd = u' } = switch_removal body u in
-    let { Types.fst = body'; Types.snd = acc } = eta2127 in
+    let { Types.fst = eta2149; Types.snd = u' } = switch_removal body u in
+    let { Types.fst = body'; Types.snd = acc } = eta2149 in
     { Types.fst = { Types.fst = (Csyntax.Sdowhile (e, body')); Types.snd =
     acc }; Types.snd = u' }
   | Csyntax.Sfor (s1, e, s2, s3) ->
-    let { Types.fst = eta2130; Types.snd = u' } = switch_removal s1 u in
-    let { Types.fst = s1'; Types.snd = acc1 } = eta2130 in
-    let { Types.fst = eta2129; Types.snd = u'' } = switch_removal s2 u' in
-    let { Types.fst = s2'; Types.snd = acc2 } = eta2129 in
-    let { Types.fst = eta2128; Types.snd = u''' } = switch_removal s3 u'' in
-    let { Types.fst = s3'; Types.snd = acc3 } = eta2128 in
+    let { Types.fst = eta2152; Types.snd = u' } = switch_removal s1 u in
+    let { Types.fst = s1'; Types.snd = acc1 } = eta2152 in
+    let { Types.fst = eta2151; Types.snd = u'' } = switch_removal s2 u' in
+    let { Types.fst = s2'; Types.snd = acc2 } = eta2151 in
+    let { Types.fst = eta2150; Types.snd = u''' } = switch_removal s3 u'' in
+    let { Types.fst = s3'; Types.snd = acc3 } = eta2150 in
     { Types.fst = { Types.fst = (Csyntax.Sfor (s1', e, s2', s3'));
     Types.snd = (List.append acc1 (List.append acc2 acc3)) }; Types.snd =
     u''' }
@@ -258,10 +258,10 @@ let rec switch_removal st u =
   | Csyntax.Sreturn x ->
     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
   | Csyntax.Sswitch (e, branches) ->
-    let { Types.fst = eta2131; Types.snd = u' } =
+    let { Types.fst = eta2153; Types.snd = u' } =
       switch_removal_branches branches u
     in
-    let { Types.fst = sf_branches; Types.snd = acc } = eta2131 in
+    let { Types.fst = sf_branches; Types.snd = acc } = eta2153 in
     let { Types.fst = switch_tmp; Types.snd = u'' } =
       Identifiers.fresh PreIdentifiers.SymbolTag u'
     in
@@ -275,15 +275,15 @@ let rec switch_removal st u =
     Types.snd = (List.Cons ({ Types.fst = switch_tmp; Types.snd =
     (Csyntax.typeof e) }, acc)) }; Types.snd = u''' }
   | Csyntax.Slabel (label, body) ->
-    let { Types.fst = eta2132; Types.snd = u' } = switch_removal body u in
-    let { Types.fst = body'; Types.snd = acc } = eta2132 in
+    let { Types.fst = eta2154; Types.snd = u' } = switch_removal body u in
+    let { Types.fst = body'; Types.snd = acc } = eta2154 in
     { Types.fst = { Types.fst = (Csyntax.Slabel (label, body')); Types.snd =
     acc }; Types.snd = u' }
   | Csyntax.Sgoto x ->
     { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
   | Csyntax.Scost (cost, body) ->
-    let { Types.fst = eta2133; Types.snd = u' } = switch_removal body u in
-    let { Types.fst = body'; Types.snd = acc } = eta2133 in
+    let { Types.fst = eta2155; Types.snd = u' } = switch_removal body u in
+    let { Types.fst = body'; Types.snd = acc } = eta2155 in
     { Types.fst = { Types.fst = (Csyntax.Scost (cost, body')); Types.snd =
     acc }; Types.snd = u' }
 (** val switch_removal_branches :
@@ -293,17 +293,17 @@ let rec switch_removal st u =
 and switch_removal_branches l u =
   match l with
   | Csyntax.LSdefault st ->
-    let { Types.fst = eta2134; Types.snd = u' } = switch_removal st u in
-    let { Types.fst = st'; Types.snd = acc1 } = eta2134 in
+    let { Types.fst = eta2156; Types.snd = u' } = switch_removal st u in
+    let { Types.fst = st'; Types.snd = acc1 } = eta2156 in
     { Types.fst = { Types.fst = (Csyntax.LSdefault st'); Types.snd = acc1 };
     Types.snd = u' }
   | Csyntax.LScase (sz, int, st, tl) ->
-    let { Types.fst = eta2136; Types.snd = u' } =
+    let { Types.fst = eta2158; Types.snd = u' } =
       switch_removal_branches tl u
     in
-    let { Types.fst = tl_result; Types.snd = acc1 } = eta2136 in
-    let { Types.fst = eta2135; Types.snd = u'' } = switch_removal st u' in
-    let { Types.fst = st'; Types.snd = acc2 } = eta2135 in
+    let { Types.fst = tl_result; Types.snd = acc1 } = eta2158 in
+    let { Types.fst = eta2157; Types.snd = u'' } = switch_removal st u' in
+    let { Types.fst = st'; Types.snd = acc2 } = eta2157 in
     { Types.fst = { Types.fst = (Csyntax.LScase (sz, int, st', tl_result));
     Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
 
@@ -311,21 +311,21 @@ and switch_removal_branches l u =
     (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
     Identifiers.universe) Types.prod -> 'a1 **)
 let ret_st x =
-  let { Types.fst = eta2137; Types.snd = u } = x in eta2137.Types.fst
+  let { Types.fst = eta2159; Types.snd = u } = x in eta2159.Types.fst
 
 (** val ret_vars :
     (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
     Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
     List.list **)
 let ret_vars x =
-  let { Types.fst = eta2138; Types.snd = u } = x in eta2138.Types.snd
+  let { Types.fst = eta2160; Types.snd = u } = x in eta2160.Types.snd
 
 (** val ret_u :
     (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
     Identifiers.universe) Types.prod -> Identifiers.universe **)
 let ret_u x =
-  let { Types.fst = eta2139; Types.snd = u } = x in
-  let { Types.fst = s; Types.snd = vars } = eta2139 in u
+  let { Types.fst = eta2161; Types.snd = u } = x in
+  let { Types.fst = s; Types.snd = vars } = eta2161 in u
 
 (** val least_identifier : PreIdentifiers.identifier **)
 let least_identifier =
@@ -405,10 +405,10 @@ let max_id_of_function f =
     Types.prod List.list) Types.prod **)
 let function_switch_removal f =
   let u = Fresh.universe_of_max (max_id_of_function f) in
-  let { Types.fst = eta2140; Types.snd = u' } =
+  let { Types.fst = eta2162; Types.snd = u' } =
     switch_removal f.Csyntax.fn_body u
   in
-  let { Types.fst = st; Types.snd = vars } = eta2140 in
+  let { Types.fst = st; Types.snd = vars } = eta2162 in
   let result = { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
     f.Csyntax.fn_params; Csyntax.fn_vars =
     (List.append vars f.Csyntax.fn_vars); Csyntax.fn_body = st }