From fa9df2efe5666789bf91bb7761567cd53e6c451f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 18 Dec 2016 18:14:58 +0100 Subject: [stm] Break stm/toplevel dependency loop. Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore. --- vernac/search.ml | 381 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 381 insertions(+) create mode 100644 vernac/search.ml (limited to 'vernac/search.ml') diff --git a/vernac/search.ml b/vernac/search.ml new file mode 100644 index 000000000..e1b56b131 --- /dev/null +++ b/vernac/search.ml @@ -0,0 +1,381 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* env -> constr -> bool +type display_function = global_reference -> env -> constr -> unit + +(* This option restricts the output of [SearchPattern ...], +[SearchAbout ...], etc. to the names of the symbols matching the +query, separated by a newline. This type of output is useful for +editors (like emacs), to generate a list of completion candidates +without having to parse thorugh the types of all symbols. *) + +type glob_search_about_item = + | GlobSearchSubPattern of constr_pattern + | GlobSearchString of string + +module SearchBlacklist = + Goptions.MakeStringTable + (struct + let key = ["Search";"Blacklist"] + let title = "Current search blacklist : " + let member_message s b = + str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s + let synchronous = true + end) + +(* The functions iter_constructors and iter_declarations implement the behavior + needed for the Coq searching commands. + These functions take as first argument the procedure + that will be called to treat each entry. This procedure receives the name + of the object, the assumptions that will make it possible to print its type, + and the constr term that represent its type. *) + +let iter_constructors indsp u fn env nconstr = + for i = 1 to nconstr do + let typ = Inductiveops.type_of_constructor env ((indsp, i), u) in + fn (ConstructRef (indsp, i)) env typ + done + +let iter_named_context_name_type f = + List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl)) + +(* General search over hypothesis of a goal *) +let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = + let env = Global.env () in + let iter_hyp idh typ = fn (VarRef idh) env typ in + let evmap,e = Pfedit.get_goal_context glnum in + let pfctxt = named_context e in + iter_named_context_name_type iter_hyp pfctxt + +(* General search over declarations *) +let iter_declarations (fn : global_reference -> env -> constr -> unit) = + let env = Global.env () in + let iter_obj (sp, kn) lobj = match object_tag lobj with + | "VARIABLE" -> + begin try + let decl = Global.lookup_named (basename sp) in + fn (VarRef (NamedDecl.get_id decl)) env (NamedDecl.get_type decl) + with Not_found -> (* we are in a section *) () end + | "CONSTANT" -> + let cst = Global.constant_of_delta_kn kn in + let gr = ConstRef cst in + let typ = Global.type_of_global_unsafe gr in + fn gr env typ + | "INDUCTIVE" -> + let mind = Global.mind_of_delta_kn kn in + let mib = Global.lookup_mind mind in + let iter_packet i mip = + let ind = (mind, i) in + let u = Declareops.inductive_instance mib in + let i = (ind, u) in + let typ = Inductiveops.type_of_inductive env i in + let () = fn (IndRef ind) env typ in + let len = Array.length mip.mind_user_lc in + iter_constructors ind u fn env len + in + Array.iteri iter_packet mib.mind_packets + | _ -> () + in + try Declaremods.iter_all_segments iter_obj + with Not_found -> () + +let generic_search glnumopt fn = + (match glnumopt with + | None -> () + | Some glnum -> iter_hypothesis glnum fn); + iter_declarations fn + +(** This module defines a preference on constrs in the form of a + [compare] function (preferred constr must be big for this + functions, so preferences such as small constr must use a reversed + order). This priority will be used to order search results and + propose first results which are more likely to be relevant to the + query, this is why the type [t] contains the other elements + required of a search. *) +module ConstrPriority = struct + + (* The priority is memoised here. Because of the very localised use + of this module, it is not worth it making a convenient interface. *) + type t = + Globnames.global_reference * Environ.env * Constr.t * priority + and priority = int + + module ConstrSet = CSet.Make(Constr) + + (** A measure of the size of a term *) + let rec size t = + Constr.fold (fun s t -> 1 + s + size t) 0 t + + (** Set of the "symbols" (definitions, inductives, constructors) + which appear in a term. *) + let rec symbols acc t = + let open Constr in + match kind t with + | Const _ | Ind _ | Construct _ -> ConstrSet.add t acc + | _ -> Constr.fold symbols acc t + + (** The number of distinct "symbols" (see {!symbols}) which appear + in a term. *) + let num_symbols t = + ConstrSet.(cardinal (symbols empty t)) + + let priority t : priority = + -(3*(num_symbols t) + size t) + + let compare (_,_,_,p1) (_,_,_,p2) = + compare p1 p2 +end + +module PriorityQueue = Heap.Functional(ConstrPriority) + +let rec iter_priority_queue q fn = + (* use an option to make the function tail recursive. Will be + obsoleted with Ocaml 4.02 with the [match … with | exception …] + syntax. *) + let next = begin + try Some (PriorityQueue.maximum q) + with Heap.EmptyHeap -> None + end in + match next with + | Some (gref,env,t,_) -> + fn gref env t; + iter_priority_queue (PriorityQueue.remove q) fn + | None -> () + +let prioritize_search seq fn = + let acc = ref PriorityQueue.empty in + let iter gref env t = + let p = ConstrPriority.priority t in + acc := PriorityQueue.add (gref,env,t,p) !acc + in + let () = seq iter in + iter_priority_queue !acc fn + +(** Filters *) + +(** This function tries to see whether the conclusion matches a pattern. *) +(** FIXME: this is quite dummy, we may find a more efficient algorithm. *) +let rec pattern_filter pat ref env typ = + let typ = Termops.strip_outer_cast typ in + if Constr_matching.is_matching env Evd.empty pat typ then true + else match kind_of_term typ with + | Prod (_, _, typ) + | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ + | _ -> false + +let rec head_filter pat ref env typ = + let typ = Termops.strip_outer_cast typ in + if Constr_matching.is_matching_head env Evd.empty pat typ then true + else match kind_of_term typ with + | Prod (_, _, typ) + | LetIn (_, _, _, typ) -> head_filter pat ref env typ + | _ -> false + +let full_name_of_reference ref = + let (dir,id) = repr_path (path_of_global ref) in + DirPath.to_string dir ^ "." ^ Id.to_string id + +(** Whether a reference is blacklisted *) +let blacklist_filter_aux () = + let l = SearchBlacklist.elements () in + fun ref env typ -> + let name = full_name_of_reference ref in + let is_not_bl str = not (String.string_contains ~where:name ~what:str) in + List.for_all is_not_bl l + +let module_filter (mods, outside) ref env typ = + let sp = path_of_global ref in + let sl = dirpath sp in + let is_outside md = not (is_dirpath_prefix_of md sl) in + let is_inside md = is_dirpath_prefix_of md sl in + if outside then List.for_all is_outside mods + else List.is_empty mods || List.exists is_inside mods + +let name_of_reference ref = Id.to_string (basename_of_global ref) + +let search_about_filter query gr env typ = match query with +| GlobSearchSubPattern pat -> + Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat typ +| GlobSearchString s -> + String.string_contains ~where:(name_of_reference gr) ~what:s + + +(** SearchPattern *) + +let search_pattern gopt pat mods pr_search = + let blacklist_filter = blacklist_filter_aux () in + let filter ref env typ = + module_filter mods ref env typ && + pattern_filter pat ref env typ && + blacklist_filter ref env typ + in + let iter ref env typ = + if filter ref env typ then pr_search ref env typ + in + generic_search gopt iter + +(** SearchRewrite *) + +let eq = Coqlib.glob_eq + +let rewrite_pat1 pat = + PApp (PRef eq, [| PMeta None; pat; PMeta None |]) + +let rewrite_pat2 pat = + PApp (PRef eq, [| PMeta None; PMeta None; pat |]) + +let search_rewrite gopt pat mods pr_search = + let pat1 = rewrite_pat1 pat in + let pat2 = rewrite_pat2 pat in + let blacklist_filter = blacklist_filter_aux () in + let filter ref env typ = + module_filter mods ref env typ && + (pattern_filter pat1 ref env typ || + pattern_filter pat2 ref env typ) && + blacklist_filter ref env typ + in + let iter ref env typ = + if filter ref env typ then pr_search ref env typ + in + generic_search gopt iter + +(** Search *) + +let search_by_head gopt pat mods pr_search = + let blacklist_filter = blacklist_filter_aux () in + let filter ref env typ = + module_filter mods ref env typ && + head_filter pat ref env typ && + blacklist_filter ref env typ + in + let iter ref env typ = + if filter ref env typ then pr_search ref env typ + in + generic_search gopt iter + +(** SearchAbout *) + +let search_about gopt items mods pr_search = + let blacklist_filter = blacklist_filter_aux () in + let filter ref env typ = + let eqb b1 b2 = if b1 then b2 else not b2 in + module_filter mods ref env typ && + List.for_all + (fun (b,i) -> eqb b (search_about_filter i ref env typ)) items && + blacklist_filter ref env typ + in + let iter ref env typ = + if filter ref env typ then pr_search ref env typ + in + generic_search gopt iter + +type search_constraint = + | Name_Pattern of Str.regexp + | Type_Pattern of Pattern.constr_pattern + | SubType_Pattern of Pattern.constr_pattern + | In_Module of Names.DirPath.t + | Include_Blacklist + +type 'a coq_object = { + coq_object_prefix : string list; + coq_object_qualid : string list; + coq_object_object : 'a; +} + +let interface_search = + let rec extract_flags name tpe subtpe mods blacklist = function + | [] -> (name, tpe, subtpe, mods, blacklist) + | (Name_Pattern regexp, b) :: l -> + extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l + | (Type_Pattern pat, b) :: l -> + extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l + | (SubType_Pattern pat, b) :: l -> + extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l + | (In_Module id, b) :: l -> + extract_flags name tpe subtpe ((id, b) :: mods) blacklist l + | (Include_Blacklist, b) :: l -> + extract_flags name tpe subtpe mods b l + in + fun ?glnum flags -> + let (name, tpe, subtpe, mods, blacklist) = + extract_flags [] [] [] [] false flags + in + let blacklist_filter = blacklist_filter_aux () in + let filter_function ref env constr = + let id = Names.Id.to_string (Nametab.basename_of_global ref) in + let path = Libnames.dirpath (Nametab.path_of_global ref) in + let toggle x b = if x then b else not b in + let match_name (regexp, flag) = + toggle (Str.string_match regexp id 0) flag + in + let match_type (pat, flag) = + toggle (Constr_matching.is_matching env Evd.empty pat constr) flag + in + let match_subtype (pat, flag) = + toggle + (Constr_matching.is_matching_appsubterm ~closed:false + env Evd.empty pat constr) flag + in + let match_module (mdl, flag) = + toggle (Libnames.is_dirpath_prefix_of mdl path) flag + in + List.for_all match_name name && + List.for_all match_type tpe && + List.for_all match_subtype subtpe && + List.for_all match_module mods && + (blacklist || blacklist_filter ref env constr) + in + let ans = ref [] in + let print_function ref env constr = + let fullpath = DirPath.repr (Nametab.dirpath_of_global ref) in + let qualid = Nametab.shortest_qualid_of_global Id.Set.empty ref in + let (shortpath, basename) = Libnames.repr_qualid qualid in + let shortpath = DirPath.repr shortpath in + (* [shortpath] is a suffix of [fullpath] and we're looking for the missing + prefix *) + let rec prefix full short accu = match full, short with + | _, [] -> + let full = List.rev_map Id.to_string full in + (full, accu) + | _ :: full, m :: short -> + prefix full short (Id.to_string m :: accu) + | _ -> assert false + in + let (prefix, qualid) = prefix fullpath shortpath [Id.to_string basename] in + let answer = { + coq_object_prefix = prefix; + coq_object_qualid = qualid; + coq_object_object = string_of_ppcmds (pr_lconstr_env env Evd.empty constr); + } in + ans := answer :: !ans; + in + let iter ref env typ = + if filter_function ref env typ then print_function ref env typ + in + let () = generic_search glnum iter in + !ans + +let blacklist_filter ref env typ = + blacklist_filter_aux () ref env typ -- cgit v1.2.3 From 921ea3983d45051ae85b0e20bf13de2eff38e53e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 8 Feb 2017 18:13:25 +0100 Subject: [pp] Remove uses of expensive string_of_ppcmds. In general we want to avoid this as much as we can, as it will need to make choices regarding the output backend (width, etc...) and it is expensive. It is better to serve the printing backends the pretty print document itself. --- checker/reduction.ml | 6 +++--- engine/universes.ml | 7 +++---- ide/ide_slave.ml | 2 +- stm/stm.ml | 20 +++++++++++--------- tools/fake_ide.ml | 4 +++- vernac/search.ml | 2 +- vernac/search.mli | 2 +- vernac/vernacentries.ml | 7 ++++--- 8 files changed, 27 insertions(+), 23 deletions(-) (limited to 'vernac/search.ml') diff --git a/checker/reduction.ml b/checker/reduction.ml index ec16aa261..28c0126b4 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -176,9 +176,9 @@ let sort_cmp env univ pb s0 s1 = then begin if !Flags.debug then begin let op = match pb with CONV -> "=" | CUMUL -> "<=" in - Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds - (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() - ++ Univ.pr_universes univ)) + Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.( + str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() + ++ Univ.pr_universes univ) end; raise NotConvertible end diff --git a/engine/universes.ml b/engine/universes.ml index 6720fcef8..30a9ef163 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -416,10 +416,9 @@ let constr_of_global gr = (* Should be an error as we might forget constraints, allow for now to make firstorder work with "using" clauses *) c - else raise (Invalid_argument - ("constr_of_global: globalization of polymorphic reference " ^ - Pp.string_of_ppcmds (Nametab.pr_global_env Id.Set.empty gr) ^ - " would forget universes.")) + else CErrors.user_err ~hdr:"constr_of_global" + Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ + str " would forget universes.") else c let constr_of_reference = constr_of_global diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index e3e1a8890..2065a4546 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -255,7 +255,7 @@ let status force = let export_coq_object t = { Interface.coq_object_prefix = t.Search.coq_object_prefix; Interface.coq_object_qualid = t.Search.coq_object_qualid; - Interface.coq_object_object = t.Search.coq_object_object + Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object) } let pattern_of_string ?env s = diff --git a/stm/stm.ml b/stm/stm.ml index ee142b293..b9dbb7891 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -6,11 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr +let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n" (System.process_id ()) Pp.pp_with pp; flush stderr let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else () let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () +let stm_pperr_endline s = if false then begin stm_pp_err (s ()) end else () + open Vernacexpr open CErrors open Pp @@ -994,11 +997,11 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = in let aux_interp cmd = if is_filtered_command cmd then - stm_prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) + stm_pperr_endline Pp.(fun () -> str "ignoring " ++ pr_vernac expr) else match cmd with | VernacShow ShowScript -> ShowScript.show_script () | expr -> - stm_prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); + stm_pperr_endline Pp.(fun () -> str "interpreting " ++ pr_vernac expr); try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) with e -> let e = CErrors.push e in @@ -1431,11 +1434,10 @@ end = struct (* {{{ *) | Some (safe, err) -> err, safe | None -> Stateid.dummy, Stateid.dummy in let e_msg = iprint (e, info) in - stm_prerr_endline (fun () -> "failed with the following exception:"); - stm_prerr_endline (fun () -> string_of_ppcmds e_msg); + stm_pperr_endline Pp.(fun () -> str "failed with the following exception: " ++ fnl () ++ e_msg); let e_safe_states = List.filter State.is_cached_and_valid my_states in RespError { e_error_at; e_safe_id; e_msg; e_safe_states } - + let perform_states query = if query = [] then [] else let is_tac e = match classify_vernac e with @@ -1880,10 +1882,10 @@ end = struct (* {{{ *) let open Notations in try let pt, uc = Future.join f in - stm_prerr_endline (fun () -> string_of_ppcmds(hov 0 ( + stm_pperr_endline (fun () -> hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ - str"uc=" ++ Evd.pr_evar_universe_context uc))); + str"uc=" ++ Evd.pr_evar_universe_context uc)); (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> Tactics.exact_no_check pt) @@ -2514,7 +2516,7 @@ let reset_task_queue = Slaves.reset_task_queue (* Document building *) let process_transaction ?(newtip=Stateid.fresh ()) ~tty ({ verbose; loc; expr } as x) c = - stm_prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x)); + stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in try let head = VCS.current_branch () in diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 5dd2a9220..7a891239b 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -12,6 +12,8 @@ let error s = prerr_endline ("fake_id: error: "^s); exit 1 +let pperr_endline pp = Format.eprintf "@[%a@]\n%!" Pp.pp_with pp + type coqtop = { xml_printer : Xml_printer.t; xml_parser : Xml_parser.t; @@ -170,7 +172,7 @@ let print_document () = Str.global_replace (Str.regexp "^[\n ]*") "" (if String.length s > 20 then String.sub s 0 17 ^ "..." else s) in - prerr_endline (Pp.string_of_ppcmds + pperr_endline ( (Document.print doc (fun b state_id { name; text } -> Pp.str (Printf.sprintf "%s[%10s, %3s] %s" diff --git a/vernac/search.ml b/vernac/search.ml index e1b56b131..540573843 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -367,7 +367,7 @@ let interface_search = let answer = { coq_object_prefix = prefix; coq_object_qualid = qualid; - coq_object_object = string_of_ppcmds (pr_lconstr_env env Evd.empty constr); + coq_object_object = constr; } in ans := answer :: !ans; in diff --git a/vernac/search.mli b/vernac/search.mli index c9167c485..82b79f75d 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -67,7 +67,7 @@ type 'a coq_object = { } val interface_search : ?glnum:int -> (search_constraint * bool) list -> - string coq_object list + constr coq_object list (** {6 Generic search function} *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 999fe297e..32e18a014 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -39,8 +39,9 @@ module NamedDecl = Context.Named.Declaration let (f_interp_redexp, interp_redexp_hook) = Hook.make () let debug = false -let vernac_prerr_endline x = - if debug then prerr_endline (x ()) else () +(* XXX Should move to a common library *) +let vernac_pperr_endline pp = + if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else () (* Misc *) @@ -1933,7 +1934,7 @@ let vernac_load interp fname = * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) let interp ?proof ~loc locality poly c = - vernac_prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); + vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c); match c with (* The below vernac are candidates for removal from the main type and to be put into a new doc_command datatype: *) -- cgit v1.2.3