Computation/Eval.v

   1 Require Export Computation.Monad.
   2 Require Export Computation.Termination.
   3
   4 (* evaluate up to [n] computation steps *)
   5 Fixpoint bounded_eval (A:Set) (n:nat) (c:#A) {struct n} : option A :=
   6   match n with
   7     | O      => None
   8     | (S n') =>
   9       match c with
  10         | Return b   => Some b
  11         | Bind _ f c' =>
  12           match (bounded_eval _ n' c') with
  13             | None   => None
  14             | Some a => bounded_eval A n' (f a)
  15           end
  16       end
  17   end.
  18
  19 Inductive Unit : Set := unit : Unit.
  20
  21 (*
  22  * In theory we'd like to be able to do this (below), but it violates
  23  * the Prop/Set separation:
  24  *
  25  * "Elimination of an inductive object of sort Prop is not allowed on a
  26  *  predicate in sort Set because proofs can be eliminated only to
  27  *  build proofs."
  28  *)
  29 (*
  30 Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
  31   match t with
  32     | (Terminates_intro t') =>
  33       match t' with
  34         | (ex_intro x y) => x
  35       end
  36   end.
  37 *)
  38
  39 Definition eval (A:Set) (c:#A) (t:Terminates c) : A :=
  40   match eval' c Unit (Return unit) (termination_is_safe A c t) with
  41     | exist x pf => x
  42   end.
  43
  44 Implicit Arguments eval [A].
  45 Implicit Arguments bounded_eval [A].