module Language.Syntactic.Constraint where
import Data.Constraint
import Language.Syntactic.Syntax
import Language.Syntactic.Interpretation.Equality
import Language.Syntactic.Interpretation.Render
import Language.Syntactic.Interpretation.Evaluation
class (c1 a, c2 a) => (c1 :/\: c2) a
instance (c1 a, c2 a) => (c1 :/\: c2) a
infixr 5 :/\:
class Top a
instance Top a
type Sub sub sup = forall a . Dict (sub a) -> Dict (sup a)
weakL :: Sub (c1 :/\: c2) c1
weakL Dict = Dict
weakR :: Sub (c1 :/\: c2) c2
weakR Dict = Dict
class sub :< sup
where
sub :: Sub sub sup
instance p :< p
where
sub = id
instance (p :/\: ps) :< p
where
sub = weakL
instance (ps :< q) => ((p :/\: ps) :< q)
where
sub = sub . weakR
data (expr :| pred) sig
where
C :: pred (DenResult sig) => expr sig -> (expr :| pred) sig
infixl 4 :|
instance Project sub sup => Project sub (sup :| pred)
where
prj (C s) = prj s
instance Equality dom => Equality (dom :| pred)
where
equal (C a) (C b) = equal a b
exprHash (C a) = exprHash a
instance Render dom => Render (dom :| pred)
where
renderArgs args (C a) = renderArgs args a
instance Eval dom => Eval (dom :| pred)
where
evaluate (C a) = evaluate a
instance ToTree dom => ToTree (dom :| pred)
where
toTreeArgs args (C a) = toTreeArgs args a
data (expr :|| pred) sig
where
C' :: pred (DenResult sig) => expr sig -> (expr :|| pred) sig
infixl 4 :||
instance Project sub sup => Project sub (sup :|| pred)
where
prj (C' s) = prj s
instance Equality dom => Equality (dom :|| pred)
where
equal (C' a) (C' b) = equal a b
exprHash (C' a) = exprHash a
instance Render dom => Render (dom :|| pred)
where
renderArgs args (C' a) = renderArgs args a
instance Eval dom => Eval (dom :|| pred)
where
evaluate (C' a) = evaluate a
instance ToTree dom => ToTree (dom :|| pred)
where
toTreeArgs args (C' a) = toTreeArgs args a
class Constrained expr
where
type Sat (expr :: * -> *) :: * -> Constraint
exprDict :: expr a -> Dict (Sat expr (DenResult a))
instance Constrained dom => Constrained (AST dom)
where
type Sat (AST dom) = Sat dom
exprDict (Sym s) = exprDict s
exprDict (s :$ _) = exprDict s
instance Constrained (sub1 :+: sub2)
where
type Sat (sub1 :+: sub2) = Top
exprDict (InjL s) = Dict
exprDict (InjR s) = Dict
instance Constrained dom => Constrained (dom :| pred)
where
type Sat (dom :| pred) = pred :/\: Sat dom
exprDict (C s) = case exprDict s of Dict -> Dict
instance Constrained (dom :|| pred)
where
type Sat (dom :|| pred) = pred
exprDict (C' s) = Dict
type ConstrainedBy expr c = (Constrained expr, Sat expr :< c)
exprDictSub :: ConstrainedBy expr p => expr a -> Dict (p (DenResult a))
exprDictSub = sub . exprDict
exprDictPlus :: (Constrained dom1, Constrained dom2, Sat dom1 ~ Sat dom2) =>
AST (dom1 :+: dom2) a -> Dict (Sat dom1 (DenResult a))
exprDictPlus (s :$ _) = exprDictPlus s
exprDictPlus (Sym (InjL a)) = exprDict a
exprDictPlus (Sym (InjR a)) = exprDict a
class (Project sub sup, Sat sup a) => InjectC sub sup a
where
injC :: (DenResult sig ~ a) => sub sig -> sup sig
instance InjectC sub sup sig => InjectC sub (AST sup) sig
where
injC = Sym . injC
instance (InjectC sub sup sig, pred sig) => InjectC sub (sup :| pred) sig
where
injC = C . injC
instance (InjectC sub sup sig, pred sig) => InjectC sub (sup :|| pred) sig
where
injC = C' . injC
instance Sat expr sig => InjectC expr expr sig
where
injC = id
instance InjectC expr1 (expr1 :+: expr2) sig
where
injC = InjL
instance InjectC expr1 expr3 sig => InjectC expr1 (expr2 :+: expr3) sig
where
injC = InjR . injC
appSymC :: (ApplySym sig f dom, InjectC sym (AST dom) (DenResult sig)) =>
sym sig -> f
appSymC = appSym' . injC
data ASTE dom
where
ASTE :: ASTF dom a -> ASTE dom
liftASTE
:: (forall a . ASTF dom a -> b)
-> ASTE dom
-> b
liftASTE f (ASTE a) = f a
liftASTE2
:: (forall a b . ASTF dom a -> ASTF dom b -> c)
-> ASTE dom -> ASTE dom -> c
liftASTE2 f (ASTE a) (ASTE b) = f a b
data ASTB dom
where
ASTB :: Sat dom a => ASTF dom a -> ASTB dom
liftASTB
:: (forall a . Sat dom a => ASTF dom a -> b)
-> ASTB dom
-> b
liftASTB f (ASTB a) = f a
liftASTB2
:: (forall a b . (Sat dom a, Sat dom b) => ASTF dom a -> ASTF dom b -> c)
-> ASTB dom -> ASTB dom -> c
liftASTB2 f (ASTB a) (ASTB b) = f a b