Type-level sanitized labels for HaTeX/TeX-my-math

Eqns.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Text.LaTeX.Eqns where

{-
build-depends:
  base >= 4.10
  , HaTeX >= 3.22 (version because of fixEnv), sym
  , TeX-my-math
  , symbols (Data.Symbol.*)
  , reflection (only dev helpers at bottom)
-}

import Data.Proxy (Proxy(..))
import Data.String (fromString)
import Data.Symbol.Ascii
import Data.Type.Bool
import Data.Type.Equality
import GHC.TypeLits
import Data.Reflection

import Text.LaTeX (LaTeX, label, raw, render)
import Text.LaTeX.Base.Class (LaTeXC, fixEnv, fromLaTeX)

import Math.LaTeX.Prelude hiding (Symbol)

-- Almost standard type-level list, but con-ing a proxy and carrying
-- exactly one latex type.
-- with this parameter order, EqnT can be used as a `proxy labels`
data EqnT latex labels where
    ENil :: EqnT l '[]
    Eqn :: (LaTeXC l, KnownSymbol λ)
        => (proxy λ, l) -> EqnT l λs -> EqnT l (λ:λs)

type DEqn l λ = forall λs. (LaTeXC l, KnownSymbol λ) => EqnT l λs -> EqnT l (λ:λs)
type Λ λ = forall l. DEqn l λ -- convenience shorthand. Λ = greek Lambda


-- sugar like automatic align &s and visual label handling like TeX-my-math
-- `equations` can be added
equations' :: LaTeXC l => String -> [l] -> (EqnT l '[] -> EqnT l ls) -> l
equations' name args de = fixEnv name args . body . de $ ENil
  where
    body :: LaTeXC l => EqnT l ls -> l
    body ENil = mempty
    body (Eqn e es) = labeledEqn e <> raw"\\" <> body es
    labeledEqn :: (KnownSymbol λ, LaTeXC l) => (proxy λ, l) -> l
    labeledEqn (λ, l) = (<>) l . label . fromString . symbolVal $ λ

eqn :: LaTeXC l => l -> DEqn l λ
eqn l = Eqn $ (Proxy, l)

-- the only TeX-my-math specific things
type MathLaTeXC l σ = (LaTeXC l, SymbolClass σ, SCConstraint σ LaTeX)
eqn' :: forall l σ λ. MathLaTeXC l σ => LaTeXMath σ -> DEqn l λ
eqn' = eqn . fromLaTeX . toMathLaTeX

test :: LaTeX
test = equations' "align" []
    $ (eqn' $ 𝑥◝2 :: Λ "la")
    . (eqn' $ 𝑎-𝑏 :: Λ "eq:lb")

--------------------------------------------------------------------------------
-- symbol checking

data Set a -- mark element as set, see type family Elem
data Range a b

type family MaybeSuccess (success :: Bool) errmsg t where
    MaybeSuccess True errmsg t = t
    MaybeSuccess False errmsg t = TypeError errmsg

type family Elem (x::k0) (set::k1) :: Bool where
    Elem x '[]             = False
    Elem x (x     : set)   = True
    Elem x (Set b : set)   = x ∈ b || x ∈ set
    Elem x (s     : set)   = x ∈ set
    Elem x (set :: Symbol) = x ∈ ToList set
    Elem x (Range a b)     = CmpSymbol x a ∈ '[GT,EQ] && CmpSymbol x b ∈ '[LT,EQ]
type x ∈ set = x `Elem` set

-- the most efficient search algorithm…
type family Subset (a::k0) (b::k1) :: Bool where
    Subset '[]           b  = True
    Subset (a:as)        b = a ∈ b && as ⊆ b
    Subset (a :: Symbol) b = ToList a ⊆ b
type  a ⊆ b = Subset a b

-- Charsets
type AlphaSym = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
 -- [Set a, Set b] is the union of sets respecting Elem and Subset
type AlphaRange = [Set (Range "a" "z"), Set (Range "A" "Z")]
type LaTeXLabelTrad = Set ":._" : AlphaRange

-- Filters
type IsAlpha  sym = sym ⊆ AlphaSym -- slow (O(exp(m)) algorithm), flexible
type IsAlpha' sym = sym ⊆ AlphaRange -- faster
type AlphaErr a = Text "Non-alphanumeric character in type " :<>: ShowType a
type Λα  λ = Λ (MaybeSuccess (IsAlpha  λ) (AlphaErr λ) λ)
type Λα' λ = Λ (MaybeSuccess (IsAlpha' λ) (AlphaErr λ) λ)

type IsLaTeXLabelTrad λ = λ ⊆ LaTeXLabelTrad
type LaTeXLabelErr a =
    Text "Label contains forbidden characters: " :<>: ShowType a
    :$$: Text "Allowed characters are [a-zA-Z:._]."
type SafeLabel λ = Λ (MaybeSuccess (IsLaTeXLabelTrad λ) (LaTeXLabelErr λ) λ)
type Σ λ = SafeLabel λ -- because :._ are probably safe as well

---- slow
testAlpha :: LaTeX
testAlpha = equations' "align" []
    $ (eqn'$ 𝑥◝2 :: Λα "allowed")
    . (eqn'$ 𝑎-𝑏 :: Λα "eq:forbidden")

-- faster
testAlpha' :: LaTeX
testAlpha' = equations' "align" []
    $ (eqn'$ 𝑥◝2 :: Λα' "allowed")
    . (eqn'$ 𝑎-𝑏 :: Λα' "eq:forbidden'")

-- [a-zA-Z:._] allowed
testTrad :: LaTeX
testTrad = equations' "align" []
    $ (eqn'$ 𝑥◝2 :: Σ "eq:aLlo._wed")
    . (eqn'$ 𝑎-𝑏 :: Σ "eq@forbidden")

-- development helpers for code inspection
instance Reifies True Bool where reflect _ = True
instance Reifies False Bool where reflect _ = False

decons :: proxy (x:xs) -> (Proxy x, Proxy xs)
decons p = (Proxy, Proxy)

instance Reifies '[] [String] where
    reflect p = []

instance (Reifies ns [String], KnownSymbol n) => Reifies (n : (ns :: [Symbol])) [String] where
    reflect p = let (p0, ps) = decons p in reflect p0 : reflect ps