From 188b77b083ca895d2fd589bfd23b8fc199e1808b Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Fri, 2 May 2025 13:52:17 +0200 Subject: [PATCH] improvement on the typechecker --- .../api/GF/Compile/Compute/Concrete2.hs | 22 ++++----- .../api/GF/Compile/TypeCheck/ConcreteNew.hs | 45 ++++++++++++++++++- 2 files changed, 52 insertions(+), 15 deletions(-) diff --git a/src/compiler/api/GF/Compile/Compute/Concrete2.hs b/src/compiler/api/GF/Compile/Compute/Concrete2.hs index 8afe8b92e..26ff0a277 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete2.hs +++ b/src/compiler/api/GF/Compile/Compute/Concrete2.hs @@ -4,11 +4,11 @@ module GF.Compile.Compute.Concrete2 (Env, Scope, Value(..), Variants(..), Constraint, OptionInfo(..), ChoiceMap, cleanOptions, ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM, mapVariants, unvariants, variants2consts, consts2variants, - runEvalM, runEvalMWithOpts, stdPredef, globals, + runEvalM, runEvalMWithOpts, stdPredef, globals, withState, PredefImpl, Predef(..), ($\), pdCanonicalArgs, pdArity, normalForm, normalFlatForm, - eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect, + eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect, State(..), newResiduation, getMeta, setMeta, MetaState(..), variants, try, evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4, mapC, mapCM) where @@ -727,6 +727,9 @@ runEvalMWithOpts g cs (EvalM f) = Check $ \(es,ws) -> where 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 f) = EvalM $ \g k state r ws -> case f g (\x state xs ws -> Success (x:xs) ws) state [] ws of @@ -764,12 +767,11 @@ variants' c f xs = EvalM (\g k state@(State choices metas opts) r msgs -> Fail msg msgs -> Fail msg msgs Success ts msgs -> backtrack g (j+1) xs choices metas opts ts msgs -try :: (a -> EvalM b) -> [a] -> Message -> EvalM b -try f xs msg = EvalM (\g k state r msgs -> +try :: (a -> EvalM b) -> ([(b,State)] -> EvalM b) -> [a] -> EvalM b +try f select xs = EvalM (\g k state r msgs -> let (res,msgs') = backtrack g xs state [] msgs - in case res of - [] -> Fail msg msgs' - res -> continue g k res r msgs') + in case select res of + EvalM f' -> f' g k state r msgs') where backtrack g [] state res msgs = (res,msgs) backtrack g (x:xs) state res msgs = @@ -778,12 +780,6 @@ try f xs msg = EvalM (\g k state r msgs -> Fail msg _ -> backtrack g xs state res msgs Success res msgs -> backtrack g xs state res msgs - continue g k [] r msgs = Success r msgs - continue g k ((x,state):res) r msgs = - case k x state r msgs of - Fail msg msgs -> Fail msg msgs - Success r msgs -> continue g k res r msgs - newResiduation :: Scope -> EvalM MetaId newResiduation scope = EvalM (\g k (State choices metas opts) r msgs -> let meta_id = Map.size metas+1 diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs index 1194ae4b3..70dbdccb2 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs @@ -470,8 +470,9 @@ resolveOverloads scope c t0 q args mb_ty = do (c2,c3) = split c23 arg_tys <- mapCM (checkArg g) c1 args let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys - try (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty) v_ttys (pp "Overload resolution failed") - + try (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty) + (\ttys -> fmap (\(ts,ty) -> (FV ts,ty)) (snd (minimum g ttys))) + v_ttys where checkArg g c (ImplArg arg) = do let (c1,c2) = split c @@ -484,6 +485,46 @@ resolveOverloads scope c t0 q args mb_ty = do let v = eval g (scopeEnv scope) c2 arg [] return (arg,v,arg_ty) + minimum g [] = (maxBound,err) + where + err = evalError (pp "Overload resolution failed") + minimum g (tty@((t,ty),state):ttys) = + let ty' = zonk ty + a = arity ty' + (a',res) = minimum g ttys + in case compare a a' of + GT -> (a',res) + EQ -> (a',join t ty' state res) + LT -> (a ,one t ty' state) + where + arity :: Value -> Int + arity (VProd _ _ _ ty) = 1 + arity ty + arity _ = 0 + + zonk :: Value -> Value + 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) + + join t ty state res = do + t <- withState state (zonkTerm [] t) + (ts,ty') <- res + unify scope ty ty' + return (t:ts,ty) + 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 ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Implicit arg case