This file is indexed.

/usr/lib/ats2-postiats-0.1.3/libc/SATS/stdio.sats is in ats2-lang 0.1.3-1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

   1
   2
   3
   4
   5
   6
   7
   8
   9
  10
  11
  12
  13
  14
  15
  16
  17
  18
  19
  20
  21
  22
  23
  24
  25
  26
  27
  28
  29
  30
  31
  32
  33
  34
  35
  36
  37
  38
  39
  40
  41
  42
  43
  44
  45
  46
  47
  48
  49
  50
  51
  52
  53
  54
  55
  56
  57
  58
  59
  60
  61
  62
  63
  64
  65
  66
  67
  68
  69
  70
  71
  72
  73
  74
  75
  76
  77
  78
  79
  80
  81
  82
  83
  84
  85
  86
  87
  88
  89
  90
  91
  92
  93
  94
  95
  96
  97
  98
  99
 100
 101
 102
 103
 104
 105
 106
 107
 108
 109
 110
 111
 112
 113
 114
 115
 116
 117
 118
 119
 120
 121
 122
 123
 124
 125
 126
 127
 128
 129
 130
 131
 132
 133
 134
 135
 136
 137
 138
 139
 140
 141
 142
 143
 144
 145
 146
 147
 148
 149
 150
 151
 152
 153
 154
 155
 156
 157
 158
 159
 160
 161
 162
 163
 164
 165
 166
 167
 168
 169
 170
 171
 172
 173
 174
 175
 176
 177
 178
 179
 180
 181
 182
 183
 184
 185
 186
 187
 188
 189
 190
 191
 192
 193
 194
 195
 196
 197
 198
 199
 200
 201
 202
 203
 204
 205
 206
 207
 208
 209
 210
 211
 212
 213
 214
 215
 216
 217
 218
 219
 220
 221
 222
 223
 224
 225
 226
 227
 228
 229
 230
 231
 232
 233
 234
 235
 236
 237
 238
 239
 240
 241
 242
 243
 244
 245
 246
 247
 248
 249
 250
 251
 252
 253
 254
 255
 256
 257
 258
 259
 260
 261
 262
 263
 264
 265
 266
 267
 268
 269
 270
 271
 272
 273
 274
 275
 276
 277
 278
 279
 280
 281
 282
 283
 284
 285
 286
 287
 288
 289
 290
 291
 292
 293
 294
 295
 296
 297
 298
 299
 300
 301
 302
 303
 304
 305
 306
 307
 308
 309
 310
 311
 312
 313
 314
 315
 316
 317
 318
 319
 320
 321
 322
 323
 324
 325
 326
 327
 328
 329
 330
 331
 332
 333
 334
 335
 336
 337
 338
 339
 340
 341
 342
 343
 344
 345
 346
 347
 348
 349
 350
 351
 352
 353
 354
 355
 356
 357
 358
 359
 360
 361
 362
 363
 364
 365
 366
 367
 368
 369
 370
 371
 372
 373
 374
 375
 376
 377
 378
 379
 380
 381
 382
 383
 384
 385
 386
 387
 388
 389
 390
 391
 392
 393
 394
 395
 396
 397
 398
 399
 400
 401
 402
 403
 404
 405
 406
 407
 408
 409
 410
 411
 412
 413
 414
 415
 416
 417
 418
 419
 420
 421
 422
 423
 424
 425
 426
 427
 428
 429
 430
 431
 432
 433
 434
 435
 436
 437
 438
 439
 440
 441
 442
 443
 444
 445
 446
 447
 448
 449
 450
 451
 452
 453
 454
 455
 456
 457
 458
 459
 460
 461
 462
 463
 464
 465
 466
 467
 468
 469
 470
 471
 472
 473
 474
 475
 476
 477
 478
 479
 480
 481
 482
 483
 484
 485
 486
 487
 488
 489
 490
 491
 492
 493
 494
 495
 496
 497
 498
 499
 500
 501
 502
 503
 504
 505
 506
 507
 508
 509
 510
 511
 512
 513
 514
 515
 516
 517
 518
 519
 520
 521
 522
 523
 524
 525
 526
 527
 528
 529
 530
 531
 532
 533
 534
 535
 536
 537
 538
 539
 540
 541
 542
 543
 544
 545
 546
 547
 548
 549
 550
 551
 552
 553
 554
 555
 556
 557
 558
 559
 560
 561
 562
 563
 564
 565
 566
 567
 568
 569
 570
 571
 572
 573
 574
 575
 576
 577
 578
 579
 580
 581
 582
 583
 584
 585
 586
 587
 588
 589
 590
 591
 592
 593
 594
 595
 596
 597
 598
 599
 600
 601
 602
 603
 604
 605
 606
 607
 608
 609
 610
 611
 612
 613
 614
 615
 616
 617
 618
 619
 620
 621
 622
 623
 624
 625
 626
 627
 628
 629
 630
 631
 632
 633
 634
 635
 636
 637
 638
 639
 640
 641
 642
 643
 644
 645
 646
 647
 648
 649
 650
 651
 652
 653
 654
 655
 656
 657
 658
 659
 660
 661
 662
 663
 664
 665
 666
 667
 668
 669
 670
 671
 672
 673
 674
 675
 676
 677
 678
 679
 680
 681
 682
 683
 684
 685
 686
 687
 688
 689
 690
 691
 692
 693
 694
 695
 696
 697
 698
 699
 700
 701
 702
 703
 704
 705
 706
 707
 708
 709
 710
 711
 712
 713
 714
 715
 716
 717
 718
 719
 720
 721
 722
 723
 724
 725
 726
 727
 728
 729
 730
 731
 732
 733
 734
 735
 736
 737
 738
 739
 740
 741
 742
 743
 744
 745
 746
 747
 748
 749
 750
 751
 752
 753
 754
 755
 756
 757
 758
 759
 760
 761
 762
 763
 764
 765
 766
 767
 768
 769
 770
 771
 772
 773
 774
 775
 776
 777
 778
 779
 780
 781
 782
 783
 784
 785
 786
 787
 788
 789
 790
 791
 792
 793
 794
 795
 796
 797
 798
 799
 800
 801
 802
 803
 804
 805
 806
 807
 808
 809
 810
 811
 812
 813
 814
 815
 816
 817
 818
 819
 820
 821
 822
 823
 824
 825
 826
 827
 828
 829
 830
 831
 832
 833
 834
 835
 836
 837
 838
 839
 840
 841
 842
 843
 844
 845
 846
 847
 848
 849
 850
 851
 852
 853
 854
 855
 856
 857
 858
 859
 860
 861
 862
 863
 864
 865
 866
 867
 868
 869
 870
 871
 872
 873
 874
 875
 876
 877
 878
 879
 880
 881
 882
 883
 884
 885
 886
 887
 888
 889
 890
 891
 892
 893
 894
 895
 896
 897
 898
 899
 900
 901
 902
 903
 904
 905
 906
 907
 908
 909
 910
 911
 912
 913
 914
 915
 916
 917
 918
 919
 920
 921
 922
 923
 924
 925
 926
 927
 928
 929
 930
 931
 932
 933
 934
 935
 936
 937
 938
 939
 940
 941
 942
 943
 944
 945
 946
 947
 948
 949
 950
 951
 952
 953
 954
 955
 956
 957
 958
 959
 960
 961
 962
 963
 964
 965
 966
 967
 968
 969
 970
 971
 972
 973
 974
 975
 976
 977
 978
 979
 980
 981
 982
 983
 984
 985
 986
 987
 988
 989
 990
 991
 992
 993
 994
 995
 996
 997
 998
 999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
