include "joint/Joint.ma".
include "utilities/lists.ma".

definition lin_params__: params__ ≝
 mk_params__ unit unit unit unit registers_move Register nat unit False.
definition lin_params_ : params_ ≝ mk_params_ lin_params__ unit.
definition lin_params0 : params0 ≝ mk_params0 lin_params__ unit unit.
definition lin_params1 : params1 ≝ mk_params1 lin_params0 unit.

definition pre_lin_statement ≝ joint_statement lin_params_.

definition well_formed_P ≝
  λA, B: Type[0].
  λcode: list (option A × B).
    match code with
    [ nil ⇒ False
    | cons hd tl ⇒
      match \fst hd with
      [ Some lbl ⇒ False
      | None ⇒ True]].

definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals).

definition lin_params: ∀globals. params globals ≝
 λglobals.
  mk_params globals unit lin_params1 (Σcode:list (lin_statement globals). well_formed_P … code)
   (λcode:Σcode.?. λl.
    find ?? (λs. let 〈l',x〉 ≝ s in
     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code).

definition lin_function ≝ λglobals. joint_function … (lin_params globals).

definition lin_program ≝ joint_program lin_params.