attr.elpi

/*
 * Copyright (C) BlueRock Security Inc. 2022-2024
 *
 * SPDX-License-Identifier: LGPL-2.1 WITH BedRock Exception for use over network, see repository root for details.
 */

/** * Attribute parser for Elpi commands */
/**
OVERVIEW

[attr.parse (E : string -> prop) (F : string -> list A -> prop) (ElpiOpts : list prop) (Opts
: list A) : prop] parses non-Elpi attributes from left to right, using
predicate [E] to report errors, using predicate [F] to map each
attribute's name to its list of options [O : list A], and generating
an output list [Opts] of all options (reversing their order).
Elpi attributes are assumed while <<F>> runs and output in <<ElpiOpts>>.

The error predicate [E Msg] receives an error message [Msg]. It should
panic (e.g., using [coq.error]).

The user-supplied attribute parsing predicate [F (N : string) (O :
list A) : prop] receives each attribute's name [N], in turn. If it
fails, [attr.parse] rejects the attribute with an error. If it
succeeds, it should generate a list of options [O] to be included in
the list returned by [attr.parse]. It may use any of the following
attribute value parsers to relate the attribute's options [O] to its
value.


ATTRIBUTE VALUE PARSERS

Attribute value parsers presuppose attribute parsing is ongoing. They
examine the current attribute's _value_ (of type [attribute-value]).

***Type-based parsers.*** The simplest attribute value parsers require
the current attribute's value to have a certain type and report type
errors using the error predicate [E] passed to [attr.parse]:

- [attr.is-string (S : string) : prop]

- [attr.is-loc (L : loc) : prop]

- [attr.is-map-norecurse (M : list attribute) : prop]

***String parsers.*** A few parsers require the current attribute's
value to be a string of a certain form and report parse errors using
the error predicate [E] passed to [attr.parse]:

- [attr.is-no-value : prop] (accepts the empty string)

- [attr.is-nonempty-string (S : string) : prop] (accepts a non-empty
string [S])

- [attr.is-bool (B : bool) : prop] (accepts a boolean value [B] parsed
the same as in Elpi's attribute parser)

***Attribute map parser.*** The following parser requires the current
attribute's value to be an attribute map and recursively parses its
attributes (left-to-right) using the given predicate [F], generating
an output list [O] of all options (preserving their order).

- [attr.is-map (F : string -> list A -> prop) (O : list A) : prop]


EXAMPLE

The following command accepts attributes [e] carrying no value, [b]
carrying a boolean, [s] carrying a non-empty string, and [m(v)]
carrying an arbitrary string.

<<
  Require Import bedrock.elpi.extra.extra.
  Elpi Command TestAttr.
  Elpi Accumulate File extra.Command.
  Elpi Accumulate lp:{{

    % Some defaults
    pred flage o:bool.	flage ff.
    pred flagb o:bool.	flagb ff.
    pred flags o:string.	flags "S".
    pred flagm o:option string.	flagm none.

    pred parse i:string, o:list prop.
    parse "e" [flage tt] :- attr.is-no-value.
    parse "b" [flagb B] :- attr.is-bool B.
    parse "s" [flags S] :- attr.is-nonempty-string S.
    parse "m" O :- attr.is-map parsem O.

    pred parsem i:string, o:list prop.
    parsem "v" [flagm (some S)] :- attr.is-string S.

    main _ :-
      attr.parse (msg\ coq.error msg) parse _ Opts,
      Opts => coq.say "flage" {flage} "flagb" {flagb} "flags" {flags} "flagm" {flagm}.
  }}.
  Elpi Export TestAttr.
>>


DIAGNOSTIC-BASED ATTRIBUTE VALUE PARSERS

The preceding attribute value parsers [attr.is-X] have variants
[attr.check-X] that report errors via a trailing output term of type
[diagnostic], rather than by invoking the error predicate [E] passed
to [attr.parse]. (Example: [attr.check-string (S : string) (D :
diagnostic) : prop] is the diagnostic-based parser for strings.)


UTILITIES

- [attr.expects (What : string) (Msg : string) : prop] generates an
error message [Msg] of the form "Attribute PATH expects WHAT" where
[PATH] identifies the current attribute.

- [attr.report (Msg : string) : prop] reports an error message [Msg]
using the error predicate [E] passed to [attr.parse].

- [attr.assert-ok! (P : diagnostic -> prop) : prop] reports any error
diagnostic generated by [P] using the error predicate [E] passed to
[attr.parse].


OTHER ENTRY POINTS

The following variants on [attr.parse] are also available.

- [attr.parse-list (A : list attribute) (E : string -> prop) (F :
string -> list A -> prop) (Opts : list A) : prop] is a variant of
[attr.parse] that takes a list [A] of attributes to parse and does
not distinguish Elpi attributes.

- [attr.continue-parsing (A : list attribute) (F : string -> list A ->
prop) (Opts : list A) : prop] is a varaint of [attr.parse-list] that
(i) takes no error predicate because it presupposes attribute parsing
is ongoing and (ii) does not reverse its output list.


CONTEXT

The following low-level predicates presuppose attribute parsing is
ongoing.

- [attr.get-error (E : string -> prop) : prop] returns the error
predicate [E] passed to [attr.parse] or [attr.parse-with-usage].

- [attr.get-path (P : attr.path) : prop] returns the path [P] of the
current attribute. An attribute's _path_ names the attribute as well
as any enclosing attribute maps. The auxiliary predicate
[attr.path->string (P : attr.path) (S : string) : prop] converts a
path to a dot-separated string. (Example: Parsing
[#[cats(dogs=bunnies)]] visits attributes with paths "cats" and
"cats.dogs".)

- [attr.get-name (N : string) : prop] returns the name [N] of the
current attribute. (Example: Parsing [#[cats(dogs=bunnies)]] visits
attributes named "cats" and "dogs".)

- [attr.get-value (V : attribute-value) : prop] returns the value [V]
of the current attribute.


SEE ALSO

Elpi comes with a library for parsing attributes. Compared to that
library, this library

- does not support [oneof]

- does not force use of [get-option], except for Elpi attributes

- does not take a term describing supported attributes

*/

