Leonardo de Moura
b4b60dc326
feat: add List.filterMapM
2020-08-14 10:50:48 -07:00
Leonardo de Moura
bd8e2d305f
feat: add Array.filterMap
2020-08-14 10:50:48 -07:00
Leonardo de Moura
81ae6a734b
feat: mark List.toArray with [matchPattern]
2020-08-13 14:25:47 -07:00
Sebastian Ullrich
b2714d36ef
fix: String: take/drop characters, not bytes
2020-08-11 18:24:47 -07:00
Leonardo de Moura
aefc9a473f
feat: add auxiliary definitions for compiling array literals in pattern matching expressions
2020-08-07 09:23:33 -07:00
Sebastian Ullrich
c5d226ba36
feat: HasBeq for Syntax, Substring
2020-08-06 09:26:49 -07:00
Leonardo de Moura
cbb14673ef
chore: move RBTree and RBMap to Std
2020-06-25 13:26:16 -07:00
Leonardo de Moura
11ed7c6195
chore: move PersistentArray to Std
2020-06-25 13:02:21 -07:00
Leonardo de Moura
02aa8498cd
chore: move AssocList to Std
2020-06-25 12:52:23 -07:00
Leonardo de Moura
1612097788
chore: move HashMap and HashSet to Std
2020-06-25 12:46:56 -07:00
Leonardo de Moura
1be221a1f4
chore: move PersistentHashMap and PersistentHashSet to Std
2020-06-25 11:56:00 -07:00
Leonardo de Moura
59c082ef1a
chore: move Stack and Queue to Std
2020-06-25 11:35:09 -07:00
Leonardo de Moura
18431d7b52
chore: move DList to Std
2020-06-25 11:31:04 -07:00
Leonardo de Moura
7897769732
chore: move BinomialHeap to Std
2020-05-22 11:10:47 -07:00
Leonardo de Moura
bd58048449
chore: { <source> with ... } syntax
2020-05-20 15:08:43 -07:00
Sebastian Ullrich
66a0a239a3
fix: structure instances missing comma
2020-05-20 15:12:42 +02:00
Leonardo de Moura
50990b99d6
chore: remove unnecessary annotations
2020-05-12 15:02:03 -07:00
Leonardo de Moura
33a10130cf
chore: fix stdlib
2020-05-12 15:02:03 -07:00
Sebastian Ullrich
386c706f3e
feat: basic parenthesizer
2020-05-04 14:28:36 -07:00
Sebastian Ullrich
8f67db0101
refactor: never implicitly ignore monadic results
...
Also change `do e; f` to desugar to `e *> f` so that it is affected as well
2020-04-23 11:09:59 -07:00
Leonardo de Moura
e22af8d1ef
feat: add FloatArray
...
cc @dselsam
2020-04-07 18:05:54 -07:00
Leonardo de Moura
b8ea55c989
feat: expose some transcendental functions from the C library
...
cc @dselsam
2020-04-06 15:22:25 -07:00
Leonardo de Moura
705530b62b
fix: remove DecidableEq for Float
...
We cannot implement `DecidableEq Float` using C equality for
`double`. Reason: the C implementation is not even reflexive.
If we need `DecidableEq Float`, we will need to provide our own
implementation (i.e., a wrapper around the one provided by the
hardware). In this commit, we implement `HasBeq Float` instead.
cc @dselsam
2020-04-06 14:10:18 -07:00
Sebastian Ullrich
f66039f7f0
feat: generalize Array function universes
2020-04-06 13:48:09 -07:00
Leonardo de Moura
485034bbba
fix: bug at ir.cpp
2020-04-03 17:39:28 -07:00
Leonardo de Moura
c236a179f2
feat: enable externs
2020-04-03 17:19:48 -07:00
Leonardo de Moura
0e2ebd36ff
feat: make sure Float is in WHNF
2020-04-03 17:07:29 -07:00
Leonardo de Moura
71397aad36
feat: runtime primitives
2020-04-03 15:55:39 -07:00
Leonardo de Moura
52cffcb67f
feat: add Float.lean
2020-04-03 15:40:38 -07:00
Sebastian Ullrich
b6fc9428f1
fix: support Windows newlines and '\r' escape
2020-03-27 13:21:21 -07:00
Leonardo de Moura
2c12a073fa
fix: missing file
2020-03-23 15:49:22 -07:00
Leonardo de Moura
12c5075c67
fix: String.dropRight
2020-03-23 14:51:05 -07:00
Leonardo de Moura
41949ee801
refactor: String.toNat ==> String.toNat? and String.toNat!
2020-03-23 14:29:48 -07:00
Sebastian Ullrich
ed14375dad
feat: sort and deduplicate "expected" tokens in parser error messages
2020-03-19 17:17:08 -07:00
Sebastian Ullrich
e999fa678d
feat: add some useful helper functions I didn't actually use in the end
2020-03-19 17:14:31 -07:00
Leonardo de Moura
cd8bd55311
feat: make sure Char.ofNat can be efficiently reduced in the kernel and WHNF
2020-03-18 16:41:48 -07:00
Leonardo de Moura
2d7ec0b49c
fix: bug at unsafe umapMAux implementation
...
closes #125
2020-03-14 13:41:14 -07:00
Leonardo de Moura
6ad0c2cc18
feat: simplify unsafeCast
2020-03-14 13:10:56 -07:00
Leonardo de Moura
a0090b378b
feat: move Array extensionality theorems to Init
2020-03-13 06:39:13 -07:00
Leonardo de Moura
a8c3322ac8
doc: expand dependent pattern matching support for array literals
2020-03-13 06:39:13 -07:00
Leonardo de Moura
50acb88727
feat: add auxiliary function for matching array literals
2020-03-11 11:57:01 -07:00
Leonardo de Moura
0893b62598
perf: avoid unnecessary overhead at HashSet
...
List instead of AssocList saves one word per entry.
2020-03-02 08:40:15 -08:00
Leonardo de Moura
58ddeedced
feat: add List.replace
2020-03-02 08:30:20 -08:00
Leonardo de Moura
0781c74754
chore: variable order consistency
2020-02-24 18:29:24 -08:00
Leonardo de Moura
370dada9a3
feat: add findEntry? functions
2020-02-24 15:47:59 -08:00
Leonardo de Moura
36096abec0
feat: add Array.findIdxM? and Array.getIdx?
2020-02-19 14:54:55 -08:00
Leonardo de Moura
ca20bb112f
feat: add helper
2020-02-17 12:10:52 -08:00
Leonardo de Moura
3c235c3613
chore: naming convention
2020-02-09 17:10:20 -08:00
Leonardo de Moura
3f4c27efa5
feat: add getFieldViews
2020-02-05 19:15:05 -08:00
Leonardo de Moura
bcfaeaceab
feat: change ite and dite argument order
...
Motivation: make sure `propagateExpectedType` heuristic is applied in
the new frontend when processing them.
2020-02-03 14:11:29 -08:00
