0 | module Data.Linear.LNat
 1 |
 2 | import Data.Linear.Bifunctor
 3 | import Data.Linear.Notation
 4 | import Data.Linear.Interface
 5 |
 6 | %default total
 7 |
 8 | ||| Linear Nat
 9 | public export
10 | data LNat : Type where
11 |   Zero : LNat
12 |   Succ : LNat -@ LNat
13 |
14 | ||| Convert a linear nat to an unrestricted Nat, only usable at the type level
15 | ||| because we cannot call `S` with an argument that is expected to be used exactly once
16 | public export
17 | 0 toNat : LNat -@ Nat
18 | toNat Zero = Z
19 | toNat (Succ n) = S (toNat n)
20 |
21 | export
22 | Consumable LNat where
23 |   consume Zero = ()
24 |   consume (Succ n) = consume n
25 |
26 | export
27 | Duplicable LNat where
28 |   duplicate Zero = [Zero, Zero]
29 |   duplicate (Succ n) = Succ <$> duplicate n
30 |
31 | ||| Add two linear numbers
32 | export
33 | add : LNat -@ LNat -@ LNat
34 | add Zero x = x
35 | add (Succ v) x = Succ (add v x)
36 |
37 | ||| Multiply two linear numbers
38 | export
39 | mult : (1 n : LNat) -> (0 l : LNat) -> {auto 1 ls : toNat n `Copies` l} -> LNat
40 | mult Zero x {ls = []} = Zero
41 | mult (Succ v) x {ls = x :: ls} = add x (mult {ls} v x)
42 |
43 | ||| Square a linear number
44 | export
45 | square : (1 v : LNat) -> {auto 1 vs : toNat v `Copies` v} -> LNat
46 | square v {vs} = mult {ls = vs} v v
47 |