Σpring

sspring.idris

data Dependency : String -> Type -> Type
  where MkDep : (name: String) -> a -> Dependency name a

DepWrapper : Type -> Type
DepWrapper t = (String ** Dependency _ t)


dep1 : Dependency "toto" Int
dep1 = MkDep "toto" 12

dep2 : Dependency "tutu" Int
dep2 = MkDep "tutu" 14

d1 : DepWrapper Int
d1 = ("toto" ** dep1)

d2 : DepWrapper Int
d2 = ("tutu" ** dep2)

deps : List (DepWrapper Int)
deps = [d1, d2]

hasName : String -> (DepWrapper Int) -> Bool
hasName s (n ** _) = s == n

findDep : String -> List (DepWrapper Int) -> Maybe (DepWrapper Int)
findDep s xs = find (hasName s) xs

myFunction : (DepWrapper Int) -> a
myFunction (_ ** (MkDep _ v)) = v


useDep : String -> Maybe Int
useDep depname =
  let actualDep = findDep depname deps
      actualRes = map myFunction actualDep
  in actualRes