Leonardo de Moura
772fa06461
doc: add workarounds, and describe what we need in the new equation compiler
...
@dselsam The good news is that the problem is fixable.
I included a workaround `mergeCongr3` for avoiding the overhead in the current system.
2020-02-05 11:46:35 -08:00
Daniel Selsam
707a1a7e8c
doc: elabissue for equation compiler perf
2020-02-05 10:41:44 -08:00
Leonardo de Moura
eacff1a448
feat: implement withPtrEq and withPtrAddr
2020-02-04 17:48:11 -08:00
Leonardo de Moura
6f4dd5441e
chore: disable test on windows
2020-02-04 14:21:38 -08:00
Leonardo de Moura
362185147e
chore: remove unncessary annotation
2020-02-04 14:21:26 -08:00
Leonardo de Moura
b5eb64da3a
fix: add mkFilePath and try to fix Windows build
2020-02-04 11:24:33 -08:00
Leonardo de Moura
48be9094b9
test: add test for parsing Core.lean
2020-02-04 10:15:00 -08:00
Leonardo de Moura
d125966c52
chore: fix tests
2020-02-04 10:14:31 -08:00
Leonardo de Moura
63434fbb7d
chore: add parser tests
2020-02-04 10:11:50 -08:00
Sebastian Ullrich
52a0a0937e
feat: check precedence of leading parsers as well
2020-02-04 07:49:33 -08:00
Leonardo de Moura
1f359b9844
chore: remove unnecessary workaround
...
It is not needed anymore after we fixed the `app` parser
2020-02-03 20:25:09 -08:00
Leonardo de Moura
d75cd49ea2
fix: app parser
...
cc @kha
2020-02-03 20:13:38 -08:00
Leonardo de Moura
2138a11480
feat: use custom error messages at checkRBPGreater
2020-02-03 18:30:22 -08:00
Leonardo de Moura
99f7aff491
fix: liftMethod notation
2020-02-03 17:12:44 -08:00
Leonardo de Moura
31bb6a1dec
feat: extend tryCoeAndLift
...
Add combined coe+lift case.
2020-02-03 14:30:13 -08:00
Leonardo de Moura
bcfaeaceab
feat: change ite and dite argument order
...
Motivation: make sure `propagateExpectedType` heuristic is applied in
the new frontend when processing them.
2020-02-03 14:11:29 -08:00
Leonardo de Moura
a474850f5e
feat: use automatic liftM at ensureHasType
2020-02-03 13:06:36 -08:00
Leonardo de Moura
48acc748ef
feat: improve automatic liftM at do blocks
...
We now don't need to use `decide` in the following example:
```
def pred (x : Nat) : IO Bool := do
pure $ decide $ (← g 1) > 0
```
2020-02-03 12:16:57 -08:00
Leonardo de Moura
ba915d90f5
feat: do not enable constApprox in the combinator approxDefEq
2020-02-03 11:50:40 -08:00
Leonardo de Moura
17cc925115
feat: change liftMethod notation
...
cc @Kha
2020-02-03 09:38:05 -08:00
Sebastian Ullrich
b76be34119
chore: fix test
2020-02-03 16:36:37 +01:00
Leonardo de Moura
f8bfe88d6b
fix: consume unnecessary let-decls at isDefEq
...
Make sure we solve unification constraints such as `(let x := v; ?m) =?= ?m`
2020-02-02 21:54:44 -08:00
Leonardo de Moura
2abfa1bcff
fix: closes #108
2020-02-01 23:17:00 -08:00
Leonardo de Moura
8487216b1e
feat: fallback to constApprox when foApprox fails
2020-02-01 22:50:29 -08:00
Leonardo de Moura
8de49b157c
feat: add new approximation at isDefEq
2020-02-01 22:38:58 -08:00
Leonardo de Moura
a7c8978d81
feat: insert liftM automatically in do notation when needed
...
@Kha The new example demonstrates the feature in action.
I added a comment explaining why it is more effective than relying on coercions.
2020-02-01 17:33:04 -08:00
Leonardo de Moura
cd4ec6313e
chore: try macros first
2020-02-01 00:53:49 -08:00
Leonardo de Moura
d8c738bef8
feat: elaborate do notation
2020-01-31 20:11:06 -08:00
Leonardo de Moura
3d0bfcd36a
fix: assertion violation
2020-01-31 08:25:59 -08:00
Leonardo de Moura
21618361b7
refactor: remove ParserKind
2020-01-30 20:56:46 -08:00
Leonardo de Moura
3f32d9eb0b
fix: closes #111
2020-01-30 14:09:47 -08:00
Leonardo de Moura
2f0ac98b51
feat: extend scope of cdot notation
2020-01-30 11:42:37 -08:00
Leonardo de Moura
38cfa1dcb6
feat: add elabMatch skeleton
2020-01-30 10:02:15 -08:00
Leonardo de Moura
0c4030137f
feat: simplify Coe again
...
Users may add the expensive instances if they want.
The goal is to make sure the default configuration is solid, and
covers all examples we really want to support.
cc @kha @dselsam
2020-01-29 22:08:42 -08:00
Leonardo de Moura
812c47d463
feat: simplify CoeFun and CoeSort
...
The main issue is nontermination for problems that do not have
solution. When using dependent coercions, we keep creating goals of
the form `CoeSort ... (coe (coe (coe ...))) ...`. Same for `CoeFun`.
I am considering simplifying it even further, and making sure
`CoeDep` can be used at most once in a sequence of coercions `CoeTC`.
Another option is to use a very small amount of fuel to
guarantee termination when solving coercion TC problems.
cc @Kha @dselsam
2020-01-29 21:56:26 -08:00
Leonardo de Moura
f29a13323a
fix: forget to update
2020-01-29 20:08:03 -08:00
Leonardo de Moura
a656096c4b
feat: expected type propagation
2020-01-29 19:00:56 -08:00
Leonardo de Moura
b00c04c491
fix: missing ensureHasType
2020-01-29 16:29:48 -08:00
Leonardo de Moura
400a9c45c1
test: CoeSort test
2020-01-29 03:57:27 -08:00
Leonardo de Moura
c048a3f573
fix: Level.normalize
2020-01-29 03:38:35 -08:00
Leonardo de Moura
c33cd11be1
feat: add CoeHead and CoeTail to minimize nontermination
...
The adventure continues.
cc @Kha @dselsam
2020-01-28 18:20:58 -08:00
Leonardo de Moura
a7de10a74a
feat: add support for CoeFun in the new elaborator
...
cc @kha
2020-01-28 16:50:53 -08:00
Leonardo de Moura
4aa710d4a6
feat: add bridge Coe + HasNat transitivity instance
...
cc @kha @dselsam
2020-01-28 16:17:14 -08:00
Leonardo de Moura
8c7aade7b6
feat: add coercion tests
2020-01-28 15:52:04 -08:00
Leonardo de Moura
e9e4dfe1ff
feat: add new Coe.lean
2020-01-28 13:10:30 -08:00
Leonardo de Moura
07bfeab6be
feat: add CoeFun and CoeSort to new Coe prototype
2020-01-28 12:57:14 -08:00
Leonardo de Moura
bb1a90b24d
chore: fix tests
2020-01-28 10:34:27 -08:00
Leonardo de Moura
642509229f
feat: split Coe and CoeDep
...
Motivation: control term size.
```lean
synth CoeT Nat 0 (Option (Option (Option (Option (Option Nat)))))
```
is much smaller with the new encoding
2020-01-28 09:48:18 -08:00
Leonardo de Moura
a272670ead
test: new instances
2020-01-27 21:23:14 -08:00
Leonardo de Moura
9b6dfa71a2
test: new Coe prototype
2020-01-27 20:33:10 -08:00
