Changeset 2176 for src/Clight/Csyntax.ma


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/Clight/Csyntax.ma

    r1920 r2176  
    6565  | Tint: intsize → signedness → type   (**r integer types *)
    6666  | Tfloat: floatsize → type            (**r floating-point types *)
    67   | Tpointer: region → type → type      (**r pointer types ([*ty]) *)
    68   | Tarray: region → type → nat → type  (**r array types ([ty[len]]) *)
     67  | Tpointer: (*region →*) type → type      (**r pointer types ([*ty]) *)
     68  | Tarray: (*region →*) type → nat → type  (**r array types ([ty[len]]) *)
    6969  | Tfunction: typelist → type → type   (**r function types *)
    7070  | Tstruct: ident → fieldlist → type   (**r struct types *)
    7171  | Tunion: ident → fieldlist → type    (**r union types *)
    72   | Tcomp_ptr: region → ident → type    (**r pointer to named struct or union *)
     72  | Tcomp_ptr: (*region →*) ident → type    (**r pointer to named struct or union *)
    7373
    7474with typelist : Type[0] ≝
     
    8686  (it:∀i,s. P (Tint i s))
    8787  (fl:∀f. P (Tfloat f))
    88   (pt:∀s,t. P t → P (Tpointer s t))
    89   (ar:∀s,t,n. P t → P (Tarray s t n))
     88  (pt:∀t. P t → P (Tpointer t))
     89  (ar:∀t,n. P t → P (Tarray t n))
    9090  (fn:∀tl,t. P t → P (Tfunction tl t))
    9191  (st:∀i,fl. P (Tstruct i fl))
    9292  (un:∀i,fl. P (Tunion i fl))
    93   (cp:∀rg,i. P (Tcomp_ptr rg i))
     93  (cp:∀i. P (Tcomp_ptr i))
    9494  (t:type) on t : P t ≝
    9595  match t return λt'.P t' with
     
    9797  | Tint i s ⇒ it i s
    9898  | Tfloat s ⇒ fl s
    99   | Tpointer s t' ⇒ pt s t' (type_ind P vo it fl pt ar fn st un cp t')
    100   | Tarray s t' n ⇒ ar s t' n (type_ind P vo it fl pt ar fn st un cp t')
     99  | Tpointer t' ⇒ pt t' (type_ind P vo it fl pt ar fn st un cp t')
     100  | Tarray t' n ⇒ ar t' n (type_ind P vo it fl pt ar fn st un cp t')
    101101  | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it fl pt ar fn st un cp t')
    102102  | Tstruct i fs ⇒ st i fs
    103103  | Tunion i fs ⇒ un i fs
    104   | Tcomp_ptr rg i ⇒ cp rg i
     104  | Tcomp_ptr i ⇒ cp i
    105105  ].
    106106 
     
    350350
    351351(* * Natural alignment of a type, in bytes. *)
    352 (* FIXME: these are old values for 32 bit machines *)
    353 let rec alignof (t: type) : nat ≝
     352let rec alignof (t: type) : nat ≝ (*1*)
     353(* these are old values for 32 bit machines *)
    354354  match t with
    355355  [ Tvoid ⇒ 1
    356356  | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    357357  | Tfloat sz ⇒ match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    358   | Tpointer _ _ ⇒ 4
    359   | Tarray _ t' n ⇒ alignof t'
     358  | Tpointer _ ⇒ 4
     359  | Tarray t' n ⇒ alignof t'
    360360  | Tfunction _ _ ⇒ 1
    361361  | Tstruct _ fld ⇒ alignof_fields fld
    362362  | Tunion _ fld ⇒ alignof_fields fld
    363   | Tcomp_ptr _ _ ⇒ 4
     363  | Tcomp_ptr _ ⇒ 4
    364364  ]
    365365
     
    381381  (it:∀i,s. P (Tint i s))
    382382  (fl:∀f. P (Tfloat f))
    383   (pt:∀s,t. P t → P (Tpointer s t))
    384   (ar:∀s,t,n. P t → P (Tarray s t n))
     383  (pt:∀t. P t → P (Tpointer t))
     384  (ar:∀t,n. P t → P (Tarray t n))
    385385  (fn:∀tl,t. P t → P (Tfunction tl t))
    386386  (st:∀i,fl. Q fl → P (Tstruct i fl))
    387387  (un:∀i,fl. Q fl → P (Tunion i fl))
    388   (cp:∀r,i. P (Tcomp_ptr r i))
     388  (cp:∀i. P (Tcomp_ptr i))
    389389  (nl:Q Fnil)
    390390  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
     
    394394  | Tint i s ⇒ it i s
    395395  | Tfloat s ⇒ fl s
    396   | Tpointer s t' ⇒ pt s t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    397   | Tarray s t' n ⇒ ar s t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
     396  | Tpointer t' ⇒ pt t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
     397  | Tarray t' n ⇒ ar t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    398398  | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    399399  | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
    400400  | Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
    401   | Tcomp_ptr r i ⇒ cp r i
     401  | Tcomp_ptr i ⇒ cp i
    402402  ]
    403403and fieldlist_ind2
     
    406406  (it:∀i,s. P (Tint i s))
    407407  (fl:∀f. P (Tfloat f))
    408   (pt:∀s,t. P t → P (Tpointer s t))
    409   (ar:∀s,t,n. P t → P (Tarray s t n))
     408  (pt:∀t. P t → P (Tpointer t))
     409  (ar:∀t,n. P t → P (Tarray t n))
    410410  (fn:∀tl,t. P t → P (Tfunction tl t))
    411411  (st:∀i,fl. Q fl → P (Tstruct i fl))
    412412  (un:∀i,fl. Q fl → P (Tunion i fl))
    413   (cp:∀r,i. P (Tcomp_ptr r i))
     413  (cp:∀i. P (Tcomp_ptr i))
    414414  (nl:Q Fnil)
    415415  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
     
    440440  | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    441441  | Tfloat f ⇒ match f with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    442   | Tpointer r _ ⇒ size_pointer r
    443   | Tarray _ t' n ⇒ sizeof t' * max 1 n
     442  | Tpointer _ ⇒ size_pointer
     443  | Tarray t' n ⇒ sizeof t' * max 1 n
    444444  | Tfunction _ _ ⇒ 1
    445445  | Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t)
    446446  | Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t)
    447   | Tcomp_ptr r _ ⇒ size_pointer r
     447  | Tcomp_ptr _ ⇒ size_pointer
    448448  ]
    449449
     
    611611  | Tint sz sg ⇒ ASTint sz sg
    612612  | Tfloat sz ⇒ ASTfloat sz
    613   | Tpointer r _ ⇒ ASTptr r
    614   | Tarray r _ _ ⇒ ASTptr r
    615   | Tfunction _ _ ⇒ ASTptr Code
    616   | Tcomp_ptr r _ ⇒ ASTptr r
     613  | Tpointer _ ⇒ ASTptr
     614  | Tarray _ _ ⇒ ASTptr
     615  | Tfunction _ _ ⇒ ASTptr
     616  | Tcomp_ptr _ ⇒ ASTptr
    617617  | _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *)
    618618  ].
     
    623623  | Tint sz sg ⇒ Some ? (ASTint sz sg)
    624624  | Tfloat sz ⇒ Some ? (ASTfloat sz)
    625   | Tpointer r _ ⇒ Some ? (ASTptr r)
    626   | Tarray r _ _ ⇒ Some ? (ASTptr r)
    627   | Tfunction _ _ ⇒ Some ? (ASTptr Code)
    628   | Tcomp_ptr r _ ⇒ Some ? (ASTptr r)
     625  | Tpointer _ ⇒ Some ? ASTptr
     626  | Tarray _ _ ⇒ Some ? ASTptr
     627  | Tfunction _ _ ⇒ Some ? ASTptr
     628  | Tcomp_ptr _ ⇒ Some ? ASTptr
    629629  | _ ⇒ None ? (* structs and unions shouldn't be converted? *)
    630630  ].
     
    651651inductive mode: typ → Type[0] ≝
    652652  | By_value: ∀t:typ. mode t
    653   | By_reference: ∀r:region. mode (ASTptr r)
     653  | By_reference: (*∀r:region.*) mode ASTptr
    654654  | By_nothing: ∀t. mode t.
    655655
     
    659659  | Tfloat sz ⇒ By_value (ASTfloat sz)
    660660  | Tvoid ⇒ By_nothing …
    661   | Tpointer r _ ⇒ By_value (ASTptr r)
    662   | Tarray r _ _ ⇒ By_reference r
    663   | Tfunction _ _ ⇒ By_reference Code
     661  | Tpointer _ ⇒ By_value ASTptr
     662  | Tarray _ _ ⇒ By_reference
     663  | Tfunction _ _ ⇒ By_reference
    664664  | Tstruct _ fList ⇒ By_nothing …
    665665  | Tunion _ fList ⇒ By_nothing …
    666   | Tcomp_ptr r _ ⇒ By_value (ASTptr r)
     666  | Tcomp_ptr _ ⇒ By_value ASTptr
    667667  ].
    668668
Note: See TracChangeset for help on using the changeset viewer.