diff --git a/frege/compiler/Typecheck.fr b/frege/compiler/Typecheck.fr index 14ae151e..2de67329 100644 --- a/frege/compiler/Typecheck.fr +++ b/frege/compiler/Typecheck.fr @@ -99,6 +99,7 @@ import Compiler.common.Errors as E() import Compiler.common.Types as TH import Compiler.common.Resolve as R(weUse) import Compiler.common.SymbolTable +import Compiler.common.Binders(avoidBinders) import Compiler.classes.Nice @@ -266,7 +267,8 @@ checkgroup nms = do checkgroup7 nms = do g <- getST E.logmsg TRACEZ Position.null (text ("typechecking group: " ++ joined " " (map (flip QName.nice g) nms))) - syms <- mapSt findV nms + unless (null g.typEnv) do + mapSt findV nms >>= mapM_ renameSigma -- we set up typEnv with the names of the group members so that 'envTvs' will find them changeST Global.{typEnv <- (nms ++)} @@ -510,10 +512,27 @@ substInst (lit@Lit{pos, kind, value, typ=Just (ForAll [] rho)}) not (null rho.context) = pure (Right lit.{typ=Just (ForAll [] rho.{context=[]})}) substInst x = stio (Left x) +renameSigma ∷ Symbol -> StG () +renameSigma sym | sym.name.isLocal && sym.anno = do + g ← getST + outer ← mapSt findV g.typEnv + let avoid = \c → c `elem` concatMap (Sigma.vars . Symbol.typ) outer + || (any (null . Sigma.vars . Symbol.typ) outer && avoidBinders g c) + newsym = sym.{typ ← avoidSigma avoid } + when (sym.typ.vars != newsym.typ.vars) do + E.warn sym.pos (text "Renamed annotation " + <+> text (sym.typ.nicer g) + text "to " <+> text (newsym.typ.nicer g) + text "because of (potential) type variable name conflict") + changeSym newsym + pure () +renameSigma other = pure () + checkName nm = do g <- getST sym <- findV nm + -- sym <- if nm.isLocal && sym.anno then renameSigma sym else pure sym E.logmsg TRACEZ sym.pos (text ("checkName: " ++ sym.name.nice g ++ " :: " ++ sym.typ.nice g)) -- E.logmsg TRACET sym.pos (text ("checkName: " ++ sym.name.nice g ++ " :: " ++ sym.typ.nice g)) sigma <- checkSym sym diff --git a/frege/compiler/common/Binders.fr b/frege/compiler/common/Binders.fr index 59e1a59b..5ac65e38 100644 --- a/frege/compiler/common/Binders.fr +++ b/frege/compiler/common/Binders.fr @@ -46,4 +46,9 @@ allBinders g | otherwise = allAsciiBinders where flags = (Global.options g).flags - +--- a function that tells if a 'String' is member of the current binders +avoidBinders g + | isOn flags USEFRAKTUR = ( ~ '^[𝖆𝖇𝖈𝖉𝖊𝖋𝖌𝖍𝖎𝖏𝖐𝖑𝖒𝖓𝖔𝖕𝖖𝖗𝖘𝖙𝖚𝖛𝖜𝖝𝖞𝖟]+$') + | isOn flags USEGREEK = ( ~ '^[αβγδεζηθικλμνξοπρςστυφχψω]$') + | otherwise = ( ~ '^[a-z]$') + where flags = (Global.options g).flags diff --git a/frege/compiler/common/Types.fr b/frege/compiler/common/Types.fr index a36c1ae9..d5d73104 100644 --- a/frege/compiler/common/Types.fr +++ b/frege/compiler/common/Types.fr @@ -3,7 +3,7 @@ module frege.compiler.common.Types inline (isFun) where -import Data.TreeMap as Map(member, keys, insert, TreeSet, TreeMap) +import Data.TreeMap as Map(member, keys, insert, lookup, TreeSet, TreeMap) import frege.compiler.types.Types as T import Compiler.types.Global as G @@ -246,10 +246,10 @@ rhoKind RhoTau{tau} = tauKind tau 2) a 'Regex' that describes potential duplicates. If the outer 'Sigma' is indeed annotated, this can be a 'Regex' that would never match any type variable name. Otherwise, it should match every element of the supply that is currently in use. - + Of course, we simply encode this with a property function that tells us whether a certain variable must be avoided and needs replacement. - + Because the renamings of user supplied 'Sigma's can lead to hard to understand error messages, there should be a warning when the 'Sigma' was actually alpha-converted. -} @@ -257,23 +257,38 @@ rhoKind RhoTau{tau} = tauKind tau avoidSigma avoid (ForAll tvs rho) = ForAll ntvs (avoidRho (\c -> avoid c || c `elem` new) rho') where old = map _.var tvs -- old variables - binders = [ bn | b ← Binders.allAsciiBinders, - n ← [1..9], + binders = [ bn | n ← [1..3], + b ← Binders.allAsciiBinders, let {bn = b ++ show n}, not (avoid bn), bn `notElem` old -- safe new variable names - ] + ] bads = filter avoid old -- the variables that need replacement reps = Map.fromList (zip bads binders) -- a substitution for variable names - rnvar v tv = tv.{var=v, -- rename a variable - kind ← substKind (Map.singleton tv.var tv')} - where tv' = tv.{var=v, kind=KType} - new = undefined - avoidRho = undefined - rho' = rho - ntvs = tvs --- rho' = substRho rep rho --- rep = fromList [ (tv.var, rename outer tv) | tv ← tvs, tv.var `elem` outer, + mapped = Map.values reps -- names of renamed variables + ntvs = map (rnTVar reps) tvs -- rename affected type variables + new = map _.var ntvs -- the variable names of the new Sigma + subst = Map.fromList (zip bads [ tv | tv ← ntvs, tv.var `elem` mapped ]) + rho' = substRho subst rho + +avoidRho :: (String → Bool) -> Rho -> Rho +avoidRho avoid (rhofun@RhoFun{}) = rhofun.{sigma ← avoidSigma avoid, rho ← avoidRho avoid} +avoidRho avoid (rhotau@RhoTau{}) = rhotau + +rnTVar :: TreeMap String String → Tau → Tau +rnTVar tree (TApp a b) = TApp (rnTVar tree a) (rnTVar tree b) +rnTVar tree (t@TCon{}) = t +rnTVar tree (t@TVar{}) = case lookup t.var tree of + Just v → t.{kind ← rnKind tree, var=v} + Nothing → t +rnTVar tree (t@TSig _) = t +rnTVar tree (t@Meta _) = t + +rnKind :: TreeMap String String → Kind → Kind +rnKind tree (KGen t) = KGen (rnTVar tree t) +rnKind tree (KApp k1 k2) = KApp (rnKind tree k1) (rnKind tree k2) +rnKind tree k = k + {-- > sigInst subst sigma