Ignore:
Timestamp:
Jan 25, 2011, 5:30:36 PM (9 years ago)
Author:
campbell
Message:

Prevent clashes between names in AST and other parts of the development.
(Noticed when trying a large example file.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Cexec.ma

    r457 r478  
    471471
    472472ndefinition eventval_type : ∀ty:typ. Type ≝
    473 λty. match ty with [ Tint ⇒ int | Tfloat ⇒ float ].
     473λty. match ty with [ ASTint ⇒ int | ASTfloat ⇒ float ].
    474474
    475475ndefinition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    476 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ Tint ⇒ λv.EVint v | Tfloat ⇒ λv.EVfloat v ].
     476λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTfloat ⇒ λv.EVfloat v ].
    477477
    478478ndefinition mk_val: ∀ty:typ. eventval_type ty → val ≝
    479 λty:typ. match ty return λty'.eventval_type ty' → val with [ Tint ⇒ λv.Vint v | Tfloat ⇒ λv.Vfloat v ].
     479λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTfloat ⇒ λv.Vfloat v ].
    480480
    481481nlemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
     
    486486λev,ty.
    487487match ty with
    488 [ Tint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ]
    489 | Tfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ]
     488[ ASTint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ]
     489| ASTfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ]
    490490| _ ⇒ Some ? (Error ?)
    491491]. nwhd; //; nqed.
     
    494494λv,ty.
    495495match ty with
    496 [ Tint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ]
    497 | Tfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ]
     496[ ASTint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ]
     497| ASTfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ]
    498498| _ ⇒ Some ? (Error ?)
    499499]. nwhd; //; nqed.
     
    694694].
    695695
    696 nlet rec make_initial_state (p:program) : res state ≝
     696nlet rec make_initial_state (p:clight_program) : res state ≝
    697697  let ge ≝ globalenv Genv ?? p in
    698698  let m0 ≝ init_mem Genv ?? p in
     
    769769
    770770
    771 ndefinition exec_inf : program → execution ≝
     771ndefinition exec_inf : clight_program → execution ≝
    772772λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,s〉).
    773773
Note: See TracChangeset for help on using the changeset viewer.