** 
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
** 
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)
//
// Author: Hongwei Xi (gmhwxi AT gmail DOT com)
// Start Time: April, 2011
//
(* ****** ****** *)

%{#
#include "libc/CATS/stdio.cats"
%} // end of [%{#]

(* ****** ****** *)

#define ATS_PACKNAME "ATSLIB.libc"
#define ATS_EXTERN_PREFIX "atslib_" // prefix for external names

(* ****** ****** *)

#define RD(x) x // for commenting: read-only
typedef SHR(a:type) = a // for commenting purpose
typedef NSH(a:type) = a // for commenting purpose

(* ****** ****** *)

sortdef fm = file_mode

(* ****** ****** *)

staload
TYPES =
"libc/sys/SATS/types.sats"
stadef fildes = $TYPES.fildes
stadef fildes_v = $TYPES.fildes_v

(* ****** ****** *)

(*
abstype FILEref = ptr // declared in [prelude/basic_dyn.sats]
*)

(* ****** ****** *)
//
// HX-2011-04-02:
//
absview
FILE_view (l:addr, m:fm)
viewdef FILE_v (l:addr, m:fm) = FILE_view (l, m)

absvtype
FILEptr_vtype (addr, fm) = ptr
vtypedef FILEptr (l:addr, m: fm) = FILEptr_vtype (l, m)

(* ****** ****** *)
//
vtypedef
FILEptr0 (m:fm) = [l:addr | l >= null] FILEptr (l, m)
//
vtypedef FILEptr1 (m:fm) = [l:agz] FILEptr (l, m)
vtypedef FILEptr1 (*none*) = [l:agz;m:fm] FILEptr (l, m)
//
(* ****** ****** *)

stadef fmlte = file_mode_lte

