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

(* Here is the structure of parameter records (downward edges are coercions,
   the ↓ edges are the only explicitly defined coercions). lin_params and
   graph_params are simple wrappers of unserialized_params, and the coercions
   from them to params instantiate the missing bits with values for linarized
   programs and graph programs respectively. 

        lin_params      graph_params
          |       \_____ /____   |
          |             /     \  |
          \_______     /      ↓  ↓
                  \   _\____ params
                   \_/  \      |
                    / \  \     ↓
              _____/   unserialized_params
             /      _______/   | 
            /      /           | 
     stmt_params  /   local_params
        |      __/             |
    inst_params       funct_params

inst_params : types needed to define instructions
stmt_params : adds successor type needed to define statements
funct_params : types of result register and parameters of function
local_params : adds types of local registers
params : adds type of code and lookup function
graph_params : is made just of inst_params and local_params, and the coercion
  to params adds structure common to graph languages *)

record inst_params : Type[1] ≝ 
 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
 ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *)
 ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *)
 ; dpl_reg: Type[0]   (* low address registers *)
 ; dph_reg: Type[0]   (* high address registers *)
 ; dpl_arg: Type[0]   (* low address registers *)
 ; dph_arg: Type[0]   (* high address registers *)
 ; snd_arg : Type[0]  (* second argument of binary op *)
 ; pair_move: Type[0] (* argument of move instructions *)
 ; call_args: Type[0] (* arguments of function calls *)
 ; call_dest: Type[0] (* possible destination of function computation *)
 ; ext_instruction: Type[0] (* other instructions not fitting in the general framework *)
 ; ext_forall_labels : (label → Prop) → ext_instruction → Prop
 ; ext_fin_instruction: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
 ; ext_fin_forall_labels : (label → Prop) → ext_fin_instruction → Prop
 }.
 
inductive joint_instruction (p:inst_params) (globals: list ident): Type[0] ≝
  | COMMENT: String → joint_instruction p globals
  | COST_LABEL: costlabel → joint_instruction p globals
  | MOVE: pair_move p → joint_instruction p globals
  | POP: acc_a_reg p → joint_instruction p globals
  | PUSH: acc_a_arg 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_arg p → acc_b_arg 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_arg p → snd_arg p → joint_instruction p globals
  (* int done with generic move *)
(*| INT: generic_reg p → Byte → joint_instruction p globals *)
  | CLEAR_CARRY: joint_instruction p globals
  | SET_CARRY: joint_instruction p globals
  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals
  | STORE: dpl_arg p → dph_arg p → acc_a_arg 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: ext_instruction p → joint_instruction p globals.

coercion extension_to_instruction :
  ∀p,globals.∀c : ext_instruction p.joint_instruction p globals ≝
  extension
  on _c : ext_instruction ? to joint_instruction ??.

