This file is indexed.

/usr/lib/ats2-postiats-0.1.3/prelude/basics_sta.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
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-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 of the file:
// Hongwei Xi (gmhwxiATgmailDOTcom)
// Start Time: September, 2011
//
(* ****** ****** *)

#include "prelude/params.hats"

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

#if VERBOSE_PRELUDE #then
#print "Loading [basics_sta.sats] starts!\n"
#endif // end of [VERBOSE_PRELUDE]

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

#define RD(x) x // for commenting: read-only

(* ****** ****** *)
(*
//
// HX-2012-05-24:
// the following two styles are equivalent:
//
stadef
bool_kind = $extkind"atstype_bool"
tkindef bool_kind = "atstype_bool"
*)
(* ****** ****** *)
//
tkindef bool_kind = "atstype_bool"
//
abst@ype
bool_t0ype = tkind_t0ype (bool_kind)
stadef bool = bool_t0ype // shorthand
abst@ype
bool_bool_t0ype (b: bool) = bool_t0ype
stadef bool = bool_bool_t0ype // shorthand
//
typedef Bool = [b:bool] bool (b)
typedef boolLte
  (b1:bool) = [b2:bool] bool (b2 <= b1) // b2 -> b1
typedef boolGte
  (b1:bool) = [b2:bool] bool (b2 >= b1) // b1 -> b2
//
abst@ype atstype_bool // HX-2013-09: for internal use
//
(* ****** ****** *)

tkindef
byte_kind = "atstype_byte"
abst@ype
byte_t0ype = tkind_t0ype (byte_kind)
stadef byte = byte_t0ype

(* ****** ****** *)
//
// char is signed
//
sortdef int8 = {
  i:int | ~128 <= i; i < 128
} // end of [int8]
sortdef uint8 =
  { i:int | 0 <= i; i < 256 }
// end of [uint8]
//
tkindef char_kind = "atstype_char"
//
abst@ype
char_t0ype = tkind_t0ype (char_kind)
stadef char = char_t0ype // shorthand
abst@ype
char_int_t0ype (c:int) = char_t0ype
stadef char = char_int_t0ype // shorthand
typedef Char = [c:int8] char (c)
typedef charNZ = [c:int8 | c != 0] char (c)
//
// signed characters
//
tkindef schar_kind = "atstype_schar"
//
abst@ype
schar_t0ype = tkind_t0ype (schar_kind)
stadef schar = schar_t0ype // shorthand
abst@ype
schar_int_t0ype (c:int) = schar_t0ype
stadef schar = schar_int_t0ype // shorthand
typedef sChar = [c:int8] schar (c)
//
// unsigned characters
//
tkindef uchar_kind = "atstype_uchar"
//
abst@ype
uchar_t0ype = tkind_t0ype (uchar_kind)
stadef uchar = uchar_t0ype // shorthand
abst@ype
uchar_int_t0ype (c:int) = uchar_t0ype
stadef uchar = uchar_int_t0ype // shorthand
typedef uChar = [c:uint8] uchar (c)
//
(* ****** ****** *)

sortdef tk = tkind

(* ****** ****** *)
//
abst@ype
g0int_t0ype (tk:tk) = tkind_t0ype (tk)
stadef g0int = g0int_t0ype // shorthand
abst@ype
g1int_int_t0ype (tk:tkind, int) = g0int (tk)
stadef g1int = g1int_int_t0ype // shorthand
//
typedef g1int (tk:tkind) = [i:int] g1int (tk, i)
typedef g1int0 (tk:tkind) = [i:int | i >= 0] g1int (tk, i)
typedef g1int1 (tk:tkind) = [i:int | i >= 1] g1int (tk, i)
//
(* ****** ****** *)
//
typedef g1intLt
  (tk:tk, n:int) = [i:int | i < n] g1int (tk, i)
typedef g1intLte
  (tk:tk, n:int) = [i:int | i <= n] g1int (tk, i)
