CaPriCon.hs 25.5 KB
Newer Older
1
2
3
{-# LANGUAGE UndecidableInstances, OverloadedStrings, NoMonomorphismRestriction, DeriveGeneric, ConstraintKinds #-}
module Data.CaPriCon(
  -- * Expression nodes
4
  IsCapriconString(..),BindType(..),Node(..),ApHead(..),Application(..),ContextNode(..),Env,COCExpression(..),
5
  -- ** Managing De Bruijin indices
6
  adjust_depth,adjust_telescope_depth,inc_depth,free_vars,is_free_in,
7
8
9
10
  -- ** Expression directories
  StringPattern,NodeDir(..),AHDir(..),ApDir,
  findPattern,freshContext,
  -- * Showing nodes
11
  ListBuilder(..),NodeDoc(..),doc2raw,doc2latex,showNode,showNode'
12
  ) where
13
14

import Definitive
15
16
import Language.Format
import GHC.Generics (Generic)
17

18
19
20
21
sequence2 :: (Applicative f,Traversable t,Traversable u) => t (u (f a)) -> f (t (u a))
sequence2 = sequence.map sequence
sequence3 :: (Applicative f,Traversable t,Traversable u,Traversable v) => t (u (v (f a))) -> f (t (u (v a)))
sequence3 = sequence.map sequence2
22

23
type FreeMap f a = Cofree f (Maybe a)
24
25
26
27
28
29
30
31
32
33
instance (Semigroup a, Semigroup (Coforest f a)) => Semigroup (Cofree f a) where
  Step a b + Step a' b' = Step (a+a') (b+b')
instance (Monoid a, Monoid (Coforest f a)) => Monoid (Cofree f a) where
  zero = Step zero zero
instance (DataMap (f (FreeMap f a)) k (FreeMap f a)) => DataMap (FreeMap f a) [k] a where
  at [] = lens (\(Step a _) -> a) (\(Step _ m) a -> Step a m)
  at (h:t) = coforest.at h.l'Just zero.at t
coforest :: Lens' (Cofree f a) (Coforest f a)
coforest = lens (\(Step _ m) -> m) (\(Step a _) m -> Step a m)

34
35
36
37
38
39
class (Ord str,Show str,Monoid str,Sequence str,IsString str) => IsCapriconString str where
  toString :: str -> String
instance IsCapriconString String where
  toString = id

type ListStream = [Word8]
40
41
42
43
44
45
46
47
newtype ListBuilder = ListBuilder (ListStream -> ListStream)
instance Semigroup ListBuilder where ListBuilder a + ListBuilder b = ListBuilder (a . b)
instance Monoid ListBuilder where zero = ListBuilder id
instance SerialStreamType ListStream where
  type StreamBuilder ListStream = ListBuilder
instance SerialStream ListStream where
  encodeByte _ b = ListBuilder (b:)
  toSerialStream (ListBuilder k) = k []
48
49

-- | Inductive types
50
51
type UniverseSize = Int
type SymbolRef = Int
52
53
data BindType = Lambda | Prod
              deriving (Show,Eq,Ord,Generic)
54
data Node str = Bind BindType str (NodeType str) (Node str)
55
              | Cons (Application str)
56
              | Universe UniverseSize
57
          deriving (Show,Generic)
58
59
type NodeType str = Node str
data ApHead str = Sym SymbolRef | Mu [(str,Node str,Node str)] [Node str] (Application str)
60
61
62
            deriving (Show,Generic)
data Application str = Ap (ApHead str) [Node str]
                 deriving (Show,Generic) 
63
type Env str = [(str,NodeType str)]
64

65
66
type ListSerializable a = (Serializable ListStream a)
type ListFormat a = (Format ListStream a)
67
68
69
70
71
72
73
74
75
instance ListSerializable BindType
instance ListFormat BindType
instance ListSerializable str => ListSerializable (Node str)
instance ListFormat str => ListFormat (Node str)
instance ListSerializable str => ListSerializable (ApHead str)
instance ListFormat str => ListFormat (ApHead str)
instance ListSerializable str => ListSerializable (Application str)
instance ListFormat str => ListFormat (Application str)

76
class Monad m => COCExpression str m e | e -> str where
77
  mkUniverse :: UniverseSize -> m e
78
79
  mkVariable :: str -> m e
  mkBind :: BindType -> e -> m e
80
  mkApply :: e -> e -> m e
81
82
  mkMu :: e -> m e
  checkType :: e -> m e
83
  conversionDelta :: e -> e -> m (UniverseSize,UniverseSize)
84
85
86
87

  substHyp :: str -> e -> m (e -> e,Env str)
  pullTerm :: e -> m e
  insertHypBefore :: Maybe str -> str -> e -> m (e -> e,Env str)
88
instance (IsCapriconString str,Monad m,MonadReader (Env str) m) => COCExpression str (MaybeT m) (Node str) where
89
  mkUniverse = pure . Universe
90
91
  mkVariable v = hypIndex v <&> \i -> Cons (Ap (Sym i) [])
  mkBind b e = ask >>= \case
92
    (x,tx):_ -> pure $ Bind b x tx e
93
    _ -> zero
94
  mkApply f x = return (subst f (Cons (Ap (Sym 0) [inc_depth 1 x])))
95
96
  mkMu e = do
    te <- checkType e
97
98
99
100
    mte <- mu_type te^.maybeT
    let args (Bind Prod _ tx e') = tx:args e'
        args _ = []
    return (subst e (Cons (Ap (Mu [] (args mte) (Ap (Sym 0) [])) [])))
101
102
  checkType e = type_of e^.maybeT
  conversionDelta a b = return (convertible a b)^.maybeT
103

104
105
106
107
  substHyp h x = do
    i <- hypIndex h
    lift $ do
      ctx <- ask
108
      return (substn x i,let (ch,ct) = splitAt i ctx in zipWith (\j -> second $ substn (inc_depth (negate (1+j)) x) (i-j-1)) [0..] ch+drop 1 ct)
109
110
111
112
113
114
115
116
117
118
  pullTerm = return
  insertHypBefore Nothing h th = lift $ do
    ctx <- ask
    return (inc_depth 1,(h,th):ctx)
  insertHypBefore (Just h) h' th' = do
    hi <- hypIndex h
    lift $ do
      ctx <- ask
      let adj i j = if i+j>=hi then j+1 else j
      return (
119
        adjust_depth (adj (-1)),
120
121
122
123
124
125
        foldr (\x k i -> case compare hi i of
                           LT -> x:k (i+1)
                           EQ -> second (adjust_depth (adj i)) x:(h',inc_depth (negate (hi+1)) th'):k (i+1)
                           GT -> second (adjust_depth (adj i)) x:k (i+1))
          (\_ -> []) ctx 0)

126
127
128
129
130
hypIndex :: (IsCapriconString str,MonadReader (Env str) m) => str -> MaybeT m Int
hypIndex h = ask >>= \l -> case [i | (i,x) <- zip [0..] l, fst x==h] of
  i:_ -> return i
  _ -> zero
    
131
data ContextNode str = ContextNode SymbolRef (Node str)
132
133
134
                     deriving (Show,Generic)
instance ListSerializable str => ListSerializable (ContextNode str)
instance ListFormat str => ListFormat (ContextNode str)
135
restrictEnv :: SymbolRef -> Env str -> Env str
136
restrictEnv n e = drop (length e-n) e
137

138
instance (IsCapriconString str,MonadReader (Env str) m,Monad m) => COCExpression str (MaybeT m) (ContextNode str) where
139
  mkUniverse u = ask >>= \ctx -> ContextNode (length ctx)<$>mkUniverse u
140
  mkVariable i = local (dropWhile ((/=i) . fst)) (ask >>= \ctx -> ContextNode (length ctx)<$>mkVariable i)
141
142
  mkBind t ce@(ContextNode de e) | de>0 = ContextNode (de-1) <$> local (restrictEnv de) (mkBind t e)
                                 | otherwise = return ce
143
144
145
146
  mkApply (ContextNode df f) (ContextNode dx x) = do
    let dm = max df dx
    ContextNode dm <$> mkApply (inc_depth (dm-df) f) (inc_depth (dm-dx) x)
  mkMu (ContextNode d e) = ContextNode d <$> local (restrictEnv d) (mkMu e)
147
148
  checkType (ContextNode d e) = ContextNode d <$> local (restrictEnv d) (checkType e)
  conversionDelta (ContextNode da a) (ContextNode db b) =
149
150
151
    let dm = max da db in
      local (restrictEnv dm)
      $ conversionDelta (inc_depth (dm-da) a) (inc_depth (dm-db) b)
152
153
154
155
156
157
  
  pullTerm (ContextNode d e) = ask <&> \l -> ContextNode (length l) (inc_depth (length l-d) e)
  substHyp h vh = do
    hi <- hypIndex h
    ContextNode dm vh' <- pullTerm vh
    first (\f cv@(ContextNode d v) ->
158
             if d+hi <= dm then cv
159
160
161
162
             else ContextNode (d-1) (inc_depth (d-dm) $ f $ inc_depth (dm-d) v)) <$>
      substHyp h vh'
  insertHypBefore h h' cth' = do
    ContextNode dh th' <- pullTerm cth'
163
164
    hi <- maybe (return (-1)) hypIndex h
    first (\f cx@(ContextNode d x) ->
165
             if d+hi < dh then cx
166
             else ContextNode (d+1) (inc_depth (d-dh) $ f $ inc_depth (dh-d) x))
167
            <$> insertHypBefore h h' th'
168

169
170
171
data NodeDir str a = NodeDir
  (Map BindType (NodeDir str (NodeDir str a)))
  (ApDir str a)
172
  (Map Int a)
173
174
  deriving (Eq,Ord,Show,Generic)
instance Functor (NodeDir str) where
175
  map f (NodeDir a b c) = NodeDir (map3 f a) (map3 f b) (map f c)
176
instance Foldable (NodeDir str) where
177
  fold (NodeDir a b c) = (fold.map fold.map2 fold) a + (fold.map fold.map2 fold) b + fold c
178
instance Traversable (NodeDir str) where
179
  sequence (NodeDir a b c) = NodeDir<$>sequence3 a<*>sequence3 b<*>sequence c
180
181

instance (Serializable ListStream str,Serializable ListStream a) => Serializable ListStream (Cofree (NodeDir str) a) where encode = encodeCofree
182
instance (ListSerializable str, ListSerializable a) => ListSerializable (NodeDir str a)
183
instance (Format ListStream str,Format ListStream a) => Format ListStream (Cofree (NodeDir str) a) where datum = datumCofree
184
instance (ListFormat str, ListFormat a) => ListFormat (NodeDir str a)
185

186
187
188
i'NodeDir :: Iso (NodeDir str a) (NodeDir str' a')
             ((,,) (Map BindType (NodeDir str (NodeDir str a)))
               (ApDir str a)
189
               (Map Int a))
190
191
             ((,,) (Map BindType (NodeDir str' (NodeDir str' a')))
               (ApDir str' a')
192
193
194
               (Map Int a'))
i'NodeDir = iso (\(x,y,z) -> NodeDir x y z) (\(NodeDir x y z) -> (x,y,z))

195
196
type ApDir str a = AHDir str (FreeMap (NodeDir str) a)
data AHDir str a = AHDir
197
  (Map Int a)
198
199
200
  (Map Int (ApDir str a))
  deriving (Eq,Ord,Show,Generic)
instance Functor (AHDir str) where
201
  map f (AHDir a b) = AHDir (map f a) ((map2.map2) f b)
202
instance Foldable (AHDir str) where
203
  fold (AHDir a b) = fold a + (fold.map fold.map2 fold.map3 fold) b
204
instance Traversable (AHDir str) where
205
  sequence (AHDir a b) = AHDir<$>sequence a<*>(sequence3.map3 sequence) b
206
207
208
209
210
instance (ListSerializable str, ListSerializable a) => ListSerializable (AHDir str a)
instance (ListFormat str, ListFormat a) => ListFormat (AHDir str a)
i'AHDir :: Iso (AHDir str a) (AHDir str' a')
           ((,) (Map Int a) (Map Int (ApDir str a)))
           ((,) (Map Int a') (Map Int (ApDir str' a')))
211
212
213
214
215
i'AHDir = iso (uncurry AHDir) (\(AHDir x y) -> (x,y))

i'Cofree :: Iso (Cofree f a) (Cofree f' a') (a,Coforest f a) (a',Coforest f' a')
i'Cofree = iso (uncurry Step) (\(Step x y) -> (x,y))

216
217
218
instance Semigroup (NodeDir str a) where NodeDir a b c + NodeDir a' b' c' = NodeDir (a+a') (b+b') (c+c')
instance Monoid (NodeDir str a) where zero = NodeDir zero zero zero
instance DataMap (NodeDir str a) (Node str) a where
219
220
221
222
  at (Bind t _ tx e) = from i'NodeDir.l'1.at t.l'Just zero.at tx.l'Just zero.at e
  at (Cons a) = from i'NodeDir.l'2.atAp a
  at (Universe u) = from i'NodeDir.l'3.at u

223
224
225
instance Semigroup (AHDir str a) where AHDir a b + AHDir a' b' = AHDir (a+a') (b+b')
instance Monoid (AHDir str a) where zero = AHDir zero zero
instance DataMap (AHDir str a) (ApHead str) a where
226
227
228
  at (Sym i) = from i'AHDir.l'1.at i
  at (Mu xs _ a) = from i'AHDir.l'2.at (length xs).l'Just zero.atAp a

229
type StringPattern str = [str :+: Int]
230

231
232
atAp :: Application str -> Lens' (ApDir str a) (Maybe a)
atAp (Ap h xs) = at h.l'Just zero.at xs
233
234
235
236
237
238
239

mayChoose (Just x) = return x
mayChoose Nothing = zero

(<++>) :: WriterT w [] a -> WriterT w [] a -> WriterT w [] a
a <++> b = a & from writerT %~ (+ b^..writerT)

240
findPattern :: NodeDir str a -> Node str -> [([([(str,Node str)],Int,Node str)],a)]
241
findPattern = \x y -> go [] x y^..writerT
242
243
244
  where go :: [(str,Node str)] -> NodeDir str a -> Node str -> WriterT [([(str,Node str)],Int,Node str)] [] a
        go_a :: [(str,Node str)] -> ApDir str a -> Application str -> WriterT [([(str,Node str)],Int,Node str)] [] a
        go_ah :: [(str,Node str)] -> AHDir str a -> ApHead str -> WriterT [([(str,Node str)],Int,Node str)] [] a
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
        withEnv env d x m = foldr (\(i,as) ma -> ma <++> (foldl'.foldl') (\l a -> (tell [(env,i-length env,x)] >> return a) <++> l) zero as)
                            m (d^??from i'NodeDir.l'2.from i'AHDir.l'1.ascList.each.sat ((>=length env) . fst))
        go env d wh@(Bind t x tx e) = withEnv env d wh $ do
          d' <- mayChoose (d^.from i'NodeDir.l'1.at t)
          d'' <- go env d' tx
          go ((x,tx):env) d'' e
        go env d wh@(Cons a) = withEnv env d wh $ go_a env (d^.from i'NodeDir.l'2) a
        go env d wh@(Universe u) = withEnv env d wh $ mayChoose (d^.from i'NodeDir.l'3.at u)

        go_a env d (Ap ah xs) = do
          d' <- go_ah env d ah
          foldr
            (\x ma d'' -> ma =<< go env (d''^.from i'Cofree.l'2) x)
            (\d''' -> mayChoose (d'''^.from i'Cofree.l'1))
            xs d' 

        go_ah env d (Sym i) | i<length env = mayChoose (d^.from i'AHDir.l'1.at i)
                            | otherwise = []^.writerT
        go_ah env d (Mu tenv _ a) = do
          d' <- mayChoose (d^.from i'AHDir.l'2.at (length tenv))
          go_a env d' a

-- `adjust_depth f e` produces an expression `e'` whose variables (de
-- Bruijin indices) are adjusted from `e` by the function `f`.
--
-- `f` takes two arguments `i` and `d`, where `i` is the previous
-- variable depth, and `d` is the current depth of the considered node
-- (the number of binders between the top-level and the node in
-- question).
--
275
 -- For example, `adjust_depth (\i d -> i-d+1) (Bind Lambda "x" (Universe 0) (Cons (Ap (Sym 1) [])))
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
--               == Bind Lambda "x" (Universe 0) (Cons (Ap (Sym 2) []))`

adjust_depth f = go 0
  where go d (Bind t x tx e) = Bind t x (go d tx) (go (d+1) e)
        go _ (Universe u) = Universe u
        go d (Cons a) = Cons (go_a d a)
        go_a d (Ap (Sym i) subs) | i<d = Ap (Sym i) (map (go d) subs)
                                 | otherwise = Ap (Sym (d+f (i-d))) (map (go d) subs)
        go_a d (Ap (Mu env t a') subs) = Ap (Mu
                                            (reverse $ zipWith (\i (x,tx,tx') -> (x,go (d+i) tx,go (d+i) tx')) [0..] (reverse env))
                                            (zipWith (\i -> go (d+length env+i)) [0..] t)
                                            (go_a (d+length env) a')) (map (go d) subs)
inc_depth 0 = \x -> x
inc_depth dx = adjust_depth (+dx)
adjust_telescope_depth field f = zipWith (field . adjust_depth . \i j -> if j<i then j else i+f (j-i)) [0..]
291
free_vars :: Node str -> Set Int
292
293
294
295
296
297
298
299
free_vars (Bind _ _ tx e) = free_vars tx + delete (-1) (map (subtract 1) (free_vars e))
free_vars (Cons a) = freeA a
  where freeA (Ap (Sym i) xs) = singleton' i + foldMap free_vars xs
        freeA (Ap (Mu env _ a') xs) = foldMap free_vars xs +
          map (subtract envS) (freeA a' - fromKList [0..envS-1])
          where envS = length env
free_vars _ = zero

300
301
302
303
304
305
306
307
is_free_in :: Int -> Node str -> Bool
is_free_in = map2 not go
  where go v (Bind _ _ t e) = go v t && go (v+1) e
        go v (Cons a) = go_a v a
        go _ (Universe _) = True
        go_a v (Ap (Sym v') subs) = v/=v' && all (go v) subs
        go_a v (Ap (Mu env _ a) subs) = go_a (v+length env) a && all (go v) subs

308
subst :: Show str => Node str -> Node str -> Node str
309
subst = flip substn 0
310
substn :: Show str => Node str -> Int -> Node str -> Node str
311
substn val n | n>=0 = getId . go n
312
313
314
             | otherwise = error "'subst' should not be called with a negative index"
  where go d (Bind t x tx e) = do
          tx' <- go d tx
315
          Bind t x tx' <$> go (d+1) e
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
        go _ (Universe u) = pure (Universe u)
        go d (Cons a) = go_a d a

        go_a d (Ap (Sym i) xs) = traverse (go d) xs >>= \xs' ->
          case compare i d of
            EQ -> rec_subst xs' (inc_depth d val)
            LT -> return $ Cons $ Ap (Sym i) xs'
            GT -> return $ Cons $ Ap (Sym (i-1)) xs'
        go_a d (Ap (Mu e t a) xs) = do
          x <- go_a (d+length e) a
          xs' <- traverse (go d) xs
          e' <- sequence $ reverse $ zipWith (\d' (y,ty,ty') -> liftA2 (y,,) (go (d+d') ty) (go (d+d') ty'))
                [0..] (reverse e)
          t' <- sequence $ zipWith (\d' -> go (d+d')) [length e..] t
          case x of
            Cons a' -> return (Cons (Ap (Mu e' t' a') xs'))
            _ -> rec_subst xs' =<< go_mu d e' t' x
  
        go_mu d env (tx':t) (Bind Lambda x tx e) = go_mu d ((x,tx,tx'):env) t e
        go_mu _ env _ (Cons (Ap (Sym i) xs))
          | i < length env = do
              let envS = length env
                  muEnv = reverse $ map (by l'3) env
              a' <- Cons . Ap (Sym i) <$>
                sequence (fold [if nonempty (free_vars x - fromKList [0..envS-1])
                                then [ return $ inc_depth envS $ foldl' (\e (x',tx,_) -> Bind Lambda x' tx e) x env
342
                                     , return $ subst x (Cons (Ap (Mu [] muEnv (Ap (Sym 0) [])) [Cons (Ap (Sym j) []) | j <- reverse [1..envS]]))]
343
344
345
346
                                else [return x]
                               | x <- xs])
              return $ foldl' (\e (x,_,tx) -> Bind Lambda x tx e) a' env
        go_mu _ e t (Cons a) = return $ Cons (Ap (Mu e t a) [])
347
        go_mu _ _ _ x' = error $ "Cannot produce an induction principle for a term : "+show x'
348

349
        rec_subst (y:t) (Bind Lambda _ _ e) = rec_subst t (subst y e)
350
351
        rec_subst xs (Cons (Ap h hxs)) = return (Cons (Ap h (hxs+xs)))
        rec_subst [] x = return x
352
        rec_subst _ x = error $ "Invalid substitution of non-lambda expression : "+show x
353

354
fresh env v = head $ select (not . (`elem` env)) (v:[v+fromString (show i) | i <- [0..]])
355
356
357
freshContext = go []
  where go env ((n,v):t) = let n' = fresh env n in (n',(n,v)):go (n':env) t
        go _ [] = []
358

359
360
361
362
363
data NodeDoc str = DocSeq [NodeDoc str]
                 | DocParen (NodeDoc str)
                 | DocMu (NodeDoc str)
                 | DocSubscript (NodeDoc str) (NodeDoc str)
                 | DocAssoc str (NodeDoc str)
364
                 | DocVarName str
365
366
367
368
369
370
371
                 | DocText str
                 | DocArrow
                 | DocSpace
                 deriving Show
par lvl d msg | d>lvl = DocParen msg
              | otherwise = msg

372
373
374
375
376
377
378
instance Functor NodeDoc where
  map f (DocSeq l) = DocSeq (map2 f l)
  map f (DocParen x) = DocParen (map f x)
  map f (DocMu x) = DocMu (map f x)
  map f (DocSubscript x y) = DocSubscript (map f x) (map f y)
  map f (DocAssoc v x) = DocAssoc (f v) (map f x)
  map f (DocText x) = DocText (f x)
379
  map f (DocVarName x) = DocVarName (f x)
380
381
  map _ DocArrow = DocArrow
  map _ DocSpace = DocSpace
382
383
384
385
386
387
388
389
390
391
instance IsString str => IsString (NodeDoc str) where fromString = DocText . fromString

doc2raw :: IsCapriconString str => NodeDoc str -> str
doc2raw (DocSeq l) = fold (map doc2raw l)
doc2raw (DocParen p) = "("+doc2raw p+")"
doc2raw (DocMu m) = "μ("+doc2raw m+")"
doc2raw (DocSubscript v x) = doc2raw v+doc2raw x
doc2raw (DocAssoc x v) = "("+x+" : "+doc2raw v+")"
doc2raw DocArrow = " -> "
doc2raw (DocText x) = x
392
doc2raw (DocVarName x) = x
393
394
395
396
397
398
399
doc2raw DocSpace = " "

doc2latex :: IsCapriconString str => NodeDoc str -> str
doc2latex (DocSeq l) = fold (map doc2latex l)
doc2latex (DocParen p) = "("+doc2latex p+")"
doc2latex (DocMu m) = "\\mu("+doc2latex m+")"
doc2latex (DocSubscript v x) = doc2latex v+"_{"+doc2latex x+"}"
400
doc2latex (DocAssoc x v) = "(\\mathit{"+latexName x+"}:"+doc2latex v+")"
401
doc2latex DocArrow = " \\rightarrow "
402
doc2latex (DocText x) = x
403
doc2latex (DocVarName x) = "\\mathrm{"+latexName x+"}"
404
405
doc2latex DocSpace = "\\,"

406
407
latexName :: IsCapriconString str => str -> str
latexName s = fromString $ go $ toString s
408
  where go ('.':t) = go t+"}^{*"
409
410
        go x = x

411
showNode = showNode' zero
412
showNode' :: IsCapriconString str => NodeDir str ([str],StringPattern str) -> [(str,Node str)] -> Node str -> NodeDoc str
413
showNode' dir = go 0
414
  where go d env x | Just ret <- toPat d env x = ret
415
416
417
        go _ _ (Universe u) = DocSubscript "Set" (fromString (show u))
        go d env whole@(Bind t aname atype body) | t == Lambda || 0`is_free_in`body = par 0 d $ DocSeq (DocText (bind_head t):drop 1 (bind_tail env whole))
                                                 | otherwise = par 0 d $ DocSeq [go 1 env atype,DocArrow,go 0 ((aname,atype):env) body]
418
419
          where bind_head Lambda = "λ"
                bind_head Prod = "∀"
420
421
                bind_sep Prod = "," ; bind_sep Lambda = "."
                bind_tail env' x | Just ret <- toPat 0 (env'+env) x = [bind_sep t,DocSpace,ret]
422
                bind_tail env' (Bind t' x tx e) | t==t' && (t==Lambda || 0`is_free_in`e) =
423
                                                    [DocSpace,DocAssoc x' (go 0 env' tx)] + bind_tail ((x',tx):env') e
424
                  where x' = fresh (map fst env') x
425
                bind_tail env' x = [bind_sep t,DocSpace,go 0 env' x]
426
427
428
        go d env (Cons a) = showA d a
          where showA _ (Ap h xs) =
                  let ni = case h of
429
                             Sym i -> DocVarName $ case drop i env of
430
431
432
                               (h',_):_ -> h'
                               _ -> "#"+fromString (show i)
                             Mu _ _ a' -> DocMu (showA 0 a')
433
                      lvl = if empty xs then 1000 else 1
434
                  in par lvl d $ DocSeq $ intercalate [DocSpace] $ map pure (ni:map (go 2 env) xs)
435

436
437
438
        toPat d env x
          | (pats,(_,k)):_ <- findPattern dir x =
              let holes = c'map $ fromAList [(i,(env',hole)) | (env',i,hole) <- pats] in
439
                Just $ par (if all (has t'1) k then 1000 else 1 :: Int) d $ DocSeq $ intercalate [DocSpace] $ map pure $
440
                [case word of
441
                   Left w -> DocText w
442
443
444
445
446
                   Right i | Just (env',hole) <- lookup i holes ->
                               go 2 env $
                               let (hole',env'') =
                                     fix (\kj -> \case
                                             (Cons (Ap h t@(_:_)),_:env0)
447
                                               | Cons (Ap (Sym 0) []) <- last t
448
449
450
451
452
                                               , not (is_free_in 0 (Cons (Ap h (init t))))
                                                 -> kj (inc_depth (-1) (Cons (Ap h (init t))),env0)
                                             (Cons (Ap (Sym j') []),_:env0) | j'>0 -> kj (Cons (Ap (Sym (j'-1)) []),env0)
                                             e -> e) (hole,env')
                               in foldl' (\e (n,t) -> Bind Lambda n t e) hole' env''
453
                           | otherwise -> DocText "?"
454
455
456
                | word <- k]
          | otherwise = Nothing

457
type_of :: (IsCapriconString str,MonadReader (Env str) m) => Node str -> m (Maybe (Node str))
458
type_of = yb maybeT . go
459
460
  where go (Bind Lambda x tx e) = Bind Prod x tx <$> local ((x,tx):) (go e)
        go (Bind Prod x tx e) = do
461
          a <- go tx
462
          b <- local ((x,tx):) $ go e
463
464
465
466
467
468
469
470
          case (a,b) of
            (Universe ua,Universe ub) -> return (Universe (max ua ub))
            _ -> zero
        go (Universe u) = return (Universe (u+1))
        go (Cons a) = go' a
          where go' (Ap (Sym i) subs) = do
                  e <- ask
                  case drop i e of
471
                    (_,ti):_ -> rec_subst subs (inc_depth (i+1) ti)
472
473
                    _ -> zero
                go' (Ap (Mu env _ a') subs) = do
474
                  ta <- local (map (\(x,tx,_) -> (x,tx)) env +) (go' a')
475
                  preret <- maybeT $^ mu_type $ foldl' (\e (x,tx,_) -> Bind Prod x tx e) ta env
476
                  rec_subst subs (subst (Cons a') preret)
477
                      
478
                rec_subst (y:t) (Bind Prod _ _ e) = rec_subst t (subst y e)
479
480
481
                rec_subst [] x = return x
                rec_subst _ _ = zero

482
mu_type :: MonadReader (Env str) m => Node str -> m (Maybe (Node str))
483
484
485
486
487
488
489
490
491
492
493
mu_type (inc_depth 1 -> root_type) = yb maybeT $ go 0 root_type
  where
    root_args = go' root_type
      where go' (Bind Prod x tx e) = (x,tx):go' e
            go' _ = []
    nargs = length root_args
    bind t = flip $ foldr (\(x,tx) e -> Bind t x tx e) 
    constr_ind d d' i = d' <= i && i < d+d'

    go d (Bind Prod x tx e) = do
      tx' <- go_col d x tx
494
      e' <- local ((x,tx):) (go (d+1) e)
495
496
497
498
499
500
501
502
503
504
      return (Bind Prod x tx' e')
    go _ (Cons (Ap (Sym i) args)) = return $ Cons (Ap (Sym i) $ args + [Cons (Ap (Sym nargs) [])])
    go _ _ = zero

    go_col d xn = go_col' 0 (c'set zero)
      where go_col' d' recs (Bind Prod x tx@(Cons (Ap (Sym i) subs)) e)
              | constr_ind d d' i = do
                  let tx' = bind Prod (adjust_telescope_depth second (+(d+d')) root_args)
                            (adjust_depth (\i' -> if constr_ind d d' i' then (i'-d')+(nargs-d) else i'+nargs) tx)
                      tIx = Cons $ Ap (Sym (i+1)) $ map (inc_depth 1) subs + [Cons (Ap (Sym 0) [])]
505
506
                  e' <- local (((x,tx):) . (undefined:)) (go_col' (d'+2) (touch (1 :: Int) (map (+2) recs))
                                                          (adjust_depth (\j -> if j==0 then j else j+1) e))
507
                  return $ Bind Prod x tx' (Bind Prod x tIx e')
508
            go_col' d' recs (Bind Prod x tx e) = Bind Prod x tx <$> local ((x,tx):) (go_col' (d'+1) (map (+1) recs) e)
509
510
            go_col' d' recs (Cons (Ap (Sym i) xs))
              | constr_ind d d' i = do
511
                  let args = reverse $ select (not . (`isKeyIn`recs)) [0..d'-1]
512
513
514
515
516
517
518
519
520
521
522
523
524
525
                      lastE = bind Lambda (adjust_telescope_depth second (+(d+d')) root_args)
                              (Cons (Ap (Sym (nargs-d-1))
                                     [Cons (Ap (Sym (j'+nargs)) args')
                                     | j <- args
                                     , let (j',args') | (j+1)`isKeyIn`recs = (j+1,[Cons (Ap (Sym k) []) | k <- reverse [0..nargs-1]])
                                                      | otherwise = (j,[])
                                     ]))
                  return $ Cons (Ap (Sym i) $ xs+[lastE])
                  
            go_col' d' _ (Universe u) = do
              let tIH = bind Prod (adjust_telescope_depth second (+(d+d')) root_args) ihRoot
                  ihRoot = Cons (Ap (Sym (nargs-d-1)) [Cons (Ap (Sym (j+nargs)) []) | j <- reverse [0..d'-1]])
              return $ Bind Prod xn tIH (Universe (u+1))
            go_col' _ _ _ = zero
526

527
528
convertible :: Node str -> Node str -> Maybe (Int,Int)
convertible = \x y -> map ((getMax<#>getMax) . fst) ((tell (Max 0,Max 0) >> go False x y)^..writerT)
529
530
  where go inv (Bind b _ tx e) (Bind b' _ tx' e') = guard (b==b') >> go (not inv) tx tx' >> go inv e e'
        go inv (Cons ax) (Cons ay) = go_a inv ax ay
531
        go inv (Universe u) (Universe v) | u>v = tellInv inv (Max (u-v),zero)
532
533
534
535
536
537
538
539
540
541
542
                                         | otherwise = return ()
        go _ _ _ = lift Nothing
        
        go_a inv (Ap hi ai) (Ap hj aj) = go_ah inv hi hj >> sequence_ (zipWith (go inv) ai aj)
  
        go_ah _ (Sym i) (Sym j) | i==j = return ()
        go_ah inv (Mu _ _ x) (Mu _ _ y) = go_a inv x y
        go_ah _ _ _ = lift Nothing
        
        tellInv True (x,y) = tell (y,x)
        tellInv False (x,y) = tell (x,y)