Add sums, vectors and arithmetic encodings.

Also define pretty printing of terms.

1 files changed, 48 insertions, 0 deletions

diff --git a/src/Encoded/Fin.idr b/src/Encoded/Fin.idr
new file mode 100644
index 0000000..901c612
--- /dev/null
+++ b/src/Encoded/Fin.idr
@@ -0,0 +1,48 @@
+module Encoded.Fin
+
+import public Data.Nat
+
+import Data.Stream
+import Encoded.Arith
+import Encoded.Pair
+import Term.Semantics
+import Term.Syntax
+
+export
+Fin : Nat -> Ty
+Fin k = N
+
+oldShow : Nat -> String
+oldShow = show
+
+export
+zero : Term (Fin (S k)) ctx
+zero = Zero
+
+export
+suc : Term (Fin k ~> Fin (S k)) ctx
+suc = Abs' Suc
+
+export
+inject : Term (Fin k ~> Fin (S k)) ctx
+inject = Id
+
+export
+absurd : {ty : Ty} -> Term (Fin 0 ~> ty) ctx
+absurd = Arb
+
+export
+induct : {ty : Ty} -> Term (Fin (S k) ~> ty ~> (Fin k * ty ~> ty) ~> ty) ctx
+induct = rec
+
+export
+forget : Term (Fin k ~> N) ctx
+forget = Id
+
+export
+allSem : (k : Nat) -> List (TypeOf (Fin k))
+allSem k = take k nats
+
+export
+divmod' : (k : Nat) -> {auto 0 ok : NonZero k} -> Term (N ~> N * Fin k) ctx
+divmod' k = Abs' (\n => App divmod [<n, Lit k])