Changeset 880 for src/Cminor/syntax.ma


Ignore:
Timestamp:
Jun 3, 2011, 5:35:31 PM (8 years ago)
Author:
campbell
Message:

Add type information into Cminor.
As a result, the Clight to Cminor stage now does extra type checking.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r878 r880  
    33include "common/CostLabel.ma".
    44
    5 inductive expr : Type[0] ≝
    6 | Id : ident → expr
    7 | Cst : constant → expr
    8 | Op1 : unary_operation → expr → expr
    9 | Op2 : binary_operation → expr → expr → expr
    10 | Mem : memory_chunk → expr → expr
    11 | Cond : expr → expr → expr → expr
    12 | Ecost : costlabel → expr → expr.
     5(* TODO: consider making the typing stricter. *)
     6
     7inductive expr : typ → Type[0] ≝
     8| Id : ∀t. ident → expr t
     9| Cst : ∀t. constant → expr t
     10| Op1 : ∀t,t'. unary_operation → expr t → expr t'
     11| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
     12| Mem : ∀t. memory_chunk → expr (ASTptr Any) → expr t
     13| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
     14| Ecost : ∀t. costlabel → expr t → expr t.
    1315
    1416inductive stmt : Type[0] ≝
    1517| St_skip : stmt
    16 | St_assign : ident → expr → stmt
    17 | St_store : memory_chunk → expr → expr → stmt
     18| St_assign : ∀t. ident → expr t → stmt
     19| St_store : ∀t. memory_chunk → expr (ASTptr Any) → expr t → stmt
    1820(* ident for returned value, expression to identify fn, args. *)
    19 | St_call : option ident → expr → list expr → stmt
    20 | St_tailcall : expr → list expr → stmt
     21| St_call : option ident → expr (ASTptr Code) → list (Σt. expr t) → stmt
     22| St_tailcall : expr (ASTptr Code) → list (Σt. expr t) → stmt
    2123| St_seq : stmt → stmt → stmt
    22 | St_ifthenelse : expr → stmt → stmt → stmt
     24| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
    2325| St_loop : stmt → stmt
    2426| St_block : stmt → stmt
    2527| St_exit : nat → stmt
    2628(* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
    27 | St_switch : expr → list (int × nat) → nat → stmt
    28 | St_return : option expr → stmt
     29| St_switch : ∀sz,sg. expr (ASTint sz sg) → list (int × nat) → nat → stmt
     30| St_return : option (Σt. expr t) → stmt
    2931| St_label : ident → stmt → stmt
    3032| St_goto : ident → stmt
Note: See TracChangeset for help on using the changeset viewer.