From 95463f6dbae318b055e2cb7927ac7acb320c8382 Mon Sep 17 00:00:00 2001
From: aarne <unknown>
Date: Tue, 13 Sep 2005 21:05:32 +0000
Subject: [PATCH] fix in tc

---
 doc/gf-bib.bib              |  8 ++++++++
 grammars/logic/Logic.gf     |  9 +++++++--
 src/GF/Grammar/TypeCheck.hs | 15 +++++++++++----
 3 files changed, 26 insertions(+), 6 deletions(-)

diff --git a/doc/gf-bib.bib b/doc/gf-bib.bib
index ecdb33462..629e279a7 100644
--- a/doc/gf-bib.bib
+++ b/doc/gf-bib.bib
@@ -990,6 +990,14 @@
   address =      {{Siena}, {Italy}}
 }
 
+@InProceedings{ranta-nancy,
+  author =       {A. Ranta},
+  title =        {Resource Grammars for Dialogue Systems and Grammar Writing by Examples},
+  booktitle =    {{TALK Meeting}},
+  year =         2005,
+  address =      {{Nancy}}
+}
+
 @InProceedings{curry,
     AUTHOR = "H. B. Curry",
     TITLE = "Some logical aspects of grammatical structure",
diff --git a/grammars/logic/Logic.gf b/grammars/logic/Logic.gf
index 41fd5cef8..5f49fc2e1 100644
--- a/grammars/logic/Logic.gf
+++ b/grammars/logic/Logic.gf
@@ -73,7 +73,8 @@ fun
   Pron : (A : Dom) -> Elem A -> Elem A ;
 
 def 
-  -- proof normalization
+  -- proof normalization; does not tc 13/9/2005
+
   ConjEl _ _ (ConjI _ _ a _) = a ;
   ConjEr _ _ (ConjI _ _ _ b) = b ;
   DisjE _ _ _ (DisjIl _ _ a) d _ = d a ;
@@ -81,7 +82,11 @@ def
   ImplE _ _ (ImplI _ _ b) a = b a ;
   NegE _ (NegI _ b) a = b a ;
   UnivE _ _ (UnivI _ _ b) a = b a ;
-  ExistE _ _ _ (ExistI _ _ a b) d = d a b ;
+---  ExistE _ _ _ (ExistI _ _ a b) d = d a b ; 
+--- does not tc 13/9/2005: {a{-2-}<>a{-0-}}
+--- moreover: no problem with
+--- ConjEr _ _ (ConjI _ _ a _) = a ;
+--- But this changes when A B are used instead of _ _
 
   -- Hypo and Pron are identities
   Hypo _ a = a ;
diff --git a/src/GF/Grammar/TypeCheck.hs b/src/GF/Grammar/TypeCheck.hs
index 66416f1d4..3158aae17 100644
--- a/src/GF/Grammar/TypeCheck.hs
+++ b/src/GF/Grammar/TypeCheck.hs
@@ -5,9 +5,9 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/04/21 16:22:30 $ 
--- > CVS $Author: bringert $
--- > CVS $Revision: 1.14 $
+-- > CVS $Date: 2005/09/13 22:05:32 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.15 $
 --
 -- (Description of the module)
 -----------------------------------------------------------------------------
@@ -243,7 +243,14 @@ cont2val = type2val . cont2exp
 justTypeCheckSrc :: Grammar -> Exp -> Val -> Err Constraints
 justTypeCheckSrc gr e v = do
   (_,constrs0) <- checkExp (grammar2theorySrc gr) (initTCEnv []) e v
-  return $ fst $ splitConstraintsSrc gr constrs0
+  return $ filter notJustMeta constrs0
+----  return $ fst $ splitConstraintsSrc gr constrs0
+---- this change was to force proper tc of abstract modules. 
+---- May not be quite right. AR 13/9/2005 
+ where 
+   notJustMeta (c,k) = case (c,k) of
+     (VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
+     _ -> True
 
 grammar2theorySrc :: Grammar -> Theory
 grammar2theorySrc gr (m,f) = case lookupFunTypeSrc gr m f of