Idris2Doc : Data.Recursion.Free

# Data.Recursion.Free

```Module partially based on McBride's paper:
Turing-Completeness Totally Free

It gives us a type to describe computation using general recursion
and functions to run these computations for a while or to completion
if we are able to prove them total.

The content of the Erased section is new. Instead of producing the
domain/evaluation pair by computing a Dybjer-Setzer code we build a
specialised structure that allows us to make the domain proof runtime
irrelevant.```
dataGeneral : (a : Type) -> (a -> Type) -> Type -> Type
`  Syntax for a program using general recursion`

Totality: total
Constructors:
Tell : x -> Generalabx
`  We can return a value without performing any recursive call.`
Ask : (i : a) -> (bi -> Generalabx) -> Generalabx
`  Or we can pick an input and ask an oracle to give us a return value  for it. The second argument is a continuation explaining what we want  to do with the returned value.`
PiG : (a : Type) -> (a -> Type) -> Type
`  Type of functions using general recursion`

Totality: total
`  Check whehther we are ready to return a value`

Totality: total
bind : Generalabx -> (x -> Generalaby) -> Generalaby
`  Monadic bind (defined outside of the interface to be able to use it for  map and (<*>)).`

Totality: total
call : PiGab
`  Perform a recursive call and return the value provided by the oracle.`

Totality: total
engine : PiGab -> Nat -> Generalabx -> Generalabx
`  Recursively call expand a set number of times.`

Totality: total
expand : PiGab -> Generalabx -> Generalabx
`  Use a function using general recursion to expand all of the oracle calls.`

Totality: total
fold : (x -> y) -> ((i : a) -> (bi -> y) -> y) -> Generalabx -> y
`  Recursor for General`

Totality: total
late : PiGab -> Generalabx -> Latex
`  Rely on an oracle using general recursion to convert a function using  general recursion into a process returning a value in the (distant) future.`

Totality: total
lazy : PiGab -> (i : a) -> Late (bi)
`  Interpret a function using general recursion as a process returning  a value in the (distant) future.`

Totality: total
monadMorphism : Monadm => ((i : a) -> m (bi)) -> Generalabx -> mx
`  Given a monadic oracle we can give a monad morphism interpreting a  function using general recursion as a monadic process.`

Totality: total
petrol : PiGab -> Nat -> (i : a) -> Maybe (bi)
`  Check whether recursively calling expand a set number of times is enough  to produce a value.`

Totality: total