Types.hs 28.5 KB
Newer Older
Marc Coiffier's avatar
Marc Coiffier committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
{-# LANGUAGE CPP, RecursiveDo, ViewPatterns, PatternSynonyms, ScopedTypeVariables, UndecidableInstances #-}
module Curly.Core.Types (
  -- * Type constructors
  TypeClass(..),NativeType(..),TypeShape(..),
  -- * Type paths
  TypeIndex(..),pattern In,pattern Out,PathRoot(..),TypePath,
  t'ImplicitRoot,t'ContextRoot,
  -- * Types
  Type(..),
  argumentType,builtinType,rigidTypeFun,
  typeConstraints,
  extractFirstArgument,
  mapTypePaths,mapTypePathsMonotonic,traverseTypeShapes,mapTypeShapes,
  selectConstraints,clearContexts,abstractStructTypes,abstractImplicitType,
  functionFrom,
16
  freezeType,thawType,isComplexType,compareConstrainedness,isSubtypeOf,constraintType,
Marc Coiffier's avatar
Marc Coiffier committed
17
18
19
20
21
22
23
  -- * Implicit instances
  InstanceMap,isValidInstanceMap
  )
       where

import Definitive
import Curly.Core
24
import Curly.Core.Documentation
Marc Coiffier's avatar
Marc Coiffier committed
25
26
27
28
29
30
31
32
33
34
35
import Language.Format
import qualified Data.Map
import Control.DeepSeq

i'equivRel :: Iso (Relation e a a) (Relation e' a' a') (Equiv e a) (Equiv e' a')
i'equivRel = iso (\(Equiv r) -> r) Equiv
t'assoc :: (OrderedMap m k a,OrderedMap m' k' a') => Traversal (k,a) (k',a') m m'
t'assoc = i'ascList.traverse
i'ascList :: (OrderedMap m k a,OrderedMap m' k' a') => Iso [(k,a)] [(k',a')] m m'
i'ascList = iso (by ascList) (yb ascList)

36
data TypeClass s = Function | NamedType Int s | ClassType Int [Set Int] s
37
38
39
40
41
               deriving (Eq,Ord,Generic)
instance Identifier s => Show (TypeClass s) where
  show Function = "->"
  show (NamedType _ s) = identName s
  show (ClassType _ _ s) = identName s
Marc Coiffier's avatar
Marc Coiffier committed
42
43
44
45
46
instance HasIdents s s' (TypeClass s) (TypeClass s') where
  ff'idents _ Function = pure Function
  ff'idents k (NamedType n s) = NamedType n<$>k s
  ff'idents k (ClassType n is s) = ClassType n is<$>k s
instance NFData s => NFData (TypeClass s)
47
48
instance Serializable Bytes s => Serializable Bytes (TypeClass s)
instance Format Bytes s => Format Bytes (TypeClass s)
Marc Coiffier's avatar
Marc Coiffier committed
49
50
51
52
53
54

typeClassNArgs :: TypeClass s -> Int
typeClassNArgs Function = 2
typeClassNArgs (NamedType n _) = n
typeClassNArgs (ClassType n _ _) = n

55
data NativeType = NT_RigidType String | NT_Int | NT_String | NT_Array | NT_Unit | NT_File | NT_Syntax | NT_Expr 
Marc Coiffier's avatar
Marc Coiffier committed
56
57
                deriving (Eq,Ord,Generic)
instance Show NativeType where
58
  show (NT_RigidType t) = "#."+t
Marc Coiffier's avatar
Marc Coiffier committed
59
60
  show NT_Int = "#int" ; show NT_String = "#string"
  show NT_Unit = "#unit" ; show NT_File = "#file"
61
  show NT_Syntax = "#syn" ; show NT_Expr = "#expr"
62
  show NT_Array = "#array"
63
64
instance Serializable Bytes NativeType
instance Format Bytes NativeType
Marc Coiffier's avatar
Marc Coiffier committed
65
66
67
68
instance NFData NativeType

-- | An index into a type
data TypeIndex s = TypeIndex (TypeClass s) Int
69
70
71
                 deriving (Eq,Ord,Generic)
instance Identifier s => Show (TypeIndex s) where
  show (TypeIndex c n) = show c+":"+show n
Marc Coiffier's avatar
Marc Coiffier committed
72
73
instance HasIdents s s' (TypeIndex s) (TypeIndex s') where
  ff'idents k (TypeIndex c i) = forl ff'idents c k <&> \c' -> TypeIndex c' i
74
75
instance Serializable Bytes s => Serializable Bytes (TypeIndex s)
instance Format Bytes s => Format Bytes (TypeIndex s)
Marc Coiffier's avatar
Marc Coiffier committed
76
instance NFData s => NFData (TypeIndex s)
77
pattern In :: TypeIndex t
Marc Coiffier's avatar
Marc Coiffier committed
78
pattern In = TypeIndex Function 0
79
pattern Out :: TypeIndex t
Marc Coiffier's avatar
Marc Coiffier committed
80
81
pattern Out = TypeIndex Function 1

