Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 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/memoryInjections.ml

    r2649 r2717  
    11open Preamble
    22
     3open SmallstepExec
     4
     5open Cexec
     6
     7open Sets
     8
     9open Listb
     10
     11open IO
     12
     13open IOMonad
     14
     15open Star
     16
     17open ClassifyOp
     18
     19open Events
     20
     21open Smallstep
     22
     23open Extra_bool
     24
     25open Values
     26
     27open FrontEndVal
     28
     29open Hide
     30
     31open ByteValues
     32
     33open Division
     34
     35open Z
     36
     37open BitVectorZ
     38
     39open Pointers
     40
     41open GenMem
     42
     43open FrontEndMem
     44
     45open Globalenvs
     46
     47open Csem
     48
     49open BitVectorTrie
     50
     51open CostLabel
     52
     53open Coqlib
     54
     55open Proper
     56
     57open PositiveMap
     58
     59open Deqsets
     60
     61open ErrorMessages
     62
     63open PreIdentifiers
     64
     65open Errors
     66
     67open Extralib
     68
     69open Setoids
     70
     71open Monad
     72
     73open Option
     74
     75open Lists
     76
     77open Positive
     78
     79open Identifiers
     80
     81open Exp
     82
     83open Arithmetic
     84
     85open Vector
     86
     87open Div_and_mod
     88
     89open Jmeq
     90
     91open Russell
     92
     93open List
     94
     95open Util
     96
     97open FoldStuff
     98
     99open BitVector
     100
     101open Extranat
     102
     103open Bool
     104
     105open Relations
     106
     107open Nat
     108
     109open Integers
     110
     111open Hints_declaration
     112
     113open Core_notation
     114
     115open Pts
     116
     117open Logic
     118
     119open Types
     120
     121open AST
     122
     123open Csyntax
     124
    3125open TypeComparison
    4 
    5 open ClassifyOp
    6 
    7 open Smallstep
    8 
    9 open Csyntax
    10 
    11 open Extra_bool
    12 
    13 open FrontEndVal
    14 
    15 open Hide
    16 
    17 open ByteValues
    18 
    19 open GenMem
    20 
    21 open FrontEndMem
    22 
    23 open Globalenvs
    24 
    25 open Csem
    26 
    27 open SmallstepExec
    28 
    29 open CostLabel
    30 
    31 open PositiveMap
    32 
    33 open Deqsets
    34 
    35 open Lists
    36 
    37 open Identifiers
    38 
    39 open Integers
    40 
    41 open AST
    42 
    43 open Division
    44 
    45 open Arithmetic
    46 
    47 open Extranat
    48 
    49 open Vector
    50 
    51 open FoldStuff
    52 
    53 open BitVector
    54 
    55 open Z
    56 
    57 open BitVectorZ
    58 
    59 open Pointers
    60 
    61 open Coqlib
    62 
    63 open Values
    64 
    65 open Events
    66 
    67 open Proper
    68 
    69 open ErrorMessages
    70 
    71 open Option
    72 
    73 open Setoids
    74 
    75 open Monad
    76 
    77 open Positive
    78 
    79 open PreIdentifiers
    80 
    81 open Errors
    82 
    83 open IOMonad
    84 
    85 open IO
    86 
    87 open Div_and_mod
    88 
    89 open Jmeq
    90 
    91 open Russell
    92 
    93 open Util
    94 
    95 open Bool
    96 
    97 open Relations
    98 
    99 open Nat
    100 
    101 open List
    102 
    103 open Hints_declaration
    104 
    105 open Core_notation
    106 
    107 open Pts
    108 
    109 open Logic
    110 
    111 open Types
    112 
    113 open Extralib
    114 
    115 open Cexec
    116 
    117 open Sets
    118 
    119 open Listb
    120 
    121 open Star
    122126
    123127open Frontend_misc
Note: See TracChangeset for help on using the changeset viewer.