diff options
Diffstat (limited to 'src/Encoded')
| -rw-r--r-- | src/Encoded/Arith.idr | 81 | ||||
| -rw-r--r-- | src/Encoded/Bool.idr | 26 | ||||
| -rw-r--r-- | src/Encoded/Fin.idr | 48 | ||||
| -rw-r--r-- | src/Encoded/Pair.idr | 41 | ||||
| -rw-r--r-- | src/Encoded/Sum.idr | 80 | ||||
| -rw-r--r-- | src/Encoded/Union.idr | 2 | ||||
| -rw-r--r-- | src/Encoded/Vect.idr | 66 |
7 files changed, 344 insertions, 0 deletions
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,5 +1,6 @@ module Encoded.Bool +import Term.Semantics import Term.Syntax export @@ -7,6 +8,15 @@ 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,6 +2,7 @@ module Encoded.Pair import Encoded.Bool import Encoded.Union +import Term.Semantics import Term.Syntax export @@ -9,6 +10,17 @@ export 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 $ let t = Var (There $ There Here) in @@ -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]] |