max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
20530 commits 1 branch 0 tags 5.3 GiB
Commit graph

1256 commits

Author SHA1 Message Date
Sebastian Ullrich
eb5a171764 feat: adjust semantics to new syntax 2020-08-19 09:56:23 -07:00
Leonardo de Moura
9158ba60ea feat: add IO.toEIO 2020-08-19 09:43:26 -07:00
Leonardo de Moura
390aef535e chore: remove workaround 2020-08-18 17:22:51 -07:00
Leonardo de Moura
64f5ac37c1 fix: missing instance 2020-08-18 17:22:22 -07:00
Leonardo de Moura
4eef5a2fb6 fix: missing instance 2020-08-18 17:22:08 -07:00
Leonardo de Moura
58c4d8bfc0 refactor: add MonadStateOf 
@Kha I tried to remove `MonadExceptOf` by adding `HasThrow` and
`HasCatch`, but this change impacts our ability to define polymorphic
methods such as `finally` which is parametrized by `[MonadExcept]`.
If we remove the `outParam` from `[MonadExcept]`, then we will need to
know the exception at `finally`, or add two instances `[HasCatch]` and
`[HasThrow]`. So, it seems it is more convenient to have
`[MonadExceptOf]` and `[MonadExcept]`. Thus, I applied this approach
to `[MonadState]`
 2020-08-18 16:35:33 -07:00
Leonardo de Moura
e70ff5b773 refactor: simplify CoreM using StateRefT 2020-08-18 16:02:29 -07:00
Leonardo de Moura
b8044fdf97 chore: remove MonadExceptOf from MonadIO 
@Kha we currently do not need this feature. We may add it back when needed.
 2020-08-18 15:40:16 -07:00
Leonardo de Moura
5605735137 feat: remove outparam from MonadState 
We add helper classes with `outParam`.

@Kha This is similar to the `MonadExceptOf` modification.
Motivation: the new `StateRefT` (state monad implemented using
`IO.Ref`) makes is it quite cheap to have multiple states on the
stack. But, we need a mechanism for accessing the different states in
a convenient way.
Note that, I did not add a `MonadStateOf` class, but helper classes
such as `HasGet` which uses `outParam`. I will do the same for `MonadExcept`.

Summary:
- `get` gets the state on the top of the Monad stack
- `getThe σ` gets the state with type `σ`
- `modify f` modifies the state on the top of the Monad stack.
   We use `modify fun s => { s with ... }` quite often, and we cannot
   infer type of `s` here.
- `modifyThe σ f` allows us to select which state on the stack we are modifying.
- I didn't add `setThe`, since we usually can infer the state type at
  `set s`. In the whole codebase, we have only one instance where this
  is not true.
 2020-08-18 15:15:31 -07:00
Leonardo de Moura
f01d45a6c1 feat: add StateRef 2020-08-18 13:54:51 -07:00
Leonardo de Moura
1e496fb32d feat: helper instance 2020-08-18 13:26:14 -07:00
Leonardo de Moura
aa2f834c0f feat: add mkMonadIO and modifyGet 2020-08-18 13:25:15 -07:00
Leonardo de Moura
3342ba08d2 feat: implement let elaborators without using match_syntax 
@Kha I had to do this because of the `ident` vs `Term.id` recurrent
issue. `match_syntax` fails if a `Term.id` is used at `Term.letIdDecl`
where an `ident` is expected.
We should try to remove `Term.id` in the future.
 2020-08-17 09:27:54 -07:00
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
Leonardo de Moura
6c234daad7 chore: MonadExceptCore => MonadExceptOf 2020-08-13 09:28:23 -07:00
Wojciech Nawrocki
55655869b7 feat: default to binary file mode on Windows 2020-08-13 09:21:35 -07:00
Leonardo de Moura
d7add53229 feat: add MonadExceptCore 2020-08-13 09:19:26 -07:00
Sebastian Ullrich
b2714d36ef fix: String: take/drop characters, not bytes 2020-08-11 18:24:47 -07:00
Leonardo de Moura
f1c7665a93 feat: validate patterns, and collect pattern variables 2020-08-11 18:19:29 -07:00
Leonardo de Moura
5a09883cc7 chore: add namedPattern 2020-08-11 15:04:09 -07:00
Leonardo de Moura
61f8b4ef07 feat: add support for maximum recursion depth checks at MacroM 2020-08-10 16:50:12 -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
Sebastian Ullrich
0f7f49aa06 feat: dbgTraceVal 2020-08-06 09:26:48 -07:00
Leonardo de Moura
447000a797 fix: >>= associativity 2020-08-03 14:00:19 -07:00
Sebastian Ullrich
719819bf49 fix: finally shouldn't call finalizer when finalizer throws 2020-07-10 07:42:26 -07:00
Sebastian Ullrich
b40ef65b39 feat: add IO.eprint(ln) for printing to stderr 
Most useful when stdout is being consumed by another program
 2020-07-06 09:22:47 -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
2dd1d3ac3e chore: move ShareCommon to Std 2020-06-25 11:45:29 -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
decab1ea57 fix: missing import 2020-06-25 11:20:47 -07:00
Leonardo de Moura
c6e7ea8fd5 feat: add ParserDescr.parser constructor for embedding parser definitions into parser descriptions 2020-06-16 14:06:46 -07:00
Leonardo de Moura
f61e4ffbbd chore: ParserDescr.parser ==> ParserDescr.cat 2020-06-16 13:40:16 -07:00
Sebastian Ullrich
6404af6983 feat: IO.Prim.withIsolatedStreams 2020-06-16 10:41:42 -07:00
Sebastian Ullrich
f4c28fbe5f chore: remove unnecessary getByte/putByte IO primitives 2020-06-16 12:06:53 +02:00
Simon Hudon
a64e78b90b feat: add std streams 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2020-06-16 12:06:53 +02:00
Leonardo de Moura
09eb27404f chore: remove <$ and $> notation 
cc @Kha
 2020-06-15 14:52:31 -07:00
Leonardo de Moura
1477d23546 feat: remove ParserDescr.prec and update ParserDescr.trailingNode/ParserDescr.node 2020-06-10 14:57:55 -07:00
Leonardo de Moura
f23780a334 chore: add hack for allowing old and new frontends to parse Core.lean 2020-06-09 14:11:34 -07:00
Leonardo de Moura
e62e30ad0f chore: remove whitespace 2020-06-09 14:11:34 -07:00
Leonardo de Moura
8972c7e666 feat: revised syntax commands 2020-06-08 16:12:06 -07:00
Leonardo de Moura
1554f7f99a fix: ParserDescr 
This commit also adds the new constructor `ParserDescr.rblLt`
 2020-06-08 16:12:05 -07:00
Leonardo de Moura
dbe4aa447e chore: explicit lbp at ParserDescr.symbol 2020-05-27 16:12:53 -07:00