Li-yao (Apr 01 2024 at 11:31): Li-yao (Apr 01 2024 at 11:31):Why does String Notation require the name of an inductive type only, rather than any constant of the right type? What if I want a notation for list bool? I could use via but that seems like a lot of boilerplate?
Julin Shaji (Apr 01 2024 at 13:54):I too once wanted something like list bool. Ended up making a new isomorphic type for it.
https://tildegit.org/famubu/playground/src/branch/master/coq/string_notation.v
How does a syntax with via look like?
I didn't really understand what's mentioned at https://coq.inria.fr/doc/V8.19.0/refman/user-extensions/syntax-extensions.html#string-notations
Li-yao (Apr 01 2024 at 18:46):Here's an example:
From Coq Require Import List Strings.Byte.
Import ListNotations.
Inductive adhoc_list_bool : Set :=
| Nil
| Cons : bool -> adhoc_list_bool -> adhoc_list_bool.
Definition list_bool := list bool.
Fixpoint parse_binary (s : list Byte.byte) : adhoc_list_bool :=
match s with
| c :: s =>
if Byte.eqb c "0" then Cons false (parse_binary s)
else if Byte.eqb c "1" then Cons true (parse_binary s)
else Nil
| [] => Nil
end.
Fixpoint print_binary (x : adhoc_list_bool) : list Byte.byte :=
match x with
| Nil => nil
| Cons b s => (if b then "0" else "1")%byte :: print_binary s
end.
Declare Scope bstr_scope.
Delimit Scope bstr_scope with bstr.
Bind Scope bstr_scope with list_bool.
String Notation list_bool
parse_binary (* (1) Parse notation to adhoc_list_bool *)
print_binary
(via adhoc_list_bool mapping
[ [nil] => Nil, (* (2) Replace Nil with nil and Cons with cons *)
[cons] => Cons
]) : bstr_scope.
Definition a : list_bool := "010".
Print a.
It needs to be an inductive because printing is dispatched on constructors unless via is given. But parameterized inductives work fine, e.g.,
Notation string := (list Byte.byte).
Definition id_string := @id string.
String Notation string id_string id_string : list_scope.
from the test suite. The limitation of requiring a name rather than a term is just a syntactic / engineering issue, if you want to extend the grammar to accept terms and not just names, feel free to.
Last updated: Oct 13 2024 at 01:02 UTC