ITP: support for qualified ident and infix ident

command "search" and transformations taking idents as arguments now can
support qualified idents and infix symbols.

For example, "search (+) (*)" returns the distributivity axioms

FIXME: "search Int.(+)" fails, probably missing namespaced for
imported modules

src/parser/lexer.mli

@@ -11,6 +11,10 @@
 
 val parse_term : Lexing.lexbuf -> Ptree.term
 
+val parse_qualid: Lexing.lexbuf -> Ptree.qualid
+
+val parse_list_qualid: Lexing.lexbuf -> Ptree.qualid list
+
 val parse_list_ident: Lexing.lexbuf -> Ptree.ident list
 
 val parse_program_file : Ptree.incremental -> Lexing.lexbuf -> unit

src/parser/lexer.mll

@@ -245,7 +245,11 @@ rule token = parse
 
   let parse_term lb = Loc.with_location (Parser.term_eof token) lb
 
-  let parse_list_ident lb = Loc.with_location (Parser.ident_comma_list token) lb
+  let parse_qualid lb = Loc.with_location (Parser.qualid_eof token) lb
+
+  let parse_list_ident lb = Loc.with_location (Parser.ident_comma_list_eof token) lb
+
+  let parse_list_qualid lb = Loc.with_location (Parser.qualid_comma_list_eof token) lb
 
   let parse_logic_file env path lb =
     open_file token (Lexing.from_string "") (Typing.open_file env path);

src/parser/parser.mly

@@ -220,7 +220,9 @@ end
 %start <Ptree.incremental -> unit> open_file
 %start <unit> logic_file program_file
 %start <Ptree.term> term_eof
-%start <Ptree.ident list> ident_comma_list
+%start <Ptree.qualid> qualid_eof
+%start <Ptree.qualid list> qualid_comma_list_eof
+%start <Ptree.ident list> ident_comma_list_eof
 %%
 
 (* parsing of a single term *)
@@ -1063,10 +1065,6 @@ sident:
 | ident   { $1 }
 | STRING  { mk_id $1 $startpos $endpos }
 
-(* Parsing of a list *)
-ident_comma_list:
-| comma_list1(ident) EOF { $1 }
-
 (* Labels and position markers *)
 
 labels(X): X label* { add_lab $1 $2 }
@@ -1097,3 +1095,14 @@ semicolon_list1(X):
 | x = X ; SEMICOLON ; xl = semicolon_list1(X) { x :: xl }
 
 located(X): X { $1, $startpos, $endpos }
+
+
+(* Parsing of a list of qualified identifiers for the ITP *)
+qualid_eof:
+| qualid EOF { $1 }
+
+qualid_comma_list_eof:
+| comma_list1(qualid) EOF { $1 }
+
+ident_comma_list_eof:
+| comma_list1(ident) EOF { $1 }

src/session/itp_server.ml

@@ -233,8 +233,10 @@ let get_exception_message ses id e =
         (print_term ses id) t1 (print_term ses id) t2, Loc.dummy_position, ""
   | Generic_arg_trans_utils.Arg_trans (s) ->
       Pp.sprintf "Error in transformation function: %s \n" s, Loc.dummy_position, ""
-  | Args_wrapper.Arg_hyp_not_found (s) ->
-      Pp.sprintf "Following hypothesis was not found: %s \n" s, Loc.dummy_position, ""
+  | Args_wrapper.Arg_qid_not_found q ->
+      Pp.sprintf "Following hypothesis was not found: %a \n" Typing.print_qualid q, Loc.dummy_position, ""
+  | Args_wrapper.Arg_error s ->
+      Pp.sprintf "Transformation raised a general error: %s \n" s, Loc.dummy_position, ""
   | Args_wrapper.Arg_theory_not_found (s) ->
       Pp.sprintf "Theory not found: %s" s, Loc.dummy_position, ""
   | Args_wrapper.Arg_parse_type_error(loc, arg, e) ->

src/session/server_utils.ml

@@ -126,10 +126,11 @@ let list_provers cont _args =
   Pp.sprintf "%a" (Pp.print_list Pp.newline Pp.string) l
 
 
