Changeset 2773 for extracted/compiler.ml


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

    r2746 r2773  
    11open Preamble
    22
     3open CostLabel
     4
     5open Coqlib
     6
     7open Proper
     8
     9open PositiveMap
     10
     11open Deqsets
     12
     13open ErrorMessages
     14
     15open PreIdentifiers
     16
     17open Errors
     18
     19open Extralib
     20
     21open Lists
     22
     23open Positive
     24
     25open Identifiers
     26
     27open Exp
     28
     29open Arithmetic
     30
     31open Vector
     32
     33open Div_and_mod
     34
     35open Util
     36
     37open FoldStuff
     38
     39open BitVector
     40
     41open Jmeq
     42
     43open Russell
     44
     45open List
     46
     47open Setoids
     48
     49open Monad
     50
     51open Option
     52
     53open Extranat
     54
     55open Bool
     56
     57open Relations
     58
     59open Nat
     60
     61open Integers
     62
     63open Hints_declaration
     64
     65open Core_notation
     66
     67open Pts
     68
     69open Logic
     70
     71open Types
     72
     73open AST
     74
     75open Csyntax
     76
     77open Label
     78
     79open Sets
     80
     81open Listb
     82
     83open Star
     84
     85open Frontend_misc
     86
     87open CexecInd
     88
     89open CexecSound
     90
     91open Casts
     92
     93open ClassifyOp
     94
     95open Smallstep
     96
     97open Extra_bool
     98
     99open FrontEndVal
     100
     101open Hide
     102
     103open ByteValues
     104
     105open GenMem
     106
     107open FrontEndMem
     108
     109open Globalenvs
     110
     111open Csem
     112
     113open SmallstepExec
     114
     115open Division
     116
     117open Z
     118
     119open BitVectorZ
     120
     121open Pointers
     122
     123open Values
     124
     125open Events
     126
     127open IOMonad
     128
     129open IO
     130
     131open Cexec
     132
     133open TypeComparison
     134
     135open SimplifyCasts
     136
     137open MemProperties
     138
     139open MemoryInjections
     140
     141open Fresh
     142
     143open SwitchRemoval
     144
     145open FrontEndOps
     146
     147open Cminor_syntax
     148
     149open ToCminor
     150
     151open Initialisation
     152
    3153open BitVectorTrie
    4 
    5 open CostLabel
    6 
    7 open Coqlib
    8 
    9 open Proper
    10 
    11 open PositiveMap
    12 
    13 open Deqsets
    14 
    15 open ErrorMessages
    16 
    17 open PreIdentifiers
    18 
    19 open Errors
    20 
    21 open Extralib
    22 
    23 open Setoids
    24 
    25 open Monad
    26 
    27 open Option
    28 
    29 open Lists
    30 
    31 open Positive
    32 
    33 open Identifiers
    34 
    35 open Exp
    36 
    37 open Arithmetic
    38 
    39 open Vector
    40 
    41 open Div_and_mod
    42 
    43 open Jmeq
    44 
    45 open Russell
    46 
    47 open List
    48 
    49 open Util
    50 
    51 open FoldStuff
    52 
    53 open BitVector
    54 
    55 open Extranat
    56 
    57 open Bool
    58 
    59 open Relations
    60 
    61 open Nat
    62 
    63 open Integers
    64 
    65 open Hints_declaration
    66 
    67 open Core_notation
    68 
    69 open Pts
    70 
    71 open Logic
    72 
    73 open Types
    74 
    75 open AST
    76 
    77 open Csyntax
    78 
    79 open Label
    80 
    81 open Sets
    82 
    83 open Listb
    84 
    85 open Star
    86 
    87 open Frontend_misc
    88 
    89 open CexecInd
    90 
    91 open CexecSound
    92 
    93 open Casts
    94 
    95 open ClassifyOp
    96 
    97 open Smallstep
    98 
    99 open Extra_bool
    100 
    101 open FrontEndVal
    102 
    103 open Hide
    104 
    105 open ByteValues
    106 
    107 open GenMem
    108 
    109 open FrontEndMem
    110 
    111 open Globalenvs
    112 
    113 open Csem
    114 
    115 open SmallstepExec
    116 
    117 open Division
    118 
    119 open Z
    120 
    121 open BitVectorZ
    122 
    123 open Pointers
    124 
    125 open Values
    126 
    127 open Events
    128 
    129 open IOMonad
    130 
    131 open IO
    132 
    133 open Cexec
    134 
    135 open TypeComparison
    136 
    137 open SimplifyCasts
    138 
    139 open MemProperties
    140 
    141 open MemoryInjections
    142 
    143 open Fresh
    144 
    145 open SwitchRemoval
    146 
    147 open FrontEndOps
    148 
    149 open Cminor_syntax
    150 
    151 open ToCminor
    152 
    153 open Initialisation
    154154
    155155open Graphs
     
    191191  let p0 = SwitchRemoval.program_switch_removal p in
    192192  let { Types.fst = p'; Types.snd = init_cost } = Label.clight_label p0 in
    193   let p3 = SimplifyCasts.simplify_program p' in
     193  let p1 = SimplifyCasts.simplify_program p' in
    194194  Obj.magic
    195195    (Monad.m_bind0 (Monad.max_def Errors.res0)
    196       (Obj.magic (ToCminor.clight_to_cminor p3)) (fun p4 ->
    197       let p5 = ToRTLabs.cminor_to_rtlabs init_cost p4 in
    198       (match CostCheck.check_cost_program p5 with
     196      (Obj.magic (ToCminor.clight_to_cminor p1)) (fun p2 ->
     197      let p3 = ToRTLabs.cminor_to_rtlabs init_cost p2 in
     198      (match CostCheck.check_cost_program p3 with
    199199       | Bool.True ->
    200          (match CostInj.check_program_cost_injectivity p5 with
     200         (match CostInj.check_program_cost_injectivity p3 with
    201201          | Bool.True ->
    202202            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    203               { Types.fst = init_cost; Types.snd = p' }; Types.snd = p5 }
     203              { Types.fst = init_cost; Types.snd = p' }; Types.snd = p3 }
    204204          | Bool.False ->
    205205            Obj.magic (Errors.Error
     
    277277
    278278(** val back_end :
    279     RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program **)
     279    RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program Errors.res **)
    280280let back_end p =
    281281  let p0 = RTLabsToRTL.rtlabs_to_rtl p in
    282   let p3 = RTLToERTL.rtl_to_ertl p0 in
    283   let p4 = ERTLToERTLptr.ertl_to_ertlptr p3 in
    284   let p5 = ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p4 in
    285   let p6 = LTLToLIN.ltl_to_lin p5 in LINToASM.lin_to_asm p6
    286 
    287 type object_code = BitVector.byte List.list
    288 
    289 type costlabel_map1 = CostLabel.costlabel BitVectorTrie.bitVectorTrie
     282  let p1 = RTLToERTL.rtl_to_ertl p0 in
     283  let p2 = ERTLToERTLptr.ertl_to_ertlptr p1 in
     284  let p3 = ERTLptrToLTL.ertlptr_to_ltl compute_fixpoint colour_graph p2 in
     285  let p4 = LTLToLIN.ltl_to_lin p3 in
     286  Errors.opt_to_res (Errors.msg ErrorMessages.AssemblyTooLarge)
     287    (LINToASM.lin_to_asm p4)
    290288
    291289open Assembly
     
    302300
    303301(** val assembler :
    304     ASM.pseudo_assembly_program -> (object_code, costlabel_map1) Types.prod
    305     Errors.res **)
     302    ASM.pseudo_assembly_program -> ASM.labelled_object_code Errors.res **)
    306303let assembler p =
    307   let { Types.fst = preamble0; Types.snd = list_instr } = p in
    308   let p' = { Types.fst = preamble0; Types.snd = list_instr } in
    309304  Obj.magic
    310305    (Monad.m_bind0 (Monad.max_def Errors.res0)
    311306      (Obj.magic
    312307        (Errors.opt_to_res (Errors.msg ErrorMessages.Jump_expansion_failed)
    313           (Policy.jump_expansion' (Types.coerc_pair_sigma p'))))
    314       (fun sigma_pol ->
    315       let sigma0 = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
     308          (Policy.jump_expansion' p))) (fun sigma_pol ->
     309      let sigma = fun ppc -> (Types.pi1 sigma_pol).Types.fst ppc in
    316310      let pol = fun ppc -> (Types.pi1 sigma_pol).Types.snd ppc in
    317       Obj.magic (Errors.OK (Types.pi1 (Assembly.assembly p sigma0 pol)))))
     311      Obj.magic (Errors.OK (Types.pi1 (Assembly.assembly p sigma pol)))))
    318312
    319313open AbstractStatus
     
    327321(** val lift_cost_map_back_to_front :
    328322    Csyntax.clight_program -> BitVector.byte BitVectorTrie.bitVectorTrie ->
    329     CostLabel.costlabel BitVectorTrie.bitVectorTrie -> (CostLabel.costlabel
    330     -> (__, __) Types.sum) -> StructuredTraces.as_cost_map ->
    331     Label.clight_cost_map **)
    332 let lift_cost_map_back_to_front clight code_memory lbls dec k asm_cost_map =
    333   StructuredTraces.lift_sigma_map_id Nat.O dec k asm_cost_map
     323    CostLabel.costlabel BitVectorTrie.bitVectorTrie ->
     324    StructuredTraces.as_cost_map -> Label.clight_cost_map **)
     325let lift_cost_map_back_to_front clight code_memory lbls k asm_cost_map =
     326  StructuredTraces.lift_sigma_map_id Nat.O
     327    (BitVectorTrie.strong_decidable_in_codomain
     328      (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S (Nat.S
     329      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     330      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (Obj.magic lbls))
     331    (Obj.magic k) (Obj.magic asm_cost_map)
    334332
    335333open UtilBranch
     
    337335open ASMCostsSplit
    338336
    339 type strong_decidable = (__, __) Types.sum
    340 
    341 (** val strong_decidable_in_codomain :
    342     Deqsets.deqSet -> Nat.nat -> __ BitVectorTrie.bitVectorTrie -> __ ->
    343     strong_decidable **)
    344 let strong_decidable_in_codomain a0 n m =
    345   BitVectorTrie.bitVectorTrie_rect_Type0 (fun a' a1 ->
    346     Bool.bool_inv_rect_Type0 (Deqsets.eqb a0 a' a1) (fun _ -> Types.Inl __)
    347       (fun _ -> Types.Inr __)) (fun n0 l r hl hr a1 ->
    348     match hl a1 with
    349     | Types.Inl _ -> Types.Inl __
    350     | Types.Inr _ ->
    351       (match hr a1 with
    352        | Types.Inl _ -> Types.Inl __
    353        | Types.Inr _ -> Types.Inr __)) (fun n0 a1 -> Types.Inr __) n m
    354 
    355337(** val compile :
    356     Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,
     338    Csyntax.clight_program -> (ASM.labelled_object_code,
    357339    (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
    358340    Errors.res **)
     
    361343    (Monad.m_bind3 (Monad.max_def Errors.res0) (Obj.magic (front_end p))
    362344      (fun init_cost p' p0 ->
    363       let p3 = back_end p0 in
    364       Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p3))
    365         (fun p4 ->
    366         let k = ASMCostsSplit.aSM_cost_map p4 in
    367         let k' =
    368           lift_cost_map_back_to_front p'
    369             (Fetch.load_code_memory p4.Types.fst) p4.Types.snd
    370             (Obj.magic
    371               (strong_decidable_in_codomain
    372                 (Identifiers.deq_identifier PreIdentifiers.CostTag) (Nat.S
    373                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    374                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    375                 Nat.O)))))))))))))))) (Obj.magic p4).Types.snd)) k
    376         in
    377         Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = p4;
    378           Types.snd = { Types.dpi1 = p'; Types.dpi2 = k' } })))
    379 
     345      Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (back_end p0))
     346        (fun p1 ->
     347        Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (assembler p1))
     348          (fun p2 ->
     349          let k = ASMCostsSplit.aSM_cost_map p2 in
     350          let k' =
     351            lift_cost_map_back_to_front p' (Fetch.load_code_memory p2.ASM.oc)
     352              p2.ASM.costlabels k
     353          in
     354          Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = p2;
     355            Types.snd = { Types.dpi1 = p'; Types.dpi2 = k' } }))))
     356
Note: See TracChangeset for help on using the changeset viewer.