{-# OPTIONS_GHC -Wno-orphans -Wno-redundant-constraints #-}
{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE ScopedTypeVariables         #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE KindSignatures    #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE PatternSynonyms   #-}
{-# LANGUAGE RankNTypes        #-}
{-# LANGUAGE TemplateHaskell   #-}
module Language.SOAS.Impl.Generated where

import Data.Bifunctor.TH
import qualified Data.Map as Map
import Data.String (IsString(..))
import qualified Control.Monad.Foil as Foil
import           Control.Monad.Free.Foil.TH.MkFreeFoil
import qualified Language.SOAS.Syntax.Abs    as Raw
import qualified Language.SOAS.Syntax.Lex    as Raw
import qualified Language.SOAS.Syntax.Par    as Raw
import qualified Language.SOAS.Syntax.Print  as Raw
import Data.ZipMatchK
import Generics.Kind.TH (deriveGenericK)
import Language.SOAS.FreeFoilConfig (soasConfig)

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> :set -XDataKinds
-- >>> import qualified Control.Monad.Foil as Foil
-- >>> import qualified Language.SOAS.Syntax.Abs as Raw
-- >>> import Control.Monad.Free.Foil
-- >>> import Data.String (fromString)

-- * Generated code

mkFreeFoil soasConfig

deriveGenericK ''OpArg'Sig
deriveGenericK ''Term'Sig
deriveGenericK ''OpArgTyping'Sig
deriveGenericK ''Type'Sig
deriveGenericK ''Subst'
deriveGenericK ''Constraint'
deriveGenericK ''OpTyping'
deriveGenericK ''Binders'
deriveGenericK ''TypeBinders'

deriveBifunctor ''OpArg'Sig
deriveBifunctor ''Term'Sig
deriveBifunctor ''OpArgTyping'Sig
deriveBifunctor ''ScopedOpArgTyping'Sig
deriveBifunctor ''Type'Sig

deriveBifoldable ''OpArg'Sig
deriveBifoldable ''Term'Sig
deriveBifoldable ''OpArgTyping'Sig
deriveBifoldable ''ScopedOpArgTyping'Sig
deriveBifoldable ''Type'Sig

deriveBitraversable ''OpArg'Sig
deriveBitraversable ''Term'Sig
deriveBitraversable ''OpArgTyping'Sig
deriveBitraversable ''ScopedOpArgTyping'Sig
deriveBitraversable ''Type'Sig

instance Foil.Sinkable (Subst' a)
instance Foil.Sinkable (Constraint' a)
instance Foil.Sinkable (OpTyping' a)

instance Foil.SinkableK (Binders' a)
instance Foil.SinkableK (TypeBinders' a)

instance Foil.HasNameBinders (Binders' a)
instance Foil.CoSinkable (Binders' a)

instance Foil.HasNameBinders (TypeBinders' a)
instance Foil.CoSinkable (TypeBinders' a)

mkFreeFoilConversions soasConfig

-- | Ignore 'Raw.BNFC'Position' when matching terms.
instance ZipMatchK Raw.BNFC'Position where zipMatchWithK :: forall (as :: LoT (*)) (bs :: LoT (*)) (cs :: LoT (*)).
Mappings as bs cs
-> (BNFC'Position :@@: as)
-> (BNFC'Position :@@: bs)
-> Maybe (BNFC'Position :@@: cs)
zipMatchWithK = Mappings as bs cs
-> BNFC'Position -> BNFC'Position -> Maybe BNFC'Position
Mappings as bs cs
-> (BNFC'Position :@@: as)
-> (BNFC'Position :@@: bs)
-> Maybe (BNFC'Position :@@: cs)
forall {k} (as :: LoT k) (bs :: LoT k) (cs :: LoT k) a.
Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaChooseLeft
-- | Match 'Raw.OpIdent' via 'Eq'.
instance ZipMatchK Raw.OpIdent where zipMatchWithK :: forall (as :: LoT (*)) (bs :: LoT (*)) (cs :: LoT (*)).
Mappings as bs cs
-> (OpIdent :@@: as)
-> (OpIdent :@@: bs)
-> Maybe (OpIdent :@@: cs)
zipMatchWithK = Mappings as bs cs
-> (OpIdent :@@: as)
-> (OpIdent :@@: bs)
-> Maybe (OpIdent :@@: cs)
Mappings as bs cs -> OpIdent -> OpIdent -> Maybe OpIdent
forall {k} a (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
Eq a =>
Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaEq
-- | Match 'Raw.MetaVarIdent' via 'Eq'.
instance ZipMatchK Raw.MetaVarIdent where zipMatchWithK :: forall (as :: LoT (*)) (bs :: LoT (*)) (cs :: LoT (*)).
Mappings as bs cs
-> (MetaVarIdent :@@: as)
-> (MetaVarIdent :@@: bs)
-> Maybe (MetaVarIdent :@@: cs)
zipMatchWithK = Mappings as bs cs
-> (MetaVarIdent :@@: as)
-> (MetaVarIdent :@@: bs)
-> Maybe (MetaVarIdent :@@: cs)
Mappings as bs cs
-> MetaVarIdent -> MetaVarIdent -> Maybe MetaVarIdent
forall {k} a (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
Eq a =>
Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaEq

instance ZipMatchK a => ZipMatchK (Term'Sig a)
instance ZipMatchK a => ZipMatchK (OpArg'Sig a)
instance ZipMatchK a => ZipMatchK (Type'Sig a)

instance Foil.UnifiablePattern (Binders' a)

-- |
-- >>> "?m[App(Lam(x.x), Lam(y.y))]" :: Term' Raw.BNFC'Position Foil.VoidS
-- ?m [App (Lam (x0 . x0), Lam (x0 . x0))]
-- >>> "Lam(y. Let(Lam(x. x), f. ?m[y, App(f, y)]))" :: Term' Raw.BNFC'Position Foil.VoidS
-- Lam (x0 . Let (Lam (x1 . x1), x1 . ?m [x0, App (x1, x0)]))
instance IsString (Term' Raw.BNFC'Position Foil.VoidS) where
  fromString :: String -> Term' BNFC'Position 'VoidS
fromString = Scope 'VoidS
-> Map VarIdent (Name 'VoidS)
-> Term' BNFC'Position
-> Term' BNFC'Position 'VoidS
forall (o :: S) a.
(Distinct o, Ord VarIdent) =>
Scope o -> Map VarIdent (Name o) -> Term' a -> Term' a o
toTerm' Scope 'VoidS
Foil.emptyScope Map VarIdent (Name 'VoidS)
forall k a. Map k a
Map.empty (Term' BNFC'Position -> Term' BNFC'Position 'VoidS)
-> (String -> Term' BNFC'Position)
-> String
-> Term' BNFC'Position 'VoidS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Token] -> Either String (Term' BNFC'Position))
-> String -> Term' BNFC'Position
forall a. ([Token] -> Either String a) -> String -> a
unsafeParse [Token] -> Either String (Term' BNFC'Position)
Raw.pTerm

instance IsString (Type' Raw.BNFC'Position Foil.VoidS) where
  fromString :: String -> Type' BNFC'Position 'VoidS
fromString = Scope 'VoidS
-> Map VarIdent (Name 'VoidS)
-> Type' BNFC'Position
-> Type' BNFC'Position 'VoidS
forall (o :: S) a.
(Distinct o, Ord VarIdent) =>
Scope o -> Map VarIdent (Name o) -> Type' a -> Type' a o
toType' Scope 'VoidS
Foil.emptyScope Map VarIdent (Name 'VoidS)
forall k a. Map k a
Map.empty (Type' BNFC'Position -> Type' BNFC'Position 'VoidS)
-> (String -> Type' BNFC'Position)
-> String
-> Type' BNFC'Position 'VoidS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Token] -> Either String (Type' BNFC'Position))
-> String -> Type' BNFC'Position
forall a. ([Token] -> Either String a) -> String -> a
unsafeParse [Token] -> Either String (Type' BNFC'Position)
Raw.pType

-- |
-- >>> "Lam : ∀ a b. (a.b) → a→b" :: OpTyping' Raw.BNFC'Position Foil.VoidS
-- Lam : ∀ x0 x1 . (x0 . x1) → x0 → x1
instance IsString (OpTyping' Raw.BNFC'Position Foil.VoidS) where
  fromString :: String -> OpTyping' BNFC'Position 'VoidS
fromString = Scope 'VoidS
-> Map VarIdent (Name 'VoidS)
-> OpTyping' BNFC'Position
-> OpTyping' BNFC'Position 'VoidS
forall (o :: S) a.
(Distinct o, Ord VarIdent) =>
Scope o -> Map VarIdent (Name o) -> OpTyping' a -> OpTyping' a o
toOpTyping' Scope 'VoidS
Foil.emptyScope Map VarIdent (Name 'VoidS)
forall k a. Map k a
Map.empty (OpTyping' BNFC'Position -> OpTyping' BNFC'Position 'VoidS)
-> (String -> OpTyping' BNFC'Position)
-> String
-> OpTyping' BNFC'Position 'VoidS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Token] -> Either String (OpTyping' BNFC'Position))
-> String -> OpTyping' BNFC'Position
forall a. ([Token] -> Either String a) -> String -> a
unsafeParse [Token] -> Either String (OpTyping' BNFC'Position)
Raw.pOpTyping

-- |
-- >>> "?m[x y] ↦ App(y, x)" :: Subst' Raw.BNFC'Position Foil.VoidS
-- ?m [x0 x1] ↦ App (x1, x0)
instance IsString (Subst' Raw.BNFC'Position Foil.VoidS) where
  fromString :: String -> Subst' BNFC'Position 'VoidS
fromString = Scope 'VoidS
-> Map VarIdent (Name 'VoidS)
-> Subst' BNFC'Position
-> Subst' BNFC'Position 'VoidS
forall (o :: S) a.
(Distinct o, Ord VarIdent) =>
Scope o -> Map VarIdent (Name o) -> Subst' a -> Subst' a o
toSubst' Scope 'VoidS
Foil.emptyScope Map VarIdent (Name 'VoidS)
forall k a. Map k a
Map.empty (Subst' BNFC'Position -> Subst' BNFC'Position 'VoidS)
-> (String -> Subst' BNFC'Position)
-> String
-> Subst' BNFC'Position 'VoidS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Token] -> Either String (Subst' BNFC'Position))
-> String -> Subst' BNFC'Position
forall a. ([Token] -> Either String a) -> String -> a
unsafeParse [Token] -> Either String (Subst' BNFC'Position)
Raw.pSubst

-- |
-- >>> "∀ x y. ?m[x, y] = App(y, x)" :: Constraint' Raw.BNFC'Position Foil.VoidS
-- ∀ x0 x1 . ?m [x0, x1] = App (x1, x0)
instance IsString (Constraint' Raw.BNFC'Position Foil.VoidS) where
  fromString :: String -> Constraint' BNFC'Position 'VoidS
fromString = Scope 'VoidS
-> Map VarIdent (Name 'VoidS)
-> Constraint' BNFC'Position
-> Constraint' BNFC'Position 'VoidS
forall (o :: S) a.
(Distinct o, Ord VarIdent) =>
Scope o
-> Map VarIdent (Name o) -> Constraint' a -> Constraint' a o
toConstraint' Scope 'VoidS
Foil.emptyScope Map VarIdent (Name 'VoidS)
forall k a. Map k a
Map.empty (Constraint' BNFC'Position -> Constraint' BNFC'Position 'VoidS)
-> (String -> Constraint' BNFC'Position)
-> String
-> Constraint' BNFC'Position 'VoidS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Token] -> Either String (Constraint' BNFC'Position))
-> String -> Constraint' BNFC'Position
forall a. ([Token] -> Either String a) -> String -> a
unsafeParse [Token] -> Either String (Constraint' BNFC'Position)
Raw.pConstraint

instance Show (Term' a n) where show :: Term' a n -> String
show = Term' a -> String
forall a. Print a => a -> String
Raw.printTree (Term' a -> String)
-> (Term' a n -> Term' a) -> Term' a n -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term' a n -> Term' a
forall a (o :: S). Term' a o -> Term' a
fromTerm'
instance Show (Type' a n) where show :: Type' a n -> String
show = Type' a -> String
forall a. Print a => a -> String
Raw.printTree (Type' a -> String)
-> (Type' a n -> Type' a) -> Type' a n -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type' a n -> Type' a
forall a (o :: S). Type' a o -> Type' a
fromType'
instance Show (Subst' a n) where show :: Subst' a n -> String
show = Subst' a -> String
forall a. Print a => a -> String
Raw.printTree (Subst' a -> String)
-> (Subst' a n -> Subst' a) -> Subst' a n -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst' a n -> Subst' a
forall a (o :: S). Subst' a o -> Subst' a
fromSubst'
instance Show (Constraint' a n) where show :: Constraint' a n -> String
show = Constraint' a -> String
forall a. Print a => a -> String
Raw.printTree (Constraint' a -> String)
-> (Constraint' a n -> Constraint' a) -> Constraint' a n -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint' a n -> Constraint' a
forall a (o :: S). Constraint' a o -> Constraint' a
fromConstraint'
instance Show (OpTyping' a n) where show :: OpTyping' a n -> String
show = OpTyping' a -> String
forall a. Print a => a -> String
Raw.printTree (OpTyping' a -> String)
-> (OpTyping' a n -> OpTyping' a) -> OpTyping' a n -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpTyping' a n -> OpTyping' a
forall a (o :: S). OpTyping' a o -> OpTyping' a
fromOpTyping'

-- * User-defined helpers

unsafeParse :: ([Raw.Token] -> Either String a) -> String -> a
unsafeParse :: forall a. ([Token] -> Either String a) -> String -> a
unsafeParse [Token] -> Either String a
parse String
input =
  case [Token] -> Either String a
parse (String -> [Token]
Raw.myLexer String
input) of
    Left String
err -> String -> a
forall a. HasCallStack => String -> a
error String
err
    Right a
x -> a
x