(* ****** ****** *)
//
castfn
FILEptr2ptr{l:addr}{m:fm} (filp: !FILEptr (l, m)):<> ptr (l)
//
overload ptrcast with FILEptr2ptr
//
(* ****** ****** *)

castfn
FILEptr_encode
  {l:addr}{m:fm} (
  pf: FILE_v (l, m) | p: ptr l
) : FILEptr (l, m)
overload encode with FILEptr_encode

castfn
FILEptr_decode
  {l:agz}{m:fm} (
  p: FILEptr (l, m)
) : (FILE_v (l, m) | ptr l)
overload decode with FILEptr_decode

(* ****** ****** *)

praxi
FILEptr_free_null
  {l:alez}{m:fm} (p: FILEptr (l, m)):<prf> void
// end of [FILEptr_free_null]

(* ****** ****** *)

castfn
FILEptr_refize (filp: FILEptr1):<> FILEref

(* ****** ****** *)

castfn
FILEref_vttakeout // a lock is associated with FILEref-value
  {m:fm} (filr: FILEref):<> [l:agz] vttakeout0 (FILEptr (l, m))
// end of [FILEref_vttakeout]

(* ****** ****** *)
//
abst@ype whence_type = int
//
typedef whence = whence_type
//
macdef SEEK_SET = $extval (whence, "SEEK_SET")
macdef SEEK_CUR = $extval (whence, "SEEK_CUR")
macdef SEEK_END = $extval (whence, "SEEK_END")
//
(* ****** ****** *)
(*
//
// FILE *fopen (const char *path, const char *mode);
//
The fopen function opens the file whose name is the string pointed to by
path and associates a stream with it.

The argument mode points to a string beginning with one of the follow
ing sequences (Additional characters may follow these sequences.):

  r      Open  text  file  for  reading.  The stream is positioned at the
         beginning of the file.

  r+     Open for reading and writing.  The stream is positioned  at  the
         beginning of the file.

  w      Truncate  file  to  zero length or create text file for writing.
         The stream is positioned at the beginning of the file.

  w+     Open for reading and writing.  The file is created  if  it  does
         not  exist, otherwise it is truncated.  The stream is positioned
         at the beginning of the file.

  a      Open for appending (writing at end of file).  The file is created
         if it does not exist.  The stream is positioned at the end of the
         file.

  a+     Open for reading and appending (writing at end  of  file).   The
         file  is created if it does not exist.  The stream is positioned
         at the end of the file.

*)

fun fopen{m:fm}
(
  path: NSH(string), fmode(m)
) :<!wrt> FILEptr0 (m) = "mac#%"

fun fopen_exn{m:fm}
(
  path: NSH(string), fmode(m)
) :<!exnwrt> FILEptr1 (m) = "ext#%"

fun fopen_ref_exn{m:fm}
(
  path: NSH(string), fmode(m)
) :<!exnwrt> FILEref(*none*) = "ext#%"

(* ****** ****** *)
//
symintr fclose
symintr fclose_exn
//
fun fclose0
  (filr: FILEref):<!wrt> int = "mac#%"
fun fclose1
  {l:addr}{m:fm}
(
  filp: !FILEptr (l, m) >> ptr l
) :<!wrt>
  [i:int | i <= 0]
(
  option_v (FILE_v (l, m), i < 0) | int i
) = "mac#%" // endfun
//
overload fclose with fclose0
overload fclose with fclose1
//
fun fclose0_exn
  (filr: FILEref):<!exnwrt> void = "ext#%"
fun fclose1_exn
  (filp: FILEptr1(*none*)):<!exnwrt> void = "ext#%"
//
overload fclose_exn with fclose0_exn
overload fclose_exn with fclose1_exn
//
(* ****** ****** *)

(*
fun fclose_stdin ():<!exnwrt> void = "ext#%"
fun fclose_stdout ():<!exnwrt> void = "ext#%"
fun fclose_stderr ():<!exnwrt> void = "ext#%"
*)

(* ****** ****** *)
(*
//
// FILE *freopen (const char *path, const char *mode, FILE *stream);
//
The [freopen] function opens the file whose name is the string pointed to
by path and associates the stream pointed to by stream with it.  The original
stream (if it exists) is closed.  The mode argument is used just as in the
fopen function.  The primary use of the freopen function is to change the file
associated with a standard text stream (stderr, stdin, or stdout).
//
*)
//
symintr freopen
symintr freopen_exn
//
fun freopen0 {m2:fm}
(
  path: NSH(string), m2: fmode m2, filr: FILEref
) :<!wrt> Ptr0 = "mac#%"
//
// HX-2012-07:
// the original stream is closed even if [freopen] fails.
//
fun freopen1
  {m1,m2:fm}{l0:addr}
