Skip to content

Commit

Permalink
Enhance kind system to deal with bounded generics and bounded wildcards.
Browse files Browse the repository at this point in the history 
This works fine with native definitions, pity is at the moment that
we can't use them yet from Frege code.
  • Loading branch information
@Ingo60
Ingo60 committed Apr 7, 2018
1 parent 8484ea6 commit b518102
Show file tree
Hide file tree
Showing 6 changed files with 144 additions and 50 deletions.
24 changes: 18 additions & 6 deletions frege/compiler/Kinds.fr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,10 @@ import Compiler.types.Global as G

import Compiler.common.Errors as E()
import Compiler.common.SymbolTable
import Compiler.common.Types as T(unifySigma, substSigma)

import Compiler.classes.Nice
import Compiler.instances.Nicer

import Lib.PP(group, break, text, <+>, <>)
import frege.compiler.Utilities as U()
Expand Down Expand Up @@ -243,15 +245,22 @@ type Envs = [TreeMap String Kind]
If kind errors are detected, error messages will be written.
-}
unifyTauKind :: [QName] -> Envs -> Tau -> Kind -> StG (Kind, Envs)
unifyTauKind names env (tvar@TVar{}) exp
| Just _ ← tvar.wildTau, KGen tau ← tvar.kind = unifyTauKind names env tau exp
unifyTauKind names env (TVar{pos,var,kind}) exp = do
g <- getST
E.logmsg TRACEK pos (text ("unifyTauKind: " ++ var
++ " initial " ++ show varkind
++ " expected " ++ show exp))
++ " initial " ++ nicer varkind g
++ " expected " ++ nicer exp g))
case unifyKind varkind exp of
Just (KGen t) → do
let subst = fold (\tm tv -> TreeMap.insert tm tv.var tv.{var,pos,kind=KVar}) empty
(U.freeTVars [] (RhoTau [] t))
t' = T.substTau subst t
pure (KGen t', updenv env var (KGen t'))
Just k -> do
-- let k = unVar kn
E.logmsg TRACEK pos (text ("unifyTauKind: " ++ var ++ " result " ++ show k))
E.logmsg TRACEK pos (text ("unifyTauKind: " ++ var ++ " result " ++ nicer k g))
--if (varkind == KGen && k == KType)
--then return (k, updenv env var varkind)
--else return (k, updenv env var k)
Expand All @@ -263,8 +272,8 @@ unifyTauKind names env (TVar{pos,var,kind}) exp = do
E.error pos (text ("kind error, type variable `"
++ var
++ "` has kind "
++ show varkind
++ ", expected was " ++ show exp))
++ nicer varkind g
++ ", expected was " ++ nicer exp g))
pure (varkind, updenv env var varkind)
where varkind = fromMaybe kind (findenv env var)

Expand Down Expand Up @@ -359,7 +368,10 @@ findenv [] k = Nothing

unifyKind :: Kind -> Kind -> Maybe Kind
unifyKind (a@KGen{}) KType = Just a
unifyKind (a@KGen{}) (b@KGen{}) = if a `keq` b then Just a else Nothing
unifyKind (a@KGen x) (b@KGen y) = if x'.textualEq y then Just a else Nothing
where
subst = T.unifyTau empty x y
x' = T.substTau subst x
unifyKind KType KType = Just KType
unifyKind KType (b@KGen{}) = Just b
unifyKind KVar x = Just x
Expand Down
17 changes: 10 additions & 7 deletions frege/compiler/Utilities.fr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -416,24 +416,27 @@ transSigma sigma = validSigma sigma >>= transSigma1 empty
> transSigma1 outer (ForAll bound rho)
Pre: All type variables free in rho appear either in @outer@ or in @bound@
-}
private transSigma1 ∷ [String] → SigmaS → StG Sigma
private transSigma1 ∷ SigmaEnv QName → SigmaS → StG Sigma
private transSigma1 outer sigma = do
-- sigma <- validSigma1 outer sigma
case sigma of
ForAll bound rho -> do
let inner = map _.var bound
rho <- transRho (outer DL.`union` inner) rho
let free = freeTVars (outer \\ inner) rho
inner ← transBounds sigma.bound
let env = fold (\tm tv → tm.insertS tv.var tv) outer inner
-- unshadowedOuter = fold (\tm tv → tm.delete tv.var) outer inner
rho <- transRho env rho
let -- freeTV = freeTVars (keys unshadowedOuter) rho -- same as inner?
constraints rho = case rho of
RhoTau{} -> (rho.context, rho.{context=[]})
RhoFun{} -> (rho.context ++ subctx, rho.{context=[], rho=subrho})
where (subctx, subrho) = constraints rho.rho
(ctx, rrho) = constraints rho
nrho = rrho.{context=ctx}
case rho of
RhoTau _ _ -> return (ForAll free nrho)
_ -> return (ForAll free (unTau nrho))
RhoTau _ _ -> return (ForAll inner nrho)
_ -> return (ForAll inner (unTau nrho))


