Implement stage 1

module Main where

import Katrin

import Katrin.Core

import Katrin.Algebra

import System.Environment

-- | An excellent main function.

-- | ~ Chef Excellence

main :: IO ()

main = putStrLn "Nothing to see here."

main = do

    args <- getArgs

    let n = read (head args) :: Int

    let exp = Application ( (Lambda "x") (Application (Value "succ") (Value "x")) ) (Literal n)

    print $ (foldExpression algKatrinEval =<< foldExpression algKatrinBeta =<< foldExpression algKatrinBeta exp)

- base

- text

default-extensions:

- OverloadedStrings

- LambdaCase

library:

  source-dirs: src

  ghc-options:

  - -Wall

  - -Wno-name-shadowing

  - -Wno-unused-matches

executables:

  katrin:

module Katrin where

import Katrin.Core

import Katrin.Algebra

import Prelude hiding (String)  -- so I don't accidentally use String instead of Text

import Data.Text (Text)

import qualified Data.Text as Text

-- List stuff just for trying out algebras, nothing to do with Katrin

foldListExample :: Int

foldListExample = foldList (ListAlg 0 (+)) (Cons 1 $ Cons 2 $ Cons 42 Nil)  -- = 1 + 2 + 42 = 45

-- | An example type definition for natural numbers.

-- Corresponds to "data Nat = One | Succ Nat".

typeExampleNat :: TypeDef

typeExampleNat = TypeDef

    (ValueId "Nat")

    $ SumType (ProductType (ConstrId "One") []) (ProductType (ConstrId "Succ") [ValueId "Nat"])

defExampleNat :: Def

defExampleNat = Def

    (ValueId "two")

    (Variable $ ValueId "Nat")

    (Application (Variable $ ValueId "Succ") (Variable $ ValueId "One"))

katrinExample01 :: Katrin

katrinExample01 = Katrin [typeExampleNat] [defExampleNat]