-let find_any_id nt s =
-  try (Stdlib.Mstr.find s nt.Theory.ns_pr).Decl.pr_name with
-  | Not_found -> try (Stdlib.Mstr.find s nt.Theory.ns_ls).Term.ls_name with
-    | Not_found -> (Stdlib.Mstr.find s nt.Theory.ns_ts).Ty.ts_name
+let symbol_name s =
+  match s with
+  | Args_wrapper.Tstysymbol ts -> ts.Ty.ts_name
+  | Args_wrapper.Tsprsymbol pr -> pr.Decl.pr_name
+  | Args_wrapper.Tslsymbol ls -> ls.Term.ls_name
 
 (* The id you are trying to use is undefined *)
 exception Undefined_id of string
@@ -139,10 +140,10 @@ exception Number_of_arguments
 let print_id s tables =
   (* let tables = Args_wrapper.build_name_tables task in*)
   let km = tables.Trans.known_map in
-  let id = try find_any_id tables.Trans.namespace s with
+  let id = try Args_wrapper.find_symbol s tables with
   | Not_found -> raise (Undefined_id s) in
   let d =
-    try Ident.Mid.find id km with
+    try Ident.Mid.find (symbol_name id) km with
     | Not_found -> raise Not_found (* Should not happen *)
   in
   Pp.string_of (Why3printer.print_decl tables) d
@@ -188,8 +189,9 @@ let do_search km idl =
 
 let search s tables =
   let ids = List.rev_map
-              (fun s -> try find_any_id tables.Trans.namespace s
-                        with Not_found -> raise (Undefined_id s)) s
+              (fun s -> try symbol_name (Args_wrapper.find_symbol s tables)
+                        with Args_wrapper.Arg_parse_type_error _ |
+                             Args_wrapper.Arg_qid_not_found _ -> raise (Undefined_id s)) s
   in
   let l = do_search tables.Trans.known_map ids in
   if Decl.Sdecl.is_empty l then

src/transform/apply.ml

@@ -60,7 +60,7 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
   let g, task = Task.task_separate_goal task in
   let g = term_decl g in
   let d = find_hypothesis name task in
-  if d = None then raise (Arg_hyp_not_found "apply");
+  if d = None then raise (Arg_error "apply");
   let d = Opt.get d in
   let t = term_decl d in
   let (lp, lv, nt) = intros t in
@@ -160,7 +160,7 @@ let rewrite_in rev h h1 =
   (* Return instantiated premises and the hypothesis correctly rewritten *)
   let lp_new found_eq =
     match found_eq with
-    | None -> raise (Arg_hyp_not_found "rewrite")
+    | None -> raise (Arg_error "rewrite")
     | Some (lp, lv, t1, t2) ->
       fold (fun d acc ->
         match d.d_node with

src/transform/args_wrapper.ml

@@ -21,7 +21,8 @@ exception Arg_parse_error of string * string
 exception Arg_expected of string * string
 exception Arg_theory_not_found of string
 exception Arg_expected_none of string
-exception Arg_hyp_not_found of string
+exception Arg_qid_not_found of Ptree.qualid
+exception Arg_error of string
 
 let () = Exn_printer.register
     (fun fmt e ->
@@ -187,22 +188,22 @@ type (_, _) trans_typ =
   | Topt        : string * ('a -> 'c, 'b) trans_typ -> (('a option -> 'c), 'b) trans_typ
   | Toptbool    : string * ('a, 'b) trans_typ -> (bool -> 'a, 'b) trans_typ
 
-let find_pr s tables =
-  Mstr.find s tables.namespace.ns_pr
+let find_pr q tables =
+  Theory.ns_find_pr tables.namespace (Typing.string_list_of_qualid q)
 
-let find_ts s tables =
-  Mstr.find s tables.namespace.ns_ts
+let find_ts q tables =
+  Theory.ns_find_ts tables.namespace (Typing.string_list_of_qualid q)
 
-let find_ls s tables =
-  Mstr.find s tables.namespace.ns_ls
+let find_ls q tables =
+  Theory.ns_find_ls tables.namespace (Typing.string_list_of_qualid q)
 
-let find_symbol s tables =
-  try Tsprsymbol (find_pr s tables) with
+let find_symbol q tables =
+  try Tsprsymbol (find_pr q tables) with
         | Not_found ->
-          try Tslsymbol (find_ls s tables) with
+          try Tslsymbol (find_ls q tables) with
           | Not_found ->
-            try Tstysymbol (find_ts s tables) with
-            | Not_found -> raise (Arg_hyp_not_found s)
+            try Tstysymbol (find_ts q tables) with
+            | Not_found -> raise (Arg_qid_not_found q)
 
 
 let type_ptree ~as_fmla t tables =
@@ -227,9 +228,26 @@ let parse_and_type ~as_fmla s task =
   with
   | Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))
 
