source: src/joint/Joint.ma @ 1220

Last change on this file since 1220 was 1220, checked in by sacerdot, 8 years ago

ERTL ported to the new joint syntax.

File size: 4.0 KB
Line 
1include "ASM/I8051.ma".
2include "common/CostLabel.ma".
3include "common/AST.ma".
4include "common/Registers.ma".
5include "common/Graphs.ma".
6
7record params: Type[1] ≝
8{
9  acc_a_reg: Type[0];
10  acc_b_reg: Type[0];
11  dpl_reg: Type[0];
12  dph_reg: Type[0];
13  pair_reg: Type[0];
14  generic_reg: Type[0];
15 
16  extend_statements: Type[0];
17 
18  resultT: Type[0];
19  localsT: Type[0];
20  paramsT: Type[0]
21}.
22
23inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝
24  | joint_instr_comment: String → joint_instruction p globals
25  | joint_instr_cost_label: costlabel → joint_instruction p globals
26  | joint_instr_int: generic_reg p → Byte → joint_instruction p globals
27  | joint_instr_move: pair_reg p → joint_instruction p globals
28  | joint_instr_pop: acc_a_reg p → joint_instruction p globals
29  | joint_instr_push: acc_a_reg p → joint_instruction p globals
30  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
31  | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals
32  | joint_instr_op1: Op1 → acc_a_reg p → joint_instruction p globals
33  | joint_instr_op2: Op2 → acc_a_reg p → generic_reg p → joint_instruction p globals
34  | joint_instr_clear_carry: joint_instruction p globals
35  | joint_instr_set_carry: joint_instruction p globals
36  | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
37  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
38  | joint_instr_call_id: ident → nat → joint_instruction p globals
39  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
40
41inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
42  | joint_st_sequential: joint_instruction p globals → label → joint_statement p globals
43  | joint_st_goto: label → joint_statement p globals
44  | joint_st_return: joint_statement p globals
45  | joint_st_extension: extend_statements p → joint_statement p globals.
46
47record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
48 { pmemoryT: Type[0]
49 ; lookup: pmemoryT → label → option (joint_statement preparams globals)
50 }.
51
52record joint_internal_function (globals: list ident) (pre) (p:sem_params_ pre globals): Type[0] ≝
53{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
54  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
55(*  joint_if_sig: signature;  -- dropped in front end *)
56  joint_if_result   : resultT pre;
57  joint_if_params   : paramsT pre;
58  joint_if_locals   : localsT pre;
59  joint_if_stacksize: nat;
60  joint_if_graph    : pmemoryT … p;
61  joint_if_entry    : Σl: label. lookup … p joint_if_graph l ≠ None ?;
62  joint_if_exit     : Σl: label. lookup … p joint_if_graph l ≠ None ?
63}.
64
65definition set_luniverse ≝
66  λglobals  : list ident.
67  λpre.
68  λp: sem_params_ pre globals.
69  λint_fun  : joint_internal_function globals … p.
70  λluniverse: universe LabelTag.
71  let runiverse ≝ joint_if_runiverse … int_fun in
72  let params    ≝ joint_if_params … int_fun in
73  let locals    ≝ joint_if_locals … int_fun in
74  let result    ≝ joint_if_result … int_fun in
75  let stacksize ≝ joint_if_stacksize … int_fun in
76  let graph     ≝ joint_if_graph … int_fun in
77  let entry     ≝ joint_if_entry … int_fun in
78  let exit      ≝ joint_if_exit … int_fun in
79    mk_joint_internal_function globals ? p
80      luniverse runiverse result params locals
81      stacksize graph entry exit.
82
83definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
84
85definition joint_program :=
86 λglobals:list ident.λpre.λp: sem_params_ pre globals.
87  program (joint_function … p) nat.
88
89(****************************************************************************)
90
91(* Used in LTL and LIN *) 
92inductive registers_move: Type[0] ≝
93 | from_acc: Register → registers_move
94 | to_acc: Register → registers_move.
Note: See TracBrowser for help on using the repository browser.