summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/GF/Grammar/AbsCompute.hs20
-rw-r--r--src/GF/Grammar/Lookup.hs12
-rw-r--r--src/GF/Grammar/TypeCheck.hs51
-rw-r--r--src/GF/UseGrammar/Custom.hs8
-rw-r--r--src/GF/UseGrammar/Editing.hs18
5 files changed, 71 insertions, 38 deletions
diff --git a/src/GF/Grammar/AbsCompute.hs b/src/GF/Grammar/AbsCompute.hs
index d80fc57f3..55d051f81 100644
--- a/src/GF/Grammar/AbsCompute.hs
+++ b/src/GF/Grammar/AbsCompute.hs
@@ -17,10 +17,13 @@ compute :: GFCGrammar -> Exp -> Err Exp
compute = computeAbsTerm
computeAbsTerm :: GFCGrammar -> Exp -> Err Exp
-computeAbsTerm gr = computeAbsTermIn gr []
+computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) []
-computeAbsTermIn :: GFCGrammar -> [Ident] -> Exp -> Err Exp
-computeAbsTermIn gr xs e = errIn ("computing" +++ prt e) $ compt xs e where
+--- a hack to make compute work on source grammar as well
+type LookDef = Ident -> Ident -> Err (Maybe Term)
+
+computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
+computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
compt vv t = case t of
Prod x a b -> liftM2 (Prod x) (compt vv a) (compt (x:vv) b)
Abs x b -> liftM (Abs x) (compt (x:vv) b)
@@ -46,11 +49,12 @@ computeAbsTermIn gr xs e = errIn ("computing" +++ prt e) $ compt xs e where
_ -> do
return $ mkAbs yy $ mkApp f aa'
- look (Q m f) = case lookupAbsDef gr m f of
- Ok (Just EData) -> Nothing -- canonical --- should always be QC
- Ok md -> md
- _ -> Nothing
- look _ = Nothing
+ look t = case t of
+ (Q m f) -> case lookd m f of
+ Ok (Just EData) -> Nothing -- canonical --- should always be QC
+ Ok md -> md
+ _ -> Nothing
+ _ -> Nothing
beta :: [Ident] -> Exp -> Exp
beta vv c = case c of
diff --git a/src/GF/Grammar/Lookup.hs b/src/GF/Grammar/Lookup.hs
index 19dc4cda1..be69a1656 100644
--- a/src/GF/Grammar/Lookup.hs
+++ b/src/GF/Grammar/Lookup.hs
@@ -101,6 +101,18 @@ qualifAnnotPar m t = case t of
Con c -> QC m c
_ -> composSafeOp (qualifAnnotPar m) t
+lookupAbsDef :: SourceGrammar -> Ident -> Ident -> Err (Maybe Term)
+lookupAbsDef gr m c = errIn ("looking up absdef of" +++ prt c) $ do
+ mi <- lookupModule gr m
+ case mi of
+ ModMod mo -> do
+ info <- lookupInfo mo c
+ case info of
+ AbsFun _ (Yes t) -> return $ return t
+ AnyInd _ n -> lookupAbsDef gr n c
+ _ -> return Nothing
+ _ -> Bad $ prt m +++ "is not an abstract module"
+
lookupLincat :: SourceGrammar -> Ident -> Ident -> Err Type
lookupLincat gr m c | elem c [zIdent "String", zIdent "Int"] =
diff --git a/src/GF/Grammar/TypeCheck.hs b/src/GF/Grammar/TypeCheck.hs
index a029235a8..fa96624f6 100644
--- a/src/GF/Grammar/TypeCheck.hs
+++ b/src/GF/Grammar/TypeCheck.hs
@@ -7,6 +7,7 @@ import Abstract
import AbsCompute
import Refresh
import LookAbs
+import qualified Lookup ---
import TC
@@ -24,14 +25,14 @@ annotate gr exp = annotateIn gr [] exp Nothing
justTypeCheck :: GFCGrammar -> Exp -> Val -> Err Constraints
justTypeCheck gr e v = do
(_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
- constrs1 <- reduceConstraints gr 0 constrs0
- return $ fst $ splitConstraints constrs1
+ constrs1 <- reduceConstraints (lookupAbsDef gr) 0 constrs0
+ return $ fst $ splitConstraints gr constrs1
-- type check in empty context, return the expression itself if valid
checkIfValidExp :: GFCGrammar -> Exp -> Err Exp
checkIfValidExp gr e = do
(_,_,constrs0) <- inferExp (grammar2theory gr) (initTCEnv []) e
- constrs1 <- reduceConstraints gr 0 constrs0
+ constrs1 <- reduceConstraints (lookupAbsDef gr) 0 constrs0
ifNull (return e) (Bad . unwords . prConstrs) constrs1
annotateIn :: GFCGrammar -> Binds -> Exp -> Maybe Val -> Err Tree
@@ -45,7 +46,7 @@ annotateIn gr gamma exp = maybe (infer exp) (check exp) where
env = initTCEnv gamma
theory = grammar2theory gr
aexp2treeC (a,c) = do
- c' <- reduceConstraints gr (length gamma) c
+ c' <- reduceConstraints (lookupAbsDef gr) (length gamma) c
aexp2tree (a,c')
-- invariant way of creating TCEnv from context
@@ -53,34 +54,48 @@ initTCEnv gamma =
(length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma)
-- process constraints after eqVal by computing by defs
-reduceConstraints :: GFCGrammar -> Int -> Constraints -> Err Constraints
-reduceConstraints gr i = liftM concat . mapM redOne where
+reduceConstraints :: LookDef -> Int -> Constraints -> Err Constraints
+reduceConstraints look i = liftM concat . mapM redOne where
redOne (u,v) = do
- u' <- computeVal gr u
- v' <- computeVal gr v
+ u' <- computeVal look u
+ v' <- computeVal look v
eqVal i u' v'
-computeVal :: GFCGrammar -> Val -> Err Val
-computeVal gr v = case v of
+computeVal :: LookDef -> Val -> Err Val
+computeVal look v = case v of
VClos g@(_:_) e -> do
e' <- compt (map fst g) e --- bindings of g in e?
whnf $ VClos g e'
+{- ----
+ _ -> do ---- how to compute a Val, really??
+ e <- val2exp v
+ e' <- compt [] e
+ whnf $ vClos e'
+-}
VApp f c -> liftM2 VApp (compv f) (compv c) >>= whnf
_ -> whnf v
where
- compt = computeAbsTermIn gr
- compv = computeVal gr
+ compt = computeAbsTermIn look
+ compv = computeVal look
-- take apart constraints that have the form (? <> t), usable as solutions
-splitConstraints :: Constraints -> (Constraints,MetaSubst)
-splitConstraints cs = csmsu where
+splitConstraints :: GFCGrammar -> Constraints -> (Constraints,MetaSubst)
+splitConstraints gr = splitConstraintsGen (lookupAbsDef gr)
+
+splitConstraintsSrc :: Grammar -> Constraints -> (Constraints,MetaSubst)
+splitConstraintsSrc gr = splitConstraintsGen (Lookup.lookupAbsDef gr)
+
+splitConstraintsGen :: LookDef -> Constraints -> (Constraints,MetaSubst)
+splitConstraintsGen look cs = csmsu where
csmsu = (nub [(a,b) | (a,b) <- csf1,a /= b],msf1)
(csf1,msf1) = unif (csf,msf) -- alternative: filter first
(csf,msf) = foldr mkOne ([],[]) cs
csmsf = foldr mkOne ([],msu) csu
- (csu,msu) = unif (cs,[]) -- alternative: unify first
+ (csu,msu) = unif (cs1,[]) -- alternative: unify first
+
+ cs1 = errVal cs $ reduceConstraints look 0 cs
mkOne (u,v) = case (u,v) of
(VClos g (Meta m), v) | null g -> sub m v
@@ -112,6 +127,9 @@ performMetaSubstNode subst n@(N (b,a,v,(c,m),s)) = let
Meta m -> errVal e $ maybe (return e) val2expSafe $ lookup m subst
_ -> composSafeOp metaSubstExp e
+reduceConstraintsNode gr = changeConstrs red where
+ red cs = errVal cs $ reduceConstraints (lookupAbsDef gr) 0 cs
+
-- weak heuristic to narrow down menus; not used for TC. 15/11/2001
-- the age-old method from GF 0.9
possibleConstraints :: GFCGrammar -> Constraints -> Bool
@@ -191,8 +209,7 @@ cont2val = type2val . cont2exp
justTypeCheckSrc :: Grammar -> Exp -> Val -> Err Constraints
justTypeCheckSrc gr e v = do
(_,constrs0) <- checkExp (grammar2theorySrc gr) (initTCEnv []) e v
------ constrs1 <- reduceConstraints gr 0 constrs0
- return $ fst $ splitConstraints constrs0
+ return $ fst $ splitConstraintsSrc gr constrs0
grammar2theorySrc :: Grammar -> Theory
grammar2theorySrc gr (m,f) = case lookupFunTypeSrc gr m f of
diff --git a/src/GF/UseGrammar/Custom.hs b/src/GF/UseGrammar/Custom.hs
index dfffd2b2a..f28bfc6e1 100644
--- a/src/GF/UseGrammar/Custom.hs
+++ b/src/GF/UseGrammar/Custom.hs
@@ -264,12 +264,10 @@ customTermCommand =
in
[tr | t <- generateTrees gr False cat 2 Nothing (Just t),
Ok tr <- [annotate gr $ MM.qualifTerm (absId g) t]])
-
- ,(strCI "typecheck", \g t -> let gr = grammar g in
- err (const []) (return . const t)
- (checkIfValidExp gr (tree2exp t)))
+ ,(strCI "typecheck", \g t -> err (const [t]) (return . loc2tree)
+ (reCheckState (grammar g) (tree2loc t)))
,(strCI "solve", \g t -> err (const [t]) (return . loc2tree)
- (uniqueRefinements (grammar g) (tree2loc t)))
+ (solveAll (grammar g) (tree2loc t)))
,(strCI "context", \g t -> err (const [t]) (return . loc2tree)
(contextRefinements (grammar g) (tree2loc t)))
,(strCI "reindex", \g t -> let gr = grammar g in
diff --git a/src/GF/UseGrammar/Editing.hs b/src/GF/UseGrammar/Editing.hs
index 45e180b0d..12113b91f 100644
--- a/src/GF/UseGrammar/Editing.hs
+++ b/src/GF/UseGrammar/Editing.hs
@@ -187,10 +187,11 @@ refineWithTreeReal :: Bool -> CGrammar -> Tree -> Meta -> Action
refineWithTreeReal der gr tree m state = do
state' <- replaceSubTree tree state
let cs0 = allConstrs state'
- (cs,ms) = splitConstraints cs0
+ (cs,ms) = splitConstraints gr cs0
v = vClos $ tree2exp (bodyTree tree)
msubst = (m,v) : ms
- metaSubstRefinements gr msubst $ mapLoc (performMetaSubstNode msubst) state'
+ metaSubstRefinements gr msubst $
+ mapLoc (reduceConstraintsNode gr . performMetaSubstNode msubst) state'
-- without dep. types, no constraints, no grammar needed - simply: do
-- testErr (actIsMeta state) "move pointer to meta"
@@ -339,12 +340,13 @@ reCheckState gr st = annotate gr (tree2exp (loc2tree st)) >>= return . tree2loc
-- extract metasubstitutions from constraints and solve them
solveAll :: CGrammar -> State -> Err State
-solveAll gr st0 = do
- st <- reCheckState gr st0
- let cs0 = allConstrs st
- (cs,ms) = splitConstraints cs0
- metaSubstRefinements gr ms $ mapLoc (performMetaSubstNode ms) st
-
+solveAll gr st = solve st >>= solve where
+ solve st0 = do ---- why need twice?
+ st <- reCheckState gr st0
+ let cs0 = allConstrs st
+ (cs,ms) = splitConstraints gr cs0
+ metaSubstRefinements gr ms $
+ mapLoc (reduceConstraintsNode gr . performMetaSubstNode ms) st
-- active refinements
generated by cgit v1.2.3 (git 2.39.1) at 2026-05-20 08:41:12 +0000