Changeset 2951 for extracted/eRTLptrToLTL.ml
 Timestamp:
 Mar 25, 2013, 11:30:01 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/eRTLptrToLTL.ml
r2890 r2951 1 1 open Preamble 2 3 open Extra_bool 4 5 open Coqlib 6 7 open Values 8 9 open FrontEndVal 10 11 open GenMem 12 13 open FrontEndMem 14 15 open Globalenvs 2 16 3 17 open String … … 167 181 arg_decision > 'a1 **) 168 182 let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 169  Arg_decision_colour x_ 22106 > h_arg_decision_colour x_22106170  Arg_decision_spill x_ 22107 > h_arg_decision_spill x_22107171  Arg_decision_imm x_ 22108 > h_arg_decision_imm x_22108183  Arg_decision_colour x_19209 > h_arg_decision_colour x_19209 184  Arg_decision_spill x_19210 > h_arg_decision_spill x_19210 185  Arg_decision_imm x_19211 > h_arg_decision_imm x_19211 172 186 173 187 (** val arg_decision_rect_Type5 : … … 175 189 arg_decision > 'a1 **) 176 190 let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 177  Arg_decision_colour x_ 22113 > h_arg_decision_colour x_22113178  Arg_decision_spill x_ 22114 > h_arg_decision_spill x_22114179  Arg_decision_imm x_ 22115 > h_arg_decision_imm x_22115191  Arg_decision_colour x_19216 > h_arg_decision_colour x_19216 192  Arg_decision_spill x_19217 > h_arg_decision_spill x_19217 193  Arg_decision_imm x_19218 > h_arg_decision_imm x_19218 180 194 181 195 (** val arg_decision_rect_Type3 : … … 183 197 arg_decision > 'a1 **) 184 198 let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 185  Arg_decision_colour x_ 22120 > h_arg_decision_colour x_22120186  Arg_decision_spill x_ 22121 > h_arg_decision_spill x_22121187  Arg_decision_imm x_ 22122 > h_arg_decision_imm x_22122199  Arg_decision_colour x_19223 > h_arg_decision_colour x_19223 200  Arg_decision_spill x_19224 > h_arg_decision_spill x_19224 201  Arg_decision_imm x_19225 > h_arg_decision_imm x_19225 188 202 189 203 (** val arg_decision_rect_Type2 : … … 191 205 arg_decision > 'a1 **) 192 206 let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 193  Arg_decision_colour x_ 22127 > h_arg_decision_colour x_22127194  Arg_decision_spill x_ 22128 > h_arg_decision_spill x_22128195  Arg_decision_imm x_ 22129 > h_arg_decision_imm x_22129207  Arg_decision_colour x_19230 > h_arg_decision_colour x_19230 208  Arg_decision_spill x_19231 > h_arg_decision_spill x_19231 209  Arg_decision_imm x_19232 > h_arg_decision_imm x_19232 196 210 197 211 (** val arg_decision_rect_Type1 : … … 199 213 arg_decision > 'a1 **) 200 214 let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 201  Arg_decision_colour x_ 22134 > h_arg_decision_colour x_22134202  Arg_decision_spill x_ 22135 > h_arg_decision_spill x_22135203  Arg_decision_imm x_ 22136 > h_arg_decision_imm x_22136215  Arg_decision_colour x_19237 > h_arg_decision_colour x_19237 216  Arg_decision_spill x_19238 > h_arg_decision_spill x_19238 217  Arg_decision_imm x_19239 > h_arg_decision_imm x_19239 204 218 205 219 (** val arg_decision_rect_Type0 : … … 207 221 arg_decision > 'a1 **) 208 222 let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function 209  Arg_decision_colour x_ 22141 > h_arg_decision_colour x_22141210  Arg_decision_spill x_ 22142 > h_arg_decision_spill x_22142211  Arg_decision_imm x_ 22143 > h_arg_decision_imm x_22143223  Arg_decision_colour x_19244 > h_arg_decision_colour x_19244 224  Arg_decision_spill x_19245 > h_arg_decision_spill x_19245 225  Arg_decision_imm x_19246 > h_arg_decision_imm x_19246 212 226 213 227 (** val arg_decision_inv_rect_Type4 : … … 799 813 800 814 (** val translate_step : 801 AST.ident List.list > Nat.nat > Fixpoints.valuation>802 Interference.coloured_graph > Nat.nat > Graphs.label>803 Joint.joint_step > Blocks.bind_step_block **)804 let translate_step globals localss after grph stack_sz lbl s =815 AST.ident List.list > Joint.joint_internal_function > Nat.nat > 816 Fixpoints.valuation > Interference.coloured_graph > Nat.nat > 817 Graphs.label > Joint.joint_step > Blocks.bind_step_block **) 818 let translate_step globals fn localss after grph stack_sz lbl s = 805 819 Bind_new.Bret 806 820 (let lookup = fun r > grph.Interference.colouring (Types.Inl r) in … … 956 970 Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun) 957 971 in 958 let coloured_graph = build globals (Types.pi1 int_fun) after in 972 let coloured_graph = 973 build globals (Types.pi1 int_fun) 974 (Fixpoints.fix_lfp Liveness.register_lattice 975 (Liveness.liveafter globals (Types.pi1 int_fun)) after) 976 in 959 977 let stack_sz = 960 978 Nat.plus coloured_graph.Interference.spilled_no … … 965 983 TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue = 966 984 List.Nil; TranslateUtils.new_regs = List.Nil; TranslateUtils.f_step = 967 (translate_step globals (Types.pi1 int_fun).Joint.joint_if_local_stacksize 968 after coloured_graph stack_sz); TranslateUtils.f_fin = 969 (translate_fin_step globals) } 985 (translate_step globals (Types.pi1 int_fun) 986 (Types.pi1 int_fun).Joint.joint_if_local_stacksize 987 (Fixpoints.fix_lfp Liveness.register_lattice 988 (Liveness.liveafter globals (Types.pi1 int_fun)) after) coloured_graph 989 stack_sz); TranslateUtils.f_fin = (translate_fin_step globals) } 970 990 971 991 (** val ertlptr_to_ltl :
Note: See TracChangeset
for help on using the changeset viewer.