search

Lysxia / coq-ceres

Coq library for serialization to S-expressions
MIT License
18 stars 1 forks source link

Deserialize: nullary constructors cannot be numbers #16

Open liyishuai opened 4 years ago

liyishuai commented 4 years ago

Is it a bug or feature?

Instance Deserialize__unit : Deserialize unit :=
  Deser.match_con "unit type" [("204", tt)] [].

Goal (from_string "204" = inl
        (DeserError [ ]
           ("could not read type '" ++ "unit type" ++ "', " ++
            "unexpected atom (expected list or nullary constructor name)"))).
Proof. reflexivity. Qed.
Lysxia commented 4 years ago

I'd classify that as working as expected, but it might also be a good idea to generalize match_con a little. At the same time, the match_con stuff is really meant to be used in a very formulaic manner entirely derived from the type declaration. If you want to have any say in the encoding, you might want to just pattern-match on the S-expression directly in this definition.

liyishuai commented 4 years ago

Yea I can live with this feature, provided documentation.

Lysxia commented 4 years ago

Sadly, generalizing match_con to allow arbitrary atoms as constructor tags breaks the current API. I hoped coercions would smooth this out but they don't. We could have the generalized version as a separate function, but I still feel like this is a rather odd use case. Instead, I can add some documentation about defining parsers by manual pattern-matching.