Add test driver.HEADonly-codebruijn

1 files changed, 116 insertions, 0 deletions

diff --git a/src/Encoded/Test.idr b/src/Encoded/Test.idr
new file mode 100644
index 0000000..ad6e114
--- /dev/null
+++ b/src/Encoded/Test.idr
@@ -0,0 +1,116 @@
+module Encoded.Test
+
+import Data.Stream
+import Data.String
+
+import Encoded.Arith
+import Encoded.Container
+import Encoded.Fin
+import Encoded.Pair
+import Encoded.Sum
+import Encoded.Term
+import Encoded.Vect
+
+import System
+
+import Term.Compile
+import Term.Pretty
+import Term.Syntax
+import Term.Semantics
+
+%ambiguity_depth 4
+
+-- ListC : Ty -> Container
+-- ListC ty = Cases [<(Nothing, 0), (Just ty, 1)]
+
+-- List : Ty -> Ty
+-- List = W . ListC
+
+-- nil : {ty : Ty} -> Term (List ty) ctx
+-- nil = App (intro . tag (There Here)) [<Vect.nil {ty = List ty}]
+
+-- cons : {ty : Ty} -> Term (ty ~> List ty ~> List ty) ctx
+-- cons = AbsAll [<_, _] (\[<x, xs] =>
+--   App (intro . tag @{IsSnoc} Here) [<App pair [<x, App Vect.cons [<xs, Vect.nil]]])
+
+-- sum : Term (List N ~> N) ctx
+-- sum = App (elim {c = ListC N})
+--   [<Const 0
+--   , Abs' (\x => App fst x + App index [<App snd [<x], zero])
+--   ]
+
+-- fromList' : List Nat -> Term (List N) [<List N, N ~> List N ~> List N]
+-- fromList' [] = Var (There Here)
+-- fromList' (x :: xs) = App (Var Here) [<Op (Lit x), fromList' xs]
+
+-- fromList : List Nat -> Term (List N) [<]
+-- fromList xs = App (Abs $ Abs $ fromList' xs) [<Test.nil, Test.cons]
+
+%inline
+layoutOptions : LayoutOptions
+layoutOptions = MkLayoutOptions (AvailablePerLine 213 0.5)
+
+data Mode = Color | NoColor | FastCompile | Compile | Profile
+
+%inline
+render : Len ctx => Mode -> Term ty ctx -> IO ()
+render Color t =
+  renderIO $
+  layoutSmart layoutOptions $ prettyTerm t
+render NoColor t =
+  putStrLn $
+  renderShow (layoutSmart layoutOptions $ prettyTerm {ann = ()} t) ""
+render _ t = pure ()
+
+run : Show (TypeOf ty) => Len ctx => Mode -> Term ty ctx -> All TypeOf ctx -> IO ()
+run FastCompile t args =
+  putStrLn $
+  renderShow (layoutCompact $ compileTerm {ann = ()} Run t) ""
+run Compile t args =
+  putStrLn $
+  renderShow (layoutSmart layoutOptions $ compileTerm {ann = ()} Run t) ""
+run Profile t args =
+  putStrLn $
+  renderShow (layoutSmart layoutOptions $ compileTerm {ann = ()} Profile t) ""
+run _ t args = printLn (sem t args)
+
+parseArgs : List String -> IO (Mode, Bool, Nat, Nat)
+parseArgs [_, "--color", k, n] = pure (Color, True, stringToNatOrZ k, stringToNatOrZ n)
+parseArgs [_, "--no-color", k, n] = pure (NoColor, True, stringToNatOrZ k, stringToNatOrZ n)
+parseArgs [_, "--fast-compile", k, n] = pure (FastCompile, False, stringToNatOrZ k, stringToNatOrZ n)
+parseArgs [_, "--compile", k, n] = pure (Compile, False, stringToNatOrZ k, stringToNatOrZ n)
+parseArgs [_, "--profile", k, n] = pure (Profile, False, stringToNatOrZ k, stringToNatOrZ n)
+parseArgs [_, k, n] = pure (Color, False, stringToNatOrZ k, stringToNatOrZ n)
+parseArgs _ = do putStrLn "Bad arguments"; exitFailure
+
+lit : Term (N ~> Term) ctx
+lit = Abs' (\n => Rec n Zero Suc)
+
+add : Term (N ~> N ~> Term) ctx
+add = AbsAll [<_,_] (\[<k, n] =>
+  App Rec [<App lit [<k], App lit [<n], App (Abs . Suc . Var) [<0]])
+
+AssumeNat : Eliminator N ctx
+AssumeNat =
+  MkElim
+    { var = Arb
+    , zero = 0
+    , suc = Op Suc
+    , rec = Arb
+    , abs = Arb
+    , app = Arb
+    }
+
+main : IO ()
+main = do
+  args <- getArgs
+  (mode, print, k, n) <- parseArgs args
+  let t : Term Term [<] = App add [<Op (Lit k), Op (Lit n)]
+  let t : Term Term [<] = App reduce [<4096, t]
+  if print then render mode t else pure ()
+  let t : Term N [<] = App Elim [<pack AssumeNat, t]
+  run mode t [<]
+
+  -- let ns = take n nats
+  -- let t : Term (List N) [<] = fromList ns
+  -- let t : Term N [<] = App sum [<t]