{--
Expand All @@ -448,7 +451,7 @@ transCtx (Ctx pos name tau) = do
{--
* check a rho and translate it to 'QName' form
-}
transRho :: [String] -> RhoS -> StG Rho
transRho :: SigmaEnv QName -> RhoS -> StG Rho
transRho outer (RhoFun ctx sig rho) = do
sig <- transSigma1 outer sig
rho <- transRho outer rho
Expand Down
3 changes: 2 additions & 1 deletion frege/compiler/classes/Nice.fr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ import frege.compiler.types.SNames
import frege.compiler.types.Packs
import frege.compiler.types.QNames
import frege.compiler.types.Symbols
import frege.compiler.types.Types(SigmaT, RhoT)
import frege.compiler.types.Global

--- things that need the environment to print nicely
Expand Down Expand Up @@ -106,7 +107,7 @@ protected category (symv@SymV {name,nativ, expr}) g = if isJust nativ then "nati
| MName _ _ <- name = "member " ++ funval
| otherwise = funval
funval | isJust nativ = "function"
| Just x <- symv.gExpr g = "function"
| ForAll _ RhoFun{} <- symv.typ = "function"
| otherwise = "value"
protected category (SymA {name}) g = "type alias"
protected category (SymL {alias}) g = case g.find alias of
Expand Down
18 changes: 10 additions & 8 deletions frege/compiler/passes/Transdef.fr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -589,8 +589,9 @@ transDatDcl env fname (d@DatDcl {pos}) = do
let transSigma1 (ForAll [] (RhoTau [] t)) = transTau t
transSigma1 s = do -- field types can be sigmas
ForAll bound frho <- U.validSigma1 (map _.var bndrs) s
frho <- U.transRho (map _.var bound ++ map _.var bndrs) frho
bounds ← U.transBounds bound
let env = fold (\tm tv → tm.insertS tv.var tv) TreeMap.empty (bounds ++ bndrs)
frho <- U.transRho env frho
stio (ForAll bounds frho)
sigmas <- mapSt (transSigma1 • ConField.typ) d.flds
let nfs sigs = zipWith ConField.{typ=} con.flds sigs
Expand Down Expand Up @@ -618,7 +619,7 @@ transJavDcl env fname (d@JavDcl {pos}) = do
-- extract and translate generic type arguments
let doit (Just gs) = mapM transTau gs >>= mapM forceTau
doit Nothing = pure sym.typ.tvars
gargs ← doit d.gargs -- fromMaybe (pure (sym.typ.tvars sym.pos)) (map transTau <$> d.gargs)
gargs ← doit d.gargs -- fromMaybe (pure (sym.typ.tvars sym.pos)) (map transTau <$> d.gargs)
let bound = sym.typ.vars
-- check that generic type arguments do not contain free type variables
forM_ gargs $ \tau → do
Expand All @@ -635,13 +636,14 @@ transJavDcl env fname (d@JavDcl {pos}) = do
v ← free ]
<+> text "may not be used here.")
)
-- fix type arguments that are not generic to kind *
ktype t = case t of
TVar{kind=KVar} → t.{kind=KType}
_ → t
let typ = sym.typ.{bound ← map ktype}
!kind = foldr KApp KType (map _.kind typ.bound)
let purity = d.isPure || (nativ `elem` pureTypes)
-- let hasphantoms = any (`elem` [KVar, KType]) sym.typ.kinds
-- when (not purity && not hasphantoms) do
-- E.error pos (msgdoc ("mutable native type " ++ sym.name.nice g ++ " needs a state phantom type"))
-- U.hint pos (msgdoc ("declaration should read: data "
-- ++ sym.typ.nice g ++ " state = native " ++ unJust (sym.nativ)))
changeSym sym.{pur = purity, mutable = d.isMutable, gargs}
changeSym sym.{pur = purity, mutable = d.isMutable, gargs, typ, kind}
foreach d.defs (transdef [] (MName tname))
U.nativeType nativ tname
when (nativ ~ ´\[\]$´) do
Expand Down
86 changes: 81 additions & 5 deletions frege/java/Lang.fr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,16 +44,20 @@ protected package frege.java.Lang
inline (Byte.unsigned)
where

