diff --git a/CHANGES.md b/CHANGES.md index f33f0967..a8fde2c6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,4 +1,10 @@ -## unreleased +## Version 0.19.2 + + - [serlib] Fix (@ejgallego, #398, fixes #397 fixes sr-lab/coqpyt#35 , + thanks to @laetitia-teo and @Nfsaavedra for the bug + report) + +## Version 0.19.1 - [serlib] Support `btauto` Coq plugin (@ejgallego, #362) - [serlib] Support `extraction` Coq plugin (@ejgallego, @toku-sa-n, diff --git a/serlib/ser_cPrimitives.ml b/serlib/ser_cPrimitives.ml index 1dc87cea..8b21b0bf 100644 --- a/serlib/ser_cPrimitives.ml +++ b/serlib/ser_cPrimitives.ml @@ -16,10 +16,12 @@ (* Written by: Emilio J. Gallego Arias and others *) (************************************************************************) -open Sexplib -open Sexplib.Std -open Ppx_hash_lib.Std.Hash.Builtin -open Ppx_compare_lib.Builtin +(* open Sexplib *) +(* open Sexplib.Std *) +(* open Ppx_hash_lib.Std.Hash.Builtin *) +(* open Ppx_compare_lib.Builtin *) + +module UVars = Ser_uvars type t = [%import: CPrimitives.t] @@ -27,42 +29,45 @@ type t = type const = [%import: CPrimitives.const] - [@@deriving sexp,yojson,hash] + [@@deriving sexp,yojson,hash,compare] + +(* GADTs ... *) +module PTP = struct -(* XXX: GADTs ... *) -type 'a prim_type = [%import: 'a CPrimitives.prim_type] -and 'a prim_ind = [%import: 'a CPrimitives.prim_ind] -and ind_or_type = [%import: CPrimitives.ind_or_type] - [@@deriving sexp_of] + type 'a t = 'a CPrimitives.prim_type -let prim_type_of_sexp (x : Sexp.t) : 'a prim_type = - match x with - | Sexp.Atom "PT_int63" -> - PT_int63 - | Sexp.Atom "PT_float64" -> - PT_float64 - | Sexp.Atom "PT_array" -> - Obj.magic PT_array - | _ -> - Sexplib.Conv_error.no_variant_match () + [@@@ocaml.warning "-27"] -type op_or_type = [%import: CPrimitives.op_or_type] - [@@deriving sexp_of] + (* Non-GADT version *) + type 'a _t = + | PT_int63 + | PT_float64 + | PT_array + [@@deriving sexp,yojson,hash,compare] +end -let hash_fold_op_or_type st x = hash_fold_string st (Sexp.to_string (sexp_of_op_or_type x)) -let compare_op_or_type x y = compare_string (Sexp.to_string (sexp_of_op_or_type x)) (Sexp.to_string (sexp_of_op_or_type y)) +module Prim_type_ = SerType.Pierce1(PTP) +type 'a prim_type = 'a Prim_type_.t + [@@deriving sexp,yojson,hash,compare] -let op_or_type_of_sexp (x : Sexp.t) : op_or_type = - match x with - | Sexp.List [Sexp.Atom "OT_op"; p] -> - OT_op (t_of_sexp p) - | Sexp.List [Sexp.Atom "OT_type"; p] -> - OT_type (prim_type_of_sexp p) - | Sexp.List [Sexp.Atom "OT_const"; p] -> - OT_const (const_of_sexp p) - | _ -> - Sexplib.Conv_error.no_variant_match () +module OOTP = struct -(* XXX *) -let op_or_type_to_yojson = Obj.magic -let op_or_type_of_yojson = Obj.magic + type ptype = + | PT_int63 + | PT_float64 + | PT_array + [@@deriving sexp,yojson,hash,compare] + + (* op_or_type *) + type _t = + | OT_op of t + | OT_type of ptype + | OT_const of const + [@@deriving sexp,yojson,hash,compare] + + type t = CPrimitives.op_or_type +end + +module Op_or_type_ = SerType.Pierce(OOTP) +type op_or_type = Op_or_type_.t + [@@deriving sexp,yojson,hash,compare] diff --git a/tests/genarg/dune b/tests/genarg/dune index 11ec5940..f1253f9e 100644 --- a/tests/genarg/dune +++ b/tests/genarg/dune @@ -161,3 +161,8 @@ (alias runtest) (deps (:input tactic_notation.v)) (action (run ./test_roundtrip %{input}))) + +(rule + (alias runtest) + (deps (:input primitives.v)) + (action (run ./test_roundtrip %{input}))) diff --git a/tests/genarg/primitives.v b/tests/genarg/primitives.v new file mode 100644 index 00000000..80608368 --- /dev/null +++ b/tests/genarg/primitives.v @@ -0,0 +1,11 @@ +Require Export CarryType. + +Primitive int := #int63_type. +Primitive lsl := #int63_lsl. + +Set Universe Polymorphism. + +Primitive array := #array_type. + +Primitive make : forall A, int -> A -> array A := #array_make. +Arguments make {_} _ _.