Changeset 2960 for extracted/toCminor.ml


Ignore:
Timestamp:
Mar 26, 2013, 4:51:40 PM (7 years ago)
Author:
sacerdot
Message:

New extraction, it diverges in RTL execution now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toCminor.ml

    r2951 r2960  
    198198    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    199199let rec var_type_rect_Type4 h_Global h_Stack h_Local = function
    200 | Global x_13081 -> h_Global x_13081
    201 | Stack x_13082 -> h_Stack x_13082
     200| Global x_138 -> h_Global x_138
     201| Stack x_139 -> h_Stack x_139
    202202| Local -> h_Local
    203203
     
    205205    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    206206let rec var_type_rect_Type5 h_Global h_Stack h_Local = function
    207 | Global x_13087 -> h_Global x_13087
    208 | Stack x_13088 -> h_Stack x_13088
     207| Global x_144 -> h_Global x_144
     208| Stack x_145 -> h_Stack x_145
    209209| Local -> h_Local
    210210
     
    212212    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    213213let rec var_type_rect_Type3 h_Global h_Stack h_Local = function
    214 | Global x_13093 -> h_Global x_13093
    215 | Stack x_13094 -> h_Stack x_13094
     214| Global x_150 -> h_Global x_150
     215| Stack x_151 -> h_Stack x_151
    216216| Local -> h_Local
    217217
     
    219219    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    220220let rec var_type_rect_Type2 h_Global h_Stack h_Local = function
    221 | Global x_13099 -> h_Global x_13099
    222 | Stack x_13100 -> h_Stack x_13100
     221| Global x_156 -> h_Global x_156
     222| Stack x_157 -> h_Stack x_157
    223223| Local -> h_Local
    224224
     
    226226    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    227227let rec var_type_rect_Type1 h_Global h_Stack h_Local = function
    228 | Global x_13105 -> h_Global x_13105
    229 | Stack x_13106 -> h_Stack x_13106
     228| Global x_162 -> h_Global x_162
     229| Stack x_163 -> h_Stack x_163
    230230| Local -> h_Local
    231231
     
    233233    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    234234let rec var_type_rect_Type0 h_Global h_Stack h_Local = function
    235 | Global x_13111 -> h_Global x_13111
    236 | Stack x_13112 -> h_Stack x_13112
     235| Global x_168 -> h_Global x_168
     236| Stack x_169 -> h_Stack x_169
    237237| Local -> h_Local
    238238
     
    12211221let rec destination_rect_Type4 vars h_IdDest h_MemDest = function
    12221222| IdDest (id, ty) -> h_IdDest id ty __
    1223 | MemDest x_14567 -> h_MemDest x_14567
     1223| MemDest x_216 -> h_MemDest x_216
    12241224
    12251225(** val destination_rect_Type5 :
     
    12281228let rec destination_rect_Type5 vars h_IdDest h_MemDest = function
    12291229| IdDest (id, ty) -> h_IdDest id ty __
    1230 | MemDest x_14572 -> h_MemDest x_14572
     1230| MemDest x_221 -> h_MemDest x_221
    12311231
    12321232(** val destination_rect_Type3 :
     
    12351235let rec destination_rect_Type3 vars h_IdDest h_MemDest = function
    12361236| IdDest (id, ty) -> h_IdDest id ty __
    1237 | MemDest x_14577 -> h_MemDest x_14577
     1237| MemDest x_226 -> h_MemDest x_226
    12381238
    12391239(** val destination_rect_Type2 :
     
    12421242let rec destination_rect_Type2 vars h_IdDest h_MemDest = function
    12431243| IdDest (id, ty) -> h_IdDest id ty __
    1244 | MemDest x_14582 -> h_MemDest x_14582
     1244| MemDest x_231 -> h_MemDest x_231
    12451245
    12461246(** val destination_rect_Type1 :
     
    12491249let rec destination_rect_Type1 vars h_IdDest h_MemDest = function
    12501250| IdDest (id, ty) -> h_IdDest id ty __
    1251 | MemDest x_14587 -> h_MemDest x_14587
     1251| MemDest x_236 -> h_MemDest x_236
    12521252
    12531253(** val destination_rect_Type0 :
     
    12561256let rec destination_rect_Type0 vars h_IdDest h_MemDest = function
    12571257| IdDest (id, ty) -> h_IdDest id ty __
    1258 | MemDest x_14592 -> h_MemDest x_14592
     1258| MemDest x_241 -> h_MemDest x_241
    12591259
    12601260(** val destination_inv_rect_Type4 :
     
    13821382    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13831383    'a1) -> labgen -> 'a1 **)
    1384 let rec labgen_rect_Type4 h_mk_labgen x_14627 =
    1385   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1386     x_14627
     1384let rec labgen_rect_Type4 h_mk_labgen x_276 =
     1385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_276
    13871386  in
    13881387  h_mk_labgen labuniverse0 label_genlist0 __
     
    13911390    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13921391    'a1) -> labgen -> 'a1 **)
    1393 let rec labgen_rect_Type5 h_mk_labgen x_14629 =
    1394   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1395     x_14629
     1392let rec labgen_rect_Type5 h_mk_labgen x_278 =
     1393  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_278
    13961394  in
    13971395  h_mk_labgen labuniverse0 label_genlist0 __
     
    14001398    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14011399    'a1) -> labgen -> 'a1 **)
    1402 let rec labgen_rect_Type3 h_mk_labgen x_14631 =
    1403   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1404     x_14631
     1400let rec labgen_rect_Type3 h_mk_labgen x_280 =
     1401  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_280
    14051402  in
    14061403  h_mk_labgen labuniverse0 label_genlist0 __
     
    14091406    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14101407    'a1) -> labgen -> 'a1 **)
    1411 let rec labgen_rect_Type2 h_mk_labgen x_14633 =
    1412   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1413     x_14633
     1408let rec labgen_rect_Type2 h_mk_labgen x_282 =
     1409  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_282
    14141410  in
    14151411  h_mk_labgen labuniverse0 label_genlist0 __
     
    14181414    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14191415    'a1) -> labgen -> 'a1 **)
    1420 let rec labgen_rect_Type1 h_mk_labgen x_14635 =
    1421   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1422     x_14635
     1416let rec labgen_rect_Type1 h_mk_labgen x_284 =
     1417  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_284
    14231418  in
    14241419  h_mk_labgen labuniverse0 label_genlist0 __
     
    14271422    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14281423    'a1) -> labgen -> 'a1 **)
    1429 let rec labgen_rect_Type0 h_mk_labgen x_14637 =
    1430   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1431     x_14637
     1424let rec labgen_rect_Type0 h_mk_labgen x_286 =
     1425  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_286
    14321426  in
    14331427  h_mk_labgen labuniverse0 label_genlist0 __
     
    15541548    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15551549    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14653 =
    1557   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14653 in
     1550let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_302 =
     1551  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_302 in
    15581552  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15591553
     
    15611555    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15621556    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14655 =
    1564   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14655 in
     1557let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_304 =
     1558  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_304 in
    15651559  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15661560
     
    15681562    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15691563    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14657 =
    1571   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14657 in
     1564let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_306 =
     1565  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_306 in
    15721566  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15731567
     
    15751569    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15761570    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14659 =
    1578   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14659 in
     1571let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_308 =
     1572  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_308 in
    15791573  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15801574
     
    15821576    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15831577    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14661 =
    1585   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14661 in
     1578let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_310 =
     1579  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_310 in
    15861580  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15871581
     
    15891583    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15901584    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14663 =
    1592   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14663 in
     1585let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_312 =
     1586  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_312 in
    15931587  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15941588
     
    16741668let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16751669| DoNotConvert -> h_DoNotConvert
    1676 | ConvertTo (x_14685, x_14684) -> h_ConvertTo x_14685 x_14684
     1670| ConvertTo (x_334, x_333) -> h_ConvertTo x_334 x_333
    16771671
    16781672(** val convert_flag_rect_Type5 :
     
    16811675let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16821676| DoNotConvert -> h_DoNotConvert
    1683 | ConvertTo (x_14690, x_14689) -> h_ConvertTo x_14690 x_14689
     1677| ConvertTo (x_339, x_338) -> h_ConvertTo x_339 x_338
    16841678
    16851679(** val convert_flag_rect_Type3 :
     
    16881682let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    16891683| DoNotConvert -> h_DoNotConvert
    1690 | ConvertTo (x_14695, x_14694) -> h_ConvertTo x_14695 x_14694
     1684| ConvertTo (x_344, x_343) -> h_ConvertTo x_344 x_343
    16911685
    16921686(** val convert_flag_rect_Type2 :
     
    16951689let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    16961690| DoNotConvert -> h_DoNotConvert
    1697 | ConvertTo (x_14700, x_14699) -> h_ConvertTo x_14700 x_14699
     1691| ConvertTo (x_349, x_348) -> h_ConvertTo x_349 x_348
    16981692
    16991693(** val convert_flag_rect_Type1 :
     
    17021696let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    17031697| DoNotConvert -> h_DoNotConvert
    1704 | ConvertTo (x_14705, x_14704) -> h_ConvertTo x_14705 x_14704
     1698| ConvertTo (x_354, x_353) -> h_ConvertTo x_354 x_353
    17051699
    17061700(** val convert_flag_rect_Type0 :
     
    17091703let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17101704| DoNotConvert -> h_DoNotConvert
    1711 | ConvertTo (x_14710, x_14709) -> h_ConvertTo x_14710 x_14709
     1705| ConvertTo (x_359, x_358) -> h_ConvertTo x_359 x_358
    17121706
    17131707(** val convert_flag_inv_rect_Type4 :
     
    20322026        (Cminor_syntax.St_cost (l, s1')) })))
    20332027
    2034 (** val alloc_params :
     2028(** val alloc_params_main :
    20352029    var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag ->
    20362030    AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list
     
    20382032    Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt)
    20392033    Types.prod Types.sig0 Errors.res **)
    2040 let alloc_params vars lbls statement uv ul rettyp params s =
     2034let alloc_params_main vars lbls statement uv ul rettyp params s =
    20412035  Util.foldl (fun su it ->
    20422036    let { Types.fst = id; Types.snd = ty } = it in
    20432037    Obj.magic
    20442038      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2045         (fun eta2436 ->
    2046         let result = eta2436 in
     2039        (fun eta650 ->
     2040        let result = eta650 in
    20472041        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20482042        (fun _ ->
     
    20622056             | Local -> (fun _ -> Errors.OK result)) __)))) __))) (Errors.OK
    20632057    s) params
     2058
     2059(** val alloc_params :
     2060    var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag ->
     2061    AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list
     2062    -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod
     2063    Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt)
     2064    Types.prod Types.sig0 Errors.res **)
     2065let alloc_params vars lbls statement uv ul rettyp params su =
     2066  (let { Types.fst = tl; Types.snd = s0 } = Types.pi1 su in
     2067  (match s0 with
     2068   | Cminor_syntax.St_skip ->
     2069     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2070   | Cminor_syntax.St_assign (x, x0, x1) ->
     2071     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2072   | Cminor_syntax.St_store (x, x0, x1) ->
     2073     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2074   | Cminor_syntax.St_call (x, x0, x1) ->
     2075     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2076   | Cminor_syntax.St_seq (x, x0) ->
     2077     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2078   | Cminor_syntax.St_ifthenelse (x, x0, x1, x2, x3) ->
     2079     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2080   | Cminor_syntax.St_return x ->
     2081     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2082   | Cminor_syntax.St_label (x, x0) ->
     2083     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2084   | Cminor_syntax.St_goto x ->
     2085     (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
     2086   | Cminor_syntax.St_cost (cl, s') ->
     2087     (fun _ ->
     2088       Obj.magic
     2089         (Monad.m_bind0 (Monad.max_def Errors.res0)
     2090           (Obj.magic
     2091             (alloc_params_main vars lbls statement uv ul rettyp params
     2092               { Types.fst = tl; Types.snd = s' })) (fun tls ->
     2093           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     2094             (Types.pi1 tls).Types.fst; Types.snd = (Cminor_syntax.St_cost
     2095             (cl, (Types.pi1 tls).Types.snd)) }))))) __
    20642096
    20652097(** val populate_lenv :
Note: See TracChangeset for help on using the changeset viewer.