:index takes an index type

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

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;

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;

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 }

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 *)

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"))
   ()
-
+
+
+let () = declare "bad_index"
+  ~source_elpi:"bad_index.elpi"
+  ~description:"bad indexing directive"
+  ~expectation:Test.(FailureOutput (Str.regexp "Wrong indexing"))
+  ()
+