import frege.prelude.PreludeArrays (ArrayElement, JArray, PrimitiveArrayElement)
import frege.prelude.PreludeArrays (ArrayElement, JArray, PrimitiveArrayElement, ArrayOf)
import frege.prelude.PreludeBase
import frege.control.Semigroupoid
import frege.control.Category
import frege.prelude.PreludeBase public(Throwable, Object,
ClassNotFoundException,
NumberFormatException,
InterruptedException)
import frege.prelude.PreludeIO (Exceptional, Mutable, MutableIO, Serializable, STMutable)
import frege.prelude.PreludeIO (Exceptional, Mutable, MutableIO, Serializable, STMutable, readonly)
import frege.prelude.PreludeIO public(Exception)
-- import frege.prelude.PreludeText
import frege.prelude.PreludeMonad
import frege.prelude.PreludeList (ListSource, length, map, fold, zipWith, null, zip)
import frege.prelude.Maybe (mapMaybe)

-- -------------------------------------------------------------------------
-- ---------------------- several exceptions -------------------------------
Expand Down Expand Up @@ -506,11 +510,83 @@ instance Enum Short where
instance PrimitiveArrayElement Short where
native javaClass "short.class" :: Class Short

data JEnum e = pure native "java.lang.Enum" {}
data JEnum (e ≤ JEnum e) = pure native "java.lang.Enum" {e}

