Leonardo de Moura
4001407f10
refactor: add MonadError class abbreviation
2020-12-14 09:15:26 -08:00
Leonardo de Moura
3b6d65c3c3
chore: use deriving Inhabited
2020-12-13 10:09:20 -08:00
Leonardo de Moura
44d0fe993a
feat: ensure scoped instances cannot be used outside namespaces
2020-12-05 16:26:31 -08:00
Leonardo de Moura
9d304df757
feat: heterogeneous Append experiment
...
@Kha This one required a bunch of manual fixes. The main issue is that
before we added the string interpolation feature, we created
`MessageData`s using `++` and coercions. For example, given
`(e : Expr)`, we would write
```
let msg : MessageData := "type: " ++ e
```
and rely on the coercions `String -> MessageData` and
`Expr -> MessageData`, and the instance `Append MessageData`.
However, heterogeneous operators "block" the expected type propagation downwards.
This kind of code is obsolete now since we can write a more compact
version using string interpolation
```
let msg := m!"type: {e}"
```
2020-12-01 16:32:41 -08:00
Leonardo de Moura
0869f38de4
chore: update structure, class, inductive
2020-11-27 15:09:30 -08:00
Leonardo de Moura
c305c2691f
chore: use :=
2020-11-19 07:22:31 -08:00
Leonardo de Moura
396e767f3d
refactor: move Ref to Prelude and rename it to MonadRef
...
`MacroM` will implement `MonadRef` because
1- It will be easier to throw errors from macros
2- We will be able to `getRef` to retrieve the syntax node at macro
rules.
I renamed `Ref` to `MonadRef` to make it consistent with other classes
providing monadic methods (e.g. `MonadEnv`, `MonadState`, etc).
cc @Kha
2020-11-13 16:00:31 -08:00
Leonardo de Moura
f17e226638
chore: naming convention
...
Example: `mkNameStr` => `Name.mkStr`
cc @Kha
2020-11-11 10:08:55 -08:00
Leonardo de Moura
ff493751b5
chore: HasFormat ==> ToFormat
2020-10-27 16:19:14 -07:00
Leonardo de Moura
10c32fcf94
chore: HasToString => ToString
2020-10-27 16:11:48 -07:00
Leonardo de Moura
13c2a8ff51
chore: remove #lang lean4 header
2020-10-25 09:54:07 -07:00
Leonardo de Moura
82ee2e361b
chore: cleanup
2020-10-21 18:43:47 -07:00
Leonardo de Moura
43efdd50f7
chore: move to new frontend
2020-10-14 17:38:17 -07:00
Leonardo de Moura
6ac227a63c
chore: elabAttrs, elabDeclAttrs
2020-09-20 07:39:14 -07:00
Leonardo de Moura
a28679358e
refactor: remove MonadError
2020-09-18 09:58:13 -07:00
Leonardo de Moura
163b0a7a3f
fix: protected
...
- `protected` outside of a namespace is an error.
- Fix `protected` in recursive definitions.
cc @Kha
2020-09-14 13:09:04 -07:00
Leonardo de Moura
5ced8867b0
feat: anonymous instances and support for all kinds of definition at mutual
2020-09-01 17:00:00 -07:00
Leonardo de Moura
d74551b19e
feat: elaborate header of mutually recursive definitions
2020-09-01 16:13:04 -07:00
Leonardo de Moura
9f16d01058
refactor: reduce DeclModifiers dependencies
2020-08-31 10:12:06 -07:00
Leonardo de Moura
bb3c8a2105
refactor: polymorphic applyAttributes
2020-08-27 10:46:33 -07:00
Leonardo de Moura
de2df5955f
refactor: polymorphic checkNotAlreadyDeclared
2020-08-26 13:42:57 -07:00
Leonardo de Moura
8a9b031a9d
refactor: add Lean/Elab/Attributes.lean
2020-08-26 09:54:48 -07:00
Leonardo de Moura
a413da856f
refactor: polymorphic elabAttrs and elabAttr
2020-08-26 09:50:03 -07:00
Leonardo de Moura
05a0e7f6d0
refactor: build all main monads on top of ECoreM
2020-08-20 18:36:04 -07:00
Leonardo de Moura
68a4c145f7
refactor: implement attribute hooks using CoreM
...
We were using a mix of `IO` and `Except`
2020-08-19 14:44:54 -07:00
Leonardo de Moura
5ba9aad7a3
refactor: eliminate ref plumbing
2020-08-13 10:37:53 -07:00
Leonardo de Moura
0118de09b9
chore: add mkAuxDefinition
2020-07-24 10:45:32 -07:00
Leonardo de Moura
78af3d5cba
feat: add instances to parent classes
2020-07-24 10:05:19 -07:00
Leonardo de Moura
6f402a081c
fix: register class for class inductive
2020-07-15 16:32:23 -07:00
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
d5f64f52a9
feat: add CtorView and modifier validation for inductive and constructors
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
249bda16c0
chore: remove prelude commands from Lean package
2020-06-25 11:21:17 -07:00
Sebastian Ullrich
4b84f8fa88
fix: nullary attributes in new frontend
2020-06-16 21:59:40 +02:00
Leonardo de Moura
4ccc3fef52
chore: move Init.Lean files to Lean package
2020-05-26 15:04:35 -07:00
