Changeset 2649 for extracted/fetch.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/fetch.ml

    r2601 r2649  
    11open Preamble
    22
    3 open Char
     3open Extranat
     4
     5open Vector
     6
     7open Div_and_mod
     8
     9open Jmeq
     10
     11open Russell
     12
     13open List
     14
     15open Util
     16
     17open FoldStuff
     18
     19open Bool
     20
     21open Relations
     22
     23open Nat
     24
     25open BitVector
     26
     27open Hints_declaration
     28
     29open Core_notation
     30
     31open Pts
     32
     33open Logic
     34
     35open Types
     36
     37open BitVectorTrie
     38
     39open Arithmetic
    440
    541open String
    642
    7 open Extranat
    8 
    9 open Vector
    10 
    11 open Div_and_mod
    12 
    13 open Jmeq
    14 
    15 open Russell
    16 
    17 open List
    18 
    19 open Util
    20 
    21 open FoldStuff
    22 
    23 open Bool
    24 
    25 open Relations
    26 
    27 open Nat
    28 
    29 open BitVector
    30 
    31 open Hints_declaration
    32 
    33 open Core_notation
    34 
    35 open Pts
    36 
    37 open Logic
    38 
    39 open Types
    40 
    41 open BitVectorTrie
    42 
    43 open Arithmetic
    44 
    4543open LabelledObjects
    4644
    47 open Coqlib
    48 
    49 open Floats
    50 
    5145open Integers
    5246
     
    6054
    6155open Deqsets
     56
     57open ErrorMessages
    6258
    6359open PreIdentifiers
     
    8985    Nat.O))))))))))))))))
    9086    (LabelledObjects.index_of0
    91       (LabelledObjects.instruction_matches_identifier ASM.aSMTag id)
    92       code_mem)
     87      (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag
     88        id) code_mem)
    9389
    9490type label_map = Nat.nat Identifiers.identifier_map
     
    10096  (Types.pi1
    10197    (FoldStuff.foldl_strong program0 (fun prefix0 x tl _ labels_costs_ppc ->
    102       (let { Types.fst = eta27681; Types.snd = ppc } =
     98      (let { Types.fst = eta24561; Types.snd = ppc } =
    10399         Types.pi1 labels_costs_ppc
    104100       in
    105101      (fun _ ->
    106       (let { Types.fst = labels; Types.snd = costs } = eta27681 in
     102      (let { Types.fst = labels; Types.snd = costs } = eta24561 in
    107103      (fun _ ->
    108104      (let { Types.fst = label; Types.snd = instr } = x in
     
    111107        match label with
    112108        | Types.None -> labels
    113         | Types.Some l -> Identifiers.add ASM.aSMTag labels l ppc
     109        | Types.Some l -> Identifiers.add PreIdentifiers.ASMTag labels l ppc
    114110      in
    115111      let costs1 =
     
    130126      { Types.fst = { Types.fst = labels1; Types.snd = costs1 }; Types.snd =
    131127      (Nat.S ppc) })) __)) __)) __) { Types.fst = { Types.fst =
    132       (Identifiers.empty_map ASM.aSMTag); Types.snd = (BitVectorTrie.Stub
    133       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    134       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))) };
    135       Types.snd = Nat.O })).Types.fst
     128      (Identifiers.empty_map PreIdentifiers.ASMTag); Types.snd =
     129      (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     130      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     131      Nat.O))))))))))))))))) }; Types.snd = Nat.O })).Types.fst
    136132
    137133(** val create_label_cost_map :
     
    147143  Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    148144    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    149     Nat.O)))))))))))))))) (Identifiers.lookup_def ASM.aSMTag labels id Nat.O)
     145    Nat.O))))))))))))))))
     146    (Identifiers.lookup_def PreIdentifiers.ASMTag labels id Nat.O)
    150147
    151148(** val bitvector_max_nat : Nat.nat -> Nat.nat **)
Note: See TracChangeset for help on using the changeset viewer.