include "Clight/Csem.ma".

(* I previously had a complicated definition that said a labelled Clight state
   was one with a syntactic form that would emit a cost label in the trace when
   the next step is evaluated.  This is the wrong notion.
   
   We want a labelled Clight state to indicate that we can measure the time of
   some correspondingly labelled machine code from there.  Only explicit
   statement level cost labels are useful for this.  Cost labels that appear
   in the middle of expressions are only useful for allowing the amount of time
   measured to differ.
   
   (Otherwise you see something silly like "x=(y-1) ? c1: 1 : c2: z;" as a
   labelled state, even though the labels c1 and c2 will appear in the *middle*
   of the corresponding machine code, and so you measure the wrong thing and
   can't prove it.)
 *)

definition Clight_labelled : state → bool ≝
λs. match s with
[ State f s k e m ⇒ match s with [ Scost _ _ ⇒ true | _ ⇒ false ]
| _ ⇒ false
].


(* At the moment this doesn't say anything about "jumps", just calls, returns
   and everything else. *)
include "common/StructuredTraces.ma".

definition Clight_classify : state → status_class ≝
λs. match s with
[ State _ _ _ _ _ ⇒ cl_other
| Callstate _ _ _ _ _ ⇒ cl_call
| Returnstate _ _ _ ⇒ cl_return
| Finalstate _ ⇒ cl_other
].

(* Help avoid ambiguous input fun *)
definition Clight_state ≝ state.

definition cl_genv ≝ genv.

definition cl_env ≝ env.

definition cl_cont ≝ cont.

definition cl_eval_expr ≝ eval_expr.

(* creating aliases constructors for states and continuations *)
definition ClState ≝ State.

definition ClReturnstate ≝ Returnstate.

definition ClCallstate ≝ Callstate.

definition ClKseq ≝ Kseq.