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

73 commits

Author SHA1 Message Date
Leonardo de Moura
2e0629133f feat(library/init/lean/ir): add emit_lit 2018-05-09 18:29:54 -07:00
Leonardo de Moura
fc840eab3f feat(library/init/lean/ir): add emit_unop 2018-05-09 18:20:46 -07:00
Leonardo de Moura
c7153f7661 chore(library/init/lean/ir/extract_cpp): cleanup 2018-05-09 18:03:00 -07:00
Leonardo de Moura
9345765815 feat(library/init/lean/ir/extract_cpp): start IR => C++ extractor 2018-05-09 17:47:55 -07:00
Leonardo de Moura
7d196f58c3 chore(library/init/lean/ir): remove ashr 2018-05-09 17:43:25 -07:00
Leonardo de Moura
5baae4724f feat(library/init/lean/ir): distinguish free and dealloc 2018-05-09 17:43:12 -07:00
Leonardo de Moura
3be7540efe chore(library/init): use mfor instead of mmap' 2018-05-09 15:41:53 -07:00
Leonardo de Moura
6368d0c5f6 chore(library/init/lean/name_mangling): allow custom prefix when mangling names 2018-05-09 15:01:12 -07:00
Leonardo de Moura
0c0972f317 feat(library/init/lean): name mangling 2018-05-09 09:19:32 -07:00
Leonardo de Moura
3f883bd949 chore(library/init/lean/parser/parser): add monad_fail instance 2018-05-09 09:19:14 -07:00
Leonardo de Moura
874f9caf13 feat(library/init/control/state): modify monad_run instance for state_t 
@Kha, I was having to use `(run ...).1` in many places
in my code. So, I changed the instance
```
instance (σ m out) [monad_run out m] : monad_run (λ α, σ → out (α × σ)) (state_t σ m) :=
⟨λ α x, run ∘ (λ σ, x.run σ)⟩
```
to
```
instance (σ : Type u) (m out : Type u → Type v) [functor m] [monad_run out m] : monad_run (λ α, σ → out α) (state_t σ m) :=
⟨λ α x, run ∘ (λ σ, prod.fst <$> (x.run σ))⟩
```
If we want to get the resultant state in an action `act`, we can just
use `run (act >> get) init_state`.
 2018-05-08 17:32:54 -07:00
Leonardo de Moura
b0641ba770 feat(frontends/lean/elaborator): add support for definitions such as monad_run.run 
cc @Kha
 2018-05-08 17:14:52 -07:00
Leonardo de Moura
ab39ef261d refactor(library/init/lean/ir/ssa_check): use format instead of blockid_error 2018-05-08 15:47:02 -07:00
Leonardo de Moura
60a275a464 chore(library/init/lean/ir/elim_phi): use idiom: define run for every monad 2018-05-08 15:46:30 -07:00
Leonardo de Moura
7f85f0893c refactor(library/init/lean/ir): cleanup 2018-05-08 15:38:43 -07:00
Leonardo de Moura
00147df082 chore(library/init/lean/ir/ssa_check): use format for error messages 2018-05-08 14:50:58 -07:00
Leonardo de Moura
9373133800 chore(library/init/lean/ir/type_check): cleanup 2018-05-08 14:50:28 -07:00
Leonardo de Moura
e40f37b08e feat(library/init/lean/ir): add type checker 2018-05-07 18:07:04 -07:00
Leonardo de Moura
f7c4134452 refactor(library/init/lean/ir): we can use the cast instruction for boxing/unboxing 2018-05-07 18:07:04 -07:00
Leonardo de Moura
79f351d177 fix(library/init/lean/ir): parser and test 2018-05-07 18:07:04 -07:00
Leonardo de Moura
0a9bd8caa8 chore(library/init/lean/ir): improve sizet syntax 2018-05-07 18:07:04 -07:00
Leonardo de Moura
e6b509781f feat(library/init/lean/ir/ir): platform independent object size and offset 2018-05-07 18:07:04 -07:00
Leonardo de Moura
883f6923e2 chore(library/init/lean/ir/elim_phi): fix typo 2018-05-06 10:15:17 -07:00
Leonardo de Moura
88082cd16d fix(library/init/lean/ir/parser): case 2018-05-06 10:11:58 -07:00
Leonardo de Moura
e2e124626f feat(library/init/lean/ir): add elim_phi function 2018-05-06 10:07:44 -07:00
Leonardo de Moura
89b4bb7210 feat(library/init/data/hashable): add hashable nat instance 2018-05-06 07:53:29 -07:00
Leonardo de Moura
3079d2d007 feat(library/init/lean/name): add hashable instance 2018-05-06 07:49:17 -07:00
Leonardo de Moura
e64cb10ded feat(library/init): add hashable type class 2018-05-05 20:48:57 -07:00
Leonardo de Moura
d5fe509c36 chore(*): remove end after each match-expression 
`end` is not optional anymore
 2018-05-04 11:30:06 -07:00
