0 | module Data.Tensor.Shape.Axis
  1 |
  2 | import Data.Vect.Quantifiers
  3 |
  4 | import Data.Container.Base
  5 | import Misc
  6 |
  7 | ||| The name for an axis is an arbitrary string
  8 | public export
  9 | AxisName : Type
 10 | AxisName = String
 11 |
 12 | ||| An axis is a container together with its name
 13 | public export
 14 | record Axis where
 15 |   constructor (~>)
 16 |   name : AxisName
 17 |   cont : Cont
 18 |
 19 | public export infixr 0 ~> -- Constructor for container-based axes
 20 | public export infixr 0 ~~> -- 'Constructor' for cubical axes
 21 |
 22 | public export
 23 | rename : Axis -> AxisName -> Axis
 24 | rename a str = str ~> a.cont
 25 |
 26 | ||| In some cases we TensorType might need to assign a default name to an axis,
 27 | ||| one which is internal and will not be exposed to the user.
 28 | ||| This is the default name for such cases
 29 | public export
 30 | TTInternalName : AxisName
 31 | TTInternalName = "__tensortype_tempaxis__"
 32 |
 33 | namespace Cubical
 34 |   ||| A "constructor" for cubical axes
 35 |   public export
 36 |   (~~>) : AxisName -> Nat -> Axis
 37 |   (~~>) axisName n = axisName ~> Vect n
 38 |
 39 |   ||| Follows the pattern of `IsCubical` from `Base.Object.Definition`
 40 |   public export
 41 |   data IsCubical : Axis -> Type where
 42 |     MkIsCubical : (name : AxisName) -> (n : Nat) -> IsCubical (name ~~> n)
 43 |
 44 |   ||| Evidence of axis cubicality -> evidence of underlying container cubicality
 45 |   public export
 46 |   toContCubical : {0 a : Axis} -> IsCubical a -> IsCubical a.cont
 47 |   toContCubical (MkIsCubical _ n) = MkIsCubical n
 48 |
 49 |   ||| Extract the dimension from IsCubical with axis implicit
 50 |   public export
 51 |   dimHelper : {0 a : Axis} -> IsCubical a -> Nat
 52 |   dimHelper (MkIsCubical _ n) = n
 53 |
 54 |   ||| Extract the dimension from an axis which we know is cubical
 55 |   public export
 56 |   dim : (0 a : Axis) -> IsCubical a => Nat
 57 |   dim _ @{ic} = dimHelper ic
 58 |
 59 |   ||| Extract the dimensions of cubical axes, with shape implicit
 60 |   public export
 61 |   dimsHelper : {0 shape : Vect r Axis} ->
 62 |     All IsCubical shape -> List Nat
 63 |   dimsHelper [] = []
 64 |   dimsHelper (ic :: ns) = dimHelper ic :: dimsHelper ns
 65 |
 66 |   ||| Extract the dimensions of cubical axes, with shape explicit
 67 |   public export
 68 |   dims : (0 shape : Vect r Axis) -> All IsCubical shape => List Nat
 69 |   dims _ @{ac} = dimsHelper ac
 70 |
 71 |   ||| Product of all the dimensions of a cubical tensors, i.e. its size
 72 |   public export
 73 |   size : (0 shape : Vect r Axis) -> (ac : All IsCubical shape) => Nat
 74 |   size shape = prod (dims shape)
 75 |
 76 | namespace Naperian
 77 |   ||| Follows the pattern of `IsNaperian` from `Base.Object.Definition`
 78 |   public export
 79 |   data IsNaperian : Axis -> Type where
 80 |     MkIsNaperian : (name : AxisName) -> (pos : Type) ->
 81 |       IsNaperian (name ~> Nap pos)
 82 |
 83 |   ||| Evidence of axis being Naperian -> evidence of container being Naperian
 84 |   %hint
 85 |   public export
 86 |   toContNaperian : {0 a : Axis} -> IsNaperian a -> IsNaperian a.cont
 87 |   toContNaperian (MkIsNaperian _ pos) = MkIsNaperian pos
 88 |   
 89 |   ||| Extract the position type from IsNaperian with axis implicit
 90 |   public export
 91 |   LogHelper : {0 a : Axis} -> IsNaperian a => Type
 92 |   LogHelper @{MkIsNaperian _ pos} = pos
 93 |
 94 |   ||| Extract the position type from an axis which we know is Naperian
 95 |   public export
 96 |   Log : (0 a : Axis) -> IsNaperian a => Type
 97 |   Log a @{inn} = LogHelper @{inn}
 98 |
 99 | namespace IsConcrete
100 |   public export
101 |   data IsConcrete : Axis -> Type where
102 |     MkIsConcrete : (name : AxisName) -> IsConcrete c -> IsConcrete (name ~> c)
103 |
104 |   public export
105 |   toContConcrete : {0 a : Axis} -> IsConcrete a -> IsConcrete a.cont
106 |   toContConcrete (MkIsConcrete _ ic) = ic