Changeset 2176 for src/Clight/Csyntax.ma

Timestamp:

Jul 12, 2012, 1:28:28 PM (9 years ago)

Author:

campbell

Message:

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

File:

• src/Clight/Csyntax.ma (modified) (12 diffs)

src/Clight/Csyntax.ma

@@ -65 +65 @@
   | Tint: intsize → signedness → type   (**r integer types *)
   | Tfloat: floatsize → type            (**r floating-point types *)
-  | Tpointer: region → type → type      (**r pointer types ([*ty]) *)
-  | Tarray: region → type → nat → type  (**r array types ([ty[len]]) *)
+  | Tpointer: (*region →*) type → type      (**r pointer types ([*ty]) *)
+  | Tarray: (*region →*) type → nat → type  (**r array types ([ty[len]]) *)
   | Tfunction: typelist → type → type   (**r function types *)
   | Tstruct: ident → fieldlist → type   (**r struct types *)
   | Tunion: ident → fieldlist → type    (**r union types *)
-  | Tcomp_ptr: region → ident → type    (**r pointer to named struct or union *)
+  | Tcomp_ptr: (*region →*) ident → type    (**r pointer to named struct or union *)
 
 with typelist : Type[0] ≝
@@ -86 +86 @@
   (it:∀i,s. P (Tint i s))
   (fl:∀f. P (Tfloat f))
-  (pt:∀s,t. P t → P (Tpointer s t))
-  (ar:∀s,t,n. P t → P (Tarray s t n))
+  (pt:∀t. P t → P (Tpointer t))
+  (ar:∀t,n. P t → P (Tarray t n))
   (fn:∀tl,t. P t → P (Tfunction tl t))
   (st:∀i,fl. P (Tstruct i fl))
   (un:∀i,fl. P (Tunion i fl))
-  (cp:∀rg,i. P (Tcomp_ptr rg i))
+  (cp:∀i. P (Tcomp_ptr i))
   (t:type) on t : P t ≝
   match t return λt'.P t' with
@@ -97 +97 @@
   | Tint i s ⇒ it i s
   | Tfloat s ⇒ fl s
-  | Tpointer s t' ⇒ pt s t' (type_ind P vo it fl pt ar fn st un cp t')
-  | Tarray s t' n ⇒ ar s t' n (type_ind P vo it fl pt ar fn st un cp t')
+  | Tpointer t' ⇒ pt t' (type_ind P vo it fl pt ar fn st un cp t')
+  | Tarray t' n ⇒ ar t' n (type_ind P vo it fl pt ar fn st un cp t')
   | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it fl pt ar fn st un cp t')
   | Tstruct i fs ⇒ st i fs
   | Tunion i fs ⇒ un i fs
-  | Tcomp_ptr rg i ⇒ cp rg i
+  | Tcomp_ptr i ⇒ cp i
   ].
   
@@ -350 +350 @@
 
 (* * Natural alignment of a type, in bytes. *)
-(* FIXME: these are old values for 32 bit machines *)
-let rec alignof (t: type) : nat ≝
+let rec alignof (t: type) : nat ≝ (*1*) 
+(* these are old values for 32 bit machines *)
   match t with
   [ Tvoid ⇒ 1
   | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
   | Tfloat sz ⇒ match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ]
-  | Tpointer _ _ ⇒ 4
-  | Tarray _ t' n ⇒ alignof t'
+  | Tpointer _ ⇒ 4
+  | Tarray t' n ⇒ alignof t'
   | Tfunction _ _ ⇒ 1
   | Tstruct _ fld ⇒ alignof_fields fld
   | Tunion _ fld ⇒ alignof_fields fld
-  | Tcomp_ptr _ _ ⇒ 4
+  | Tcomp_ptr _ ⇒ 4
   ]
 
@@ -381 +381 @@
   (it:∀i,s. P (Tint i s))
   (fl:∀f. P (Tfloat f))
-  (pt:∀s,t. P t → P (Tpointer s t))
-  (ar:∀s,t,n. P t → P (Tarray s t n))
+  (pt:∀t. P t → P (Tpointer t))
+  (ar:∀t,n. P t → P (Tarray t n))
   (fn:∀tl,t. P t → P (Tfunction tl t))
   (st:∀i,fl. Q fl → P (Tstruct i fl))
   (un:∀i,fl. Q fl → P (Tunion i fl))
-  (cp:∀r,i. P (Tcomp_ptr r i))
+  (cp:∀i. P (Tcomp_ptr i))
   (nl:Q Fnil)
   (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
@@ -394 +394 @@
   | Tint i s ⇒ it i s
   | Tfloat s ⇒ fl s
-  | Tpointer s t' ⇒ pt s t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
-  | Tarray s t' n ⇒ ar s t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
+  | Tpointer t' ⇒ pt t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
+  | Tarray t' n ⇒ ar t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
   | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
   | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
   | Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
-  | Tcomp_ptr r i ⇒ cp r i
+  | Tcomp_ptr i ⇒ cp i
   ]
 and fieldlist_ind2
@@ -406 +406 @@
   (it:∀i,s. P (Tint i s))
   (fl:∀f. P (Tfloat f))
-  (pt:∀s,t. P t → P (Tpointer s t))
-  (ar:∀s,t,n. P t → P (Tarray s t n))
+  (pt:∀t. P t → P (Tpointer t))
+  (ar:∀t,n. P t → P (Tarray t n))
   (fn:∀tl,t. P t → P (Tfunction tl t))
   (st:∀i,fl. Q fl → P (Tstruct i fl))
   (un:∀i,fl. Q fl → P (Tunion i fl))
-  (cp:∀r,i. P (Tcomp_ptr r i))
+  (cp:∀i. P (Tcomp_ptr i))
   (nl:Q Fnil)
   (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
@@ -440 +440 @@
   | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
   | Tfloat f ⇒ match f with [ F32 ⇒ 4 | F64 ⇒ 8 ]
-  | Tpointer r _ ⇒ size_pointer r
-  | Tarray _ t' n ⇒ sizeof t' * max 1 n
+  | Tpointer _ ⇒ size_pointer 
+  | Tarray t' n ⇒ sizeof t' * max 1 n
   | Tfunction _ _ ⇒ 1
   | Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t)
   | Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t)
-  | Tcomp_ptr r _ ⇒ size_pointer r
+  | Tcomp_ptr _ ⇒ size_pointer 
   ]
 
