joelburget

(update accounts from { "balance": (- from-bal amount) })
(update accounts to   { "balance": (+ to-bal amount) })))

;; 

(update accounts "brian" { "balance": (- previous-balance 1000000) })
(update accounts "brian" { "balance": (+ previous-balance 1000000) })

joelburget

λ> main
Sat
SMTModel {modelObjectives = [], modelAssocs = [("arg1",5 :: Integer),("arg2",True :: Bool)]}

joelburget

λ> main
Sat
SMTModel {modelObjectives = [], modelAssocs = [("arg1",6 :: Integer),("arg2",0 :: Integer)]}

joelburget

❯ opam install coq
The following actions will be performed:
  ∗  install coq 8.7.1+1

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫
[default] https://opam.ocaml.org/archives/coq.8.7.1+1+opam.tar.gz downloaded

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=  🐫
[ERROR] The compilation of coq failed at "make -j4".
Processing  1/1: [coq: rm]

joelburget

~/code/coq/jscoq2 v8.7*
❯ make coq
mkdir -p coq-external coq-pkgs
git clone --depth=1 -b v8.7+vm+allow_disable https://github.com/ejgallego/coq.git coq-external/coq-v8.7+32bit || true
fatal: destination path 'coq-external/coq-v8.7+32bit' already exists and is not an empty directory.
cd coq-external/coq-v8.7+32bit && ./configure -local -native-compiler no -enable-vm no -coqide no
You have OCaml 4.06.0. Good!
You have OCamlfind 1.7.3. Good!
You have Camlp5 7.03. Good!

joelburget

~/code/coq/jscoq2 v8.7*
❯ make coq
mkdir -p coq-external coq-pkgs
git clone --depth=1 -b v8.7+vm+allow_disable https://github.com/ejgallego/coq.git coq-external/coq-v8.7+32bit || true
fatal: destination path 'coq-external/coq-v8.7+32bit' already exists and is not an empty directory.
cd coq-external/coq-v8.7+32bit && ./configure -local -native-compiler no -enable-vm no -coqide no
You have OCaml 4.06.0. Good!
You have OCamlfind 1.7.3. Good!
You have Camlp5 7.03. Good!
You have native-code compilation. Good!

joelburget

❯ ./build.sh
# To setup the new switch in the current shell, you need to run:
eval (opam config env)
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C coq-js jscoq32
CAML_LD_LIBRARY_PATH=/Users/joel/code/coq/jscoq//coq-external/coq-v8.7+32bit//kernel/byterun:/Users/joel/.opam/4.06.0+32bit/lib/stublibs \
	ocamlfind ocamlc -rectypes -safe-string  -w @a-39-44-45 -w -31 -linkall -linkpkg -thread -verbose  \
	   -package str,dynlink,threads,camlp5,camlp5.gramlib                     \
	   -package js_of_ocaml-ppx,js_of_ocaml-lwt,yojson,ppx_deriving_yojson /Users/joel/code/coq/jscoq//coq-external/coq-v8.7+32bit//lib/clib.cma /Users/joel/code/coq/jscoq//coq-external/coq-v8.7+32bit//lib/lib.cma /Users/joel/code/coq/jscoq//coq-external/coq-v8.7+32bit//intf/intf.cma /Users/joel/code/coq/jscoq//coq-external/coq-v8.7+32bit//kernel/kernel.cma /Users/joel/code/coq/jscoq//coq-external/coq-v8.7+32bit//library/library.cma /Users/joel/code/coq/jscoq//coq-external/coq-v8.7+32bit//engine/engine.cma /Users/joel/code/coq/j

joelburget

❯ ./build.sh
# To setup the new switch in the current shell, you need to run:
eval (opam config env)
/Applications/Xcode.app/Contents/Developer/usr/bin/make -C coq-js jscoq32
CAML_LD_LIBRARY_PATH=/Users/joel/code/coq/jscoq//coq-external/coq-v8.7//kernel/byterun:/Users/joel/.opam/4.06.0/lib/stublibs \
	ocamlfind ocamlc -rectypes -safe-string  -w @a-39-44-45 -w -31 -linkall -linkpkg -thread -verbose  \
	   -package str,dynlink,threads,camlp5,camlp5.gramlib                     \
	   -package js_of_ocaml-ppx,js_of_ocaml-lwt,yojson,ppx_deriving_yojson /Users/joel/code/coq/jscoq//coq-external/coq-v8.7//lib/clib.cma /Users/joel/code/coq/jscoq//coq-external/coq-v8.7//lib/lib.cma /Users/joel/code/coq/jscoq//coq-external/coq-v8.7//intf/intf.cma /Users/joel/code/coq/jscoq//coq-external/coq-v8.7//kernel/kernel.cma /Users/joel/code/coq/jscoq//coq-external/coq-v8.7//library/library.cma /Users/joel/code/coq/jscoq//coq-external/coq-v8.7//engine/engine.cma /Users/joel/code/coq/jscoq//coq-external/coq-v8.7//pretyping/pretyping

joelburget

Require Coq.Bool.Bool. Open Scope bool.
Require Coq.Strings.String. Open Scope string_scope.
Require Coq.Arith.PeanoNat. Open Scope nat_scope.
Require Coq.Lists.List. Open Scope list_scope.
Require Coq.Vectors.Vector. Open Scope vector_scope.
Require Fin.
Require Coq.Arith.EqNat.

Module Export LocalVectorNotations.
Notation " [ ] " := (Vector.nil _) (format "[ ]") : vector_scope.

joelburget

-- Use "uninterpreted" types to disallow pattern matching on constructors
type Seq :: * -> * -> *
type Tup :: * -> * -> *

-- This also doesn't work -- djinn treats them as Void
-- data Seq a b
-- data Tup a b

iden :: Seq a a
comp :: Seq a b -> Seq b c -> Seq a c