pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-28 07:16:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

DeepAndShallowEmbeddings: Coq 8.4 support

Browse source
This commit is contained in:
Adam Chlipala 2016-04-11 08:13:49 -04:00
parent e50cbae0c3
commit 145bff88c6
2 changed files with 13 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
DeepAndShallowEmbeddings.v
View file

@ -6,6 +6,7 @@
Require Import Frap. Require Import Frap.
Set Implicit Arguments. Set Implicit Arguments.
Set Asymmetric Patterns.
(** * Shared notations and definitions; main material starts afterward. *) (** * Shared notations and definitions; main material starts afterward. *)
@ -229,7 +230,7 @@ Module Shallow.
induct i; unfold hoare_triple in *; simplify; propositional; auto. induct i; unfold hoare_triple in *; simplify; propositional; auto.
specialize (IHi (max (h $! i) acc) h); propositional. specialize (IHi (max (h $! i) acc) h); propositional.
cases (array_max i (max (h $! i) acc)); simplify; propositional; subst. cases (array_max i (max (h $! i) acc) h); simplify; propositional; subst.
apply IHi; auto. apply IHi; auto.
simplify. simplify.
cases (j0 ==n i); subst; auto. cases (j0 ==n i); subst; auto.
@ -359,8 +360,8 @@ Module Deep.
Fixpoint interp {result} (c : cmd result) (h : heap) : heap * result := Fixpoint interp {result} (c : cmd result) (h : heap) : heap * result :=
match c with match c with
| Return r => (h, r) | Return _ r => (h, r)
| Bind c1 c2 => | Bind _ _ c1 c2 =>
let (h', r) := interp c1 h in let (h', r) := interp c1 h in
interp (c2 r) h' interp (c2 r) h'
| Read a => (h, h $! a) | Read a => (h, h $! a)
@ -551,15 +552,15 @@ Module Deeper.
Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result := Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result :=
match c with match c with
| Return r => Answer r | Return _ r => Answer r
| Bind c1 c2 => | Bind _ _ c1 c2 =>
match step c1 h with match step c1 h with
| Answer r => Stepped h (c2 r) | Answer r => Stepped h (c2 r)
| Stepped h' c1' => Stepped h' (Bind c1' c2) | Stepped h' c1' => Stepped h' (Bind c1' c2)
end end
| Read a => Answer (h $! a) | Read a => Answer (h $! a)
| Write a v => Stepped (h $+ (a, v)) (Return tt) | Write a v => Stepped (h $+ (a, v)) (Return tt)
| Loop init body => | Loop _ init body =>
Stepped h (r <- body init; Stepped h (r <- body init;
match r with match r with
| Done r' => Return r' | Done r' => Return r'
@ -889,8 +890,8 @@ Module DeeperWithFail.
Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result := Fixpoint step {result} (c : cmd result) (h : heap) : stepResult result :=
match c with match c with
| Return r => Answer r | Return _ r => Answer r
| Bind c1 c2 => | Bind _ _ c1 c2 =>
match step c1 h with match step c1 h with
| Answer r => Stepped h (c2 r) | Answer r => Stepped h (c2 r)
| Stepped h' c1' => Stepped h' (Bind c1' c2) | Stepped h' c1' => Stepped h' (Bind c1' c2)
@ -898,13 +899,13 @@ Module DeeperWithFail.
end end
| Read a => Answer (h $! a) | Read a => Answer (h $! a)
| Write a v => Stepped (h $+ (a, v)) (Return tt) | Write a v => Stepped (h $+ (a, v)) (Return tt)
| Loop init body => | Loop _ init body =>
Stepped h (r <- body init; Stepped h (r <- body init;
match r with match r with
| Done r' => Return r' | Done r' => Return r'
| Again r' => Loop r' body | Again r' => Loop r' body
end) end)
| Fail => Failed | Fail _ => Failed
end. end.
Fixpoint multiStep {result} (c : cmd result) (h : heap) (n : nat) : stepResult result := Fixpoint multiStep {result} (c : cmd result) (h : heap) (n : nat) : stepResult result :=
@ -1236,10 +1237,7 @@ Module DeeperWithFail.
| Done (_, acc) => acc = fold_left f ls init | Done (_, acc) => acc = fold_left f ls init
| Again (i, acc) => acc = fold_left f (firstn i ls) init | Again (i, acc) => acc = fold_left f (firstn i ls) init
end). end).
cases (length ls <=? a); ht. cases (length ls <=? a); ht; auto; simp; auto.
apply H.
simp; auto.
simp.
rewrite H2 by assumption. rewrite H2 by assumption.
simplify. simplify.
reflexivity. reflexivity.

1
_CoqProject
View file

@ -22,3 +22,4 @@ AbstractInterpretation.v
LambdaCalculusAndTypeSoundness_template.v LambdaCalculusAndTypeSoundness_template.v
LambdaCalculusAndTypeSoundness.v LambdaCalculusAndTypeSoundness.v
TypesAndMutation.v TypesAndMutation.v
DeepAndShallowEmbeddings.v