Changeset 2176 for src/common/AST.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/common/AST.ma

    r2105 r2176  
    5454
    5555
    56 (* Memory spaces *)
     56(* Memory spaces
     57
     58   For full 8051 memory spaces support we have internal memory pointers,
     59   PData pointers which are 8 bit pointers to the first page of XData, and
     60   a tagged Any pointer for any of the spaces.
     61   
     62   We only support the 16 bit XData and Code pointers for now.  Some commented
     63   out code is still present to suggest how to add the rest, which includes
     64   having pointers and pointer types contain a region field to indicate what
     65   kind of pointer they are (in addition to the region in the block which
     66   indicates where the pointer points to).
     67
     68 *)
    5769
    5870inductive region : Type[0] ≝
    59   | Any : region
     71(*  | Any : region
    6072  | Data : region
    6173  | IData : region
    62   | PData : region
     74  | PData : region*)
    6375  | XData : region
    6476  | Code : region.
     
    6779λr1,r2.
    6880  match r1 with
    69   [ Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
     81  [ (*Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
    7082  | Data ⇒  match r2 with [ Data ⇒ true | _ ⇒ false ]
    7183  | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ]
    7284  | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ]
    73   | XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
     85  |*) XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
    7486  | Code ⇒  match r2 with [ Code ⇒ true | _ ⇒ false ]
    7587  ].
     
    90102#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
    91103
     104(*
    92105(* Carefully defined to be convertably nonzero *)
    93106definition size_pointer : region → nat ≝
    94107λsp. S match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ].
     108*)
     109definition size_pointer : nat ≝ 2.
    95110
    96111(* We maintain some reasonable type information through the front end of the
     
    115130inductive typ : Type[0] ≝
    116131  | ASTint : intsize → signedness → typ
    117   | ASTptr : region → typ
     132  | ASTptr : (*region →*) typ
    118133  | ASTfloat : floatsize → typ.
    119134
     
    124139| SigType_Float: SigType
    125140*)
    126 definition SigType_Ptr ≝ ASTptr Any.
     141definition SigType_Ptr ≝ ASTptr (*Any*).
    127142
    128143(* Define these carefully so that we always know that the result is nonzero,
     
    233248  match ty with
    234249  [ ASTint sz _ ⇒ size_intsize sz
    235   | ASTptr r ⇒ size_pointer r
     250  | ASTptr  ⇒ size_pointer
    236251  | ASTfloat sz ⇒ size_floatsize sz ].
    237252
     
    282297  | Init_float64: float → init_data
    283298  | Init_space: nat → init_data
    284   | Init_null: region → init_data
    285   | Init_addrof: region → ident → nat → init_data.   (*r address of symbol + offset *)
     299  | Init_null: (*region →*) init_data
     300  | Init_addrof: (*region →*) ident → nat → init_data.   (*r address of symbol + offset *)
    286301
    287302(* * Whole programs consist of:
Note: See TracChangeset for help on using the changeset viewer.