Leonardo de Moura
11a8a7c4f3 feat(library/init): use usize instead of uint32 in the low level array access primitives 2018-05-04 10:40:14 -07:00
Leonardo de Moura
af4f831a9f feat(library/init/data/hashmap): hash function produces an uint32 instead of nat 
Most efficient hash functions use uint32/uint64 and produce values
that do not fit in out small nat representation. Thus, GMP big numbers
would have to be created.
 2018-05-03 17:56:10 -07:00
Leonardo de Moura
82bf618972 feat(library/init/lean/disjoint_set): disjoint sets 
We need this datastructure to eliminate phi nodes from the IR.
The phi nodes need to be eliminated when mapping to C++ and/or
interpreting the IR.
 2018-05-02 22:24:33 -07:00
Leonardo de Moura
bf71068b14 feat(library/init/lean/ir): parse IR definitions 2018-05-02 16:59:50 -07:00
Leonardo de Moura
0d49ae3f69 feat(library/init/lean/parser): add not_followed_by and not_followed_by_sat 
The new parsers are useful to implement the longest match rule.
 2018-05-02 15:55:57 -07:00
Leonardo de Moura
beae2d936b chore(library/init/lean/ir/parser): remove leftover 2018-05-02 12:44:23 -07:00
Leonardo de Moura
f44bfb3e59 feat(library/init/lean/parser/parser): use dlist to implement expected messages 
The idiom `p1 <|> p2 <|> ... <|> pn` generates many append operations.
`dlist` provides an O(1) append.
 2018-05-02 12:43:21 -07:00
Leonardo de Moura
4d6cbf62a2 refactor(library/init/lean/parser/parser): we don't need to store the whole message in ok_eps 
In the original parsec paper, they store messages in OK silent/epsilon
results too. This is not necessary, we only need the "expected" field
for the `ok_eps` constructor.
 2018-05-02 11:37:57 -07:00
Leonardo de Moura
6e2ebb5fab feat(library/init/lean/ir): add IR instruction parser 2018-05-01 17:45:50 -07:00
Leonardo de Moura
6672cc2a34 fix(library/init/lean/parser/parser): bug 2018-05-01 17:15:12 -07:00
Leonardo de Moura
7361dc7b96 chore(library/init/lean): join_with ==> join_sep 2018-05-01 17:14:49 -07:00
Leonardo de Moura
3c53ef1562 chore(library/init/lean/ir): rename instructions gets and sets to sget and sset 
Motivation: consistency with `swrite` and `sread`
 2018-05-01 17:01:45 -07:00
Leonardo de Moura
619394f3da feat(library/init/lean/parser/string): parser for string literals 2018-05-01 16:17:16 -07:00
Leonardo de Moura
ffdc6cca8a refactor(library/init/lean/ir): move reserved set to different file 2018-05-01 15:27:25 -07:00
Leonardo de Moura
0daeb7d17f feat(library/init/lean/ir/format): escape identifiers when needed 2018-05-01 14:27:38 -07:00
Leonardo de Moura
4aafa82a9c feat(library/init/lean/ir/format): IR => format 2018-05-01 13:39:57 -07:00
Leonardo de Moura
92fa43e7d8 feat(library/init/lean/ir/ir): use name 2018-05-01 12:40:49 -07:00
Leonardo de Moura
263391bdbb refactor(library/init/lean): add init/lean/parser/identifier 2018-05-01 11:53:55 -07:00
Leonardo de Moura
7305a7a65e feat(library/init/lean): identifier parser 2018-05-01 10:29:34 -07:00
Leonardo de Moura
05239d20cd refactor(library/init/lean/ir): split ir.lean 2018-05-01 08:43:34 -07:00
Leonardo de Moura
ba8b85f4c0 chore(library/init/lean/parser/parser): adjust variable names 2018-04-30 16:36:09 -07:00