{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}

#ifndef MIN_VERSION_GLASGOW_HASKELL
#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0
#endif
  -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10

#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0)
#else
{-# LANGUAGE OverlappingInstances #-}
#endif

-- | \"Syntactic sugar\"
--
-- For details, see "Combining Deep and Shallow Embedding for EDSL"
-- (TFP 2013, <https://emilaxelsson.github.io/documents/svenningsson2013combining.pdf>).

module Language.Syntactic.Sugar where



import Data.Typeable

import Language.Syntactic.Syntax



-- | It is usually assumed that @(`desugar` (`sugar` a))@ has the same meaning
-- as @a@.
class Syntactic a
  where
    type Domain a :: * -> *
    type Internal a
    desugar :: a -> ASTF (Domain a) (Internal a)
    sugar   :: ASTF (Domain a) (Internal a) -> a

instance Syntactic (ASTF sym a)
  where
    type Domain (ASTF sym a)   = sym
    type Internal (ASTF sym a) = a
    desugar :: ASTF sym a -> ASTF (Domain (ASTF sym a)) (Internal (ASTF sym a))
desugar = ASTF sym a -> ASTF (Domain (ASTF sym a)) (Internal (ASTF sym a))
forall a. a -> a
id
    sugar :: ASTF (Domain (ASTF sym a)) (Internal (ASTF sym a)) -> ASTF sym a
sugar   = ASTF (Domain (ASTF sym a)) (Internal (ASTF sym a)) -> ASTF sym a
forall a. a -> a
id

instance Syntactic (ASTFull sym a)
  where
    type Domain (ASTFull sym a)   = sym
    type Internal (ASTFull sym a) = a
    desugar :: ASTFull sym a
-> ASTF (Domain (ASTFull sym a)) (Internal (ASTFull sym a))
desugar = ASTFull sym a
-> ASTF (Domain (ASTFull sym a)) (Internal (ASTFull sym a))
forall (sym :: * -> *) a. ASTFull sym a -> ASTF sym a
unASTFull
    sugar :: ASTF (Domain (ASTFull sym a)) (Internal (ASTFull sym a))
-> ASTFull sym a
sugar   = ASTF (Domain (ASTFull sym a)) (Internal (ASTFull sym a))
-> ASTFull sym a
forall (sym :: * -> *) a. ASTF sym a -> ASTFull sym a
ASTFull

-- | Syntactic type casting
resugar :: (Syntactic a, Syntactic b, Domain a ~ Domain b, Internal a ~ Internal b) => a -> b
resugar :: a -> b
resugar = AST (Domain b) (Full (Internal b)) -> b
forall a. Syntactic a => ASTF (Domain a) (Internal a) -> a
sugar (AST (Domain b) (Full (Internal b)) -> b)
-> (a -> AST (Domain b) (Full (Internal b))) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> AST (Domain b) (Full (Internal b))
forall a. Syntactic a => a -> ASTF (Domain a) (Internal a)
desugar

-- | N-ary syntactic functions
--
-- 'desugarN' has any type of the form:
--
-- > desugarN ::
-- >     ( Syntactic a
-- >     , Syntactic b
-- >     , ...
-- >     , Syntactic x
-- >     , Domain a ~ sym
-- >     , Domain b ~ sym
-- >     , ...
-- >     , Domain x ~ sym
-- >     ) => (a -> b -> ... -> x)
-- >       -> (  ASTF sym (Internal a)
-- >          -> ASTF sym (Internal b)
-- >          -> ...
-- >          -> ASTF sym (Internal x)
-- >          )
--
-- ...and vice versa for 'sugarN'.
class SyntacticN f internal | f -> internal
  where
    desugarN :: f -> internal
    sugarN   :: internal -> f

instance {-# OVERLAPS #-}
         (Syntactic f, Domain f ~ sym, fi ~ AST sym (Full (Internal f))) => SyntacticN f fi
  where
    desugarN :: f -> fi
desugarN = f -> fi
forall a. Syntactic a => a -> ASTF (Domain a) (Internal a)
desugar
    sugarN :: fi -> f
sugarN   = fi -> f
forall a. Syntactic a => ASTF (Domain a) (Internal a) -> a
sugar

instance {-# OVERLAPS #-}
    ( Syntactic a
    , Domain a ~ sym
    , ia ~ Internal a
    , SyntacticN f fi
    ) =>
      SyntacticN (a -> f) (AST sym (Full ia) -> fi)
  where
    desugarN :: (a -> f) -> AST sym (Full ia) -> fi
desugarN a -> f
f = f -> fi
forall f internal. SyntacticN f internal => f -> internal
desugarN (f -> fi) -> (AST sym (Full ia) -> f) -> AST sym (Full ia) -> fi
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f
f (a -> f) -> (AST sym (Full ia) -> a) -> AST sym (Full ia) -> f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST sym (Full ia) -> a
forall a. Syntactic a => ASTF (Domain a) (Internal a) -> a
sugar
    sugarN :: (AST sym (Full ia) -> fi) -> a -> f
sugarN AST sym (Full ia) -> fi
f   = fi -> f
forall f internal. SyntacticN f internal => internal -> f
sugarN (fi -> f) -> (a -> fi) -> a -> f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST sym (Full ia) -> fi
f (AST sym (Full ia) -> fi) -> (a -> AST sym (Full ia)) -> a -> fi
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> AST sym (Full ia)
forall a. Syntactic a => a -> ASTF (Domain a) (Internal a)
desugar

-- | \"Sugared\" symbol application
--
-- 'sugarSym' has any type of the form:
--
-- > sugarSym ::
-- >     ( sub :<: AST sup
-- >     , Syntactic a
-- >     , Syntactic b
-- >     , ...
-- >     , Syntactic x
-- >     , Domain a ~ Domain b ~ ... ~ Domain x
-- >     ) => sub (Internal a :-> Internal b :-> ... :-> Full (Internal x))
-- >       -> (a -> b -> ... -> x)
sugarSym
    :: ( Signature sig
       , fi  ~ SmartFun sup sig
       , sig ~ SmartSig fi
       , sup ~ SmartSym fi
       , SyntacticN f fi
       , sub :<: sup
       )
    => sub sig -> f
sugarSym :: sub sig -> f
sugarSym = fi -> f
forall f internal. SyntacticN f internal => internal -> f
sugarN (fi -> f) -> (sub sig -> fi) -> sub sig -> f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sub sig -> fi
forall sig f (sup :: * -> *) (sub :: * -> *).
(Signature sig, f ~ SmartFun sup sig, sig ~ SmartSig f,
 sup ~ SmartSym f, sub :<: sup) =>
sub sig -> f
smartSym

-- | \"Sugared\" symbol application
--
-- 'sugarSymTyped' has any type of the form:
--
-- > sugarSymTyped ::
-- >     ( sub :<: AST (Typed sup)
-- >     , Syntactic a
-- >     , Syntactic b
-- >     , ...
-- >     , Syntactic x
-- >     , Domain a ~ Domain b ~ ... ~ Domain x
-- >     , Typeable (Internal x)
-- >     ) => sub (Internal a :-> Internal b :-> ... :-> Full (Internal x))
-- >       -> (a -> b -> ... -> x)
sugarSymTyped
    :: ( Signature sig
       , fi        ~ SmartFun (Typed sup) sig
       , sig       ~ SmartSig fi
       , Typed sup ~ SmartSym fi
       , SyntacticN f fi
       , sub :<: sup
       , Typeable (DenResult sig)
       )
    => sub sig -> f
sugarSymTyped :: sub sig -> f
sugarSymTyped = fi -> f
forall f internal. SyntacticN f internal => internal -> f
sugarN (fi -> f) -> (sub sig -> fi) -> sub sig -> f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. sub sig -> fi
forall sig f (sup :: * -> *) (sub :: * -> *).
(Signature sig, f ~ SmartFun (Typed sup) sig, sig ~ SmartSig f,
 Typed sup ~ SmartSym f, sub :<: sup, Typeable (DenResult sig)) =>
sub sig -> f
smartSymTyped