Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[WIP] Pairs #10

Open
wants to merge 78 commits into
base: master
Choose a base branch
from
Open

[WIP] Pairs #10

wants to merge 78 commits into from

Conversation

robrix
Copy link
Contributor

@robrix robrix commented Jan 8, 2016

  • Defines a Pair type.
  • Defines a constructor for Pairs.
  • Defines eliminators for Pairs.
  • Unification is specialized to Term'.

@robrix
Stub in a Surface.Language module.
5417077
@robrix
Add a type synonym for Term Expression.
b18aa6d
@robrix
Export Surface.Language.
d106732
@robrix
Move all of Surface to Surface.Language.
98b6b9f
@robrix
Stub in a Surface.Pair module.
79d199f
@robrix
Define a Pair type.
d94175e
@robrix
Export Pair.
a464292
@robrix
Move checkIsType up a bit.
ea1c0fb
@robrix
Remove a redundant import.
b8beb6d
@robrix
Write a few lambdas inline.
7f40acd
@robrix
Check function types more or less the same as pi types.
b6563ba
@robrix
Test for unification against the return type, not its kind.
80e7d35
@robrix
Check that the return type is a type.
9f6a92d
@robrix
Just check against type.
73d0bd5
@robrix
Unify the types.
82e1cc7
@robrix
Move _type into the Language module.
9261a7d
@robrix
Remove a redundant import.
09a144d
@robrix
Ignore the tags file.
f3a9a12
@robrix
Rename the parameters.
2c63002
@robrix
Test the type of _Pair.
4fe94bd
@robrix
Move the language tests into their own module.
11b820e
@robrix
Stub in a Pair module.
70b7600
@robrix
Don’t import Surface.Pair.
82b2d08
@robrix
Stub in a Definition type.
75fb47c
@robrix
Only represent the type of definitions for now.
5f74131
@robrix
Modules are lists of definitions.
72e7f99
@robrix
Remove a redundant import.
3ac0257
@robrix
Remove a bogus $.
e7dcfeb
@robrix
Define Definition using record syntax.
f2add1e
@robrix
Add a lookup operator for Module.
68a1a71
@robrix
Add a type synonym for environments.
369ee1f
@robrix
Stub in the reduction of terms to weak head normal form.
c41e8bf
@robrix
Lookup variables for whnf.
12de9d8
@robrix
Substitute inside applications in whnf.
cda5fec
@robrix
Reduce applications to whnf correctly.
b793b40
@robrix
byUnifying recurs via expectUnifiable.
7d65f48
@robrix
Use the Term' shorthand everywhere we can.
05eb00b
@robrix
Module is defined in terms of Term'.
7a4651e
@robrix
Abstract Definition over a term type.
d1af2bb
@robrix
Abstract Definition over the expression type.
7c1a611
@robrix
Abstract Module over the expression type.
0b1b6fc
@robrix
Abstract Module and Definition over the term type.
74ac43f
@robrix
Move the Module types into Data.Term.Types.
4329f99
@robrix
We’re no longer dependent on StandaloneDeriving.
1e98610
@robrix
Equality of conflicts.
1a1a2d8
@robrix
Inequality of other comparisons.
c7aca05
@robrix
Move the Unification module under Surface.
bc5c75f
@robrix
Move the Unifiable instance for Expression into Surface.Unification.
bdd3daa
@robrix
Stub in a Surface.Renaming module.
444187a
@robrix
Move the Unifiable typeclass into Data.Term.Types.
3efe2a7
@robrix
Resort the exports.
a51b467
@robrix
Export Surface.Renaming.
c70f301
@robrix
Move renaming into Surface.Renaming.
91a9e19
@robrix
Move unification into Surface.Unification.
30af305
@robrix
annotation typechecking doesn’t use expectUnifiable.
17bfaf1
@robrix
Minimize the set of constraints necessary for annotation.
0d97693
@robrix
Minimize the constraints necessary for rename.
905dde2
@robrix
Minimize the constraints necessary for renameUnification.
9f18d6a
@robrix
Remove a redundant import.
a75a412
@robrix
Typecheck types without checkInferred.
6f8d0fd
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@robrix