Ignore:
Timestamp:
Mar 8, 2013, 9:07:28 PM (7 years ago)
Author:
sacerdot
Message:

Everything extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cminor_semantics.ml

    r2810 r2827  
    123123let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function
    124124| Kend -> h_Kend
    125 | Kseq (x_10, x_9) ->
    126   h_Kseq x_10 x_9 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_9)
    127 | Kblock x_11 -> h_Kblock x_11 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_11)
     125| Kseq (x_70, x_69) ->
     126  h_Kseq x_70 x_69 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_69)
     127| Kblock x_71 -> h_Kblock x_71 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_71)
    128128
    129129(** val cont_rect_Type3 :
     
    132132let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function
    133133| Kend -> h_Kend
    134 | Kseq (x_24, x_23) ->
    135   h_Kseq x_24 x_23 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23)
    136 | Kblock x_25 -> h_Kblock x_25 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_25)
     134| Kseq (x_84, x_83) ->
     135  h_Kseq x_84 x_83 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_83)
     136| Kblock x_85 -> h_Kblock x_85 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_85)
    137137
    138138(** val cont_rect_Type2 :
     
    141141let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function
    142142| Kend -> h_Kend
    143 | Kseq (x_31, x_30) ->
    144   h_Kseq x_31 x_30 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_30)
    145 | Kblock x_32 -> h_Kblock x_32 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_32)
     143| Kseq (x_91, x_90) ->
     144  h_Kseq x_91 x_90 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_90)
     145| Kblock x_92 -> h_Kblock x_92 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_92)
    146146
    147147(** val cont_rect_Type1 :
     
    150150let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function
    151151| Kend -> h_Kend
    152 | Kseq (x_38, x_37) ->
    153   h_Kseq x_38 x_37 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_37)
    154 | Kblock x_39 -> h_Kblock x_39 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_39)
     152| Kseq (x_98, x_97) ->
     153  h_Kseq x_98 x_97 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_97)
     154| Kblock x_99 -> h_Kblock x_99 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_99)
    155155
    156156(** val cont_rect_Type0 :
     
    159159let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function
    160160| Kend -> h_Kend
    161 | Kseq (x_45, x_44) ->
    162   h_Kseq x_45 x_44 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_44)
    163 | Kblock x_46 -> h_Kblock x_46 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_46)
     161| Kseq (x_105, x_104) ->
     162  h_Kseq x_105 x_104 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_104)
     163| Kblock x_106 ->
     164  h_Kblock x_106 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_106)
    164165
    165166(** val cont_inv_rect_Type4 :
     
    221222let rec stack_rect_Type4 h_SStop h_Scall = function
    222223| SStop -> h_SStop
    223 | Scall (dest, f, x_105, en, k, x_101) ->
    224   h_Scall dest f x_105 en __ __ k __ x_101
    225     (stack_rect_Type4 h_SStop h_Scall x_101)
     224| Scall (dest, f, x_165, en, k, x_161) ->
     225  h_Scall dest f x_165 en __ __ k __ x_161
     226    (stack_rect_Type4 h_SStop h_Scall x_161)
    226227
    227228(** val stack_rect_Type3 :
     
    231232let rec stack_rect_Type3 h_SStop h_Scall = function
    232233| SStop -> h_SStop
    233 | Scall (dest, f, x_121, en, k, x_117) ->
    234   h_Scall dest f x_121 en __ __ k __ x_117
    235     (stack_rect_Type3 h_SStop h_Scall x_117)
     234| Scall (dest, f, x_181, en, k, x_177) ->
     235  h_Scall dest f x_181 en __ __ k __ x_177
     236    (stack_rect_Type3 h_SStop h_Scall x_177)
    236237
    237238(** val stack_rect_Type2 :
     
    241242let rec stack_rect_Type2 h_SStop h_Scall = function
    242243| SStop -> h_SStop
    243 | Scall (dest, f, x_129, en, k, x_125) ->
    244   h_Scall dest f x_129 en __ __ k __ x_125
    245     (stack_rect_Type2 h_SStop h_Scall x_125)
     244| Scall (dest, f, x_189, en, k, x_185) ->
     245  h_Scall dest f x_189 en __ __ k __ x_185
     246    (stack_rect_Type2 h_SStop h_Scall x_185)
    246247
    247248(** val stack_rect_Type1 :
     
    251252let rec stack_rect_Type1 h_SStop h_Scall = function
    252253| SStop -> h_SStop
    253 | Scall (dest, f, x_137, en, k, x_133) ->
    254   h_Scall dest f x_137 en __ __ k __ x_133
    255     (stack_rect_Type1 h_SStop h_Scall x_133)
     254| Scall (dest, f, x_197, en, k, x_193) ->
     255  h_Scall dest f x_197 en __ __ k __ x_193
     256    (stack_rect_Type1 h_SStop h_Scall x_193)
    256257
    257258(** val stack_rect_Type0 :
     
    261262let rec stack_rect_Type0 h_SStop h_Scall = function
    262263| SStop -> h_SStop
    263 | Scall (dest, f, x_145, en, k, x_141) ->
    264   h_Scall dest f x_145 en __ __ k __ x_141
    265     (stack_rect_Type0 h_SStop h_Scall x_141)
     264| Scall (dest, f, x_205, en, k, x_201) ->
     265  h_Scall dest f x_205 en __ __ k __ x_201
     266    (stack_rect_Type0 h_SStop h_Scall x_201)
    266267
    267268(** val stack_inv_rect_Type4 :
     
    701702                  (Obj.magic
    702703                    (trace_map_inv (fun e ->
    703                       let { Types.dpi1 = ty; Types.dpi2 = e1 } = e in
    704                       (fun _ -> eval_expr ge ty e1 en sp m)) args))
     704                      let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
     705                      (fun _ -> eval_expr ge ty e0 en sp m)) args))
    705706                  (fun tr' vargs ->
    706707                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     
    735736                 (GenMem.free m sp), st0)) }))
    736737         | Types.Some e ->
    737            let { Types.dpi1 = ty; Types.dpi2 = e1 } = e in
     738           let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
    738739           (fun _ ->
    739740           Obj.magic
    740741             (Monad.m_bind2 (Monad.max_def Errors.res0)
    741                (Obj.magic (eval_expr ge ty e1 en sp m)) (fun tr v ->
     742               (Obj.magic (eval_expr ge ty e0 en sp m)) (fun tr v ->
    742743               Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
    743744                 Types.snd = (Returnstate ((Types.Some v),
     
    750751      | Cminor_syntax.St_goto l ->
    751752        (fun _ ->
    752           let sk = find_label_always l (Cminor_syntax.f_body f) Kend f en in
     753          let sk = find_label_always l f.Cminor_syntax.f_body Kend f en in
    753754          Obj.magic
    754755            (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     
    767768       (let { Types.fst = m'; Types.snd = sp } =
    768769          GenMem.alloc m (Z.z_of_nat Nat.O)
    769             (Z.z_of_nat (Cminor_syntax.f_stacksize f))
     770            (Z.z_of_nat f.Cminor_syntax.f_stacksize)
    770771        in
    771772       Obj.magic
    772773         (Monad.m_bind0 (Monad.max_def Errors.res0)
    773            (Obj.magic (bind_params args (Cminor_syntax.f_params f)))
    774            (fun en ->
     774           (Obj.magic (bind_params args f.Cminor_syntax.f_params)) (fun en ->
    775775           Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    776              Events.e0; Types.snd = (State (f, (Cminor_syntax.f_body f),
    777              (init_locals (Types.pi1 en) (Cminor_syntax.f_vars f)), m', sp,
     776             Events.e0; Types.snd = (State (f, f.Cminor_syntax.f_body,
     777             (init_locals (Types.pi1 en) f.Cminor_syntax.f_vars), m', sp,
    778778             Kend, st0)) })))
    779779   | AST.External fn ->
     
    782782         (Obj.magic
    783783           (IOMonad.err_to_io
    784              (IO.check_eventval_list args (AST.sig_args (AST.ef_sig fn)))))
     784             (IO.check_eventval_list args fn.AST.ef_sig.AST.sig_args)))
    785785         (fun evargs ->
    786786         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    787787           (Obj.magic
    788              (IO.do_io (AST.ef_id fn) evargs
    789                (AST.proj_sig_res (AST.ef_sig fn)))) (fun evres ->
     788             (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
     789           (fun evres ->
    790790           let res =
    791              match AST.sig_res (AST.ef_sig fn) with
     791             match fn.AST.ef_sig.AST.sig_res with
    792792             | Types.None -> Types.None
    793793             | Types.Some x0 ->
    794                Types.Some
    795                  (IO.mk_val (AST.proj_sig_res (AST.ef_sig fn)) evres)
     794               Types.Some (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)
    796795           in
    797796           Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
    798              (Events.eextcall (AST.ef_id fn) evargs
    799                (IO.mk_eventval (AST.proj_sig_res (AST.ef_sig fn)) evres));
     797             (Events.eextcall fn.AST.ef_id evargs
     798               (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
    800799             Types.snd = (Returnstate (res, m, st0)) }))))
    801800| Returnstate (result, m, st0) ->
     
    880879        (Obj.magic
    881880          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    882             (Globalenvs.find_symbol ge (AST.prog_main p)))) (fun b ->
     881            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
    883882        Monad.m_bind0 (Monad.max_def Errors.res0)
    884883          (Obj.magic
    885884            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    886885              (Globalenvs.find_funct_ptr ge b))) (fun f ->
    887           Obj.magic (Errors.OK (Callstate ((AST.prog_main p), f, List.Nil, m,
     886          Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
    888887            SStop)))))))
    889888
     
    910909        (Obj.magic
    911910          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    912             (Globalenvs.find_symbol ge (AST.prog_main p)))) (fun b ->
     911            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
    913912        Monad.m_bind0 (Monad.max_def Errors.res0)
    914913          (Obj.magic
    915914            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    916915              (Globalenvs.find_funct_ptr ge b))) (fun f ->
    917           Obj.magic (Errors.OK (Callstate ((AST.prog_main p), f, List.Nil, m,
     916          Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
    918917            SStop)))))))
    919918
Note: See TracChangeset for help on using the changeset viewer.