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

    r2717 r2773  
    11open Preamble
    22
     3open Deqsets
     4
     5open Setoids
     6
     7open Monad
     8
     9open Option
     10
     11open Extranat
     12
     13open Vector
     14
    315open Div_and_mod
    416
     
    719open Russell
    820
     21open List
     22
     23open Util
     24
     25open FoldStuff
     26
    927open Bool
    1028
     
    1331open Nat
    1432
     33open BitVector
     34
    1535open Hints_declaration
    1636
     
    2343open Types
    2444
    25 open List
    26 
    27 open Util
    28 
    29 open Extranat
    30 
    31 open Vector
    32 
    33 open FoldStuff
    34 
    35 open BitVector
    36 
    3745open BitVectorTrie
    3846
    3947open BitVectorTrieSet
    4048
     49open State
     50
    4151open String
    4252
     53open Exp
     54
     55open Arithmetic
     56
     57open Integers
     58
     59open AST
     60
     61open LabelledObjects
     62
     63open Proper
     64
     65open PositiveMap
     66
     67open ErrorMessages
     68
     69open PreIdentifiers
     70
     71open Errors
     72
     73open Extralib
     74
     75open Lists
     76
     77open Positive
     78
     79open Identifiers
     80
     81open CostLabel
     82
     83open ASM
     84
    4385open Sets
    4486
    4587open Listb
    4688
    47 open LabelledObjects
    48 
    4989open Graphs
    5090
     
    5595open Registers
    5696
    57 open CostLabel
    58 
    5997open Hide
    6098
    61 open Proper
    62 
    63 open PositiveMap
    64 
    65 open Deqsets
    66 
    67 open ErrorMessages
    68 
    69 open PreIdentifiers
    70 
    71 open Errors
    72 
    73 open Extralib
    74 
    75 open Setoids
    76 
    77 open Monad
    78 
    79 open Option
    80 
    81 open Lists
    82 
    83 open Identifiers
    84 
    85 open Integers
    86 
    87 open AST
    88 
    8999open Division
    90100
    91 open Exp
    92 
    93 open Arithmetic
    94 
    95 open Positive
    96 
    97101open Z
    98102
     
    110114
    111115open LIN
    112 
    113 open ASM
    114 
    115 open State
    116116
    117117type aSM_universe = { id_univ : Identifiers.universe;
    118118                      current_funct : AST.ident;
    119                       ident_map : ASM.identifier0 Identifiers.identifier_map;
    120                       label_map : ASM.identifier0 Identifiers.identifier_map
     119                      ident_map : ASM.identifier Identifiers.identifier_map;
     120                      label_map : ASM.identifier Identifiers.identifier_map
    121121                                  Identifiers.identifier_map;
    122122                      address_map : BitVector.word Identifiers.identifier_map }
    123123
    124124val aSM_universe_rect_Type4 :
    125   AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    126   ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
    127   Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    128   Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
     125  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
     126  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     127  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
     128  __ -> 'a1) -> aSM_universe -> 'a1
    129129
    130130val aSM_universe_rect_Type5 :
    131   AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    132   ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
    133   Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    134   Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
     131  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
     132  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     133  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
     134  __ -> 'a1) -> aSM_universe -> 'a1
    135135
    136136val aSM_universe_rect_Type3 :
    137   AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    138   ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
    139   Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    140   Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
     137  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
     138  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     139  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
     140  __ -> 'a1) -> aSM_universe -> 'a1
    141141
    142142val aSM_universe_rect_Type2 :
    143   AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    144   ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
    145   Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    146   Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
     143  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
     144  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     145  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
     146  __ -> 'a1) -> aSM_universe -> 'a1
    147147
    148148val aSM_universe_rect_Type1 :
    149   AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    150   ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
    151   Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    152   Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
     149  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
     150  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     151  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
     152  __ -> 'a1) -> aSM_universe -> 'a1
    153153
    154154val aSM_universe_rect_Type0 :
    155   AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    156   ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
    157   Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    158   Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
     155  AST.ident List.list -> (Identifiers.universe -> AST.ident -> ASM.identifier
     156  Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     157  Identifiers.identifier_map -> BitVector.word Identifiers.identifier_map ->
     158  __ -> 'a1) -> aSM_universe -> 'a1
    159159
    160160val id_univ : AST.ident List.list -> aSM_universe -> Identifiers.universe
     
    163163
    164164val ident_map :
    165   AST.ident List.list -> aSM_universe -> ASM.identifier0
     165  AST.ident List.list -> aSM_universe -> ASM.identifier
    166166  Identifiers.identifier_map
    167167
    168168val label_map :
    169   AST.ident List.list -> aSM_universe -> ASM.identifier0
     169  AST.ident List.list -> aSM_universe -> ASM.identifier
    170170  Identifiers.identifier_map Identifiers.identifier_map
    171171
     
    176176val aSM_universe_inv_rect_Type4 :
    177177  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    178   -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     178  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    179179  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    180180  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     
    182182val aSM_universe_inv_rect_Type3 :
    183183  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    184   -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     184  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    185185  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    186186  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     
    188188val aSM_universe_inv_rect_Type2 :
    189189  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    190   -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     190  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    191191  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    192192  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     
    194194val aSM_universe_inv_rect_Type1 :
    195195  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    196   -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     196  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    197197  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    198198  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     
    200200val aSM_universe_inv_rect_Type0 :
    201201  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    202   -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     202  -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    203203  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    204204  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
     
    210210
    211211val identifier_of_label :
    212   AST.ident List.list -> Graphs.label -> ASM.identifier0
     212  AST.ident List.list -> Graphs.label -> ASM.identifier
    213213  Monad.smax_def__o__monad
    214214
    215215val identifier_of_ident :
    216   AST.ident List.list -> AST.ident -> ASM.identifier0
    217   Monad.smax_def__o__monad
     216  AST.ident List.list -> AST.ident -> ASM.identifier Monad.smax_def__o__monad
    218217
    219218val start_funct_translation :
     
    225224
    226225val aSM_fresh :
    227   AST.ident List.list -> ASM.identifier0 Monad.smax_def__o__monad
     226  AST.ident List.list -> ASM.identifier Monad.smax_def__o__monad
    228227
    229228val register_address : I8051.register -> ASM.subaddressing_mode
     
    255254  AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod -> __
    256255
    257 val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program
    258 
     256val get_symboltable :
     257  AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list
     258  Monad.smax_def__o__monad
     259
     260val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program Types.option
     261
Note: See TracChangeset for help on using the changeset viewer.