diff --git a/src/compiler.ml b/src/compiler.ml index b1b3621d9..5a0d9fc26 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -632,9 +632,16 @@ end = struct (* {{{ *) | Some Structured.External -> duplicate_err "external" | Some _ -> error ~loc "external predicates cannot be indexed" end - | Index i :: rest -> + | Index(i,index_type) :: rest -> + let it = + match index_type with + | None -> None + | Some "Map" -> Some Map + | Some "Hash" -> Some HashMap + | Some "DTree" -> Some DiscriminationTree + | Some s -> error ~loc ("unknown indexing directive " ^ s) in begin match r with - | None -> aux (Some (Structured.Index i)) rest + | None -> aux (Some (Structured.Index(i,it))) rest | Some (Structured.Index _) -> duplicate_err "index" | Some _ -> error ~loc "external predicates cannot be indexed" end @@ -643,7 +650,7 @@ end = struct (* {{{ *) let attributes = aux None attributes in let attributes = match attributes with - | None -> Structured.Index [1] + | None -> Structured.Index([1],None) | Some x -> x in { Type.attributes; loc; name; ty } @@ -2388,17 +2395,22 @@ let compile_clause modes initial_depth state if morelcs <> 0 then error ~loc "sigma in a toplevel clause is not supported"; state, cl -let chose_indexing state predicate l = +let chose_indexing state predicate l k = let all_zero = List.for_all ((=) 0) in - let rec aux argno = function + let rec check_map default argno = function (* TODO: @FissoreD here we should raise an error if n > arity of the predicate? *) - | [] -> error ("Wrong indexing for " ^ Symbols.show state predicate) - | 0 :: l -> aux (argno+1) l + | [] -> error ("Wrong indexing for " ^ Symbols.show state predicate ^ ": no argument selected.") + | 0 :: l -> check_map default (argno+1) l | 1 :: l when all_zero l -> MapOn argno - | _ -> Trie l - (* TODO: @FissoreD we should add some syntax if we don't want to lose the indexing with Hash *) - (* | _ -> Hash l *) - in aux 0 l + | _ -> default () + in + match k with + | Some Ast.Structured.DiscriminationTree -> Trie l + | Some HashMap -> Hash l + | None -> check_map (fun () -> Trie l) 0 l + | Some Map -> check_map (fun () -> + error ("Wrong indexing for " ^ Symbols.show state predicate ^ + ": Map indexes exactly one argument at depth 1")) 0 l let check_rule_pattern_in_clique state clique { D.CHR.pattern; rule_name } = try @@ -2436,8 +2448,8 @@ let run let mode = try C.Map.find name modes with Not_found -> [] in let declare_index, index = match tindex with - | Some (Ast.Structured.Index l) -> true, chose_indexing state name l - | _ -> false, chose_indexing state name [1] in + | Some (Ast.Structured.Index(l,k)) -> true, chose_indexing state name l k + | _ -> false, chose_indexing state name [1] None in try let _, old_tindex = C.Map.find name map in if old_tindex <> index then diff --git a/src/parser/ast.ml b/src/parser/ast.ml index b9dc05b06..12ebe8c1f 100644 --- a/src/parser/ast.ml +++ b/src/parser/ast.ml @@ -135,7 +135,7 @@ type raw_attribute = | Before of string | Replace of string | External - | Index of int list + | Index of int list * string option [@@deriving show] module Clause = struct @@ -307,7 +307,8 @@ and cattribute = { } and tattribute = | External - | Index of int list + | Index of int list * tindex option +and tindex = Map | HashMap | DiscriminationTree and 'a shorthand = { iloc : Loc.t; full_name : 'a; diff --git a/src/parser/ast.mli b/src/parser/ast.mli index e44625ee7..39b13a4e8 100644 --- a/src/parser/ast.mli +++ b/src/parser/ast.mli @@ -72,7 +72,7 @@ type raw_attribute = | Before of string | Replace of string | External - | Index of int list + | Index of int list * string option [@@ deriving show] module Clause : sig @@ -213,7 +213,8 @@ and cattribute = { } and tattribute = | External - | Index of int list + | Index of int list * tindex option +and tindex = Map | HashMap | DiscriminationTree and 'a shorthand = { iloc : Loc.t; full_name : 'a; diff --git a/src/parser/grammar.mly b/src/parser/grammar.mly index d78ed9009..4773e8142 100644 --- a/src/parser/grammar.mly +++ b/src/parser/grammar.mly @@ -296,7 +296,7 @@ attribute: | BEFORE; s = STRING { Before s } | REPLACE; s = STRING { Replace s } | EXTERNAL { External } -| INDEX; LPAREN; l = nonempty_list(indexing) ; RPAREN { Index l } +| INDEX; LPAREN; l = nonempty_list(indexing) ; RPAREN; o = option(STRING) { Index (l,o) } indexing: | FRESHUV { 0 } diff --git a/src/parser/test_parser.ml b/src/parser/test_parser.ml index 81442c685..c22e361b6 100644 --- a/src/parser/test_parser.ml +++ b/src/parser/test_parser.ml @@ -9,9 +9,9 @@ let error s a1 a2 = let f2 = Filename.temp_file "parser_out" "txt" in let oc1 = open_out f1 in let oc2 = open_out f2 in - output_string oc1 "new:\n"; + output_string oc1 "\nnew:\n"; output_string oc1 (Program.show a1); - output_string oc2 "reference:\n"; + output_string oc2 "\nreference:\n"; output_string oc2 (Program.show a2); flush_all (); close_out oc1; @@ -43,9 +43,9 @@ let test s x y w z att b = let p = Parser.program_from ~loc lexbuf in if p <> exp then error s p exp - with Parse.ParseError(loc,message) -> - Printf.eprintf "error parsing '%s' at %s\n%s%!" s (Loc.show loc) message; - exit 1 + with Parse.ParseError(loc,message) -> + Printf.eprintf "error parsing '%s' at %s\n%s%!" s (Loc.show loc) message; + exit 1 let testR s x y w z attributes to_match to_remove guard new_goal = let exp = [Program.(Chr { Chr.to_match; to_remove; guard; new_goal; loc=(mkLoc x y w z); attributes })] in @@ -55,10 +55,25 @@ let testR s x y w z attributes to_match to_remove guard new_goal = let p = Parser.program_from ~loc lexbuf in if p <> exp then error s p exp - with Parse.ParseError(loc,message) -> + with Parse.ParseError(loc,message) -> + Printf.eprintf "error parsing '%s' at %s\n%s%!" s (Loc.show loc) message; + exit 1 + +let testT s x y w z attributes () = + let lexbuf = Lexing.from_string s in + let loc = Loc.initial "(input)" in + try + let p = Parser.program_from ~loc lexbuf in + match p with + | [Program.Pred _] -> () + | [Program.Type _] -> () + | _ -> + Printf.eprintf "error parsing '%s' at %s\n%s%!" s (Loc.show loc) "not a type declaration"; + exit 1 + with Parse.ParseError(loc,message) -> Printf.eprintf "error parsing '%s' at %s\n%s%!" s (Loc.show loc) message; exit 1 - + let testF s i msg = let lexbuf = Lexing.from_string s in let loc = Loc.initial "(input)" in @@ -136,6 +151,8 @@ let _ = testF "x. x]" 5 "unexpected keyword"; testF "x. +" 4 "unexpected start"; test ":name \"x\" x." 0 11 1 0 [Name "x"] (c"x"); + testT ":index (1) \"foobar\" pred x." 0 11 1 0 [Index ([1],Some "foobar")] (); + testT ":index (1) pred x." 0 11 1 0 [Index ([1], None)] (); testF "p :- g (f x) \\ y." 14 ".*bind.*must follow.*name.*"; testF "foo i:term, o:term. foo A B :- A = [B]." 6 "unexpected keyword"; (* 01234567890123456789012345 *) diff --git a/tests/suite/elpi_specific.ml b/tests/suite/elpi_specific.ml index 42bcc804a..a2760c832 100644 --- a/tests/suite/elpi_specific.ml +++ b/tests/suite/elpi_specific.ml @@ -437,4 +437,11 @@ let () = declare "trace-browser-elab-broken2" ~description:"fatal broken trace elaboration" ~expectation:(FailureOutput (Str.regexp "broken.*step_id 217.*json object 1857")) () - \ No newline at end of file + + +let () = declare "bad_index" + ~source_elpi:"bad_index.elpi" + ~description:"bad indexing directive" + ~expectation:Test.(FailureOutput (Str.regexp "Wrong indexing")) + () + \ No newline at end of file