From: Adam Chlipala <adamc@hcoop.net>
Date: Sat, 13 Oct 2007 13:38:46 +0000 (+0000)
Subject: Add special case for function applications in base type rule checks
X-Git-Tag: release_2010-11-19~172
X-Git-Url: https://git.hcoop.net/hcoop/domtool2.git/commitdiff_plain/4ecbfd4c845e35126c61e182146005f27d45339a?ds=sidebyside

Add special case for function applications in base type rule checks
---

diff --git a/src/tycheck.sml b/src/tycheck.sml
index d486603..e2feb90 100644
--- 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)