diff --git a/src/compiler/GF/Compile/TypeCheck/Abstract.hs b/src/compiler/GF/Compile/TypeCheck/Abstract.hs index c766602597..ad163e9a6d 100644 --- a/src/compiler/GF/Compile/TypeCheck/Abstract.hs +++ b/src/compiler/GF/Compile/TypeCheck/Abstract.hs @@ -38,13 +38,16 @@ initTCEnv gamma = -- interface to TC type checker -type2val :: Type -> Val -type2val = VClos [] +type2val :: Type -> NotVal +type2val = NVClos [] + +type2nval :: Type -> NotVal +type2nval = NVClos [] cont2exp :: Context -> Term cont2exp c = mkProd c eType [] -- to check a context -cont2val :: Context -> Val +cont2val :: Context -> NotVal cont2val = type2val . cont2exp -- some top-level batch-mode checkers for the compiler @@ -61,9 +64,11 @@ notJustMeta (c,k) = case (c,k) of grammar2theory :: SourceGrammar -> Theory grammar2theory gr (m,f) = case lookupFunType gr m f of - Ok t -> return $ type2val t + Ok t -> case lookupAbsDef gr m f of -- TODO: Don't lookup twice + Ok (Just n, Just eqs) -> return (type2val t, Just (n, eqs)) + _ -> return (type2val t, Nothing) Bad s -> case lookupCatContext gr m f of - Ok cont -> return $ cont2val cont + Ok cont -> return (cont2val cont,Nothing) _ -> Bad s checkContext :: SourceGrammar -> Context -> [Message] @@ -74,7 +79,7 @@ checkTyp gr typ = err (\x -> [pp x]) ppConstrs $ justTypeCheck gr typ vType checkDef :: SourceGrammar -> Fun -> Type -> Equation -> [Message] checkDef gr (m,fun) typ eq = err (\x -> [pp x]) ppConstrs $ do - (b,cs) <- checkBranch (grammar2theory gr) (initTCEnv []) eq (type2val typ) + (b,cs) <- checkBranch (grammar2theory gr) (initTCEnv []) eq (type2nval typ) (constrs,_) <- unifyVal cs return $ filter notJustMeta constrs diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs index c0df83394d..4cf36ac81b 100644 --- a/src/compiler/GF/Compile/TypeCheck/TC.hs +++ b/src/compiler/GF/Compile/TypeCheck/TC.hs @@ -16,6 +16,7 @@ module GF.Compile.TypeCheck.TC ( AExp(..), Theory, checkExp, + checkNExp, inferExp, checkBranch, eqVal, @@ -31,6 +32,7 @@ import Control.Monad import Data.Maybe import GF.Text.Pretty + data AExp = AVr Ident Val | ACn QIdent Val @@ -54,10 +56,27 @@ data AExp = type ALabelling = (Label, AExp) type AAssign = (Label, (Val, AExp)) -type Theory = QIdent -> Err Val +type Theory = QIdent -> Err (NotVal, Maybe (Int, [Equation])) + +lookupConst :: Theory -> QIdent -> Err (Val, Maybe (Int, [Equation])) +lookupConst th f = do + (nv,info) <- th f + -- checkWhnf (pp (snd f)) th v + v <- whnf th nv + return (v, info) + +checkWhnf :: Doc -> Theory -> Val -> Err () +checkWhnf ctx th v = do + v' <- whnf th (unVal v) + when (v /= v') $ error . render $ ("Not whnf:" <+>) $ + ctx <+> ":" <+> (ppVal v <+> "<>" <+> ppVal v') + $$ show v $$ show v' + +ppVal = ppValue Unqualified 0 -lookupConst :: Theory -> QIdent -> Err Val -lookupConst th f = th f +unVal :: Val -> NotVal +unVal (VClos e t) = NVClos e t +unVal v = NVVal v lookupVar :: Env -> Ident -> Err Val lookupVar g x = maybe (Bad (render ("unknown variable" <+> x))) return $ lookup x ((identW,VClos [] (Meta 0)):g) @@ -68,76 +87,128 @@ type TCEnv = (Int,Env,Env) --emptyTCEnv :: TCEnv --emptyTCEnv = (0,[],[]) -whnf :: Val -> Err Val -whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug +whnf :: Theory -> NotVal -> Err Val +whnf th v = ---- errIn ("whnf" +++ prt v) $ ---- debug case v of - VApp u w -> do - u' <- whnf u - w' <- whnf w - app u' w' - VClos env e -> eval env e - _ -> return v - -app :: Val -> Val -> Err Val -app u v = case u of - VClos env (Abs _ x e) -> eval ((x,v):env) e - _ -> return $ VApp u v - -eval :: Env -> Term -> Err Val -eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $ + NVVal v -> return v + NVClos env e -> eval th env e + +app :: Theory -> Val -> Val -> Err Val +app th u v = case u of + VClos env (Abs _ x e) -> do + val <- eval th ((x,v):env) e + evalDef th val + VApp u' v' -> do + let val = VApp u' (v' ++ [v]) + evalDef th val + _ -> do + return $ VApp u [v] + +evalDef :: Theory -> Val -> Err Val +evalDef th e = case e of + VApp (VCn c (Just (n, eqs))) xs | length xs == n -> do + e' <- tryMatchEqns eqs xs + case e' of + Just (NVClos env tm) -> eval th env tm + _ -> return e + _ -> do + return e + +tryMatchEqns :: [Equation] -> [Val] -> Err (Maybe NotVal) +tryMatchEqns ((pts,repl):eqs) xs = do + me' <- tryMatchEqn [] pts xs repl + case me' of + Nothing -> tryMatchEqns eqs xs + Just e' -> return $ Just e' +tryMatchEqns [] xs = return Nothing + +tryMatchEqn :: Env -> [Patt] -> [Val] -> Term -> Err (Maybe NotVal) +tryMatchEqn env [] [] repl = return $ Just $ NVClos env repl +tryMatchEqn env (PW: ps) (v: vs) repl = + tryMatchEqn env ps vs repl +tryMatchEqn env (PV c: ps) (v: vs) repl = + tryMatchEqn ((c,v):env) ps vs repl -- TODO: Is this sound? +tryMatchEqn env (PP (q,p) pp: ps) (VApp (VCn (r,f) _) tt: vs) repl + | p == f && length pp == length tt = tryMatchEqn env (pp ++ ps) (tt ++ vs) repl +-- tryMatchEqn env (p: ps) (v: vs) repl = _ +tryMatchEqn env (a:_) (b:_) _ = do + return Nothing +tryMatchEqn env _ _ _ = Bad "tryMatchEqn: Non-matching length" + +eval :: Theory -> Env -> Term -> Err Val +eval th env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $ case e of Vr x -> lookupVar env x - Q c -> return $ VCn c - QC c -> return $ VCn c ---- == Q ? + Q c -> do + (_ty, defEqns) <- lookupConst th c + return $ VCn c defEqns + QC c -> do + (_ty, defEqns) <- lookupConst th c + return $ VCn c defEqns ---- == Q ? Sort c -> return $ VType --- the only sort is Type - App f a -> join $ liftM2 app (eval env f) (eval env a) - RecType xs -> do xs <- mapM (\(l,e) -> eval env e >>= \e -> return (l,e)) xs + App f a -> do + join $ liftM2 (app th) (eval th env f) (eval th env a) + RecType xs -> do xs <- mapM (\(l,e) -> eval th env e >>= \e -> return (l,e)) xs return (VRecType xs) - _ -> return $ VClos env e + _ -> do + return $ VClos env e -eqVal :: Int -> Val -> Val -> Err [(Val,Val)] -eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $ +eqNVal :: Theory -> Int -> NotVal -> NotVal -> Err [(Val,Val)] +eqNVal th k u1 u2 = do + w1 <- whnf th u1 + w2 <- whnf th u2 + eqVal th k w1 w2 + +eqVal :: Theory -> Int -> Val -> Val -> Err [(Val,Val)] +eqVal th k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $ do - w1 <- whnf u1 - w2 <- whnf u2 + -- w1 <- whnf th u1 + -- w2 <- whnf th u2 + let (w1,w2) = (u1,u2) let v = VGen k case (w1,w2) of - (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2) + (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal th k f1 f2) (fmap concat $ zipWithM (eqVal th k) a1 a2) (VClos env1 (Abs _ x1 e1), VClos env2 (Abs _ x2 e2)) -> - eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2) + eqNVal th (k+1) (NVClos ((x1,v x1):env1) e1) (NVClos ((x2,v x1):env2) e2) (VClos env1 (Prod _ x1 a1 e1), VClos env2 (Prod _ x2 a2 e2)) -> liftM2 (++) - (eqVal k (VClos env1 a1) (VClos env2 a2)) - (eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)) + (eqNVal th k (NVClos env1 a1) (NVClos env2 a2)) + (eqNVal th (k+1) (NVClos ((x1,v x1):env1) e1) (NVClos ((x2,v x1):env2) e2)) (VGen i _, VGen j _) -> return [(w1,w2) | i /= j] - (VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j] + (VCn (_, i) _, VCn (_,j) _) -> return [(w1,w2) | i /= j] --- thus ignore qualifications; valid because inheritance cannot --- be qualified. Simplifies annotation. AR 17/3/2005 - _ -> return [(w1,w2) | w1 /= w2] + _ -> do + return [(w1,w2) | w1 /= w2] -- invariant: constraints are in whnf checkType :: Theory -> TCEnv -> Term -> Err (AExp,[(Val,Val)]) checkType th tenv e = checkExp th tenv e vType -checkExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)]) -checkExp th tenv@(k,rho,gamma) e ty = do - typ <- whnf ty +checkNExp :: Theory -> TCEnv -> Term -> NotVal -> Err (AExp, [(Val,Val)]) +checkNExp th tenv@(k,rho,gamma) e ty = do + typ <- whnf th ty + checkWhnf (pp "checkNExp:") th typ + checkExp th tenv e typ + +checkExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)]) +checkExp th tenv@(k,rho,gamma) e typ = do let v = VGen k case e of Meta m -> return $ (AMeta m typ,[]) Abs _ x t -> case typ of VClos env (Prod _ y a b) -> do - a' <- whnf $ VClos env a --- - (t',cs) <- checkExp th - (k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b) + a' <- whnf th $ NVClos env a --- + (t',cs) <- checkNExp th + (k+1,(x,v x):rho, (x,a'):gamma) t (NVClos ((y,v x):env) b) return (AAbs x a' t', cs) _ -> Bad (render ("function type expected for" <+> ppTerm Unqualified 0 e <+> "instead of" <+> ppValue Unqualified 0 typ)) Let (x, (mb_typ, e1)) e2 -> do (val,e1,cs1) <- case mb_typ of Just typ -> do (_,cs1) <- checkType th tenv typ - val <- eval rho typ + val <- eval th rho typ (e1,cs2) <- checkExp th tenv e1 val return (val,e1,cs1++cs2) Nothing -> do (e1,val,cs) <- inferExp th tenv e1 @@ -148,7 +219,8 @@ checkExp th tenv@(k,rho,gamma) e ty = do Prod _ x a b -> do testErr (typ == vType) "expected Type" (a',csa) <- checkType th tenv a - (b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b + aWhnf <- whnf th (NVClos rho a) + (b',csb) <- checkType th (k+1, (x,v x):rho, (x,aWhnf):gamma) b return (AProd x a' b', csa ++ csb) R xs -> @@ -164,25 +236,28 @@ checkExp th tenv@(k,rho,gamma) e ty = do P r l -> do (r',cs) <- checkExp th tenv r (VRecType [(l,typ)]) return (AP r' l typ,cs) - Glue x y -> do cs1 <- eqVal k valAbsFloat typ + Glue x y -> do cs1 <- eqVal th k valAbsFloat typ (x,cs2) <- checkExp th tenv x typ (y,cs3) <- checkExp th tenv y typ return (AGlue x y,cs1++cs2++cs3) _ -> checkInferExp th tenv e typ -checkInferExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)]) +checkInferExp :: Theory -> TCEnv -> Term -> Val -> Err (AExp, [(Val,Val)]) checkInferExp th tenv@(k,_,_) e typ = do (e',w,cs1) <- inferExp th tenv e - cs2 <- eqVal k w typ + checkWhnf (pp "checkInferExp w:") th w + checkWhnf (pp "checkInferExp typ:") th typ + cs2 <- eqVal th k w typ return (e',cs1 ++ cs2) inferExp :: Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val,Val)]) -inferExp th tenv@(k,rho,gamma) e = case e of +inferExp th tenv@(k,rho,gamma) e = + case e of Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x Q (m,c) | m == cPredefAbs && isPredefCat c -> return (ACn (m,c) vType, vType, []) - | otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c) - QC c -> mkAnnot (ACn c) $ noConstr $ lookupConst th c ---- + | otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ fmap fst $ lookupConst th (m,c) + QC c -> mkAnnot (ACn c) $ noConstr $ fmap fst $ lookupConst th c ---- EInt i -> return (AInt i, valAbsInt, []) EFloat i -> return (AFloat i, valAbsFloat, []) K i -> return (AStr i, valAbsString, []) @@ -193,7 +268,7 @@ inferExp th tenv@(k,rho,gamma) e = case e of Let (x, (mb_typ, e1)) e2 -> do (val1,e1,cs1) <- case mb_typ of Just typ -> do (_,cs1) <- checkType th tenv typ - val <- eval rho typ + val <- eval th rho typ (e1,cs2) <- checkExp th tenv e1 val return (val,e1,cs1++cs2) Nothing -> do (e1,val,cs) <- inferExp th tenv e1 @@ -202,11 +277,13 @@ inferExp th tenv@(k,rho,gamma) e = case e of return (ALet (x,(val1,e1)) e2, val2, cs1++cs2) App f t -> do (f',w,csf) <- inferExp th tenv f - typ <- whnf w + -- typ <- whnf th w + let typ = w case typ of VClos env (Prod _ x a b) -> do - (a',csa) <- checkExp th tenv t (VClos env a) - b' <- whnf $ VClos ((x,VClos rho t):env) b + (a',csa) <- checkNExp th tenv t (NVClos env a) + rhoT <- whnf th $ NVClos rho t -- New whnf + b' <- whnf th $ NVClos ((x,rhoT):env) b return $ (AApp f' a' b', b', csf ++ csa) _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ)) _ -> Bad (render ("cannot infer type of expression" <+> ppTerm Unqualified 0 e)) @@ -219,10 +296,10 @@ checkLabelling th tenv (lbl,typ) = do checkAssign :: Theory -> TCEnv -> [(Label,Val)] -> Assign -> Err (AAssign, [(Val,Val)]) checkAssign th tenv@(k,rho,gamma) typs (lbl,(Just typ,exp)) = do (atyp,cs1) <- checkType th tenv typ - val <- eval rho typ + val <- eval th rho typ cs2 <- case lookup lbl typs of Nothing -> return [] - Just val0 -> eqVal k val val0 + Just val0 -> eqVal th k val val0 (aexp,cs3) <- checkExp th tenv exp val return ((lbl,(val,aexp)),cs1++cs2++cs3) checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do @@ -232,7 +309,7 @@ checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do Just val -> do (aexp,cs) <- checkExp th tenv exp val return ((lbl,(val,aexp)),cs) -checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Term],AExp),[(Val,Val)]) +checkBranch :: Theory -> TCEnv -> Equation -> NotVal -> Err (([Term],AExp),[(Val,Val)]) checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $ chB tenv' ps' ty where @@ -241,24 +318,29 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $ tenv' = (k, rho2++rho, gamma) ---- k' ? (k,rho,gamma) = tenv + chB :: (Int, [(Ident, Val)], [(Ident, Val)]) -> [Term] -> NotVal -> Err (([Term], AExp), [(Val, Val)]) chB tenv@(k,rho,gamma) ps ty = case ps of p:ps2 -> do - typ <- whnf ty + typ <- whnf th ty case typ of VClos env (Prod _ y a b) -> do - a' <- whnf $ VClos env a + a' <- whnf th $ NVClos env a (p', sigma, binds, cs1) <- checkP tenv p y a' let tenv' = (length binds, sigma ++ rho, binds ++ gamma) - ((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b) + ((ps',exp),cs2) <- chB tenv' ps2 (NVClos ((y,p'):env) b) return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt _ -> Bad (render ("Product expected for definiens" <+> ppTerm Unqualified 0 t <+> "instead of" <+> ppValue Unqualified 0 typ)) [] -> do - (e,cs) <- checkExp th tenv t ty + (e,cs) <- checkNExp th tenv t ty return (([],e),cs) checkP env@(k,rho,gamma) t x a = do (delta,cs) <- checkPatt th env t a let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]] - return (VClos sigma t, sigma, delta, cs) + -- traceM . render $ ("\ncheckP:" <+>) + -- $ "Making closure:" <+> vcat ["" <+> ppTerm Unqualified 0 t , pp $ show (VClos sigma t)] + -- $$ "In context:" <+> show tenv + sigmaT <- whnf th $ NVClos sigma t -- New whnf + return (sigmaT, sigma, delta, cs) ps2ts k = foldr p2t ([],0,[],k) p2t p (ps,i,g,k) = case p of @@ -289,6 +371,7 @@ checkPatt th tenv exp val = do _ -> [] -- no other cases are possible --- ad hoc, to find types of variables + checkExpP :: (a, Env, c) -> Term -> Val -> Err (AExp, Val, [a2]) checkExpP tenv@(k,rho,gamma) exp val = case exp of Meta m -> return $ (AMeta m val, val, []) Vr x -> return $ (AVr x val, val, []) @@ -297,18 +380,24 @@ checkPatt th tenv exp val = do K s -> return (AStr s, valAbsString, []) Q c -> do - typ <- lookupConst th c + (typ, _eqn) <- lookupConst th c return $ (ACn c typ, typ, []) QC c -> do - typ <- lookupConst th c + (typ, _eqn) <- lookupConst th c return $ (ACn c typ, typ, []) ---- App f t -> do (f',w,csf) <- checkExpP tenv f val - typ <- whnf w + -- typ <- whnf th w + let typ = w -- Already normalized case typ of VClos env (Prod _ x a b) -> do - (a',_,csa) <- checkExpP tenv t (VClos env a) - b' <- whnf $ VClos ((x,VClos rho t):env) b + -- traceM . render $ ("\ncheckPatt:" <+>) + -- $ "Making closure:" <+> vcat ["" <+> ppTerm Unqualified 0 t , pp $ show (VClos env t)] + envA <- whnf th $ NVClos env a -- New whnf + (a',_,csa) <- checkExpP tenv t envA + rhoT <- whnf th $ NVClos rho t -- New whnf + b' <- whnf th $ NVClos ((x,rhoT):env) b + checkWhnf (pp "checkPatt") th b' return $ (AApp f' a' b', b', csf ++ csa) _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ)) _ -> Bad (render ("cannot typecheck pattern" <+> ppTerm Unqualified 0 exp)) diff --git a/src/compiler/GF/Compile/Update.hs b/src/compiler/GF/Compile/Update.hs index 7bbe1d8dc2..836d9652f3 100644 --- a/src/compiler/GF/Compile/Update.hs +++ b/src/compiler/GF/Compile/Update.hs @@ -38,10 +38,11 @@ buildAnyTree m = go Map.empty case Map.lookup c map of Just i -> case unifyAnyInfo m i j of Ok k -> go (Map.insert c k map) is - Bad _ -> fail $ render ("conflicting information in module"<+>m $$ + Bad msg -> fail $ render ("conflicting information in module"<+>m $$ nest 4 (ppJudgement Qualified (c,i)) $$ "and" $+$ - nest 4 (ppJudgement Qualified (c,j))) + nest 4 (ppJudgement Qualified (c,j)) $+$ + msg) Nothing -> go (Map.insert c j map) is extendModule :: FilePath -> SourceGrammar -> SourceModule -> Check SourceModule @@ -203,7 +204,7 @@ unifyAnyInfo m i j = case (i,j) of liftM2 ResParam (unifyMaybeL mt1 mt2) (unifyMaybe mv1 mv2) (ResValue (L l1 t1), ResValue (L l2 t2)) | t1==t2 -> return (ResValue (L l1 t1)) - | otherwise -> fail "" + | otherwise -> fail "non-matching ResValue" (_, ResOverload ms t) | elem m ms -> return $ ResOverload ms t (ResOper mt1 m1, ResOper mt2 m2) -> @@ -222,7 +223,7 @@ unifyAnyInfo m i j = case (i,j) of _ -> fail "informations" -- | this is what happens when matching two values in the same module -unifyMaybeL :: Eq a => Maybe (L a) -> Maybe (L a) -> Err (Maybe (L a)) +unifyMaybeL :: (Eq a, Show a) => Maybe (L a) -> Maybe (L a) -> Err (Maybe (L a)) unifyMaybeL = unifyMaybeBy unLoc unifAbsArrity :: Maybe Int -> Maybe Int -> Err (Maybe Int) @@ -230,5 +231,12 @@ unifAbsArrity = unifyMaybe unifAbsDefs :: Maybe [L Equation] -> Maybe [L Equation] -> Err (Maybe [L Equation]) unifAbsDefs (Just xs) (Just ys) = return (Just (xs ++ ys)) +-- unifAbsDefs Nothing ys = return ys +-- unifAbsDefs xs Nothing = return xs unifAbsDefs Nothing Nothing = return Nothing -unifAbsDefs _ _ = fail "" +unifAbsDefs Nothing (Just ys) = fail $ "Can't unify Nothing with def " ++ render (pp ys) +unifAbsDefs xs Nothing = fail $ "Can't unify def " ++ show xs ++ " with Nothing" +-- Cannot use def with data. Hint: replace data with fun for $name + +instance (Pretty a, Pretty b) => Pretty (a,b) where + pp (a,b) = "(" <+> pp a <+> ", " <+> pp b <+> ")" diff --git a/src/compiler/GF/CompileInParallel.hs b/src/compiler/GF/CompileInParallel.hs index ed498a6903..987c4a9c1d 100644 --- a/src/compiler/GF/CompileInParallel.hs +++ b/src/compiler/GF/CompileInParallel.hs @@ -61,7 +61,7 @@ parallelBatchCompile jobs opts rootfiles0 = usesPresent (_,paths) = take 1 libs==["present"] where - libs = [p|path<-paths, + libs = [p | path<-paths, let (d,p0) = splitAt n path p = dropSlash p0, d==lib_dir,p `elem` all_modes] @@ -171,11 +171,11 @@ batchCompile1 lib_dir (opts,filepaths) = <+>length (nub (map (dropFileName.fst) ds))<+>"directories." let n = length es if n>0 - then fail $ "Errors prevented "++show n++" module"++['s'|n/=1]++ + then fail $ "Errors prevented "++show n++" module"++['s' | n/=1] ++ " from being compiled." else return (maximum ts,(cnc,gr)) -splitEither es = ([x|Left x<-es],[y|Right y<-es]) +splitEither es = ([x | Left x<-es],[y | Right y<-es]) canonical path = liftIO $ D.canonicalizePath path `catch` const (return path) diff --git a/src/compiler/GF/Data/Operations.hs b/src/compiler/GF/Data/Operations.hs index e9b95f8abb..05ca6e9f6b 100644 --- a/src/compiler/GF/Data/Operations.hs +++ b/src/compiler/GF/Data/Operations.hs @@ -24,7 +24,7 @@ module GF.Data.Operations ( liftErr, -- ** Checking - checkUnique, unifyMaybeBy, unifyMaybe, + checkUnique, unifyMaybeBy, unifyMaybe, unifyMaybeWith, -- ** Monadic operations on lists and pairs mapPairsM, pairM, @@ -89,16 +89,21 @@ checkUnique ss = ["overloaded" +++ show s | s <- nub overloads] where overloaded s = length (filter (==s) ss) > 1 -- | this is what happens when matching two values in the same module -unifyMaybe :: (Eq a, Fail.MonadFail m) => Maybe a -> Maybe a -> m (Maybe a) +unifyMaybe :: (Eq a, Fail.MonadFail m, Show a) => Maybe a -> Maybe a -> m (Maybe a) unifyMaybe = unifyMaybeBy id -unifyMaybeBy :: (Eq b, Fail.MonadFail m) => (a->b) -> Maybe a -> Maybe a -> m (Maybe a) +unifyMaybeBy :: (Eq b, Fail.MonadFail m, Show a) => (a->b) -> Maybe a -> Maybe a -> m (Maybe a) unifyMaybeBy f (Just p1) (Just p2) | f p1==f p2 = return (Just p1) - | otherwise = fail "" + | otherwise = fail $ "non-matching values: " ++ show p1 ++ " and " ++ show p2 unifyMaybeBy _ Nothing mp2 = return mp2 unifyMaybeBy _ mp1 _ = return mp1 +unifyMaybeWith :: Applicative m => (a -> a -> m a) -> Maybe a -> Maybe a -> m (Maybe a) +unifyMaybeWith f (Just p1) (Just p2) = Just <$> f p1 p2 +unifyMaybeWith _ Nothing mp2 = pure mp2 +unifyMaybeWith _ mp1 _ = pure mp1 + -- printing indent :: Int -> String -> String diff --git a/src/compiler/GF/Grammar/Printer.hs b/src/compiler/GF/Grammar/Printer.hs index 74fd511b78..b587dcd8df 100644 --- a/src/compiler/GF/Grammar/Printer.hs +++ b/src/compiler/GF/Grammar/Printer.hs @@ -17,6 +17,7 @@ module GF.Grammar.Printer , ppTerm , ppPatt , ppValue + , ppNValue , ppConstrs , ppQIdent , ppMeta @@ -276,16 +277,19 @@ ppPatt q d (PTilde t) = prec d 2 ('~' <> ppTerm q 6 t) ppValue :: TermPrintQual -> Int -> Val -> Doc ppValue q d (VGen i x) = x <> "{-" <> i <> "-}" ---- latter part for debugging -ppValue q d (VApp u v) = prec d 4 (ppValue q 4 u <+> ppValue q 5 v) -ppValue q d (VCn (_,c)) = pp c +ppValue q d (VApp u v) = prec d 4 (ppValue q 4 u <+> hsep (ppValue q 5 <$> v)) +ppValue q d (VCn (_,c) _) = pp c ppValue q d (VClos env e) = case e of Meta _ -> ppTerm q d e <> ppEnv env _ -> ppTerm q d e ---- ++ prEnv env ---- for debugging ppValue q d (VRecType xs) = braces (hsep (punctuate ',' [l <> '=' <> ppValue q 0 v | (l,v) <- xs])) ppValue q d VType = pp "Type" +ppNValue :: TermPrintQual -> Int -> NotVal -> Doc +ppNValue q d (NVClos env e) = ppValue q d (VClos env e) + ppConstrs :: Constraints -> [Doc] -ppConstrs = map (\(v,w) -> braces (ppValue Unqualified 0 v <+> "<>" <+> ppValue Unqualified 0 w)) +ppConstrs = map $ \(v,w) -> braces (ppValue Unqualified 0 v <+> "<>" <+> ppValue Unqualified 0 w) ppEnv :: Env -> Doc ppEnv e = hcat (map (\(x,t) -> braces (x <> ":=" <> ppValue Unqualified 0 t)) e) diff --git a/src/compiler/GF/Grammar/Unify.hs b/src/compiler/GF/Grammar/Unify.hs index 3a7f0edef4..b17e84de67 100644 --- a/src/compiler/GF/Grammar/Unify.hs +++ b/src/compiler/GF/Grammar/Unify.hs @@ -108,8 +108,8 @@ occCheck s u = case u of val2term :: Val -> Term val2term v = case v of VClos g e -> substTerm [] (map (\(x,v) -> (x,val2term v)) g) e - VApp f c -> App (val2term f) (val2term c) - VCn c -> Q c + VApp f cs -> foldl App (val2term f) (map val2term cs) + VCn c _ -> Q c VGen i x -> Vr x VRecType xs -> RecType (map (\(l,v) -> (l,val2term v)) xs) VType -> typeType diff --git a/src/compiler/GF/Grammar/Values.hs b/src/compiler/GF/Grammar/Values.hs index c8fcb3945f..fae0c017b4 100644 --- a/src/compiler/GF/Grammar/Values.hs +++ b/src/compiler/GF/Grammar/Values.hs @@ -14,7 +14,7 @@ module GF.Grammar.Values ( -- ** Values used in TC type checking - Val(..), Env, + Val(..), NotVal(..), Env, -- ** Annotated tree used in editing Binds, Constraints, MetaSubst, -- ** For TC @@ -29,9 +29,12 @@ import GF.Grammar.Predef -- values used in TC type checking -data Val = VGen Int Ident | VApp Val Val | VCn QIdent | VRecType [(Label,Val)] | VType | VClos Env Term +data Val = VGen Int Ident | VApp Val [Val] | VCn QIdent (Maybe (Int, [Equation])) | VRecType [(Label,Val)] | VType | VClos Env Term deriving (Eq,Show) +data NotVal = NVClos Env Term | NVVal Val + deriving (Show) + type Env = [(Ident,Val)] type Binds = [(Ident,Val)] @@ -42,13 +45,13 @@ type MetaSubst = [(MetaId,Val)] -- for TC valAbsInt :: Val -valAbsInt = VCn (cPredefAbs, cInt) +valAbsInt = VCn (cPredefAbs, cInt) Nothing valAbsFloat :: Val -valAbsFloat = VCn (cPredefAbs, cFloat) +valAbsFloat = VCn (cPredefAbs, cFloat) Nothing valAbsString :: Val -valAbsString = VCn (cPredefAbs, cString) +valAbsString = VCn (cPredefAbs, cString) Nothing vType :: Val vType = VType diff --git a/src/compiler/GF/Infra/Ident.hs b/src/compiler/GF/Infra/Ident.hs index ad47d91cdc..143503d8d3 100644 --- a/src/compiler/GF/Infra/Ident.hs +++ b/src/compiler/GF/Infra/Ident.hs @@ -61,7 +61,10 @@ data Ident = -- (It is also possible to use regular Haskell 'String's, with somewhat -- reduced performance and increased memory use.) newtype RawIdent = Id { rawId2utf8 :: UTF8.ByteString } - deriving (Eq, Ord, Show, Read) + deriving (Eq, Ord, Read) + +instance Show RawIdent where + showsPrec d (Id s) = showParen (d >= 11) $ showString "Id " . showsPrec 11 s pack = UTF8.fromString unpack = UTF8.toString