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

    r2717 r2773  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open String
    4 
    5 open LabelledObjects
    6 
    7 open BitVectorTrie
    86
    97open Exp
     
    119open Arithmetic
    1210
     11open Vector
     12
     13open FoldStuff
     14
     15open BitVector
     16
     17open Extranat
     18
    1319open Integers
    1420
    1521open AST
    1622
    17 open CostLabel
     23open LabelledObjects
    1824
    1925open Proper
     
    3743open Option
    3844
    39 open Lists
    40 
    41 open Positive
    42 
    43 open Identifiers
    44 
    45 open Extranat
    46 
    47 open Vector
    48 
    4945open Div_and_mod
    5046
     
    5349open Russell
    5450
    55 open Types
     51open Util
    5652
    5753open List
    5854
    59 open Util
    60 
    61 open FoldStuff
     55open Lists
    6256
    6357open Bool
     58
     59open Relations
     60
     61open Nat
     62
     63open Positive
    6464
    6565open Hints_declaration
     
    7171open Logic
    7272
    73 open Relations
     73open Types
    7474
    75 open Nat
     75open Identifiers
    7676
    77 open BitVector
     77open CostLabel
    7878
    7979open ASM
     
    9696
    9797val strip_target :
    98   ASM.identifier0 ASM.preinstruction -> (ASM.subaddressing_mode ->
     98  ASM.identifier ASM.preinstruction -> (ASM.subaddressing_mode ->
    9999  ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum
    100100
    101101val expand_relative_jump_unsafe :
    102   Assembly.jump_length -> ASM.identifier0 ASM.preinstruction ->
     102  Assembly.jump_length -> ASM.identifier ASM.preinstruction ->
    103103  ASM.instruction List.list
    104104
     
    122122
    123123val select_reljump_length :
    124   Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
    125   -> Nat.nat -> Assembly.jump_length
     124  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
     125  Nat.nat -> Assembly.jump_length
    126126
    127127val select_call_length :
    128   Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
    129   -> Assembly.jump_length
     128  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
     129  Assembly.jump_length
    130130
    131131val select_jump_length :
    132   Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
    133   -> Assembly.jump_length
     132  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier ->
     133  Assembly.jump_length
    134134
    135135val destination_of :
    136   ASM.identifier0 ASM.preinstruction -> ASM.identifier0 Types.option
     136  ASM.identifier ASM.preinstruction -> ASM.identifier Types.option
    137137
    138 val length_of : ASM.identifier0 ASM.preinstruction -> Nat.nat
     138val length_of : ASM.identifier ASM.preinstruction -> Nat.nat
    139139
    140140val jump_expansion_step_instruction :
    141   Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
     141  Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
    142142  ASM.preinstruction -> Assembly.jump_length Types.option
    143143
Note: See TracChangeset for help on using the changeset viewer.