|
(** Non-termination and state monad with extraction *)
Require Import List.
Set Implicit Arguments.
Set Asymmetric Patterns.
Module MemSig.
Definition t: Type := list Type.
Definition Nth (sig: t) (n: nat) :=
nth n sig unit.
End MemSig.
(** A memory of type [Mem.t s] is the union of cells whose type is specified
by [s]. *)
Module Mem.
Inductive t: MemSig.t -> Type :=
| Nil: t nil
| Cons: forall (T: Type), option T -> forall (sig: MemSig.t), t sig ->
t (T :: sig).
End Mem.
Module Ref.
Inductive t (sig: MemSig.t) (T: Type): Type :=
| Input: t sig T.
Definition Read (sig: MemSig.t) (T: Type) (ref: t sig T) (s: Mem.t sig)
: option T :=
match ref with
| Input => None
end.
End Ref.
Module Monad.
Definition t (sig: MemSig.t) (A: Type) :=
Mem.t sig -> option A * Mem.t sig.
Definition Return (sig: MemSig.t) (A: Type) (x: A): t sig A :=
fun s =>
(Some x, s).
Definition Bind (sig: MemSig.t) (A B: Type) (x: t sig A) (f: A -> t sig B)
: t sig B :=
fun s =>
match x s with
| (Some x', s') => f x' s'
| (None, s') => (None, s')
end.
Definition Select (T: Type) (f g: unit -> T): T :=
f tt.
(** Read in a reference. *)
Definition Read (sig: MemSig.t) (T: Type) (ref: Ref.t sig T)
: t sig T :=
fun s =>
match Ref.Read ref s with
| None => (None, s)
| Some x => (Some x, s)
end.
End Monad.
Import Monad.
Definition pop (sig: MemSig.t) (T: Type) (trace: Ref.t sig (list T))
: Monad.t sig T :=
Bind (Read trace) (fun _ s => (None, s)).
Definition sig: MemSig.t := (list nat: Type) :: nil.
Definition trace: Ref.t sig (list nat).
Admitted.
Definition Gre (sig: MemSig.t) (trace: _)
(f: bool -> bool): Monad.t sig nat :=
Select (fun _ => pop trace) (fun _ => Return 0).
Definition Arg :=
Gre trace (fun _ => false).
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
