Changeset 2717 for extracted/toCminor.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (8 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toCminor.ml

    r2649 r2717  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open CostLabel
    46
     
    3032
    3133open Identifiers
     34
     35open Exp
    3236
    3337open Arithmetic
     
    196200    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    197201let rec var_type_rect_Type4 h_Global h_Stack h_Local = function
    198 | Global x_11147 -> h_Global x_11147
    199 | Stack x_11148 -> h_Stack x_11148
     202| Global x_12977 -> h_Global x_12977
     203| Stack x_12978 -> h_Stack x_12978
    200204| Local -> h_Local
    201205
     
    203207    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    204208let rec var_type_rect_Type5 h_Global h_Stack h_Local = function
    205 | Global x_11153 -> h_Global x_11153
    206 | Stack x_11154 -> h_Stack x_11154
     209| Global x_12983 -> h_Global x_12983
     210| Stack x_12984 -> h_Stack x_12984
    207211| Local -> h_Local
    208212
     
    210214    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    211215let rec var_type_rect_Type3 h_Global h_Stack h_Local = function
    212 | Global x_11159 -> h_Global x_11159
    213 | Stack x_11160 -> h_Stack x_11160
     216| Global x_12989 -> h_Global x_12989
     217| Stack x_12990 -> h_Stack x_12990
    214218| Local -> h_Local
    215219
     
    217221    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    218222let rec var_type_rect_Type2 h_Global h_Stack h_Local = function
    219 | Global x_11165 -> h_Global x_11165
    220 | Stack x_11166 -> h_Stack x_11166
     223| Global x_12995 -> h_Global x_12995
     224| Stack x_12996 -> h_Stack x_12996
    221225| Local -> h_Local
    222226
     
    224228    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    225229let rec var_type_rect_Type1 h_Global h_Stack h_Local = function
    226 | Global x_11171 -> h_Global x_11171
    227 | Stack x_11172 -> h_Stack x_11172
     230| Global x_13001 -> h_Global x_13001
     231| Stack x_13002 -> h_Stack x_13002
    228232| Local -> h_Local
    229233
     
    231235    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    232236let rec var_type_rect_Type0 h_Global h_Stack h_Local = function
    233 | Global x_11177 -> h_Global x_11177
    234 | Stack x_11178 -> h_Stack x_11178
     237| Global x_13007 -> h_Global x_13007
     238| Stack x_13008 -> h_Stack x_13008
    235239| Local -> h_Local
    236240
     
    12191223let rec destination_rect_Type4 vars h_IdDest h_MemDest = function
    12201224| IdDest (id, ty) -> h_IdDest id ty __
    1221 | MemDest x_11225 -> h_MemDest x_11225
     1225| MemDest x_14463 -> h_MemDest x_14463
    12221226
    12231227(** val destination_rect_Type5 :
     
    12261230let rec destination_rect_Type5 vars h_IdDest h_MemDest = function
    12271231| IdDest (id, ty) -> h_IdDest id ty __
    1228 | MemDest x_11230 -> h_MemDest x_11230
     1232| MemDest x_14468 -> h_MemDest x_14468
    12291233
    12301234(** val destination_rect_Type3 :
     
    12331237let rec destination_rect_Type3 vars h_IdDest h_MemDest = function
    12341238| IdDest (id, ty) -> h_IdDest id ty __
    1235 | MemDest x_11235 -> h_MemDest x_11235
     1239| MemDest x_14473 -> h_MemDest x_14473
    12361240
    12371241(** val destination_rect_Type2 :
     
    12401244let rec destination_rect_Type2 vars h_IdDest h_MemDest = function
    12411245| IdDest (id, ty) -> h_IdDest id ty __
    1242 | MemDest x_11240 -> h_MemDest x_11240
     1246| MemDest x_14478 -> h_MemDest x_14478
    12431247
    12441248(** val destination_rect_Type1 :
     
    12471251let rec destination_rect_Type1 vars h_IdDest h_MemDest = function
    12481252| IdDest (id, ty) -> h_IdDest id ty __
    1249 | MemDest x_11245 -> h_MemDest x_11245
     1253| MemDest x_14483 -> h_MemDest x_14483
    12501254
    12511255(** val destination_rect_Type0 :
     
    12541258let rec destination_rect_Type0 vars h_IdDest h_MemDest = function
    12551259| IdDest (id, ty) -> h_IdDest id ty __
    1256 | MemDest x_11250 -> h_MemDest x_11250
     1260| MemDest x_14488 -> h_MemDest x_14488
    12571261
    12581262(** val destination_inv_rect_Type4 :
     
    13821386    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13831387    'a1) -> labgen -> 'a1 **)
    1384 let rec labgen_rect_Type4 h_mk_labgen x_11285 =
     1388let rec labgen_rect_Type4 h_mk_labgen x_14523 =
    13851389  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1386     x_11285
     1390    x_14523
    13871391  in
    13881392  h_mk_labgen labuniverse0 label_genlist0 __
     
    13911395    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13921396    'a1) -> labgen -> 'a1 **)
    1393 let rec labgen_rect_Type5 h_mk_labgen x_11287 =
     1397let rec labgen_rect_Type5 h_mk_labgen x_14525 =
    13941398  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1395     x_11287
     1399    x_14525
    13961400  in
    13971401  h_mk_labgen labuniverse0 label_genlist0 __
     
    14001404    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14011405    'a1) -> labgen -> 'a1 **)
    1402 let rec labgen_rect_Type3 h_mk_labgen x_11289 =
     1406let rec labgen_rect_Type3 h_mk_labgen x_14527 =
    14031407  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1404     x_11289
     1408    x_14527
    14051409  in
    14061410  h_mk_labgen labuniverse0 label_genlist0 __
     
    14091413    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14101414    'a1) -> labgen -> 'a1 **)
    1411 let rec labgen_rect_Type2 h_mk_labgen x_11291 =
     1415let rec labgen_rect_Type2 h_mk_labgen x_14529 =
    14121416  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1413     x_11291
     1417    x_14529
    14141418  in
    14151419  h_mk_labgen labuniverse0 label_genlist0 __
     
    14181422    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14191423    'a1) -> labgen -> 'a1 **)
    1420 let rec labgen_rect_Type1 h_mk_labgen x_11293 =
     1424let rec labgen_rect_Type1 h_mk_labgen x_14531 =
    14211425  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1422     x_11293
     1426    x_14531
    14231427  in
    14241428  h_mk_labgen labuniverse0 label_genlist0 __
     
    14271431    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14281432    'a1) -> labgen -> 'a1 **)
    1429 let rec labgen_rect_Type0 h_mk_labgen x_11295 =
     1433let rec labgen_rect_Type0 h_mk_labgen x_14533 =
    14301434  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1431     x_11295
     1435    x_14533
    14321436  in
    14331437  h_mk_labgen labuniverse0 label_genlist0 __
     
    15541558    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15551559    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_11311 =
    1557   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11311 in
     1560let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14549 =
     1561  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14549 in
    15581562  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15591563
     
    15611565    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15621566    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_11313 =
    1564   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11313 in
     1567let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14551 =
     1568  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14551 in
    15651569  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15661570
     
    15681572    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15691573    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_11315 =
    1571   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11315 in
     1574let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14553 =
     1575  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14553 in
    15721576  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15731577
     
    15751579    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15761580    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_11317 =
    1578   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11317 in
     1581let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14555 =
     1582  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14555 in
    15791583  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15801584
     
    15821586    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15831587    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_11319 =
    1585   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11319 in
     1588let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14557 =
     1589  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14557 in
    15861590  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15871591
     
    15891593    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15901594    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_11321 =
    1592   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_11321 in
     1595let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14559 =
     1596  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14559 in
    15931597  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15941598
     
    16741678let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16751679| DoNotConvert -> h_DoNotConvert
    1676 | ConvertTo (x_11343, x_11342) -> h_ConvertTo x_11343 x_11342
     1680| ConvertTo (x_14581, x_14580) -> h_ConvertTo x_14581 x_14580
    16771681
    16781682(** val convert_flag_rect_Type5 :
     
    16811685let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16821686| DoNotConvert -> h_DoNotConvert
    1683 | ConvertTo (x_11348, x_11347) -> h_ConvertTo x_11348 x_11347
     1687| ConvertTo (x_14586, x_14585) -> h_ConvertTo x_14586 x_14585
    16841688
    16851689(** val convert_flag_rect_Type3 :
     
    16881692let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    16891693| DoNotConvert -> h_DoNotConvert
    1690 | ConvertTo (x_11353, x_11352) -> h_ConvertTo x_11353 x_11352
     1694| ConvertTo (x_14591, x_14590) -> h_ConvertTo x_14591 x_14590
    16911695
    16921696(** val convert_flag_rect_Type2 :
     
    16951699let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    16961700| DoNotConvert -> h_DoNotConvert
    1697 | ConvertTo (x_11358, x_11357) -> h_ConvertTo x_11358 x_11357
     1701| ConvertTo (x_14596, x_14595) -> h_ConvertTo x_14596 x_14595
    16981702
    16991703(** val convert_flag_rect_Type1 :
     
    17021706let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    17031707| DoNotConvert -> h_DoNotConvert
    1704 | ConvertTo (x_11363, x_11362) -> h_ConvertTo x_11363 x_11362
     1708| ConvertTo (x_14601, x_14600) -> h_ConvertTo x_14601 x_14600
    17051709
    17061710(** val convert_flag_rect_Type0 :
     
    17091713let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17101714| DoNotConvert -> h_DoNotConvert
    1711 | ConvertTo (x_11368, x_11367) -> h_ConvertTo x_11368 x_11367
     1715| ConvertTo (x_14606, x_14605) -> h_ConvertTo x_14606 x_14605
    17121716
    17131717(** val convert_flag_inv_rect_Type4 :
     
    20322036    Obj.magic
    20332037      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2034         (fun eta1273 ->
    2035         let result = eta1273 in
     2038        (fun eta2862 ->
     2039        let result = eta2862 in
    20362040        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20372041        (fun _ ->
Note: See TracChangeset for help on using the changeset viewer.