avoid using withState

This commit is contained in:
Krasimir Angelov
2025-05-28 14:20:16 +00:00
parent 52eb5899d4
commit 2c427b69fe
2 changed files with 14 additions and 30 deletions
@@ -4,7 +4,7 @@ module GF.Compile.Compute.Concrete2
(Env, Scope, Value(..), Variants(..), Constraint, OptionInfo(..), ChoiceMap, cleanOptions, (Env, Scope, Value(..), Variants(..), Constraint, OptionInfo(..), ChoiceMap, cleanOptions,
ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM, ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM,
mapVariants, unvariants, variants2consts, consts2variants, mapVariants, unvariants, variants2consts, consts2variants,
runEvalM, runEvalMWithOpts, stdPredef, globals, withState, runEvalM, runEvalMWithOpts, stdPredef, globals,
PredefImpl, Predef(..), ($\), PredefImpl, Predef(..), ($\),
pdCanonicalArgs, pdArity, pdCanonicalArgs, pdArity,
normalForm, normalFlatForm, normalForm, normalFlatForm,
@@ -729,9 +729,6 @@ runEvalMWithOpts g cs (EvalM f) = Check $ \(es,ws) ->
where where
init = State cs Map.empty [] init = State cs Map.empty []
withState :: State -> EvalM a -> EvalM a
withState state (EvalM f) = EvalM $ \g k _ r ws -> f g k state r ws
reset :: EvalM a -> EvalM [a] reset :: EvalM a -> EvalM [a]
reset (EvalM f) = EvalM $ \g k state r ws -> reset (EvalM f) = EvalM $ \g k state r ws ->
case f g (\x state xs ws -> Success (x:xs) ws) state [] ws of case f g (\x state xs ws -> Success (x:xs) ws) state [] ws of
@@ -769,7 +766,7 @@ variants' c f xs = EvalM (\g k state@(State choices metas opts) r msgs ->
Fail msg msgs -> Fail msg msgs Fail msg msgs -> Fail msg msgs
Success ts msgs -> backtrack g (j+1) xs choices metas opts ts msgs Success ts msgs -> backtrack g (j+1) xs choices metas opts ts msgs
try :: (a -> EvalM b) -> ([(b,State)] -> EvalM b) -> [a] -> EvalM b try :: (a -> EvalM b) -> ([b] -> EvalM b) -> [a] -> EvalM b
try f select xs = EvalM (\g k state r msgs -> try f select xs = EvalM (\g k state r msgs ->
let (res,msgs') = backtrack g xs state [] msgs let (res,msgs') = backtrack g xs state [] msgs
in case select res of in case select res of
@@ -778,7 +775,7 @@ try f select xs = EvalM (\g k state r msgs ->
backtrack g [] state res msgs = (res,msgs) backtrack g [] state res msgs = (res,msgs)
backtrack g (x:xs) state res msgs = backtrack g (x:xs) state res msgs =
case f x of case f x of
EvalM f -> case f g (\x state res msgs -> Success ((x,state):res) msgs) state res msgs of EvalM f -> case f g (\y state ys msgs -> Success (y:ys) msgs) state res msgs of
Fail msg _ -> backtrack g xs state res msgs Fail msg _ -> backtrack g xs state res msgs
Success res msgs -> backtrack g xs state res msgs Success res msgs -> backtrack g xs state res msgs
@@ -518,45 +518,32 @@ resolveOverloads scope c t0 q args mb_ty = do
minimum g [] = (maxBound,err) minimum g [] = (maxBound,err)
where where
err = evalError (pp "Overload resolution failed") err = evalError (pp "Overload resolution failed")
minimum g (tty@((t,ty),state):ttys) = minimum g (tty@(t,ty):ttys) =
let ty' = zonk ty let a = arity ty
a = arity ty'
(a',res) = minimum g ttys (a',res) = minimum g ttys
in case compare a a' of in case compare a a' of
GT -> (a',res) GT -> (a',res)
EQ -> (a',join t ty' state res) EQ -> (a',join t ty res)
LT -> (a ,one t ty' state) LT -> (a ,one t ty)
where where
arity :: Value -> Int arity :: Value -> Int
arity (VProd _ _ _ ty) = 1 + arity ty arity (VProd _ _ _ ty) = 1 + arity ty
arity _ = 0 arity _ = 0
zonk :: Value -> Value one t ty = do
zonk (VProd bt x ty1 ty2) = VProd bt x (zonk ty1) (zonk ty2)
zonk (VMeta i vs) =
case Map.lookup i (metaVars state) of
Just (Bound _ v) -> zonk (apply g v vs)
Just (Residuation _ (Just v)) -> zonk (apply g v vs)
_ -> VMeta i (map zonk vs)
zonk (VSusp i k vs) =
case Map.lookup i (metaVars state) of
Just (Bound _ v) -> zonk (apply g (k v) vs)
Just (Residuation _ (Just v)) -> zonk (apply g (k v) vs)
_ -> VSusp i k (map zonk vs)
zonk v = v
one t ty state = do
t <- withState state (zonkTerm [] t)
return ([t],ty) return ([t],ty)
join t ty state res = do join t ty res = do
t <- withState state (zonkTerm [] t)
(ts,ty') <- res (ts,ty') <- res
unify scope ty ty' unify scope ty ty'
return (t:ts,ty) return (t:ts,ty)
reapply2 :: Scope -> Choice -> Term -> Value -> [(Term,Value,Value)] -> Maybe Rho -> EvalM (Term,Rho) reapply2 :: Scope -> Choice -> Term -> Value -> [(Term,Value,Value)] -> Maybe Rho -> EvalM (Term,Rho)
reapply2 scope c fun fun_ty [] mb_ty = instSigma scope c fun fun_ty mb_ty reapply2 scope c fun fun_ty [] mb_ty = do
(t,ty) <- instSigma scope c fun fun_ty mb_ty
t <- zonkTerm (scopeVars scope) t
ty <- zonkValue ty
return (t,ty)
reapply2 scope c fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Implicit arg case reapply2 scope c fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Implicit arg case
(bt, x, arg_ty', res_ty) <- unifyFun scope fun_ty (bt, x, arg_ty', res_ty) <- unifyFun scope fun_ty
unless (bt == Implicit) $ unless (bt == Implicit) $