Changeset 1052


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

removed offsets after reading cerco mailing list

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1044 r1052  
    111111  | Stub _ ⇒ λ_.None ?
    112112  ]) b.
     113
     114definition member ≝
     115  λA.
     116  λn.
     117  λb: BitVector n.
     118  λt: BitVectorTrie A n.
     119  match lookup_opt A n b t with
     120  [ None ⇒ false
     121  | _    ⇒ true
     122  ].
     123
     124definition member_p ≝
     125  λA.
     126  λn.
     127  λb: BitVector n.
     128  λt: BitVectorTrie A n.
     129  match lookup_opt A n b t with
     130  [ None ⇒ False
     131  | _    ⇒ True
     132  ].
    113133 
    114134lemma forall_lookup:
  • 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 ≝
  • src/common/AST.ma

    r1047 r1052  
    121121  | ASTint : intsize → signedness → typ
    122122  | ASTptr : region → typ
    123   | ASToffset: typ
    124123  | ASTfloat : floatsize → typ.
    125124
     
    201200  [ ASTint sz _ ⇒ size_intsize sz
    202201  | ASTptr r ⇒ size_pointer r
    203   | ASToffset ⇒ 1 (* dpm: what!? need this for typesize pos --- not sure what correct size of an offset should be? *)
    204202  | ASTfloat sz ⇒ size_floatsize sz ].
    205203
  • src/utilities/HMap.ma

    r1050 r1052  
    230230  ].
    231231
     232lemma map_double_r_property_p_exists:
     233  ∀key_type.
     234  ∀elt_type.
     235  ∀left: map key_type elt_type.
     236    map_double_r_property_p key_type elt_type left →
     237      ∃l_sz, l_key, l_elt, l_l, l_r.
     238        left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r.
     239  #KEY_TYPE #ELT_TYPE #LEFT
     240  cases LEFT
     241  [ normalize #HYP cases HYP
     242  | #L_SZ #L_KEY #L_ELT #L_LEFT #L_RIGHT
     243    #HYP
     244    @ex_intro
     245    [1: @L_SZ
     246    |2: @ex_intro
     247        [1: @L_KEY
     248        |2: @ex_intro
     249            [1: @L_ELT
     250            |2: @ex_intro
     251                [1: @L_LEFT
     252                |2: @ex_intro
     253                    [1: @L_RIGHT
     254                    |2: %
     255                    ]
     256                ]
     257            ]
     258        ]
     259    ]
     260  ]
     261qed.
     262
     263lemma map_double_r_property_p_exists_l_r_not_nil_p:
     264  ∀key_type.
     265  ∀elt_type.
     266  ∀left: map key_type elt_type.
     267    map_double_r_property_p key_type elt_type left →
     268      ∃l_sz, l_key, l_elt, l_l, l_r.
     269        (left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r) ∧
     270        map_not_nil_p key_type elt_type l_r.
     271  #KEY_TYPE #ELT_TYPE #LEFT
     272  cases LEFT
     273  [ normalize #HYP cases HYP
     274  | #L_SZ #L_KEY #L_ELT #L_LEFT #L_RIGHT
     275    #HYP
     276    @ex_intro
     277    [1: @L_SZ
     278    |2: @ex_intro
     279        [1: @L_KEY
     280        |2: @ex_intro
     281            [1: @L_ELT
     282            |2: @ex_intro
     283                [1: @L_LEFT
     284                |2: @ex_intro
     285                    [1: @L_RIGHT
     286                    |2: @conj
     287                        [1: %
     288                        |2: generalize in match HYP
     289                            cases L_RIGHT
     290                            [1: normalize //
     291                            |2: #NEW_SZ #NEW_KEY #NEW_ELT #NEW_L #NEW_R
     292                                normalize //
     293                            ]
     294                        ]
     295                    ]
     296                ]
     297            ]
     298        ]
     299    ]
     300  ]
     301qed.
     302
    232303definition map_double_r ≝
    233304  λkey_type.
     
    246317    ]
    247318  ].
    248 
    249 definition 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   ]
    278 qed.
    279319
    280320definition map_double_l ≝
Note: See TracChangeset for help on using the changeset viewer.