source: src/joint/Joint.ma @ 1176

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

...

File size: 3.4 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 { next: Type[0]
9 
10 ; acc_a_reg: Type[0]
11 ; acc_b_reg: Type[0]
12 ; dpl_reg: Type[0]
13 ; dph_reg: Type[0]
14 ; pair_reg: Type[0]
15 ; generic_reg: Type[0]
16 
17 ; extend_statements: Type[0]
18 
19 ; resultT: Type[0]
20 ; localsT: Type[0]
21 ; paramsT: Type[0]
22 }.
23
24inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝
25  | joint_instr_comment: String → joint_instruction p globals
26  | joint_instr_cost_label: costlabel → joint_instruction p globals
27  | joint_instr_int: generic_reg p → Byte → joint_instruction p globals
28  | joint_instr_move: pair_reg p → joint_instruction p globals
29  | joint_instr_pop: acc_a_reg p → joint_instruction p globals
30  | joint_instr_push: acc_a_reg p → joint_instruction p globals
31  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
32  | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals
33  | joint_instr_op1: Op1 → acc_a_reg p → joint_instruction p globals
34  | joint_instr_op2: Op2 → acc_a_reg p → generic_reg p → joint_instruction p globals
35  | joint_instr_clear_carry: joint_instruction p globals
36  | joint_instr_set_carry: joint_instruction p globals
37  | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
38  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
39  | joint_instr_call_id: ident → nat → joint_instruction p globals
40  | joint_instr_cond: acc_a_reg p → next p → joint_instruction p globals.
41
42inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
43  | joint_st_sequential: joint_instruction p globals → next p → joint_statement p globals
44  | joint_st_goto: next p → joint_statement p globals
45  | joint_st_return: joint_statement p globals
46  | joint_st_extension: extend_statements p → joint_statement p globals.
47
48record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝
49 { pmemoryT: Type[0]
50 ; lookup: pmemoryT → next preparams → option (joint_statement preparams globals)
51 }.
52
53record joint_internal_function (globals: list ident) (pre) (p:sem_params_ pre globals): Type[0] ≝
54{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
55  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
56(*  joint_if_sig: signature;  -- dropped in front end *)
57  joint_if_result   : resultT pre;
58  joint_if_params   : paramsT pre;
59  joint_if_locals   : localsT pre;
60  joint_if_stacksize: nat;
61  joint_if_graph    : pmemoryT … p;
62  joint_if_entry    : Σl: next pre. lookup … p joint_if_graph l ≠ None ?;
63  joint_if_exit     : Σl: next pre. lookup … p joint_if_graph l ≠ None ?
64}.
65
66definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
67
68record joint_program (globals: list ident) (pre) (p:sem_params_ pre globals) : Type[0] ≝
69{
70  joint_pr_vars: list (ident × nat);
71  joint_pr_functs: list (ident × (joint_function … p));
72  joint_pr_main: option ident
73}.
74
75(****************************************************************************)
76
77(* Used in LTL and LIN *) 
78inductive registers_move: Type[0] ≝
79 | from_acc: Register → registers_move
80 | to_acc: Register → registers_move.
Note: See TracBrowser for help on using the repository browser.