Idris2Doc : 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
dataGeneral : (a : Type) -> (a -> Type) -> Type -> Type
  Syntax for a program using general recursion

Totality: total
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
already : Generalabx -> Maybex
  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