source: src/joint/Joint.ma @ 1248

Last change on this file since 1248 was 1246, checked in by sacerdot, 9 years ago

Yet another change to Joint.ma to accomodate all passes.
The concrete memory representation for the code of internal functions is
back, at the price of more complexity in the definition of the parameters.

Note: I do not understand any more the well_formed_P invariant for LIN code.
Moreover, the invariant does not seem to hold for code produced using LTLToLin.

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
[1182]43  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
[733]44
[1246]45inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
[1233]46  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
[1182]47  | joint_st_goto: label → joint_statement p globals
[1176]48  | joint_st_return: joint_statement p globals
49  | joint_st_extension: extend_statements p → joint_statement p globals.
[1169]50
[1246]51record params (globals: list ident): Type[1] ≝
52 { pars_:> params_
53 ; codeT: Type[0]
54 ; lookup: codeT → label → option (joint_statement pars_ globals)
55 }.
56
57record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
[1176]58{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
59  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
60(*  joint_if_sig: signature;  -- dropped in front end *)
[1233]61  joint_if_result   : resultT p;
62  joint_if_params   : paramsT p;
63  joint_if_locals   : localsT p;
[1236]64(*CSC: XXXXX stacksize unused for LTL-...*)
[1176]65  joint_if_stacksize: nat;
[1246]66  joint_if_code     : codeT … p;
[1236]67(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
[1246]68  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
[1236]69(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
[1246]70  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
[1176]71}.
72
[1245]73(* Currified form *)
74definition set_joint_if_exit ≝
75  λpars,globals.
76  λexit: label.
77  λp: joint_internal_function pars globals.
[1246]78  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
[1245]79   mk_joint_internal_function pars globals
80    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
81    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
[1246]82    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
[1245]83
[1220]84definition set_luniverse ≝
85  λglobals  : list ident.
[1246]86  λp:params globals.
87  λint_fun  : joint_internal_function globals p.
[1220]88  λluniverse: universe LabelTag.
89  let runiverse ≝ joint_if_runiverse … int_fun in
90  let params    ≝ joint_if_params … int_fun in
91  let locals    ≝ joint_if_locals … int_fun in
92  let result    ≝ joint_if_result … int_fun in
93  let stacksize ≝ joint_if_stacksize … int_fun in
[1246]94  let code      ≝ joint_if_code … int_fun in
[1220]95  let entry     ≝ joint_if_entry … int_fun in
96  let exit      ≝ joint_if_exit … int_fun in
[1246]97    mk_joint_internal_function globals p
[1220]98      luniverse runiverse result params locals
[1246]99      stacksize code entry exit.
[1220]100
[1233]101definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
[1176]102
[1246]103definition joint_program ≝
104 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
[1176]105
106(****************************************************************************)
107
[1169]108(* Used in LTL and LIN *) 
109inductive registers_move: Type[0] ≝
110 | from_acc: Register → registers_move
[1176]111 | to_acc: Register → registers_move.
Note: See TracBrowser for help on using the repository browser.