(
  path: NSH(string), m2: fmode m2, filp: FILEptr (l0, m1)
) :<!wrt> [
  l:addr | l==null || l==l0
] (
  option_v (FILE_v (l, m2), l > null) | ptr l
) = "mac#%" // end of [freopen1]
//
overload freopen with freopen0
overload freopen with freopen1
//
fun
freopen0_exn
  {m2:fm}
(
  path: NSH(string), m2: fmode m2, filr: FILEref
) :<!exnwrt> void = "ext#%" // end of [freopen0_exn]
overload freopen_exn with freopen0_exn
//
(* ****** ****** *)

(*
fun freopen_stdin
  (path: NSH(string)):<!exnwrt> void = "ext#%"
// end of [freopen_stdin]
fun freopen_stdout
  (path: NSH(string)):<!exnwrt> void = "ext#%"
// end of [freopen_stdout]
fun freopen_stderr
  (path: NSH(string)):<!exnwrt> void = "ext#%"
// end of [freopen_stderr]
*)

(* ****** ****** *)
(*
//
// int fileno (FILE* filp) ;
// 
The function fileno examines the argument stream and returns its integer
descriptor. In case fileno detects that its argument is not a valid stream,
it must return -1 and set errno to EBADF.
*)
//
symintr fileno
//
fun fileno0 (filr: FILEref):<> int = "mac#%"
overload fileno with fileno0
fun fileno1 (filp: !FILEptr1(*none*)):<> int = "mac#%"
overload fileno with fileno1

(* ****** ****** *)

(*
//
// HX-2011-08
//
*)
dataview
fdopen_v
(
  fd:int, addr, m: fmode
) =
  | {l:agz}
    fdopen_v_succ (fd, l, m) of FILE_v (l, m)
  | fdopen_v_fail (fd, null, m) of fildes_v (fd)
// end of [fdopen_v]

fun fdopen
  {fd:int}{m:fm}
(
  fd: fildes (fd), m: fmode (m)
) : [l:agez] 
(
  fdopen_v (fd, l, m) | ptr l
) = "mac#%" // end of [fdopen]

fun fdopen_exn
  {fd:int}{m:fm}
  (fd: fildes (fd), m: fmode (m)): FILEptr1 (m) = "ext#%"
// end of [fdopen_exn]

(* ****** ****** *)
(*  
//
// int feof (FILE *stream);
//
The function feof() returns a nonzero value if the end of the given file
stream has been reached.
//
*)
//
symintr feof
//
fun feof0 (filr: FILEref):<> int = "mac#%"
overload feof with feof0
fun feof1 (filp: !FILEptr1(*none*)):<> int = "mac#%"
overload feof with feof1

(* ****** ****** *)
(*
//
// int ferror (FILE *stream);
//
The function [ferror] tests the error indicator for the stream pointed to by
stream, returning non-zero if it is set.  The error indicator can only be
reset by the [clearerr] function.
*)
//
symintr ferror
//
fun ferror0 (filr: FILEref):<> int = "mac#%"
overload ferror with ferror0
fun ferror1 (filp: !FILEptr1(*none*)):<> int = "mac#%"
overload ferror with ferror1

(* ****** ****** *)
(*
//
// void clearerr (FILE *stream);
//
The function [clearerr] clears the end-of-file and error indicators for
the stream pointed to by stream.
//
*)
//
symintr clearerr
//
fun clearerr0
  (filr: FILEref):<!wrt> void = "mac#%"
overload clearerr with clearerr0
fun clearerr1
  (filp: !FILEptr1(*none*)):<!wrt> void = "mac#%"
overload clearerr with clearerr1

(* ****** ****** *)
(*
//
// int fflush (FILE *stream);
//
The function fflush forces a write of all user-space buffered data for the
given output or update stream via the streams underlying write function.
The open status of the stream is unaffected.
//
Upon successful completion 0 is returned.  Otherwise, EOF is returned and
the global variable errno is set to indicate the error.
*)
//
symintr fflush
symintr fflush_exn
//
fun fflush0
  (out: FILEref):<!wrt> int = "mac#%"
fun fflush1 {m:fm}
(
  pf: fmlte (m, w) | out: !FILEptr1 (m)
) :<!wrt> [i:int | i <= 0] int (i) = "mac#%"
//
overload fflush with fflush0
overload fflush with fflush1
//
fun fflush0_exn
  (out: FILEref):<!exnwrt> void = "ext#%"
overload fflush_exn with fflush0_exn
//
(* ****** ****** *)
//
fun fflush_all ():<!exnwrt> void = "ext#%"
fun fflush_stdout ():<!exnwrt> void = "ext#%"
//
(* ****** ****** *)
(*
//
// int fgetc (FILE *stream)
//
[fgetc] reads the next character from stream and returns it as an
unsigned char cast to an int, or EOF on end of file or error. Note
that EOF must be a negative number!
//
*)
//
symintr fgetc
//
fun fgetc0
  (inp: FILEref):<!wrt> int = "mac#%"