notation "r ← a1 .op. a2" with precedence 50 for
  @{'op2 $op $r $a1 $a2}.
notation "r ← . op . a" with precedence 50 for
  @{'op1 $op $r $a}.
notation "r ← a" with precedence 50 for
  @{'mov $r $a}. (* to be set in individual languages *)
notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
  @{'opaccs $op $r $s $a1 $a2}.

interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).


definition inst_forall_labels : ∀p : inst_params.∀globals.
    (label → Prop) → joint_instruction p globals → Prop ≝
λp,g,P,inst. match inst with
  [ COND _ l ⇒ P l
  | extension ext_s ⇒ ext_forall_labels p P ext_s
  | _ ⇒ True
 ].

record funct_params : Type[1] ≝
  { resultT : Type[0]
  ; paramsT : Type[0]
  }.
  
record local_params : Type[1] ≝
 { funct_pars :> funct_params
 ; localsT: Type[0]
 }.

record unserialized_params : Type[1] ≝
 { u_inst_pars :> inst_params
 ; u_local_pars :> local_params
 }.

record stmt_params : Type[1] ≝
  { unserialized_pars :> unserialized_params
  ; succ : Type[0]
  ; succ_forall_labels : (label → Prop) → succ → Prop
  }. 

inductive joint_statement (p: stmt_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
  | extension_fin : ext_fin_instruction p → joint_statement p globals.

coercion extension_fin_to_statement :
  ∀p : stmt_params.∀globals.∀c : ext_fin_instruction p.joint_statement p globals ≝
  extension_fin
  on _c : ext_fin_instruction ? to joint_statement ??.

record params : Type[1] ≝
 { stmt_pars :> stmt_params
 ; codeT: list ident → Type[0]
 ; code_has_label: ∀globals.codeT globals → label → Prop
 ; forall_statements : ∀globals.(joint_statement stmt_pars globals → Prop) →
    codeT globals → Prop
 }.


definition stmt_forall_labels : ∀p : stmt_params.∀globals.
    (label → Prop) → joint_statement p globals → Prop ≝
  λp,g,P,stmt. match stmt with
  [ sequential inst next ⇒ inst_forall_labels p g P inst ∧ succ_forall_labels p P next
  | GOTO l ⇒ P l
  | RETURN ⇒ True
  | extension_fin c ⇒ ext_fin_forall_labels … P c
  ].

record lin_params : Type[1] ≝
  { l_u_pars :> unserialized_params }.

include "utilities/option.ma".

definition lin_params_to_params ≝
  λlp : lin_params.
     mk_params
      (mk_stmt_params lp unit (λ_.λ_.True))
    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    (* code_has_label ≝ *)(λglobals,code,lbl.Exists ?
        (λl_stmt. \fst l_stmt = Some ? lbl) code)
    (* forall_statements ≝ *)(λglobals,P,code.All ?
        (λl_stmt. P (\snd l_stmt)) code).

coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
  on _lp : lin_params to params.

record graph_params : Type[1] ≝
  { g_u_pars :> unserialized_params }.

(* One common instantiation of params via Graphs of joint_statements
   (all languages but LIN) *)
definition graph_params_to_params ≝
  λgp : graph_params.
     mk_params
      (mk_stmt_params gp label (λP.P))
    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    (* code_has_label ≝ *)(λglobals,code,lbl.lookup … code lbl ≠ None ?)
    (* forall_statements ≝ *)(λglobals,P,code.
      ∀l,s.lookup … code l = Some ? s → P s).
    
coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
on _gp : graph_params to params.
   

definition labels_present : ∀globals.∀p : params.
  codeT p globals → (joint_statement p globals) → Prop ≝
λglobals,p,code,s. stmt_forall_labels p globals
  (λl.code_has_label ?? code l) s.

definition code_closed : ∀p : params.∀globals.
  codeT p globals → Prop ≝ λp,globals,code.
    forall_statements … (labels_present … code) code.

(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))).

record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
  (* Paolo: if we want this machinery to work for RTLabs too, we will need the
     following, right? *)
(*  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 globals ;
(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
  joint_if_entry    : Σl: label. code_has_label … joint_if_code l;
(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
  joint_if_exit     : Σl: label. code_has_label …  … joint_if_code l
}.

definition joint_closed_internal_function ≝
  λglobals,p.
    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).

(* Currified form *)
definition set_joint_if_exit ≝
  λglobals,pars.
  λexit: label.
  λp:joint_internal_function globals pars.
  λprf: code_has_label … (joint_if_code … p) exit.
   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) (mk_Sig … exit prf).

definition set_joint_code ≝
  λglobals: list ident.
  λpars: params.
  λint_fun: joint_internal_function globals pars.
  λgraph: codeT pars globals.
  λentry.
  λexit.
    mk_joint_internal_function globals pars
      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
      graph entry exit.

definition set_joint_if_graph ≝
  λglobals,pars.
  λgraph.
  λp:joint_internal_function globals pars.
  λentry_prf: code_has_label … graph (joint_if_entry … p).
  λexit_prf: code_has_label … graph (joint_if_exit … p).
    set_joint_code globals pars p 
      graph
      (mk_Sig … (joint_if_entry … p) entry_prf)
      (mk_Sig … (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).
    
(* Paolo: probably should move these elsewhere *)
definition graph_dom ≝ λX.λg : graph X.Σl : label.lookup … g l ≠ None ?.
definition graph_dom_add_incl : ∀X.∀g : graph X.∀l : label.∀x : X.
  graph_dom ? g → graph_dom ? (add … g l x) ≝ λX,g,l,x,sig_l.
  mk_Sig … (pi1 ?? sig_l) ?.
@graph_add_lookup
@(pi2 … sig_l)
qed.

(* Specialized for graph_params *)
definition add_graph ≝
  λg_pars : graph_params.λglobals.λl:label.λstmt.
    λp:joint_internal_function globals g_pars.
   let code ≝ add … (joint_if_code … p) l stmt in
    mk_joint_internal_function ? g_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)
     code
     (graph_dom_add_incl … (joint_if_entry … p))
     (graph_dom_add_incl … (joint_if_exit … p)).

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:params. program (λglobals. joint_function globals p) nat.