82
{- | The path of a node inside a type.
Marc Coiffier's avatar
Marc Coiffier committed
83
84
85
86
87
88
89
90
91
92
93
94

A path is comprised of two parts : a canonical path, which uniquely identifies the node within
its type graph; and a set of equivalent paths that are shared between all types.
-}
data PathRoot = ArgumentRoot Int | TypeRoot | ImplicitRoot Int | ContextRoot Int | NamedRoot String
              deriving (Eq,Ord,Show,Generic)
t'ImplicitRoot :: Traversal' PathRoot Int
t'ImplicitRoot k (ImplicitRoot n) = ImplicitRoot<$>k n
t'ImplicitRoot _ x = pure x
t'ContextRoot :: Traversal' PathRoot Int
t'ContextRoot k (ContextRoot n) = ContextRoot<$>k n
t'ContextRoot _ x = pure x
95
96
instance Serializable Bytes PathRoot
instance Format Bytes PathRoot
Marc Coiffier's avatar
Marc Coiffier committed
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
instance NFData PathRoot
type TypePath s = (PathRoot,[TypeIndex s])
pathIdents :: FixFold s s' (TypePath s) (TypePath s')
pathIdents = l'2.each.ff'idents

-- | The shape of a Curly type
data TypeShape s = TypeCons (TypeClass s)
                 | NativeType NativeType
                 | PolyType
                 | SkolemType Int
                 | TypeMismatch (TypeShape s) (TypeShape s)
                 | HiddenTypeError
                 deriving (Show,Eq,Ord,Generic)
instance Ord s => Semigroup (TypeShape s) where
  TypeCons c + TypeCons c' | c == c' = TypeCons c
  NativeType t + NativeType t' | t == t' = NativeType t
  SkolemType x + SkolemType x' | x == x' = SkolemType x
  PolyType + t = t
  t + PolyType = t
  t + t' = TypeMismatch t t'
