Luko van der Maas (Oct 31 2023 at 14:22): Luko van der Maas (Oct 31 2023 at 14:22):I am looking to add some predicates I have written to convert strings to Coq strings to the coq-elpi builtins, but I have reached a few problems. Where should I add the predicates, elpi/coq-HOAS.elpi? And what documentation should I write? And most importantly, can I quote coq in .elpi files like that and should I? I can't find any files that do it.
Luko van der Maas (Oct 31 2023 at 14:23):pred int->bools i:int, o:list bool.
pred int->bools.unpadded i:int, o:list bool.
int->bools.unpadded 0 [] :- !.
int->bools.unpadded INT BITS :-
if ({ calc (INT mod 2) } == 1) (BIT is tt) (BIT is ff),
BITS = [BIT | { int->bools.unpadded { calc (INT div 2) } }].
int->bools INT BITS :-
int->bools.unpadded INT BITSSHORT,
std.length BITSSHORT SIZE,
std.map { std.iota { calc (8 - SIZE) } } (x\ r\ r = ff) PADDING,
std.append BITSSHORT PADDING BITS.
pred string->ascii i:string, o:list (list bool).
string->ascii.aux INDEX STRING BS :-
INT is rhc (substring STRING INDEX 1),
int->bools INT BS.
string->ascii S BSS :-
LENGTH is size S,
std.map {std.iota LENGTH} (x\ r\ string->ascii.aux x S r) BSS.
pred string->stringterm i:string, o:term.
pred string->stringterm.aux i:list bool, i:term, o:term.
string->stringterm.aux X ACC RES :-
std.map X (x\ r\ if (x == tt) (r = {{ true }}) (r = {{ false }})) BITSTERM,
RES = app [{{ String }}, app [{{ Ascii }} | BITSTERM], ACC].
string->stringterm STRING T :-
string->ascii STRING BSS,
foldr BSS {{ EmptyString }} string->stringterm.aux T.
pred list->listterm i:list term, o:term.
list->listterm TS T :- foldr TS {{ [] }} (x\ a\ r\ r = {{ cons lp:x lp:a }}) T.
These are the predicates I am looking to add
Luko van der Maas (Oct 31 2023 at 14:24):Where this should be added to elpi for it to work
pred foldr i:list B, i:A, i:(B -> A -> A -> prop), o:A.
foldr [] A _ A.
foldr [X|XS] A F R :- foldr XS A F A', F X A' R.
fold_right should go here: https://github.com/LPCIC/elpi/blob/master/src/builtin_stdlib.elpi
the other should go to: https://github.com/LPCIC/coq-elpi/blob/master/elpi/coq-lib.elpi
Luko van der Maas (Oct 31 2023 at 14:46):When adding the others to coq-lib.ml and running make I get the following error:
File "./theories/elpi.v", line 8, characters 0-48:
Error: File "coq-builtin.elpi", line 510, column 31, character 21695::
The reference String was not found in the current
I get why it happens but don't know how I should fix it
Luko van der Maas (Oct 31 2023 at 15:02):I have added pull requests:
https://github.com/LPCIC/elpi/pull/203
https://github.com/LPCIC/coq-elpi/pull/530
Enrico Tassi (Oct 31 2023 at 15:10):I guess one way is to Require Import Stringin theories/elpi.v, but I'd need more time to think if this has side effects.
Last updated: Oct 13 2024 at 01:02 UTC