include "ASM/I8051.ma".
include "common/CostLabel.ma".
include "common/AST.ma".
include "common/Registers.ma".
include "utilities/sigma.ma". (* CSC: Only for Sigma type projections *)
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]
 ; call_args: Type[0]
 ; call_dest: Type[0]
 
 ; extend_statements: Type[0]
 }.

record params_: Type[1] ≝
 { pars__:> params__
 ; succ: Type[0]
 }.

(* One common instantiation of params via Graphs of joint_statements
   (all languages but LIN) *)
definition graph_params_ : params__ → params_ ≝
 λpars__. mk_params_ pars__ label.

inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
  | COMMENT: String → joint_instruction p globals
  | COST_LABEL: costlabel → joint_instruction p globals
  | INT: generic_reg p → Byte → joint_instruction p globals
  | MOVE: pair_reg p → joint_instruction p globals
  | POP: acc_a_reg p → joint_instruction p globals
  | PUSH: acc_a_reg p → joint_instruction p globals
  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
  | OP2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
  | CLEAR_CARRY: joint_instruction p globals
  | SET_CARRY: joint_instruction p globals
  | LOAD: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
  | STORE: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
  | COND: acc_a_reg p → label → joint_instruction p globals
  | extension: extend_statements p → joint_instruction p globals.

inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
  | sequential: joint_instruction p globals → succ p → joint_statement p globals
  | GOTO: label → joint_statement p globals
  | RETURN: joint_statement p globals.

record params0: Type[1] ≝
 { pars__' :> params__
 ; resultT: Type[0]
 ; paramsT: Type[0]
 }.

record params1 : Type[1] ≝
 { pars0 :> params0
 ; localsT: Type[0]
 }.

record params (globals: list ident): Type[1] ≝
 { succ_ : Type[0]
 ; pars1 :> params1
 ; codeT: Type[0]
 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
 }.
 
definition params__of_params: ∀globals. params globals → params_ ≝
 λglobals,pars. mk_params_ pars (succ_ … pars).
coercion params__of_params: ∀globals.∀p: params globals. params_ ≝ params__of_params
 on _p: params ? to params_.

include alias "common/Graphs.ma". (* To pick the right lookup *)

(* One common instantiation of params via Graphs of joint_statements
   (all languages but LIN) *)
definition graph_params: params1 → ∀globals: list ident. params globals ≝
 λpars1,globals.
  mk_params globals label pars1
   (graph (joint_statement (graph_params_ pars1) globals)) (lookup …).


(* CSC: special case where localsT is a list of register (RTL and ERTL) *)
definition rtl_ertl_params1 ≝ λpars0. mk_params1 pars0 (list register).
definition rtl_ertl_params ≝ λpars0. graph_params (rtl_ertl_params1 pars0).

record joint_internal_function (globals: list ident) (p:params 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 p;
  joint_if_params   : paramsT p;
  joint_if_locals   : localsT p;
(*CSC: XXXXX stacksize unused for LTL-...*)
  joint_if_stacksize: nat;
  joint_if_code     : codeT … p;
(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
}.

(* Currified form *)
definition set_joint_if_exit ≝
  λglobals,pars.
  λexit: label.
  λp:joint_internal_function globals pars.
  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
   mk_joint_internal_function globals pars
    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).

definition set_joint_if_graph ≝
  λglobals,pars.
  λgraph.
  λp:joint_internal_function globals pars.
  λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
   mk_joint_internal_function globals pars
    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    graph (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).

definition set_luniverse ≝
  λglobals,pars.
  λp : joint_internal_function globals pars.
  λluniverse: universe LabelTag.
   mk_joint_internal_function globals pars
    luniverse (joint_if_runiverse … p) (joint_if_result … p)
    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).

definition set_runiverse ≝
  λglobals,pars.
  λp : joint_internal_function globals pars.
  λruniverse: universe RegisterTag.
   mk_joint_internal_function globals pars
    (joint_if_luniverse … p) runiverse (joint_if_result … p)
    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).

(* Specialized for graph_params *)
definition add_graph ≝
  λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals).
   let code ≝ add … (joint_if_code ?? p) l stmt in
    mk_joint_internal_function … (graph_params … globals)
     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
  normalize nodelta;
  [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
  #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
qed.

definition set_locals ≝
  λglobals,pars.
  λp : joint_internal_function globals pars.
  λlocals.
   mk_joint_internal_function globals pars
    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    (joint_if_params … p) locals (joint_if_stacksize … p)
    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).

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

definition joint_program ≝
 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.

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

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