fun fgetc1 {m:fm}
(
  pf: fmlte (m, r) | inp: !FILEptr1 (m)
) :<!wrt> intLte (UCHAR_MAX) = "mac#%"
//
overload fgetc with fgetc0
overload fgetc with fgetc1
//
(* ****** ****** *)

macdef getc = fgetc

(* ****** ****** *)

fun getchar0 ():<!wrt> int = "mac#%"
fun getchar1 (
) :<!wrt> [i:int | i <= UCHAR_MAX] int i = "mac#%"

(* ****** ****** *)
//
symintr fgets
//
fun fgets0
  {sz:int}{n0:pos | n0 <= sz}
(
  buf: &b0ytes(sz) >> bytes(sz), n0: int n0, inp: FILEref
) :<!wrt> Ptr0 = "mac#%" // = addr@(buf) or NULL
fun fgets1
  {sz:int}{n0:pos | n0 <= sz}{m:fm}
(
  pfm: fmlte (m, r)
| buf: &b0ytes(sz) >> bytes(sz), n0: int n0, inp: !FILEptr1 (m)
) :<!wrt> Ptr0 = "mac#%" // = addr@(buf) or NULL
//
overload fgets with fgets0
overload fgets with fgets1
//
dataview
fgets_v (
  sz:int, n0: int, addr, addr
) =
  | {l0:addr}
    fgets_v_fail (sz, n0, l0, null) of b0ytes(sz) @ l0
  | {n:nat | n < n0} {l0:agz}
    fgets_v_succ (sz, n0, l0, l0) of strbuf(sz, n) @ l0
// end of [fgets_v]
//
fun fgets1_err
  {sz,n0:int | sz >= n0; n0 > 0}{l0:addr}{m:fm}
(
  pf_mod: fmlte (m, r), pf_buf: b0ytes (sz) @ l0
| p0: ptr (l0), n0: int (n0), inp: !FILEptr1 (m)
) :<> [l1:addr] (fgets_v (sz, n0, l0, l1) | ptr l1) = "mac#%"
// end of [fgets_err]
//
overload fgets with fgets1_err
//
(* ****** ****** *)
//
// HX-2013-05:
// A complete line is read each time // [nullp] for error
//
fun fgets0_gc
  (bsz: intGte(1), inp: FILEref): Strptr0 = "ext#%"
fun fgets1_gc {m:fm}
(
  pf_mod: fmlte (m, r) | bsz: intGte(1), inp: FILEptr1 (m)
) : Strptr0 = "ext#%" // end of [fget1_gc]

(* ****** ****** *)
(*
//
// int fgetpos(FILE *stream, fpos_t *pos);
//
The [fgetpos] function stores the file position indicator of the given file
stream in the given position variable. The position variable is of type
fpos_t (which is defined in stdio.h) and is an object that can hold every
possible position in a FILE. [fgetpos] returns zero upon success, and a
non-zero value upon failure.
//
*)
//
symintr fgetpos
//
abst@ype fpos_t = $extype"ats_fpos_type"
//
fun fgetpos0
(
  filp: FILEref, pos: &fpos_t? >> opt (fpos_t, i==0)
) :<!wrt> #[i:int | i <= 0] int (i) = "mac#%"
fun fgetpos1
(
  filp: !FILEptr1, pos: &fpos_t? >> opt (fpos_t, i==0)
) :<!wrt> #[i:int | i <= 0] int (i) = "mac#%"
//
overload fgetpos with fgetpos0
overload fgetpos with fgetpos1
//
symintr fgetpos_exn
//
fun fgetpos0_exn 
  (filp: FILEref, pos: &fpos_t? >> _) :<!exnwrt> void = "ext#%"
overload fgetpos_exn with fgetpos0_exn 
//
(* ****** ****** *)
(*
//
// int fputc (int c, FILE *stream)
//
The function [fputc] writes the given character [c] to the given output
stream. The return value is the character, unless there is an error, in
which case the return value is EOF.
//
*)
//
symintr fputc
//
typedef
fputc0_type
  (a:t0p) = (a, FILEref) -<0,!wrt> int
fun fputc0_int : fputc0_type (int) = "mac#%" 
fun fputc0_char : fputc0_type (char) = "mac#%" 
overload fputc with fputc0_int of 0
overload fputc with fputc0_char of 0
//
typedef
fputc1_type
  (a:t0p) = {m:fm}
(
  fmlte (m, w) | a, !FILEptr1 (m)
) -<0,!wrt> intLte (UCHAR_MAX)
fun fputc1_int : fputc1_type (int) = "mac#%"
fun fputc1_char : fputc1_type (char) = "mac#%"
overload fputc with fputc1_int of 10
overload fputc with fputc1_char of 10
//
symintr fputc_exn
//
typedef
fputc0_exn_type
  (a:t0p) = (a, FILEref) -<0,!exnwrt> void