namespace attr {

  %%% Entry points

  pred continue-parsing i:list attribute, i:(string -> list A -> prop), o:list A.
  pred parse-list i:list attribute, i:(string -> prop) i:(string -> list A -> prop), o:list A.
  pred parse i:(string -> prop) i:(string -> list A -> prop), o:list prop, o:list A.

  %%% Context

  kind path type.
  pred path->string i:path, o:string.

  pred get-error o:(string -> prop).
  pred get-path o:path.
  pred get-name o:string.
  pred get-value o:attribute-value.

  %%% Errors

  pred report i:string.
  pred assert-ok! i:diagnostic -> prop.
  pred expects i:string o:string.

  %%% Attribute values

  pred check-string o:string, o:diagnostic.
  pred is-string o:string.

  pred check-no-value o:diagnostic.	% Empty string
  pred is-no-value.

  pred check-nonempty-string o:string, o:diagnostic.
  pred is-nonempty-string o:string.

  pred check-bool o:bool, o:diagnostic.	% String as a boolean
  pred is-bool o:bool.

  pred check-loc o:loc, o:diagnostic.
  pred is-loc o:loc.

  pred check-map-norecurse o:list attribute, o:diagnostic.
  pred is-map-norecurse o:list attribute.

  pred check-map i:(string -> list A -> prop), o:list A, o:diagnostic.	% Continue parsing
  pred is-map i:(string -> list A -> prop), o:list A.

}

namespace attr {

  %%% Paths

  type path.rev list string -> attr.path.

  pred path.nil o:attr.path.
  path.nil (path.rev []).

  pred path.snoc i:string, i:attr.path, o:attr.path.
  path.snoc Name (path.rev Path) (path.rev [Name|Path]).

  path->string (path.rev Path) S :-
    std.string.concat "." {std.rev Path} S.

  pred path.dot i:attr.path, i:string, o:string.
  path.dot Path Id S :- path->string {path.snoc Id Path} S.

  %%% Context

