clean up some old unused stuff
This commit is contained in:
parent
88985405ce
commit
426c138c2b
3 changed files with 5 additions and 93 deletions
|
|
@ -2,7 +2,6 @@ module Quox.Context
|
|||
|
||||
import Quox.Syntax.Shift
|
||||
import Quox.Pretty
|
||||
import public Quox.NatExtra
|
||||
|
||||
import Data.DPair
|
||||
import Data.Nat
|
||||
|
|
@ -44,14 +43,12 @@ toSnocList : Telescope tm _ _ -> SnocList (Exists tm)
|
|||
toSnocList [<] = [<]
|
||||
toSnocList (tel :< t) = toSnocList tel :< Evidence _ t
|
||||
|
||||
private
|
||||
toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
|
||||
toListAcc [<] acc = acc
|
||||
toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc)
|
||||
|
||||
export %inline
|
||||
toList : Telescope tm _ _ -> List (Exists tm)
|
||||
toList tel = toListAcc tel []
|
||||
toList tel = toListAcc tel [] where
|
||||
toListAcc : Telescope tm _ _ -> List (Exists tm) -> List (Exists tm)
|
||||
toListAcc [<] acc = acc
|
||||
toListAcc (tel :< t) acc = toListAcc tel (Evidence _ t :: acc)
|
||||
|
||||
export %inline
|
||||
toSnocList' : Telescope' a _ _ -> SnocList a
|
||||
|
|
@ -100,16 +97,6 @@ find p [<] = empty
|
|||
find p (ctx :< x) = (guard (p x) $> VZ) <|> (VS <$> find p ctx)
|
||||
|
||||
|
||||
||| a triangle of bindings. each type binding in a context counts the ues of
|
||||
||| others in its type, and all of these together form a triangle.
|
||||
public export
|
||||
Triangle : (tm : Nat -> Type) -> (len : Nat) -> Type
|
||||
Triangle = Context . Context
|
||||
|
||||
public export
|
||||
Triangle' : Type -> (len : Nat) -> Type
|
||||
Triangle' a = Context $ Context (\_ => a)
|
||||
|
||||
export
|
||||
0 telescopeLTE : Telescope _ from to -> from `LTE` to
|
||||
telescopeLTE [<] = reflexive
|
||||
|
|
@ -165,28 +152,6 @@ export %inline
|
|||
(<$) : (forall n. tm1 n) -> Telescope tm2 from to -> Telescope tm1 from to
|
||||
x <$ tel = const x <$> tel
|
||||
|
||||
export
|
||||
teleLte' : Telescope tm from to -> from `LTE'` to
|
||||
teleLte' [<] = LTERefl
|
||||
teleLte' (tel :< _) = LTESuccR (teleLte' tel)
|
||||
|
||||
|
||||
export
|
||||
tabulate : ((n : Nat) -> tm n) ->
|
||||
(from, to : Nat) -> from `LTE'` to => Telescope tm from to
|
||||
tabulate f from from @{LTERefl} = [<]
|
||||
tabulate f from (S to) @{LTESuccR _} = tabulate f from to :< f to
|
||||
|
||||
export
|
||||
tabulate0 : ((n : Nat) -> tm n) -> (n : Nat) -> Context tm n
|
||||
tabulate0 f n = tabulate f 0 n
|
||||
|
||||
|
||||
export
|
||||
pure : from `LTE'` to => a -> Telescope' a from to
|
||||
pure @{LTERefl} x = [<]
|
||||
pure @{LTESuccR _} x = pure x :< x
|
||||
|
||||
|
||||
export %inline
|
||||
zipWith : (forall n. tm1 n -> tm2 n -> tm3 n) ->
|
||||
|
|
@ -194,14 +159,6 @@ zipWith : (forall n. tm1 n -> tm2 n -> tm3 n) ->
|
|||
Telescope tm3 from to
|
||||
zipWith f tel1 tel2 = f <$> tel1 <*> tel2
|
||||
|
||||
export %inline
|
||||
zipWith3 : (forall n. tm1 n -> tm2 n -> tm3 n -> tm4 n) ->
|
||||
Telescope tm1 from to ->
|
||||
Telescope tm2 from to ->
|
||||
Telescope tm3 from to ->
|
||||
Telescope tm4 from to
|
||||
zipWith3 f tel1 tel2 tel3 = f <$> tel1 <*> tel2 <*> tel3
|
||||
|
||||
export %inline
|
||||
zipWithLazy : forall tm1, tm2, tm3.
|
||||
(forall n. tm1 n -> tm2 n -> tm3 n) ->
|
||||
|
|
@ -209,22 +166,6 @@ zipWithLazy : forall tm1, tm2, tm3.
|
|||
Telescope (\n => Lazy (tm3 n)) from to
|
||||
zipWithLazy f = zipWith $ delay .: f
|
||||
|
||||
export %inline
|
||||
zipWith3Lazy : forall tm1, tm2, tm3, tm4.
|
||||
(forall n. tm1 n -> tm2 n -> tm3 n -> tm4 n) ->
|
||||
Telescope tm1 from to ->
|
||||
Telescope tm2 from to ->
|
||||
Telescope tm3 from to ->
|
||||
Telescope (\n => Lazy (tm4 n)) from to
|
||||
zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
|
||||
|
||||
|
||||
export
|
||||
unzip : Telescope (\i => (tm1 i, tm2 i)) from to ->
|
||||
(Telescope tm1 from to, Telescope tm2 from to)
|
||||
unzip [<] = ([<], [<])
|
||||
unzip (tel :< (x, y)) = let (xs, ys) = unzip tel in (xs :< x, ys :< y)
|
||||
|
||||
|
||||
export
|
||||
lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
|
||||
|
|
@ -264,37 +205,9 @@ foldLazy : Monoid a => Telescope' (Lazy a) from to -> a
|
|||
foldLazy = foldMap force
|
||||
|
||||
|
||||
export %inline
|
||||
and : Telescope' (Lazy Bool) _ _ -> Bool
|
||||
and = force . fold @{All}
|
||||
|
||||
export %inline
|
||||
all : (forall n. tm n -> Bool) -> Telescope tm _ _ -> Bool
|
||||
all p = and . map (delay . p)
|
||||
|
||||
export %inline
|
||||
all2 : (forall n. tm n -> tm2 n -> Bool) ->
|
||||
Telescope tm from to -> Telescope tm2 from to -> Bool
|
||||
all2 p = and .: zipWithLazy p
|
||||
|
||||
|
||||
export %inline
|
||||
or : Telescope' (Lazy Bool) _ _ -> Bool
|
||||
or = force . fold @{Any}
|
||||
|
||||
export %inline
|
||||
any : (forall n. tm n -> Bool) -> Telescope tm _ _ -> Bool
|
||||
any p = or . map (delay . p)
|
||||
|
||||
export %inline
|
||||
any2 : (forall n. tm1 n -> tm2 n -> Bool) ->
|
||||
Telescope tm1 from to -> Telescope tm2 from to -> Bool
|
||||
any2 p = or .: zipWithLazy p
|
||||
|
||||
|
||||
export %inline
|
||||
(forall n. Eq (tm n)) => Eq (Telescope tm from to) where
|
||||
(==) = all2 (==)
|
||||
(==) = foldLazy @{All} .: zipWithLazy (==)
|
||||
|
||||
export %inline
|
||||
(forall n. Ord (tm n)) => Ord (Telescope tm from to) where
|
||||
|
|
|
|||
|
|
@ -1,57 +0,0 @@
|
|||
module Quox.NatExtra
|
||||
|
||||
import public Data.Nat
|
||||
import Data.Nat.Division
|
||||
import Data.SnocList
|
||||
import Data.Vect
|
||||
|
||||
%default total
|
||||
|
||||
|
||||
public export
|
||||
data LTE' : Nat -> Nat -> Type where
|
||||
LTERefl : LTE' n n
|
||||
LTESuccR : LTE' m n -> LTE' m (S n)
|
||||
%builtin Natural LTE'
|
||||
|
||||
public export %hint
|
||||
lteZero' : {n : Nat} -> LTE' 0 n
|
||||
lteZero' {n = 0} = LTERefl
|
||||
lteZero' {n = S n} = LTESuccR lteZero'
|
||||
|
||||
public export %hint
|
||||
lteSucc' : LTE' m n -> LTE' (S m) (S n)
|
||||
lteSucc' LTERefl = LTERefl
|
||||
lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p
|
||||
|
||||
public export
|
||||
fromLte : {n : Nat} -> LTE m n -> LTE' m n
|
||||
fromLte LTEZero = lteZero'
|
||||
fromLte (LTESucc p) = lteSucc' $ fromLte p
|
||||
|
||||
public export
|
||||
toLte : {n : Nat} -> m `LTE'` n -> m `LTE` n
|
||||
toLte LTERefl = reflexive
|
||||
toLte (LTESuccR p) = lteSuccRight (toLte p)
|
||||
|
||||
|
||||
private
|
||||
0 baseNZ : n `GTE` 2 => NonZero n
|
||||
baseNZ @{LTESucc _} = SIsNonZero
|
||||
|
||||
parameters {base : Nat} {auto 0 _ : base `GTE` 2} (chars : Vect base Char)
|
||||
private
|
||||
showAtBase' : List Char -> Nat -> List Char
|
||||
showAtBase' acc 0 = acc
|
||||
showAtBase' acc k =
|
||||
let dig = natToFinLT (modNatNZ k base baseNZ) @{boundModNatNZ {}} in
|
||||
showAtBase' (index dig chars :: acc)
|
||||
(assert_smaller k $ divNatNZ k base baseNZ)
|
||||
|
||||
export
|
||||
showAtBase : Nat -> String
|
||||
showAtBase = pack . showAtBase' []
|
||||
|
||||
export
|
||||
showHex : Nat -> String
|
||||
showHex = showAtBase $ fromList $ unpack "0123456789ABCDEF"
|
||||
Loading…
Add table
Add a link
Reference in a new issue