Changeset 1050 for src/RTLabs


Ignore:
Timestamp:
Jul 4, 2011, 10:43:37 AM (8 years ago)
Author:
mulligan
Message:

adding dependent types to map datastructure to remove all option types. some changes to rtlabs to rtl translation pass.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1049 r1050  
    123123
    124124definition initialize_local_env_internal ≝
    125   λeq.
    126125  λruniverse.
    127   λptrs.
    128126  λlenv.
    129127  λr.
    130     let fresh ≝ snd ? ? (fresh_reg runiverse) in
    131     let rt ≝
    132       match member ? eq r ptrs with
    133       [ true  ⇒ register_ptr r fresh
    134       | false ⇒ register_int r
    135       ]
    136     in
    137     add_local_env ? ? 〈r, rt〉 lenv.
     128  λt.
     129  match size_of_sig_type t with
     130  [ None ⇒ None ?
     131  | Some size ⇒
     132    let rs ≝ register_freshes runiverse size in
     133      add_local_env r rs lenv
     134  ].
    138135
    139136definition initialize_local_env ≝
     
    141138  λptrs.
    142139  λregisters.
    143     foldl ? ? (initialize_local_env_internal (eq_identifier RegisterTag) runiverse ptrs) [ ] registers.
     140  let registers ≝ registers @
     141    match result with
     142    [ None ⇒ [ ]
     143    | Some rt ⇒ [ rt ]
     144    ]
     145  in
     146    foldl ? ? (initialize_local_env_internal runiverse) [ ] registers.
     147
     148
     149let initialize_local_env runiverse registers result =
     150  let registers =
     151    registers @ (match result with None -> [] | Some (r, t) -> [(r, t)]) in
     152  let f lenv (r, t) =
     153    let rs = register_freshes runiverse (size_of_sig_type t) in
     154    add_local_env r rs lenv in
     155  List.fold_left f Register.Map.empty registers
     156 
     157 
     158definition map_list_local_env_internal ≝
     159  λlenv.
     160  λres.
     161  λr.
     162    res @ (find_local_env r lenv).
     163   
     164definition map_list_local_env ≝
     165  λlenv.
     166  λregs.
     167 
     168
     169let map_list_local_env lenv regs =
     170  let f res r = res @ (find_local_env r lenv) in
     171  List.fold_left f [] regs
    144172
    145173definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.