Module ImpPrelude

Require Export String.
Require Export List.
Require Extraction.
Require Import Ascii.
Require Import BinNums.
Require Export ImpCore.
Require Export PArith.


Import Notations.
Local Open Scope impure.

Definition iandb (k1 k2: ??bool): ?? bool :=
  DO r1 <~ k1 ;;
  if r1 then k2 else RET false.

Extraction Inline iandb.


Axiom caml_string: Type.
Extract Constant caml_string => "string".

Definition nl: string := String (ascii_of_pos 10%positive) EmptyString.

Inductive pstring: Type :=
  | Str: string -> pstring
  | CamlStr: caml_string -> pstring
  | Concat: pstring -> pstring -> pstring.

Coercion Str: string >-> pstring.
Bind Scope string_scope with pstring.

Notation "x +; y" := (Concat x y)
    (at level 65, left associativity): string_scope.


Record cref {A} := {
  set: A -> ?? unit;
  get: unit -> ?? A
}.
Arguments cref: clear implicits.

Axiom make_cref: forall {A}, A -> ?? cref A.
Extract Constant make_cref => "(fun x -> let r = ref x in { set = (fun y -> r:=y); get = (fun () -> !r) })".



Record logger {A:Type} := {
  log_insert: A -> ?? unit;
  log_info: unit -> ?? pstring;
}.
Arguments logger: clear implicits.

Axiom count_logger: unit -> ?? logger unit.
Extract Constant count_logger => "(fun () -> let count = ref 0 in { log_insert = (fun () -> count := !count + 1); log_info = (fun () -> (CamlStr (string_of_int !count))) })".



Axiom phys_eq: forall {A}, A -> A -> ?? bool.

Axiom phys_eq_correct: forall A (x y:A), WHEN phys_eq x y ~> b THEN b=true -> x=y.


Module PhysEqModel.

Definition phys_eq {A} (x y: A) := ret false.

Lemma phys_eq_correct: forall A (x y:A), WHEN phys_eq x y ~> b THEN b=true -> x=y.

End PhysEqModel.

Extract Inlined Constant phys_eq => "(==)".
#[global] Hint Resolve phys_eq_correct: wlp.




Program Definition jourdan_phys_eq_aux {A B} (x y: A)
  (fast_path: unit -> x=y -> B)
  (slow_path: unit -> B)
  (Hdet: forall (Heq: x=y), fast_path tt Heq = slow_path tt)
  : {r: B | r = slow_path tt} :=
    det_coerce (DO b <~ mk_annot (phys_eq x y);;
                match b with
                | true => RET (fast_path tt _)
                | false => RET (slow_path tt)
                end)
                slow_path _.

Definition jourdan_phys_eq {A B} (x y: A)
  (fast_path: {_:unit | x=y } -> B)
  (slow_path: unit -> B)
  (Hdet: forall (Heq: x=y), fast_path (exist _ tt Heq) = slow_path tt)
  : B
 := ` (jourdan_phys_eq_aux x y (fun _ Heq => fast_path (exist _ tt Heq)) slow_path Hdet).

Lemma jourdan_phys_eq_correct {A B} (x y: A)
  (fast_path: {_:unit | x=y } -> B)
  (slow_path: unit -> B)
  (Hdet: forall (Heq: x=y), fast_path (exist _ tt Heq) = slow_path tt):
  jourdan_phys_eq x y fast_path slow_path Hdet = slow_path tt.



Axiom struct_eq: forall {A}, A -> A -> ?? bool.
Axiom struct_eq_correct: forall A (x y:A), WHEN struct_eq x y ~> b THEN if b then x=y else x<>y.
Extract Inlined Constant struct_eq => "(=)".
#[global] Hint Resolve struct_eq_correct: wlp.



Axiom hashcode: Type.
Extract Constant hashcode => "int".

Axiom hash_older: hashcode -> hashcode -> ?? bool.
Extract Inlined Constant hash_older => "(<)".

Module Dict.

Record hash_params {A:Type} := {
  test_eq: A -> A -> ??bool;
  test_eq_correct: forall x y, WHEN test_eq x y ~> r THEN r=true -> x=y;
  hashing: A -> ??hashcode;
  log: A -> ??unit
}.
Arguments hash_params: clear implicits.


Record t {A B:Type} := {
  set: A * B -> ?? unit;
  get: A -> ?? option B
}.
Arguments t: clear implicits.

End Dict.

Module HConsingDefs.

Record hashinfo {A: Type} := {
  hdata: A;
  hcodes: list hashcode;
}.
Arguments hashinfo: clear implicits.

Record hashP {A:Type}:= {
  hash_eq: A -> A -> ?? bool;
  get_hid: A -> hashcode;
  set_hid: A -> hashcode -> A;
}.
Arguments hashP: clear implicits.

Axiom unknown_hid: hashcode.
Extract Constant unknown_hid => "-1".

Definition ignore_hid {A} (hp: hashP A) (hv:A) := set_hid hp hv unknown_hid.

Record hashExport {A:Type}:= {
  get_info: hashcode -> ?? hashinfo A;
  iterall: ((list pstring) -> hashcode -> hashinfo A -> ?? unit) -> ?? unit;
}.
Arguments hashExport: clear implicits.

Record hashConsing {A:Type}:= {
  hC: hashinfo A -> ?? A;
  next_hid: unit -> ?? hashcode;
  remove: hashinfo A -> ??unit;
  next_log: pstring -> ?? unit;
  export: unit -> ?? hashExport A ;
}.
Arguments hashConsing: clear implicits.

End HConsingDefs.

Inductive recMode:= StdRec | MemoRec | BareRec | BuggyRec.


Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q.

Ltac exploit x :=
    refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _ _) _)
 || refine (modusponens _ _ (x _ _ _) _)
 || refine (modusponens _ _ (x _ _) _)
 || refine (modusponens _ _ (x _) _).