Changeset 2951 for extracted/joint.mli


Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/joint.mli

    r2867 r2951  
    13371337val good_if_rect_Type4 :
    13381338  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
    1339   -> __ -> __ -> __ -> 'a1) -> 'a1
     1339  -> __ -> __ -> 'a1) -> 'a1
    13401340
    13411341val good_if_rect_Type5 :
    13421342  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
    1343   -> __ -> __ -> __ -> 'a1) -> 'a1
     1343  -> __ -> __ -> 'a1) -> 'a1
    13441344
    13451345val good_if_rect_Type3 :
    13461346  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
    1347   -> __ -> __ -> __ -> 'a1) -> 'a1
     1347  -> __ -> __ -> 'a1) -> 'a1
    13481348
    13491349val good_if_rect_Type2 :
    13501350  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
    1351   -> __ -> __ -> __ -> 'a1) -> 'a1
     1351  -> __ -> __ -> 'a1) -> 'a1
    13521352
    13531353val good_if_rect_Type1 :
    13541354  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
    1355   -> __ -> __ -> __ -> 'a1) -> 'a1
     1355  -> __ -> __ -> 'a1) -> 'a1
    13561356
    13571357val good_if_rect_Type0 :
    13581358  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
    1359   -> __ -> __ -> __ -> 'a1) -> 'a1
     1359  -> __ -> __ -> 'a1) -> 'a1
    13601360
    13611361val good_if_inv_rect_Type4 :
    13621362  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
    1363   -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
     1363  -> __ -> __ -> __ -> 'a1) -> 'a1
    13641364
    13651365val good_if_inv_rect_Type3 :
    13661366  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
    1367   -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
     1367  -> __ -> __ -> __ -> 'a1) -> 'a1
    13681368
    13691369val good_if_inv_rect_Type2 :
    13701370  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
    1371   -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
     1371  -> __ -> __ -> __ -> 'a1) -> 'a1
    13721372
    13731373val good_if_inv_rect_Type1 :
    13741374  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
    1375   -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
     1375  -> __ -> __ -> __ -> 'a1) -> 'a1
    13761376
    13771377val good_if_inv_rect_Type0 :
    13781378  params -> AST.ident List.list -> joint_internal_function -> (__ -> __ -> __
    1379   -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
     1379  -> __ -> __ -> __ -> 'a1) -> 'a1
     1380
     1381val good_if_discr :
     1382  params -> AST.ident List.list -> joint_internal_function -> __
    13801383
    13811384val good_if_jmdiscr :
     
    14021405type joint_function = joint_closed_internal_function AST.fundef
    14031406
    1404 type joint_program = (joint_function, Nat.nat) AST.program
     1407type joint_program = { joint_prog : (joint_function, AST.init_data List.list)
     1408                                    AST.program;
     1409                       init_cost_label : CostLabel.costlabel }
     1410
     1411val joint_program_rect_Type4 :
     1412  params -> ((joint_function, AST.init_data List.list) AST.program ->
     1413  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1414
     1415val joint_program_rect_Type5 :
     1416  params -> ((joint_function, AST.init_data List.list) AST.program ->
     1417  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1418
     1419val joint_program_rect_Type3 :
     1420  params -> ((joint_function, AST.init_data List.list) AST.program ->
     1421  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1422
     1423val joint_program_rect_Type2 :
     1424  params -> ((joint_function, AST.init_data List.list) AST.program ->
     1425  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1426
     1427val joint_program_rect_Type1 :
     1428  params -> ((joint_function, AST.init_data List.list) AST.program ->
     1429  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1430
     1431val joint_program_rect_Type0 :
     1432  params -> ((joint_function, AST.init_data List.list) AST.program ->
     1433  CostLabel.costlabel -> 'a1) -> joint_program -> 'a1
     1434
     1435val joint_prog :
     1436  params -> joint_program -> (joint_function, AST.init_data List.list)
     1437  AST.program
     1438
     1439val init_cost_label : params -> joint_program -> CostLabel.costlabel
     1440
     1441val joint_program_inv_rect_Type4 :
     1442  params -> joint_program -> ((joint_function, AST.init_data List.list)
     1443  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
     1444
     1445val joint_program_inv_rect_Type3 :
     1446  params -> joint_program -> ((joint_function, AST.init_data List.list)
     1447  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
     1448
     1449val joint_program_inv_rect_Type2 :
     1450  params -> joint_program -> ((joint_function, AST.init_data List.list)
     1451  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
     1452
     1453val joint_program_inv_rect_Type1 :
     1454  params -> joint_program -> ((joint_function, AST.init_data List.list)
     1455  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
     1456
     1457val joint_program_inv_rect_Type0 :
     1458  params -> joint_program -> ((joint_function, AST.init_data List.list)
     1459  AST.program -> CostLabel.costlabel -> __ -> 'a1) -> 'a1
     1460
     1461val joint_program_discr : params -> joint_program -> joint_program -> __
     1462
     1463val joint_program_jmdiscr : params -> joint_program -> joint_program -> __
     1464
     1465val dpi1__o__joint_prog__o__inject :
     1466  params -> (joint_program, 'a1) Types.dPair -> (joint_function,
     1467  AST.init_data List.list) AST.program Types.sig0
     1468
     1469val eject__o__joint_prog__o__inject :
     1470  params -> joint_program Types.sig0 -> (joint_function, AST.init_data
     1471  List.list) AST.program Types.sig0
     1472
     1473val joint_prog__o__inject :
     1474  params -> joint_program -> (joint_function, AST.init_data List.list)
     1475  AST.program Types.sig0
     1476
     1477val dpi1__o__joint_prog :
     1478  params -> (joint_program, 'a1) Types.dPair -> (joint_function,
     1479  AST.init_data List.list) AST.program
     1480
     1481val eject__o__joint_prog :
     1482  params -> joint_program Types.sig0 -> (joint_function, AST.init_data
     1483  List.list) AST.program
    14051484
    14061485type stack_cost_model = (AST.ident, Nat.nat) Types.prod List.list
     
    14081487val stack_cost : params -> joint_program -> stack_cost_model
    14091488
     1489open Extra_bool
     1490
     1491open Coqlib
     1492
     1493open Values
     1494
     1495open FrontEndVal
     1496
     1497open GenMem
     1498
     1499open FrontEndMem
     1500
     1501open Globalenvs
     1502
    14101503val globals_stacksize : params -> joint_program -> Nat.nat
    14111504
Note: See TracChangeset for help on using the changeset viewer.