From 01d550e4b00c10fc7fbc20ec044aae29b9764205 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 10 Apr 2016 13:48:58 -0400 Subject: [PATCH] DeepAndShallowEmbeddings: ran some code in OCaml --- .gitignore | 1 + DeepAndShallowEmbeddings.v | 234 +++++++++++++++++++++++++++++++++++++ DeepInterp.ml | 24 ++++ 3 files changed, 259 insertions(+) create mode 100644 DeepAndShallowEmbeddings.v create mode 100644 DeepInterp.ml diff --git a/.gitignore b/.gitignore index 21d21e7..6838b09 100644 --- a/.gitignore +++ b/.gitignore @@ -15,3 +15,4 @@ Makefile.coq *.vo frap.tgz .coq-native +Deep.ml* diff --git a/DeepAndShallowEmbeddings.v b/DeepAndShallowEmbeddings.v new file mode 100644 index 0000000..5f5967d --- /dev/null +++ b/DeepAndShallowEmbeddings.v @@ -0,0 +1,234 @@ +(** Formal Reasoning About Programs + * Chapter 11: Deep and Shallow Embeddings + * Author: Adam Chlipala + * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *) + +Require Import Frap. + +(** * Shared notations and definitions *) + +Notation "m $! k" := (match m $? k with Some n => n | None => O end) (at level 30). +Definition heap := fmap nat nat. +Definition assertion := heap -> Prop. + +Hint Extern 1 (_ <= _) => linear_arithmetic. +Hint Extern 1 (@eq nat _ _) => linear_arithmetic. + +Example h0 : heap := $0 $+ (0, 2) $+ (1, 1) $+ (2, 8) $+ (3, 6). + +Hint Rewrite max_l max_r using linear_arithmetic. + + +(** * Shallow embedding of a language very similar to the one we used last chapter *) + +Module Shallow. + Definition cmd result := heap -> heap * result. + + Definition hoare_triple (P : assertion) {result} (c : cmd result) (Q : result -> assertion) := + forall h, P h + -> let (h', r) := c h in + Q r h'. + + Notation "{{ h ~> P }} c {{ r & h' ~> Q }}" := + (hoare_triple (fun h => P) c (fun r h' => Q)) (at level 90, c at next level). + + Theorem consequence : forall P {result} (c : cmd result) Q + (P' : assertion) (Q' : _ -> assertion), + hoare_triple P c Q + -> (forall h, P' h -> P h) + -> (forall r h, Q r h -> Q' r h) + -> hoare_triple P' c Q'. + Proof. + unfold hoare_triple; simplify. + specialize (H h). + specialize (H0 h). + cases (c h). + auto. + Qed. + + Fixpoint array_max (i acc : nat) : cmd nat := + fun h => + match i with + | O => (h, acc) + | S i' => + let h_i' := h $! i' in + array_max i' (max h_i' acc) h + end. + + Lemma array_max_ok' : forall len i acc, + {{ h ~> forall j, i <= j < len -> h $! j <= acc }} + array_max i acc + {{ r&h ~> forall j, j < len -> h $! j <= r }}. + Proof. + induct i; unfold hoare_triple in *; simplify; propositional; auto. + + specialize (IHi (max (h $! i) acc) h); propositional. + cases (array_max i (max (h $! i) acc)); simplify; propositional; subst. + apply IHi; auto. + simplify. + cases (j0 ==n i); subst; auto. + assert (h $! j0 <= acc) by auto. + linear_arithmetic. + Qed. + + Theorem array_max_ok : forall len, + {{ _ ~> True }} + array_max len 0 + {{ r&h ~> forall i, i < len -> h $! i <= r }}. + Proof. + simplify. + eapply consequence. + apply array_max_ok' with (len := len). + + simplify. + linear_arithmetic. + + auto. + Qed. + + Example run_array_max0 : array_max 4 0 h0 = (h0, 8). + Proof. + unfold h0. + simplify. + reflexivity. + Qed. + + Fixpoint increment_all (i : nat) : cmd unit := + fun h => + match i with + | O => (h, tt) + | S i' => increment_all i' (h $+ (i', S (h $! i'))) + end. + + Lemma increment_all_ok' : forall len h0 i, + {{ h ~> (forall j, j < i -> h $! j = h0 $! j) + /\ (forall j, i <= j < len -> h $! j = S (h0 $! j)) }} + increment_all i + {{ _&h ~> forall j, j < len -> h $! j = S (h0 $! j) }}. + Proof. + induct i; unfold hoare_triple in *; simplify; propositional; auto. + + specialize (IHi (h $+ (i, S (h $! i)))); propositional. + cases (increment_all i (h $+ (i, S (h $! i)))); simplify; propositional; subst. + apply H; simplify; auto. + + cases (j0 ==n i); subst; auto. + simplify; auto. + simplify; auto. + Qed. + + Theorem increment_all_ok : forall len h0, + {{ h ~> h = h0 }} + increment_all len + {{ _&h ~> forall j, j < len -> h $! j = S (h0 $! j) }}. + Proof. + simplify. + eapply consequence. + apply increment_all_ok' with (len := len). + + simplify; subst; propositional. + linear_arithmetic. + + simplify. + auto. + Qed. + + Example run_increment_all0 : increment_all 4 h0 = ($0 $+ (0, 3) $+ (1, 2) $+ (2, 9) $+ (3, 7), tt). + Proof. + unfold h0. + simplify. + f_equal. + maps_equal. + Qed. +End Shallow. + + +(** * A basic deep embedding *) + +Module Deep. + Inductive cmd : Type -> Type := + | Return {result} (r : result) : cmd result + | Bind {result result'} (c1 : cmd result') (c2 : result' -> cmd result) : cmd result + | Read (a : nat) : cmd nat + | Write (a v : nat) : cmd unit. + + Notation "x <- c1 ; c2" := (Bind c1 (fun x => c2)) (right associativity, at level 80). + + Fixpoint array_max (i acc : nat) : cmd nat := + match i with + | O => Return acc + | S i' => + h_i' <- Read i'; + array_max i' (max h_i' acc) + end. + + Fixpoint increment_all (i : nat) : cmd unit := + match i with + | O => Return tt + | S i' => + v <- Read i'; + _ <- Write i' (S v); + increment_all i' + end. + + Fixpoint interp {result} (c : cmd result) (h : heap) : heap * result := + match c with + | Return r => (h, r) + | Bind c1 c2 => + let (h', r) := interp c1 h in + interp (c2 r) h' + | Read a => (h, h $! a) + | Write a v => (h $+ (a, v), tt) + end. + + Example run_array_max0 : interp (array_max 4 0) h0 = (h0, 8). + Proof. + unfold h0. + simplify. + reflexivity. + Qed. + + Example run_increment_all0 : interp (increment_all 4) h0 = ($0 $+ (0, 3) $+ (1, 2) $+ (2, 9) $+ (3, 7), tt). + Proof. + unfold h0. + simplify. + f_equal. + maps_equal. + Qed. + + Inductive hoare_triple : assertion -> forall {result}, cmd result -> (result -> assertion) -> Prop := + | HtReturn : forall P {result} (v : result), + hoare_triple P (Return v) (fun r h => P h /\ r = v) + | HtBind : forall P {result' result} (c1 : cmd result') (c2 : result' -> cmd result) Q R, + hoare_triple P c1 Q + -> (forall r, hoare_triple (Q r) (c2 r) R) + -> hoare_triple P (Bind c1 c2) R + | HtRead : forall P a, + hoare_triple P (Read a) (fun r h => P h /\ r = h $! a) + | HtWrite : forall P a v, + hoare_triple P (Write a v) (fun _ h => exists h', P h' /\ h = h' $+ (a, v)) + | HtConsequence : forall {result} (c : cmd result) P Q (P' : assertion) (Q' : _ -> assertion), + hoare_triple P c Q + -> (forall h, P' h -> P h) + -> (forall r h, Q r h -> Q' r h) + -> hoare_triple P' c Q'. + + Theorem hoare_triple_sound : forall P {result} (c : cmd result) Q, + hoare_triple P c Q + -> forall h, P h + -> let (h', r) := interp c h in + Q r h'. + Proof. + induct 1; simplify; propositional; eauto. + + specialize (IHhoare_triple h). + cases (interp c1 h). + apply H1; eauto. + + specialize (IHhoare_triple h). + cases (interp c h). + eauto. + Qed. + + Extraction "Deep.ml" array_max increment_all. +End Deep. diff --git a/DeepInterp.ml b/DeepInterp.ml new file mode 100644 index 0000000..72754c6 --- /dev/null +++ b/DeepInterp.ml @@ -0,0 +1,24 @@ +let rec i2n n = + match n with + | 0 -> O + | _ -> S (i2n (n - 1)) + +let interp c = + let h : (nat, nat) Hashtbl.t = Hashtbl.create 0 in + Hashtbl.add h (i2n 0) (i2n 2); + Hashtbl.add h (i2n 1) (i2n 1); + Hashtbl.add h (i2n 2) (i2n 8); + Hashtbl.add h (i2n 3) (i2n 6); + + let rec interp' (c : 'a cmd) : 'a = + match c with + | Return v -> v + | Bind (c1, c2) -> interp' (c2 (interp' c1)) + | Read a -> + Obj.magic (try + Hashtbl.find h a + with Not_found -> O) + | Write (a, v) -> Obj.magic (Hashtbl.replace h a v) + + in let v = interp' c in + h, v