Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2117 r2176  
    8282     addresses of the memory region in question - here there are no real
    8383     pointers, so use the real region. *)
    84   let ptr ≝ mk_pointer (block_region m b) b ? (mk_offset p) in
     84  let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset p) in
    8585  match id with
    8686  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
     
    8989  | Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n)
    9090  | Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n)
    91   | Init_addrof r' symb ofs ⇒
     91  | Init_addrof (*r'*) symb ofs ⇒
    9292      match find_symbol … ge symb with
    9393      [ None ⇒ None ?
    94       | Some b' ⇒
     94      | Some b' ⇒ (*
    9595        match pointer_compat_dec b' r' with
    96         [ inl pc ⇒ store (ASTptr r') m ptr (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
    97         | inr _ ⇒ None ?
    98         ]
     96        [ inl pc ⇒*) store (ASTptr (*r'*)) m ptr (Vptr (mk_pointer (*r'*) b' (*pc*) (shift_offset ? zero_offset (repr I16 ofs))))
     97        (*| inr _ ⇒ None ?
     98        ]*)
    9999      ]
    100100  | Init_space n ⇒ Some ? m
    101   | Init_null r' ⇒ store (ASTptr r') m ptr (Vnull r')
     101  | Init_null (*r'*) ⇒ store (ASTptr (*r'*)) m ptr (Vnull (*r'*))
    102102  ].
    103 cases b //
    104 qed.
     103(*cases b //
     104qed.*)
    105105
    106106definition size_init_data : init_data → nat ≝
     
    112112  | Init_float64 _ ⇒ 8
    113113  | Init_space n ⇒ max n 0
    114   | Init_null r ⇒ size_pointer r
    115   | Init_addrof r _ _ ⇒ size_pointer r].
     114  | Init_null (*r*) ⇒ size_pointer (*r*)
     115  | Init_addrof (*r*) _ _ ⇒ size_pointer (*r*)].
    116116
    117117let rec store_init_data_list (F:Type[0]) (ge:genv_t F)
     
    230230lemma find_funct_find_funct_ptr : ∀F,ge,v,f.
    231231  find_funct F ge v = Some F f →
    232   ∃pty,b,c. v = Vptr (mk_pointer pty b c zero_offset)  ∧ find_funct_ptr F ge b = Some F f.
     232  ∃(*pty,*)b(*,c*). v = Vptr (mk_pointer (*pty*) b (*c*) zero_offset)  ∧ find_funct_ptr F ge b = Some F f.
    233233#F #ge *
    234234[ #f #E normalize in E; destruct
    235235| #sz #i #f #E normalize in E; destruct
    236236| #f #fn #E normalize in E; destruct
    237 | #r #f #E normalize in E; destruct
    238 | * #pty #b #c * #off #f #E whd in E:(??%?);
     237| (*#r*) #f #E normalize in E; destruct
     238| * (*#pty*) #b (*#c*) * #off #f #E whd in E:(??%?);
    239239  cases off in E ⊢ %; [ 2,3: #x ]
    240240  #E whd in E:(??%?); destruct
    241   %{pty} %{b} %{c} % // @E
     241  (*%{pty}*) %{b} (*%{c}*) % // @E
    242242] qed.
    243243
     
    510510  ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'.
    511511#A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P
    512 cases b * * [ 2,3,5,6,8,9,11,12,14,15,17,18: #bp ]
    513 [ 12: | *: #F whd in F:(??%?); destruct ]
     512cases b * * [ 2,3,5,6(*,8,9,11,12,14,15,17,18*): #bp ]
     513[ 4: (*12:*) | *: #F whd in F:(??%?); destruct ]
    514514>vars_irrelevant_to_find_funct_ptr
    515515>vars_irrelevant_to_find_funct_ptr
     
    656656#A #B #V #iV #tf #p #v #f #FF
    657657cases (find_funct_find_funct_ptr ???? FF)
    658 #r * #b * #pc * #E destruct #FFP
     658#b * #E destruct #FFP
    659659change with (find_funct_ptr ???) in ⊢ (??%?);
    660660@(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *)
     
    676676#A #B #ge #ge' #m #b #o #d #SYM
    677677whd in ⊢ (??%%);
    678 cases d #d' try @refl
    679 #id #n whd in ⊢ (??%%);
     678cases d try #d' try @refl
     679#n whd in ⊢ (??%%);
    680680whd in match (find_symbol A ??); whd in match (find_symbol B ??); >SYM @refl
    681681qed.
Note: See TracChangeset for help on using the changeset viewer.