+let parse_qualid s =
+  try
+    let lb = Lexing.from_string s in
+    Lexer.parse_qualid lb
+  with
+  | Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))
+
+let parse_list_qualid s =
+  try
+    let lb = Lexing.from_string s in
+    Lexer.parse_list_qualid lb
+  with
+  | Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))
+
 let parse_list_ident s =
-  let lb = Lexing.from_string s in
-  Lexer.parse_list_ident lb
+  try
+    let lb = Lexing.from_string s in
+    Lexer.parse_list_ident lb
+  with
+  | Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))
 
 let parse_int s =
   try int_of_string s
@@ -363,65 +381,70 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
       let tys = Ty.ts_int in (* TODO: parsing + typing of s *)
       wrap_to_store t' (f tys) tail env tables task
     | Tprsymbol t', s :: tail ->
-      let pr = try (find_pr s tables) with
-               | Not_found -> raise (Arg_hyp_not_found s) in
+       let q = parse_qualid s in
+       let pr = try (find_pr q tables) with
+                | Not_found -> raise (Arg_qid_not_found q) in
       wrap_to_store t' (f pr) tail env tables task
     | Tprlist t', s :: tail ->
-        let pr_list = parse_list_ident s in
+        let pr_list = parse_list_qualid s in
         let pr_list =
         List.map (fun id ->
-                    try find_pr id.Ptree.id_str tables with
-                    | Not_found -> raise (Arg_hyp_not_found s))
+                    try find_pr id tables with
+                    | Not_found -> raise (Arg_qid_not_found id))
                  pr_list in
         wrap_to_store t' (f pr_list) tail env tables task
     | Tlsymbol t', s :: tail ->
-      let pr = try (find_ls s tables) with
-               | Not_found -> raise (Arg_hyp_not_found s) in
+       let q = parse_qualid s in
+       let pr = try (find_ls q tables) with
+               | Not_found -> raise (Arg_qid_not_found q) in
       wrap_to_store t' (f pr) tail env tables task
     | Tsymbol t', s :: tail ->
-      let symbol = find_symbol s tables in
-      wrap_to_store t' (f symbol) tail env tables task
+       let q = parse_qualid s in
+       let symbol = find_symbol q tables in
+       wrap_to_store t' (f symbol) tail env tables task
     | Tlist t', s :: tail ->
-      let pr_list = parse_list_ident s in
-      let pr_list =
-        List.map (fun id -> find_symbol id.Ptree.id_str tables) pr_list in
-      wrap_to_store t' (f pr_list) tail env tables task
+       let pr_list = parse_list_qualid s in
+       let pr_list =
+         List.map (fun id -> find_symbol id tables) pr_list in
+       wrap_to_store t' (f pr_list) tail env tables task
     | Ttheory t', s :: tail ->
-      let th = parse_theory env s in
-      wrap_to_store t' (f th) tail env tables task
+       let th = parse_theory env s in
+       wrap_to_store t' (f th) tail env tables task
     | Tstring t', s :: tail ->
-      wrap_to_store t' (f s) tail env tables task
+       wrap_to_store t' (f s) tail env tables task
     | Tstringlist t', s :: tail ->