typedef g1intGt
  (tk:tk, n:int) = [i:int | i > n] g1int (tk, i)
typedef g1intGte
  (tk:tk, n:int) = [i:int | i >= n] g1int (tk, i)
typedef g1intBtw
  (tk:tk, lb:int, ub:int) = [i: int | lb <= i; i < ub] g1int (tk, i)
typedef g1intBtwe
  (tk:tk, lb:int, ub:int) = [i: int | lb <= i; i <= ub] g1int (tk, i)
//
(* ****** ****** *)
//
abst@ype
g0uint_t0ype (tk:tkind) = tkind_t0ype (tk)
stadef g0uint = g0uint_t0ype // shorthand
abst@ype
g1uint_int_t0ype (tk:tkind, int) = g0uint (tk)
stadef g1uint = g1uint_int_t0ype // shorthand
//
typedef g1uint (tk:tk) = [i:int] g1uint (tk, i)
typedef g1uint0 (tk:tk) = [i:int | i >= 0] g1uint (tk, i)
typedef g1uint1 (tk:tk) = [i:int | i >= 1] g1uint (tk, i)
//
(* ****** ****** *)
//
typedef g1uintLt
  (tk:tk, n:int) = [i:nat | i < n] g1uint (tk, i)
typedef g1uintLte
  (tk:tk, n:int) = [i:nat | i <= n] g1uint (tk, i)
typedef g1uintGt
  (tk:tk, n:int) = [i:int | i > n] g1uint (tk, i)
typedef g1uintGte
  (tk:tk, n:int) = [i:int | i >= n] g1uint (tk, i)
typedef g1uintBtw
  (tk:tk, lb:int, ub:int) = [i: int | lb <= i; i < ub] g1uint (tk, i)
typedef g1uintBtwe
  (tk:tk, lb:int, ub:int) = [i: int | lb <= i; i <= ub] g1uint (tk, i)
