Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in / Register
Toggle navigation
Open sidebar
Glasgow Haskell Compiler
GHC
Commits
43a5970a
Commit
43a5970a
authored
Dec 04, 2015
by
Simon Peyton Jones
Browse files
Comments only
parent
67565a72
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
5 additions
and
8 deletions
+5
-8
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSMonad.hs
+5
-8
No files found.
compiler/typecheck/TcSMonad.hs
View file @
43a5970a
...
...
@@ -662,8 +662,8 @@ Definition [Can-rewrite relation]
A "can-rewrite" relation between flavours, written f1 >= f2, is a
binary relation with the following properties
R1
.
>= is transitive
R2
.
If f1 >= f, and f2 >= f,
(
R1
)
>= is transitive
(
R2
)
If f1 >= f, and f2 >= f,
then either f1 >= f2 or f2 >= f1
Lemma. If f1 >= f then f1 >= f1
...
...
@@ -690,7 +690,7 @@ See Note [Flavours with roles].
Theorem: S(f,a) is well defined as a function.
Proof: Suppose (a -f1-> t1) and (a -f2-> t2) are both in S,
and f1 >= f and f2 >= f
Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF)
Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF
1
)
Notation: repeated application.
S^0(f,t) = t
...
...
@@ -702,9 +702,6 @@ A generalised substitution S is "inert" iff
(IG1) there is an n such that
for every f,t, S^n(f,t) = S^(n+1)(f,t)
(IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t
that is, each individual binding is "self-stable"
By (IG1) we define S*(f,t) to be the result of exahaustively
applying S(f,_) to t.
...
...
@@ -719,8 +716,8 @@ guarantee that this recursive use will terminate.
Note [Extending the inert equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Th
is is the main theorem!
Th
eorem [Stability under extension]
This is the main theorem!
Suppose we have a "work item"
a -fw-> t
and an inert generalised substitution S,
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment