Skip to content

Commit

Permalink
Merge pull request #177 from LPCIC/replace-clause
Browse files Browse the repository at this point in the history
New attribute :replace
  • Loading branch information
gares authored Mar 29, 2023
2 parents 6d9608b + 24cdb1b commit e8b50c7
Show file tree
Hide file tree
Showing 12 changed files with 82 additions and 7 deletions.
5 changes: 5 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,8 @@
# UNRELEASED

- Elpi:
- New attribute `:replace` which replaces a named clause by an unnamed one

# v1.16.9 (March 2023)

Requires Menhir 20211230 and OCaml 4.08 or above.
Expand Down
20 changes: 19 additions & 1 deletion ELPI.md
Original file line number Diff line number Diff line change
Expand Up @@ -241,7 +241,25 @@ such clause using the `:before` attribute.
fatal-error Msg :- !, M is "elpi: " ^ Msg, coq-err M.
```

The `:after` attribute is also available.
The `:after` and `:replace` attributes is also available.

The `:replace` attribute cannot be given to a named clause. This is to avoid
the following ambiguity:

```prolog
:name "replace-me"
p 1.
% from one accumulated file
:replace "replace-me" :name "replace-me"
p 2.
% from another accumulated file
:replace "replace-me" :name "replace-me"
p 3.
```
Here the order in which replacement is performed would matter.


## Conditional compilation

Expand Down
22 changes: 18 additions & 4 deletions src/compiler.ml
Original file line number Diff line number Diff line change
Expand Up @@ -559,6 +559,8 @@ end = struct (* {{{ *)
error ~loc ("duplicate attribute " ^ s) in
let illegal_err a =
error ~loc ("illegal attribute " ^ show_raw_attribute a) in
let illegal_replace s =
error ~loc ("replacing clause for "^ s ^" cannot have a name attribute") in
let rec aux r = function
| [] -> r
| Name s :: rest ->
Expand All @@ -570,13 +572,21 @@ end = struct (* {{{ *)
| Before s :: rest ->
if r.insertion <> None then duplicate_err "insertion";
aux { r with insertion = Some (Before s) } rest
| Replace s :: rest ->
if r.insertion <> None then duplicate_err "insertion";
aux { r with insertion = Some (Replace s) } rest
| If s :: rest ->
if r.ifexpr <> None then duplicate_err "if";
aux { r with ifexpr = Some s } rest
| (External | Index _) as a :: _-> illegal_err a
in
{ c with Clause.attributes =
aux { insertion = None; id = None; ifexpr = None } attributes }
let attributes = aux { insertion = None; id = None; ifexpr = None } attributes in
begin
match attributes.insertion, attributes.id with
| Some (Replace x), Some _ -> illegal_replace x
| _ -> ()
end;
{ c with Clause.attributes }

let structure_chr_attributes ({ Chr.attributes; loc } as c) =
let duplicate_err s =
Expand All @@ -590,7 +600,7 @@ end = struct (* {{{ *)
| If s :: rest ->
if r.cifexpr <> None then duplicate_err "if";
aux { r with cifexpr = Some s } rest
| (Before _ | After _ | External | Index _) as a :: _ -> illegal_err a
| (Before _ | After _ | Replace _ | External | Index _) as a :: _ -> illegal_err a
in
let cid = Loc.show loc in
{ c with Chr.attributes = aux { cid; cifexpr = None } attributes }
Expand All @@ -614,7 +624,7 @@ end = struct (* {{{ *)
| Some (Structured.Index _) -> duplicate_err "index"
| Some _ -> error ~loc "external predicates cannot be indexed"
end
| (Before _ | After _ | Name _ | If _) as a :: _ -> illegal_err a
| (Before _ | After _ | Replace _ | Name _ | If _) as a :: _ -> illegal_err a
in
let attributes = aux None attributes in
let attributes =
Expand Down Expand Up @@ -1910,8 +1920,12 @@ end = struct (* {{{ *)
match l, loc_name with
| [],_ -> error ~loc:c.Ast.Clause.loc ("unable to graft this clause: no clause named " ^
match loc_name with
| Ast.Structured.Replace x -> x
| Ast.Structured.After x -> x
| Ast.Structured.Before x -> x)
| { Ast.Clause.attributes = { Assembled.id = Some n }} :: xs,
Ast.Structured.Replace name when n = name ->
c :: xs
| { Ast.Clause.attributes = { Assembled.id = Some n }} as x :: xs,
Ast.Structured.After name when n = name ->
c :: x :: xs
Expand Down
3 changes: 2 additions & 1 deletion src/parser/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -133,6 +133,7 @@ type raw_attribute =
| Name of string
| After of string
| Before of string
| Replace of string
| External
| Index of int list
[@@deriving show]
Expand Down Expand Up @@ -299,7 +300,7 @@ and attribute = {
id : string option;
ifexpr : string option;
}
and insertion = Before of string | After of string
and insertion = Before of string | After of string | Replace of string
and cattribute = {
cid : string;
cifexpr : string option
Expand Down
3 changes: 2 additions & 1 deletion src/parser/ast.mli
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ type raw_attribute =
| Name of string
| After of string
| Before of string
| Replace of string
| External
| Index of int list
[@@ deriving show]
Expand Down Expand Up @@ -205,7 +206,7 @@ and attribute = {
id : string option;
ifexpr : string option;
}
and insertion = Before of string | After of string
and insertion = Before of string | After of string | Replace of string
and cattribute = {
cid : string;
cifexpr : string option
Expand Down
2 changes: 2 additions & 0 deletions src/parser/grammar.mly
Original file line number Diff line number Diff line change
Expand Up @@ -294,6 +294,7 @@ attribute:
| NAME; s = STRING { Name s }
| AFTER; s = STRING { After s }
| BEFORE; s = STRING { Before s }
| REPLACE; s = STRING { Replace s }
| EXTERNAL { External }
| INDEX; LPAREN; l = nonempty_list(indexing) ; RPAREN { Index l }

Expand Down Expand Up @@ -393,6 +394,7 @@ constant:
| NAME { Func.from_string "name" }
| BEFORE { Func.from_string "before" }
| AFTER { Func.from_string "after" }
| REPLACE { Func.from_string "replace" }
| INDEX { Func.from_string "index" }
| c = IO { Func.from_string @@ String.make 1 c }
| CUT { Func.cutf }
Expand Down
1 change: 1 addition & 0 deletions src/parser/lexer.mll.in
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,7 @@ and token = parse
| "sigma" { SIGMA }
| "after" { AFTER }
| "before" { BEFORE }
| "replace" { REPLACE }
| "name" { NAME }
| "if" { IF }
| "index" { INDEX }
Expand Down
1 change: 1 addition & 0 deletions src/parser/test_lexer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ type t = Tokens.token =
| SHORTEN
| RULE
| RPAREN
| REPLACE
| RCURLY
| RBRACKET
| QUOTED of ( string )
Expand Down
1 change: 1 addition & 0 deletions src/parser/tokens.mly
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,7 @@
%token IF
%token BEFORE
%token AFTER
%token REPLACE
%token NAME
%token INDEX
%token CONS
Expand Down
9 changes: 9 additions & 0 deletions tests/sources/graft_replace_err.elpi
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
pred p o:int.
:name "replace_me"
p 1.

:name "foo"
:replace "replace_me"
p 2.

main :- fail.
9 changes: 9 additions & 0 deletions tests/sources/graft_replace_ok.elpi
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
pred p o:int.
:name "replace_me"
p 1.

:replace "replace_me"
p 2.

main :-
std.findall (p _) [p 2].
13 changes: 13 additions & 0 deletions tests/suite/elpi_specific.ml
Original file line number Diff line number Diff line change
Expand Up @@ -290,6 +290,19 @@ let () = declare "IO_COLON"
~typecheck:true
()

let () = declare "graft_replace_ok"
~source_elpi:"graft_replace_ok.elpi"
~description:"replacing a clase"
~typecheck:true
()

let () = declare "graft_replace_err"
~source_elpi:"graft_replace_err.elpi"
~description:"replacing a clase"
~typecheck:true
~expectation:Test.(FailureOutput (Str.regexp "name attribute"))
()

let mk_tmp_file =
let tmp = ref 0 in
let dir = Filename.get_temp_dir_name () in
Expand Down

0 comments on commit e8b50c7

Please sign in to comment.