Changeset 708 for src/Clight/Cexec.ma


Ignore:
Timestamp:
Mar 23, 2011, 2:28:55 PM (9 years ago)
Author:
campbell
Message:

Use a more normalize-friendly definition of clight_exec to make the destruct
tactic usable again, and recomplete the equivalence proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r702 r708  
    667667  OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
    668668
     669let rec is_final (s:state) : option int ≝
     670match s with
     671[ Returnstate res k m ⇒
     672  match k with
     673  [ Kstop ⇒
     674    match res with
     675    [ Vint r ⇒ Some ? r
     676    | _ ⇒ None ?
     677    ]
     678  | _ ⇒ None ?
     679  ]
     680| _ ⇒ None ?
     681].
     682
    669683definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
    670684#st elim st;
     
    713727λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
    714728
    715 definition is_final : state → option int ≝
    716 λs.match is_final_state s with
    717 [ inl r ⇒ Some ? (sig_eject … r)
    718 | inr _ ⇒ None ?
    719 ].
    720 
    721729definition clight_exec : execstep ≝
    722730  mk_execstep … is_final mem_of_state exec_step.
Note: See TracChangeset for help on using the changeset viewer.