Commit bdfaa27c authored by William Mansky's avatar William Mansky

Sample program using kvnode.

parent 5a278173
# This configuration file was generated by running:
# D:\OCaml64\home\wmans\.opam\4.07.0+mingw64c\bin\coq_makefile.exe
###############################################################################
# #
# Project files. #
# #
###############################################################################
COQMF_VFILES =
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
COQMF_MLPACKFILES =
COQMF_MLLIBFILES =
COQMF_CMDLINE_VFILES =
###############################################################################
# #
# Path directives (-I, -R, -Q). #
# #
###############################################################################
COQMF_OCAMLLIBS =
COQMF_SRC_SUBDIRS =
COQMF_COQLIBS =
COQMF_COQLIBS_NOML =
COQMF_CMDLINE_COQLIBS =
###############################################################################
# #
# Coq configuration. #
# #
###############################################################################
COQMF_LOCAL=0
COQMF_COQLIB=D:\OCaml64\home\wmans\.opam\4.07.0+mingw64c/lib/coq/
COQMF_DOCDIR=D:\OCaml64\home\wmans\.opam\4.07.0+mingw64c/doc/
COQMF_OCAMLFIND=D:\OCaml64\home\wmans\.opam\4.07.0+mingw64c\bin/ocamlfind.exe
COQMF_CAMLP5O=D:/OCaml64/home/wmans/.opam/4.07.0+mingw64c/bin/camlp5o
COQMF_CAMLP5BIN=D:\OCaml64\home\wmans\.opam\4.07.0+mingw64c\bin/
COQMF_CAMLP5LIB=D:/OCaml64/home/wmans/.opam/4.07.0+mingw64c/lib/camlp5
COQMF_CAMLP5OPTIONS=-loc loc
COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50-58-59 -safe-string -strict-sequence
COQMF_HASNATDYNLINK=true
COQMF_COQ_SRC_SUBDIRS=config dev lib clib kernel library engine pretyping interp parsing proofs tactics toplevel printing grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml
COQMF_WINDRIVE=D:
###############################################################################
# #
# Extra variables. #
# #
###############################################################################
COQMF_OTHERFLAGS =
COQMF_INSTALLCOQDOCROOT = orphan_
From gpfsl.lang Require Export notation.
From gpfsl.logic Require Export new_delete for_loop.
From gpfsl.examples Require Export kvnode_code.
Notation store := 0.
Notation next := 1.
Definition push : val :=
λ: ["st"],
let: "n" := new [ #2] in
("n" + #store) <-ʳᵉˡ !(make_node []);;
("n" + #next) <-ʳᵉˡ !"st";;
"st".
Definition nth : val :=
rec: "nth" ["st"; "i"] :=
if: "i" = #0 then !ᵃᶜ("st"+ #store)
else let: "st'" := !ᵃᶜ("st" + #next) in "nth" ["st'"; "i" - #1].
Definition geti : val :=
λ: ["st"; "i"; "out"],
read [nth ["st"; "i"]; "out"].
Definition seti : val :=
λ: ["st"; "i"; "in"],
write [nth ["st"; "i"]; "in"].
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment