0 | module Idrall.APIv1
  1 |
  2 | import public Idrall.Expr
  3 | import public Idrall.Value
  4 | import public Idrall.Error
  5 | import Idrall.Eval
  6 | import Idrall.Check
  7 | import Idrall.ParserNew
  8 | import Idrall.Resolve
  9 | import public Idrall.IOEither
 10 | import Idrall.Path
 11 |
 12 | import System.Directory
 13 | import Data.List
 14 | import Data.String
 15 |
 16 | -- Test Stuff
 17 |
 18 | parseWith : String -> Either String (Expr ImportStatement, Int)
 19 | parseWith = Idrall.ParserNew.parseExprNew
 20 |
 21 | public export
 22 | exprFromString : String -> IOEither Error (Expr Void)
 23 | exprFromString x = do
 24 |   x' <- mapErr (ParseError initFC) (liftEither (parseWith x))
 25 |   resolve [] Nothing (fst x')
 26 |
 27 | export
 28 | resolveFromString : Maybe FilePath -> String -> IOEither Error (Expr Void)
 29 | resolveFromString path x = do
 30 |   x' <- mapErr (ParseError initFC) (liftEither (parseWith x))
 31 |   resolve [] path (fst x')
 32 |
 33 | public export
 34 | roundTripEval : String -> IOEither Error Value
 35 | roundTripEval x = do
 36 |   x' <- exprFromString x
 37 |   liftEither (eval Empty x')
 38 |
 39 | export
 40 | roundTripCheckEval : String -> IOEither Error Value
 41 | roundTripCheckEval x = do
 42 |   x' <- exprFromString x
 43 |   _ <- liftEither (infer initCxt x')
 44 |   liftEither (eval Empty x')
 45 |
 46 | evalQuote : Expr Void -> Either Error (Expr Void)
 47 | evalQuote x = do
 48 |   v <- eval Empty x
 49 |   e <- quote [] v
 50 |   pure e
 51 |
 52 | export
 53 | roundTripEvalQuote : String -> IOEither Error (Expr Void)
 54 | roundTripEvalQuote x = do
 55 |   xE <- exprFromString x
 56 |   liftEither (evalQuote xE)
 57 |
 58 | export
 59 | roundTripCheckEvalQuote : String -> IOEither Error (Expr Void)
 60 | roundTripCheckEvalQuote x = do
 61 |   xV <- roundTripCheckEval x
 62 |   xE <- liftEither (quote [] xV)
 63 |   pure $ xE
 64 |
 65 | export
 66 | roundTripEvalQuoteConv : String -> String -> IOEither Error ()
 67 | roundTripEvalQuoteConv x y = do
 68 |   xE <- exprFromString x
 69 |   xNf <- liftEither (evalQuote xE)
 70 |   yE <- exprFromString y
 71 |   yNf <- liftEither (evalQuote yE)
 72 |   _ <- liftEither $ conv Empty !(liftEither $ eval Empty xNf) !(liftEither $ eval Empty yNf)
 73 |   pure ()
 74 |
 75 | public export
 76 | roundTripSynth : String -> IOEither Error (Expr Void, Value)
 77 | roundTripSynth x = do
 78 |   x' <- exprFromString x
 79 |   liftEither (infer initCxt x')
 80 |
 81 | export
 82 | roundTripSynthEvalQuote : String -> IOEither Error (Expr Void)
 83 | roundTripSynthEvalQuote x = do
 84 |   x' <- exprFromString x
 85 |   _ <- liftEither (infer initCxt x')
 86 |   liftEither (evalQuote x')
 87 |
 88 | public export
 89 | roundTripCheck : String -> String -> IOEither Error ()
 90 | roundTripCheck x y = do
 91 |   x' <- exprFromString x
 92 |   y' <- roundTripEval y
 93 |   _ <- liftEither (check initCxt x' y')
 94 |   pure ()
 95 |
 96 | public export
 97 | roundTripConv : String -> String -> IOEither Error ()
 98 | roundTripConv x y = do
 99 |   do x' <- roundTripEval x
100 |      y' <- roundTripEval y
101 |      _ <- liftEither $ conv Empty x' y'
102 |      pure ()
103 |
104 | public export
105 | valueFromString : String -> IOEither Error Value
106 | valueFromString x = do
107 |   _ <- roundTripSynth x
108 |   roundTripEval x
109 |
110 | public export
111 | showIOEither : Show a => Show b => IOEither a b -> IO String
112 | showIOEither (MkIOEither x) =
113 |   do x' <- x
114 |      case x' of
115 |           (Left l) => pure $ "Error: " ++ show l
116 |           (Right r) => pure $ "Success: " ++ show r
117 |
118 | public export
119 | doStuff : Show a => Show b => (String -> IOEither a b) -> String -> IO ()
120 | doStuff f x =
121 |   putStrLn !(showIOEither (f x))
122 |