{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Symantics.
module Hcompta.LCC.Sym
 ( module Hcompta.LCC.Sym
 , module Hcompta.LCC.Sym.Account
 , module Hcompta.LCC.Sym.Addable
 , module Hcompta.LCC.Sym.Amount
 , module Hcompta.LCC.Sym.Compta
 , module Hcompta.LCC.Sym.Date
 , module Hcompta.LCC.Sym.FileSystem
 , module Hcompta.LCC.Sym.Journal
 , module Hcompta.LCC.Sym.Negable
 , module Hcompta.LCC.Sym.Posting
 , module Hcompta.LCC.Sym.Quantity
 , module Hcompta.LCC.Sym.Subable
 , module Hcompta.LCC.Sym.Transaction
 , module Hcompta.LCC.Sym.Unit
 , module Hcompta.LCC.Sym.Zipper
 ) where

import Hcompta.LCC.Sym.Account
import Hcompta.LCC.Sym.Addable
import Hcompta.LCC.Sym.Amount
import Hcompta.LCC.Sym.Compta
import Hcompta.LCC.Sym.Date
import Hcompta.LCC.Sym.FileSystem
import Hcompta.LCC.Sym.Journal
import Hcompta.LCC.Sym.Negable
import Hcompta.LCC.Sym.Posting
import Hcompta.LCC.Sym.Quantity
import Hcompta.LCC.Sym.Subable
import Hcompta.LCC.Sym.Transaction
import Hcompta.LCC.Sym.Unit
import Hcompta.LCC.Sym.Zipper

import Hcompta.LCC.Account (Account)
import Hcompta.LCC.Amount (Amounts, Quantity, Unit)
import Hcompta.LCC.Journal (Journal, PathFile)
import Hcompta.LCC.Compta (Compta)
import Hcompta.LCC.Posting (Posting, Date)
import Hcompta.LCC.Transaction (Transaction)
import Hcompta.Quantity (Addable, Negable, Subable)

import Control.Applicative (Alternative)
import Data.Bool (Bool)
import Data.Either (Either(..))
import Data.Eq (Eq)
import Data.Foldable (Foldable)
import Data.Map.Strict (Map)
import Data.Maybe (Maybe)
import Data.NonNull (NonNull)
import Data.Ord (Ord)
import Data.Proxy
import Data.Traversable (Traversable)
import Data.TreeMap.Strict.Zipper (Zipper)
import Text.Show (Show)

{-
import Hcompta.LCC.Grammar
import Hcompta.LCC.Journal
import Hcompta.LCC.Read
import Language.Symantic.Grammar
import qualified Text.Megaparsec as P
import qualified Data.Strict as S
import System.IO (IO)
import Prelude hiding (read, readFile)
-}

type SS =
 [ Proxy Account
 , Proxy Addable
 , Proxy Alternative
 , Proxy Amounts
 , Proxy (->)
 , Proxy Bool
 , Proxy Date
 , Proxy Either
 , Proxy Eq
 , Proxy Foldable
 , Proxy Journal
 , Proxy Map
 , Proxy Maybe
 , Proxy Negable
 , Proxy NonNull
 , Proxy Ord
 , Proxy PathFile
 , Proxy Posting
 , Proxy Quantity
 , Proxy Show
 , Proxy Subable
 , Proxy Transaction
 , Proxy Traversable
 , Proxy Unit
 , Proxy Zipper
 -- , Proxy (Compta () (SymsFix FixSS))
 ]


{-
data Error_App cs
 =   Error_App_not_applicable
 |   Error_App_type_mismatch (Sym.EType cs) (Sym.EType cs)
 deriving (Eq, Show)

app
 :: Sym.Inj_TyConst cs (->)
 => Sym.ETermClosed cs is
 -> Sym.ETermClosed cs is
 -> Either (Error_App cs) (Sym.ETermClosed cs is)
app (Sym.ETermClosed ty_f (Sym.TermClosed te_f))
    (Sym.ETermClosed ty_a (Sym.TermClosed te_a)) =
	case ty_f of
	 ty_fun Sym.:$ ty_arg Sym.:$ ty_res
	  | Just Refl <- Sym.kind_of ty_fun `Sym.eq_skind` (Sym.kind::Sym.SKind (Kind.Type -> Kind.Type -> Kind.Type))
	  , Just Refl <- ty_fun `Sym.eq_Type` Sym.ty @(->) ->
		case ty_arg `Sym.eq_Type` ty_a of
		 Just Refl -> Right $ Sym.ETermClosed ty_res $ Sym.TermClosed $ te_f Sym..$ te_a
		 Nothing -> Left $ Error_App_type_mismatch (Sym.EType ty_arg) (Sym.EType ty_a)
	 _ -> Left $ Error_App_not_applicable
feed_args :: Sym.TermAVT src -> [Sym.TermAVT src] -> Sym.TermAVT src
feed_args te as = go te as
	where
	go f [] = f
	go f (x:xs) =
		case f `app` x of
		 Right f' -> f' `go` as
		 Left _err -> f `go` xs
-}
{-
type SRC = ()
x0 ::
 IO ( ( Either (P.ParseError Char P.Dec)
                 (S.Either [At SRC (Error_Compta SRC)] (CanonFile, Journal [Transaction]))
        , Context_Read SRC [Transaction] )
      , Context_Sym SRC SS )
x0 = readJournal @SS "./Hcompta/LCC/Journal/02.jnl" (:)

y0
 -- :: CF (P.ParsecT P.Dec Text m) a
 :: ( m ~ S.StateT (Context_Read j) (S.StateT (Context_Sym cs is) IO)
    , is ~ Ifaces
    , cs ~ Sym.TyConsts_of_Ifaces is
    -- , e ~ P.ParseError Char P.Dec
    )
 => CF (P.ParsecT P.Dec Text m)
       ( Sym.Term_Name
       , Either (At (Sym.Error_Term Meta cs is))
                (Sym.ETerm cs is) )
y0 = g_term
-}