fun fputc0_exn_int : fputc0_exn_type (int) = "ext#%"
fun fputc0_exn_char : fputc0_exn_type (char) = "ext#%"
overload fputc_exn with fputc0_exn_int of 0
overload fputc_exn with fputc0_exn_char of 0
//
(* ****** ****** *)

macdef putc = fputc

(* ****** ****** *)

fun putchar0 (c: int):<!wrt> int = "mac#%"
fun putchar1
  (c: int):<!wrt> [i:int | i <= UCHAR_MAX] int i = "mac#%"
// end of [putchar1]

(* ****** ****** *)
(*
//
// int fputs (const char* s, FILE *stream)
//
The function [fputs] writes a string to a file. it returns
a non-negative number on success, or EOF on error.
*)

//
symintr fputs
symintr fputs_exn
//
fun fputs0
(
  str: NSH(string), fil: FILEref
) :<!wrt> int = "mac#%"
fun fputs1 {m:fm}
(
  pf: fmlte (m, w) | str: NSH(string), out: !FILEptr1 (m)
) :<!wrt> int = "mac#%"
//
overload fputs with fputs0
overload fputs with fputs1
//
fun fputs0_exn
(
  str: NSH(string), fil: FILEref
) :<!exnwrt> void = "ext#%"
//
overload fputs_exn with fputs0_exn
//
(* ****** ****** *)
//
// [puts] puts a newline at the end
//
fun puts
  (inp: NSH(string)):<!wrt> int = "mac#%"
// end of [puts]
fun puts_exn
  (inp: NSH(string)):<!exnwrt> void = "ext#%"
// end of [puts_exn]

(* ****** ****** *)
(*
//
// size_t fread (void *ptr, size_t size, size_t nmemb, FILE *stream);
//
The function [fread] reads [nmemb] elements of data, each [size] bytes
long, from the stream pointed to by stream, storing them at the location
given by ptr. The return value is the number of items that are actually
read.
//
[fread] does not distinguish between end-of-file and error, and callers
must use [feof] and [ferror] to determine which occurred.
//
*)
//
symintr fread
//
fun
fread0 // [isz]: the size of each item
  {isz:pos}
  {nbf:int}
  {n:int | n*isz <= nbf}
(
  buf: &bytes(nbf) >> _
, isz: size_t isz, n: size_t n
, inp: FILEref(*none*)
) :<!wrt> sizeLte n = "mac#%"
fun
fread1 // [isz]: the size of each item
  {isz:pos}
  {nbf:int}
  {n:int | n*isz <= nbf}
  {m:fm}
(
  pfm: fmlte (m, r)
| buf: &bytes(nbf) >> _
, isz: size_t isz, n: size_t n
, inp: !FILEptr1 (m)
) :<!wrt> sizeLte n = "mac#%"
//
overload fread with fread0
overload fread with fread1
//
symintr fread_exn
//
fun
fread0_exn // [isz]: the size of each item
  {isz:pos}
  {nbf:int}
  {n:int | n*isz <= nbf}
(
  buf: &bytes(nbf) >> _, isz: size_t isz, n: size_t n, inp: FILEref
) :<!exnwrt> sizeLte n = "ext#%" // endfun
overload fread_exn with fread0_exn

(* ****** ****** *)
(*
//
// size_t fwrite (
//   const void *ptr,  size_t size,  size_t nmemb, FILE *stream
// ) ;
//
The function [fwrite] writes [nmemb] elements of data, each [size] bytes
long, to the stream pointed to by stream, obtaining them from the location
given by [ptr]. The return value is the number of items that are actually
written.
//
*)
//
symintr fwrite
//
fun
fwrite0 // [isz]: the size of each item
  {isz:pos}
  {nbf:int}
  {n:int | n*isz <= nbf}
(
  buf: &RD(bytes(nbf))
, isz: size_t isz, n: size_t n
, out: FILEref
) :<!wrt> sizeLte (n) = "mac#%"
fun
fwrite1 // [isz]: the size of each item
  {isz:pos}
  {nbf:int}
  {n:int | n*isz <= nbf}
  {m:fm}
(
  pfm: fmlte (m, w)
| buf: &RD(bytes(nbf))
, isz: size_t isz, n: size_t n
, out: !FILEptr1 (m)
) :<!wrt> sizeLte (n) = "mac#%"
//
overload fwrite with fwrite0
overload fwrite with fwrite1
//
symintr fwrite_exn
//
fun
fwrite0_exn // [isz]: the size of each item
  {isz:pos}
  {nbf:int}
  {n:int | n*isz <= nbf}
