diff options
Diffstat (limited to 'src/Encoded/Pair.idr')
| -rw-r--r-- | src/Encoded/Pair.idr | 41 |
1 files changed, 41 insertions, 0 deletions
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]] |