
  0 | module Data.Container.Applicative.Concrete.Instances
  1 | 
  2 | import Data.Container.Base
  3 | import Data.Container.Applicative.Object.Instances
  4 | import Data.Container.Applicative.Extension.Instances
  5 | import Data.Container.Applicative.TreeUtils
  6 | 
  7 | public export
  8 | fromRoseTreeSame : RoseTreeSame a -> RoseTree' a
  9 | fromRoseTreeSame (Leaf a) = LeafS <| \_ => a
 10 | fromRoseTreeSame (Node a rts) =
 11 |   let t = fromRoseTreeSame <$> fromList rts
 12 |   in NodeS (shapeExt <$> t) <| \case
 13 |     AtNode => a
 14 |     SubTree ps posSt =>
 15 |       let rw1 : (shapeExt t = shapeExt (shapeExt <$> t)) := sym (mapShapeExt t)
 16 |           rw2 : (shapeExt (index t (rewrite sym (mapShapeExt {f=shapeExt} t) in ps)) = index (shapeExt <$> t) ps) := mapIndexCont {c=List} {f=shapeExt} t ps
 17 |       in index
 18 |       (index t (rewrite rw1 in ps))
 19 |       (rewrite rw2 in posSt)
 20 |       -- for some reason all the explicit type annotations above are needed
 21 |       -- to convince the typechecker
 22 | 
 23 | public export
 24 | toRoseTreeSame : RoseTree' a -> RoseTreeSame a
 25 | toRoseTreeSame (LeafS <| contentAt) = Leaf (contentAt AtLeaf)
 26 | toRoseTreeSame (NodeS (len <| content) <| contentAt)
 27 |   = Node (contentAt AtNode)
 28 |          (toList $ toRoseTreeSame 
 29 |                 <$> (\i => content i <| contentAt . SubTree i)
 30 |                 <$> positionsCont)
 31 | 
 32 | 
 33 | public export
 34 | FromConcrete RoseTree where
 35 |   concreteType = RoseTreeSame
 36 |   concreteFunctor = %search
 37 |   fromConcreteTy = fromRoseTreeSame
 38 |   toConcreteTy = toRoseTreeSame
 39 |