
   0 | module Data.Container.Base.Concrete.Instances
   1 | 
   2 | import Data.Fin
   3 | import Data.Vect
   4 | import Data.List
   5 | import Data.DPair
   6 | 
   7 | import Data.Container.Base.Object.Definition
   8 | import Data.Container.Base.Extension.Definition
   9 | import Data.Container.Base.Concrete.Definition
  10 | import Data.Container.Base.Object.Instances
  11 | import Data.Container.Base.Extension.Instances
  12 | 
  13 | import Data.Container.Base.TreeUtils
  14 | 
  15 | -- import public Data.Functor.Naperian
  16 | import public Data.Tree
  17 | 
  18 | import Misc
  19 | 
  20 | %hide Data.Vect.fromList
  21 | 
  22 | namespace ConversionFunctions
  23 |   public export
  24 |   toScalar : a -> Scalar' a
  25 |   toScalar a = () <| (\_ => a)
  26 | 
  27 |   public export
  28 |   extract : Scalar' a -> a
  29 |   extract (() <| f) = f ()
  30 | 
  31 |   public export
  32 |   fromMaybe : Maybe a -> Maybe' a
  33 |   fromMaybe Nothing = (False <| absurd)
  34 |   fromMaybe (Just a) = (True <| \_ => a)
  35 | 
  36 |   public export
  37 |   toMaybe : Maybe' a -> Maybe a
  38 |   toMaybe (False <| absurd) = Nothing
  39 |   toMaybe (True <| f) = Just (f ())
  40 | 
  41 |   public export
  42 |   fromList : List a -> List' a
  43 |   fromList [] = (0 <| absurd)
  44 |   fromList (x :: xs) = let (l <| c) = fromList xs
  45 |                        in (S l <| cons x c)
  46 | 
  47 |   public export
  48 |   toList : List' a -> List a
  49 |   toList (0 <| _) = []
  50 |   toList ((S k) <| ind) = head ind :: toList (k <| tail ind)
  51 |   
  52 |   public export
  53 |   fromVect : Vect n a -> Vect' n a
  54 |   fromVect v = () <| \i => index i v
  55 |   
  56 |   public export
  57 |   toVect : {n : Nat} -> Vect' n a -> Vect n a
  58 |   toVect (_ <| index) = Vect.Fin.tabulate index
  59 | 
  60 |   public export
  61 |   fromBinTreeSame : BinTreeSame a -> BinTree' a
  62 |   fromBinTreeSame (Leaf x) = LeafS <| \_ => x
  63 |   fromBinTreeSame (Node x lt rt) =
  64 |     let fblt = fromBinTreeSame lt
  65 |         fbrt = fromBinTreeSame rt
  66 |     in NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
  67 |         AtNode => x
  68 |         GoLeft posL => index fblt posL
  69 |         GoRight posR => index fbrt posR
  70 | 
  71 |   public export
  72 |   toBinTreeSame : BinTree' a -> BinTreeSame a
  73 |   toBinTreeSame (LeafS <| index) = Leaf (index AtLeaf)
  74 |   toBinTreeSame (NodeS lt rt <| index) =
  75 |     Node (index AtNode)
  76 |          (toBinTreeSame (lt <| index . GoLeft))
  77 |          (toBinTreeSame (rt <| index . GoRight))
  78 |   
  79 |   
  80 |   public export
  81 |   fromTreeHelper : BinTreePosNode LeafS -> a
  82 |   fromTreeHelper AtNode impossible
  83 |   fromTreeHelper (GoLeft x) impossible
  84 |   fromTreeHelper (GoRight x) impossible
  85 |   
  86 |   public export
  87 |   fromBinTreeNode : BinTreeNode a -> BinTreeNode' a
  88 |   fromBinTreeNode (Leaf ()) = LeafS <| fromTreeHelper
  89 |   fromBinTreeNode (Node node leftTree rightTree)
  90 |     = let fblt = fromBinTreeNode leftTree
  91 |           fbrt = fromBinTreeNode rightTree
  92 |       in (NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
  93 |             AtNode => node
  94 |             GoLeft posL => index fblt posL
  95 |             GoRight posR => index fbrt posR)
  96 | 
  97 |   public export
  98 |   toBinTreeNode : BinTreeNode' a -> BinTreeNode a
  99 |   toBinTreeNode (LeafS <| index) = Leaf ()
 100 |   toBinTreeNode (NodeS lt rt <| index) = 
 101 |     Node (index AtNode)
 102 |          (toBinTreeNode (lt <| index . GoLeft))
 103 |          (toBinTreeNode (rt <| index . GoRight))
 104 |   
 105 |   public export
 106 |   fromBinTreeLeaf : BinTreeLeaf a -> BinTreeLeaf' a
 107 |   fromBinTreeLeaf (Leaf leaf) = LeafS <| \_ => leaf
 108 |   fromBinTreeLeaf (Node node lt rt) =
 109 |     let fblt = fromBinTreeLeaf lt
 110 |         fbrt = fromBinTreeLeaf rt
 111 |     in NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
 112 |           GoLeft posL => index fblt posL
 113 |           GoRight posR => index fbrt posR
 114 | 
 115 |   public export
 116 |   toBinTreeLeaf : BinTreeLeaf' a -> BinTreeLeaf a
 117 |   toBinTreeLeaf (LeafS <| content) = Leaf (content AtLeaf)
 118 |   toBinTreeLeaf (NodeS l r <| content) =
 119 |     Node' (toBinTreeLeaf (l <| content . GoLeft))
 120 |           (toBinTreeLeaf (r <| content . GoRight))
 121 | 
 122 |   -- ||| Indexing an element of `xs` and then applying `f` to it is the same as
 123 |   -- ||| mapping `f` over xs, and then indexing the result
 124 |   -- public export
 125 |   -- mapIndexPreserve : {0 f : a -> b} ->
 126 |   --   (xs : List a) ->
 127 |   --   (i : Fin (length (f <$> xs))) ->
 128 |   --   f (index' xs (rewrite sym (lengthMap {f=f} xs) in i))
 129 |   --     = index' (f <$> xs) i
 130 |   -- mapIndexPreserve (x :: xs) FZ = Refl
 131 |   -- mapIndexPreserve (x :: xs) (FS j) = mapIndexPreserve xs j
 132 | 
 133 | 
 134 | public export
 135 | FromConcrete Scalar where
 136 |   concreteType = id
 137 |   concreteFunctor = MkFunctor id
 138 |   fromConcreteTy = pure
 139 |   toConcreteTy = extract
 140 | 
 141 | public export
 142 | FromConcrete Maybe where
 143 |   concreteType = Maybe
 144 |   concreteFunctor = %search
 145 |   fromConcreteTy = fromMaybe
 146 |   toConcreteTy = toMaybe
 147 | 
 148 | public export
 149 | FromConcrete List where
 150 |   concreteType = List
 151 |   concreteFunctor = %search -- TODO how to find the result of the search and place it here directly?
 152 |   fromConcreteTy = fromList
 153 |   toConcreteTy = toList
 154 | 
 155 | public export
 156 | {n : Nat} -> FromConcrete (Vect n) where
 157 |   concreteType = Vect n
 158 |   concreteFunctor = %search
 159 |   fromConcreteTy = fromVect
 160 |   toConcreteTy = toVect
 161 | 
 162 | public export
 163 | FromConcrete BinTree where
 164 |   concreteType = BinTreeSame
 165 |   concreteFunctor = %search
 166 |   fromConcreteTy = fromBinTreeSame
 167 |   toConcreteTy = toBinTreeSame
 168 | 
 169 | public export
 170 | FromConcrete BinTreeNode where
 171 |   concreteType = BinTreeNode
 172 |   concreteFunctor = %search
 173 |   fromConcreteTy = fromBinTreeNode
 174 |   toConcreteTy = toBinTreeNode
 175 | 
 176 | public export
 177 | FromConcrete BinTreeLeaf where
 178 |   concreteType = BinTreeLeaf
 179 |   concreteFunctor = %search
 180 |   fromConcreteTy = fromBinTreeLeaf
 181 |   toConcreteTy = toBinTreeLeaf
 182 | 
 183 |