
  0 | ||| Utilities for graph traversals.
  1 | module Data.Graph.Indexed.Query.Util
  2 | 
  3 | import Data.Graph.Indexed.Query.Visited
  4 | 
  5 | %default total
  6 | 
  7 | ||| Extract a value from a `Left` because we know the `Right` is
  8 | ||| uninhabited.
  9 | public export %inline
 10 | fromLeft : Either a Void -> a
 11 | fromLeft (Left v) = v
 12 | fromLeft (Right _) impossible
 13 | 
 14 | ||| Convert a binary function to one returning an `Left`
 15 | public export %inline
 16 | fleft2 : (a -> b -> c) -> a -> b -> Either c Void
 17 | fleft2 f x = Left . f x
 18 | 
 19 | ||| Convert a ternary function to one returning an `Left`
 20 | public export %inline
 21 | fleft3 : (a -> b -> c -> d) -> a -> b -> c -> Either d Void
 22 | fleft3 f x y = Left . f x y
 23 | 
 24 | ||| Internal alias for stateful functions when visiting large graphs
 25 | public export
 26 | 0 MVis : Type -> Nat -> Type -> Type
 27 | MVis t n a = MBuffer t n -> F1 t a
 28 | 
 29 | export %inline
 30 | fromLeftMVis : R1 s (Either a Void) -@ R1 s a
 31 | fromLeftMVis (x # m) = fromLeft x # m
 32 |