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/linearise.ml

    r2827 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
     
    318332
    319333(** val linearise :
    320     Joint.uns_params -> (Joint.joint_function, Nat.nat) AST.program ->
    321     (Joint.joint_function, Nat.nat) AST.program **)
     334    Joint.uns_params -> Joint.joint_program -> Joint.joint_program **)
    322335let linearise p pr =
    323   AST.transform_program pr (fun globals ->
    324     AST.transf_fundef (fun f_in ->
    325       (Types.pi1 (linearise_int_fun p globals f_in)).Types.fst))
    326 
     336  { Joint.joint_prog =
     337    (AST.transform_program pr.Joint.joint_prog (fun globals ->
     338      AST.transf_fundef (fun f_in ->
     339        (Types.pi1 (linearise_int_fun p globals f_in)).Types.fst)));
     340    Joint.init_cost_label = pr.Joint.init_cost_label }
     341
Note: See TracChangeset for help on using the changeset viewer.