diff options
Diffstat (limited to 'src/Total/Encoded')
| -rw-r--r-- | src/Total/Encoded/Util.idr | 444 |
1 files changed, 0 insertions, 444 deletions
diff --git a/src/Total/Encoded/Util.idr b/src/Total/Encoded/Util.idr deleted file mode 100644 index f56d1bc..0000000 --- a/src/Total/Encoded/Util.idr +++ /dev/null @@ -1,444 +0,0 @@ -module Total.Encoded.Util - -import public Data.Fin -import public Data.List1 -import public Data.List.Elem -import public Data.List.Quantifiers -import public Total.Syntax - -%prefix_record_projections off - -namespace Bool - export - B : Ty - B = N - - export - true : FullTerm B [<] - true = zero - - export - false : FullTerm B [<] - false = suc zero - - export - if' : FullTerm (B ~> ty ~> ty ~> ty) [<] - if' = abs' (S $ S $ S Z) (\b, t, f => rec b t (abs $ drop f)) - -namespace Arb - export - arb : {ty : Ty} -> FullTerm ty [<] - arb {ty = N} = zero - arb {ty = ty ~> ty'} = abs (lift arb) - -namespace Union - export - (<+>) : Ty -> Ty -> Ty - N <+> N = N - N <+> (u ~> u') = u ~> u' - (t ~> t') <+> N = t ~> t' - (t ~> t') <+> (u ~> u') = (t <+> u) ~> (t' <+> u') - - export - swap : {t, u : Ty} -> FullTerm ((t <+> u) ~> (u <+> t)) [<] - swap {t = N, u = N} = id - swap {t = N, u = u ~> u'} = id - swap {t = t ~> t', u = N} = id - swap {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop swap . f . drop swap) - - export - injL : {t, u : Ty} -> FullTerm (t ~> (t <+> u)) [<] - export - injR : {t, u : Ty} -> FullTerm (u ~> (t <+> u)) [<] - export - prjL : {t, u : Ty} -> FullTerm ((t <+> u) ~> t) [<] - export - prjR : {t, u : Ty} -> FullTerm ((t <+> u) ~> u) [<] - - injL {t = N, u = N} = id - injL {t = N, u = u ~> u'} = abs' (S $ S Z) (\n, _ => app (lift (prjR . injL)) n) - injL {t = t ~> t', u = N} = id - injL {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop injL . f . drop prjL) - - injR = swap . injL - - prjL {t = N, u = N} = id - prjL {t = N, u = u ~> u'} = abs' (S Z) (\f => app (drop (prjL . injR) . f) (drop arb)) - prjL {t = t ~> t', u = N} = id - prjL {t = t ~> t', u = u ~> u'} = abs' (S Z) (\f => drop prjL . f . drop injL) - - prjR = prjL . swap - -namespace Unit - export - Unit : Ty - Unit = N - -namespace Pair - export - (*) : Ty -> Ty -> Ty - t * u = B ~> (t <+> u) - - export - pair : {t, u : Ty} -> FullTerm (t ~> u ~> (t * u)) [<] - pair = abs' (S $ S $ S Z) - (\fst, snd, b => app' (lift if') [<b, app (lift injL) fst, app (lift injR) snd]) - - export - fst : {t, u : Ty} -> FullTerm ((t * u) ~> t) [<] - fst = abs' (S Z) (\p => app (drop prjL . p) (drop true)) - - export - snd : {t, u : Ty} -> FullTerm ((t * u) ~> u) [<] - snd = abs' (S Z) (\p => app (drop prjR . p) (drop false)) - - export - mapSnd : {t, u, v : Ty} -> FullTerm ((u ~> v) ~> (t * u) ~> (t * v)) [<] - mapSnd = abs' (S $ S Z) (\f, p => app' (lift pair) [<app (lift fst) p , app (f . lift snd) p]) - - export - Product : SnocList Ty -> Ty - Product = foldl (*) Unit - - export - pair' : {tys : SnocList Ty} -> FullTerm (tys ~>* Product tys) [<] - pair' {tys = [<]} = arb - pair' {tys = tys :< ty} = abs' (S $ S Z) (\p, t => app' (lift pair) [<p, t]) .* pair' - - export - project : {tys : SnocList Ty} -> Elem ty tys -> FullTerm (Product tys ~> ty) [<] - project {tys = tys :< ty} Here = snd - project {tys = tys :< ty} (There i) = project i . fst - - export - mapProd : - {ctx, tys, tys' : SnocList Ty} -> - {auto 0 prf : SnocList.length tys = SnocList.length tys'} -> - All (flip FullTerm ctx) (zipWith (~>) tys tys') -> - FullTerm (Product tys ~> Product tys') ctx - mapProd {tys = [<], tys' = [<]} [<] = lift id - mapProd {tys = tys :< ty, tys' = tys' :< ty', prf} (fs :< f) = - abs' (S Z) - (\p => - app' (lift pair) - [<app (drop (mapProd fs {prf = injective prf}) . lift fst) p - , app (drop f . lift snd) p - ]) - - replicate : Nat -> a -> SnocList a - replicate 0 x = [<] - replicate (S n) x = replicate n x :< x - - replicateLen : (n : Nat) -> SnocList.length (replicate n x) = n - replicateLen 0 = Refl - replicateLen (S k) = cong S (replicateLen k) - - export - Vect : Nat -> Ty -> Ty - Vect n ty = Product (replicate n ty) - - zipReplicate : - {0 f : a -> b -> c} -> - {0 p : c -> Type} -> - {n : Nat} -> - p (f x y) -> - SnocList.Quantifiers.All.All p (zipWith f (replicate n x) (replicate n y)) - zipReplicate {n = 0} z = [<] - zipReplicate {n = S k} z = zipReplicate z :< z - - export - mapVect : - {n : Nat} -> - {ty, ty' : Ty} -> - FullTerm ((ty ~> ty') ~> Vect n ty ~> Vect n ty') [<] - mapVect = - abs' (S Z) - (\f => mapProd {prf = trans (replicateLen n) (sym $ replicateLen n)} $ zipReplicate f) - - export - nil : {ty : Ty} -> FullTerm (Vect 0 ty) [<] - nil = arb - - export - cons : {n : Nat} -> {ty : Ty} -> FullTerm (ty ~> Vect n ty ~> Vect (S n) ty) [<] - cons = abs' (S $ S Z) (\t, ts => app' (lift pair) [<ts, t]) - - export - head : {n : Nat} -> {ty : Ty} -> FullTerm (Vect (S n) ty ~> ty) [<] - head = snd - - export - tail : {n : Nat} -> {ty : Ty} -> FullTerm (Vect (S n) ty ~> Vect n ty) [<] - tail = fst - - export - index : {n : Nat} -> {ty : Ty} -> (i : Fin n) -> FullTerm (Vect n ty ~> ty) [<] - index FZ = head - index (FS i) = index i . tail - - export - enumerate : (n : Nat) -> FullTerm (Vect n N) [<] - enumerate 0 = arb - enumerate (S k) = app' pair [<app' mapVect [<abs' (S Z) suc, enumerate k], zero] - -namespace Sum - export - (+) : Ty -> Ty -> Ty - t + u = B * (t <+> u) - - export - left : {t, u : Ty} -> FullTerm (t ~> (t + u)) [<] - left = abs' (S Z) (\e => app' (drop pair) [<drop true, app (drop injL) e]) - - export - right : {t, u : Ty} -> FullTerm (u ~> (t + u)) [<] - right = abs' (S Z) (\e => app' (drop pair) [<drop false, app (drop injR) e]) - - export - case' : {t, u, ty : Ty} -> FullTerm ((t + u) ~> (t ~> ty) ~> (u ~> ty) ~> ty) [<] - case' = abs' (S $ S $ S Z) - (\s, f, g => - app' (lift if') - [<app (lift fst) s - , app (f . lift (prjL . snd)) s - , app (g . lift (prjR . snd)) s]) - - export - either : {t, u, ty : Ty} -> FullTerm ((t ~> ty) ~> (u ~> ty) ~> (t + u) ~> ty) [<] - either = abs' (S $ S $ S Z) (\f, g, s => app' (lift case') [<s, f, g]) - - Sum' : Ty -> List Ty -> Ty - Sum' ty [] = ty - Sum' ty (ty' :: tys) = ty + Sum' ty' tys - - export - Sum : List1 Ty -> Ty - Sum (ty ::: tys) = Sum' ty tys - - put' : - {ty, ty' : Ty} -> - {tys : List Ty} -> - (i : Elem ty (ty' :: tys)) -> - FullTerm (ty ~> Sum' ty' tys) [<] - put' {tys = []} Here = id - put' {tys = _ :: _} Here = left - put' {tys = _ :: _} (There i) = right . put' i - - export - put : {tys : List1 Ty} -> {ty : Ty} -> (i : Elem ty (forget tys)) -> FullTerm (ty ~> Sum tys) [<] - put {tys = _ ::: _} i = put' i - - any' : - {ctx : SnocList Ty} -> - {ty, ty' : Ty} -> - {tys : List Ty} -> - All (flip FullTerm ctx . (~> ty)) (ty' :: tys) -> - FullTerm (Sum' ty' tys ~> ty) ctx - any' (t :: []) = t - any' (t :: u :: ts) = app' (lift either) [<t, any' (u :: ts)] - - export - any : - {ctx : SnocList Ty} -> - {tys : List1 Ty} -> - {ty : Ty} -> - All (flip FullTerm ctx . (~> ty)) (forget tys) -> - FullTerm (Sum tys ~> ty) ctx - any {tys = _ ::: _} = any' - -namespace Nat - export - isZero : FullTerm (N ~> B) [<] - isZero = abs' (S Z) (\m => rec m (drop true) (abs (lift false))) - - export - add : FullTerm (N ~> N ~> N) [<] - add = abs' (S $ S Z) (\m, n => rec m n (abs' (S Z) suc)) - - export - sum : {n : Nat} -> FullTerm (Vect n N ~> N) [<] - sum {n = 0} = abs zero - sum {n = S k} = abs' (S Z) - (\ns => app' (lift add) [<app (lift head) ns, app (lift (sum . tail)) ns]) - - export - pred : FullTerm (N ~> N) [<] - pred = abs' (S Z) - (\m => - app' (lift case') - [<rec m - (lift $ app left (arb {ty = Unit})) - (app' (lift either) - [<abs (lift $ app right zero) - , abs' (S Z) (\n => app (lift right) (suc n)) - ]) - , abs zero - , drop id - ]) - - export - sub : FullTerm (N ~> N ~> N) [<] - sub = abs' (S $ S Z) (\m, n => rec n m (lift pred)) - - export - le : FullTerm (N ~> N ~> B) [<] - le = abs' (S Z) (\m => lift isZero . app (lift sub) m) - - export - lt : FullTerm (N ~> N ~> B) [<] - lt = abs' (S Z) (\m => app (lift le) (suc m)) - - export - cond : - {ctx : SnocList Ty} -> - {ty : Ty} -> - List (FullTerm N ctx, FullTerm (N ~> ty) ctx) -> - FullTerm (N ~> ty) ctx - cond [] = lift arb - cond ((n, v) :: xs) = - abs' (S Z) - (\t => - app' (lift if') - [<app' (lift le) [<t, drop n] - , app (drop v) t - , app (drop $ cond xs) (app' (lift sub) [<t, drop n])]) - -namespace Data - public export - Shape : Type - Shape = (Ty, Nat) - - public export - Container : Type - Container = List1 Shape - - public export - fillShape : Shape -> Ty -> Ty - fillShape (shape, n) ty = shape * Vect n ty - - public export - fill : Container -> Ty -> Ty - fill c ty = Sum (map (flip fillShape ty) c) - - export - fix : Container -> Ty - fix c = Product [<N, N ~> N, N ~> fill c N] - -- ^ ^ ^- tags and next positions - -- | |- offset - -- |- pred (number of tags in structure) - - mapShape : - {shape : Shape} -> - {ty, ty' : Ty} -> - FullTerm ((ty ~> ty') ~> fillShape shape ty ~> fillShape shape ty') [<] - mapShape {shape = (shape, n)} = mapSnd . mapVect - - gmap : - {0 f : a -> b} -> - {0 P : a -> Type} -> - {0 Q : b -> Type} -> - ({x : a} -> P x -> Q (f x)) -> - {xs : List a} -> - All P xs -> - All Q (map f xs) - gmap f [] = [] - gmap f (px :: pxs) = f px :: gmap f pxs - - forgetMap : - (0 f : a -> b) -> - (0 xs : List1 a) -> - forget (map f xs) = map f (forget xs) - forgetMap f (head ::: tail) = Refl - - calcOffsets : - {ctx : SnocList Ty} -> - {c : Container} -> - {n : Nat} -> - (ts : FullTerm (Vect n (fix c)) ctx) -> - (acc : FullTerm N ctx) -> - List (FullTerm N ctx, FullTerm (N ~> N) ctx) - calcOffsets {n = 0} ts acc = [] - calcOffsets {n = S k} ts acc = - let hd = app (lift head) ts in - let n = app (lift $ project $ There $ There Here) hd in - let offset = app (lift $ project $ There Here) hd in - (n, app (lift add) acc . offset) :: - calcOffsets - (app (lift tail) ts) - (app' (lift add) [<suc n, acc]) - - calcData : - {ctx : SnocList Ty} -> - {c : Container} -> - {n : Nat} -> - (ts : FullTerm (Vect n (fix c)) ctx) -> - (acc : FullTerm N ctx) -> - List (FullTerm N ctx, FullTerm (N ~> fill c N) ctx) - calcData {n = 0} ts acc = [] - calcData {n = S k} ts acc = - let hd = app (lift head) ts in - let n = app (lift $ project $ There $ There Here) hd in - (n, app (lift $ project Here) hd) :: - calcData - (app (lift tail) ts) - (app' (lift add) [<suc n, acc]) - - export - intro : - {c : Container} -> - {shape : Shape} -> - Elem shape (forget c) -> - FullTerm (fillShape shape (fix c) ~> fix c) [<] - intro {shape = (shape, n)} i = abs' (S Z) - (\t => - app' (lift $ pair' {tys = [<N, N ~> N, N ~> fill c N]}) - [<app (lift (sum . app mapVect (abs' (S Z) suc . project (There $ There Here)) . snd)) t - , cond ((zero, abs' (S Z) suc) :: calcOffsets (app (lift snd) t) (suc zero)) - , cond - ( (zero, - abs - (app - (lift $ put {tys = map (flip fillShape N) c} $ - rewrite forgetMap (flip fillShape N) c in - elemMap (flip fillShape N) i) - (app' (lift mapSnd) [<abs (lift $ enumerate n), drop t]))) - :: calcData (app (lift snd) t) (suc zero) - ) - ]) - - export - elim : - {c : Container} -> - {ctx : SnocList Ty} -> - {ty : Ty} -> - All (flip FullTerm ctx . (~> ty) . flip Data.fillShape ty) (forget c) -> - FullTerm (fix c ~> ty) ctx - elim cases = abs' (S Z) - (\t => - let tags = suc (app (lift $ project $ There $ There Here) t) in - let offset = app (lift $ project $ There Here) (drop $ drop t) in - let vals = app (lift $ project $ Here) (drop $ drop t) in - app' - (rec tags - (lift arb) - (abs' (S $ S Z) (\rec, n => - app - (any {tys = map (flip fillShape N) c} - (rewrite forgetMap (flip fillShape N) c in - gmap - (\f => - drop (drop $ drop f) . - app (lift mapShape) (rec . app (lift add) (app offset n))) - cases) . - vals) - n))) - [<zero]) - - -- elim cases (#tags-1,offset,data) = - -- let - -- step : (N -> ty) -> (N -> ty) - -- step rec n = - -- case rec n of - -- i => cases(i) . mapShape (rec . (+ offset n)) - -- in - -- rec #tags arb step 0 |