From 24cdb1baf60c13a0de154578cb39f4ae1f97b706 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 29 Mar 2023 15:37:25 +0200 Subject: [PATCH] New attribute :replace --- CHANGES.md | 5 +++++ ELPI.md | 20 +++++++++++++++++++- src/compiler.ml | 22 ++++++++++++++++++---- src/parser/ast.ml | 3 ++- src/parser/ast.mli | 3 ++- src/parser/grammar.mly | 2 ++ src/parser/lexer.mll.in | 1 + src/parser/test_lexer.ml | 1 + src/parser/tokens.mly | 1 + tests/sources/graft_replace_err.elpi | 9 +++++++++ tests/sources/graft_replace_ok.elpi | 9 +++++++++ tests/suite/elpi_specific.ml | 13 +++++++++++++ 12 files changed, 82 insertions(+), 7 deletions(-) create mode 100644 tests/sources/graft_replace_err.elpi create mode 100644 tests/sources/graft_replace_ok.elpi diff --git a/CHANGES.md b/CHANGES.md index 432799106..6dcdb5b51 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -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. diff --git a/ELPI.md b/ELPI.md index 7cdadf1a9..c3d05ae3e 100644 --- a/ELPI.md +++ b/ELPI.md @@ -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 diff --git a/src/compiler.ml b/src/compiler.ml index be6c33dfc..24036aacc 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -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 -> @@ -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 = @@ -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 } @@ -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 = @@ -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 diff --git a/src/parser/ast.ml b/src/parser/ast.ml index 17c403179..b9dc05b06 100644 --- a/src/parser/ast.ml +++ b/src/parser/ast.ml @@ -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] @@ -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 diff --git a/src/parser/ast.mli b/src/parser/ast.mli index 09f127fa2..e44625ee7 100644 --- a/src/parser/ast.mli +++ b/src/parser/ast.mli @@ -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] @@ -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 diff --git a/src/parser/grammar.mly b/src/parser/grammar.mly index 709dcd91a..d78ed9009 100644 --- a/src/parser/grammar.mly +++ b/src/parser/grammar.mly @@ -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 } @@ -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 } diff --git a/src/parser/lexer.mll.in b/src/parser/lexer.mll.in index f9cebdcd7..2b731cec8 100644 --- a/src/parser/lexer.mll.in +++ b/src/parser/lexer.mll.in @@ -164,6 +164,7 @@ and token = parse | "sigma" { SIGMA } | "after" { AFTER } | "before" { BEFORE } +| "replace" { REPLACE } | "name" { NAME } | "if" { IF } | "index" { INDEX } diff --git a/src/parser/test_lexer.ml b/src/parser/test_lexer.ml index 5719a3664..2895675f7 100644 --- a/src/parser/test_lexer.ml +++ b/src/parser/test_lexer.ml @@ -14,6 +14,7 @@ type t = Tokens.token = | SHORTEN | RULE | RPAREN + | REPLACE | RCURLY | RBRACKET | QUOTED of ( string ) diff --git a/src/parser/tokens.mly b/src/parser/tokens.mly index ae4cfccb3..f4e919b56 100644 --- a/src/parser/tokens.mly +++ b/src/parser/tokens.mly @@ -57,6 +57,7 @@ %token IF %token BEFORE %token AFTER +%token REPLACE %token NAME %token INDEX %token CONS diff --git a/tests/sources/graft_replace_err.elpi b/tests/sources/graft_replace_err.elpi new file mode 100644 index 000000000..fc0764b0b --- /dev/null +++ b/tests/sources/graft_replace_err.elpi @@ -0,0 +1,9 @@ +pred p o:int. +:name "replace_me" +p 1. + +:name "foo" +:replace "replace_me" +p 2. + +main :- fail. \ No newline at end of file diff --git a/tests/sources/graft_replace_ok.elpi b/tests/sources/graft_replace_ok.elpi new file mode 100644 index 000000000..ffec625a0 --- /dev/null +++ b/tests/sources/graft_replace_ok.elpi @@ -0,0 +1,9 @@ +pred p o:int. +:name "replace_me" +p 1. + +:replace "replace_me" +p 2. + +main :- + std.findall (p _) [p 2]. \ No newline at end of file diff --git a/tests/suite/elpi_specific.ml b/tests/suite/elpi_specific.ml index ba8b5c0f8..ffd4a1d88 100644 --- a/tests/suite/elpi_specific.ml +++ b/tests/suite/elpi_specific.ml @@ -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