  namespace internal {
    type error (string -> prop) -> prop.
    type path attr.path -> prop.
    type name string -> prop.
    type value attribute-value -> prop.

    pred not-running i:string.
    not-running Whence :-
      coq.error {calc (Whence ^ ": attribute parser not running")}.

    pred get! i:string, i:prop.
    get! _ P :- P, !.
    get! Whence _ :- not-running Whence.

  }

  get-error E :- internal.get! "attr.get-error" (internal.error E).
  get-path P :- internal.get! "attr.get-path" (internal.path P).
  get-name N :- internal.get! "attr.get-name" (internal.name N).
  get-value V :- internal.get! "attr.get-value" (internal.value V).

  %%% Errors

  report Msg :- get-error E, E Msg.
  assert-ok! F :-
    F D, !,
    if (D = error Msg) (report Msg) true.
  expects What Msg :-
    Msg is ("Attribute " ^ { path->string {get-path} } ^ " expects " ^ What).

  %%% Entry points

  continue-parsing L F O :-
    if (internal.error _) true (internal.not-running "attr.continue-parsing"),
    std.map L (a\ l\ sigma Prefix Path N V\
      a = attribute N V,
      get-path Prefix,
      path.snoc N Prefix Path,
      internal.path Path =>
      internal.name N =>
      internal.value V =>
      if (F N l) true (
        sigma FullName Msg\
        path->string Path FullName,
        Msg is "Unexpected attribute: " ^ FullName,
        report Msg
      )
    ) Lists,
    std.flatten Lists O.

  parse-list L E F O :-
    path.nil Nil,
    internal.path Nil =>
    internal.error E =>
    continue-parsing L F O',
    std.rev O' O.

  parse E F ElpiOpts O :- std.do! [
    list.partition {attributes} parse.elpi Elpi User,
    std.map-filter Elpi parse.option ElpiOpts,
    ElpiOpts => parse-list User E F O,
  ].
  namespace parse {

    pred elpi i:attribute.	% May fail
    elpi (attribute N _) :- rex.match "^elpi\\." N.

    pred option i:attribute, o:prop.	% May fail
    option (attribute N (leaf-loc L)) (get-option N L).
    option (attribute N (leaf-str S)) (get-option N S).

  }

  %%% Attribute value parsers

  check-string S D :-
    get-value V,
    if (V = leaf-str S) (D = ok) (D is error {expects "a string"}).
  is-string S :- assert-ok! (check-string S).

  check-no-value D :- std.do-ok! D [
    check-string S,
    check-no-value.aux S,
  ].
  pred check-no-value.aux i:string, o:diagnostic.
  check-no-value.aux S D :-
    if (S = "") (D = ok) (D is error {expects "no value"}).
  is-no-value :- assert-ok! (check-no-value).

  check-nonempty-string S D :- std.do-ok! D [
    check-string S,
    check-nonempty-string.aux S,
  ].
  pred check-nonempty-string.aux i:string, o:diagnostic.
  check-nonempty-string.aux S D :-
    if (S = "") (D is error {expects "a non-empty string"}) (D = ok).
  is-nonempty-string S :- assert-ok! (check-nonempty-string S).

  check-bool B D :- std.do-ok! D [
    check-string S,
    coq.typecheck-attribute { path->string {get-path} }
      {hack.bool-attribute-type} S B,
  ].
  % Plain [bool] above gets parsed as [bool : type].
  pred hack.bool-attribute-type o:attribute-type.
  hack.bool-attribute-type bool.
  is-bool B :- assert-ok! (check-bool B).

  check-loc L D :-
    get-value V,
    if (V = leaf-loc L) (D = ok) (D is error {expects "a location"}).
  is-loc L :- assert-ok! (check-loc L).

  check-map-norecurse L D :-
    get-value V,
    if (V = node L) (D = ok) (D is error {expects "an attribute list"}).
  is-map-norecurse L :- assert-ok! (check-map-norecurse L).

  check-map F O D :- std.do-ok! D [
    check-map-norecurse L,
    (d\ d = ok, continue-parsing L F O),
  ].
  is-map F O :- assert-ok! (check-map F O).

}