1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465(************************************************************************)(* v * The Coq Proof Assistant / The Coq Development Team *)(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(************************************************************************)(************************************************************************)(* Coq serialization API/Plugin *)(* Copyright 2016-2018 MINES ParisTech *)(************************************************************************)(* Status: Very Experimental *)(************************************************************************)openSexplibopenSexplib.StdopenPpx_hash_lib.Std.Hash.BuiltinopenPpx_compare_lib.Builtintypet=[%import:CPrimitives.t][@@deriving sexp,yojson,hash,compare]typeconst=[%import:CPrimitives.const][@@derivingsexp,yojson,hash](* XXX: GADTs ... *)type'aprim_type =[%import:'aCPrimitives.prim_type]and'aprim_ind=[%import:'aCPrimitives.prim_ind]andind_or_type=[%import:CPrimitives.ind_or_type][@@derivingsexp_of]letprim_type_of_sexp (x:Sexp.t):'aprim_type =matchxwith|Sexp.Atom"PT_int63"->PT_int63|Sexp.Atom"PT_float64"->PT_float64|Sexp.Atom"PT_array"->Obj.magicPT_array|_->Sexplib.Conv_error.no_variant_match()typeop_or_type=[%import:CPrimitives.op_or_type][@@derivingsexp_of]lethash_fold_op_or_typestx=hash_fold_stringst(Sexp.to_string(sexp_of_op_or_typex))letcompare_op_or_typexy=compare_string(Sexp.to_string(sexp_of_op_or_typex))(Sexp.to_string(sexp_of_op_or_typey))letop_or_type_of_sexp(x:Sexp.t):op_or_type=matchxwith|Sexp.List[Sexp.Atom"OT_op";p]->OT_op(t_of_sexpp)|Sexp.List[Sexp.Atom"OT_type";p]->OT_type(prim_type_of_sexpp)|Sexp.List[Sexp.Atom"OT_const";p]->OT_const(const_of_sexp p)|_->Sexplib.Conv_error.no_variant_match ()(* XXX *)letop_or_type_to_yojson=Obj.magicletop_or_type_of_yojson=Obj.magic