+{-# LANGUAGE ExistentialQuantification #-}
module Hcompta.LCC.Compta where
-import Control.Applicative (Applicative(..))
import Control.Monad (Monad(..))
import Data.Bool (Bool(..))
import Data.Either (either)
import Data.Eq (Eq)
import Data.Function (($), (.), id)
-import Data.Functor (Functor(..), (<$>))
-import Data.Typeable (Typeable)
+import Data.Functor ((<$>))
+import Data.Functor.Identity (Identity(..))
import Prelude (error)
import Text.Show (Show(..))
import qualified Control.Monad.Classes as MC
import qualified Control.Monad.Trans.State.Strict as SS
+import qualified Hcompta.LCC.Lib.Strict as S
import Hcompta.LCC.Amount
import Hcompta.LCC.Balance
import Hcompta.LCC.Transaction
import Language.Symantic as Sym
import qualified Hcompta as H
-import qualified Hcompta.LCC.Lib.Strict as S
-- * Type 'LCC'
data LCC src
} deriving (Eq, Show)
instance H.Get Style_Amounts (LCC src) where
get = lcc_style
+instance H.Sumable Balance (LCC src) where
+ b += l = b H.+= lcc_journals l
-- ** Type 'State_Sym'
data State_Sym src ss
stateN _px f = S.StateT $ SS.state $ \st ->
(\a -> st{state_sym_types=a}) <$> f (state_sym_types st)
--- * Type 'Context'
-type Context m = SS.State m
+-- * Type 'Database'
+newtype Database db a = Database (S.StateT db Identity a)
+
+-- * Type 'Query'
+newtype Query db a = Query { runQuery :: db -> a }
+
+-- * Type 'Queryable'
+class Queryable db a where
+ query :: Query db a
+instance Queryable (LCC src) Balance where
+ query = Query $ H.sum . lcc_journals
+
+{-
+-- * Type 'Base'
+data Base =
+ forall db.
+ Typeable db =>
+ Base (Type src vs db) db
+
+-- * Type 'DataBase'
+data DataBase = forall db. Typeable db => DataBase db
-- * Type 'Code'
newtype Code src ss m a
= Code (S.StateT (State_Sym src (Sym.Proxy (Code src ss) ': ss)) m a)
deriving (Functor, Applicative, Monad, Typeable)
+-}
+{-
-- * Class 'Balanceable'
-class Balanceable ctx where
- balance :: Context ctx Balance
+class Balanceable a where
+ balance :: a -> Balance
instance Balanceable (LCC src) where
- balance = do
- js <- SS.gets lcc_journals
- return (H.sum js)
+ balance = H.sum . lcc_journals @src
+-}
+
+-- LCC src
+type instance MC.CanDo (S.StateT (LCC src) m) (MC.EffState (LCC src)) = 'True
+instance Monad m => MC.MonadStateN 'MC.Zero (LCC src) (S.StateT (LCC src) m) where
+ stateN _px = S.StateT . SS.state
+
+
+
{-
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Main where
+import Control.Arrow (left)
import Control.Applicative (Applicative(..))
-import Control.Monad (Monad(..), void)
+import Control.Monad (Monad(..), void, when)
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Trans.Class as MT (MonadTrans(..))
import Data.Bool (Bool(..))
import Data.Function (($), (.), id)
import Data.Functor (Functor(..), (<$>))
import Data.Maybe (Maybe(..), maybe)
+import Data.Monoid (Monoid(..))
import Data.Semigroup ((<>))
import Data.String (String)
import Data.Text (Text)
-import Prelude (error, succ, Integer)
+import Prelude (error, succ, Integer, undefined)
import System.Console.Haskeline as HL
import System.IO (IO, putStr, putStrLn, print)
import Text.Show (Show(..))
import qualified Control.Monad.Classes as MC
+import qualified Control.Monad.Classes.Run as MC
import qualified Control.Monad.Trans.State.Strict as SS
import qualified Data.Char as Char
import qualified Data.List as L
{ historyFile = Just ".hcompta.history"
, autoAddHistory = False
} $
- S.evalState (LCC.state_sym @LCC.Sym.SRC @LCC.Sym.SS) $
- unREPL (loop True 0)
+ MC.evalStateStrict evalTeUnit $
+ S.evalState (LCC.state_sym @LCC.Sym.SRC @(Proxy Eval ': LCC.Sym.SS)) $
+ unREPL $ loop True 0
where
loop :: forall src ss.
Show src =>
Syms ss Eval =>
- Syms ss View =>
- Syms ss (BetaT View) =>
+ -- Syms ss View =>
+ -- Syms ss (BetaT View) =>
+ SymInj ss Eval =>
ReadTe src ss =>
- Gram_Term src ss (G src ss (InputT IO)) =>
+ Gram_Term src ss (G src ss (SS.StateT (TermVT src ss '[]) (InputT IO))) =>
Bool -> Integer -> REPL src ss ()
loop ok i = do
let prompt =
case line of
Nothing -> loop ok i
Just l -> do
- void $ REPL $ lift $
+ void $ REPL $ lift $ lift $
HL.modifyHistory $
HL.addHistoryRemovingAllDupes l
REPL (parseTe $ Text.pack l) >>= \case
loop False (succ i)
Right expr ->
case expr of
- Command_Def nam ast -> runTe nam ast
- Command_Eval ast -> runTe "it" ast
+ Command_Def nam ast -> runTe nam ast
+ Command_Bind nam ast -> runTe nam ast
+ Command_Eval ast -> runTe "ans" ast
where
runTe nam ast =
case readTe ast of
REPL $ do
MC.modify $ \(imps::Imports NameTe, mods) ->
(imps, insTerm nam te mods)
- evalTe te
+ lr_r <- evalTe te
+ case lr_r of
+ Right r ->
+ when (nam == NameTe "base") $ MC.put r
+ Left (Error_Eval_Cannot_prove_Constraint (TypeVT q)) ->
+ printTy q >>= ansiIO . ("Cannot prove Constraint: " <>)
loop True (succ i)
- insTerm :: Sym.NameTe -> Sym.TermVT src ss '[] -> Sym.Modules src ss -> Sym.Modules src ss
- insTerm n t = Sym.insertTermVT ([] `Sym.Mod` t) n (Sym.Fixity2 Sym.infixN5)
-
+ insTerm ::
+ Sym.NameTe ->
+ Sym.TermVT src ss '[] ->
+ Sym.Modules src ss ->
+ Sym.Modules src ss
+ insTerm n t =
+ Sym.insertTermVT ([] `Sym.Mod` t) n $
+ Sym.Fixity2 Sym.infixN5
+
+type instance MC.CanDo (S.StateT (LCC.State_Sym src ss) m) (MC.EffState (TermVT src ss '[])) = 'False
+-- type instance MC.CanDo (S.StateT (LCC.State_Sym src ss) m) (MC.EffState (EvalVT src)) = 'False
+
+-- * Type 'G'
type G src ss m =
P.ParsecT P.Dec Text
(S.StateT (LCC.State_Sym src ss) m)
+-- * Type 'Command'
data Command src ss
= Command_Eval (AST_Term src ss)
| Command_Def NameTe (AST_Term src ss)
+ | Command_Bind NameTe (AST_Term src ss)
deriving (Eq, Show)
parseTe ::
forall ss src m.
Monad m =>
Gram_Term src ss (G src ss m) =>
- Text -> S.StateT (LCC.State_Sym src ss) m
- (Either (P.ParseError Char P.Dec) (Command src ss))
+ Text ->
+ S.StateT (LCC.State_Sym src ss) m
+ (Either (P.ParseError Char P.Dec) (Command src ss))
parseTe = P.runParserT g ""
where
g :: G src ss m (Command src ss)
- g = G.unCF $ G.try gCmdLet G.<+> gCmdEval
+ g = G.unCF $
+ G.try gCmdLet G.<+>
+ G.try gCmdBind G.<+>
+ gCmdEval
gCmdLet =
Command_Def
<$ G.optional (G.try $ G.symbol "let")
Command_Eval
<$> Sym.g_term
<* G.eoi
+ gCmdBind =
+ Command_Bind
+ <$> Sym.g_NameTe
+ <* G.symbol "<-"
+ <*> Sym.g_term
+ <* G.eoi
-- * Type 'ReadTe'
type ReadTe src ss =
readTe ::
forall src ss.
( Syms ss Eval
- , Syms ss View
- , Syms ss (BetaT View)
+ -- , Syms ss View
+ -- , Syms ss (BetaT View)
, ReadTe src ss
) =>
AST_Term src ss ->
ansiIO :: MonadIO m => D.ANSI_IO -> m ()
ansiIO = liftIO . (`D.ansiIO` IO.stdout)
+-- * Type 'Error_Eval'
+data Error_Eval src
+ = Error_Eval_Cannot_prove_Constraint (TypeVT src)
+ deriving (Eq, Show)
+
evalTe ::
forall src ss m.
Source src =>
- Syms ss View =>
Syms ss Eval =>
- Syms ss (BetaT View) =>
+ -- Syms ss View =>
+ -- Syms ss (BetaT View) =>
+ SymInj ss Eval =>
+ SourceInj (TypeVT src) src =>
MonadIO m =>
TermVT src ss '[] ->
- S.StateT (LCC.State_Sym src ss) m ()
-evalTe (TermVT (Term q t (TeSym te))) = do
+ S.StateT (LCC.State_Sym src ss)
+ (SS.StateT (TermVT src ss '[]) m)
+ (Either (Error_Eval src) (TermVT src ss '[]))
+evalTe te@(TermVT (Term q t (TeSym sym))) = do
printTy (q #> t) >>= ansiIO . ("Type: " <>)
- case proveConstraint q of
- Nothing -> printTy q >>= ansiIO . ("Cannot prove Constraint: " <>)
- Just Dict -> liftIO $ do
- Text.putStrLn $ "View: " <> view (betaT $ te CtxTeZ)
- case t of
- io:@aTy | Just HRefl <- proj_ConstKiTy @_ @IO io -> do
- a <- eval $ te CtxTeZ
- printTe aTy a
- aTy ->
- let a = eval $ te CtxTeZ in
+ -- liftIO $ Text.putStrLn $ "View: " <> view (betaT $ sym CtxTeZ)
+ case t of
+ io:@aTy | Just HRefl <- proj_ConstKiTy @_ @IO io -> do
+ case proveConstraint q of
+ Nothing -> return $ Left $ Error_Eval_Cannot_prove_Constraint $ TypeVT q
+ Just Dict -> do
+ a <- liftIO $ eval $ sym CtxTeZ
+ let r = TermVT $ teEval_uneval aTy a
printTe aTy a
+ return $ Right r
+ _ -> do
+ r@(TermVT (Term q' t' (TeSym sym'))) <- completeTe te
+ printTy (q' #> t') >>= ansiIO . ("Type: Completed: " <>)
+ case proveConstraint q' of
+ Nothing -> return $ Left $ Error_Eval_Cannot_prove_Constraint $ TypeVT q'
+ Just Dict -> do
+ let a = eval $ sym' CtxTeZ
+ printTe t' a
+ return $ Right r
+
+completeTe ::
+ forall src ss m.
+ Source src =>
+ Syms ss Eval =>
+ -- Syms ss View =>
+ -- Syms ss (BetaT View) =>
+ SourceInj (TypeVT src) src =>
+ MonadIO m =>
+ TermVT src ss '[] ->
+ S.StateT (LCC.State_Sym src ss)
+ (SS.StateT (TermVT src ss '[]) m)
+ (TermVT src ss '[])
+completeTe t = do
+ liftIO $ putStrLn "completeTe"
+ st :: TermVT src ss '[] <- MC.get
+ case betaTerms $ G.BinTree0 t `G.BinTree2` G.BinTree0 st of
+ Left _ -> do
+ liftIO $ putStrLn "completeTe: Left"
+ return t
+ Right s -> do
+ liftIO $ putStrLn "completeTe: Right"
+ return s
printTy ::
forall src ss m vs t d.
, config_Doc_Type_imports = impsTy
} 0 ty <> D.eol
-printTe :: Source src => Type src vs a -> a -> IO ()
+printTe :: Source src => MonadIO m => Type src vs a -> a -> m ()
printTe aTy a =
case proveConstraint $ LCC.Sym.tyWriteable
(allocVarsR (lenVars aTy) $ LCC.Sym.tyContext_Write @_ @'[] ~> LCC.Sym.tyANSI_IO) aTy of
- Just Dict -> (`D.ansiIO` IO.stdout) $ write a context_write
- Nothing ->
+ Just Dict -> ansiIO $ write a context_write
+ Nothing -> liftIO $
case proveConstraint $ Sym.tyShow aTy of
Nothing -> putStrLn $ "No Show instance for type: " <> show aTy
- Just Dict -> print a
+ Just Dict -> do
+ putStrLn "Show:"
+ print a
-- * Type 'REPL'
-- /Read Eval Print Loop/ monad.
newtype REPL src ss a
= REPL
- { unREPL :: S.StateT (LCC.State_Sym src ss) (InputT IO) a }
+ { unREPL :: S.StateT (LCC.State_Sym src ss)
+ (SS.StateT (TermVT src ss '[])
+ (InputT IO))
+ a }
deriving ( Functor
, Applicative
, Monad
instance MonadTrans (REPL src ss) where
lift = REPL . lift . lift
-}
-type instance MC.CanDo (REPL src ss) (MC.EffState (LCC.State_Sym src ss)) = 'False
+type instance MC.CanDo (REPL src ss) (MC.EffState (LCC.State_Sym src ss)) = 'False
type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.Imports ns, Sym.Modules src ss)) = 'False
type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.Imports ns, Sym.ModulesTy src)) = 'False
+type instance MC.CanDo (REPL src ss) (MC.EffState (Sym.TermVT src ss '[])) = 'False
+-- type instance MC.CanDo (REPL src ss) (MC.EffState (EvalVT src)) = 'False
+{-
-- * Type 'State_REPL'
-data State_REPL
+data State_REPL src ss
= State_REPL
- { state_repl_env :: ()
+ { state_repl_terms :: LCC.State_Sym src ss
+ , state_repl_db :: db
}
+-- State_REPL src ss db
+type instance MC.CanDo (S.StateT (State_REPL src ss db) m) (MC.EffState (State_REPL src ss db)) = 'True
+instance Monad m => MC.MonadStateN 'MC.Zero (State_REPL src ss db) (S.StateT (State_REPL src ss db) m) where
+ stateN _px = S.StateT . SS.state
+
+-- LCC.State_Sym src ss
+type instance MC.CanDo (S.StateT (State_REPL src ss db) m) (MC.EffState (State_REPL src ss db)) = 'True
+instance Monad m => MC.MonadStateN 'MC.Zero (State_REPL src ss db) (S.StateT (LCC.State_Sym src ss) m) where
+ stateN _px f = S.StateT $ SS.state $ \st ->
+ (\a -> st{state_repl_terms=a}) <$> f (state_repl_terms st)
+-}
readLine :: String -> REPL src ss (Maybe String)
readLine prompt = do
- line <- REPL . lift $ getInputLine prompt
+ line <- REPL . lift . lift $ getInputLine prompt
case line of
Just l@(':':_) -> return $ Just l
Just l@(_:_) | L.last l == ' ' -> readLines l
where
readLines :: String -> REPL src ss (Maybe String)
readLines acc = do
- line <- REPL . lift $ getInputLine ""
+ line <- REPL . lift . lift $ getInputLine ""
case line of
Just l@(_:_) | L.last l == ' ' -> readLines $ acc <> l
Just l -> return $ Just $ acc <> l
G.try (Command_Def <$> Sym.g_NameTe <* G.lexeme (G.char '=') <*> Sym.g_term <* G.eoi) G.<+>
(Command_Eval <$> Sym.g_term <* G.eoi)
-}
+
+
+evalTeUnit :: Source src => SymInj ss () => TermVT src ss '[]
+evalTeUnit = TermVT $ Sym.teUnit -- Term noConstraint Sym.tyUnit $ teSym @() $ Sym.unit
+
+{-
+evalTeUnit :: Source src => EvalVT src
+evalTeUnit = EvalVT (Sym.tyUnit @_ @'[]) $ eval Sym.unit
+
+-- * Type 'EvalVT'
+data EvalVT src = forall vs t. EvalVT (Type src vs t) t
+
+appEvalVT ::
+ SourceInj (TypeVT src) src =>
+ Constable (->) =>
+ EvalVT src ->
+ EvalVT src ->
+ Either (Error_Beta src) (EvalVT src)
+appEvalVT (EvalVT tf te_fun) (EvalVT ta te_arg) =
+ let (tf',ta') = appendVars tf ta in
+ case unTyFun tf' of
+ Nothing -> Left $ Error_Beta_Term_not_a_function $ TypeVT tf'
+ Just (af,_rf) -> do
+ mgu <-
+ (Error_Beta_Unify `left`) $
+ case (unQualsTy af, unQualsTy ta') of
+ (TypeK af', TypeK ta'') -> unifyType mempty af' ta''
+ let tf'' = subst mgu tf'
+ let ta'' = subst mgu ta'
+ appEval tf'' te_fun ta'' te_arg $ \tr te_res ->
+ normalizeVarsTy tr $ \tr' ->
+ EvalVT tr' te_res
+
+appEval ::
+ forall src vs fun arg ret.
+ SourceInj (TypeVT src) src =>
+ Constable (->) =>
+ Type src vs fun -> fun ->
+ Type src vs arg -> arg ->
+ (forall res. Type src vs res -> res -> ret) ->
+ Either (Error_Beta src) ret
+appEval tf fun ta arg k =
+ case tf of
+ a2b :@ a2b_a :@ a2b_b
+ | Just HRefl <- proj_ConstKiTy @(K (->)) @(->) a2b ->
+ case a2b_a `eqType` ta of
+ Nothing -> Left $ Error_Beta_Type_mismatch (TypeVT a2b_a) (TypeVT ta)
+ Just Refl -> Right $ k a2b_b $ fun arg
+ _ -> Left $ Error_Beta_Term_not_a_function $ TypeVT tf
+-}
+
+
+
+-- * Class 'Sym_Eval'
+type instance Sym Eval = Sym_Eval
+class Sym_Eval term where
+ uneval :: a -> term a
+ default uneval :: Sym_Eval (UnT term) => Trans term => a -> term a
+ uneval = trans . uneval
+
+-- Interpreting
+instance Sym_Eval Eval where
+ uneval a = Eval a
+{-
+instance Sym_Eval View where
+ uneval = View $ \_p _v -> "()"
+instance (Sym_Eval r1, Sym_Eval r2) => Sym_Eval (Dup r1 r2) where
+ uneval = uneval `Dup` uneval
+-}
+
+-- Transforming
+instance (Sym_Eval term, Sym_Lambda term) => Sym_Eval (BetaT term)
+
+-- Typing
+instance NameTyOf Eval where
+ nameTyOf _c = [] `Mod` "Eval"
+instance ClassInstancesFor Eval where
+instance TypeInstancesFor Eval
+instance FixityOf Eval
+
+-- Compiling
+instance
+ ( SymInj ss Eval
+ ) => Gram_Term_AtomsFor src ss g Eval where
+instance ModuleFor src ss Eval
+
+-- ** 'Type's
+tyEval :: Source src => LenInj vs => Type src vs Eval
+tyEval = tyConst @(K Eval) @Eval
+
+-- ** 'Term's
+teEval_uneval ::
+ Source src => SymInj ss Eval =>
+ Type src vs a -> a ->
+ Term src ss ts vs (() #> a)
+teEval_uneval ty a =
+ Term (noConstraintLen $ lenVars ty) ty $
+ symInj @Eval $
+ TeSym $ \_c -> uneval a
sourcephile / git / comptalang.git / commitdiff