From 6385ecf96cd60885c221e3144b5a5ec63eb5c831 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 22 Jun 2023 17:57:48 +0100 Subject: Add encodings for containers. Remove useless junk. --- src/Encoded/Arith.idr | 15 ++-- src/Encoded/Bool.idr | 10 --- src/Encoded/Container.idr | 208 ++++++++++++++++++++++++++++++++++++++++++++++ src/Encoded/Fin.idr | 5 -- src/Encoded/Pair.idr | 12 --- src/Encoded/Sum.idr | 52 ++++++------ src/Encoded/Vect.idr | 8 -- src/Term/Pretty.idr | 7 +- src/Term/Syntax.idr | 22 ++++- 9 files changed, 268 insertions(+), 71 deletions(-) create mode 100644 src/Encoded/Container.idr (limited to 'src') diff --git a/src/Encoded/Arith.idr b/src/Encoded/Arith.idr index d2f83bc..fe9bc68 100644 --- a/src/Encoded/Arith.idr +++ b/src/Encoded/Arith.idr @@ -32,10 +32,15 @@ pred = Abs' (\n => App (Rec n (Const Zero) - (Abs' (\f => - Rec (App f [ Rec k (Suc Zero) (Const Zero))) - (Const $ Abs' (\k => Rec k (Suc Zero) (Abs' Suc . shift f)))))) + (Abs $ Abs $ + let f = Var (There Here) in + let k = Var Here in + Rec k + (Lit 1) + (Const $ + Rec (App f [ App if' - [ Bool -toBool = (== 0) - export True : Term B ctx True = Lit 0 diff --git a/src/Encoded/Container.idr b/src/Encoded/Container.idr new file mode 100644 index 0000000..1334bc2 --- /dev/null +++ b/src/Encoded/Container.idr @@ -0,0 +1,208 @@ +module Encoded.Container + +import Encoded.Arith +import Encoded.Bool +import Encoded.Fin +import Encoded.Pair +import Encoded.Sum +import Encoded.Vect +import Term.Syntax + +%ambiguity_depth 4 +%prefix_record_projections off + +public export +Case : Type +Case = (Maybe Ty, Nat) + +public export +record Container where + constructor Cases + constructors : SnocList Case + {auto 0 ok : NonEmpty constructors} + +%name Container c + +public export +semCase : Case -> Ty -> Ty +semCase (Just tag, k) ty = tag * Vect k ty +semCase (Nothing, k) ty = Vect k ty + +public export +sem : Container -> Ty -> Ty +sem c ty = Sum (map (flip semCase ty) c.constructors) @{mapNonEmpty c.ok} + +unitCase : Case -> Ty +unitCase (Just tag, k) = tag +unitCase (Nothing, k) = N + +unitSem : Container -> Ty +unitSem c = Sum (map unitCase c.constructors) @{mapNonEmpty c.ok} + +dmapCase : + {c : Case} -> + {ty, ty' : Ty} -> + Term ((Fin (snd c) ~> ty ~> ty') ~> semCase c ty ~> semCase c ty') ctx +dmapCase {c = (Just tag, k)} = Abs' (\f => App (mapSnd . dmap) [ {ty : Ty} -> Term (semCase c ty ~> unitCase c) ctx +forgetCase {c = (Just tag, k)} = fst +forgetCase {c = (Nothing, k)} = Arb + +recurse : {c : Case} -> {ty : Ty} -> Term (semCase c ty ~> Vect (snd c) ty) ctx +recurse {c = (Just tag, k)} = snd +recurse {c = (Nothing, k)} = Id + +export +W : Container -> Ty +W c = N * (N ~> N * N) * (N ~> unitSem c) +-- ^ ^ ^- data +-- | + index mapping function: each index has a different base and stride +-- +- pred(fuel) for induction + +fuel : {c : Container} -> Term (W c ~> N) ctx +fuel = fst . fst + +offset : {c : Container} -> Term (W c ~> N ~> N * N) ctx +offset = snd . fst + +vals : {c : Container} -> Term (W c ~> N ~> unitSem c) ctx +vals = snd + +-- Adds a value to the start of a stream +cons : {ty : Ty} -> Term (ty ~> (N ~> ty) ~> (N ~> ty)) ctx +cons = Abs $ Abs $ Abs $ + let x = Var (There $ There Here) in + let xs = Var (There Here) in + let n = Var Here in + App rec [ + {c : Case} -> + Term (semCase c (W cont) ~> N) ctx +getFuel {c = (tag, k)} = App foldr [ Term (Fin k ~> (N ~> N * N) ~> (N ~> N * N)) ctx +stepOffset = Abs $ Abs $ Abs $ + let i = Var (There $ There Here) in + let f = Var (There Here) in + let x = Var Here in + App bimap + -- Suc is for the initial tag + [ + {c : Case} -> + Term (semCase c (W cont) ~> N ~> N * N) ctx +getOffset {c = (tag, 0)} = Const $ Const $ App pair [ + App cons + [ + let dm = App (divmod' k) [ + {c : Case} -> + (i : Elem c cont.constructors) -> + Term (semCase c (W cont) ~> N ~> unitSem cont) ctx +getVals i {c = (tag', 0)} = + Abs' (\x => Const $ App (tag @{mapNonEmpty cont.ok} (elemMap unitCase i) . forgetCase) [ + App Container.cons + [ + let dm = App (divmod' k) [ + {c : Case} -> + (i : Elem c cont.constructors) -> + Term (semCase c (W cont) ~> W cont) ctx +introCase i = Abs' (\x => + App pair [ ({x : a} -> Elem x sx -> p (f x)) -> All p (map f sx) +gtabulate {sx = [<]} g = [<] +gtabulate {sx = sx :< x} g = gtabulate (g . There) :< g Here + +export +intro : {c : Container} -> Term (sem c (W c) ~> W c) ctx +intro = + App (any @{mapNonEmpty c.ok}) {sty = map (~> W c) $ map (flip semCase (W c)) c.constructors} $ + rewrite mapFusion (~> W c) (flip semCase (W c)) c.constructors in + gtabulate introCase + +calcIndex : Term (N * N ~> N ~> N) ctx +calcIndex = Abs' (\bs => App (plus . fst) [ + {ty : Ty} -> + Term ((Fin (snd c) ~> ty) ~> (semCase c ty ~> ty) ~> unitCase c ~> ty) ctx +fillCase {c = (Just tag, k)} = Abs $ Abs $ Abs $ + let f = Var (There $ There Here) in + let sem = Var (There Here) in + let val = Var Here in + App sem [ + {ty : Ty} -> + Term + (map (\c => semCase c ty ~> ty) c.constructors ~>* + (N ~> N * N) ~> + (N ~> unitSem c) ~> + (N ~> ty) ~> + (N ~> ty)) + ctx +elimStep = AbsAll (_ :< _ :< _ :< _ :< _) + (\(fs :< offsets :< vals :< rec :< n) => + let val = App vals [ ty) (map unitCase c.constructors) :< unitSem c} $ + rewrite mapFusion (~> ty) unitCase c.constructors in + gtabulate (\i => + Syntax.App fillCase + [ semCase c ty ~> ty) i) fs + ]) :< + val) + +export +elim : + {c : Container} -> + {ty : Ty} -> + Term (map (\c => semCase c ty ~> ty) c.constructors ~>* W c ~> ty) ctx +elim = AbsAll (_ :< _) + (\(fs :< x) => + App + (Rec (App fuel [ 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 [ 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 $ diff --git a/src/Encoded/Sum.idr b/src/Encoded/Sum.idr index e3729f9..6c6da6a 100644 --- a/src/Encoded/Sum.idr +++ b/src/Encoded/Sum.idr @@ -1,13 +1,10 @@ module Encoded.Sum -import public Data.List -import public Data.List.Elem -import public Data.List.Quantifiers +import public Data.SnocList.Operations import Encoded.Bool import Encoded.Pair import Encoded.Union -import Term.Semantics import Term.Syntax -- Binary Sums ----------------------------------------------------------------- @@ -16,13 +13,6 @@ 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 [ NonEmpty (map f xs) -mapNonEmpty IsNonEmpty = IsNonEmpty +mapNonEmpty : NonEmpty sx -> NonEmpty (map f sx) +mapNonEmpty IsSnoc = IsSnoc export -Sum : (tys : List Ty) -> {auto 0 ok : NonEmpty tys} -> Ty -Sum = foldr1 (+) +Sum : (sty : SnocList Ty) -> {auto 0 ok : NonEmpty sty} -> Ty +Sum [ + {sty : SnocList 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 [ + Term (map (~> ty) sty ~>* Sum sty ~> ty) ctx +any {sty = [ + {sty : SnocList 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 + {auto 0 ok : NonEmpty sty} -> + Elem ty sty -> + Term (ty ~> Sum sty) ctx +tag {sty = [ 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 diff --git a/src/Term/Pretty.idr b/src/Term/Pretty.idr index ed2dd45..ffa88bd 100644 --- a/src/Term/Pretty.idr +++ b/src/Term/Pretty.idr @@ -50,6 +50,10 @@ public export interface Renderable (0 a : Type) where fromSyntax : Syntax -> a +export +Renderable () where + fromSyntax _ = () + export Renderable AnsiStyle where fromSyntax Bound = italic @@ -150,7 +154,6 @@ parameters (names : Stream String) prettyFullTerm : (len : Len ctx) => Prec -> FullTerm ty ctx' -> ctx' `Thins` ctx -> Doc Syntax prettyBinding : (len : Len ctx) => Prec -> Binding ty ctx' -> ctx' `Thins` ctx -> Doc Syntax prettySpline : (len : Len ctx) => Prec -> Spline ty ctx -> Doc Syntax - prettyArg : (len : Len ctx) => Term ty ctx' -> Doc Syntax prettyTerm' d (t `Over` thin) = prettyFullTerm d t thin @@ -239,7 +242,7 @@ name k = export canonicalNames : Stream String -canonicalNames = map (fastPack . name) nats +canonicalNames = map (fastPack . reverse . name) nats export prettyTerm : Renderable ann => (len : Len ctx) => Term ty ctx -> Doc ann diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr index 6a05271..211e039 100644 --- a/src/Term/Syntax.idr +++ b/src/Term/Syntax.idr @@ -23,7 +23,7 @@ Lit (S k) = Suc (Lit k) -- HOAS -infix 4 ~>* +infixr 4 ~>* public export (~>*) : SnocList Ty -> Ty -> Ty @@ -38,10 +38,28 @@ App : {sty : SnocList Ty} -> Term (sty ~>* ty) ctx -> All (flip Term ctx) sty -> App t [<] = t App t (us :< u) = App (App t us) u +export +AbsAll : + (sty : SnocList Ty) -> + (All (flip Term (ctx ++ sty)) sty -> Term ty (ctx ++ sty)) -> + Term (sty ~>* ty) ctx +AbsAll [<] f = f [<] +AbsAll (sty :< ty') f = AbsAll sty (\vars => Abs' (\x => f (mapProperty shift vars :< x))) + export (.) : {ty, ty' : Ty} -> Term (ty' ~> ty'') ctx -> Term (ty ~> ty') ctx -> Term (ty ~> ty'') ctx t . u = Abs (App (shift t) [ + {ty : Ty} -> + Term (ty ~> ty') ctx -> + Term (sty ~>* ty) ctx -> + Term (sty ~>* ty') ctx +(t .: u) {sty = [<]} = App t u +(t .: u) {sty = sty :< ty''} = Abs' (\f => shift t . f) .: u + -- Incomplete Evaluation data IsFunc : FullTerm (ty ~> ty') ctx -> Type where @@ -112,6 +130,8 @@ Rec' Zero thin u v = Just u Rec' (Suc t) thin u v = let rec = maybe (Rec (t `Over` thin) u v) id (Rec' t thin u v) in Just $ maybe (App v rec) id $ (App' 1 v rec) +Rec' t thin (Zero `Over` thin1) (Const Zero `Over` thin2) = + Just (Zero `Over` Empty) Rec' t thin u v = Nothing eval' : {ty : Ty} -> (fuel : Nat) -> (ratio : Double) -> Term ty ctx -> (Nat, Term ty ctx) -- cgit v1.2.3