(
  buf: &RD(bytes(nbf))
, isz: size_t isz, n: size_t n
, out: FILEref(*none*)
) :<!exnwrt> sizeLte (n) = "ext#%"
overload fwrite_exn with fwrite0_exn

(* ****** ****** *)
(*
//
// int fseek (FILE *stream, long offset, int whence)
//
The [fseek] function sets the file position indicator for the stream
pointed to by stream.  The new position, measured in bytes, is obtained by
adding offset bytes to the position specified by whence.  If whence is set
to [SEEK_SET], [SEEK_CUR], or [SEEK_END], the offset is relative to the
start of the file, the current position indicator, or end-of-file,
respectively.  A successful call to the [fseek] function clears the end-
of-file indicator for the stream and undoes any effects of the [ungetc]
function on the same stream. Upon success, [fseek] returns 0. Otherwise,
it returns -1.
//
*)
//
symintr fseek
symintr fseek_exn
//
fun fseek0
(
  filr: FILEref, offset: lint, whence: whence
) :<!wrt> int = "mac#%"
fun fseek1
(
  f: !FILEptr1(*none*), offset: lint, whence: whence
) :<!wrt> int = "mac#%"
//
overload fseek with fseek0
overload fseek with fseek1
//
fun fseek0_exn
(
  filr: FILEref, offset: lint, whence: whence
) :<!exnwrt> void = "ext#%"
//
overload fseek_exn with fseek0_exn
//
(* ****** ****** *)
(*
//
// void fsetpos(FILE *stream, const fpos_t *pos);
//
The [fsetpos] function moves the file position indicator for the given
stream to a location specified by the position object. The type fpos_t is
defined in stdio.h.  The return value for fsetpos() is zero upon success,
non-zero on failure.
//
*)
//
symintr fsetpos
symintr fsetpos_exn
//
fun fsetpos0
  (filp: FILEref(*none*), pos: &RD(fpos_t)):<!wrt> int = "mac#%"
fun fsetpos1
  (filp: !FILEptr1(*none*), pos: &RD(fpos_t)):<!wrt> int = "mac#%"
//
overload fsetpos with fsetpos0
overload fsetpos with fsetpos1
//
fun fsetpos0_exn
  (filp: FILEref(*none*), pos: &RD(fpos_t)):<!exnwrt> void = "ext#%"
//
overload fsetpos_exn with fsetpos0_exn
//
(* ****** ****** *)

(*
//
// long ftell (FILE *stream)
//
[ftell] returns the current offset of the given file stream upon on
success. Otherwise, -1 is returned and the global variable errno is set to
indicate the error.
//
*)
//
symintr ftell
symintr ftell_exn
//
fun ftell0
  (filr: FILEref):<!wrt> lint = "mac#%"
fun ftell1
  (filp: !FILEptr1(*none*)):<!wrt> lint = "mac#%"
overload ftell with ftell0
overload ftell with ftell1
//
fun ftell0_exn
  (filr: FILEref):<!exnwrt> lint = "ext#%"
//
overload ftell_exn with ftell0_exn
//
(* ****** ****** *)

(*
//
// perror - print a system error message
//
The routine [perror(s)] produces a message on the standard error output,
describing the last error encountered during a call to a system or library
function.  First (if s is not NULL and *s is not NULL) the argument string
s is printed, followed by a colon and a blank.  Then the message and a
newline.
//
*)
fun perror
  (msg: NSH(string)):<!wrt> void = "mac#%"
// end of [perror]

(* ****** ****** *)

abstype pmode_type (m:fm) = string
typedef pmode (m:fm) = pmode_type (m)

absview popen_view (l:addr)
viewdef popen_v (l:addr) = popen_view (l)

praxi popen_v_free_null (pf: popen_v (null)): void

fun popen{m:fm}
(
  cmd: NSH(string), mode: pmode (m)
) : [l:addr] (popen_v (l) | FILEptr (l, m))

fun popen_exn{m:fm}
(
  cmd: NSH(string), mode: pmode (m)
) : FILEref = "ext#%" // endfun

fun pclose0_exn (filr: FILEref): int = "ext#%"
fun pclose1_exn
  {l:agz}{m:fm}
  (pf: popen_v l | filr: FILEptr (l, m)): int= "ext#%"
// end of [pclose1_exn]

(* ****** ****** *)

fun remove
  (inp: NSH(string)):<!wrt> int = "mac#%"
fun remove_exn
  (inp: NSH(string)):<!exnwrt> void = "ext#%"

(* ****** ****** *)

fun rename
(
  oldpath: NSH(string), newpath: NSH(string)
) :<!wrt> int = "mac#%" // end of [fun]

fun rename_exn
(
  oldpath: NSH(string), newpath: NSH(string)
) :<!exnwrt> void = "ext#%" // end of [fun]

