similarity index 73%
rename from Computation/Eval.v
rename to src/Computation/Eval.v
index 28a00a0..7693483 100644 (file)
@@ -1,7 +1,7 @@
Require Export Computation.Termination.

-(* evaluate up to [n] computation steps *)
+(** evaluate up to [n] computation steps *)
Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
match n with
| O      => None
@@ -16,17 +16,10 @@ Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
end
end.

-Inductive Unit : Set := unit : Unit.
-
-(*
- * In theory we'd like to be able to do this (below), but it violates
- * the Prop/Set separation:
- *
- * "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."
+(** 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') =>
@@ -34,8 +27,13 @@ Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
| (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
@@ -43,3 +41,4 @@ Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=

Implicit Arguments eval [A].
Implicit Arguments bounded_eval [A].
+