Std.ProofDirectedExtraction

A deliberately small proof-directed data pipeline.

Accepted(shape) stores data together with erased evidence for the indexed constructor that accepted it. Once the package exists, extract is total: matching the package refines the result of Sem, so there is no runtime validation branch and no Option in the accepted path.

Types

type Shape = NumberShape | FlagShape

Functions

# fn Sem(shape: Shape) -> Type
# fn accepted_flag_example() -> Accepted(FlagShape())
# fn accepted_number_example() -> Accepted(NumberShape())
# fn contextual_example() -> AcceptedRemainder(Cons('a', Cons('b', Nil())), Cons('b', Nil()))
# fn contextual_remainder_example() -> List(Char)
# fn extract(shape: Shape, accepted: Accepted(shape)) -> Sem(shape)
# fn extract_flag_example() -> Bool
# fn extract_number_example() -> Int
# fn remainder(original: List(Char), rest: List(Char), accepted: AcceptedRemainder(original, rest)) -> List(Char)

Types

Functions

# fn Sem(shape: Shape) -> Type

# fn accepted_flag_example() -> Accepted(FlagShape())

# fn accepted_number_example() -> Accepted(NumberShape())

# fn contextual_example() -> AcceptedRemainder(Cons('a', Cons('b', Nil())), Cons('b', Nil()))

# fn contextual_remainder_example() -> List(Char)

# fn extract(shape: Shape, accepted: Accepted(shape)) -> Sem(shape)

# fn extract_flag_example() -> Bool

# fn extract_number_example() -> Int

# fn remainder(original: List(Char), rest: List(Char), accepted: AcceptedRemainder(original, rest)) -> List(Char)