Changeset 2773 for extracted/lINToASM.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/lINToASM.ml

    r2743 r2773  
    11open Preamble
    22
     3open Deqsets
     4
     5open Setoids
     6
     7open Monad
     8
     9open Option
     10
     11open Extranat
     12
     13open Vector
     14
    315open Div_and_mod
    416
     
    719open Russell
    820
     21open List
     22
     23open Util
     24
     25open FoldStuff
     26
    927open Bool
    1028
     
    1331open Nat
    1432
     33open BitVector
     34
    1535open Hints_declaration
    1636
     
    2343open Types
    2444
    25 open List
    26 
    27 open Util
    28 
    29 open Extranat
    30 
    31 open Vector
    32 
    33 open FoldStuff
    34 
    35 open BitVector
    36 
    3745open BitVectorTrie
    3846
    3947open BitVectorTrieSet
    4048
     49open State
     50
    4151open String
    4252
     53open Exp
     54
     55open Arithmetic
     56
     57open Integers
     58
     59open AST
     60
     61open LabelledObjects
     62
     63open Proper
     64
     65open PositiveMap
     66
     67open ErrorMessages
     68
     69open PreIdentifiers
     70
     71open Errors
     72
     73open Extralib
     74
     75open Lists
     76
     77open Positive
     78
     79open Identifiers
     80
     81open CostLabel
     82
     83open ASM
     84
    4385open Sets
    4486
    4587open Listb
    4688
    47 open LabelledObjects
    48 
    4989open Graphs
    5090
     
    5595open Registers
    5696
    57 open CostLabel
    58 
    5997open Hide
    6098
    61 open Proper
    62 
    63 open PositiveMap
    64 
    65 open Deqsets
    66 
    67 open ErrorMessages
    68 
    69 open PreIdentifiers
    70 
    71 open Errors
    72 
    73 open Extralib
    74 
    75 open Setoids
    76 
    77 open Monad
    78 
    79 open Option
    80 
    81 open Lists
    82 
    83 open Identifiers
    84 
    85 open Integers
    86 
    87 open AST
    88 
    8999open Division
    90100
    91 open Exp
    92 
    93 open Arithmetic
    94 
    95 open Positive
    96 
    97101open Z
    98102
     
    110114
    111115open LIN
    112 
    113 open ASM
    114 
    115 open State
    116116
    117117type aSM_universe = { id_univ : Identifiers.universe;
    118118                      current_funct : AST.ident;
    119                       ident_map : ASM.identifier0 Identifiers.identifier_map;
    120                       label_map : ASM.identifier0 Identifiers.identifier_map
     119                      ident_map : ASM.identifier Identifiers.identifier_map;
     120                      label_map : ASM.identifier Identifiers.identifier_map
    121121                                  Identifiers.identifier_map;
    122122                      address_map : BitVector.word Identifiers.identifier_map }
     
    124124(** val aSM_universe_rect_Type4 :
    125125    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    126     ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     126    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    127127    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    128128    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    129 let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_24106 =
     129let rec aSM_universe_rect_Type4 globals h_mk_ASM_universe x_19468 =
    130130  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    131131    ident_map0; label_map = label_map0; address_map = address_map0 } =
    132     x_24106
     132    x_19468
    133133  in
    134134  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    137137(** val aSM_universe_rect_Type5 :
    138138    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    139     ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     139    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    140140    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    141141    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    142 let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_24108 =
     142let rec aSM_universe_rect_Type5 globals h_mk_ASM_universe x_19470 =
    143143  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    144144    ident_map0; label_map = label_map0; address_map = address_map0 } =
    145     x_24108
     145    x_19470
    146146  in
    147147  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    150150(** val aSM_universe_rect_Type3 :
    151151    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    152     ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     152    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    153153    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    154154    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    155 let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_24110 =
     155let rec aSM_universe_rect_Type3 globals h_mk_ASM_universe x_19472 =
    156156  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    157157    ident_map0; label_map = label_map0; address_map = address_map0 } =
    158     x_24110
     158    x_19472
    159159  in
    160160  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    163163(** val aSM_universe_rect_Type2 :
    164164    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    165     ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     165    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    166166    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    167167    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    168 let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_24112 =
     168let rec aSM_universe_rect_Type2 globals h_mk_ASM_universe x_19474 =
    169169  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    170170    ident_map0; label_map = label_map0; address_map = address_map0 } =
    171     x_24112
     171    x_19474
    172172  in
    173173  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    176176(** val aSM_universe_rect_Type1 :
    177177    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    178     ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     178    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    179179    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    180180    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    181 let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_24114 =
     181let rec aSM_universe_rect_Type1 globals h_mk_ASM_universe x_19476 =
    182182  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    183183    ident_map0; label_map = label_map0; address_map = address_map0 } =
    184     x_24114
     184    x_19476
    185185  in
    186186  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    189189(** val aSM_universe_rect_Type0 :
    190190    AST.ident List.list -> (Identifiers.universe -> AST.ident ->
    191     ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     191    ASM.identifier Identifiers.identifier_map -> ASM.identifier
    192192    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    193193    Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1 **)
    194 let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_24116 =
     194let rec aSM_universe_rect_Type0 globals h_mk_ASM_universe x_19478 =
    195195  let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
    196196    ident_map0; label_map = label_map0; address_map = address_map0 } =
    197     x_24116
     197    x_19478
    198198  in
    199199  h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     
    210210
    211211(** val ident_map :
    212     AST.ident List.list -> aSM_universe -> ASM.identifier0
     212    AST.ident List.list -> aSM_universe -> ASM.identifier
    213213    Identifiers.identifier_map **)
    214214let rec ident_map globals xxx =
     
    216216
    217217(** val label_map :
    218     AST.ident List.list -> aSM_universe -> ASM.identifier0
     218    AST.ident List.list -> aSM_universe -> ASM.identifier
    219219    Identifiers.identifier_map Identifiers.identifier_map **)
    220220let rec label_map globals xxx =
     
    229229(** val aSM_universe_inv_rect_Type4 :
    230230    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    231     -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     231    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    232232    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    233233    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
     
    237237(** val aSM_universe_inv_rect_Type3 :
    238238    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    239     -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     239    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    240240    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    241241    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
     
    245245(** val aSM_universe_inv_rect_Type2 :
    246246    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    247     -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     247    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    248248    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    249249    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
     
    253253(** val aSM_universe_inv_rect_Type1 :
    254254    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    255     -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     255    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    256256    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    257257    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
     
    261261(** val aSM_universe_inv_rect_Type0 :
    262262    AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
    263     -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
     263    -> ASM.identifier Identifiers.identifier_map -> ASM.identifier
    264264    Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
    265265    Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1 **)
     
    279279let new_ASM_universe p =
    280280  let globals_addr_internal = fun res_offset x_size ->
    281     let { Types.fst = res1; Types.snd = offset0 } = res_offset in
    282     let { Types.fst = eta28996; Types.snd = size } = x_size in
    283     let { Types.fst = x; Types.snd = region0 } = eta28996 in
     281    let { Types.fst = res; Types.snd = offset } = res_offset in
     282    let { Types.fst = eta27824; Types.snd = size } = x_size in
     283    let { Types.fst = x; Types.snd = region } = eta27824 in
    284284    { Types.fst =
    285     (Identifiers.add PreIdentifiers.SymbolTag res1 x
     285    (Identifiers.add PreIdentifiers.SymbolTag res x
    286286      (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    287287        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    288         Nat.O)))))))))))))))) offset0)); Types.snd =
    289     (Z.zplus offset0 (Z.z_of_nat size)) }
     288        Nat.O)))))))))))))))) offset)); Types.snd =
     289    (Z.zplus offset (Z.z_of_nat size)) }
    290290  in
    291291  let addresses =
     
    300300
    301301(** val identifier_of_label :
    302     AST.ident List.list -> Graphs.label -> ASM.identifier0
     302    AST.ident List.list -> Graphs.label -> ASM.identifier
    303303    Monad.smax_def__o__monad **)
    304 let identifier_of_label g0 l =
     304let identifier_of_label g l =
    305305  Obj.magic (fun u ->
    306306    let current = u.current_funct in
     
    309309        (Identifiers.empty_map PreIdentifiers.LabelTag)
    310310    in
    311     let { Types.fst = eta28997; Types.snd = lmap0 } =
    312       match Identifiers.lookup0 PreIdentifiers.LabelTag lmap l with
     311    let { Types.fst = eta27825; Types.snd = lmap0 } =
     312      match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
    313313      | Types.None ->
    314314        let { Types.fst = id; Types.snd = univ } =
     
    321321          lmap }
    322322    in
    323     let { Types.fst = id; Types.snd = univ } = eta28997 in
     323    let { Types.fst = id; Types.snd = univ } = eta27825 in
    324324    { Types.fst = { id_univ = univ; current_funct = current; ident_map =
    325325    u.ident_map; label_map =
     
    328328
    329329(** val identifier_of_ident :
    330     AST.ident List.list -> AST.ident -> ASM.identifier0
     330    AST.ident List.list -> AST.ident -> ASM.identifier
    331331    Monad.smax_def__o__monad **)
    332 let identifier_of_ident g0 i =
     332let identifier_of_ident g i =
    333333  Obj.magic (fun u ->
    334334    let imap = u.ident_map in
    335     let { Types.fst = eta28998; Types.snd = imap0 } =
    336       match Identifiers.lookup0 PreIdentifiers.SymbolTag imap i with
     335    let { Types.fst = eta27826; Types.snd = imap0 } =
     336      match Identifiers.lookup PreIdentifiers.SymbolTag imap i with
    337337      | Types.None ->
    338338        let { Types.fst = id; Types.snd = univ } =
     
    345345          imap }
    346346    in
    347     let { Types.fst = id; Types.snd = univ } = eta28998 in
     347    let { Types.fst = id; Types.snd = univ } = eta27826 in
    348348    { Types.fst = { id_univ = univ; current_funct = u.current_funct;
    349349    ident_map = imap0; label_map = u.label_map; address_map =
     
    353353    AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod ->
    354354    Types.unit0 Monad.smax_def__o__monad **)
    355 let start_funct_translation g0 id_f =
     355let start_funct_translation g id_f =
    356356  Obj.magic (fun u -> { Types.fst = { id_univ = u.id_univ; current_funct =
    357357    id_f.Types.fst; ident_map = u.ident_map; label_map = u.label_map;
     
    366366
    367367(** val aSM_fresh :
    368     AST.ident List.list -> ASM.identifier0 Monad.smax_def__o__monad **)
    369 let aSM_fresh g0 =
     368    AST.ident List.list -> ASM.identifier Monad.smax_def__o__monad **)
     369let aSM_fresh g =
    370370  Obj.magic (fun u ->
    371371    let { Types.fst = id; Types.snd = univ } =
     
    577577let vector_cast n m dflt v =
    578578  Util.if_then_else_safe (Nat.leb n m) (fun _ ->
    579     Vector.append0 (Nat.minus m n) n (Vector.replicate (Nat.minus m n) dflt)
    580       v) (fun _ -> (Vector.vsplit (Nat.minus n m) m v).Types.snd)
     579    Vector.append (Nat.minus m n) n (Vector.replicate (Nat.minus m n) dflt) v)
     580    (fun _ -> (Vector.vsplit (Nat.minus n m) m v).Types.snd)
    581581
    582582(** val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode **)
     
    820820           | BackEndOps.DivuModu ->
    821821             ASM.Instruction (ASM.DIV (ASM.ACC_A, ASM.ACC_B)))
    822       | Joint.OP1 (op4, x0, x1) ->
     822      | Joint.OP1 (op1, x0, x1) ->
    823823        Monad.m_return0 (Monad.smax_def State.state_monad)
    824           (match op4 with
     824          (match op1 with
    825825           | BackEndOps.Cmpl -> ASM.Instruction (ASM.CPL ASM.ACC_A)
    826826           | BackEndOps.Inc -> ASM.Instruction (ASM.INC ASM.ACC_A)
    827827           | BackEndOps.Rl -> ASM.Instruction (ASM.RL ASM.ACC_A))
    828       | Joint.OP2 (op4, x0, x1, reg) ->
     828      | Joint.OP2 (op2, x0, x1, reg) ->
    829829        Monad.m_return0 (Monad.smax_def State.state_monad)
    830830          ((match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
     
    836836            | ASM.DIRECT d ->
    837837              (fun _ ->
    838                 match op4 with
     838                match op2 with
    839839                | BackEndOps.Add ->
    840840                  ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DIRECT d)))
     
    857857            | ASM.REGISTER r ->
    858858              (fun _ ->
    859                 match op4 with
     859                match op2 with
    860860                | BackEndOps.Add ->
    861861                  ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.REGISTER r)))
     
    877877            | ASM.ACC_A ->
    878878              (fun _ ->
    879                 match op4 with
     879                match op2 with
    880880                | BackEndOps.Add ->
    881881                  ASM.Instruction (ASM.ADD (ASM.ACC_A, accumulator_address))
     
    891891            | ASM.DATA b ->
    892892              (fun _ ->
    893                 match op4 with
     893                match op2 with
    894894                | BackEndOps.Add ->
    895895                  ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DATA b)))
     
    999999    (start_funct_translation globals id_def) (fun x ->
    10001000    match id_def.Types.snd with
    1001     | AST.Internal int0 ->
    1002       let code = (Types.pi1 int0).Joint.joint_if_code in
     1001    | AST.Internal int ->
     1002      let code = (Types.pi1 int).Joint.joint_if_code in
    10031003      Monad.m_bind0 (Monad.smax_def State.state_monad)
    10041004        (identifier_of_ident globals id_def.Types.fst) (fun id ->
     
    10101010              ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction
    10111011              ASM.RET) }, List.Nil))
    1012           | List.Cons (hd0, tl) ->
    1013             (match hd0.Types.fst with
     1012          | List.Cons (hd, tl) ->
     1013            (match hd.Types.fst with
    10141014             | Types.None ->
    10151015               Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
    1016                  ({ Types.fst = (Types.Some id); Types.snd = hd0.Types.snd },
     1016                 ({ Types.fst = (Types.Some id); Types.snd = hd.Types.snd },
    10171017                 tl))
    10181018             | Types.Some x0 ->
    10191019               Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons
    10201020                 ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction
    1021                  ASM.NOP) }, (List.Cons (hd0, tl)))))))
     1021                 ASM.NOP) }, (List.Cons (hd, tl)))))))
    10221022    | AST.External x0 ->
    10231023      Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil)
    10241024
    1025 (** val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program **)
     1025(** val get_symboltable :
     1026    AST.ident List.list -> (ASM.identifier, AST.ident) Types.prod List.list
     1027    Monad.smax_def__o__monad **)
     1028let get_symboltable globals =
     1029  Obj.magic (fun u ->
     1030    let imap = u.ident_map in
     1031    let f = fun iold inew x -> List.Cons ({ Types.fst = inew; Types.snd =
     1032      iold }, x)
     1033    in
     1034    { Types.fst = u; Types.snd =
     1035    (Identifiers.foldi PreIdentifiers.SymbolTag f imap List.Nil) })
     1036
     1037(** val lin_to_asm :
     1038    LIN.lin_program -> ASM.pseudo_assembly_program Types.option **)
    10261039let lin_to_asm p =
    10271040  State.state_run (new_ASM_universe p)
     
    10471060            (List.map (fun x -> x.Types.fst.Types.fst) p.AST.prog_vars)
    10481061            p.AST.prog_main) (fun main ->
    1049           let code0 = List.Cons ({ Types.fst = Types.None; Types.snd =
    1050             (ASM.Call main) }, (List.Cons ({ Types.fst = (Types.Some
    1051             exit_label); Types.snd = (ASM.Jmp exit_label) }, code)))
    1052           in
    1053           Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst =
    1054             List.Nil; Types.snd = code0 }))))
    1055 
     1062          Monad.m_bind0 (Monad.smax_def State.state_monad)
     1063            (get_symboltable
     1064              (List.map (fun x -> x.Types.fst.Types.fst) p.AST.prog_vars))
     1065            (fun symboltable ->
     1066            Monad.m_return0 (Monad.smax_def State.state_monad)
     1067              (let code0 = List.Cons ({ Types.fst = Types.None; Types.snd =
     1068                 (ASM.Call main) }, (List.Cons ({ Types.fst = (Types.Some
     1069                 exit_label); Types.snd = (ASM.Jmp exit_label) }, code)))
     1070               in
     1071              Monad.m_bind0 (Monad.max_def Option.option)
     1072                (Obj.magic (ASM.code_size_opt code0)) (fun _ ->
     1073                Monad.m_return0 (Monad.max_def Option.option)
     1074                  { ASM.preamble = List.Nil; ASM.code = code0;
     1075                  ASM.renamed_symbols = symboltable; ASM.final_label =
     1076                  exit_label })))))))
     1077
Note: See TracChangeset for help on using the changeset viewer.