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/switchRemoval.mli

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