ident.elpi

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

/** * Coq identifiers */

namespace ident {

  % Gallina type <<Ident.rep>> in ltac2-extra

  pred of_rep_opt i:term, o:option id.	% May panic
  pred of_rep i:term, o:id.	% May panic
  pred as_rep i:id, o:term.

  /*
  Implementation
  */

  pred of_name i:name, o:option id.
  pred to_name i:option id, o:name.

  of_name N O :- std.do! [
    coq.name->id N Id,
    ( Id = "_", !, O = none
    ; O = some Id ),
  ].

  to_name O N :- std.do! [
    ( O = some Id, !
    ; Id = "_" ),
    coq.string->name Id N
  ].

  of_rep_opt T O :- std.do! [
    coq.eval_whd_all T Tred,
    ( Tred = {{ lib:bedrock.ltac2.extra.Ident.rep.Rep lp:{{ fun N _ _ }} }}, !, of_name N O
    ; coq.error "ident.of_rep_opt: Expected <<Ident.rep>> constructor:" {coq.term->string Tred} ),
  ].

  of_rep T Id :-
    ( of_rep_opt T (some Id), !
    ; coq.error "ident.of_rep: No name hint:" {coq.term->string T} ).

  as_rep Id T :- std.do! [
    coq.string->name Id N,
    T = {{ lib:bedrock.ltac2.extra.Ident.rep.Rep lp:{{ fun N {{ lib:core.unit.type }} (x\ {{ lib:core.unit.tt }}) }} }},
  ].

}