Initialize repository

1 files changed, 185 insertions, 0 deletions

diff --git a/theories/nix/tests.v b/theories/nix/tests.v
new file mode 100644
index 0000000..cbce874
--- /dev/null
+++ b/theories/nix/tests.v
@@ -0,0 +1,185 @@
+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.