Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (8 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/rTLabsToRTL.ml

    r2743 r2773  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open Graphs
    46
     
    3133open FrontEndOps
    3234
    33 open BitVectorTrie
    34 
    3535open CostLabel
    3636
     
    4949open Extralib
    5050
     51open Lists
     52
     53open Positive
     54
     55open Identifiers
     56
     57open Exp
     58
     59open Arithmetic
     60
     61open Vector
     62
     63open Div_and_mod
     64
     65open Util
     66
     67open FoldStuff
     68
     69open BitVector
     70
     71open Jmeq
     72
     73open Russell
     74
     75open List
     76
    5177open Setoids
    5278
     
    5480
    5581open Option
    56 
    57 open Lists
    58 
    59 open Positive
    60 
    61 open Identifiers
    62 
    63 open Exp
    64 
    65 open Arithmetic
    66 
    67 open Vector
    68 
    69 open Div_and_mod
    70 
    71 open Jmeq
    72 
    73 open Russell
    74 
    75 open List
    76 
    77 open Util
    78 
    79 open FoldStuff
    80 
    81 open BitVector
    8282
    8383open Extranat
     
    152152    -> 'a1) -> register_type -> 'a1 **)
    153153let rec register_type_rect_Type4 h_register_int h_register_ptr = function
    154 | Register_int x_20782 -> h_register_int x_20782
    155 | Register_ptr (x_20784, x_20783) -> h_register_ptr x_20784 x_20783
     154| Register_int x_16092 -> h_register_int x_16092
     155| Register_ptr (x_16094, x_16093) -> h_register_ptr x_16094 x_16093
    156156
    157157(** val register_type_rect_Type5 :
     
    159159    -> 'a1) -> register_type -> 'a1 **)
    160160let rec register_type_rect_Type5 h_register_int h_register_ptr = function
    161 | Register_int x_20788 -> h_register_int x_20788
    162 | Register_ptr (x_20790, x_20789) -> h_register_ptr x_20790 x_20789
     161| Register_int x_16098 -> h_register_int x_16098
     162| Register_ptr (x_16100, x_16099) -> h_register_ptr x_16100 x_16099
    163163
    164164(** val register_type_rect_Type3 :
     
    166166    -> 'a1) -> register_type -> 'a1 **)
    167167let rec register_type_rect_Type3 h_register_int h_register_ptr = function
    168 | Register_int x_20794 -> h_register_int x_20794
    169 | Register_ptr (x_20796, x_20795) -> h_register_ptr x_20796 x_20795
     168| Register_int x_16104 -> h_register_int x_16104
     169| Register_ptr (x_16106, x_16105) -> h_register_ptr x_16106 x_16105
    170170
    171171(** val register_type_rect_Type2 :
     
    173173    -> 'a1) -> register_type -> 'a1 **)
    174174let rec register_type_rect_Type2 h_register_int h_register_ptr = function
    175 | Register_int x_20800 -> h_register_int x_20800
    176 | Register_ptr (x_20802, x_20801) -> h_register_ptr x_20802 x_20801
     175| Register_int x_16110 -> h_register_int x_16110
     176| Register_ptr (x_16112, x_16111) -> h_register_ptr x_16112 x_16111
    177177
    178178(** val register_type_rect_Type1 :
     
    180180    -> 'a1) -> register_type -> 'a1 **)
    181181let rec register_type_rect_Type1 h_register_int h_register_ptr = function
    182 | Register_int x_20806 -> h_register_int x_20806
    183 | Register_ptr (x_20808, x_20807) -> h_register_ptr x_20808 x_20807
     182| Register_int x_16116 -> h_register_int x_16116
     183| Register_ptr (x_16118, x_16117) -> h_register_ptr x_16118 x_16117
    184184
    185185(** val register_type_rect_Type0 :
     
    187187    -> 'a1) -> register_type -> 'a1 **)
    188188let rec register_type_rect_Type0 h_register_int h_register_ptr = function
    189 | Register_int x_20812 -> h_register_int x_20812
    190 | Register_ptr (x_20814, x_20813) -> h_register_ptr x_20814 x_20813
     189| Register_int x_16122 -> h_register_int x_16122
     190| Register_ptr (x_16124, x_16123) -> h_register_ptr x_16124 x_16123
    191191
    192192(** val register_type_inv_rect_Type4 :
     
    239239    PreIdentifiers.identifier -> local_env -> Registers.register List.list **)
    240240let find_local_env r lenv =
    241   Option.opt_safe (Identifiers.lookup0 PreIdentifiers.RegisterTag lenv r)
     241  Option.opt_safe (Identifiers.lookup PreIdentifiers.RegisterTag lenv r)
    242242
    243243(** val find_local_env_arg :
     
    255255    Joint.params -> AST.ident List.list -> Nat.nat -> Registers.register
    256256    List.list Monad.smax_def__o__monad **)
    257 let fresh_registers p g0 n =
     257let fresh_registers p g n =
    258258  let f = fun acc ->
    259259    Monad.m_bind0 (Monad.smax_def State.state_monad)
    260       (TranslateUtils.fresh_register p g0) (fun m ->
     260      (TranslateUtils.fresh_register p g) (fun m ->
    261261      Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons (m, acc)))
    262262  in
     
    271271  (match regs with
    272272   | List.Nil -> (fun _ -> List.Nil)
    273    | List.Cons (hd0, tl) ->
     273   | List.Cons (hd, tl) ->
    274274     (fun _ ->
    275        List.append (find_local_env hd0.Types.fst lenv)
     275       List.append (find_local_env hd.Types.fst lenv)
    276276         (map_list_local_env lenv tl))) __
    277277
     
    279279    AST.ident List.list -> (Registers.register, AST.typ) Types.prod List.list
    280280    -> local_env Monad.smax_def__o__monad **)
    281 let initialize_local_env globals registers0 =
     281let initialize_local_env globals registers =
    282282  let f = fun r_sig lenv ->
    283     let { Types.fst = r; Types.snd = sig1 } = r_sig in
    284     let size = size_of_sig_type sig1 in
     283    let { Types.fst = r; Types.snd = sig0 } = r_sig in
     284    let size = size_of_sig_type sig0 in
    285285    Monad.m_bind0 (Monad.smax_def State.state_monad)
    286286      (fresh_registers (Joint.graph_params_to_params RTL.rTL) globals size)
     
    289289        (Identifiers.add PreIdentifiers.RegisterTag lenv r regs))
    290290  in
    291   Monad.m_fold (Monad.smax_def State.state_monad) f registers0
     291  Monad.m_fold (Monad.smax_def State.state_monad) f registers
    292292    (Identifiers.empty_map PreIdentifiers.RegisterTag)
    293293
     
    297297    (Registers.register, AST.typ) Types.prod Types.option -> local_env
    298298    Monad.smax_def__o__monad **)
    299 let initialize_locals_params_ret globals locals params0 ret =
     299let initialize_locals_params_ret globals locals params ret =
    300300  Obj.magic (fun def ->
    301301    (let { Types.fst = def'; Types.snd = lenv } =
     
    305305            | Types.None -> List.Nil
    306306            | Types.Some r_sig -> List.Cons (r_sig, List.Nil))
    307            (List.append locals params0)) def
     307           (List.append locals params)) def
    308308     in
    309309    (fun _ ->
    310     let params' = map_list_local_env lenv params0 in
     310    let params' = map_list_local_env lenv params in
    311311    let ret' =
    312312      (match ret with
     
    347347  (match args with
    348348   | List.Nil -> (fun _ -> List.Nil)
    349    | List.Cons (hd0, tl) ->
    350      (fun _ -> List.append (find_local_env_arg hd0 env) (rtl_args tl env)))
    351     __
     349   | List.Cons (hd, tl) ->
     350     (fun _ -> List.append (find_local_env_arg hd env) (rtl_args tl env))) __
    352351
    353352(** val vrsplit :
     
    372371  (match l with
    373372   | List.Nil -> (fun _ -> List.Nil)
    374    | List.Cons (hd0, tl) ->
    375      (fun _ -> List.Cons (hd0, (list_inject_All_aux tl)))) __
     373   | List.Cons (hd, tl) ->
     374     (fun _ -> List.Cons (hd, (list_inject_All_aux tl)))) __
    376375
    377376(** val translate_op :
     
    379378    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    380379    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
    381 let translate_op globals op4 destrs srcrs1 srcrs2 =
     380let translate_op globals op destrs srcrs1 srcrs2 =
    382381  let l =
    383382    List.append
    384       (match op4 with
     383      (match op with
    385384       | BackEndOps.Add -> List.Nil
    386385       | BackEndOps.Addc -> List.Cons (Joint.CLEAR_CARRY, List.Nil)
     
    389388       | BackEndOps.Or -> List.Nil
    390389       | BackEndOps.Xor -> List.Nil)
    391       (Util.map3 (fun x x0 x1 -> Joint.OP2 (op4, x, x0, x1))
     390      (Util.map3 (fun x x0 x1 -> Joint.OP2 (op, x, x0, x1))
    392391        (Obj.magic destrs) (Obj.magic srcrs1) (Obj.magic srcrs2))
    393392  in
     
    406405    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    407406    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
    408 let translate_op_asym_unsigned globals op4 destrs srcrs1 srcrs2 =
     407let translate_op_asym_unsigned globals op destrs srcrs1 srcrs2 =
    409408  let l = List.length destrs in
    410409  let srcrs1' =
     
    416415      srcrs2
    417416  in
    418   translate_op globals op4 destrs srcrs1' srcrs2'
     417  translate_op globals op destrs srcrs1' srcrs2'
    419418
    420419(** val nat_to_args :
     
    432431
    433432(** val size_of_cst : AST.typ -> FrontEndOps.constant -> Nat.nat **)
    434 let size_of_cst typ0 = function
     433let size_of_cst typ = function
    435434| FrontEndOps.Ointconst (size, x, x0) -> AST.size_intsize size
    436435| FrontEndOps.Oaddrsymbol (x, x0) -> Nat.S (Nat.S Nat.O)
     
    450449             (Joint.psd_argument_from_byte b) })) destrs
    451450           (Types.pi1 (split_into_bytes size const)))
    452      | FrontEndOps.Oaddrsymbol (id, offset0) ->
     451     | FrontEndOps.Oaddrsymbol (id, offset) ->
    453452       (fun _ _ ->
    454          let { Types.fst = r5; Types.snd = r6 } = make_addr destrs in
    455          List.Cons ((Joint.ADDRESS (id, (Obj.magic r5), (Obj.magic r6))),
     453         let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
     454         List.Cons ((Joint.ADDRESS (id, (Obj.magic r1), (Obj.magic r2))),
    456455         List.Nil))
    457      | FrontEndOps.Oaddrstack offset0 ->
     456     | FrontEndOps.Oaddrstack offset ->
    458457       (fun _ _ ->
    459          let { Types.fst = r5; Types.snd = r6 } = make_addr destrs in
     458         let { Types.fst = r1; Types.snd = r2 } = make_addr destrs in
    460459         List.Cons
    461460         ((let x = Joint.Extension_seq
    462              (Obj.magic (RTL.Rtl_stack_address (r5, r6)))
     461             (Obj.magic (RTL.Rtl_stack_address (r1, r2)))
    463462           in
    464463          x), List.Nil))) __ __
     
    522521    List.list **)
    523522let translate_fill_with_zero globals destrs =
    524   let res1 = nat_to_args (List.length destrs) Nat.O in
    525   translate_move globals destrs res1
     523  let res = nat_to_args (List.length destrs) Nat.O in
     524  translate_move globals destrs res
    526525
    527526(** val last : 'a1 List.list -> 'a1 Types.option **)
    528527let rec last = function
    529528| List.Nil -> Types.None
    530 | List.Cons (hd0, tl) ->
     529| List.Cons (hd, tl) ->
    531530  (match tl with
    532    | List.Nil -> Types.Some hd0
     531   | List.Nil -> Types.Some hd
    533532   | List.Cons (x, x0) -> last tl)
    534533
     
    537536    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    538537    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
    539 let translate_op_asym_signed globals op4 destrs srcrs1 srcrs2 =
     538let translate_op_asym_signed globals op destrs srcrs1 srcrs2 =
    540539  Bind_new.Bnew (fun tmp1 -> Bind_new.Bnew (fun tmp2 ->
    541540    let l = List.length destrs in
     
    562561    BindLists.bappend (let l0 = srcrs1init.Types.snd in Bind_new.Bret l0)
    563562      (BindLists.bappend (let l0 = srcrs2init.Types.snd in Bind_new.Bret l0)
    564         (translate_op globals op4 destrs srcrs1init.Types.fst
     563        (translate_op globals op destrs srcrs1init.Types.fst
    565564          srcrs2init.Types.fst))))
    566565
     
    661660    -> Registers.register List.list -> Registers.register List.list ->
    662661    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
    663 let translate_op1 globals ty ty' op4 destrs srcrs =
    664   (match op4 with
     662let translate_op1 globals ty ty' op1 destrs srcrs =
     663  (match op1 with
    665664   | FrontEndOps.Ocastint (x, src_sign, x0, x1) ->
    666665     (fun _ _ -> translate_cast globals src_sign destrs srcrs)
     
    904903let translate_lt_signed globals destrs srcrs1 srcrs2 =
    905904  Bind_new.Bnew (fun tmp_last_s1 -> Bind_new.Bnew (fun tmp_last_s2 ->
    906     let p3 = shift_signed globals tmp_last_s1 srcrs1 in
    907     let new_srcrs1 = (Types.pi1 p3).Types.fst in
    908     let shift_srcrs1 = (Types.pi1 p3).Types.snd in
    909     let p4 = shift_signed globals tmp_last_s2 srcrs2 in
    910     let new_srcrs2 = (Types.pi1 p4).Types.fst in
    911     let shift_srcrs2 = (Types.pi1 p4).Types.snd in
     905    let p1 = shift_signed globals tmp_last_s1 srcrs1 in
     906    let new_srcrs1 = (Types.pi1 p1).Types.fst in
     907    let shift_srcrs1 = (Types.pi1 p1).Types.snd in
     908    let p2 = shift_signed globals tmp_last_s2 srcrs2 in
     909    let new_srcrs2 = (Types.pi1 p2).Types.fst in
     910    let shift_srcrs2 = (Types.pi1 p2).Types.snd in
    912911    BindLists.bappend (let l = shift_srcrs1 in Bind_new.Bret l)
    913912      (BindLists.bappend (let l = shift_srcrs2 in Bind_new.Bret l)
     
    928927    Joint.psd_argument List.list -> (Registers.register, Joint.joint_seq)
    929928    BindLists.bind_list **)
    930 let translate_cmp is_unsigned globals cmp1 destrs srcrs1 srcrs2 =
    931   match cmp1 with
     929let translate_cmp is_unsigned globals cmp destrs srcrs1 srcrs2 =
     930  match cmp with
    932931  | Integers.Ceq ->
    933932    BindLists.bappend (translate_ne globals destrs srcrs1 srcrs2)
     
    948947    Joint.psd_argument List.list -> Joint.psd_argument List.list ->
    949948    (Registers.register, Joint.joint_seq List.list) Bind_new.bind_new **)
    950 let translate_op2 globals ty1 ty2 ty3 op4 destrs srcrs1 srcrs2 =
    951   (match op4 with
     949let translate_op2 globals ty1 ty2 ty3 op2 destrs srcrs1 srcrs2 =
     950  (match op2 with
    952951   | FrontEndOps.Oadd (sz, sg) ->
    953952     (fun _ _ _ -> translate_op globals BackEndOps.Add destrs srcrs1 srcrs2)
     
    10811080    Joint.params -> AST.ident List.list -> (Registers.register,
    10821081    Joint.joint_seq List.list) Bind_new.bind_new -> Blocks.bind_step_block **)
    1083 let ensure_bind_step_block p g0 b =
     1082let ensure_bind_step_block p g b =
    10841083  Obj.magic
    10851084    (Monad.m_bind0 (Monad.max_def Bind_new.bindNew) (Obj.magic b) (fun l ->
    1086       Obj.magic (Bind_new.Bret (Blocks.ensure_step_block p g0 l))))
     1085      Obj.magic (Bind_new.Bret (Blocks.ensure_step_block p g l))))
    10871086
    10881087(** val translate_statement :
     
    11061105         (translate_cst ty globals cst (find_local_env destr lenv))));
    11071106       Types.dpi2 = (Obj.magic lbl') })
    1108    | RTLabs_syntax.St_op1 (ty, ty', op4, destr, srcr, lbl') ->
     1107   | RTLabs_syntax.St_op1 (ty, ty', op1, destr, srcr, lbl') ->
    11091108     (fun _ -> { Types.dpi1 = (Types.Inl
    11101109       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
    1111          (translate_op1 globals ty' ty op4 (find_local_env destr lenv)
     1110         (translate_op1 globals ty' ty op1 (find_local_env destr lenv)
    11121111           (find_local_env srcr lenv)))); Types.dpi2 = (Obj.magic lbl') })
    1113    | RTLabs_syntax.St_op2 (ty1, ty2, ty3, op4, destr, srcr1, srcr2, lbl') ->
     1112   | RTLabs_syntax.St_op2 (ty1, ty2, ty3, op2, destr, srcr1, srcr2, lbl') ->
    11141113     (fun _ -> { Types.dpi1 = (Types.Inl
    11151114       (ensure_bind_step_block (Joint.graph_params_to_params RTL.rTL) globals
    1116          (translate_op2 globals ty2 ty3 ty1 op4 (find_local_env destr lenv)
     1115         (translate_op2 globals ty2 ty3 ty1 op2 (find_local_env destr lenv)
    11171116           (find_local_env_arg srcr1 lenv) (find_local_env_arg srcr2 lenv))));
    11181117       Types.dpi2 = (Obj.magic lbl') })
     
    11981197      pr.Types.dpi2
    11991198  in
    1200   Identifiers.foldi0 PreIdentifiers.LabelTag f_trans
    1201     def.RTLabs_syntax.f_graph init')) __
     1199  Identifiers.foldi PreIdentifiers.LabelTag f_trans def.RTLabs_syntax.f_graph
     1200    init')) __
    12021201
    12031202(** val rtlabs_to_rtl : RTLabs_syntax.rTLabs_program -> RTL.rtl_program **)
Note: See TracChangeset for help on using the changeset viewer.