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

13447 commits

Author SHA1 Message Date
Leonardo de Moura
9960ca01f0 feat: reject protected constructors in a private inductive datatype 
In a private inductive datatype, all constructors are private.
 2020-07-13 16:22:49 -07:00
Leonardo de Moura
2744ae96bb feat: check unsafe annotations in mutually inductive datatype declarations 2020-07-13 16:22:49 -07:00
Leonardo de Moura
2bf10b3d2c feat: add inferMod field to CtorView 2020-07-13 16:22:49 -07:00
Leonardo de Moura
2cc2e71a53 feat: elaborate constructors 2020-07-13 16:22:49 -07:00
Leonardo de Moura
3fc6d8ce61 chore: improve constructor syntax 
I think
```
inductive Foo
| private mk : Foo -> Foo
```
looks better than
```
inductive Foo
private | mk : Foo -> Foo
```

cc @Kha
 2020-07-13 16:22:48 -07:00
Leonardo de Moura
d5f64f52a9 feat: add CtorView and modifier validation for inductive and constructors 2020-07-13 16:22:48 -07:00
Leonardo de Moura
6e12987dd9 feat: add declModifiers to constructor declarations 
The goal is to allow users to attach doc strings and
`private/protected` to constructor declarations.

TODO: reject non applicable modifiers such as `unsafe` and `partial`.

cc @Kha
 2020-07-13 16:22:48 -07:00
Leonardo de Moura
83431dc88e feat: elaborate protected 2020-07-13 16:22:48 -07:00
Leonardo de Moura
667f2ed601 feat: resolve inductive and ctor names 2020-07-13 16:22:48 -07:00
Leonardo de Moura
18fce4f455 feat: add Expr.inferImplicit 2020-07-13 16:22:48 -07:00
Sebastian Ullrich
162e63030c leanmake: allow setting linker options 2020-07-13 21:39:04 +02:00
Leonardo de Moura
cda11dea25 feat: check universe parameters in mutually recursive inductive declaration 2020-07-11 08:01:36 -07:00
Leonardo de Moura
2949586244 feat: add local declarations for mutually inductive datatypes 2020-07-11 08:01:36 -07:00
Leonardo de Moura
c8636f2bf7 chore: generalize withDeclId 2020-07-11 08:01:36 -07:00
Leonardo de Moura
e26ec036ba feat: add instantiateForall 2020-07-11 08:01:36 -07:00
Sebastian Ullrich
fb02fbb867 fix: freeing Environments in tests 2020-07-10 07:42:26 -07:00
Sebastian Ullrich
719819bf49 fix: finally shouldn't call finalizer when finalizer throws 2020-07-10 07:42:26 -07:00
Sebastian Ullrich
c38f4fe837 feat: unsafe functions for freeing compacted regions 2020-07-10 07:42:26 -07:00
Sebastian Ullrich
ebd72d200f fix: alloc/free mismatch detected by asan 2020-07-10 07:42:26 -07:00
Leonardo de Moura
f559576994 feat: inductive datatype header validation 2020-07-09 15:34:25 -07:00
Leonardo de Moura
a488ec903e fix: remove old assertions 2020-07-08 12:45:53 -07:00
Leonardo de Moura
707ca63f87 chore: remove leftover MK_THREAD_LOCAL_GET 
cc @Kha
 2020-07-08 11:58:22 -07:00
Leonardo de Moura
d044e9f47e chore: remove instance cache 
If the missing cache generates perf problems in the future, we should
add the cache at `MetaM`.

cc @Kha
 2020-07-08 09:40:34 -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
Sebastian Ullrich
0f6b9f5c94 chore: clean up stage 0 executable build 
Previously we were building identical libInit/Std/Lean.a from the same stage0/stdlib sources. Now we simply link
everything right into libleancpp.a, again.
 2020-07-03 19:26:00 +02:00
Leonardo de Moura
36c971546c feat: add elabMutualInductive 2020-06-26 15:41:09 -07:00
Leonardo de Moura
30f03ad18c feat: add mutual syntax 2020-06-26 12:47:43 -07:00
Leonardo de Moura
1ad5b5984a feat: add Inductive.lean 2020-06-26 12:44:13 -07:00
Leonardo de Moura
b6f6e44f7c fix: build 
@Kha It is not clear why this change fixed the build on my
Linux (running on VirtualBox). The issue seems to be due
circular dependencies between the static libraries, and the order the
static libraries are processed. Note that the build worked on my OSX
without this change.
 2020-06-25 15:30:11 -07:00
Leonardo de Moura
b291c36a1f chore: cleanup 2020-06-25 13:30: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
249bda16c0 chore: remove prelude commands from Lean package 2020-06-25 11:21:17 -07:00
Leonardo de Moura
decab1ea57 fix: missing import 2020-06-25 11:20:47 -07:00
Sebastian Ullrich
81376d3902 feat: allow capturing expected type in elab 
/cc @leodemoura
 2020-06-25 14:58:45 +02:00
Sebastian Ullrich
51e4b49ba6 feat: allow arbitrary syntax in macro/elab 2020-06-25 13:54:11 +02:00
Leonardo de Moura
80bb6f174d feat: expand elab command 
cc @Kha
 2020-06-24 20:16:56 -07:00
Leonardo de Moura
cefbc27720 feat: add elab and elab_rules command syntax 2020-06-24 18:34:23 -07:00
Leonardo de Moura
196435c73b chore: use new fun syntax in old pretty printer 2020-06-17 21:28:03 -07:00
Leonardo de Moura
7ece1172a3 chore: remove TODOs 2020-06-17 21:28:03 -07:00
Leonardo de Moura
dbbacb3bfd chore: remove comment from Linter 
Old frontend is just providing `Syntax.missing`
 2020-06-17 21:28:03 -07:00
Sebastian Ullrich
52f2f04dff chore: leanmake: don't use CMake-like output by default 2020-06-17 18:20:05 +02:00
Sebastian Ullrich
9739356b91 fix: let syntax in old pretty printer 
/cc @leodemoura

I didn't remove support for let binding groups, but that's good enough for the time being
 2020-06-17 18:01:18 +02:00
Leonardo de Moura
0c089b8cbd feat: elaborate syntaxAbbrev as a definition 
@Kha I elaborated it as a definition. It works because we can now
reference Parser declarations in `syntax` command.
This change allowed us to replace `p.getArg 0` with `p` in the
`Websever` demo.
 2020-06-16 15:43:17 -07:00