Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/cminor_semantics.ml

    r2636 r2649  
    1515open Identifiers
    1616
    17 open Floats
    18 
    1917open Integers
    2018
     
    3937open Pointers
    4038
     39open ErrorMessages
     40
    4141open Option
    4242
     
    4646
    4747open Positive
    48 
    49 open Char
    50 
    51 open String
    5248
    5349open PreIdentifiers
     
    452448     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
    453449
    454 (** val unknownLocal : String.string **)
    455 let unknownLocal = "unknown local"
    456   (*failwith "AXIOM TO BE REALIZED"*)
    457 
    458 (** val failedConstant : String.string **)
    459 let failedConstant = "failed constant"
    460   (*failwith "AXIOM TO BE REALIZED"*)
    461 
    462 (** val failedOp : String.string **)
    463 let failedOp = "failed op"
    464   (*failwith "AXIOM TO BE REALIZED"*)
    465 
    466 (** val failedLoad : String.string **)
    467 let failedLoad = "failed load"
    468   (*failwith "AXIOM TO BE REALIZED"*)
    469 
    470450(** val eval_expr :
    471451    genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block ->
     
    475455   | Cminor_syntax.Id (x, i) ->
    476456     (fun _ ->
    477        let r = Identifiers.lookup_present AST.symbolTag en i in
     457       let r = Identifiers.lookup_present PreIdentifiers.SymbolTag en i in
    478458       Errors.OK { Types.fst = Events.e0; Types.snd = r })
    479459   | Cminor_syntax.Cst (x, c) ->
     
    482462         (Monad.m_bind0 (Monad.max_def Errors.res0)
    483463           (Obj.magic
    484              (Errors.opt_to_res (Errors.msg failedConstant)
     464             (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant)
    485465               (FrontEndOps.eval_constant x (Globalenvs.find_symbol ge) sp c)))
    486466           (fun r ->
     
    493473           Monad.m_bind0 (Monad.max_def Errors.res0)
    494474             (Obj.magic
    495                (Errors.opt_to_res (Errors.msg failedOp)
     475               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
    496476                 (FrontEndOps.eval_unop ty ty' op0 v))) (fun r ->
    497477             Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
     
    505485             Monad.m_bind0 (Monad.max_def Errors.res0)
    506486               (Obj.magic
    507                  (Errors.opt_to_res (Errors.msg failedOp)
     487                 (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
    508488                   (FrontEndOps.eval_binop m ty1 ty2 ty' op0 v1 v2)))
    509489               (fun r ->
     
    517497           Monad.m_bind0 (Monad.max_def Errors.res0)
    518498             (Obj.magic
    519                (Errors.opt_to_res (Errors.msg failedLoad)
     499               (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
    520500                 (FrontEndMem.loadv ty m v))) (fun r ->
    521501             Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
     
    544524             (Events.eapp (Events.echarge l) tr); Types.snd = r }))))) __
    545525
    546 (** val badState : String.string **)
    547 let badState = "bad state"
    548   (*failwith "AXIOM TO BE REALIZED"*)
    549 
    550526(** val k_exit :
    551527    Nat.nat -> cont -> Cminor_syntax.internal_function -> env -> cont
     
    553529let rec k_exit n k f en =
    554530  (match k with
    555    | Kend -> (fun _ -> Errors.Error (Errors.msg badState))
     531   | Kend -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadState))
    556532   | Kseq (x, k') -> (fun _ -> k_exit n k' f en)
    557533   | Kblock k' ->
     
    596572   | Cminor_syntax.St_label (l', s') ->
    597573     (fun _ ->
    598        match Identifiers.identifier_eq Cminor_syntax.label l l' with
     574       match Identifiers.identifier_eq PreIdentifiers.Label l l' with
    599575       | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
    600576       | Types.Inr _ -> find_label l s' k f en)
     
    611587   | Types.Some sk -> (fun _ -> sk)) __
    612588
    613 (** val wrongNumberOfParameters : String.string **)
    614 let wrongNumberOfParameters = "wrong number of parameters"
    615   (*failwith "AXIOM TO BE REALIZED"*)
    616 
    617589(** val bind_params :
    618590    Values.val0 List.list -> (AST.ident, AST.typ) Types.prod List.list -> env
     
    622594  | List.Nil ->
    623595    (match ids with
    624      | List.Nil -> Errors.OK (Identifiers.empty_map AST.symbolTag)
    625      | List.Cons (x, x0) -> Errors.Error (Errors.msg wrongNumberOfParameters))
     596     | List.Nil -> Errors.OK (Identifiers.empty_map PreIdentifiers.SymbolTag)
     597     | List.Cons (x, x0) ->
     598       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
    626599  | List.Cons (v, vt) ->
    627600    (match ids with
    628      | List.Nil -> Errors.Error (Errors.msg wrongNumberOfParameters)
     601     | List.Nil ->
     602       Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
    629603     | List.Cons (idh, idt) ->
    630604       let { Types.fst = id; Types.snd = ty } = idh in
     
    633607           (Obj.magic (bind_params vt idt)) (fun en ->
    634608           Obj.magic (Errors.OK
    635              (Identifiers.add AST.symbolTag (Types.pi1 en) idh.Types.fst v)))))
     609             (Identifiers.add PreIdentifiers.SymbolTag (Types.pi1 en)
     610               idh.Types.fst v)))))
    636611
    637612(** val init_locals :
     
    639614let init_locals =
    640615  List.foldr (fun idty en ->
    641     Identifiers.add AST.symbolTag en idty.Types.fst Values.Vundef)
     616    Identifiers.add PreIdentifiers.SymbolTag en idty.Types.fst Values.Vundef)
    642617
    643618(** val trace_map_inv :
     
    657632             Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr');
    658633               Types.snd = (List.Cons (h', t')) })))))) __
    659 
    660 (** val failedStore : String.string **)
    661 let failedStore = "failed store"
    662   (*failwith "AXIOM TO BE REALIZED"*)
    663 
    664 (** val badFunctionValue : String.string **)
    665 let badFunctionValue = "bad function value"
    666   (*failwith "AXIOM TO BE REALIZED"*)
    667 
    668 (** val returnMismatch : String.string **)
    669 let returnMismatch = "return mismatch"
    670   (*failwith "AXIOM TO BE REALIZED"*)
    671634
    672635(** val eval_step :
     
    703666            (Monad.m_bind2 (Monad.max_def Errors.res0)
    704667              (Obj.magic (eval_expr ge x e1 en sp m)) (fun tr v ->
    705               let en' = Identifiers.update_present AST.symbolTag en id v in
     668              let en' =
     669                Identifiers.update_present PreIdentifiers.SymbolTag en id v
     670              in
    706671              Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
    707672                Types.snd = (State (f, Cminor_syntax.St_skip, en', m, sp, k,
     
    717682                Monad.m_bind0 (Monad.max_def Errors.res0)
    718683                  (Obj.magic
    719                     (Errors.opt_to_res (Errors.msg failedStore)
     684                    (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
    720685                      (FrontEndMem.storev ty m vdst v))) (fun m' ->
    721686                  Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     
    729694              Monad.m_bind0 (Monad.max_def Errors.res0)
    730695                (Obj.magic
    731                   (Errors.opt_to_res (Errors.msg badFunctionValue)
     696                  (Errors.opt_to_res
     697                    (Errors.msg ErrorMessages.BadFunctionValue)
    732698                    (Globalenvs.find_funct ge vf))) (fun fd ->
    733699                Monad.m_bind2 (Monad.max_def Errors.res0)
     
    800766       (let { Types.fst = m'; Types.snd = sp } =
    801767          GenMem.alloc m (Z.z_of_nat Nat.O)
    802             (Z.z_of_nat f.Cminor_syntax.f_stacksize) AST.XData
     768            (Z.z_of_nat f.Cminor_syntax.f_stacksize)
    803769        in
    804770       Obj.magic
     
    835801     | SStop ->
    836802       (match result with
    837         | Types.None -> Errors.Error (Errors.msg returnMismatch)
     803        | Types.None ->
     804          Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
    838805        | Types.Some v ->
    839806          (match v with
    840            | Values.Vundef -> Errors.Error (Errors.msg returnMismatch)
     807           | Values.Vundef ->
     808             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
    841809           | Values.Vint (sz, r) ->
    842810             (match sz with
    843               | AST.I8 -> (fun x -> Errors.Error (Errors.msg returnMismatch))
     811              | AST.I8 ->
     812                (fun x -> Errors.Error
     813                  (Errors.msg ErrorMessages.ReturnMismatch))
    844814              | AST.I16 ->
    845                 (fun x -> Errors.Error (Errors.msg returnMismatch))
     815                (fun x -> Errors.Error
     816                  (Errors.msg ErrorMessages.ReturnMismatch))
    846817              | AST.I32 ->
    847818                (fun r5 ->
     
    850821                      { Types.fst = Events.e0; Types.snd = (Finalstate r5) })))
    851822               r
    852            | Values.Vnull -> Errors.Error (Errors.msg returnMismatch)
    853            | Values.Vptr x -> Errors.Error (Errors.msg returnMismatch)))
     823           | Values.Vnull ->
     824             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
     825           | Values.Vptr x ->
     826             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)))
    854827     | Scall (dst, f, sp, en, k, st') ->
    855828       (match result with
     
    861834                 Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip, en,
    862835                 m, sp, k, st')) })
    863            | Types.Some x -> Errors.Error (Errors.msg returnMismatch))
     836           | Types.Some x ->
     837             Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
    864838        | Types.Some v ->
    865839          (match dst with
    866840           | Types.None ->
    867              (fun _ -> Errors.Error (Errors.msg returnMismatch))
     841             (fun _ -> Errors.Error
     842               (Errors.msg ErrorMessages.ReturnMismatch))
    868843           | Types.Some idty ->
    869844             (fun _ ->
     
    871846                 (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
    872847                   Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
    873                    (Identifiers.update_present AST.symbolTag en
     848                   (Identifiers.update_present PreIdentifiers.SymbolTag en
    874849                     idty.Types.fst v), m, sp, k, st')) }))) __))
    875 | Finalstate r -> IOMonad.err_to_io (Errors.Error (Errors.msg badState))
     850| Finalstate r ->
     851  IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.BadState))
    876852
    877853(** val is_final0 : state0 -> Integers.int Types.option **)
     
    886862  { SmallstepExec.is_final = (fun x -> Obj.magic is_final0);
    887863    SmallstepExec.step = (Obj.magic eval_step) }
    888 
    889 (** val mainMissing : String.string **)
    890 let mainMissing = "main missing"
    891   (*failwith "AXIOM TO BE REALIZED"*)
    892864
    893865(** val make_global0 : Cminor_syntax.cminor_program -> genv **)
     
    904876      Monad.m_bind0 (Monad.max_def Errors.res0)
    905877        (Obj.magic
    906           (Errors.opt_to_res (Errors.msg mainMissing)
     878          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    907879            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
    908880        Monad.m_bind0 (Monad.max_def Errors.res0)
    909881          (Obj.magic
    910             (Errors.opt_to_res (Errors.msg mainMissing)
     882            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    911883              (Globalenvs.find_funct_ptr ge b))) (fun f ->
    912884          Obj.magic (Errors.OK (Callstate (f, List.Nil, m, SStop)))))))
     
    933905      Monad.m_bind0 (Monad.max_def Errors.res0)
    934906        (Obj.magic
    935           (Errors.opt_to_res (Errors.msg mainMissing)
     907          (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    936908            (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
    937909        Monad.m_bind0 (Monad.max_def Errors.res0)
    938910          (Obj.magic
    939             (Errors.opt_to_res (Errors.msg mainMissing)
     911            (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
    940912              (Globalenvs.find_funct_ptr ge b))) (fun f ->
    941913          Obj.magic (Errors.OK (Callstate (f, List.Nil, m, SStop)))))))
Note: See TracChangeset for help on using the changeset viewer.