This repository was archived by the owner on May 20, 2018. It is now read-only.

[WIP] Diff entire types - #183

Open

robrix wants to merge 31 commits into

diff-entire-types

Commits on Dec 20, 2015

Stub in term diffs.
Rob Rix
committed
4fa9b4e
Lift terms into term diffs.
Rob Rix
committed
35d828b
Diff/unify terms recursively.
Rob Rix
committed
f080077
Use an inner `unify` function.
Rob Rix
committed
532672a
Share the visited sets left to right.
Rob Rix
committed
e6a3707
The visited set is internal to the constructor.
Rob Rix
committed
365dd7d
TermDiff is public.
Rob Rix
committed
218a4da
Phrase the equality check as `if` instead of `guard`.
Rob Rix
committed
4a098da
Produce the whnf reductions of the terms.
Rob Rix
committed
c23fff4
Add a property to produce the unified term, if any.
Rob Rix
committed
2a38e39
Document `unified`.
Rob Rix
committed
1dc654e
Remove the initial return in `equate`.
Rob Rix
committed
e3507fe
Reduce terms to weak head normal form independently.
Rob Rix
committed
7809812
Diff terms independently.
Rob Rix
committed
e4227f0
Disallow recurrence when reducing to whnf.
Rob Rix
committed
d72ca5e
Definitional equality/unification is done via type diffing.
Rob Rix
committed
15afa6b
Remove the public `visited` set parameter.
Rob Rix
committed
00c79a9
Call into TermDiff directly when testing for type mismatches.
Rob Rix
committed
8ff0bce
Rename TermDiff to Unification.
Rob Rix
committed
94a197a
Add a property to expose the expected term.
Rob Rix
committed
e1c57db
Add a property to expose the actual term.
Rob Rix
committed
2eee237
Unifications can be described as their expected/actual types.
Rob Rix
committed
b14a5b8
Rename the unification.
Rob Rix
committed
8671b4e
Label the expected/actual terms.
Rob Rix
committed
3fe6d37
Print the unification.
Rob Rix
committed
0df5b9e

Commits on Dec 21, 2015

Replace definitional equality with Unification.
Rob Rix
committed
0357145
AnnotatedTerm is a Functor.
Rob Rix
committed
43c9827

Commits on Dec 25, 2015

Merge branch 'master' into diff-entire-types
Rob Rix
committed
3f0a7a1
Elaborate into unifications deeply.
Rob Rix
committed
7571784
Print failed unifications distinct from successful ones.
Rob Rix
committed
a27e24a
Print the context & environment on type mismatches in `elaborateType`.
Rob Rix
committed
61b5941