Ignore:
Timestamp:
Mar 28, 2013, 10:27:41 AM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabs_syntax.ml

    r2951 r2997  
    139139    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    140140let rec statement_rect_Type4 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    141 | St_skip x_14946 -> h_St_skip x_14946
    142 | St_cost (x_14948, x_14947) -> h_St_cost x_14948 x_14947
    143 | St_const (t, x_14951, x_14950, x_14949) ->
    144   h_St_const t x_14951 x_14950 x_14949
    145 | St_op1 (t', t, x_14955, x_14954, x_14953, x_14952) ->
    146   h_St_op1 t' t x_14955 x_14954 x_14953 x_14952
    147 | St_op2 (t', t1, t2, x_14960, x_14959, x_14958, x_14957, x_14956) ->
    148   h_St_op2 t' t1 t2 x_14960 x_14959 x_14958 x_14957 x_14956
    149 | St_load (x_14964, x_14963, x_14962, x_14961) ->
    150   h_St_load x_14964 x_14963 x_14962 x_14961
    151 | St_store (x_14968, x_14967, x_14966, x_14965) ->
    152   h_St_store x_14968 x_14967 x_14966 x_14965
    153 | St_call_id (x_14972, x_14971, x_14970, x_14969) ->
    154   h_St_call_id x_14972 x_14971 x_14970 x_14969
    155 | St_call_ptr (x_14976, x_14975, x_14974, x_14973) ->
    156   h_St_call_ptr x_14976 x_14975 x_14974 x_14973
    157 | St_cond (x_14979, x_14978, x_14977) -> h_St_cond x_14979 x_14978 x_14977
     141| St_skip x_48 -> h_St_skip x_48
     142| St_cost (x_50, x_49) -> h_St_cost x_50 x_49
     143| St_const (t, x_53, x_52, x_51) -> h_St_const t x_53 x_52 x_51
     144| St_op1 (t', t, x_57, x_56, x_55, x_54) -> h_St_op1 t' t x_57 x_56 x_55 x_54
     145| St_op2 (t', t1, t2, x_62, x_61, x_60, x_59, x_58) ->
     146  h_St_op2 t' t1 t2 x_62 x_61 x_60 x_59 x_58
     147| St_load (x_66, x_65, x_64, x_63) -> h_St_load x_66 x_65 x_64 x_63
     148| St_store (x_70, x_69, x_68, x_67) -> h_St_store x_70 x_69 x_68 x_67
     149| St_call_id (x_74, x_73, x_72, x_71) -> h_St_call_id x_74 x_73 x_72 x_71
     150| St_call_ptr (x_78, x_77, x_76, x_75) -> h_St_call_ptr x_78 x_77 x_76 x_75
     151| St_cond (x_81, x_80, x_79) -> h_St_cond x_81 x_80 x_79
    158152| St_return -> h_St_return
    159153
     
    174168    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    175169let rec statement_rect_Type5 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    176 | St_skip x_14992 -> h_St_skip x_14992
    177 | St_cost (x_14994, x_14993) -> h_St_cost x_14994 x_14993
    178 | St_const (t, x_14997, x_14996, x_14995) ->
    179   h_St_const t x_14997 x_14996 x_14995
    180 | St_op1 (t', t, x_15001, x_15000, x_14999, x_14998) ->
    181   h_St_op1 t' t x_15001 x_15000 x_14999 x_14998
    182 | St_op2 (t', t1, t2, x_15006, x_15005, x_15004, x_15003, x_15002) ->
    183   h_St_op2 t' t1 t2 x_15006 x_15005 x_15004 x_15003 x_15002
    184 | St_load (x_15010, x_15009, x_15008, x_15007) ->
    185   h_St_load x_15010 x_15009 x_15008 x_15007
    186 | St_store (x_15014, x_15013, x_15012, x_15011) ->
    187   h_St_store x_15014 x_15013 x_15012 x_15011
    188 | St_call_id (x_15018, x_15017, x_15016, x_15015) ->
    189   h_St_call_id x_15018 x_15017 x_15016 x_15015
    190 | St_call_ptr (x_15022, x_15021, x_15020, x_15019) ->
    191   h_St_call_ptr x_15022 x_15021 x_15020 x_15019
    192 | St_cond (x_15025, x_15024, x_15023) -> h_St_cond x_15025 x_15024 x_15023
     170| St_skip x_94 -> h_St_skip x_94
     171| St_cost (x_96, x_95) -> h_St_cost x_96 x_95
     172| St_const (t, x_99, x_98, x_97) -> h_St_const t x_99 x_98 x_97
     173| St_op1 (t', t, x_103, x_102, x_101, x_100) ->
     174  h_St_op1 t' t x_103 x_102 x_101 x_100
     175| St_op2 (t', t1, t2, x_108, x_107, x_106, x_105, x_104) ->
     176  h_St_op2 t' t1 t2 x_108 x_107 x_106 x_105 x_104
     177| St_load (x_112, x_111, x_110, x_109) -> h_St_load x_112 x_111 x_110 x_109
     178| St_store (x_116, x_115, x_114, x_113) -> h_St_store x_116 x_115 x_114 x_113
     179| St_call_id (x_120, x_119, x_118, x_117) ->
     180  h_St_call_id x_120 x_119 x_118 x_117
     181| St_call_ptr (x_124, x_123, x_122, x_121) ->
     182  h_St_call_ptr x_124 x_123 x_122 x_121
     183| St_cond (x_127, x_126, x_125) -> h_St_cond x_127 x_126 x_125
    193184| St_return -> h_St_return
    194185
     
    209200    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    210201let rec statement_rect_Type3 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    211 | St_skip x_15038 -> h_St_skip x_15038
    212 | St_cost (x_15040, x_15039) -> h_St_cost x_15040 x_15039
    213 | St_const (t, x_15043, x_15042, x_15041) ->
    214   h_St_const t x_15043 x_15042 x_15041
    215 | St_op1 (t', t, x_15047, x_15046, x_15045, x_15044) ->
    216   h_St_op1 t' t x_15047 x_15046 x_15045 x_15044
    217 | St_op2 (t', t1, t2, x_15052, x_15051, x_15050, x_15049, x_15048) ->
    218   h_St_op2 t' t1 t2 x_15052 x_15051 x_15050 x_15049 x_15048
    219 | St_load (x_15056, x_15055, x_15054, x_15053) ->
    220   h_St_load x_15056 x_15055 x_15054 x_15053
    221 | St_store (x_15060, x_15059, x_15058, x_15057) ->
    222   h_St_store x_15060 x_15059 x_15058 x_15057
    223 | St_call_id (x_15064, x_15063, x_15062, x_15061) ->
    224   h_St_call_id x_15064 x_15063 x_15062 x_15061
    225 | St_call_ptr (x_15068, x_15067, x_15066, x_15065) ->
    226   h_St_call_ptr x_15068 x_15067 x_15066 x_15065
    227 | St_cond (x_15071, x_15070, x_15069) -> h_St_cond x_15071 x_15070 x_15069
     202| St_skip x_140 -> h_St_skip x_140
     203| St_cost (x_142, x_141) -> h_St_cost x_142 x_141
     204| St_const (t, x_145, x_144, x_143) -> h_St_const t x_145 x_144 x_143
     205| St_op1 (t', t, x_149, x_148, x_147, x_146) ->
     206  h_St_op1 t' t x_149 x_148 x_147 x_146
     207| St_op2 (t', t1, t2, x_154, x_153, x_152, x_151, x_150) ->
     208  h_St_op2 t' t1 t2 x_154 x_153 x_152 x_151 x_150
     209| St_load (x_158, x_157, x_156, x_155) -> h_St_load x_158 x_157 x_156 x_155
     210| St_store (x_162, x_161, x_160, x_159) -> h_St_store x_162 x_161 x_160 x_159
     211| St_call_id (x_166, x_165, x_164, x_163) ->
     212  h_St_call_id x_166 x_165 x_164 x_163
     213| St_call_ptr (x_170, x_169, x_168, x_167) ->
     214  h_St_call_ptr x_170 x_169 x_168 x_167
     215| St_cond (x_173, x_172, x_171) -> h_St_cond x_173 x_172 x_171
    228216| St_return -> h_St_return
    229217
     
    244232    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    245233let rec statement_rect_Type2 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    246 | St_skip x_15084 -> h_St_skip x_15084
    247 | St_cost (x_15086, x_15085) -> h_St_cost x_15086 x_15085
    248 | St_const (t, x_15089, x_15088, x_15087) ->
    249   h_St_const t x_15089 x_15088 x_15087
    250 | St_op1 (t', t, x_15093, x_15092, x_15091, x_15090) ->
    251   h_St_op1 t' t x_15093 x_15092 x_15091 x_15090
    252 | St_op2 (t', t1, t2, x_15098, x_15097, x_15096, x_15095, x_15094) ->
    253   h_St_op2 t' t1 t2 x_15098 x_15097 x_15096 x_15095 x_15094
    254 | St_load (x_15102, x_15101, x_15100, x_15099) ->
    255   h_St_load x_15102 x_15101 x_15100 x_15099
    256 | St_store (x_15106, x_15105, x_15104, x_15103) ->
    257   h_St_store x_15106 x_15105 x_15104 x_15103
    258 | St_call_id (x_15110, x_15109, x_15108, x_15107) ->
    259   h_St_call_id x_15110 x_15109 x_15108 x_15107
    260 | St_call_ptr (x_15114, x_15113, x_15112, x_15111) ->
    261   h_St_call_ptr x_15114 x_15113 x_15112 x_15111
    262 | St_cond (x_15117, x_15116, x_15115) -> h_St_cond x_15117 x_15116 x_15115
     234| St_skip x_186 -> h_St_skip x_186
     235| St_cost (x_188, x_187) -> h_St_cost x_188 x_187
     236| St_const (t, x_191, x_190, x_189) -> h_St_const t x_191 x_190 x_189
     237| St_op1 (t', t, x_195, x_194, x_193, x_192) ->
     238  h_St_op1 t' t x_195 x_194 x_193 x_192
     239| St_op2 (t', t1, t2, x_200, x_199, x_198, x_197, x_196) ->
     240  h_St_op2 t' t1 t2 x_200 x_199 x_198 x_197 x_196
     241| St_load (x_204, x_203, x_202, x_201) -> h_St_load x_204 x_203 x_202 x_201
     242| St_store (x_208, x_207, x_206, x_205) -> h_St_store x_208 x_207 x_206 x_205
     243| St_call_id (x_212, x_211, x_210, x_209) ->
     244  h_St_call_id x_212 x_211 x_210 x_209
     245| St_call_ptr (x_216, x_215, x_214, x_213) ->
     246  h_St_call_ptr x_216 x_215 x_214 x_213
     247| St_cond (x_219, x_218, x_217) -> h_St_cond x_219 x_218 x_217
    263248| St_return -> h_St_return
    264249
     
    279264    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    280265let rec statement_rect_Type1 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    281 | St_skip x_15130 -> h_St_skip x_15130
    282 | St_cost (x_15132, x_15131) -> h_St_cost x_15132 x_15131
    283 | St_const (t, x_15135, x_15134, x_15133) ->
    284   h_St_const t x_15135 x_15134 x_15133
    285 | St_op1 (t', t, x_15139, x_15138, x_15137, x_15136) ->
    286   h_St_op1 t' t x_15139 x_15138 x_15137 x_15136
    287 | St_op2 (t', t1, t2, x_15144, x_15143, x_15142, x_15141, x_15140) ->
    288   h_St_op2 t' t1 t2 x_15144 x_15143 x_15142 x_15141 x_15140
    289 | St_load (x_15148, x_15147, x_15146, x_15145) ->
    290   h_St_load x_15148 x_15147 x_15146 x_15145
    291 | St_store (x_15152, x_15151, x_15150, x_15149) ->
    292   h_St_store x_15152 x_15151 x_15150 x_15149
    293 | St_call_id (x_15156, x_15155, x_15154, x_15153) ->
    294   h_St_call_id x_15156 x_15155 x_15154 x_15153
    295 | St_call_ptr (x_15160, x_15159, x_15158, x_15157) ->
    296   h_St_call_ptr x_15160 x_15159 x_15158 x_15157
    297 | St_cond (x_15163, x_15162, x_15161) -> h_St_cond x_15163 x_15162 x_15161
     266| St_skip x_232 -> h_St_skip x_232
     267| St_cost (x_234, x_233) -> h_St_cost x_234 x_233
     268| St_const (t, x_237, x_236, x_235) -> h_St_const t x_237 x_236 x_235
     269| St_op1 (t', t, x_241, x_240, x_239, x_238) ->
     270  h_St_op1 t' t x_241 x_240 x_239 x_238
     271| St_op2 (t', t1, t2, x_246, x_245, x_244, x_243, x_242) ->
     272  h_St_op2 t' t1 t2 x_246 x_245 x_244 x_243 x_242
     273| St_load (x_250, x_249, x_248, x_247) -> h_St_load x_250 x_249 x_248 x_247
     274| St_store (x_254, x_253, x_252, x_251) -> h_St_store x_254 x_253 x_252 x_251
     275| St_call_id (x_258, x_257, x_256, x_255) ->
     276  h_St_call_id x_258 x_257 x_256 x_255
     277| St_call_ptr (x_262, x_261, x_260, x_259) ->
     278  h_St_call_ptr x_262 x_261 x_260 x_259
     279| St_cond (x_265, x_264, x_263) -> h_St_cond x_265 x_264 x_263
    298280| St_return -> h_St_return
    299281
     
    314296    Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
    315297let rec statement_rect_Type0 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
    316 | St_skip x_15176 -> h_St_skip x_15176
    317 | St_cost (x_15178, x_15177) -> h_St_cost x_15178 x_15177
    318 | St_const (t, x_15181, x_15180, x_15179) ->
    319   h_St_const t x_15181 x_15180 x_15179
    320 | St_op1 (t', t, x_15185, x_15184, x_15183, x_15182) ->
    321   h_St_op1 t' t x_15185 x_15184 x_15183 x_15182
    322 | St_op2 (t', t1, t2, x_15190, x_15189, x_15188, x_15187, x_15186) ->
    323   h_St_op2 t' t1 t2 x_15190 x_15189 x_15188 x_15187 x_15186
    324 | St_load (x_15194, x_15193, x_15192, x_15191) ->
    325   h_St_load x_15194 x_15193 x_15192 x_15191
    326 | St_store (x_15198, x_15197, x_15196, x_15195) ->
    327   h_St_store x_15198 x_15197 x_15196 x_15195
    328 | St_call_id (x_15202, x_15201, x_15200, x_15199) ->
    329   h_St_call_id x_15202 x_15201 x_15200 x_15199
    330 | St_call_ptr (x_15206, x_15205, x_15204, x_15203) ->
    331   h_St_call_ptr x_15206 x_15205 x_15204 x_15203
    332 | St_cond (x_15209, x_15208, x_15207) -> h_St_cond x_15209 x_15208 x_15207
     298| St_skip x_278 -> h_St_skip x_278
     299| St_cost (x_280, x_279) -> h_St_cost x_280 x_279
     300| St_const (t, x_283, x_282, x_281) -> h_St_const t x_283 x_282 x_281
     301| St_op1 (t', t, x_287, x_286, x_285, x_284) ->
     302  h_St_op1 t' t x_287 x_286 x_285 x_284
     303| St_op2 (t', t1, t2, x_292, x_291, x_290, x_289, x_288) ->
     304  h_St_op2 t' t1 t2 x_292 x_291 x_290 x_289 x_288
     305| St_load (x_296, x_295, x_294, x_293) -> h_St_load x_296 x_295 x_294 x_293
     306| St_store (x_300, x_299, x_298, x_297) -> h_St_store x_300 x_299 x_298 x_297
     307| St_call_id (x_304, x_303, x_302, x_301) ->
     308  h_St_call_id x_304 x_303 x_302 x_301
     309| St_call_ptr (x_308, x_307, x_306, x_305) ->
     310  h_St_call_ptr x_308 x_307 x_306 x_305
     311| St_cond (x_311, x_310, x_309) -> h_St_cond x_311 x_310 x_309
    333312| St_return -> h_St_return
    334313
     
    464443    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
    465444    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
    466     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
     445    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    467446    internal_function -> 'a1 **)
    468 let rec internal_function_rect_Type4 h_mk_internal_function x_15499 =
     447let rec internal_function_rect_Type4 h_mk_internal_function x_601 =
    469448  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    470449    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    471     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15499
     450    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_601
    472451  in
    473452  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
    474     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
     453    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
    475454
    476455(** val internal_function_rect_Type5 :
     
    479458    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
    480459    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
    481     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
     460    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    482461    internal_function -> 'a1 **)
    483 let rec internal_function_rect_Type5 h_mk_internal_function x_15501 =
     462let rec internal_function_rect_Type5 h_mk_internal_function x_603 =
    484463  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    485464    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    486     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15501
     465    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_603
    487466  in
    488467  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
    489     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
     468    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
    490469
    491470(** val internal_function_rect_Type3 :
     
    494473    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
    495474    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
    496     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
     475    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    497476    internal_function -> 'a1 **)
    498 let rec internal_function_rect_Type3 h_mk_internal_function x_15503 =
     477let rec internal_function_rect_Type3 h_mk_internal_function x_605 =
    499478  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    500479    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    501     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15503
     480    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_605
    502481  in
    503482  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
    504     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
     483    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
    505484
    506485(** val internal_function_rect_Type2 :
     
    509488    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
    510489    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
    511     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
     490    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    512491    internal_function -> 'a1 **)
    513 let rec internal_function_rect_Type2 h_mk_internal_function x_15505 =
     492let rec internal_function_rect_Type2 h_mk_internal_function x_607 =
    514493  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    515494    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    516     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15505
     495    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_607
    517496  in
    518497  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
    519     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
     498    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
    520499
    521500(** val internal_function_rect_Type1 :
     
    524503    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
    525504    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
    526     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
     505    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    527506    internal_function -> 'a1 **)
    528 let rec internal_function_rect_Type1 h_mk_internal_function x_15507 =
     507let rec internal_function_rect_Type1 h_mk_internal_function x_609 =
    529508  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    530509    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    531     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15507
     510    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_609
    532511  in
    533512  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
    534     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
     513    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
    535514
    536515(** val internal_function_rect_Type0 :
     
    539518    Types.prod List.list -> (Registers.register, AST.typ) Types.prod
    540519    List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
    541     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) ->
     520    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
    542521    internal_function -> 'a1 **)
    543 let rec internal_function_rect_Type0 h_mk_internal_function x_15509 =
     522let rec internal_function_rect_Type0 h_mk_internal_function x_611 =
    544523  let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
    545524    f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
    546     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15509
     525    f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_611
    547526  in
    548527  h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
    549     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0
     528    f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
    550529
    551530(** val f_labgen : internal_function -> Identifiers.universe **)
     
    595574    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
    596575    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
    597     Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
     576    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
    598577let internal_function_inv_rect_Type4 hterm h1 =
    599578  let hcut = internal_function_rect_Type4 h1 hterm in hcut __
     
    605584    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
    606585    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
    607     Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
     586    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
    608587let internal_function_inv_rect_Type3 hterm h1 =
    609588  let hcut = internal_function_rect_Type3 h1 hterm in hcut __
     
    615594    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
    616595    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
    617     Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
     596    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
    618597let internal_function_inv_rect_Type2 hterm h1 =
    619598  let hcut = internal_function_rect_Type2 h1 hterm in hcut __
     
    625604    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
    626605    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
    627     Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
     606    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
    628607let internal_function_inv_rect_Type1 hterm h1 =
    629608  let hcut = internal_function_rect_Type1 h1 hterm in hcut __
     
    635614    (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
    636615    statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
    637     Graphs.label Types.sig0 -> __ -> 'a1) -> 'a1 **)
     616    Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
    638617let internal_function_inv_rect_Type0 hterm h1 =
    639618  let hcut = internal_function_rect_Type0 h1 hterm in hcut __
     
    647626       a10 } = x
    648627     in
    649     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)) y
     628    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __)) y
    650629
    651630type rTLabs_program =
Note: See TracChangeset for help on using the changeset viewer.