X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=blobdiff_plain;f=src%2FComputation%2FEval.v;fp=src%2FComputation%2FEval.v;h=76934831c00083c7f70343bc042ba1b01b0fc7ce;hp=0000000000000000000000000000000000000000;hb=1ff31872c2b89ffb4c6c6250b1d51436b6b1400f;hpb=bb471fbb694313a6aa61816752bd179b3af6711d

diff --git a/src/Computation/Eval.v b/src/Computation/Eval.v
new file mode 100644
index 0000000..7693483
--- /dev/null
+++ b/src/Computation/Eval.v
@@ -0,0 +1,44 @@
+Require Export Computation.Monad.
+Require Export Computation.Termination.
+
+(** evaluate up to [n] computation steps *)
+Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
+  match n with
+    | O      => None
+    | (S n') =>
+      match c with
+        | Return b   => Some b
+        | Bind _ f c' =>
+          match (bounded_eval _ n' c') with
+            | None   => None
+            | Some a => bounded_eval A n' (f a)
+          end
+      end
+  end.
+
+(** In theory we'd like to be able to do this (below), but it violates the Prop/Set separation.
+ *)
+(**
+<<
+Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
+  match t with
+    | (Terminates_intro t') =>
+      match t' with
+        | (ex_intro x y) => x
+      end
+  end.
+ 
+ "Elimination of an inductive object of sort Prop is not allowed on a
+  predicate in sort Set because proofs can be eliminated only to
+  build proofs."
+>>*)
+
+Inductive Unit : Set := unit : Unit.
+Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
+  match eval' c Unit (Return unit) (termination_is_safe A c t) with
+    | exist x pf => x
+  end.
+
+Implicit Arguments eval [A].
+Implicit Arguments bounded_eval [A].
+