From 0ddaf1b2c9ca66cf0ae03d2f6ad792c7885dfc32 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 21 Jun 2023 16:05:44 +0100
Subject: Add sums, vectors and arithmetic encodings.

Also define pretty printing of terms.
---
 src/Encoded/Arith.idr | 81 +++++++++++++++++++++++++++++++++++++++++++++++++++
 src/Encoded/Bool.idr  | 26 +++++++++++++++++
 src/Encoded/Fin.idr   | 48 ++++++++++++++++++++++++++++++
 src/Encoded/Pair.idr  | 41 ++++++++++++++++++++++++++
 src/Encoded/Sum.idr   | 80 ++++++++++++++++++++++++++++++++++++++++++++++++++
 src/Encoded/Union.idr |  2 ++
 src/Encoded/Vect.idr  | 66 +++++++++++++++++++++++++++++++++++++++++
 7 files changed, 344 insertions(+)
 create mode 100644 src/Encoded/Arith.idr
 create mode 100644 src/Encoded/Fin.idr
 create mode 100644 src/Encoded/Sum.idr
 create mode 100644 src/Encoded/Vect.idr

(limited to 'src/Encoded')

diff --git a/src/Encoded/Arith.idr b/src/Encoded/Arith.idr
new file mode 100644
index 0000000..d2f83bc
--- /dev/null
+++ b/src/Encoded/Arith.idr
@@ -0,0 +1,81 @@
+module Encoded.Arith
+
+import Encoded.Bool
+import Encoded.Pair
+import Term.Syntax
+
+export
+rec : {ty : Ty} -> Term (N ~> ty ~> (N * ty ~> ty) ~> ty) ctx
+rec = Abs $ Abs $ Abs $
+  let n = Var $ There $ There Here in
+  let z = Var $ There Here in
+  let s = Var Here in
+  let 
+    p : Term (N * ty) (ctx :< N :< ty :< (N * ty ~> ty))
+    p = Rec n
+      (App pair [<Zero, z])
+      (Abs' (\p =>
+        App pair
+          [<Suc (App fst [<p])
+          , App (shift s) [<p]]))
+  in
+  App snd [<p]
+
+export
+plus : Term (N ~> N ~> N) ctx
+plus = Abs' (\n => Rec n Id (Abs' (Abs' Suc .)))
+
+export
+pred : Term (N ~> N) ctx
+-- pred = Abs' (\n => App rec [<n, Zero, fst])
+pred = Abs'
+  (\n => App
+    (Rec n
+      (Const Zero)
+      (Abs' (\f =>
+        Rec (App f [<Zero])
+          (Abs' (\k => Rec k (Suc Zero) (Const Zero)))
+          (Const $ Abs' (\k => Rec k (Suc Zero) (Abs' Suc . shift f))))))
+    [<Lit 1])
+
+export
+minus : Term (N ~> N ~> N) ctx
+minus = Abs $ Abs $
+  let m = Var $ There Here in
+  let n = Var Here in
+  Rec n m pred
+
+export
+mult : Term (N ~> N ~> N) ctx
+mult = Abs' (\n =>
+  Rec n
+    (Const Zero)
+    (Abs $ Abs $
+      let f = Var $ There Here in
+      let m = Var Here in
+      App plus [<m, App f [<m]]))
+
+export
+lte : Term (N ~> N ~> B) ctx
+lte = Abs' (\m => isZero . App minus [<m])
+
+export
+equal : Term (N ~> N ~> B) ctx
+equal = Abs $ Abs $
+  let m = Var $ There Here in
+  let n = Var Here in
+  App and [<App lte [<m, n], App lte [<n, m]]
+
+export
+divmod : Term (N ~> N ~> N * N) ctx
+divmod = Abs $ Abs $
+  let n = Var (There Here) in
+  let d = Var Here in
+  Rec
+    n
+    (App pair [<Zero, Zero])
+    (Abs' (\p =>
+      App if'
+        [<App lte [<shift d, App snd [<p]]
+        , App pair [<Suc (App fst [<p]), Zero]
+        , App mapSnd [<Abs' Suc, p]]))
diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr
index d185856..11bb894 100644
--- a/src/Encoded/Bool.idr
+++ b/src/Encoded/Bool.idr
@@ -1,11 +1,21 @@
 module Encoded.Bool
 
+import Term.Semantics
 import Term.Syntax
 
 export
 B : Ty
 B = N
 
+export
+Show (TypeOf B) where
+  show 0 = "true"
+  show (S k) = "false"
+
+export
+toBool : TypeOf B -> Bool
+toBool = (== 0)
+
 export
 True : Term B ctx
 True = Lit 0
@@ -20,3 +30,19 @@ if' = Abs' (\b =>
   Rec b
     (Abs $ Const $ Var Here)
     (Const $ Const $ Abs $ Var Here))
+
+export
+and : Term (B ~> B ~> B) ctx
+and = Abs' (\b => App if' [<b, Id, Const False])
+
+export
+or : Term (B ~> B ~> B) ctx
+or = Abs' (\b => App if' [<b, Const True, Id])
+
+export
+not : Term (B ~> B) ctx
+not = Abs' (\b => App if' [<b, False, True])
+
+export
+isZero : Term (N ~> B) ctx
+isZero = Id
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])
diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
index b2a95ab..32bb06c 100644
--- a/src/Encoded/Pair.idr
+++ b/src/Encoded/Pair.idr
@@ -2,12 +2,24 @@ module Encoded.Pair
 
 import Encoded.Bool
 import Encoded.Union
