Changeset 2717 for extracted/cexec.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cexec.ml

    r2649 r2717  
    2929open Extralib
    3030
     31open BitVectorTrie
     32
    3133open CostLabel
    3234
     
    4446
    4547open Division
     48
     49open Exp
    4650
    4751open Arithmetic
     
    805809                 Obj.magic
    806810                   (IO.ret { Types.fst = (Events.eapp tr2 tr3); Types.snd =
    807                      (Csem.Callstate (fd, vargs, (Csem.Kcall (Types.None, f,
    808                      e1, k)), m)) })
     811                     (Csem.Callstate (vf, fd, vargs, (Csem.Kcall (Types.None,
     812                     f, e1, k)), m)) })
    809813               | Types.Some lhs' ->
    810814                 Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
     
    814818                     (IO.ret { Types.fst =
    815819                       (Events.eapp tr1 (Events.eapp tr2 tr3)); Types.snd =
    816                        (Csem.Callstate (fd, vargs, (Csem.Kcall ((Types.Some
    817                        { Types.fst = locofs; Types.snd =
     820                       (Csem.Callstate (vf, fd, vargs, (Csem.Kcall
     821                       ((Types.Some { Types.fst = locofs; Types.snd =
    818822                       (Csyntax.typeof lhs') }), f, e1, k)), m)) })))))))
    819823   | Csyntax.Ssequence (s1, s2) ->
     
    10351039     IO.ret { Types.fst = (Events.echarge lbl); Types.snd = (Csem.State (f,
    10361040       s', k, e1, m)) })
    1037 | Csem.Callstate (f0, vargs, k, m) ->
     1041| Csem.Callstate (x, f0, vargs, k, m) ->
    10381042  (match f0 with
    10391043   | Csyntax.CL_Internal f ->
     
    10441048     Obj.magic
    10451049       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    1046          (let x =
     1050         (let x0 =
    10471051            IOMonad.err_to_io
    10481052              (exec_bind_parameters e1 m1 f.Csyntax.fn_params vargs)
    10491053          in
    1050          Obj.magic x) (fun m2 ->
     1054         Obj.magic x0) (fun m2 ->
    10511055         Obj.magic
    10521056           (IO.ret { Types.fst = Events.e0; Types.snd = (Csem.State (f,
     
    10551059     Obj.magic
    10561060       (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    1057          (let x =
     1061         (let x0 =
    10581062            IOMonad.err_to_io
    10591063              (IO.check_eventval_list vargs
    10601064                (Csyntax.typlist_of_typelist argtys))
    10611065          in
    1062          Obj.magic x) (fun evargs ->
     1066         Obj.magic x0) (fun evargs ->
    10631067         Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
    10641068           (Obj.magic
     
    11431147            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    11441148              (Globalenvs.find_funct_ptr ge0 b))) (fun f ->
    1145           Obj.magic (Errors.OK (Csem.Callstate (f, List.Nil, Csem.Kstop,
    1146             m0)))))))
     1149          Obj.magic (Errors.OK (Csem.Callstate ((Values.Vptr
     1150            { Pointers.pblock = b; Pointers.poff = Pointers.zero_offset }),
     1151            f, List.Nil, Csem.Kstop, m0)))))))
    11471152
    11481153(** val is_final0 : Csem.state0 -> Integers.int Types.option **)
    11491154let rec is_final0 = function
    11501155| Csem.State (x, x0, x1, x2, x3) -> Types.None
    1151 | Csem.Callstate (x, x0, x1, x2) -> Types.None
     1156| Csem.Callstate (x, x0, x1, x2, x3) -> Types.None
    11521157| Csem.Returnstate (x, x0, x1) -> Types.None
    11531158| Csem.Finalstate r -> Types.Some r
     
    11561161    Csem.state0 -> (Integers.int Types.sig0, __) Types.sum **)
    11571162let is_final_state st =
    1158   Csem.state_rect_Type0 (fun f s k e1 m -> Types.Inr __) (fun f l k m ->
     1163  Csem.state_rect_Type0 (fun f s k e1 m -> Types.Inr __) (fun vf f l k m ->
    11591164    Types.Inr __) (fun v k m -> Types.Inr __) (fun r -> Types.Inl r) st
    11601165
    1161 (** val exec_steps :
     1166(** val exec_steps0 :
    11621167    Nat.nat -> Csem.genv0 -> Csem.state0 -> (IO.io_out, IO.io_in,
    11631168    (Events.trace, Csem.state0) Types.prod) IOMonad.iO **)
    1164 let rec exec_steps n ge0 s =
     1169let rec exec_steps0 n ge0 s =
    11651170  match is_final_state s with
    11661171  | Types.Inl x -> IO.ret { Types.fst = Events.e0; Types.snd = s }
     
    11731178           (Obj.magic (exec_step ge0 s)) (fun t s' ->
    11741179           Monad.m_bind2 (Monad.max_def IOMonad.iOMonad)
    1175              (Obj.magic (exec_steps n' ge0 s')) (fun t' s'' ->
     1180             (Obj.magic (exec_steps0 n' ge0 s')) (fun t' s'' ->
    11761181             Obj.magic
    11771182               (IO.ret { Types.fst = (Events.eapp t t'); Types.snd = s'' })))))
Note: See TracChangeset for help on using the changeset viewer.