Changeset 718 for src/Clight/Cexec.ma


Ignore:
Timestamp:
Mar 29, 2011, 5:54:37 PM (9 years ago)
Author:
campbell
Message:

Add an AST type (i.e., intermediate language type) for pointers.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r708 r718  
    442442
    443443definition eventval_type : ∀ty:typ. Type[0] ≝
    444 λty. match ty with [ ASTint ⇒ int | ASTfloat ⇒ float ].
     444λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
    445445
    446446definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    447 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTfloat ⇒ λv.EVfloat v ].
     447λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
     448*; qed.
    448449
    449450definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    450 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTfloat ⇒ λv.Vfloat v ].
     451λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
     452*; qed.
    451453
    452454lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
    453455  eventval_match (mk_eventval ty v) ty (mk_val ty v).
    454 #ty cases ty; normalize; //; qed.
     456#ty cases ty; normalize; // * *; qed.
    455457
    456458definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
     
    467469[ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
    468470| ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
    469 | _ ⇒ Some ? (Error ?)
     471| _ ⇒ Error ?
    470472].
    471473
Note: See TracChangeset for help on using the changeset viewer.