From 9636715a5e06c8c174fd44cbf2847c4a8d2a87c7 Mon Sep 17 00:00:00 2001
From: dos-reis <gdr@axiomatics.org>
Date: Thu, 16 Oct 2008 08:57:52 +0000
Subject: 	* interp/i-spec1.boot (categoryImplies): New. 
 (evalCategory): Use it.

---
 src/interp/i-spec1.boot | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'src/interp/i-spec1.boot')

diff --git a/src/interp/i-spec1.boot b/src/interp/i-spec1.boot
index cec4db2b..ee6d9787 100644
--- a/src/interp/i-spec1.boot
+++ b/src/interp/i-spec1.boot
@@ -1201,9 +1201,26 @@ isDomainValuedVariable form ==
         objValUnwrap(val)
   nil
 
+
+++ returns true if category form `c1' implies category form `c2'.
+++ Both are assumed to be definite categories, i.e. they contain
+++ no variables.
+categoryImplies(c1,c2) ==
+  c2 = $Type => true
+  c1 is ["Join",:cats] =>  
+    or/[categoryImplies(c,c2) for c in cats] => true
+  c1 = c2
+  -- ??? Should also check conditional definition and
+  -- ??? possibly attributes
+
+++ returns true if domain `d' satisfies category `c'.
 evalCategory(d,c) ==
   -- tests whether domain d has category c
-  isPartialMode d or ofCategory(d,c)
+  isPartialMode d => true            -- maybe too generous
+  -- If this is a local variable then, its declared type 
+  -- must imply category `c' satisfaction.
+  IDENTP d and (m := getmode(d,$env)) => categoryImplies(m,c)
+  ofCategory(d,c)
 
 isOkInterpMode m ==
   isPartialMode(m) => isLegitimateMode(m,nil,nil)
-- 
cgit v1.2.3