-
Notifications
You must be signed in to change notification settings - Fork 0
/
core-strings.boba
169 lines (142 loc) · 5.29 KB
/
core-strings.boba
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
import { * } "core-kinds" as kinds
import { * } "core-boolean" as bools
import { * } "core-numbers" as nums
import native "strings"
import native "unicode/utf8"
type Rune (t : Trust) (c : Clearance)
native trust-rune
: z... (Rune t c)^s ===[ e... ][ p... ][ True ]==> z... (Rune True c)^s
=
#
native clear-rune
: z... (Rune t c)^s ===[ e... ][ p... ][ True ]==> z... (Rune t True)^s
=
#
native eq-rune
: z... (Rune t c)^s (Rune t c)^r ===[ e... ][ p... ][ True ]==> z... Bool^q
=
# runeR := fiber.PopOneValue().(rune)
# runeL := fiber.PopOneValue().(rune)
# fiber.PushValue(runeL == runeR)
type String (t : Trust) (c : Clearance)
native trust-string
: z... (String t c)^s ===[ e... ][ p... ][ True ]==> z... (String True c)^s
=
#
native distrust-string
: z... (String t c)^s ===[ e... ][ p... ][ True ]==> z... (String False c)^s
=
#
native clear-string
: z... (String t c)^s ===[ e... ][ p... ][ True ]==> z... (String t True)^s
=
#
native secret-string
: z... (String t c)^s ===[ e... ][ p... ][ True ]==> z... (String t False)^s
=
#
native nil-string
: z... ===[ e... ][ p... ][ True ]==> z... (String t c)^s
=
# fiber.PushValue("")
native snoc-string
: z... (String t1 c1)^s (Rune t2 c2)^r ===[ e... ][ p... ][ True ]==> z... (String (t1 && t2) (c1 && c2))^q
=
# r := fiber.PopOneValue().(rune)
# str := fiber.PopOneValue().(string)
# newStr := strings.Clone(str)
# newStr = newStr + string(r)
# fiber.PushValue(newStr)
native head-string
: z... (String t c)^s ===[ e... ][ p... ][ True ]==> z... (Rune t c)^r
=
# str := fiber.PopOneValue().(string)
# r, _ := utf8.DecodeRuneInString(str)
# fiber.PushValue(r)
native tail-string
: z... (String t c)^s ===[ e... ][ p... ][ True ]==> z... (String t c)^r
=
# str := fiber.PopOneValue().(string)
# _, ind := utf8.DecodeRuneInString(str)
# fiber.PushValue(str[ind:])
native decode-rune-in-string
: z... (String t c)^s ===[ e... ][ p... ][ True ]==> z... (INative one)^q (Rune t c)^r
=
# str := fiber.PopOneValue().(string)
# r, s := utf8.DecodeRuneInString(str)
# fiber.PushValue(s)
# fiber.PushValue(r)
native length-string
: z... (String t c)^s ===[ e... ][ p... ][ True ]==> z... (INative one)^r
=
# strLen := int(len(fiber.PopOneValue().(string)))
# fiber.PushValue(strLen)
native left-slice-string
: z... (INative u)^q (String t c)^r ===[ e... ][ p... ][ True ]==> z... (String t c)^s
=
# str := fiber.PopOneValue().(string)
# ind := fiber.PopOneValue().(int)
# fiber.PushValue(str[ind:])
about :
/// Clone returns a fresh copy of s. It guarantees to make a copy of s
/// into a new allocation, which can be important when retaining only a
/// small substring of a much larger string. Using Clone can help such
/// programs use less memory. Of course, since using Clone makes a copy,
/// overuse of Clone can make programs use more memory. Clone should
/// typically be used only rarely, and only when profiling indicates that
/// it is needed. For strings of length zero the string "" will be
/// returned and no allocation is made.
native clone-string
: z... (String t c)^s1 ===[ e... ][ p... ][ True ]==> z... (String t c)^s1 (String t c)^s2
=
# str := fiber.PeekOneValue().(string)
# fiber.PushValue(strings.Clone(str))
about :
/// Compare returns an integer comparing two strings lexicographically.
/// The result will be 0 if a == b, -1 if a < b, and +1 if a > b.
/// Compare is included only for symmetry with package bytes. It is usually
/// clearer and always faster to use the built-in string comparison
/// operators ==, <, >, and so on.
native compare-string
: z... (String t1 c1)^s1 (String t2 c2)^s2 ===[ e... ][ p... ][ True ]==> z... (I32 one)^s3
=
# strR := fiber.PopOneValue().(string)
# strL := fiber.PopOneValue().(string)
# fiber.PushValue(strings.Compare(strL, strR))
about :
/// Concatenates two strings on the top of the value stack, such that
/// the second from the top appears before the top in the resulting string.
/// Trust and clearance are preserved such that untrusted or uncleared strings
/// taint the result.
native concat-string
: z... (String t1 c1)^s1 (String t2 c2)^s2 ===[ e... ][ p... ][ True ]==> z... (String (t1 && t2) (c1 && c2))^s3
=
# strR := fiber.PopOneValue().(string)
# strL := fiber.PopOneValue().(string)
# fiber.PushValue(strL + strR)
about :
/// Pushes a `Bool` result of checking whether the two strings are equal.
native eq-string
: z... (String t1 c1)^s1 (String t2 c2)^s2 ===[ e... ][ p... ][ True ]==> z... Bool^s3
=
# strR := fiber.PopOneValue().(string)
# strL := fiber.PopOneValue().(string)
# fiber.PushValue(strL == strR)
effect io!
type Console : Permission
native print-rune
: z... (Rune t True)^s ===[ e..., io! ][ p..., Console ][ True ]==> z...
=
# r := fiber.PopOneValue().(rune)
# print(r)
native print-string
: z... (String t True)^s ===[ e..., io! ][ p..., Console ][ True ]==> z...
=
# str := fiber.PopOneValue().(string)
# print(str)
native println-string
: z... (String t True)^s ===[ e..., io! ][ p..., Console ][ True ]==> z...
=
# str := fiber.PopOneValue().(string)
# println(str)
export { * }