From mininix Require Export nix.interp nix.notations.
From stdpp Require Import options.
Open Scope Z_scope.

(** Compare base vals without comparing the proofs. Since we do not have
definitional proof irrelevance, comparing the proofs would fail (and in practice
make Coq loop). *)
Definition res_eq (rv : res val) (bl2 : base_lit) :=
  match rv with
  | Res (Some (VLit bl1 _)) => bl1 = bl2
  | _ => False
  end.
Infix "=?" := res_eq.

Definition float_1 :=
  ceil: (Float.of_Z 20 /: 3).
Goal interp 100 ∅ float_1 =? 7.
Proof. by vm_compute. Qed.

Definition float_2 :=
  Float.of_Z 100000000000000000000000000000000000000000000000000000000000000000000000000000 *:
  Float.of_Z 100000000000000000000000000000000000000000000000000000000000000000000000000000 *:
  Float.of_Z 100000000000000000000000000000000000000000000000000000000000000000000000000000 *:
  Float.of_Z 100000000000000000000000000000000000000000000000000000000000000000000000000000 *:
  Float.of_Z 100000000000000000000000000000000000000000000000000000000000000000000000000000.
Goal interp 100 ∅ float_2 =? NFloat (Binary.B754_infinity false).
Proof. by vm_compute. Qed.

