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/fixpoints.mli

    r2773 r2951  
    140140
    141141type fixpoint =
    142   equations -> valuation
     142  valuation
    143143  (* singleton inductive, whose constructor was mk_fixpoint *)
    144144
    145145val fixpoint_rect_Type4 :
    146   property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint ->
     146  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
    147147  'a1
    148148
    149149val fixpoint_rect_Type5 :
    150   property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint ->
     150  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
    151151  'a1
    152152
    153153val fixpoint_rect_Type3 :
    154   property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint ->
     154  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
    155155  'a1
    156156
    157157val fixpoint_rect_Type2 :
    158   property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint ->
     158  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
    159159  'a1
    160160
    161161val fixpoint_rect_Type1 :
    162   property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint ->
     162  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
    163163  'a1
    164164
    165165val fixpoint_rect_Type0 :
    166   property_lattice -> ((equations -> valuation) -> __ -> 'a1) -> fixpoint ->
    167   'a1
    168 
    169 val fix_lfp : property_lattice -> fixpoint -> equations -> valuation
     166  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
     167  'a1
     168
     169val fix_lfp : property_lattice -> equations -> fixpoint -> valuation
    170170
    171171val fixpoint_inv_rect_Type4 :
    172   property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
    173   'a1) -> 'a1
     172  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
     173  -> 'a1
    174174
    175175val fixpoint_inv_rect_Type3 :
    176   property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
    177   'a1) -> 'a1
     176  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
     177  -> 'a1
    178178
    179179val fixpoint_inv_rect_Type2 :
    180   property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
    181   'a1) -> 'a1
     180  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
     181  -> 'a1
    182182
    183183val fixpoint_inv_rect_Type1 :
    184   property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
    185   'a1) -> 'a1
     184  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
     185  -> 'a1
    186186
    187187val fixpoint_inv_rect_Type0 :
    188   property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
    189   'a1) -> 'a1
    190 
    191 val fixpoint_discr : property_lattice -> fixpoint -> fixpoint -> __
    192 
    193 val fixpoint_jmdiscr : property_lattice -> fixpoint -> fixpoint -> __
     188  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
     189  -> 'a1
     190
     191val fixpoint_discr :
     192  property_lattice -> equations -> fixpoint -> fixpoint -> __
     193
     194val fixpoint_jmdiscr :
     195  property_lattice -> equations -> fixpoint -> fixpoint -> __
     196
     197val dpi1__o__fix_lfp__o__inject :
     198  property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
     199  Types.sig0
     200
     201val eject__o__fix_lfp__o__inject :
     202  property_lattice -> equations -> fixpoint Types.sig0 -> valuation
     203  Types.sig0
     204
     205val fix_lfp__o__inject :
     206  property_lattice -> equations -> fixpoint -> valuation Types.sig0
    194207
    195208val dpi1__o__fix_lfp :
    196   property_lattice -> (fixpoint, 'a1) Types.dPair -> equations -> valuation
     209  property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
    197210
    198211val eject__o__fix_lfp :
    199   property_lattice -> fixpoint Types.sig0 -> equations -> valuation
    200 
    201 type fixpoint_computer = property_lattice -> fixpoint
    202 
     212  property_lattice -> equations -> fixpoint Types.sig0 -> valuation
     213
     214type fixpoint_computer = property_lattice -> equations -> fixpoint
     215
     216val dpi1__o__apply_fixpoint :
     217  property_lattice -> equations -> (fixpoint, 'a1) Types.dPair ->
     218  Graphs.label -> __
     219
     220val eject__o__apply_fixpoint :
     221  property_lattice -> equations -> fixpoint Types.sig0 -> Graphs.label -> __
     222
Note: See TracChangeset for help on using the changeset viewer.