forked from GitHub/gf-core
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.
This commit is contained in:
@@ -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<length xs = Right (Vr (reverse xs !! j))
|
||||
| otherwise = Left j
|
||||
| j<length xs = Vr (reverse xs !! j)
|
||||
| otherwise = error ("variable #"++show j++" is out of scope")
|
||||
|
||||
|
||||
pushs xs e = foldr push e xs
|
||||
push x (env,xs) = ((x,gen xs):env,x:xs)
|
||||
gen xs = VGen (length xs) []
|
||||
|
||||
nfcase (p,f) = liftM ((,) p) (v2txs xs' (bind f env'))
|
||||
nfcase (p,f) = (,) p (v2txs xs' (bind f env'))
|
||||
where (env',xs') = pushs (pattVars p) ([],xs)
|
||||
|
||||
bind (Bind f) x = if stop
|
||||
|
||||
Reference in New Issue
Block a user