@@ -611 +611 @@
   | Tint sz sg ⇒ ASTint sz sg
   | Tfloat sz ⇒ ASTfloat sz
-  | Tpointer r _ ⇒ ASTptr r
-  | Tarray r _ _ ⇒ ASTptr r
-  | Tfunction _ _ ⇒ ASTptr Code
-  | Tcomp_ptr r _ ⇒ ASTptr r
+  | Tpointer _ ⇒ ASTptr
+  | Tarray _ _ ⇒ ASTptr
+  | Tfunction _ _ ⇒ ASTptr
+  | Tcomp_ptr _ ⇒ ASTptr
   | _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *)
   ].
@@ -623 +623 @@
   | Tint sz sg ⇒ Some ? (ASTint sz sg)
   | Tfloat sz ⇒ Some ? (ASTfloat sz)
-  | Tpointer r _ ⇒ Some ? (ASTptr r)
-  | Tarray r _ _ ⇒ Some ? (ASTptr r)
-  | Tfunction _ _ ⇒ Some ? (ASTptr Code)
-  | Tcomp_ptr r _ ⇒ Some ? (ASTptr r)
+  | Tpointer _ ⇒ Some ? ASTptr
+  | Tarray _ _ ⇒ Some ? ASTptr
+  | Tfunction _ _ ⇒ Some ? ASTptr
+  | Tcomp_ptr _ ⇒ Some ? ASTptr
   | _ ⇒ None ? (* structs and unions shouldn't be converted? *)
   ].
@@ -651 +651 @@
 inductive mode: typ → Type[0] ≝
   | By_value: ∀t:typ. mode t
-  | By_reference: ∀r:region. mode (ASTptr r)
+  | By_reference: (*∀r:region.*) mode ASTptr
   | By_nothing: ∀t. mode t.
 
@@ -659 +659 @@
   | Tfloat sz ⇒ By_value (ASTfloat sz)
   | Tvoid ⇒ By_nothing …
-  | Tpointer r _ ⇒ By_value (ASTptr r)
-  | Tarray r _ _ ⇒ By_reference r
-  | Tfunction _ _ ⇒ By_reference Code
+  | Tpointer _ ⇒ By_value ASTptr
+  | Tarray _ _ ⇒ By_reference
+  | Tfunction _ _ ⇒ By_reference
   | Tstruct _ fList ⇒ By_nothing …
   | Tunion _ fList ⇒ By_nothing …
-  | Tcomp_ptr r _ ⇒ By_value (ASTptr r)
+  | Tcomp_ptr _ ⇒ By_value ASTptr
   ].