{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Drawing a term as an SVG diagram of a cube.
--
-- The geometry lives in "Rzk.Render.Geometry"; what is here is the part that
-- knows about terms: which subshape of the cube a tope carves out, which term
-- inhabits each of them, and what to label it with.
module Rzk.TypeCheck.Render where

import           Control.Monad            (forM)
import           Control.Monad.Reader     (asks)
import           Data.List                (intercalate, (\\))
import           Data.Maybe               (catMaybes)

import           Control.Monad.Foil       (Distinct)
import qualified Control.Monad.Foil       as Foil
import           Control.Monad.Free.Foil  (AST (Var))

import           Language.Rzk.Foil.Syntax
import           Language.Rzk.Foil.Names (Binder (..), TModality (..),
                                           binderName)
import           Rzk.Render.Geometry
import           Rzk.TypeCheck.Context
import           Rzk.TypeCheck.Display
import           Rzk.TypeCheck.Eval
import           Rzk.TypeCheck.Monad

-- * The subshapes of a cube

cube2powerT :: Int -> TermT n
cube2powerT :: forall (n :: S). Int -> TermT n
cube2powerT Int
1   = TermT n
forall (n :: S). TermT n
cube2T
cube2powerT Int
dim = TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
cubeProductT (Int -> TermT n
forall (n :: S). Int -> TermT n
cube2powerT (Int
dim Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) TermT n
forall (n :: S). TermT n
cube2T

splits :: [a] -> [([a], [a])]
splits :: forall a. [a] -> [([a], [a])]
splits [] = [([], [])]
splits (a
x:[a]
xs) = ([], a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) ([a], [a]) -> [([a], [a])] -> [([a], [a])]
forall a. a -> [a] -> [a]
: [ (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
before, [a]
after) | ([a]
before, [a]
after) <- [a] -> [([a], [a])]
forall a. [a] -> [([a], [a])]
splits [a]
xs ]

verticesFrom :: [TermT n] -> [(ShapeId, TermT n)]
verticesFrom :: forall (n :: S). [TermT n] -> [(ShapeId, TermT n)]
verticesFrom [TermT n]
ts = [(String, TermT n)] -> (ShapeId, TermT n)
forall {a} {n :: S}. [([a], TermT n)] -> ([[a]], TermT n)
combine ([(String, TermT n)] -> (ShapeId, TermT n))
-> [[(String, TermT n)]] -> [(ShapeId, TermT n)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TermT n -> [(String, TermT n)])
-> [TermT n] -> [[(String, TermT n)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TermT n -> [(String, TermT n)]
forall {a} {n :: S}. IsString a => TermT n -> [(a, TermT n)]
mk [TermT n]
ts
  where
    mk :: TermT n -> [(a, TermT n)]
mk TermT n
t = [(a
"0", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t TermT n
forall (n :: S). TermT n
cube2_0T), (a
"1", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t TermT n
forall (n :: S). TermT n
cube2_1T)]
    combine :: [([a], TermT n)] -> ([[a]], TermT n)
combine [([a], TermT n)]
xs = ([[[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((([a], TermT n) -> [a]) -> [([a], TermT n)] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map ([a], TermT n) -> [a]
forall a b. (a, b) -> a
fst [([a], TermT n)]
xs)], (TermT n -> TermT n -> TermT n) -> [TermT n] -> TermT n
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeAndT ((([a], TermT n) -> TermT n) -> [([a], TermT n)] -> [TermT n]
forall a b. (a -> b) -> [a] -> [b]
map ([a], TermT n) -> TermT n
forall a b. (a, b) -> b
snd [([a], TermT n)]
xs))

subTopes2 :: Int -> TermT n -> [(ShapeId, TermT n)]
-- 1-dim
subTopes2 :: forall (n :: S). Int -> TermT n -> [(ShapeId, TermT n)]
subTopes2 Int
1 TermT n
t =
  [ (String -> ShapeId
words String
"0", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"1", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"0 1", TermT n
forall (n :: S). TermT n
topeTopT) ]
-- 2-dim
subTopes2 Int
2 TermT n
ts =
  -- vertices
  [ (String -> ShapeId
words String
"00", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
s TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"01", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
s TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"10", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
s TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"11", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
s TermT n
forall (n :: S). TermT n
cube2_1T)
  -- edges and the diagonal
  , (String -> ShapeId
words String
"00 01", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"10 11", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"00 10", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
s TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"01 11", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
s TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"00 11", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
s TermT n
t)
  -- triangles
  , (String -> ShapeId
words String
"00 01 11", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t TermT n
s)
  , (String -> ShapeId
words String
"00 10 11", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
s TermT n
t)
  ]
  where
    t :: TermT n
t = TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT TermT n
forall (n :: S). TermT n
cube2T TermT n
ts
    s :: TermT n
s = TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
secondT TermT n
forall (n :: S). TermT n
cube2T TermT n
ts
-- 3-dim
subTopes2 Int
3 TermT n
t =
  -- vertices
  [ (String -> ShapeId
words String
"000", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"001", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"010", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"011", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"100", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"101", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"110", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_1T)
  -- edges
  , (String -> ShapeId
words String
"000 001", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"010 011", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"000 010", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"001 011", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"100 101", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"110 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"100 110", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"101 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"000 100", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"001 101", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_1T)
  , (String -> ShapeId
words String
"010 110", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_0T)
  , (String -> ShapeId
words String
"011 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_1T)
  -- face diagonals
  , (String -> ShapeId
words String
"000 011", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
t3)
  , (String -> ShapeId
words String
"100 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
t3)
  , (String -> ShapeId
words String
"000 101", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
t3)
  , (String -> ShapeId
words String
"010 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
t3)
  , (String -> ShapeId
words String
"000 110", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
t2)
  , (String -> ShapeId
words String
"001 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
t2)
  -- the long diagonal
  , (String -> ShapeId
words String
"000 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
t2 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
t1)
  -- face triangles
  , (String -> ShapeId
words String
"000 001 011", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t2 TermT n
t3)
  , (String -> ShapeId
words String
"000 010 011", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t3 TermT n
t2)
  , (String -> ShapeId
words String
"100 101 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t2 TermT n
t3)
  , (String -> ShapeId
words String
"100 110 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t3 TermT n
t2)
  , (String -> ShapeId
words String
"000 001 101", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t1 TermT n
t3)
  , (String -> ShapeId
words String
"000 100 101", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t3 TermT n
t1)
  , (String -> ShapeId
words String
"010 011 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t1 TermT n
t3)
  , (String -> ShapeId
words String
"010 110 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t3 TermT n
t1)
  , (String -> ShapeId
words String
"000 010 110", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t1 TermT n
t2)
  , (String -> ShapeId
words String
"000 100 110", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_0T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t2 TermT n
t1)
  , (String -> ShapeId
words String
"001 011 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t1 TermT n
t2)
  , (String -> ShapeId
words String
"001 101 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t3 TermT n
forall (n :: S). TermT n
cube2_1T TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t2 TermT n
t1)
  -- diagonal triangles
  , (String -> ShapeId
words String
"000 001 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
t2 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t2 TermT n
t3)
  , (String -> ShapeId
words String
"000 010 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
t3 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t1 TermT n
t2)
  , (String -> ShapeId
words String
"000 100 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
t3 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t2 TermT n
t1)
  , (String -> ShapeId
words String
"000 011 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t1 TermT n
t2 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t2 TermT n
t3)
  , (String -> ShapeId
words String
"000 101 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t2 TermT n
t1 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
t3)
  , (String -> ShapeId
words String
"000 110 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t3 TermT n
t1 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t1 TermT n
t2)
  -- tetrahedra
  , (String -> ShapeId
words String
"000 001 011 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t1 TermT n
t2 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t2 TermT n
t3)
  , (String -> ShapeId
words String
"000 010 011 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t1 TermT n
t3 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t3 TermT n
t2)
  , (String -> ShapeId
words String
"000 001 101 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t2 TermT n
t1 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t1 TermT n
t3)
  , (String -> ShapeId
words String
"000 100 101 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t2 TermT n
t3 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t3 TermT n
t1)
  , (String -> ShapeId
words String
"000 010 110 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t3 TermT n
t1 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t1 TermT n
t2)
  , (String -> ShapeId
words String
"000 100 110 111", TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t3 TermT n
t2 TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
`topeAndT` TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeLEQT TermT n
t2 TermT n
t1)
  ]
  where
    t1 :: TermT n
t1 = TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT  TermT n
forall (n :: S). TermT n
cube2T (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT (Int -> TermT n
forall (n :: S). Int -> TermT n
cube2powerT Int
2) TermT n
t)
    t2 :: TermT n
t2 = TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
secondT TermT n
forall (n :: S). TermT n
cube2T (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT (Int -> TermT n
forall (n :: S). Int -> TermT n
cube2powerT Int
2) TermT n
t)
    t3 :: TermT n
t3 = TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
secondT TermT n
forall (n :: S). TermT n
cube2T TermT n
t
subTopes2 Int
dim TermT n
_ = String -> [(ShapeId, TermT n)]
forall a. HasCallStack => String -> a
error (Int -> String
forall a. Show a => a -> String
show Int
dim String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" dimensions are not supported")

componentWiseEQT :: Int -> TermT n -> TermT n -> TermT n
componentWiseEQT :: forall (n :: S). Int -> TermT n -> TermT n -> TermT n
componentWiseEQT Int
1 TermT n
t TermT n
s = TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeEQT TermT n
t TermT n
s
componentWiseEQT Int
2 TermT n
t TermT n
s = TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeAndT
  (Int -> TermT n -> TermT n -> TermT n
forall (n :: S). Int -> TermT n -> TermT n -> TermT n
componentWiseEQT Int
1 (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT  TermT n
forall (n :: S). TermT n
cube2T TermT n
t) (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT  TermT n
forall (n :: S). TermT n
cube2T TermT n
s))
  (Int -> TermT n -> TermT n -> TermT n
forall (n :: S). Int -> TermT n -> TermT n -> TermT n
componentWiseEQT Int
1 (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
secondT TermT n
forall (n :: S). TermT n
cube2T TermT n
t) (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
secondT TermT n
forall (n :: S). TermT n
cube2T TermT n
s))
componentWiseEQT Int
3 TermT n
t TermT n
s = TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeAndT
  (Int -> TermT n -> TermT n -> TermT n
forall (n :: S). Int -> TermT n -> TermT n -> TermT n
componentWiseEQT Int
2 (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT  (Int -> TermT n
forall (n :: S). Int -> TermT n
cube2powerT Int
2) TermT n
t) (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT (Int -> TermT n
forall (n :: S). Int -> TermT n
cube2powerT Int
2) TermT n
s))
  (Int -> TermT n -> TermT n -> TermT n
forall (n :: S). Int -> TermT n -> TermT n -> TermT n
componentWiseEQT Int
1 (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
secondT TermT n
forall (n :: S). TermT n
cube2T TermT n
t) (TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
secondT TermT n
forall (n :: S). TermT n
cube2T TermT n
s))
componentWiseEQT Int
dim TermT n
_ TermT n
_ = String -> TermT n
forall a. HasCallStack => String -> a
error (String
"cannot work with " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
dim String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" dimensions")
-- * Rendering

-- | Is the variable an anonymous one (written @_@)? Its cells are left
-- unlabelled.
isAnonymous :: Foil.Name n -> TypeCheck n Bool
isAnonymous :: forall (n :: S). Name n -> TypeCheck n Bool
isAnonymous Name n
x = (Context n -> Bool)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Maybe VarIdent -> Maybe VarIdent -> Bool
forall a. Eq a => a -> a -> Bool
== VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
"_") (Maybe VarIdent -> Bool)
-> (Context n -> Maybe VarIdent) -> Context n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder -> Maybe VarIdent
binderName (Binder -> Maybe VarIdent)
-> (Context n -> Binder) -> Context n -> Maybe VarIdent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig (VarInfo n -> Binder)
-> (Context n -> VarInfo n) -> Context n -> Binder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name n -> Context n -> VarInfo n
forall (n :: S). Name n -> Context n -> VarInfo n
lookupVarInfo Name n
x)

-- | Render a term in the current context.
ppInContext :: TermT n -> TypeCheck n String
ppInContext :: forall (n :: S). TermT n -> TypeCheck n String
ppInContext TermT n
t = do
  naming <- (Context n -> Naming n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Naming n)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Context n -> Naming n
forall (n :: S). Context n -> Naming n
namingOfContext
  pure (ppTerm naming (untyped t))

renderObjectsFor
  :: Distinct n
  => String -> Int -> TermT n -> TermT n
  -> TypeCheck n [(ShapeId, RenderObjectData)]
renderObjectsFor :: forall (n :: S).
Distinct n =>
String
-> Int
-> TermT n
-> TermT n
-> TypeCheck n [(ShapeId, RenderObjectData)]
renderObjectsFor String
mainColor Int
dim TermT n
t TermT n
term = ([Maybe (ShapeId, RenderObjectData)]
 -> [(ShapeId, RenderObjectData)])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Maybe (ShapeId, RenderObjectData)]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(ShapeId, RenderObjectData)]
forall a b.
(a -> b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe (ShapeId, RenderObjectData)]
-> [(ShapeId, RenderObjectData)]
forall a. [Maybe a] -> [a]
catMaybes (ReaderT
   (Context n)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   [Maybe (ShapeId, RenderObjectData)]
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [(ShapeId, RenderObjectData)])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Maybe (ShapeId, RenderObjectData)]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(ShapeId, RenderObjectData)]
forall a b. (a -> b) -> a -> b
$
  [(ShapeId, TermT n)]
-> ((ShapeId, TermT n)
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (ShapeId, RenderObjectData)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Maybe (ShapeId, RenderObjectData)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Int -> TermT n -> [(ShapeId, TermT n)]
forall (n :: S). Int -> TermT n -> [(ShapeId, TermT n)]
subTopes2 Int
dim TermT n
t) (((ShapeId, TermT n)
  -> ReaderT
       (Context n)
       (ExceptT TypeErrorInScopedContext (State CheckLog))
       (Maybe (ShapeId, RenderObjectData)))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [Maybe (ShapeId, RenderObjectData)])
-> ((ShapeId, TermT n)
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (ShapeId, RenderObjectData)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Maybe (ShapeId, RenderObjectData)]
forall a b. (a -> b) -> a -> b
$ \(ShapeId
shapeId, TermT n
tope) ->
    TermT n -> TypeCheck n Bool
forall (n :: S). Distinct n => TermT n -> TypeCheck n Bool
checkTopeEntails TermT n
tope TypeCheck n Bool
-> (Bool
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (ShapeId, RenderObjectData)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
False -> Maybe (ShapeId, RenderObjectData)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (ShapeId, RenderObjectData)
forall a. Maybe a
Nothing
      Bool
True -> TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
term TypeCheck n (TermT n)
-> (TermT n
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (ShapeId, RenderObjectData)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        UniverseTopeT{} -> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
forall (n :: S) a.
Distinct n =>
TermT n -> TypeCheck n a -> TypeCheck n a
localTope TermT n
term (ReaderT
   (Context n)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   (Maybe (ShapeId, RenderObjectData))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (ShapeId, RenderObjectData)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
forall a b. (a -> b) -> a -> b
$ TermT n -> TypeCheck n Bool
forall (n :: S). Distinct n => TermT n -> TypeCheck n Bool
checkTopeEntails TermT n
tope TypeCheck n Bool
-> (Bool
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (ShapeId, RenderObjectData)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Bool
False -> Maybe (ShapeId, RenderObjectData)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (ShapeId, RenderObjectData)
forall a. Maybe a
Nothing
          Bool
True -> Maybe (ShapeId, RenderObjectData)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (ShapeId, RenderObjectData)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe (ShapeId, RenderObjectData)))
-> Maybe (ShapeId, RenderObjectData)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
forall a b. (a -> b) -> a -> b
$ (ShapeId, RenderObjectData) -> Maybe (ShapeId, RenderObjectData)
forall a. a -> Maybe a
Just (ShapeId
shapeId, RenderObjectData
            { renderObjectDataLabel :: String
renderObjectDataLabel = String
""
            , renderObjectDataFullLabel :: String
renderObjectDataFullLabel = String
""
            , renderObjectDataColor :: String
renderObjectDataColor = String
"orange"  -- FIXME: orange for topes?
            })
        TermT n
_ -> do
          term' <- TermT n -> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall (n :: S) a.
Distinct n =>
TermT n -> TypeCheck n a -> TypeCheck n a
localTope TermT n
tope (TypeCheck n (TermT n) -> TypeCheck n (TermT n))
-> TypeCheck n (TermT n) -> TypeCheck n (TermT n)
forall a b. (a -> b) -> a -> b
$ TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
term
          let argIsOfT TermT n
arg =
                [Name n] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TermT n -> [Name n]
forall (n :: S). TermT n -> [Name n]
freeVarsOfTermT TermT n
arg [Name n] -> [Name n] -> [Name n]
forall a. Eq a => [a] -> [a] -> [a]
\\ TermT n -> [Name n]
forall (n :: S). TermT n -> [Name n]
freeVarsOfTermT TermT n
t)
          label <- case term' of
            AppT TypeInfo (TermT n)
_ (Var Name n
z) TermT n
arg -> Name n -> TypeCheck n Bool
forall (n :: S). Name n -> TypeCheck n Bool
isAnonymous Name n
z TypeCheck n Bool
-> (Bool
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         String)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Bool
True -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
""
              Bool
False
                | TermT n -> Bool
argIsOfT TermT n
arg -> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall (n :: S). TermT n -> TypeCheck n String
ppInContext (Name n -> TermT n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
z)
                | Bool
otherwise    -> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall (n :: S). TermT n -> TypeCheck n String
ppInContext TermT n
term'
            TermT n
_ -> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall (n :: S). TermT n -> TypeCheck n String
ppInContext TermT n
term'
          color <- case term' of
            Var{} -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"purple"
            AppT TypeInfo (TermT n)
_ (Var Name n
x) TermT n
arg -> Name n -> TypeCheck n Bool
forall (n :: S). Name n -> TypeCheck n Bool
isAnonymous Name n
x TypeCheck n Bool
-> (Bool
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         String)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Bool
True -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
mainColor
              Bool
False
                | TermT n -> Bool
argIsOfT TermT n
arg -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"purple"
                | Bool
otherwise    -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
mainColor
            TermT n
_ -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
mainColor
          hide <- asks ctxRenderHideTerm
          return $ Just (shapeId, hideTermData hide mainColor RenderObjectData
            { renderObjectDataLabel = label
            , renderObjectDataFullLabel = label
            , renderObjectDataColor = color
            })

renderObjectsInSubShapeFor
  :: Distinct n
  => String -> Int -> [Foil.Name n] -> Foil.Name n
  -> TermT n -> TermT n -> TermT n
  -> TypeCheck n [(ShapeId, RenderObjectData)]
renderObjectsInSubShapeFor :: forall (n :: S).
Distinct n =>
String
-> Int
-> [Name n]
-> Name n
-> TermT n
-> TermT n
-> TermT n
-> TypeCheck n [(ShapeId, RenderObjectData)]
renderObjectsInSubShapeFor String
mainColor Int
dim [Name n]
sub Name n
super TermT n
retType TermT n
f TermT n
x = ([Maybe (ShapeId, RenderObjectData)]
 -> [(ShapeId, RenderObjectData)])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Maybe (ShapeId, RenderObjectData)]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(ShapeId, RenderObjectData)]
