Changeset 1046 for src/common


Ignore:
Timestamp:
Jun 29, 2011, 12:15:09 PM (8 years ago)
Author:
mulligan
Message:

syntax of rtlabs was wrong: cast not const. more added to rtlabs --> rtl pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1045 r1046  
    4242
    4343definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
     44
     45inductive quantity: Type[0] ≝
     46  | q_int: Byte → quantity
     47  | q_offset: quantity
     48  | q_ptr: quantity.
     49 
     50inductive abstract_size: Type[0] ≝
     51  | size_q: quantity → abstract_size
     52  | size_prod: list abstract_size → abstract_size
     53  | size_sum: list abstract_size → abstract_size
     54  | size_array: nat → abstract_size → abstract_size.
     55
     56inductive cast: Type[0] ≝
     57  | cast_int: Byte → cast                     (* integer constant *)
     58(*  | cast_float: float → cast                (* float constant *) *)
     59  | cast_addrsymbol of identifier → cast      (* address of a global symbol *)
     60  | cast_stack: cast                          (* address of the stack *)
     61  | cast_offset: abstract_offset → cast       (* offset *)
     62  | cast_sizeof: abstract_size → cast.        (* size of a type *)
    4463
    4564(* Memory spaces *)
Note: See TracChangeset for help on using the changeset viewer.