+import Term.Semantics
 import Term.Syntax
 
 export
 (*) : Ty -> Ty -> Ty
 ty1 * ty2 = B ~> (ty1 <+> ty2)
 
+export
+[ShowPair]
+{ty1, ty2 : Ty} ->
+Show (TypeOf ty1) =>
+Show (TypeOf ty2) =>
+Show (TypeOf (ty1 * ty2)) where
+  show f = fastConcat
+    [ "(", show (sem prL [<] (f $ sem True [<]))
+    , ", ", show (sem prR [<] (f $ sem False [<]))
+    , ")"]
+
 export
 pair : {ty1, ty2 : Ty} -> Term (ty1 ~> ty2 ~> (ty1 * ty2)) ctx
 pair = Abs $ Abs $ Abs $
@@ -23,3 +35,32 @@ fst = Abs $ App (prL . Var Here) [<True]
 export
 snd : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty2) ctx
 snd = Abs $ App (prR . Var Here) [<False]
+
+export
+bimap :
+  {ty1, ty1', ty2, ty2' : Ty} ->
+  Term ((ty1 ~> ty1') ~> (ty2 ~> ty2') ~> ty1 * ty2 ~> ty1' * ty2') ctx
+bimap = Abs $ Abs $ Abs $ Abs $
+  let f = Var (There $ There $ There Here) in
+  let g = Var (There $ There Here) in
+  let x = Var (There $ Here) in
+  let b = Var Here in
+  App if'
+    [<b
+    , App (inL . f . prL . x) [<True]
+    , App (inR . g . prR . x) [<False]
+    ]
+
+export
+mapSnd : {ty1, ty2, ty2' : Ty} -> Term ((ty2 ~> ty2') ~> ty1 * ty2 ~> ty1 * ty2') ctx
+mapSnd = Abs $ Abs $
+  let f = Var (There Here) in
+  let x = Var Here in
+  App pair [<App fst [<x], App (f . snd) [<x]]
+
+export
+uncurry : {ty1, ty2, ty : Ty} -> Term ((ty1 ~> ty2 ~> ty) ~> ty1 * ty2 ~> ty) ctx
+uncurry = Abs $ Abs $
+  let f = Var $ There Here in
+  let p = Var Here in
+  App f [<App fst [<p], App snd [<p]]
diff --git a/src/Encoded/Sum.idr b/src/Encoded/Sum.idr
new file mode 100644
index 0000000..e3729f9
--- /dev/null
+++ b/src/Encoded/Sum.idr
@@ -0,0 +1,80 @@
+module Encoded.Sum
+
+import public Data.List
+import public Data.List.Elem
+import public Data.List.Quantifiers
+
+import Encoded.Bool
+import Encoded.Pair
+import Encoded.Union
+import Term.Semantics
+import Term.Syntax
+
+-- Binary Sums -----------------------------------------------------------------
+
+export
+(+) : Ty -> Ty -> Ty
+ty1 + ty2 = B * (ty1 <+> ty2)
+
+export
+{ty1, ty2 : Ty} -> Show (TypeOf ty1) => Show (TypeOf ty2) => Show (TypeOf (ty1 + ty2)) where
+  show p =
+    if toBool (sem fst [<] p)
+    then fastConcat ["Left (", show (sem (prL . snd) [<] p), ")"]
+    else fastConcat ["Right (", show (sem (prR . snd) [<] p), ")"]
+
+export
+left : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 + ty2)) ctx
+left = Abs' (\t => App pair [<True, App inL [<t]])
+
+export
+right : {ty1, ty2 : Ty} -> Term (ty2 ~> (ty1 + ty2)) ctx
+right = Abs' (\t => App pair [<False, App inR [<t]])
+
+export
+case' : {ty1, ty2, ty : Ty} -> Term ((ty1 + ty2) ~> (ty1 ~> ty) ~> (ty2 ~> ty) ~> ty) ctx
+case' = Abs' (\t =>
+  App if'
+    [<App fst [<t]
+    , Abs $ Const $ App (Var Here . prL . snd) [<shift t]
+    , Const $ Abs $ App (Var Here . prR . snd) [<shift t]
+    ])
+
+export
+either : {ty1, ty2, ty : Ty} -> Term ((ty1 ~> ty) ~> (ty2 ~> ty) ~> (ty1 + ty2) ~> ty) ctx
+either = Abs $ Abs $ Abs $
+  let f = Var $ There $ There Here in
+  let g = Var $ There Here in
+  let x = Var Here in
+  App case' [<x, f, g]
+
+-- N-ary Sums ------------------------------------------------------------------
+
+public export
+mapNonEmpty : NonEmpty xs -> NonEmpty (map f xs)
+mapNonEmpty IsNonEmpty = IsNonEmpty
+
+export
+Sum : (tys : List Ty) -> {auto 0 ok : NonEmpty tys} -> Ty
+Sum = foldr1 (+)
+
+export
+any :
+  {tys : List Ty} ->
+  {ty : Ty} ->
+  {auto 0 ok : NonEmpty tys} ->
+  All (\ty' => Term (ty' ~> ty) ctx) tys ->
+  Term (Sum tys ~> ty) ctx
+any [f] = f
+any (f :: fs@(_ :: _)) = App either [<f, any fs]
+
+export
+tag :
+  {tys : List Ty} ->
+  {ty : Ty} ->
+  {auto 0 ok : NonEmpty tys} ->
+  Elem ty tys ->
+  Term (ty ~> Sum tys) ctx
+tag {tys = [_]} Here = Id
+tag {tys = _ :: _ :: _} Here = left
+tag {tys = _ :: _ :: _} (There i) = right . tag i
diff --git a/src/Encoded/Union.idr b/src/Encoded/Union.idr
index 5c3b95c..00b07e7 100644
--- a/src/Encoded/Union.idr
+++ b/src/Encoded/Union.idr
@@ -2,6 +2,8 @@ module Encoded.Union
 
 import Term.Syntax
 
