mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-22 01:22:51 -06:00
fix in tc
This commit is contained in:
@@ -990,6 +990,14 @@
|
|||||||
address = {{Siena}, {Italy}}
|
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,
|
@InProceedings{curry,
|
||||||
AUTHOR = "H. B. Curry",
|
AUTHOR = "H. B. Curry",
|
||||||
TITLE = "Some logical aspects of grammatical structure",
|
TITLE = "Some logical aspects of grammatical structure",
|
||||||
|
|||||||
@@ -73,7 +73,8 @@ fun
|
|||||||
Pron : (A : Dom) -> Elem A -> Elem A ;
|
Pron : (A : Dom) -> Elem A -> Elem A ;
|
||||||
|
|
||||||
def
|
def
|
||||||
-- proof normalization
|
-- proof normalization; does not tc 13/9/2005
|
||||||
|
|
||||||
ConjEl _ _ (ConjI _ _ a _) = a ;
|
ConjEl _ _ (ConjI _ _ a _) = a ;
|
||||||
ConjEr _ _ (ConjI _ _ _ b) = b ;
|
ConjEr _ _ (ConjI _ _ _ b) = b ;
|
||||||
DisjE _ _ _ (DisjIl _ _ a) d _ = d a ;
|
DisjE _ _ _ (DisjIl _ _ a) d _ = d a ;
|
||||||
@@ -81,7 +82,11 @@ def
|
|||||||
ImplE _ _ (ImplI _ _ b) a = b a ;
|
ImplE _ _ (ImplI _ _ b) a = b a ;
|
||||||
NegE _ (NegI _ b) a = b a ;
|
NegE _ (NegI _ b) a = b a ;
|
||||||
UnivE _ _ (UnivI _ _ 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 and Pron are identities
|
||||||
Hypo _ a = a ;
|
Hypo _ a = a ;
|
||||||
|
|||||||
@@ -5,9 +5,9 @@
|
|||||||
-- Stability : (stable)
|
-- Stability : (stable)
|
||||||
-- Portability : (portable)
|
-- Portability : (portable)
|
||||||
--
|
--
|
||||||
-- > CVS $Date: 2005/04/21 16:22:30 $
|
-- > CVS $Date: 2005/09/13 22:05:32 $
|
||||||
-- > CVS $Author: bringert $
|
-- > CVS $Author: aarne $
|
||||||
-- > CVS $Revision: 1.14 $
|
-- > CVS $Revision: 1.15 $
|
||||||
--
|
--
|
||||||
-- (Description of the module)
|
-- (Description of the module)
|
||||||
-----------------------------------------------------------------------------
|
-----------------------------------------------------------------------------
|
||||||
@@ -243,7 +243,14 @@ cont2val = type2val . cont2exp
|
|||||||
justTypeCheckSrc :: Grammar -> Exp -> Val -> Err Constraints
|
justTypeCheckSrc :: Grammar -> Exp -> Val -> Err Constraints
|
||||||
justTypeCheckSrc gr e v = do
|
justTypeCheckSrc gr e v = do
|
||||||
(_,constrs0) <- checkExp (grammar2theorySrc gr) (initTCEnv []) e v
|
(_,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 :: Grammar -> Theory
|
||||||
grammar2theorySrc gr (m,f) = case lookupFunTypeSrc gr m f of
|
grammar2theorySrc gr (m,f) = case lookupFunTypeSrc gr m f of
|
||||||
|
|||||||
Reference in New Issue
Block a user