From bd270b05ff92b15c15d5dfebd52576d0e15d0b04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= Date: Sun, 29 Nov 2020 14:51:55 +0100 Subject: [PATCH 1/4] Remove the `Either Int` from value2term This prevents HUGE space leak and makes compiling a PGF a LOT faster For example, an application grammar moved from taking over 50GB of ram and taking 5 minutes (most of which is spent on garbage colelction) to taking 1.2 seconds and using 42mb of memory The price we pay is that the "variable #n is out of scope" error is now lazy and will happen when we try to evaluate the term instead of happening when the function returns and allowing the caller to chose how to handle the error. I don't think this should matter in practice, since it's very rare; at least Inari has never encountered it. --- src/compiler/GF/Compile/Compute/Concrete.hs | 66 +++++++++++---------- 1 file changed, 34 insertions(+), 32 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index 4b54c8c84..a346de882 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -493,57 +493,59 @@ vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res pf (_,v) = ppV v pa (_,v) = ppV v ppV v = case value2term' True loc [] v of - Left i -> "variable #" <> pp i <+> "is out of scope" - Right t -> ppTerm Unqualified 10 t + -- Left i -> "variable #" <> pp i <+> "is out of scope" + t -> ppTerm Unqualified 10 t -- | Convert a value back to a term value2term :: GLocation -> [Ident] -> Value -> Either Int Term -value2term = value2term' False +value2term loc xs v0 = Right $ value2term' False loc xs v0 + +value2term' :: Bool -> p -> [Ident] -> Value -> Term value2term' stop loc xs v0 = case v0 of - VApp pre vs -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs) - VCApp f vs -> liftM (foldl App (QC f)) (mapM v2t vs) - VGen j vs -> liftM2 (foldl App) (var j) (mapM v2t vs) - VMeta j env vs -> liftM (foldl App (Meta j)) (mapM v2t vs) - VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f) - VAbs bt x f -> liftM (Abs bt x) (v2t' x f) - VInt n -> return (EInt n) - VFloat f -> return (EFloat f) - VString s -> return (if null s then Empty else K s) - VSort s -> return (Sort s) - VImplArg v -> liftM ImplArg (v2t v) - VTblType p res -> liftM2 Table (v2t p) (v2t res) - VRecType rs -> liftM RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs) - VRec as -> liftM R (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as) - VV t _ vs -> liftM (V t) (mapM v2t vs) - VT wild v cs -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs) - VFV vs -> liftM FV (mapM v2t vs) - VC v1 v2 -> liftM2 C (v2t v1) (v2t v2) - VS v1 v2 -> liftM2 S (v2t v1) (v2t v2) - VP v l -> v2t v >>= \t -> return (P t l) - VPatt p -> return (EPatt p) - VPattType v -> v2t v >>= return . EPattType - VAlts v vvs -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs) - VStrs vs -> liftM Strs (mapM v2t vs) + VApp pre vs -> applyMany (Q (cPredef,predefName pre)) vs + VCApp f vs -> applyMany (QC f) vs + VGen j vs -> applyMany (var j) vs + VMeta j env vs -> applyMany (Meta j) vs + VProd bt v x f -> Prod bt x (v2t v) (v2t' x f) + VAbs bt x f -> Abs bt x (v2t' x f) + VInt n -> EInt n + VFloat f -> EFloat f + VString s -> if null s then Empty else K s + VSort s -> Sort s + VImplArg v -> ImplArg (v2t v) + VTblType p res -> Table (v2t p) (v2t res) + VRecType rs -> RecType [(l, v2t v) | (l,v) <- rs] + VRec as -> R [(l, (Nothing, v2t v)) | (l,v) <- as] + VV t _ vs -> V t (map v2t vs) + VT wild v cs -> T ((if wild then TWild else TTyped) (v2t v)) (map nfcase cs) + VFV vs -> FV (map v2t vs) + VC v1 v2 -> C (v2t v1) (v2t v2) + VS v1 v2 -> S (v2t v1) (v2t v2) + VP v l -> P (v2t v) l + VPatt p -> EPatt p + VPattType v -> EPattType $ v2t v + VAlts v vvs -> Alts (v2t v) [(v2t x, v2t y) | (x,y) <- vvs] + VStrs vs -> Strs (map v2t vs) -- VGlue v1 v2 -> Glue (v2t v1) (v2t v2) -- VExtR v1 v2 -> ExtR (v2t v1) (v2t v2) - VError err -> return (Error err) - + VError err -> Error err where + applyMany f vs = foldl App f (map v2t vs) v2t = v2txs xs v2txs = value2term' stop loc v2t' x f = v2txs (x:xs) (bind f (gen xs)) var j - | j Date: Sun, 29 Nov 2020 15:03:08 +0100 Subject: [PATCH 2/4] Remove last traces of the Either in value2term --- src/compiler/GF/Compile/Compute/Concrete.hs | 21 ++++++++++--------- .../GF/Compile/TypeCheck/ConcreteNew.hs | 10 ++++----- 2 files changed, 16 insertions(+), 15 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index a346de882..dd2180937 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -30,11 +30,12 @@ import Debug.Trace(trace) normalForm :: GlobalEnv -> L Ident -> Term -> Term normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc) +nfx :: GlobalEnv -> Term -> Err Term nfx env@(GE _ _ _ loc) t = do v <- eval env [] t case value2term loc [] v of - Left i -> fail ("variable #"++show i++" is out of scope") - Right t -> return t + -- Left i -> fail ("variable #"++show i++" is out of scope") + t -> return t eval :: GlobalEnv -> Env -> Term -> Err Value eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t @@ -289,8 +290,8 @@ glue env (v1,v2) = glu v1 v2 then VC v1 (VC (VApp BIND []) v2) else let loc = gloc env vt v = case value2term loc (local env) v of - Left i -> Error ('#':show i) - Right t -> t + -- Left i -> Error ('#':show i) + t -> t originalMsg = render $ ppL loc (hang "unsupported token gluing" 4 (Glue (vt v1) (vt v2))) term = render $ pp $ Glue (vt v1) (vt v2) @@ -356,8 +357,8 @@ select env vv = match loc cs v = case value2term loc [] v of - Left i -> bad ("variable #"++show i++" is out of scope") - Right t -> err bad return (matchPattern cs t) + -- Left i -> bad ("variable #"++show i++" is out of scope") + t -> err bad return (matchPattern cs t) where bad = fail . ("In pattern matching: "++) @@ -384,8 +385,8 @@ valueTable env i cs = convertv cs' vty = case value2term (gloc env) [] vty of - Left i -> fail ("variable #"++show i++" is out of scope") - Right pty -> convert' cs' =<< paramValues'' env pty + -- Left i -> fail ("variable #"++show i++" is out of scope") + pty -> convert' cs' =<< paramValues'' env pty convert cs' ty = convert' cs' =<< paramValues' env ty @@ -497,8 +498,8 @@ vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res t -> ppTerm Unqualified 10 t -- | Convert a value back to a term -value2term :: GLocation -> [Ident] -> Value -> Either Int Term -value2term loc xs v0 = Right $ value2term' False loc xs v0 +value2term :: GLocation -> [Ident] -> Value -> Term +value2term = value2term' False value2term' :: Bool -> p -> [Ident] -> Value -> Term value2term' stop loc xs v0 = diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index d85af5361..628f7ea4c 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -568,9 +568,9 @@ unifyVar ge scope i env vs ty2 = do -- Check whether i is bound Bound ty1 -> do v <- liftErr (eval ge env ty1) unify ge scope (vapply (geLoc ge) v vs) ty2 Unbound scope' _ -> case value2term (geLoc ge) (scopeVars scope') ty2 of - Left i -> let (v,_) = reverse scope !! i - in tcError ("Variable" <+> pp v <+> "has escaped") - Right ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)] + -- Left i -> let (v,_) = reverse scope !! i + -- in tcError ("Variable" <+> pp v <+> "has escaped") + ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)] if i `elem` ms2 then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$ nest 2 (ppTerm Unqualified 0 ty2')) @@ -766,8 +766,8 @@ zonkTerm t = composOp zonkTerm t tc_value2term loc xs v = case value2term loc xs v of - Left i -> tcError ("Variable #" <+> pp i <+> "has escaped") - Right t -> return t + -- Left i -> tcError ("Variable #" <+> pp i <+> "has escaped") + t -> return t From c2ffa6763bb36956f9b353c2d2cd6711ab0796f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= Date: Sun, 29 Nov 2020 21:36:11 +0100 Subject: [PATCH 3/4] Github actions: Fix build for stack --- .github/workflows/build-all-versions.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build-all-versions.yml b/.github/workflows/build-all-versions.yml index fca637189..f4ba6a2f1 100644 --- a/.github/workflows/build-all-versions.yml +++ b/.github/workflows/build-all-versions.yml @@ -14,7 +14,7 @@ jobs: strategy: matrix: os: [ubuntu-latest, macos-latest, windows-latest] - cabal: ["3.2"] + cabal: ["latest"] ghc: - "8.6.5" - "8.8.3" @@ -65,7 +65,7 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - stack: ["2.3.3"] + stack: ["latest"] ghc: ["7.10.3","8.0.2", "8.2.2", "8.4.4", "8.6.5", "8.8.4"] # ghc: ["8.8.3"] From 7faf8c9dad5a88c38f7fa3633f8a1b286ac570c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andreas=20K=C3=A4llberg?= Date: Mon, 12 Jul 2021 16:38:29 +0800 Subject: [PATCH 4/4] Clean up redundant case expressions --- src/compiler/GF/Compile/Compute/Concrete.hs | 21 +++++++++---------- .../GF/Compile/TypeCheck/ConcreteNew.hs | 4 ++-- 2 files changed, 12 insertions(+), 13 deletions(-) diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs index dd2180937..47e2f5cde 100644 --- a/src/compiler/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/GF/Compile/Compute/Concrete.hs @@ -33,9 +33,9 @@ normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc) nfx :: GlobalEnv -> Term -> Err Term nfx env@(GE _ _ _ loc) t = do v <- eval env [] t - case value2term loc [] v of + return (value2term loc [] v) + -- Old value2term error message: -- Left i -> fail ("variable #"++show i++" is out of scope") - t -> return t eval :: GlobalEnv -> Env -> Term -> Err Value eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t @@ -289,9 +289,9 @@ glue env (v1,v2) = glu v1 v2 (v1,v2) -> if flag optPlusAsBind (opts env) then VC v1 (VC (VApp BIND []) v2) else let loc = gloc env - vt v = case value2term loc (local env) v of + vt v = value2term loc (local env) v + -- Old value2term error message: -- Left i -> Error ('#':show i) - t -> t originalMsg = render $ ppL loc (hang "unsupported token gluing" 4 (Glue (vt v1) (vt v2))) term = render $ pp $ Glue (vt v1) (vt v2) @@ -356,9 +356,9 @@ select env vv = (v1,v2) -> ok2 VS v1 v2 match loc cs v = - case value2term loc [] v of + err bad return (matchPattern cs (value2term loc [] v)) + -- Old value2term error message: -- Left i -> bad ("variable #"++show i++" is out of scope") - t -> err bad return (matchPattern cs t) where bad = fail . ("In pattern matching: "++) @@ -384,9 +384,8 @@ valueTable env i cs = wild = case i of TWild _ -> True; _ -> False convertv cs' vty = - case value2term (gloc env) [] vty of - -- Left i -> fail ("variable #"++show i++" is out of scope") - pty -> convert' cs' =<< paramValues'' env pty + convert' cs' =<< paramValues'' env (value2term (gloc env) [] vty) + -- Old value2term error message: Left i -> fail ("variable #"++show i++" is out of scope") convert cs' ty = convert' cs' =<< paramValues' env ty @@ -493,9 +492,9 @@ vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res pf (_,VString n) = pp n pf (_,v) = ppV v pa (_,v) = ppV v - ppV v = case value2term' True loc [] v of + ppV v = ppTerm Unqualified 10 (value2term' True loc [] v) + -- Old value2term error message: -- Left i -> "variable #" <> pp i <+> "is out of scope" - t -> ppTerm Unqualified 10 t -- | Convert a value back to a term value2term :: GLocation -> [Ident] -> Value -> Term diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index 628f7ea4c..ed3a20ce0 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -765,9 +765,9 @@ zonkTerm (Meta i) = do zonkTerm t = composOp zonkTerm t tc_value2term loc xs v = - case value2term loc xs v of + return $ value2term loc xs v + -- Old value2term error message: -- Left i -> tcError ("Variable #" <+> pp i <+> "has escaped") - t -> return t