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/aSMCostsSplit.ml

    r2717 r2773  
    11open Preamble
     2
     3open Fetch
     4
     5open Hide
     6
     7open Division
     8
     9open Z
     10
     11open BitVectorZ
     12
     13open Pointers
     14
     15open Coqlib
     16
     17open Values
     18
     19open Events
     20
     21open IOMonad
     22
     23open IO
     24
     25open Sets
     26
     27open Listb
    228
    329open StructuredTraces
     
    531open AbstractStatus
    632
    7 open Status
    8 
    9 open StatusProofs
    10 
    11 open Sets
    12 
    13 open Listb
    14 
    15 open Interpret
    16 
    17 open Fetch
     33open BitVectorTrie
    1834
    1935open String
    20 
    21 open LabelledObjects
    22 
    23 open BitVectorTrie
    2436
    2537open Exp
     
    2739open Arithmetic
    2840
     41open Vector
     42
     43open FoldStuff
     44
     45open BitVector
     46
     47open Extranat
     48
    2949open Integers
    3050
    3151open AST
    3252
    33 open CostLabel
     53open LabelledObjects
    3454
    3555open Proper
     
    5373open Option
    5474
    55 open Lists
    56 
    57 open Positive
    58 
    59 open Identifiers
    60 
    61 open Extranat
    62 
    63 open Vector
    64 
    6575open Div_and_mod
    6676
     
    6979open Russell
    7080
    71 open Types
     81open Util
    7282
    7383open List
    7484
    75 open Util
    76 
    77 open FoldStuff
     85open Lists
    7886
    7987open Bool
     88
     89open Relations
     90
     91open Nat
     92
     93open Positive
    8094
    8195open Hints_declaration
     
    87101open Logic
    88102
    89 open Relations
     103open Types
    90104
    91 open Nat
     105open Identifiers
    92106
    93 open BitVector
     107open CostLabel
    94108
    95109open ASM
     110
     111open Status
     112
     113open StatusProofs
     114
     115open Interpret
    96116
    97117open ASMCosts
     
    103123    BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat -> Nat.nat
    104124    Identifiers.identifier_map Types.sig0 **)
    105 let rec traverse_code_internal code_memory cost_labels program_counter0 program_size =
     125let rec traverse_code_internal code_memory cost_labels program_counter program_size =
    106126  (match program_size with
    107127   | Nat.O -> (fun _ -> Identifiers.empty_map PreIdentifiers.CostTag)
     
    115135             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    116136             (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O))
    117            program_counter0
     137           program_counter
    118138       in
    119139       let cost_mapping =
     
    123143       (match BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    124144                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    125                 (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter0
     145                (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) program_counter
    126146                cost_labels with
    127147        | Types.None -> (fun _ -> Types.pi1 cost_mapping)
     
    129149          (fun _ ->
    130150            let cost =
    131               ASMCosts.block_cost code_memory program_counter0 cost_labels
     151              ASMCosts.block_cost code_memory program_counter cost_labels
    132152            in
    133153            Identifiers.add PreIdentifiers.CostTag (Types.pi1 cost_mapping)
     
    149169
    150170(** val compute_costs :
    151     BitVector.byte List.list -> CostLabel.costlabel
    152     BitVectorTrie.bitVectorTrie -> Nat.nat Identifiers.identifier_map
    153     Types.sig0 **)
    154 let compute_costs program0 cost_labels =
    155   let code_memory = Fetch.load_code_memory program0 in
     171    ASM.object_code -> CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
     172    Nat.nat Identifiers.identifier_map Types.sig0 **)
     173let compute_costs program cost_labels =
     174  let code_memory = Fetch.load_code_memory program in
    156175  traverse_code code_memory cost_labels
    157176
    158177(** val aSM_cost_map :
    159     (BitVector.byte List.list, CostLabel.costlabel
    160     BitVectorTrie.bitVectorTrie) Types.prod -> StructuredTraces.as_cost_map **)
     178    ASM.labelled_object_code -> StructuredTraces.as_cost_map **)
    161179let aSM_cost_map p =
    162   let cost_map = compute_costs p.Types.fst p.Types.snd in
     180  let cost_map = compute_costs p.ASM.oc p.ASM.costlabels in
    163181  (fun l_sig ->
    164182  Identifiers.lookup_present PreIdentifiers.CostTag (Types.pi1 cost_map)
    165183    (StructuredTraces.as_cost_get_label
    166       (ASMCosts.aSM_abstract_status (Fetch.load_code_memory p.Types.fst)
    167         p.Types.snd) l_sig))
     184      (ASMCosts.aSM_abstract_status (Fetch.load_code_memory p.ASM.oc)
     185        p.ASM.costlabels) l_sig))
    168186
Note: See TracChangeset for help on using the changeset viewer.