source: src/joint/Joint.ma @ 1220

include "ASM/I8051.ma".
include "common/CostLabel.ma".
include "common/AST.ma".
include "common/Registers.ma".
include "common/Graphs.ma".

record params: Type[1] ≝
{ 
  acc_a_reg: Type[0];
  acc_b_reg: Type[0];
  dpl_reg: Type[0];
  dph_reg: Type[0];
  pair_reg: Type[0];
  generic_reg: Type[0];
 
  extend_statements: Type[0];
 
  resultT: Type[0];
  localsT: Type[0];
  paramsT: Type[0]
}.

inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝
  | joint_instr_comment: String → joint_instruction p globals
  | joint_instr_cost_label: costlabel → joint_instruction p globals
  | joint_instr_int: generic_reg p → Byte → joint_instruction p globals
  | joint_instr_move: pair_reg p → joint_instruction p globals
  | joint_instr_pop: acc_a_reg p → joint_instruction p globals
  | joint_instr_push: acc_a_reg p → joint_instruction p globals
  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
  | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals
  | joint_instr_op1: Op1 → acc_a_reg p → joint_instruction p globals
  | joint_instr_op2: Op2 → acc_a_reg p → generic_reg p → joint_instruction p globals
  | joint_instr_clear_carry: joint_instruction p globals
  | joint_instr_set_carry: joint_instruction p globals
  | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
  | joint_instr_call_id: ident → nat → joint_instruction p globals
  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.

inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
  | joint_st_sequential: joint_instruction p globals → label → joint_statement p globals
  | joint_st_goto: label → joint_statement p globals
  | joint_st_return: joint_statement p globals
  | joint_st_extension: extend_statements p → joint_statement p globals.

record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
 { pmemoryT: Type[0]
 ; lookup: pmemoryT → label → option (joint_statement preparams globals)
 }.

record joint_internal_function (globals: list ident) (pre) (p:sem_params_ pre globals): Type[0] ≝
{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
(*  joint_if_sig: signature;  -- dropped in front end *)
  joint_if_result   : resultT pre;
  joint_if_params   : paramsT pre;
  joint_if_locals   : localsT pre;
  joint_if_stacksize: nat;
  joint_if_graph    : pmemoryT … p;
  joint_if_entry    : Σl: label. lookup … p joint_if_graph l ≠ None ?;
  joint_if_exit     : Σl: label. lookup … p joint_if_graph l ≠ None ?
}.

definition set_luniverse ≝
  λglobals  : list ident.
  λpre.
  λp: sem_params_ pre globals.
  λint_fun  : joint_internal_function globals … p.
  λluniverse: universe LabelTag.
  let runiverse ≝ joint_if_runiverse … int_fun in
  let params    ≝ joint_if_params … int_fun in
  let locals    ≝ joint_if_locals … int_fun in
  let result    ≝ joint_if_result … int_fun in
  let stacksize ≝ joint_if_stacksize … int_fun in
  let graph     ≝ joint_if_graph … int_fun in
  let entry     ≝ joint_if_entry … int_fun in
  let exit      ≝ joint_if_exit … int_fun in
    mk_joint_internal_function globals ? p
      luniverse runiverse result params locals
      stacksize graph entry exit.

definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).

definition joint_program :=
 λglobals:list ident.λpre.λp: sem_params_ pre globals.
  program (joint_function … p) nat.

(****************************************************************************)

(* Used in LTL and LIN *)  
inductive registers_move: Type[0] ≝
 | from_acc: Register → registers_move
 | to_acc: Register → registers_move.