Add initial filesmain

4 files changed, 120 insertions, 0 deletions

diff --git a/.envrc b/.envrc
new file mode 100644
index 0000000..c9c0b69
--- /dev/null
+++ b/.envrc
@@ -0,0 +1,8 @@
+if type lorri &>/dev/null; then
+    echo "direnv: using lorri"
+    eval "$(lorri direnv)"
+else
+    # fall back to using direnv's builtin nix support
+    # to prevent bootstrapping problems.
+    use nix
+fi
diff --git a/coq/padic.v b/coq/padic.v
new file mode 100644
index 0000000..af28184
--- /dev/null
+++ b/coq/padic.v
@@ -0,0 +1,88 @@
+Require Import Coq.Bool.Bool.
+Require Import Coq.Lists.List.
+Import ListNotations.
+
+Local Open Scope list.
+
+CoInductive padic : Type := padic_seq : bool -> padic -> padic.
+
+CoFixpoint map (f: bool -> bool) (p: padic) :=
+  match p with
+  | padic_seq a b => padic_seq (f a) (map f b)
+  end.
+
+CoFixpoint shuffle (a b: padic): padic :=
+  match a, b with
+    padic_seq ahd atl, padic_seq bhd btl =>
+      padic_seq ahd (padic_seq bhd (shuffle atl btl))
+  end.
+
+CoFixpoint zip (f: bool -> bool -> bool) (a b: padic): padic :=
+  match a, b with
+  | padic_seq a' a'', padic_seq b' b'' =>
+    padic_seq (f a' b') (zip f a'' b'')
+  end.
+
+CoFixpoint zip3 (f: bool -> bool -> bool -> bool) (a b c: padic): padic :=
+  match a, b, c with
+  | padic_seq a' a'', padic_seq b' b'', padic_seq c' c'' =>
+    padic_seq (f a' b' c') (zip3 f a'' b'' c'')
+  end.
+
+CoFixpoint zero : padic := padic_seq false zero.
+
+Definition one : padic := padic_seq true zero.
+
+CoFixpoint neg_one : padic := padic_seq true neg_one.
+
+Definition memory (p: padic) := padic_seq false p.
+
+Definition neg (p: padic) : padic := map negb p.
+
+Definition inv_memory p := neg (memory (neg p)).
+
+Definition full_add_s a b c := xorb (xorb a b) c.
+
+Definition full_add_c a b c := (a && b) || (c && (xorb a b)).
+
+Definition full_add (a b c: bool) : bool * bool :=
+  (full_add_s a b c, full_add_c a b c).
+
+CoFixpoint full_add_sum (a b c: padic) : padic :=
+  match a, b, c with
+  | padic_seq ah atl, padic_seq bh btl, padic_seq ch ctl =>
+    padic_seq (xorb (xorb ah bh) ch) (full_add_sum atl btl ctl)
+  end.
+
+CoFixpoint full_add_carry (a b c: padic) : padic :=
+  match a, b, c with
+  | padic_seq ah atl, padic_seq bh btl, padic_seq ch ctl =>
+    padic_seq ((ah && bh) || (ch && (xorb ah bh))) (full_add_carry atl btl ctl)
+  end.
+
+Definition add'' (a b: padic) : padic :=
+  zip3 full_add_s a b (memory (zip3 full_add_c a b zero)).
+
+CoFixpoint add' (c: bool) (a b: padic) : padic :=
+  match a, b with
+    padic_seq ahd atl, padic_seq bhd btl =>
+      let (s, c') := full_add ahd bhd c in
+      padic_seq s (add' c' atl btl)
+  end.
+
+Definition add : padic -> padic -> padic := add' false.
+
+Fixpoint get (n: nat) (p: padic) : list bool :=
+  match n, p with
+  | S n', padic_seq ahd atl => ahd :: get n' atl
+  | O, _ => nil
+  end.
+
+Definition negate a := add one (neg a).
+
+Goal add one neg_one = zero.
+
+
+Compute (get 4 (negate one)).
+Compute (get 4 (shuffle neg_one zero)).
+Compute (get 10 (add one neg_one)).
diff --git a/default.nix b/default.nix
new file mode 100644
index 0000000..0cec7d2
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,16 @@
+with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/269fc4ddb896c1c5994eb4bb8c750ec18cb3db82.tar.gz") {};
+let
+  ncoq = coq_8_12;
+  ncoqPackages = coqPackages_8_12;
+in
+stdenv.mkDerivation {
+  name = "padicted";
+  src = ./.;
+
+  buildInputs = [ ncoq dune_2 gcc
+                  ocaml ocamlPackages.findlib ocamlPackages.menhir
+                  ocamlPackages.ocamlgraph
+                ];
+
+  enableParallelBuilding = true;
+}
diff --git a/shell.nix b/shell.nix
new file mode 100644
index 0000000..a80b1be
--- /dev/null
+++ b/shell.nix
@@ -0,0 +1,8 @@
+with import <nixpkgs> {};
+
+mkShell {
+  buildInputs = (import ./.).buildInputs ++ [ ocamlPackages.ocp-indent
+                                              ocamlPackages.merlin ocamlPackages.utop
+                                              # (import ./.)
+                                            ];
+}