From b549b15af70b0cd09e379f75877bc7e55cfee192 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 18 Apr 2021 16:23:25 -0400 Subject: [PATCH] Revising for next lecture --- DeepAndShallowEmbeddings.v | 8 +++++--- DeepAndShallowEmbeddings_template.v | 6 +++--- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v index ec1b18d..309d2ed 100644 --- a/DeepAndShallowEmbeddings.v +++ b/DeepAndShallowEmbeddings.v @@ -14,8 +14,8 @@ Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 3 Definition heap := fmap nat nat. Definition assertion := heap -> Prop. -Hint Extern 1 (_ <= _) => linear_arithmetic : core. -Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. +Local Hint Extern 1 (_ <= _) => linear_arithmetic : core. +Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6). @@ -494,6 +494,7 @@ Module Deep. eauto. Qed. End Deep. + (* We use Coq's *extraction* feature to produce OCaml versions of our deeply * embedded programs. Then we can run them using OCaml intepreters, which are * able to take advantage of the side effects built into OCaml, as a @@ -839,6 +840,7 @@ End Deeper. Extraction "Deeper.ml" Deeper.index_of. + (** * Adding the possibility of program failure *) (* Let's model another effect that can be implemented using native OCaml @@ -1270,7 +1272,7 @@ Module DeeperWithFail. apply IHls; linear_arithmetic. Qed. - Hint Resolve le_max : core. + Local Hint Resolve le_max : core. (* Finally, a short proof of [array_max], appealing mostly to the generic * proof of [heapfold] *) diff --git a/DeepAndShallowEmbeddings_template.v b/DeepAndShallowEmbeddings_template.v index dec4c7b..c0cfe9d 100644 --- a/DeepAndShallowEmbeddings_template.v +++ b/DeepAndShallowEmbeddings_template.v @@ -9,8 +9,8 @@ Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 3 Definition heap := fmap nat nat. Definition assertion := heap -> Prop. -Hint Extern 1 (_ <= _) => linear_arithmetic : core. -Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. +Local Hint Extern 1 (_ <= _) => linear_arithmetic : core. +Local Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6). @@ -1085,7 +1085,7 @@ Module DeeperWithFail. apply IHls; linear_arithmetic. Qed. - Hint Resolve le_max : core. + Local Hint Resolve le_max : core. Theorem array_max_ok : forall ls : list nat, {{ h ~> forall i, i < length ls -> h $! i = nth_default 0 ls i}}