ExtLib.Data.Monads.FuelMonad
Require Import ExtLib.Structures.Monads.
Require Import BinPos.
Set Implicit Arguments.
Set Strict Implicit.
Inductive FixResult (T : Type) :=
| Term : T -> FixResult T
| Diverge : FixResult T.
Arguments Diverge {_}.
Arguments Term {_} _.
Require Import BinPos.
Set Implicit Arguments.
Set Strict Implicit.
Inductive FixResult (T : Type) :=
| Term : T -> FixResult T
| Diverge : FixResult T.
Arguments Diverge {_}.
Arguments Term {_} _.
The GFix monad is like monad fix except that
it encapsulates the "gas" that is used as the measure
This is essentially ReaderT (optionT m))
Inductive GFix (T : Type) : Type := mkGFix
{ runGFix : N -> FixResult T }.
Global Instance MonadFix_GFix : MonadFix GFix :=
{ mfix := fun T U f v => mkGFix (fun n : N =>
match n with
| N0 => Diverge
| Npos g =>
let F := fix rec (acc : T -> FixResult U) (gas : positive) (x : T)
: FixResult U :=
match gas return FixResult U with
| xI p =>
runGFix (f (fun x => mkGFix (fun n => rec (fun x => rec acc p x) p x)) x) n
| xO p =>
rec (fun x => rec acc p x) p x
| xH => runGFix (f (fun x => mkGFix (fun _ => acc x)) x) n
end
in F (fun x => runGFix (f (fun _ => mkGFix (fun _ => Diverge)) x) n) g v
end)
}.
Global Instance Monad_GFix : Monad GFix :=
{ ret := fun _ v => mkGFix (fun _ => Term v)
; bind := fun _ _ c1 c2 =>
mkGFix (fun gas =>
match runGFix c1 gas with
| Diverge => Diverge
| Term v => runGFix (c2 v) gas
end)
}.
End gfix.
{ runGFix : N -> FixResult T }.
Global Instance MonadFix_GFix : MonadFix GFix :=
{ mfix := fun T U f v => mkGFix (fun n : N =>
match n with
| N0 => Diverge
| Npos g =>
let F := fix rec (acc : T -> FixResult U) (gas : positive) (x : T)
: FixResult U :=
match gas return FixResult U with
| xI p =>
runGFix (f (fun x => mkGFix (fun n => rec (fun x => rec acc p x) p x)) x) n
| xO p =>
rec (fun x => rec acc p x) p x
| xH => runGFix (f (fun x => mkGFix (fun _ => acc x)) x) n
end
in F (fun x => runGFix (f (fun _ => mkGFix (fun _ => Diverge)) x) n) g v
end)
}.
Global Instance Monad_GFix : Monad GFix :=
{ ret := fun _ v => mkGFix (fun _ => Term v)
; bind := fun _ _ c1 c2 =>
mkGFix (fun gas =>
match runGFix c1 gas with
| Diverge => Diverge
| Term v => runGFix (c2 v) gas
end)
}.
End gfix.
Demo
Require Import ExtLib.Data.Monads.IdentityMonad.
Definition foo : nat -> GFix ident nat :=
mfix (fun recur n =>
match n with
| 0 => ret 0
| S n => recur n
end).
Eval compute in runGFix (foo 10) 100000000000000000000000.