Changeset 2827 for extracted/toCminor.ml


Ignore:
Timestamp:
Mar 8, 2013, 9:07:28 PM (8 years ago)
Author:
sacerdot
Message:

Everything extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toCminor.ml

    r2797 r2827  
    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_12925 -> h_Global x_12925
    201 | Stack x_12926 -> h_Stack x_12926
     200| Global x_13042 -> h_Global x_13042
     201| Stack x_13043 -> h_Stack x_13043
    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_12931 -> h_Global x_12931
    208 | Stack x_12932 -> h_Stack x_12932
     207| Global x_13048 -> h_Global x_13048
     208| Stack x_13049 -> h_Stack x_13049
    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_12937 -> h_Global x_12937
    215 | Stack x_12938 -> h_Stack x_12938
     214| Global x_13054 -> h_Global x_13054
     215| Stack x_13055 -> h_Stack x_13055
    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_12943 -> h_Global x_12943
    222 | Stack x_12944 -> h_Stack x_12944
     221| Global x_13060 -> h_Global x_13060
     222| Stack x_13061 -> h_Stack x_13061
    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_12949 -> h_Global x_12949
    229 | Stack x_12950 -> h_Stack x_12950
     228| Global x_13066 -> h_Global x_13066
     229| Stack x_13067 -> h_Stack x_13067
    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_12955 -> h_Global x_12955
    236 | Stack x_12956 -> h_Stack x_12956
     235| Global x_13072 -> h_Global x_13072
     236| Stack x_13073 -> h_Stack x_13073
    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_14411 -> h_MemDest x_14411
     1223| MemDest x_14528 -> h_MemDest x_14528
    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_14416 -> h_MemDest x_14416
     1230| MemDest x_14533 -> h_MemDest x_14533
    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_14421 -> h_MemDest x_14421
     1237| MemDest x_14538 -> h_MemDest x_14538
    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_14426 -> h_MemDest x_14426
     1244| MemDest x_14543 -> h_MemDest x_14543
    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_14431 -> h_MemDest x_14431
     1251| MemDest x_14548 -> h_MemDest x_14548
    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_14436 -> h_MemDest x_14436
     1258| MemDest x_14553 -> h_MemDest x_14553
    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_14471 =
     1384let rec labgen_rect_Type4 h_mk_labgen x_14588 =
    13851385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1386     x_14471
     1386    x_14588
    13871387  in
    13881388  h_mk_labgen labuniverse0 label_genlist0 __
     
    13911391    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13921392    'a1) -> labgen -> 'a1 **)
    1393 let rec labgen_rect_Type5 h_mk_labgen x_14473 =
     1393let rec labgen_rect_Type5 h_mk_labgen x_14590 =
    13941394  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1395     x_14473
     1395    x_14590
    13961396  in
    13971397  h_mk_labgen labuniverse0 label_genlist0 __
     
    14001400    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14011401    'a1) -> labgen -> 'a1 **)
    1402 let rec labgen_rect_Type3 h_mk_labgen x_14475 =
     1402let rec labgen_rect_Type3 h_mk_labgen x_14592 =
    14031403  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1404     x_14475
     1404    x_14592
    14051405  in
    14061406  h_mk_labgen labuniverse0 label_genlist0 __
     
    14091409    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14101410    'a1) -> labgen -> 'a1 **)
    1411 let rec labgen_rect_Type2 h_mk_labgen x_14477 =
     1411let rec labgen_rect_Type2 h_mk_labgen x_14594 =
    14121412  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1413     x_14477
     1413    x_14594
    14141414  in
    14151415  h_mk_labgen labuniverse0 label_genlist0 __
     
    14181418    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14191419    'a1) -> labgen -> 'a1 **)
    1420 let rec labgen_rect_Type1 h_mk_labgen x_14479 =
     1420let rec labgen_rect_Type1 h_mk_labgen x_14596 =
    14211421  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1422     x_14479
     1422    x_14596
    14231423  in
    14241424  h_mk_labgen labuniverse0 label_genlist0 __
     
    14271427    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14281428    'a1) -> labgen -> 'a1 **)
    1429 let rec labgen_rect_Type0 h_mk_labgen x_14481 =
     1429let rec labgen_rect_Type0 h_mk_labgen x_14598 =
    14301430  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1431     x_14481
     1431    x_14598
    14321432  in
    14331433  h_mk_labgen labuniverse0 label_genlist0 __
     
    15541554    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15551555    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14497 =
    1557   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14497 in
     1556let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14614 =
     1557  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14614 in
    15581558  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15591559
     
    15611561    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15621562    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14499 =
    1564   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14499 in
     1563let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14616 =
     1564  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14616 in
    15651565  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15661566
     
    15681568    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15691569    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14501 =
    1571   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14501 in
     1570let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14618 =
     1571  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14618 in
    15721572  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15731573
     
    15751575    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15761576    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14503 =
    1578   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14503 in
     1577let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14620 =
     1578  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14620 in
    15791579  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15801580
     
    15821582    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15831583    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14505 =
    1585   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14505 in
     1584let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14622 =
     1585  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14622 in
    15861586  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15871587
     
    15891589    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15901590    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14507 =
    1592   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14507 in
     1591let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14624 =
     1592  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14624 in
    15931593  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15941594
     
    16741674let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16751675| DoNotConvert -> h_DoNotConvert
    1676 | ConvertTo (x_14529, x_14528) -> h_ConvertTo x_14529 x_14528
     1676| ConvertTo (x_14646, x_14645) -> h_ConvertTo x_14646 x_14645
    16771677
    16781678(** val convert_flag_rect_Type5 :
     
    16811681let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16821682| DoNotConvert -> h_DoNotConvert
    1683 | ConvertTo (x_14534, x_14533) -> h_ConvertTo x_14534 x_14533
     1683| ConvertTo (x_14651, x_14650) -> h_ConvertTo x_14651 x_14650
    16841684
    16851685(** val convert_flag_rect_Type3 :
     
    16881688let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    16891689| DoNotConvert -> h_DoNotConvert
    1690 | ConvertTo (x_14539, x_14538) -> h_ConvertTo x_14539 x_14538
     1690| ConvertTo (x_14656, x_14655) -> h_ConvertTo x_14656 x_14655
    16911691
    16921692(** val convert_flag_rect_Type2 :
     
    16951695let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    16961696| DoNotConvert -> h_DoNotConvert
    1697 | ConvertTo (x_14544, x_14543) -> h_ConvertTo x_14544 x_14543
     1697| ConvertTo (x_14661, x_14660) -> h_ConvertTo x_14661 x_14660
    16981698
    16991699(** val convert_flag_rect_Type1 :
     
    17021702let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    17031703| DoNotConvert -> h_DoNotConvert
    1704 | ConvertTo (x_14549, x_14548) -> h_ConvertTo x_14549 x_14548
     1704| ConvertTo (x_14666, x_14665) -> h_ConvertTo x_14666 x_14665
    17051705
    17061706(** val convert_flag_rect_Type0 :
     
    17091709let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17101710| DoNotConvert -> h_DoNotConvert
    1711 | ConvertTo (x_14554, x_14553) -> h_ConvertTo x_14554 x_14553
     1711| ConvertTo (x_14671, x_14670) -> h_ConvertTo x_14671 x_14670
    17121712
    17131713(** val convert_flag_inv_rect_Type4 :
     
    17861786              ((Csyntax.typ_of_type ty), id, (Types.pi1 e2'0))) }))
    17871787        | MemDest e1' ->
    1788           Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
    1789             ul }; Types.snd = (Cminor_syntax.St_store
    1790             ((Csyntax.typ_of_type (Csyntax.typeof e2)), (Types.pi1 e1'),
    1791             (Types.pi1 e2'))) }))))
     1788          (match TypeComparison.type_eq_dec (Csyntax.typeof e1)
     1789                   (Csyntax.typeof e2) with
     1790           | Types.Inl _ ->
     1791             Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
     1792               ul }; Types.snd = (Cminor_syntax.St_store
     1793               ((Csyntax.typ_of_type (Csyntax.typeof e2)), (Types.pi1 e1'),
     1794               (Types.pi1 e2'))) })
     1795           | Types.Inr _ ->
     1796             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))))
    17921797| Csyntax.Scall (ret, ef, args) ->
    17931798  Obj.magic
     
    18211826                 in
    18221827                (fun _ ->
    1823                 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv1;
     1828                (let { Types.fst = tmp2; Types.snd = uv2 } =
     1829                   alloc_tmp vars (Csyntax.Tpointer (Csyntax.typeof e1)) uv1
     1830                 in
     1831                (fun _ ->
     1832                Obj.magic (Errors.OK { Types.fst = { Types.fst = uv2;
    18241833                  Types.snd = ul }; Types.snd = (Cminor_syntax.St_seq
    1825                   ((Cminor_syntax.St_call ((Types.Some { Types.fst = tmp;
    1826                   Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
     1834                  ((Cminor_syntax.St_store (AST.ASTptr, (Cminor_syntax.Id
     1835                  (AST.ASTptr, tmp2)), (Types.pi1 e1'))),
     1836                  (Cminor_syntax.St_seq ((Cminor_syntax.St_call ((Types.Some
     1837                  { Types.fst = tmp; Types.snd =
     1838                  (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
    18271839                  (Types.pi1 ef'0), (Types.pi1 args'))),
    18281840                  (Cminor_syntax.St_store
    18291841                  ((Csyntax.typ_of_type (Csyntax.typeof e1)),
    18301842                  (Types.pi1 e1'), (Cminor_syntax.Id
    1831                   ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))) })))
    1832                   __)))))
     1843                  ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))))) })))
     1844                  __)) __)))))
    18331845| Csyntax.Ssequence (s1, s2) ->
    18341846  Obj.magic
     
    20322044    Obj.magic
    20332045      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2034         (fun eta2434 ->
    2035         let result = eta2434 in
     2046        (fun eta2436 ->
     2047        let result = eta2436 in
    20362048        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20372049        (fun _ ->
Note: See TracChangeset for help on using the changeset viewer.