Changeset 1053


Ignore:
Timestamp:
Jul 4, 2011, 6:20:23 PM (8 years ago)
Author:
mulligan
Message:

changes

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1052 r1053  
    102102      〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
    103103
    104 definition float_free_p
     104definition size_of_sig_type
    105105  λsig.
    106106  match sig with
    107   [ ASTfloat _ ⇒ False
    108   | _ ⇒ True
    109   ].
    110 
    111 definition size_of_sig_type ≝
    112   λsig.
    113   λprf: float_free_p sig.
    114   match sig return λx. float_free_p x → nat with
    115107  [ ASTint isize sign ⇒
    116     λast_int_prf.
    117       let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
    118         isize' ÷ (nat_of_bitvector ? int_size)
    119   | ASTfloat _ ⇒
    120     λast_float_prf. ?
    121   | ASToffset ⇒
    122     λast_offset_prf.
    123       nat_of_bitvector ? int_size
    124   | ASTptr rgn ⇒
    125     λast_ptr_prf.
    126       nat_of_bitvector ? ptr_size
    127   ].
    128   normalize in ast_float_prf;
    129   cases ast_float_prf;
     108    let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
     109      isize' ÷ (nat_of_bitvector ? int_size)
     110  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
     111  | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
     112  ].
     113  cases not_implemented;
    130114qed.
    131115
     
    158142  λruniverse.
    159143  λlenv.
    160   λr.
    161   λt.
    162   match size_of_sig_type t with
    163   [ None ⇒ None ?
    164   | Some size ⇒
    165     let rs ≝ register_freshes runiverse size in
    166       Some ? (add_local_env r rs lenv)
    167   ].
     144  λr_sig.
     145  let 〈r, sig〉 ≝ r_sig in
     146  let size ≝ size_of_sig_type sig in
     147  let rs ≝ register_freshes runiverse size in
     148    add_local_env r rs lenv.
    168149
    169150definition initialize_local_env ≝
    170151  λruniverse.
    171   λptrs.
    172152  λregisters.
     153  λresult.
    173154  let registers ≝ registers @
    174155    match result with
     
    177158    ]
    178159  in
    179     foldl ? ? (
    180       λbvt. λr.
    181       match bvt with
    182       [ None ⇒ None ?
    183       | Some bvt' ⇒ initialize_local_env_internal runiverse bvt' r typ
    184       ]) ? ?.
    185 
    186 let initialize_local_env runiverse registers result =
    187   let registers =
    188     registers @ (match result with None → [ ] | Some (r, t) → [(r, t)]) in
    189   let f lenv (r, t) =
    190     let rs = register_freshes runiverse (size_of_sig_type t) in
    191     add_local_env r rs lenv in
    192   List.fold_left f Register.Map.empty registers
     160    foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers.
    193161 
    194162definition map_list_local_env_internal ≝
     
    201169  λlenv.
    202170  λregs.
    203  
    204 
    205 let map_list_local_env lenv regs =
    206   let f res r = res @ (find_local_env r lenv) in
    207   List.fold_left f [] regs
    208 
    209 definition filter_and_to_list_local_env_internal ≝
    210   λlenv.
    211   λl.
    212   λr.
    213   match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
    214   [ Some entry ⇒
    215     match entry with
    216     [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
    217     | register_int r ⇒ (l @ [ r ])
    218     ]
    219   | None       ⇒ [ ] (* dpm: should this be none? *)
    220   ].
    221 
    222 definition filter_and_to_list_local_env ≝
    223   λlenv.
    224   λregisters.
    225     foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.
    226 
    227 definition list_of_register_type ≝
    228   λrt.
    229   match rt with
    230   [ register_ptr r1 r2 ⇒ [ r1; r2 ]
    231   | register_int r ⇒ [ r ]
    232   ].
    233 
    234 definition find_and_list ≝
    235   λr.
    236   λlenv.
    237   match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
    238   [ None      ⇒ [ ] (* dpm: should this be none? *)
    239   | Some lkup ⇒ list_of_register_type lkup
    240   ].
    241 
    242 definition find_and_list_args ≝
    243   λargs.
    244   λlenv.
    245     map ? ? (λr. find_and_list r lenv) args.
     171    foldl ? ? (map_list_local_env_internal lenv) [ ] regs.
     172
     173definition make_addr ≝
     174  λA.
     175  λlst: list A.
     176  λprf: length A lst = 2. (* do not use on arguments other than those of length 2 *)
     177  match lst return λx. length A x = 2 → A × A with
     178  [ nil ⇒ λlst_nil_prf. ?
     179  | cons hd tl ⇒ λprf.
     180    match tl return λx. length A x = 1 → A × A with
     181    [ nil ⇒ λtl_nil_prf. ?
     182    | cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉
     183    ] ?
     184  ] prf.
     185  [1: normalize in lst_nil_prf;
     186      destruct(lst_nil_prf);
     187  |2: normalize in prf;
     188      destruct(prf)
     189      @e0
     190  |3: normalize in tl_nil_prf;
     191      destruct(tl_nil_prf);
     192  ]
     193qed.
    246194
    247195definition find_and_addr ≝
    248196  λr.
    249197  λlenv.
    250   match find_and_list r lenv with
    251   [ cons hd tl ⇒
    252     match tl with
    253     [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉
    254     | nil          ⇒ None ?
    255     ]
    256   | nil ⇒ None ? (* dpm: was assert false *)
    257   ].
     198    make_addr ? (find_local_env r lenv).
    258199
    259200definition rtl_args ≝
    260201  λregs_list.
    261202  λlenv.
    262     flatten ? (find_and_list_args regs_list lenv).
     203    flatten ? (map ? ? (
     204      λr. find_local_env r lenv) regs_list).
    263205
    264206definition change_label ≝
     
    284226  | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
    285227  | rtl_st_return r ⇒ rtl_st_return r
    286   | _ ⇒ ?
    287   ].
    288 
     228  ].
     229
     230(* Ack! Should generating a fresh label ever fail?  This seems to be a side-effect
     231   of implementing everything as a bitvector, which is bounded.  If we implemented
     232   labels as unbounded nats then this function will never fail.
     233*)
    289234let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
    290235  match stmt_list with
     
    304249    ]
    305250  ].
    306  
     251
    307252(* dpm: had to lift this into option *)
    308253let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
     
    321266        [ None ⇒ None ?
    322267        | Some def ⇒ add_translates tl tmp_lbl dest_lbl def
    323         ]
    324       ]
    325     ]
    326   ].
    327  
    328 
    329 (* dpm: horrendous, use dependent types.
    330   length destr = length srcrs *)
    331 let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
    332                        (dest_lbl: label) (def: ?) ≝
    333   match destrs with
    334   [ nil ⇒
    335     match srcrs with
    336     [ nil        ⇒ Some ? def
    337     | cons hd tl ⇒ None ?
    338     ]
    339   | cons hd tl ⇒
    340     match srcrs with
    341     [ nil        ⇒ None ?
    342     | cons hd' tl' ⇒
    343       match tl with
    344       [ nil            ⇒
    345         match tl' with
    346         (* one element lists *)
    347         [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
    348         | cons hd'' tl'' ⇒ None ?
    349         ]
    350       | cons hd'' tl'' ⇒
    351         match tl' with
    352         [ nil ⇒ None ?
    353         (* multielement lists *)
    354         | cons hd''' tl''' ⇒
    355           let tmp_lbl ≝ fresh_label def in
    356           match tmp_lbl with
    357           [ None ⇒ None ?
    358           | Some tmp_lbl ⇒
    359             let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
    360               translate_move tl tl' tmp_lbl dest_lbl def
    361           ]
    362268        ]
    363269      ]
     
    411317  | cast_sizeof size ⇒ ?
    412318  (* | cast_float f ⇒ None ? *) (* what are we doing with floats? *)
     319  ].
     320
     321definition filter_and_to_list_local_env_internal ≝
     322  λlenv.
     323  λl.
     324  λr.
     325  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
     326  [ Some entry ⇒
     327    match entry with
     328    [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ])
     329    | register_int r ⇒ (l @ [ r ])
     330    ]
     331  | None       ⇒ [ ] (* dpm: should this be none? *)
     332  ].
     333
     334definition filter_and_to_list_local_env ≝
     335  λlenv.
     336  λregisters.
     337    foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers.
     338
     339definition list_of_register_type ≝
     340  λrt.
     341  match rt with
     342  [ register_ptr r1 r2 ⇒ [ r1; r2 ]
     343  | register_int r ⇒ [ r ]
     344  ].
     345
     346definition find_and_list ≝
     347  λr.
     348  λlenv.
     349  match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with
     350  [ None      ⇒ [ ] (* dpm: should this be none? *)
     351  | Some lkup ⇒ list_of_register_type lkup
     352  ].
     353
     354definition find_and_list_args ≝
     355  λargs.
     356  λlenv.
     357    map ? ? (λr. find_and_list r lenv) args.
     358 
     359(* dpm: horrendous, use dependent types.
     360  length destr = length srcrs *)
     361let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label)
     362                       (dest_lbl: label) (def: ?) ≝
     363  match destrs with
     364  [ nil ⇒
     365    match srcrs with
     366    [ nil        ⇒ Some ? def
     367    | cons hd tl ⇒ None ?
     368    ]
     369  | cons hd tl ⇒
     370    match srcrs with
     371    [ nil        ⇒ None ?
     372    | cons hd' tl' ⇒
     373      match tl with
     374      [ nil            ⇒
     375        match tl' with
     376        (* one element lists *)
     377        [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def)
     378        | cons hd'' tl'' ⇒ None ?
     379        ]
     380      | cons hd'' tl'' ⇒
     381        match tl' with
     382        [ nil ⇒ None ?
     383        (* multielement lists *)
     384        | cons hd''' tl''' ⇒
     385          let tmp_lbl ≝ fresh_label def in
     386          match tmp_lbl with
     387          [ None ⇒ None ?
     388          | Some tmp_lbl ⇒
     389            let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in
     390              translate_move tl tl' tmp_lbl dest_lbl def
     391          ]
     392        ]
     393      ]
     394    ]
    413395  ].
    414396
  • src/common/Identifiers.ma

    r816 r1053  
    3939    ]
    4040  ].
    41    
    4241   
    4342definition word_of_identifier ≝
Note: See TracChangeset for help on using the changeset viewer.