Set Implicit Arguments.
Require Export Common.
Inductive val : Type :=
| val_int : int -> val
| val_clo : var -> trm -> val
| val_err : val
with trm : Type :=
| trm_val : val -> trm
| trm_var : var -> trm
| trm_abs : var -> trm -> trm
| trm_app : trm -> trm -> trm
| trm_try : trm -> trm -> trm
| trm_raise : trm -> trm
| trm_rand : trm.
Coercion trm_val : val >-> trm.
Fixpoint subst (x:var) (v:val) (t:trm) : trm :=
let s := subst x v in
match t with
| trm_val v => t
| trm_var y => If x = y then trm_val v else t
| trm_abs y t3 => trm_abs y (If x = y then t3 else s t3)
| trm_app t1 t2 => trm_app (s t1) (s t2)
| trm_try t1 t2 => trm_try (s t1) (s t2)
| trm_raise t1 => trm_raise (s t1)
| trm_rand => t
end.
Parameter ParamDeterministic : Prop.
Module AssumeDeterministic.
Parameter Deterministic : ParamDeterministic = True.
End AssumeDeterministic.
Module BehaviorsWithoutErrors.
Inductive beh :=
| beh_ret : val -> beh
| beh_exn : val -> beh.
Coercion beh_ret : val >-> beh.
End BehaviorsWithoutErrors.
Module BehaviorsWithErrors.
Inductive beh :=
| beh_ret : val -> beh
| beh_exn : val -> beh
| beh_err : beh.
Coercion beh_ret : val >-> beh.
End BehaviorsWithErrors.
|