+-- Binary Union ----------------------------------------------------------------
+
 export
 (<+>) : Ty -> Ty -> Ty
 N <+> N = N
diff --git a/src/Encoded/Vect.idr b/src/Encoded/Vect.idr
new file mode 100644
index 0000000..a427196
--- /dev/null
+++ b/src/Encoded/Vect.idr
@@ -0,0 +1,66 @@
+module Encoded.Vect
+
+import Data.String
+
+import Encoded.Bool
+import Encoded.Pair
+import Encoded.Fin
+
+import Term.Semantics
+import Term.Syntax
+
+export
+Vect : Nat -> Ty -> Ty
+Vect k ty = Fin k ~> ty
+
+export
+[ShowVect]
+{k : Nat} ->
+Show (TypeOf ty) =>
+Show (TypeOf (Vect k ty)) where
+  show f = "[" ++ joinBy ", " (map (show . f) $ allSem k) ++ "]"
+
+export
+nil : {ty : Ty} -> Term (Vect 0 ty) ctx
+nil = absurd
+
+export
+cons : {k : Nat} -> {ty : Ty} -> Term (ty ~> Vect k ty ~> Vect (S k) ty) ctx
+cons = Abs $ Abs $ Abs $
+  let x = Var $ There $ There Here in
+  let xs = Var $ There Here in
+  let i = Var Here in
+  App induct [<i, x, App uncurry [<Abs $ Const $ App (shift xs) (Var Here)]]
+
+export
+tabulate : Term ((Fin k ~> ty) ~> Vect k ty) ctx
+tabulate = Id
+
+export
+dmap :
+  {k : Nat} ->
+  {ty1, ty2 : Ty} ->
+  Term ((Fin k ~> ty1 ~> ty2) ~> Vect k ty1 ~> Vect k ty2) ctx
+dmap =
+  Abs $ Abs $ Abs $
+    let f = Var (There $ There Here) in
+    let xs = Var (There Here) in
+    let i = Var Here in
+    App f [<i, App xs i]
+
+export
+map : {k : Nat} -> {ty1, ty2 : Ty} -> Term ((ty1 ~> ty2) ~> Vect k ty1 ~> Vect k ty2) ctx
+map = Abs' (\f => App dmap (Const f))
+
+export
+index : {k : Nat} -> {ty : Ty} -> Term (Vect k ty ~> Fin k ~> ty) ctx
+index = Id
+
+export
+foldr : {k : Nat} -> {ty, ty' : Ty} -> Term (ty' ~> (ty ~> ty' ~> ty') ~> Vect k ty ~> ty') ctx
+foldr {k = 0} = Abs $ Const $ Const $ Var Here
+foldr {k = S k} = Abs $ Abs $ Abs $
+  let z = Var (There $ There Here) in
+  let c = Var (There Here) in
+  let xs = Var Here in
+  App c [<App xs [<zero], App foldr [<z, c, xs . suc]]
-- 
cgit v1.2.3