include "LIN/joint_LTL_LIN_semantics.ma".
include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)

definition lin_succ_pc: unit → address → res address :=
 λ_.λaddr. addr_add addr 1.

axiom BadOldPointer: String.
(*CSC: XXX factorize the code with graph_fetch_function!!! *)
definition lin_fetch_function:
 ∀globals. genv … (lin_params globals) → pointer → res (joint_internal_function globals (lin_params globals)) ≝
 λglobals,ge,old.
  let b ≝ pblock old in
  do def ← opt_to_res ? [MSG BadOldPointer] (find_funct_ptr … ge b);
  match def with
  [ Internal fn ⇒ OK … fn
  | External _ ⇒ Error … [MSG BadOldPointer]].

axiom BadLabel: String.
definition lin_pointer_of_label:
 ∀globals. genv … (lin_params globals) → pointer → label → res (Σp:pointer. ptype p = Code) ≝
 λglobals,ge,old,l.
  do fn ← lin_fetch_function … ge old ;
  do pos ←
   opt_to_res ? [MSG BadLabel]
    (position_of ?
      (λs. let 〈l',x〉 ≝ s in
        match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
     (joint_if_code … (lin_params …) fn)) ;
  OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
// qed.

(*CSC: XXX factorize code with graph_fetch_statement?*)
axiom BadProgramCounter: String.
definition lin_fetch_statement:
 ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params unit) → res (pre_lin_statement globals) ≝
 λglobals,ge,st.
  do ppc ← pointer_of_address (pc … st) ;
  do fn ← lin_fetch_function … ge ppc ;
  let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *)
  do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ;
  OK … (\snd found).

definition lin_fullexec: fullexec io_out io_in ≝
 ltl_lin_fullexec … lin_succ_pc … lin_fetch_statement lin_pointer_of_label.