HCoop
/
hcoop
/
domtool2.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(from parent 1:
ca6ffb3
)
Add special case for function applications in base type rule checks
author
Adam Chlipala
<adamc@hcoop.net>
Sat, 13 Oct 2007 13:38:46 +0000
(13:38 +0000)
committer
Adam Chlipala
<adamc@hcoop.net>
Sat, 13 Oct 2007 13:38:46 +0000
(13:38 +0000)
src/tycheck.sml
patch
|
blob
|
blame
|
history
diff --git
a/src/tycheck.sml
b/src/tycheck.sml
index
d486603
..
e2feb90
100644
(file)
--- a/
src/tycheck.sml
+++ b/
src/tycheck.sml
@@
-184,10
+184,21
@@
fun baseCondition t =
| _ => false))
| _ => NONE
+fun simplifyKindOf e =
+ case e of
+ (EApp ((EVar s, _), e'), _) =>
+ (case Env.function s of
+ NONE => e
+ | SOME f =>
+ case f [e'] of
+ NONE => e
+ | SOME e => e)
+ | _ => e
+
fun hasTyp (e, t1, t2) =
if (case baseCondition t2 of
NONE => false
- | SOME rule => rule
e
) then
+ | SOME rule => rule
(simplifyKindOf e)
) then
()
else
subTyp (t1, t2)