//
(* ****** ****** *)
//
tkindef int_kind = "atstype_int"
//
typedef int0 = g0int (int_kind)
typedef int1 (i:int) = g1int (int_kind, i)
//
stadef int = int1 // 2nd-select
stadef int = int0 // 1st-select
//
typedef Int = [i:int] int1 (i)
typedef Nat = [i:int | i >= 0] int1 (i)
//
typedef intLt (n:int) = g1intLt (int_kind, n)
typedef intLte (n:int) = g1intLte (int_kind, n)
typedef intGt (n:int) = g1intGt (int_kind, n)
typedef intGte (n:int) = g1intGte (int_kind, n)
typedef intBtw (lb:int, ub:int) = g1intBtw (int_kind, lb, ub)
typedef intBtwe (lb:int, ub:int) = g1intBtwe (int_kind, lb, ub)
//
typedef Two = intBtw (0, 2)
typedef Sgn = intBtwe (~1, 1)
//
typedef natLt (n:int) = intBtw (0, n)
typedef natLte (n:int) = intBtwe (0, n)
//
tkindef uint_kind = "atstype_uint"
//
typedef uint0 = g0uint (uint_kind)
typedef uint1 (n:int) = g1uint (uint_kind, n)
//
stadef uint = uint1 // 2nd-select
stadef uint = uint0 // 1st-select
//
stadef uInt = [n:int] uint1 (n)
//
typedef uintLt (n:int) = g1uintLt (uint_kind, n)
typedef uintLte (n:int) = g1uintLte (uint_kind, n)
typedef uintGt (n:int) = g1uintGt (uint_kind, n)
typedef uintGte (n:int) = g1uintGte (uint_kind, n)
typedef uintBtw (lb:int, ub:int) = g1uintBtw (uint_kind, lb, ub)
typedef uintBtwe (lb:int, ub:int) = g1uintBtwe (uint_kind, lb, ub)
//
abst@ype atstype_int // HX-2013-09: for internal use
abst@ype atstype_uint // HX-2013-09: for internal use
//
(* ****** ****** *)
//
tkindef
lint_kind = "atstype_lint"
typedef
lint0 = g0int (lint_kind)
typedef
lint1 (i:int) = g1int (lint_kind, i)
stadef lint = lint1 // 2nd-select
stadef lint = lint0 // 1st-select
//
tkindef
ulint_kind = "atstype_ulint"
typedef
ulint0 = g0uint (ulint_kind)
typedef
ulint1 (i:int) = g1uint (ulint_kind, i)
stadef ulint = ulint1 // 2nd-select
stadef ulint = ulint0 // 1st-select
//
tkindef
llint_kind = "atstype_llint"
typedef llint0 = g0int (llint_kind)
typedef llint1 (i:int) = g1int (llint_kind, i)
stadef llint = llint1 // 2nd-select
stadef llint = llint0 // 1st-select
//
tkindef
ullint_kind = "atstype_ullint"
typedef
ullint0 = g0uint (ullint_kind)
typedef
ullint1 (i:int) = g1uint (ullint_kind, i)
stadef ullint = ullint1 // 2nd-select
stadef ullint = ullint0 // 1st-select
//
(* ****** ****** *)
//
tkindef
intptr_kind = "atstype_intptr"
typedef
intptr0 = g0int (intptr_kind)
typedef
intptr1 (i:int) = g1int (intptr_kind, i)
stadef intptr = intptr1 // 2nd-select
stadef intptr = intptr0 // 1st-select
//
tkindef
uintptr_kind = "atstype_uintptr"
typedef
uintptr0 = g0uint (uintptr_kind)
typedef
uintptr1 (i:int) = g1uint (uintptr_kind, i)
stadef uintptr = uintptr1 // 2nd-select
stadef uintptr = uintptr0 // 1st-select
//
(* ****** ****** *)
//
tkindef
sint_kind = "atstype_sint"
typedef
sint0 = g0int (sint_kind)
typedef
sint1 (i:int) = g1int (sint_kind, i)
stadef sint = sint1 // 2nd-select
stadef sint = sint0 // 1st-select
//
tkindef
usint_kind = "atstype_usint"
typedef
usint0 = g0uint (usint_kind)
typedef
usint1 (i:int) = g1uint (usint_kind, i)
stadef usint = usint1 // 2nd-select
stadef usint = usint0 // 1st-select
//
(* ****** ****** *)
//
tkindef
size_kind = "atstype_size"
typedef size0_t = g0uint (size_kind)
typedef size1_t (i:int) = g1uint (size_kind, i)
//
stadef size_t = size1_t // 2nd-select
stadef size_t = size0_t // 1st-select
//
typedef Size =
  [i:int | i >= 0] g1uint (size_kind, i)
typedef Size_t = Size
//
typedef sizeLt (n:int) = g1uintLt (size_kind, n)
typedef sizeLte (n:int) = g1uintLte (size_kind, n)
typedef sizeGt (n:int) = g1uintGt (size_kind, n)
typedef sizeGte (n:int) = g1uintGte (size_kind, n)
typedef sizeBtw (lb:int, ub:int) = g1uintBtw (size_kind, lb, ub)
typedef sizeBtwe (lb:int, ub:int) = g1uintBtwe (size_kind, lb, ub)
//
tkindef ssize_kind = "atstype_ssize"
typedef ssize0_t = g0int (ssize_kind)
typedef ssize1_t (i:int) = g1int (ssize_kind , i) 
//
stadef ssize_t = ssize1_t // 2nd-select
stadef ssize_t = ssize0_t // 1st-select
//
typedef SSize =
  [i:int] g1int (ssize_kind, i)
typedef SSize_t = SSize
//
typedef ssizeLt (n:int) = g1intLt (ssize_kind, n)
typedef ssizeLte (n:int) = g1intLte (ssize_kind, n)
typedef ssizeGt (n:int) = g1intGt (ssize_kind, n)
typedef ssizeGte (n:int) = g1intGte (ssize_kind, n)
typedef ssizeBtw (lb:int, ub:int) = g1intBtw (ssize_kind, lb, ub)
typedef ssizeBtwe (lb:int, ub:int) = g1intBtwe (ssize_kind, lb, ub)
//
abst@ype atstype_size // HX-2013-09: for internal use
abst@ype atstype_ssize // HX-2013-09: for internal use
//
(* ****** ****** *)

typedef sizeof_t (a:vt@ype) = size_t (sizeof(a?))

(* ****** ****** *)
//
tkindef
int8_kind = "atstype_int8"
typedef
int8_0 = g0int (int8_kind)
typedef
int8_1 (i:int) = g1int (int8_kind, i)
stadef int8 = int8_1 // 2nd-select
stadef int8 = int8_0 // 1st-select
stadef Int8 = [i:int] int8_1 (i)
//
tkindef
uint8_kind = "atstype_uint8"
typedef
uint8_0 = g0uint (uint8_kind)
typedef
uint8_1 (i:int) = g1uint (uint8_kind, i)
stadef uint8 = uint8_1 // 2nd-select
stadef uint8 = uint8_0 // 1st-select
stadef uInt8 = [i:nat] uint8_1 (i)
//
(* ****** ****** *)
//
tkindef
int16_kind = "atstype_int16"
typedef
int16_0 = g0int (int16_kind)
typedef
int16_1 (i:int) = g1int (int16_kind, i)
stadef int16 = int16_1 // 2nd-select
stadef int16 = int16_0 // 1st-select
stadef Int16 = [i:int] int16_1 (i)
//
tkindef
uint16_kind = "atstype_uint16"
typedef
uint16_0 = g0uint (uint16_kind)
typedef
uint16_1 (i:int) = g1uint (uint16_kind, i)
stadef uint16 = uint16_1 // 2nd-select
stadef uint16 = uint16_0 // 1st-select
stadef uInt16 = [i:nat] uint16_1 (i)
//
(* ****** ****** *)
//
tkindef
int32_kind = "atstype_int32"
typedef
int32_0 = g0int (int32_kind)
typedef
int32_1 (i:int) = g1int (int32_kind, i)
stadef int32 = int32_1 // 2nd-select
stadef int32 = int32_0 // 1st-select
stadef Int32 = [i:int] int32_1 (i)
//
tkindef
uint32_kind = "atstype_uint32"
typedef
uint32_0 = g0uint (uint32_kind)
typedef
uint32_1 (i:int) = g1uint (uint32_kind, i)
stadef uint32 = uint32_1 // 2nd-select
stadef uint32 = uint32_0 // 1st-select
stadef uInt32 = [i:nat] uint32_1 (i)
//
(* ****** ****** *)
//
tkindef
int64_kind = "atstype_int64"
typedef
int64_0 = g0int (int64_kind)
typedef
int64_1 (i:int) = g1int (int64_kind, i)
stadef int64 = int64_1 // 2nd-select
stadef int64 = int64_0 // 1st-select
stadef Int64 = [i:int] int64_1 (i)
//
tkindef
uint64_kind = "atstype_uint64"
typedef
uint64_0 = g0uint (uint64_kind)
typedef
uint64_1 (i:int) = g1uint (uint64_kind, i)
stadef uint64 = uint64_1 // 2nd-select
stadef uint64 = uint64_0 // 1st-select
stadef uInt64 = [i:nat] uint64_1 (i)

