- Timestamp:
- Sep 22, 2011, 2:50:44 AM (9 years ago)
- Location:
- src/joint
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/Joint.ma
r1245 r1246 5 5 include "common/Graphs.ma". 6 6 7 record params_ : Type[1] ≝7 record params__: Type[1] ≝ 8 8 { acc_a_reg: Type[0] 9 9 ; acc_b_reg: Type[0] … … 20 20 }. 21 21 22 record params : Type[1] ≝23 { pars_ :> params_22 record params_: Type[1] ≝ 23 { pars__:> params__ 24 24 ; succ: Type[0] 25 25 }. 26 26 27 inductive joint_instruction (p:params_ ) (globals: list ident): Type[0] ≝27 inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝ 28 28 | joint_instr_comment: String → joint_instruction p globals 29 29 | joint_instr_cost_label: costlabel → joint_instruction p globals … … 43 43 | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals. 44 44 45 inductive joint_statement (p:params ) (globals: list ident): Type[0] ≝45 inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝ 46 46 | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals 47 47 | joint_st_goto: label → joint_statement p globals … … 49 49 | joint_st_extension: extend_statements p → joint_statement p globals. 50 50 51 record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝ 51 record params (globals: list ident): Type[1] ≝ 52 { pars_:> params_ 53 ; codeT: Type[0] 54 ; lookup: codeT → label → option (joint_statement pars_ globals) 55 }. 56 57 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝ 52 58 { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) 53 59 joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*) … … 58 64 (*CSC: XXXXX stacksize unused for LTL-...*) 59 65 joint_if_stacksize: nat; 60 joint_if_ lookup : label → option (joint_statement p globals);66 joint_if_code : codeT … p; 61 67 (*CSC: XXXXX entry unused for LIN, but invariant in that case... *) 62 joint_if_entry : Σl: label. joint_if_lookupl ≠ None ?;68 joint_if_entry : Σl: label. lookup … joint_if_code l ≠ None ?; 63 69 (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *) 64 joint_if_exit : Σl: label. joint_if_lookupl ≠ None ?70 joint_if_exit : Σl: label. lookup … joint_if_code l ≠ None ? 65 71 }. 66 72 … … 70 76 λexit: label. 71 77 λp: joint_internal_function pars globals. 72 λprf: joint_if_lookup … pexit ≠ None ?.78 λprf: lookup … (joint_if_code … p) exit ≠ None ?. 73 79 mk_joint_internal_function pars globals 74 80 (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) 75 81 (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) 76 (joint_if_lookup … p) (joint_if_entry … p) (dp … exit prf). 77 82 (joint_if_code … p) (joint_if_entry … p) (dp … exit prf). 78 83 79 84 definition set_luniverse ≝ 80 λp:params.81 85 λglobals : list ident. 82 λint_fun : joint_internal_function p globals. 86 λp:params globals. 87 λint_fun : joint_internal_function globals p. 83 88 λluniverse: universe LabelTag. 84 89 let runiverse ≝ joint_if_runiverse … int_fun in … … 87 92 let result ≝ joint_if_result … int_fun in 88 93 let stacksize ≝ joint_if_stacksize … int_fun in 89 let lookup ≝ joint_if_lookup… int_fun in94 let code ≝ joint_if_code … int_fun in 90 95 let entry ≝ joint_if_entry … int_fun in 91 96 let exit ≝ joint_if_exit … int_fun in 92 mk_joint_internal_function … globals97 mk_joint_internal_function globals p 93 98 luniverse runiverse result params locals 94 stacksize lookupentry exit.99 stacksize code entry exit. 95 100 96 101 definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals). 97 102 98 definition joint_program ≝ λp:params. program (joint_function p) nat. 103 definition joint_program ≝ 104 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat. 99 105 100 106 (****************************************************************************) -
src/joint/semantics.ma
r1233 r1246 206 206 axiom BadFunction : String. 207 207 208 (*CSC: move elsewhere *)208 (*CSC: move elsewhere, also in LIN.ma *) 209 209 definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝ 210 210 λA,P,c. match c with [ dp w _ ⇒ w ].
Note: See TracChangeset
for help on using the changeset viewer.