Merge pull request 'Expands CLI support with output forms and decoding' (#7) from feat/ternary-representation into main
Reviewed-on: #7
This commit is contained in:
commit
e22ff06bfe
@ -1,6 +1,7 @@
|
|||||||
module Compiler where
|
module Compiler where
|
||||||
|
|
||||||
import Eval
|
import Eval
|
||||||
|
import Library
|
||||||
import Parser
|
import Parser
|
||||||
import Research
|
import Research
|
||||||
|
|
||||||
@ -11,13 +12,8 @@ import qualified Data.Map as Map
|
|||||||
evaluateFile :: FilePath -> IO T
|
evaluateFile :: FilePath -> IO T
|
||||||
evaluateFile filePath = do
|
evaluateFile filePath = do
|
||||||
contents <- readFile filePath
|
contents <- readFile filePath
|
||||||
let linesOfFile = lines contents
|
let asts = parseTricu contents
|
||||||
let env = foldl evaluateLine Map.empty linesOfFile
|
let finalEnv = evalTricu library asts
|
||||||
case Map.lookup "__result" env of
|
case Map.lookup "__result" finalEnv of
|
||||||
Just finalResult -> return finalResult
|
Just finalResult -> return finalResult
|
||||||
Nothing -> error "No result found in final environment"
|
Nothing -> error "No result found in final environment"
|
||||||
|
|
||||||
evaluateLine :: Env -> String -> Env
|
|
||||||
evaluateLine env line =
|
|
||||||
let ast = parseSingle line
|
|
||||||
in evalSingle env ast
|
|
||||||
|
43
src/Eval.hs
43
src/Eval.hs
@ -30,33 +30,36 @@ evalSingle env term = case term of
|
|||||||
in Map.insert "__result" result env
|
in Map.insert "__result" result env
|
||||||
|
|
||||||
evalTricu :: Map String T -> [TricuAST] -> Map String T
|
evalTricu :: Map String T -> [TricuAST] -> Map String T
|
||||||
evalTricu env [] = env
|
evalTricu env list = evalTricu' env (filter (/= SEmpty) list)
|
||||||
evalTricu env [lastLine] =
|
where
|
||||||
|
evalTricu' :: Map String T -> [TricuAST] -> Map String T
|
||||||
|
evalTricu' env [] = env
|
||||||
|
evalTricu' env [lastLine] =
|
||||||
let lastLineNoLambda = eliminateLambda lastLine
|
let lastLineNoLambda = eliminateLambda lastLine
|
||||||
updatedEnv = evalSingle env lastLineNoLambda
|
updatedEnv = evalSingle env lastLineNoLambda
|
||||||
in Map.insert "__result" (result updatedEnv) updatedEnv
|
in Map.insert "__result" (result updatedEnv) updatedEnv
|
||||||
evalTricu env (line:rest) =
|
evalTricu' env (line:rest) =
|
||||||
let lineNoLambda = eliminateLambda line
|
let lineNoLambda = eliminateLambda line
|
||||||
updatedEnv = evalSingle env lineNoLambda
|
updatedEnv = evalSingle env lineNoLambda
|
||||||
in evalTricu updatedEnv rest
|
in evalTricu updatedEnv rest
|
||||||
|
|
||||||
evalAST :: Map String T -> TricuAST -> T
|
evalAST :: Map String T -> TricuAST -> T
|
||||||
evalAST env term = case term of
|
evalAST env term = case term of
|
||||||
SVar name -> case Map.lookup name env of
|
SVar name -> case Map.lookup name env of
|
||||||
Just value -> value
|
Just value -> value
|
||||||
Nothing -> error $ "Variable " ++ name ++ " not defined"
|
Nothing -> error $ "Variable " ++ name ++ " not defined"
|
||||||
TLeaf -> Leaf
|
TLeaf -> Leaf
|
||||||
TStem t -> Stem (evalAST env t)
|
TStem t -> Stem (evalAST env t)
|
||||||
TFork t1 t2 -> Fork (evalAST env t1) (evalAST env t2)
|
TFork t1 t2 -> Fork (evalAST env t1) (evalAST env t2)
|
||||||
SApp t1 t2 -> apply (evalAST env t1) (evalAST env t2)
|
SApp t1 t2 -> apply (evalAST env t1) (evalAST env t2)
|
||||||
SStr str -> ofString str
|
SStr str -> ofString str
|
||||||
SInt num -> ofNumber num
|
SInt num -> ofNumber num
|
||||||
SList elems -> ofList (map (evalAST Map.empty) elems)
|
SList elems -> ofList (map (evalAST Map.empty) elems)
|
||||||
SEmpty -> Leaf
|
SEmpty -> Leaf
|
||||||
SFunc name args body ->
|
SFunc name args body ->
|
||||||
error $ "Unexpected function definition " ++ name
|
error $ "Unexpected function definition " ++ name
|
||||||
++ " in evalAST; define via evalSingle."
|
++ " in evalAST; define via evalSingle."
|
||||||
SLambda {} -> error "Internal error: SLambda found in evalAST after elimination."
|
SLambda {} -> error "Internal error: SLambda found in evalAST after elimination."
|
||||||
|
|
||||||
eliminateLambda :: TricuAST -> TricuAST
|
eliminateLambda :: TricuAST -> TricuAST
|
||||||
eliminateLambda (SLambda (v:vs) body)
|
eliminateLambda (SLambda (v:vs) body)
|
||||||
@ -117,5 +120,5 @@ tS = SApp (SApp TLeaf (SApp TLeaf (SApp (SApp TLeaf TLeaf) TLeaf))) TLeaf
|
|||||||
|
|
||||||
result :: Map String T -> T
|
result :: Map String T -> T
|
||||||
result r = case Map.lookup "__result" r of
|
result r = case Map.lookup "__result" r of
|
||||||
Just a -> a
|
Just a -> a
|
||||||
Nothing -> error "No __result field found in provided environment"
|
Nothing -> error "No __result field found in provided environment"
|
||||||
|
@ -104,7 +104,6 @@ tricuLexer = do
|
|||||||
, closeBracket
|
, closeBracket
|
||||||
]
|
]
|
||||||
|
|
||||||
|
|
||||||
lexTricu :: String -> [LToken]
|
lexTricu :: String -> [LToken]
|
||||||
lexTricu input = case runParser tricuLexer "" input of
|
lexTricu input = case runParser tricuLexer "" input of
|
||||||
Left err -> error $ "Lexical error:\n" ++ errorBundlePretty err
|
Left err -> error $ "Lexical error:\n" ++ errorBundlePretty err
|
||||||
|
@ -37,7 +37,7 @@ library = evalTricu Map.empty $ parseTricu $ unlines
|
|||||||
, "emptyList = matchList true (\\y z : false)"
|
, "emptyList = matchList true (\\y z : false)"
|
||||||
, "head = matchList t (\\hd tl : hd)"
|
, "head = matchList t (\\hd tl : hd)"
|
||||||
, "tail = matchList t (\\hd tl : tl)"
|
, "tail = matchList t (\\hd tl : tl)"
|
||||||
, "listConcat = y (\\self : matchList (\\k : k) (\\h r k : pair h (self r k)))"
|
, "lconcat = y (\\self : matchList (\\k : k) (\\h r k : pair h (self r k)))"
|
||||||
, "lAnd = triage (\\x : false) (\\_ x : x) (\\_ _ x : x)"
|
, "lAnd = triage (\\x : false) (\\_ x : x) (\\_ _ x : x)"
|
||||||
, "lOr = triage (\\x : x) (\\_ _ : true) (\\_ _ x : true)"
|
, "lOr = triage (\\x : x) (\\_ _ : true) (\\_ _ x : true)"
|
||||||
, "hmap = y (\\self : matchList (\\f : t) (\\hd tl f : pair (f hd) (self tl f)))"
|
, "hmap = y (\\self : matchList (\\f : t) (\\hd tl f : pair (f hd) (self tl f)))"
|
||||||
|
54
src/Main.hs
54
src/Main.hs
@ -1,11 +1,11 @@
|
|||||||
module Main where
|
module Main where
|
||||||
|
|
||||||
import Compiler
|
import Compiler
|
||||||
import Eval (evalTricu, result)
|
import Eval (evalTricu, result, toAST)
|
||||||
import Library (library)
|
import Library (library)
|
||||||
import Parser (parseTricu)
|
import Parser (parseTricu)
|
||||||
import REPL (repl)
|
import REPL
|
||||||
import Research (T)
|
import Research
|
||||||
|
|
||||||
import Text.Megaparsec (runParser)
|
import Text.Megaparsec (runParser)
|
||||||
import System.Console.CmdArgs
|
import System.Console.CmdArgs
|
||||||
@ -14,7 +14,11 @@ import qualified Data.Map as Map
|
|||||||
|
|
||||||
data TricuArgs
|
data TricuArgs
|
||||||
= Repl
|
= Repl
|
||||||
| Compile { file :: FilePath }
|
| Compile { file :: FilePath, output :: Maybe FilePath, form :: CompiledForm }
|
||||||
|
| Decode { input :: Maybe FilePath }
|
||||||
|
deriving (Show, Data, Typeable)
|
||||||
|
|
||||||
|
data CompiledForm = TreeCalculus | AST | Ternary | Ascii
|
||||||
deriving (Show, Data, Typeable)
|
deriving (Show, Data, Typeable)
|
||||||
|
|
||||||
replMode :: TricuArgs
|
replMode :: TricuArgs
|
||||||
@ -24,14 +28,31 @@ replMode = Repl
|
|||||||
&= name "repl"
|
&= name "repl"
|
||||||
|
|
||||||
compileMode :: TricuArgs
|
compileMode :: TricuArgs
|
||||||
compileMode = Compile { file = def &= typ "FILE" &= help "Relative or absolute path to compile" }
|
compileMode = Compile
|
||||||
|
{ file = def &= typ "FILE"
|
||||||
|
&= help "Relative or absolute path to file input for compilation" &= name "f"
|
||||||
|
, output = def &= typ "OUTPUT"
|
||||||
|
&= help "Optional output file path for resulting output" &= name "o"
|
||||||
|
, form = TreeCalculus &= typ "FORM"
|
||||||
|
&= help "Output form: (tree|ast|ternary|ascii)"
|
||||||
|
&= name "t"
|
||||||
|
}
|
||||||
&= help "Compile a file and return the result of the expression in the final line"
|
&= help "Compile a file and return the result of the expression in the final line"
|
||||||
&= explicit
|
&= explicit
|
||||||
&= name "compile"
|
&= name "compile"
|
||||||
|
|
||||||
|
decodeMode :: TricuArgs
|
||||||
|
decodeMode = Decode
|
||||||
|
{ input = def &= typ "FILE"
|
||||||
|
&= help "Optional file path containing a Tree Calculus value. Defaults to stdin." &= name "f"
|
||||||
|
}
|
||||||
|
&= help "Decode a Tree Calculus value into a string representation"
|
||||||
|
&= explicit
|
||||||
|
&= name "decode"
|
||||||
|
|
||||||
main :: IO ()
|
main :: IO ()
|
||||||
main = do
|
main = do
|
||||||
args <- cmdArgs $ modes [replMode, compileMode]
|
args <- cmdArgs $ modes [replMode, compileMode, decodeMode]
|
||||||
&= help "tricu: Exploring Tree Calculus"
|
&= help "tricu: Exploring Tree Calculus"
|
||||||
&= program "tricu"
|
&= program "tricu"
|
||||||
&= summary "tricu - compiler and repl"
|
&= summary "tricu - compiler and repl"
|
||||||
@ -40,8 +61,23 @@ main = do
|
|||||||
Repl -> do
|
Repl -> do
|
||||||
putStrLn "Welcome to the tricu REPL"
|
putStrLn "Welcome to the tricu REPL"
|
||||||
putStrLn "You can exit with `CTRL+D` or the `:_exit` command.`"
|
putStrLn "You can exit with `CTRL+D` or the `:_exit` command.`"
|
||||||
repl Map.empty
|
repl library
|
||||||
Compile filePath -> do
|
Compile { file = filePath, output = maybeOutputPath, form = form } -> do
|
||||||
result <- evaluateFile filePath
|
result <- evaluateFile filePath
|
||||||
print result
|
let fRes = formatResult form result
|
||||||
|
case maybeOutputPath of
|
||||||
|
Just outputPath -> do
|
||||||
|
writeFile outputPath fRes
|
||||||
|
putStrLn $ "Output to: " ++ outputPath
|
||||||
|
Nothing -> putStr fRes
|
||||||
|
Decode { input = maybeInputPath } -> do
|
||||||
|
value <- case maybeInputPath of
|
||||||
|
Just inputPath -> readFile inputPath
|
||||||
|
Nothing -> getContents
|
||||||
|
putStrLn $ decodeResult $ result $ evalTricu library $ parseTricu value
|
||||||
|
|
||||||
|
formatResult :: CompiledForm -> T -> String
|
||||||
|
formatResult TreeCalculus = show
|
||||||
|
formatResult AST = show . toAST
|
||||||
|
formatResult Ternary = toTernaryString
|
||||||
|
formatResult Ascii = toAscii
|
||||||
|
@ -11,7 +11,8 @@ import Text.Megaparsec.Error (errorBundlePretty, ParseErrorBundle)
|
|||||||
|
|
||||||
import qualified Data.Set as Set
|
import qualified Data.Set as Set
|
||||||
|
|
||||||
type Parser = Parsec Void [LToken]
|
type Parser = Parsec Void [LToken]
|
||||||
|
type AltParser = Parsec Void String
|
||||||
|
|
||||||
data TricuAST
|
data TricuAST
|
||||||
= SVar String
|
= SVar String
|
||||||
@ -242,6 +243,42 @@ isLiteral _ = False
|
|||||||
isNewline (LNewline) = True
|
isNewline (LNewline) = True
|
||||||
isNewline _ = False
|
isNewline _ = False
|
||||||
|
|
||||||
|
-- Alternative parsers
|
||||||
|
altSC :: AltParser ()
|
||||||
|
altSC = skipMany (char ' ' <|> char '\t' <|> char '\n')
|
||||||
|
|
||||||
|
parseTernaryTerm :: AltParser TricuAST
|
||||||
|
parseTernaryTerm = do
|
||||||
|
altSC
|
||||||
|
term <- choice parseTernaryTerm'
|
||||||
|
altSC
|
||||||
|
pure term
|
||||||
|
where
|
||||||
|
parseTernaryTerm' =
|
||||||
|
[ try (between (char '(') (char ')') parseTernaryTerm)
|
||||||
|
, try parseTernaryLeaf
|
||||||
|
, try parseTernaryStem
|
||||||
|
, try parseTernaryFork
|
||||||
|
]
|
||||||
|
|
||||||
|
parseTernaryLeaf :: AltParser TricuAST
|
||||||
|
parseTernaryLeaf = char '0' *> pure TLeaf
|
||||||
|
|
||||||
|
parseTernaryStem :: AltParser TricuAST
|
||||||
|
parseTernaryStem = char '1' *> (TStem <$> parseTernaryTerm)
|
||||||
|
|
||||||
|
parseTernaryFork :: AltParser TricuAST
|
||||||
|
parseTernaryFork = do
|
||||||
|
char '2'
|
||||||
|
term1 <- parseTernaryTerm
|
||||||
|
term2 <- parseTernaryTerm
|
||||||
|
pure $ TFork term1 term2
|
||||||
|
|
||||||
|
parseTernary :: String -> Either String TricuAST
|
||||||
|
parseTernary input = case runParser (parseTernaryTerm <* eof) "" input of
|
||||||
|
Left err -> Left (errorBundlePretty err)
|
||||||
|
Right ast -> Right ast
|
||||||
|
|
||||||
-- Error Handling
|
-- Error Handling
|
||||||
handleParseError :: ParseErrorBundle [LToken] Void -> String
|
handleParseError :: ParseErrorBundle [LToken] Void -> String
|
||||||
handleParseError bundle =
|
handleParseError bundle =
|
||||||
@ -259,4 +296,3 @@ showError (FancyError offset fancy) =
|
|||||||
showError (TrivialError offset Nothing expected) =
|
showError (TrivialError offset Nothing expected) =
|
||||||
"Parse error at offset " ++ show offset ++ ": expected one of "
|
"Parse error at offset " ++ show offset ++ ": expected one of "
|
||||||
++ show (Set.toList expected)
|
++ show (Set.toList expected)
|
||||||
|
|
||||||
|
@ -28,10 +28,10 @@ repl env = runInputT defaultSettings (loop env)
|
|||||||
newEnv <- liftIO $ (processInput env input `catch` errorHandler env)
|
newEnv <- liftIO $ (processInput env input `catch` errorHandler env)
|
||||||
loop newEnv
|
loop newEnv
|
||||||
|
|
||||||
processInput :: Env -> String -> IO (Env)
|
processInput :: Env -> String -> IO Env
|
||||||
processInput env input = do
|
processInput env input = do
|
||||||
let clearEnv = Map.delete "__result" env
|
let asts = parseTricu input
|
||||||
newEnv = evalSingle clearEnv (parseSingle input)
|
newEnv = evalTricu env asts
|
||||||
case Map.lookup "__result" newEnv of
|
case Map.lookup "__result" newEnv of
|
||||||
Just r -> do
|
Just r -> do
|
||||||
putStrLn $ "tricu > " ++ show r
|
putStrLn $ "tricu > " ++ show r
|
||||||
|
@ -18,16 +18,6 @@ apply (Fork (Fork a1 a2) a3) Leaf = a1
|
|||||||
apply (Fork (Fork a1 a2) a3) (Stem u) = apply a2 u
|
apply (Fork (Fork a1 a2) a3) (Stem u) = apply a2 u
|
||||||
apply (Fork (Fork a1 a2) a3) (Fork u v) = apply (apply a3 u) v
|
apply (Fork (Fork a1 a2) a3) (Fork u v) = apply (apply a3 u) v
|
||||||
|
|
||||||
reduce :: T -> T
|
|
||||||
reduce expr =
|
|
||||||
let next = step expr
|
|
||||||
in if next == expr then expr else reduce next
|
|
||||||
|
|
||||||
step :: T -> T
|
|
||||||
step (Fork left right) = reduce (apply (reduce left) (reduce right))
|
|
||||||
step (Stem inner) = Stem (reduce inner)
|
|
||||||
step t = t
|
|
||||||
|
|
||||||
-- SKI Combinators
|
-- SKI Combinators
|
||||||
_S :: T
|
_S :: T
|
||||||
_S = Fork (Stem (Fork Leaf Leaf)) Leaf
|
_S = Fork (Stem (Fork Leaf Leaf)) Leaf
|
||||||
@ -88,6 +78,12 @@ toList (Fork x rest) = case toList rest of
|
|||||||
Left err -> Left err
|
Left err -> Left err
|
||||||
toList _ = Left "Invalid Tree Calculus list"
|
toList _ = Left "Invalid Tree Calculus list"
|
||||||
|
|
||||||
|
-- Outputs
|
||||||
|
toTernaryString :: T -> String
|
||||||
|
toTernaryString Leaf = "0"
|
||||||
|
toTernaryString (Stem t) = "1" ++ toTernaryString t
|
||||||
|
toTernaryString (Fork t1 t2) = "2" ++ toTernaryString t1 ++ toTernaryString t2
|
||||||
|
|
||||||
-- Utility
|
-- Utility
|
||||||
type Env = Map.Map String T
|
type Env = Map.Map String T
|
||||||
|
|
||||||
|
21
test/Spec.hs
21
test/Spec.hs
@ -1,12 +1,15 @@
|
|||||||
module Main where
|
module Main where
|
||||||
|
|
||||||
|
import Compiler
|
||||||
import Eval
|
import Eval
|
||||||
import Lexer
|
import Lexer
|
||||||
import Library
|
import Library
|
||||||
import Parser
|
import Parser
|
||||||
import REPL
|
import REPL
|
||||||
import Research
|
import Research
|
||||||
|
|
||||||
import Control.Exception (evaluate, try, SomeException)
|
import Control.Exception (evaluate, try, SomeException)
|
||||||
|
import Control.Monad.IO.Class (liftIO)
|
||||||
import Test.Tasty
|
import Test.Tasty
|
||||||
import Test.Tasty.HUnit
|
import Test.Tasty.HUnit
|
||||||
import Test.Tasty.QuickCheck
|
import Test.Tasty.QuickCheck
|
||||||
@ -28,6 +31,7 @@ tests = testGroup "Tricu Tests"
|
|||||||
, evaluationTests
|
, evaluationTests
|
||||||
, lambdaEvalTests
|
, lambdaEvalTests
|
||||||
, libraryTests
|
, libraryTests
|
||||||
|
, compilerTests
|
||||||
, propertyTests
|
, propertyTests
|
||||||
]
|
]
|
||||||
|
|
||||||
@ -213,7 +217,7 @@ evaluationTests = testGroup "Evaluation Tests"
|
|||||||
let input = "x = t t\nx = t\nx"
|
let input = "x = t t\nx = t\nx"
|
||||||
env = evalTricu Map.empty (parseTricu input)
|
env = evalTricu Map.empty (parseTricu input)
|
||||||
(result env) @?= Leaf
|
(result env) @?= Leaf
|
||||||
, testCase "Apply identity to Boolean Not" $ do
|
, testCase "Apply identity to Boolean Not" $ do
|
||||||
let not = "(t (t (t t) (t t t)) t)"
|
let not = "(t (t (t t) (t t t)) t)"
|
||||||
let input = "x = (\\a : a)\nx " ++ not
|
let input = "x = (\\a : a)\nx " ++ not
|
||||||
env = evalTricu Map.empty (parseTricu input)
|
env = evalTricu Map.empty (parseTricu input)
|
||||||
@ -364,7 +368,7 @@ libraryTests = testGroup "Library Tests"
|
|||||||
env = evalTricu library (parseTricu input)
|
env = evalTricu library (parseTricu input)
|
||||||
result env @?= Stem Leaf
|
result env @?= Stem Leaf
|
||||||
, testCase "Concatenate strings" $ do
|
, testCase "Concatenate strings" $ do
|
||||||
let input = "listConcat \"Hello, \" \"world!\""
|
let input = "lconcat \"Hello, \" \"world!\""
|
||||||
env = decodeResult $ result $ evalTricu library (parseTricu input)
|
env = decodeResult $ result $ evalTricu library (parseTricu input)
|
||||||
env @?= "Hello, world!"
|
env @?= "Hello, world!"
|
||||||
, testCase "Verifying Equality" $ do
|
, testCase "Verifying Equality" $ do
|
||||||
@ -373,6 +377,19 @@ libraryTests = testGroup "Library Tests"
|
|||||||
result env @?= Stem Leaf
|
result env @?= Stem Leaf
|
||||||
]
|
]
|
||||||
|
|
||||||
|
compilerTests :: TestTree
|
||||||
|
compilerTests = testGroup "Compiler tests"
|
||||||
|
[ testCase "Forks" $ do
|
||||||
|
res <- liftIO $ evaluateFile "./test/fork.tri"
|
||||||
|
res @?= Fork Leaf Leaf
|
||||||
|
, testCase "File ends with comment" $ do
|
||||||
|
res <- liftIO $ evaluateFile "./test/comments-1.tri"
|
||||||
|
res @?= Fork (Stem Leaf) Leaf
|
||||||
|
, testCase "Mapping and Equality" $ do
|
||||||
|
res <- liftIO $ evaluateFile "./test/map.tri"
|
||||||
|
res @?= Stem Leaf
|
||||||
|
]
|
||||||
|
|
||||||
propertyTests :: TestTree
|
propertyTests :: TestTree
|
||||||
propertyTests = testGroup "Property Tests"
|
propertyTests = testGroup "Property Tests"
|
||||||
[ testProperty "Lexing and parsing round-trip" $ \input ->
|
[ testProperty "Lexing and parsing round-trip" $ \input ->
|
||||||
|
1
test/ascii.tri
Normal file
1
test/ascii.tri
Normal file
@ -0,0 +1 @@
|
|||||||
|
t (t (t (t (t t) (t t t)) t) t t) t
|
9
test/comments-1.tri
Normal file
9
test/comments-1.tri
Normal file
@ -0,0 +1,9 @@
|
|||||||
|
-- This is a tricu comment!
|
||||||
|
-- t (t t) (t (t t t))
|
||||||
|
-- t (t t t) (t t)
|
||||||
|
-- x = (\a : a)
|
||||||
|
t (t t) t -- Fork (Stem Leaf) Leaf
|
||||||
|
-- t t
|
||||||
|
-- x
|
||||||
|
-- x = (\a : a)
|
||||||
|
-- t
|
1
test/fork.tri
Normal file
1
test/fork.tri
Normal file
@ -0,0 +1 @@
|
|||||||
|
t t t
|
24
test/map.tri
Normal file
24
test/map.tri
Normal file
@ -0,0 +1,24 @@
|
|||||||
|
false = t
|
||||||
|
true = t t
|
||||||
|
_ = t
|
||||||
|
k = t t
|
||||||
|
i = t (t k) t
|
||||||
|
s = t (t (k t)) t
|
||||||
|
m = s i i
|
||||||
|
b = s (k s) k
|
||||||
|
c = s (s (k s) (s (k k) s)) (k k)
|
||||||
|
iC = (\a b c : s a (k c) b)
|
||||||
|
yi = (\i : b m (c b (i m)))
|
||||||
|
y = yi iC
|
||||||
|
triage = (\a b c : t (t a b) c)
|
||||||
|
pair = t
|
||||||
|
matchList = (\oe oc : triage oe _ oc)
|
||||||
|
lconcat = y (\self : matchList (\k : k) (\h r k : pair h (self r k)))
|
||||||
|
hmap = y (\self : matchList (\f : t) (\hd tl f : pair (f hd) (self tl f)))
|
||||||
|
map = (\f l : hmap l f)
|
||||||
|
lAnd = triage (\x : false) (\_ x : x) (\_ _ x : x)
|
||||||
|
lOr = triage (\x : x) (\_ _ : true) (\_ _ x : true)
|
||||||
|
equal = y (\self : triage (triage true (\z : false) (\y z : false)) (\ax : triage false (self ax) (\y z : false)) (\ax ay : triage false (\z : false) (\bx by : lAnd (self ax bx) (self ay by))))
|
||||||
|
|
||||||
|
x = map (\i : lconcat "Successfully concatenated " i) [("two strings!")]
|
||||||
|
equal x [("Successfully concatenated two strings!")]
|
Loading…
x
Reference in New Issue
Block a user