Changeset 2649 for extracted/csyntax.ml


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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/csyntax.ml

    r2601 r2649  
    77open Deqsets
    88
     9open ErrorMessages
     10
    911open PreIdentifiers
    1012
     
    2527open Identifiers
    2628
     29open Arithmetic
     30
     31open Vector
     32
     33open Div_and_mod
     34
     35open Jmeq
     36
     37open Russell
     38
     39open List
     40
     41open Util
     42
     43open FoldStuff
     44
     45open BitVector
     46
     47open Extranat
     48
     49open Bool
     50
     51open Relations
     52
     53open Nat
     54
     55open Integers
     56
     57open Hints_declaration
     58
     59open Core_notation
     60
     61open Pts
     62
     63open Logic
     64
     65open Types
     66
     67open AST
     68
    2769open Coqlib
    28 
    29 open Floats
    30 
    31 open Arithmetic
    32 
    33 open Char
    34 
    35 open String
    36 
    37 open Vector
    38 
    39 open Div_and_mod
    40 
    41 open Jmeq
    42 
    43 open Russell
    44 
    45 open List
    46 
    47 open Util
    48 
    49 open FoldStuff
    50 
    51 open BitVector
    52 
    53 open Extranat
    54 
    55 open Bool
    56 
    57 open Relations
    58 
    59 open Nat
    60 
    61 open Integers
    62 
    63 open Hints_declaration
    64 
    65 open Core_notation
    66 
    67 open Pts
    68 
    69 open Logic
    70 
    71 open Types
    72 
    73 open AST
    7470
    7571open CostLabel
     
    12051201    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12061202    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1207 let rec function_rect_Type4 h_mk_function x_3416 =
     1203let rec function_rect_Type4 h_mk_function x_2206 =
    12081204  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1209     fn_body = fn_body0 } = x_3416
     1205    fn_body = fn_body0 } = x_2206
    12101206  in
    12111207  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12141210    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12151211    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1216 let rec function_rect_Type5 h_mk_function x_3418 =
     1212let rec function_rect_Type5 h_mk_function x_2208 =
    12171213  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1218     fn_body = fn_body0 } = x_3418
     1214    fn_body = fn_body0 } = x_2208
    12191215  in
    12201216  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12231219    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12241220    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1225 let rec function_rect_Type3 h_mk_function x_3420 =
     1221let rec function_rect_Type3 h_mk_function x_2210 =
    12261222  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1227     fn_body = fn_body0 } = x_3420
     1223    fn_body = fn_body0 } = x_2210
    12281224  in
    12291225  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12321228    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12331229    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1234 let rec function_rect_Type2 h_mk_function x_3422 =
     1230let rec function_rect_Type2 h_mk_function x_2212 =
    12351231  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1236     fn_body = fn_body0 } = x_3422
     1232    fn_body = fn_body0 } = x_2212
    12371233  in
    12381234  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12411237    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12421238    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1243 let rec function_rect_Type1 h_mk_function x_3424 =
     1239let rec function_rect_Type1 h_mk_function x_2214 =
    12441240  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1245     fn_body = fn_body0 } = x_3424
     1241    fn_body = fn_body0 } = x_2214
    12461242  in
    12471243  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    12501246    (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
    12511247    Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1 **)
    1252 let rec function_rect_Type0 h_mk_function x_3426 =
     1248let rec function_rect_Type0 h_mk_function x_2216 =
    12531249  let { fn_return = fn_return0; fn_params = fn_params0; fn_vars = fn_vars0;
    1254     fn_body = fn_body0 } = x_3426
     1250    fn_body = fn_body0 } = x_2216
    12551251  in
    12561252  h_mk_function fn_return0 fn_params0 fn_vars0 fn_body0
     
    13241320    clight_fundef -> 'a1 **)
    13251321let rec clight_fundef_rect_Type4 h_CL_Internal h_CL_External = function
    1326 | CL_Internal x_3448 -> h_CL_Internal x_3448
    1327 | CL_External (x_3451, x_3450, x_3449) -> h_CL_External x_3451 x_3450 x_3449
     1322| CL_Internal x_2238 -> h_CL_Internal x_2238
     1323| CL_External (x_2241, x_2240, x_2239) -> h_CL_External x_2241 x_2240 x_2239
    13281324
    13291325(** val clight_fundef_rect_Type5 :
     
    13311327    clight_fundef -> 'a1 **)
    13321328let rec clight_fundef_rect_Type5 h_CL_Internal h_CL_External = function
    1333 | CL_Internal x_3455 -> h_CL_Internal x_3455
    1334 | CL_External (x_3458, x_3457, x_3456) -> h_CL_External x_3458 x_3457 x_3456
     1329| CL_Internal x_2245 -> h_CL_Internal x_2245
     1330| CL_External (x_2248, x_2247, x_2246) -> h_CL_External x_2248 x_2247 x_2246
    13351331
    13361332(** val clight_fundef_rect_Type3 :
     
    13381334    clight_fundef -> 'a1 **)
    13391335let rec clight_fundef_rect_Type3 h_CL_Internal h_CL_External = function
    1340 | CL_Internal x_3462 -> h_CL_Internal x_3462
    1341 | CL_External (x_3465, x_3464, x_3463) -> h_CL_External x_3465 x_3464 x_3463
     1336| CL_Internal x_2252 -> h_CL_Internal x_2252
     1337| CL_External (x_2255, x_2254, x_2253) -> h_CL_External x_2255 x_2254 x_2253
    13421338
    13431339(** val clight_fundef_rect_Type2 :
     
    13451341    clight_fundef -> 'a1 **)
    13461342let rec clight_fundef_rect_Type2 h_CL_Internal h_CL_External = function
    1347 | CL_Internal x_3469 -> h_CL_Internal x_3469
    1348 | CL_External (x_3472, x_3471, x_3470) -> h_CL_External x_3472 x_3471 x_3470
     1343| CL_Internal x_2259 -> h_CL_Internal x_2259
     1344| CL_External (x_2262, x_2261, x_2260) -> h_CL_External x_2262 x_2261 x_2260
    13491345
    13501346(** val clight_fundef_rect_Type1 :
     
    13521348    clight_fundef -> 'a1 **)
    13531349let rec clight_fundef_rect_Type1 h_CL_Internal h_CL_External = function
    1354 | CL_Internal x_3476 -> h_CL_Internal x_3476
    1355 | CL_External (x_3479, x_3478, x_3477) -> h_CL_External x_3479 x_3478 x_3477
     1350| CL_Internal x_2266 -> h_CL_Internal x_2266
     1351| CL_External (x_2269, x_2268, x_2267) -> h_CL_External x_2269 x_2268 x_2267
    13561352
    13571353(** val clight_fundef_rect_Type0 :
     
    13591355    clight_fundef -> 'a1 **)
    13601356let rec clight_fundef_rect_Type0 h_CL_Internal h_CL_External = function
    1361 | CL_Internal x_3483 -> h_CL_Internal x_3483
    1362 | CL_External (x_3486, x_3485, x_3484) -> h_CL_External x_3486 x_3485 x_3484
     1357| CL_Internal x_2273 -> h_CL_Internal x_2273
     1358| CL_External (x_2276, x_2275, x_2274) -> h_CL_External x_2276 x_2275 x_2274
    13631359
    13641360(** val clight_fundef_inv_rect_Type4 :
     
    14721468| Fcons (id, t, fld') -> Nat.max (sizeof t) (sizeof_union fld')
    14731469
    1474 (** val unknownField : String.string **)
    1475 let unknownField = "unknown field"
    1476   (*failwith "AXIOM TO BE REALIZED"*)
    1477 
    14781470(** val field_offset_rec :
    14791471    AST.ident -> fieldlist -> Nat.nat -> Nat.nat Errors.res **)
     
    14811473  match fld with
    14821474  | Fnil ->
    1483     Errors.Error (List.Cons ((Errors.MSG unknownField), (List.Cons
    1484       ((Errors.CTX (AST.symbolTag, id)), List.Nil))))
     1475    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
     1476      (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
    14851477  | Fcons (id', t, fld') ->
    14861478    (match AST.ident_eq id id' with
     
    14971489let rec field_type id = function
    14981490| Fnil ->
    1499   Errors.Error (List.Cons ((Errors.MSG unknownField), (List.Cons ((Errors.CTX
    1500     (AST.symbolTag, id)), List.Nil))))
     1491  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.UnknownField),
     1492    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil))))
    15011493| Fcons (id', t, fld') ->
    15021494  (match AST.ident_eq id id' with
     
    15391531(** val mode_rect_Type4 :
    15401532    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1541 let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_3536 = function
     1533let rec mode_rect_Type4 h_By_value h_By_reference h_By_nothing x_2326 = function
    15421534| By_value t -> h_By_value t
    15431535| By_reference -> h_By_reference
     
    15461538(** val mode_rect_Type5 :
    15471539    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1548 let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_3541 = function
     1540let rec mode_rect_Type5 h_By_value h_By_reference h_By_nothing x_2331 = function
    15491541| By_value t -> h_By_value t
    15501542| By_reference -> h_By_reference
     
    15531545(** val mode_rect_Type3 :
    15541546    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1555 let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_3546 = function
     1547let rec mode_rect_Type3 h_By_value h_By_reference h_By_nothing x_2336 = function
    15561548| By_value t -> h_By_value t
    15571549| By_reference -> h_By_reference
     
    15601552(** val mode_rect_Type2 :
    15611553    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1562 let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_3551 = function
     1554let rec mode_rect_Type2 h_By_value h_By_reference h_By_nothing x_2341 = function
    15631555| By_value t -> h_By_value t
    15641556| By_reference -> h_By_reference
     
    15671559(** val mode_rect_Type1 :
    15681560    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1569 let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_3556 = function
     1561let rec mode_rect_Type1 h_By_value h_By_reference h_By_nothing x_2346 = function
    15701562| By_value t -> h_By_value t
    15711563| By_reference -> h_By_reference
     
    15741566(** val mode_rect_Type0 :
    15751567    (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1 **)
    1576 let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_3561 = function
     1568let rec mode_rect_Type0 h_By_value h_By_reference h_By_nothing x_2351 = function
    15771569| By_value t -> h_By_value t
    15781570| By_reference -> h_By_reference
Note: See TracChangeset for help on using the changeset viewer.