@@ -1449,58 +1449,6 @@ def post_slice(xs:n=>a, start:Post n, end:Post n) -> List a given (n|Ix, a) =
14491449 to_list for i:(Fin slice_size).
14501450 xs[unsafe_from_ordinal(n=n, ordinal i + ordinal start)]
14511451
1452- '## Dynamic buffer
1453-
1454- struct DynBuffer(a) =
1455- size : Ptr Nat
1456- max_size : Ptr Nat
1457- buffer : Ptr (Ptr a)
1458-
1459- def with_dynamic_buffer(action: (DynBuffer a) -> {IO} b) -> {IO} b given (a|Storable, b) =
1460- initMaxSize = 256
1461- sizePtr <- with_alloc 1
1462- store(sizePtr, 0)
1463- maxSizePtr <- with_alloc 1
1464- store(maxSizePtr, initMaxSize)
1465- bufferPtr <- with_alloc 1
1466- store(bufferPtr, malloc initMaxSize)
1467- result = action $ DynBuffer(sizePtr, maxSizePtr, bufferPtr)
1468- free $ load bufferPtr
1469- result
1470-
1471- def maybe_increase_buffer_size(db: DynBuffer a, sizeDelta:Nat) -> {IO} () given (a|Storable) =
1472- size = load db.size
1473- max_size = load db.max_size
1474- bufPtr = load db.buffer
1475- newSize = sizeDelta + size
1476- if newSize > max_size then
1477- -- TODO: maybe this should use integer arithmetic?
1478- newMaxSize = f_to_n $ 2.0 `pow` (ceil $ log2 $ n_to_f newSize)
1479- newBufPtr = malloc newMaxSize
1480- memcpy(newBufPtr, bufPtr, size)
1481- free bufPtr
1482- store(db.max_size, newMaxSize)
1483- store(db.buffer , newBufPtr)
1484-
1485- def add_at_nat_ptr(ptr: Ptr Nat, n:Nat) -> {IO} () =
1486- store(ptr, load ptr + n)
1487-
1488- def extend_dynamic_buffer(buf: DynBuffer a, new:List a) -> {IO} () given (a|Storable) =
1489- AsList(n, xs) = new
1490- maybe_increase_buffer_size(buf, n)
1491- bufPtr = load buf.buffer
1492- size = load buf.size
1493- store_table(bufPtr +>> size, xs)
1494- add_at_nat_ptr(buf.size, n)
1495-
1496- def load_dynamic_buffer(buf: DynBuffer a) -> {IO} (List a) given (a|Storable) =
1497- bufPtr = load buf.buffer
1498- size = load buf.size
1499- AsList(size, table_from_ptr bufPtr)
1500-
1501- def push_dynamic_buffer(buf: DynBuffer a, x:a) -> {IO} () given (a|Storable) =
1502- extend_dynamic_buffer(buf, to_list [x])
1503-
15041452'## Strings and Characters
15051453
15061454String : Type = List Char
@@ -1718,46 +1666,6 @@ def bounded_iter(
17181666 then Done fallback
17191667 else body i
17201668
1721- '### Environment Variables
1722-
1723- def from_c_string(s:CString) -> {IO} (Maybe String) =
1724- case c_string_ptr s of
1725- Nothing -> Nothing
1726- Just(ptr) ->
1727- Just do
1728- buf <- with_dynamic_buffer
1729- i <- iter
1730- c = load $ ptr +>> i
1731- if c == '\NUL'
1732- then Done $ load_dynamic_buffer buf
1733- else
1734- push_dynamic_buffer(buf, c)
1735- Continue
1736-
1737- foreign "getenv" getenvFFI : (RawPtr) -> {IO} RawPtr
1738-
1739- def get_env(name:String) -> {IO} Maybe String =
1740- cStr <- with_c_string name
1741- getenvFFI cStr.ptr | CString | from_c_string
1742-
1743- def check_env(name:String) -> {IO} Bool =
1744- is_just $ get_env name
1745-
1746- '### More Stream IO
1747-
1748- def fread(stream:Stream ReadMode) -> {IO} String =
1749- -- TODO: allow reading longer files!
1750- n = 4096
1751- ptr:(Ptr Char) <- with_alloc n
1752- buf <- with_dynamic_buffer
1753- iter \_.
1754- numRead = i_to_w32 $ i64_to_i $ freadFFI(ptr.val, 1, n_to_i64 n, stream.ptr)
1755- extend_dynamic_buffer(buf, string_from_char_ptr(numRead, ptr))
1756- if numRead == n_to_w32 n
1757- then Continue
1758- else Done ()
1759- load_dynamic_buffer buf
1760-
17611669'### Print
17621670
17631671def get_output_stream() -> {IO} Stream WriteMode =
@@ -1769,20 +1677,6 @@ def print(s:String) -> {IO} () =
17691677 fwrite(stream, s)
17701678 fwrite(stream, "\n")
17711679
1772- '### Shelling Out
1773-
1774- foreign "popen" popenFFI : (RawPtr, RawPtr) -> {IO} RawPtr
1775- foreign "remove" removeFFI : (RawPtr) -> {IO} Int64
1776- foreign "mkstemp" mkstempFFI : (RawPtr) -> {IO} Int32
1777- foreign "close" closeFFI : (Int32) -> {IO} Int32
1778-
1779- def shell_out(command:String) -> {IO} String =
1780- modeStr = "r"
1781- with_c_string command \command'.
1782- with_c_string modeStr \modeStr'.
1783- pipe = Stream $ popenFFI(command'.ptr, modeStr'.ptr)
1784- fread pipe
1785-
17861680'## Partial functions
17871681A partial function in this context is a function that can error.
17881682i.e. a function that is not actually defined for all of its supposed domain.
@@ -1797,58 +1691,6 @@ def error(s:String) -> a given (a|Data) = unsafe_io \.
17971691
17981692def todo() ->> a given (a|Data) = error "TODO: implement it!"
17991693
1800- '### File Operations
1801-
1802- def delete_file(f:FilePath) -> {IO} () =
1803- s <- with_c_string(f)
1804- removeFFI s.ptr
1805- ()
1806-
1807- def with_file(
1808- f:FilePath,
1809- mode:StreamMode,
1810- action:(Stream mode) -> {IO} a
1811- ) -> {IO} a given (a|Data) =
1812- stream = fopen(f, mode)
1813- if is_null_raw_ptr stream.ptr
1814- then
1815- error $ "Unable to open file: " <> f
1816- else
1817- result = action stream
1818- fclose stream
1819- result
1820-
1821- def write_file(f:FilePath, s:String) -> {IO} () =
1822- with_file(f, WriteMode) \stream. fwrite(stream, s)
1823-
1824- def read_file(f:FilePath) -> {IO} String =
1825- with_file(f, ReadMode) \stream. fread stream
1826-
1827- def has_file(f:FilePath) -> {IO} Bool =
1828- stream = fopen(f, ReadMode)
1829- result = not (is_null_raw_ptr stream.ptr)
1830- if result then fclose stream
1831- result
1832-
1833- '### Temporary Files
1834-
1835- def new_temp_file() -> {IO} FilePath =
1836- s <- with_c_string "/tmp/dex-XXXXXX"
1837- fd = mkstempFFI s.ptr
1838- closeFFI fd
1839- string_from_char_ptr(15, (Ptr s.ptr))
1840-
1841- def with_temp_file(action: (FilePath) -> {IO} a) -> {IO} a given (a) =
1842- tmpFile = new_temp_file()
1843- result = action tmpFile
1844- delete_file tmpFile
1845- result
1846-
1847- def with_temp_files(action: (n=>FilePath) -> {IO} a) -> {IO} a given (n|Ix, a) =
1848- tmpFiles = for i. new_temp_file()
1849- result = action tmpFiles
1850- for i. delete_file tmpFiles[i]
1851- result
18521694
18531695'### Table operations
18541696
@@ -2391,11 +2233,6 @@ def evalpoly(coefficients:n=>v, x:Float) -> v given (n|Ix, v|VSpace) =
23912233 -- Evaluate a polynomial at x. Same as Numpy's polyval.
23922234 fold zero \i c. coefficients[i] + x .* c
23932235
2394- '## TestMode
2395- -- TODO: move this to be in Testing Helpers
2396-
2397- def dex_test_mode() -> Bool = unsafe_io \. check_env "DEX_TEST_MODE"
2398-
23992236'## Exception effect
24002237-- TODO: move `error` and `todo` to here.
24012238
@@ -2429,15 +2266,6 @@ instance Subset(b, Either(a,b)) given (a|Data, b|Data)
24292266 Left( x) -> error "Can't project Left branch to Right branch"
24302267 Right(x) -> x
24312268
2432- '## Testing Helpers
2433-
2434- -- -- Reliably causes a segfault if pointers aren't initialized to zero.
2435- -- -- TODO: add this test when we cache modules
2436- -- justSomeDataToTestCaching = toList for i:(Fin 100).
2437- -- if ordinal i == 0
2438- -- then Left (toList [1,2,3])
2439- -- else Right 1
2440-
24412269'### Index set for tables
24422270
24432271def int_to_reversed_digits(k:Nat) -> a=>b given (a|Ix, b|Ix) =
@@ -2465,8 +2293,7 @@ instance Ix(a=>b) given (a|Ix, b|Ix)
24652293instance NonEmpty(a=>b) given (a|Ix, b|NonEmpty)
24662294 first_ix = unsafe_from_ordinal 0
24672295
2468- '### stack
2469- -- TODO: replace `DynBuffer` with this?
2296+ '### Stack
24702297
24712298struct Stack(h:Heap, a|Data) =
24722299 size_ref : Ref h Nat
@@ -2544,13 +2371,138 @@ def with_stack_internal(f:(given (h:Heap), Stack(h, Char)) -> {State h} ()) -> L
25442371 f stack
25452372 stack.read()
25462373
2374+ '### Environment Variables
2375+
2376+ def from_c_string(s:CString) -> {IO} (Maybe String) =
2377+ case c_string_ptr s of
2378+ Nothing -> Nothing
2379+ Just(ptr) ->
2380+ Just do
2381+ stack <- with_stack Char
2382+ i <- iter
2383+ c = load $ ptr +>> i
2384+ if c == '\NUL'
2385+ then Done $ stack.read()
2386+ else
2387+ stack.push(c)
2388+ Continue
2389+
25472390def show_any(x:a) -> String given (a) = unsafe_coerce(to=String, %showAny(x))
25482391
25492392def coerce_table(m|Ix, x:n=>a) -> m => a given (n|Ix, a|Data) =
25502393 if size m == size n
25512394 then unsafe_coerce(to=m=>a, x)
25522395 else error "mismatched sizes in table coercion"
25532396
2397+ '### GetEnv
2398+
2399+ foreign "getenv" getenvFFI : (RawPtr) -> {IO} RawPtr
2400+
2401+ def get_env(name:String) -> {IO} Maybe String =
2402+ cStr <- with_c_string name
2403+ getenvFFI cStr.ptr | CString | from_c_string
2404+
2405+ def check_env(name:String) -> {IO} Bool =
2406+ is_just $ get_env name
2407+
2408+ '## Testing Helpers
2409+
2410+ -- -- Reliably causes a segfault if pointers aren't initialized to zero.
2411+ -- -- TODO: add this test when we cache modules
2412+ -- justSomeDataToTestCaching = toList for i:(Fin 100).
2413+ -- if ordinal i == 0
2414+ -- then Left (toList [1,2,3])
2415+ -- else Right 1
2416+
2417+ '### TestMode
2418+
2419+ def dex_test_mode() -> Bool = unsafe_io \. check_env "DEX_TEST_MODE"
2420+
2421+
2422+ '### More Stream IO
2423+
2424+ def fread(stream:Stream ReadMode) -> {IO} String =
2425+ -- TODO: allow reading longer files!
2426+ n = 4096
2427+ ptr:(Ptr Char) <- with_alloc n
2428+ stack <- with_stack Char
2429+ iter \_.
2430+ numRead = i_to_w32 $ i64_to_i $ freadFFI(ptr.val, 1, n_to_i64 n, stream.ptr)
2431+ AsList(_, new_chars) = string_from_char_ptr(numRead, ptr)
2432+ stack.extend(new_chars)
2433+ if numRead == n_to_w32 n
2434+ then Continue
2435+ else Done ()
2436+ stack.read()
2437+
2438+
2439+ '### Shelling Out
2440+
2441+ foreign "popen" popenFFI : (RawPtr, RawPtr) -> {IO} RawPtr
2442+ foreign "remove" removeFFI : (RawPtr) -> {IO} Int64
2443+ foreign "mkstemp" mkstempFFI : (RawPtr) -> {IO} Int32
2444+ foreign "close" closeFFI : (Int32) -> {IO} Int32
2445+
2446+ def shell_out(command:String) -> {IO} String =
2447+ modeStr = "r"
2448+ with_c_string command \command'.
2449+ with_c_string modeStr \modeStr'.
2450+ pipe = Stream $ popenFFI(command'.ptr, modeStr'.ptr)
2451+ fread pipe
2452+
2453+ '### File Operations
2454+
2455+ def delete_file(f:FilePath) -> {IO} () =
2456+ s <- with_c_string(f)
2457+ removeFFI s.ptr
2458+ ()
2459+
2460+ def with_file(
2461+ f:FilePath,
2462+ mode:StreamMode,
2463+ action:(Stream mode) -> {IO} a
2464+ ) -> {IO} a given (a|Data) =
2465+ stream = fopen(f, mode)
2466+ if is_null_raw_ptr stream.ptr
2467+ then
2468+ error $ "Unable to open file: " <> f
2469+ else
2470+ result = action stream
2471+ fclose stream
2472+ result
2473+
2474+ def write_file(f:FilePath, s:String) -> {IO} () =
2475+ with_file(f, WriteMode) \stream. fwrite(stream, s)
2476+
2477+ def read_file(f:FilePath) -> {IO} String =
2478+ with_file(f, ReadMode) \stream. fread stream
2479+
2480+ def has_file(f:FilePath) -> {IO} Bool =
2481+ stream = fopen(f, ReadMode)
2482+ result = not (is_null_raw_ptr stream.ptr)
2483+ if result then fclose stream
2484+ result
2485+
2486+ '### Temporary Files
2487+
2488+ def new_temp_file() -> {IO} FilePath =
2489+ s <- with_c_string "/tmp/dex-XXXXXX"
2490+ fd = mkstempFFI s.ptr
2491+ closeFFI fd
2492+ string_from_char_ptr(15, (Ptr s.ptr))
2493+
2494+ def with_temp_file(action: (FilePath) -> {IO} a) -> {IO} a given (a) =
2495+ tmpFile = new_temp_file()
2496+ result = action tmpFile
2497+ delete_file tmpFile
2498+ result
2499+
2500+ def with_temp_files(action: (n=>FilePath) -> {IO} a) -> {IO} a given (n|Ix, a) =
2501+ tmpFiles = for i. new_temp_file()
2502+ result = action tmpFiles
2503+ for i. delete_file tmpFiles[i]
2504+ result
2505+
25542506'### Linear Algebra
25552507
25562508def linspace(n|Ix, low:Float, high:Float) -> n=>Float =
0 commit comments