source: src/joint/Joint.ma @ 1250

Last change on this file since 1250 was 1250, checked in by sacerdot, 9 years ago
  1. Sigma types projections moved to utilities/extralib.ma
  2. Extended statement turned into extended instructions, decreasing the amount of code in the translations
File size: 4.6 KB
RevLine 
[733]1include "ASM/I8051.ma".
[757]2include "common/CostLabel.ma".
[733]3include "common/AST.ma".
[757]4include "common/Registers.ma".
[1176]5include "common/Graphs.ma".
[733]6
[1246]7record params__: Type[1] ≝
[1233]8 { acc_a_reg: Type[0]
9 ; acc_b_reg: Type[0]
10 ; dpl_reg: Type[0]
11 ; dph_reg: Type[0]
12 ; pair_reg: Type[0]
13 ; generic_reg: Type[0]
[1176]14 
[1233]15 ; extend_statements: Type[0]
[1176]16 
[1233]17 ; resultT: Type[0]
18 ; localsT: Type[0]
19 ; paramsT: Type[0]
20 }.
[1164]21
[1246]22record params_: Type[1] ≝
23 { pars__:> params__
[1233]24 ; succ: Type[0]
25 }.
26
[1246]27inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
[1169]28  | joint_instr_comment: String → joint_instruction p globals
29  | joint_instr_cost_label: costlabel → joint_instruction p globals
30  | joint_instr_int: generic_reg p → Byte → joint_instruction p globals
31  | joint_instr_move: pair_reg p → joint_instruction p globals
32  | joint_instr_pop: acc_a_reg p → joint_instruction p globals
33  | joint_instr_push: acc_a_reg p → joint_instruction p globals
34  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
35  | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals
36  | joint_instr_op1: Op1 → acc_a_reg p → joint_instruction p globals
37  | joint_instr_op2: Op2 → acc_a_reg p → generic_reg p → joint_instruction p globals
38  | joint_instr_clear_carry: joint_instruction p globals
39  | joint_instr_set_carry: joint_instruction p globals
40  | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
41  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
42  | joint_instr_call_id: ident → nat → joint_instruction p globals
[1250]43  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals
44  | joint_instr_extension: extend_statements p → joint_instruction p globals.
[733]45
[1246]46inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
[1233]47  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
[1182]48  | joint_st_goto: label → joint_statement p globals
[1250]49  | joint_st_return: joint_statement p globals.
[1169]50
[1250]51
[1246]52record params (globals: list ident): Type[1] ≝
53 { pars_:> params_
54 ; codeT: Type[0]
55 ; lookup: codeT → label → option (joint_statement pars_ globals)
56 }.
57
58record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
[1176]59{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
60  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
61(*  joint_if_sig: signature;  -- dropped in front end *)
[1233]62  joint_if_result   : resultT p;
63  joint_if_params   : paramsT p;
64  joint_if_locals   : localsT p;
[1236]65(*CSC: XXXXX stacksize unused for LTL-...*)
[1176]66  joint_if_stacksize: nat;
[1246]67  joint_if_code     : codeT … p;
[1236]68(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
[1246]69  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
[1236]70(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
[1246]71  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
[1176]72}.
73
[1245]74(* Currified form *)
75definition set_joint_if_exit ≝
76  λpars,globals.
77  λexit: label.
78  λp: joint_internal_function pars globals.
[1246]79  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
[1245]80   mk_joint_internal_function pars globals
81    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
82    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
[1246]83    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
[1245]84
[1220]85definition set_luniverse ≝
86  λglobals  : list ident.
[1246]87  λp:params globals.
88  λint_fun  : joint_internal_function globals p.
[1220]89  λluniverse: universe LabelTag.
90  let runiverse ≝ joint_if_runiverse … int_fun in
91  let params    ≝ joint_if_params … int_fun in
92  let locals    ≝ joint_if_locals … int_fun in
93  let result    ≝ joint_if_result … int_fun in
94  let stacksize ≝ joint_if_stacksize … int_fun in
[1246]95  let code      ≝ joint_if_code … int_fun in
[1220]96  let entry     ≝ joint_if_entry … int_fun in
97  let exit      ≝ joint_if_exit … int_fun in
[1246]98    mk_joint_internal_function globals p
[1220]99      luniverse runiverse result params locals
[1246]100      stacksize code entry exit.
[1220]101
[1233]102definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
[1176]103
[1246]104definition joint_program ≝
105 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
[1176]106
107(****************************************************************************)
108
[1169]109(* Used in LTL and LIN *) 
110inductive registers_move: Type[0] ≝
111 | from_acc: Register → registers_move
[1176]112 | to_acc: Register → registers_move.
Note: See TracBrowser for help on using the repository browser.