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).