AdamBrouwersHarries · October 20, 2023 18:01 · Oct 20, 2023 · Oct 20, 2023
diff --git a/isort.idr b/isort.idr
@@ -1,4 +1,4 @@
-module Linear.Reproduction
+module ISort
 
 import Data.Linear.Interface
 import Data.Linear.Notation

diff --git a/isort.idr b/isort.idr
@@ -0,0 +1,216 @@
+module Linear.Reproduction
+
+import Data.Linear.Interface
+import Data.Linear.Notation
+import Data.Linear.LNat
+import Data.Linear.LEither
+import Data.Linear.LMaybe
+import Data.Linear.LVect
+
+-- Some useful things defined for LNats
+
+-- Comparisons between linear nats
+infix 5 <@
+
+public export
+(<@) : LNat -@ LNat -@ Bool
+(<@) Zero Zero = False
+(<@) Zero (Succ y) = y `seq` True
+(<@) (Succ x) Zero = x `seq` False
+(<@) (Succ x) (Succ y) = x <@ y
+
+public export
+fromNat : Nat -> LNat
+fromNat 0 = Zero
+fromNat (S k) = Succ (fromNat k)
+
+public export
+Num LNat where
+    (+) Zero y = y
+    (+) (Succ x) y = Succ (x + y)
+
+    (*) Zero y = y
+    (*) (Succ x) y = y + (x * y)
+
+    fromInteger i = fromNat $ integerToNat i
+
+public export
+lnatToInteger : LNat -> Integer
+lnatToInteger Zero = 0
+lnatToInteger (Succ x) = 1 + lnatToInteger x
+
+prim__integerToLNat : Integer -> LNat
+prim__integerToLNat i
+  = if intToBool (prim__lte_Integer 0 i)
+      then believe_me i
+      else Zero
+
+public export
+integerToLNat : Integer -> LNat
+integerToLNat 0 = Zero -- Force evaluation and hence caching of x at compile time
+integerToLNat x
+  = if intToBool (prim__lte_Integer x 0)
+       then Zero
+       else Succ (assert_total (integerToLNat (prim__sub_Integer x 1)))
+
+
+public export
+Show LNat where
+    show n = show (the Integer (lnatToInteger n))
+
+-- Proofs about LNats
+-- LTE etc copied from the Nat implementation
+public export
+data LTE  : (1 n : LNat) -> (1 m : LNat) -> Type where
+  LTEZero : LTE Zero    right
+  LTESucc : LTE left right -> LTE (Succ left) (Succ right)
+
+public export
+GTE : LNat -@ LNat -@ Type
+GTE left right = LTE right left
+
+public export
+LT : LNat -@ LNat -@ Type
+LT left right = LTE (Succ left) right
+
+namespace LT
+  ||| LT is defined in terms of LTE which makes it annoying to use.
+  ||| This convenient view of allows us to avoid having to constantly
+  ||| perform nested matches to obtain another LT subproof instead of
+  ||| an LTE one.
+  public export
+  data View : LT m n -> Type where
+    LTZero : View (LTESucc LTEZero)
+    LTSucc : (lt : m `LT` n) -> View (LTESucc lt)
+
+  ||| Deconstruct an LT proof into either a base case or a further *LT*
+  export
+  view : (lt : LT m n) -> View lt
+  view (LTESucc LTEZero) = LTZero
+  view (LTESucc lt@(LTESucc _)) = LTSucc lt
+
+  ||| A convenient alias for trivial LT proofs
+  export
+  ltZero : Zero `LT` Succ m
+  ltZero = LTESucc LTEZero
+
+public export
+GT : LNat -@ LNat -@ Type
+GT left right = LT right left
+
+export
+succNotLTEzero : Not (LTE (Succ m) Zero)
+succNotLTEzero LTEZero impossible
+
+export
+fromLteSucc : LTE (Succ m) (Succ n) -> LTE m n
+fromLteSucc (LTESucc x) = x
+
+export
+succNotLTEpred : {x : LNat} -> Not $ LTE (Succ x) x
+succNotLTEpred {x =   Zero} prf = succNotLTEzero prf
+succNotLTEpred {x = Succ _} prf = succNotLTEpred $ fromLteSucc prf
+
+public export
+isLTE : (1 m : LNat) -> (1 n : LNat) -> Dec (LTE m n)
+isLTE Zero n = consume n `seq` Yes LTEZero
+isLTE (Succ k) Zero = consume k `seq` No succNotLTEzero
+isLTE (Succ k) (Succ j)
+    = case isLTE k j of
+           No contra => No (contra . fromLteSucc)
+           Yes prf => Yes (LTESucc prf)
+
+public export
+isLTEBool : (1 m : LNat) -> (1 n : LNat) -> Bool
+isLTEBool m n = case isLTE m n of
+                     (Yes prf) => True
+                     (No contra) => False
+
+public export
+isLT : (1 m : LNat) -> (1 n : LNat) -> Dec (LT m n)
+isLT m n = isLTE (Succ m) n
+
+public export
+isGT :  (1 m : LNat) -> (1 n : LNat) -> Dec (GT m n)
+isGT m n = isLT n m
+
+
+export
+lteSuccRight : LTE n m -> LTE n (Succ m)
+lteSuccRight LTEZero     = LTEZero
+lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)
+
+export
+lteSuccLeft : LTE (Succ n) m -> LTE n m
+lteSuccLeft (LTESucc x) = lteSuccRight x
+
+export
+lteAddRight : (n : LNat) -> LTE n (n + m)
+lteAddRight Zero = LTEZero
+lteAddRight (Succ k) {m} = LTESucc (lteAddRight {m} k)
+
+export
+notLTEImpliesGT : {a, b : LNat} -> Not (a `LTE` b) -> a `GT` b
+notLTEImpliesGT {a = Zero  }           not_z_lte_b    = absurd $ not_z_lte_b LTEZero
+notLTEImpliesGT {a = Succ a} {b = Zero  } notLTE = LTESucc LTEZero
+notLTEImpliesGT {a = Succ a} {b = Succ k} notLTE = LTESucc (notLTEImpliesGT (notLTE . LTESucc))
+
+infix 1 ##
+
+-- Dependent pair of linear and linear
+public export
+record DPairLL (t : Type) (f : t -> Type) where
+  constructor (##)
+  1 fst : t
+  1 snd : f fst
+
+public export
+isLinLTE : (1 m : LNat) -> (1 n : LNat) -> DPairLL LNat (\x => DPairLL LNat (\y => (Dec $ LTE x y, x === m, y === n)))
+isLinLTE Zero n = Zero ## (n ## (Yes LTEZero, Refl, Refl))
+isLinLTE (Succ x) Zero = (Succ x) ## (Zero ## (No succNotLTEzero, Refl, Refl))
+isLinLTE (Succ x) (Succ z) = case isLinLTE x z of
+                                  (x ## (y ## (Yes prf, Refl, Refl))) => (Succ x ## (Succ y ## (Yes (LTESucc prf), Refl, Refl)))
+                                  (x ## (y ## (No contra, Refl, Refl))) => (Succ x ## (Succ y ## (No (contra . fromLteSucc), Refl, Refl)))
+
+-- Stuff with sorted vectors.
+data LSortedVect : Nat -> LNat -> Type where
+    Nil : (1 e : LNat) -> LSortedVect 1 e
+    Cons : (1 e : LNat) -> (1 es : LSortedVect n o) -> (0 prf : LTE e o) -> LSortedVect (S n) e
+
+-- Hints for interactive editing
+%name LSortedVect xs, ys, zs, ws, es, ms
+
+Show (LSortedVect l m) where
+    show sv = "[" ++ printSortedVect sv where
+        printSortedVect : LSortedVect n e -> String
+        printSortedVect ([] e) = (show e) ++ "]"
+        printSortedVect (Cons e es prf) = (show e) ++ "," ++ printSortedVect es
+
+Show (DPairLL LNat (\m => LSortedVect l m)) where
+    show (_ ## snd) = show snd
+
+
+-- Given a proof of Not (n <= m), produce a proof of m <= n
+flipOrdContra : {n, m : LNat} -> Not (LTE n m) -> LTE m n
+flipOrdContra f = lteSuccLeft $ notLTEImpliesGT f
+
+-- Insert a new element into a sorted Vector.
+-- Returns back a vector one element longer, with either the smallest element being `x`, or remaining unchanged.
+insert : (1 x : LNat) -> (1 xs : LSortedVect l m) -> LEither (LSortedVect (S l) x) (LSortedVect (S l) m)
+insert x ([] m) = case isLinLTE x m of
+                       (x ## (m ## (Yes prf, Refl, Refl))) => Left $ Cons x (Nil m) prf
+                       (x ## (m ## (No contra, Refl, Refl))) => Right $ Cons m (Nil x) (flipOrdContra contra)
+insert x (Cons m ms p) = case isLinLTE x m of
+                                (x ## (m ## ((Yes prf), (Refl, Refl)))) => Left $ Cons x (Cons m ms p) prf
+                                (x ## (m ## ((No contra), (Refl, Refl)))) => case insert x ms of
+                                                                                  (Left ms') => Right (Cons m ms' (flipOrdContra contra))
+                                                                                  (Right ms') => Right (Cons m ms' p)
+
+isort : (xs : LVect (S n) LNat) -> DPairLL LNat (\m =>LSortedVect (S n) m)
+isort (x :: []) = (x ## Nil x)
+isort (x :: (y :: xs)) = let (m' ## sv) = isort (y :: xs) in
+    case insert x sv of
+        (Left z) => x ## z
+        (Right z) => m' ## z
+
+sortedVector = isort [41, 2, 6, 3, 7, 3, 9, 11, 13, 29]