source: Deliverables/D3.3/id-lookup-branch/joint/Joint.ma @ 1197

Last change on this file since 1197 was 1182, checked in by mulligan, 9 years ago

changes to semantics: removing parameterised "next" element in joint params (representing labels) as these are actually fixed across ertl, ltl and lin.

File size: 3.3 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 joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
66
67record joint_program (globals: list ident) (pre) (p:sem_params_ pre globals) : Type[0] ≝
68{
69  joint_pr_vars: list (ident × nat);
70  joint_pr_functs: list (ident × (joint_function … p));
71  joint_pr_main: option ident
72}.
73
74(****************************************************************************)
75
76(* Used in LTL and LIN *) 
77inductive registers_move: Type[0] ≝
78 | from_acc: Register → registers_move
79 | to_acc: Register → registers_move.
Note: See TracBrowser for help on using the repository browser.