(* ****** ****** *)
//
abst@ype
g0float_t0ype (tk:tk) = tkind_t0ype (tk)
stadef g0float = g0float_t0ype // shorthand
//
tkindef float_kind = "atstype_float"
typedef float = g0float (float_kind)
//
tkindef double_kind = "atstype_double"
typedef double = g0float (double_kind)
//
tkindef ldouble_kind = "atstype_ldouble"
typedef ldouble = g0float (ldouble_kind)
//
(* ****** ****** *)
//
// HX: unindexed type for pointers
//
tkindef ptr_kind = "atstype_ptrk"
abstype ptr_type = tkind_type (ptr_kind)
stadef ptr = ptr_type // a shorthand
abstype ptr_addr_type (l:addr) = ptr_type
stadef ptr = ptr_addr_type // a shorthand
typedef Ptr = [l:addr] ptr (l)
typedef Ptr0 = [l:addr | l >= null] ptr (l)
typedef Ptr1 = [l:addr | l >  null] ptr (l)
typedef
Ptrnull (l:addr) =
  [l1:addr | l1 == null || l1 == l] ptr (l1)
// end of [Ptrnull]
//
// HX-2012-02-14: it is an expriment for now:
//
stadef ptr (n:int) = ptr_addr_type (addr_of_int(n))
//
(* ****** ****** *)

(*
** HX: persistent read-only strings
*)
(*
//
// HX-2013-04: this confuses type-erasure
//
abstype
string_type = $extype"atstype_string"
*)
abstype
string_type = ptr // = char* in C
abstype
string_int_type (n: int) = string_type
//
stadef string0 = string_type
stadef string1 = string_int_type
stadef string = string1 // 2nd-select
stadef string = string0 // 1st-select
typedef String = [n:int] string_int_type (n)
typedef String0 = [n:int | n >= 0] string_int_type (n)
typedef String1 = [n:int | n >= 1] string_int_type (n)
//
(* ****** ****** *)

abstype
stropt_int_type (n:int) = ptr
stadef stropt = stropt_int_type
typedef Stropt = [n:int] stropt_int_type (n)
typedef Stropt0 = [n:int] stropt_int_type (n)
typedef Stropt1 = [n:int | n >= 0] stropt_int_type (n)
stadef stropt = Stropt // HX: this may be a bit confusing :)

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

(*
** HX: linear mutable strings
*)
absvtype
strptr_addr_vtype (l:addr) = ptr
stadef strptr = strptr_addr_vtype
vtypedef Strptr0 = [l:addr] strptr (l)
vtypedef Strptr1 = [l:addr | l > null] strptr (l)
stadef strptr = Strptr0

absvtype
strnptr_addr_int_vtype (l:addr, n:int) = ptr
stadef strnptr = strnptr_addr_int_vtype
vtypedef strnptr (n:int) = [l:addr] strnptr (l, n)
vtypedef Strnptr0 = [l:addr;n:int] strnptr (l, n)
vtypedef Strnptr1 = [l:addr;n:int | n >= 0] strnptr (l, n)

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

(*
** HX: persistent mutable strings
*)
abstype
strref_addr_type (l:addr) = ptr
stadef strref = strref_addr_type
typedef Strref0 = [l:addr] strref (l)
typedef Strref1 = [l:addr | l > null] strref (l)

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

abst@ype
atsvoid_t0ype
(*
= $extype"atsvoid_t0ype"
*)
typedef void = atsvoid_t0ype // = C-void

(* ****** ****** *)
//
absvtype
exception_vtype = $extype"atstype_exnconptr"
//
vtypedef exn = exception_vtype // boxed vtype
//
(* ****** ****** *)

absvt@ype // covariance
opt_vt0ype_bool_vt0ype (a:vt@ype+, opt:bool) = a
stadef opt = opt_vt0ype_bool_vt0ype

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

typedef bytes (n:int) = @[byte][n]
viewdef bytes_v (l:addr, n:int) = bytes (n) @ l
typedef b0ytes (n:int) = @[byte?][n]
viewdef b0ytes_v (l:addr, n:int) = b0ytes (n) @ l