forall a b.
(a -> b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe (ShapeId, RenderObjectData)]
-> [(ShapeId, RenderObjectData)]
forall a. [Maybe a] -> [a]
catMaybes (ReaderT
   (Context n)
   (ExceptT TypeErrorInScopedContext (State CheckLog))
   [Maybe (ShapeId, RenderObjectData)]
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      [(ShapeId, RenderObjectData)])
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [Maybe (ShapeId, RenderObjectData)]
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     [(ShapeId, RenderObjectData)]
forall a b. (a -> b) -> a -> b
$ do
  let reduceContext :: [ModalTope n] -> TermT n
reduceContext
        = (TermT n -> TermT n -> TermT n) -> TermT n -> [TermT n] -> TermT n
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeOrT TermT n
forall (n :: S). TermT n
topeBottomT
        ([TermT n] -> TermT n)
-> ([ModalTope n] -> [TermT n]) -> [ModalTope n] -> TermT n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([TermT n] -> TermT n) -> [[TermT n]] -> [TermT n]
forall a b. (a -> b) -> [a] -> [b]
map ((TermT n -> TermT n -> TermT n) -> TermT n -> [TermT n] -> TermT n
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n
topeAndT TermT n
forall (n :: S). TermT n
topeTopT)
        ([[TermT n]] -> [TermT n])
