Changeset 1052 for src/RTLabs


Ignore:
Timestamp:
Jul 4, 2011, 3:31:18 PM (8 years ago)
Author:
mulligan
Message:

removed offsets after reading cerco mailing list

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1050 r1052  
    102102      〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
    103103
     104definition float_free_p ≝
     105  λsig.
     106  match sig with
     107  [ ASTfloat _ ⇒ False
     108  | _ ⇒ True
     109  ].
     110
    104111definition size_of_sig_type ≝
    105112  λsig.
    106   match sig with
     113  λprf: float_free_p sig.
     114  match sig return λx. float_free_p x → nat with
    107115  [ ASTint isize sign ⇒
    108     let isize' ≝ match isize with [ I8 ⇒ 8 | I16 ⇒ 16 | I32 ⇒ 32 ] in
    109       Some ? (isize' ÷ (nat_of_bitvector ? int_size))
    110   | ASTfloat _ ⇒ None ?
    111   | ASToffset ⇒ Some ? (nat_of_bitvector ? int_size)
    112   | ASTptr rgn ⇒ Some ? (nat_of_bitvector ? ptr_size)
    113   ].
     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;
     130qed.
    114131
    115132inductive register_type: Type[0] ≝
     
    117134  | register_ptr: register → register → register_type.
    118135
    119 definition local_env ≝ map register (list register).
    120 definition mem_local_env ≝ map_member register (list register) register_ord.
    121 definition add_local_env ≝ map_insert register (list register) register_ord.
    122 definition find_local_env ≝ map_lookup register (list register) register_ord.
     136definition local_env ≝ BitVectorTrie (list register).
     137
     138definition mem_local_env ≝
     139  λr: register.
     140  match r with
     141  [ an_identifier w ⇒ member (list register) 16 w
     142  ].
     143
     144definition add_local_env ≝
     145  λr: register.
     146  match r with
     147  [ an_identifier w ⇒ insert (list register) 16 w
     148  ].
     149
     150definition find_local_env ≝
     151  λr: register.
     152  λbvt.
     153  match r with
     154  [ an_identifier w ⇒ lookup (list register) 16 w bvt [ ]
     155  ].
    123156
    124157definition initialize_local_env_internal ≝
     
    131164  | Some size ⇒
    132165    let rs ≝ register_freshes runiverse size in
    133       add_local_env r rs lenv
     166      Some ? (add_local_env r rs lenv)
    134167  ].
    135168
     
    144177    ]
    145178  in
    146     foldl ? ? (initialize_local_env_internal runiverse) [ ] registers.
    147 
     179    foldl ? ? (
     180      λbvt. λr.
     181      match bvt with
     182      [ None ⇒ None ?
     183      | Some bvt' ⇒ initialize_local_env_internal runiverse bvt' r typ
     184      ]) ? ?.
    148185
    149186let initialize_local_env runiverse registers result =
    150187  let registers =
    151     registers @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
     188    registers @ (match result with None → [ ] | Some (r, t) → [(r, t)]) in
    152189  let f lenv (r, t) =
    153190    let rs = register_freshes runiverse (size_of_sig_type t) in
    154191    add_local_env r rs lenv in
    155192  List.fold_left f Register.Map.empty registers
    156  
    157193 
    158194definition map_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.