Changeset 2841
 Timestamp:
 Mar 11, 2013, 12:40:46 PM (4 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/compiler.ma
r2835 r2841 31 31  lin_pass: pass. 32 32 33 definition with_stack_model : Type[0] → Type[0] ≝ 34 λA:Type[0].A × (ident → option ℕ). 35 33 36 definition syntax_of_pass : pass → Type[0] ≝ 34 37 λpass. … … 40 43  cminor_pass ⇒ Cminor_program 41 44  rtlabs_pass ⇒ RTLabs_program 42  rtl_separate_pass ⇒ rtl_program43  rtl_uniq_pass ⇒ rtl_program44  ertl_pass ⇒ ertl_program45  ertlptr_pass ⇒ ertlptr_program46  ltl_pass ⇒ ltl_program47  lin_pass ⇒ lin_program ].45  rtl_separate_pass ⇒ with_stack_model rtl_program 46  rtl_uniq_pass ⇒ with_stack_model rtl_program 47  ertl_pass ⇒ with_stack_model ertl_program 48  ertlptr_pass ⇒ with_stack_model ertlptr_program 49  ltl_pass ⇒ with_stack_model ltl_program 50  lin_pass ⇒ with_stack_model lin_program ]. 48 51 49 52 definition observe_pass ≝ ∀pass. syntax_of_pass pass → unit. … … 73 76 74 77 (* The compiler backend *) 75 include "ERTLptr/ Uses.ma". (* Included by the untrusted code *)78 include "ERTLptr/uses.ma". (* Included by the untrusted code *) 76 79 axiom compute_fixpoint : fixpoint_computer. 77 80 axiom colour_graph : coloured_graph_computer. 81 82 include "common/AssocList.ma". 83 84 (* Inefficient, replace with Trie lookup *) 85 definition lookup_stack_cost ≝ 86 λP,p,id. 87 assoc_list_lookup ?? id (eq_identifier …) (stack_cost P p). 78 88 79 89 definition back_end : … … 82 92 λobserve,p. 83 93 let p ≝ rtlabs_to_rtl p in 84 let i ≝ observe rtl_separate_pass p in 85 let i ≝ observe rtl_uniq_pass p in 94 let st ≝ lookup_stack_cost … p in 95 let i ≝ observe rtl_separate_pass 〈p,st〉 in 96 let i ≝ observe rtl_uniq_pass 〈p,st〉 in 86 97 let p ≝ rtl_to_ertl p in 87 let i ≝ observe ertl_pass p in 98 let st ≝ lookup_stack_cost … p in 99 let i ≝ observe ertl_pass 〈p,st〉 in 88 100 let p ≝ ertl_to_ertlptr p in 89 let i ≝ observe ertlptr_pass p in 90 let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in (* TODO: abstract over colouring *) 91 let i ≝ observe ltl_pass p in 101 let st ≝ lookup_stack_cost … p in 102 let i ≝ observe ertlptr_pass 〈p,st〉 in 103 let 〈p,stack_cost,max_stack〉 ≝ ertlptr_to_ltl compute_fixpoint colour_graph p in 104 (* The two stack models are the same *) 105 let st ≝ lookup_stack_cost … p in 106 let i ≝ observe ltl_pass 〈p,st〉 in 107 let st ≝ lookup_stack_cost … p in 92 108 let p ≝ ltl_to_lin p in 93 let i ≝ observe lin_pass p in 109 let st ≝ lookup_stack_cost … p in 110 let i ≝ observe lin_pass 〈p,st〉 in 94 111 ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ; 95 112 return 〈p,stack_cost,max_stack〉. 
src/semantics.ma
r2828 r2841 38 38 mk_preclassified_system_pass lin_pass (joint_preclassified_system LIN_semantics) ? 39 39 ]. 40 try % 41 whd in ⊢ (??%%); 42 cases daemon (* XXX False! Leads to core dump! *) 40 % 43 41 qed. 44 42
Note: See TracChangeset
for help on using the changeset viewer.