- Timestamp:
- Apr 18, 2011, 12:30:53 PM (10 years ago)
- Location:
- src
- Files:
-
- 15 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASM.ma
r722 r757 22 22 | ADDR16: Word → addressing_mode. 23 23 24 (* dpm: renamed register to registr to avoid clash with brian's types *) 24 25 inductive addressing_mode_tag : Type[0] ≝ 25 26 direct: addressing_mode_tag 26 27 | indirect: addressing_mode_tag 27 28 | ext_indirect: addressing_mode_tag 28 | regist er: addressing_mode_tag29 | registr: addressing_mode_tag 29 30 | acc_a: addressing_mode_tag 30 31 | acc_b: addressing_mode_tag … … 49 50 | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ] 50 51 | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ] 51 | regist er ⇒ match b with [ register ⇒ true | _ ⇒ false ]52 | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ] 52 53 | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ] 53 54 | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ] … … 73 74 | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ] 74 75 | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ] 75 | regist er ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]76 | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ] 76 77 | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ] 77 78 | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ] … … 120 121 | JNZ: A → jump A 121 122 | CJNE: 122 [[acc_a]] × [[direct; data]] ⊎ [[regist er; indirect]] × [[data]] → A → jump A123 | DJNZ: [[regist er ; direct]] → A → jump A.123 [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → jump A 124 | DJNZ: [[registr ; direct]] → A → jump A. 124 125 125 126 inductive preinstruction (A: Type[0]) : Type[0] ≝ 126 ADD: [[acc_a]] → [[ regist er ; direct ; indirect ; data ]] → preinstruction A127 | ADDC: [[acc_a]] → [[ regist er ; direct ; indirect ; data ]] → preinstruction A128 | SUBB: [[acc_a]] → [[ regist er ; direct ; indirect ; data ]] → preinstruction A129 | INC: [[ acc_a ; regist er ; direct ; indirect ; dptr ]] → preinstruction A130 | DEC: [[ acc_a ; regist er ; direct ; indirect ]] → preinstruction A127 ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A 128 | ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A 129 | SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A 130 | INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A 131 | DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A 131 132 | MUL: [[acc_a]] → [[acc_b]] → preinstruction A 132 133 | DIV: [[acc_a]] → [[acc_b]] → preinstruction A … … 135 136 (* logical operations *) 136 137 | ANL: 137 [[acc_a]] × [[ regist er ; direct ; indirect ; data ]] ⊎138 [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎ 138 139 [[direct]] × [[ acc_a ; data ]] ⊎ 139 140 [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A 140 141 | ORL: 141 [[acc_a]] × [[ regist er ; data ; direct ; indirect ]] ⊎142 [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎ 142 143 [[direct]] × [[ acc_a ; data ]] ⊎ 143 144 [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A 144 145 | XRL: 145 [[acc_a]] × [[ data ; regist er ; direct ; indirect ]] ⊎146 [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎ 146 147 [[direct]] × [[ acc_a ; data ]] → preinstruction A 147 148 | CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A … … 155 156 (* data transfer *) 156 157 | MOV: 157 [[acc_a]] × [[ regist er ; direct ; indirect ; data ]] ⊎158 [[ regist er ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎159 [[direct]] × [[ acc_a ; regist er ; direct ; indirect ; data ]] ⊎158 [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎ 159 [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎ 160 [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎ 160 161 [[dptr]] × [[data16]] ⊎ 161 162 [[carry]] × [[bit_addr]] ⊎ … … 168 169 | PUSH: [[direct]] → preinstruction A 169 170 | POP: [[direct]] → preinstruction A 170 | XCH: [[acc_a]] → [[ regist er ; direct ; indirect ]] → preinstruction A171 | XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A 171 172 | XCHD: [[acc_a]] → [[indirect]] → preinstruction A 172 173 -
src/ASM/Assembly.ma
r719 r757 15 15 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 16 16 | ADD addr1 addr2 ⇒ 17 match addr2 return λx. bool_to_Prop (is_in ? [[regist er;direct;indirect;data]] x) → ? with17 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 18 18 [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ] 19 19 | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ] … … 22 22 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 23 23 | ADDC addr1 addr2 ⇒ 24 match addr2 return λx. bool_to_Prop (is_in ? [[regist er;direct;indirect;data]] x) → ? with24 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 25 25 [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ] 26 26 | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ] … … 38 38 [ inl addrs ⇒ match addrs with 39 39 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 40 match addr2 return λx. bool_to_Prop (is_in ? [[regist er;direct;indirect;data]] x) → ? with40 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 41 41 [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ] 42 42 | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ] … … 80 80 [ ([[true; true; false; true; false; true; false; false]]) ] 81 81 | DEC addr ⇒ 82 match addr return λx. bool_to_Prop (is_in ? [[acc_a;regist er;direct;indirect]] x) → ? with82 match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with 83 83 [ ACC_A ⇒ λ_. 84 84 [ ([[false; false; false; true; false; true; false; false]]) ] … … 99 99 [ RELATIVE b2 ⇒ λ_. b2 100 100 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 101 match addr1 return λx. bool_to_Prop (is_in ? [[regist er;direct]] x) → ? with101 match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with 102 102 [ REGISTER r ⇒ λ_. 103 103 [ ([[true; true; false; true; true]]) @@ r ; b2 ] … … 170 170 [ DATA b2 ⇒ λ_. b2 171 171 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 172 match addr1 return λx. bool_to_Prop (is_in ? [[regist er;indirect]] x) → list Byte with172 match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with 173 173 [ REGISTER r⇒ λ_. 174 174 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ] … … 177 177 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]] 178 178 | INC addr ⇒ 179 match addr return λx. bool_to_Prop (is_in ? [[acc_a;regist er;direct;indirect;dptr]] x) → ? with179 match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with 180 180 [ ACC_A ⇒ λ_. 181 181 [ ([[false;false;false;false;false;true;false;false]]) ] … … 214 214 match addrs with 215 215 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 216 match addr2 return λx. bool_to_Prop (is_in ? [[regist er;direct;indirect;data]] x) → ? with216 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 217 217 [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ] 218 218 | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ] … … 221 221 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 222 222 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 223 match addr1 return λx. bool_to_Prop (is_in ? [[regist er;indirect]] x) → ? with223 match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with 224 224 [ REGISTER r ⇒ λ_. 225 225 match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with … … 240 240 [ DIRECT b1 ⇒ λ_. b1 241 241 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in 242 match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;regist er;direct;indirect;data]] x) → ? with242 match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with 243 243 [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1] 244 244 | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ] … … 295 295 match addrs with 296 296 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 297 match addr2 return λx. bool_to_Prop (is_in ? [[regist er;data;direct;indirect]] x) → ? with297 match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with 298 298 [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ] 299 299 | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ] … … 354 354 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 355 355 | SUBB addr1 addr2 ⇒ 356 match addr2 return λx. bool_to_Prop (is_in ? [[regist er;direct;indirect;data]] x) → ? with356 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with 357 357 [ REGISTER r ⇒ λ_. 358 358 [ ([[true;false;false;true;true]]) @@ r ] … … 367 367 [ ([[true;true;false;false;false;true;false;false]]) ] 368 368 | XCH addr1 addr2 ⇒ 369 match addr2 return λx. bool_to_Prop (is_in ? [[regist er;direct;indirect]] x) → ? with369 match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with 370 370 [ REGISTER r ⇒ λ_. 371 371 [ ([[true;true;false;false;true]]) @@ r ] … … 383 383 match addrs with 384 384 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 385 match addr2 return λx. bool_to_Prop (is_in ? [[data;regist er;direct;indirect]] x) → ? with385 match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with 386 386 [ REGISTER r ⇒ λ_. 387 387 [ ([[false;true;true;false;true]]) @@ r ] -
src/ASM/I8051.ma
r746 r757 140 140 definition RegisterSPH ≝ Register07. 141 141 142 definition register_address: Register → [[ acc_a; direct; regist er ]] ≝142 definition register_address: Register → [[ acc_a; direct; registr ]] ≝ 143 143 λr: Register. 144 144 match r with -
src/ASM/Interpret.ma
r712 r757 156 156 157 157 include alias "arithmetics/nat.ma". 158 include alias "ASM/BitVectorTrie.ma". 158 159 159 160 definition execute_1: Status → Status ≝ … … 172 173 let ov_flag ≝ get_index' ? 2 ? flags in 173 174 let s ≝ set_arg_8 s ACC_A result in 174 set_flags s cy_flag (Some Bit ac_flag) ov_flag 175 set_flags s cy_flag (Some Bit ac_flag) ov_flag 175 176 | ADDC addr1 addr2 ⇒ 176 177 let old_cy_flag ≝ get_cy_flag s in … … 240 241 | INC addr ⇒ 241 242 match addr return λx. bool_to_Prop (is_in … [[ acc_a; 242 regist er;243 registr; 243 244 direct; 244 245 indirect; … … 427 428 | _ ⇒ λother: False. ⊥ 428 429 ] (subaddressing_modein … addr) 429 | MOVC addr1 addr2 ⇒430 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with431 [ ACC_DPTR ⇒ λacc_dptr: True.432 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in433 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in434 let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in435 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in436 set_8051_sfr s SFR_ACC_A result437 | ACC_PC ⇒ λacc_pc: True.438 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in439 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in440 (* DPM: Under specified: does the carry from PC incrementation affect the *)441 (* addition of the PC with the DPTR? At the moment, no. *)442 let s ≝ set_program_counter s inc_pc in443 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in444 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in445 set_8051_sfr s SFR_ACC_A result446 | _ ⇒ λother: False. ⊥447 ] (subaddressing_modein … addr2)448 430 | MOVX addr ⇒ 449 431 (* DPM: only copies --- doesn't affect I/O *) … … 631 613 ] (subaddressing_modein … addr2) 632 614 ] 615 | MOVC addr1 addr2 ⇒ 616 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → ? with 617 [ ACC_DPTR ⇒ λacc_dptr: True. 618 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in 619 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 620 let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in 621 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in 622 set_8051_sfr s SFR_ACC_A result 623 | ACC_PC ⇒ λacc_pc: True. 624 let big_acc ≝ (zero 8) @@ (get_8051_sfr s SFR_ACC_A) in 625 let 〈carry,inc_pc〉 ≝ half_add ? (program_counter s) (bitvector_of_nat 16 1) in 626 (* DPM: Under specified: does the carry from PC incrementation affect the *) 627 (* addition of the PC with the DPTR? At the moment, no. *) 628 let s ≝ set_program_counter s inc_pc in 629 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in 630 let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in 631 set_8051_sfr s SFR_ACC_A result 632 | _ ⇒ λother: False. ⊥ 633 ] (subaddressing_modein … addr2) 633 634 | NOP ⇒ s 634 635 ] -
src/ASM/Status.ma
r705 r757 755 755 ] (subaddressing_modein … a). 756 756 757 definition get_arg_8: Status → bool → [[ direct ; indirect ; regist er ;757 definition get_arg_8: Status → bool → [[ direct ; indirect ; registr ; 758 758 acc_a ; acc_b ; data ; acc_dptr ; 759 759 acc_pc ; ext_indirect ; 760 760 ext_indirect_dptr ]] → Byte ≝ 761 761 λs, l, a. 762 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; regist er ;762 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 763 763 acc_a ; acc_b ; data ; acc_dptr ; 764 764 acc_pc ; ext_indirect ; … … 820 820 qed. 821 821 822 definition set_arg_8: Status → [[ direct ; indirect ; regist er ;822 definition set_arg_8: Status → [[ direct ; indirect ; registr ; 823 823 acc_a ; acc_b ; ext_indirect ; 824 824 ext_indirect_dptr ]] → Byte → Status ≝ 825 825 λs, a, v. 826 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; regist er ;826 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 827 827 acc_a ; acc_b ; ext_indirect ; 828 828 ext_indirect_dptr ]] x) → ? with -
src/ERTL/ERTLToLTL.ma
r753 r757 3 3 4 4 axiom translate_ERTL_func: 5 ∀globals: list Identifier.6 list ( Identifier × ERTLFunction) → list (Identifier × (LTLFunctionDefinition globals)).5 ∀globals: list ident. 6 list (ident × ertl_function) → list (ident × (ltl_function_definition globals)). 7 7 8 definition translate: ∀e: ERTLProgram. LTLProgram (ERTL_Pr_Vars e) ≝8 definition translate: ∀e: ertl_program. ltl_program (ertl_pr_vars e) ≝ 9 9 λp. 10 let globals ≝ map ? ? \fst ( ERTL_Pr_Vars p) in11 let ltl_pr_funcs ≝ map ? ? ? ( ERTL_Pr_Funcs p) in12 mk_ LTLProgram (ERTL_Pr_Vars p) ltl_pr_funcs (ERTL_Pr_Main p).10 let globals ≝ map ? ? \fst (ertl_pr_vars p) in 11 let ltl_pr_funcs ≝ map ? ? ? (ertl_pr_funcs p) in 12 mk_ltl_program (ertl_pr_vars p) ltl_pr_funcs (ertl_pr_main p). 13 13 # H1 14 @ (translate_ ERTL_func globals) in ⊢ (? × %) (* dpm here *)14 @ (translate_ertl_func globals) in ⊢ (? × %) (* dpm here *) -
src/LIN/JointLTLLIN.ma
r733 r757 1 1 include "ASM/String.ma". 2 2 include "ASM/I8051.ma". 3 include "common/CostLabel.ma". 3 4 include "common/AST.ma". 5 include "common/Registers.ma". 4 6 5 inductive JointInstruction (globals: list Identifier): Type[0] ≝6 | Joint_Instr_Comment: String → JointInstruction globals7 | Joint_Instr_CostLabel: Identifier → JointInstruction globals8 | Joint_Instr_Int: Register → Byte → JointInstruction globals9 | Joint_Instr_Pop: JointInstruction globals10 | Joint_Instr_Push: JointInstruction globals11 | Joint_Instr_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → JointInstruction globals12 | Joint_Instr_FromAcc: Register → JointInstruction globals13 | Joint_Instr_ToAcc: Register → JointInstruction globals14 | Joint_Instr_OpAccs: OpAccs → JointInstruction globals15 | Joint_Instr_Op1: Op1 → JointInstruction globals16 | Joint_Instr_Op2: Op2 → Register → JointInstruction globals17 | Joint_Instr_ClearCarry: JointInstruction globals18 | Joint_Instr_Load: JointInstruction globals19 | Joint_Instr_Store: JointInstruction globals20 | Joint_Instr_CallId: Identifier → JointInstruction globals21 | Joint_Instr_CondAcc: Identifier → JointInstruction globals.7 inductive joint_instruction (globals: list ident): Type[0] ≝ 8 | joint_instr_comment: String → joint_instruction globals 9 | joint_instr_cost_label: costlabel → joint_instruction globals 10 | joint_instr_int: register → Byte → joint_instruction globals 11 | joint_instr_pop: joint_instruction globals 12 | joint_instr_push: joint_instruction globals 13 | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → joint_instruction globals 14 | joint_instr_from_acc: register → joint_instruction globals 15 | joint_instr_to_acc: register → joint_instruction globals 16 | joint_instr_opaccs: OpAccs → joint_instruction globals 17 | joint_instr_op1: Op1 → joint_instruction globals 18 | joint_instr_op2: Op2 → register → joint_instruction globals 19 | joint_instr_clear_carry: joint_instruction globals 20 | joint_instr_load: joint_instruction globals 21 | joint_instr_store: joint_instruction globals 22 | joint_instr_call_id: ident → joint_instruction globals 23 | joint_instr_cond_acc: ident → joint_instruction globals. 22 24 23 inductive JointStatement (A: Type[0]) (globals: list Identifier): Type[0] ≝24 | Joint_St_Sequential: JointInstruction globals → A → JointStatement A globals25 | Joint_St_Goto: Identifier → JointStatement A globals26 | Joint_St_Return: JointStatement A globals.25 inductive joint_statement (A: Type[0]) (globals: list ident): Type[0] ≝ 26 | joint_st_sequential: joint_instruction globals → A → joint_statement A globals 27 | joint_st_goto: ident → joint_statement A globals 28 | joint_st_return: joint_statement A globals. -
src/LIN/LIN.ma
r723 r757 1 1 include "LIN/JointLTLLIN.ma". 2 2 3 definition PreLINStatement ≝ JointStatement unit.3 definition pre_lin_statement ≝ joint_statement unit. 4 4 5 definition LINStatement ≝5 definition lin_statement ≝ 6 6 λglobals. 7 option Identifier × (PreLINStatement globals).7 option ident × (pre_lin_statement globals). 8 8 9 definition WellFormedP ≝9 definition well_formed_P ≝ 10 10 λA, B: Type[0]. 11 11 λcode: list (option A × B). … … 19 19 ]. 20 20 21 inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝22 LIN_Fu_Internal: ∀code: list (LINStatement globals). WellFormedP ? ? code → LINFunctionDefinition globals23 | LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.21 inductive lin_function_definition (globals: list ident): Type[0] ≝ 22 lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals 23 | lin_fu_external: external_function → lin_function_definition globals. 24 24 25 record LINProgram: Type[0] ≝25 record lin_program: Type[0] ≝ 26 26 { 27 LIN_Pr_vars: list (Identifier× nat);28 LIN_Pr_funs: list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) LIN_Pr_vars)));29 LIN_Pr_main: option Identifier27 lin_pr_vars: list (ident × nat); 28 lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars))); 29 lin_pr_main: option ident 30 30 }. 31 31 32 definition LIN_Pr_vars:33 LINProgram → list (Identifier× nat).32 definition lin_pr_vars: 33 lin_program → list (ident × nat). 34 34 # r 35 35 cases r … … 38 38 qed. 39 39 40 definition LIN_Pr_funs:41 ∀p: LINProgram.42 list ( Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) (LIN_Pr_vars p)))).40 definition lin_pr_funcs: 41 ∀p: lin_program. 42 list (ident × (lin_function_definition (map ? ? (fst ? ?) (lin_pr_vars p)))). 43 43 # r 44 44 cases r -
src/LIN/LINToASM.ma
r734 r757 4 4 include "LIN/LIN.ma". 5 5 6 let rec association (i: Identifier) (l: list (Identifier× nat))7 on l: member i (eq_ bv?) (map ? ? (fst ? ?) l) → nat ≝8 match l return λl. member i (eq_ bv?) (map ? ? (fst ? ?) l) → nat with6 let rec association (i: ident) (l: list (ident × nat)) 7 on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝ 8 match l return λl. member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat with 9 9 [ nil ⇒ λabsd. ? 10 10 | cons hd tl ⇒ 11 λprf: member i (eq_ bv?) (map ? ? (fst ? ?) (cons ? hd tl)).12 (match eq_ bv ? (\fst hd) i return λb. eq_bv? (\fst hd) i = b → nat with11 λprf: member i (eq_identifier ?) (map ? ? (fst ? ?) (cons ? hd tl)). 12 (match eq_identifier ? (\fst hd) i return λb. eq_identifier ? (\fst hd) i = b → nat with 13 13 [ true ⇒ λeq_prf. \snd hd 14 14 | false ⇒ λeq_prf. association i tl ? 15 ]) (refl ? (eq_ bv? (\fst hd) i))15 ]) (refl ? (eq_identifier ? (\fst hd) i)) 16 16 ]. 17 17 [ cases absd … … 27 27 28 28 definition statement_labels ≝ 29 λg: list Identifier.30 λs: LINStatement g.29 λg: list ident. 30 λs: lin_statement g. 31 31 let 〈label, instr〉 ≝ s in 32 32 let generated ≝ 33 33 match instr with 34 [ Joint_St_Sequential instr' _ ⇒34 [ joint_st_sequential instr' _ ⇒ 35 35 match instr' with 36 [ Joint_Instr_CostLabel lbl ⇒ set_insert ? lbl(set_empty ?)37 | Joint_Instr_CondAcc lbl ⇒ set_insert ? lbl(set_empty ?)36 [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) 37 | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) 38 38 | _ ⇒ set_empty ? 39 39 ] 40 | Joint_St_Goto lbl ⇒ set_insert ? lbl(set_empty ?)41 | Joint_St_Return ⇒ set_empty ?40 | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) 41 | joint_st_return ⇒ set_empty ? 42 42 ] in 43 43 match label with 44 44 [ None ⇒ generated 45 | Some lbl ⇒ set_insert ? lblgenerated45 | Some lbl ⇒ set_insert ? (word_of_identifier ? lbl) generated 46 46 ]. 47 47 48 48 definition function_labels_internal ≝ 49 λglobals: list Identifier.49 λglobals: list ident. 50 50 λlabels: BitVectorTrieSet ?. 51 λstatement: LINStatement globals.51 λstatement: lin_statement globals. 52 52 set_union ? labels (statement_labels globals statement). 53 53 … … 55 55 definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝ 56 56 λA: Type[0]. 57 λglobals: list Identifier.58 λf: A × ( LINFunctionDefinition globals).57 λglobals: list ident. 58 λf: A × (lin_function_definition globals). 59 59 let 〈ignore, fun_def〉 ≝ f in 60 60 match fun_def return λ_. BitVectorTrieSet ? with 61 [ LIN_Fu_Internal stmts proof ⇒61 [ lin_fu_internal stmts proof ⇒ 62 62 foldl ? ? (function_labels_internal globals) (set_empty ?) stmts 63 | LIN_Fu_External _ ⇒ set_empty ?63 | lin_fu_external _ ⇒ set_empty ? 64 64 ]. 65 65 66 66 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet ? ≝ 67 67 λA: Type[0]. 68 λglobals: list Identifier.68 λglobals: list ident. 69 69 λlabels: BitVectorTrieSet ?. 70 λfunct: A × ( LINFunctionDefinition globals).70 λfunct: A × (lin_function_definition globals). 71 71 set_union ? labels (function_labels ? globals funct). 72 72 73 73 definition program_labels ≝ 74 74 λprogram. 75 foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) ( LIN_Pr_vars program)))76 (set_empty ?) ( LIN_Pr_funs program).75 foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program))) 76 (set_empty ?) (lin_pr_funcs program). 77 77 78 78 definition data_of_int ≝ λbv. DATA bv. … … 83 83 84 84 definition translate_statements ≝ 85 λglobals: list ( Identifier× nat).86 λglobals_old: list Identifier.87 λprf: ∀i: Identifier. member i (eq_bv ?) globals_old → member i (eq_bv?) (map ? ? (fst ? ?) globals).88 λstatement: PreLINStatement globals_old.85 λglobals: list (ident × nat). 86 λglobals_old: list ident. 87 λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals). 88 λstatement: pre_lin_statement globals_old. 89 89 match statement with 90 [ Joint_St_Return ⇒ Instruction (RET ?)91 | Joint_St_Goto lbl ⇒ Jmp lbl92 | Joint_St_Sequential instr _ ⇒90 [ joint_st_return ⇒ Instruction (RET ?) 91 | joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl) 92 | joint_st_sequential instr _ ⇒ 93 93 match instr with 94 [ Joint_Instr_Comment comment ⇒ Comment comment95 | Joint_Instr_CostLabel lbl ⇒ Cost lbl96 | Joint_Instr_Pop ⇒ Instruction (POP ? accumulator_address)97 | Joint_Instr_Push ⇒ Instruction (PUSH ? accumulator_address)98 | Joint_Instr_ClearCarry ⇒ Instruction (CLR ? CARRY)99 | Joint_Instr_CallId f ⇒ Call f100 | Joint_Instr_OpAccs accs ⇒94 [ joint_instr_comment comment ⇒ Comment comment 95 | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl) 96 | joint_instr_pop ⇒ Instruction (POP ? accumulator_address) 97 | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address) 98 | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY) 99 | joint_instr_call_id f ⇒ Call (word_of_identifier ? f) 100 | joint_instr_opaccs accs ⇒ 101 101 match accs with 102 102 [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B) … … 104 104 | Modu ⇒ ? 105 105 ] 106 | Joint_Instr_Op1 op1 ⇒106 | joint_instr_op1 op1 ⇒ 107 107 match op1 with 108 108 [ Cmpl ⇒ Instruction (CPL ? ACC_A) 109 109 | Inc ⇒ Instruction (INC ? ACC_A) 110 110 ] 111 | Joint_Instr_Op2 op2 reg ⇒111 | joint_instr_op2 op2 reg ⇒ 112 112 match op2 with 113 113 [ Add ⇒ 114 let reg' ≝ register_address regin115 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 116 direct; 117 regist er ]] x) → ? with114 let reg' ≝ register_address (Register_of_register reg) in 115 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 116 direct; 117 registr ]] x) → ? with 118 118 [ ACC_A ⇒ λacc_a: True. 119 119 Instruction (ADD ? ACC_A accumulator_address) … … 125 125 ] (subaddressing_modein … reg') 126 126 | Addc ⇒ 127 let reg' ≝ register_address regin128 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 129 direct; 130 regist er ]] x) → ? with127 let reg' ≝ register_address (Register_of_register reg) in 128 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 129 direct; 130 registr ]] x) → ? with 131 131 [ ACC_A ⇒ λacc_a: True. 132 132 Instruction (ADDC ? ACC_A accumulator_address) … … 138 138 ] (subaddressing_modein … reg') 139 139 | Sub ⇒ 140 let reg' ≝ register_address regin141 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 142 direct; 143 regist er ]] x) → ? with140 let reg' ≝ register_address (Register_of_register reg) in 141 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 142 direct; 143 registr ]] x) → ? with 144 144 [ ACC_A ⇒ λacc_a: True. 145 145 Instruction (SUBB ? ACC_A accumulator_address) … … 151 151 ] (subaddressing_modein … reg') 152 152 | And ⇒ 153 let reg' ≝ register_address regin154 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 155 direct; 156 regist er ]] x) → ? with153 let reg' ≝ register_address (Register_of_register reg) in 154 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 155 direct; 156 registr ]] x) → ? with 157 157 [ ACC_A ⇒ λacc_a: True. 158 158 Instruction (NOP ?) … … 164 164 ] (subaddressing_modein … reg') 165 165 | Or ⇒ 166 let reg' ≝ register_address regin167 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 168 direct; 169 regist er ]] x) → ? with166 let reg' ≝ register_address (Register_of_register reg) in 167 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 168 direct; 169 registr ]] x) → ? with 170 170 [ ACC_A ⇒ λacc_a: True. 171 171 Instruction (NOP ?) … … 177 177 ] (subaddressing_modein … reg') 178 178 | Xor ⇒ 179 let reg' ≝ register_address regin180 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 181 direct; 182 regist er ]] x) → ? with179 let reg' ≝ register_address (Register_of_register reg) in 180 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 181 direct; 182 registr ]] x) → ? with 183 183 [ ACC_A ⇒ λacc_a: True. 184 184 Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) … … 190 190 ] (subaddressing_modein … reg') 191 191 ] 192 | Joint_Instr_Int reg byte ⇒193 let reg' ≝ register_address regin194 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 195 direct; 196 regist er ]] x) → ? with192 | joint_instr_int reg byte ⇒ 193 let reg' ≝ register_address (Register_of_register reg) in 194 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 195 direct; 196 registr ]] x) → ? with 197 197 [ REGISTER r ⇒ λregister7: True. 198 198 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) … … 203 203 | _ ⇒ λother: False. ⊥ 204 204 ] (subaddressing_modein … reg') 205 | Joint_Instr_FromAcc reg ⇒206 let reg' ≝ register_address regin207 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 208 direct; 209 regist er ]] x) → ? with205 | joint_instr_from_acc reg ⇒ 206 let reg' ≝ register_address (Register_of_register reg) in 207 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 208 direct; 209 registr ]] x) → ? with 210 210 [ REGISTER r ⇒ λregister8: True. 211 211 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) … … 216 216 | _ ⇒ λother: False. ⊥ 217 217 ] (subaddressing_modein … reg') 218 | Joint_Instr_ToAcc reg ⇒219 let reg' ≝ register_address regin220 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 221 direct; 222 regist er ]] x) → ? with218 | joint_instr_to_acc reg ⇒ 219 let reg' ≝ register_address (Register_of_register reg) in 220 match reg' return λx. bool_to_Prop (is_in … [[ acc_a; 221 direct; 222 registr ]] x) → ? with 223 223 [ REGISTER r ⇒ λregister9: True. 224 224 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) … … 229 229 | _ ⇒ λother: False. ⊥ 230 230 ] (subaddressing_modein … reg') 231 | Joint_Instr_Load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))232 | Joint_Instr_Store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))233 | Joint_Instr_Address addr proof ⇒231 | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) 232 | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) 233 | joint_instr_address addr proof ⇒ 234 234 let look ≝ association addr globals (prf ? proof) in 235 235 Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) 236 | Joint_Instr_CondAcc lbl ⇒236 | joint_instr_cond_acc lbl ⇒ 237 237 (* dpm: this should be handled in translate_code! *) 238 WithLabel (JNZ ? lbl)238 WithLabel (JNZ ? (word_of_identifier ? lbl)) 239 239 ] 240 240 ]. … … 248 248 λglobals_old. 249 249 λprf. 250 λstatement: LINStatement globals_old.250 λstatement: lin_statement globals_old. 251 251 〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉. 252 252 253 253 definition translate_code ≝ 254 λglobals: list ( Identifier× nat).255 λglobals_old: list Identifier.254 λglobals: list (ident × nat). 255 λglobals_old: list ident. 256 256 λprf. 257 λcode: list ( LINStatement globals_old).257 λcode: list (lin_statement globals_old). 258 258 map ? ? (build_translated_statement globals globals_old prf) code. 259 259 260 260 lemma translate_code_preserves_WellFormedP: 261 261 ∀globals, globals_old, prf, code. 262 WellFormedP ? ? code → WellFormedP ? ? (translate_code globals globals_old prf code).262 well_formed_P ? ? code → well_formed_P ? ? (translate_code globals globals_old prf code). 263 263 #G #GO #P #C 264 264 elim C … … 279 279 let 〈id, def〉 ≝ id_def in 280 280 match def with 281 [ LIN_Fu_Internal code proof ⇒282 match translate_code globals globals_old prf code return λtranscode. WellFormedP ? ? transcode → list labelled_instruction with281 [ lin_fu_internal code proof ⇒ 282 match translate_code globals globals_old prf code return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with 283 283 [ nil ⇒ λprf2. ⊥ 284 | cons hd tl ⇒ λ_. 〈Some ? id, \snd hd〉 :: tl 284 | cons hd tl ⇒ λ_. 285 let rest ≝ 〈Some ? id, \snd hd〉 :: tl in 286 map ? ? ( 287 λr. 288 match fst ? ? r with 289 [ Some id' ⇒ 〈Some ? (word_of_identifier ? id'), snd ? ? r〉 290 | None ⇒ 〈None ?, \snd r〉 291 ]) rest 285 292 ] (translate_code_preserves_WellFormedP globals globals_old prf code proof) 286 293 | _ ⇒ [ ] -
src/LTL/LTL.ma
r753 r757 1 1 include "common/Graphs.ma". 2 2 include "utilities/IdentifierTools.ma". 3 4 3 include "LIN/LIN.ma". 5 4 6 definition LTLStatement ≝ JointStatement Identifier.5 definition ltl_statement ≝ joint_statement ident. 7 6 8 definition LTLStatementGraph ≝ λglobals. graph (LTLStatement globals).7 definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals). 9 8 10 record LTLInternalFunction (globals: list Identifier): Type[0] ≝9 record ltl_internal_function (globals: list ident): Type[0] ≝ 11 10 { 12 LTL_IF_LUniverse: Universe; 13 LTL_IF_StackSize: nat; 14 LTL_IF_Graph: LTLStatementGraph globals; 15 LTL_IF_Entry: label; 16 LTL_IF_Exit: label 11 ltl_if_luniverse: universe LabelTag; 12 ltl_if_runiverse: universe RegisterTag; 13 ltl_if_StackSize: nat; 14 ltl_if_Graph: ltl_statement_graph globals; 15 ltl_if_Entry: label; 16 ltl_if_Exit: label 17 17 }. 18 18 19 inductive LTLFunctionDefinition (globals: list Identifier): Type[0] ≝20 | LTL_Fu_InternalFunction: LTLInternalFunction globals → LTLFunctionDefinition globals21 | LTL_Fu_ExternalFunction: ExternalFunction → LTLFunctionDefinition globals.19 inductive ltl_function_definition (globals: list ident): Type[0] ≝ 20 | ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals 21 | ltl_fu_external_function: external_function → ltl_function_definition globals. 22 22 23 record LTLProgram (globals: list (Identifier× nat)): Type[0] ≝23 record ltl_program (globals: list (ident × nat)): Type[0] ≝ 24 24 { 25 LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition (map ? ? \fst globals)));26 LTL_Pr_Main: option Identifier25 ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals))); 26 ltl_pr_main: option ident 27 27 }. -
src/LTL/LTLToLIN.ma
r753 r757 6 6 axiom LTLTag: String. 7 7 8 definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝9 λglobals: list Identifier.10 λs: LTLStatement globals.8 definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝ 9 λglobals: list ident. 10 λs: ltl_statement globals. 11 11 match s with 12 [ Joint_St_Return ⇒ Joint_St_Return ? globals13 | Joint_St_Sequential instr _ ⇒ Joint_St_Sequential ? globals instr it14 | Joint_St_Goto lbl ⇒ Joint_St_Goto ? globals lbl12 [ joint_st_return ⇒ joint_st_return ? globals 13 | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it 14 | joint_st_goto lbl ⇒ joint_st_goto ? globals lbl 15 15 ]. 16 16 17 definition require: Identifier→ BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝18 λl: Identifier.17 definition require: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ 18 λl: ident. 19 19 λg: BitVectorTrieSet 16. 20 20 set_insert ? l g. 21 21 22 definition mark: Identifier→ BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝23 λl: Identifier.22 definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝ 23 λl: ident. 24 24 λg: BitVectorTrieSet 16. 25 25 set_insert ? l g. 26 26 27 definition marked: Identifier→ BitVectorTrieSet 16 → bool ≝28 λl: Identifier.27 definition marked: ident → BitVectorTrieSet 16 → bool ≝ 28 λl: ident. 29 29 λg: BitVectorTrieSet 16. 30 30 set_member ? l g. … … 32 32 definition graph_lookup ≝ 33 33 λglobals. 34 λl: Identifier.35 λg: LTLStatementGraph globals.34 λl: ident. 35 λg: ltl_statement_graph globals. 36 36 lookup LabelTag (LTLStatement globals) g (an_identifier LabelTag l). 37 37 … … 58 58 visit globals g required visited generated l2 n. 59 59 60 let rec visit (globals: list Identifier) (g: LTLStatementGraph globals)60 let rec visit (globals: list ident) (g: ltl_statement_graph globals) 61 61 (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16) 62 (generated: list ( PreLINStatement globals)) (l: Identifier) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝62 (generated: list (pre_lin_statement globals)) (l: ident) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝ 63 63 match n with 64 64 [ O ⇒ 〈required, generated〉 … … 71 71 let generated'' ≝ translated_statement :: generated in 72 72 match statement with 73 [ Joint_St_Sequential instr l2 ⇒73 [ joint_st_sequential instr l2 ⇒ 74 74 match instr with 75 [ Joint_Instr_CondAcc l1 ⇒75 [ joint_instr_cond_acc l1 ⇒ 76 76 let required' ≝ 77 77 if marked l2 visited' then … … 101 101 visit globals g required' visited' generated'' l2 n' 102 102 ] 103 | Joint_St_Goto lbl ⇒103 | joint_st_goto lbl ⇒ 104 104 let required' ≝ 105 105 if marked lbl visited' then … … 111 111 else 112 112 visit globals g required' visited' generated'' lbl n' 113 | Joint_St_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)113 | joint_st_Return ⇒ 〈required, generated''〉 (* dpm: correct? *) 114 114 ] 115 115 ] -
src/common/AST.ma
r747 r757 497 497 498 498 (* dpm: should go to standard library *) 499 let rec member (i: Identifier) (eq_i: Identifier → Identifier→ bool)500 (g: list Identifier) on g: Prop ≝499 let rec member (i: ident) (eq_i: ident → ident → bool) 500 (g: list ident) on g: Prop ≝ 501 501 match g with 502 502 [ nil ⇒ False -
src/common/CostLabel.ma
r747 r757 7 7 (* For use in importing programs in intermediate languages. *) 8 8 definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?. 9 10 (* dpm: fix identifier/costlabel mismatch *) 11 axiom Identifier_of_costlabel: costlabel → Identifier. -
src/common/Identifiers.ma
r753 r757 24 24 OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉. 25 25 // qed. 26 27 definition eq_identifier ≝ 28 λt. 29 λl, r: identifier t. 30 match l with 31 [ an_identifier l' ⇒ 32 match r with 33 [ an_identifier r' ⇒ 34 eq_bv ? l' r' 35 ] 36 ]. 37 38 39 definition word_of_identifier ≝ 40 λt. 41 λl: identifier t. 42 match l with 43 [ an_identifier l' ⇒ l' 44 ]. 26 45 27 46 definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y). -
src/common/Registers.ma
r738 r757 6 6 include "ASM/BitVectorTrie.ma". 7 7 include "common/Identifiers.ma". 8 include "ASM/I8051.ma". 8 9 9 10 axiom RegisterTag : String. … … 14 15 15 16 definition register_env ≝ identifier_map RegisterTag. 17 18 (* dpm: fix the Register/register mismatch *) 19 axiom Register_of_register: register → Register.
Note: See TracChangeset
for help on using the changeset viewer.