Ignore:
Timestamp:
Apr 15, 2011, 4:26:23 PM (9 years ago)
Author:
campbell
Message:

An experimental branch of the Cminor semantics.

Location:
Deliverables/D3.3
Files:
2 added
1 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/Cminor-experiment/syntax.ma

    r754 r755  
    1212| Ecost : costlabel → expr → expr.
    1313
    14 inductive stmt : Type[0] ≝
    15 | St_skip : stmt
    16 | St_assign : ident → expr → stmt
    17 | St_store : memory_chunk → expr → expr → stmt
     14inductive Fin : nat → Type[0] ≝
     15| FO : ∀n. Fin (S n)
     16| FS : ∀n. Fin n → Fin (S n).
     17
     18inductive stmt : ∀blockdepth:nat. Type[0] ≝
     19| St_skip : ∀n. stmt n
     20| St_assign : ident → expr → ∀n. stmt n
     21| St_store : memory_chunk → expr → expr → ∀n. stmt n
    1822(* ident for returned value, expression to identify fn, args, signature. *)
    19 | St_call : option ident → expr → list expr → signature → stmt
    20 | St_tailcall : expr → list expr → signature → stmt
    21 | St_seq : stmt → stmt → stmt
    22 | St_ifthenelse : expr → stmt → stmt → stmt
    23 | St_loop : stmt → stmt
    24 | St_block : stmt → stmt
    25 | St_exit : nat → stmt
     23| St_call : option ident → expr → list expr → signature → ∀n. stmt n
     24| St_tailcall : expr → list expr → signature → ∀n. stmt n
     25| St_seq : ∀n. stmt n → stmt n → stmt n
     26| St_ifthenelse : expr → ∀n. stmt n → stmt n → stmt n
     27| St_loop : ∀n. stmt n → stmt n
     28| St_block : ∀n. stmt (S n) → stmt n
     29| St_exit : ∀n. Fin n → stmt n
    2630(* 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_label : ident → stmt → stmt
    30 | St_goto : ident → stmt
    31 | St_cost : costlabel → stmt → stmt.
     31| St_switch : expr → ∀n. list (int × (Fin n)) → Fin n → stmt n
     32| St_return : option expr → ∀n. stmt n
     33| St_label : ident → ∀n. stmt n → stmt n
     34| St_goto : ident → ∀n. stmt n
     35| St_cost : costlabel → ∀n. stmt n → stmt n.
    3236
    3337record internal_function : Type[0] ≝
     
    3741; f_ptrs      : list ident
    3842; f_stacksize : nat
    39 ; f_body      : stmt
     43; f_body      : stmt O
    4044}.
    4145(* XXX: matita interpretations bug workaround *)
Note: See TracChangeset for help on using the changeset viewer.