-      let list = List.map (fun id -> id.Ptree.id_str) (parse_list_ident s) in
-      wrap_to_store t' (f list) tail env tables task
+       let list = List.map (fun id -> id.Ptree.id_str) (parse_list_ident s) in
+       wrap_to_store t' (f list) tail env tables task
     | Topt (optname, t'), s :: s' :: tail when s = optname ->
-      begin match t' with
+       begin match t' with
         | Tint t' ->
           let arg = Some (parse_int s') in
           wrap_to_store t' (f arg) tail env tables task
         | Tprsymbol t' ->
-          let arg = try Some (find_pr s' tables) with
-                    | Not_found -> raise (Arg_hyp_not_found s') in
+           let q = parse_qualid s' in
+           let arg = try Some (find_pr q tables) with
+                    | Not_found -> raise (Arg_qid_not_found q) in
           wrap_to_store t' (f arg) tail env tables task
         | Tsymbol t' ->
-          let arg = Some (find_symbol s' tables) in
-          wrap_to_store t' (f arg) tail env tables task
+           let q = parse_qualid s' in
+           let arg = Some (find_symbol q tables) in
+           wrap_to_store t' (f arg) tail env tables task
         | Tformula t' ->
-          let arg = Some (parse_and_type ~as_fmla:true s' tables) in
-          wrap_to_store t' (f arg) tail env tables task
+           let arg = Some (parse_and_type ~as_fmla:true s' tables) in
+           wrap_to_store t' (f arg) tail env tables task
         | Tterm t' ->
-          let arg = Some (parse_and_type ~as_fmla:false s' tables) in
-          wrap_to_store t' (f arg) tail env tables task
+           let arg = Some (parse_and_type ~as_fmla:false s' tables) in
+           wrap_to_store t' (f arg) tail env tables task
         | Ttheory t' ->
-          let arg = Some (parse_theory env s') in
-          wrap_to_store t' (f arg) tail env tables task
+           let arg = Some (parse_theory env s') in
+           wrap_to_store t' (f arg) tail env tables task
         | Tstring t' ->
-          let arg = Some s' in
-          wrap_to_store t' (f arg) tail env tables task
+           let arg = Some s' in
+           wrap_to_store t' (f arg) tail env tables task
         | _ -> raise (Arg_expected (string_of_trans_typ t', s'))
-      end
+       end
     | Topt (_, t'), _ ->
-      wrap_to_store (trans_typ_tail t') (f None) l env tables task
+       wrap_to_store (trans_typ_tail t') (f None) l env tables task
     | Toptbool (optname, t'), s :: tail when s = optname ->
       wrap_to_store t' (f true) tail env tables task
     | Toptbool (_, t'), _ ->
@@ -447,3 +470,6 @@ let wrap_and_register : type a b. desc:Pp.formatted -> string -> (a, b) trans_ty
       Trans.register_transform_with_args_l ~desc:(type_desc ^^ desc) name trans
     | No ->
       Trans.register_transform_with_args ~desc:(type_desc ^^ desc) name trans
+
+
+let find_symbol s tables = find_symbol (parse_qualid s) tables

src/transform/args_wrapper.mli

@@ -5,7 +5,8 @@ exception Arg_parse_error of string * string
 exception Arg_expected of string * string
 exception Arg_theory_not_found of string
 exception Arg_expected_none of string
-exception Arg_hyp_not_found of string
+exception Arg_qid_not_found of Ptree.qualid
+exception Arg_error of string
 
 
 (** Pre-processing of tasks, to build unique names for all declared
@@ -18,6 +19,8 @@ type symbol =
   | Tsprsymbol of Decl.prsymbol
   | Tslsymbol of Term.lsymbol
 
+val find_symbol : string -> Trans.naming_table -> symbol
+
 type (_, _) trans_typ =
   | Ttrans      : ((task Trans.trans), task) trans_typ
   | Ttrans_l    : ((task Trans.tlist), task list) trans_typ

tests/demo-itp.mlw

@@ -22,6 +22,15 @@ module TestTaskPrinting
 
 end
 
+
+module TestInfixSymbols
+
+function (+) int int : int
+
+goal g : false
+
+end
+
 module TestAutoFocus
 
   use import int.Int