Changeset 2649 for extracted/aST.mli


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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/aST.mli

    r2601 r2649  
    1313open Arithmetic
    1414
    15 open Char
    16 
    17 open String
    18 
    1915open Vector
    2016
     
    4339open Integers
    4440
    45 open Coqlib
    46 
    47 open Floats
    48 
    4941open Proper
    5042
     
    5345open Deqsets
    5446
     47open ErrorMessages
     48
    5549open PreIdentifiers
    5650
     
    7064
    7165open Identifiers
    72 
    73 val symbolTag : String.string
    7466
    7567type ident = PreIdentifiers.identifier
     
    351343| Init_int16 of bvint
    352344| Init_int32 of bvint
    353 | Init_float32 of Floats.float
    354 | Init_float64 of Floats.float
    355345| Init_space of Nat.nat
    356346| Init_null
     
    358348
    359349val init_data_rect_Type4 :
    360   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
    361   -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
    362   'a1) -> init_data -> 'a1
     350  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
     351  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
    363352
    364353val init_data_rect_Type5 :
    365   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
    366   -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
    367   'a1) -> init_data -> 'a1
     354  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
     355  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
    368356
    369357val init_data_rect_Type3 :
    370   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
    371   -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
    372   'a1) -> init_data -> 'a1
     358  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
     359  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
    373360
    374361val init_data_rect_Type2 :
    375   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
    376   -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
    377   'a1) -> init_data -> 'a1
     362  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
     363  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
    378364
    379365val init_data_rect_Type1 :
    380   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
    381   -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
    382   'a1) -> init_data -> 'a1
     366  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
     367  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
    383368
    384369val init_data_rect_Type0 :
    385   (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Floats.float -> 'a1)
    386   -> (Floats.float -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> (ident -> Nat.nat ->
    387   'a1) -> init_data -> 'a1
     370  (bvint -> 'a1) -> (bvint -> 'a1) -> (bvint -> 'a1) -> (Nat.nat -> 'a1) ->
     371  'a1 -> (ident -> Nat.nat -> 'a1) -> init_data -> 'a1
    388372
    389373val init_data_inv_rect_Type4 :
    390374  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    391   -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
    392   (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1) ->
    393   'a1
     375  -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
     376  -> 'a1) -> 'a1
    394377
    395378val init_data_inv_rect_Type3 :
    396379  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    397   -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
    398   (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1) ->
    399   'a1
     380  -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
     381  -> 'a1) -> 'a1
    400382
    401383val init_data_inv_rect_Type2 :
    402384  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    403   -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
    404   (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1) ->
    405   'a1
     385  -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
     386  -> 'a1) -> 'a1
    406387
    407388val init_data_inv_rect_Type1 :
    408389  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    409   -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
    410   (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1) ->
    411   'a1
     390  -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
     391  -> 'a1) -> 'a1
    412392
    413393val init_data_inv_rect_Type0 :
    414394  init_data -> (bvint -> __ -> 'a1) -> (bvint -> __ -> 'a1) -> (bvint -> __
    415   -> 'a1) -> (Floats.float -> __ -> 'a1) -> (Floats.float -> __ -> 'a1) ->
    416   (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __ -> 'a1) ->
    417   'a1
     395  -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> 'a1) -> (ident -> Nat.nat -> __
     396  -> 'a1) -> 'a1
    418397
    419398val init_data_discr : init_data -> init_data -> __
     
    499478
    500479val transf_program_gen :
    501   String.string -> Identifiers.universe -> (Identifiers.universe -> 'a1 ->
    502   ('a2, Identifiers.universe) Types.prod) -> (ident, 'a1) Types.prod
    503   List.list -> ((ident, 'a2) Types.prod List.list, Identifiers.universe)
    504   Types.prod
     480  PreIdentifiers.identifierTag -> Identifiers.universe ->
     481  (Identifiers.universe -> 'a1 -> ('a2, Identifiers.universe) Types.prod) ->
     482  (ident, 'a1) Types.prod List.list -> ((ident, 'a2) Types.prod List.list,
     483  Identifiers.universe) Types.prod
    505484
    506485val transform_program_gen :
    507   String.string -> Identifiers.universe -> ('a1, 'a3) program -> (ident
    508   List.list -> Identifiers.universe -> 'a1 -> ('a2, Identifiers.universe)
    509   Types.prod) -> (('a2, 'a3) program, Identifiers.universe) Types.prod
     486  PreIdentifiers.identifierTag -> Identifiers.universe -> ('a1, 'a3) program
     487  -> (ident List.list -> Identifiers.universe -> 'a1 -> ('a2,
     488  Identifiers.universe) Types.prod) -> (('a2, 'a3) program,
     489  Identifiers.universe) Types.prod
    510490
    511491val map_partial :
Note: See TracChangeset for help on using the changeset viewer.