{-# LANGUAGE CPP
, ScopedTypeVariables
, GADTs
, DataKinds
, PolyKinds
, TypeInType
, TypeOperators
, Rank2Types
, MultiParamTypeClasses
, FlexibleContexts
, FlexibleInstances
, FunctionalDependencies
, UndecidableInstances
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.ABT
(
module Language.Hakaru.Syntax.Variable
, resolveVar
, View(..)
, unviewABT
, ABT(..)
, caseVarSyn
, binds
, binds_
, caseBinds
, underBinders
, maxNextFree
, maxNextBind
, maxNextFreeOrBind
, rename
, renames
, subst
, substM
, substs
, binder
, binderM
, Binders(binders)
, withMetadata
, cataABT
, cataABTM
, paraABT
, dupABT
, TrivialABT()
, MemoizedABT()
, MetaABT(..)
) where
import Data.Text (Text, empty)
import qualified Data.Foldable as F
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative hiding (empty)
import Data.Monoid (Monoid(..))
#endif
import Control.Monad.Identity
import Data.Kind
import Data.Number.Nat
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Types.Sing
import Language.Hakaru.Syntax.Variable
#ifdef __TRACE_DISINTEGRATE__
import Debug.Trace (trace)
#endif
data View :: (k -> Type) -> [k] -> k -> Type where
Syn :: !(rec a) -> View rec '[] a
Var :: {-# UNPACK #-} !(Variable a) -> View rec '[] a
Bind
:: {-# UNPACK #-} !(Variable a)
-> !(View rec xs b)
-> View rec (a ': xs) b
instance Functor12 View where
fmap12 :: (forall (i :: k3). a i -> b i) -> View a j l -> View b j l
fmap12 forall (i :: k3). a i -> b i
f (Syn a l
t) = b l -> View b '[] l
forall k (rec :: k -> *) (a :: k). rec a -> View rec '[] a
Syn (a l -> b l
forall (i :: k3). a i -> b i
f a l
t)
fmap12 forall (i :: k3). a i -> b i
_ (Var Variable l
x) = Variable l -> View b '[] l
forall k (a :: k) (rec :: k -> *). Variable a -> View rec '[] a
Var Variable l
x
fmap12 forall (i :: k3). a i -> b i
f (Bind Variable a
x View a xs l
e) = Variable a -> View b xs l -> View b (a : xs) l
forall a (a :: a) (rec :: a -> *) (xs :: [a]) (b :: a).
Variable a -> View rec xs b -> View rec (a : xs) b
Bind Variable a
x ((forall (i :: k3). a i -> b i) -> View a xs l -> View b xs l
forall k1 k2 k3 (f :: (k1 -> *) -> k2 -> k3 -> *) (a :: k1 -> *)
(b :: k1 -> *) (j :: k2) (l :: k3).
Functor12 f =>
(forall (i :: k1). a i -> b i) -> f a j l -> f b j l
fmap12 forall (i :: k3). a i -> b i
f View a xs l
e)
instance Foldable12 View where
foldMap12 :: (forall (i :: k3). a i -> m) -> View a j l -> m
foldMap12 forall (i :: k3). a i -> m
f (Syn a l
t) = a l -> m
forall (i :: k3). a i -> m
f a l
t
foldMap12 forall (i :: k3). a i -> m
_ (Var Variable l
_) = m
forall a. Monoid a => a
mempty
foldMap12 forall (i :: k3). a i -> m
f (Bind Variable a
_ View a xs l
e) = (forall (i :: k3). a i -> m) -> View a xs l -> m
forall k1 k2 k3 (f :: (k1 -> *) -> k2 -> k3 -> *) m (a :: k1 -> *)
(j :: k2) (l :: k3).
(Foldable12 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j l -> m
foldMap12 forall (i :: k3). a i -> m
f View a xs l
e
instance Traversable12 View where
traverse12 :: (forall (i :: k3). a i -> f (b i)) -> View a j l -> f (View b j l)
traverse12 forall (i :: k3). a i -> f (b i)
f (Syn a l
t) = b l -> View b '[] l
forall k (rec :: k -> *) (a :: k). rec a -> View rec '[] a
Syn (b l -> View b '[] l) -> f (b l) -> f (View b '[] l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a l -> f (b l)
forall (i :: k3). a i -> f (b i)
f a l
t
traverse12 forall (i :: k3). a i -> f (b i)
_ (Var Variable l
x) = View b '[] l -> f (View b '[] l)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (View b '[] l -> f (View b '[] l))
-> View b '[] l -> f (View b '[] l)
forall a b. (a -> b) -> a -> b
$ Variable l -> View b '[] l
forall k (a :: k) (rec :: k -> *). Variable a -> View rec '[] a
Var Variable l
x
traverse12 forall (i :: k3). a i -> f (b i)
f (Bind Variable a
x View a xs l
e) = Variable a -> View b xs l -> View b (a : xs) l
forall a (a :: a) (rec :: a -> *) (xs :: [a]) (b :: a).
Variable a -> View rec xs b -> View rec (a : xs) b
Bind Variable a
x (View b xs l -> View b (a : xs) l)
-> f (View b xs l) -> f (View b (a : xs) l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (i :: k3). a i -> f (b i))
-> View a xs l -> f (View b xs l)
forall k1 k2 k3 (t :: (k1 -> *) -> k2 -> k3 -> *) (f :: * -> *)
(a :: k1 -> *) (b :: k1 -> *) (j :: k2) (l :: k3).
(Traversable12 t, Applicative f) =>
(forall (i :: k1). a i -> f (b i)) -> t a j l -> f (t b j l)
traverse12 forall (i :: k3). a i -> f (b i)
f View a xs l
e
instance (Show1 (Sing :: k -> Type), Show1 rec)
=> Show2 (View (rec :: k -> Type))
where
showsPrec2 :: Int -> View rec i j -> ShowS
showsPrec2 Int
p (Syn rec j
t) = Int -> String -> rec j -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"Syn" rec j
t
showsPrec2 Int
p (Var Variable j
x) = Int -> String -> Variable j -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"Var" Variable j
x
showsPrec2 Int
p (Bind Variable a
x View rec xs j
v) = Int -> String -> Variable a -> View rec xs j -> ShowS
forall k k1 k2 (a :: k -> *) (b :: k1 -> k2 -> *) (i :: k)
(j :: k1) (l :: k2).
(Show1 a, Show2 b) =>
Int -> String -> a i -> b j l -> ShowS
showParen_12 Int
p String
"Bind" Variable a
x View rec xs j
v
instance (Show1 (Sing :: k -> Type), Show1 rec)
=> Show1 (View (rec :: k -> Type) xs)
where
showsPrec1 :: Int -> View rec xs i -> ShowS
showsPrec1 = Int -> View rec xs i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2
show1 :: View rec xs i -> String
show1 = View rec xs i -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2
instance (Show1 (Sing :: k -> Type), Show1 rec)
=> Show (View (rec :: k -> Type) xs a)
where
showsPrec :: Int -> View rec xs a -> ShowS
showsPrec = Int -> View rec xs a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: View rec xs a -> String
show = View rec xs a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
class ABT (syn :: ([k] -> k -> Type) -> k -> Type) (abt :: [k] -> k -> Type) | abt -> syn where
syn :: syn abt a -> abt '[] a
var :: Variable a -> abt '[] a
bind :: Variable a -> abt xs b -> abt (a ': xs) b
caseBind :: abt (x ': xs) a -> (Variable x -> abt xs a -> r) -> r
viewABT :: abt xs a -> View (syn abt) xs a
freeVars :: abt xs a -> VarSet (KindOf a)
nextFree :: abt xs a -> Nat
nextFree = VarSet (KindOf a) -> Nat
forall k (kproxy :: KProxy k). VarSet kproxy -> Nat
nextVarID (VarSet (KindOf a) -> Nat)
-> (abt xs a -> VarSet (KindOf a)) -> abt xs a -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt xs a -> VarSet (KindOf a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> VarSet (KindOf a)
freeVars
nextBind :: abt xs a -> Nat
nextFreeOrBind :: abt xs a -> Nat
nextFreeOrBind abt xs a
e = abt xs a -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFree abt xs a
e Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
`max` abt xs a -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextBind abt xs a
e
unviewABT :: (ABT syn abt) => View (syn abt) xs a -> abt xs a
unviewABT :: View (syn abt) xs a -> abt xs a
unviewABT (Syn syn abt a
t) = syn abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn syn abt a
t
unviewABT (Var Variable a
x) = Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
x
unviewABT (Bind Variable a
x View (syn abt) xs a
v) = Variable a -> abt xs a -> abt (a : xs) a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
x (View (syn abt) xs a -> abt xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
View (syn abt) xs a -> abt xs a
unviewABT View (syn abt) xs a
v)
caseVarSyn
:: (ABT syn abt)
=> abt '[] a
-> (Variable a -> r)
-> (syn abt a -> r)
-> r
caseVarSyn :: abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] a
e Variable a -> r
var_ syn abt a -> r
syn_ =
case abt '[] a -> View (syn abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] a
e of
Syn syn abt a
t -> syn abt a -> r
syn_ syn abt a
t
Var Variable a
x -> Variable a -> r
var_ Variable a
x
binds :: (ABT syn abt) => List1 Variable xs -> abt ys b -> abt (xs ++ ys) b
binds :: List1 Variable xs -> abt ys b -> abt (xs ++ ys) b
binds List1 Variable xs
Nil1 abt ys b
e = abt ys b
abt (xs ++ ys) b
e
binds (Cons1 Variable x
x List1 Variable xs
xs) abt ys b
e = Variable x -> abt (xs ++ ys) b -> abt (x : (xs ++ ys)) b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable x
x (List1 Variable xs -> abt ys b -> abt (xs ++ ys) b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (ys :: [k]) (b :: k).
ABT syn abt =>
List1 Variable xs -> abt ys b -> abt (xs ++ ys) b
binds List1 Variable xs
xs abt ys b
e)
binds_ :: (ABT syn abt) => List1 Variable xs -> abt '[] b -> abt xs b
binds_ :: List1 Variable xs -> abt '[] b -> abt xs b
binds_ List1 Variable xs
Nil1 abt '[] b
e = abt xs b
abt '[] b
e
binds_ (Cons1 Variable x
x List1 Variable xs
xs) abt '[] b
e = Variable x -> abt xs b -> abt (x : xs) b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable x
x (List1 Variable xs -> abt '[] b -> abt xs b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (b :: k).
ABT syn abt =>
List1 Variable xs -> abt '[] b -> abt xs b
binds_ List1 Variable xs
xs abt '[] b
e)
caseBinds :: (ABT syn abt) => abt xs a -> (List1 Variable xs, abt '[] a)
caseBinds :: abt xs a -> (List1 Variable xs, abt '[] a)
caseBinds = View (syn abt) xs a -> (List1 Variable xs, abt '[] a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
View (syn abt) xs a -> (List1 Variable xs, abt '[] a)
go (View (syn abt) xs a -> (List1 Variable xs, abt '[] a))
-> (abt xs a -> View (syn abt) xs a)
-> abt xs a
-> (List1 Variable xs, abt '[] a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt xs a -> View (syn abt) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
where
go :: (ABT syn abt)
=> View (syn abt) xs a -> (List1 Variable xs, abt '[] a)
go :: View (syn abt) xs a -> (List1 Variable xs, abt '[] a)
go (Syn syn abt a
t) = (List1 Variable xs
forall k (a :: k -> *). List1 a '[]
Nil1, syn abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn syn abt a
t)
go (Var Variable a
x) = (List1 Variable xs
forall k (a :: k -> *). List1 a '[]
Nil1, Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
x)
go (Bind Variable a
x View (syn abt) xs a
v) = let ~(List1 Variable xs
xs,abt '[] a
e) = View (syn abt) xs a -> (List1 Variable xs, abt '[] a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
View (syn abt) xs a -> (List1 Variable xs, abt '[] a)
go View (syn abt) xs a
v in (Variable a -> List1 Variable xs -> List1 Variable (a : xs)
forall a (a :: a -> *) (x :: a) (xs :: [a]).
a x -> List1 a xs -> List1 a (x : xs)
Cons1 Variable a
x List1 Variable xs
xs, abt '[] a
e)
underBinders
:: (ABT syn abt)
=> (abt '[] a -> abt '[] b)
-> abt xs a
-> abt xs b
underBinders :: (abt '[] a -> abt '[] b) -> abt xs a -> abt xs b
underBinders abt '[] a -> abt '[] b
f abt xs a
e =
let (List1 Variable xs
vars, abt '[] a
e') = abt xs a -> (List1 Variable xs, abt '[] a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> (List1 Variable xs, abt '[] a)
caseBinds abt xs a
e
in List1 Variable xs -> abt '[] b -> abt xs b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (b :: k).
ABT syn abt =>
List1 Variable xs -> abt '[] b -> abt xs b
binds_ List1 Variable xs
vars (abt '[] a -> abt '[] b
f abt '[] a
e')
maxNextFree :: (ABT syn abt, F.Foldable f) => f (Some2 abt) -> Nat
maxNextFree :: f (Some2 abt) -> Nat
maxNextFree = MaxNat -> Nat
unMaxNat (MaxNat -> Nat)
-> (f (Some2 abt) -> MaxNat) -> f (Some2 abt) -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Some2 abt -> MaxNat) -> f (Some2 abt) -> MaxNat
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap (\(Some2 abt i j
e) -> Nat -> MaxNat
MaxNat (Nat -> MaxNat) -> Nat -> MaxNat
forall a b. (a -> b) -> a -> b
$ abt i j -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFree abt i j
e)
maxNextBind :: (ABT syn abt, F.Foldable f) => f (Some2 abt) -> Nat
maxNextBind :: f (Some2 abt) -> Nat
maxNextBind = MaxNat -> Nat
unMaxNat (MaxNat -> Nat)
-> (f (Some2 abt) -> MaxNat) -> f (Some2 abt) -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Some2 abt -> MaxNat) -> f (Some2 abt) -> MaxNat
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap (\(Some2 abt i j
e) -> Nat -> MaxNat
MaxNat (Nat -> MaxNat) -> Nat -> MaxNat
forall a b. (a -> b) -> a -> b
$ abt i j -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextBind abt i j
e)
maxNextFreeOrBind :: (ABT syn abt, F.Foldable f) => f (Some2 abt) -> Nat
maxNextFreeOrBind :: f (Some2 abt) -> Nat
maxNextFreeOrBind =
MaxNat -> Nat
unMaxNat (MaxNat -> Nat)
-> (f (Some2 abt) -> MaxNat) -> f (Some2 abt) -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Some2 abt -> MaxNat) -> f (Some2 abt) -> MaxNat
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
F.foldMap (\(Some2 abt i j
e) -> Nat -> MaxNat
MaxNat (Nat -> MaxNat) -> Nat -> MaxNat
forall a b. (a -> b) -> a -> b
$ abt i j -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFreeOrBind abt i j
e)
newtype TrivialABT (syn :: ([k] -> k -> Type) -> k -> Type) (xs :: [k]) (a :: k) =
TrivialABT (View (syn (TrivialABT syn)) xs a)
instance (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), Foldable21 syn)
=> ABT (syn :: ([k] -> k -> Type) -> k -> Type) (TrivialABT syn)
where
syn :: syn (TrivialABT syn) a -> TrivialABT syn '[] a
syn syn (TrivialABT syn) a
t = View (syn (TrivialABT syn)) '[] a -> TrivialABT syn '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
View (syn (TrivialABT syn)) xs a -> TrivialABT syn xs a
TrivialABT (syn (TrivialABT syn) a -> View (syn (TrivialABT syn)) '[] a
forall k (rec :: k -> *) (a :: k). rec a -> View rec '[] a
Syn syn (TrivialABT syn) a
t)
var :: Variable a -> TrivialABT syn '[] a
var Variable a
x = View (syn (TrivialABT syn)) '[] a -> TrivialABT syn '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
View (syn (TrivialABT syn)) xs a -> TrivialABT syn xs a
TrivialABT (Variable a -> View (syn (TrivialABT syn)) '[] a
forall k (a :: k) (rec :: k -> *). Variable a -> View rec '[] a
Var Variable a
x)
bind :: Variable a -> TrivialABT syn xs b -> TrivialABT syn (a : xs) b
bind Variable a
x (TrivialABT View (syn (TrivialABT syn)) xs b
v) = View (syn (TrivialABT syn)) (a : xs) b -> TrivialABT syn (a : xs) b
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
View (syn (TrivialABT syn)) xs a -> TrivialABT syn xs a
TrivialABT (Variable a
-> View (syn (TrivialABT syn)) xs b
-> View (syn (TrivialABT syn)) (a : xs) b
forall a (a :: a) (rec :: a -> *) (xs :: [a]) (b :: a).
Variable a -> View rec xs b -> View rec (a : xs) b
Bind Variable a
x View (syn (TrivialABT syn)) xs b
v)
caseBind :: TrivialABT syn (x : xs) a
-> (Variable x -> TrivialABT syn xs a -> r) -> r
caseBind (TrivialABT View (syn (TrivialABT syn)) (x : xs) a
v) Variable x -> TrivialABT syn xs a -> r
k =
case View (syn (TrivialABT syn)) (x : xs) a
v of
Bind Variable a
x View (syn (TrivialABT syn)) xs a
v' -> Variable x -> TrivialABT syn xs a -> r
k Variable x
Variable a
x (View (syn (TrivialABT syn)) xs a -> TrivialABT syn xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
View (syn (TrivialABT syn)) xs a -> TrivialABT syn xs a
TrivialABT View (syn (TrivialABT syn)) xs a
v')
viewABT :: TrivialABT syn xs a -> View (syn (TrivialABT syn)) xs a
viewABT (TrivialABT View (syn (TrivialABT syn)) xs a
v) = View (syn (TrivialABT syn)) xs a
v
freeVars :: TrivialABT syn xs a -> VarSet (KindOf a)
freeVars = View (syn (TrivialABT syn)) xs a -> VarSet (KindOf a)
forall (xs :: [k]) (a :: k).
View (syn (TrivialABT syn)) xs a -> VarSet (KindOf a)
go (View (syn (TrivialABT syn)) xs a -> VarSet (KindOf a))
-> (TrivialABT syn xs a -> View (syn (TrivialABT syn)) xs a)
-> TrivialABT syn xs a
-> VarSet (KindOf a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TrivialABT syn xs a -> View (syn (TrivialABT syn)) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
where
go :: View (syn (TrivialABT syn)) xs a
-> VarSet (KindOf a)
go :: View (syn (TrivialABT syn)) xs a -> VarSet (KindOf a)
go (Syn syn (TrivialABT syn) a
t) = (forall (xs :: [k]) (a :: k).
TrivialABT syn xs a -> VarSet (KindOf a))
-> syn (TrivialABT syn) a -> VarSet (KindOf a)
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (xs :: [k]) (a :: k).
TrivialABT syn xs a -> VarSet (KindOf a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> VarSet (KindOf a)
freeVars syn (TrivialABT syn) a
t
go (Var Variable a
x) = Variable a -> VarSet (KindOf a)
forall k (a :: k). Variable a -> VarSet (KindOf a)
singletonVarSet Variable a
x
go (Bind Variable a
x View (syn (TrivialABT syn)) xs a
v) = Variable a -> VarSet (KindOf a) -> VarSet (KindOf a)
forall k (a :: k).
Variable a -> VarSet (KindOf a) -> VarSet (KindOf a)
deleteVarSet Variable a
x (View (syn (TrivialABT syn)) xs a -> VarSet (KindOf a)
forall (xs :: [k]) (a :: k).
View (syn (TrivialABT syn)) xs a -> VarSet (KindOf a)
go View (syn (TrivialABT syn)) xs a
v)
nextBind :: TrivialABT syn xs a -> Nat
nextBind = View (syn (TrivialABT syn)) xs a -> Nat
forall (xs :: [k]) (a :: k).
View (syn (TrivialABT syn)) xs a -> Nat
go (View (syn (TrivialABT syn)) xs a -> Nat)
-> (TrivialABT syn xs a -> View (syn (TrivialABT syn)) xs a)
-> TrivialABT syn xs a
-> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TrivialABT syn xs a -> View (syn (TrivialABT syn)) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
where
go :: View (syn (TrivialABT syn)) xs a -> Nat
go :: View (syn (TrivialABT syn)) xs a -> Nat
go (Syn syn (TrivialABT syn) a
t) = MaxNat -> Nat
unMaxNat (MaxNat -> Nat) -> MaxNat -> Nat
forall a b. (a -> b) -> a -> b
$ (forall (h :: [k]) (i :: k). TrivialABT syn h i -> MaxNat)
-> syn (TrivialABT syn) a -> MaxNat
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 (Nat -> MaxNat
MaxNat (Nat -> MaxNat)
-> (TrivialABT syn h i -> Nat) -> TrivialABT syn h i -> MaxNat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TrivialABT syn h i -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextBind) syn (TrivialABT syn) a
t
go (Var Variable a
_) = MaxNat -> Nat
unMaxNat (MaxNat -> Nat) -> MaxNat -> Nat
forall a b. (a -> b) -> a -> b
$ MaxNat
forall a. Monoid a => a
mempty
go (Bind Variable a
x View (syn (TrivialABT syn)) xs a
v) = Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max (Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
x) (View (syn (TrivialABT syn)) xs a -> Nat
forall (xs :: [k]) (a :: k).
View (syn (TrivialABT syn)) xs a -> Nat
go View (syn (TrivialABT syn)) xs a
v)
nextFreeOrBind :: TrivialABT syn xs a -> Nat
nextFreeOrBind = View (syn (TrivialABT syn)) xs a -> Nat
forall (xs :: [k]) (a :: k).
View (syn (TrivialABT syn)) xs a -> Nat
go (View (syn (TrivialABT syn)) xs a -> Nat)
-> (TrivialABT syn xs a -> View (syn (TrivialABT syn)) xs a)
-> TrivialABT syn xs a
-> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TrivialABT syn xs a -> View (syn (TrivialABT syn)) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
where
go :: View (syn (TrivialABT syn)) xs a -> Nat
go :: View (syn (TrivialABT syn)) xs a -> Nat
go (Syn syn (TrivialABT syn) a
t) = MaxNat -> Nat
unMaxNat (MaxNat -> Nat) -> MaxNat -> Nat
forall a b. (a -> b) -> a -> b
$ (forall (h :: [k]) (i :: k). TrivialABT syn h i -> MaxNat)
-> syn (TrivialABT syn) a -> MaxNat
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 (Nat -> MaxNat
MaxNat (Nat -> MaxNat)
-> (TrivialABT syn h i -> Nat) -> TrivialABT syn h i -> MaxNat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TrivialABT syn h i -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFreeOrBind) syn (TrivialABT syn) a
t
go (Var Variable a
x) = Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
x
go (Bind Variable a
x View (syn (TrivialABT syn)) xs a
v) = Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max (Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
x) (View (syn (TrivialABT syn)) xs a -> Nat
forall (xs :: [k]) (a :: k).
View (syn (TrivialABT syn)) xs a -> Nat
go View (syn (TrivialABT syn)) xs a
v)
instance (Show1 (Sing :: k -> Type), Show1 (syn (TrivialABT syn)))
=> Show2 (TrivialABT (syn :: ([k] -> k -> Type) -> k -> Type))
where
showsPrec2 :: Int -> TrivialABT syn i j -> ShowS
showsPrec2 Int
p (TrivialABT (Syn syn (TrivialABT syn) j
t)) = Int -> String -> syn (TrivialABT syn) j -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"syn" syn (TrivialABT syn) j
t
showsPrec2 Int
p (TrivialABT (Var Variable j
x)) = Int -> String -> Variable j -> ShowS
forall k (a :: k -> *) (i :: k).
Show1 a =>
Int -> String -> a i -> ShowS
showParen_1 Int
p String
"var" Variable j
x
showsPrec2 Int
p (TrivialABT (Bind Variable a
x View (syn (TrivialABT syn)) xs j
v)) = Int -> String -> Variable a -> TrivialABT syn xs j -> ShowS
forall k1 k2 (a :: k1 -> *) (b :: k2 -> *) (i :: k1) (j :: k2).
(Show1 a, Show1 b) =>
Int -> String -> a i -> b j -> ShowS
showParen_11 Int
p String
"bind" Variable a
x (View (syn (TrivialABT syn)) xs j -> TrivialABT syn xs j
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
View (syn (TrivialABT syn)) xs a -> TrivialABT syn xs a
TrivialABT View (syn (TrivialABT syn)) xs j
v)
instance (Show1 (Sing :: k -> Type), Show1 (syn (TrivialABT syn)))
=> Show1 (TrivialABT (syn :: ([k] -> k -> Type) -> k -> Type) xs)
where
showsPrec1 :: Int -> TrivialABT syn xs i -> ShowS
showsPrec1 = Int -> TrivialABT syn xs i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2
show1 :: TrivialABT syn xs i -> String
show1 = TrivialABT syn xs i -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2
instance (Show1 (Sing :: k -> Type), Show1 (syn (TrivialABT syn)))
=> Show (TrivialABT (syn :: ([k] -> k -> Type) -> k -> Type) xs a)
where
showsPrec :: Int -> TrivialABT syn xs a -> ShowS
showsPrec = Int -> TrivialABT syn xs a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: TrivialABT syn xs a -> String
show = TrivialABT syn xs a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
data MemoizedABT (syn :: ([k] -> k -> Type) -> k -> Type) (xs :: [k]) (a :: k) =
MemoizedABT
{ MemoizedABT syn xs a -> VarSet (KindOf a)
_memoizedFreeVars :: VarSet (KindOf a)
, MemoizedABT syn xs a -> Nat
memoizedNextFree :: Nat
, MemoizedABT syn xs a -> Nat
memoizedNextBind :: {-# UNPACK #-} !Nat
, MemoizedABT syn xs a -> View (syn (MemoizedABT syn)) xs a
memoizedView :: !(View (syn (MemoizedABT syn)) xs a)
}
memoizedFreeVars :: MemoizedABT syn xs a -> VarSet (KindOf a)
memoizedFreeVars :: MemoizedABT syn xs a -> VarSet (KindOf a)
memoizedFreeVars (MemoizedABT VarSet (KindOf a)
xs Nat
_ Nat
_ View (syn (MemoizedABT syn)) xs a
_) = VarSet (KindOf a)
xs
instance (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), Foldable21 syn)
=> ABT (syn :: ([k] -> k -> Type) -> k -> Type) (MemoizedABT syn)
where
syn :: syn (MemoizedABT syn) a -> MemoizedABT syn '[] a
syn syn (MemoizedABT syn) a
t =
VarSet (KindOf a)
-> Nat
-> Nat
-> View (syn (MemoizedABT syn)) '[] a
-> MemoizedABT syn '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
VarSet (KindOf a)
-> Nat
-> Nat
-> View (syn (MemoizedABT syn)) xs a
-> MemoizedABT syn xs a
MemoizedABT
((forall (xs :: [k]) (a :: k).
MemoizedABT syn xs a -> VarSet (KindOf a))
-> syn (MemoizedABT syn) a -> VarSet (KindOf a)
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (xs :: [k]) (a :: k).
MemoizedABT syn xs a -> VarSet (KindOf a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> VarSet (KindOf a)
freeVars syn (MemoizedABT syn) a
t)
(MaxNat -> Nat
unMaxNat (MaxNat -> Nat) -> MaxNat -> Nat
forall a b. (a -> b) -> a -> b
$ (forall (h :: [k]) (i :: k). MemoizedABT syn h i -> MaxNat)
-> syn (MemoizedABT syn) a -> MaxNat
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 (Nat -> MaxNat
MaxNat (Nat -> MaxNat)
-> (MemoizedABT syn h i -> Nat) -> MemoizedABT syn h i -> MaxNat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MemoizedABT syn h i -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFree) syn (MemoizedABT syn) a
t)
(MaxNat -> Nat
unMaxNat (MaxNat -> Nat) -> MaxNat -> Nat
forall a b. (a -> b) -> a -> b
$ (forall (h :: [k]) (i :: k). MemoizedABT syn h i -> MaxNat)
-> syn (MemoizedABT syn) a -> MaxNat
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 (Nat -> MaxNat
MaxNat (Nat -> MaxNat)
-> (MemoizedABT syn h i -> Nat) -> MemoizedABT syn h i -> MaxNat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MemoizedABT syn h i -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextBind) syn (MemoizedABT syn) a
t)
(syn (MemoizedABT syn) a -> View (syn (MemoizedABT syn)) '[] a
forall k (rec :: k -> *) (a :: k). rec a -> View rec '[] a
Syn syn (MemoizedABT syn) a
t)
var :: Variable a -> MemoizedABT syn '[] a
var Variable a
x =
VarSet (KindOf a)
-> Nat
-> Nat
-> View (syn (MemoizedABT syn)) '[] a
-> MemoizedABT syn '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
VarSet (KindOf a)
-> Nat
-> Nat
-> View (syn (MemoizedABT syn)) xs a
-> MemoizedABT syn xs a
MemoizedABT
(Variable a -> VarSet (KindOf a)
forall k (a :: k). Variable a -> VarSet (KindOf a)
singletonVarSet Variable a
x)
(Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
x)
Nat
0
(Variable a -> View (syn (MemoizedABT syn)) '[] a
forall k (a :: k) (rec :: k -> *). Variable a -> View rec '[] a
Var Variable a
x)
bind :: Variable a -> MemoizedABT syn xs b -> MemoizedABT syn (a : xs) b
bind Variable a
x (MemoizedABT VarSet (KindOf a)
xs Nat
_ Nat
nb View (syn (MemoizedABT syn)) xs b
v) =
let xs' :: VarSet (KindOf a)
xs' = Variable a -> VarSet (KindOf a) -> VarSet (KindOf a)
forall k (a :: k).
Variable a -> VarSet (KindOf a) -> VarSet (KindOf a)
deleteVarSet Variable a
x VarSet (KindOf a)
xs
in VarSet (KindOf a)
-> Nat
-> Nat
-> View (syn (MemoizedABT syn)) (a : xs) b
-> MemoizedABT syn (a : xs) b
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
VarSet (KindOf a)
-> Nat
-> Nat
-> View (syn (MemoizedABT syn)) xs a
-> MemoizedABT syn xs a
MemoizedABT
VarSet (KindOf a)
xs'
(VarSet (KindOf a) -> Nat
forall k (kproxy :: KProxy k). VarSet kproxy -> Nat
nextVarID VarSet (KindOf a)
xs')
((Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
x) Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
`max` Nat
nb)
(Variable a
-> View (syn (MemoizedABT syn)) xs b
-> View (syn (MemoizedABT syn)) (a : xs) b
forall a (a :: a) (rec :: a -> *) (xs :: [a]) (b :: a).
Variable a -> View rec xs b -> View rec (a : xs) b
Bind Variable a
x View (syn (MemoizedABT syn)) xs b
v)
caseBind :: MemoizedABT syn (x : xs) a
-> (Variable x -> MemoizedABT syn xs a -> r) -> r
caseBind (MemoizedABT VarSet (KindOf a)
xs Nat
nf Nat
nb View (syn (MemoizedABT syn)) (x : xs) a
v) Variable x -> MemoizedABT syn xs a -> r
k =
case View (syn (MemoizedABT syn)) (x : xs) a
v of
Bind Variable a
x View (syn (MemoizedABT syn)) xs a
v' ->
Variable x -> MemoizedABT syn xs a -> r
k Variable x
Variable a
x (MemoizedABT syn xs a -> r) -> MemoizedABT syn xs a -> r
forall a b. (a -> b) -> a -> b
$ VarSet (KindOf a)
-> Nat
-> Nat
-> View (syn (MemoizedABT syn)) xs a
-> MemoizedABT syn xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
VarSet (KindOf a)
-> Nat
-> Nat
-> View (syn (MemoizedABT syn)) xs a
-> MemoizedABT syn xs a
MemoizedABT
(Variable a -> VarSet (KindOf a) -> VarSet (KindOf a)
forall k (a :: k).
Variable a -> VarSet (KindOf a) -> VarSet (KindOf a)
insertVarSet Variable a
x VarSet (KindOf a)
xs)
((Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
x) Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
`max` Nat
nf)
Nat
nb
View (syn (MemoizedABT syn)) xs a
v'
viewABT :: MemoizedABT syn xs a -> View (syn (MemoizedABT syn)) xs a
viewABT = MemoizedABT syn xs a -> View (syn (MemoizedABT syn)) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
MemoizedABT syn xs a -> View (syn (MemoizedABT syn)) xs a
memoizedView
freeVars :: MemoizedABT syn xs a -> VarSet (KindOf a)
freeVars = MemoizedABT syn xs a -> VarSet (KindOf a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
MemoizedABT syn xs a -> VarSet (KindOf a)
memoizedFreeVars
nextFree :: MemoizedABT syn xs a -> Nat
nextFree = MemoizedABT syn xs a -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
MemoizedABT syn xs a -> Nat
memoizedNextFree
nextBind :: MemoizedABT syn xs a -> Nat
nextBind = MemoizedABT syn xs a -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k]) (a :: k).
MemoizedABT syn xs a -> Nat
memoizedNextBind
instance (Show1 (Sing :: k -> Type), Show1 (syn (MemoizedABT syn)))
=> Show2 (MemoizedABT (syn :: ([k] -> k -> Type) -> k -> Type))
where
showsPrec2 :: Int -> MemoizedABT syn i j -> ShowS
showsPrec2 Int
p (MemoizedABT VarSet (KindOf j)
xs Nat
nf Nat
nb View (syn (MemoizedABT syn)) i j
v) =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
"MemoizedABT "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> VarSet (KindOf j) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 VarSet (KindOf j)
xs
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Nat
nf
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Nat
nb
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> View (syn (MemoizedABT syn)) i j -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 View (syn (MemoizedABT syn)) i j
v
)
instance (Show1 (Sing :: k -> Type), Show1 (syn (MemoizedABT syn)))
=> Show1 (MemoizedABT (syn :: ([k] -> k -> Type) -> k -> Type) xs)
where
showsPrec1 :: Int -> MemoizedABT syn xs i -> ShowS
showsPrec1 = Int -> MemoizedABT syn xs i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2
show1 :: MemoizedABT syn xs i -> String
show1 = MemoizedABT syn xs i -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2
instance (Show1 (Sing :: k -> Type), Show1 (syn (MemoizedABT syn)))
=> Show (MemoizedABT (syn :: ([k] -> k -> Type) -> k -> Type) xs a)
where
showsPrec :: Int -> MemoizedABT syn xs a -> ShowS
showsPrec = Int -> MemoizedABT syn xs a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: MemoizedABT syn xs a -> String
show = MemoizedABT syn xs a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
data MetaABT
(meta :: Type)
(syn :: ([k] -> k -> Type) -> k -> Type)
(xs :: [k])
(a :: k) =
MetaABT
{ MetaABT meta syn xs a -> Maybe meta
getMetadata :: !(Maybe meta)
, MetaABT meta syn xs a -> View (syn (MetaABT meta syn)) xs a
metaView :: !(View (syn (MetaABT meta syn)) xs a)
}
withMetadata
:: meta
-> MetaABT meta syn xs a
-> MetaABT meta syn xs a
withMetadata :: meta -> MetaABT meta syn xs a -> MetaABT meta syn xs a
withMetadata meta
x (MetaABT Maybe meta
_ View (syn (MetaABT meta syn)) xs a
v) = Maybe meta
-> View (syn (MetaABT meta syn)) xs a -> MetaABT meta syn xs a
forall k meta (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k])
(a :: k).
Maybe meta
-> View (syn (MetaABT meta syn)) xs a -> MetaABT meta syn xs a
MetaABT (meta -> Maybe meta
forall a. a -> Maybe a
Just meta
x) View (syn (MetaABT meta syn)) xs a
v
instance (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), Foldable21 syn)
=> ABT (syn :: ([k] -> k -> Type) -> k -> Type) (MetaABT meta syn)
where
syn :: syn (MetaABT meta syn) a -> MetaABT meta syn '[] a
syn syn (MetaABT meta syn) a
t = Maybe meta
-> View (syn (MetaABT meta syn)) '[] a -> MetaABT meta syn '[] a
forall k meta (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k])
(a :: k).
Maybe meta
-> View (syn (MetaABT meta syn)) xs a -> MetaABT meta syn xs a
MetaABT Maybe meta
forall a. Maybe a
Nothing (syn (MetaABT meta syn) a -> View (syn (MetaABT meta syn)) '[] a
forall k (rec :: k -> *) (a :: k). rec a -> View rec '[] a
Syn syn (MetaABT meta syn) a
t)
var :: Variable a -> MetaABT meta syn '[] a
var Variable a
x = Maybe meta
-> View (syn (MetaABT meta syn)) '[] a -> MetaABT meta syn '[] a
forall k meta (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k])
(a :: k).
Maybe meta
-> View (syn (MetaABT meta syn)) xs a -> MetaABT meta syn xs a
MetaABT Maybe meta
forall a. Maybe a
Nothing (Variable a -> View (syn (MetaABT meta syn)) '[] a
forall k (a :: k) (rec :: k -> *). Variable a -> View rec '[] a
Var Variable a
x)
bind :: Variable a -> MetaABT meta syn xs b -> MetaABT meta syn (a : xs) b
bind Variable a
x (MetaABT Maybe meta
meta View (syn (MetaABT meta syn)) xs b
v) = Maybe meta
-> View (syn (MetaABT meta syn)) (a : xs) b
-> MetaABT meta syn (a : xs) b
forall k meta (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k])
(a :: k).
Maybe meta
-> View (syn (MetaABT meta syn)) xs a -> MetaABT meta syn xs a
MetaABT Maybe meta
meta (Variable a
-> View (syn (MetaABT meta syn)) xs b
-> View (syn (MetaABT meta syn)) (a : xs) b
forall a (a :: a) (rec :: a -> *) (xs :: [a]) (b :: a).
Variable a -> View rec xs b -> View rec (a : xs) b
Bind Variable a
x View (syn (MetaABT meta syn)) xs b
v)
caseBind :: MetaABT meta syn (x : xs) a
-> (Variable x -> MetaABT meta syn xs a -> r) -> r
caseBind (MetaABT Maybe meta
meta View (syn (MetaABT meta syn)) (x : xs) a
v) Variable x -> MetaABT meta syn xs a -> r
k =
case View (syn (MetaABT meta syn)) (x : xs) a
v of
Bind Variable a
x View (syn (MetaABT meta syn)) xs a
v' -> Variable x -> MetaABT meta syn xs a -> r
k Variable x
Variable a
x (Maybe meta
-> View (syn (MetaABT meta syn)) xs a -> MetaABT meta syn xs a
forall k meta (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k])
(a :: k).
Maybe meta
-> View (syn (MetaABT meta syn)) xs a -> MetaABT meta syn xs a
MetaABT Maybe meta
meta View (syn (MetaABT meta syn)) xs a
v')
viewABT :: MetaABT meta syn xs a -> View (syn (MetaABT meta syn)) xs a
viewABT = MetaABT meta syn xs a -> View (syn (MetaABT meta syn)) xs a
forall meta k (syn :: ([k] -> k -> *) -> k -> *) (xs :: [k])
(a :: k).
MetaABT meta syn xs a -> View (syn (MetaABT meta syn)) xs a
metaView
freeVars :: MetaABT meta syn xs a -> VarSet (KindOf a)
freeVars = View (syn (MetaABT meta syn)) xs a -> VarSet (KindOf a)
forall (xs :: [k]) (a :: k).
View (syn (MetaABT meta syn)) xs a -> VarSet (KindOf a)
go (View (syn (MetaABT meta syn)) xs a -> VarSet (KindOf a))
-> (MetaABT meta syn xs a -> View (syn (MetaABT meta syn)) xs a)
-> MetaABT meta syn xs a
-> VarSet (KindOf a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaABT meta syn xs a -> View (syn (MetaABT meta syn)) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
where
go :: View (syn (MetaABT meta syn)) xs a
-> VarSet (KindOf a)
go :: View (syn (MetaABT meta syn)) xs a -> VarSet (KindOf a)
go (Syn syn (MetaABT meta syn) a
t) = (forall (xs :: [k]) (a :: k).
MetaABT meta syn xs a -> VarSet (KindOf a))
-> syn (MetaABT meta syn) a -> VarSet (KindOf a)
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 forall (xs :: [k]) (a :: k).
MetaABT meta syn xs a -> VarSet (KindOf a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> VarSet (KindOf a)
freeVars syn (MetaABT meta syn) a
t
go (Var Variable a
x) = Variable a -> VarSet (KindOf a)
forall k (a :: k). Variable a -> VarSet (KindOf a)
singletonVarSet Variable a
x
go (Bind Variable a
x View (syn (MetaABT meta syn)) xs a
v) = Variable a -> VarSet (KindOf a) -> VarSet (KindOf a)
forall k (a :: k).
Variable a -> VarSet (KindOf a) -> VarSet (KindOf a)
deleteVarSet Variable a
x (View (syn (MetaABT meta syn)) xs a -> VarSet (KindOf a)
forall (xs :: [k]) (a :: k).
View (syn (MetaABT meta syn)) xs a -> VarSet (KindOf a)
go View (syn (MetaABT meta syn)) xs a
v)
nextBind :: MetaABT meta syn xs a -> Nat
nextBind = View (syn (MetaABT meta syn)) xs a -> Nat
forall (xs :: [k]) (a :: k).
View (syn (MetaABT meta syn)) xs a -> Nat
go (View (syn (MetaABT meta syn)) xs a -> Nat)
-> (MetaABT meta syn xs a -> View (syn (MetaABT meta syn)) xs a)
-> MetaABT meta syn xs a
-> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaABT meta syn xs a -> View (syn (MetaABT meta syn)) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
where
go :: View (syn (MetaABT meta syn)) xs a -> Nat
go :: View (syn (MetaABT meta syn)) xs a -> Nat
go (Syn syn (MetaABT meta syn) a
t) = MaxNat -> Nat
unMaxNat (MaxNat -> Nat) -> MaxNat -> Nat
forall a b. (a -> b) -> a -> b
$ (forall (h :: [k]) (i :: k). MetaABT meta syn h i -> MaxNat)
-> syn (MetaABT meta syn) a -> MaxNat
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 (Nat -> MaxNat
MaxNat (Nat -> MaxNat)
-> (MetaABT meta syn h i -> Nat) -> MetaABT meta syn h i -> MaxNat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaABT meta syn h i -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextBind) syn (MetaABT meta syn) a
t
go (Var Variable a
_) = MaxNat -> Nat
unMaxNat (MaxNat -> Nat) -> MaxNat -> Nat
forall a b. (a -> b) -> a -> b
$ MaxNat
forall a. Monoid a => a
mempty
go (Bind Variable a
x View (syn (MetaABT meta syn)) xs a
v) = Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max (Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
x) (View (syn (MetaABT meta syn)) xs a -> Nat
forall (xs :: [k]) (a :: k).
View (syn (MetaABT meta syn)) xs a -> Nat
go View (syn (MetaABT meta syn)) xs a
v)
nextFreeOrBind :: MetaABT meta syn xs a -> Nat
nextFreeOrBind = View (syn (MetaABT meta syn)) xs a -> Nat
forall (xs :: [k]) (a :: k).
View (syn (MetaABT meta syn)) xs a -> Nat
go (View (syn (MetaABT meta syn)) xs a -> Nat)
-> (MetaABT meta syn xs a -> View (syn (MetaABT meta syn)) xs a)
-> MetaABT meta syn xs a
-> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaABT meta syn xs a -> View (syn (MetaABT meta syn)) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
where
go :: View (syn (MetaABT meta syn)) xs a -> Nat
go :: View (syn (MetaABT meta syn)) xs a -> Nat
go (Syn syn (MetaABT meta syn) a
t) = MaxNat -> Nat
unMaxNat (MaxNat -> Nat) -> MaxNat -> Nat
forall a b. (a -> b) -> a -> b
$ (forall (h :: [k]) (i :: k). MetaABT meta syn h i -> MaxNat)
-> syn (MetaABT meta syn) a -> MaxNat
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
(a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 (Nat -> MaxNat
MaxNat (Nat -> MaxNat)
-> (MetaABT meta syn h i -> Nat) -> MetaABT meta syn h i -> MaxNat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaABT meta syn h i -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFreeOrBind) syn (MetaABT meta syn) a
t
go (Var Variable a
x) = Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
x
go (Bind Variable a
x View (syn (MetaABT meta syn)) xs a
v) = Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max (Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
x) (View (syn (MetaABT meta syn)) xs a -> Nat
forall (xs :: [k]) (a :: k).
View (syn (MetaABT meta syn)) xs a -> Nat
go View (syn (MetaABT meta syn)) xs a
v)
instance ( Show1 (Sing :: k -> Type)
, Show1 (syn (MetaABT meta syn))
, Show meta)
=> Show2 (MetaABT meta (syn :: ([k] -> k -> Type) -> k -> Type))
where
showsPrec2 :: Int -> MetaABT meta syn i j -> ShowS
showsPrec2 Int
p (MetaABT Maybe meta
meta View (syn (MetaABT meta syn)) i j
v) =
Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
( String -> ShowS
showString String
"MetaABT "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe meta -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Maybe meta
meta
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> View (syn (MetaABT meta syn)) i j -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 View (syn (MetaABT meta syn)) i j
v
)
instance ( Show1 (Sing :: k -> Type)
, Show1 (syn (MetaABT meta syn))
, Show meta)
=> Show1 (MetaABT meta (syn :: ([k] -> k -> Type) -> k -> Type) xs)
where
showsPrec1 :: Int -> MetaABT meta syn xs i -> ShowS
showsPrec1 = Int -> MetaABT meta syn xs i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2
show1 :: MetaABT meta syn xs i -> String
show1 = MetaABT meta syn xs i -> String
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
a i j -> String
show2
instance ( Show1 (Sing :: k -> Type)
, Show1 (syn (MetaABT meta syn))
, Show meta)
=> Show (MetaABT meta (syn :: ([k] -> k -> Type) -> k -> Type) xs a)
where
showsPrec :: Int -> MetaABT meta syn xs a -> ShowS
showsPrec = Int -> MetaABT meta syn xs a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
show :: MetaABT meta syn xs a -> String
show = MetaABT meta syn xs a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1
freshen
:: (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type))
=> Variable (a :: k)
-> VarSet (KindOf a)
-> Variable a
freshen :: Variable a -> VarSet (KindOf a) -> Variable a
freshen Variable a
x VarSet (KindOf a)
xs
| Variable a
x Variable a -> VarSet (KindOf a) -> Bool
forall k (a :: k) (kproxy :: KProxy k).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> VarSet kproxy -> Bool
`memberVarSet` VarSet (KindOf a)
xs = let i :: Nat
i = VarSet (KindOf a) -> Nat
forall k (kproxy :: KProxy k). VarSet kproxy -> Nat
nextVarID VarSet (KindOf a)
xs in Nat
i Nat -> Variable a -> Variable a
`seq` Variable a
x{varID :: Nat
varID = Nat
i}
| Bool
otherwise = Variable a
x
rename
:: forall k syn abt (a :: k) xs (b :: k)
. (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), Functor21 syn, ABT syn abt)
=> Variable a
-> Variable a
-> abt xs b
-> abt xs b
rename :: Variable a -> Variable a -> abt xs b -> abt xs b
rename Variable a
x Variable a
y =
#ifdef __TRACE_DISINTEGRATE__
trace ("renaming " ++ show (varID x)
++ " to " ++ show (varID y)) $
#endif
abt xs b -> abt xs b
forall (xs' :: [k]) (b' :: k). abt xs' b' -> abt xs' b'
start
where
start :: forall xs' b'. abt xs' b' -> abt xs' b'
start :: abt xs' b' -> abt xs' b'
start abt xs' b'
e = abt xs' b' -> View (syn abt) xs' b' -> abt xs' b'
forall (xs' :: [k]) (b' :: k).
abt xs' b' -> View (syn abt) xs' b' -> abt xs' b'
loop abt xs' b'
e (abt xs' b' -> View (syn abt) xs' b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs' b'
e)
loop :: forall xs' b'. abt xs' b' -> View (syn abt) xs' b' -> abt xs' b'
loop :: abt xs' b' -> View (syn abt) xs' b' -> abt xs' b'
loop abt xs' b'
_ (Syn syn abt b'
t) = syn abt b' -> abt '[] b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (syn abt b' -> abt '[] b') -> syn abt b' -> abt '[] b'
forall a b. (a -> b) -> a -> b
$! (forall (xs' :: [k]) (b' :: k). abt xs' b' -> abt xs' b')
-> syn abt b' -> syn abt b'
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 forall (xs' :: [k]) (b' :: k). abt xs' b' -> abt xs' b'
start syn abt b'
t
loop abt xs' b'
e (Var Variable b'
z) =
case Variable a -> Variable b' -> Maybe (TypeEq a b')
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> Variable b -> Maybe (TypeEq a b)
varEq Variable a
x Variable b'
z of
Just TypeEq a b'
Refl -> Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
y
Maybe (TypeEq a b')
Nothing -> abt xs' b'
e
loop abt xs' b'
e (Bind Variable a
z View (syn abt) xs b'
v) =
#ifdef __TRACE_DISINTEGRATE__
trace ("checking varEq "++ show (varID x) ++ " " ++ show (varID z)) $
#endif
case Variable a -> Variable a -> Maybe (TypeEq a a)
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> Variable b -> Maybe (TypeEq a b)
varEq Variable a
x Variable a
z of
Just TypeEq a a
Refl -> abt xs' b'
e
Maybe (TypeEq a a)
Nothing -> Variable a -> abt xs b' -> abt (a : xs) b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
z (abt xs b' -> abt (a : xs) b') -> abt xs b' -> abt (a : xs) b'
forall a b. (a -> b) -> a -> b
$ abt xs b' -> View (syn abt) xs b' -> abt xs b'
forall (xs' :: [k]) (b' :: k).
abt xs' b' -> View (syn abt) xs' b' -> abt xs' b'
loop (abt (a : xs) b'
-> (Variable a -> abt xs b' -> abt xs b') -> abt xs b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt xs' b'
abt (a : xs) b'
e ((Variable a -> abt xs b' -> abt xs b') -> abt xs b')
-> (Variable a -> abt xs b' -> abt xs b') -> abt xs b'
forall a b. (a -> b) -> a -> b
$ (abt xs b' -> abt xs b') -> Variable a -> abt xs b' -> abt xs b'
forall a b. a -> b -> a
const abt xs b' -> abt xs b'
forall a. a -> a
id) View (syn abt) xs b'
v
subst
:: forall k syn abt (a :: k) xs (b :: k)
. (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), Traversable21 syn, ABT syn abt)
=> Variable a
-> abt '[] a
-> abt xs b
-> abt xs b
subst :: Variable a -> abt '[] a -> abt xs b -> abt xs b
subst Variable a
x abt '[] a
e =
#ifdef __TRACE_DISINTEGRATE__
trace ("about to subst " ++ show (varID x)) $
#endif
Identity (abt xs b) -> abt xs b
forall a. Identity a -> a
runIdentity (Identity (abt xs b) -> abt xs b)
-> (abt xs b -> Identity (abt xs b)) -> abt xs b -> abt xs b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable a
-> abt '[] a
-> (forall (b' :: k). Variable b' -> Identity (abt '[] b'))
-> abt xs b
-> Identity (abt xs b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k) (m :: * -> *).
(JmEq1 Sing, Show1 Sing, Traversable21 syn, ABT syn abt,
Applicative m, Functor m, Monad m) =>
Variable a
-> abt '[] a
-> (forall (b' :: k). Variable b' -> m (abt '[] b'))
-> abt xs b
-> m (abt xs b)
substM Variable a
x abt '[] a
e forall (b' :: k). Variable b' -> Identity (abt '[] b')
forall (m :: * -> *) (b' :: k).
(Applicative m, Functor m, Monad m) =>
Variable b' -> m (abt '[] b')
varCase
where
varCase :: forall m b'. (Applicative m, Functor m, Monad m)
=> Variable b' -> m (abt '[] b')
varCase :: Variable b' -> m (abt '[] b')
varCase = abt '[] b' -> m (abt '[] b')
forall (m :: * -> *) a. Monad m => a -> m a
return (abt '[] b' -> m (abt '[] b'))
-> (Variable b' -> abt '[] b') -> Variable b' -> m (abt '[] b')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable b' -> abt '[] b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var
substM
:: forall k syn abt (a :: k) xs (b :: k) m
. (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type),
Traversable21 syn, ABT syn abt,
Applicative m, Functor m, Monad m)
=> Variable a
-> abt '[] a
-> (forall b'. Variable b' -> m (abt '[] b'))
-> abt xs b
-> m (abt xs b)
substM :: Variable a
-> abt '[] a
-> (forall (b' :: k). Variable b' -> m (abt '[] b'))
-> abt xs b
-> m (abt xs b)
substM Variable a
x abt '[] a
e forall (b' :: k). Variable b' -> m (abt '[] b')
vf =
Nat -> abt xs b -> m (abt xs b)
forall (xs' :: [k]) (b' :: k). Nat -> abt xs' b' -> m (abt xs' b')
start ([Some2 abt] -> Nat
forall k2 (syn :: ([k2] -> k2 -> *) -> k2 -> *)
(abt :: [k2] -> k2 -> *) (f :: * -> *).
(ABT syn abt, Foldable f) =>
f (Some2 abt) -> Nat
maxNextFreeOrBind [abt '[] a -> Some2 abt
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
x), abt '[] a -> Some2 abt
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
a i j -> Some2 a
Some2 abt '[] a
e])
where
start :: forall xs' b'. Nat -> abt xs' b' -> m (abt xs' b')
start :: Nat -> abt xs' b' -> m (abt xs' b')
start Nat
n abt xs' b'
f = Nat -> abt xs' b' -> View (syn abt) xs' b' -> m (abt xs' b')
forall (xs' :: [k]) (b' :: k).
Nat -> abt xs' b' -> View (syn abt) xs' b' -> m (abt xs' b')
loop Nat
n abt xs' b'
f (abt xs' b' -> View (syn abt) xs' b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs' b'
f)
loop :: forall xs' b'
. Nat -> abt xs' b' -> View (syn abt) xs' b' -> m (abt xs' b')
loop :: Nat -> abt xs' b' -> View (syn abt) xs' b' -> m (abt xs' b')
loop Nat
n abt xs' b'
_ (Syn syn abt b'
t) = syn abt b' -> abt '[] b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (syn abt b' -> abt '[] b') -> m (syn abt b') -> m (abt '[] b')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (h :: [k]) (i :: k). abt h i -> m (abt h i))
-> syn abt b' -> m (syn abt b')
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 (Nat -> abt h i -> m (abt h i)
forall (xs' :: [k]) (b' :: k). Nat -> abt xs' b' -> m (abt xs' b')
start Nat
n) syn abt b'
t
loop Nat
_ abt xs' b'
_ (Var Variable b'
z) =
#ifdef __TRACE_DISINTEGRATE__
trace ("checking varEq " ++ show (varID x) ++ " " ++ show (varID z)) $
#endif
case Variable a -> Variable b' -> Maybe (TypeEq a b')
forall k (a :: k) (b :: k).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> Variable b -> Maybe (TypeEq a b)
varEq Variable a
x Variable b'
z of
Just TypeEq a b'
Refl -> abt '[] a -> m (abt '[] a)
forall (m :: * -> *) a. Monad m => a -> m a
return abt '[] a
e
Maybe (TypeEq a b')
Nothing -> Variable b' -> m (abt '[] b')
forall (b' :: k). Variable b' -> m (abt '[] b')
vf Variable b'
z
loop Nat
n abt xs' b'
f (Bind Variable a
z View (syn abt) xs b'
b) =
if (Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
x Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
z) then abt xs' b' -> m (abt xs' b')
forall (m :: * -> *) a. Monad m => a -> m a
return abt xs' b'
f
else do
let i :: Nat
i = Nat
1 Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max Nat
n (abt xs' b' -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFreeOrBind abt xs' b'
f)
z' :: Variable a
z' = Nat
i Nat -> Variable a -> Variable a
`seq` Variable a
z{varID :: Nat
varID = Nat
i}
abt xs b'
f'' <- Variable a
-> abt '[] a
-> (forall (b' :: k). Variable b' -> m (abt '[] b'))
-> abt xs b'
-> m (abt xs b')
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k) (m :: * -> *).
(JmEq1 Sing, Show1 Sing, Traversable21 syn, ABT syn abt,
Applicative m, Functor m, Monad m) =>
Variable a
-> abt '[] a
-> (forall (b' :: k). Variable b' -> m (abt '[] b'))
-> abt xs b
-> m (abt xs b)
substM Variable a
z (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
z') forall (b' :: k). Variable b' -> m (abt '[] b')
vf (View (syn abt) xs b' -> abt xs b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
View (syn abt) xs a -> abt xs a
unviewABT View (syn abt) xs b'
b)
Variable a -> abt xs b' -> abt (a : xs) b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
z' (abt xs b' -> abt (a : xs) b')
-> m (abt xs b') -> m (abt (a : xs) b')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat -> abt xs b' -> View (syn abt) xs b' -> m (abt xs b')
forall (xs' :: [k]) (b' :: k).
Nat -> abt xs' b' -> View (syn abt) xs' b' -> m (abt xs' b')
loop Nat
i abt xs b'
f'' (abt xs b' -> View (syn abt) xs b'
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs b'
f'')
renames
:: forall k
(syn :: ([k] -> k -> Type) -> k -> Type)
(abt :: [k] -> k -> Type)
(xs :: [k])
(a :: k)
. ( ABT syn abt
, JmEq1 (Sing :: k -> Type)
, Show1 (Sing :: k -> Type)
, Functor21 syn
)
=> Assocs (Variable :: k -> Type)
-> abt xs a
-> abt xs a
renames :: Assocs Variable -> abt xs a -> abt xs a
renames Assocs Variable
rho0 =
\abt xs a
e0 -> (abt xs a -> Assoc Variable -> abt xs a)
-> abt xs a -> IntMap (Assoc Variable) -> abt xs a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl (\abt xs a
e (Assoc Variable a
x Variable a
v) -> Variable a -> Variable a -> abt xs a -> abt xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
(JmEq1 Sing, Show1 Sing, Functor21 syn, ABT syn abt) =>
Variable a -> Variable a -> abt xs b -> abt xs b
rename Variable a
x Variable a
v abt xs a
e) abt xs a
e0 (Assocs Variable -> IntMap (Assoc Variable)
forall k (ast :: k -> *). Assocs ast -> IntMap (Assoc ast)
unAssocs Assocs Variable
rho0)
substs
:: forall k
(syn :: ([k] -> k -> Type) -> k -> Type)
(abt :: [k] -> k -> Type)
(xs :: [k])
(a :: k)
. ( ABT syn abt
, JmEq1 (Sing :: k -> Type)
, Show1 (Sing :: k -> Type)
, Traversable21 syn
)
=> Assocs (abt '[])
-> abt xs a
-> abt xs a
substs :: Assocs (abt '[]) -> abt xs a -> abt xs a
substs Assocs (abt '[])
rho0 =
\abt xs a
e0 -> (abt xs a -> Assoc (abt '[]) -> abt xs a)
-> abt xs a -> IntMap (Assoc (abt '[])) -> abt xs a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl (\abt xs a
e (Assoc Variable a
x abt '[] a
v) -> Variable a -> abt '[] a -> abt xs a -> abt xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
(JmEq1 Sing, Show1 Sing, Traversable21 syn, ABT syn abt) =>
Variable a -> abt '[] a -> abt xs b -> abt xs b
subst Variable a
x abt '[] a
v abt xs a
e) abt xs a
e0 (Assocs (abt '[]) -> IntMap (Assoc (abt '[]))
forall k (ast :: k -> *). Assocs ast -> IntMap (Assoc ast)
unAssocs Assocs (abt '[])
rho0)
binder
:: (ABT syn abt)
=> Text
-> Sing a
-> (abt '[] a -> abt xs b)
-> abt (a ': xs) b
binder :: Text -> Sing a -> (abt '[] a -> abt xs b) -> abt (a : xs) b
binder Text
hint Sing a
typ abt '[] a -> abt xs b
hoas = Variable a -> abt xs b -> abt (a : xs) b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
x abt xs b
body
where
body :: abt xs b
body = abt '[] a -> abt xs b
hoas (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
x)
x :: Variable a
x = Text -> Nat -> Sing a -> Variable a
forall k (a :: k). Text -> Nat -> Sing a -> Variable a
Variable Text
hint (abt xs b -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextBind abt xs b
body) Sing a
typ
binderM
:: (MonadFix m, ABT syn abt)
=> Text
-> Sing a
-> (abt '[] a -> m (abt xs b))
-> m (abt (a ': xs) b)
binderM :: Text -> Sing a -> (abt '[] a -> m (abt xs b)) -> m (abt (a : xs) b)
binderM Text
hint Sing a
typ abt '[] a -> m (abt xs b)
hoas = do
(Variable a
var', abt xs b
body) <- ((Variable a, abt xs b) -> m (Variable a, abt xs b))
-> m (Variable a, abt xs b)
forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix (((Variable a, abt xs b) -> m (Variable a, abt xs b))
-> m (Variable a, abt xs b))
-> ((Variable a, abt xs b) -> m (Variable a, abt xs b))
-> m (Variable a, abt xs b)
forall a b. (a -> b) -> a -> b
$ \ ~(Variable a
_, abt xs b
b) -> do
let v :: Variable a
v = Text -> Nat -> Sing a -> Variable a
forall k (a :: k). Text -> Nat -> Sing a -> Variable a
Variable Text
hint (abt xs b -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextBind abt xs b
b) Sing a
typ
abt xs b
b' <- abt '[] a -> m (abt xs b)
hoas (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
v)
(Variable a, abt xs b) -> m (Variable a, abt xs b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Variable a
v, abt xs b
b')
abt (a : xs) b -> m (abt (a : xs) b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Variable a -> abt xs b -> abt (a : xs) b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind Variable a
var' abt xs b
body)
class (ABT syn abt) =>
Binders syn abt xs as | abt -> syn, abt xs -> as, abt as -> xs where
binders :: (as -> abt '[] b) -> abt xs b
instance (ABT syn abt) =>
Binders syn abt '[] () where
binders :: (() -> abt '[] b) -> abt '[] b
binders () -> abt '[] b
hoas = () -> abt '[] b
hoas ()
instance (Binders syn abt xs as, SingI x) =>
Binders syn abt (x ': xs) (abt '[] x, as) where
binders :: ((abt '[] x, as) -> abt '[] b) -> abt (x : xs) b
binders (abt '[] x, as) -> abt '[] b
hoas = Text -> Sing x -> (abt '[] x -> abt xs b) -> abt (x : xs) b
forall a (syn :: ([a] -> a -> *) -> a -> *) (abt :: [a] -> a -> *)
(a :: a) (xs :: [a]) (b :: a).
ABT syn abt =>
Text -> Sing a -> (abt '[] a -> abt xs b) -> abt (a : xs) b
binder Text
empty Sing x
forall k (a :: k). SingI a => Sing a
sing ((as -> abt '[] b) -> abt xs b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) as (b :: k).
Binders syn abt xs as =>
(as -> abt '[] b) -> abt xs b
binders ((as -> abt '[] b) -> abt xs b)
-> (abt '[] x -> as -> abt '[] b) -> abt '[] x -> abt xs b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((abt '[] x, as) -> abt '[] b) -> abt '[] x -> as -> abt '[] b
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (abt '[] x, as) -> abt '[] b
hoas)
cataABT
:: forall k
(abt :: [k] -> k -> Type)
(syn :: ([k] -> k -> Type) -> k -> Type)
(r :: [k] -> k -> Type)
. (ABT syn abt, Functor21 syn)
=> (forall a. Variable a -> r '[] a)
-> (forall x xs a. Variable x -> r xs a -> r (x ': xs) a)
-> (forall a. syn r a -> r '[] a)
-> forall xs a. abt xs a -> r xs a
cataABT :: (forall (a :: k). Variable a -> r '[] a)
-> (forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> r xs a -> r (x : xs) a)
-> (forall (a :: k). syn r a -> r '[] a)
-> forall (xs :: [k]) (a :: k). abt xs a -> r xs a
cataABT forall (a :: k). Variable a -> r '[] a
var_ forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> r xs a -> r (x : xs) a
bind_ forall (a :: k). syn r a -> r '[] a
syn_ = abt xs a -> r xs a
forall (xs :: [k]) (a :: k). abt xs a -> r xs a
start
where
start :: forall ys b. abt ys b -> r ys b
start :: abt ys b -> r ys b
start = View (syn abt) ys b -> r ys b
forall (ys :: [k]) (b :: k). View (syn abt) ys b -> r ys b
loop (View (syn abt) ys b -> r ys b)
-> (abt ys b -> View (syn abt) ys b) -> abt ys b -> r ys b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt ys b -> View (syn abt) ys b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
loop :: forall ys b. View (syn abt) ys b -> r ys b
loop :: View (syn abt) ys b -> r ys b
loop (Syn syn abt b
t) = syn r b -> r '[] b
forall (a :: k). syn r a -> r '[] a
syn_ ((forall (xs :: [k]) (a :: k). abt xs a -> r xs a)
-> syn abt b -> syn r b
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 forall (xs :: [k]) (a :: k). abt xs a -> r xs a
start syn abt b
t)
loop (Var Variable b
x) = Variable b -> r '[] b
forall (a :: k). Variable a -> r '[] a
var_ Variable b
x
loop (Bind Variable a
x View (syn abt) xs b
e) = Variable a -> r xs b -> r (a : xs) b
forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> r xs a -> r (x : xs) a
bind_ Variable a
x (View (syn abt) xs b -> r xs b
forall (ys :: [k]) (b :: k). View (syn abt) ys b -> r ys b
loop View (syn abt) xs b
e)
{-# INLINE cataABT #-}
cataABTM
:: forall k
(abt :: [k] -> k -> Type)
(syn :: ([k] -> k -> Type) -> k -> Type)
(r :: [k] -> k -> Type)
(f :: Type -> Type)
. (ABT syn abt, Traversable21 syn, Applicative f)
=> (forall a. Variable a -> f (r '[] a))
-> (forall x xs a. Variable x -> f (r xs a) -> f (r (x ': xs) a))
-> (forall a. f (syn r a) -> f (r '[] a))
-> forall xs a. abt xs a -> f (r xs a)
cataABTM :: (forall (a :: k). Variable a -> f (r '[] a))
-> (forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> f (r xs a) -> f (r (x : xs) a))
-> (forall (a :: k). f (syn r a) -> f (r '[] a))
-> forall (xs :: [k]) (a :: k). abt xs a -> f (r xs a)
cataABTM forall (a :: k). Variable a -> f (r '[] a)
var_ forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> f (r xs a) -> f (r (x : xs) a)
bind_ forall (a :: k). f (syn r a) -> f (r '[] a)
syn_ = abt xs a -> f (r xs a)
forall (xs :: [k]) (a :: k). abt xs a -> f (r xs a)
start
where
start :: forall ys b. abt ys b -> f (r ys b)
start :: abt ys b -> f (r ys b)
start = View (syn abt) ys b -> f (r ys b)
forall (ys :: [k]) (b :: k). View (syn abt) ys b -> f (r ys b)
loop (View (syn abt) ys b -> f (r ys b))
-> (abt ys b -> View (syn abt) ys b) -> abt ys b -> f (r ys b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt ys b -> View (syn abt) ys b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
loop :: forall ys b. View (syn abt) ys b -> f (r ys b)
loop :: View (syn abt) ys b -> f (r ys b)
loop (Syn syn abt b
t) = f (syn r b) -> f (r '[] b)
forall (a :: k). f (syn r a) -> f (r '[] a)
syn_ ((forall (xs :: [k]) (a :: k). abt xs a -> f (r xs a))
-> syn abt b -> f (syn r b)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (xs :: [k]) (a :: k). abt xs a -> f (r xs a)
start syn abt b
t)
loop (Var Variable b
x) = Variable b -> f (r '[] b)
forall (a :: k). Variable a -> f (r '[] a)
var_ Variable b
x
loop (Bind Variable a
x View (syn abt) xs b
e) = Variable a -> f (r xs b) -> f (r (a : xs) b)
forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> f (r xs a) -> f (r (x : xs) a)
bind_ Variable a
x (View (syn abt) xs b -> f (r xs b)
forall (ys :: [k]) (b :: k). View (syn abt) ys b -> f (r ys b)
loop View (syn abt) xs b
e)
{-# INLINE cataABTM #-}
paraABT
:: forall k
(abt :: [k] -> k -> Type)
(syn :: ([k] -> k -> Type) -> k -> Type)
(r :: [k] -> k -> Type)
. (ABT syn abt, Functor21 syn)
=> (forall a. Variable a -> r '[] a)
-> (forall x xs a. Variable x -> abt xs a -> r xs a -> r (x ': xs) a)
-> (forall a. syn (Pair2 abt r) a -> r '[] a)
-> forall xs a. abt xs a -> r xs a
paraABT :: (forall (a :: k). Variable a -> r '[] a)
-> (forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> abt xs a -> r xs a -> r (x : xs) a)
-> (forall (a :: k). syn (Pair2 abt r) a -> r '[] a)
-> forall (xs :: [k]) (a :: k). abt xs a -> r xs a
paraABT forall (a :: k). Variable a -> r '[] a
var_ forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> abt xs a -> r xs a -> r (x : xs) a
bind_ forall (a :: k). syn (Pair2 abt r) a -> r '[] a
syn_ = abt xs a -> r xs a
forall (xs :: [k]) (a :: k). abt xs a -> r xs a
start
where
start :: forall ys b. abt ys b -> r ys b
start :: abt ys b -> r ys b
start = View (syn abt) ys b -> r ys b
forall (ys :: [k]) (b :: k). View (syn abt) ys b -> r ys b
loop (View (syn abt) ys b -> r ys b)
-> (abt ys b -> View (syn abt) ys b) -> abt ys b -> r ys b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt ys b -> View (syn abt) ys b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT
loop :: forall ys b. View (syn abt) ys b -> r ys b
loop :: View (syn abt) ys b -> r ys b
loop (Syn syn abt b
t) = syn (Pair2 abt r) b -> r '[] b
forall (a :: k). syn (Pair2 abt r) a -> r '[] a
syn_ ((forall (h :: [k]) (i :: k). abt h i -> Pair2 abt r h i)
-> syn abt b -> syn (Pair2 abt r) b
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
(a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 (\abt h i
e -> abt h i -> r h i -> Pair2 abt r h i
forall k1 k2 (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (i :: k1)
(j :: k2).
a i j -> b i j -> Pair2 a b i j
Pair2 abt h i
e (abt h i -> r h i
forall (xs :: [k]) (a :: k). abt xs a -> r xs a
start abt h i
e)) syn abt b
t)
loop (Var Variable b
x) = Variable b -> r '[] b
forall (a :: k). Variable a -> r '[] a
var_ Variable b
x
loop (Bind Variable a
x View (syn abt) xs b
e) = Variable a -> abt xs b -> r xs b -> r (a : xs) b
forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> abt xs a -> r xs a -> r (x : xs) a
bind_ Variable a
x (View (syn abt) xs b -> abt xs b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
View (syn abt) xs a -> abt xs a
unviewABT View (syn abt) xs b
e) (View (syn abt) xs b -> r xs b
forall (ys :: [k]) (b :: k). View (syn abt) ys b -> r ys b
loop View (syn abt) xs b
e)
{-# INLINE paraABT #-}
resolveVar
:: (JmEq1 (Sing :: k -> Type), Show1 (Sing :: k -> Type), ABT syn abt)
=> abt '[] (a :: k)
-> Assocs (abt '[])
-> Either (Variable a) (syn abt a)
resolveVar :: abt '[] a -> Assocs (abt '[]) -> Either (Variable a) (syn abt a)
resolveVar abt '[] a
e Assocs (abt '[])
xs =
((Variable a -> Either (Variable a) (syn abt a))
-> (syn abt a -> Either (Variable a) (syn abt a))
-> Either (Variable a) (syn abt a))
-> (syn abt a -> Either (Variable a) (syn abt a))
-> (Variable a -> Either (Variable a) (syn abt a))
-> Either (Variable a) (syn abt a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (abt '[] a
-> (Variable a -> Either (Variable a) (syn abt a))
-> (syn abt a -> Either (Variable a) (syn abt a))
-> Either (Variable a) (syn abt a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] a
e) syn abt a -> Either (Variable a) (syn abt a)
forall a b. b -> Either a b
Right ((Variable a -> Either (Variable a) (syn abt a))
-> Either (Variable a) (syn abt a))
-> (Variable a -> Either (Variable a) (syn abt a))
-> Either (Variable a) (syn abt a)
forall a b. (a -> b) -> a -> b
$ \Variable a
x ->
case Variable a -> Assocs (abt '[]) -> Maybe (abt '[] a)
forall k (a :: k) (ast :: k -> *).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> Assocs ast -> Maybe (ast a)
lookupAssoc Variable a
x Assocs (abt '[])
xs of
Just abt '[] a
e' -> abt '[] a -> Assocs (abt '[]) -> Either (Variable a) (syn abt a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
(JmEq1 Sing, Show1 Sing, ABT syn abt) =>
abt '[] a -> Assocs (abt '[]) -> Either (Variable a) (syn abt a)
resolveVar abt '[] a
e' Assocs (abt '[])
xs
Maybe (abt '[] a)
Nothing -> Variable a -> Either (Variable a) (syn abt a)
forall a b. a -> Either a b
Left Variable a
x
dupABT
:: (ABT syn abt0, ABT syn abt1, Functor21 syn)
=> abt0 xs a
-> abt1 xs a
dupABT :: abt0 xs a -> abt1 xs a
dupABT = (forall (a :: k3). Variable a -> abt1 '[] a)
-> (forall (x :: k3) (xs :: [k3]) (a :: k3).
Variable x -> abt1 xs a -> abt1 (x : xs) a)
-> (forall (a :: k3). syn abt1 a -> abt1 '[] a)
-> forall (xs :: [k3]) (a :: k3). abt0 xs a -> abt1 xs a
forall k (abt :: [k] -> k -> *) (syn :: ([k] -> k -> *) -> k -> *)
(r :: [k] -> k -> *).
(ABT syn abt, Functor21 syn) =>
(forall (a :: k). Variable a -> r '[] a)
-> (forall (x :: k) (xs :: [k]) (a :: k).
Variable x -> r xs a -> r (x : xs) a)
-> (forall (a :: k). syn r a -> r '[] a)
-> forall (xs :: [k]) (a :: k). abt xs a -> r xs a
cataABT forall (a :: k3). Variable a -> abt1 '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var forall (x :: k3) (xs :: [k3]) (a :: k3).
Variable x -> abt1 xs a -> abt1 (x : xs) a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) (xs :: [k]) (b :: k).
ABT syn abt =>
Variable a -> abt xs b -> abt (a : xs) b
bind forall (a :: k3). syn abt1 a -> abt1 '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn