Changeset 2951 for extracted/lIN.ml


Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/lIN.ml

    r2773 r2951  
    11open Preamble
     2
     3open Extra_bool
     4
     5open Coqlib
     6
     7open Values
     8
     9open FrontEndVal
     10
     11open GenMem
     12
     13open FrontEndMem
     14
     15open Globalenvs
    216
    317open String
     
    113127type lin_program = Joint.joint_program
    114128
     129(** val lIN_premain : lin_program -> Joint.joint_closed_internal_function **)
     130let lIN_premain p =
     131  let l3 = Positive.P1 Positive.One in
     132  let code = List.Cons ({ Types.fst = Types.None; Types.snd =
     133    (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
     134    (Obj.magic Types.It))) }, (List.Cons ({ Types.fst = Types.None;
     135    Types.snd = (Joint.Sequential ((Joint.CALL ((Types.Inl
     136    p.Joint.joint_prog.AST.prog_main),
     137    (Obj.magic (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
     138    (Obj.magic Types.It))), (Obj.magic Types.It))) }, (List.Cons
     139    ({ Types.fst = (Types.Some l3); Types.snd = (Joint.Final (Joint.GOTO
     140    l3)) }, List.Nil)))))
     141  in
     142  { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0 Positive.One));
     143  Joint.joint_if_runiverse = Positive.One; Joint.joint_if_result =
     144  (Obj.magic Types.It); Joint.joint_if_params = (Obj.magic Types.It);
     145  Joint.joint_if_stacksize = Nat.O; Joint.joint_if_local_stacksize = Nat.O;
     146  Joint.joint_if_code = (Obj.magic code); Joint.joint_if_entry =
     147  (Obj.magic Nat.O) }
     148
Note: See TracChangeset for help on using the changeset viewer.