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

147 commits

Author SHA1 Message Date
Leonardo de Moura
4c8420406d chore(stage0): update 2019-06-24 15:48:11 -07:00
Leonardo de Moura
b225112234 chore(stage0): update 2019-06-24 15:48:11 -07:00
Leonardo de Moura
e4344b0c94 chore(library/init/lean/parser/default): update default 2019-06-21 14:20:40 -07:00
Leonardo de Moura
bc9e460f62 fix(library/init/lean/compiler/ir): collectUsedDecls must take initialization functions into account 
Move builtin parser level to its own directory
 2019-06-21 13:34:42 -07:00
Leonardo de Moura
8ad653ae2d chore(stage0): update 2019-06-20 09:55:55 -07:00
Leonardo de Moura
db325cb924 fix(stag0): missing file 2019-06-20 09:23:41 -07:00
Leonardo de Moura
e0ddacfd3e feat(library/init/lean/attributes,frontends/lean): allow attributes to specify when they should be applied 2019-06-20 09:17:03 -07:00
Leonardo de Moura
e86e6af049 feat(library/init/lean/attributes): add applicationTime field and remove unnecessary parameters 2019-06-20 08:48:26 -07:00
Leonardo de Moura
766467d095 fix(stage0): missing files 2019-06-18 18:35:18 -07:00
Leonardo de Moura
08cdb757b4 feat(library/init/lean/environment): add Environment.addAndCompile 
To fix `BuiltinParserAttribute`, we need to be able to add auxiliary declarations programmatically.
 2019-06-18 18:20:17 -07:00
Leonardo de Moura
0dfca42f6d chore(library/init/lean/compiler/initattr): remove unnecessary @[export] 2019-06-18 16:15:48 -07:00
Leonardo de Moura
9da080d398 feat(library/compiler/init_attribute): switch to @[init] attribute in Lean 2019-06-18 16:03:52 -07:00
Leonardo de Moura
36aa33091b chore(stage0): update 2019-06-07 17:16:36 -07:00
Leonardo de Moura
f176a7963c feat(library/init/lean/compiler/ir/emitcpp): register arity 0 declarations 2019-06-07 17:15:16 -07:00
Leonardo de Moura
3651dc7618 feat(library/init/lean): add evalConst 
The implementation is good enough for implementing extensible parsers,
elaborators and tactics, but there are a few TODOs

1- We should have a better story for standalone applications.
   Most of them don't need `evalConst`, and the global table is
   just initialization overhead.

2- The global table introduces a dependency on the `Lean.Name`
   implementation. So, all standalone applications will depend on it.

3- We are not storing arity 0 constants in the table.
   This one should be easy to fix in the future.
 2019-06-07 16:31:28 -07:00
Leonardo de Moura
c3a7cc4617 feat(library/init/lean/compiler/ir/emitcpp): register functions 2019-06-07 15:34:55 -07:00
Leonardo de Moura
373011bc20 chore(library/init/lean/format): export group 2019-06-07 10:35:04 -07:00
Leonardo de Moura
452485a706 chore(library/init/lean/format): export functions 2019-06-07 10:10:13 -07:00
Leonardo de Moura
b292fc13cc chore(library/init/lean/compiler/inline): export typo 2019-06-06 15:28:20 -07:00
Leonardo de Moura
e4063f5eec chore(stage0): update 2019-06-06 15:20:13 -07:00
Leonardo de Moura
57e250a768 chore(stage0): remove leftover 2019-06-06 15:09:41 -07:00
Leonardo de Moura
9b457cc77c feat(library/init/lean/compiler/inline): implement tester functions and export them 2019-06-06 15:07:08 -07:00
Leonardo de Moura
72290483e4 chore(library/init/lean/compiler): attributes.lean ==> inline.lean 2019-06-06 14:08:13 -07:00
Leonardo de Moura
e05cdc2b08 feat(library/init/lean/compiler): declare function inlining attributes in Lean 
Remark: they are not active yet since we haven't removed the ones
defined in C++ yet.
 2019-06-06 11:05:54 -07:00
Leonardo de Moura
c8a972c57b fix(library/init/lean/attributes): typos at @[export] 2019-06-06 10:41:17 -07:00
Leonardo de Moura
fb77d71d23 feat(library/init/lean/attributes): export attribute API 2019-06-05 16:55:47 -07:00
Leonardo de Moura
d212abb9ee feat(library/init/lean/syntax): export helper functions for creating syntax in C++ 2019-06-05 16:49:58 -07:00
Leonardo de Moura
02847f6dc7 chore(stage0): update 2019-06-05 15:29:13 -07:00
Leonardo de Moura
fd29b7e45d feat(util/io): add helper functions for consuming IO results in C++ 2019-06-05 13:53:38 -07:00
Leonardo de Moura
642992eeca chore(library/init/lean/attributes): missing @[export] 2019-06-05 13:30:26 -07:00
Leonardo de Moura
e379d58802 chore(stage0): update 2019-06-05 13:18:59 -07:00
Sebastian Ullrich
1f51a96794 chore(stage0): fix build 2019-06-05 10:54:01 +02:00
Leonardo de Moura
4ee3332763 chore(stage0): update 2019-06-04 16:56:53 -07:00
Leonardo de Moura
4a26f0028c chore(library/init/lean/environment): remove unnecessary function 2019-06-03 15:17:40 -07:00
Leonardo de Moura
ed1a433d52 feat(library/init/lean/modifiers): add privatePrefix 2019-06-03 10:33:40 -07:00
Leonardo de Moura
224195a1fb feat(library/init/lean/modifiers): environment extension for private declarations 2019-06-03 10:10:00 -07:00
Leonardo de Moura
cd73105dff refactor(kernel/environment,library/private,library/init/lean/environment): move main module name to header 2019-06-03 09:14:23 -07:00
Leonardo de Moura
23029cb386 chore(stage0): update 2019-06-03 08:24:53 -07:00
Leonardo de Moura
c92fe75053 fix(library/init/lean/compiler/constfolding): Usize => USize 
Camel case auto-conversion bug.
 2019-06-01 09:42:22 -07:00
Leonardo de Moura
70c9733897 chore(stage0): update 2019-05-30 09:41:16 -07:00
Leonardo de Moura
8333e48037 chore(stage0): update 2019-05-30 09:16:09 -07:00
Leonardo de Moura
0e8abd81bb chore(stage0): update 2019-05-25 16:35:43 -07:00
Leonardo de Moura
074002eb84 chore(stage0): update 2019-05-23 18:34:22 -07:00
Leonardo de Moura
c6f717e55b chore(stage0): update 2019-05-23 18:20:12 -07:00
Leonardo de Moura
f9f4e6c14b feat(library/init/lean/compiler/ir): add expandresetreuse 2019-05-23 08:58:16 -07:00
Leonardo de Moura
aede2476de chore(stage0): update 
We changed the IR representation, and the C++ code interacts with both
stage0 and stage1.
 2019-05-23 08:22:36 -07:00
Leonardo de Moura
3e76e43843 fix(library/init/lean/compiler/ir/borrow): visit join point body 2019-05-22 17:31:56 -07:00
Leonardo de Moura
fe0141918a fix(library/init/lean/compiler/ir) bug at addDecAfterFullApp 2019-05-22 16:30:42 -07:00
Leonardo de Moura
a570e35161 chore(stage0): update 2019-05-22 11:45:58 -07:00
Leonardo de Moura
2408d6dd80 fix(library/init/lean/compiler/ir/boxing): created boxed version for externs 2019-05-22 10:56:51 -07:00