Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_2966.v Sprache: Coq

Original von: Coq^©

(** 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.13 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.