1 files changed, 199 insertions, 0 deletions
diff --git a/lib/Impure/ImpHCons.v b/lib/Impure/ImpHCons.v
new file mode 100644
index 00000000..637116cc
--- /dev/null
+++ b/lib/Impure/ImpHCons.v
@@ -0,0 +1,199 @@
+Require Export ImpIO.
+
+Import Notations.
+Local Open Scope impure.
+
+
+Axiom string_of_hashcode: hashcode -> ?? caml_string.
+Extract Constant string_of_hashcode => "string_of_int".
+
+Axiom hash: forall {A}, A -> ?? hashcode.
+Extract Constant hash => "Hashtbl.hash".
+
+(**************************)
+(* (Weak) Sets            *)
+
+
+Import Dict.
+
+Axiom make_dict: forall {A B}, (hash_params A) -> ?? Dict.t A B.
+Extract Constant make_dict => "ImpHConsOracles.make_dict".
+
+
+Module Sets.
+
+Definition t {A} (mod: A -> Prop) := Dict.t A {x | mod x}.
+
+Definition empty {A} (hp: hash_params A) {mod:A -> Prop}: ?? t mod :=
+  make_dict hp.
+
+Program Fixpoint add {A} (l: list A) {mod: A -> Prop} (d: t mod): forall {H:forall x, List.In x l -> mod x}, ?? unit :=
+  match l with
+  | nil => fun H => RET ()
+  | x::l' => fun H =>
+    d.(set)(x,x);;
+    add l' d
+  end.
+
+Program Definition create {A} (hp: hash_params A) (l:list A): ?? t (fun x => List.In x l) :=
+  DO d <~ empty hp (mod:=fun x => List.In x l);;
+  add l (mod:=fun x => List.In x l) d (H:=_);;
+  RET d.
+Global Opaque create.
+
+Definition is_present {A} (hp: hash_params A) (x:A) {mod} (d:t mod): ?? bool :=
+  DO oy <~ (d.(get)) x;;
+  match oy with
+  | Some y => hp.(test_eq) x (`y)
+  | None => RET false
+  end.
+
+Local Hint Resolve test_eq_correct: wlp.
+
+Lemma is_present_correct A (hp: hash_params A) x mod (d:t mod):
+ WHEN is_present hp x d ~> b THEN b=true -> mod x.
+Proof.
+  wlp_simplify; subst; eauto.
+  - apply proj2_sig.
+  - discriminate. 
+Qed.
+Hint Resolve is_present_correct: wlp.
+Global Opaque is_present.
+
+Definition msg_assert_incl: pstring := "Sets.assert_incl".
+
+Fixpoint assert_incl {A} (hp: hash_params A) (l: list A) {mod} (d:t mod): ?? unit :=
+  match l with
+  | nil => RET ()
+  | x::l' =>
+    DO b <~ is_present hp x d;;
+    if b then
+      assert_incl hp l' d
+    else (
+      hp.(log) x;;
+      FAILWITH msg_assert_incl
+    )
+  end.
+
+Lemma assert_incl_correct A (hp: hash_params A) l mod (d:t mod):
+ WHEN assert_incl hp l d ~> _ THEN forall x, List.In x l -> mod x.
+Proof.
+  induction l; wlp_simplify; subst; eauto.
+Qed.
+Hint Resolve assert_incl_correct: wlp.
+Global Opaque assert_incl.
+
+Definition assert_list_incl {A} (hp: hash_params A) (l1 l2: list A): ?? unit :=
+  (* println "";;print("dict_create ");;*)
+  DO d <~ create hp l2;;
+  (*print("assert_incl ");;*)
+  assert_incl hp l1 d.
+
+Lemma assert_list_incl_correct A (hp: hash_params A) l1 l2:
+ WHEN assert_list_incl hp l1 l2 ~> _ THEN List.incl l1 l2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque assert_list_incl.
+Hint Resolve assert_list_incl_correct: wlp.
+
+End Sets.
+
+
+
+
+(********************************)
+(* (Weak) HConsing              *)
+
+Module HConsing.
+
+Export HConsingDefs.
+
+(* NB: this axiom is NOT intended to be called directly, but only through [hCons...] functions below. *)
+Axiom xhCons: forall {A}, (hashP A) -> ?? hashConsing A.
+Extract Constant xhCons => "ImpHConsOracles.xhCons".
+
+Definition hCons_eq_msg: pstring := "xhCons: hash eq differs".
+
+Definition hCons {A} (hp: hashP A): ?? (hashConsing A) :=
+  DO hco <~ xhCons hp ;;
+  RET {|
+      hC := (fun x =>
+         DO x' <~ hC hco x ;;
+         DO b0 <~ hash_eq hp x.(hdata) x' ;;
+         assert_b b0 hCons_eq_msg;;
+         RET x');
+      next_hid := hco.(next_hid);
+      next_log := hco.(next_log);
+      export := hco.(export);
+      remove := hco.(remove)
+      |}.
+
+
+Lemma hCons_correct A (hp: hashP A):
+  WHEN hCons hp ~> hco THEN
+    (forall x y, WHEN hp.(hash_eq) x y ~> b THEN b=true -> (ignore_hid hp x)=(ignore_hid hp y)) ->
+    forall x, WHEN hco.(hC) x ~> x' THEN ignore_hid hp x.(hdata)=ignore_hid hp x'.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hCons.
+Hint Resolve hCons_correct: wlp.
+
+
+
+(* hashV: extending a given type with hash-consing *)
+Record hashV {A:Type}:= {
+  data: A;
+  hid: hashcode
+}.
+Arguments hashV: clear implicits.
+
+Definition hashV_C {A} (test_eq: A -> A -> ?? bool) : hashP (hashV A) := {|
+  hash_eq := fun v1 v2 => test_eq v1.(data) v2.(data);
+  get_hid := hid;
+  set_hid := fun v id => {| data := v.(data); hid := id |}
+|}.
+
+Definition liftHV (x:nat) := {| data := x; hid := unknown_hid |}.
+
+Definition hConsV {A} (hasheq: A -> A -> ?? bool): ?? (hashConsing (hashV A)) :=
+  hCons (hashV_C hasheq).
+
+Lemma hConsV_correct A (hasheq: A -> A -> ?? bool):
+  WHEN hConsV hasheq ~> hco THEN
+    (forall x y, WHEN hasheq x y ~> b THEN b=true -> x=y) -> 
+    forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data).
+Proof.
+  Local Hint Resolve f_equal2: core.
+  wlp_simplify.
+  exploit H; eauto.
+  + wlp_simplify.
+  + intros; congruence.
+Qed.
+Global Opaque hConsV.
+Hint Resolve hConsV_correct: wlp.
+
+Definition hC_known {A} (hco:hashConsing (hashV A)) (unknownHash_msg: hashinfo (hashV A) -> ?? pstring) (x:hashinfo (hashV A)): ?? hashV A :=
+  DO clock <~ hco.(next_hid)();;
+  DO x' <~ hco.(hC) x;;
+  DO ok <~ hash_older x'.(hid) clock;;
+  if ok 
+  then RET x'
+  else
+    hco.(remove) x;; 
+    DO msg <~ unknownHash_msg x;;
+    FAILWITH msg.
+
+Lemma hC_known_correct A (hco:hashConsing (hashV A)) msg x:
+  WHEN hC_known hco msg x ~> x' THEN
+    (forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data)) ->
+    x.(hdata).(data)=x'.(data).
+Proof.
+  wlp_simplify.
+  unfold wlp in * |- ; eauto.
+Qed.
+Global Opaque hC_known.
+Hint Resolve hC_known_correct: wlp.
+
+End HConsing.