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

    r2717 r2773  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open String
    46
     7open Exp
     8
     9open Arithmetic
     10
     11open Vector
     12
     13open FoldStuff
     14
     15open BitVector
     16
     17open Extranat
     18
     19open Integers
     20
     21open AST
     22
    523open LabelledObjects
    624
    7 open BitVectorTrie
    8 
    9 open Exp
    10 
    11 open Arithmetic
    12 
    13 open Integers
    14 
    15 open AST
     25open Proper
     26
     27open PositiveMap
     28
     29open Deqsets
     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 List
     54
     55open Lists
     56
     57open Bool
     58
     59open Relations
     60
     61open Nat
     62
     63open Positive
     64
     65open Hints_declaration
     66
     67open Core_notation
     68
     69open Pts
     70
     71open Logic
     72
     73open Types
     74
     75open Identifiers
    1676
    1777open CostLabel
    18 
    19 open Proper
    20 
    21 open PositiveMap
    22 
    23 open Deqsets
    24 
    25 open ErrorMessages
    26 
    27 open PreIdentifiers
    28 
    29 open Errors
    30 
    31 open Extralib
    32 
    33 open Setoids
    34 
    35 open Monad
    36 
    37 open Option
    38 
    39 open Lists
    40 
    41 open Positive
    42 
    43 open Identifiers
    44 
    45 open Extranat
    46 
    47 open Vector
    48 
    49 open Div_and_mod
    50 
    51 open Jmeq
    52 
    53 open Russell
    54 
    55 open Types
    56 
    57 open List
    58 
    59 open Util
    60 
    61 open FoldStuff
    62 
    63 open Bool
    64 
    65 open Hints_declaration
    66 
    67 open Core_notation
    68 
    69 open Pts
    70 
    71 open Logic
    72 
    73 open Relations
    74 
    75 open Nat
    76 
    77 open BitVector
    7878
    7979open ASM
     
    134134
    135135(** val strip_target :
    136     ASM.identifier0 ASM.preinstruction -> (ASM.subaddressing_mode ->
     136    ASM.identifier ASM.preinstruction -> (ASM.subaddressing_mode ->
    137137    ASM.subaddressing_mode ASM.preinstruction, ASM.instruction) Types.sum **)
    138138let strip_target = function
     
    184184
    185185(** val expand_relative_jump_unsafe :
    186     Assembly.jump_length -> ASM.identifier0 ASM.preinstruction ->
     186    Assembly.jump_length -> ASM.identifier ASM.preinstruction ->
    187187    ASM.instruction List.list **)
    188188let expand_relative_jump_unsafe jmp_len i =
     
    347347(** val create_label_map :
    348348    ASM.labelled_instruction List.list -> Fetch.label_map Types.sig0 **)
    349 let create_label_map program0 =
    350   (Fetch.create_label_cost_map program0).Types.fst
     349let create_label_map program =
     350  (Fetch.create_label_cost_map program).Types.fst
    351351
    352352(** val select_reljump_length :
    353     Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
     353    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
    354354    -> Nat.nat -> Assembly.jump_length **)
    355355let select_reljump_length labels old_sigma inc_sigma ppc lbl ins_len =
     
    411411
    412412(** val select_call_length :
    413     Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
     413    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
    414414    -> Assembly.jump_length **)
    415415let select_call_length labels old_sigma inc_sigma ppc lbl =
     
    473473
    474474(** val select_jump_length :
    475     Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
     475    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
    476476    -> Assembly.jump_length **)
    477477let select_jump_length labels old_sigma inc_sigma ppc lbl =
     
    535535
    536536(** val destination_of :
    537     ASM.identifier0 ASM.preinstruction -> ASM.identifier0 Types.option **)
     537    ASM.identifier ASM.preinstruction -> ASM.identifier Types.option **)
    538538let destination_of = function
    539539| ASM.ADD (x, x0) -> Types.None
     
    576576| ASM.JMP x -> Types.None
    577577
    578 (** val length_of : ASM.identifier0 ASM.preinstruction -> Nat.nat **)
     578(** val length_of : ASM.identifier ASM.preinstruction -> Nat.nat **)
    579579let length_of = function
    580580| ASM.ADD (x, x0) -> Nat.O
     
    639639
    640640(** val jump_expansion_step_instruction :
    641     Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier0
     641    Fetch.label_map -> ppc_pc_map -> ppc_pc_map -> Nat.nat -> ASM.identifier
    642642    ASM.preinstruction -> Assembly.jump_length Types.option **)
    643643let jump_expansion_step_instruction labels old_sigma inc_sigma ppc i =
     
    652652    ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map ->
    653653    ppc_pc_map Types.option Types.sig0 **)
    654 let jump_expansion_start program0 labels =
     654let jump_expansion_start program labels =
    655655  let final_policy =
    656     FoldStuff.foldl_strong (Types.pi1 program0) (fun prefix0 x tl _ p ->
    657       let { Types.fst = pc; Types.snd = sigma0 } = Types.pi1 p in
     656    FoldStuff.foldl_strong (Types.pi1 program) (fun prefix x tl _ p ->
     657      let { Types.fst = pc; Types.snd = sigma } = Types.pi1 p in
    658658      let { Types.fst = label; Types.snd = instr } = x in
    659659      let isize = instruction_size_jmplen Assembly.Short_jump instr in
     
    664664        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    665665          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    666           (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S (List.length prefix0)))
     666          (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S (List.length prefix)))
    667667        { Types.fst = (Nat.plus pc isize); Types.snd = Assembly.Short_jump }
    668         sigma0) }) { Types.fst = Nat.O; Types.snd =
     668        sigma) }) { Types.fst = Nat.O; Types.snd =
    669669      (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    670670        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
Note: See TracChangeset for help on using the changeset viewer.