From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Mon, 7 Jul 2025 21:52:08 +0200 Subject: Initialize repository --- theories/nix/tests.v | 185 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 185 insertions(+) create mode 100644 theories/nix/tests.v (limited to 'theories/nix/tests.v') 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. -- cgit v1.2.3