Stream: Coq users

Topic: Why String Notation takes an inductive type


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Jason Gross (Apr 04 2024 at 09:58):

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: Jun 23 2024 at 04:03 UTC