(* ****** ****** *)
//
abstype
cloref_t0ype_type (a:t@ype) = ptr
stadef cloref = cloref_t0ype_type
//
absvtype
cloptr_vt0ype_vtype (a:t@ype) = ptr
stadef cloptr = cloptr_vt0ype_vtype
vtypedef cloptr0 = cloptr_vt0ype_vtype (void)
//
(* ****** ****** *)
//
// HX: for memory deallocation (with/without GC)
//
absview
mfree_gc_addr_view (addr)
stadef mfree_gc_v = mfree_gc_addr_view
absview
mfree_ngc_addr_view (addr)
stadef mfree_ngc_v = mfree_ngc_addr_view
//
absview
mfree_libc_addr_view (addr) // libc-mfree
stadef mfree_libc_v = mfree_libc_addr_view
//
(* ****** ****** *)

absvt@ype
arrpsz_vt0ype_int_vt0ype
  (a:vt@ype+, n:int) = $extype"atstype_arrpsz"
stadef arrpsz = arrpsz_vt0ype_int_vt0ype

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

absprop // invariance
vbox_view_prop (v:view)
propdef vbox (v:view) = vbox_view_prop (v)

abstype // invariance
ref_vt0ype_type (a:vt@ype) = ptr
typedef ref (a:vt@ype) = ref_vt0ype_type (a)

(* ****** ****** *)
//
viewdef vtakeout
  (v1: view, v2: view) = (v2, v2 -<lin,prf> v1)
viewdef vtakeout0 (v:view) = vtakeout (void, v)
//
vtypedef vttakeout
  (vt1: vt@ype, vt2: vt@ype) = (vt2 -<lin,prf> vt1 | vt2)
viewdef vttakeout0 (vt:vt@ype) = vttakeout (void, vt)
//
(* ****** ****** *)
//
vtypedef
vtakeoutptr
  (a:vt@ype) = [l:addr] (a@l, a@l -<lin,prf> void | ptr l)
//
(* ****** ****** *)
//
vtypedef
vstrptr (l:addr) = vttakeout0 (strptr l)
//
vtypedef vStrptr0 = [l:addr] vstrptr (l)
vtypedef vStrptr1 = [l:addr | l > null] vstrptr (l)
//
(* ****** ****** *)

typedef
bottom_t0ype_uni = {a:t@ype} (a)
typedef
bottom_t0ype_exi = [a:t@ype | false] (a)

vtypedef
bottom_vt0ype_uni = {a:vt@ype} (a)
vtypedef
bottom_vt0ype_exi = [a:vt@ype | false] (a)

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

typedef
cmpval_fun
  (a: t@ype) = (a, a) -<fun> int
typedef
cmpval_funenv
  (a: t@ype, vt: t@ype) = (a, a, !vt) -<fun> int
stadef cmpval = cmpval_fun
stadef cmpval = cmpval_funenv

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

typedef cmpref_fun
  (a: vt@ype) = (&RD(a), &RD(a)) -<fun> int
typedef cmpref_funenv
  (a: vt@ype, vt: vt@ype) = (&RD(a), &RD(a), !vt) -<fun> int
stadef cmpref = cmpref_fun
stadef cmpref = cmpref_funenv

(* ****** ****** *)
//
// HX: [lazy(T)] :
// suspended evaluation of type T
//
abstype
lazy_t0ype_type (t@ype+) = ptr
typedef lazy (a:t@ype) = lazy_t0ype_type (a)
//
(* ****** ****** *)
//
// HX: [lazy_vt(VT)] :
// suspended computation of viewtype VT
//
absvtype
lazy_vt0ype_vtype (vt@ype+) = ptr
vtypedef lazy_vt (a: vt@ype)= lazy_vt0ype_vtype (a)
//
(* ****** ****** *)

abst@ype
undefined_t0ype = $extype"atstype_undefined"
absvt@ype
undefined_vt0ype = $extype"atstype_undefined"

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

#if VERBOSE_PRELUDE #then
#print "Loading [basics_sta.sats] finishes!\n"
#endif // end of [VERBOSE_PRELUDE]

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

(* end of [basics_sta.sats] *)