tobast/mpri-funcprog-project
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Remove marks in Coq files.

Browse source
This commit is contained in:
François Pottier 2017-09-28 15:15:51 +02:00
parent b69e9ec88f
commit 548479586f
2 changed files with 1 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
coq/LambdaCalculusBigStep.v
View file

@ -121,7 +121,7 @@ Qed.
(* In conclusion, we have the following equivalence: *) (* In conclusion, we have the following equivalence: *)
Theorem star_cbv_bigcbv_eq: Lemma star_cbv_bigcbv_eq:
forall t v, forall t v,
(star cbv t v /\ is_value v) <-> bigcbv t v. (star cbv t v /\ is_value v) <-> bigcbv t v.
Proof. Proof.
@ -141,13 +141,11 @@ Qed.
(* We break the mutual induction between [cvalue] and [cenv] by inlining the (* We break the mutual induction between [cvalue] and [cenv] by inlining the
definition of [cenv] into the definition of [cvalue]. *) definition of [cenv] into the definition of [cvalue]. *)
(* CVALUE *)
Inductive cvalue := Inductive cvalue :=
| Clo: {bind term} -> list cvalue -> cvalue. | Clo: {bind term} -> list cvalue -> cvalue.
Definition cenv := Definition cenv :=
list cvalue. list cvalue.
(* CVALUE *)
(* This dummy cvalue is passed below as an argument to [nth], but is really (* This dummy cvalue is passed below as an argument to [nth], but is really
irrelevant, as the condition [x < length e] ensures that the dummy cvalue irrelevant, as the condition [x < length e] ensures that the dummy cvalue

8
coq/LambdaCalculusInterpreter.v
View file

@ -21,7 +21,6 @@ Require Import LambdaCalculusBigStep.
evaluation diverges. (Exercise: exhibit a term that reduces to itself evaluation diverges. (Exercise: exhibit a term that reduces to itself
in one or more reduction steps. Prove in Coq that this is the case.) *) in one or more reduction steps. Prove in Coq that this is the case.) *)
(* FAILINTERPRET *)
Fail Fixpoint interpret (e : cenv) (t : term) : cvalue := Fail Fixpoint interpret (e : cenv) (t : term) : cvalue :=
match t with match t with
| Var x => | Var x =>
@ -35,13 +34,10 @@ Fail Fixpoint interpret (e : cenv) (t : term) : cvalue :=
match cv1 with Clo u1 e' => match cv1 with Clo u1 e' =>
interpret (cv2 :: e') u1 interpret (cv2 :: e') u1
end end
(* FAILINTERPRET *)
| Let t1 t2 => | Let t1 t2 =>
let cv1 := interpret e t1 in let cv1 := interpret e t1 in
interpret (cv1 :: e) t2 interpret (cv1 :: e) t2
(* FAILINTERPRET *)
end. end.
(* FAILINTERPRET *)
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
@ -62,7 +58,6 @@ Fail Fixpoint interpret (e : cenv) (t : term) : cvalue :=
[interpret] by well-founded recursion. This can be done in Coq but is more [interpret] by well-founded recursion. This can be done in Coq but is more
complicated, so (here) not worth the trouble. *) complicated, so (here) not worth the trouble. *)
(* FIXINTERPRET *)
Fixpoint interpret (n : nat) e t : option cvalue := Fixpoint interpret (n : nat) e t : option cvalue :=
match n with match n with
| 0 => None (* not enough fuel *) | 0 => None (* not enough fuel *)
@ -76,13 +71,10 @@ Fixpoint interpret (n : nat) e t : option cvalue :=
match cv1 with Clo u1 e' => match cv1 with Clo u1 e' =>
interpret n (cv2 :: e') u1 interpret n (cv2 :: e') u1
end end
(* FIXINTERPRET *)
| Let t1 t2 => | Let t1 t2 =>
interpret n e t1 >>= fun cv1 => interpret n e t1 >>= fun cv1 =>
interpret n (cv1 :: e) t2 interpret n (cv1 :: e) t2
(* FIXINTERPRET *)
end end. end end.
(* FIXINTERPRET *)
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)