Changeset 1050


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.

Location:
src
Files:
2 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 ≝
  • src/utilities/HMap.ma

    r1049 r1050  
    170170  ].
    171171
     172definition map_single_l_safe ≝
     173  λkey_type.
     174  λelt_type.
     175  λkey: key_type.
     176  λelt: elt_type.
     177  λleft: map key_type elt_type.
     178  λright: map key_type elt_type.
     179  λprf: map_not_nil_p key_type elt_type right.
     180  match right return λx. map_not_nil_p key_type elt_type x → map key_type elt_type with
     181  [ map_nil ⇒ λright_nil_absrd. ?
     182  | map_fork r_sz r_key r_elt r_l r_r ⇒
     183    λright_fork_prf. map_binsert ? ? r_key r_elt (map_binsert ? ? key elt left r_l) r_r
     184  ] prf.
     185  normalize in right_nil_absrd;
     186  cases right_nil_absrd
     187qed.
     188
    172189definition map_single_r ≝
    173190  λkey_type.
     
    181198  | map_fork l_sz l_key l_elt l_l l_r ⇒
    182199      Some ? (map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right))
     200  ].
     201
     202definition map_single_r_safe ≝
     203  λkey_type.
     204  λelt_type.
     205  λkey: key_type.
     206  λelt: elt_type.
     207  λleft: map key_type elt_type.
     208  λright: map key_type elt_type.
     209  λprf: map_not_nil_p key_type elt_type left.
     210  match left return λx. map_not_nil_p key_type elt_type x → map key_type elt_type with
     211  [ map_nil ⇒ λleft_nil_absrd. ?
     212  | map_fork l_sz l_key l_elt l_l l_r ⇒
     213      λleft_fork_prf. map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right)
     214  ] prf.
     215  normalize in left_nil_absrd;
     216  cases left_nil_absrd
     217qed.
     218
     219definition map_double_r_property_p ≝
     220  λkey_type.
     221  λelt_type.
     222  λleft: map key_type elt_type.
     223  match left with
     224  [ map_nil ⇒ False
     225  | map_fork l_sz l_key l_elt l_l l_r ⇒
     226    match l_r with
     227    [ map_nil ⇒ False
     228    | _ ⇒ True
     229    ]
    183230  ].
    184231
     
    199246    ]
    200247  ].
     248
     249definition map_double_r_safe ≝
     250  λkey_type.
     251  λelt_type.
     252  λkey: key_type.
     253  λelt: elt_type.
     254  λleft: map key_type elt_type.
     255  λright: map key_type elt_type.
     256  λprf: map_double_r_property_p key_type elt_type left.
     257  match left return λx. map_double_r_property_p key_type elt_type x → map key_type elt_type with
     258  [ map_nil ⇒ λleft_nil_absrd. ?
     259  | map_fork l_sz l_key l_elt l_l l_r ⇒ λouter_prf.
     260    match l_r return λx. map_double_r_property_p key_type elt_type x → map key_type elt_type with
     261    [ map_nil ⇒ λl_r_nil_absrd. ?
     262    | map_fork lr_sz lr_key lr_elt lr_l lr_r ⇒
     263      λl_r_fork_prf. map_binsert … lr_key lr_elt (map_binsert … l_key l_elt l_l lr_l) (map_binsert … key elt lr_r right)
     264    ] ?
     265  ] prf.
     266  [1: normalize in left_nil_absrd;
     267      cases left_nil_absrd;
     268  |3: normalize in l_r_nil_absrd;
     269      cases l_r_nil_absrd;
     270  |2: normalize in outer_prf;
     271      generalize in match outer_prf;
     272      cases l_r;
     273      [ normalize //
     274      | #SZ #KEY_TYPE #ELT_TYPE #LEFT #RIGHT
     275        normalize
     276        #HYP
     277  ]
     278qed.
    201279
    202280definition map_double_l ≝
Note: See TracChangeset for help on using the changeset viewer.