From 320510506b7b6ce30c6e4a35fb0dfc3b8cf615dc Mon Sep 17 00:00:00 2001
From: FURUHASHI Sadayuki <frsyuki@users.sourceforge.jp>
Date: Wed, 4 Jul 2012 17:40:11 -0700
Subject: [PATCH] MessagePack for OCaml moved to
https://github.com/msgpack/msgpack-ocaml
---
ocaml/.gitignore | 11 -
ocaml/OMakefile | 8 -
ocaml/OMakeroot | 45 -
ocaml/README | 1 +
ocaml/README.markdown | 22 -
ocaml/bleis-hooks/commit-msg | 14 -
ocaml/bleis-hooks/common.sh | 60 -
ocaml/bleis-hooks/pre-commit | 22 -
ocaml/ocaml/.gitignore | 2 -
ocaml/ocaml/META | 6 -
ocaml/ocaml/OMakefile | 80 -
ocaml/ocaml/base.ml | 142 --
ocaml/ocaml/config.ml | 1 -
ocaml/ocaml/hList.ml | 191 --
ocaml/ocaml/main.ml | 2 -
ocaml/ocaml/msgpack.mli | 46 -
ocaml/ocaml/msgpackCore.ml | 2581 ----------------------------
ocaml/ocaml/msgpackCore.mli | 141 --
ocaml/ocaml/pack.ml | 206 ---
ocaml/ocaml/pack.mli | 32 -
ocaml/ocaml/packTest.ml | 175 --
ocaml/ocaml/serialize.ml | 20 -
ocaml/ocaml/serialize.mli | 4 -
ocaml/ocaml/serializeTest.ml | 16 -
ocaml/proof/.gitignore | 2 -
ocaml/proof/CoqBuildRule | 14 -
ocaml/proof/DeserializeImplement.v | 630 -------
ocaml/proof/ExtractUtil.v | 95 -
ocaml/proof/ListUtil.v | 259 ---
ocaml/proof/Main.v | 3 -
ocaml/proof/MultiByte.v | 334 ----
ocaml/proof/OCamlBase.v | 8 -
ocaml/proof/OMakefile | 26 -
ocaml/proof/Object.v | 122 --
ocaml/proof/Pow.v | 162 --
ocaml/proof/Prefix.v | 674 --------
ocaml/proof/ProofUtil.v | 5 -
ocaml/proof/SerializeImplement.v | 465 -----
ocaml/proof/SerializeSpec.v | 99 --
ocaml/proof/SerializedList.v | 521 ------
ocaml/proof/Soundness.v | 623 -------
ocaml/proof/Util.v | 39 -
42 files changed, 1 insertion(+), 7908 deletions(-)
delete mode 100644 ocaml/.gitignore
delete mode 100644 ocaml/OMakefile
delete mode 100644 ocaml/OMakeroot
create mode 100644 ocaml/README
delete mode 100644 ocaml/README.markdown
delete mode 100755 ocaml/bleis-hooks/commit-msg
delete mode 100755 ocaml/bleis-hooks/common.sh
delete mode 100755 ocaml/bleis-hooks/pre-commit
delete mode 100644 ocaml/ocaml/.gitignore
delete mode 100644 ocaml/ocaml/META
delete mode 100644 ocaml/ocaml/OMakefile
delete mode 100644 ocaml/ocaml/base.ml
delete mode 100644 ocaml/ocaml/config.ml
delete mode 100644 ocaml/ocaml/hList.ml
delete mode 100644 ocaml/ocaml/main.ml
delete mode 100644 ocaml/ocaml/msgpack.mli
delete mode 100644 ocaml/ocaml/msgpackCore.ml
delete mode 100644 ocaml/ocaml/msgpackCore.mli
delete mode 100644 ocaml/ocaml/pack.ml
delete mode 100644 ocaml/ocaml/pack.mli
delete mode 100644 ocaml/ocaml/packTest.ml
delete mode 100644 ocaml/ocaml/serialize.ml
delete mode 100644 ocaml/ocaml/serialize.mli
delete mode 100644 ocaml/ocaml/serializeTest.ml
delete mode 100644 ocaml/proof/.gitignore
delete mode 100644 ocaml/proof/CoqBuildRule
delete mode 100644 ocaml/proof/DeserializeImplement.v
delete mode 100644 ocaml/proof/ExtractUtil.v
delete mode 100644 ocaml/proof/ListUtil.v
delete mode 100644 ocaml/proof/Main.v
delete mode 100644 ocaml/proof/MultiByte.v
delete mode 100644 ocaml/proof/OCamlBase.v
delete mode 100644 ocaml/proof/OMakefile
delete mode 100644 ocaml/proof/Object.v
delete mode 100644 ocaml/proof/Pow.v
delete mode 100644 ocaml/proof/Prefix.v
delete mode 100644 ocaml/proof/ProofUtil.v
delete mode 100644 ocaml/proof/SerializeImplement.v
delete mode 100644 ocaml/proof/SerializeSpec.v
delete mode 100644 ocaml/proof/SerializedList.v
delete mode 100644 ocaml/proof/Soundness.v
delete mode 100644 ocaml/proof/Util.v
diff --git a/ocaml/.gitignore b/ocaml/.gitignore
deleted file mode 100644
index fbfb0c56..00000000
--- a/ocaml/.gitignore
+++ /dev/null
@@ -1,11 +0,0 @@
-*~
-*.omc
-.omakedb
-.omakedb.lock
-*.vo
-*.glob
-*.cm[iox]
-*.o
-*.annot
-*.opt
-*.run
\ No newline at end of file
diff --git a/ocaml/OMakefile b/ocaml/OMakefile
deleted file mode 100644
index 496727d5..00000000
--- a/ocaml/OMakefile
+++ /dev/null
@@ -1,8 +0,0 @@
-NATIVE_ENABLED = true
-BYTE_ENABLED = true
-
-.PHONY: clean
-.SUBDIRS: ocaml proof
-
-clean:
- rm -rf *.vo *.glob *~ *.omc .omakedb .omakedb.lock
diff --git a/ocaml/OMakeroot b/ocaml/OMakeroot
deleted file mode 100644
index 35c219da..00000000
--- a/ocaml/OMakeroot
+++ /dev/null
@@ -1,45 +0,0 @@
-########################################################################
-# Permission is hereby granted, free of charge, to any person
-# obtaining a copy of this file, to deal in the File without
-# restriction, including without limitation the rights to use,
-# copy, modify, merge, publish, distribute, sublicense, and/or
-# sell copies of the File, and to permit persons to whom the
-# File is furnished to do so, subject to the following condition:
-#
-# THE FILE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-# OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
-# IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-# DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR
-# OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE FILE OR
-# THE USE OR OTHER DEALINGS IN THE FILE.
-
-########################################################################
-# The standard OMakeroot file.
-# You will not normally need to modify this file.
-# By default, your changes should be placed in the
-# OMakefile in this directory.
-#
-# If you decide to modify this file, note that it uses exactly
-# the same syntax as the OMakefile.
-#
-
-#
-# Include the standard installed configuration files.
-# Any of these can be deleted if you are not using them,
-# but you probably want to keep the Common file.
-#
-open build/C
-open build/OCaml
-open build/LaTeX
-
-#
-# The command-line variables are defined *after* the
-# standard configuration has been loaded.
-#
-DefineCommandVars()
-
-#
-# Include the OMakefile in this directory.
-#
-.SUBDIRS: .
diff --git a/ocaml/README b/ocaml/README
new file mode 100644
index 00000000..b6f4984e
--- /dev/null
+++ b/ocaml/README
@@ -0,0 +1 @@
+MessagePack for OCaml moved to https://github.com/msgpack/msgpack-ocaml.
diff --git a/ocaml/README.markdown b/ocaml/README.markdown
deleted file mode 100644
index c62c25e5..00000000
--- a/ocaml/README.markdown
+++ /dev/null
@@ -1,22 +0,0 @@
-MsgPack for OCaml
-==============================
-
-See http://wiki.msgpack.org/display/MSGPACK/QuickStart+for+OCaml
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/ocaml/bleis-hooks/commit-msg b/ocaml/bleis-hooks/commit-msg
deleted file mode 100755
index 38d4baf7..00000000
--- a/ocaml/bleis-hooks/commit-msg
+++ /dev/null
@@ -1,14 +0,0 @@
-#! /bin/sh
-
-if [ -n "${GIT_DIR}" ]; then
- hooksdir="./${GIT_DIR}/hooks/"
-else
- hooksdir="./"
-fi
-
-. "${hooksdir}common.sh"
-
-ticket="$(extractTicketId)"
-if [ -n "${ticket}" ]; then
- appendMsgTo1stLine "$1" "${ticket}"
-fi
diff --git a/ocaml/bleis-hooks/common.sh b/ocaml/bleis-hooks/common.sh
deleted file mode 100755
index 556e74eb..00000000
--- a/ocaml/bleis-hooks/common.sh
+++ /dev/null
@@ -1,60 +0,0 @@
-#! /bin/sh
-
-getGitBranchName()
-{
- branch="$(git symbolic-ref HEAD 2>/dev/null)" ||
- "$(git describe --contains --all HEAD)"
- echo ${branch##refs/heads/}
-}
-
-isOnMasterBranch()
-{
- if [ "$(getGitBranchName)" = "master" ]; then
- return 0
- fi
- return 1
-}
-
-appendMsgTo1stLine()
-{
- mv $1 $1.$$
- if [ -s "$1.$$" ]; then
- if head -1 "$1.$$" | grep "$2" > /dev/null; then
- cp "$1.$$" "$1"
- else
- sed '1s/$/ '"$2"'/' "$1.$$" > $1
- fi
- else
- echo "$2" > "$1"
- fi
- rm -f $1.$$
-}
-
-extractTicketId()
-{
- echo "$(getGitBranchName)" \
- | awk 'BEGIN{ FS="[/]"}
- $1 == "id" { printf "refs #%s", $2 }
- $2 == "id" { printf "refs #%s", $3 }'
-}
-
-hasTicketId()
-{
- first="$(git cat-file -p $1 \
- | sed '1,/^$/d' | head -1 \
- | sed '/.*refs #[0-9][0-9]*.*/!d')"
-
- if [ -n "${first}" ]; then
- echo "true"
- else
- echo "false"
- fi
-}
-
-extractParents()
-{
- parents="$(git cat-file -p $1 \
- | grep '^parent [0-9a-f]\{40\}$')"
- echo "${parents##parent }"
-}
-
diff --git a/ocaml/bleis-hooks/pre-commit b/ocaml/bleis-hooks/pre-commit
deleted file mode 100755
index 9b7766bc..00000000
--- a/ocaml/bleis-hooks/pre-commit
+++ /dev/null
@@ -1,22 +0,0 @@
-#! /bin/sh
-
-if [ -z "$(git branch)" ]; then
- exit 0
-fi
-
-if [ -n "${GIT_DIR}" ]; then
- hooksdir="./${GIT_DIR}/hooks/"
-else
- hooksdir="./"
-fi
-
-. "${hooksdir}common.sh"
-
-isOnMasterBranch
-if [ $? -eq 0 ]; then
- echo "can't commit on master branch."
- echo "please commit on topic branch."
- exit 1
-fi
-
-exit 0
diff --git a/ocaml/ocaml/.gitignore b/ocaml/ocaml/.gitignore
deleted file mode 100644
index e60d7ce4..00000000
--- a/ocaml/ocaml/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-runner
-doc
diff --git a/ocaml/ocaml/META b/ocaml/ocaml/META
deleted file mode 100644
index 1170b98f..00000000
--- a/ocaml/ocaml/META
+++ /dev/null
@@ -1,6 +0,0 @@
-name="msgpack"
-version="0.1.0"
-description="a library for MessagePack."
-requires="extlib, num"
-archive(byte)="msgpack.cmo"
-archive(native)="msgpack.cmx"
\ No newline at end of file
diff --git a/ocaml/ocaml/OMakefile b/ocaml/ocaml/OMakefile
deleted file mode 100644
index a438b483..00000000
--- a/ocaml/ocaml/OMakefile
+++ /dev/null
@@ -1,80 +0,0 @@
-.PHONY: all clean check doc install
-
-# ------------------------------
-# camlp4
-# ------------------------------
-public.UseCamlp4(files) =
- protected.CAMLP4CMO = $(addprefix $(ROOT)/camlp4/,$(addsuffix .cmo,$(files)))
- OCAMLPPFLAGS+=-pp 'camlp4o $(CAMLP4CMO)'
- OCAMLDEPFLAGS+=-pp 'camlp4o $(CAMLP4CMO)'
- export
- .SCANNER: scan-ocaml-%.ml: %.ml $(CAMLP4CMO)
-
-# ------------------------------
-# findlib
-# ------------------------------
-USE_OCAMLFIND = true
-
-if $(not $(OCAMLFIND_EXISTS))
- eprintln('This project requires ocamlfind, but is was not found.')
- eprintln('You need to install ocamlfind and run "omake --configure".')
- exit 1
-
-OCAMLPACKS[] =
- oUnit
- extlib
- num
-
-OCAML_WARN_FLAGS=$`(if $(equal $<,msgpackCore.ml),-annot,-w A -warn-error A ) #`
-OCAMLFLAGS=$(OCAML_WARN_FLAGS) -annot
-# ------------------------------
-# library
-# ------------------------------
-FILES[] =
- pack
- base
- hList
- msgpackCore
- serialize
- config
-
-msgpackCore.ml : ../proof/msgpackCore.ml
- cp $^ $@
-
-msgpackCore.mli : ../proof/msgpackCore.mli
- cp $^ $@
-
-# ------------------------------
-# test code
-# ------------------------------
-TEST_FILES[] =
- packTest
- serializeTest
-
-TEST_PROGRAM = runner
-
-# ------------------------------
-# build rule
-# ------------------------------
-PROGRAM = msgpack
-OCAMLLINK = $(OCAMLC)
-OCAMLOPTLINK = $(OCAMLOPT)
-OCAMLC += -for-pack $(capitalize $(PROGRAM))
-OCAMLOPT += -for-pack $(capitalize $(PROGRAM))
-
-.DEFAULT: all
-
-all : $(OCamlPackage $(PROGRAM), $(FILES))
-
-check : $(OCamlProgram $(TEST_PROGRAM), $(TEST_FILES) $(FILES))
- ./$(TEST_PROGRAM)
-
-doc:
- mkdir -p doc
- ocamldoc -d doc -html msgpack.mli
-
-install: all
- ocamlfind install msgpack META *.cmo *.cmx *.cmi
-
-clean:
- rm -rf *.cm[iox] *.o *~ *.omc .omakedb .omakedb.lock *.cmxa *.a *.opt *.run *.annot runner msgpackCore.*
diff --git a/ocaml/ocaml/base.ml b/ocaml/ocaml/base.ml
deleted file mode 100644
index e1ccdde5..00000000
--- a/ocaml/ocaml/base.ml
+++ /dev/null
@@ -1,142 +0,0 @@
-let (@@) f g = f g
-let (+>) f g = g f
-let ($) f g x = f (g x)
-let (!$) = Lazy.force
-external id : 'a -> 'a = "%identity"
-
-let uncurry f a b = f (a,b)
-let curry f (a,b) = f a b
-let flip f a b = f b a
-let const a _ = a
-
-let sure f =
- function
- Some x ->
- Some (f x)
- | None ->
- None
-
-let option f x = try Some (f x) with Not_found -> None
-let maybe f x = try `Val (f x) with e -> `Error e
-let tee f x = try ignore @@ f x; x with _ -> x
-
-type ('a,'b) either = Left of 'a | Right of 'b
-let left x = Left x
-let right x = Right x
-
-let failwithf fmt = Printf.kprintf (fun s () -> failwith s) fmt
-
-let lookup x xs = (option @@ List.assoc x) xs
-
-let string_of_list xs =
- Printf.sprintf "[%s]"
- @@ String.concat ";" xs
-
-let rec unfold f init =
- match f init with
- Some (a, b) -> a :: unfold f b
- | None -> []
-
-let rec range a b =
- if a >= b then
- []
- else
- a::range (a+1) b
-
-let rec interperse delim =
- function
- [] -> []
- | [x] -> [x]
- | x::xs -> x::delim::interperse delim xs
-
-let map_accum_left f init xs =
- let f (accum,ys) x =
- let accum',y =
- f accum x in
- (accum',y::ys) in
- let accum,ys =
- List.fold_left f (init,[]) xs in
- accum,List.rev ys
-
-let rec map_accum_right f init =
- function
- [] ->
- init,[]
- | x::xs ->
- let (accum,ys) =
- map_accum_right f init xs in
- let (accum,y) =
- f accum x in
- accum,y::ys
-
-let rec filter_map f =
- function
- x::xs ->
- begin match f x with
- Some y -> y::filter_map f xs
- | None -> filter_map f xs
- end
- | [] ->
- []
-
-let rec group_by f =
- function
- [] ->
- []
- | x1::x2::xs when f x1 x2 ->
- begin match group_by f @@ x2::xs with
- y::ys ->
- (x1::y)::ys
- | _ ->
- failwith "must not happen"
- end
- | x::xs ->
- [x]::group_by f xs
-
-let index x xs =
- let rec loop i = function
- [] ->
- raise Not_found
- | y::ys ->
- if x = y then
- i
- else
- loop (i+1) ys in
- loop 0 xs
-
-let string_of_char =
- String.make 1
-
-let hex =
- Printf.sprintf "0x%x"
-
-let open_out_with path f =
- let ch =
- open_out_bin path in
- maybe f ch
- +> tee (fun _ -> close_out ch)
- +> function
- `Val v -> v
- | `Error e -> raise e
-
-let open_in_with path f =
- let ch =
- open_in_bin path in
- maybe f ch
- +> tee (fun _ -> close_in ch)
- +> function
- `Val v -> v
- | `Error e -> raise e
-
-let forever f () =
- while true do
- f ()
- done
-
-let undefined = Obj.magic 42
-let undef = undefined
-
-let p fmt = Printf.kprintf (fun s () -> print_endline s; flush stdout) fmt
-
-let ret x _ =
- x
diff --git a/ocaml/ocaml/config.ml b/ocaml/ocaml/config.ml
deleted file mode 100644
index 9a6723a5..00000000
--- a/ocaml/ocaml/config.ml
+++ /dev/null
@@ -1 +0,0 @@
-let version = (1,0,0)
diff --git a/ocaml/ocaml/hList.ml b/ocaml/ocaml/hList.ml
deleted file mode 100644
index 732a6f10..00000000
--- a/ocaml/ocaml/hList.ml
+++ /dev/null
@@ -1,191 +0,0 @@
-open Base
-
-let rec last =
- function
- [] ->
- invalid_arg "HList.last"
- | [x] ->
- x
- | _::xs ->
- last xs
-
-let init xs =
- let rec init' ys =
- function
- [] ->
- invalid_arg "HList.init"
- | [_] ->
- List.rev ys
- | x::xs ->
- init' (x::ys) xs in
- init' [] xs
-
-let null =
- function
- [] ->
- true
- | _ ->
- false
-
-let fold_left1 f =
- function
- [] ->
- invalid_arg "HList.fold_left1"
- | x::xs ->
- List.fold_left f x xs
-
-let rec fold_right1 f =
- function
- [] ->
- invalid_arg "HList.fold_right1"
- | [x] ->
- x
- | x::xs ->
- f x (fold_right1 f xs)
-
-let conj =
- List.fold_left (&&) true
-
-let disj =
- List.fold_left (||) false
-
-let sum =
- List.fold_left (+) 0
-
-let product =
- List.fold_left ( * ) 1
-
-let concat_map f xs =
- List.fold_right ((@) $ f) xs []
-
-let maximum xs =
- fold_left1 max xs
-
-let minimum xs =
- fold_left1 min xs
-
-let rec scanl f y =
- function
- [] ->
- [y]
- | x::xs ->
- y::scanl f (f y x) xs
-
-let scanl1 f =
- function
- [] ->
- []
- | x::xs ->
- scanl f x xs
-
-let rec scanr f z =
- function
- [] ->
- [z]
- | x::xs ->
- match scanr f z xs with
- y::_ as yss ->
- (f x y) :: yss
- | _ ->
- failwith "must not happen"
-
-let scanr1 f =
- function
- [] ->
- []
- | x::xs ->
- scanr f x xs
-
-let replicate n x =
- let rec loop i ys =
- if i = 0 then
- ys
- else
- loop (i-1) (x::ys) in
- loop n []
-
-let rec take n =
- function
- [] ->
- []
- | x::xs ->
- if n <= 0 then
- []
- else
- x :: take (n - 1) xs
-
-let rec drop n =
- function
- [] ->
- []
- | xs when n <= 0 ->
- xs
- | _::xs ->
- drop (n-1) xs
-
-let rec splitAt n xs =
- match n,xs with
- 0,_ | _,[] ->
- [],xs
- | _,y::ys ->
- let p,q =
- splitAt (n-1) ys in
- y::p,q
-
-let rec takeWhile f =
- function
- x::xs when f x ->
- x :: takeWhile f xs
- | _ ->
- []
-
-let rec dropWhile f =
- function
- x::xs when f x ->
- dropWhile f xs
- | xs ->
- xs
-
-let rec span f =
- function
- x::xs when f x ->
- let ys,zs =
- span f xs in
- x::ys,zs
- | xs ->
- [],xs
-
-let break f =
- span (not $ f)
-
-let rec zip_with f xs ys =
- match xs,ys with
- [],_ | _,[] ->
- []
- | x::xs',y::ys' ->
- (f x y)::zip_with f xs' ys'
-
-let rec zip_with3 f xs ys zs =
- match xs,ys,zs with
- [],_,_ | _,[],_ | _,_,[] ->
- []
- | x::xs',y::ys',z::zs' ->
- (f x y z)::zip_with3 f xs' ys' zs'
-
-let zip xs ys =
- zip_with (fun x y -> (x,y)) xs ys
-
-let zip3 xs ys zs =
- zip_with3 (fun x y z -> (x,y,z)) xs ys zs
-
-let unzip xs =
- List.fold_right (fun (x,y) (xs,ys) -> (x::xs,y::ys)) xs ([],[])
-
-let unzip3 xs =
- List.fold_right (fun (x,y,z) (xs,ys,zs) -> (x::xs,y::ys,z::zs)) xs ([],[],[])
-
-let lookup x xs =
- try
- Some (List.assoc x xs)
- with Not_found ->
- None
diff --git a/ocaml/ocaml/main.ml b/ocaml/ocaml/main.ml
deleted file mode 100644
index f7c81958..00000000
--- a/ocaml/ocaml/main.ml
+++ /dev/null
@@ -1,2 +0,0 @@
-let _ =
- print_endline "hello"
diff --git a/ocaml/ocaml/msgpack.mli b/ocaml/ocaml/msgpack.mli
deleted file mode 100644
index cd227da5..00000000
--- a/ocaml/ocaml/msgpack.mli
+++ /dev/null
@@ -1,46 +0,0 @@
-(** MessagePack for OCaml *)
-
-(** Conversion MessagePack object between OCaml and Coq. *)
-module Pack : sig
- (** exception when MesagePack object is invalid form *)
- exception Not_conversion of string
-end
-
-(** MessagePack Serializer *)
-module Serialize : sig
- (** MesagePack object. See also {{:http://redmine.msgpack.org/projects/msgpack/wiki/FormatSpec}MessagePack specification}. *)
- type t =
- [ `Bool of bool
- | `Nil
- | `PFixnum of int
- | `NFixnum of int
- | `Uint8 of int
- | `Uint16 of int
- | `Uint32 of int64
- | `Uint64 of Big_int.big_int
- | `Int8 of int
- | `Int16 of int
- | `Int32 of int32
- | `Int64 of int64
- | `Float of float
- | `Double of float
- | `FixRaw of char list
- | `Raw16 of char list
- | `Raw32 of char list
- | `FixArray of t list
- | `Array16 of t list
- | `Array32 of t list
- | `FixMap of (t * t) list
- | `Map16 of (t * t) list
- | `Map32 of (t * t) list ]
-
- (** [MessagePack.Serialize.deserialize_string str] deserialize MessagePack string [str] to MessagePack object. *)
- val deserialize_string : string -> t
-
- (** [MessagePack.Serialize.serialize_string obj] serialize MessagePack object [obj] to MessagePack string. *)
- val serialize_string : t -> string
-end
-
-module Config : sig
- val version : int * int * int
-end
diff --git a/ocaml/ocaml/msgpackCore.ml b/ocaml/ocaml/msgpackCore.ml
deleted file mode 100644
index 4f9303b7..00000000
--- a/ocaml/ocaml/msgpackCore.ml
+++ /dev/null
@@ -1,2581 +0,0 @@
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-
-(** val fst : ('a1 * 'a2) -> 'a1 **)
-
-let fst = function
- | (x, y) -> x
-
-(** val snd : ('a1 * 'a2) -> 'a2 **)
-
-let snd = function
- | (x, y) -> y
-
-(** val length : 'a1 list -> int **)
-
-let rec length = function
- | [] -> 0
- | y::l' -> succ (length l')
-
-(** val app : 'a1 list -> 'a1 list -> 'a1 list **)
-
-let rec app l m =
- match l with
- | [] -> m
- | a::l1 -> a::(app l1 m)
-
-(** val plus : int -> int -> int **)
-
-let rec plus = (+)
-
-(** val mult : int -> int -> int **)
-
-let rec mult = ( * )
-
-type positive =
- | XI of positive
- | XO of positive
- | XH
-
-(** val psucc : positive -> positive **)
-
-let rec psucc = function
- | XI p -> XO (psucc p)
- | XO p -> XI p
- | XH -> XO XH
-
-(** val pplus : positive -> positive -> positive **)
-
-let rec pplus x y =
- match x with
- | XI p ->
- (match y with
- | XI q -> XO (pplus_carry p q)
- | XO q -> XI (pplus p q)
- | XH -> XO (psucc p))
- | XO p ->
- (match y with
- | XI q -> XI (pplus p q)
- | XO q -> XO (pplus p q)
- | XH -> XI p)
- | XH ->
- (match y with
- | XI q -> XO (psucc q)
- | XO q -> XI q
- | XH -> XO XH)
-
-(** val pplus_carry : positive -> positive -> positive **)
-
-and pplus_carry x y =
- match x with
- | XI p ->
- (match y with
- | XI q -> XI (pplus_carry p q)
- | XO q -> XO (pplus_carry p q)
- | XH -> XI (psucc p))
- | XO p ->
- (match y with
- | XI q -> XO (pplus_carry p q)
- | XO q -> XI (pplus p q)
- | XH -> XO (psucc p))
- | XH ->
- (match y with
- | XI q -> XI (psucc q)
- | XO q -> XO (psucc q)
- | XH -> XI XH)
-
-(** val pmult_nat : positive -> int -> int **)
-
-let rec pmult_nat x pow2 =
- match x with
- | XI p -> plus pow2 (pmult_nat p (plus pow2 pow2))
- | XO p -> pmult_nat p (plus pow2 pow2)
- | XH -> pow2
-
-(** val nat_of_P : positive -> int **)
-
-let nat_of_P x =
- pmult_nat x (succ 0)
-
-(** val p_of_succ_nat : int -> positive **)
-
-let rec p_of_succ_nat n0 =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
- (fun _ -> XH)
- (fun x -> psucc (p_of_succ_nat x))
- n0
-
-(** val pmult : positive -> positive -> positive **)
-
-let rec pmult x y =
- match x with
- | XI p -> pplus y (XO (pmult p y))
- | XO p -> XO (pmult p y)
- | XH -> y
-
-type n =
- | N0
- | Npos of positive
-
-(** val nplus : n -> n -> n **)
-
-let nplus n0 m =
- match n0 with
- | N0 -> m
- | Npos p -> (match m with
- | N0 -> n0
- | Npos q -> Npos (pplus p q))
-
-(** val nmult : n -> n -> n **)
-
-let nmult n0 m =
- match n0 with
- | N0 -> N0
- | Npos p -> (match m with
- | N0 -> N0
- | Npos q -> Npos (pmult p q))
-
-(** val nat_of_N : n -> int **)
-
-let nat_of_N = function
- | N0 -> 0
- | Npos p -> nat_of_P p
-
-(** val n_of_nat : int -> n **)
-
-let n_of_nat n0 =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
- (fun _ -> N0)
- (fun n' -> Npos (p_of_succ_nat n'))
- n0
-
-(** val flat_map : ('a1 -> 'a2 list) -> 'a1 list -> 'a2 list **)
-
-let rec flat_map f = function
- | [] -> []
- | x::t -> app (f x) (flat_map f t)
-
-(** val eucl_dev : int -> int -> (int * int) **)
-
-let eucl_dev = fun n m -> (m/n, m mod n)
-
-type ascii =
- | Ascii of bool * bool * bool * bool * bool * bool * bool * bool
-
-(** val zero : ascii **)
-
-let zero =
- Ascii (false, false, false, false, false, false, false, false)
-
-(** val one : ascii **)
-
-let one =
- Ascii (true, false, false, false, false, false, false, false)
-
-(** val shift : bool -> ascii -> ascii **)
-
-let shift c = function
- | Ascii (a1, a2, a3, a4, a5, a6, a7, a8) -> Ascii (c, a1, a2, a3, a4, a5,
- a6, a7)
-
-(** val ascii_of_pos : positive -> ascii **)
-
-let ascii_of_pos =
- let rec loop n0 p =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
- (fun _ -> zero)
- (fun n' ->
- match p with
- | XI p' -> shift true (loop n' p')
- | XO p' -> shift false (loop n' p')
- | XH -> one)
- n0
- in loop (succ (succ (succ (succ (succ (succ (succ (succ 0))))))))
-
-(** val ascii_of_N : n -> ascii **)
-
-let ascii_of_N = function
- | N0 -> zero
- | Npos p -> ascii_of_pos p
-
-(** val ascii_of_nat : int -> ascii **)
-
-let ascii_of_nat a =
- ascii_of_N (n_of_nat a)
-
-(** val n_of_digits : bool list -> n **)
-
-let rec n_of_digits = function
- | [] -> N0
- | b::l' ->
- nplus (if b then Npos XH else N0)
- (nmult (Npos (XO XH)) (n_of_digits l'))
-
-(** val n_of_ascii : ascii -> n **)
-
-let n_of_ascii = function
- | Ascii (a0, a1, a2, a3, a4, a5, a6, a7) ->
- n_of_digits (a0::(a1::(a2::(a3::(a4::(a5::(a6::(a7::[]))))))))
-
-(** val nat_of_ascii : ascii -> int **)
-
-let nat_of_ascii a =
- nat_of_N (n_of_ascii a)
-
-(** val take : int -> 'a1 list -> 'a1 list **)
-
-let rec take n0 xs =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
- (fun _ -> [])
- (fun m -> match xs with
- | [] -> []
- | x::xs0 -> x::(take m xs0))
- n0
-
-(** val drop : int -> 'a1 list -> 'a1 list **)
-
-let rec drop n0 xs =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
- (fun _ -> xs)
- (fun m -> match xs with
- | [] -> []
- | x::xs0 -> drop m xs0)
- n0
-
-(** val split_at : int -> 'a1 list -> 'a1 list * 'a1 list **)
-
-let split_at n0 xs =
- ((take n0 xs), (drop n0 xs))
-
-(** val pair : 'a1 list -> ('a1 * 'a1) list **)
-
-let rec pair = function
- | [] -> []
- | k::l -> (match l with
- | [] -> []
- | v::ys -> (k, v)::(pair ys))
-
-(** val pow : int -> int **)
-
-let rec pow n0 =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
- (fun _ -> succ 0)
- (fun n' -> mult (succ (succ 0)) (pow n'))
- n0
-
-(** val divmod : int -> int -> (int * int) **)
-
-let divmod n0 m =
- eucl_dev m n0
-
-type ascii8 = ascii
-
-type ascii16 = ascii8 * ascii8
-
-type ascii32 = ascii16 * ascii16
-
-type ascii64 = ascii32 * ascii32
-
-(** val nat_of_ascii8 : ascii -> int **)
-
-let nat_of_ascii8 =
- nat_of_ascii
-
-(** val ascii8_of_nat : int -> ascii **)
-
-let ascii8_of_nat =
- ascii_of_nat
-
-(** val ascii16_of_nat : int -> ascii * ascii **)
-
-let ascii16_of_nat a =
- let (q, r) =
- divmod a (pow (succ (succ (succ (succ (succ (succ (succ (succ 0)))))))))
- in
- ((ascii8_of_nat q), (ascii8_of_nat r))
-
-(** val nat_of_ascii16 : ascii16 -> int **)
-
-let nat_of_ascii16 = function
- | (a1, a2) ->
- plus
- (mult (nat_of_ascii8 a1)
- (pow (succ (succ (succ (succ (succ (succ (succ (succ 0))))))))))
- (nat_of_ascii8 a2)
-
-(** val ascii32_of_nat : int -> (ascii * ascii) * (ascii * ascii) **)
-
-let ascii32_of_nat a =
- let (q, r) =
- divmod a
- (pow (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ
- (succ (succ (succ (succ (succ 0)))))))))))))))))
- in
- ((ascii16_of_nat q), (ascii16_of_nat r))
-
-(** val nat_of_ascii32 : ascii32 -> int **)
-
-let nat_of_ascii32 = function
- | (a1, a2) ->
- plus
- (mult (nat_of_ascii16 a1)
- (pow (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ
- (succ (succ (succ (succ (succ (succ 0))))))))))))))))))
- (nat_of_ascii16 a2)
-
-(** val list_of_ascii8 : ascii8 -> ascii8 list **)
-
-let list_of_ascii8 x =
- x::[]
-
-(** val list_of_ascii16 : ascii16 -> ascii8 list **)
-
-let list_of_ascii16 = function
- | (x1, x2) -> app (list_of_ascii8 x1) (list_of_ascii8 x2)
-
-(** val list_of_ascii32 : ascii32 -> ascii8 list **)
-
-let list_of_ascii32 = function
- | (x1, x2) -> app (list_of_ascii16 x1) (list_of_ascii16 x2)
-
-(** val list_of_ascii64 : ascii64 -> ascii8 list **)
-
-let list_of_ascii64 = function
- | (x1, x2) -> app (list_of_ascii32 x1) (list_of_ascii32 x2)
-
-type object0 =
- | Bool of bool
- | Nil
- | PFixnum of ascii8
- | NFixnum of ascii8
- | Uint8 of ascii8
- | Uint16 of ascii16
- | Uint32 of ascii32
- | Uint64 of ascii64
- | Int8 of ascii8
- | Int16 of ascii16
- | Int32 of ascii32
- | Int64 of ascii64
- | Float of ascii32
- | Double of ascii64
- | FixRaw of ascii8 list
- | Raw16 of ascii8 list
- | Raw32 of ascii8 list
- | FixArray of object0 list
- | Array16 of object0 list
- | Array32 of object0 list
- | FixMap of (object0 * object0) list
- | Map16 of (object0 * object0) list
- | Map32 of (object0 * object0) list
-
-(** val atat : ('a1 -> 'a2) -> 'a1 -> 'a2 **)
-
-let atat f x =
- f x
-
-(** val serialize : object0 -> ascii8 list **)
-
-let rec serialize = function
- | Bool b ->
- if b
- then (Ascii (true, true, false, false, false, false, true, true))::[]
- else (Ascii (false, true, false, false, false, false, true, true))::[]
- | Nil -> (Ascii (false, false, false, false, false, false, true, true))::[]
- | PFixnum a ->
- let Ascii (b1, b2, b3, b4, b5, b6, b7, b) = a in
- (Ascii (b1, b2, b3, b4, b5, b6, b7, false))::[]
- | NFixnum a ->
- let Ascii (b1, b2, b3, b4, b5, b, b0, b6) = a in
- (Ascii (b1, b2, b3, b4, b5, true, true, true))::[]
- | Uint8 c -> (Ascii (false, false, true, true, false, false, true,
- true))::(list_of_ascii8 c)
- | Uint16 c -> (Ascii (true, false, true, true, false, false, true,
- true))::(list_of_ascii16 c)
- | Uint32 c -> (Ascii (false, true, true, true, false, false, true,
- true))::(list_of_ascii32 c)
- | Uint64 c -> (Ascii (true, true, true, true, false, false, true,
- true))::(list_of_ascii64 c)
- | Int8 c -> (Ascii (false, false, false, false, true, false, true,
- true))::(list_of_ascii8 c)
- | Int16 c -> (Ascii (true, false, false, false, true, false, true,
- true))::(list_of_ascii16 c)
- | Int32 c -> (Ascii (false, true, false, false, true, false, true,
- true))::(list_of_ascii32 c)
- | Int64 c -> (Ascii (true, true, false, false, true, false, true,
- true))::(list_of_ascii64 c)
- | Float c -> (Ascii (false, true, false, true, false, false, true,
- true))::(list_of_ascii32 c)
- | Double c -> (Ascii (true, true, false, true, false, false, true,
- true))::(list_of_ascii64 c)
- | FixRaw xs ->
- let Ascii (b1, b2, b3, b4, b5, b, b0, b6) =
- atat ascii8_of_nat (length xs)
- in
- (Ascii (b1, b2, b3, b4, b5, true, false, true))::xs
- | Raw16 xs ->
- let (s1, s2) = atat ascii16_of_nat (length xs) in
- (Ascii (false, true, false, true, true, false, true,
- true))::(s1::(s2::xs))
- | Raw32 xs ->
- let (p, p0) = atat ascii32_of_nat (length xs) in
- let (s1, s2) = p in
- let (s3, s4) = p0 in
- (Ascii (true, true, false, true, true, false, true,
- true))::(s1::(s2::(s3::(s4::xs))))
- | FixArray xs ->
- let ys = flat_map serialize xs in
- let Ascii (b1, b2, b3, b4, b, b0, b5, b6) =
- atat ascii8_of_nat (length xs)
- in
- (Ascii (b1, b2, b3, b4, true, false, false, true))::ys
- | Array16 xs ->
- let ys = flat_map serialize xs in
- let (s1, s2) = ascii16_of_nat (length xs) in
- (Ascii (false, false, true, true, true, false, true,
- true))::(s1::(s2::ys))
- | Array32 xs ->
- let ys = flat_map serialize xs in
- let (p, p0) = atat ascii32_of_nat (length xs) in
- let (s1, s2) = p in
- let (s3, s4) = p0 in
- (Ascii (true, false, true, true, true, false, true,
- true))::(s1::(s2::(s3::(s4::ys))))
- | FixMap xs ->
- let ys =
- flat_map (fun p -> app (serialize (fst p)) (serialize (snd p))) xs
- in
- let Ascii (b1, b2, b3, b4, b, b0, b5, b6) =
- atat ascii8_of_nat (length xs)
- in
- (Ascii (b1, b2, b3, b4, false, false, false, true))::ys
- | Map16 xs ->
- let ys =
- flat_map (fun p -> app (serialize (fst p)) (serialize (snd p))) xs
- in
- let (s1, s2) = ascii16_of_nat (length xs) in
- (Ascii (false, true, true, true, true, false, true,
- true))::(s1::(s2::ys))
- | Map32 xs ->
- let ys =
- flat_map (fun p -> app (serialize (fst p)) (serialize (snd p))) xs
- in
- let (p, p0) = atat ascii32_of_nat (length xs) in
- let (s1, s2) = p in
- let (s3, s4) = p0 in
- (Ascii (true, true, true, true, true, false, true,
- true))::(s1::(s2::(s3::(s4::ys))))
-
-(** val compact : object0 list -> ascii8 list **)
-
-let compact xs =
- flat_map (fun x -> match x with
- | FixRaw xs0 -> xs0
- | _ -> []) xs
-
-(** val deserialize : int -> ascii8 list -> object0 list **)
-
-let rec deserialize n0 xs =
- (fun fO fS n -> if n=0 then fO () else fS (n-1))
- (fun _ ->
- match xs with
- | [] -> []
- | a::ys ->
- let Ascii (b1, b2, b3, b4, b5, b6, b7, b) = a in
- if b1
- then if b2
- then if b3
- then if b4
- then if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- s1::l ->
- (match l with
- |
- [] -> []
- |
- s2::l0 ->
- (match l0 with
- |
- [] -> []
- |
- s3::l1 ->
- (match l1 with
- |
- [] -> []
- |
- s4::ys0 ->
- let n1 =
- nat_of_ascii32 ((s1, s2),
- (s3, s4))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys0)
- in
- (Map32 (pair zs))::ws))))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- c1::l ->
- (match l with
- |
- [] -> []
- |
- c2::l0 ->
- (match l0 with
- |
- [] -> []
- |
- c3::l1 ->
- (match l1 with
- |
- [] -> []
- |
- c4::l2 ->
- (match l2 with
- |
- [] -> []
- |
- c5::l3 ->
- (match l3 with
- |
- [] -> []
- |
- c6::l4 ->
- (match l4 with
- |
- [] -> []
- |
- c7::l5 ->
- (match l5 with
- |
- [] -> []
- |
- c8::ys0 -> (Uint64 (((c1,
- c2), (c3, c4)), ((c5, c6),
- (c7,
- c8))))::
- (deserialize 0 ys0)))))))))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b4
- then if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- s1::l ->
- (match l with
- |
- [] -> []
- |
- s2::l0 ->
- (match l0 with
- |
- [] -> []
- |
- s3::l1 ->
- (match l1 with
- |
- [] -> []
- |
- s4::ys0 ->
- let n1 =
- nat_of_ascii32 ((s1, s2),
- (s3, s4))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys0)
- in
- (Raw32 (compact zs))::ws))))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- c1::l ->
- (match l with
- |
- [] -> []
- |
- c2::l0 ->
- (match l0 with
- |
- [] -> []
- |
- c3::l1 ->
- (match l1 with
- |
- [] -> []
- |
- c4::l2 ->
- (match l2 with
- |
- [] -> []
- |
- c5::l3 ->
- (match l3 with
- |
- [] -> []
- |
- c6::l4 ->
- (match l4 with
- |
- [] -> []
- |
- c7::l5 ->
- (match l5 with
- |
- [] -> []
- |
- c8::ys0 -> (Double (((c1,
- c2), (c3, c4)), ((c5, c6),
- (c7,
- c8))))::
- (deserialize 0 ys0)))))))))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- c1::l ->
- (match l with
- |
- [] -> []
- |
- c2::l0 ->
- (match l0 with
- |
- [] -> []
- |
- c3::l1 ->
- (match l1 with
- |
- [] -> []
- |
- c4::l2 ->
- (match l2 with
- |
- [] -> []
- |
- c5::l3 ->
- (match l3 with
- |
- [] -> []
- |
- c6::l4 ->
- (match l4 with
- |
- [] -> []
- |
- c7::l5 ->
- (match l5 with
- |
- [] -> []
- |
- c8::ys0 -> (Int64 (((c1,
- c2), (c3, c4)), ((c5, c6),
- (c7,
- c8))))::
- (deserialize 0 ys0)))))))))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (Bool
- true)::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b3
- then if b4
- then if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- s1::l ->
- (match l with
- |
- [] -> []
- |
- s2::l0 ->
- (match l0 with
- |
- [] -> []
- |
- s3::l1 ->
- (match l1 with
- |
- [] -> []
- |
- s4::ys0 ->
- let n1 =
- nat_of_ascii32 ((s1, s2),
- (s3, s4))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys0)
- in
- (Array32 zs)::ws))))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- c1::l ->
- (match l with
- |
- [] -> []
- |
- c2::ys0 -> (Uint16 (c1,
- c2))::
- (deserialize 0 ys0)))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b4
- then if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- c1::l ->
- (match l with
- |
- [] -> []
- |
- c2::ys0 -> (Int16 (c1,
- c2))::
- (deserialize 0 ys0)))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b2
- then if b3
- then if b4
- then if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- s1::l ->
- (match l with
- |
- [] -> []
- |
- s2::ys0 ->
- let n1 =
- nat_of_ascii16 (s1, s2)
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys0)
- in
- (Map16 (pair zs))::ws))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- c1::l ->
- (match l with
- |
- [] -> []
- |
- c2::l0 ->
- (match l0 with
- |
- [] -> []
- |
- c3::l1 ->
- (match l1 with
- |
- [] -> []
- |
- c4::ys0 -> (Uint32 ((c1,
- c2), (c3,
- c4)))::
- (deserialize 0 ys0)))))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b4
- then if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- s1::l ->
- (match l with
- |
- [] -> []
- |
- s2::ys0 ->
- let n1 =
- nat_of_ascii16 (s1, s2)
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys0)
- in
- (Raw16 (compact zs))::ws))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- c1::l ->
- (match l with
- |
- [] -> []
- |
- c2::l0 ->
- (match l0 with
- |
- [] -> []
- |
- c3::l1 ->
- (match l1 with
- |
- [] -> []
- |
- c4::ys0 -> (Float ((c1,
- c2), (c3,
- c4)))::
- (deserialize 0 ys0)))))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- c1::l ->
- (match l with
- |
- [] -> []
- |
- c2::l0 ->
- (match l0 with
- |
- [] -> []
- |
- c3::l1 ->
- (match l1 with
- |
- [] -> []
- |
- c4::ys0 -> (Int32 ((c1,
- c2), (c3,
- c4)))::
- (deserialize 0 ys0)))))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (Bool
- false)::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b3
- then if b4
- then if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- s1::l ->
- (match l with
- |
- [] -> []
- |
- s2::ys0 ->
- let n1 =
- nat_of_ascii16 (s1, s2)
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys0)
- in
- (Array16 zs)::ws))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- c1::ys0 -> (Uint8
- c1)::
- (deserialize 0 ys0))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b4
- then if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then []
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b5
- then if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then (match ys with
- |
- [] -> []
- |
- c1::ys0 -> (Int8
- c1)::
- (deserialize 0 ys0))
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize 0 ys)
- in
- (FixArray zs)::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b6
- then if b7
- then if b
- then (NFixnum (Ascii (b1, b2,
- b3, b4, b5, true, true,
- true)))::
- (deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, b5, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at n1)
- (deserialize n1 ys)
- in
- (FixRaw (compact zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b7
- then if b
- then Nil::(deserialize 0 ys)
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys)
- else if b
- then let n1 =
- nat_of_ascii8 (Ascii (b1,
- b2, b3, b4, false, false,
- false, false))
- in
- let (
- zs, ws) =
- atat
- (split_at
- (mult (succ (succ 0)) n1))
- (deserialize 0 ys)
- in
- (FixMap (pair zs))::ws
- else (PFixnum (Ascii (b1, b2,
- b3, b4, b5, b6, b7,
- false)))::
- (deserialize 0 ys))
- (fun m ->
- match xs with
- | [] -> []
- | y::ys -> (FixRaw (y::[]))::(deserialize m ys))
- n0
-
diff --git a/ocaml/ocaml/msgpackCore.mli b/ocaml/ocaml/msgpackCore.mli
deleted file mode 100644
index 914b4d64..00000000
--- a/ocaml/ocaml/msgpackCore.mli
+++ /dev/null
@@ -1,141 +0,0 @@
-val fst : ('a1 * 'a2) -> 'a1
-
-val snd : ('a1 * 'a2) -> 'a2
-
-val length : 'a1 list -> int
-
-val app : 'a1 list -> 'a1 list -> 'a1 list
-
-val plus : int -> int -> int
-
-val mult : int -> int -> int
-
-type positive =
- | XI of positive
- | XO of positive
- | XH
-
-val psucc : positive -> positive
-
-val pplus : positive -> positive -> positive
-
-val pplus_carry : positive -> positive -> positive
-
-val pmult_nat : positive -> int -> int
-
-val nat_of_P : positive -> int
-
-val p_of_succ_nat : int -> positive
-
-val pmult : positive -> positive -> positive
-
-type n =
- | N0
- | Npos of positive
-
-val nplus : n -> n -> n
-
-val nmult : n -> n -> n
-
-val nat_of_N : n -> int
-
-val n_of_nat : int -> n
-
-val flat_map : ('a1 -> 'a2 list) -> 'a1 list -> 'a2 list
-
-val eucl_dev : int -> int -> (int * int)
-
-type ascii =
- | Ascii of bool * bool * bool * bool * bool * bool * bool * bool
-
-val zero : ascii
-
-val one : ascii
-
-val shift : bool -> ascii -> ascii
-
-val ascii_of_pos : positive -> ascii
-
-val ascii_of_N : n -> ascii
-
-val ascii_of_nat : int -> ascii
-
-val n_of_digits : bool list -> n
-
-val n_of_ascii : ascii -> n
-
-val nat_of_ascii : ascii -> int
-
-val take : int -> 'a1 list -> 'a1 list
-
-val drop : int -> 'a1 list -> 'a1 list
-
-val split_at : int -> 'a1 list -> 'a1 list * 'a1 list
-
-val pair : 'a1 list -> ('a1 * 'a1) list
-
-val pow : int -> int
-
-val divmod : int -> int -> (int * int)
-
-type ascii8 = ascii
-
-type ascii16 = ascii8 * ascii8
-
-type ascii32 = ascii16 * ascii16
-
-type ascii64 = ascii32 * ascii32
-
-val nat_of_ascii8 : ascii -> int
-
-val ascii8_of_nat : int -> ascii
-
-val ascii16_of_nat : int -> ascii * ascii
-
-val nat_of_ascii16 : ascii16 -> int
-
-val ascii32_of_nat : int -> (ascii * ascii) * (ascii * ascii)
-
-val nat_of_ascii32 : ascii32 -> int
-
-val list_of_ascii8 : ascii8 -> ascii8 list
-
-val list_of_ascii16 : ascii16 -> ascii8 list
-
-val list_of_ascii32 : ascii32 -> ascii8 list
-
-val list_of_ascii64 : ascii64 -> ascii8 list
-
-type object0 =
- | Bool of bool
- | Nil
- | PFixnum of ascii8
- | NFixnum of ascii8
- | Uint8 of ascii8
- | Uint16 of ascii16
- | Uint32 of ascii32
- | Uint64 of ascii64
- | Int8 of ascii8
- | Int16 of ascii16
- | Int32 of ascii32
- | Int64 of ascii64
- | Float of ascii32
- | Double of ascii64
- | FixRaw of ascii8 list
- | Raw16 of ascii8 list
- | Raw32 of ascii8 list
- | FixArray of object0 list
- | Array16 of object0 list
- | Array32 of object0 list
- | FixMap of (object0 * object0) list
- | Map16 of (object0 * object0) list
- | Map32 of (object0 * object0) list
-
-val atat : ('a1 -> 'a2) -> 'a1 -> 'a2
-
-val serialize : object0 -> ascii8 list
-
-val compact : object0 list -> ascii8 list
-
-val deserialize : int -> ascii8 list -> object0 list
-
diff --git a/ocaml/ocaml/pack.ml b/ocaml/ocaml/pack.ml
deleted file mode 100644
index e70e96ee..00000000
--- a/ocaml/ocaml/pack.ml
+++ /dev/null
@@ -1,206 +0,0 @@
-open Base
-open MsgpackCore
-
-exception Not_conversion of string
-
-type t =
- [ `Bool of bool
- | `Nil
- | `PFixnum of int
- | `NFixnum of int
- | `Uint8 of int
- | `Uint16 of int
- | `Uint32 of int64
- | `Uint64 of Big_int.big_int
- | `Int8 of int
- | `Int16 of int
- | `Int32 of int32
- | `Int64 of int64
- | `Float of float
- | `Double of float
- | `FixRaw of char list
- | `Raw16 of char list
- | `Raw32 of char list
- | `FixArray of t list
- | `Array16 of t list
- | `Array32 of t list
- | `FixMap of (t * t) list
- | `Map16 of (t * t) list
- | `Map32 of (t * t) list ]
-
-let ascii8 n =
- Ascii(n land 0b0000_0001 <> 0,
- n land 0b0000_0010 <> 0,
- n land 0b0000_0100 <> 0,
- n land 0b0000_1000 <> 0,
- n land 0b0001_0000 <> 0,
- n land 0b0010_0000 <> 0,
- n land 0b0100_0000 <> 0,
- n land 0b1000_0000 <> 0)
-
-let ascii8_of_char c =
- c +> Char.code +> ascii8
-
-let ascii16 n =
- (ascii8 (n lsr 8), ascii8 n)
-
-let ascii32 n =
- (ascii16 (Int64.to_int (Int64.shift_right_logical n 16)),
- ascii16 (Int64.to_int (Int64.logand n 0xFFFFL)))
-
-let ascii64 n =
- let open Big_int in
- let x =
- shift_right_big_int n 32
- +> int64_of_big_int
- +> ascii32 in
- let y =
- and_big_int n (big_int_of_int64 0xFFFF_FFFFL)
- +> int64_of_big_int
- +> ascii32 in
- (x, y)
-
-let ascii32_of_int32 n =
- (ascii16 (Int32.to_int (Int32.shift_right_logical n 16)),
- ascii16 (Int32.to_int n))
-
-let ascii64_of_int64 n =
- (ascii32 (Int64.shift_right_logical n 32),
- ascii32 n)
-
-let not_conversion msg =
- raise @@ Not_conversion msg
-
-let rec pack = function
- `Nil ->
- Nil
- | `Bool b ->
- Bool b
- | `PFixnum n ->
- if 0 <= n && n < 128 then
- PFixnum (ascii8 n)
- else
- not_conversion "pfixnum"
- | `NFixnum n ->
- if -32 <= n && n < 0 then
- NFixnum (ascii8 n)
- else
- not_conversion "nfixnum"
- | `Uint8 n ->
- if 0 <= n && n <= 0xFF then
- Uint8 (ascii8 n)
- else
- not_conversion "uint8"
- | `Uint16 n ->
- if 0 <= n && n <= 0xFF_FF then
- Uint16 (ascii16 n)
- else
- not_conversion "uint16"
- | `Uint32 n ->
- if 0L <= n && n <= 0xFFFF_FFFFL then
- Uint32 (ascii32 n)
- else
- not_conversion "uint32"
- | `Uint64 n ->
- let open Big_int in
- let (<=%) = le_big_int in
- let (<<) = shift_left_big_int in
- if zero_big_int <=% n && n <=% (unit_big_int << 64) then
- Uint64 (ascii64 n)
- else
- not_conversion "uint64"
- | `Int8 n ->
- if -127 <= n && n <= 128 then
- Int8 (ascii8 n)
- else
- not_conversion "int8"
- | `Int16 n ->
- if -32767 <= n && n <= 32768 then
- Int16 (ascii16 n)
- else
- not_conversion "int16"
- | `Int32 n ->
- Int32 (ascii16 (Int32.to_int (Int32.shift_right_logical n 16)),
- ascii16 (Int32.to_int n))
- | `Int64 n ->
- Int64 (ascii64_of_int64 n)
- | `Float n ->
- Float (ascii32_of_int32 @@ Int32.bits_of_float n)
- | `Double n ->
- Double (ascii64_of_int64 @@ Int64.bits_of_float n)
- | `FixRaw cs ->
- FixRaw (List.map ascii8_of_char cs)
- | `Raw16 cs ->
- Raw16 (List.map ascii8_of_char cs)
- | `Raw32 cs ->
- Raw32 (List.map ascii8_of_char cs)
- | `FixArray xs ->
- FixArray (List.map pack xs)
- | `Array16 xs ->
- Array16 (List.map pack xs)
- | `Array32 xs ->
- Array32 (List.map pack xs)
- | `FixMap xs ->
- FixMap (List.map (fun (x,y) -> (pack x, pack y)) xs)
- | `Map16 xs ->
- Map16 (List.map (fun (x,y) -> (pack x, pack y)) xs)
- | `Map32 xs ->
- Map32 (List.map (fun (x,y) -> (pack x, pack y)) xs)
-
-let of_ascii8 (Ascii(b1,b2,b3,b4,b5,b6,b7,b8)) =
- List.fold_left (fun x y -> 2 * x + (if y then 1 else 0)) 0 [ b8; b7; b6; b5; b4; b3; b2; b1 ]
-
-let char_of_ascii8 c =
- c +> of_ascii8 +> Char.chr
-
-let of_ascii16 (c1, c2) =
- of_ascii8 c1 lsl 8 + of_ascii8 c2
-
-let of_ascii32 (c1,c2) =
- let (+%) = Int64.add in
- let (<<) = Int64.shift_left in
- ((Int64.of_int (of_ascii16 c1)) << 16) +% Int64.of_int (of_ascii16 c2)
-
-let int32_of_ascii32 (c1,c2) =
- let (+%) = Int32.add in
- let (<<) = Int32.shift_left in
- ((Int32.of_int @@ of_ascii16 c1) << 16) +% (Int32.of_int @@ of_ascii16 c2)
-
-let int64_of_ascii64 (c1,c2) =
- let (+%) = Int64.add in
- let (<<) = Int64.shift_left in
- (of_ascii32 c1 << 32) +% (of_ascii32 c2)
-
-let of_ascii64 (c1, c2) =
- let open Big_int in
- let (+%) = add_big_int in
- let (<<) = shift_left_big_int in
- ((big_int_of_int64 @@ of_ascii32 c1) << 32) +% (big_int_of_int64 @@ of_ascii32 c2)
-
-let int width n =
- (n lsl (Sys.word_size-width-1)) asr (Sys.word_size-width-1);;
-
-let rec unpack = function
- | Nil -> `Nil
- | Bool b -> `Bool b
- | PFixnum c -> `PFixnum (of_ascii8 c)
- | NFixnum c -> `NFixnum (int 8 @@ of_ascii8 c)
- | Uint8 c -> `Uint8 (of_ascii8 c)
- | Uint16 c -> `Uint16 (of_ascii16 c)
- | Uint32 c -> `Uint32 (of_ascii32 c)
- | Uint64 c -> `Uint64 (of_ascii64 c)
- | Int8 c -> `Int8 (int 8 @@ of_ascii8 c)
- | Int16 c -> `Int16 (int 16 @@ of_ascii16 c)
- | Int32 c -> `Int32 (int32_of_ascii32 c)
- | Int64 c -> `Int64 (int64_of_ascii64 c)
- | Float c -> `Float (Int32.float_of_bits (int32_of_ascii32 c))
- | Double c -> `Double (Int64.float_of_bits (int64_of_ascii64 c))
- | FixRaw cs -> `FixRaw (List.map char_of_ascii8 cs)
- | Raw16 cs -> `Raw16 (List.map char_of_ascii8 cs)
- | Raw32 cs -> `Raw32 (List.map char_of_ascii8 cs)
- | FixArray xs -> `FixArray (List.map unpack xs)
- | Array16 xs -> `Array16 (List.map unpack xs)
- | Array32 xs -> `Array32 (List.map unpack xs)
- | FixMap xs -> `FixMap (List.map (fun (x,y) -> (unpack x, unpack y)) xs)
- | Map16 xs -> `Map16 (List.map (fun (x,y) -> (unpack x, unpack y)) xs)
- | Map32 xs -> `Map32 (List.map (fun (x,y) -> (unpack x, unpack y)) xs)
diff --git a/ocaml/ocaml/pack.mli b/ocaml/ocaml/pack.mli
deleted file mode 100644
index 55c4c36a..00000000
--- a/ocaml/ocaml/pack.mli
+++ /dev/null
@@ -1,32 +0,0 @@
-exception Not_conversion of string
-
-type t =
- [ `Bool of bool
- | `Nil
- | `PFixnum of int
- | `NFixnum of int
- | `Uint8 of int
- | `Uint16 of int
- | `Uint32 of int64
- | `Uint64 of Big_int.big_int
- | `Int8 of int
- | `Int16 of int
- | `Int32 of int32
- | `Int64 of int64
- | `Float of float
- | `Double of float
- | `FixRaw of char list
- | `Raw16 of char list
- | `Raw32 of char list
- | `FixArray of t list
- | `Array16 of t list
- | `Array32 of t list
- | `FixMap of (t * t) list
- | `Map16 of (t * t) list
- | `Map32 of (t * t) list ]
-
-val pack : t -> MsgpackCore.object0
-val unpack : MsgpackCore.object0 -> t
-
-val char_of_ascii8 : MsgpackCore.ascii -> char
-val ascii8_of_char : char -> MsgpackCore.ascii
diff --git a/ocaml/ocaml/packTest.ml b/ocaml/ocaml/packTest.ml
deleted file mode 100644
index a68a711a..00000000
--- a/ocaml/ocaml/packTest.ml
+++ /dev/null
@@ -1,175 +0,0 @@
-open Base
-open OUnit
-open MsgpackCore
-open Pack
-open Printf
-
-let c0 =
- Ascii (false,false,false,false,false,false,false,false)
-let c1 =
- Ascii (true, false,false,false,false,false,false,false)
-let c255 =
- Ascii (true,true,true,true,true,true,true,true)
-
-let valid = [
- "nil",[
- Nil, `Nil
- ], [];
- "bool",[
- Bool true , `Bool true;
- Bool false, `Bool false
- ], [];
- "pfixnum",[
- PFixnum c0,`PFixnum 0;
- PFixnum c1,`PFixnum 1;
- ], [
- `PFixnum 128;
- `PFixnum (~-1);
- ];
- "nfixnum",[
- NFixnum c255, `NFixnum ~-1;
- NFixnum (Ascii (false,false,false,false,false,true,true,true)), `NFixnum ~-32
- ],[
- `NFixnum 0;
- `NFixnum (~-33)
- ];
- "uint8", [
- Uint8 c0, `Uint8 0;
- Uint8 c1, `Uint8 1;
- Uint8 c255, `Uint8 255
- ],[
- `Uint8 ~-1;
- `Uint8 256
- ];
- "uint16", [
- Uint16 (c0,c0), `Uint16 0;
- Uint16 (c0,c1), `Uint16 1;
- Uint16 (c1,c0), `Uint16 256;
- Uint16 (c255,c255), `Uint16 65535;
- ],[
- `Uint16 ~-1;
- `Uint16 65536
- ];
- "uint32", [
- Uint32 ((c0,c0), (c0,c0)), `Uint32 0L;
- Uint32 ((c255,c255), (c255,c255)), `Uint32 0xFFFF_FFFFL
- ],[
- `Uint32 (-1L);
- `Uint32 0x1FFFF_FFFFL
- ];
- "uint64", [
- Uint64 (((c0,c0), (c0,c0)),((c0,c0), (c0,c0))), `Uint64 Big_int.zero_big_int;
- Uint64 (((c0,c0), (c0,c0)),((c0,c0), (c0,c1))), `Uint64 Big_int.unit_big_int;
- Uint64 (((c255,c255), (c255,c255)),((c255,c255), (c255,c255))), `Uint64 (Big_int.big_int_of_string "18446744073709551615")
- ],[
- `Uint64 (Big_int.big_int_of_string "-1");
- `Uint64 (Big_int.big_int_of_string "18446744073709551617")
- ];
- "int8", [
- Int8 c0, `Int8 0;
- Int8 c1, `Int8 1;
- Int8 c255, `Int8 (~-1)
- ],[
- `Int8 129
- ];
- "int16", [
- Int16 (c0,c0), `Int16 0;
- Int16 (c0,c1), `Int16 1;
- Int16 (c1,c0), `Int16 256;
- Int16 (c255,c255), `Int16 ~-1;
- ],[
- `Int16 65536
- ];
- "int32", [
- Int32 ((c0,c0), (c0,c0)), `Int32 0l;
- Int32 ((c255,c255), (c255,c255)), `Int32 (-1l)
- ],[];
- "int64", [
- Int64 (((c0,c0), (c0,c0)),((c0,c0), (c0,c0))), `Int64 0L;
- Int64 (((c0,c0), (c0,c0)),((c0,c0), (c0,c1))), `Int64 1L;
- Int64 (((c255,c255), (c255,c255)),((c255,c255), (c255,c255))), `Int64 (-1L)
- ],[];
- "float", [
- Float ((c0,c0),(c0,c0)), `Float 0.0;
- (* 0.5 = 3f_00_00_00 *)
- Float ((Ascii (true,true,true,true,true,true,false,false),c0),(c0,c0)), `Float 0.5;
- ], [];
- "double", [
- Double (((c0,c0),(c0,c0)),((c0,c0),(c0,c0))), `Double 0.0;
- (* 0.5 = 3f_e0_00_00_00_00_00_00 *)
- Double (((Ascii (true,true,true,true,true,true,false,false),
- Ascii (false,false,false,false,false,true,true,true)),
- (c0,c0)),
- ((c0,c0),(c0,c0))), `Double 0.5
- ],[];
- "fixraw", [
- FixRaw [], `FixRaw [];
- FixRaw [ c0 ], `FixRaw [ '\000'];
- FixRaw [ c0; c1 ], `FixRaw [ '\000'; '\001'];
- ],[];
- "raw16", [
- Raw16 [], `Raw16 [];
- Raw16 [ c0 ], `Raw16 [ '\000'];
- Raw16 [ c0; c1 ], `Raw16 [ '\000'; '\001'];
- ], [];
- "raw32", [
- Raw32 [], `Raw32 [];
- Raw32 [ c0 ], `Raw32 [ '\000'];
- Raw32 [ c0; c1 ], `Raw32 [ '\000'; '\001'];
- ], [];
- "fixarray", [
- FixArray [], `FixArray [];
- FixArray [ PFixnum c0 ], `FixArray [`PFixnum 0 ];
- FixArray [ FixArray [ PFixnum c0 ] ], `FixArray [`FixArray [ `PFixnum 0] ];
- ], [];
- "array16", [
- Array16 [], `Array16 [];
- Array16 [ PFixnum c0 ], `Array16 [`PFixnum 0 ];
- Array16 [ Array16 [ PFixnum c0 ] ], `Array16 [`Array16 [ `PFixnum 0] ];
- ], [];
- "array32", [
- Array32 [], `Array32 [];
- Array32 [ PFixnum c0 ], `Array32 [`PFixnum 0 ];
- Array32 [ Array32 [ PFixnum c0 ] ], `Array32 [`Array32 [ `PFixnum 0] ];
- ], [];
- "fixmap", [
- FixMap [], `FixMap [];
- FixMap [ PFixnum c0, PFixnum c1 ], `FixMap [`PFixnum 0, `PFixnum 1 ];
- ], [];
- "map16", [
- Map16 [], `Map16 [];
- Map16 [ PFixnum c0, PFixnum c1 ], `Map16 [`PFixnum 0, `PFixnum 1 ];
- ], [];
- "map32", [
- Map32 [], `Map32 [];
- Map32 [ PFixnum c0, PFixnum c1 ], `Map32 [`PFixnum 0, `PFixnum 1 ];
- ], [];
-]
-
-
-let _ = begin "pack.ml" >::: [
- "変換のテスト" >:::
- valid +> HList.concat_map begin fun (name, ok, ng) ->
- let xs =
- ok +> List.map begin fun (expect, actual) ->
- (sprintf "%sが変換できる" name) >:: (fun _ -> assert_equal expect (pack actual));
- end in
- let ys =
- ng +> List.map begin fun actual ->
- (sprintf "%sのエラーチェック" name) >:: (fun _ -> assert_raises (Not_conversion name) (fun () -> pack actual))
- end in
- xs @ ys
- end;
- "復元のテスト" >:::
- valid +> HList.concat_map begin fun (name, ok, _) ->
- ok +> List.map begin fun (actual, expect) ->
- (sprintf "%sが復元できる" name) >:: begin fun _ ->
- match expect, unpack actual with
- `Uint64 n1, `Uint64 n2 ->
- assert_equal ~cmp:Big_int.eq_big_int n1 n2
- | x, y ->
- assert_equal x y
- end
- end
- end;
-] end +> run_test_tt_main
diff --git a/ocaml/ocaml/serialize.ml b/ocaml/ocaml/serialize.ml
deleted file mode 100644
index e6e30d75..00000000
--- a/ocaml/ocaml/serialize.ml
+++ /dev/null
@@ -1,20 +0,0 @@
-open Base
-open ExtString
-
-type t = Pack.t
-
-let deserialize_string str =
- str
- +> String.explode
- +> List.map Pack.ascii8_of_char
- +> MsgpackCore.deserialize 0
- +> List.hd
- +> Pack.unpack
-
-let serialize_string obj =
- obj
- +> Pack.pack
- +> MsgpackCore.serialize
- +> List.map Pack.char_of_ascii8
- +> String.implode
-
diff --git a/ocaml/ocaml/serialize.mli b/ocaml/ocaml/serialize.mli
deleted file mode 100644
index 69719e55..00000000
--- a/ocaml/ocaml/serialize.mli
+++ /dev/null
@@ -1,4 +0,0 @@
-type t = Pack.t
-
-val deserialize_string : string -> t
-val serialize_string : t -> string
diff --git a/ocaml/ocaml/serializeTest.ml b/ocaml/ocaml/serializeTest.ml
deleted file mode 100644
index 32c8bab4..00000000
--- a/ocaml/ocaml/serializeTest.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-open Base
-open OUnit
-open Serialize
-
-let _ = begin "serialize.ml" >::: [
- "Rubyのライブラリとの互換テスト(deserialize)" >:: begin fun _ ->
- (* [1,2,3].to_msgpack *)
- assert_equal (`FixArray [`PFixnum 1; `PFixnum 2; `PFixnum 3]) @@
- deserialize_string "\147\001\002\003"
- end;
- "Rubyのライブラリとの互換テスト(serialize)" >:: begin fun _ ->
- assert_equal "\147\001\002\003" @@
- serialize_string @@ `FixArray [`PFixnum 1; `PFixnum 2; `PFixnum 3]
- end
-] end +> run_test_tt_main
-
diff --git a/ocaml/proof/.gitignore b/ocaml/proof/.gitignore
deleted file mode 100644
index ffb82899..00000000
--- a/ocaml/proof/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-msgpackCore.ml
-msgpackCore.mli
diff --git a/ocaml/proof/CoqBuildRule b/ocaml/proof/CoqBuildRule
deleted file mode 100644
index 57be1c52..00000000
--- a/ocaml/proof/CoqBuildRule
+++ /dev/null
@@ -1,14 +0,0 @@
-public.COQC = coqc
-public.COQC_FLAGS =
-public.COQLIB = $(shell coqc -where)
-public.COQDEP = coqdep -w -coqlib $`(COQLIB) -I .
-
-public.CoqProof(files) =
- vo=$(addsuffix .vo,$(files))
- value $(vo)
-
-%.vo %.glob: %.v
- $(COQC) $(COQC_FLAGS) $<
-
-.SCANNER: %.vo: %.v
- $(COQDEP) $<
diff --git a/ocaml/proof/DeserializeImplement.v b/ocaml/proof/DeserializeImplement.v
deleted file mode 100644
index f9e1f728..00000000
--- a/ocaml/proof/DeserializeImplement.v
+++ /dev/null
@@ -1,630 +0,0 @@
-Require Import Ascii List.
-Require Import ListUtil Object MultiByte Util SerializeSpec Pow SerializedList ProofUtil.
-
-Open Scope char_scope.
-
-Definition compact (xs : list object) : list ascii8 :=
- List.flat_map (fun x => match x with
- FixRaw xs => xs
- | _ => []
- end)
- xs.
-
-Fixpoint deserialize (n : nat) (xs : list ascii8) {struct xs} :=
- match n with
- | 0 =>
- match xs with
- | "192" :: ys =>
- Nil::deserialize 0 ys
- | "194" :: ys =>
- Bool false :: deserialize 0 ys
- | "195" :: ys =>
- Bool true :: deserialize 0 ys
- | Ascii b1 b2 b3 b4 b5 b6 b7 false :: ys =>
- PFixnum (Ascii b1 b2 b3 b4 b5 b6 b7 false) :: deserialize 0 ys
- | (Ascii b1 b2 b3 b4 b5 true true true) :: ys =>
- NFixnum (Ascii b1 b2 b3 b4 b5 true true true) :: deserialize 0 ys
- | "204" :: c1 :: ys =>
- Uint8 c1 :: deserialize 0 ys
- | "205" :: c1 :: c2 :: ys =>
- Uint16 (c1, c2) :: deserialize 0 ys
- | "206" :: c1 :: c2 :: c3 :: c4 :: ys =>
- Uint32 ((c1, c2), (c3, c4)) :: deserialize 0 ys
- | "207" :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: c8 :: ys =>
- Uint64 (((c1, c2), (c3, c4)), ((c5, c6), (c7, c8))) :: deserialize 0 ys
- | "208" :: c1 :: ys =>
- Int8 c1 :: deserialize 0 ys
- | "209" :: c1 :: c2 :: ys =>
- Int16 (c1, c2) :: deserialize 0 ys
- | "210" :: c1 :: c2 :: c3 :: c4 :: ys =>
- Int32 ((c1, c2), (c3, c4)) :: deserialize 0 ys
- | "211" :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: c8 :: ys =>
- Int64 (((c1, c2), (c3, c4)), ((c5, c6), (c7, c8))) :: deserialize 0 ys
- | "202" :: c1 :: c2 :: c3 :: c4 :: ys =>
- Float ((c1,c2), (c3, c4)) :: deserialize 0 ys
- | "203" :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: c8 :: ys =>
- Double (((c1, c2), (c3, c4)), ((c5, c6), (c7, c8))) :: deserialize 0 ys
- | Ascii b1 b2 b3 b4 b5 true false true :: ys =>
- let n :=
- nat_of_ascii8 (Ascii b1 b2 b3 b4 b5 false false false) in
- let (zs, ws) :=
- split_at n @@ deserialize n ys in
- FixRaw (compact zs) :: ws
- | "218" :: s1 :: s2 :: ys =>
- let n :=
- nat_of_ascii16 (s1,s2) in
- let (zs, ws) :=
- split_at n @@ deserialize n ys in
- Raw16 (compact zs) :: ws
- | "219" :: s1 :: s2 :: s3 :: s4 :: ys =>
- let n :=
- nat_of_ascii32 ((s1,s2),(s3,s4)) in
- let (zs, ws) :=
- split_at n @@ deserialize n ys in
- Raw32 (compact zs) :: ws
- | Ascii b1 b2 b3 b4 true false false true :: ys =>
- let n :=
- nat_of_ascii8 (Ascii b1 b2 b3 b4 false false false false) in
- let (zs, ws) :=
- split_at n @@ deserialize 0 ys in
- FixArray zs :: ws
- | "220" :: s1 :: s2 :: ys =>
- let n :=
- nat_of_ascii16 (s1,s2) in
- let (zs, ws) :=
- split_at n @@ deserialize 0 ys in
- Array16 zs :: ws
- | "221" :: s1 :: s2 :: s3 :: s4 :: ys =>
- let n :=
- nat_of_ascii32 ((s1, s2), (s3, s4)) in
- let (zs, ws) :=
- split_at n @@ deserialize 0 ys in
- Array32 zs :: ws
- | Ascii b1 b2 b3 b4 false false false true :: ys =>
- let n :=
- nat_of_ascii8 (Ascii b1 b2 b3 b4 false false false false) in
- let (zs, ws) :=
- split_at (2 * n) @@ deserialize 0 ys in
- FixMap (pair zs) :: ws
- | "222" :: s1 :: s2 :: ys =>
- let n :=
- nat_of_ascii16 (s1,s2) in
- let (zs, ws) :=
- split_at (2 * n) @@ deserialize 0 ys in
- Map16 (pair zs) :: ws
- | "223" :: s1 :: s2 :: s3 :: s4 :: ys =>
- let n :=
- nat_of_ascii32 ((s1, s2), (s3, s4)) in
- let (zs, ws) :=
- split_at (2 * n) @@ deserialize 0 ys in
- Map32 (pair zs) :: ws
- | _ =>
- []
- end
- | S m =>
- match xs with
- | y::ys => FixRaw [ y ]::deserialize m ys
- | _ => []
- end
- end.
-
-Definition DeserializeCorrect os bs :=
- SerializedList os bs ->
- deserialize 0 bs = os.
-
-Lemma correct_bot :
- DeserializeCorrect [] [].
-Proof with auto.
-unfold DeserializeCorrect...
-Qed.
-
-Lemma correct_nil : forall os bs,
- DeserializeCorrect os bs ->
- DeserializeCorrect (Nil :: os) ("192"::bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H0.
-apply H in H3.
-rewrite <- H3...
-Qed.
-
-Lemma correct_false: forall os bs,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Bool false) :: os) ("194"::bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H0.
-apply H in H3.
-rewrite <- H3...
-Qed.
-
-Lemma correct_true: forall os bs,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Bool true) :: os) ("195"::bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H0.
-apply H in H3.
-rewrite <- H3...
-Qed.
-
-Lemma correct_pfixnum: forall os bs x1 x2 x3 x4 x5 x6 x7,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((PFixnum (Ascii x1 x2 x3 x4 x5 x6 x7 false))::os)
- ((Ascii x1 x2 x3 x4 x5 x6 x7 false)::bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H0.
-apply H in H2.
-rewrite <- H2.
-destruct x1,x2,x3,x4,x5,x6,x7; reflexivity.
-Qed.
-
-Lemma correct_nfixnum: forall os bs x1 x2 x3 x4 x5,
- DeserializeCorrect os bs ->
- DeserializeCorrect
- ((NFixnum (Ascii x1 x2 x3 x4 x5 true true true))::os)
- ((Ascii x1 x2 x3 x4 x5 true true true)::bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H0.
-apply H in H2.
-rewrite <- H2.
-destruct x1,x2,x3,x4,x5; reflexivity.
-Qed.
-
-Lemma correct_uint8 : forall os bs c,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Uint8 c)::os) ("204"::list_of_ascii8 c ++ bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H0.
-apply H in H2.
-rewrite <- H2...
-Qed.
-
-Lemma correct_uint16 : forall os bs c,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Uint16 c)::os) ("205"::list_of_ascii16 c ++ bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-destruct c.
-inversion H0.
-apply H in H2.
-rewrite <- H2...
-Qed.
-
-Lemma correct_uint32 : forall os bs c,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Uint32 c)::os) ("206"::list_of_ascii32 c ++ bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-destruct c.
-destruct a, a0.
-inversion H0.
-apply H in H2.
-rewrite <- H2...
-Qed.
-
-Lemma correct_uint64 : forall os bs c,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Uint64 c)::os) ("207"::list_of_ascii64 c ++ bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-destruct c.
-destruct a, a0.
-destruct a, a0, a1, a2.
-inversion H0.
-apply H in H2.
-rewrite <- H2...
-Qed.
-
-Lemma correct_int8 : forall os bs c,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Int8 c)::os) ("208"::list_of_ascii8 c ++ bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H0.
-apply H in H2.
-rewrite <- H2...
-Qed.
-
-Lemma correct_int16 : forall os bs c,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Int16 c)::os) ("209"::list_of_ascii16 c ++ bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-destruct c.
-inversion H0.
-apply H in H2.
-rewrite <- H2...
-Qed.
-
-Lemma correct_int32 : forall os bs c,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Int32 c)::os) ("210"::list_of_ascii32 c ++ bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-destruct c.
-destruct a, a0.
-inversion H0.
-apply H in H2.
-rewrite <- H2...
-Qed.
-
-Lemma correct_int64 : forall os bs c,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Int64 c)::os) ("211"::list_of_ascii64 c ++ bs).
-Proof.
-unfold DeserializeCorrect.
-intros.
-destruct c.
-destruct a, a0.
-destruct a, a0, a1, a2.
-inversion H0.
-apply H in H2.
-rewrite <- H2.
-reflexivity.
-Qed.
-
-Lemma correct_float : forall os bs c,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Float c)::os) ("202"::list_of_ascii32 c ++ bs).
-Proof.
-unfold DeserializeCorrect.
-intros.
-destruct c.
-destruct a, a0.
-inversion H0.
-apply H in H2.
-rewrite <- H2.
-reflexivity.
-Qed.
-
-Lemma correct_double : forall os bs c,
- DeserializeCorrect os bs ->
- DeserializeCorrect ((Double c)::os) ("203"::list_of_ascii64 c ++ bs).
-Proof.
-unfold DeserializeCorrect.
-intros.
-destruct c.
-destruct a, a0.
-destruct a, a0, a1, a2.
-inversion H0.
-apply H in H2.
-rewrite <- H2.
-reflexivity.
-Qed.
-
-Lemma deserialize_take_length: forall xs ys,
- take (List.length xs) (deserialize (List.length xs) (xs ++ ys)) = List.map (fun x => FixRaw [ x ]) xs.
-Proof with auto.
-induction xs; [ reflexivity | intros ].
-simpl.
-rewrite IHxs...
-Qed.
-
-Lemma deserialize_drop_length: forall xs ys,
- drop (List.length xs) (deserialize (List.length xs) (xs ++ ys)) = deserialize 0 ys.
-Proof with auto.
-induction xs; [ reflexivity | intros ].
-simpl.
-rewrite IHxs...
-Qed.
-
-Lemma compact_eq : forall xs,
- compact (List.map (fun x => FixRaw [ x ]) xs) = xs.
-Proof with auto.
-induction xs; [ reflexivity | intros ].
-simpl.
-rewrite IHxs...
-Qed.
-
-Lemma correct_fixraw: forall os bs cs b1 b2 b3 b4 b5,
- DeserializeCorrect os bs ->
- Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (List.length cs) ->
- List.length cs < pow 5 ->
- DeserializeCorrect (FixRaw cs :: os) ((Ascii b1 b2 b3 b4 b5 true false true) :: cs ++ bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H2.
-assert (bs0 = bs); [| rewrite_for bs0 ].
- apply app_same in H11...
-apply H in H13.
-assert (length cs < pow 8).
- transitivity (pow 5); auto.
- apply pow_lt...
-destruct b1,b2,b3,b4,b5;
- ((replace (deserialize 0 _ ) with
- (let n := nat_of_ascii8 (ascii8_of_nat (length cs)) in
- let (zs, ws) := split_at n @@ deserialize n (cs++bs) in
- FixRaw (compact zs) :: ws));
- [ unfold atat, split_at;
- rewrite nat_ascii8_embedding, deserialize_take_length, deserialize_drop_length, compact_eq, <- H13
- | rewrite <- H7])...
-Qed.
-
-Lemma correct_raw16: forall os bs cs s1 s2,
- DeserializeCorrect os bs ->
- (s1, s2) = ascii16_of_nat (List.length cs) ->
- List.length cs < pow 16 ->
- DeserializeCorrect (Raw16 cs :: os) ("218" :: s1 :: s2 :: cs ++ bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H2.
-assert (bs0 = bs); [| rewrite_for bs0 ].
- apply app_same in H8...
-apply H in H10.
-change (deserialize 0 _ ) with
- (let (zs, ws) :=
- split_at (nat_of_ascii16 (s1,s2)) @@ deserialize (nat_of_ascii16 (s1,s2)) (cs++bs) in
- Raw16 (compact zs) :: ws).
-unfold atat, split_at.
-rewrite H7, nat_ascii16_embedding, deserialize_take_length, deserialize_drop_length, compact_eq, H10...
-Qed.
-
-Lemma correct_raw32: forall os bs cs s1 s2 s3 s4,
- DeserializeCorrect os bs ->
- ((s1, s2), (s3, s4)) = ascii32_of_nat (List.length cs) ->
- List.length cs < pow 32 ->
- DeserializeCorrect (Raw32 cs :: os) ("219" :: s1 :: s2 :: s3 :: s4 :: cs ++ bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H2.
-assert (bs0 = bs); [| rewrite_for bs0 ].
- apply app_same in H10...
-apply H in H12.
-change (deserialize 0 _ ) with
- (let (zs, ws) :=
- split_at (nat_of_ascii32 ((s1,s2),(s3,s4))) @@ deserialize (nat_of_ascii32 ((s1,s2),(s3,s4))) (cs++bs) in
- Raw32 (compact zs) :: ws).
-unfold atat, split_at.
-rewrite H7, nat_ascii32_embedding, deserialize_take_length, deserialize_drop_length, compact_eq, H12...
-Qed.
-
-Lemma correct_fixarray : forall os bs n xs ys b1 b2 b3 b4,
- DeserializeCorrect os bs ->
- (xs, ys) = split_at n os ->
- n < pow 4 ->
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat n ->
- DeserializeCorrect (FixArray xs :: ys) (Ascii b1 b2 b3 b4 true false false true :: bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H3.
-assert (os = os0); [| rewrite_for os0 ].
- apply split_at_soundness in H0.
- apply split_at_soundness in H12.
- rewrite H0, H12...
-apply H in H9.
-assert (n0 < pow 8).
- transitivity (pow 4); auto.
- apply pow_lt...
-destruct b1, b2, b3, b4;
- (replace (deserialize 0 (_ :: bs)) with
- (let (zs, ws) :=
- split_at (nat_of_ascii8 (ascii8_of_nat n0)) @@ deserialize 0 bs
- in
- FixArray zs :: ws);
- [ unfold atat; rewrite H9, nat_ascii8_embedding, <- H12 | rewrite <- H14])...
-Qed.
-
-Lemma correct_array16 : forall os bs n xs ys s1 s2 ,
- DeserializeCorrect os bs ->
- n < pow 16 ->
- (s1, s2) = ascii16_of_nat n ->
- (xs, ys) = split_at n os ->
- DeserializeCorrect (Array16 xs :: ys) ("220" :: s1 :: s2 :: bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H3.
-assert (os = os0).
- apply split_at_soundness in H2.
- apply split_at_soundness in H10.
- rewrite H2, H10...
-
- rewrite_for os0.
- apply H in H9.
- assert ( n = nat_of_ascii16 (s1, s2)).
- rewrite H1.
- rewrite nat_ascii16_embedding...
-
- simpl.
- change (nat_of_ascii8 s1 * 256 + nat_of_ascii8 s2) with (nat_of_ascii16 (s1, s2)).
- rewrite <- H13.
- inversion H2.
- rewrite <- H9...
-Qed.
-
-Lemma correct_array32: forall os bs n xs ys s1 s2 s3 s4,
- DeserializeCorrect os bs ->
- (xs, ys) = split_at n os ->
- n < pow 32 ->
- ((s1, s2), (s3, s4)) = ascii32_of_nat n ->
- DeserializeCorrect (Array32 xs :: ys) ("221" :: s1 :: s2 :: s3 :: s4 :: bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H3.
-assert (os = os0).
- apply split_at_soundness in H0.
- apply split_at_soundness in H12.
- rewrite H0, H12...
-
- rewrite_for os0.
- apply H in H9.
- change (deserialize 0 ("221" :: s1 :: s2 :: s3 :: s4 :: bs)) with
- (let (zs, ws) := split_at (nat_of_ascii32 (s1, s2, (s3, s4))) (deserialize 0 bs) in
- Array32 zs :: ws).
- rewrite H9, H14, nat_ascii32_embedding, <- H12...
-Qed.
-
-Lemma correct_fixmap: forall os bs n xs ys b1 b2 b3 b4,
- DeserializeCorrect os bs ->
- (xs, ys) = split_at (2 * n) os ->
- length xs = 2 * n ->
- n < pow 4 ->
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat n ->
- DeserializeCorrect (FixMap (pair xs) :: ys) (Ascii b1 b2 b3 b4 false false false true :: bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H4.
-assert ( n < pow 8).
- transitivity (pow 4); auto.
- apply pow_lt...
-assert ( n0 < pow 8).
- transitivity (pow 4); auto.
- apply pow_lt...
-assert (n0 = n); [| rewrite_for n0 ].
- rewrite H3 in H16.
- apply ascii8_of_nat_eq in H16...
-assert (xs0 = xs); [| rewrite_for xs0 ].
- rewrite <- (unpair_pair _ n xs), <- (unpair_pair _ n xs0); auto.
- rewrite H5...
-assert (os0 = os); [| rewrite_for os0 ].
- apply split_at_soundness in H0.
- apply split_at_soundness in H13.
- rewrite H0, H13...
-apply H in H11.
-destruct b1, b2, b3, b4;
- (replace (deserialize 0 (_ :: bs)) with
- (let (zs, ws) :=
- split_at (2 * (nat_of_ascii8 (ascii8_of_nat n))) @@ deserialize 0 bs
- in
- FixMap (pair zs) :: ws);
- [ unfold atat; rewrite nat_ascii8_embedding, H11, <- H13
- | rewrite <- H16 ])...
-Qed.
-
-Lemma correct_map16: forall os bs n xs ys s1 s2,
- DeserializeCorrect os bs ->
- (xs, ys) = split_at (2 * n) os ->
- length xs = 2 * n ->
- n < pow 16 ->
- (s1, s2) = ascii16_of_nat n ->
- DeserializeCorrect (Map16 (pair xs) :: ys) ("222" :: s1 :: s2 :: bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H4.
-assert (n0 = n).
- rewrite H3 in H14.
- apply ascii16_of_nat_eq in H14...
-rewrite_for n0.
-assert (xs0 = xs).
- rewrite <- (unpair_pair _ n xs), <- (unpair_pair _ n xs0); auto.
- rewrite H5...
-rewrite_for xs0.
-assert (os0 = os).
- apply split_at_soundness in H0.
- apply split_at_soundness in H11.
- rewrite H0, H11...
-rewrite_for os0.
-apply H in H10.
-change (deserialize 0 ("222" :: s1 :: s2 :: bs)) with
- (let (zs, ws) := split_at (2 * nat_of_ascii16 (s1, s2)) @@ deserialize 0 bs in
- Map16 (pair zs) :: ws).
-unfold atat.
-rewrite H10, H14, nat_ascii16_embedding, <- H11...
-Qed.
-
-Lemma correct_map32: forall os bs n xs ys s1 s2 s3 s4,
- DeserializeCorrect os bs ->
- (xs, ys) = split_at (2 * n) os ->
- length xs = 2 * n ->
- n < pow 32 ->
- ((s1, s2), (s3, s4)) = ascii32_of_nat n ->
- DeserializeCorrect (Map32 (pair xs) :: ys) ("223" :: s1 :: s2 :: s3 :: s4 :: bs).
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-inversion H4.
-assert (n0 = n); [| rewrite_for n0 ].
- rewrite H3 in H16.
- apply ascii32_of_nat_eq in H16...
-assert (xs0 = xs); [| rewrite_for xs0 ].
- rewrite <- (unpair_pair _ n xs), <- (unpair_pair _ n xs0); auto.
- rewrite H5...
-assert (os0 = os); [| rewrite_for os0 ].
- apply split_at_soundness in H0.
- apply split_at_soundness in H13.
- rewrite H0, H13...
-apply H in H11.
-change (deserialize 0 ("223" :: s1 :: s2 :: s3 :: s4 :: bs)) with
- (let (zs, ws) := split_at (2 * nat_of_ascii32 ((s1, s2),(s3,s4))) @@ deserialize 0 bs in
- Map32 (pair zs) :: ws).
-unfold atat.
-rewrite H16, H11, nat_ascii32_embedding, <- H13...
-Qed.
-
-Lemma correct_intro : forall os bs,
- (SerializedList os bs -> DeserializeCorrect os bs) ->
- DeserializeCorrect os bs.
-Proof with auto.
-unfold DeserializeCorrect.
-intros.
-apply H in H0...
-Qed.
-
-Theorem deserialize_correct : forall os bs,
- DeserializeCorrect os bs.
-Proof with auto.
-intros.
-apply correct_intro.
-intros.
-pattern os, bs.
-apply SerializedList_ind; intros; auto.
- apply correct_bot...
- apply correct_nil...
- apply correct_true...
- apply correct_false...
- apply correct_pfixnum...
- apply correct_nfixnum...
- apply correct_uint8...
- apply correct_uint16...
- apply correct_uint32...
- apply correct_uint64...
- apply correct_int8...
- apply correct_int16...
- apply correct_int32...
- apply correct_int64...
- apply correct_float...
- apply correct_double...
- apply correct_fixraw...
- simpl; apply correct_raw16...
- simpl; apply correct_raw32...
- apply correct_fixarray with (os:=os0) (n:=n)...
- apply correct_array16 with (os:=os0) (n:=n)...
- apply correct_array32 with (os:=os0) (n:=n)...
- apply correct_fixmap with (os:=os0) (n:=n)...
- apply correct_map16 with (os:=os0) (n:=n)...
- apply correct_map32 with (os:=os0) (n:=n)...
-Qed.
-
-Lemma app_nil: forall A (xs : list A),
- xs ++ [] = xs.
-Proof.
-induction xs.
- reflexivity.
-simpl.
-rewrite IHxs.
-reflexivity.
-Qed.
-
diff --git a/ocaml/proof/ExtractUtil.v b/ocaml/proof/ExtractUtil.v
deleted file mode 100644
index 42fcbca4..00000000
--- a/ocaml/proof/ExtractUtil.v
+++ /dev/null
@@ -1,95 +0,0 @@
-Require Ascii.
-Require String.
-Require List.
-
-
-(* basic types for OCaml *)
-Parameter mlunit mlchar mlint mlstring : Set.
-
-(* unit *)
-Extract Constant mlunit => "unit".
-
-(* bool *)
-Extract Inductive bool => "bool" ["true" "false"].
-Extract Inductive sumbool => "bool" ["true" "false"].
-
-(* int *)
-Extract Constant mlint => "int".
-Parameter mlint_of_nat : nat -> mlint.
-Parameter nat_of_mlint : mlint -> nat.
-Extract Constant mlint_of_nat =>
- "let rec iter = function O -> 0 | S p -> succ (iter p) in iter".
-Extract Constant nat_of_mlint =>
- "let rec iter = function 0 -> O | n -> S (iter (pred n)) in iter".
-
-(* char *)
-Extract Constant mlchar => "char".
-Parameter mlchar_of_mlint : mlint -> mlchar.
-Parameter mlint_of_mlchar : mlchar -> mlint.
-Extract Constant mlchar_of_mlint => "char_of_int".
-Extract Constant mlint_of_mlchar => "int_of_char".
-
-(* list *)
-Extract Inductive list => "list" ["[]" "(::)"].
-
-(* option *)
-Extract Inductive option => "option" ["None" "Some"].
-
-(* string *)
-Extract Constant mlstring => "string".
-Extract Inductive String.string => "ascii list" ["[]" "(::)"].
-Parameter string_of_list : List.list Ascii.ascii -> String.string.
-Parameter list_of_string : String.string -> List.list Ascii.ascii.
-Extract Constant list_of_string => "(fun x -> x)".
-Extract Constant string_of_list => "(fun x -> x)".
-
-Parameter mlstring_of_list : forall {A:Type},
- (A->mlchar) -> List.list A -> mlstring.
-Parameter list_of_mlstring : forall {A:Type},
- (mlchar->A) -> mlstring -> List.list A.
-Extract Constant mlstring_of_list =>
- "(fun f s -> String.concat """"
- (List.map (fun x -> String.make 1 (f x)) s))".
-Extract Constant list_of_mlstring => "
-(fun f s ->
- let rec explode_rec n =
- if n >= String.length s then
- []
- else
- f (String.get s n) :: explode_rec (succ n)
- in
- explode_rec 0)
-".
-
-Parameter mlstring_of_mlint : mlint -> mlstring.
-Extract Constant mlstring_of_mlint => "string_of_int".
-
-
-(* print to stdout *)
-Parameter print_mlstring : mlstring -> mlunit.
-Parameter println_mlstring : mlstring -> mlunit.
-Parameter prerr_mlstring : mlstring -> mlunit.
-Parameter prerrln_mlstring : mlstring -> mlunit.
-Parameter semicolon_flipped : forall {A:Type}, A -> mlunit -> A.
-Extract Constant semicolon_flipped => "(fun x f -> f; x)".
-Extract Constant print_mlstring => "print_string".
-Extract Constant println_mlstring => "print_endline".
-Extract Constant prerr_mlstring => "print_string".
-Extract Constant prerrln_mlstring => "print_endline".
-
-CoInductive llist (A: Type) : Type :=
- LNil | LCons (x: A) (xs: llist A).
-
-Implicit Arguments LNil [A].
-Implicit Arguments LCons [A].
-
-Parameter get_contents_mlchars : llist mlchar.
-Extract Constant get_contents_mlchars => "
- let rec iter store =
- lazy
- begin
- try (LCons (input_char stdin, iter())) with
- | End_of_file -> LNil
- end
- in
- iter ()".
diff --git a/ocaml/proof/ListUtil.v b/ocaml/proof/ListUtil.v
deleted file mode 100644
index 22a82821..00000000
--- a/ocaml/proof/ListUtil.v
+++ /dev/null
@@ -1,259 +0,0 @@
-Require Import List Omega.
-
-Notation "[ ]" := nil : list_scope.
-Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
-
-Lemma app_same : forall A (xs ys zs : list A),
- xs ++ ys = xs ++ zs -> ys = zs.
-Proof.
-induction xs; intros; simpl in H.
- auto.
-
- inversion H.
- apply IHxs in H1.
- auto.
-Qed.
-Lemma length_lt_O: forall A (x : A) xs,
- length (x::xs) > 0.
-Proof.
-intros.
-simpl.
-omega.
-Qed.
-
-Lemma length_inv: forall A (x y : A) xs ys,
- length (x :: xs) = length (y :: ys) ->
- length xs = length ys.
-Proof.
-intros.
-inversion H.
-auto.
-Qed.
-
-Hint Resolve length_lt_O.
-
-
-Fixpoint take {A} n (xs : list A) :=
- match n, xs with
- | O , _ => []
- | _ , [] => []
- | S m, x::xs =>
- x::take m xs
- end.
-
-Fixpoint drop {A} n (xs : list A) :=
- match n, xs with
- | O , _ => xs
- | _ , [] => []
- | S m, x::xs =>
- drop m xs
- end.
-
-Definition split_at {A} (n : nat) (xs : list A) : list A * list A :=
- (take n xs, drop n xs).
-
-Lemma take_length : forall A ( xs ys : list A) n,
- n = List.length xs ->
- take n (xs ++ ys) = xs.
-Proof.
-induction xs; intros; simpl in *.
- rewrite H.
- reflexivity.
-
- rewrite H.
- simpl.
- rewrite IHxs; auto.
-Qed.
-
-Lemma drop_length : forall A ( xs ys : list A) n,
- n = List.length xs ->
- drop n (xs ++ ys) = ys.
-Proof.
-induction xs; intros; simpl in *.
- rewrite H.
- reflexivity.
-
- rewrite H.
- simpl.
- rewrite IHxs; auto.
-Qed.
-
-Lemma split_at_length : forall A (xs ys : list A),
- (xs, ys) = split_at (length xs) (xs ++ ys).
-Proof.
-intros.
-unfold split_at.
-rewrite take_length, drop_length; auto.
-Qed.
-
-Lemma take_length_lt : forall A (xs ys : list A) n,
- ys = take n xs ->
- List.length ys <= n.
-Proof.
-induction xs; intros.
- rewrite H.
- destruct n; simpl; omega...
-
- destruct n.
- rewrite H.
- simpl.
- auto...
-
- destruct ys; [ discriminate |].
- inversion H.
- rewrite <- H2.
- apply IHxs in H2.
- simpl.
- omega...
-Qed.
-
-Lemma split_at_length_lt : forall A (xs ys zs : list A) n,
- (xs, ys) = split_at n zs ->
- List.length xs <= n.
-Proof.
-intros.
-unfold split_at in *.
-inversion H.
-apply (take_length_lt _ zs).
-reflexivity.
-Qed.
-
-Lemma split_at_soundness : forall A (xs ys zs : list A) n,
- (ys,zs) = split_at n xs ->
- xs = ys ++ zs.
-Proof.
-induction xs; induction n; intros; simpl;
- try (inversion H; reflexivity).
-
- unfold split_at in *.
- simpl in H.
- destruct ys.
- inversion H.
-
- rewrite (IHxs ys zs n); auto.
- inversion H.
- reflexivity.
-
- inversion H.
- reflexivity.
-Qed.
-
-Lemma take_nil : forall A n,
- take n ([] : list A) = [].
-Proof.
-induction n; auto.
-Qed.
-
-Lemma take_drop_length : forall A ( xs ys : list A) n,
- take n xs = ys ->
- drop n xs = [ ] ->
- xs = ys.
-Proof.
-induction xs; intros; simpl in *.
- rewrite take_nil in H.
- assumption.
-
- destruct n.
- simpl in H0.
- discriminate.
-
- simpl in *.
- destruct ys.
- discriminate.
-
- inversion H.
- rewrite H3.
- apply IHxs in H3; auto.
- rewrite H3.
- reflexivity.
-Qed.
-
-Fixpoint pair { A } ( xs : list A ) :=
- match xs with
- | [] => []
- | [x] => []
- | k :: v :: ys =>
- (k, v) :: pair ys
- end.
-
-Definition unpair {A} (xs : list (A * A)) :=
- flat_map (fun x => [ fst x; snd x]) xs.
-
-Lemma pair_unpair : forall A ( xs : list ( A * A )),
- pair (unpair xs) = xs.
-Proof.
-induction xs; intros; simpl; auto.
-rewrite IHxs.
-destruct a.
-simpl.
-reflexivity.
-Qed.
-
-Lemma unpair_pair : forall A n ( xs : list A),
- List.length xs = 2 * n ->
- unpair (pair xs) = xs.
-Proof.
-induction n; intros.
- destruct xs; auto.
- simpl in H.
- discriminate.
-
- destruct xs.
- simpl in H.
- discriminate...
-
- destruct xs.
- simpl in H.
- assert (1 <> S (n + S (n + 0))); [ omega | contradiction ]...
-
- replace (2 * S n) with (2 + 2 * n) in H; [| omega ].
- simpl in *.
- inversion H.
- apply IHn in H1.
- rewrite H1.
- reflexivity.
-Qed.
-
-Lemma pair_length' : forall A n (xs : list A),
- n = List.length (pair xs) ->
- 2 * n <= List.length xs.
-Proof.
-induction n; intros; simpl.
- omega...
-
- destruct xs; simpl in *; [ discriminate |].
- destruct xs; simpl in *; [ discriminate |].
- inversion H.
- apply IHn in H1.
- omega.
-Qed.
-
-
-Lemma pair_length : forall A (xs : list A),
- 2 * List.length (pair xs) <= List.length xs.
-Proof.
-intros.
-apply pair_length'.
-reflexivity.
-Qed.
-
-Lemma unpair_length : forall A ( xs : list (A * A)),
- List.length (unpair xs) = 2 * List.length xs.
-Proof.
-induction xs; simpl; auto.
-rewrite IHxs.
-omega.
-Qed.
-
-Lemma unpair_split_at: forall A (x1 x2 : A) xs ys,
- (unpair ((x1, x2) :: xs), ys) =
- split_at (2 * length ((x1, x2) :: xs)) (x1 :: x2 :: unpair xs ++ ys).
-Proof.
-intros.
-replace (2 * (length ((x1,x2) :: xs))) with (length (unpair ((x1,x2)::xs))).
- apply split_at_length.
-
- simpl.
- rewrite unpair_length.
- omega.
-Qed.
\ No newline at end of file
diff --git a/ocaml/proof/Main.v b/ocaml/proof/Main.v
deleted file mode 100644
index e189c802..00000000
--- a/ocaml/proof/Main.v
+++ /dev/null
@@ -1,3 +0,0 @@
-Require Import ExtrOcamlBasic ExtrOcamlIntConv ExtrOcamlNatInt.
-Require Import SerializeImplement DeserializeImplement.
-Extraction "msgpackCore.ml" serialize deserialize.
diff --git a/ocaml/proof/MultiByte.v b/ocaml/proof/MultiByte.v
deleted file mode 100644
index 3aa33416..00000000
--- a/ocaml/proof/MultiByte.v
+++ /dev/null
@@ -1,334 +0,0 @@
-(*
- 16bits,32bits,64bitsの定義。BigEndian。
-*)
-Require Import List Ascii NArith Omega Euclid.
-Require Import Pow.
-
-Open Scope char_scope.
-
-(* * 型の定義 *)
-Definition ascii8 : Set := ascii.
-Definition ascii16 : Set := (ascii8 * ascii8)%type.
-Definition ascii32 : Set := (ascii16 * ascii16)%type.
-Definition ascii64 : Set := (ascii32 * ascii32)%type.
-
-(** ** natとの相互変換 *)
-Definition nat_of_ascii8 :=
- nat_of_ascii.
-
-Definition ascii8_of_nat :=
- ascii_of_nat.
-
-Definition ascii16_of_nat (a : nat) :=
- let (q,r,_,_) := divmod a (pow 8) (pow_lt_O 8) in
- (ascii8_of_nat q, ascii8_of_nat r).
-
-Definition nat_of_ascii16 (a : ascii16) :=
- let (a1, a2) := a in
- (nat_of_ascii8 a1) * (pow 8) + (nat_of_ascii8 a2).
-
-Definition ascii32_of_nat (a : nat) :=
- let (q,r,_,_) := divmod a (pow 16) (pow_lt_O 16) in
- (ascii16_of_nat q, ascii16_of_nat r).
-
-Definition nat_of_ascii32 (a : ascii32) :=
- let (a1, a2) := a in
- (nat_of_ascii16 a1) * (pow 16) + (nat_of_ascii16 a2).
-
-Definition ascii64_of_nat (a : nat) :=
- let (q,r,_,_) := divmod a (pow 32) (pow_lt_O 32) in
- (ascii32_of_nat q, ascii32_of_nat r).
-
-Definition nat_of_ascii64 (a : ascii64) :=
- let (a1, a2) := a in
- (nat_of_ascii32 a1) * (pow 32) + (nat_of_ascii32 a2).
-
-(** ** natに戻せることの証明 *)
-Lemma nat_ascii8_embedding : forall n,
- n < pow 8 ->
- nat_of_ascii8 (ascii8_of_nat n) = n.
-Proof.
-intros.
-unfold nat_of_ascii8,ascii8_of_nat.
-rewrite nat_ascii_embedding.
- reflexivity.
-
- simpl in H.
- assumption.
-Qed.
-
-Lemma nat_ascii16_embedding : forall n,
- n < pow 16 ->
- nat_of_ascii16 (ascii16_of_nat n) = n.
-Proof.
-intros.
-unfold ascii16_of_nat, nat_of_ascii16.
-destruct divmod.
-rewrite (nat_ascii8_embedding q), (nat_ascii8_embedding r); try omega.
-apply divmod_lt_q with (t := 8) in e;
- change (8+8) with 16; assumption.
-Qed.
-
-Lemma nat_ascii32_embedding : forall n,
- n < pow 32 ->
- nat_of_ascii32 (ascii32_of_nat n) = n.
-Proof.
-intros.
-unfold ascii32_of_nat, nat_of_ascii32.
-destruct divmod.
-rewrite (nat_ascii16_embedding q), (nat_ascii16_embedding r); try omega.
-apply divmod_lt_q with (t := 16) in e;
- change (16+16) with 32; assumption.
-Qed.
-
-Lemma nat_ascii64_embedding : forall n,
- n < pow 64 ->
- nat_of_ascii64 (ascii64_of_nat n) = n.
-Proof.
-intros.
-unfold ascii64_of_nat, nat_of_ascii64.
-destruct divmod.
-rewrite (nat_ascii32_embedding q), (nat_ascii32_embedding r); try omega.
-apply divmod_lt_q with (t := 32) in e;
- change (32+32) with 64; assumption.
-Qed.
-
-(** ** ascii8への変換 *)
-Definition list_of_ascii8 (x : ascii8) :=
- x :: nil.
-
-Definition list_of_ascii16 (p : ascii16) :=
- match p with
- (x1,x2) => (list_of_ascii8 x1) ++ (list_of_ascii8 x2)
- end.
-
-Definition list_of_ascii32 (p : ascii32) :=
- match p with
- (x1,x2) => (list_of_ascii16 x1) ++ (list_of_ascii16 x2)
- end.
-
-Definition list_of_ascii64 (p : ascii64) :=
- match p with
- (x1,x2) => (list_of_ascii32 x1) ++ (list_of_ascii32 x2)
- end.
-
-Lemma list_of_ascii8_eq : forall c1 c2,
- list_of_ascii8 c1 = list_of_ascii8 c2 ->
- c1 = c2.
-Proof.
-intros.
-unfold list_of_ascii8 in H.
-inversion H.
-reflexivity.
-Qed.
-
-Lemma list_of_ascii16_eq : forall c1 c2,
- list_of_ascii16 c1 = list_of_ascii16 c2 ->
- c1 = c2.
-Proof.
-intros.
-destruct c1; destruct c2.
-inversion H.
-reflexivity.
-Qed.
-
-Lemma list_of_ascii32_eq : forall c1 c2,
- list_of_ascii32 c1 = list_of_ascii32 c2 ->
- c1 = c2.
-Proof.
-intros.
-destruct c1; destruct c2.
-destruct a; destruct a0; destruct a1; destruct a2.
-inversion H.
-reflexivity.
-Qed.
-
-Lemma list_of_ascii64_eq : forall c1 c2,
- list_of_ascii64 c1 = list_of_ascii64 c2 ->
- c1 = c2.
-Proof.
-intros.
-destruct c1; destruct c2.
-destruct a; destruct a0; destruct a1; destruct a2.
-destruct a; destruct a3; destruct a0; destruct a4;
-destruct a1; destruct a5; destruct a2; destruct a6.
-inversion H.
-reflexivity.
-Qed.
-
-(** 0でないことの証明 *)
-Lemma ascii8_not_O: forall n,
- 0 < n < pow 8 ->
- "000" <> ascii8_of_nat n.
-Proof.
-intros.
-destruct H.
-apply nat_ascii8_embedding in H0.
-destruct (ascii8_of_nat n).
-intro.
-destruct b; destruct b0; destruct b1; destruct b2; destruct b3; destruct b4; destruct b5; destruct b6; inversion H1.
-compute in H0.
-rewrite <- H0 in H.
-inversion H.
-Qed.
-
-Lemma ascii16_not_O: forall n,
- 0 < n < pow 16 ->
- ("000","000") <> ascii16_of_nat n.
-Proof.
-intros.
-unfold ascii16_of_nat.
-destruct divmod.
-destruct H.
-intro.
-inversion H1.
-generalize e; intro.
-apply divmod_not_O in e; auto with pow.
-decompose [or] e.
- apply ascii8_not_O in H3; auto.
- apply divmod_lt_q with (t:=8) in e0; auto with pow.
-
- apply ascii8_not_O in H4; auto with pow.
-Qed.
-
-Lemma ascii32_not_O: forall n,
- 0 < n < pow 32 ->
- ("000","000",("000","000")) <> ascii32_of_nat n.
-Proof.
-intros.
-unfold ascii32_of_nat.
-destruct divmod.
-destruct H.
-intro.
-inversion H1.
-generalize e; intro.
-apply divmod_not_O in e.
- decompose [or] e.
- apply divmod_lt_q with (t:=16) in e0.
- apply ascii16_not_O in H3.
- contradiction.
-
- split; assumption.
-
- assumption.
-
- exact H0.
-
- apply ascii16_not_O in H4.
- contradiction.
-
- split; assumption.
-
- assumption.
-
- apply pow_lt_O.
-Qed.
-
-(* ** 2^n未満なら等価性が変らないことの証明 *)
-Lemma ascii8_of_nat_eq : forall n m,
- n < pow 8 ->
- m < pow 8 ->
- ascii8_of_nat n = ascii8_of_nat m ->
- n = m.
-Proof.
-intros.
-rewrite <- (nat_ascii8_embedding n), <- (nat_ascii8_embedding m), <- H1; auto.
-Qed.
-
-Lemma ascii16_of_nat_eq : forall n m,
- n < pow 16 ->
- m < pow 16 ->
- ascii16_of_nat n = ascii16_of_nat m ->
- n = m.
-Proof.
-intros.
-rewrite <- (nat_ascii16_embedding n), <- (nat_ascii16_embedding m), <- H1; auto.
-Qed.
-
-Lemma ascii32_of_nat_eq : forall n m,
- n < pow 32 ->
- m < pow 32 ->
- ascii32_of_nat n = ascii32_of_nat m ->
- n = m.
-Proof.
-intros.
-rewrite <- (nat_ascii32_embedding n), <- (nat_ascii32_embedding m), <- H1; auto.
-Qed.
-
-Lemma ascii8_of_nat_O:
- "000" = ascii8_of_nat 0.
-Proof.
-compute.
-reflexivity.
-Qed.
-
-Lemma ascii16_of_nat_O:
- ("000", "000") = ascii16_of_nat 0.
-Proof.
-unfold ascii16_of_nat.
-destruct divmod.
-apply divmod_O_pow in e.
-decompose [and] e.
-rewrite H, H0.
-rewrite <- ascii8_of_nat_O.
-reflexivity.
-Qed.
-
-Lemma ascii32_of_nat_O:
- (("000", "000"),("000","000")) = ascii32_of_nat 0.
-Proof.
-unfold ascii32_of_nat.
-destruct divmod.
-apply divmod_O_pow in e.
-decompose [and] e.
-rewrite H, H0.
-rewrite <- ascii16_of_nat_O.
-reflexivity.
-Qed.
-
-(* lengthが等しいことの証明 *)
-Lemma ascii8_length : forall c1 c2,
- length (list_of_ascii8 c1) = length (list_of_ascii8 c2).
-Proof.
-auto.
-Qed.
-
-Lemma ascii16_length : forall c1 c2,
- length (list_of_ascii16 c1) = length (list_of_ascii16 c2).
-Proof.
-destruct c1,c2.
-auto.
-Qed.
-
-Lemma ascii32_length : forall c1 c2,
- length (list_of_ascii32 c1) = length (list_of_ascii32 c2).
-Proof.
-destruct c1 as [a1 a2] ,c2 as [a3 a4].
-destruct a1,a2,a3,a4.
-auto.
-Qed.
-
-Lemma ascii64_length : forall c1 c2,
- length (list_of_ascii64 c1) = length (list_of_ascii64 c2).
-Proof.
-destruct c1 as [a1 a2] ,c2 as [a3 a4].
-destruct a1 as [b1 b2], a2 as [b3 b4], a3 as [b5 b6], a4 as [b7 b8].
-destruct b1,b2,b3,b4,b5,b6,b7,b8.
-auto.
-Qed.
-
-Lemma ascii5 : forall n b1 b2 b3 b4 b5 b6 b7 b8,
- n < pow 5 ->
- Ascii b1 b2 b3 b4 b5 b6 b7 b8 = ascii8_of_nat n ->
- b6 = false /\ b7 = false /\ b8 = false.
-Proof.
-intros.
-simpl in H.
-do 32 (destruct n; [ inversion H0; auto | idtac]).
-do 32 (apply Lt.lt_S_n in H).
-inversion H.
-Qed.
-
-Hint Resolve ascii16_length ascii32_length ascii64_length
- list_of_ascii8_eq list_of_ascii16_eq list_of_ascii32_eq list_of_ascii64_eq
- : ascii.
\ No newline at end of file
diff --git a/ocaml/proof/OCamlBase.v b/ocaml/proof/OCamlBase.v
deleted file mode 100644
index f5c0be5a..00000000
--- a/ocaml/proof/OCamlBase.v
+++ /dev/null
@@ -1,8 +0,0 @@
-Require Export String.
-Require Export List.
-Require Export ExtractUtil.
-Require Export Util.
-
-Open Scope string_scope.
-
-Notation "op ; x" := (semicolon_flipped x op) (at level 50).
diff --git a/ocaml/proof/OMakefile b/ocaml/proof/OMakefile
deleted file mode 100644
index 5ce19233..00000000
--- a/ocaml/proof/OMakefile
+++ /dev/null
@@ -1,26 +0,0 @@
-open CoqBuildRule
-.PHONY: all clean
-
-FILES[] =
- Pow
- MultiByte
- ListUtil
- Object
- SerializeSpec
- Prefix
- Soundness
- SerializeImplement
- SerializedList
- DeserializeImplement
- OCamlBase
- Util
- ExtractUtil
- Main
-
-.DEFAULT: all
-
-all: msgpackCore.ml msgpackCore.mli
-msgpackCore.ml msgpackCore.mli: $(CoqProof $(FILES))
- echo "Proof complete"
-clean:
- rm -rf *.vo *.glob *~ *.omc .omakedb .omakedb.lock *.cm[iox] *.annot *.o msgpackCore.ml msgpackCore.mli
diff --git a/ocaml/proof/Object.v b/ocaml/proof/Object.v
deleted file mode 100644
index a80928e7..00000000
--- a/ocaml/proof/Object.v
+++ /dev/null
@@ -1,122 +0,0 @@
-(* -*- coding:utf-8 -*- *)
-Require Import List Ascii.
-Require Import Pow MultiByte ListUtil.
-
-Open Scope char_scope.
-
-(** MsgPackで使うオブジェクトの定義 *)
-Inductive object :=
-| Bool (_ : bool)
-| Nil
-| PFixnum (_ : ascii8)
-| NFixnum (_ : ascii8)
-| Uint8 (_ : ascii8)
-| Uint16 (_ : ascii16)
-| Uint32 (_ : ascii32)
-| Uint64 (_ : ascii64)
-| Int8 (_ : ascii8)
-| Int16 (_ : ascii16)
-| Int32 (_ : ascii32)
-| Int64 (_ : ascii64)
-| Float (_ : ascii32)
-| Double (_ : ascii64)
-| FixRaw (_ : list ascii8)
-| Raw16 (_ : list ascii8)
-| Raw32 (_ : list ascii8)
-| FixArray ( _ : list object)
-| Array16 ( _ : list object)
-| Array32 ( _ : list object)
-| FixMap ( _ : list (object * object)%type)
-| Map16 ( _ : list (object * object)%type)
-| Map32 ( _ : list (object * object)%type).
-
-(** 妥当なオブジェクトの定義 *)
-Inductive Valid : object -> Prop :=
-| VBool : forall b,
- Valid (Bool b)
-| VPFixNum : forall n,
- nat_of_ascii8 n < 128 -> Valid (PFixnum n)
-| VNFixNum : forall n,
- (* 負の数を導入したくないので、補数表現を使う *)
- 223 < nat_of_ascii8 n /\ nat_of_ascii8 n < 256 -> Valid (NFixnum n)
-| VUint8 : forall c, Valid (Uint8 c)
-| VUint16 : forall c, Valid (Uint16 c)
-| VUint32 : forall c, Valid (Uint32 c)
-| VUint64 : forall c, Valid (Uint64 c)
-| VInt8 : forall c, Valid (Int8 c)
-| VInt16 : forall c, Valid (Int16 c)
-| VInt32 : forall c, Valid (Int32 c)
-| VInt64 : forall c, Valid (Int64 c)
-| VFloat : forall c, Valid (Float c)
-| VDouble : forall c, Valid (Double c)
-| VFixRaw : forall xs,
- length xs < pow 5 -> Valid (FixRaw xs)
-| VRaw16 : forall xs,
- length xs < pow 16 -> Valid (Raw16 xs)
-| VRaw32 : forall xs,
- length xs < pow 32 -> Valid (Raw32 xs)
-| VFixArrayNil :
- Valid (FixArray [])
-| VFixArrayCons : forall x xs,
- Valid x ->
- Valid (FixArray xs) ->
- length (x::xs) < pow 4 ->
- Valid (FixArray (x::xs))
-| VArray16Nil :
- Valid (Array16 [])
-| VArray16Cons: forall x xs,
- Valid x ->
- Valid (Array16 xs) ->
- length (x::xs) < pow 16 ->
- Valid (Array16 (x::xs))
-| VArray32Nil :
- Valid (Array32 [])
-| VArray32Cons : forall x xs,
- Valid x ->
- Valid (Array32 xs) ->
- length (x::xs) < pow 32 ->
- Valid (Array32 (x::xs))
-| VFixMapNil:
- Valid (FixMap [])
-| VFixMapCons : forall k v xs,
- Valid k ->
- Valid v ->
- Valid (FixMap xs) ->
- length ((k,v)::xs) < pow 4 ->
- Valid (FixMap ((k,v)::xs))
-| VMap16Nil :
- Valid (Map16 [])
-| VMap16Cons : forall k v xs,
- Valid k ->
- Valid v ->
- Valid (Map16 xs) ->
- length ((k,v)::xs) < pow 16 ->
- Valid (Map16 ((k,v)::xs))
-| VMap32Nil :
- Valid (Map32 [])
-| VMap32Cons : forall k v xs,
- Valid k ->
- Valid v ->
- Valid (Map32 xs) ->
- length ((k,v)::xs) < pow 32 ->
- Valid (Map32 ((k,v)::xs)).
-
-Lemma varray16_inv1: forall x xs,
- Valid (Array16 (x::xs)) ->
- ("000", "000") <> ascii16_of_nat (length (x :: xs)).
-Proof.
-intros.
-apply ascii16_not_O.
-split; [ apply length_lt_O | inversion H; auto ].
-Qed.
-
-Lemma varray16_inv2 : forall A (x y : A) xs ys,
- pow 16 > length (x :: xs) ->
- pow 16 > length (y :: ys) ->
- ascii16_of_nat (length (x :: xs)) = ascii16_of_nat (length (y :: ys)) ->
- ascii16_of_nat (length xs) = ascii16_of_nat (length ys).
-Proof.
-intros.
-apply ascii16_of_nat_eq in H1; auto.
-Qed.
-
diff --git a/ocaml/proof/Pow.v b/ocaml/proof/Pow.v
deleted file mode 100644
index 23c0666e..00000000
--- a/ocaml/proof/Pow.v
+++ /dev/null
@@ -1,162 +0,0 @@
-(**
- 算術演算関連の補題
-*)
-
-Require Import Omega NArith Euclid.
-
-(** ** 算術演算 *)
-Lemma mult_S_lt_reg_l :
- forall n m p, 0 < n -> n * m < n * p -> m < p.
-Proof.
-intros.
-destruct n.
- inversion H.
-
-elim (le_or_lt m p).
- intro.
- inversion H1.
- rewrite H2 in H0.
- elim (lt_irrefl _ H0).
- omega.
-
- intro.
- apply (mult_S_lt_compat_l n _ _) in H1.
- omega.
-Qed.
-
-Lemma plus_elim: forall p a b,
- a + p < b -> a < b.
-Proof.
-intros.
-omega.
-Qed.
-
-(** ** pow *)
-Fixpoint pow (n : nat) :=
- match n with
- | 0 =>
- 1
- | S n' =>
- 2 * pow n'
- end.
-
-Lemma pow_lt_O : forall n,
- 0 < pow n.
-Proof.
-induction n; simpl; omega.
-Qed.
-
-Hint Resolve pow_lt_O.
-
-Lemma pow_add: forall n m,
- pow n * pow m = pow (n + m).
-Proof.
-induction n; intros.
- simpl in *.
- omega.
-
- simpl.
- repeat rewrite plus_0_r.
- rewrite <- IHn, mult_plus_distr_r.
- reflexivity.
-Qed.
-
-(** ** divmod *)
-Definition divmod (n m : nat) (P : 0 < m) :=
- eucl_dev m P n.
-
-Lemma divmod_lt_q : forall (n m q r s t: nat),
- n < pow (s + t) ->
- n = q * pow s + r ->
- q < pow t.
-Proof.
-intros.
-rewrite H0 in H.
-apply plus_elim in H.
-rewrite <- pow_add, mult_comm in H.
-apply mult_S_lt_reg_l in H.
- assumption.
-
- apply pow_lt_O.
-Qed.
-
-Lemma divmod_not_O: forall n m q r,
- 0 < n ->
- 0 < m ->
- n = q * m + r ->
- 0 < q \/ 0 < r.
-Proof.
-intros.
-rewrite H1 in H.
-destruct q.
- simpl in H.
- right.
- assumption.
-
- left.
- omega.
-Qed.
-
-Lemma divmod_O: forall n q r,
- 0 = q * n + r ->
- n <> 0 ->
- q = 0 /\ r = 0.
-Proof.
-intros.
-destruct q; destruct n; destruct r; try omega.
- simpl in H.
- discriminate.
-
- simpl in H.
- discriminate.
-Qed.
-
-Lemma divmod_O_pow: forall n q r,
- 0 = q * pow n + r ->
- q = 0 /\ r = 0.
-Proof.
-intros.
-apply (divmod_O (pow n) _ _); auto.
-intro.
-generalize (pow_lt_O n); intros.
-omega.
-Qed.
-
-Lemma plus_O : forall n,
- n + 0 = n.
-Proof.
-Admitted.
-
-Lemma plus_double : forall n,
- n < n + n.
-Admitted.
-
-Lemma pow_lt : forall n m,
- n < m ->
- pow n < pow m.
-Proof.
-induction n; induction m; simpl; intros.
- inversion H.
-
- destruct m; auto.
- transitivity (pow (S m));
- [ apply IHm | idtac];
- omega.
-
- inversion H.
-
- simpl in IHm.
- inversion H; simpl.
- repeat (rewrite plus_O in *).
- apply (Plus.plus_lt_compat_r O _).
- transitivity (pow n); auto.
- apply plus_double.
-
- assert (S n < m); auto.
- apply IHm in H2.
- transitivity (pow m); auto.
- rewrite plus_O.
- apply plus_double.
-Qed.
-
-Hint Resolve pow_lt pow_lt_O: pow.
diff --git a/ocaml/proof/Prefix.v b/ocaml/proof/Prefix.v
deleted file mode 100644
index d9e456f3..00000000
--- a/ocaml/proof/Prefix.v
+++ /dev/null
@@ -1,674 +0,0 @@
-Require Import List Ascii.
-Require Import ListUtil Object SerializeSpec MultiByte ProofUtil Pow.
-
-Definition Prefix obj1 x : Prop := forall obj2 y xs ys,
- Serialized obj1 x ->
- Serialized obj2 y ->
- Valid obj1 ->
- Valid obj2 ->
- x ++ xs = y ++ ys ->
- x = y.
-
-Ltac destruct_serialize obj y :=
- match goal with
- | [ H1 : _ ++ _ = y ++ _,
- H2 : Serialized obj y |- _ ] =>
- destruct y as [ | a ] ;
- [ inversion H2 | inversion H1 ; rewrite_for a; inversion H2 ];
- auto
- end.
-
-(* 結果が1バイトになる変換 *)
-Ltac straight_forward :=
- intros;
- unfold Prefix;
- intros obj2 y xs ys S1 S2 V1 V2 Happ;
- destruct_serialize obj2 y.
-
-Lemma prefix_true :
- Prefix (Bool true) ["195"].
-Proof.
-straight_forward.
-Qed.
-
-Lemma prefix_false :
- Prefix (Bool false) ["194"].
-Proof.
-straight_forward.
-Qed.
-
-Lemma prefix_nil :
- Prefix Nil ["192"].
-Proof.
-straight_forward.
-Qed.
-
-Lemma prefix_pfixnum: forall x1 x2 x3 x4 x5 x6 x7,
- Prefix (PFixnum (Ascii x1 x2 x3 x4 x5 x6 x7 false))
- [Ascii x1 x2 x3 x4 x5 x6 x7 false].
-Proof.
-straight_forward.
-Qed.
-
-Lemma prefix_nfixnum : forall x1 x2 x3 x4 x5,
- Prefix (NFixnum (Ascii x1 x2 x3 x4 x5 true true true))
- [Ascii x1 x2 x3 x4 x5 true true true].
-Proof.
-straight_forward.
-Qed.
-
-(* 結果が固定長多バイトになる変換 *)
-Lemma prefix_same : forall A (x y xs ys : list A),
- x ++ xs = y ++ ys ->
- length x = length y ->
- x = y.
-Proof.
-induction x; induction y; intros; auto.
- simpl in H0.
- discriminate.
-
- simpl in H0.
- discriminate.
-
- inversion H.
- inversion H0.
- apply IHx in H3; auto.
- rewrite_for y.
- reflexivity.
-Qed.
-
-Ltac same_as_uint8 :=
- unfold Prefix;
- intros c obj2 y xs ys S1 S2 V1 V2 Happ;
- destruct_serialize obj2 y;
- rewrite_for y;
- apply prefix_same in Happ; simpl; auto with ascii.
-
-Lemma prefix_uint8 : forall c,
- Prefix (Uint8 c) ("204"::list_of_ascii8 c).
-Proof.
-same_as_uint8.
-Qed.
-
-Lemma prefix_uint16: forall c,
- Prefix (Uint16 c) ("205"::list_of_ascii16 c).
-Proof.
-same_as_uint8.
-Qed.
-
-Lemma prefix_uint32: forall c,
- Prefix (Uint32 c) ("206"::list_of_ascii32 c).
-Proof.
-same_as_uint8.
-Qed.
-
-Lemma prefix_uint64 : forall c,
- Prefix (Uint64 c) ("207"::list_of_ascii64 c).
-Proof.
-same_as_uint8.
-Qed.
-
-Lemma prefix_int8 : forall c,
- Prefix (Int8 c) ("208"::list_of_ascii8 c).
-Proof.
-same_as_uint8.
-Qed.
-
-Lemma prefix_int16 : forall c,
- Prefix (Int16 c) ("209"::list_of_ascii16 c).
-Proof.
-same_as_uint8.
-Qed.
-
-Lemma prefix_int32 : forall c,
- Prefix (Int32 c) ("210"::list_of_ascii32 c).
-Proof.
-same_as_uint8.
-Qed.
-
-Lemma prefix_int64 : forall c,
- Prefix (Int64 c) ("211"::list_of_ascii64 c).
-Proof.
-same_as_uint8.
-Qed.
-
-Lemma prefix_float : forall c,
- Prefix (Float c) ("202"::list_of_ascii32 c).
-Proof.
-same_as_uint8.
-Qed.
-
-Lemma prefix_double : forall c,
- Prefix (Double c) ("203"::list_of_ascii64 c).
-Proof.
-same_as_uint8.
-Qed.
-
-Lemma app_length_eq : forall A (xs ys zs ws : list A),
- xs ++zs = ys ++ ws ->
- length xs = length ys ->
- xs = ys.
-Proof.
-induction xs; induction ys; simpl; intros; auto.
- inversion H0.
-
- inversion H0.
-
- inversion H.
- inversion H0.
- assert (xs = ys); [| rewrite_for xs; auto].
- apply (IHxs _ zs ws); auto.
-Qed.
-
-Lemma prefix_fixraw : forall cs b1 b2 b3 b4 b5,
- Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
- Prefix (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true)::cs).
-Proof.
-unfold Prefix.
-intros.
-destruct_serialize obj2 y.
-rewrite_for obj2.
-rewrite_for y.
-inversion H2.
-inversion H3.
-assert (cs = cs0); [| rewrite_for cs; auto ].
-apply (app_length_eq _ _ _ xs ys); auto.
-rewrite <- (nat_ascii8_embedding (length cs)),
- <- (nat_ascii8_embedding (length cs0)).
- rewrite <- H, <- H8.
- reflexivity.
-
- transitivity (pow 5); auto with pow.
-
- transitivity (pow 5); auto with pow.
-Qed.
-
-Lemma prefix_raw16 : forall cs s1 s2,
- (s1,s2) = ascii16_of_nat (length cs) ->
- Prefix (Raw16 cs) ("218"::s1::s2::cs).
-Proof.
-unfold Prefix.
-intros.
-destruct_serialize obj2 y.
-rewrite_for obj2.
-rewrite_for y.
-inversion H2.
-inversion H3.
-inversion H7.
-assert (cs = cs0); [| rewrite_for cs; auto ].
-apply (app_length_eq _ _ _ xs ys); auto.
-rewrite <- (nat_ascii16_embedding (length cs)),
- <- (nat_ascii16_embedding (length cs0)); auto.
-rewrite <- H, <- H8, H12, H13.
-reflexivity.
-Qed.
-
-Lemma prefix_raw32 : forall cs s1 s2 s3 s4,
- ((s1,s2),(s3,s4)) = ascii32_of_nat (length cs) ->
- Prefix (Raw32 cs) ("219"::s1::s2::s3::s4::cs).
-Proof.
-unfold Prefix.
-intros.
-destruct_serialize obj2 y.
-rewrite_for obj2.
-rewrite_for y.
-inversion H2.
-inversion H3.
-inversion H7.
-assert (cs = cs0); [| rewrite_for cs; auto ].
-apply (app_length_eq _ _ _ xs ys); auto.
-rewrite <- (nat_ascii32_embedding (length cs)),
- <- (nat_ascii32_embedding (length cs0)); auto.
-rewrite <- H, <- H8, H12, H13, H14, H15.
-reflexivity.
-Qed.
-
-Lemma prefix_fixarray_nil:
- Prefix (FixArray []) ["144"].
-Proof.
-straight_forward.
-apply ascii8_not_O in H7; [ contradiction |].
-rewrite_for obj2.
-inversion V2.
-split; [ simpl; omega |].
-transitivity (pow 4); [ exact H13 | apply pow_lt; auto ].
-Qed.
-
-Lemma prefix_array16_nil:
- Prefix (Array16 []) ["220"; "000"; "000"].
-Proof.
-unfold Prefix; intros.
-destruct_serialize obj2 y.
-rewrite_for obj2.
-rewrite_for y.
-inversion H3.
-rewrite <- H9, <- H11 in *.
-assert (("000", "000") <> ascii16_of_nat ((length (x::xs0)))); try contradiction.
-inversion H2.
-apply ascii16_not_O.
-split; auto.
-simpl.
-omega.
-Qed.
-
-Lemma prefix_array32_nil:
- Prefix (Array32 []) ["221"; "000"; "000";"000"; "000"].
-Proof.
-unfold Prefix; intros.
-destruct_serialize obj2 y.
-rewrite_for obj2.
-rewrite_for y.
-inversion H3.
-rewrite <- H9, <- H11, <- H12, <- H13 in *.
-assert (("000", "000",("000","000")) <> ascii32_of_nat ((length (x::xs0)))); try contradiction.
-inversion H2.
-apply ascii32_not_O.
-split; auto.
-simpl.
-omega.
-Qed.
-
-Lemma prefix_fixmap_nil:
- Prefix (FixMap []) ["128"].
-Proof.
-unfold Prefix; intros.
-destruct_serialize obj2 y.
-rewrite_for obj2.
-apply ascii8_not_O in H12; [ contradiction |].
-inversion H2.
-split; [ simpl; omega |].
-transitivity (pow 4); [ exact H21 |].
-apply pow_lt.
-auto.
-Qed.
-
-Lemma prefix_map16_nil:
- Prefix (Map16 []) ["222"; "000"; "000"].
-Proof.
-unfold Prefix; intros.
-destruct_serialize obj2 y.
-rewrite_for obj2.
-rewrite_for y.
-inversion H3.
-rewrite <- H10, <- H12 in *.
-assert (("000", "000") <> ascii16_of_nat ((length ((x1, x2)::xs0)))); try contradiction.
-inversion H2.
-apply ascii16_not_O.
-split.
- simpl.
- omega.
-
- exact H19.
-Qed.
-
-Lemma prefix_map32_nil:
- Prefix (Map32 []) ["223"; "000"; "000";"000"; "000"].
-Proof.
-unfold Prefix; intros.
-destruct_serialize obj2 y.
-rewrite_for obj2.
-rewrite_for y.
-inversion H3.
-rewrite <- H10, <- H12, <- H13, <- H14 in *.
-assert (("000", "000",("000","000")) <> ascii32_of_nat ((length ((x1, x2)::xs0)))); try contradiction.
-inversion H2.
-apply ascii32_not_O.
-split.
- simpl.
- omega.
-
- exact H21.
-Qed.
-
-Lemma prefix_fixarray_cons: forall x xs y ys b1 b2 b3 b4 b5 b6 b7 b8,
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
- Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length (x::xs)) ->
- Serialized x y ->
- Prefix x y ->
- Serialized (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
- Prefix (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
- Prefix (FixArray (x :: xs)) ((Ascii b5 b6 b7 b8 true false false true)::y ++ ys).
-Proof.
-unfold Prefix.
-intros.
-destruct_serialize obj2 y0; rewrite_for y0; rewrite_for obj2.
- inversion H6.
- rewrite_for b5.
- rewrite_for b6.
- rewrite_for b7.
- rewrite_for b8.
- apply ascii8_not_O in H0; [contradiction |].
- split; [ simpl; omega |].
- inversion H7.
- transitivity (pow 4); [ exact H19 | apply pow_lt; auto].
-
- assert (y ++ ys = y1 ++ ys1); [| rewrite_for (y++ys); reflexivity ].
- generalize H12; intro Happ; clear H12.
- rewrite <- (app_assoc y ys xs0), <- (app_assoc y1 ys1 ys0) in Happ.
- inversion H7.
- inversion H8.
- apply (H2 x0 y1 (ys++xs0) (ys1++ys0))in H1; auto.
- rewrite_for y1.
- apply app_same in Happ.
- apply (H4 (FixArray xs1) (Ascii b0 b9 b10 b11 true false false true :: ys1) xs0 ys0) in H3; auto.
- inversion H3.
- reflexivity.
-
- simpl.
- unfold ascii8 in *.
- rewrite <- Happ.
- rewrite H0 in H18.
- apply ascii8_of_nat_eq in H18; [
- | transitivity (pow 4); [| apply pow_lt]; auto
- | transitivity (pow 4); [| apply pow_lt]; auto ].
- simpl in H18.
- inversion H18.
- rewrite <- H28 in H16.
- rewrite <- H16 in H.
- inversion H.
- reflexivity.
-Qed.
-
-Lemma prefix_array16_cons: forall x xs y ys s1 s2 t1 t2,
- (t1, t2) = ascii16_of_nat (length xs) ->
- (s1, s2) = ascii16_of_nat (length (x :: xs)) ->
- Serialized x y ->
- Prefix x y ->
- Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
- Prefix (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
- Prefix (Array16 (x::xs)) ("220"::s1::s2::y ++ ys).
-Proof.
-unfold Prefix.
-intros.
-destruct_serialize obj2 y0.
- rewrite_for y0.
- inversion H9.
- rewrite_for s1.
- rewrite_for s2.
- apply ascii16_not_O in H0; [ contradiction |].
- inversion H7.
- split; [ simpl; omega | exact H17 ].
-
- rewrite_for y0.
- rewrite_for obj2.
- inversion H9.
- rewrite_for s0.
- rewrite_for s3.
- assert( y++ ys = y1 ++ ys1); [| rewrite_for (y++ys); reflexivity ].
- rewrite <- (app_assoc y ys xs0), <- (app_assoc y1 ys1 ys0) in H18.
- inversion H7.
- inversion H8.
- apply (H2 x0 y1 (ys++xs0) (ys1++ys0))in H1; auto.
- rewrite_for y1.
- apply app_same in H18.
- apply (H4 (Array16 xs1) ("220" :: t0 :: t3 :: ys1) xs0 ys0) in H3; auto.
- inversion H3.
- reflexivity.
-
- simpl.
- unfold ascii8 in *.
- rewrite <- H18.
- rewrite H0 in H13.
- apply ascii16_of_nat_eq in H13; auto.
- simpl in H13.
- inversion H13.
- rewrite <- H26 in H11.
- rewrite <- H11 in H.
- inversion H.
- reflexivity.
-Qed.
-
-Lemma prefix_array32_cons: forall x xs y ys s1 s2 s3 s4 t1 t2 t3 t4,
- (t1, t2, (t3, t4)) = ascii32_of_nat (length xs) ->
- (s1, s2, (s3, s4)) = ascii32_of_nat (length (x :: xs)) ->
- Serialized x y ->
- Prefix x y ->
- Serialized (Array32 xs) ("221" :: t1 :: t2 :: t3 :: t4 :: ys) ->
- Prefix (Array32 xs) ("221" :: t1 :: t2 :: t3 :: t4 :: ys) ->
- Prefix (Array32 (x :: xs)) ("221" :: s1 :: s2 :: s3 :: s4 :: y ++ ys).
-Proof.
-unfold Prefix.
-intros.
-destruct_serialize obj2 y0;
- rewrite_for y0; rewrite_for obj2; inversion H9.
- rewrite_for s1.
- rewrite_for s2.
- rewrite_for s3.
- rewrite_for s4.
- apply ascii32_not_O in H0; [ contradiction |].
- inversion H7.
- split; [ simpl; omega | exact H15 ].
-
- rewrite_for s0.
- rewrite_for s5.
- rewrite_for s6.
- rewrite_for s7.
- assert( y++ ys = y1 ++ ys1); [| rewrite_for (y++ys); reflexivity ].
- rewrite <- (app_assoc y ys xs0), <- (app_assoc y1 ys1 ys0) in H20.
- inversion H7.
- inversion H8.
- apply (H2 x0 y1 (ys++xs0) (ys1++ys0)) in H1; auto.
- rewrite_for y1.
- apply app_same in H20.
- apply (H4 (Array32 xs1) ("221" :: t0 :: t5 :: t6 :: t7 :: ys1) xs0 ys0) in H3; auto.
- inversion H3.
- reflexivity.
-
- simpl.
- unfold ascii8 in *.
- rewrite <- H20.
- rewrite H0 in H13.
- apply ascii32_of_nat_eq in H13; auto.
- simpl in H13.
- inversion H13.
- rewrite <- H26 in H11.
- rewrite <- H11 in H.
- inversion H.
- reflexivity.
-Qed.
-
-Lemma prefix_fixmap_cons: forall x1 x2 xs y1 y2 ys b1 b2 b3 b4 b5 b6 b7 b8,
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
- Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length ((x1,x2)::xs)) ->
- Serialized x1 y1 -> Prefix x1 y1 ->
- Serialized x2 y2 -> Prefix x2 y2 ->
- Serialized (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
- Prefix (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
- Prefix (FixMap ((x1, x2) :: xs)) (Ascii b5 b6 b7 b8 false false false true :: y1 ++ y2 ++ ys).
-Proof.
-unfold Prefix.
-intros.
-destruct_serialize obj2 y; rewrite_for y; rewrite_for obj2.
- rewrite_for b5.
- rewrite_for b6.
- rewrite_for b7.
- rewrite_for b8.
- apply ascii8_not_O in H0; [ contradiction |].
- split; [ simpl; omega |].
- inversion H9.
- transitivity (pow 4); auto.
- apply pow_lt.
- auto.
-
-assert (y1 ++ y2 ++ ys = y0 ++ y3 ++ ys1); [| rewrite_for (y1 ++ y2 ++ ys); reflexivity ].
-generalize H14; intro Happ; clear H14.
-replace ((y1 ++ y2 ++ ys) ++ xs0) with (y1 ++ y2 ++ ys ++ xs0) in Happ;
- [| repeat (rewrite app_assoc); reflexivity ].
-replace ((y0 ++ y3 ++ ys1) ++ ys0) with (y0 ++ y3 ++ ys1 ++ ys0) in Happ;
- [| repeat (rewrite app_assoc); reflexivity ].
-inversion H9.
-inversion H10.
-apply (H2 x0 y0 (y2 ++ ys ++ xs0) (y3 ++ ys1 ++ ys0))in H1; auto.
-rewrite_for y1.
-apply app_same in Happ.
-apply (H4 x3 y3 (ys ++ xs0) (ys1 ++ ys0)) in H3; auto.
-rewrite_for y3.
-apply app_same in Happ.
-apply (H6 (FixMap xs1) (Ascii b0 b9 b10 b11 false false false true :: ys1) xs0 ys0) in H5; auto.
- inversion H5.
- reflexivity.
-
- simpl.
- unfold ascii8 in *.
- rewrite <- Happ.
- rewrite H0 in H20.
- apply ascii8_of_nat_eq in H20; [
- | transitivity (pow 4); [| apply pow_lt]; auto
- | transitivity (pow 4); [| apply pow_lt]; auto ].
- simpl in H20.
- inversion H20.
- rewrite H3 in H.
- rewrite <- H19 in H.
- inversion H.
- reflexivity.
-Qed.
-
-Lemma prefix_map16_cons: forall x1 x2 xs y1 y2 ys s1 s2 t1 t2,
- (t1, t2) = ascii16_of_nat (length xs) ->
- (s1, s2) = ascii16_of_nat (length ((x1, x2) :: xs)) ->
- Serialized x1 y1 ->
- Prefix x1 y1 ->
- Serialized x2 y2 ->
- Prefix x2 y2 ->
- Serialized (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
- Prefix (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
- Prefix (Map16 ((x1, x2) :: xs)) ("222" :: s1 :: s2 :: y1 ++ y2 ++ ys).
-Proof.
-unfold Prefix.
-intros.
-destruct_serialize obj2 y; rewrite_for y; rewrite_for obj2.
- inversion H11.
- rewrite_for s1.
- rewrite_for s2.
- apply ascii16_not_O in H0; [ contradiction |].
- inversion H9.
- split; [ simpl; omega | exact H20 ].
-
- inversion H14.
- rewrite_for s1.
- rewrite_for s2.
- assert( y1 ++ y2 ++ ys = y0 ++ y3 ++ ys1); [| rewrite_for (y1 ++ y2 ++ ys); reflexivity ].
- replace ((y1 ++ y2 ++ ys) ++ xs0) with (y1 ++ y2 ++ ys ++ xs0) in H21;
- [| repeat (rewrite app_assoc); reflexivity ].
- replace ((y0 ++ y3 ++ ys1) ++ ys0) with (y0 ++ y3 ++ ys1 ++ ys0) in H21;
- [| repeat (rewrite app_assoc); reflexivity ].
- inversion H9.
- inversion H10.
- apply (H2 x0 y0 (y2 ++ ys ++ xs0) (y3 ++ ys1 ++ ys0))in H1; auto.
- rewrite_for y1.
- apply app_same in H21.
- apply (H4 x3 y3 (ys ++ xs0) (ys1 ++ ys0)) in H3; auto.
- rewrite_for y3.
- apply app_same in H21.
- apply (H6 (Map16 xs1) ("222" :: t0 :: t3 :: ys1) xs0 ys0) in H5; auto.
- inversion H5.
- reflexivity.
-
- simpl.
- unfold ascii8 in *.
- rewrite <- H21.
- rewrite H0 in H15.
- apply ascii16_of_nat_eq in H15; auto.
- simpl in H15.
- inversion H15.
- rewrite H3 in H.
- rewrite <- H13 in H.
- inversion H.
- reflexivity.
-Qed.
-
-Lemma prefix_map32_cons : forall x1 x2 xs y1 y2 ys s1 s2 s3 s4 t1 t2 t3 t4,
- (t1, t2, (t3, t4)) = ascii32_of_nat (length xs) ->
- (s1, s2, (s3, s4)) = ascii32_of_nat (length ((x1, x2) :: xs)) ->
- Serialized x1 y1 ->
- Prefix x1 y1 ->
- Serialized x2 y2 ->
- Prefix x2 y2 ->
- Serialized (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
- Prefix (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
- Prefix (Map32 ((x1, x2) :: xs)) ("223" :: s1 :: s2 :: s3 :: s4 :: y1 ++ y2 ++ ys).
-Proof.
-unfold Prefix.
-intros.
-destruct_serialize obj2 y; rewrite_for y; rewrite_for obj2.
- inversion H11.
- rewrite_for s1.
- rewrite_for s2.
- rewrite_for s3.
- rewrite_for s4.
- apply ascii32_not_O in H0; [ contradiction |].
- inversion H9.
- split; [ simpl; omega | exact H20 ].
-
- inversion H14.
- rewrite_for s1.
- rewrite_for s2.
- rewrite_for s3.
- rewrite_for s4.
- generalize H23; intro Happ; clear H23.
- assert( y1 ++ y2 ++ ys = y0 ++ y3 ++ ys1); [| rewrite_for (y1 ++ y2 ++ ys); reflexivity ].
- replace ((y1 ++ y2 ++ ys) ++ xs0) with (y1 ++ y2 ++ ys ++ xs0) in Happ;
- [| repeat (rewrite app_assoc); reflexivity ].
- replace ((y0 ++ y3 ++ ys1) ++ ys0) with (y0 ++ y3 ++ ys1 ++ ys0) in Happ;
- [| repeat (rewrite app_assoc); reflexivity ].
- inversion H9.
- inversion H10.
- apply (H2 x0 y0 (y2 ++ ys ++ xs0) (y3 ++ ys1 ++ ys0)) in H1; auto.
- rewrite_for y1.
- apply app_same in Happ.
- apply (H4 x3 y3 (ys ++ xs0) (ys1 ++ ys0)) in H3; auto.
- rewrite_for y3.
- apply app_same in Happ.
- apply (H6 (Map32 xs1) ("223" :: t0 :: t5 :: t6 :: t7 :: ys1) xs0 ys0) in H5; auto.
- inversion H5.
- reflexivity.
-
- simpl.
- unfold ascii8 in *.
- rewrite <- Happ.
- rewrite H0 in H15.
- apply ascii32_of_nat_eq in H15; auto.
- simpl in H15.
- inversion H15.
- rewrite H3 in H.
- rewrite <- H13 in H.
- inversion H.
- reflexivity.
-Qed.
-
-Hint Resolve
- prefix_true prefix_false
- prefix_nil prefix_pfixnum prefix_nfixnum
- prefix_uint8 prefix_uint16 prefix_uint32 prefix_uint64
- prefix_int8 prefix_int16 prefix_int32 prefix_int64
- prefix_float prefix_double
- prefix_raw16 prefix_raw32
- prefix_fixarray_nil prefix_array16_nil prefix_array32_nil
- prefix_fixmap_nil prefix_map16_nil prefix_map32_nil
- : prefix.
-
-Lemma prefix_intro: forall obj x,
- (Serialized obj x -> Prefix obj x)->
- Prefix obj x.
-Proof.
-unfold Prefix.
-intros.
-apply H with (xs:=xs) (ys:=ys) in H1; auto.
-Qed.
-
-Lemma prefix : forall obj1 x,
- Prefix obj1 x.
-Proof.
-intros.
-apply prefix_intro.
-intro.
-pattern obj1,x.
-apply Serialized_ind; intros; auto with prefix.
- apply prefix_fixraw; auto.
- apply prefix_fixarray_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
- apply prefix_array16_cons with (t1:=t1) (t2:=t2); auto.
- apply prefix_array32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
- apply prefix_fixmap_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
- apply prefix_map16_cons with (t1:=t1) (t2:=t2); auto.
- apply prefix_map32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
-Qed.
diff --git a/ocaml/proof/ProofUtil.v b/ocaml/proof/ProofUtil.v
deleted file mode 100644
index 191544e6..00000000
--- a/ocaml/proof/ProofUtil.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Ltac rewrite_for x :=
- match goal with
- | [ H : x = _ |- _ ] => rewrite H in *; clear H
- | [ H : _ = x |- _ ] => rewrite <- H in *; clear H
- end.
\ No newline at end of file
diff --git a/ocaml/proof/SerializeImplement.v b/ocaml/proof/SerializeImplement.v
deleted file mode 100644
index 0bfd6ddf..00000000
--- a/ocaml/proof/SerializeImplement.v
+++ /dev/null
@@ -1,465 +0,0 @@
-Require Import Ascii List.
-Require Import ListUtil Object MultiByte Util SerializeSpec ProofUtil.
-
-Open Scope char_scope.
-
-Fixpoint serialize (obj : object) : list ascii8 :=
- match obj with
- | Nil => [ "192" ]
- | Bool false => [ "194" ]
- | Bool true => [ "195" ]
- | PFixnum (Ascii b1 b2 b3 b4 b5 b6 b7 _) =>
- [ Ascii b1 b2 b3 b4 b5 b6 b7 false ]
- | NFixnum (Ascii b1 b2 b3 b4 b5 _ _ _) =>
- [ Ascii b1 b2 b3 b4 b5 true true true ]
- | Uint8 c => "204"::list_of_ascii8 c
- | Uint16 c => "205"::list_of_ascii16 c
- | Uint32 c => "206"::list_of_ascii32 c
- | Uint64 c => "207"::list_of_ascii64 c
- | Int8 c => "208"::list_of_ascii8 c
- | Int16 c => "209"::list_of_ascii16 c
- | Int32 c => "210"::list_of_ascii32 c
- | Int64 c => "211"::list_of_ascii64 c
- | Float c => "202"::list_of_ascii32 c
- | Double c => "203"::list_of_ascii64 c
- | FixRaw xs =>
- match ascii8_of_nat @@ length xs with
- | Ascii b1 b2 b3 b4 b5 _ _ _ =>
- (Ascii b1 b2 b3 b4 b5 true false true)::xs
- end
- | Raw16 xs =>
- let (s1,s2) :=
- ascii16_of_nat @@ length xs
- in
- "218"::s1::s2::xs
- | Raw32 xs =>
- match ascii32_of_nat @@ length xs with
- | ((s1,s2),(s3,s4)) =>
- "219"::s1::s2::s3::s4::xs
- end
- | FixArray xs =>
- let ys :=
- flat_map serialize xs
- in
- match ascii8_of_nat @@ length xs with
- | Ascii b1 b2 b3 b4 _ _ _ _ =>
- (Ascii b1 b2 b3 b4 true false false true)::ys
- end
- | Array16 xs =>
- let ys :=
- flat_map serialize xs
- in
- let (s1, s2) :=
- ascii16_of_nat (length xs)
- in
- "220"::s1::s2::ys
- | Array32 xs =>
- let ys :=
- flat_map serialize xs
- in
- match ascii32_of_nat @@ length xs with
- | ((s1,s2),(s3,s4)) =>
- "221"::s1::s2::s3::s4::ys
- end
- | FixMap xs =>
- let ys :=
- flat_map (fun p => serialize (fst p) ++ serialize (snd p)) xs
- in
- match ascii8_of_nat @@ length xs with
- | Ascii b1 b2 b3 b4 _ _ _ _ =>
- (Ascii b1 b2 b3 b4 false false false true)::ys
- end
- | Map16 xs =>
- let ys :=
- flat_map (fun p => serialize (fst p) ++ serialize (snd p)) xs
- in
- let (s1, s2) :=
- ascii16_of_nat (length xs)
- in
- "222"::s1::s2::ys
- | Map32 xs =>
- let ys :=
- flat_map (fun p => serialize (fst p) ++ serialize (snd p)) xs
- in
- match ascii32_of_nat @@ length xs with
- | ((s1,s2),(s3,s4)) =>
- "223"::s1::s2::s3::s4::ys
- end
- end.
-
-Definition Correct obj xs :=
- Serialized obj xs ->
- serialize obj = xs.
-
-Ltac straitfoward :=
- unfold Correct;
- intros;
- simpl;
- reflexivity.
-
-Lemma correct_nil:
- Correct Nil ["192"].
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_false:
- Correct (Bool false) ["194"].
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_true:
- Correct (Bool true) ["195"].
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_pfixnum: forall x1 x2 x3 x4 x5 x6 x7,
- Correct (PFixnum (Ascii x1 x2 x3 x4 x5 x6 x7 false))
- [Ascii x1 x2 x3 x4 x5 x6 x7 false].
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_nfixnum: forall x1 x2 x3 x4 x5,
- Correct (NFixnum (Ascii x1 x2 x3 x4 x5 true true true))
- [Ascii x1 x2 x3 x4 x5 true true true].
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_uint8 : forall c,
- Correct (Uint8 c) ("204"::list_of_ascii8 c).
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_uint16 : forall c,
- Correct (Uint16 c) ("205"::list_of_ascii16 c).
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_uint32 : forall c,
- Correct (Uint32 c) ("206"::list_of_ascii32 c).
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_uint64 : forall c,
- Correct (Uint64 c) ("207"::list_of_ascii64 c).
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_int8 : forall c,
- Correct (Int8 c) ("208"::list_of_ascii8 c).
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_int16 : forall c,
- Correct (Int16 c) ("209"::list_of_ascii16 c).
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_int32 : forall c,
- Correct (Int32 c) ("210"::list_of_ascii32 c).
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_int64 : forall c,
- Correct (Int64 c) ("211"::list_of_ascii64 c).
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_float : forall c,
- Correct (Float c) ("202"::list_of_ascii32 c).
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_double : forall c,
- Correct (Double c) ("203"::list_of_ascii64 c).
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_fixraw : forall cs b1 b2 b3 b4 b5,
- Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
- Correct (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true)::cs).
-Proof.
-unfold Correct.
-intros.
-inversion H0.
-simpl.
-unfold atat.
-rewrite_for (ascii8_of_nat (length cs)).
-reflexivity.
-Qed.
-
-Lemma correct_raw16: forall cs s1 s2,
- (s1,s2) = ascii16_of_nat (length cs) ->
- Correct (Raw16 cs) ("218"::s1::s2::cs).
-Proof.
-unfold Correct.
-intros.
-inversion H0.
-simpl.
-unfold atat.
-rewrite_for (ascii16_of_nat (length cs)).
-reflexivity.
-Qed.
-
-Lemma correct_raw32 : forall cs s1 s2 s3 s4,
- ((s1,s2),(s3,s4)) = ascii32_of_nat (length cs) ->
- Correct (Raw32 cs) ("219"::s1::s2::s3::s4::cs).
-Proof.
-unfold Correct.
-intros.
-inversion H0.
-simpl.
-unfold atat.
-rewrite_for (ascii32_of_nat (length cs)).
-reflexivity.
-Qed.
-
-Lemma correct_fixarray_nil :
- Correct (FixArray []) ["144"].
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_array16_nil :
- Correct (Array16 []) ["220"; "000"; "000"].
-Proof.
-unfold Correct.
-intros.
-simpl.
-rewrite <- ascii16_of_nat_O.
-reflexivity.
-Qed.
-
-Lemma correct_array32_nil:
- Correct (Array32 []) ["221"; "000"; "000";"000"; "000"].
-Proof.
-unfold Correct.
-intros.
-simpl.
-unfold atat.
-rewrite <- ascii32_of_nat_O.
-reflexivity.
-Qed.
-
-Lemma correct_fixmap_nil:
- Correct (FixMap []) ["128"].
-Proof.
-straitfoward.
-Qed.
-
-Lemma correct_map16_nil:
- Correct (Map16 []) ["222"; "000"; "000"].
-Proof.
-unfold Correct.
-intros.
-simpl.
-rewrite <- ascii16_of_nat_O.
-reflexivity.
-Qed.
-
-Lemma correct_map32_nil:
- Correct (Map32 []) ["223"; "000"; "000";"000"; "000"].
-Proof.
-unfold Correct.
-intros.
-simpl.
-unfold atat.
-rewrite <- ascii32_of_nat_O.
-reflexivity.
-Qed.
-
-Lemma correct_fixarray_cons: forall x xs y ys b1 b2 b3 b4 b5 b6 b7 b8,
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
- Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length (x::xs)) ->
- Serialized x y ->
- Correct x y ->
- Serialized (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
- Correct (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
- Correct (FixArray (x :: xs)) ((Ascii b5 b6 b7 b8 true false false true)::y ++ ys).
-Proof.
-unfold Correct.
-intros.
-simpl in *.
-unfold atat in *.
-rewrite_for (ascii8_of_nat (S (length xs))).
-apply H2 in H1.
-apply H4 in H3.
-rewrite_for (ascii8_of_nat (length xs)).
-rewrite_for y.
-inversion H3.
-reflexivity.
-Qed.
-
-Lemma correct_array16_cons: forall x xs t1 t2 s1 s2 y ys,
- (t1, t2) = ascii16_of_nat (length xs) ->
- (s1, s2) = ascii16_of_nat (length (x :: xs)) ->
- Serialized x y ->
- (Serialized x y -> Correct x y) ->
- Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
- (Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
- Correct (Array16 xs) ("220" :: t1 :: t2 :: ys)) ->
- Correct (Array16 (x :: xs)) ("220" :: s1 :: s2 :: y ++ ys).
-Proof.
-unfold Correct.
-intros.
-simpl in *.
-rewrite_for (ascii16_of_nat (S (length xs))).
-apply H2 in H1; auto.
-apply H4 in H3; auto.
-rewrite_for (ascii16_of_nat (length xs)).
-rewrite_for y.
-inversion H3.
-reflexivity.
-Qed.
-
-Lemma correct_array32_cons: forall x xs y ys s1 s2 s3 s4 t1 t2 t3 t4,
- ((t1,t2),(t3,t4)) = ascii32_of_nat (length xs) ->
- ((s1,s2),(s3,s4)) = ascii32_of_nat (length (x::xs)) ->
- Serialized x y ->
- (Serialized x y -> Correct x y) ->
- Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) ->
- (Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) -> Correct (Array32 xs) ("221"::t1::t2::t3::t4::ys)) ->
- Correct (Array32 (x::xs)) ("221"::s1::s2::s3::s4::y ++ ys).
-Proof.
-unfold Correct.
-intros.
-simpl in *.
-unfold atat in *.
-rewrite_for (ascii32_of_nat (S (length xs))).
-apply H2 in H1; auto.
-apply H4 in H3; auto.
-rewrite_for (ascii32_of_nat (length xs)).
-rewrite_for y.
-inversion H3.
-reflexivity.
-Qed.
-
-Lemma correct_fixmap_cons: forall x1 x2 xs y1 y2 ys b1 b2 b3 b4 b5 b6 b7 b8,
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
- Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length ((x1,x2)::xs)) ->
- Serialized x1 y1 -> Correct x1 y1 ->
- Serialized x2 y2 -> Correct x2 y2 ->
- Serialized (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
- Correct (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
- Correct (FixMap ((x1, x2) :: xs)) (Ascii b5 b6 b7 b8 false false false true :: y1 ++ y2 ++ ys).
-Proof.
-unfold Correct.
-intros.
-simpl in *.
-unfold atat in *.
-rewrite_for (ascii8_of_nat (S (length xs))).
-apply H2 in H1.
-apply H4 in H3.
-apply H6 in H5.
-rewrite_for (ascii8_of_nat (length xs)).
-rewrite_for y1.
-rewrite_for y2.
-inversion H5.
-rewrite <- app_assoc.
-reflexivity.
-Qed.
-
-Lemma correct_map16_cons: forall x1 x2 xs y1 y2 ys s1 s2 t1 t2,
- (t1, t2) = ascii16_of_nat (length xs) ->
- (s1, s2) = ascii16_of_nat (length ((x1, x2) :: xs)) ->
- Serialized x1 y1 ->
- Correct x1 y1 ->
- Serialized x2 y2 ->
- Correct x2 y2 ->
- Serialized (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
- Correct (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
- Correct (Map16 ((x1, x2) :: xs)) ("222" :: s1 :: s2 :: y1 ++ y2 ++ ys).
-Proof.
-unfold Correct.
-intros.
-simpl in *.
-rewrite_for (ascii16_of_nat (S (length xs))).
-apply H2 in H1.
-apply H4 in H3.
-apply H6 in H5.
-rewrite_for (ascii16_of_nat (length xs)).
-rewrite_for y1.
-rewrite_for y2.
-inversion H5.
-rewrite <- app_assoc.
-reflexivity.
-Qed.
-
-Lemma correct_map32_cons : forall x1 x2 xs y1 y2 ys s1 s2 s3 s4 t1 t2 t3 t4,
- (t1, t2, (t3, t4)) = ascii32_of_nat (length xs) ->
- (s1, s2, (s3, s4)) = ascii32_of_nat (length ((x1, x2) :: xs)) ->
- Serialized x1 y1 ->
- Correct x1 y1 ->
- Serialized x2 y2 ->
- Correct x2 y2 ->
- Serialized (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
- Correct (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
- Correct (Map32 ((x1, x2) :: xs)) ("223" :: s1 :: s2 :: s3 :: s4 :: y1 ++ y2 ++ ys).
-Proof.
-unfold Correct.
-intros.
-simpl in *.
-unfold atat in *.
-rewrite_for (ascii32_of_nat (S (length xs))).
-apply H2 in H1.
-apply H4 in H3.
-apply H6 in H5.
-rewrite_for (ascii32_of_nat (length xs)).
-rewrite_for y1.
-rewrite_for y2.
-inversion H5.
-rewrite <- app_assoc.
-reflexivity.
-Qed.
-
-Lemma correct_intro : forall obj xs,
- (Serialized obj xs -> Correct obj xs) ->
- Correct obj xs.
-Proof.
-unfold Correct.
-intros.
-apply H in H0; auto.
-Qed.
-
-Hint Resolve
- correct_true correct_false
- correct_nil correct_pfixnum correct_nfixnum
- correct_uint8 correct_uint16 correct_uint32 correct_uint64
- correct_int8 correct_int16 correct_int32 correct_int64
- correct_float correct_double
- correct_raw16 correct_raw32
- correct_fixarray_nil correct_array16_nil correct_array32_nil
- correct_fixmap_nil correct_map16_nil correct_map32_nil
- : correct.
-
-
-Theorem serialize_correct : forall obj xs,
- Correct obj xs.
-Proof.
-intros.
-apply correct_intro.
-intro.
-pattern obj,xs.
-apply Serialized_ind; intros; auto with correct.
- apply correct_fixraw; auto.
- apply correct_fixarray_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
- apply correct_array16_cons with (t1:=t1) (t2:=t2); auto.
- apply correct_array32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
- apply correct_fixmap_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
- apply correct_map16_cons with (t1:=t1) (t2:=t2); auto.
- apply correct_map32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
-Qed.
diff --git a/ocaml/proof/SerializeSpec.v b/ocaml/proof/SerializeSpec.v
deleted file mode 100644
index a071c62a..00000000
--- a/ocaml/proof/SerializeSpec.v
+++ /dev/null
@@ -1,99 +0,0 @@
-Require Import List Ascii.
-Require Import MultiByte Object ListUtil.
-
-Open Scope list_scope.
-Open Scope char_scope.
-
-Inductive Serialized : object -> list ascii8 -> Prop :=
-| SNil :
- Serialized Nil ["192"]
-| STrue :
- Serialized (Bool true) ["195"]
-| SFalse :
- Serialized (Bool false) ["194"]
-| SPFixnum : forall x1 x2 x3 x4 x5 x6 x7,
- Serialized (PFixnum (Ascii x1 x2 x3 x4 x5 x6 x7 false))
- [Ascii x1 x2 x3 x4 x5 x6 x7 false]
-| SNFixnum : forall x1 x2 x3 x4 x5,
- Serialized (NFixnum (Ascii x1 x2 x3 x4 x5 true true true))
- [Ascii x1 x2 x3 x4 x5 true true true]
-| SUint8 : forall c,
- Serialized (Uint8 c) ("204"::list_of_ascii8 c)
-| SUint16 : forall c,
- Serialized (Uint16 c) ("205"::list_of_ascii16 c)
-| SUint32 : forall c,
- Serialized (Uint32 c) ("206"::list_of_ascii32 c)
-| SUint64 : forall c,
- Serialized (Uint64 c) ("207"::list_of_ascii64 c)
-| SInt8 : forall c,
- Serialized (Int8 c) ("208"::list_of_ascii8 c)
-| SInt16 : forall c,
- Serialized (Int16 c) ("209"::list_of_ascii16 c)
-| SInt32 : forall c,
- Serialized (Int32 c) ("210"::list_of_ascii32 c)
-| SInt64 : forall c,
- Serialized (Int64 c) ("211"::list_of_ascii64 c)
-| SFloat : forall c,
- Serialized (Float c) ("202"::list_of_ascii32 c)
-| SDouble : forall c,
- Serialized (Double c) ("203"::list_of_ascii64 c)
-| SFixRaw : forall cs b1 b2 b3 b4 b5,
- Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
- Serialized (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true)::cs)
-| SRaw16 : forall cs s1 s2,
- (s1,s2) = ascii16_of_nat (length cs) ->
- Serialized (Raw16 cs) ("218"::s1::s2::cs)
-| SRaw32 : forall cs s1 s2 s3 s4,
- ((s1,s2),(s3,s4)) = ascii32_of_nat (length cs) ->
- Serialized (Raw32 cs) ("219"::s1::s2::s3::s4::cs)
-| SFixArrayNil :
- Serialized (FixArray []) ["144"]
-| SFixArrayCons : forall x xs y ys b1 b2 b3 b4 b5 b6 b7 b8,
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
- Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length (x::xs)) ->
- Serialized x y ->
- Serialized (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
- Serialized (FixArray (x::xs)) ((Ascii b5 b6 b7 b8 true false false true)::y ++ ys)
-| SArray16Nil :
- Serialized (Array16 []) ["220"; "000"; "000"]
-| SArray16Cons : forall x xs y ys s1 s2 t1 t2,
- (t1,t2) = ascii16_of_nat (length xs) ->
- (s1,s2) = ascii16_of_nat (length (x::xs)) ->
- Serialized x y ->
- Serialized (Array16 xs) ("220"::t1::t2::ys) ->
- Serialized (Array16 (x::xs)) ("220"::s1::s2::y ++ ys)
-| SArray32Nil :
- Serialized (Array32 []) ["221"; "000"; "000";"000"; "000"]
-| SArray32Cons : forall x xs y ys s1 s2 s3 s4 t1 t2 t3 t4,
- ((t1,t2),(t3,t4)) = ascii32_of_nat (length xs) ->
- ((s1,s2),(s3,s4)) = ascii32_of_nat (length (x::xs)) ->
- Serialized x y ->
- Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) ->
- Serialized (Array32 (x::xs)) ("221"::s1::s2::s3::s4::y ++ ys)
-| SFixMapNil :
- Serialized (FixMap []) ["128"]
-| SFixMapCons : forall x1 x2 xs y1 y2 ys b1 b2 b3 b4 b5 b6 b7 b8,
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
- Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length ((x1,x2)::xs)) ->
- Serialized x1 y1 ->
- Serialized x2 y2 ->
- Serialized (FixMap xs) ((Ascii b1 b2 b3 b4 false false false true)::ys) ->
- Serialized (FixMap ((x1,x2)::xs)) ((Ascii b5 b6 b7 b8 false false false true)::y1 ++ y2 ++ ys)
-| SMap16Nil :
- Serialized (Map16 []) ["222"; "000"; "000"]
-| SMap16Cons : forall x1 x2 xs y1 y2 ys s1 s2 t1 t2,
- (t1,t2) = ascii16_of_nat (length xs) ->
- (s1,s2) = ascii16_of_nat (length ((x1,x2)::xs)) ->
- Serialized x1 y1 ->
- Serialized x2 y2 ->
- Serialized (Map16 xs) ("222"::t1::t2::ys) ->
- Serialized (Map16 ((x1,x2)::xs)) ("222"::s1::s2::y1 ++ y2 ++ ys)
-| SMap32Nil :
- Serialized (Map32 []) ["223"; "000"; "000";"000"; "000"]
-| SMap32Cons : forall x1 x2 xs y1 y2 ys s1 s2 s3 s4 t1 t2 t3 t4,
- ((t1,t2),(t3,t4)) = ascii32_of_nat (length xs) ->
- ((s1,s2),(s3,s4)) = ascii32_of_nat (length ((x1,x2)::xs)) ->
- Serialized x1 y1 ->
- Serialized x2 y2 ->
- Serialized (Map32 xs) ("223"::t1::t2::t3::t4::ys) ->
- Serialized (Map32 ((x1,x2)::xs)) ("223"::s1::s2::s3::s4::y1 ++ y2 ++ ys).
diff --git a/ocaml/proof/SerializedList.v b/ocaml/proof/SerializedList.v
deleted file mode 100644
index e2da9e5f..00000000
--- a/ocaml/proof/SerializedList.v
+++ /dev/null
@@ -1,521 +0,0 @@
-Require Import Ascii List.
-Require Import ListUtil Object MultiByte Util SerializeSpec Pow.
-
-Open Scope char_scope.
-
-Definition lift P (o : object) (b : list ascii) := forall os bs,
- P os bs -> P (o::os) (b ++ bs).
-
-Inductive SerializedList : list object -> list ascii8 -> Prop :=
-| SLbot :
- SerializedList [] []
-| SLNil:
- lift SerializedList Nil ["192"]
-| SLTrue :
- lift SerializedList (Bool true) ["195"]
-| SLFalse :
- lift SerializedList (Bool false) ["194"]
-| SLPFixnum : forall x1 x2 x3 x4 x5 x6 x7,
- lift SerializedList (PFixnum (Ascii x1 x2 x3 x4 x5 x6 x7 false))
- [Ascii x1 x2 x3 x4 x5 x6 x7 false]
-| SLNFixnum : forall x1 x2 x3 x4 x5,
- lift SerializedList (NFixnum (Ascii x1 x2 x3 x4 x5 true true true))
- [Ascii x1 x2 x3 x4 x5 true true true]
-| SLUint8 : forall c,
- lift SerializedList (Uint8 c) ("204" :: list_of_ascii8 c)
-| SLUint16 : forall c,
- lift SerializedList (Uint16 c) ("205" :: list_of_ascii16 c)
-| SLUint32 : forall c,
- lift SerializedList (Uint32 c) ("206" :: list_of_ascii32 c)
-| SLUint64 : forall c,
- lift SerializedList (Uint64 c) ("207" :: list_of_ascii64 c)
-| SLInt8 : forall c,
- lift SerializedList (Int8 c) ("208" :: list_of_ascii8 c)
-| SLInt16 : forall c,
- lift SerializedList (Int16 c) ("209" :: list_of_ascii16 c)
-| SLInt32 : forall c,
- lift SerializedList (Int32 c) ("210" :: list_of_ascii32 c)
-| SLInt64 : forall c,
- lift SerializedList (Int64 c) ("211" :: list_of_ascii64 c)
-| SLFloat : forall c,
- lift SerializedList (Float c) ("202" :: list_of_ascii32 c)
-| SLDouble : forall c,
- lift SerializedList (Double c) ("203" :: list_of_ascii64 c)
-| SLFixRaw : forall cs b1 b2 b3 b4 b5,
- Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
- List.length cs < pow 5 ->
- lift SerializedList (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true) :: cs)
-| SLRaw16 : forall cs s1 s2,
- (s1,s2) = ascii16_of_nat (length cs) ->
- List.length cs < pow 16 ->
- lift SerializedList (Raw16 cs) ("218" :: s1 :: s2 :: cs)
-| SLRaw32 : forall cs s1 s2 s3 s4,
- ((s1,s2),(s3,s4)) = ascii32_of_nat (length cs) ->
- List.length cs < pow 32 ->
- lift SerializedList (Raw32 cs) ("219" :: s1 :: s2 :: s3 :: s4 :: cs)
-| SLFixArray : forall os n b1 b2 b3 b4 xs ys bs,
- SerializedList os bs ->
- (xs,ys) = split_at n os ->
- n < pow 4 ->
- (Ascii b1 b2 b3 b4 false false false false) = ascii8_of_nat n ->
- SerializedList ((FixArray xs) :: ys) ((Ascii b1 b2 b3 b4 true false false true) :: bs)
-| SLArray16 : forall os n xs ys bs s1 s2,
- SerializedList os bs ->
- (xs,ys) = split_at n os ->
- n < pow 16 ->
- (s1,s2) = ascii16_of_nat n ->
- SerializedList ((Array16 xs)::ys) ("220" :: s1 :: s2 :: bs)
-| SLArray32 : forall os n xs ys bs s1 s2 s3 s4,
- SerializedList os bs ->
- (xs,ys) = split_at n os ->
- n < pow 32 ->
- ((s1,s2),(s3,s4)) = ascii32_of_nat n ->
- SerializedList ((Array32 xs)::ys) ("221" :: s1 :: s2 :: s3 :: s4 :: bs)
-| SLFixMap : forall os n b1 b2 b3 b4 xs ys bs,
- SerializedList os bs ->
- (xs,ys) = split_at (2 * n) os ->
- List.length xs = 2 * n ->
- n < pow 4 ->
- (Ascii b1 b2 b3 b4 false false false false) = ascii8_of_nat n ->
- SerializedList ((FixMap (pair xs)) :: ys) ((Ascii b1 b2 b3 b4 false false false true) :: bs)
-| SLMap16 : forall os n xs ys bs s1 s2,
- SerializedList os bs ->
- (xs,ys) = split_at (2 * n) os ->
- List.length xs = 2 * n ->
- n < pow 16 ->
- (s1,s2) = ascii16_of_nat n ->
- SerializedList ((Map16 (pair xs))::ys) ("222" :: s1 :: s2 :: bs)
-| SLMap32 : forall os n xs ys bs s1 s2 s3 s4,
- SerializedList os bs ->
- (xs,ys) = split_at (2 * n) os ->
- List.length xs = 2 * n ->
- n < pow 32 ->
- ((s1,s2),(s3,s4)) = ascii32_of_nat n ->
- SerializedList ((Map32 (pair xs))::ys) ("223" :: s1 :: s2 :: s3 :: s4 :: bs).
-
-Lemma app_cons: forall A (xs ys zs : list A) x,
- x :: (xs ++ ys) ++ zs = x :: (xs ++ ys ++ zs).
-Proof.
-induction xs; intros; simpl; auto.
-rewrite (IHxs ys zs a).
-reflexivity.
-Qed.
-
-Definition Soundness o bs := forall os bs',
- Serialized o bs ->
- Valid o ->
- SerializedList os bs' ->
- SerializedList (o :: os) (bs ++ bs').
-
-Ltac straitfoward P :=
- intros;
- unfold Soundness;
- intros os bs' Hs Hv Hsl;
- apply P;
- auto.
-
-Lemma soundness_nil:
- Soundness Nil ["192"].
-Proof.
-straitfoward SLNil.
-Qed.
-
-Lemma soundness_false:
- Soundness (Bool false) ["194"].
-Proof.
-straitfoward SLFalse.
-Qed.
-
-Lemma soundness_true:
- Soundness (Bool true) ["195"].
-Proof.
-straitfoward SLTrue.
-Qed.
-
-Lemma soundness_pfixnum: forall x1 x2 x3 x4 x5 x6 x7,
- Soundness (PFixnum (Ascii x1 x2 x3 x4 x5 x6 x7 false))
- [Ascii x1 x2 x3 x4 x5 x6 x7 false].
-Proof.
-straitfoward SLPFixnum.
-Qed.
-
-Lemma soundness_nfixnum: forall x1 x2 x3 x4 x5,
- Soundness (NFixnum (Ascii x1 x2 x3 x4 x5 true true true))
- [Ascii x1 x2 x3 x4 x5 true true true].
-Proof.
-straitfoward SLNFixnum.
-Qed.
-
-Lemma soundness_uint8 : forall c,
- Soundness (Uint8 c) ("204"::list_of_ascii8 c).
-Proof.
-straitfoward SLUint8.
-Qed.
-
-Lemma soundness_uint16 : forall c,
- Soundness (Uint16 c) ("205"::list_of_ascii16 c).
-Proof.
-straitfoward SLUint16.
-Qed.
-
-Lemma soundness_uint32 : forall c,
- Soundness (Uint32 c) ("206"::list_of_ascii32 c).
-Proof.
-straitfoward SLUint32.
-Qed.
-
-Lemma soundness_uint64 : forall c,
- Soundness (Uint64 c) ("207"::list_of_ascii64 c).
-Proof.
-straitfoward SLUint64.
-Qed.
-
-Lemma soundness_int8 : forall c,
- Soundness (Int8 c) ("208"::list_of_ascii8 c).
-Proof.
-straitfoward SLInt8.
-Qed.
-
-Lemma soundness_int16 : forall c,
- Soundness (Int16 c) ("209"::list_of_ascii16 c).
-Proof.
-straitfoward SLInt16.
-Qed.
-
-Lemma soundness_int32 : forall c,
- Soundness (Int32 c) ("210"::list_of_ascii32 c).
-Proof.
-straitfoward SLInt32.
-Qed.
-
-Lemma soundness_int64 : forall c,
- Soundness (Int64 c) ("211"::list_of_ascii64 c).
-Proof.
-straitfoward SLInt64.
-Qed.
-
-Lemma soundness_float : forall c,
- Soundness (Float c) ("202"::list_of_ascii32 c).
-Proof.
-straitfoward SLFloat.
-Qed.
-
-Lemma soundness_double : forall c,
- Soundness (Double c) ("203"::list_of_ascii64 c).
-Proof.
-straitfoward SLDouble.
-Qed.
-
-Lemma soundness_fixraw : forall cs b1 b2 b3 b4 b5,
- Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
- Soundness (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true)::cs).
-Proof.
-straitfoward SLFixRaw.
-inversion Hv.
-assumption.
-Qed.
-
-Lemma soundness_raw16: forall cs s1 s2,
- (s1,s2) = ascii16_of_nat (length cs) ->
- Soundness (Raw16 cs) ("218"::s1::s2::cs).
-Proof.
-straitfoward SLRaw16.
-inversion Hv.
-assumption.
-Qed.
-
-Lemma soundness_raw32 : forall cs s1 s2 s3 s4,
- ((s1,s2),(s3,s4)) = ascii32_of_nat (length cs) ->
- Soundness (Raw32 cs) ("219"::s1::s2::s3::s4::cs).
-Proof.
-straitfoward SLRaw32.
-inversion Hv.
-assumption.
-Qed.
-
-Lemma soundness_fixarray_nil :
- Soundness (FixArray []) ["144"].
-Proof.
-unfold Soundness.
-intros.
-apply (SLFixArray os 0); auto.
-Qed.
-
-Lemma soundness_array16_nil :
- Soundness (Array16 []) ["220"; "000"; "000"].
-Proof.
-unfold Soundness.
-intros.
-apply (SLArray16 os 0 _ _ bs' "000" "000"); auto.
-rewrite <- ascii16_of_nat_O.
-reflexivity.
-Qed.
-
-Lemma soundness_array32_nil:
- Soundness (Array32 []) ["221"; "000"; "000";"000"; "000"].
-Proof.
-unfold Soundness.
-intros.
-apply (SLArray32 os 0 _ _ bs' "000" "000" "000" "000"); auto.
-rewrite <- ascii32_of_nat_O.
-reflexivity.
-Qed.
-
-Lemma soundness_fixmap_nil:
- Soundness (FixMap []) ["128"].
-Proof.
-unfold Soundness.
-intros.
-apply (SLFixMap os 0 _ _ _ _ [] _ bs'); auto.
-Qed.
-
-Lemma soundness_map16_nil:
- Soundness (Map16 []) ["222"; "000"; "000"].
-Proof.
-unfold Soundness.
-intros.
-apply (SLMap16 os 0 [] _ bs' "000" "000"); auto.
-rewrite <- ascii16_of_nat_O.
-reflexivity.
-Qed.
-
-Lemma soundness_map32_nil:
- Soundness (Map32 []) ["223"; "000"; "000";"000"; "000"].
-Proof.
-unfold Soundness.
-intros.
-apply (SLMap32 os 0 [] _ bs' "000" "000" "000" "000"); auto.
-rewrite <- ascii32_of_nat_O.
-reflexivity.
-Qed.
-
-Lemma soundness_fixarray_cons: forall x xs y ys b1 b2 b3 b4 b5 b6 b7 b8,
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
- Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length (x::xs)) ->
- Serialized x y ->
- Soundness x y ->
- Serialized (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
- Soundness (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
- Soundness (FixArray (x :: xs)) ((Ascii b5 b6 b7 b8 true false false true)::y ++ ys).
-Proof.
-unfold Soundness.
-intros.
-simpl.
-rewrite app_cons.
-inversion H6.
-apply (SLFixArray (x::(xs++os)) (length (x::xs))); auto.
- apply (H2 (xs++os) (ys++bs')) in H1; auto.
- apply (H4 os bs') in H3; auto.
- inversion H3.
- apply split_at_soundness in H21.
- rewrite H21 in *.
- assumption.
-
- apply split_at_length.
-Qed.
-
-Lemma soundness_array16_cons: forall x xs t1 t2 s1 s2 y ys,
- (t1, t2) = ascii16_of_nat (length xs) ->
- (s1, s2) = ascii16_of_nat (length (x :: xs)) ->
- Serialized x y ->
- Soundness x y ->
- Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
- Soundness (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
- Soundness (Array16 (x :: xs)) ("220" :: s1 :: s2 :: y ++ ys).
-Proof.
-unfold Soundness.
-intros.
-simpl.
-rewrite app_cons.
-inversion H6.
-apply (SLArray16 (x::(xs++os)) (length (x::xs))); auto.
- apply (H2 (xs++os) (ys++bs')) in H1; auto.
- apply (H4 os bs') in H3; auto.
- inversion H3.
- apply split_at_soundness in H19.
- rewrite H19 in *.
- assumption.
-
- apply split_at_length.
-Qed.
-
-Lemma soundness_array32_cons: forall x xs y ys s1 s2 s3 s4 t1 t2 t3 t4,
- ((t1,t2),(t3,t4)) = ascii32_of_nat (length xs) ->
- ((s1,s2),(s3,s4)) = ascii32_of_nat (length (x::xs)) ->
- Serialized x y ->
- Soundness x y ->
- Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) ->
- Soundness (Array32 xs) ("221"::t1::t2::t3::t4::ys) ->
- Soundness (Array32 (x::xs)) ("221"::s1::s2::s3::s4::y ++ ys).
-Proof.
-unfold Soundness.
-intros.
-simpl.
-rewrite app_cons.
-inversion H6.
-apply (SLArray32 (x::(xs++os)) (length (x::xs))); auto.
- apply (H2 (xs++os) (ys++bs')) in H1; auto.
- apply (H4 os bs') in H3; auto.
- inversion H3.
- apply split_at_soundness in H21.
- rewrite H21 in *.
- assumption.
-
- apply split_at_length.
-Qed.
-
-
-Lemma soundness_fixmap_cons: forall x1 x2 xs y1 y2 ys b1 b2 b3 b4 b5 b6 b7 b8,
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
- Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length ((x1,x2)::xs)) ->
- Serialized x1 y1 -> Soundness x1 y1 ->
- Serialized x2 y2 -> Soundness x2 y2 ->
- Serialized (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
- Soundness (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
- Soundness (FixMap ((x1, x2) :: xs)) (Ascii b5 b6 b7 b8 false false false true :: y1 ++ y2 ++ ys).
-Proof with auto.
-unfold Soundness.
-intros.
-simpl.
-rewrite app_cons.
-rewrite <- app_assoc.
-rewrite <- (pair_unpair _ ( (x1, x2) :: xs )).
-inversion H8.
-apply (SLFixMap (x1::x2::unpair xs++os) (length ((x1,x2)::xs))); auto.
- apply (H2 ( x2 :: unpair xs ++ os ) ( y2 ++ ys ++ bs' )) in H1; auto.
- apply (H4 ( unpair xs ++ os) ( ys ++ bs')) in H3; auto.
- apply (H6 os bs') in H5; auto.
- inversion H5.
- rewrite (unpair_pair _ n); auto.
- apply split_at_soundness in H25.
- rewrite <- H25...
-
- apply unpair_split_at.
-
- apply unpair_length.
-Qed.
-
-Lemma soundness_map16_cons: forall x1 x2 xs y1 y2 ys s1 s2 t1 t2,
- (t1, t2) = ascii16_of_nat (length xs) ->
- (s1, s2) = ascii16_of_nat (length ((x1, x2) :: xs)) ->
- Serialized x1 y1 ->
- Soundness x1 y1 ->
- Serialized x2 y2 ->
- Soundness x2 y2 ->
- Serialized (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
- Soundness (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
- Soundness (Map16 ((x1, x2) :: xs)) ("222" :: s1 :: s2 :: y1 ++ y2 ++ ys).
-Proof with auto.
-unfold Soundness.
-intros.
-simpl.
-rewrite app_cons.
-rewrite <- app_assoc.
-rewrite <- (pair_unpair _ ( (x1, x2) :: xs )).
-inversion H8.
-apply (SLMap16 (x1::x2::unpair xs++os) (length ((x1,x2)::xs))); auto.
- apply (H2 ( x2 :: unpair xs ++ os ) ( y2 ++ ys ++ bs' )) in H1; auto.
- apply (H4 ( unpair xs ++ os) ( ys ++ bs')) in H3; auto.
- apply (H6 os bs') in H5; auto.
- inversion H5.
- rewrite (unpair_pair _ n); auto.
- apply split_at_soundness in H23.
- rewrite <- H23...
-
- apply unpair_split_at.
-
- apply unpair_length.
-Qed.
-
-Lemma soundness_map32_cons : forall x1 x2 xs y1 y2 ys s1 s2 s3 s4 t1 t2 t3 t4,
- (t1, t2, (t3, t4)) = ascii32_of_nat (length xs) ->
- (s1, s2, (s3, s4)) = ascii32_of_nat (length ((x1, x2) :: xs)) ->
- Serialized x1 y1 ->
- Soundness x1 y1 ->
- Serialized x2 y2 ->
- Soundness x2 y2 ->
- Serialized (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
- Soundness (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
- Soundness (Map32 ((x1, x2) :: xs)) ("223" :: s1 :: s2 :: s3 :: s4 :: y1 ++ y2 ++ ys).
-Proof with auto.
-unfold Soundness.
-intros.
-simpl.
-rewrite app_cons.
-rewrite <- app_assoc.
-rewrite <- (pair_unpair _ ( (x1, x2) :: xs )).
-inversion H8.
-apply (SLMap32 (x1::x2::unpair xs++os) (length ((x1,x2)::xs))); auto.
- apply (H2 ( x2 :: unpair xs ++ os ) ( y2 ++ ys ++ bs' )) in H1; auto.
- apply (H4 ( unpair xs ++ os) ( ys ++ bs')) in H3; auto.
- apply (H6 os bs') in H5; auto.
- inversion H5.
- rewrite (unpair_pair _ n); auto.
- apply split_at_soundness in H25.
- rewrite <- H25...
-
- apply unpair_split_at.
-
- apply unpair_length.
-Qed.
-
-Lemma soundness_intro : forall obj xs,
- (Serialized obj xs -> Soundness obj xs) ->
- Soundness obj xs.
-Proof.
-unfold Soundness.
-intros.
-eapply H in H0; auto.
-apply H0.
-auto.
-Qed.
-
-Hint Resolve
- soundness_true soundness_false
- soundness_nil soundness_pfixnum soundness_nfixnum
- soundness_uint8 soundness_uint16 soundness_uint32 soundness_uint64
- soundness_int8 soundness_int16 soundness_int32 soundness_int64
- soundness_float soundness_double
- soundness_raw16 soundness_raw32
- soundness_fixarray_nil soundness_array16_nil soundness_array32_nil
- soundness_fixmap_nil soundness_map16_nil soundness_map32_nil
- : soundness.
-
-
-Theorem serialize_soundness : forall obj xs,
- Soundness obj xs.
-Proof.
-intros.
-apply soundness_intro.
-intro.
-pattern obj,xs.
-apply Serialized_ind; intros; auto with soundness.
- apply soundness_fixraw; auto.
- apply soundness_fixarray_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
- apply soundness_array16_cons with (t1:=t1) (t2:=t2); auto.
- apply soundness_array32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
- apply soundness_fixmap_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
- apply soundness_map16_cons with (t1:=t1) (t2:=t2); auto.
- apply soundness_map32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
-Qed.
-
-Lemma sl_soundness: forall o os bs bs',
- Serialized o bs ->
- Valid o ->
- SerializedList os bs' ->
- SerializedList (o :: os) (bs ++ bs').
-Proof.
-intros.
-apply soundness_intro; auto.
-intro.
-pattern o, bs.
-apply Serialized_ind; intros; auto with soundness.
- apply soundness_fixraw; auto.
- apply soundness_fixarray_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
- apply soundness_array16_cons with (t1:=t1) (t2:=t2); auto.
- apply soundness_array32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
- apply soundness_fixmap_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
- apply soundness_map16_cons with (t1:=t1) (t2:=t2); auto.
- apply soundness_map32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
-Qed.
-
diff --git a/ocaml/proof/Soundness.v b/ocaml/proof/Soundness.v
deleted file mode 100644
index a3072e80..00000000
--- a/ocaml/proof/Soundness.v
+++ /dev/null
@@ -1,623 +0,0 @@
-Require Import Ascii.
-Require Import ListUtil Object MultiByte SerializeSpec Prefix ProofUtil Pow.
-
-Definition Soundness obj1 x : Prop := forall obj2,
- Serialized obj1 x ->
- Serialized obj2 x ->
- Valid obj1 ->
- Valid obj2 ->
- obj1 = obj2.
-
-Ltac straightfoward :=
- intros;
- unfold Soundness;
- intros obj2 Hs1 Hs2 V1 V2;
- inversion Hs2;
- reflexivity.
-
-Lemma soundness_nil:
- Soundness Nil ["192"].
-Proof.
-straightfoward.
-Qed.
-
-Lemma soundness_true :
- Soundness (Bool true) ["195"].
-Proof.
-straightfoward.
-Qed.
-
-Lemma soundness_false :
- Soundness (Bool false) ["194"].
-Proof.
-straightfoward.
-Qed.
-
-Lemma soundness_pfixnum: forall x1 x2 x3 x4 x5 x6 x7,
- Soundness (PFixnum (Ascii x1 x2 x3 x4 x5 x6 x7 false))
- [Ascii x1 x2 x3 x4 x5 x6 x7 false].
-Proof.
-straightfoward.
-Qed.
-
-Lemma soundness_nfixnum: forall x1 x2 x3 x4 x5,
- Soundness (NFixnum (Ascii x1 x2 x3 x4 x5 true true true))
- [Ascii x1 x2 x3 x4 x5 true true true].
-Proof.
-straightfoward.
-Qed.
-
-Lemma soundness_uint8 : forall c,
- Soundness (Uint8 c) ("204"::list_of_ascii8 c).
-Proof.
-intros.
-unfold Soundness.
-intros obj2 Hs1 Hs2 V1 V2.
-inversion Hs2.
-rewrite_for obj2.
-auto.
-Qed.
-
-Lemma soundness_uint16 : forall c,
- Soundness (Uint16 c) ("205"::list_of_ascii16 c).
-Proof.
-intros.
-unfold Soundness.
-intros obj2 Hs1 Hs2 V1 V2.
-inversion Hs2.
-assert (c = c0); [| rewrite_for c ]; auto with ascii.
-Qed.
-
-Lemma soundness_uint32 : forall c,
- Soundness (Uint32 c) ("206"::list_of_ascii32 c).
-Proof.
-intros.
-unfold Soundness.
-intros obj2 Hs1 Hs2 V1 V2.
-inversion Hs2.
-assert (c = c0); [| rewrite_for c ]; auto with ascii.
-Qed.
-
-Lemma soundness_uint64 : forall c,
- Soundness (Uint64 c) ("207"::list_of_ascii64 c).
-Proof.
-intros.
-unfold Soundness.
-intros obj2 Hs1 Hs2 V1 V2.
-inversion Hs2.
-assert (c = c0); [| rewrite_for c ]; auto with ascii.
-Qed.
-
-Lemma soundness_int8 : forall c,
- Soundness (Int8 c) ("208"::list_of_ascii8 c).
-Proof.
-intros.
-unfold Soundness.
-intros obj2 Hs1 Hs2 V1 V2.
-inversion Hs2.
-assert (c = c0); [| rewrite_for c ]; auto with ascii.
-Qed.
-
-Lemma soundness_int16 : forall c,
- Soundness (Int16 c) ("209"::list_of_ascii16 c).
-Proof.
-intros.
-unfold Soundness.
-intros obj2 Hs1 Hs2 V1 V2.
-inversion Hs2.
-assert (c = c0); [| rewrite_for c ]; auto with ascii.
-Qed.
-
-Lemma soundness_int32 : forall c,
- Soundness (Int32 c) ("210"::list_of_ascii32 c).
-Proof.
-intros.
-unfold Soundness.
-intros obj2 Hs1 Hs2 V1 V2.
-inversion Hs2.
-assert (c = c0); [| rewrite_for c ]; auto with ascii.
-Qed.
-
-Lemma soundness_int64 : forall c,
- Soundness (Int64 c) ("211"::list_of_ascii64 c).
-Proof.
-intros.
-unfold Soundness.
-intros obj2 Hs1 Hs2 V1 V2.
-inversion Hs2.
-assert (c = c0); [| rewrite_for c ]; auto with ascii.
-Qed.
-
-Lemma soundness_float : forall c,
- Soundness (Float c) ("202"::list_of_ascii32 c).
-Proof.
-intros.
-unfold Soundness.
-intros obj2 Hs1 Hs2 V1 V2.
-inversion Hs2.
-assert (c = c0); [| rewrite_for c ]; auto with ascii.
-Qed.
-
-Lemma soundness_double : forall c,
- Soundness (Double c) ("203"::list_of_ascii64 c).
-Proof.
-intros.
-unfold Soundness.
-intros obj2 Hs1 Hs2 V1 V2.
-inversion Hs2.
-assert (c = c0); [| rewrite_for c ]; auto with ascii.
-Qed.
-
-Lemma soundness_fixraw : forall cs b1 b2 b3 b4 b5,
- Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
- Soundness (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true)::cs).
-Proof.
-straightfoward.
-Qed.
-
-Lemma soundness_raw16: forall cs s1 s2,
- (s1,s2) = ascii16_of_nat (length cs) ->
- Soundness (Raw16 cs) ("218"::s1::s2::cs).
-Proof.
-straightfoward.
-Qed.
-
-Lemma soundness_raw32 : forall cs s1 s2 s3 s4,
- ((s1,s2),(s3,s4)) = ascii32_of_nat (length cs) ->
- Soundness (Raw32 cs) ("219"::s1::s2::s3::s4::cs).
-Proof.
-straightfoward.
-Qed.
-
-Lemma soundness_fixarray_nil :
- Soundness (FixArray []) ["144"].
-Proof.
-unfold Soundness.
-intros.
-inversion H0; auto.
-apply ascii8_not_O in H10; [ contradiction |].
-split; [ simpl; omega |].
-rewrite_for obj2.
-inversion H2.
-transitivity (pow 4); [ assumption |].
-apply pow_lt.
-auto.
-Qed.
-
-Lemma soundness_array16_nil :
- Soundness (Array16 []) ["220"; "000"; "000"].
-Proof.
-unfold Soundness.
-intros.
-inversion H0; auto.
-apply ascii16_not_O in H8; [ contradiction |].
-split; [ simpl; omega |].
-rewrite_for obj2.
-inversion H2.
-assumption.
-Qed.
-
-Lemma soundness_array32_nil:
- Soundness (Array32 []) ["221"; "000"; "000";"000"; "000"].
-Proof.
-unfold Soundness.
-intros.
-inversion H0; auto.
-apply ascii32_not_O in H10; [ contradiction |].
-split; [ simpl; omega |].
-rewrite_for obj2.
-inversion H2.
-assumption.
-Qed.
-
-Lemma soundness_fixmap_nil:
- Soundness (FixMap []) ["128"].
-Proof.
-unfold Soundness.
-intros.
-inversion H0; auto.
-apply ascii8_not_O in H10; [ contradiction |].
-split; [ simpl; omega |].
-rewrite_for obj2.
-inversion H2.
-transitivity (pow 4); [ assumption |].
-apply pow_lt.
-auto.
-Qed.
-
-Lemma soundness_map16_nil:
- Soundness (Map16 []) ["222"; "000"; "000"].
-Proof.
-unfold Soundness.
-intros.
-inversion H0; auto.
-apply ascii16_not_O in H7; [ contradiction |].
-split; [ simpl; omega |].
-rewrite_for obj2.
-inversion H2.
-assumption.
-Qed.
-
-Lemma soundness_map32_nil:
- Soundness (Map32 []) ["223"; "000"; "000";"000"; "000"].
-Proof.
-unfold Soundness.
-intros.
-inversion H0; auto.
-apply ascii32_not_O in H10; [ contradiction |].
-split; [ simpl; omega |].
-rewrite_for obj2.
-inversion H2.
-assumption.
-Qed.
-
-Lemma soundness_fixarray_cons: forall x xs y ys b1 b2 b3 b4 b5 b6 b7 b8,
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
- Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length (x::xs)) ->
- Serialized x y ->
- Soundness x y ->
- Serialized (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
- Soundness (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
- Soundness (FixArray (x :: xs)) ((Ascii b5 b6 b7 b8 true false false true)::y ++ ys).
-Proof.
-unfold Soundness.
-intros.
-inversion H6.
- rewrite_for b5.
- rewrite_for b6.
- rewrite_for b7.
- rewrite_for b8.
- apply ascii8_not_O in H0; [ contradiction |].
- split; [ simpl; omega |].
- inversion H7.
- transitivity (pow 4); [| apply pow_lt ]; auto.
-
- rewrite_for obj2.
- inversion H7.
- inversion H8.
- assert (y = y0).
- generalize prefix.
- unfold Prefix.
- intro Hprefix.
- apply (Hprefix x _ x0 _ ys ys0); auto.
-
- rewrite_for y0.
- apply H2 with (obj2:=x0) in H1; auto.
- apply app_same in H15.
- apply H4 with (obj2:=(FixArray xs0)) in H3; auto.
- inversion H3.
- rewrite H1.
- reflexivity.
-
- rewrite H16 in H0.
- apply ascii8_of_nat_eq in H0; [| transitivity (pow 4); [| apply pow_lt]; auto
- | transitivity (pow 4); [| apply pow_lt]; auto].
- simpl H0.
- inversion H0.
- rewrite <- H29 in H.
- rewrite <- H14 in H.
- inversion H.
- rewrite_for b9.
- rewrite_for b10.
- rewrite_for ys.
- assumption.
-Qed.
-
-Lemma soundness_array16_cons: forall x xs t1 t2 s1 s2 y ys,
- (t1, t2) = ascii16_of_nat (length xs) ->
- (s1, s2) = ascii16_of_nat (length (x :: xs)) ->
- Serialized x y ->
- (Serialized x y -> Soundness x y) ->
- Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
- (Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
- Soundness (Array16 xs) ("220" :: t1 :: t2 :: ys)) ->
- Soundness (Array16 (x :: xs)) ("220" :: s1 :: s2 :: y ++ ys).
-Proof.
-unfold Soundness.
-intros.
-inversion H6.
- rewrite_for s1.
- rewrite_for s2.
- apply ascii16_not_O in H0; [ contradiction |].
- split; [ simpl; omega |].
- inversion H7.
- assumption.
-
- rewrite_for obj2.
- inversion H7.
- inversion H8.
- assert (y = y0).
- generalize prefix.
- unfold Prefix.
- intro Hprefix.
- apply (Hprefix x _ x0 _ ys ys0); auto.
-
- rewrite_for y0.
- apply H2 with (obj2:=x0) in H1; auto.
- apply app_same in H11.
- apply H4 with (obj2:=(Array16 xs0)) in H3; auto.
- inversion H3.
- rewrite H1.
- reflexivity.
-
- rewrite H14 in H0.
- simpl in H0.
- apply ascii16_of_nat_eq in H0; auto.
- inversion H0.
- rewrite <- H27 in H.
- rewrite <- H12 in H.
- inversion H.
- rewrite_for t0.
- rewrite_for t3.
- rewrite_for ys.
- assumption.
-Qed.
-
-Lemma soundness_array32_cons: forall x xs y ys s1 s2 s3 s4 t1 t2 t3 t4,
- ((t1,t2),(t3,t4)) = ascii32_of_nat (length xs) ->
- ((s1,s2),(s3,s4)) = ascii32_of_nat (length (x::xs)) ->
- Serialized x y ->
- (Serialized x y -> Soundness x y) ->
- Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) ->
- (Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) -> Soundness (Array32 xs) ("221"::t1::t2::t3::t4::ys)) ->
- Soundness (Array32 (x::xs)) ("221"::s1::s2::s3::s4::y ++ ys).
-Proof.
-unfold Soundness.
-intros.
-inversion H6.
- rewrite_for s1.
- rewrite_for s2.
- rewrite_for s3.
- rewrite_for s4.
- apply ascii32_not_O in H0; [ contradiction |].
- split; [ simpl; omega |].
- inversion H7.
- assumption.
-
- rewrite_for obj2.
- inversion H7.
- inversion H8.
- assert (y = y0).
- generalize prefix.
- unfold Prefix.
- intro Hprefix.
- apply (Hprefix x _ x0 _ ys ys0); auto.
-
- rewrite_for y0.
- apply H2 with (obj2:=x0) in H1; auto.
- apply app_same in H15.
- apply H4 with (obj2:=(Array32 xs0)) in H3; auto.
- inversion H3.
- rewrite H1.
- reflexivity.
-
- rewrite H16 in H0.
- simpl in H0.
- apply ascii32_of_nat_eq in H0; auto.
- inversion H0.
- rewrite <- H29 in H.
- rewrite <- H14 in H.
- inversion H.
- rewrite_for t0.
- rewrite_for t5.
- rewrite_for t6.
- rewrite_for t7.
- rewrite_for ys.
- assumption.
-Qed.
-
-Lemma soundness_fixmap_cons: forall x1 x2 xs y1 y2 ys b1 b2 b3 b4 b5 b6 b7 b8,
- Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
- Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length ((x1,x2)::xs)) ->
- Serialized x1 y1 -> Soundness x1 y1 ->
- Serialized x2 y2 -> Soundness x2 y2 ->
- Serialized (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
- Soundness (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
- Soundness (FixMap ((x1, x2) :: xs)) (Ascii b5 b6 b7 b8 false false false true :: y1 ++ y2 ++ ys).
-Proof.
-unfold Soundness.
-intros.
-inversion H8.
- rewrite_for b5.
- rewrite_for b6.
- rewrite_for b7.
- rewrite_for b8.
- apply ascii8_not_O in H0; [ contradiction |].
- split; [ simpl; omega |].
- inversion H9.
- transitivity (pow 4); [| apply pow_lt]; auto.
-
- rewrite_for obj2.
- inversion H9.
- inversion H10.
- generalize prefix.
- unfold Prefix.
- intro Hprefix.
- assert (y1 = y0).
- apply (Hprefix x1 _ x0 _ (y2 ++ ys) (y3 ++ ys0)); auto.
-
- rewrite_for y0.
- apply app_same in H15.
- assert (y2 = y3).
- apply (Hprefix x2 _ x3 _ ys ys0); auto.
-
- rewrite_for y3.
- apply H2 with (obj2:=x0) in H1; auto.
- apply H4 with (obj2:=x3) in H3; auto.
- apply H6 with (obj2:=(FixMap xs0)) in H5; auto.
- inversion H5.
- rewrite H1, H3.
- reflexivity.
-
- rewrite H18 in H0.
- simpl in H0.
- apply ascii8_of_nat_eq in H0; [| transitivity (pow 4); [| apply pow_lt]; auto
- | transitivity (pow 4); [| apply pow_lt]; auto].
- inversion H0.
- rewrite <- H36 in H.
- rewrite <- H17 in H.
- inversion H.
- rewrite_for b0.
- rewrite_for b9.
- rewrite_for b10.
- rewrite_for b11.
- apply app_same in H15.
- rewrite_for ys.
- assumption.
-Qed.
-
-Lemma soundness_map16_cons: forall x1 x2 xs y1 y2 ys s1 s2 t1 t2,
- (t1, t2) = ascii16_of_nat (length xs) ->
- (s1, s2) = ascii16_of_nat (length ((x1, x2) :: xs)) ->
- Serialized x1 y1 ->
- Soundness x1 y1 ->
- Serialized x2 y2 ->
- Soundness x2 y2 ->
- Serialized (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
- Soundness (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
- Soundness (Map16 ((x1, x2) :: xs)) ("222" :: s1 :: s2 :: y1 ++ y2 ++ ys).
-Proof.
-unfold Soundness.
-intros.
-inversion H8.
- rewrite_for s1.
- rewrite_for s2.
- apply ascii16_not_O in H0; [ contradiction |].
- split; [ simpl; omega |].
- inversion H9.
- assumption.
-
- rewrite_for obj2.
- inversion H9.
- inversion H10.
- generalize prefix.
- unfold Prefix.
- intro Hprefix.
- assert (y1 = y0).
- apply (Hprefix x1 _ x0 _ (y2 ++ ys) (y3 ++ ys0)); auto.
-
- rewrite_for y0.
- apply app_same in H13.
- assert (y2 = y3).
- apply (Hprefix x2 _ x3 _ ys ys0); auto.
-
- rewrite_for y3.
-
- apply H2 with (obj2:=x0) in H1; auto.
- apply H4 with (obj2:=x3) in H3; auto.
- apply H6 with (obj2:=(Map16 xs0)) in H5; auto.
- inversion H5.
- rewrite H1, H3.
- reflexivity.
-
- rewrite H15 in H0.
- simpl in H0.
- apply ascii16_of_nat_eq in H0; auto.
- inversion H0.
- rewrite <- H34 in H.
- rewrite <- H14 in H.
- inversion H.
- rewrite_for t0.
- rewrite_for t3.
- apply app_same in H13.
- rewrite_for ys.
- assumption.
-Qed.
-
-Lemma soundness_map32_cons : forall x1 x2 xs y1 y2 ys s1 s2 s3 s4 t1 t2 t3 t4,
- (t1, t2, (t3, t4)) = ascii32_of_nat (length xs) ->
- (s1, s2, (s3, s4)) = ascii32_of_nat (length ((x1, x2) :: xs)) ->
- Serialized x1 y1 ->
- Soundness x1 y1 ->
- Serialized x2 y2 ->
- Soundness x2 y2 ->
- Serialized (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
- Soundness (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
- Soundness (Map32 ((x1, x2) :: xs)) ("223" :: s1 :: s2 :: s3 :: s4 :: y1 ++ y2 ++ ys).
-Proof.
-unfold Soundness.
-intros.
-inversion H8.
- rewrite_for s1.
- rewrite_for s2.
- rewrite_for s3.
- rewrite_for s4.
- apply ascii32_not_O in H0; [ contradiction |].
- split; [ simpl; omega |].
- inversion H9.
- assumption.
-
- rewrite_for obj2.
- inversion H9.
- inversion H10.
- generalize prefix.
- unfold Prefix.
- intro Hprefix.
- assert (y1 = y0).
- apply (Hprefix x1 _ x0 _ (y2 ++ ys) (y3 ++ ys0)); auto.
-
- rewrite_for y0.
- apply app_same in H15.
- assert (y2 = y3).
- apply (Hprefix x2 _ x3 _ ys ys0); auto.
-
- rewrite_for y3.
- apply H2 with (obj2:=x0) in H1; auto.
- apply H4 with (obj2:=x3) in H3; auto.
- apply H6 with (obj2:=(Map32 xs0)) in H5; auto.
- inversion H5.
- rewrite H1, H3.
- reflexivity.
-
- rewrite H18 in H0.
- simpl in H0.
- apply ascii32_of_nat_eq in H0; auto.
- inversion H0.
- rewrite <- H36 in H.
- rewrite <- H17 in H.
- inversion H.
- rewrite_for t0.
- rewrite_for t5.
- rewrite_for t6.
- rewrite_for t7.
- apply app_same in H15.
- rewrite_for ys.
- assumption.
-Qed.
-
-Hint Resolve
- soundness_true soundness_false
- soundness_nil soundness_pfixnum soundness_nfixnum
- soundness_uint8 soundness_uint16 soundness_uint32 soundness_uint64
- soundness_int8 soundness_int16 soundness_int32 soundness_int64
- soundness_float soundness_double
- soundness_raw16 soundness_raw32
- soundness_fixarray_nil soundness_array16_nil soundness_array32_nil
- soundness_fixmap_nil soundness_map16_nil soundness_map32_nil
- : soundness.
-
-Lemma soundness_intro: forall obj x,
- (Serialized obj x -> Soundness obj x)->
- Soundness obj x.
-Proof.
-unfold Soundness.
-intros.
-apply H in H1; auto.
-Qed.
-
-Theorem soundness : forall obj1 x,
- Soundness obj1 x.
-Proof.
-intros.
-apply soundness_intro.
-intro.
-pattern obj1,x.
-apply Serialized_ind; intros; auto with soundness.
- apply soundness_fixraw; auto.
- apply soundness_fixarray_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
- apply soundness_array16_cons with (t1:=t1) (t2:=t2); auto.
- apply soundness_array32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
- apply soundness_fixmap_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
- apply soundness_map16_cons with (t1:=t1) (t2:=t2); auto.
- apply soundness_map32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
-Qed.
diff --git a/ocaml/proof/Util.v b/ocaml/proof/Util.v
deleted file mode 100644
index 1e104b36..00000000
--- a/ocaml/proof/Util.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Ascii List.
-Require Import ExtractUtil.
-
-Definition mlchar_of_ascii a :=
- mlchar_of_mlint (mlint_of_nat (Ascii.nat_of_ascii a)).
-Definition mlstring_of_string s :=
- mlstring_of_list mlchar_of_ascii (list_of_string s).
-Definition ascii_of_mlchar c :=
- Ascii.ascii_of_nat (nat_of_mlint (mlint_of_mlchar c)).
-Definition string_of_mlstring s :=
- string_of_list (list_of_mlstring ascii_of_mlchar s).
-
-Definition print s := print_mlstring (mlstring_of_string s).
-Definition println s := println_mlstring (mlstring_of_string s).
-Definition prerr s := prerr_mlstring (mlstring_of_string s).
-Definition prerrln s := prerrln_mlstring (mlstring_of_string s).
-
-CoFixpoint lmap {A B:Type} (f: A -> B) (xs : llist A) : llist B :=
- match xs with
- | LNil => LNil
- | LCons x xs => LCons (f x) (lmap f xs)
- end.
-
-Fixpoint ltake {A:Type} n (xs: llist A) :=
- match (n, xs) with
- | (O, _) => List.nil
- | (_, LNil) => List.nil
- | (S n', LCons x xs) => List.cons x (ltake n' xs)
- end.
-
-Definition get_contents := lmap ascii_of_mlchar get_contents_mlchars.
-
-Definition id {A:Type} (x:A) := x.
-
-Definition atat {A B:Type} (f:A -> B) (x: A) := f x.
-Infix "@@" := atat (right associativity, at level 75).
-
-Definition doll {A B C:Type} (g:B->C) (f:A->B) (x:A) := g (f x).
-Infix "$" := doll (at level 75).