instance Ord s => Monoid (TypeShape s) where zero = PolyType
instance Ord s' => HasIdents s s' (TypeShape s) (TypeShape s') where
  ff'idents k (TypeCons c) = map TypeCons (forl ff'idents c k)
  ff'idents k (TypeMismatch t t') = liftA2 TypeMismatch (forl ff'idents t k) (forl ff'idents t' k)
  ff'idents _ (NativeType n) = pure (NativeType n)
  ff'idents _ PolyType = pure PolyType
  ff'idents _ (SkolemType x) = pure (SkolemType x)
  ff'idents _ HiddenTypeError = pure HiddenTypeError
125
instance Serializable Bytes s => Serializable Bytes (TypeShape s) where
126
127
128
129
130
131
132
133
  encode p (TypeCons Function) = encodeAlt p 0 ()
  encode p (TypeCons (NamedType n s)) = encodeAlt p 1 (n,s)
  encode p (TypeCons (ClassType n is s)) = encodeAlt p 2 (n,is,s)
  encode p (NativeType t) = encodeAlt p 3 t
  encode p PolyType = encodeAlt p 4 ()
  encode p (SkolemType x) = encodeAlt p 5 x
  encode p (TypeMismatch t t') = encodeAlt p 6 (t,t')
  encode p HiddenTypeError = encodeAlt p 7 ()
134
instance (Format Bytes s,Ord s) => Format Bytes (TypeShape s) where
Marc Coiffier's avatar
Marc Coiffier committed
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
  datum = datumOf [FormatAlt (uncurry0 $ TypeCons Function)
                  ,FormatAlt (\(n,s) -> TypeCons (NamedType n s))
                  ,FormatAlt (\(n,is,s) -> TypeCons (ClassType n is s))
                  ,FormatAlt NativeType
                  ,FormatAlt (uncurry0 PolyType)
                  ,FormatAlt SkolemType
                  ,FormatAlt (uncurry TypeMismatch)
                  ,FormatAlt (uncurry0 HiddenTypeError)]
instance NFData s => NFData (TypeShape s)

{- | A Curly type.

A Curly type may be understood as a (possibly infinite) set of
constraints over its graph ("the node A must be a function", "the
output of B must be an Int", ...).

In that sense, Curly types are monoids by isomorphism with the set
monoid (@C(a+b)=C(a)+C(b)@ where @C(a)@ is the constraint set of the
type @a@). This monoid instance is used to perform type inference by
unifying constraints on the appropriate types.

-}
newtype Type s = Type (Equiv (TypeShape s) (TypePath s))
               deriving Generic
159
160
instance (Ord s,Serializable Bytes s) => Serializable Bytes (Type s)
instance (Ord s,Format Bytes s) => Format Bytes (Type s)
Marc Coiffier's avatar
Marc Coiffier committed
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
instance NFData s => NFData (Type s)
type TypeRel s = Equiv (TypeShape s) (TypePath s)
i'typeRel :: Iso (TypeRel s) (TypeRel s') (Type s) (Type s')
i'typeRel = iso (\(Type s) -> s) Type
instance Identifier s => Semigroup (Type s) where
  t + t' = getId (zipTypes (\_ _ -> pure ()) t t')
instance Identifier s => Monoid (Type s) where zero = Type zero
instance (Ord s,Ord s') => HasIdents s s' (Type s) (Type s') where
  ff'idents k (Type e) = map Type
                         $ forl (i'equivRel.i'ranges
                                 .t'assoc.(
                                   l'1.pathIdents
                                   .+l'2.t'assoc.(l'1.pathIdents
                                                  .+l'2.ff'idents))) e k
instance Identifier s => Eq (Type s) where t == t' = compare t t' == EQ
instance Identifier s => Ord (Type s) where
  compare t t' = case zipTypes cmpNodes t t' of
    Left x -> x
    Right _ -> EQ
    where cmpNodes PolyType _ = unit
          cmpNodes _ PolyType = unit
          cmpNodes s s' = case compare s s' of
            EQ -> unit
            x -> Left x
185
186

compareConstrainedness :: Identifier s => Type s -> Type s -> Maybe Ordering
Marc Coiffier's avatar
Marc Coiffier committed
187
188
189
190
191
192
193
194
195
compareConstrainedness t t' = case fst (zipTypes cmp t t') of
    (True,False) -> Just GT
    (False,True) -> Just LT
    (False,False) -> Just EQ
    (True,True) -> Nothing
    where cmp x y | x==y = unit
          cmp PolyType _ = tell (False,True)
          cmp _ PolyType = tell (True,False)
          cmp _ _ = tell (True,True)
196
isSubtypeOf :: Identifier s => Type s -> Type s -> Bool
Marc Coiffier's avatar
Marc Coiffier committed
197
198
199
isSubtypeOf t t' = compareConstrainedness t t' `elem` [Just GT,Just EQ]

instance Identifier s => Show (Type s) where
200
  show (Type e) = (arguments+implicits+body+context+subs)
Marc Coiffier's avatar
Marc Coiffier committed
201
    where paths :: Map (Set (TypePath s)) (Maybe (TypeClass s),Maybe String,String)
202
          ~(paths,_,_) = execS (traverseTypeShapes f (Type e)^..state) (c'map zero,tail (namesFrom ['a'..'z']),tail (namesFrom ['A'..'Z']))
Marc Coiffier's avatar
Marc Coiffier committed
203
204
205
206
207
208
            where f ps x = x <$ do
                    let p:_ = ps
                    modify $ \(m,as,bs) ->
                      let ins a b c = insert (fromKList ps) (a,b,c) m
                      in if isKeyIn (fromKList ps) m then (m,as,bs) else case x of
                      TypeCons c -> let short = guard (length ps>1) >> pure (head bs)
209
210
211
212
                                    in (ins (Just c) short (showPat (showC c) [let p' = second (+[TypeIndex c i]) p
                                                                               in case lookup (e^.l'rangeSet p') paths of
                                                                                 Just (pri,ms,s) -> fromMaybe ((if hasPrecedence i c pri then format "(%s)" else id) s) ms
                                                                                 Nothing -> "#<path:"+showPath p'+">"
Marc Coiffier's avatar
Marc Coiffier committed
213
214
215
216
217
218
219
220
221
                                                                              | i <- [0..typeClassNArgs c-1]]),
                                        as,maybe id (pure tail) short bs)
                      PolyType | length ps>1 -> (ins Nothing Nothing (head as),tail as,bs)
                               | otherwise -> (ins Nothing Nothing "*",as,bs)
                      NativeType t -> (ins Nothing Nothing (showNT t),as,bs)
                      SkolemType _ | length ps>1 -> (ins Nothing Nothing (head bs),as,tail bs)
                                   | otherwise -> (ins Nothing Nothing ".",as,bs)
                      _ -> (ins Nothing Nothing "∅",as,bs)
          hasPrecedence 0 Function (Just Function) = True
222
          hasPrecedence _ _ (Just c) | typeClassNArgs c==0 = False
Marc Coiffier's avatar
Marc Coiffier committed
223
224
225
226
227
228
229
230
231
232
233
234
235
          hasPrecedence _ _ Nothing = False
          hasPrecedence _ x (Just y) = x > y
          showPat "_" as = intercalate " " as
          showPat ('_':p) (a:as) = format "%s%s" a (showPat p as)
          showPat (c:p) as = c:showPat p as
          showPat [] as = intercalate " " ("":as)
          showC Function = "_ -> _"
          showC (NamedType _ s) = identName s
          showC (ClassType _ _ s) = identName s
          showNT NT_Int = "#int"
          showNT NT_String = "#string"
          showNT NT_Unit = "#unit"
          showNT NT_File = "#file"
236
237
          showNT NT_Syntax = "#syn"
          showNT NT_Expr = "#expr"
238
          showNT NT_Array = "#array"
Marc Coiffier's avatar
Marc Coiffier committed
239
          showNT (NT_RigidType t) = t
240
241
242
243
          showPath (r,p) = show r+":"+foldMap showPComp p
            where showPComp In = "I"
                  showPComp Out = "O"
                  showPComp (TypeIndex c n) = format "(%s,%s)" (show c) (show n)
Marc Coiffier's avatar
Marc Coiffier committed
244
245
246
247
248
          pathList = paths^.ascList <&> \(x,(_,y,z)) -> (x,(y,z))
          namesFrom cs = "":fold (deZip (for cs (\c -> Zip (map (c:) (namesFrom cs)))))
          arguments = let x = intercalate "," [format "(%d)%s" i (snd s) | (ps,s) <- pathList, (ArgumentRoot i,[]) <- keys ps]
                      in if empty x then "" else format "[%s] " x
          implicits = let x = intercalate "," [snd s | (ps,s) <- pathList, (ImplicitRoot _,[]) <- keys ps]
249
                      in if empty x then "" else x+" => "
Marc Coiffier's avatar
Marc Coiffier committed
250
251
          body = fold [fromMaybe (snd s) (fst s) | (ps,s) <- pathList, (TypeRoot,[]) <- keys ps]
          context = let x = intercalate "," [snd s | (ps,s) <- pathList, (ContextRoot _,[]) <- keys ps]
252
                    in if empty x then "" else " <= "+x
Marc Coiffier's avatar
Marc Coiffier committed
253
254
255
          subs = interleave ("\n  where ":repeat "\n        ") $ "":[
            format "%s = %s" short long
            | (_,(Just short,long)) <- pathList]
256
257
instance Identifier s => Documented (Type s) where
  document t = docTag' "type" [Pure (show t)]
Marc Coiffier's avatar
Marc Coiffier committed
258
259
260

zipTypes :: (Monad m,Identifier s) => (TypeShape s -> TypeShape s -> m ()) -> Type s -> Type s -> m (Type s)
zipTypes zipNodes (Type ta) (Type tb) =
261
262
263
  map Type
  $ traverseEquivEdges (\_ (shl,shr) -> mergeSkol shl shr <$ zipNodes shl shr)
  $ saturate (ta' + tagEdges (zero,) tb)
Marc Coiffier's avatar
Marc Coiffier committed
264
265
266
267
  where tagEdges f = mapEquivEdgesMonotonic Just (Just . f)
        (Max nska,ta') = tell (Max (-1)) >> traverseEquivEdges go ta
          where go _ x@(SkolemType n) = tell (Max n) >> pure (x,zero)
                go _ x = pure (x,zero)
268
269
270
271
272

        mergeSkol (SkolemType n) (SkolemType _) = SkolemType n
        mergeSkol PolyType (SkolemType n) = SkolemType (n+nska+1)
        mergeSkol a b = a+b

273
274
275
276
        nextPath c i = second (+[TypeIndex c i])
        isPathPrefix (r,p) (r',p') = r==r' && let (ph',pt') = splitAt (length p) p' in ph'==p && nonempty pt'
        withoutPrefixes l = [p' | (p,p') <- zip (head l:l) l
                                , not (isPathPrefix p p')]
277
278
279
280

        unifyNodes nodes@(can:_) = l'range can %~ (+fromKList nodes)
        unifyNodes _ = id

281
282
        pathSet = c'set . yb ascList . map (,undefined)
        saturate rel =
283
          case [map (nextPath c i . fst) domL+nextDom
284
               | (can,dom) <- rel^.i'equivRel.i'domains.ascList
285
286
287
288
289
290
291
               , let domL = dom^.ascList
               , TypeCons c <- take 1 $ map (uncurry (+) . snd) domL
               , i <- [0..typeClassNArgs c-1]
               , let projDom = map (nextPath c i) (withoutPrefixes $ map fst domL)
                     nextDomL = rel^.l'domain (nextPath c i can).ascList
                     nextDom = map fst nextDomL
               , nonempty (pathSet projDom - pathSet nextDom)]
292
293
          of paths : _ -> saturate (unifyNodes paths rel)
             [] -> rel
Marc Coiffier's avatar
Marc Coiffier committed
294
295
296
297
298
299
300
301

type TypeSkel s = Free ((,) (TypeClass s):.:[]) (TypeShape s)

poly :: TypeSkel s
(-->) :: TypeSkel s -> TypeSkel s -> TypeSkel s
poly = Pure PolyType
infixr 3 -->
a --> b = Join (Compose (Function,[a,b]))
302
303

lnSkel :: Ord s => TypePath s -> TypePath s -> TypeSkel s -> Equiv (TypeShape s) (TypePath s) -> Equiv (TypeShape s) (TypePath s)
Marc Coiffier's avatar
Marc Coiffier committed
304
305
306
307
308
lnSkel p p' = \x -> case x of
  Join (Compose (c,as)) -> set (link p p') (Just (TypeCons c))
                           . compose (zipWith (\i a -> let down = (+[TypeIndex c i])
                                                       in lnSkel (second down p) (second down p') a) [0..] as)
  Pure sh -> warp (link p p') (Just . (sh+) . fold)
309
310

ln :: Ord s => [TypeIndex s] -> [TypeIndex s] -> TypeSkel s -> Equiv (TypeShape s) (TypePath s) -> Equiv (TypeShape s) (TypePath s)
Marc Coiffier's avatar
Marc Coiffier committed
311
ln p p' = lnSkel (TypeRoot,p) (TypeRoot,p')
312
313

ln' :: Ord s => [TypeIndex s] -> TypeSkel s -> Equiv (TypeShape s) (TypePath s) -> Equiv (TypeShape s) (TypePath s)
Marc Coiffier's avatar
Marc Coiffier committed
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
ln' p = ln p p

mapTypePaths :: Ord s => (TypePath s -> Maybe (TypePath s)) -> Type s -> Type s
mapTypePaths f = i'typeRel %~ mapEquivEdges f Just
mapTypePathsMonotonic :: Ord s => (TypePath s -> Maybe (TypePath s)) -> Type s -> Type s
mapTypePathsMonotonic f = i'typeRel %~ mapEquivEdgesMonotonic f Just
traverseEquivEdges :: (Ord a,Ord e,Ord e',Monad m) => ([a] -> e -> m e') -> Equiv e a -> m (Equiv e' a)
traverseEquivEdges f = traversel (i'equivRel.i'domains.i'ascList) $ \l ->
  sequence [traversel (l'2.i'ascList.each.l'2) (f (keys m)) x
           | x@(_,m) <- l]
traverseTypeShapes :: (Ord s,Monad m) => ([TypePath s] -> TypeShape s -> m (TypeShape s)) -> Type s -> m (Type s)
traverseTypeShapes f = traversel (i'typeRel.i'equivRel.i'domains.ascList) $ \l ->
  sequence [traversel (l'2.i'ascList.each.l'2) (f (keys m)) x
           | x@(_,m) <- l]
mapTypeShapes :: Ord s => ([TypePath s] -> TypeShape s -> TypeShape s) -> Type s -> Type s
mapTypeShapes f = getId . traverseTypeShapes (map2 Id f)

selectConstraints :: Ord s => (Int -> Maybe Int) -> (Int -> Maybe Int) -> Type s -> Type s
selectConstraints ip cp = mapTypePathsMonotonic f
  where f (ContextRoot n,p) = map (\n' -> (ContextRoot n',p)) (cp n)
        f (ImplicitRoot n,p) = map (\n' -> (ImplicitRoot n',p)) (ip n)
        f x = Just x

extractFirstArgument :: Identifier s => Type s -> Type s
extractFirstArgument = warp i'typeRel addCons . mapTypePaths (Just . f)
  where f (TypeRoot,p) = (TypeRoot,Out:p)
        f (ArgumentRoot 0,p) = (TypeRoot,In:p)
        f (ArgumentRoot n,p) = (ArgumentRoot (n-1),p)
        f x = x
        addCons = ln' [] (poly --> poly)
clearContexts :: Ord s => Type s -> Type s
clearContexts = selectConstraints Just (const Nothing)

isComplexType :: Ord s => Type s -> Bool
isComplexType = fst . traverseTypeShapes isC
  where isC ps x = (isCS ps x,x)
        isCS ps (TypeCons _) = any (\p -> any (isPathPrefix p) ps) ps
        isCS _ _ = False
        isPathPrefix (r,p) (r',p') = r==r' && isPrefix p p' && p/=p'
        isPrefix [] _ = True
        isPrefix (x:l) (x':l') | x==x' = isPrefix l l'
        isPrefix _ _ = False

typeConstraints :: Ord s => Type s -> ([(s,[Set Int])],[(s,[Set Int])])
typeConstraints t = let l = t^.i'typeRel.i'equivRel.i'domains.ascList.mapping (mapping ascList)
                    in ([(s,is) | ((ImplicitRoot _,[]),[(_,TypeCons (ClassType _ is s))]) <- l]
                       ,[(s,is) | ((ContextRoot _,[]),[(_,TypeCons (ClassType _ is s))]) <- l])


argumentType :: Ord s => Int -> Type s
argumentType n = Type (set (linkP (TypeRoot,[]) (ArgumentRoot n,[])) True zero)
rigidTypeFun :: Ord s => String -> Type s
rigidTypeFun n = zero
                 & ln' [] (poly --> poly)
                 . lnn [In] [] n
                 . lnn [Out] [] n
                 & Type
  where lnn p p' = lnSkel (TypeRoot,p) (NamedRoot n,p') . Pure . NativeType . NT_RigidType
        
-- | Create a pair of constructor/destructor types
abstractStructTypes :: Ord s => s -> [String] -> [String] -> Type s -> (Type s,Type s)
375
376
abstractStructTypes c pub priv (Type e) = (Type e,Type e) & mk True <#> mk False
  where (classPos,_) = (traverseTypeShapes k (Type e)^..state) (c'map zero)
Marc Coiffier's avatar
Marc Coiffier committed
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
          where k ps sh@(NativeType (NT_RigidType s))
                  | isPrivate s = do
                      for_ ps $ \(p,_) -> mat p.l'1 =- True
                      return sh
                k ps PolyType = do
                  for_ ps $ \(p,_) -> mat p.l'2 =- True
                  return PolyType
                k _ x = return x
        tc = NamedType (length pub) c
        (il,cl) = partition snd [(n,x) | (ImplicitRoot n,(x,y)) <- classPos^.ascList
                                       , x/=y]
        (toI,toC) = (to il,to cl)
          where to l = \i -> fromMaybe i $ lookup i m
                  where m = c'map $ zipWith (\i (j,_) -> (j,i)) [0..] l^..ascList
        privSet = c'set (fromKList priv)
        isPrivate s = s`isKeyIn`privSet
        isExtended = nonempty il || nonempty cl
        lntc pref = ln' pref (Pure $ TypeCons tc)
                    . compose (zipWith (\i n -> lnSkel (TypeRoot,pref+[TypeIndex tc i]) (NamedRoot n,[]) poly)
                               [0..] pub)
        delNamedRoots = mapTypePaths f'
          where f' (NamedRoot _,_) = Nothing
                f' x = Just x
        runIdGen ma = evalS (ma^..state) (0,c'map zero)
        nextID ps = id <~ \(n,m) -> case lookup ps m of
          Just i -> ((n,m),i)
          Nothing -> ((n+1,insert ps n m),n)
        mk isCons t =
          delNamedRoots $
          if isCons
          then let f (TypeRoot,p) = Just (TypeRoot,In:p)
                   f (r@(ImplicitRoot n),p) = lookup r classPos >>= \(isP,isF) -> do
                     guard (isP/=isF)
                     return (if isP then ImplicitRoot (toI n) else ContextRoot (toC n),p)
                   f (ContextRoot _,_) = Nothing
                   f x = Just x
                   g ps PolyType = SkolemType <$> nextID ps
                   g _ (NativeType (NT_RigidType _)) = pure PolyType
                   g _ x = pure x
                   addCons = ln' [] (poly --> poly) . lntc [Out]
               in warp i'typeRel addCons $ mapTypePaths f $ runIdGen $ traverseTypeShapes g t
          else let f (TypeRoot,p) = Just (TypeRoot,(if isExtended then ([In,In]+) else (Out:)) p)
                   f (r@(ImplicitRoot n),p) = lookup r classPos >>= \(isP,isF) -> do
                     guard (isP/=isF)
                     return (if isP then ContextRoot (toI n) else ImplicitRoot (toC n),p)
                   f (ContextRoot _,_) = Nothing
                   f x = Just x
                   g ps (NativeType (NT_RigidType s)) | isPrivate s = SkolemType <$> nextID ps
                                                      | otherwise = pure PolyType
                   g _ x = pure x
                   strPref = if isExtended then [Out,In] else [In]
                   addCons = lntc strPref
                             . if isExtended
                               then ln' [] ((poly --> poly) --> (poly --> poly))
                                    . ln [In,Out] [Out,Out] poly
                               else ln' [] (Pure (TypeCons Function))
               in runIdGen $ traverseTypeShapes g $ warp i'typeRel addCons $ mapTypePaths f $ t

-- | 
abstractImplicitType :: Ord s => (s,[Set Int]) -> [String] -> Type s -> Type s
abstractImplicitType (c,is) as = mapTypeShapes g . warp i'typeRel addCons . mapTypePaths f
  where f (NamedRoot r,p) = lookup r rootInds <&> \i -> (ImplicitRoot 0,TypeIndex ct i:p)
        f (ImplicitRoot _,_) = Nothing
        f (ContextRoot _,_) = Nothing
        f x = Just x
        g _ (NativeType (NT_RigidType _)) = PolyType
        g _ x = x
        ct = ClassType (length as) is c
        rootInds = c'map (fromAList (zip as [0..]))
        addCons = lnSkel (ImplicitRoot 0,[]) (ImplicitRoot 0,[]) (Pure $ TypeCons ct)

448
449
450
451
452
453
454
455
456
457
458
459
460
constraintType :: Ord s => s -> Int -> Type s
constraintType t nargs = zero
                         & compose [ln' p ((poly --> poly) --> poly)
                                    . ln (p+[In,In]) (p+[In,Out]) poly
                                    . ln (p+[In,In]) (retp+[In,TypeIndex tc i]) poly
                                   | i <- [0..nargs-1]
                                   , let p = take i (repeat Out)]
                         . ln' retp (poly --> poly)
                         . ln (retp+[In]) (retp+[Out]) (Join (Compose (tc,[])))
                         & Type
  where retp = take nargs (repeat Out)
        tc = NamedType nargs t

Marc Coiffier's avatar
Marc Coiffier committed
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
-- | `functionFrom t` is the type (t -> *)
functionFrom :: Ord s => Int -> Type s -> Type s
functionFrom shift = mapTypePaths (Just . f)
                     >>> warp i'typeRel (ln' [] (poly --> poly))
  where f (TypeRoot,p) = (TypeRoot,In:p)
        f (ImplicitRoot r,p) = (ImplicitRoot (r+shift),p)
        f x = x

freezeType :: Ord s => Type s -> Type s
freezeType = mapTypeShapes toRigid
  where toRigid ((_,p):_) PolyType = NativeType (NT_RigidType ('*':showCs p))
        toRigid _ (SkolemType n) = NativeType (NT_RigidType ('.':show n))
        toRigid _ x = x
        showCs = intercalate "," . map showC
        showC (TypeIndex _ n) = show n
thawType :: Ord s => Type s -> Type s
thawType = mapTypeShapes fromRigid
  where fromRigid _ (NativeType (NT_RigidType s)) = case identName s of
          '*':_ -> PolyType
          '.':n -> SkolemType (read n)
          _ -> NativeType (NT_RigidType s)
        fromRigid _ x = x

builtinType :: forall s. Identifier s => Builtin -> Type s
builtinType b = (zero :: Type s) & i'typeRel %~ case b of
  B_Undefined     -> ln' [] poly
487
  B_Foreign _ _   -> ln' [] poly
Marc Coiffier's avatar
Marc Coiffier committed
488
489
  B_Seq           -> ln' [] (poly --> poly --> poly)
                     . ln [Out,In] [Out,Out] poly
490

Marc Coiffier's avatar
Marc Coiffier committed
491
492
  (B_Number _)    -> ln' [] intT
  (B_String _)    -> ln' [] stringT
493
  (B_Bytes _)     -> ln' [] stringT
494
495
496
  B_Unit          -> ln' [] unitT
  B_FileDesc _    -> ln' [] fileT

Marc Coiffier's avatar
Marc Coiffier committed
497
498
499
500
501
502
503
504
  B_Open          -> ln' [] (stringT --> (fileT --> poly) --> poly)
                     . ln [Out,In,Out] [Out,Out] poly
  B_Read          -> ln' [] (fileT --> intT --> (stringT --> poly) --> poly)
                     . ln [Out,Out,In,Out] [Out,Out,Out] poly
  B_Write         -> ln' [] (fileT --> stringT --> poly --> poly)
                     . ln [Out,Out,In] [Out,Out,Out] poly
  B_Close         -> ln' [] (fileT --> poly --> poly)
                     . ln [Out,In] [Out,Out] poly
505

Marc Coiffier's avatar
Marc Coiffier committed
506
507
508
509
  B_AddInt        -> ln' [] (intT --> intT --> intT)
  B_SubInt        -> ln' [] (intT --> intT --> intT)
  B_MulInt        -> ln' [] (intT --> intT --> intT)
  B_DivInt        -> ln' [] (intT --> intT --> intT)
510
511
512
513
514
515
516
  B_CmpInt_LT     -> ln' [] (intT --> intT --> poly --> poly --> poly)
                     . ln [Out,Out,In] [Out,Out,Out,In] poly
                     . ln [Out,Out,In] [Out,Out,Out,Out] poly
  B_CmpInt_EQ     -> ln' [] (intT --> intT --> poly --> poly --> poly)
                     . ln [Out,Out,In] [Out,Out,Out,In] poly
                     . ln [Out,Out,In] [Out,Out,Out,Out] poly

Marc Coiffier's avatar
Marc Coiffier committed
517
518
519
  B_AddString     -> ln' [] (stringT --> stringT --> stringT)
  B_StringLength  -> ln' [] (stringT --> intT)
  B_ShowInt       -> ln' [] (intT --> stringT)
520
521

  
522
523
524
525
526
  B_MkArray       -> ln' [] (intT --> arrayT)
  B_ArrayLength   -> ln' [] (arrayT --> intT)
  B_ArrayAt       -> ln' [] (arrayT --> intT --> poly)
  B_ArraySet      -> ln' [] (arrayT --> intT --> poly --> poly --> poly)
                     . ln [Out,Out,Out,In] [Out,Out,Out,Out] poly
527

528
  B_SyntaxNode    -> ln' [] (arrayT --> synT)
529
530
  B_SyntaxSym     -> ln' [] (stringT --> synT)
  B_SyntaxExpr    -> ln' [] (exprT --> synT)
531
  B_SyntaxInd     -> ln' [] (synT --> (arrayT --> poly) --> (exprT --> poly) --> (stringT --> poly) --> poly)
532
533
534
535
536
537
538
539
540
541
542
                     . ln [Out,In,Out] [Out,Out,In,Out] poly
                     . ln [Out,In,Out] [Out,Out,Out,In,Out] poly
                     . ln [Out,In,Out] [Out,Out,Out,Out] poly

  B_ExprLambda    -> ln' [] (stringT --> exprT --> exprT)
  B_ExprApply     -> ln' [] (exprT --> exprT --> exprT)
  B_ExprSym       -> ln' [] (stringT --> exprT)
  B_ExprInd       -> ln' [] (exprT --> (stringT --> exprT --> poly) --> (exprT --> exprT --> poly) --> (stringT --> poly) --> poly)
                     . ln [Out,In,Out,Out] [Out,Out,In,Out,Out] poly
                     . ln [Out,In,Out,Out] [Out,Out,Out,In,Out] poly
                     . ln [Out,In,Out,Out] [Out,Out,Out,Out] poly
543

544
545
546
547
548
  B_ShowExpr      -> ln' [] (exprT --> poly --> poly)
                     . ln [Out,In] [Out,Out] poly
  B_ShowSyntax    -> ln' [] (synT --> poly --> poly)
                     . ln [Out,In] [Out,Out] poly

549
550
  B_Relocatable _ _ _ _ -> ln' [] intT
  B_RawIndex _          -> ln' [] (intT --> intT)
Marc Coiffier's avatar
Marc Coiffier committed
551
552
553
554
  where
    nativeT = Pure . NativeType
    intT = nativeT NT_Int ; stringT = nativeT NT_String
    fileT = nativeT NT_File ; unitT = nativeT NT_Unit
555
    synT = nativeT NT_Syntax ; exprT = nativeT NT_Expr
556
    arrayT = nativeT NT_Array
557

Marc Coiffier's avatar
Marc Coiffier committed
558
559
560
561
562
563
564
newtype InstanceMap s a = InstanceMap (Map s (Map (Type s) a))
                        deriving (Eq,Ord,Generic,Semigroup,Monoid)
i'InstanceMap :: Iso (InstanceMap s a) (InstanceMap s' a') (Map s (Map (Type s) a)) (Map s' (Map (Type s') a'))
i'InstanceMap = iso InstanceMap (\(InstanceMap m) -> m)
instance Functor (InstanceMap s) where map f (InstanceMap m) = InstanceMap (map2 f m)
instance Foldable (InstanceMap s) where fold (InstanceMap m) = fold (map fold m)
instance Identifier s => Traversable (InstanceMap s) where sequence (InstanceMap m) = InstanceMap <$> traverse sequence m
565
566
instance (Identifier s,Serializable Bytes s,Serializable Bytes a) => Serializable Bytes (InstanceMap s a)
instance (Identifier s,Format Bytes s,Format Bytes a) => Format Bytes (InstanceMap s a)
Marc Coiffier's avatar
Marc Coiffier committed
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
instance (Identifier s,Identifier s') => HasIdents s s' (InstanceMap s a) (InstanceMap s' a) where
  ff'idents = from i'InstanceMap.i'ascList.each.
              (l'1 .+ l'2.i'ascList.each.l'1.ff'idents)

instance Identifier s => DataMap (InstanceMap s a) (s,Set Int,Type s) a where
  at (s,is,t) = from i'InstanceMap.mat s.at (mapTypeShapes f $ mapTypePaths g t)
    where f ps x | any keepPath ps = x
                 | otherwise = PolyType
          g (ImplicitRoot i,_) | i/=0 = Nothing
          g (ImplicitRoot 0,TypeIndex _ i:_) | not (i`isKeyIn`is) = Nothing
          g (TypeRoot,_:_) = Nothing
          g x = Just x
          keepPath (ImplicitRoot 0,[]) = True
          keepPath (ImplicitRoot 0,TypeIndex _ i:_) = i`isKeyIn`is
          keepPath _ = False
          
instance Identifier s => OrderedMap (InstanceMap s a) (s,Type s) a where
  ascList = from i'InstanceMap.ascList.mapping (mapping ascList)
            .iso (\l -> [((i,j),a) | (i,li) <- l, (j,a) <- li])
            (\l -> by ascList $ c'map $ fromMAList [(i,[(j,a)]) | ((i,j),a) <- l])
  nearest cmp (i,j) (InstanceMap m) = nearest cmp i m >>= \(i',m') -> nearest cmp j m' <&> \(j',a) -> ((i',j'),a)

isValidInstanceMap :: Identifier s => InstanceMap s a -> Bool
isValidInstanceMap (InstanceMap m) = Data.Map.valid m && all Data.Map.valid m