Changeset 2773 for extracted/cexec.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cexec.ml

    r2730 r2773  
    2828
    2929open Extralib
    30 
    31 open BitVectorTrie
    3230
    3331open CostLabel
     
    178176
    179177(** val try_cast_null :
    180     GenMem.mem1 -> AST.intsize -> BitVector.bitVector -> Csyntax.type0 ->
     178    GenMem.mem -> AST.intsize -> BitVector.bitVector -> Csyntax.type0 ->
    181179    Csyntax.type0 -> Values.val0 Errors.res **)
    182180let try_cast_null m sz i ty ty' =
     
    227225
    228226(** val exec_cast :
    229     GenMem.mem1 -> Values.val0 -> Csyntax.type0 -> Csyntax.type0 ->
     227    GenMem.mem -> Values.val0 -> Csyntax.type0 -> Csyntax.type0 ->
    230228    Values.val0 Errors.res **)
    231229let exec_cast m v ty ty' =
     
    294292
    295293(** val load_value_of_type' :
    296     Csyntax.type0 -> GenMem.mem1 -> (Pointers.block, Pointers.offset)
     294    Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset)
    297295    Types.prod -> Values.val0 Types.option **)
    298296let load_value_of_type' ty m l =
     
    301299
    302300(** val exec_expr :
    303     Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr -> (Values.val0,
     301    Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr -> (Values.val0,
    304302    Events.trace) Types.prod Errors.res **)
    305 let rec exec_expr ge0 en m = function
     303let rec exec_expr ge en m = function
    306304| Csyntax.Expr (e', ty) ->
    307305  (match e' with
     
    332330     Obj.magic
    333331       (Monad.m_bind2 (Monad.max_def Errors.res0)
    334          (Obj.magic (exec_lvalue' ge0 en m e' ty)) (fun l tr ->
     332         (Obj.magic (exec_lvalue' ge en m e' ty)) (fun l tr ->
    335333         Monad.m_bind0 (Monad.max_def Errors.res0)
    336334           (Obj.magic
     
    341339     Obj.magic
    342340       (Monad.m_bind2 (Monad.max_def Errors.res0)
    343          (Obj.magic (exec_lvalue' ge0 en m e' ty)) (fun l tr ->
     341         (Obj.magic (exec_lvalue' ge en m e' ty)) (fun l tr ->
    344342         Monad.m_bind0 (Monad.max_def Errors.res0)
    345343           (Obj.magic
     
    350348     Obj.magic
    351349       (Monad.m_bind2 (Monad.max_def Errors.res0)
    352          (Obj.magic (exec_lvalue ge0 en m a)) (fun lo tr ->
     350         (Obj.magic (exec_lvalue ge en m a)) (fun lo tr ->
    353351         match ty with
    354352         | Csyntax.Tvoid ->
     
    371369         | Csyntax.Tcomp_ptr x ->
    372370           Obj.magic (Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm))))
    373    | Csyntax.Eunop (op0, a) ->
     371   | Csyntax.Eunop (op, a) ->
    374372     Obj.magic
    375373       (Monad.m_bind2 (Monad.max_def Errors.res0)
    376          (Obj.magic (exec_expr ge0 en m a)) (fun v1 tr ->
     374         (Obj.magic (exec_expr ge en m a)) (fun v1 tr ->
    377375         Monad.m_bind0 (Monad.max_def Errors.res0)
    378376           (Obj.magic
    379377             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
    380                (Csem.sem_unary_operation op0 v1 (Csyntax.typeof a))))
     378               (Csem.sem_unary_operation op v1 (Csyntax.typeof a))))
    381379           (fun v -> Obj.magic (Errors.OK { Types.fst = v; Types.snd = tr }))))
    382    | Csyntax.Ebinop (op0, a1, a2) ->
     380   | Csyntax.Ebinop (op, a1, a2) ->
    383381     Obj.magic
    384382       (Monad.m_bind2 (Monad.max_def Errors.res0)
    385          (Obj.magic (exec_expr ge0 en m a1)) (fun v1 tr1 ->
     383         (Obj.magic (exec_expr ge en m a1)) (fun v1 tr1 ->
    386384         Monad.m_bind2 (Monad.max_def Errors.res0)
    387            (Obj.magic (exec_expr ge0 en m a2)) (fun v2 tr2 ->
     385           (Obj.magic (exec_expr ge en m a2)) (fun v2 tr2 ->
    388386           Monad.m_bind0 (Monad.max_def Errors.res0)
    389387             (Obj.magic
    390388               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
    391                  (Csem.sem_binary_operation op0 v1 (Csyntax.typeof a1) v2
     389                 (Csem.sem_binary_operation op v1 (Csyntax.typeof a1) v2
    392390                   (Csyntax.typeof a2) m ty))) (fun v ->
    393391             Obj.magic (Errors.OK { Types.fst = v; Types.snd =
     
    396394     Obj.magic
    397395       (Monad.m_bind2 (Monad.max_def Errors.res0)
    398          (Obj.magic (exec_expr ge0 en m a)) (fun v tr ->
     396         (Obj.magic (exec_expr ge en m a)) (fun v tr ->
    399397         Monad.m_bind0 (Monad.max_def Errors.res0)
    400398           (Obj.magic (exec_cast m v (Csyntax.typeof a) ty')) (fun v' ->
     
    403401     Obj.magic
    404402       (Monad.m_bind2 (Monad.max_def Errors.res0)
    405          (Obj.magic (exec_expr ge0 en m a1)) (fun v tr1 ->
     403         (Obj.magic (exec_expr ge en m a1)) (fun v tr1 ->
    406404         Monad.m_bind0 (Monad.max_def Errors.res0)
    407405           (Obj.magic (exec_bool_of_val v (Csyntax.typeof a1))) (fun b ->
    408406           Monad.m_bind2 (Monad.max_def Errors.res0)
    409407             (match b with
    410               | Bool.True -> Obj.magic (exec_expr ge0 en m a2)
    411               | Bool.False -> Obj.magic (exec_expr ge0 en m a3))
     408              | Bool.True -> Obj.magic (exec_expr ge en m a2)
     409              | Bool.False -> Obj.magic (exec_expr ge en m a3))
    412410             (fun v' tr2 ->
    413411             Obj.magic (Errors.OK { Types.fst = v'; Types.snd =
     
    416414     Obj.magic
    417415       (Monad.m_bind2 (Monad.max_def Errors.res0)
    418          (Obj.magic (exec_expr ge0 en m a1)) (fun v1 tr1 ->
     416         (Obj.magic (exec_expr ge en m a1)) (fun v1 tr1 ->
    419417         Monad.m_bind0 (Monad.max_def Errors.res0)
    420418           (Obj.magic (exec_bool_of_val v1 (Csyntax.typeof a1))) (fun b1 ->
     
    422420           | Bool.True ->
    423421             Monad.m_bind2 (Monad.max_def Errors.res0)
    424                (Obj.magic (exec_expr ge0 en m a2)) (fun v2 tr2 ->
     422               (Obj.magic (exec_expr ge en m a2)) (fun v2 tr2 ->
    425423               Monad.m_bind0 (Monad.max_def Errors.res0)
    426424                 (Obj.magic (exec_bool_of_val v2 (Csyntax.typeof a2)))
     
    444442     Obj.magic
    445443       (Monad.m_bind2 (Monad.max_def Errors.res0)
    446          (Obj.magic (exec_expr ge0 en m a1)) (fun v1 tr1 ->
     444         (Obj.magic (exec_expr ge en m a1)) (fun v1 tr1 ->
    447445         Monad.m_bind0 (Monad.max_def Errors.res0)
    448446           (Obj.magic (exec_bool_of_val v1 (Csyntax.typeof a1))) (fun b1 ->
     
    457455           | Bool.False ->
    458456             Monad.m_bind2 (Monad.max_def Errors.res0)
    459                (Obj.magic (exec_expr ge0 en m a2)) (fun v2 tr2 ->
     457               (Obj.magic (exec_expr ge en m a2)) (fun v2 tr2 ->
    460458               Monad.m_bind0 (Monad.max_def Errors.res0)
    461459                 (Obj.magic (exec_bool_of_val v2 (Csyntax.typeof a2)))
     
    475473      | Csyntax.Tint (sz, x) ->
    476474        Errors.OK { Types.fst = (Values.Vint (sz,
    477           (AST.repr0 sz (Csyntax.sizeof ty')))); Types.snd = Events.e0 }
     475          (AST.repr sz (Csyntax.sizeof ty')))); Types.snd = Events.e0 }
    478476      | Csyntax.Tpointer x ->
    479477        Errors.Error (Errors.msg ErrorMessages.BadlyTypedTerm)
     
    491489     Obj.magic
    492490       (Monad.m_bind2 (Monad.max_def Errors.res0)
    493          (Obj.magic (exec_lvalue' ge0 en m e' ty)) (fun l tr ->
     491         (Obj.magic (exec_lvalue' ge en m e' ty)) (fun l tr ->
    494492         Monad.m_bind0 (Monad.max_def Errors.res0)
    495493           (Obj.magic
     
    500498     Obj.magic
    501499       (Monad.m_bind2 (Monad.max_def Errors.res0)
    502          (Obj.magic (exec_expr ge0 en m a)) (fun v tr ->
     500         (Obj.magic (exec_expr ge en m a)) (fun v tr ->
    503501         Obj.magic (Errors.OK { Types.fst = v; Types.snd =
    504502           (Events.eapp (Events.echarge l) tr) }))))
    505503(** val exec_lvalue' :
    506     Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr_descr ->
     504    Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr_descr ->
    507505    Csyntax.type0 -> ((Pointers.block, Pointers.offset) Types.prod,
    508506    Events.trace) Types.prod Errors.res **)
    509 and exec_lvalue' ge0 en m e' ty =
     507and exec_lvalue' ge en m e' ty =
    510508  match e' with
    511509  | Csyntax.Econst_int (x, x0) ->
    512510    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
    513511  | Csyntax.Evar id ->
    514     (match Identifiers.lookup0 PreIdentifiers.SymbolTag en id with
     512    (match Identifiers.lookup PreIdentifiers.SymbolTag en id with
    515513     | Types.None ->
    516514       Obj.magic
     
    520518               ErrorMessages.UnknownIdentifier), (List.Cons ((Errors.CTX
    521519               (PreIdentifiers.SymbolTag, id)), List.Nil))))
    522                (Globalenvs.find_symbol ge0 id))) (fun l ->
     520               (Globalenvs.find_symbol ge id))) (fun l ->
    523521           Obj.magic (Errors.OK { Types.fst = { Types.fst = l; Types.snd =
    524522             Pointers.zero_offset }; Types.snd = Events.e0 })))
     
    529527    Obj.magic
    530528      (Monad.m_bind2 (Monad.max_def Errors.res0)
    531         (Obj.magic (exec_expr ge0 en m a)) (fun v tr ->
     529        (Obj.magic (exec_expr ge en m a)) (fun v tr ->
    532530        match v with
    533531        | Values.Vundef ->
     
    572570       Obj.magic
    573571         (Monad.m_bind2 (Monad.max_def Errors.res0)
    574            (Obj.magic (exec_lvalue ge0 en m a)) (fun lofs tr ->
     572           (Obj.magic (exec_lvalue ge en m a)) (fun lofs tr ->
    575573           Monad.m_bind0 (Monad.max_def Errors.res0)
    576574             (Obj.magic (Csyntax.field_offset i fList)) (fun delta ->
     
    578576               Types.snd =
    579577               (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
    580                  lofs.Types.snd (AST.repr0 AST.I16 delta)) }; Types.snd =
     578                 lofs.Types.snd (AST.repr AST.I16 delta)) }; Types.snd =
    581579               tr }))))
    582580     | Csyntax.Tunion (id, fList) ->
    583581       Obj.magic
    584582         (Monad.m_bind2 (Monad.max_def Errors.res0)
    585            (Obj.magic (exec_lvalue ge0 en m a)) (fun lofs tr ->
     583           (Obj.magic (exec_lvalue ge en m a)) (fun lofs tr ->
    586584           Obj.magic (Errors.OK { Types.fst = lofs; Types.snd = tr })))
    587585     | Csyntax.Tcomp_ptr x ->
     
    590588    Errors.Error (Errors.msg ErrorMessages.BadLvalueTerm)
    591589(** val exec_lvalue :
    592     Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr ->
    593     ((Pointers.block, Pointers.offset) Types.prod, Events.trace) Types.prod
    594     Errors.res **)
    595 and exec_lvalue ge0 en m = function
    596 | Csyntax.Expr (e', ty) -> exec_lvalue' ge0 en m e' ty
     590    Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr -> ((Pointers.block,
     591    Pointers.offset) Types.prod, Events.trace) Types.prod Errors.res **)
     592and exec_lvalue ge en m = function
     593| Csyntax.Expr (e', ty) -> exec_lvalue' ge en m e' ty
    597594
    598595(** val exec_exprlist :
    599     Csem.genv0 -> Csem.env -> GenMem.mem1 -> Csyntax.expr List.list ->
     596    Csem.genv -> Csem.env -> GenMem.mem -> Csyntax.expr List.list ->
    600597    (Values.val0 List.list, Events.trace) Types.prod Errors.res **)
    601 let rec exec_exprlist ge0 e1 m = function
     598let rec exec_exprlist ge e m = function
    602599| List.Nil -> Errors.OK { Types.fst = List.Nil; Types.snd = Events.e0 }
    603 | List.Cons (e2, es) ->
     600| List.Cons (e1, es) ->
    604601  Obj.magic
    605602    (Monad.m_bind2 (Monad.max_def Errors.res0)
    606       (Obj.magic (exec_expr ge0 e1 m e2)) (fun v tr1 ->
     603      (Obj.magic (exec_expr ge e m e1)) (fun v tr1 ->
    607604      Monad.m_bind2 (Monad.max_def Errors.res0)
    608         (Obj.magic (exec_exprlist ge0 e1 m es)) (fun vs tr2 ->
     605        (Obj.magic (exec_exprlist ge e m es)) (fun vs tr2 ->
    609606        Obj.magic (Errors.OK { Types.fst = (List.Cons (v, vs)); Types.snd =
    610607          (Events.eapp tr1 tr2) }))))
    611608
    612609(** val exec_alloc_variables :
    613     Csem.env -> GenMem.mem1 -> (AST.ident, Csyntax.type0) Types.prod
    614     List.list -> (Csem.env, GenMem.mem1) Types.prod **)
     610    Csem.env -> GenMem.mem -> (AST.ident, Csyntax.type0) Types.prod List.list
     611    -> (Csem.env, GenMem.mem) Types.prod **)
    615612let rec exec_alloc_variables en m = function
    616613| List.Nil -> { Types.fst = en; Types.snd = m }
     
    624621
    625622(** val exec_bind_parameters :
    626     Csem.env -> GenMem.mem1 -> (AST.ident, Csyntax.type0) Types.prod
    627     List.list -> Values.val0 List.list -> GenMem.mem1 Errors.res **)
    628 let rec exec_bind_parameters e1 m params vs =
     623    Csem.env -> GenMem.mem -> (AST.ident, Csyntax.type0) Types.prod List.list
     624    -> Values.val0 List.list -> GenMem.mem Errors.res **)
     625let rec exec_bind_parameters e m params vs =
    629626  match params with
    630627  | List.Nil ->
     
    645642               ErrorMessages.UnknownIdentifier), (List.Cons ((Errors.CTX
    646643               (PreIdentifiers.SymbolTag, id)), List.Nil))))
    647                (Identifiers.lookup0 PreIdentifiers.SymbolTag e1 id)))
    648            (fun b ->
     644               (Identifiers.lookup PreIdentifiers.SymbolTag e id))) (fun b ->
    649645           Monad.m_bind0 (Monad.max_def Errors.res0)
    650646             (Obj.magic
     
    653649                 (PreIdentifiers.SymbolTag, id)), List.Nil))))
    654650                 (Csem.store_value_of_type ty m b Pointers.zero_offset v1)))
    655              (fun m1 -> Obj.magic (exec_bind_parameters e1 m1 params' vl)))))
     651             (fun m1 -> Obj.magic (exec_bind_parameters e m1 params' vl)))))
    656652
    657653(** val is_is_call_cont : Csem.cont -> (__, __) Types.sum **)
     
    685681
    686682(** val store_value_of_type' :
    687     Csyntax.type0 -> GenMem.mem1 -> (Pointers.block, Pointers.offset)
    688     Types.prod -> Values.val0 -> GenMem.mem1 Types.option **)
     683    Csyntax.type0 -> GenMem.mem -> (Pointers.block, Pointers.offset)
     684    Types.prod -> Values.val0 -> GenMem.mem Types.option **)
    689685let store_value_of_type' ty m l v =
    690686  let { Types.fst = loc; Types.snd = ofs } = l in
     
    692688
    693689(** val exec_step :
    694     Csem.genv0 -> Csem.state0 -> (IO.io_out, IO.io_in, (Events.trace,
    695     Csem.state0) Types.prod) IOMonad.iO **)
    696 let rec exec_step ge0 = function
    697 | Csem.State (f, s, k, e1, m) ->
     690    Csem.genv -> Csem.state -> (IO.io_out, IO.io_in, (Events.trace,
     691    Csem.state) Types.prod) IOMonad.iO **)
     692let rec exec_step ge = function
     693| Csem.State (f, s, k, e, m) ->
    698694  (match s with
    699695   | Csyntax.Sskip ->
     
    704700           IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Returnstate
    705701             (Values.Vundef, k,
    706              (GenMem.free_list m (Csem.blocks_of_env e1)))) }
     702             (GenMem.free_list m (Csem.blocks_of_env e)))) }
    707703         | Csyntax.Tint (x, x0) ->
    708704           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     
    721717      | Csem.Kseq (s0, k') ->
    722718        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s0, k',
    723           e1, m)) }
     719          e, m)) }
    724720      | Csem.Kwhile (a, s', k') ->
    725721        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    726           (Csyntax.Swhile (a, s')), k', e1, m)) }
     722          (Csyntax.Swhile (a, s')), k', e, m)) }
    727723      | Csem.Kdowhile (a, s', k') ->
    728724        Obj.magic
    729725          (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    730             (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
     726            (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
    731727            (fun v tr ->
    732728            Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
     
    738734                Obj.magic
    739735                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
    740                     (Csyntax.Sdowhile (a, s')), k', e1, m)) })
     736                    (Csyntax.Sdowhile (a, s')), k', e, m)) })
    741737              | Bool.False ->
    742738                Obj.magic
    743739                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
    744                     Csyntax.Sskip, k', e1, m)) }))))
     740                    Csyntax.Sskip, k', e, m)) }))))
    745741      | Csem.Kfor2 (a2, a3, s', k') ->
    746742        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, a3,
    747           (Csem.Kfor3 (a2, a3, s', k')), e1, m)) }
     743          (Csem.Kfor3 (a2, a3, s', k')), e, m)) }
    748744      | Csem.Kfor3 (a2, a3, s', k') ->
    749745        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    750           (Csyntax.Sfor (Csyntax.Sskip, a2, a3, s')), k', e1, m)) }
     746          (Csyntax.Sfor (Csyntax.Sskip, a2, a3, s')), k', e, m)) }
    751747      | Csem.Kswitch k' ->
    752748        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    753           Csyntax.Sskip, k', e1, m)) }
     749          Csyntax.Sskip, k', e, m)) }
    754750      | Csem.Kcall (x, x0, x1, x2) ->
    755751        (match f.Csyntax.fn_return with
     
    757753           IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Returnstate
    758754             (Values.Vundef, k,
    759              (GenMem.free_list m (Csem.blocks_of_env e1)))) }
     755             (GenMem.free_list m (Csem.blocks_of_env e)))) }
    760756         | Csyntax.Tint (x3, x4) ->
    761757           IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
     
    775771     Obj.magic
    776772       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    777          (let x = IOMonad.err_to_io (exec_lvalue ge0 e1 m a1) in Obj.magic x)
     773         (let x = IOMonad.err_to_io (exec_lvalue ge e m a1) in Obj.magic x)
    778774         (fun l tr1 ->
    779775         Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    780            (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a2) in Obj.magic x)
     776           (let x = IOMonad.err_to_io (exec_expr ge e m a2) in Obj.magic x)
    781777           (fun v2 tr2 ->
    782778           Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
     
    787783             Obj.magic
    788784               (IO.ret { Types.fst = (Events.eapp tr1 tr2); Types.snd =
    789                  (Csem.State (f, Csyntax.Sskip, k, e1, m')) })))))
     785                 (Csem.State (f, Csyntax.Sskip, k, e, m')) })))))
    790786   | Csyntax.Scall (lhs, a, al) ->
    791787     Obj.magic
    792788       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    793          (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
     789         (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
    794790         (fun vf tr2 ->
    795791         Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    796            (let x = IOMonad.err_to_io (exec_exprlist ge0 e1 m al) in
     792           (let x = IOMonad.err_to_io (exec_exprlist ge e m al) in
    797793           Obj.magic x) (fun vargs tr3 ->
    798794           Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    799795             (Obj.magic
    800796               (IOMonad.opt_to_io (Errors.msg ErrorMessages.BadFunctionValue)
    801                  (Globalenvs.find_funct_id ge0 vf))) (fun fd id ->
     797                 (Globalenvs.find_funct_id ge vf))) (fun fd id ->
    802798             Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    803799               (Obj.magic
     
    810806                   (IO.ret { Types.fst = (Events.eapp tr2 tr3); Types.snd =
    811807                     (Csem.Callstate (id, fd, vargs, (Csem.Kcall (Types.None,
    812                      f, e1, k)), m)) })
     808                     f, e, k)), m)) })
    813809               | Types.Some lhs' ->
    814810                 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    815                    (let x = IOMonad.err_to_io (exec_lvalue ge0 e1 m lhs') in
     811                   (let x = IOMonad.err_to_io (exec_lvalue ge e m lhs') in
    816812                   Obj.magic x) (fun locofs tr1 ->
    817813                   Obj.magic
     
    820816                       (Csem.Callstate (id, fd, vargs, (Csem.Kcall
    821817                       ((Types.Some { Types.fst = locofs; Types.snd =
    822                        (Csyntax.typeof lhs') }), f, e1, k)), m)) })))))))
     818                       (Csyntax.typeof lhs') }), f, e, k)), m)) })))))))
    823819   | Csyntax.Ssequence (s1, s2) ->
    824820     IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s1,
    825        (Csem.Kseq (s2, k)), e1, m)) }
     821       (Csem.Kseq (s2, k)), e, m)) }
    826822   | Csyntax.Sifthenelse (a, s1, s2) ->
    827823     Obj.magic
    828824       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    829          (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
     825         (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
    830826         (fun v tr ->
    831827         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
     
    837833               (match b with
    838834                | Bool.True -> s1
    839                 | Bool.False -> s2), k, e1, m)) }))))
     835                | Bool.False -> s2), k, e, m)) }))))
    840836   | Csyntax.Swhile (a, s') ->
    841837     Obj.magic
    842838       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    843          (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
     839         (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
    844840         (fun v tr ->
    845841         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
     
    851847               (match b with
    852848                | Bool.True ->
    853                   Csem.State (f, s', (Csem.Kwhile (a, s', k)), e1, m)
    854                 | Bool.False -> Csem.State (f, Csyntax.Sskip, k, e1, m)) }))))
     849                  Csem.State (f, s', (Csem.Kwhile (a, s', k)), e, m)
     850                | Bool.False -> Csem.State (f, Csyntax.Sskip, k, e, m)) }))))
    855851   | Csyntax.Sdowhile (a, s') ->
    856852     IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s',
    857        (Csem.Kdowhile (a, s', k)), e1, m)) }
     853       (Csem.Kdowhile (a, s', k)), e, m)) }
    858854   | Csyntax.Sfor (a1, a2, a3, s') ->
    859855     (match is_Sskip a1 with
     
    861857        Obj.magic
    862858          (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    863             (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a2) in
    864             Obj.magic x) (fun v tr ->
     859            (let x = IOMonad.err_to_io (exec_expr ge e m a2) in Obj.magic x)
     860            (fun v tr ->
    865861            Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    866862              (Obj.magic
     
    874870                  (match b with
    875871                   | Bool.True -> Csem.Kfor2 (a2, a3, s', k)
    876                    | Bool.False -> k), e1, m)) }))))
     872                   | Bool.False -> k), e, m)) }))))
    877873      | Types.Inr _ ->
    878874        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, a1,
    879           (Csem.Kseq ((Csyntax.Sfor (Csyntax.Sskip, a2, a3, s')), k)), e1,
     875          (Csem.Kseq ((Csyntax.Sfor (Csyntax.Sskip, a2, a3, s')), k)), e,
    880876          m)) })
    881877   | Csyntax.Sbreak ->
     
    884880      | Csem.Kseq (s', k') ->
    885881        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    886           Csyntax.Sbreak, k', e1, m)) }
     882          Csyntax.Sbreak, k', e, m)) }
    887883      | Csem.Kwhile (a, s', k') ->
    888884        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    889           Csyntax.Sskip, k', e1, m)) }
     885          Csyntax.Sskip, k', e, m)) }
    890886      | Csem.Kdowhile (a, s', k') ->
    891887        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    892           Csyntax.Sskip, k', e1, m)) }
     888          Csyntax.Sskip, k', e, m)) }
    893889      | Csem.Kfor2 (a2, a3, s', k') ->
    894890        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    895           Csyntax.Sskip, k', e1, m)) }
     891          Csyntax.Sskip, k', e, m)) }
    896892      | Csem.Kfor3 (x, x0, x1, x2) ->
    897893        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    898894      | Csem.Kswitch k' ->
    899895        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    900           Csyntax.Sskip, k', e1, m)) }
     896          Csyntax.Sskip, k', e, m)) }
    901897      | Csem.Kcall (x, x0, x1, x2) ->
    902898        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState))
     
    906902      | Csem.Kseq (s', k') ->
    907903        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    908           Csyntax.Scontinue, k', e1, m)) }
     904          Csyntax.Scontinue, k', e, m)) }
    909905      | Csem.Kwhile (a, s', k') ->
    910906        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    911           (Csyntax.Swhile (a, s')), k', e1, m)) }
     907          (Csyntax.Swhile (a, s')), k', e, m)) }
    912908      | Csem.Kdowhile (a, s', k') ->
    913909        Obj.magic
    914910          (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    915             (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
     911            (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
    916912            (fun v tr ->
    917913            Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
     
    923919                Obj.magic
    924920                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
    925                     (Csyntax.Sdowhile (a, s')), k', e1, m)) })
     921                    (Csyntax.Sdowhile (a, s')), k', e, m)) })
    926922              | Bool.False ->
    927923                Obj.magic
    928924                  (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
    929                     Csyntax.Sskip, k', e1, m)) }))))
     925                    Csyntax.Sskip, k', e, m)) }))))
    930926      | Csem.Kfor2 (a2, a3, s', k') ->
    931927        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, a3,
    932           (Csem.Kfor3 (a2, a3, s', k')), e1, m)) }
     928          (Csem.Kfor3 (a2, a3, s', k')), e, m)) }
    933929      | Csem.Kfor3 (x, x0, x1, x2) ->
    934930        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    935931      | Csem.Kswitch k' ->
    936932        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    937           Csyntax.Scontinue, k', e1, m)) }
     933          Csyntax.Scontinue, k', e, m)) }
    938934      | Csem.Kcall (x, x0, x1, x2) ->
    939935        IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState))
     
    945941           IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Returnstate
    946942             (Values.Vundef, (Csem.call_cont k),
    947              (GenMem.free_list m (Csem.blocks_of_env e1)))) }
     943             (GenMem.free_list m (Csem.blocks_of_env e)))) }
    948944         | Csyntax.Tint (x, x0) ->
    949945           IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
     
    967963           Obj.magic
    968964             (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    969                (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in
     965               (let x = IOMonad.err_to_io (exec_expr ge e m a) in
    970966               Obj.magic x) (fun v tr ->
    971967               Obj.magic
    972968                 (IO.ret { Types.fst = tr; Types.snd = (Csem.Returnstate (v,
    973969                   (Csem.call_cont k),
    974                    (GenMem.free_list m (Csem.blocks_of_env e1)))) })))))
     970                   (GenMem.free_list m (Csem.blocks_of_env e)))) })))))
    975971   | Csyntax.Sswitch (a, sl) ->
    976972     Obj.magic
    977973       (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    978          (let x = IOMonad.err_to_io (exec_expr ge0 e1 m a) in Obj.magic x)
     974         (let x = IOMonad.err_to_io (exec_expr ge e m a) in Obj.magic x)
    979975         (fun v tr ->
    980976         match v with
     
    997993                     (IO.ret { Types.fst = tr; Types.snd = (Csem.State (f,
    998994                       (Csem.seq_of_labeled_statement sl'), (Csem.Kswitch k),
    999                        e1, m)) }))
     995                       e, m)) }))
    1000996               | Types.Inr _ ->
    1001997                 Obj.magic (IOMonad.Wrong
     
    10241020           Obj.magic (IOMonad.Wrong (Errors.msg ErrorMessages.TypeMismatch))))
    10251021   | Csyntax.Slabel (lbl, s') ->
    1026      IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s', k, e1,
     1022     IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s', k, e,
    10271023       m)) }
    10281024   | Csyntax.Sgoto lbl ->
     
    10351031        let { Types.fst = s'; Types.snd = k' } = sk' in
    10361032        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f, s', k',
    1037           e1, m)) })
     1033          e, m)) })
    10381034   | Csyntax.Scost (lbl, s') ->
    10391035     IO.ret { Types.fst = (Events.echarge lbl); Types.snd = (Csem.State (f,
    1040        s', k, e1, m)) })
     1036       s', k, e, m)) })
    10411037| Csem.Callstate (x, f0, vargs, k, m) ->
    10421038  (match f0 with
    10431039   | Csyntax.CL_Internal f ->
    1044      let { Types.fst = e1; Types.snd = m1 } =
     1040     let { Types.fst = e; Types.snd = m1 } =
    10451041       exec_alloc_variables Csem.empty_env m
    10461042         (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
     
    10501046         (let x0 =
    10511047            IOMonad.err_to_io
    1052               (exec_bind_parameters e1 m1 f.Csyntax.fn_params vargs)
     1048              (exec_bind_parameters e m1 f.Csyntax.fn_params vargs)
    10531049          in
    10541050         Obj.magic x0) (fun m2 ->
    10551051         Obj.magic
    10561052           (IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    1057              f.Csyntax.fn_body, k, e1, m2)) })))
     1053             f.Csyntax.fn_body, k, e, m2)) })))
    10581054   | Csyntax.CL_External (f, argtys, retty) ->
    10591055     Obj.magic
     
    10801076                  (AST.proj_sig_res (Csyntax.signature_of_type argtys retty))
    10811077                  evres), k, m)) })))))
    1082 | Csem.Returnstate (res1, k, m) ->
     1078| Csem.Returnstate (res, k, m) ->
    10831079  (match k with
    10841080   | Csem.Kstop ->
    1085      (match res1 with
     1081     (match res with
    10861082      | Values.Vundef ->
    10871083        IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
     
    10931089           (fun x -> IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch))
    10941090         | AST.I32 ->
    1095            (fun r5 ->
     1091           (fun r0 ->
    10961092             IO.ret { Types.fst = Events.e0; Types.snd = (Csem.Finalstate
    1097                r5) })) r
     1093               r0) })) r
    10981094      | Values.Vnull ->
    10991095        IOMonad.Wrong (Errors.msg ErrorMessages.ReturnMismatch)
     
    11111107     IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    11121108   | Csem.Kswitch x -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    1113    | Csem.Kcall (r, f, e1, k') ->
     1109   | Csem.Kcall (r, f, e, k') ->
    11141110     (match r with
    11151111      | Types.None ->
    11161112        IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    1117           Csyntax.Sskip, k', e1, m)) }
     1113          Csyntax.Sskip, k', e, m)) }
    11181114      | Types.Some r' ->
    11191115        let { Types.fst = l; Types.snd = ty } = r' in
     
    11221118            (Obj.magic
    11231119              (IOMonad.opt_to_io (Errors.msg ErrorMessages.FailedStore)
    1124                 (store_value_of_type' ty m l res1))) (fun m' ->
     1120                (store_value_of_type' ty m l res))) (fun m' ->
    11251121            Obj.magic
    11261122              (IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
    1127                 Csyntax.Sskip, k', e1, m')) })))))
     1123                Csyntax.Sskip, k', e, m')) })))))
    11281124| Csem.Finalstate r -> IOMonad.Wrong (Errors.msg ErrorMessages.NonsenseState)
    11291125
    1130 (** val make_global0 : Csyntax.clight_program -> Csem.genv0 **)
    1131 let make_global0 p =
     1126(** val make_global : Csyntax.clight_program -> Csem.genv **)
     1127let make_global p =
    11321128  Globalenvs.globalenv Types.fst p
    11331129
    1134 (** val make_initial_state0 :
    1135     Csyntax.clight_program -> Csem.state0 Errors.res **)
    1136 let rec make_initial_state0 p =
    1137   let ge0 = make_global0 p in
     1130(** val make_initial_state :
     1131    Csyntax.clight_program -> Csem.state Errors.res **)
     1132let rec make_initial_state p =
     1133  let ge = make_global p in
    11381134  Obj.magic
    11391135    (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    11421138        (Obj.magic
    11431139          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    1144             (Globalenvs.find_symbol ge0 p.AST.prog_main))) (fun b ->
     1140            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
    11451141        Monad.m_bind0 (Monad.max_def Errors.res0)
    11461142          (Obj.magic
    11471143            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    1148               (Globalenvs.find_funct_ptr ge0 b))) (fun f ->
     1144              (Globalenvs.find_funct_ptr ge b))) (fun f ->
    11491145          Obj.magic (Errors.OK (Csem.Callstate (p.AST.prog_main, f, List.Nil,
    11501146            Csem.Kstop, m0)))))))
    11511147
    1152 (** val is_final0 : Csem.state0 -> Integers.int Types.option **)
    1153 let rec is_final0 = function
     1148(** val is_final : Csem.state -> Integers.int Types.option **)
     1149let rec is_final = function
    11541150| Csem.State (x, x0, x1, x2, x3) -> Types.None
    11551151| Csem.Callstate (x, x0, x1, x2, x3) -> Types.None
     
    11581154
    11591155(** val is_final_state :
    1160     Csem.state0 -> (Integers.int Types.sig0, __) Types.sum **)
     1156    Csem.state -> (Integers.int Types.sig0, __) Types.sum **)
    11611157let is_final_state st =
    1162   Csem.state_rect_Type0 (fun f s k e1 m -> Types.Inr __) (fun vf f l k m ->
     1158  Csem.state_rect_Type0 (fun f s k e m -> Types.Inr __) (fun vf f l k m ->
    11631159    Types.Inr __) (fun v k m -> Types.Inr __) (fun r -> Types.Inl r) st
    11641160
    1165 (** val exec_steps0 :
    1166     Nat.nat -> Csem.genv0 -> Csem.state0 -> (IO.io_out, IO.io_in,
    1167     (Events.trace, Csem.state0) Types.prod) IOMonad.iO **)
    1168 let rec exec_steps0 n ge0 s =
     1161(** val exec_steps :
     1162    Nat.nat -> Csem.genv -> Csem.state -> (IO.io_out, IO.io_in,
     1163    (Events.trace, Csem.state) Types.prod) IOMonad.iO **)
     1164let rec exec_steps n ge s =
    11691165  match is_final_state s with
    11701166  | Types.Inl x -> IO.ret { Types.fst = Events.e0; Types.snd = s }
     
    11751171       Obj.magic
    11761172         (Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    1177            (Obj.magic (exec_step ge0 s)) (fun t s' ->
     1173           (Obj.magic (exec_step ge s)) (fun t s' ->
    11781174           Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    1179              (Obj.magic (exec_steps0 n' ge0 s')) (fun t' s'' ->
     1175             (Obj.magic (exec_steps n' ge s')) (fun t' s'' ->
    11801176             Obj.magic
    11811177               (IO.ret { Types.fst = (Events.eapp t t'); Types.snd = s'' })))))
     
    11831179(** val clight_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
    11841180let clight_exec =
    1185   { SmallstepExec.is_final = (fun x -> Obj.magic is_final0);
     1181  { SmallstepExec.is_final = (fun x -> Obj.magic is_final);
    11861182    SmallstepExec.step = (Obj.magic exec_step) }
    11871183
     
    11891185let clight_fullexec =
    11901186  { SmallstepExec.es1 = clight_exec; SmallstepExec.make_global =
    1191     (Obj.magic make_global0); SmallstepExec.make_initial_state =
    1192     (Obj.magic make_initial_state0) }
    1193 
     1187    (Obj.magic make_global); SmallstepExec.make_initial_state =
     1188    (Obj.magic make_initial_state) }
     1189
Note: See TracChangeset for help on using the changeset viewer.