Changeset 2649 for extracted/label.ml


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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/label.ml

    r2601 r2649  
    33open CostLabel
    44
     5open Coqlib
     6
    57open Proper
    68
     
    911open Deqsets
    1012
     13open ErrorMessages
     14
    1115open PreIdentifiers
    1216
     
    2731open Identifiers
    2832
    29 open Coqlib
    30 
    31 open Floats
    32 
    3333open Arithmetic
    34 
    35 open Char
    36 
    37 open String
    3834
    3935open Vector
     
    168164let add_cost_before s gen =
    169165  let { Types.fst = l; Types.snd = gen0 } =
    170     Identifiers.fresh CostLabel.costTag gen
     166    Identifiers.fresh PreIdentifiers.CostTag gen
    171167  in
    172168  { Types.fst = (Csyntax.Scost (l, s)); Types.snd = gen0 }
     
    177173let add_cost_after s gen =
    178174  let { Types.fst = l; Types.snd = gen0 } =
    179     Identifiers.fresh CostLabel.costTag gen
     175    Identifiers.fresh PreIdentifiers.CostTag gen
    180176  in
    181177  { Types.fst = (Csyntax.Ssequence (s, (Csyntax.Scost (l, Csyntax.Sskip))));
     
    187183let add_cost_expr e0 gen =
    188184  let { Types.fst = l; Types.snd = gen0 } =
    189     Identifiers.fresh CostLabel.costTag gen
     185    Identifiers.fresh PreIdentifiers.CostTag gen
    190186  in
    191187  { Types.fst = (Csyntax.Expr ((Csyntax.Ecost (l, e0)),
     
    702698    Types.prod **)
    703699let clight_label p =
    704   let costgen = Identifiers.new_universe CostLabel.costTag in
     700  let costgen = Identifiers.new_universe PreIdentifiers.CostTag in
    705701  let { Types.fst = init_cost; Types.snd = costgen0 } =
    706     Identifiers.fresh CostLabel.costTag costgen
     702    Identifiers.fresh PreIdentifiers.CostTag costgen
    707703  in
    708704  { Types.fst =
    709   (AST.transform_program_gen CostLabel.costTag costgen0 p (fun x ->
     705  (AST.transform_program_gen PreIdentifiers.CostTag costgen0 p (fun x ->
    710706    label_fundef)).Types.fst; Types.snd = init_cost }
    711707
Note: See TracChangeset for help on using the changeset viewer.