From 2bd22e078aa0205f60bb414d2e7f17d73db1eaea Mon Sep 17 00:00:00 2001 From: aarne Date: Mon, 1 Nov 2004 21:41:18 +0000 Subject: [PATCH] some bug fixes in type check and solve --- examples/gfcc/Imper.gf | 4 +-- src/GF/Grammar/AbsCompute.hs | 20 ++++++++------ src/GF/Grammar/Lookup.hs | 12 +++++++++ src/GF/Grammar/TypeCheck.hs | 51 ++++++++++++++++++++++++------------ src/GF/UseGrammar/Custom.hs | 8 +++--- src/GF/UseGrammar/Editing.hs | 18 +++++++------ 6 files changed, 73 insertions(+), 40 deletions(-) diff --git a/examples/gfcc/Imper.gf b/examples/gfcc/Imper.gf index db7f3e8c8..14f3041dc 100644 --- a/examples/gfcc/Imper.gf +++ b/examples/gfcc/Imper.gf @@ -25,8 +25,8 @@ abstract Imper = { Decl : (A : Typ) -> (Var A -> Stm) -> Stm ; Assign : (A : Typ) -> Var A -> Exp A -> Stm -> Stm ; - While : Exp TInt -> Stm -> Stm -> Stm ; - IfElse : Exp TInt -> Stm -> Stm -> Stm -> Stm ; + While : Exp (TNum TInt) -> Stm -> Stm -> Stm ; + IfElse : Exp (TNum TInt) -> Stm -> Stm -> Stm -> Stm ; Block : Stm -> Stm -> Stm ; Printf : (A : Typ) -> Exp A -> Stm -> Stm ; Return : (A : Typ) -> Exp A -> Stm ; 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