(* ****** ****** *)
(*
// HX: [rewind] generates no error
*)
//
symintr rewind
//
fun rewind0
  (fil: FILEref):<!wrt> void = "mac#%"
overload rewind with rewind0
fun rewind1
  (fil: !FILEptr1(*none*)):<!wrt> void = "mac#%"
overload rewind with rewind1

(* ****** ****** *)

fun tmpfile
  () :<!wrt> FILEptr0 (rw) = "mac#%"
fun tmpfile_exn
  () :<!exnwrt> FILEptr1 (rw) = "ext#%"
fun tmpfile_ref_exn
  () :<!exnwrt> FILEref(*none*) = "ext#%"
// end of [tmpfile_ref_exn]

(* ****** ****** *)
(*
//
// int ungetc(int c, FILE *stream);
//
[ungetc] pushes [c] back to stream, cast to unsigned char, where it is
available for subsequent read operations.  Pushed-back characters will be
returned in reverse order; only one pushback is guaranteed.
//
*)
//
symintr ungetc
//
fun
ungetc0
  (c: char, f: FILEref):<!wrt> int = "mac#%"
fun
ungetc1
  {l:agz}{m:fm}
(
  pfm: fmlte (m, rw) | c: char, f: !FILEptr (l, m)
) :<!wrt> [i:int | i <= UCHAR_MAX] int (i) = "mac#%"
//
overload ungetc with ungetc0
overload ungetc with ungetc1
//
symintr ungetc_exn
//
fun ungetc0_exn
  (c: char, f: FILEref) :<!exnwrt> void = "ext#%"
//
overload ungetc_exn with ungetc0_exn
//
(* ****** ****** *)

stacst BUFSIZ : int
praxi BUFSIZ_gtez (): [BUFSIZ >= 0] void
macdef BUFSIZ = $extval (int(BUFSIZ), "BUFSIZ")

(* ****** ****** *)
//
abst@ype bufmode_t = int
//
macdef _IOFBF = $extval (bufmode_t, "_IOFBF") // fully buffered
macdef _IOLBF = $extval (bufmode_t, "_IOLBF") // line buffered
macdef _IONBF = $extval (bufmode_t, "_IONBF") // no buffering
//
(* ****** ****** *)
//
symintr setbuf_null
//
fun setbuf0_null
  (f: FILEref): void = "mac#%"
overload setbuf_null with setbuf0_null
fun setbuf1_null
  (f: !FILEptr1(*none*)): void = "mac#%"
overload setbuf_null with setbuf1_null

(* ****** ****** *)
(*
//
// HX-2010-10-03:
// the buffer can be freed only after it is no longer used by
// the stream to which it is attached!!!
*)
//
symintr setbuffer
//
fun
setbuffer0
  {n1,n2:nat | n2 <= n1}{l:addr}
(
  pf_buf: !b0ytes n1 @ l | f: FILEref, p_buf: ptr l, n2: size_t n2
) : void = "mac#%"
overload setbuffer with setbuffer0
fun
setbuffer1
  {n1,n2:nat | n2 <= n1}{lbf:addr}
(
  pf_buf: !b0ytes n1 @ lbf | f: !FILEptr1(*none*), p_buf: ptr lbf, n2: size_t n2
) : void = "mac#%"
overload setbuffer with setbuffer1

(* ****** ****** *)
//
symintr setlinebuf
//
fun setlinebuf0
  (f: FILEref): void = "mac#%"
overload setlinebuf with setlinebuf0
fun setlinebuf1
  (f: !FILEptr1(*none*)): void = "mac#%"
overload setlinebuf with setlinebuf1

(* ****** ****** *)
//
symintr setvbuf_null
//
fun setvbuf0_null
  (f: FILEref, mode: bufmode_t): int = "mac#%"
overload setvbuf_null with setvbuf0_null
fun setvbuf1_null
  (f: !FILEptr1(*none*), mode: bufmode_t): int = "mac#%"
overload setvbuf_null with setvbuf1_null

(* ****** ****** *)
//
symintr setvbuf
//
fun
setvbuf0
  {n1,n2:nat | n2 <= n1}{lbf:addr}
(
  pf_buf: !b0ytes(n1) @ lbf | fil: FILEref, mode: bufmode_t, n2: size_t n2
) : int = "mac#%"
overload setvbuf with setvbuf0
fun
setvbuf1
  {n1,n2:nat | n2 <= n1}{lbf:addr}
(
  pf_buf: !b0ytes(n1) @ lbf | fil: !FILEptr1(*none*), mode: bufmode_t, n2: size_t n2
) : int = "mac#%"
overload setvbuf with setvbuf1

(* ****** ****** *)

(* end of [stdio.sats] *)