<commit_before>\section{Cochon (Command-line Interface)}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators, TypeSynonymInstances #-}

> module Cochon where

> import Compiler
> import Control.Applicative
> import Control.Monad
> import Control.Monad.State
> import Data.Foldable
> import Data.List
> import Data.Traversable
> import System.IO (hFlush, stdout)

> import BwdFwd
> import Developments
> import Elaborator
> import MissingLibrary
> import Naming
> import Lexer
> import Parsley
> import PrettyPrint
> import ProofState
> import Root
> import Rooty
> import Rules
> import Tm hiding (In)
> import TmParse


%endif

Here we have a very basic command-driven interface to the proof state monad.

> cochon :: ProofContext -> IO ()
> cochon loc@(ls, dev) = do
>     let Right s = evalStateT prettyProofState loc
>     putStrLn s
>     putStr (showPrompt ls)
>     hFlush stdout
>     l <- getLine
>     case parse tokenize l of 
>         Left pf ->  putStrLn ("Tokenize failure: " ++ describePFailure pf id) 
>                     >> cochon loc
>         Right ts ->
>           case parse pCommand ts of
>               Left pf ->  putStrLn ("Parse failure: " ++ describePFailure pf (intercalate " " . map crushToken))
>                           >> cochon loc
>               Right Quit -> return ()
>               Right (Compile rn fn) -> do
>                   let  Right aus = evalStateT getAuncles loc
>                        mn = resolve aus rn
>                   case mn of
>                       Just (N (P (n := _))) -> do
>                           let  Right loc' = execStateT gimme loc
>                                Right dev = evalStateT getDev loc'
>                           compileCommand n (reverseDev' dev) fn
>                       Nothing -> putStrLn "Can't resolve." >> cochon loc
>               Right c -> case runStateT (doCommand c) loc of
>                   Right (s, loc') -> do
>                       putStrLn s 
>                       printChanges loc loc'
>                       cochon loc'
>                   Left ss ->  do
>                       putStrLn "I'm sorry, Dave. I'm afraid I can't do that."
>                       putStr (unlines ss)
>                       cochon loc

> describePFailure :: PFailure a -> ([a] -> String) -> String
> describePFailure (PFailure (ts, fail)) f = (case fail of
>     Abort        -> "parser aborted."
>     EndOfStream  -> "end of stream."
>     EndOfParser  -> "end of parser."
>     Expect t     -> "expected " ++ f [t] ++ "."
>   ) ++ (if length ts > 0
>        then ("\nSuccessfully parsed: ``" ++ f ts ++ "''.")
>        else "")

> data NavC  =  InC | OutC
>            |  Up | Down | Top | Bottom 
>            |  RootC
>            |  Prev | Next | First | Last
>     deriving Show

> data Command x  =  Apply
>                 |  Auncles
>                 |  DoneC
>                 |  Dump
>                 |  Elaborate x
>                 |  Compile x String
>                 |  Give x
>                 |  Go NavC
>                 |  Infer x
>                 |  Jump x
>                 |  Lambda String
>                 |  Make String (Maybe x :<: x)<commit_msg>Quick hack to make cochon responses appear below the development<commit_after>\section{Cochon (Command-line Interface)}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators, TypeSynonymInstances #-}

> module Cochon where

> import Compiler
> import Control.Applicative
> import Control.Monad
> import Control.Monad.State
> import Data.Foldable
> import Data.List
> import Data.Traversable
> import System.IO (hFlush, stdout)

> import BwdFwd
> import Developments
> import Elaborator
> import MissingLibrary
> import Naming
> import Lexer
> import Parsley
> import PrettyPrint
> import ProofState
> import Root
> import Rooty
> import Rules
> import Tm hiding (In)
> import TmParse


%endif

Here we have a very basic command-driven interface to the proof state monad.

> cochon :: ProofContext -> IO ()
> cochon loc = cochon' loc "Hello!"

> cochon' :: ProofContext -> String -> IO ()
> cochon' loc@(ls, dev) msg = do
>     --putStrLn (show loc)
>     let Right s = evalStateT prettyProofState loc
>     putStrLn s
>     putStrLn msg
>     putStr (showPrompt ls)
>     hFlush stdout
>     l <- getLine
>     case parse tokenize l of 
>         Left pf -> cochon' loc ("Tokenize failure: " ++ describePFailure pf id)
>         Right ts ->
>           case parse pCommand ts of
>               Left pf -> cochon' loc ("Parse failure: " ++ describePFailure pf (intercalate " " . map crushToken))
>               Right Quit -> return ()
>               Right (Compile rn fn) -> do
>                   let  Right aus = evalStateT getAuncles loc
>                        mn = resolve aus rn
>                   case mn of
>                       Just (N (P (n := _))) -> do
>                           let  Right loc' = execStateT gimme loc
>                                Right dev = evalStateT getDev loc'
>                           compileCommand n (reverseDev' dev) fn
>                           cochon' loc "Probably compiled."
>                       Nothing -> cochon' loc "Can't resolve."
>               Right c -> case runStateT (doCommand c) loc of
>                   Right (s, loc') -> do
>                       printChanges loc loc'
>                       cochon' loc' s
>                   Left ss ->
>                       cochon' loc (unlines ("I'm sorry, Dave. I'm afraid I can't do that.":ss))

> describePFailure :: PFailure a -> ([a] -> String) -> String
> describePFailure (PFailure (ts, fail)) f = (case fail of
>     Abort        -> "parser aborted."
>     EndOfStream  -> "end of stream."
>     EndOfParser  -> "end of parser."
>     Expect t     -> "expected " ++ f [t] ++ "."
>   ) ++ (if length ts > 0
>        then ("\nSuccessfully parsed: ``" ++ f ts ++ "''.")
>        else "")

> data NavC  =  InC | OutC
>            |  Up | Down | Top | Bottom 
>            |  RootC
>            |  Prev | Next | First | Last
>     deriving Show

> data Command x  =  Apply
>                 |  Auncles
>                 |  DoneC
>                 |  Dump
>                 |  Elaborate x
>                 |  Compile x String
>                 |  Give x
>                 |  Go NavC
>                 |  Infer x
>                 |  Jump x
>                 |  Lambda String
>                 |  Make String (Maybe x :<: x)
{'fraction_non_alphanumeric': 0.10553152039555007, 'fraction_numerical': 0.00030902348578491963, 'mean_word_length': 1.512810559006211, 'pattern_counts': {'":': 1, '<': 7, '<?xml version=': 0, '>': 217, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3985383', 'n_tokens_mistral': 1976, 'n_tokens_neox': 1894, 'n_words': 621}