{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Monad.Free.Foil where
import Control.DeepSeq
import qualified Control.Monad.Foil.Internal as Foil
import qualified Control.Monad.Foil.Relative as Foil
import Data.Bifoldable
import Data.Bifunctor
import Data.Bifunctor.Sum
import Data.Coerce (coerce)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid (All (..))
import GHC.Generics (Generic)
data ScopedAST binder sig n where
ScopedAST :: binder n l -> AST binder sig l -> ScopedAST binder sig n
instance (forall x y. NFData (binder x y), forall l. NFData (AST binder sig l)) => NFData (ScopedAST binder sig n) where
rnf :: ScopedAST binder sig n -> ()
rnf (ScopedAST binder n l
binder AST binder sig l
body) = binder n l -> ()
forall a. NFData a => a -> ()
rnf binder n l
binder () -> () -> ()
forall a b. a -> b -> b
`seq` AST binder sig l -> ()
forall a. NFData a => a -> ()
rnf AST binder sig l
body
data AST binder sig n where
Var :: Foil.Name n -> AST binder sig n
Node :: sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
deriving instance Generic (AST binder sig n)
deriving instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))
=> NFData (AST binder sig n)
instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.Sinkable (AST binder sig) where
sinkabilityProof :: forall (n :: S) (l :: S).
(Name n -> Name l) -> AST binder sig n -> AST binder sig l
sinkabilityProof Name n -> Name l
rename = \case
Var Name n
name -> Name l -> AST binder sig l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (Name n -> Name l
rename Name n
name)
Node sig (ScopedAST binder sig n) (AST binder sig n)
node -> sig (ScopedAST binder sig l) (AST binder sig l) -> AST binder sig l
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST binder sig n -> ScopedAST binder sig l)
-> (AST binder sig n -> AST binder sig l)
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> sig (ScopedAST binder sig l) (AST binder sig l)
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST binder sig n -> ScopedAST binder sig l
f ((Name n -> Name l) -> AST binder sig n -> AST binder sig l
forall (n :: S) (l :: S).
(Name n -> Name l) -> AST binder sig n -> AST binder sig l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
Foil.sinkabilityProof Name n -> Name l
rename) sig (ScopedAST binder sig n) (AST binder sig n)
node)
where
f :: ScopedAST binder sig n -> ScopedAST binder sig l
f (ScopedAST binder n l
binder AST binder sig l
body) =
(Name n -> Name l)
-> binder n l
-> (forall (l' :: S).
(Name l -> Name l') -> binder l l' -> ScopedAST binder sig l)
-> ScopedAST binder sig l
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
Foil.extendRenaming Name n -> Name l
rename binder n l
binder ((forall (l' :: S).
(Name l -> Name l') -> binder l l' -> ScopedAST binder sig l)
-> ScopedAST binder sig l)
-> (forall (l' :: S).
(Name l -> Name l') -> binder l l' -> ScopedAST binder sig l)
-> ScopedAST binder sig l
forall a b. (a -> b) -> a -> b
$ \Name l -> Name l'
rename' binder l l'
binder' ->
binder l l' -> AST binder sig l' -> ScopedAST binder sig l
forall (binder :: S -> S -> *) (n :: S) (l :: S)
(sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder l l'
binder' ((Name l -> Name l') -> AST binder sig l -> AST binder sig l'
forall (n :: S) (l :: S).
(Name n -> Name l) -> AST binder sig n -> AST binder sig l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
Foil.sinkabilityProof Name l -> Name l'
rename' AST binder sig l
body)
instance Foil.InjectName (AST binder sig) where
injectName :: forall (n :: S). Name n -> AST binder sig n
injectName = Name n -> AST binder sig n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var
substitute
:: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder)
=> Foil.Scope o
-> Foil.Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute :: forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
(i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute Scope o
scope Substitution (AST binder sig) i o
subst = \case
Var Name i
name -> Substitution (AST binder sig) i o -> Name i -> AST binder sig o
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
Foil.lookupSubst Substitution (AST binder sig) i o
subst Name i
name
Node sig (ScopedAST binder sig i) (AST binder sig i)
node -> sig (ScopedAST binder sig o) (AST binder sig o) -> AST binder sig o
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST binder sig i -> ScopedAST binder sig o)
-> (AST binder sig i -> AST binder sig o)
-> sig (ScopedAST binder sig i) (AST binder sig i)
-> sig (ScopedAST binder sig o) (AST binder sig o)
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST binder sig i -> ScopedAST binder sig o
f (Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
(i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute Scope o
scope Substitution (AST binder sig) i o
subst) sig (ScopedAST binder sig i) (AST binder sig i)
node)
where
f :: ScopedAST binder sig i -> ScopedAST binder sig o
f (ScopedAST binder i l
binder AST binder sig l
body) =
Scope o
-> binder i l
-> (forall (o' :: S).
DExt o o' =>
(Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o')
-> binder o o' -> ScopedAST binder sig o)
-> ScopedAST binder sig o
forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
(l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
DExt o o' =>
(Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
Foil.withRefreshedPattern Scope o
scope binder i l
binder ((forall (o' :: S).
DExt o o' =>
(Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o')
-> binder o o' -> ScopedAST binder sig o)
-> ScopedAST binder sig o)
-> (forall (o' :: S).
DExt o o' =>
(Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o')
-> binder o o' -> ScopedAST binder sig o)
-> ScopedAST binder sig o
forall a b. (a -> b) -> a -> b
$ \Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o'
extendSubst binder o o'
binder' ->
let subst' :: Substitution (AST binder sig) l o'
subst' = Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o'
extendSubst (Substitution (AST binder sig) i o
-> Substitution (AST binder sig) i o
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution (AST binder sig) i o
subst)
scope' :: Scope o'
scope' = binder o o' -> Scope o -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder o o'
binder' Scope o
scope
body' :: AST binder sig o'
body' = Scope o'
-> Substitution (AST binder sig) l o'
-> AST binder sig l
-> AST binder sig o'
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
(i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute Scope o'
scope' Substitution (AST binder sig) l o'
subst' AST binder sig l
body
in binder o o' -> AST binder sig o' -> ScopedAST binder sig o
forall (binder :: S -> S -> *) (n :: S) (l :: S)
(sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder o o'
binder' AST binder sig o'
body'
substituteRefreshed
:: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder)
=> Foil.Scope o
-> Foil.Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substituteRefreshed :: forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
(i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substituteRefreshed Scope o
scope Substitution (AST binder sig) i o
subst = \case
Var Name i
name -> Substitution (AST binder sig) i o -> Name i -> AST binder sig o
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
Foil.lookupSubst Substitution (AST binder sig) i o
subst Name i
name
Node sig (ScopedAST binder sig i) (AST binder sig i)
node -> sig (ScopedAST binder sig o) (AST binder sig o) -> AST binder sig o
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST binder sig i -> ScopedAST binder sig o)
-> (AST binder sig i -> AST binder sig o)
-> sig (ScopedAST binder sig i) (AST binder sig i)
-> sig (ScopedAST binder sig o) (AST binder sig o)
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST binder sig i -> ScopedAST binder sig o
f (Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
(i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substituteRefreshed Scope o
scope Substitution (AST binder sig) i o
subst) sig (ScopedAST binder sig i) (AST binder sig i)
node)
where
f :: ScopedAST binder sig i -> ScopedAST binder sig o
f (ScopedAST binder i l
binder AST binder sig l
body) =
Scope o
-> binder i l
-> (forall (o' :: S).
DExt o o' =>
(Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o')
-> binder o o' -> ScopedAST binder sig o)
-> ScopedAST binder sig o
forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
(l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
DExt o o' =>
(Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
Foil.withFreshPattern Scope o
scope binder i l
binder ((forall (o' :: S).
DExt o o' =>
(Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o')
-> binder o o' -> ScopedAST binder sig o)
-> ScopedAST binder sig o)
-> (forall (o' :: S).
DExt o o' =>
(Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o')
-> binder o o' -> ScopedAST binder sig o)
-> ScopedAST binder sig o
forall a b. (a -> b) -> a -> b
$ \Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o'
extendSubst binder o o'
binder' ->
let subst' :: Substitution (AST binder sig) l o'
subst' = Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o'
extendSubst (Substitution (AST binder sig) i o
-> Substitution (AST binder sig) i o
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution (AST binder sig) i o
subst)
scope' :: Scope o'
scope' = binder o o' -> Scope o -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder o o'
binder' Scope o
scope
body' :: AST binder sig o'
body' = Scope o'
-> Substitution (AST binder sig) l o'
-> AST binder sig l
-> AST binder sig o'
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
(i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substituteRefreshed Scope o'
scope' Substitution (AST binder sig) l o'
subst' AST binder sig l
body
in binder o o' -> AST binder sig o' -> ScopedAST binder sig o
forall (binder :: S -> S -> *) (n :: S) (l :: S)
(sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder o o'
binder' AST binder sig o'
body'
instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.RelMonad Foil.Name (AST binder sig) where
rreturn :: forall (a :: S). Name a -> AST binder sig a
rreturn = Name a -> AST binder sig a
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var
rbind :: forall (b :: S) (a :: S).
Distinct b =>
Scope b
-> AST binder sig a
-> (Name a -> AST binder sig b)
-> AST binder sig b
rbind Scope b
scope AST binder sig a
term Name a -> AST binder sig b
subst =
case AST binder sig a
term of
Var Name a
name -> Name a -> AST binder sig b
subst Name a
name
Node sig (ScopedAST binder sig a) (AST binder sig a)
node -> sig (ScopedAST binder sig b) (AST binder sig b) -> AST binder sig b
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST binder sig a -> ScopedAST binder sig b)
-> (AST binder sig a -> AST binder sig b)
-> sig (ScopedAST binder sig a) (AST binder sig a)
-> sig (ScopedAST binder sig b) (AST binder sig b)
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST binder sig a -> ScopedAST binder sig b
g' AST binder sig a -> AST binder sig b
g sig (ScopedAST binder sig a) (AST binder sig a)
node)
where
g :: AST binder sig a -> AST binder sig b
g AST binder sig a
x = Scope b
-> AST binder sig a
-> (Name a -> AST binder sig b)
-> AST binder sig b
forall (b :: S) (a :: S).
Distinct b =>
Scope b
-> AST binder sig a
-> (Name a -> AST binder sig b)
-> AST binder sig b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
Foil.rbind Scope b
scope AST binder sig a
x Name a -> AST binder sig b
subst
g' :: ScopedAST binder sig a -> ScopedAST binder sig b
g' (ScopedAST binder a l
binder AST binder sig l
body) =
Scope b
-> binder a l
-> (forall (o' :: S).
DExt b o' =>
((Name a -> AST binder sig b) -> Name l -> AST binder sig o')
-> binder b o' -> ScopedAST binder sig b)
-> ScopedAST binder sig b
forall (pattern :: S -> S -> *) (o :: S) (e :: S -> *) (n :: S)
(l :: S) r.
(CoSinkable pattern, Distinct o, InjectName e, Sinkable e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
DExt o o' =>
((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r)
-> r
Foil.withRefreshedPattern' Scope b
scope binder a l
binder ((forall (o' :: S).
DExt b o' =>
((Name a -> AST binder sig b) -> Name l -> AST binder sig o')
-> binder b o' -> ScopedAST binder sig b)
-> ScopedAST binder sig b)
-> (forall (o' :: S).
DExt b o' =>
((Name a -> AST binder sig b) -> Name l -> AST binder sig o')
-> binder b o' -> ScopedAST binder sig b)
-> ScopedAST binder sig b
forall a b. (a -> b) -> a -> b
$ \(Name a -> AST binder sig b) -> Name l -> AST binder sig o'
extendSubst binder b o'
binder' ->
let scope' :: Scope o'
scope' = binder b o' -> Scope b -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder b o'
binder' Scope b
scope
subst' :: Name l -> AST binder sig o'
subst' = (Name a -> AST binder sig b) -> Name l -> AST binder sig o'
extendSubst Name a -> AST binder sig b
subst
in binder b o' -> AST binder sig o' -> ScopedAST binder sig b
forall (binder :: S -> S -> *) (n :: S) (l :: S)
(sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder b o'
binder' (Scope o'
-> AST binder sig l
-> (Name l -> AST binder sig o')
-> AST binder sig o'
forall (b :: S) (a :: S).
Distinct b =>
Scope b
-> AST binder sig a
-> (Name a -> AST binder sig b)
-> AST binder sig b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
Foil.rbind Scope o'
scope' AST binder sig l
body Name l -> AST binder sig o'
subst')
refreshAST
:: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)
=> Foil.Scope n
-> AST binder sig n
-> AST binder sig n
refreshAST :: forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder) =>
Scope n -> AST binder sig n -> AST binder sig n
refreshAST Scope n
scope = \case
t :: AST binder sig n
t@Var{} -> AST binder sig n
t
Node sig (ScopedAST binder sig n) (AST binder sig n)
t -> sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST binder sig n -> ScopedAST binder sig n)
-> (AST binder sig n -> AST binder sig n)
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> sig (ScopedAST binder sig n) (AST binder sig n)
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder) =>
Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n
refreshScopedAST Scope n
scope) (Scope n -> AST binder sig n -> AST binder sig n
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder) =>
Scope n -> AST binder sig n -> AST binder sig n
refreshAST Scope n
scope) sig (ScopedAST binder sig n) (AST binder sig n)
t)
refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)
=> Foil.Scope n
-> ScopedAST binder sig n
-> ScopedAST binder sig n
refreshScopedAST :: forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder) =>
Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n
refreshScopedAST Scope n
scope (ScopedAST binder n l
binder AST binder sig l
body) =
Scope n
-> binder n l
-> (forall {o' :: S}.
DExt n o' =>
(Substitution (AST binder sig) n n
-> Substitution (AST binder sig) l o')
-> binder n o' -> ScopedAST binder sig n)
-> ScopedAST binder sig n
forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
(l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
DExt o o' =>
(Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
Foil.withFreshPattern Scope n
scope binder n l
binder ((forall {o' :: S}.
DExt n o' =>
(Substitution (AST binder sig) n n
-> Substitution (AST binder sig) l o')
-> binder n o' -> ScopedAST binder sig n)
-> ScopedAST binder sig n)
-> (forall {o' :: S}.
DExt n o' =>
(Substitution (AST binder sig) n n
-> Substitution (AST binder sig) l o')
-> binder n o' -> ScopedAST binder sig n)
-> ScopedAST binder sig n
forall a b. (a -> b) -> a -> b
$ \Substitution (AST binder sig) n n
-> Substitution (AST binder sig) l o'
extendSubst binder n o'
binder' ->
let scope' :: Scope o'
scope' = binder n o' -> Scope n -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder n o'
binder' Scope n
scope
subst :: Substitution (AST binder sig) l o'
subst = Substitution (AST binder sig) n n
-> Substitution (AST binder sig) l o'
extendSubst (Substitution (AST binder sig) n n
-> Substitution (AST binder sig) n n
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution (AST binder sig) n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
Foil.identitySubst)
in binder n o' -> AST binder sig o' -> ScopedAST binder sig n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
(sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder n o'
binder' (Scope o'
-> Substitution (AST binder sig) l o'
-> AST binder sig l
-> AST binder sig o'
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
(i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substituteRefreshed Scope o'
scope' Substitution (AST binder sig) l o'
subst AST binder sig l
body)
alphaEquivRefreshed
:: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)
=> Foil.Scope n
-> AST binder sig n
-> AST binder sig n
-> Bool
alphaEquivRefreshed :: forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n,
UnifiablePattern binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquivRefreshed Scope n
scope AST binder sig n
t1 AST binder sig n
t2 = Scope n -> AST binder sig n -> AST binder sig n
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder) =>
Scope n -> AST binder sig n -> AST binder sig n
refreshAST Scope n
scope AST binder sig n
t1 AST binder sig n -> AST binder sig n -> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
(l :: S).
(Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n,
Distinct l) =>
AST binder sig n -> AST binder sig l -> Bool
`unsafeEqAST` Scope n -> AST binder sig n -> AST binder sig n
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder) =>
Scope n -> AST binder sig n -> AST binder sig n
refreshAST Scope n
scope AST binder sig n
t2
alphaEquiv
:: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)
=> Foil.Scope n
-> AST binder sig n
-> AST binder sig n
-> Bool
alphaEquiv :: forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n,
UnifiablePattern binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope n
_scope (Var Name n
x) (Var Name n
y) = Name n
x Name n -> Name n -> Bool
forall a. Eq a => a -> a -> Bool
== Name n -> Name n
forall a b. Coercible a b => a -> b
coerce Name n
y
alphaEquiv Scope n
scope (Node sig (ScopedAST binder sig n) (AST binder sig n)
l) (Node sig (ScopedAST binder sig n) (AST binder sig n)
r) =
case sig (ScopedAST binder sig n) (AST binder sig n)
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> Maybe
(sig
(ScopedAST binder sig n, ScopedAST binder sig n)
(AST binder sig n, AST binder sig n))
forall scope term scope' term'.
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
forall (sig :: * -> * -> *) scope term scope' term'.
ZipMatch sig =>
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
zipMatch sig (ScopedAST binder sig n) (AST binder sig n)
l sig (ScopedAST binder sig n) (AST binder sig n)
r of
Maybe
(sig
(ScopedAST binder sig n, ScopedAST binder sig n)
(AST binder sig n, AST binder sig n))
Nothing -> Bool
False
Just sig
(ScopedAST binder sig n, ScopedAST binder sig n)
(AST binder sig n, AST binder sig n)
tt -> All -> Bool
getAll (((ScopedAST binder sig n, ScopedAST binder sig n) -> All)
-> ((AST binder sig n, AST binder sig n) -> All)
-> sig
(ScopedAST binder sig n, ScopedAST binder sig n)
(AST binder sig n, AST binder sig n)
-> All
forall m a b. Monoid m => (a -> m) -> (b -> m) -> sig a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap (Bool -> All
All (Bool -> All)
-> ((ScopedAST binder sig n, ScopedAST binder sig n) -> Bool)
-> (ScopedAST binder sig n, ScopedAST binder sig n)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ScopedAST binder sig n -> ScopedAST binder sig n -> Bool)
-> (ScopedAST binder sig n, ScopedAST binder sig n) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n,
UnifiablePattern binder) =>
Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool
alphaEquivScoped Scope n
scope)) (Bool -> All
All (Bool -> All)
-> ((AST binder sig n, AST binder sig n) -> Bool)
-> (AST binder sig n, AST binder sig n)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AST binder sig n -> AST binder sig n -> Bool)
-> (AST binder sig n, AST binder sig n) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Scope n -> AST binder sig n -> AST binder sig n -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n,
UnifiablePattern binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope n
scope)) sig
(ScopedAST binder sig n, ScopedAST binder sig n)
(AST binder sig n, AST binder sig n)
tt)
alphaEquiv Scope n
_ AST binder sig n
_ AST binder sig n
_ = Bool
False
alphaEquivScoped
:: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)
=> Foil.Scope n
-> ScopedAST binder sig n
-> ScopedAST binder sig n
-> Bool
alphaEquivScoped :: forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n,
UnifiablePattern binder) =>
Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool
alphaEquivScoped Scope n
scope
(ScopedAST binder n l
binder1 AST binder sig l
body1)
(ScopedAST binder n l
binder2 AST binder sig l
body2) =
case binder n l -> binder n l -> UnifyNameBinders binder n l l
forall (n :: S) (l :: S) (r :: S).
Distinct n =>
binder n l -> binder n r -> UnifyNameBinders binder n l r
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
(UnifiablePattern pattern, Distinct n) =>
pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
Foil.unifyPatterns binder n l
binder1 binder n l
binder2 of
Foil.SameNameBinders{} ->
case binder n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder n l
binder1 of
DistinctEvidence l
Foil.Distinct ->
let scope1 :: Scope l
scope1 = binder n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder n l
binder1 Scope n
scope
in Scope l -> AST binder sig l -> AST binder sig l -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n,
UnifiablePattern binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope l
scope1 AST binder sig l
body1 AST binder sig l
AST binder sig l
body2
Foil.RenameLeftNameBinder NameBinders n l
_ NameBinder n l -> NameBinder n l
rename1to2 ->
case binder n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder n l
binder2 of
DistinctEvidence l
Foil.Distinct ->
let scope2 :: Scope l
scope2 = binder n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder n l
binder2 Scope n
scope
in Scope l -> AST binder sig l -> AST binder sig l -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n,
UnifiablePattern binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope l
scope2 (Scope l
-> (Name l -> Name l) -> AST binder sig l -> AST binder sig l
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
Foil.liftRM Scope l
scope2 ((NameBinder n l -> NameBinder n l) -> Name l -> Name l
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
Foil.fromNameBinderRenaming NameBinder n l -> NameBinder n l
rename1to2) AST binder sig l
body1) AST binder sig l
body2
Foil.RenameRightNameBinder NameBinders n l
_ NameBinder n l -> NameBinder n l
rename2to1 ->
case binder n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder n l
binder1 of
DistinctEvidence l
Foil.Distinct ->
let scope1 :: Scope l
scope1 = binder n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder n l
binder1 Scope n
scope
in Scope l -> AST binder sig l -> AST binder sig l -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n,
UnifiablePattern binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope l
scope1 AST binder sig l
body1 (Scope l
-> (Name l -> Name l) -> AST binder sig l -> AST binder sig l
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
Foil.liftRM Scope l
scope1 ((NameBinder n l -> NameBinder n l) -> Name l -> Name l
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
Foil.fromNameBinderRenaming NameBinder n l -> NameBinder n l
rename2to1) AST binder sig l
body2)
Foil.RenameBothBinders NameBinders n lr
binder' NameBinder n l -> NameBinder n lr
rename1 NameBinder n l -> NameBinder n lr
rename2 ->
case NameBinders n lr -> DistinctEvidence lr
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct NameBinders n lr
binder' of
DistinctEvidence lr
Foil.Distinct ->
let scope' :: Scope lr
scope' = NameBinders n lr -> Scope n -> Scope lr
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern NameBinders n lr
binder' Scope n
scope
in Scope lr -> AST binder sig lr -> AST binder sig lr -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n,
UnifiablePattern binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope lr
scope'
(Scope lr
-> (Name l -> Name lr) -> AST binder sig l -> AST binder sig lr
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
Foil.liftRM Scope lr
scope' ((NameBinder n l -> NameBinder n lr) -> Name l -> Name lr
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
Foil.fromNameBinderRenaming NameBinder n l -> NameBinder n lr
rename1) AST binder sig l
body1)
(Scope lr
-> (Name l -> Name lr) -> AST binder sig l -> AST binder sig lr
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
Foil.liftRM Scope lr
scope' ((NameBinder n l -> NameBinder n lr) -> Name l -> Name lr
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
Foil.fromNameBinderRenaming NameBinder n l -> NameBinder n lr
rename2) AST binder sig l
body2)
UnifyNameBinders binder n l l
Foil.NotUnifiable -> Bool
False
unsafeEqAST
:: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
=> AST binder sig n
-> AST binder sig l
-> Bool
unsafeEqAST :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
(l :: S).
(Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n,
Distinct l) =>
AST binder sig n -> AST binder sig l -> Bool
unsafeEqAST (Var Name n
x) (Var Name l
y) = Name n
x Name n -> Name n -> Bool
forall a. Eq a => a -> a -> Bool
== Name l -> Name n
forall a b. Coercible a b => a -> b
coerce Name l
y
unsafeEqAST (Node sig (ScopedAST binder sig n) (AST binder sig n)
t1) (Node sig (ScopedAST binder sig l) (AST binder sig l)
t2) =
case sig (ScopedAST binder sig n) (AST binder sig n)
-> sig (ScopedAST binder sig l) (AST binder sig l)
-> Maybe
(sig
(ScopedAST binder sig n, ScopedAST binder sig l)
(AST binder sig n, AST binder sig l))
forall scope term scope' term'.
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
forall (sig :: * -> * -> *) scope term scope' term'.
ZipMatch sig =>
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
zipMatch sig (ScopedAST binder sig n) (AST binder sig n)
t1 sig (ScopedAST binder sig l) (AST binder sig l)
t2 of
Maybe
(sig
(ScopedAST binder sig n, ScopedAST binder sig l)
(AST binder sig n, AST binder sig l))
Nothing -> Bool
False
Just sig
(ScopedAST binder sig n, ScopedAST binder sig l)
(AST binder sig n, AST binder sig l)
tt -> All -> Bool
getAll (((ScopedAST binder sig n, ScopedAST binder sig l) -> All)
-> ((AST binder sig n, AST binder sig l) -> All)
-> sig
(ScopedAST binder sig n, ScopedAST binder sig l)
(AST binder sig n, AST binder sig l)
-> All
forall m a b. Monoid m => (a -> m) -> (b -> m) -> sig a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap (Bool -> All
All (Bool -> All)
-> ((ScopedAST binder sig n, ScopedAST binder sig l) -> Bool)
-> (ScopedAST binder sig n, ScopedAST binder sig l)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ScopedAST binder sig n -> ScopedAST binder sig l -> Bool)
-> (ScopedAST binder sig n, ScopedAST binder sig l) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ScopedAST binder sig n -> ScopedAST binder sig l -> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
(l :: S).
(Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n,
Distinct l) =>
ScopedAST binder sig n -> ScopedAST binder sig l -> Bool
unsafeEqScopedAST) (Bool -> All
All (Bool -> All)
-> ((AST binder sig n, AST binder sig l) -> Bool)
-> (AST binder sig n, AST binder sig l)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AST binder sig n -> AST binder sig l -> Bool)
-> (AST binder sig n, AST binder sig l) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry AST binder sig n -> AST binder sig l -> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
(l :: S).
(Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n,
Distinct l) =>
AST binder sig n -> AST binder sig l -> Bool
unsafeEqAST) sig
(ScopedAST binder sig n, ScopedAST binder sig l)
(AST binder sig n, AST binder sig l)
tt)
unsafeEqAST AST binder sig n
_ AST binder sig l
_ = Bool
False
unsafeEqScopedAST
:: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
=> ScopedAST binder sig n
-> ScopedAST binder sig l
-> Bool
unsafeEqScopedAST :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
(l :: S).
(Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n,
Distinct l) =>
ScopedAST binder sig n -> ScopedAST binder sig l -> Bool
unsafeEqScopedAST (ScopedAST binder n l
binder1 AST binder sig l
body1) (ScopedAST binder l l
binder2 AST binder sig l
body2) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
[ binder n l -> binder l l -> Bool
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (n' :: S)
(l' :: S).
(UnifiablePattern pattern, Distinct n) =>
pattern n l -> pattern n' l' -> Bool
Foil.unsafeEqPattern binder n l
binder1 binder l l
binder2
, case (binder n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder n l
binder1, binder l l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder l l
binder2) of
(DistinctEvidence l
Foil.Distinct, DistinctEvidence l
Foil.Distinct) -> AST binder sig l
body1 AST binder sig l -> AST binder sig l -> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
(l :: S).
(Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n,
Distinct l) =>
AST binder sig n -> AST binder sig l -> Bool
`unsafeEqAST` AST binder sig l
body2
]
class ZipMatch sig where
zipMatch
:: sig scope term
-> sig scope' term'
-> Maybe (sig (scope, scope') (term, term'))
instance (ZipMatch f, ZipMatch g) => ZipMatch (Sum f g) where
zipMatch :: forall scope term scope' term'.
Sum f g scope term
-> Sum f g scope' term'
-> Maybe (Sum f g (scope, scope') (term, term'))
zipMatch (L2 f scope term
f) (L2 f scope' term'
f') = f (scope, scope') (term, term')
-> Sum f g (scope, scope') (term, term')
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
(b :: k1).
p a b -> Sum p q a b
L2 (f (scope, scope') (term, term')
-> Sum f g (scope, scope') (term, term'))
-> Maybe (f (scope, scope') (term, term'))
-> Maybe (Sum f g (scope, scope') (term, term'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f scope term
-> f scope' term' -> Maybe (f (scope, scope') (term, term'))
forall scope term scope' term'.
f scope term
-> f scope' term' -> Maybe (f (scope, scope') (term, term'))
forall (sig :: * -> * -> *) scope term scope' term'.
ZipMatch sig =>
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
zipMatch f scope term
f f scope' term'
f'
zipMatch (R2 g scope term
g) (R2 g scope' term'
g') = g (scope, scope') (term, term')
-> Sum f g (scope, scope') (term, term')
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
(b :: k1).
q a b -> Sum p q a b
R2 (g (scope, scope') (term, term')
-> Sum f g (scope, scope') (term, term'))
-> Maybe (g (scope, scope') (term, term'))
-> Maybe (Sum f g (scope, scope') (term, term'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g scope term
-> g scope' term' -> Maybe (g (scope, scope') (term, term'))
forall scope term scope' term'.
g scope term
-> g scope' term' -> Maybe (g (scope, scope') (term, term'))
forall (sig :: * -> * -> *) scope term scope' term'.
ZipMatch sig =>
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
zipMatch g scope term
g g scope' term'
g'
zipMatch Sum f g scope term
_ Sum f g scope' term'
_ = Maybe (Sum f g (scope, scope') (term, term'))
forall a. Maybe a
Nothing
convertToAST
:: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)
=> (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall x z. Foil.Distinct x
=> Foil.Scope x
-> Map rawIdent (Foil.Name x)
-> rawPattern
-> (forall y. Foil.DExt x y
=> binder x y
-> Map rawIdent (Foil.Name y)
-> z)
-> z)
-> (rawScopedTerm -> rawTerm)
-> Foil.Scope n
-> Map rawIdent (Foil.Name n)
-> rawTerm
-> AST binder sig n
convertToAST :: forall (n :: S) (sig :: * -> * -> *) rawIdent
(binder :: S -> S -> *) rawTerm rawPattern rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) =>
(rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST binder sig n
convertToAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern rawScopedTerm -> rawTerm
getScopedTerm Scope n
scope Map rawIdent (Name n)
names rawTerm
t =
case rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig rawTerm
t of
Left rawIdent
x ->
case rawIdent -> Map rawIdent (Name n) -> Maybe (Name n)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup rawIdent
x Map rawIdent (Name n)
names of
Maybe (Name n)
Nothing -> [Char] -> AST binder sig n
forall a. HasCallStack => [Char] -> a
error [Char]
"undefined variable"
Just Name n
name -> Name n -> AST binder sig n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
name
Right sig (rawPattern, rawScopedTerm) rawTerm
node -> sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node (sig (ScopedAST binder sig n) (AST binder sig n)
-> AST binder sig n)
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> AST binder sig n
forall a b. (a -> b) -> a -> b
$
((rawPattern, rawScopedTerm) -> ScopedAST binder sig n)
-> (rawTerm -> AST binder sig n)
-> sig (rawPattern, rawScopedTerm) rawTerm
-> sig (ScopedAST binder sig n) (AST binder sig n)
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap
((rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> (rawPattern, rawScopedTerm)
-> ScopedAST binder sig n
forall (n :: S) (sig :: * -> * -> *) rawIdent
(binder :: S -> S -> *) rawTerm rawPattern rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) =>
(rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> (rawPattern, rawScopedTerm)
-> ScopedAST binder sig n
convertToScopedAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z
forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern rawScopedTerm -> rawTerm
getScopedTerm Scope n
scope Map rawIdent (Name n)
names)
((rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST binder sig n
forall (n :: S) (sig :: * -> * -> *) rawIdent
(binder :: S -> S -> *) rawTerm rawPattern rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) =>
(rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST binder sig n
convertToAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z
forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern rawScopedTerm -> rawTerm
getScopedTerm Scope n
scope Map rawIdent (Name n)
names)
sig (rawPattern, rawScopedTerm) rawTerm
node
convertToScopedAST
:: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)
=> (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall x z. Foil.Distinct x
=> Foil.Scope x
-> Map rawIdent (Foil.Name x)
-> rawPattern
-> (forall y. Foil.DExt x y
=> binder x y
-> Map rawIdent (Foil.Name y)
-> z)
-> z)
-> (rawScopedTerm -> rawTerm)
-> Foil.Scope n
-> Map rawIdent (Foil.Name n)
-> (rawPattern, rawScopedTerm)
-> ScopedAST binder sig n
convertToScopedAST :: forall (n :: S) (sig :: * -> * -> *) rawIdent
(binder :: S -> S -> *) rawTerm rawPattern rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) =>
(rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> (rawPattern, rawScopedTerm)
-> ScopedAST binder sig n
convertToScopedAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern rawScopedTerm -> rawTerm
getScopedTerm Scope n
scope Map rawIdent (Name n)
names (rawPattern
pat, rawScopedTerm
scopedTerm) =
Scope n
-> Map rawIdent (Name n)
-> rawPattern
-> (forall {y :: S}.
DExt n y =>
binder n y -> Map rawIdent (Name y) -> ScopedAST binder sig n)
-> ScopedAST binder sig n
forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern Scope n
scope Map rawIdent (Name n)
names rawPattern
pat ((forall {y :: S}.
DExt n y =>
binder n y -> Map rawIdent (Name y) -> ScopedAST binder sig n)
-> ScopedAST binder sig n)
-> (forall {y :: S}.
DExt n y =>
binder n y -> Map rawIdent (Name y) -> ScopedAST binder sig n)
-> ScopedAST binder sig n
forall a b. (a -> b) -> a -> b
$ \binder n y
binder' Map rawIdent (Name y)
names' ->
let scope' :: Scope y
scope' = binder n y -> Scope n -> Scope y
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder n y
binder' Scope n
scope
in binder n y -> AST binder sig y -> ScopedAST binder sig n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
(sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder n y
binder' ((rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z)
-> (rawScopedTerm -> rawTerm)
-> Scope y
-> Map rawIdent (Name y)
-> rawTerm
-> AST binder sig y
forall (n :: S) (sig :: * -> * -> *) rawIdent
(binder :: S -> S -> *) rawTerm rawPattern rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) =>
(rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST binder sig n
convertToAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z
forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
DExt x y =>
binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern rawScopedTerm -> rawTerm
getScopedTerm Scope y
scope' Map rawIdent (Name y)
names' (rawScopedTerm -> rawTerm
getScopedTerm rawScopedTerm
scopedTerm))
convertFromAST
:: Bifunctor sig
=> (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall x y. (Int -> rawIdent) -> binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST binder sig n
-> rawTerm
convertFromAST :: forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
rawIdent (binder :: S -> S -> *) (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST binder sig n
-> rawTerm
convertFromAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f = \case
Var Name n
x -> rawIdent -> rawTerm
fromVar (Int -> rawIdent
f (Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name n
x))
Node sig (ScopedAST binder sig n) (AST binder sig n)
node -> sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
forall a b. (a -> b) -> a -> b
$
(ScopedAST binder sig n -> (rawPattern, rawScopedTerm))
-> (AST binder sig n -> rawTerm)
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> sig (rawPattern, rawScopedTerm) rawTerm
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap
((sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> ScopedAST binder sig n
-> (rawPattern, rawScopedTerm)
forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
rawIdent (binder :: S -> S -> *) (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> ScopedAST binder sig n
-> (rawPattern, rawScopedTerm)
convertFromScopedAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar (Int -> rawIdent) -> binder x y -> rawPattern
forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f)
((sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST binder sig n
-> rawTerm
forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
rawIdent (binder :: S -> S -> *) (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST binder sig n
-> rawTerm
convertFromAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar (Int -> rawIdent) -> binder x y -> rawPattern
forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f)
sig (ScopedAST binder sig n) (AST binder sig n)
node
convertFromScopedAST
:: Bifunctor sig
=> (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall x y. (Int -> rawIdent) -> binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> ScopedAST binder sig n
-> (rawPattern, rawScopedTerm)
convertFromScopedAST :: forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
rawIdent (binder :: S -> S -> *) (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> ScopedAST binder sig n
-> (rawPattern, rawScopedTerm)
convertFromScopedAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f = \case
ScopedAST binder n l
binder AST binder sig l
body ->
( (Int -> rawIdent) -> binder n l -> rawPattern
forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern
makePattern Int -> rawIdent
f binder n l
binder
, rawTerm -> rawScopedTerm
makeScoped ((sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST binder sig l
-> rawTerm
forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
rawIdent (binder :: S -> S -> *) (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST binder sig n
-> rawTerm
convertFromAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar (Int -> rawIdent) -> binder x y -> rawPattern
forall (x :: S) (y :: S).
(Int -> rawIdent) -> binder x y -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f AST binder sig l
body))