{-# LANGUAGE OverloadedStrings, LambdaCase #-}

{-# LANGUAGE RecordWildCards #-}

module Katrin.Algebra (KatrinAlg, foldKatrin, katrinAlgTerm) where

module Katrin.Algebra where

import Katrin.Core

import Data.Text (Text)

import qualified Data.Text as T

-- | Algebraic signature (or context-free grammar) for Katrin.

data KatrinAlg katrin valueId constrId typeDef def typeExp exp = KatrinAlg {

    katrinAlg :: [typeDef] -> [def] -> katrin,

    valueIdAlg :: Text -> valueId,

    constrIdAlg :: Text -> constrId,

    typeDefAlg :: valueId -> typeExp -> typeDef,

    productTypeAlg :: constrId -> [valueId] -> typeExp,

    sumTypeAlg :: typeExp -> typeExp -> typeExp,

    defAlg :: valueId -> exp -> exp -> def,

    literalAlg :: constrId -> exp,

    applicationAlg :: exp -> exp -> exp,

    variableAlg :: valueId -> exp,

    lambdaAlg :: exp -> exp -> exp

-- | Algebraic signature (which is the context-free grammar for the tokens) for Katrin.

data AlgKatrin expression = AlgKatrin {

    algLiteral :: Int -> expression,

    algValue :: Text -> expression,

    algApplication :: expression -> expression -> expression,

    algLambda :: Text -> expression -> expression

}

{-

-- | Paramorphic variant of the algebraic signature for Katrin.

data AlgParaKatrin katrin definition identifier expression pattern = AlgParaKatrin {

    algParaKatrin :: [Definition] -> [definition] -> katrin,

    algParaDefinition :: Identifier -> identifier -> Expression -> expression -> definition,

    algParaIdentifier :: Text -> identifier,

---- CATAMORPHIC FOLD FUNCTIONS FOR KATRIN ----

    algParaLiteral :: Int -> expression,

    algParaValue :: Identifier -> identifier -> expression,

    algParaApplication :: Expression -> expression -> Expression -> expression -> expression,

    algParaLambda :: Pattern -> pattern -> Expression -> expression -> expression,

foldKatrin :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Katrin -> katrin

foldKatrin alg (Katrin tds ds) = katrinAlg alg (foldTypeDef alg <$> tds) (foldDef alg <$> ds)

    algParaBind :: Identifier -> identifier -> pattern,

    algParaMatch :: Int -> pattern

}

para2cata_katrin ::

    AlgParaKatrin katrin definition identifier expression pattern

    -> AlgKatrin (Katrin, katrin) (Definition, definition) (Identifier, identifier) (Expression, expression) (Pattern, pattern)

para2cata_katrin AlgParaKatrin{..} = AlgKatrin {

    algKatrin = \defs' -> let (defPs, defs) = unzip defs' in (Katrin defPs, algParaKatrin defPs defs),

foldValueId :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> ValueId -> valueId

foldValueId alg (ValueId t) = valueIdAlg alg t

    algDefinition = \(idP, id) (expP, exp) -> (Definition idP expP, algParaDefinition idP id expP exp),

foldConstrId :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> ConstrId -> constrId

foldConstrId alg (ConstrId t) = constrIdAlg alg t

    algIdentifier = \text -> (Identifier text, algParaIdentifier text),

foldTypeDef :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> TypeDef -> typeDef

foldTypeDef alg (TypeDef vid te) = typeDefAlg alg (foldValueId alg vid) (foldTypeExp alg te)

    algLiteral = \num -> (Literal num, algParaLiteral num),

    algValue = \(idP, id) -> (Value idP, algParaValue idP id),

    algApplication = \(exp1P, exp1) (exp2P, exp2) -> (Application exp1P exp2P, algParaApplication exp1P exp1 exp2P exp2),

    algLambda = \(patP, pat) (expP, exp) -> (Lambda patP expP, algParaLambda patP pat expP exp),

foldTypeExp :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> TypeExp -> typeExp

foldTypeExp alg (ProductType cid vids) = productTypeAlg alg (foldConstrId alg cid) (foldValueId alg <$> vids)

foldTypeExp alg (SumType te1 te2) = sumTypeAlg alg (foldTypeExp alg te1) (foldTypeExp alg te2)

    algBind = \(idP, id) -> (Bind idP, algParaBind idP id),

    algMatch = \num -> (Match num, algParaMatch num)

}

-}

foldDef :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Def -> def

foldDef alg (Def vid e1 e2) = defAlg alg (foldValueId alg vid) (foldExp alg e1) (foldExp alg e2)

-- Catamorphic fold functions

foldExp :: KatrinAlg katrin valueId constrId typeDef def typeExp exp -> Exp -> exp

foldExp alg (Literal cid) = literalAlg alg (foldConstrId alg cid)

foldExp alg (Application e1 e2) = applicationAlg alg (foldExp alg e1) (foldExp alg e2)

foldExp alg (Variable vid) = variableAlg alg (foldValueId alg vid)

foldExp alg (Lambda e1 e2) = lambdaAlg alg (foldExp alg e1) (foldExp alg e2)

{-

foldKatrin :: AlgKatrin katrin expression -> Katrin -> katrin

foldKatrin alg (Katrin exp) = algKatrin alg (foldExpression alg exp)

-}

foldExpression :: AlgKatrin expression -> Expression -> expression

foldExpression alg = \case

    (Literal num) -> algLiteral alg num

    (Value txt) -> algValue alg txt

    (Application exp1 exp2) -> algApplication alg (foldExpression alg exp1) (foldExpression alg exp2)

    (Lambda txt exp) -> algLambda alg txt (foldExpression alg exp)

---- ALGEBRAS FOR KATRIN ----

-- Algebras

-- | Term algebra for Katrin. `foldKatrin katrinAlgTerm` folds a Katrin term into a, well, Katrin term.

-- Useful for compilation into a Katrin term and for testing.

katrinAlgTerm :: KatrinAlg Katrin ValueId ConstrId TypeDef Def TypeExp Exp

katrinAlgTerm = KatrinAlg {

    katrinAlg = Katrin,

    valueIdAlg = ValueId,

    constrIdAlg = ConstrId,

    typeDefAlg = TypeDef,

    productTypeAlg = ProductType,

    sumTypeAlg = SumType,

    defAlg = Def,

    literalAlg = Literal,

    applicationAlg = Application,

    variableAlg = Variable,

    lambdaAlg = Lambda

katrinAlgTerm :: AlgKatrin Expression

katrinAlgTerm = AlgKatrin Literal Value Application Lambda

-- | Algebra that performs β-reduction on Katrin.

algKatrinBeta :: AlgKatrin (Either Text Expression)

algKatrinBeta = AlgKatrin {

    algLiteral = Right . Literal,

    algValue = Right . Value,

    algApplication = \exp1' exp2' -> do

        exp1 <- exp1'

        exp2 <- exp2'

        case exp1 of

            Lambda txt exp -> Right $ bind txt exp2 exp

            Value "succ" -> case exp2 of

                Literal n -> Right $ Literal $ n+1

                _ -> Right $ Application exp1 exp2

            Value txt -> Right $ Application exp1 exp2

            _ -> Left "Trying to apply something to a non-function.",

    algLambda = \txt exp -> exp >>= (Right . Lambda txt)

}

algKatrinEval :: AlgKatrin (Either Text Int)

algKatrinEval = AlgKatrin {

    algLiteral = \num -> Right num,

    algValue = \txt -> Left $ "Unresolved identifier " <> txt,

    algApplication = \exp1' exp2' -> Left "Unapplied Application",

    algLambda = \txt exp -> Left "Unapplied Lambda"

}

-- | Evaluation algebra into a String for Katrin. No type checking is performed.

katrinAlgEval :: KatrinAlg (ValueId -> Maybe Text) ValueId ConstrId [ValueId -> Exp] (ValueId, Text) typeExp ([Def] -> Text)

katrinAlgEval = KatrinAlg {

    katrinAlg = \tdefs defs -> \vid -> lookup vid defs,

-- | Replaces all values in an expression with fitting identifier with literal values

bind :: Text  -- Identifier to bind

    -> Expression  -- Expression to paste

    -> Expression  -- Expression to bind in

    -> Expression  -- Result

bind bindId arg = \case

    Literal num -> Literal num

    Value id

        | id == bindId -> arg

        | otherwise -> Value id

    Application exp1 exp2 -> Application (bind bindId arg exp1) (bind bindId arg exp2)

    Lambda txt exp

        | txt == bindId -> Lambda txt exp

        | otherwise -> Lambda txt (bind bindId arg exp)

    valueIdAlg = ValueId,

    constrIdAlg = ConstrId,

    typeDefAlg = \vid te -> undefined,

{-

algKatrinTemplate :: AlgKatrin katrin identitfier pattern expression definition

algKatrinTemplate = AlgKatrin {

    algKatrin = \defs -> undefined,

    productTypeAlg = undefined,

    sumTypeAlg = undefined,

    algIdentifier = \txt -> undefined,

    defAlg = \vid et e -> (vid, undefined),

    algBind = \id -> undefined,

    algMatch = \num -> undefined,

    literalAlg = \cid -> \defs -> T.pack $ show cid,

    applicationAlg = \e1 e2 -> \defs -> undefined,  -- T.concat [T.pack $ undefined, "(", T.pack $ show undefined, ")"],

    variableAlg = \vid -> \case

        [] -> T.pack $ show vid

        (Def vid te e):defs -> undefined,

    lambdaAlg = undefined

}

    algLiteral = \num -> undefined,

    algValue = \id -> undefined,

    algApplication = \exp1 exp2 -> undefined,

    algLambda = \pat exp -> undefined,

{-

Template for Katrin algebras

katrinAlgEval = KatrinAlg {

    katrinAlg = undefined,

    valueIdAlg = undefined,

    constrIdAlg = undefined,

    typeDefAlg = undefined,

    productTypeAlg = undefined,

    sumTypeAlg = undefined,

    defAlg = undefined,

    literalAlg = undefined,

    applicationAlg = undefined,

    variableAlg = undefined,

    lambdaAlg = undefined

    algDefinition = \id exp -> undefined

}

-}

import Data.Text (Text)

-- | Main data type for a Katrin library consisting of a list of type definitions and a list of definitions.

data Katrin = Katrin {typeDefs :: [TypeDef], defs :: [Def]} deriving (Show, Read, Eq)

newtype Katrin = Katrin Expression

    deriving (Show, Read, Eq)

-- | Type for an identifier of a value, like an integer, a function, a type etc.

newtype ValueId = ValueId Text deriving (Show, Read, Eq)

-- | Type for expressions, which are either a literal, a value identifier, a function application or a lambda function.

data Expression =

      Literal Int

    | Value Text

    | Application Expression Expression

    | Lambda Text Expression

    deriving (Show, Read, Eq)

-- | Type for an identifier of a constructor.

newtype ConstrId = ConstrId Text deriving (Show, Read, Eq)

data Result = Number Int | Function (Int -> Result)

-- | A type definition, consisting of an identifier for the type and the corresponding type expression.

data TypeDef = TypeDef {

    typeId :: ValueId,

    typeExp :: TypeExp

} deriving (Show, Read, Eq)

{-

instance Show Result where

    show (Number num) = "Number " <> show num

    show (Function f) = "[Function]"

-- | A type expression, consisting of stuff.

-- TODO explain that. I'm too lazy right now.

data TypeExp = ProductType ConstrId [ValueId] | SumType TypeExp TypeExp

    deriving (Show, Read, Eq)

instance Monoid a => Alternative (Either a) where

    empty = Left mempty

    (<|>) = mplus

data Def = Def {

    expId :: ValueId,

    expType :: Exp,

    exp :: Exp

} deriving (Show, Read, Eq)

data Exp =

    Literal ConstrId

    | Application {function :: Exp, argument :: Exp}

    | Variable {symbol :: ValueId}

    | Lambda {inPattern :: Exp, outExp :: Exp}

    deriving (Show, Read, Eq)

instance Monoid a => MonadPlus (Either a) where

    mzero = Left mempty

    mplus (Right x) _ = Right x

    mplus _ y = y

lookupDefinition :: [Definition] -> Identifier -> Either Text [Expression]

lookupDefinition [] _ = Left "Reached end while looking up definitions"

lookupDefinition (Definition defId exps:defs) id

    | defId == id = Right exps

    | otherwise = lookupDefinition defs id

asValue :: [Expression] -> Either Text Int

asValue (Literal num:exps) = Right num

asValue x = Left $ "Trying to use a non-literal as value: " <> pack (show x)

asFunction :: [Expression] -> Int -> [Expression]

asFunction (Lambda pat exp : exps) arg = case pat of

    Bind id -> bind id arg exp : asFunction exps arg

    Match num

        | num == arg -> exp : asFunction exps arg

        | otherwise -> exps

asFunction (_:exps) arg = asFunction exps arg

asFunction [] _ = []

-- | Replaces all values in an expression with fitting identifier with literal values

bind :: Identifier -> Int -> Expression -> Expression

bind bindId arg = \case

    Literal num -> Literal num

    Value id

        | id == bindId -> Literal arg

        | otherwise -> Value id

    Application exp1 exp2 -> Application (bind bindId arg exp1) (bind bindId arg exp2)

    Lambda pat exp -> case pat of

        Bind id

            | id == bindId -> Lambda pat exp

            | otherwise -> Lambda pat (bind bindId arg exp)

        Match num -> Lambda pat (bind bindId arg exp)

{-

apply :: Expression -> Expression -> Either Text Expression

apply exp1 exp2 = case exp1 of

    Value (Identifier "succ") -> asValue [exp2] >>= return . Literal . (+1)

-}

-}