Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (8 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/frontEndOps.ml

    r2649 r2717  
    1818
    1919open Division
     20
     21open Exp
    2022
    2123open Arithmetic
     
    9799    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    98100    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    99 let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9741 = function
    100 | Ointconst (sz, sg, x_9743) -> h_Ointconst sz sg x_9743
    101 | Oaddrsymbol (x_9745, x_9744) -> h_Oaddrsymbol x_9745 x_9744
    102 | Oaddrstack x_9746 -> h_Oaddrstack x_9746
     101let rec constant_rect_Type4 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13057 = function
     102| Ointconst (sz, sg, x_13059) -> h_Ointconst sz sg x_13059
     103| Oaddrsymbol (x_13061, x_13060) -> h_Oaddrsymbol x_13061 x_13060
     104| Oaddrstack x_13062 -> h_Oaddrstack x_13062
    103105
    104106(** val constant_rect_Type5 :
    105107    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    106108    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    107 let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9750 = function
    108 | Ointconst (sz, sg, x_9752) -> h_Ointconst sz sg x_9752
    109 | Oaddrsymbol (x_9754, x_9753) -> h_Oaddrsymbol x_9754 x_9753
    110 | Oaddrstack x_9755 -> h_Oaddrstack x_9755
     109let rec constant_rect_Type5 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13066 = function
     110| Ointconst (sz, sg, x_13068) -> h_Ointconst sz sg x_13068
     111| Oaddrsymbol (x_13070, x_13069) -> h_Oaddrsymbol x_13070 x_13069
     112| Oaddrstack x_13071 -> h_Oaddrstack x_13071
    111113
    112114(** val constant_rect_Type3 :
    113115    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    114116    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    115 let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9759 = function
    116 | Ointconst (sz, sg, x_9761) -> h_Ointconst sz sg x_9761
    117 | Oaddrsymbol (x_9763, x_9762) -> h_Oaddrsymbol x_9763 x_9762
    118 | Oaddrstack x_9764 -> h_Oaddrstack x_9764
     117let rec constant_rect_Type3 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13075 = function
     118| Ointconst (sz, sg, x_13077) -> h_Ointconst sz sg x_13077
     119| Oaddrsymbol (x_13079, x_13078) -> h_Oaddrsymbol x_13079 x_13078
     120| Oaddrstack x_13080 -> h_Oaddrstack x_13080
    119121
    120122(** val constant_rect_Type2 :
    121123    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    122124    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    123 let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9768 = function
    124 | Ointconst (sz, sg, x_9770) -> h_Ointconst sz sg x_9770
    125 | Oaddrsymbol (x_9772, x_9771) -> h_Oaddrsymbol x_9772 x_9771
    126 | Oaddrstack x_9773 -> h_Oaddrstack x_9773
     125let rec constant_rect_Type2 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13084 = function
     126| Ointconst (sz, sg, x_13086) -> h_Ointconst sz sg x_13086
     127| Oaddrsymbol (x_13088, x_13087) -> h_Oaddrsymbol x_13088 x_13087
     128| Oaddrstack x_13089 -> h_Oaddrstack x_13089
    127129
    128130(** val constant_rect_Type1 :
    129131    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    130132    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    131 let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9777 = function
    132 | Ointconst (sz, sg, x_9779) -> h_Ointconst sz sg x_9779
    133 | Oaddrsymbol (x_9781, x_9780) -> h_Oaddrsymbol x_9781 x_9780
    134 | Oaddrstack x_9782 -> h_Oaddrstack x_9782
     133let rec constant_rect_Type1 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13093 = function
     134| Ointconst (sz, sg, x_13095) -> h_Ointconst sz sg x_13095
     135| Oaddrsymbol (x_13097, x_13096) -> h_Oaddrsymbol x_13097 x_13096
     136| Oaddrstack x_13098 -> h_Oaddrstack x_13098
    135137
    136138(** val constant_rect_Type0 :
    137139    (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
    138140    Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1 **)
    139 let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_9786 = function
    140 | Ointconst (sz, sg, x_9788) -> h_Ointconst sz sg x_9788
    141 | Oaddrsymbol (x_9790, x_9789) -> h_Oaddrsymbol x_9790 x_9789
    142 | Oaddrstack x_9791 -> h_Oaddrstack x_9791
     141let rec constant_rect_Type0 h_Ointconst h_Oaddrsymbol h_Oaddrstack x_13102 = function
     142| Ointconst (sz, sg, x_13104) -> h_Ointconst sz sg x_13104
     143| Oaddrsymbol (x_13106, x_13105) -> h_Oaddrsymbol x_13106 x_13105
     144| Oaddrstack x_13107 -> h_Oaddrstack x_13107
    143145
    144146(** val constant_inv_rect_Type4 :
     
    209211    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    210212    unary_operation -> 'a1 **)
    211 let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9861 x_9860 = function
     213let rec unary_operation_rect_Type4 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13177 x_13176 = function
    212214| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    213215| Onegint (sz, sg) -> h_Onegint sz sg
     
    225227    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    226228    unary_operation -> 'a1 **)
    227 let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9872 x_9871 = function
     229let rec unary_operation_rect_Type5 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13188 x_13187 = function
    228230| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    229231| Onegint (sz, sg) -> h_Onegint sz sg
     
    241243    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    242244    unary_operation -> 'a1 **)
    243 let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9883 x_9882 = function
     245let rec unary_operation_rect_Type3 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13199 x_13198 = function
    244246| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    245247| Onegint (sz, sg) -> h_Onegint sz sg
     
    257259    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    258260    unary_operation -> 'a1 **)
    259 let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9894 x_9893 = function
     261let rec unary_operation_rect_Type2 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13210 x_13209 = function
    260262| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    261263| Onegint (sz, sg) -> h_Onegint sz sg
     
    273275    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    274276    unary_operation -> 'a1 **)
    275 let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9905 x_9904 = function
     277let rec unary_operation_rect_Type1 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13221 x_13220 = function
    276278| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    277279| Onegint (sz, sg) -> h_Onegint sz sg
     
    289291    (AST.intsize -> AST.signedness -> 'a1) -> AST.typ -> AST.typ ->
    290292    unary_operation -> 'a1 **)
    291 let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_9916 x_9915 = function
     293let rec unary_operation_rect_Type0 h_Ocastint h_Onegint h_Onotbool h_Onotint h_Oid h_Optrofint h_Ointofptr x_13232 x_13231 = function
    292294| Ocastint (sz, sg, sz', sg') -> h_Ocastint sz sg sz' sg'
    293295| Onegint (sz, sg) -> h_Onegint sz sg
     
    424426    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    425427    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    426 let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10021 x_10020 x_10019 = function
     428let rec binary_operation_rect_Type4 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13337 x_13336 x_13335 = function
    427429| Oadd (sz, sg) -> h_Oadd sz sg
    428430| Osub (sz, sg) -> h_Osub sz sg
     
    438440| Oshr (sz, sg) -> h_Oshr sz sg
    439441| Oshru (sz, sg) -> h_Oshru sz sg
    440 | Ocmp (sz, sg, sg', x_10023) -> h_Ocmp sz sg sg' x_10023
    441 | Ocmpu (sz, sg', x_10024) -> h_Ocmpu sz sg' x_10024
     442| Ocmp (sz, sg, sg', x_13339) -> h_Ocmp sz sg sg' x_13339
     443| Ocmpu (sz, sg', x_13340) -> h_Ocmpu sz sg' x_13340
    442444| Oaddpi sz -> h_Oaddpi sz
    443445| Oaddip sz -> h_Oaddip sz
    444446| Osubpi sz -> h_Osubpi sz
    445447| Osubpp sz -> h_Osubpp sz
    446 | Ocmpp (sg', x_10025) -> h_Ocmpp sg' x_10025
     448| Ocmpp (sg', x_13341) -> h_Ocmpp sg' x_13341
    447449
    448450(** val binary_operation_rect_Type5 :
     
    459461    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    460462    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    461 let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10048 x_10047 x_10046 = function
     463let rec binary_operation_rect_Type5 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13364 x_13363 x_13362 = function
    462464| Oadd (sz, sg) -> h_Oadd sz sg
    463465| Osub (sz, sg) -> h_Osub sz sg
     
    473475| Oshr (sz, sg) -> h_Oshr sz sg
    474476| Oshru (sz, sg) -> h_Oshru sz sg
    475 | Ocmp (sz, sg, sg', x_10050) -> h_Ocmp sz sg sg' x_10050
    476 | Ocmpu (sz, sg', x_10051) -> h_Ocmpu sz sg' x_10051
     477| Ocmp (sz, sg, sg', x_13366) -> h_Ocmp sz sg sg' x_13366
     478| Ocmpu (sz, sg', x_13367) -> h_Ocmpu sz sg' x_13367
    477479| Oaddpi sz -> h_Oaddpi sz
    478480| Oaddip sz -> h_Oaddip sz
    479481| Osubpi sz -> h_Osubpi sz
    480482| Osubpp sz -> h_Osubpp sz
    481 | Ocmpp (sg', x_10052) -> h_Ocmpp sg' x_10052
     483| Ocmpp (sg', x_13368) -> h_Ocmpp sg' x_13368
    482484
    483485(** val binary_operation_rect_Type3 :
     
    494496    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    495497    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    496 let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10075 x_10074 x_10073 = function
     498let rec binary_operation_rect_Type3 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13391 x_13390 x_13389 = function
    497499| Oadd (sz, sg) -> h_Oadd sz sg
    498500| Osub (sz, sg) -> h_Osub sz sg
     
    508510| Oshr (sz, sg) -> h_Oshr sz sg
    509511| Oshru (sz, sg) -> h_Oshru sz sg
    510 | Ocmp (sz, sg, sg', x_10077) -> h_Ocmp sz sg sg' x_10077
    511 | Ocmpu (sz, sg', x_10078) -> h_Ocmpu sz sg' x_10078
     512| Ocmp (sz, sg, sg', x_13393) -> h_Ocmp sz sg sg' x_13393
     513| Ocmpu (sz, sg', x_13394) -> h_Ocmpu sz sg' x_13394
    512514| Oaddpi sz -> h_Oaddpi sz
    513515| Oaddip sz -> h_Oaddip sz
    514516| Osubpi sz -> h_Osubpi sz
    515517| Osubpp sz -> h_Osubpp sz
    516 | Ocmpp (sg', x_10079) -> h_Ocmpp sg' x_10079
     518| Ocmpp (sg', x_13395) -> h_Ocmpp sg' x_13395
    517519
    518520(** val binary_operation_rect_Type2 :
     
    529531    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    530532    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    531 let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10102 x_10101 x_10100 = function
     533let rec binary_operation_rect_Type2 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13418 x_13417 x_13416 = function
    532534| Oadd (sz, sg) -> h_Oadd sz sg
    533535| Osub (sz, sg) -> h_Osub sz sg
     
    543545| Oshr (sz, sg) -> h_Oshr sz sg
    544546| Oshru (sz, sg) -> h_Oshru sz sg
    545 | Ocmp (sz, sg, sg', x_10104) -> h_Ocmp sz sg sg' x_10104
    546 | Ocmpu (sz, sg', x_10105) -> h_Ocmpu sz sg' x_10105
     547| Ocmp (sz, sg, sg', x_13420) -> h_Ocmp sz sg sg' x_13420
     548| Ocmpu (sz, sg', x_13421) -> h_Ocmpu sz sg' x_13421
    547549| Oaddpi sz -> h_Oaddpi sz
    548550| Oaddip sz -> h_Oaddip sz
    549551| Osubpi sz -> h_Osubpi sz
    550552| Osubpp sz -> h_Osubpp sz
    551 | Ocmpp (sg', x_10106) -> h_Ocmpp sg' x_10106
     553| Ocmpp (sg', x_13422) -> h_Ocmpp sg' x_13422
    552554
    553555(** val binary_operation_rect_Type1 :
     
    564566    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    565567    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    566 let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10129 x_10128 x_10127 = function
     568let rec binary_operation_rect_Type1 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13445 x_13444 x_13443 = function
    567569| Oadd (sz, sg) -> h_Oadd sz sg
    568570| Osub (sz, sg) -> h_Osub sz sg
     
    578580| Oshr (sz, sg) -> h_Oshr sz sg
    579581| Oshru (sz, sg) -> h_Oshru sz sg
    580 | Ocmp (sz, sg, sg', x_10131) -> h_Ocmp sz sg sg' x_10131
    581 | Ocmpu (sz, sg', x_10132) -> h_Ocmpu sz sg' x_10132
     582| Ocmp (sz, sg, sg', x_13447) -> h_Ocmp sz sg sg' x_13447
     583| Ocmpu (sz, sg', x_13448) -> h_Ocmpu sz sg' x_13448
    582584| Oaddpi sz -> h_Oaddpi sz
    583585| Oaddip sz -> h_Oaddip sz
    584586| Osubpi sz -> h_Osubpi sz
    585587| Osubpp sz -> h_Osubpp sz
    586 | Ocmpp (sg', x_10133) -> h_Ocmpp sg' x_10133
     588| Ocmpp (sg', x_13449) -> h_Ocmpp sg' x_13449
    587589
    588590(** val binary_operation_rect_Type0 :
     
    599601    (AST.intsize -> 'a1) -> (AST.signedness -> Integers.comparison -> 'a1) ->
    600602    AST.typ -> AST.typ -> AST.typ -> binary_operation -> 'a1 **)
    601 let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_10156 x_10155 x_10154 = function
     603let rec binary_operation_rect_Type0 h_Oadd h_Osub h_Omul h_Odiv h_Odivu h_Omod h_Omodu h_Oand h_Oor h_Oxor h_Oshl h_Oshr h_Oshru h_Ocmp h_Ocmpu h_Oaddpi h_Oaddip h_Osubpi h_Osubpp h_Ocmpp x_13472 x_13471 x_13470 = function
    602604| Oadd (sz, sg) -> h_Oadd sz sg
    603605| Osub (sz, sg) -> h_Osub sz sg
     
    613615| Oshr (sz, sg) -> h_Oshr sz sg
    614616| Oshru (sz, sg) -> h_Oshru sz sg
    615 | Ocmp (sz, sg, sg', x_10158) -> h_Ocmp sz sg sg' x_10158
    616 | Ocmpu (sz, sg', x_10159) -> h_Ocmpu sz sg' x_10159
     617| Ocmp (sz, sg, sg', x_13474) -> h_Ocmp sz sg sg' x_13474
     618| Ocmpu (sz, sg', x_13475) -> h_Ocmpu sz sg' x_13475
    617619| Oaddpi sz -> h_Oaddpi sz
    618620| Oaddip sz -> h_Oaddip sz
    619621| Osubpi sz -> h_Osubpi sz
    620622| Osubpp sz -> h_Osubpp sz
    621 | Ocmpp (sg', x_10160) -> h_Ocmpp sg' x_10160
     623| Ocmpp (sg', x_13476) -> h_Ocmpp sg' x_13476
    622624
    623625(** val binary_operation_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.