Leonardo de Moura
|
947811cab8
|
fix: zero exit points != one exit point
|
2022-09-24 08:13:17 -07:00 |
|
Sebastian Ullrich
|
3288f437c2
|
refactor: further simplify RBMap balancing
|
2022-09-24 14:16:48 +02:00 |
|
Sebastian Ullrich
|
95f2e4e2e0
|
refactor: cleanup, simplify RBMap balances
|
2022-09-24 14:16:48 +02:00 |
|
Ed Ayers
|
2a6697e077
|
feat: goal-diffs (#1610)
|
2022-09-24 11:46:11 +02:00 |
|
Leonardo de Moura
|
85c468c853
|
fix: remove internal name hack at [specialize] and [inline] attributes
|
2022-09-23 20:25:16 -07:00 |
|
Leonardo de Moura
|
011521013d
|
feat: use phase at inferConstType, save specialization
|
2022-09-23 16:45:04 -07:00 |
|
Leonardo de Moura
|
0c82e8bd0d
|
feat: make sure base phase contains an entry for each declaration being compiled at `init
|
2022-09-23 16:31:38 -07:00 |
|
Leonardo de Moura
|
2be8cb93ac
|
feat: store phase at CompilerM context
|
2022-09-23 16:30:51 -07:00 |
|
Leonardo de Moura
|
c333581689
|
fix: functions occurring as arguments of other functions are not inlined
|
2022-09-23 14:43:06 -07:00 |
|
Leonardo de Moura
|
e4f0f4b794
|
fix: shouldGenerateCode fix for axiom
|
2022-09-23 14:25:48 -07:00 |
|
Leonardo de Moura
|
5322aa79f6
|
fix: apply findJoinPoints before pullFunDecls
`pullFunDecls` affects the effectiveness of `findJoinPoints`
|
2022-09-23 14:00:24 -07:00 |
|
Leonardo de Moura
|
004822aba4
|
fix: mixing Lean and LCNF types at toLCNF
|
2022-09-23 13:56:31 -07:00 |
|
Leonardo de Moura
|
609d241ad4
|
fix: improve updateFunDeclInfo precision
|
2022-09-23 13:56:14 -07:00 |
|
Leonardo de Moura
|
8cf225e9ce
|
fix: PassInstaller staging issue
The builtin pass installer cannot be installed using `[cpass]` because
it will not be activated until we process `Passes.lean`
|
2022-09-23 08:17:58 -07:00 |
|
Leonardo de Moura
|
c165317b28
|
feat: add ImportM.runCoreM
|
2022-09-23 07:52:13 -07:00 |
|
Leonardo de Moura
|
e53ac503da
|
refactor: move PassInstaller to CoreM
|
2022-09-23 07:22:54 -07:00 |
|
Leonardo de Moura
|
aa17641f18
|
chore: LCNF imports
|
2022-09-23 07:05:57 -07:00 |
|
Leonardo de Moura
|
4323205185
|
fix: support user-defined empty inductives at toLCNF
|
2022-09-23 05:50:02 -07:00 |
|
Leonardo de Moura
|
eed569153b
|
fix: dependent field issue
|
2022-09-22 20:38:42 -07:00 |
|
Leonardo de Moura
|
5db452cfe7
|
doc: add note at LCNF internalizer
We should also new tests that expose the problem.
|
2022-09-22 20:19:01 -07:00 |
|
Leonardo de Moura
|
412a05d0d6
|
fix: ensure cases field parameters do not occur in types
|
2022-09-22 20:15:39 -07:00 |
|
Leonardo de Moura
|
a7a6103862
|
feat: add scoped notation for LCNF pretty printer
|
2022-09-22 17:07:34 -07:00 |
|
Leonardo de Moura
|
c0ac2138f7
|
fix: ensure inferForallType at LCNF handles universes like the kernel and MetaM
|
2022-09-22 16:38:16 -07:00 |
|
Leonardo de Moura
|
1437b9cd90
|
fix: non-termination when eta-expanding Eq.ndrec at toLCNF
|
2022-09-22 16:04:19 -07:00 |
|
Leonardo de Moura
|
f721e44718
|
fix: simplify compatibleTypes
Add note about "erasure confusion" in LCNF.
|
2022-09-22 15:15:32 -07:00 |
|
Leonardo de Moura
|
955d3d4ff5
|
fix: missing case at isErasedCompatible
|
2022-09-22 14:16:29 -07:00 |
|
Leonardo de Moura
|
096a6fd4fb
|
fix: use eta at compatibleTypes
|
2022-09-22 13:57:14 -07:00 |
|
Leonardo de Moura
|
1f8d8df3ac
|
fix: compatibleTypes
|
2022-09-22 12:52:39 -07:00 |
|
Leonardo de Moura
|
a2bcb3b73e
|
fix: erase propositon formers, add isErasedCompatible, remove approx. from compatibleTypes
|
2022-09-21 20:47:02 -07:00 |
|
Leonardo de Moura
|
79c8a3879b
|
fix: LCNF compatibleTypes function
|
2022-09-21 19:14:25 -07:00 |
|
Leonardo de Moura
|
917f87fee4
|
fix: forward declaration type
|
2022-09-21 18:40:38 -07:00 |
|
Leonardo de Moura
|
05f0a6c423
|
fix: skip declarations that do not have a value
|
2022-09-21 18:40:20 -07:00 |
|
Leonardo de Moura
|
a5abe864f3
|
chore: prepare to activate new code generator
|
2022-09-21 18:09:19 -07:00 |
|
Leonardo de Moura
|
9080701126
|
refactor: move compileDecl, compileDecls, and addDecl to CoreM
The new code generator entry point is in `CoreM`.
|
2022-09-21 18:09:19 -07:00 |
|
Leonardo de Moura
|
c52203ff57
|
feat: add baseExt environment extension for storing code generator results
|
2022-09-21 18:09:19 -07:00 |
|
Leonardo de Moura
|
f9898a1d45
|
chore: cleanup
|
2022-09-21 18:09:19 -07:00 |
|
Mario Carneiro
|
ef0736c303
|
feat: multiple delta (part 2)
|
2022-09-21 18:04:31 -07:00 |
|
Mario Carneiro
|
90353d7fd7
|
feat: multiple delta, delta conv, unfold
|
2022-09-21 18:04:31 -07:00 |
|
Leonardo de Moura
|
1fb112f84b
|
test: Environment.addExtraName
|
2022-09-21 15:03:11 -07:00 |
|
Leonardo de Moura
|
8987de75c1
|
feat: add Environment.addExtraName
|
2022-09-21 10:57:39 -07:00 |
|
Yuri de Wit
|
c65a206d6a
|
chore: reintroduced 'important' let paragraph
|
2022-09-21 07:36:25 -07:00 |
|
Yuri de Wit
|
64a0ec91fa
|
chore: few updates to Expr documentation
|
2022-09-21 07:36:25 -07:00 |
|
Mario Carneiro
|
b922483ebc
|
chore: remove getElem' delab
|
2022-09-21 06:21:00 -07:00 |
|
Mario Carneiro
|
2aa882a416
|
chore: remove getElem', use custom delab
|
2022-09-21 06:21:00 -07:00 |
|
Mario Carneiro
|
3e83e28e8f
|
feat: injections with names
|
2022-09-20 17:36:35 -07:00 |
|
Leonardo de Moura
|
727ee79f05
|
fix: exponential blowup at LCNF simp
|
2022-09-20 17:03:40 -07:00 |
|
Leonardo de Moura
|
a5ac950b54
|
chore: increase max recursion depth for compiler
|
2022-09-20 16:58:45 -07:00 |
|
Leonardo de Moura
|
990b031871
|
feat: add translator attribute to MonadFVarSubst class
See new comments.
|
2022-09-20 16:58:27 -07:00 |
|
Leonardo de Moura
|
111f6a319c
|
feat: add ppDecl'
It is useful for debugging purposes when we want to pretty print a
declaration before internalizing it.
|
2022-09-20 16:55:11 -07:00 |
|
Leonardo de Moura
|
17202d0882
|
fix: missing headBeta
|
2022-09-20 16:22:37 -07:00 |
|