Changeset 2717 for extracted/csyntax.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/csyntax.ml

    r2649 r2717  
    2727open Identifiers
    2828
     29open Exp
     30
    2931open Arithmetic
    3032
     
    6870
    6971open Coqlib
     72
     73open BitVectorTrie
    7074
    7175open CostLabel
     
    12011205    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12021206    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1203 let rec function_rect_Type4 h_mk_function x_2206 =
     1207let rec function_rect_Type4 h_mk_function x_4417 =
    12041208  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1205     fn_body = fn_body0 } = x_2206
     1209    fn_body = fn_body0 } = x_4417
    12061210  in
    12071211  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12101214    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12111215    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1212 let rec function_rect_Type5 h_mk_function x_2208 =
     1216let rec function_rect_Type5 h_mk_function x_4419 =
    12131217  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1214     fn_body = fn_body0 } = x_2208
     1218    fn_body = fn_body0 } = x_4419
    12151219  in
    12161220  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12191223    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12201224    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1221 let rec function_rect_Type3 h_mk_function x_2210 =
     1225let rec function_rect_Type3 h_mk_function x_4421 =
    12221226  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1223     fn_body = fn_body0 } = x_2210
     1227    fn_body = fn_body0 } = x_4421
    12241228  in
    12251229  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12281232    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12291233    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1230 let rec function_rect_Type2 h_mk_function x_2212 =
     1234let rec function_rect_Type2 h_mk_function x_4423 =
    12311235  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1232     fn_body = fn_body0 } = x_2212
     1236    fn_body = fn_body0 } = x_4423
    12331237  in
    12341238  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12371241    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12381242    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1239 let rec function_rect_Type1 h_mk_function x_2214 =
     1243let rec function_rect_Type1 h_mk_function x_4425 =
    12401244  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1241     fn_body = fn_body0 } = x_2214
     1245    fn_body = fn_body0 } = x_4425
    12421246  in
    12431247  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12461250    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12471251    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1248 let rec function_rect_Type0 h_mk_function x_2216 =
     1252let rec function_rect_Type0 h_mk_function x_4427 =
    12491253  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1250     fn_body = fn_body0 } = x_2216
     1254    fn_body = fn_body0 } = x_4427
    12511255  in
    12521256  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    13201324    clight_fundef -> 'a1 **)
    13211325let rec clight_fundef_rect_Type4 h_CL_Internal h_CL_External = function
    1322 | CL_Internal x_2238 -> h_CL_Internal x_2238
    1323 | CL_External (x_2241, x_2240, x_2239) -> h_CL_External x_2241 x_2240 x_2239
     1326| CL_Internal x_4449 -> h_CL_Internal x_4449
     1327| CL_External (x_4452, x_4451, x_4450) -> h_CL_External x_4452 x_4451 x_4450
    13241328
    13251329(** val clight_fundef_rect_Type5 :
     
    13271331    clight_fundef -> 'a1 **)
    13281332let rec clight_fundef_rect_Type5 h_CL_Internal h_CL_External = function
    1329 | CL_Internal x_2245 -> h_CL_Internal x_2245
    1330 | CL_External (x_2248, x_2247, x_2246) -> h_CL_External x_2248 x_2247 x_2246
     1333| CL_Internal x_4456 -> h_CL_Internal x_4456
     1334| CL_External (x_4459, x_4458, x_4457) -> h_CL_External x_4459 x_4458 x_4457
    13311335
    13321336(** val clight_fundef_rect_Type3 :
     
    13341338    clight_fundef -> 'a1 **)
    13351339let rec clight_fundef_rect_Type3 h_CL_Internal h_CL_External = function
    1336 | CL_Internal x_2252 -> h_CL_Internal x_2252
    1337 | CL_External (x_2255, x_2254, x_2253) -> h_CL_External x_2255 x_2254 x_2253
     1340| CL_Internal x_4463 -> h_CL_Internal x_4463
     1341| CL_External (x_4466, x_4465, x_4464) -> h_CL_External x_4466 x_4465 x_4464
    13381342
    13391343(** val clight_fundef_rect_Type2 :
     
    13411345    clight_fundef -> 'a1 **)
    13421346let rec clight_fundef_rect_Type2 h_CL_Internal h_CL_External = function
    1343 | CL_Internal x_2259 -> h_CL_Internal x_2259
    1344 | CL_External (x_2262, x_2261, x_2260) -> h_CL_External x_2262 x_2261 x_2260
     1347| CL_Internal x_4470 -> h_CL_Internal x_4470
     1348| CL_External (x_4473, x_4472, x_4471) -> h_CL_External x_4473 x_4472 x_4471
    13451349
    13461350(** val clight_fundef_rect_Type1 :
     
    13481352    clight_fundef -> 'a1 **)
    13491353let rec clight_fundef_rect_Type1 h_CL_Internal h_CL_External = function
    1350 | CL_Internal x_2266 -> h_CL_Internal x_2266
    1351 | CL_External (x_2269, x_2268, x_2267) -> h_CL_External x_2269 x_2268 x_2267
     1354| CL_Internal x_4477 -> h_CL_Internal x_4477
     1355| CL_External (x_4480, x_4479, x_4478) -> h_CL_External x_4480 x_4479 x_4478
    13521356
    13531357(** val clight_fundef_rect_Type0 :
     
    13551359    clight_fundef -> 'a1 **)
    13561360let rec clight_fundef_rect_Type0 h_CL_Internal h_CL_External = function
    1357 | CL_Internal x_2273 -> h_CL_Internal x_2273
    1358 | CL_External (x_2276, x_2275, x_2274) -> h_CL_External x_2276 x_2275 x_2274
     1361| CL_Internal x_4484 -> h_CL_Internal x_4484
     1362| CL_External (x_4487, x_4486, x_4485) -> h_CL_External x_4487 x_4486 x_4485
    13591363
    13601364(** val clight_fundef_inv_rect_Type4 :
     
    15311535(** val mode_rect_Type4 :
    15321536    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1533 let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_2326 = function
     1537let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_4537 = function
    15341538| By_value t -> h_By_value t
    15351539| By_reference -> h_By_reference
     
    15381542(** val mode_rect_Type5 :
    15391543    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1540 let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_2331 = function
     1544let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_4542 = function
    15411545| By_value t -> h_By_value t
    15421546| By_reference -> h_By_reference
     
    15451549(** val mode_rect_Type3 :
    15461550    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1547 let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_2336 = function
     1551let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_4547 = function
    15481552| By_value t -> h_By_value t
    15491553| By_reference -> h_By_reference
     
    15521556(** val mode_rect_Type2 :
    15531557    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1554 let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_2341 = function
     1558let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_4552 = function
    15551559| By_value t -> h_By_value t
    15561560| By_reference -> h_By_reference
     
    15591563(** val mode_rect_Type1 :
    15601564    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1561 let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_2346 = function
     1565let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_4557 = function
    15621566| By_value t -> h_By_value t
    15631567| By_reference -> h_By_reference
     
    15661570(** val mode_rect_Type0 :
    15671571    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1568 let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_2351 = function
     1572let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_4562 = function
    15691573| By_value t -> h_By_value t
    15701574| By_reference -> h_By_reference
Note: See TracChangeset for help on using the changeset viewer.