{-
instance ArrayElement (JEnum x) where
native javaClass "java.lang.Enum.class" :: Class (JEnum x)
--- Create a one dimensional array with elements of the instantiated type.
native newArray "new[]" :: Int -> ST s (ArrayOf s (JEnum x))
--- Get item at index from immutable array, see 'JArray.itemAt'
pure native itemAt "[i]" :: JArray (JEnum e) -> Int -> Maybe (JEnum e)
--- Get non-null element at index from immutable array, see 'JArray.elemAt'
pure native elemAt "[i]" :: JArray (JEnum x) -> Int -> (JEnum x)
--- Get item at index from mutable array, see 'JArray.getAt'
native getAt "[i]" :: Mutable s (JArray (JEnum x)) -> Int -> ST s (Maybe (JEnum x))
--- Set item or null at index in mutable array, see 'JArray.setAt'
native setAt "[]=" :: Mutable s (JArray (JEnum x)) -> Int -> Maybe (JEnum x) -> ST s ()
--- Get non null item at index from mutable array, see 'JArray.getElemAt'
native getElemAt "[i]" :: Mutable s (JArray (JEnum x)) -> Int -> ST s (JEnum x)
--- Set item at index in mutable array. see 'JArray.setElemAt'
native setElemAt "[]=" :: Mutable s (JArray (JEnum x)) -> Int -> (JEnum x) -> ST s ()
--- Modify item at index in mutable array with result of function application.
modifyAt :: ((JEnum x) -> (JEnum x)) -> Mutable s (JArray (JEnum x)) -> Int -> ST s ()
modifyAt f arr i = getAt arr i >>= setAt arr i . fmap f
--- Modify non null item at index in mutable array with result of function application.
modifyElemAt :: ((JEnum x) -> (JEnum x)) -> Mutable s (JArray (JEnum x)) -> Int -> ST s ()
modifyElemAt f arr i = getElemAt arr i >>= setElemAt arr i . f
--- The size of an 'JArray'
pure native arrayLength ".length" :: JArray (JEnum x) → Int
--- Unload 'JArray' to a list, lazily
listFromArray :: JArray (JEnum x) → [(JEnum x)]
listFromArray !ra = mapMaybe (itemAt ra) [0..arrayLength ra - 1]
--- Unload 'JArray' to a maybe list, lazily
maybeListFromArray :: JArray (JEnum x) → [Maybe (JEnum x)]
maybeListFromArray !ra = map (itemAt ra) [0..arrayLength ra - 1]
{--
Create a mutable array from a finite list.
-}
arrayFromListST :: [(JEnum x)] -> STMutable β (JArray (JEnum x))
arrayFromListST xs = do
let !len = xs.length
arr <- newArray len
let !acts = zipWith (setElemAt arr) [0..len-1] xs
sequence_ acts
pure arr
--- Create an immutable array from a finite list whose elements are 'ArrayElement`
--- Uses 'JArray.fromList' and freezes the resulting array.
arrayFromList :: [(JEnum x)] -> JArray (JEnum x)
arrayFromList !xs = (arrayFromListST xs >>= readonly id).run
{--
Create a mutable array from a finite list of 'Maybe' values.
-}
arrayFromMaybeListST ∷ [Maybe (JEnum x)] -> STMutable β (JArray (JEnum x))
arrayFromMaybeListST xs = arrayFromIndexListST ys
where
ys = [ (n,y) | (Just y, n) <- zip xs [0..]]
instance ArrayElement (JEnum e) where
native javaClass "java.lang.Enum.class" :: Class (JEnum e)
--- Create an immutable 'JArray' from a finite list of 'Maybe' values.
-- The array slots corresponding to 'Nothing' values in the input remain @null@
arrayFromMaybeList ∷ [Maybe (JEnum x)] -> JArray (JEnum x)
arrayFromMaybeList xs = ST.run(arrayFromMaybeListST xs >>= readonly id)
{--
Create a mutable array from a finite index/value list.
Indexes not mentioned in the list remain @null@ for
non primitive array elements and 0 otherwise.
-}
arrayFromIndexListST :: [(Int,(JEnum x))] -> STMutable β (JArray (JEnum x))
arrayFromIndexListST xs = do
let !len = PreludeList.fold max 0 (PreludeList.map fst xs)
arr <- newArray (if null xs then 0 else len+1)
mapM_ (\(i,a) -> setElemAt arr i a) xs
pure arr
--- Create an immutable 'JArray' from a finite index/value list. See 'arrayFromIndexListST'
arrayFromIndexList :: [(Int,(JEnum x))] -> JArray (JEnum x)
arrayFromIndexList xs = ST.run(arrayFromIndexListST xs >>= readonly id)
-}
instance ArrayElement Object where
native javaClass "java.lang.Object.class" :: Class Object

46 changes: 23 additions & 23 deletions frege/java/Util.fr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1386,18 +1386,19 @@ data Collection e = native java.util.Collection where
toList :: Mutable s (Collection e) -> ST s [e]
toList collection = collection.iterator >>= Iterator.toList




{--
A specialized Map implementation for use with enum type keys.
More: 'https://docs.oracle.com/javase/7/docs/api/java/util/EnumMap.html JavaDoc'
-}
data EnumMap k v = native java.util.EnumMap {} where
-- ^^
-- use the raw type until we can express generic bounds
-- in our kind system


native new :: Class k -> STMutable s (EnumMap k v)
| Mutable s (Map k v) -> STMutable s (EnumMap k v)
| Mutable s (EnumMap k v) -> STMutable s (EnumMap k v)
native new :: forall (k≤JEnum k) s v. Class k -> STMutable s (EnumMap k v)
| forall (k≤JEnum k) s v. Mutable s (Map k v) -> STMutable s (EnumMap k v)
| forall (k≤JEnum k) s v. Mutable s (EnumMap k v) -> STMutable s (EnumMap k v)