Definition float_3 := float_2 /: float_2.
Goal interp 100 ∅ float_3 =? NFloat (`Float.indef_nan).
Proof. by vm_compute. Qed.

Definition let_let :=
  let: "x" := 1 in let: "x" := 2 in "x".
Goal interp 100 ∅ let_let =? 2.
Proof. by vm_compute. Qed.

Definition with_let :=
  with: EAttr {[ "x" := AttrN 1 ]} in let: "x" := 2 in "x".
Goal interp 100 ∅ with_let =? 2.
Proof. by vm_compute. Qed.

Definition let_with :=
  let: "x" := 1 in with: EAttr {[ "x" := AttrN 2 ]} in "x".
Goal interp 100 ∅ let_with =? 1.
Proof. by vm_compute. Qed.

Definition with_with :=
  with: EAttr {[ "x" := AttrN 1 ]} in with: EAttr {[ "x" := AttrN 2 ]} in "x".
Goal interp 100 ∅ with_with =? 2.
Proof. by vm_compute. Qed.

Definition with_with_inherit :=
  with: EAttr {[ "x" := AttrN 1 ]} in with: EAttr {[ "x" := AttrN "x" ]} in "x".
Goal interp 100 ∅ with_with_inherit =? 1.
Proof. by vm_compute. Qed.

Definition with_loop :=
  with: EAttr {[ "x" := AttrR "x" ]} in "x".
Goal interp 100 ∅ with_loop = NoFuel.
Proof. by vm_compute. Qed.

Definition rec_attr_shadow_1 :=
  let: "foo" := EAttr {[ "bar" := AttrN 10 ]} in
  EAttr {[
    "bar" := AttrR ("foo" .: "bar");
    "foo" := AttrR (EAttr {[ "bar" := AttrN 20 ]})
  ]} .: "bar".
Goal interp 100 ∅ rec_attr_shadow_1 =? 20.
Proof. by vm_compute. Qed.

Definition rec_attr_shadow_2 :=
  EAttr {[
    "y" := AttrR (EAttr {[ "y" := AttrN "z" ]} .: "y");
    "z" := AttrR 20
  ]} .: "y".
Goal interp 100 ∅ rec_attr_shadow_2 =? 20.
Proof. by vm_compute. Qed.

Definition nested_functor_1 :=
  EAttr {[ "__functor" := AttrN $ λ: "self",
    EAttr {[ "__functor" := AttrN $ λ: "self" "x", 10 ]} ]} 10.
Goal interp 100 ∅ nested_functor_1 =? 10.
Proof. by vm_compute. Qed.

Definition nested_functor_2 :=
  EAttr {[ "__functor" := AttrN $
    EAttr {[ "__functor" := AttrN $ λ: "self" "self" "x", 10 ]} ]} 10.
Goal interp 100 ∅ nested_functor_2 =? 10.
Proof. by vm_compute. Qed.

Definition functor_loop_1 :=
  EAttr {[ "__functor" := AttrN $
    λ: "self", "self" "self"
  ]} 10.
Goal interp 1000 ∅ functor_loop_1 = NoFuel.
Proof. by vm_compute. Qed.

Definition functor_loop_2 :=
  EAttr {[ "__functor" := AttrN $
    λ: "self" "f", "f" ("self" "f")
  ]} (λ: "go" "x", "go" "x") 10.
Goal interp 1000 ∅ functor_loop_2 = NoFuel.
Proof. by vm_compute. Qed.

Fixpoint many_lets (i : nat) (e : expr) : expr :=
  match i with
  | O => e
  | S i => let: "x" +:+ pretty i := 0 in many_lets i e
  end.

Fixpoint many_adds (i : nat) : expr :=
  match i with
  | O => 0
  | S i => ("x" +:+ pretty i) +: many_adds i
  end.

Definition big_prog (i : nat) : expr := many_lets i $ many_adds i.

Definition big := big_prog 1000.

Goal interp 5000 ∅ big =? 0.
Proof. by vm_compute. Qed.

Definition matching_1 :=
  (λattr: {[ "x" := None; "y" := None ]}, "x" +: "y")
    (EAttr {[ "x" := AttrN 10; "y" := AttrN 11 ]}).
Goal interp 1000 ∅ matching_1 =? 21.
Proof. by vm_compute. Qed.

Definition matching_2 :=
  (λattr: {[ "x" := None; "y" := Some (EId' "x") ]}, "x" +: "y")
    (EAttr {[ "x" := AttrN 10 ]}).
Goal interp 1000 ∅ matching_2 =? 20.
Proof. by vm_compute. Qed.

Definition matching_3 :=
  (λattr: {[ "x" := None; "y" := None ]}, "x" +: "y")
    (EAttr {[ "x" := AttrN 10 ]}).
Goal interp 1000 ∅ matching_3 = mfail.
Proof. by vm_compute. Qed.

Definition matching_4 :=
  (λattr: {[ "x" := None; "y" := None ]}, "x" +: "y")
    (EAttr {[ "x" := AttrN 10; "y" := AttrN 11; "z" := AttrN 12 ]}).
Goal interp 1000 ∅ matching_4 = mfail.
Proof. by vm_compute. Qed.

Definition matching_5 :=
  (λattr: {[ "x" := None; "y" := None ]} .., "x" +: "y")
    (EAttr {[ "x" := AttrN 10; "y" := AttrN 11; "z" := AttrN 12 ]}).
Goal interp 1000 ∅ matching_5 =? 21.
Proof. by vm_compute. Qed.

Definition matching_6 :=
  (λattr: {[ "y" := Some (EId' "y") ]}, "y")
    (EAttr {[ "y" := AttrN 10 ]}).
Goal interp 1000 ∅ matching_6 =? 10.
Proof. by vm_compute. Qed.

Definition matching_7 :=
  (λattr: {[ "y" := Some (EId' "y") ]}, "y") (EAttr ∅).
Goal interp 1000 ∅ matching_7 = NoFuel.
Proof. by vm_compute. Qed.

Definition matching_8 :=
  (λattr: {[ "y" := Some (EId' "y") ]}.., "y")
  (EAttr {[ "x" := AttrN 10 ]}).
Goal interp 1000 ∅ matching_8 = NoFuel.
Proof. by vm_compute. Qed.

Definition list_lt_1 :=
  EList [ELit 2; ELit 3] <: EList [ELit 3].
Goal interp 1000 ∅ list_lt_1 =? true.
Proof. by vm_compute. Qed.

Definition list_lt_2 :=
  EList [ELit 2; ELit 3] <: EList [ELit 2].
Goal interp 1000 ∅ list_lt_2 =? false.
Proof. by vm_compute. Qed.

Definition list_lt_3 :=
  EList [ELit 2] <: EList [ELit 2; ELit 3].
Goal interp 1000 ∅ list_lt_3 =? true.
Proof. by vm_compute. Qed.