summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/GF/Grammar/TC.hs51
-rw-r--r--src/GF/Grammar/TypeCheck.hs11
-rw-r--r--src/GF/UseGrammar/GetTree.hs8
3 files changed, 56 insertions, 14 deletions
diff --git a/src/GF/Grammar/TC.hs b/src/GF/Grammar/TC.hs
index 411b84e30..5864c5af0 100644
--- a/src/GF/Grammar/TC.hs
+++ b/src/GF/Grammar/TC.hs
@@ -5,9 +5,9 @@
-- Stability : (stable)
-- Portability : (portable)
--
--- > CVS $Date: 2005/04/21 16:22:29 $
--- > CVS $Author: bringert $
--- > CVS $Revision: 1.9 $
+-- > CVS $Date: 2005/09/15 16:22:02 $
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.10 $
--
-- Thierry Coquand's type checking algorithm that creates a trace
-----------------------------------------------------------------------------
@@ -16,6 +16,7 @@ module GF.Grammar.TC (AExp(..),
Theory,
checkExp,
inferExp,
+ checkEqs,
eqVal,
whnf
) where
@@ -25,6 +26,7 @@ import GF.Grammar.Abstract
import GF.Grammar.AbsCompute
import Control.Monad
+import Data.List (sortBy)
data AExp =
AVr Ident Val
@@ -36,7 +38,7 @@ data AExp =
| AApp AExp AExp Val
| AAbs Ident Val AExp
| AProd Ident AExp AExp
- | AEqs [([Exp],AExp)] ---
+ | AEqs [([Exp],AExp)] --- not used
| AData Val
deriving (Eq,Show)
@@ -119,11 +121,12 @@ checkExp th tenv@(k,rho,gamma) e ty = do
return (AAbs x a' t', cs)
_ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ
+-- {- --- to get deprec when checkEqs works (15/9/2005)
Eqs es -> do
bcs <- mapM (\b -> checkBranch th tenv b typ) es
let (bs,css) = unzip bcs
return (AEqs bs, concat css)
-
+-- - }
Prod x a b -> do
testErr (typ == vType) "expected Type"
(a',csa) <- checkType th tenv a
@@ -165,7 +168,42 @@ inferExp th tenv@(k,rho,gamma) e = case e of
IC "String" -> return $ const $ Q cPredefAbs cString
_ -> Bad s
----- this is an unreliable function which should be rewritten (AR)
+checkEqs :: Theory -> TCEnv -> (Fun,Trm) -> Val -> Err [(Val,Val)]
+checkEqs th tenv@(k,rho,gamma) (fun@(m,f),def) val = case def of
+ Eqs es -> liftM concat $ mapM checkBranch es
+ _ -> liftM snd $ checkExp th tenv def val
+ where
+ checkBranch (ps,df) =
+ let
+ (ps',_,vars) = foldr p2t ([],0,[]) ps
+ fps = mkApp (Q m f) ps'
+ in errIn ("branch" +++ prt fps) $ do
+ (aexp, typ, cs1) <- inferExp th tenv fps
+ let
+ bds = binds vars aexp
+ tenv' = (k, rho, bds ++ gamma)
+ (_,cs2) <- errIn (show bds) $ checkExp th tenv' df typ
+ return $ (cs1 ++ cs2)
+ p2t p (ps,i,g) = case p of
+ PW -> (meta (MetaSymb i) : ps, i+1, g)
+ PV IW -> (meta (MetaSymb i) : ps, i+1, g)
+ PV x -> (meta (MetaSymb i) : ps, i+1,upd x i g)
+ PString s -> ( K s : ps, i, g)
+ PInt i -> (EInt i : ps, i, g)
+ PP m c xs -> (mkApp (qq (m,c)) xss : ps, i', g')
+ where (xss,i',g') = foldr p2t ([],i,g) xs
+ _ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
+ upd x i g = (x,i) : g --- to annotate pattern variables: treat as metas
+
+ -- notice: in vars, the sequence 0.. is sorted. In subst aexp, all
+ -- this occurs and nothing else.
+ binds vars aexp = [(x,v) | ((x,_),v) <- zip vars metas] where
+ metas = map snd $ sortBy (\ (x,_) (y,_) -> compare x y) $ subst aexp
+ subst aexp = case aexp of
+ AMeta (MetaSymb i) v -> [(i,v)]
+ AApp c a _ -> subst c ++ subst a
+ _ -> [] -- never matter in patterns
+
checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
chB tenv' ps' ty
@@ -207,6 +245,7 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
upd x k g = (x, VGen k x) : g --- hack to recognize pattern variables
+
checkPatt :: Theory -> TCEnv -> Exp -> Val -> Err (Binds,[(Val,Val)])
checkPatt th tenv exp val = do
(aexp,_,cs) <- checkExpP tenv exp val
diff --git a/src/GF/Grammar/TypeCheck.hs b/src/GF/Grammar/TypeCheck.hs
index 3158aae17..53c9a4ad7 100644
--- a/src/GF/Grammar/TypeCheck.hs
+++ b/src/GF/Grammar/TypeCheck.hs
@@ -5,9 +5,9 @@
-- Stability : (stable)
-- Portability : (portable)
--
--- > CVS $Date: 2005/09/13 22:05:32 $
+-- > CVS $Date: 2005/09/15 16:22:02 $
-- > CVS $Author: aarne $
--- > CVS $Revision: 1.15 $
+-- > CVS $Revision: 1.16 $
--
-- (Description of the module)
-----------------------------------------------------------------------------
@@ -247,8 +247,8 @@ justTypeCheckSrc gr e v = do
---- 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
+
+notJustMeta (c,k) = case (c,k) of
(VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
_ -> True
@@ -268,8 +268,9 @@ checkTyp gr typ = err singleton prConstrs $ justTypeCheckSrc gr typ vType
checkEquation :: Grammar -> Fun -> Trm -> [String]
checkEquation gr (m,fun) def = err singleton id $ do
typ <- lookupFunTypeSrc gr m fun
+---- cs <- checkEqs (grammar2theorySrc gr) (initTCEnv []) ((m,fun),def) (vClos typ)
cs <- justTypeCheckSrc gr def (vClos typ)
- let cs1 = cs ----- filter (not . possibleConstraint gr) cs ----
+ let cs1 = filter notJustMeta cs ----- filter (not . possibleConstraint gr) cs ----
return $ ifNull [] (singleton . prConstraints) cs1
checkConstrs :: Grammar -> Cat -> [Ident] -> [String]
diff --git a/src/GF/UseGrammar/GetTree.hs b/src/GF/UseGrammar/GetTree.hs
index e71475654..e980a3d95 100644
--- a/src/GF/UseGrammar/GetTree.hs
+++ b/src/GF/UseGrammar/GetTree.hs
@@ -5,9 +5,9 @@
-- Stability : (stable)
-- Portability : (portable)
--
--- > CVS $Date: 2005/06/03 21:51:59 $
+-- > CVS $Date: 2005/09/15 16:22:02 $
-- > CVS $Author: aarne $
--- > CVS $Revision: 1.8 $
+-- > CVS $Revision: 1.9 $
--
-- how to form linearizable trees from strings and from terms of different levels
--
@@ -24,6 +24,7 @@ import GF.Grammar.MMacros
import GF.Grammar.Macros
import GF.Compile.Rename
import GF.Grammar.TypeCheck
+import GF.Grammar.AbsCompute (beta)
import GF.Compile.PGrammar
import GF.Compile.ShellState
@@ -42,7 +43,8 @@ string2treeErr :: StateGrammar -> String -> Err Tree
string2treeErr _ "" = Bad "empty string"
string2treeErr gr s = do
t <- pTerm s
- let t1 = refreshMetas [] t
+ let t0 = beta [] t
+ let t1 = refreshMetas [] t0
let t2 = qualifTerm abstr t1
annotate grc t2
where
generated by cgit v1.2.3 (git 2.39.1) at 2026-05-20 15:49:07 +0000