[WIP] Diff entire types #183

robrix · 2015-12-20T23:59:21Z

Type mismatch errors now print the entire type, highlighting the differing portions.

# Conflicts: # Manifold.xcodeproj/project.pbxproj

robrix added 30 commits December 20, 2015 13:15

Stub in term diffs.

4fa9b4e

Lift terms into term diffs.

35d828b

Diff/unify terms recursively.

f080077

Use an inner unify function.

532672a

Share the visited sets left to right.

e6a3707

The visited set is internal to the constructor.

365dd7d

TermDiff is public.

218a4da

Phrase the equality check as if instead of guard.

4a098da

Produce the whnf reductions of the terms.

c23fff4

Add a property to produce the unified term, if any.

2a38e39

Document unified.

1dc654e

Remove the initial return in equate.

e3507fe

Reduce terms to weak head normal form independently.

7809812

Diff terms independently.

e4227f0

Disallow recurrence when reducing to whnf.

d72ca5e

Definitional equality/unification is done via type diffing.

15afa6b

Remove the public visited set parameter.

00c79a9

Call into TermDiff directly when testing for type mismatches.

8ff0bce

Rename TermDiff to Unification.

94a197a

Add a property to expose the expected term.

e1c57db

Add a property to expose the actual term.

2eee237

Unifications can be described as their expected/actual types.

b14a5b8

Rename the unification.

8671b4e

Label the expected/actual terms.

3fe6d37

Print the unification.

0df5b9e

Replace definitional equality with Unification.

0357145

AnnotatedTerm is a Functor.

43c9827

Merge branch 'master' into diff-entire-types

3f0a7a1

# Conflicts: # Manifold.xcodeproj/project.pbxproj

Elaborate into unifications deeply.

7571784

Print failed unifications distinct from successful ones.

a27e24a

Print the context & environment on type mismatches in elaborateType.

61b5941

Provide feedback