Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.mli

    r2746 r2773  
    11open Preamble
    22
     3open CostLabel
     4
     5open Coqlib
     6
     7open Proper
     8
     9open PositiveMap
     10
     11open Deqsets
     12
     13open ErrorMessages
     14
     15open PreIdentifiers
     16
     17open Errors
     18
     19open Extralib
     20
     21open Lists
     22
     23open Positive
     24
     25open Identifiers
     26
     27open Exp
     28
     29open Arithmetic
     30
     31open Vector
     32
     33open Div_and_mod
     34
     35open Util
     36
     37open FoldStuff
     38
     39open BitVector
     40
     41open Jmeq
     42
     43open Russell
     44
     45open List
     46
     47open Setoids
     48
     49open Monad
     50
     51open Option
     52
     53open Extranat
     54
     55open Bool
     56
     57open Relations
     58
     59open Nat
     60
     61open Integers
     62
     63open Hints_declaration
     64
     65open Core_notation
     66
     67open Pts
     68
     69open Logic
     70
     71open Types
     72
     73open AST
     74
     75open Csyntax
     76
     77open Label
     78
     79open Sets
     80
     81open Listb
     82
     83open Star
     84
     85open Frontend_misc
     86
     87open CexecInd
     88
     89open CexecSound
     90
     91open Casts
     92
     93open ClassifyOp
     94
     95open Smallstep
     96
     97open Extra_bool
     98
     99open FrontEndVal
     100
     101open Hide
     102
     103open ByteValues
     104
     105open GenMem
     106
     107open FrontEndMem
     108
     109open Globalenvs
     110
     111open Csem
     112
     113open SmallstepExec
     114
     115open Division
     116
     117open Z
     118
     119open BitVectorZ
     120
     121open Pointers
     122
     123open Values
     124
     125open Events
     126
     127open IOMonad
     128
     129open IO
     130
     131open Cexec
     132
     133open TypeComparison
     134
     135open SimplifyCasts
     136
     137open MemProperties
     138
     139open MemoryInjections
     140
     141open Fresh
     142
     143open SwitchRemoval
     144
     145open FrontEndOps
     146
     147open Cminor_syntax
     148
     149open ToCminor
     150
     151open Initialisation
     152
    3153open BitVectorTrie
    4 
    5 open CostLabel
    6 
    7 open Coqlib
    8 
    9 open Proper
    10 
    11 open PositiveMap
    12 
    13 open Deqsets
    14 
    15 open ErrorMessages
    16 
    17 open PreIdentifiers
    18 
    19 open Errors
    20 
    21 open Extralib
    22 
    23 open Setoids
    24 
    25 open Monad
    26 
    27 open Option
    28 
    29 open Lists
    30 
    31 open Positive
    32 
    33 open Identifiers
    34 
    35 open Exp
    36 
    37 open Arithmetic
    38 
    39 open Vector
    40 
    41 open Div_and_mod
    42 
    43 open Jmeq
    44 
    45 open Russell
    46 
    47 open List
    48 
    49 open Util
    50 
    51 open FoldStuff
    52 
    53 open BitVector
    54 
    55 open Extranat
    56 
    57 open Bool
    58 
    59 open Relations
    60 
    61 open Nat
    62 
    63 open Integers
    64 
    65 open Hints_declaration
    66 
    67 open Core_notation
    68 
    69 open Pts
    70 
    71 open Logic
    72 
    73 open Types
    74 
    75 open AST
    76 
    77 open Csyntax
    78 
    79 open Label
    80 
    81 open Sets
    82 
    83 open Listb
    84 
    85 open Star
    86 
    87 open Frontend_misc
    88 
    89 open CexecInd
    90 
    91 open CexecSound
    92 
    93 open Casts
    94 
    95 open ClassifyOp
    96 
    97 open Smallstep
    98 
    99 open Extra_bool
    100 
    101 open FrontEndVal
    102 
    103 open Hide
    104 
    105 open ByteValues
    106 
    107 open GenMem
    108 
    109 open FrontEndMem
    110 
    111 open Globalenvs
    112 
    113 open Csem
    114 
    115 open SmallstepExec
    116 
    117 open Division
    118 
    119 open Z
    120 
    121 open BitVectorZ
    122 
    123 open Pointers
    124 
    125 open Values
    126 
    127 open Events
    128 
    129 open IOMonad
    130 
    131 open IO
    132 
    133 open Cexec
    134 
    135 open TypeComparison
    136 
    137 open SimplifyCasts
    138 
    139 open MemProperties
    140 
    141 open MemoryInjections
    142 
    143 open Fresh
    144 
    145 open SwitchRemoval
    146 
    147 open FrontEndOps
    148 
    149 open Cminor_syntax
    150 
    151 open ToCminor
    152 
    153 open Initialisation
    154154
    155155open Graphs
     
    255255val colour_graph : Interference.coloured_graph_computer
    256256
    257 val back_end : RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program
    258 
    259 type object_code = BitVector.byte List.list
    260 
    261 type costlabel_map1 = CostLabel.costlabel BitVectorTrie.bitVectorTrie
     257val back_end :
     258  RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program Errors.res
    262259
    263260open Assembly
     
    274271
    275272val assembler :
    276   ASM.pseudo_assembly_program -> (object_code, costlabel_map1) Types.prod
    277   Errors.res
     273  ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res
    278274
    279275open AbstractStatus
     
    287283val lift_cost_map_back_to_front :
    288284  Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
    289   CostLabel.costlabel BitVectorTrie.bitVectorTrie -> (CostLabel.costlabel ->
    290   (__, __) Types.sum) -> StructuredTraces.as_cost_map ->
    291   Label.clight_cost_map
     285  CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
     286  StructuredTraces.as_cost_map -> Label.clight_cost_map
    292287
    293288open UtilBranch
     
    295290open ASMCostsSplit
    296291
    297 type strong_decidable = (__, __) Types.sum
    298 
    299 val strong_decidable_in_codomain :
    300   Deqsets.deqSet -> Nat.nat -> __ BitVectorTrie.bitVectorTrie -> __ ->
    301   strong_decidable
    302 
    303292val compile :
    304   Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,
     293  Csyntax.clight_program -> (ASM.labelled_object_code,
    305294  (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
    306295  Errors.res
Note: See TracChangeset for help on using the changeset viewer.