-> ([ModalTope n] -> [[TermT n]]) -> [ModalTope n] -> [TermT n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([TermT n] -> [TermT n]) -> [[TermT n]] -> [[TermT n]]
forall a b. (a -> b) -> [a] -> [b]
map ((TermT n -> Bool) -> [TermT n] -> [TermT n]
forall a. (a -> Bool) -> [a] -> [a]
filter (\TermT n
tope -> (Name n -> Bool) -> [Name n] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name n -> [Name n] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` TermT n -> [Name n]
forall (n :: S). TermT n -> [Name n]
freeVarsOfTermT TermT n
tope) [Name n]
sub))
        ([[TermT n]] -> [[TermT n]])
-> ([ModalTope n] -> [[TermT n]]) -> [ModalTope n] -> [[TermT n]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ModalTope n] -> [TermT n]) -> [[ModalTope n]] -> [[TermT n]]
forall a b. (a -> b) -> [a] -> [b]
map ((ModalTope n -> TermT n) -> [ModalTope n] -> [TermT n]
forall a b. (a -> b) -> [a] -> [b]
map ModalTope n -> TermT n
forall (n :: S). ModalTope n -> TermT n
tTope)
        ([[ModalTope n]] -> [[TermT n]])
-> ([ModalTope n] -> [[ModalTope n]])
-> [ModalTope n]
-> [[TermT n]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ModalTope n] -> [ModalTope n])
-> [[ModalTope n]] -> [[ModalTope n]]
forall a b. (a -> b) -> [a] -> [b]
map [ModalTope n] -> [ModalTope n]
forall (n :: S). Distinct n => [ModalTope n] -> [ModalTope n]
saturateTopes
        ([[ModalTope n]] -> [[ModalTope n]])
-> ([ModalTope n] -> [[ModalTope n]])
-> [ModalTope n]
-> [[ModalTope n]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ModalTope n] -> [[ModalTope n]]
forall (n :: S). Distinct n => [ModalTope n] -> [[ModalTope n]]
simplifyLHSwithDisjunctions
  contextTopes  <- (Context n -> TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ([ModalTope n] -> TermT n
reduceContext ([ModalTope n] -> TermT n)
-> (Context n -> [ModalTope n]) -> Context n -> TermT n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context n -> [ModalTope n]
forall (n :: S). Context n -> [ModalTope n]
ctxTopesNF)
  contextTopes' <- localTope (componentWiseEQT dim (Var super) x) $
    asks (reduceContext . ctxTopesNF)
  forM (subTopes2 dim (Var super)) $ \(ShapeId
shapeId, TermT n
tope) ->
    TermT n -> TermT n -> TypeCheck n Bool
forall (n :: S).
Distinct n =>
TermT n -> TermT n -> TypeCheck n Bool
checkEntails TermT n
tope TermT n
contextTopes TypeCheck n Bool
-> (Bool
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe (ShapeId, RenderObjectData)))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
False -> Maybe (ShapeId, RenderObjectData)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe (ShapeId, RenderObjectData))
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (ShapeId, RenderObjectData)
forall a. Maybe a
Nothing
      Bool
True -> do
        term <- TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S) a.
Distinct n =>
TermT n -> TypeCheck n a -> TypeCheck n a
localTope TermT n
tope (TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT (TermT n -> TermT n -> TermT n -> TermT n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT TermT n
retType TermT n
f (Name n -> TermT n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
super)))
        let argIsSuper TermT n
arg = [Name n] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TermT n -> [Name n]
forall (n :: S). TermT n -> [Name n]
freeVarsOfTermT TermT n
arg [Name n] -> [Name n] -> [Name n]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name n
super])
        label <- typeOf term >>= \case
          UniverseTopeT{} -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
""
          TermT n
_ -> case TermT n
term of
            AppT TypeInfo (TermT n)
_ (Var Name n
z) TermT n
arg -> Name n -> TypeCheck n Bool
forall (n :: S). Name n -> TypeCheck n Bool
isAnonymous Name n
z TypeCheck n Bool
-> (Bool
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         String)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Bool
True -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
""
              Bool
False
                | TermT n -> Bool
argIsSuper TermT n
arg -> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall (n :: S). TermT n -> TypeCheck n String
ppInContext (Name n -> TermT n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
z)
                | Bool
otherwise      -> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall (n :: S). TermT n -> TypeCheck n String
ppInContext TermT n
term
            TermT n
_ -> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall (n :: S). TermT n -> TypeCheck n String
ppInContext TermT n
term
        color <- checkEntails tope contextTopes' >>= \case
          Bool
True -> case TermT n
term of
            Var{} -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"purple"
            AppT TypeInfo (TermT n)
_ (Var Name n
z) TermT n
arg -> Name n -> TypeCheck n Bool
forall (n :: S). Name n -> TypeCheck n Bool
isAnonymous Name n
z TypeCheck n Bool
-> (Bool
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         String)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Bool
True -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
mainColor
              Bool
False
                | TermT n -> Bool
argIsSuper TermT n
arg -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"purple"
                | Bool
otherwise      -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
mainColor
            TermT n
_ -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
mainColor
          Bool
False -> String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"gray"
        hide <- asks ctxRenderHideTerm
        return $ Just (shapeId, hideTermData hide mainColor RenderObjectData
          { renderObjectDataLabel = label
          , renderObjectDataFullLabel = label
          , renderObjectDataColor = color
          })

renderForSubShapeSVG
  :: Distinct n
  => String -> Int -> [Foil.Name n] -> Foil.Name n
  -> TermT n -> TermT n -> TermT n
  -> TypeCheck n String
renderForSubShapeSVG :: forall (n :: S).
Distinct n =>
String
-> Int
-> [Name n]
-> Name n
-> TermT n
-> TermT n
-> TermT n
-> TypeCheck n String
renderForSubShapeSVG String
mainColor Int
dim [Name n]
sub Name n
super TermT n
retType TermT n
f TermT n
x = do
  objects <- String
-> Int
-> [Name n]
-> Name n
-> TermT n
-> TermT n
-> TermT n
-> TypeCheck n [(ShapeId, RenderObjectData)]
forall (n :: S).
Distinct n =>
String
-> Int
-> [Name n]
-> Name n
-> TermT n
-> TermT n
-> TermT n
-> TypeCheck n [(ShapeId, RenderObjectData)]
renderObjectsInSubShapeFor String
mainColor Int
dim [Name n]
sub Name n
super TermT n
retType TermT n
f TermT n
x
  pure (drawCube dim (map mk objects))
  where
    mk :: (ShapeId, b) -> (String, b)
mk (ShapeId
shapeId, b
renderData) = (String -> ShapeId -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"-" ((String -> String) -> ShapeId -> ShapeId
forall a b. (a -> b) -> [a] -> [b]
map String -> String
fill ShapeId
shapeId), b
renderData)
    fill :: String -> String
fill String
xs = String
xs String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
xs) Char
'1'

renderForSVG
  :: Distinct n => String -> Int -> TermT n -> TermT n -> TypeCheck n String
renderForSVG :: forall (n :: S).
Distinct n =>
String -> Int -> TermT n -> TermT n -> TypeCheck n String
renderForSVG String
mainColor Int
dim TermT n
t TermT n
term = do
  objects <- String
-> Int
-> TermT n
-> TermT n
-> TypeCheck n [(ShapeId, RenderObjectData)]
forall (n :: S).
Distinct n =>
String
-> Int
-> TermT n
-> TermT n
-> TypeCheck n [(ShapeId, RenderObjectData)]
renderObjectsFor String
mainColor Int
dim TermT n
t TermT n
term
  pure (drawCube dim (map mk objects))
  where
    mk :: (ShapeId, b) -> (String, b)
mk (ShapeId
shapeId, b
renderData) = (String -> ShapeId -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"-" ((String -> String) -> ShapeId -> ShapeId
forall a b. (a -> b) -> [a] -> [b]
map String -> String
fill ShapeId
shapeId), b
renderData)
    fill :: String -> String
fill String
xs = String
xs String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
3 Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
xs) Char
'1'

drawCube :: Int -> [(String, RenderObjectData)] -> String
drawCube :: Int -> [(String, RenderObjectData)] -> String
drawCube Int
dim [(String, RenderObjectData)]
objects =
  Camera Double
-> Double -> (String -> Maybe RenderObjectData) -> String
forall a.
(Floating a, Show a) =>
Camera a -> a -> (String -> Maybe RenderObjectData) -> String
renderCube Camera Double
forall a. Floating a => Camera a
defaultCamera Double
rotation (String -> [(String, RenderObjectData)] -> Maybe RenderObjectData
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, RenderObjectData)]
objects)
  where
    rotation :: Double
    rotation :: Double
rotation = if Int
dim Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2 then Double
forall a. Floating a => a
piDouble -> Double -> Double
forall a. Fractional a => a -> a -> a
/Double
7 else Double
0

-- | The dimension of a cube, if it is a power of the directed interval.
dimOf :: TermT n -> Maybe Int
dimOf :: forall (n :: S). TermT n -> Maybe Int
dimOf = \case
  Cube2T{}           -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
  CubeProductT TypeInfo (TermT n)
_ TermT n
l TermT n
r -> Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) (Int -> Int -> Int) -> Maybe Int -> Maybe (Int -> Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TermT n -> Maybe Int
forall (n :: S). TermT n -> Maybe Int
dimOf TermT n
l Maybe (Int -> Int) -> Maybe Int -> Maybe Int
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TermT n -> Maybe Int
forall (n :: S). TermT n -> Maybe Int
dimOf TermT n
r
    -- WARNING: breaks for 2 * (2 * 2)
  TermT n
_                  -> Maybe Int
forall a. Maybe a
Nothing

maxRenderDim :: Int
maxRenderDim :: Int
maxRenderDim = Int
3

renderTermSVGFor
  :: Distinct n
  => String                              -- ^ main colour
  -> Int                                 -- ^ dimensions accumulated so far (0 to 3)
  -> (Maybe (TermT n, TermT n), [Foil.Name n])  -- ^ the accumulated point, and its cube
  -> TermT n                             -- ^ the term to render
  -> TypeCheck n (Maybe String)
renderTermSVGFor :: forall (n :: S).
Distinct n =>
String
-> Int
-> (Maybe (TermT n, TermT n), [Name n])
-> TermT n
-> TypeCheck n (Maybe String)
renderTermSVGFor String
mainColor Int
accDim (Maybe (TermT n, TermT n)
mp, [Name n]
xs) TermT n
t = do
  t' <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
t
  ty <- typeOf t'
  case t of -- check the unevaluated term
    AppT TypeInfo (TermT n)
_info TermT n
f TermT n
x -> TermT n
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
renderApp TermT n
f TermT n
x
    TypeFunT TypeInfo (TermT n)
_ Binder
_orig' TModality
md' TermT n
_ Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_ ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
_
      | [Name n] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name n]
xs -> Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> TypeCheck n a
withBinder (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
"_")) TModality
md' TermT n
t' ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TypeCheck l (Maybe String))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe String))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
          String
-> Int
-> (Maybe (TermT l, TermT l), [Name l])
-> TermT l
-> TypeCheck l (Maybe String)
forall (n :: S).
Distinct n =>
String
-> Int
-> (Maybe (TermT n, TermT n), [Name n])
-> TermT n
-> TypeCheck n (Maybe String)
renderTermSVGFor String
"blue" Int
0 (Maybe (TermT l, TermT l)
forall a. Maybe a
Nothing, []) (Name l -> TermT l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder))  -- blue for types

    TermT n
_ -> case TermT n
t' of -- check the evaluated term
      AppT TypeInfo (TermT n)
_info TermT n
f TermT n
x -> TermT n
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
renderApp TermT n
f TermT n
x
      TypeFunT TypeInfo (TermT n)
_ Binder
_orig' TModality
md' TermT n
_ Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
_ ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
_
        | [Name n] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name n]
xs -> Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> TypeCheck n a
withBinder (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
"_")) TModality
md' TermT n
t' ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TypeCheck l (Maybe String))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe String))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
            String
-> Int
-> (Maybe (TermT l, TermT l), [Name l])
-> TermT l
-> TypeCheck l (Maybe String)
forall (n :: S).
Distinct n =>
String
-> Int
-> (Maybe (TermT n, TermT n), [Name n])
-> TermT n
-> TypeCheck n (Maybe String)
renderTermSVGFor String
"blue" Int
0 (Maybe (TermT l, TermT l)
forall a. Maybe a
Nothing, []) (Name l -> TermT l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder))

      TermT n
_ -> case TermT n
ty of -- check the type of the term
        TypeFunT TypeInfo (TermT n)
_ Binder
orig TModality
md TermT n
arg Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret
          | Just Int
dim <- TermT n -> Maybe Int
forall (n :: S). TermT n -> Maybe Int
dimOf TermT n
arg, Int
accDim Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
dim Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
maxRenderDim ->
              Binder
-> TModality
-> TermT n
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
-> Int
-> Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
underArg Binder
orig TModality
md TermT n
arg Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret TermT n
t' (Int
accDim Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
dim) Bool
True
          | [Name n] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name n]
xs ->
              Binder
-> TModality
-> TermT n
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
-> Int
-> Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
underArg Binder
orig TModality
md TermT n
arg Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret TermT n
t' Int
accDim Bool
False
        TermT n
_ -> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
renderAccumulated TermT n
t'
  where
    renderAccumulated :: TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
renderAccumulated TermT n
t' = ((TermT n, TermT n)
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      String)
-> Maybe (TermT n, TermT n)
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse (\(TermT n
p', TermT n
_) -> String
-> Int
-> TermT n
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall (n :: S).
Distinct n =>
String -> Int -> TermT n -> TermT n -> TypeCheck n String
renderForSVG String
mainColor Int
accDim TermT n
p' TermT n
t') Maybe (TermT n, TermT n)
mp

    renderApp :: TermT n
-> TermT n
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
renderApp TermT n
f TermT n
x = TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
f TypeCheck n (TermT n)
-> (TermT n
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      TypeFunT TypeInfo (TermT n)
_ Binder
fOrig TModality
md TermT n
fArg Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtopeArg ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret
        | Just Int
dim <- TermT n -> Maybe Int
forall (n :: S). TermT n -> Maybe Int
dimOf TermT n
fArg, Int
dim Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
maxRenderDim ->
            Binder
-> TModality
-> TermT n
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> TypeCheck n a
inScopeMaybeTope Binder
fOrig TModality
md TermT n
fArg Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtopeArg ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TypeCheck l (Maybe String))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe String))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder -> do
              ret' <- NameBinder n l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TypeCheck l (AST NameBinder (AnnSig TypeInfo TermSig) l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret
              -- FIXME: breaks for 2 * (2 * 2), but works for 2 * 2 * 2 = (2 * 2) * 2
              Just <$> renderForSubShapeSVG mainColor dim
                (Foil.sink1 xs) (Foil.nameOf binder)
                ret' (Foil.sink f) (Foil.sink x)
      TermT n
_ -> do
        t' <- TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
t
        renderAccumulated t'

    -- Go under the domain of a function type, assuming its shape tope if it has
    -- one, and render the body there.
    underArg :: Binder
-> TModality
-> TermT n
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TermT n
-> Int
-> Bool
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
underArg Binder
orig TModality
md TermT n
arg Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret TermT n
t' Int
accDim' Bool
extend =
      Binder
-> TModality
-> TermT n
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> TypeCheck n a
inScopeMaybeTope Binder
orig TModality
md TermT n
arg Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TypeCheck l (Maybe String))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe String))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder -> do
        let z :: AST NameBinder (AnnSig TypeInfo TermSig) l
z = Name l -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder)
            arg' :: AST NameBinder (AnnSig TypeInfo TermSig) l
arg' = TermT n -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
arg
        body <- case TermT n
t' of
          LambdaT TypeInfo (TermT n)
_ Binder
_orig Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
_marg ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
lamBody -> NameBinder n l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (AST NameBinder (AnnSig TypeInfo TermSig) l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
lamBody
          TermT n
_ -> do
            ret' <- NameBinder n l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (AST NameBinder (AnnSig TypeInfo TermSig) l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret
            pure (appT ret' (Foil.sink t') z)
        let mp' | Bool
extend = Maybe
  (AST NameBinder (AnnSig TypeInfo TermSig) l,
   AST NameBinder (AnnSig TypeInfo TermSig) l)
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> Maybe
     (AST NameBinder (AnnSig TypeInfo TermSig) l,
      AST NameBinder (AnnSig TypeInfo TermSig) l)
forall {n :: S}.
Maybe
  (AST NameBinder (AnnSig TypeInfo TermSig) n,
   AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe
     (AST NameBinder (AnnSig TypeInfo TermSig) n,
      AST NameBinder (AnnSig TypeInfo TermSig) n)
join' (((TermT n, TermT n)
 -> (AST NameBinder (AnnSig TypeInfo TermSig) l,
     AST NameBinder (AnnSig TypeInfo TermSig) l))
-> Maybe (TermT n, TermT n)
-> Maybe
     (AST NameBinder (AnnSig TypeInfo TermSig) l,
      AST NameBinder (AnnSig TypeInfo TermSig) l)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TermT n -> AST NameBinder (AnnSig TypeInfo TermSig) l)
-> (TermT n, TermT n)
-> (AST NameBinder (AnnSig TypeInfo TermSig) l,
    AST NameBinder (AnnSig TypeInfo TermSig) l)
forall {t} {b}. (t -> b) -> (t, t) -> (b, b)
both TermT n -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink) Maybe (TermT n, TermT n)
mp) AST NameBinder (AnnSig TypeInfo TermSig) l
arg' AST NameBinder (AnnSig TypeInfo TermSig) l
z
                | Bool
otherwise = ((TermT n, TermT n)
 -> (AST NameBinder (AnnSig TypeInfo TermSig) l,
     AST NameBinder (AnnSig TypeInfo TermSig) l))
-> Maybe (TermT n, TermT n)
-> Maybe
     (AST NameBinder (AnnSig TypeInfo TermSig) l,
      AST NameBinder (AnnSig TypeInfo TermSig) l)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TermT n -> AST NameBinder (AnnSig TypeInfo TermSig) l)
-> (TermT n, TermT n)
-> (AST NameBinder (AnnSig TypeInfo TermSig) l,
    AST NameBinder (AnnSig TypeInfo TermSig) l)
forall {t} {b}. (t -> b) -> (t, t) -> (b, b)
both TermT n -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink) Maybe (TermT n, TermT n)
mp
            xs' | Bool
extend = NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder Name l -> [Name l] -> [Name l]
forall a. a -> [a] -> [a]
: [Name n] -> [Name l]
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1 [Name n]
xs
                | Bool
otherwise = [Name n] -> [Name l]
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1 [Name n]
xs
        renderTermSVGFor mainColor accDim' (mp', xs') body

    both :: (t -> b) -> (t, t) -> (b, b)
both t -> b
f (t
x, t
y) = (t -> b
f t
x, t -> b
f t
y)

    join' :: Maybe
  (AST NameBinder (AnnSig TypeInfo TermSig) n,
   AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe
     (AST NameBinder (AnnSig TypeInfo TermSig) n,
      AST NameBinder (AnnSig TypeInfo TermSig) n)
join' Maybe
  (AST NameBinder (AnnSig TypeInfo TermSig) n,
   AST NameBinder (AnnSig TypeInfo TermSig) n)
Nothing Cube2T{} AST NameBinder (AnnSig TypeInfo TermSig) n
x = (AST NameBinder (AnnSig TypeInfo TermSig) n,
 AST NameBinder (AnnSig TypeInfo TermSig) n)
-> Maybe
     (AST NameBinder (AnnSig TypeInfo TermSig) n,
      AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just (AST NameBinder (AnnSig TypeInfo TermSig) n
x, AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cube2T)
    join' (Just (AST NameBinder (AnnSig TypeInfo TermSig) n
p, AST NameBinder (AnnSig TypeInfo TermSig) n
pt)) Cube2T{} AST NameBinder (AnnSig TypeInfo TermSig) n
x = (AST NameBinder (AnnSig TypeInfo TermSig) n,
 AST NameBinder (AnnSig TypeInfo TermSig) n)
-> Maybe
     (AST NameBinder (AnnSig TypeInfo TermSig) n,
      AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. a -> Maybe a
Just (AST NameBinder (AnnSig TypeInfo TermSig) n
p', AST NameBinder (AnnSig TypeInfo TermSig) n
pt')
      where
        pt' :: AST NameBinder (AnnSig TypeInfo TermSig) n
pt' = AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n -> TermT n -> TermT n
cubeProductT AST NameBinder (AnnSig TypeInfo TermSig) n
pt AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n
cube2T
        p' :: AST NameBinder (AnnSig TypeInfo TermSig) n
p' = AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
pairT AST NameBinder (AnnSig TypeInfo TermSig) n
pt' AST NameBinder (AnnSig TypeInfo TermSig) n
p AST NameBinder (AnnSig TypeInfo TermSig) n
x
    join' Maybe
  (AST NameBinder (AnnSig TypeInfo TermSig) n,
   AST NameBinder (AnnSig TypeInfo TermSig) n)
p (CubeProductT TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) n)
_ AST NameBinder (AnnSig TypeInfo TermSig) n
l AST NameBinder (AnnSig TypeInfo TermSig) n
r) AST NameBinder (AnnSig TypeInfo TermSig) n
x =
      Maybe
  (AST NameBinder (AnnSig TypeInfo TermSig) n,
   AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe
     (AST NameBinder (AnnSig TypeInfo TermSig) n,
      AST NameBinder (AnnSig TypeInfo TermSig) n)
join' (Maybe
  (AST NameBinder (AnnSig TypeInfo TermSig) n,
   AST NameBinder (AnnSig TypeInfo TermSig) n)
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> Maybe
     (AST NameBinder (AnnSig TypeInfo TermSig) n,
      AST NameBinder (AnnSig TypeInfo TermSig) n)
join' Maybe
  (AST NameBinder (AnnSig TypeInfo TermSig) n,
   AST NameBinder (AnnSig TypeInfo TermSig) n)
p AST NameBinder (AnnSig TypeInfo TermSig) n
l (AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n -> TermT n -> TermT n
firstT AST NameBinder (AnnSig TypeInfo TermSig) n
l AST NameBinder (AnnSig TypeInfo TermSig) n
x)) AST NameBinder (AnnSig TypeInfo TermSig) n
r (AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
-> AST NameBinder (AnnSig TypeInfo TermSig) n
forall (n :: S). TermT n -> TermT n -> TermT n
secondT AST NameBinder (AnnSig TypeInfo TermSig) n
r AST NameBinder (AnnSig TypeInfo TermSig) n
x)
    join' Maybe
  (AST NameBinder (AnnSig TypeInfo TermSig) n,
   AST NameBinder (AnnSig TypeInfo TermSig) n)
_ AST NameBinder (AnnSig TypeInfo TermSig) n
_ AST NameBinder (AnnSig TypeInfo TermSig) n
_ = Maybe
  (AST NameBinder (AnnSig TypeInfo TermSig) n,
   AST NameBinder (AnnSig TypeInfo TermSig) n)
forall a. Maybe a
Nothing -- FIXME: error?

-- | Enter a binder and assume the shape tope it carries, if any.
inScopeMaybeTope
  :: Distinct n
  => Binder -> TModality -> TermT n -> Maybe (ScopedTermT n)
  -> (forall l. (Foil.DExt n l, Distinct l) => Foil.NameBinder n l -> TypeCheck l a)
  -> TypeCheck n a
inScopeMaybeTope :: forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> TypeCheck n a
inScopeMaybeTope Binder
orig TModality
md TermT n
ty Maybe (ScopedTermT n)
mtope forall (l :: S).
(DExt n l, Distinct l) =>
NameBinder n l -> TypeCheck l a
k =
  Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> TypeCheck n a
withBinder Binder
orig TModality
md TermT n
ty ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TypeCheck l a)
 -> ReaderT
      (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
    case Maybe (ScopedTermT n)
mtope of
      Maybe (ScopedTermT n)
Nothing   -> NameBinder n l -> TypeCheck l a
forall (l :: S).
(DExt n l, Distinct l) =>
NameBinder n l -> TypeCheck l a
k NameBinder n l
binder
      Just ScopedTermT n
tope -> do
        tope' <- NameBinder n l
-> ScopedTermT n
-> TypeCheck l (AST NameBinder (AnnSig TypeInfo TermSig) l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder ScopedTermT n
tope
        localTope tope' (k binder)

renderTermSVG :: Distinct n => TermT n -> TypeCheck n (Maybe String)
renderTermSVG :: forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n (Maybe String)
renderTermSVG = String
-> Int
-> (Maybe (TermT n, TermT n), [Name n])
-> TermT n
-> TypeCheck n (Maybe String)
forall (n :: S).
Distinct n =>
String
-> Int
-> (Maybe (TermT n, TermT n), [Name n])
-> TermT n
-> TypeCheck n (Maybe String)
renderTermSVGFor String
"red" Int
0 (Maybe (TermT n, TermT n)
forall a. Maybe a
Nothing, [])  -- red for terms, by default

-- | Render the goal /cell/ for a (shape) type: introduce an abstract inhabitant
-- and render it with the proof term hidden. Under a boundary tope an abstract
-- inhabitant of an extension type reduces to the prescribed face value, so the
-- cell shows its given edges with a blank interior — the shape to inhabit, not an
-- answer. 'Nothing' for a non-shape type (a 0-cell, or a non-cube goal).
renderGoalCellSVG :: Distinct n => TermT n -> TypeCheck n (Maybe String)
renderGoalCellSVG :: forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n (Maybe String)
renderGoalCellSVG TermT n
ty =
  TypeCheck n (Maybe String) -> TypeCheck n (Maybe String)
forall (n :: S) a. TypeCheck n a -> TypeCheck n a
hidingTerm (TypeCheck n (Maybe String) -> TypeCheck n (Maybe String))
-> TypeCheck n (Maybe String) -> TypeCheck n (Maybe String)
forall a b. (a -> b) -> a -> b
$ Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> TypeCheck n (Maybe String)
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> TypeCheck n a
withBinder (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
"_")) TModality
Id TermT n
ty ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TypeCheck l (Maybe String))
 -> TypeCheck n (Maybe String))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> TypeCheck n (Maybe String)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
    TermT l -> TypeCheck l (Maybe String)
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n (Maybe String)
renderTermSVG' (Name l -> TermT l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder))

renderTermSVG' :: forall n. Distinct n => TermT n -> TypeCheck n (Maybe String)
renderTermSVG' :: forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n (Maybe String)
renderTermSVG' TermT n
t = TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
whnfT TermT n
t TypeCheck n (TermT n)
-> (TermT n
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TermT n
t' -> TermT n -> TypeCheck n (TermT n)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf TermT n
t TypeCheck n (TermT n)
-> (TermT n
    -> ReaderT
         (Context n)
         (ExceptT TypeErrorInScopedContext (State CheckLog))
         (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall a b.
ReaderT
  (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  TypeFunT TypeInfo (TermT n)
_ Binder
orig TModality
md TermT n
arg Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret ->
    Binder
-> TModality
-> TermT n
-> Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall (n :: S) a.
Distinct n =>
Binder
-> TModality
-> TermT n
-> Maybe (ScopedTermT n)
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l a)
-> TypeCheck n a
inScopeMaybeTope Binder
orig TModality
md TermT n
arg Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n)
mtope ((forall (l :: S).
  (DExt n l, Distinct l) =>
  NameBinder n l -> TypeCheck l (Maybe String))
 -> ReaderT
      (Context n)
      (ExceptT TypeErrorInScopedContext (State CheckLog))
      (Maybe String))
-> (forall (l :: S).
    (DExt n l, Distinct l) =>
    NameBinder n l -> TypeCheck l (Maybe String))
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
      case TermT n
t' of
        LambdaT TypeInfo (TermT n)
_ Binder
_orig Maybe
  (LambdaParam
     (ScopedAST NameBinder (AnnSig TypeInfo TermSig) n) (TermT n))
_marg ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
lamBody ->
          NameBinder n l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TypeCheck l (AST NameBinder (AnnSig TypeInfo TermSig) l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
lamBody TypeCheck l (AST NameBinder (AnnSig TypeInfo TermSig) l)
-> (AST NameBinder (AnnSig TypeInfo TermSig) l
    -> TypeCheck l (Maybe String))
-> TypeCheck l (Maybe String)
forall a b.
ReaderT
  (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            AppT TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) l)
_info AST NameBinder (AnnSig TypeInfo TermSig) l
f AST NameBinder (AnnSig TypeInfo TermSig) l
x -> AST NameBinder (AnnSig TypeInfo TermSig) l
-> TypeCheck l (AST NameBinder (AnnSig TypeInfo TermSig) l)
forall (n :: S). Distinct n => TermT n -> TypeCheck n (TermT n)
typeOf AST NameBinder (AnnSig TypeInfo TermSig) l
f TypeCheck l (AST NameBinder (AnnSig TypeInfo TermSig) l)
-> (AST NameBinder (AnnSig TypeInfo TermSig) l
    -> TypeCheck l (Maybe String))
-> TypeCheck l (Maybe String)
forall a b.
ReaderT
  (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
-> (a
    -> ReaderT
         (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) b)
-> ReaderT
     (Context l) (ExceptT TypeErrorInScopedContext (State CheckLog)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              TypeFunT TypeInfo (AST NameBinder (AnnSig TypeInfo TermSig) l)
_ Binder
fOrig TModality
md2 AST NameBinder (AnnSig TypeInfo TermSig) l
fArg Maybe (ScopedAST NameBinder (AnnSig TypeInfo TermSig) l)
mtope2 ScopedAST NameBinder (AnnSig TypeInfo TermSig) l
_ret
                | Just Int
dim <- AST NameBinder (AnnSig TypeInfo TermSig) l -> Maybe Int
forall (n :: S). TermT n -> Maybe Int
dimOf AST NameBinder (AnnSig TypeInfo TermSig) l
fArg -> do
                    ret' <- NameBinder n l
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TypeCheck l (AST NameBinder (AnnSig TypeInfo TermSig) l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret
                    inScopeMaybeTope fOrig md2 fArg mtope2 $ \NameBinder l l
binder2 ->
                      String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
-> TypeCheck l (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> Int
-> [Name l]
-> Name l
-> TermT l
-> TermT l
-> TermT l
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall (n :: S).
Distinct n =>
String
-> Int
-> [Name n]
-> Name n
-> TermT n
-> TermT n
-> TermT n
-> TypeCheck n String
renderForSubShapeSVG String
"red" Int
dim
                        [Name l -> Name l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder)] (NameBinder l l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder l l
binder2)
                        (AST NameBinder (AnnSig TypeInfo TermSig) l -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink AST NameBinder (AnnSig TypeInfo TermSig) l
ret') (AST NameBinder (AnnSig TypeInfo TermSig) l -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink AST NameBinder (AnnSig TypeInfo TermSig) l
f) (AST NameBinder (AnnSig TypeInfo TermSig) l -> TermT l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink AST NameBinder (AnnSig TypeInfo TermSig) l
x)
              AST NameBinder (AnnSig TypeInfo TermSig) l
_ -> NameBinder n l
-> TermT n
-> TermT n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TypeCheck l (Maybe String)
forall (n :: S) (l :: S).
DExt n l =>
NameBinder n l
-> TermT n
-> TermT n
-> ScopedTermT n
-> TypeCheck l (Maybe String)
renderApplied NameBinder n l
binder TermT n
t' TermT n
arg ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret
            AST NameBinder (AnnSig TypeInfo TermSig) l
_ -> NameBinder n l
-> TermT n
-> TermT n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TypeCheck l (Maybe String)
forall (n :: S) (l :: S).
DExt n l =>
NameBinder n l
-> TermT n
-> TermT n
-> ScopedTermT n
-> TypeCheck l (Maybe String)
renderApplied NameBinder n l
binder TermT n
t' TermT n
arg ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret
        TermT n
_ -> NameBinder n l
-> TermT n
-> TermT n
-> ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
-> TypeCheck l (Maybe String)
forall (n :: S) (l :: S).
DExt n l =>
NameBinder n l
-> TermT n
-> TermT n
-> ScopedTermT n
-> TypeCheck l (Maybe String)
renderApplied NameBinder n l
binder TermT n
t' TermT n
arg ScopedAST NameBinder (AnnSig TypeInfo TermSig) n
ret
  TermT n
_t' -> Maybe String
-> ReaderT
     (Context n)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall a.
a
-> ReaderT
     (Context n) (ExceptT TypeErrorInScopedContext (State CheckLog)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing

-- | Render a term of a function type by applying it to the variable it abstracts
-- over, and drawing that.
renderApplied
  :: Foil.DExt n l
  => Foil.NameBinder n l -> TermT n -> TermT n -> ScopedTermT n
  -> TypeCheck l (Maybe String)
renderApplied :: forall (n :: S) (l :: S).
DExt n l =>
NameBinder n l
-> TermT n
-> TermT n
-> ScopedTermT n
-> TypeCheck l (Maybe String)
renderApplied NameBinder n l
binder TermT n
t' TermT n
arg ScopedTermT n
ret = do
  ret' <- NameBinder n l
-> ScopedTermT n
-> TypeCheck l (AST NameBinder (AnnSig TypeInfo TermSig) l)
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifunctor sig, DExt n l) =>
NameBinder n l
-> ScopedAST NameBinder sig n -> TypeCheck l (AST NameBinder sig l)
openScoped NameBinder n l
binder ScopedTermT n
ret
  let z = Name l -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder)
      applied = AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (n :: S). TermT n -> TermT n -> TermT n -> TermT n
appT AST NameBinder (AnnSig TypeInfo TermSig) l
ret' (TermT n -> AST NameBinder (AnnSig TypeInfo TermSig) l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink TermT n
t') AST NameBinder (AnnSig TypeInfo TermSig) l
z
  case dimOf arg of
    Just Int
dim | Int
dim Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
maxRenderDim ->
      String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String
-> Int
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> AST NameBinder (AnnSig TypeInfo TermSig) l
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     String
forall (n :: S).
Distinct n =>
String -> Int -> TermT n -> TermT n -> TypeCheck n String
renderForSVG String
"red" Int
dim AST NameBinder (AnnSig TypeInfo TermSig) l
z AST NameBinder (AnnSig TypeInfo TermSig) l
applied
    Maybe Int
_ -> AST NameBinder (AnnSig TypeInfo TermSig) l
-> ReaderT
     (Context l)
     (ExceptT TypeErrorInScopedContext (State CheckLog))
     (Maybe String)
forall (n :: S).
Distinct n =>
TermT n -> TypeCheck n (Maybe String)
renderTermSVG' AST NameBinder (AnnSig TypeInfo TermSig) l
applied