source: src/joint/Joint.ma @ 1233

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

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

File size: 3.7 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 { 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]
14 
15 ; extend_statements: Type[0]
16 
17 ; resultT: Type[0]
18 ; localsT: Type[0]
19 ; paramsT: Type[0]
20 }.
21
22record params: Type[1] ≝
23 { pars_:> params_
24 ; succ: Type[0]
25 }.
26
27inductive joint_instruction (p:params_) (globals: list ident): Type[0] ≝
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
43  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
44
45inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
46  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
47  | joint_st_goto: label → joint_statement p globals
48  | joint_st_return: joint_statement p globals
49  | joint_st_extension: extend_statements p → joint_statement p globals.
50
51record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
52{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
53  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
54(*  joint_if_sig: signature;  -- dropped in front end *)
55  joint_if_result   : resultT p;
56  joint_if_params   : paramsT p;
57  joint_if_locals   : localsT p;
58  joint_if_stacksize: nat;
59  joint_if_lookup   : label → option (joint_statement p globals);
60  joint_if_entry    : Σl: label. joint_if_lookup l ≠ None ?;
61  joint_if_exit     : Σl: label. joint_if_lookup l ≠ None ?
62}.
63
64definition set_luniverse ≝
65  λp:params.
66  λglobals  : list ident.
67  λint_fun  : joint_internal_function p globals.
68  λluniverse: universe LabelTag.
69  let runiverse ≝ joint_if_runiverse … int_fun in
70  let params    ≝ joint_if_params … int_fun in
71  let locals    ≝ joint_if_locals … int_fun in
72  let result    ≝ joint_if_result … int_fun in
73  let stacksize ≝ joint_if_stacksize … int_fun in
74  let lookup    ≝ joint_if_lookup … int_fun in
75  let entry     ≝ joint_if_entry … int_fun in
76  let exit      ≝ joint_if_exit … int_fun in
77    mk_joint_internal_function … globals
78      luniverse runiverse result params locals
79      stacksize lookup entry exit.
80
81definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
82
83definition joint_program ≝ λp:params. program (joint_function p) nat.
84
85(****************************************************************************)
86
87(* Used in LTL and LIN *) 
88inductive registers_move: Type[0] ≝
89 | from_acc: Register → registers_move
90 | to_acc: Register → registers_move.
Note: See TracBrowser for help on using the repository browser.