mirror-core

mirror-core copied to clipboard

gmalecha

Added a reifiction function for modular reification without pmaps.

4

jesper-bengtson

Clean up the Types Language

2

This should be done with a module like it is done in the alt-mtypes branch. MTypes should also be renamed to Types.

gmalecha

Modular Types + Symbols

1

The current examples duplicate a lot of code. Part of this is for the purpose of keeping individual examples self-contained, but we really should find a way to factor out...

gmalecha

Sketch a guaranteed well-typed Expr implementation

5

This is mostly for comparison, but it also demonstrates some of the benefits of using dependent types, e.g. it makes some things easier.

gmalecha

gmalecha

Reify.v invalidates valid syntax

1

After importing MirrorCore.Reify.Reify the following command stops working: Implicit Arguments id [[A] [B] ...] Implicit Arguments is deprecated and Arguments should be used in stead, but it is still valid...

jesper-bengtson

Modular Types with Higher Kinds

4

This is an extension to @mmalvarez's work on core types that includes support for higher kinds, e.g. you have a deep embedding of types that are not of sort `Type`....

gmalecha

The MirrorCore code contains 100+ TODOs. These really need to be cleaned up.

gmalecha

Common-code elimination

1

We have a lot of duplicate code for various pieces of the automation, e.g. polymorphic lemmas for PAPPLY and polymorphic lemmas for rewriting. All of these should be combined and...

gmalecha