Skip to content

[WIP] Pairs#10

Open
robrix wants to merge 78 commits into
masterfrom
pairs
Open

[WIP] Pairs#10
robrix wants to merge 78 commits into
masterfrom
pairs

Conversation

@robrix

@robrix robrix commented Jan 8, 2016

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

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