pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

One more redaction from Interpreters_template

Browse source
This commit is contained in:
Adam Chlipala 2016-02-07 14:42:34 -05:00
parent 901cacd35a
commit 9720a6e0c6
1 changed files with 3 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
Interpreters_template.v
View file

@ -304,22 +304,6 @@ Qed.
* counts. That is, we can duplicate the loop body instead of using an explicit * counts. That is, we can duplicate the loop body instead of using an explicit
* loop. *) * loop. *)
Fixpoint seqself (c : cmd) (n : nat) : cmd :=
match n with
| O => Skip
| S n' => Sequence c (seqself c n')
end.
Fixpoint unroll (c : cmd) : cmd :=
match c with
| Skip => c
| Assign _ _ => c
| Sequence c1 c2 => Sequence (unroll c1) (unroll c2)
| Repeat (Const n) c1 => seqself (unroll c1) n
(* ^-- the crucial case! *)
| Repeat e c1 => Repeat e (unroll c1)
end.
(* This obvious-sounding fact will come in handy: self-composition gives the (* This obvious-sounding fact will come in handy: self-composition gives the
* same result, when passed two functions that map equal inputs to equal * same result, when passed two functions that map equal inputs to equal
* outputs. *) * outputs. *)
@ -334,7 +318,7 @@ Proof.
trivial. trivial.
Qed. Qed.
Theorem unroll_ok : forall c v, exec (unroll c) v = exec c v. (*Theorem unroll_ok : forall c v, exec (unroll c) v = exec c v.
Proof. Proof.
admit.
Qed. Qed.*)