{-# LANGUAGE UndecidableInstances #-}

-- | 'Syntactic' instance for functions for domains based on 'Binding'

module Language.Syntactic.Sugar.Binding where



import Language.Syntactic
import Language.Syntactic.Functional



instance
    ( Syntactic a, Domain a ~ dom
    , Syntactic b, Domain b ~ dom
    , Binding :<: dom
    ) =>
      Syntactic (a -> b)
  where
    type Domain (a -> b)   = Domain a
    type Internal (a -> b) = Internal a -> Internal b
    desugar :: (a -> b) -> ASTF (Domain (a -> b)) (Internal (a -> b))
desugar a -> b
f = (ASTF dom (Internal a) -> ASTF dom (Internal b))
-> ASTF dom (Internal a -> Internal b)
forall (sym :: * -> *) a b.
(Binding :<: sym) =>
(ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lam (b -> ASTF dom (Internal b)
forall a. Syntactic a => a -> ASTF (Domain a) (Internal a)
desugar (b -> ASTF dom (Internal b))
-> (ASTF dom (Internal a) -> b)
-> ASTF dom (Internal a)
-> ASTF dom (Internal b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f (a -> b)
-> (ASTF dom (Internal a) -> a) -> ASTF dom (Internal a) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASTF dom (Internal a) -> a
forall a. Syntactic a => ASTF (Domain a) (Internal a) -> a
sugar)
    sugar :: ASTF (Domain (a -> b)) (Internal (a -> b)) -> a -> b
sugar     = [Char] -> ASTF dom (Internal a -> Internal b) -> a -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"sugar not implemented for (a -> b)"