native clear :: Mutable s (EnumMap k v) -> ST s ()

Expand All @@ -1413,7 +1414,7 @@ data EnumMap k v = native java.util.EnumMap {} where

native get :: Mutable s (EnumMap k v) -> k -> ST s (Maybe Object)

native hashCode :: Mutable s (EnumMap k v) -> ST s Int
native hashCode :: forall (k≤JEnum k) s v . Mutable s (EnumMap k v) -> ST s Int

native keySet :: Mutable s (EnumMap k v) -> STMutable s (Set k)

Expand Down Expand Up @@ -1662,30 +1663,29 @@ instance Serializable (ArrayList e)
More: 'https://docs.oracle.com/javase/7/docs/api/java/util/EnumSet.html JavaDoc'
-}
data EnumSet e = native java.util.EnumSet {} where
-- ^^ we can't currently express generic bounds
data EnumSet (e ≤ JEnum e) = native java.util.EnumSet {e} where

native allOf java.util.EnumSet.allOf {} :: Class (JEnum e) -> STMutable s (EnumSet (JEnum e))
native allOf java.util.EnumSet.allOf {e} :: Class e -> STMutable s (EnumSet e)

native clone :: Mutable s (EnumSet e) -> STMutable s (EnumSet e)
native clone{} :: Mutable s (EnumSet e) -> STMutable s (EnumSet e)

native complementOf java.util.EnumSet.complementOf {} :: Mutable s (EnumSet (JEnum e)) -> STMutable s (EnumSet (JEnum e))
native complementOf java.util.EnumSet.complementOf {e} :: Mutable s (EnumSet e) -> STMutable s (EnumSet e)

native copyOf java.util.EnumSet.copyOf {} :: Mutable s (EnumSet (JEnum e)) -> STMutable s (EnumSet (JEnum e))
| Mutable s (Collection (JEnum e)) -> STMutable s (EnumSet (JEnum e))
native copyOf java.util.EnumSet.copyOf {e} :: Mutable s (EnumSet e) -> STMutable s (EnumSet e)
| Mutable s (Collection e) -> STMutable s (EnumSet e)

native noneOf java.util.EnumSet.noneOf {} :: Class (JEnum e) -> STMutable s (EnumSet (JEnum e))
native noneOf java.util.EnumSet.noneOf {e} :: Class e -> STMutable s (EnumSet e)

native from "java.util.EnumSet.of" {} :: JEnum e -> JEnum e -> JEnum e -> JEnum e -> STMutable s (EnumSet (JEnum e))
| JEnum e -> JEnum e -> JEnum e -> JEnum e -> JEnum e -> STMutable s (EnumSet (JEnum e))
| JEnum e -> Mutable s (JArray (JEnum e)) -> STMutable s (EnumSet (JEnum e))
| JEnum e -> STMutable s (EnumSet (JEnum e))
| JEnum e -> JEnum e -> STMutable s (EnumSet (JEnum e))
| JEnum e -> JEnum e -> JEnum e -> STMutable s (EnumSet (JEnum e))
native from "java.util.EnumSet.of" {e} :: e -> e -> e -> e -> STMutable s (EnumSet e)
| e -> e -> e -> e -> e -> STMutable s (EnumSet e)
| e -> Mutable s (JArray e) -> STMutable s (EnumSet e)
| e -> STMutable s (EnumSet e)
| e -> e -> STMutable s (EnumSet e)
| e -> e -> e -> STMutable s (EnumSet e)

native range java.util.EnumSet.range {} :: JEnum e -> JEnum e -> STMutable s (EnumSet e)
native range java.util.EnumSet.range {e} :: e -> e -> STMutable s (EnumSet e)

instance Serializable (EnumSet e)
-- instance Serializable (EnumSet e)


{--
Expand Down

0 comments on commit b518102

Please sign in to comment.