include "common/Graphs.ma".
include "utilities/IdentifierTools.ma".
include "LIN/LIN.ma".

definition ltl_statement ≝ joint_statement ident.
  
definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
  
record ltl_internal_function (globals: list ident): Type[0] ≝
{
  ltl_if_luniverse: universe LabelTag;
  ltl_if_runiverse: universe RegisterTag;
  ltl_if_StackSize: nat;
  ltl_if_Graph: ltl_statement_graph globals;
  ltl_if_Entry: label;
  ltl_if_Exit: label
}.

inductive ltl_function_definition (globals: list ident): Type[0] ≝
  | ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals
  | ltl_fu_external_function: external_function → ltl_function_definition globals.
  
record ltl_program (globals: list (ident × nat)): Type[0] ≝
{
  ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals)));
  ltl_pr_main: option ident
}.