From c789e243ff599db876e94a5ab2a13ff98baa0d6c Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 24 Sep 2010 13:14:17 +0000 Subject: Some dead code removal, thanks to Oug analyzer In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_constr.ml4 | 12 ----------- parsing/g_tactic.ml4 | 18 ----------------- parsing/lexer.ml4 | 2 -- parsing/pcoq.ml4 | 8 -------- parsing/pcoq.mli | 5 ----- parsing/ppconstr.ml | 57 ---------------------------------------------------- parsing/pptactic.ml | 50 --------------------------------------------- parsing/ppvernac.ml | 38 ----------------------------------- parsing/prettyp.ml | 27 ------------------------- parsing/prettyp.mli | 1 - parsing/printer.ml | 19 ------------------ 11 files changed, 237 deletions(-) (limited to 'parsing') diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 8931d67f3..12cffc492 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -107,18 +107,6 @@ let ident_colon = | _ -> err ()) | _ -> err ()) -let ident_with = - Gram.Entry.of_parser "ident_with" - (fun strm -> - match get_tok (stream_nth 0 strm) with - | IDENT s -> - (match get_tok (stream_nth 1 strm) with - | KEYWORD "with" -> - stream_njunk 2 strm; - Names.id_of_string s - | _ -> err ()) - | _ -> err ()) - let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None GEXTEND Gram diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index f9e146730..9b476d996 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -93,24 +93,6 @@ let check_for_coloneq = | KEYWORD "(" -> skip_binders 2 | _ -> err ()) -let guess_lpar_ipat s strm = - match get_tok (stream_nth 0 strm) with - | KEYWORD "(" -> - (match get_tok (stream_nth 1 strm) with - | KEYWORD ("("|"[") -> () - | IDENT _ -> - (match get_tok (stream_nth 2 strm) with - | KEYWORD s' when s = s' -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err () - -let guess_lpar_coloneq = - Gram.Entry.of_parser "guess_lpar_coloneq" (guess_lpar_ipat ":=") - -let guess_lpar_colon = - Gram.Entry.of_parser "guess_lpar_colon" (guess_lpar_ipat ":") - let lookup_at_as_coma = Gram.Entry.of_parser "lookup_at_as_coma" (fun strm -> diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index d1168ad19..15cdc6077 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -250,8 +250,6 @@ let rec number len = parser | [< ' ('0'..'9' as c); s >] -> number (store len c) s | [< >] -> len -let escape len c = store len c - let rec string in_comments bp len = parser | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] -> if esc then string in_comments bp (store len '"') s else len diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 95948d2ac..034c46e58 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -264,13 +264,6 @@ let get_univ s = let get_entry (u, utab) s = Hashtbl.find utab s -let get_entry_type (u, utab) s = - try - type_of_typed_entry (get_entry (u, utab) s) - with Not_found -> - errorlabstrm "Pcoq.get_entry" - (str "Unknown grammar entry " ++ str u ++ str ":" ++ str s ++ str ".") - let new_entry etyp (u, utab) s = if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr); let ename = u ^ ":" ^ s in @@ -340,7 +333,6 @@ module Prim = module Constr = struct let gec_constr = make_gen_entry uconstr rawwit_constr - let gec_constr_list = make_gen_entry uconstr (wit_list0 rawwit_constr) (* Entries that can be refered via the string -> Gram.entry table *) let constr = gec_constr "constr" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index c7edd9b92..7db89a5ff 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -147,11 +147,6 @@ val uconstr : gram_universe val utactic : gram_universe val uvernac : gram_universe -(* -val get_entry : gram_universe -> string -> typed_entry -val get_entry_type : gram_universe -> string -> entry_type -*) - val create_entry : gram_universe -> string -> entry_type -> typed_entry val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> 'a Gram.entry diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 6276a23c3..9bfa32285 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -22,14 +22,10 @@ open Constrextern open Termops (*i*) -let sep_p = fun _ -> str"." let sep_v = fun _ -> str"," ++ spc() -let sep_pp = fun _ -> str":" -let sep_bar = fun _ -> spc() ++ str"| " let pr_tight_coma () = str "," ++ cut () let latom = 0 -let lannot = 100 let lprod = 200 let llambda = 200 let lif = 200 @@ -108,10 +104,6 @@ let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) -let pr_optc pr = function - | None -> mt () - | Some x -> pr_sep_com spc pr x - let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" let pr_universe = Univ.pr_uni @@ -355,21 +347,6 @@ let pr_recursive pr_decl id = function (pr_decl true) dl ++ fnl() ++ str "for " ++ pr_id id -let is_var id = function - | CRef (Ident (_,id')) when id=id' -> true - | _ -> false - -let tm_clash = function - | (CRef (Ident (_,id)), Some (CApp (_,_,nal))) - when List.exists (function CRef (Ident (_,id')),_ -> id=id' | _ -> false) - nal - -> Some id - | (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal))) - when List.exists (function CRef (Ident (_,id')) -> id=id' | _ -> false) - nal - -> Some id - | _ -> None - let pr_asin pr (na,indnalopt) = (match na with (* Decision of printing "_" or not moved to constrextern.ml *) | Some na -> spc () ++ str "as " ++ pr_lname na @@ -387,8 +364,6 @@ let pr_case_type pr po = | Some p -> spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimple) p) -let pr_return_type pr po = pr_case_type pr po - let pr_simple_return_type pr na po = (match na with | Some (_,Name id) -> @@ -561,38 +536,6 @@ let pr pr sep inherited a = pr_with_comments loc (sep() ++ if prec_less prec inherited then strm else surround strm) - -let rec strip_context n iscast t = - if n = 0 then - [], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t - else match t with - | CLambdaN (loc,(nal,bk,t)::bll,c) -> - let n' = List.length nal in - if n' > n then - let nal1,nal2 = list_chop n nal in - [LocalRawAssum (nal1,bk,t)], CLambdaN (loc,(nal2,bk,t)::bll,c) - else - let bl', c = strip_context (n-n') iscast - (if bll=[] then c else CLambdaN (loc,bll,c)) in - LocalRawAssum (nal,bk,t) :: bl', c - | CProdN (loc,(nal,bk,t)::bll,c) -> - let n' = List.length nal in - if n' > n then - let nal1,nal2 = list_chop n nal in - [LocalRawAssum (nal1,bk,t)], CProdN (loc,(nal2,bk,t)::bll,c) - else - let bl', c = strip_context (n-n') iscast - (if bll=[] then c else CProdN (loc,bll,c)) in - LocalRawAssum (nal,bk,t) :: bl', c - | CArrow (loc,t,c) -> - let bl', c = strip_context (n-1) iscast c in - LocalRawAssum ([loc,Anonymous],default_binder_kind,t) :: bl', c - | CCast (_,c,_) -> strip_context n false c - | CLetIn (_,na,b,c) -> - let bl', c = strip_context (n-1) iscast c in - LocalRawDef (na,b) :: bl', c - | _ -> anomaly "strip_context" - type term_pr = { pr_constr_expr : constr_expr -> std_ppcmds; pr_lconstr_expr : constr_expr -> std_ppcmds; diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 864b5b227..64b8b7bc9 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -90,8 +90,6 @@ let pr_quantified_hypothesis = function | AnonHyp n -> int n | NamedHyp id -> pr_id id -let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h - let pr_binding prc = function | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) @@ -130,11 +128,6 @@ let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s) let with_evars ev s = if ev then "e" ^ s else s -let out_bindings = function - | ImplicitBindings l -> ImplicitBindings (List.map snd l) - | ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l) - | NoBindings -> NoBindings - let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = @@ -294,8 +287,6 @@ let pr_extend prc prlc prtac prpat = (**********************************************************************) (* The tactic printer *) -let sep_v = fun _ -> str"," ++ spc() - let strip_prod_binders_expr n ty = let rec strip_ty acc n ty = match ty with @@ -316,8 +307,6 @@ let pr_ltac_or_var pr = function | ArgArg x -> pr x | ArgVar (loc,id) -> pr_with_comments loc (pr_id id) -let pr_arg pr x = spc () ++ pr x - let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp) @@ -326,12 +315,6 @@ let pr_evaluable_reference_env env = function | EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp) -let pr_quantified_hypothesis = function - | AnonHyp n -> int n - | NamedHyp id -> pr_id id - -let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h - let pr_esubst prc l = let pr_qhyp = function (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" @@ -356,10 +339,6 @@ let pr_bindings prlc prc = pr_bindings_gen false prlc prc let pr_with_bindings prlc prc (c,bl) = hov 1 (prc c ++ pr_bindings prlc prc bl) -let pr_with_constr prc = function - | None -> mt () - | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c) - let pr_with_induction_names = function | None, None -> mt () | eqpat, ipat -> @@ -441,15 +420,6 @@ let pr_clauses default_is_concl pr_id = function (if occs = no_occurrences_expr then mt () else pr_with_occurrences (fun () -> str" |- *") (occs,()))) -let pr_clause_pattern pr_id = function - | (None, []) -> mt () - | (glopt,l) -> - str " in" ++ - prlist - (fun (id,nl) -> prlist (pr_arg int) nl - ++ spc () ++ pr_id id) l ++ - pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt - let pr_orient b = if b then mt () else str " <-" let pr_multi = function @@ -546,20 +516,6 @@ let pr_auto_using prc = function | l -> spc () ++ hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l) -let pr_autoarg_adding = function - | [] -> mt () - | l -> - spc () ++ str "adding [" ++ - hv 0 (prlist_with_sep spc pr_reference l) ++ str "]" - -let pr_autoarg_destructing = function - | true -> spc () ++ str "destructing" - | false -> mt () - -let pr_autoarg_usingTDB = function - | true -> spc () ++ str "using tdb" - | false -> mt () - let pr_then () = str ";" let ltop = (5,E) @@ -1037,9 +993,6 @@ let rec raw_printers = and pr_raw_tactic_level env n (t:raw_tactic_expr) = fst (make_pr_tac raw_printers env) n t -and pr_raw_match_rule env t = - snd (make_pr_tac raw_printers env) t - let pr_and_constr_expr pr (c,_) = pr c let pr_pat_and_constr_expr b (c,_) = @@ -1061,9 +1014,6 @@ let rec glob_printers = and pr_glob_tactic_level env n (t:glob_tactic_expr) = fst (make_pr_tac glob_printers env) n t -and pr_glob_match_rule env t = - snd (make_pr_tac glob_printers env) t - let pr_constr_or_lconstr_pattern b = if b then pr_lconstr_pattern else pr_constr_pattern diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index b0ae6d139..ba3371ee3 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -84,27 +84,12 @@ let rec match_vernac_rule tys = function else match_vernac_rule tys rls let sep = fun _ -> spc() -let sep_p = fun _ -> str"." -let sep_v = fun _ -> str"," let sep_v2 = fun _ -> str"," ++ spc() -let sep_pp = fun _ -> str":" let pr_ne_sep sep pr = function [] -> mt() | l -> sep() ++ pr l -let pr_entry_prec = function - | Some LeftA -> str"LEFTA " - | Some RightA -> str"RIGHTA " - | Some NonA -> str"NONA " - | None -> mt() - -let pr_prec = function - | Some LeftA -> str", left associativity" - | Some RightA -> str", right associativity" - | Some NonA -> str", no associativity" - | None -> mt() - let pr_set_entry_type = function | ETName -> str"ident" | ETReference -> str"global" @@ -168,11 +153,6 @@ let pr_explanation (e,b,f) = let a = if f then str"!" ++ a else a in if b then str "[" ++ a ++ str "]" else a -let pr_class_rawexpr = function - | FunClass -> str"Funclass" - | SortClass -> str"Sortclass" - | RefClass qid -> pr_smart_global qid - let pr_option_ref_value = function | QualidRefValue id -> pr_reference id | StringRefValue s -> qs s @@ -290,9 +270,6 @@ let pr_decl_notation prc ((loc,ntn),c,scopt) = fnl () ++ str "where " ++ qs ntn ++ str " := " ++ prc c ++ pr_opt (fun sc -> str ": " ++ str sc) scopt -let pr_vbinders l = - hv 0 (pr_binders l) - let pr_binders_arg = pr_ne_sep spc pr_binders @@ -421,21 +398,6 @@ let pr_grammar_tactic_rule n (_,pil,t) = hov 0 (prlist_with_sep sep pr_production_item pil ++ spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) -let pr_box b = let pr_boxkind = function - | PpHB n -> str"h" ++ spc() ++ int n - | PpVB n -> str"v" ++ spc() ++ int n - | PpHVB n -> str"hv" ++ spc() ++ int n - | PpHOVB n -> str"hov" ++ spc() ++ int n - | PpTB -> str"t" -in str"<" ++ pr_boxkind b ++ str">" - -let pr_paren_reln_or_extern = function - | None,L -> str"L" - | None,E -> str"E" - | Some pprim,Any -> qs pprim - | Some pprim,Prec p -> qs pprim ++ spc() ++ str":" ++ spc() ++ int p - | _ -> mt() - let pr_statement head (id,(bl,c,guard)) = assert (id<>None); hov 0 diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 62dd94893..c4e378826 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -39,7 +39,6 @@ type object_pr = { print_module : bool -> Names.module_path -> std_ppcmds; print_modtype : module_path -> std_ppcmds; print_named_decl : identifier * constr option * types -> std_ppcmds; - print_leaf_entry : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds; @@ -457,11 +456,6 @@ let gallina_print_library_entry with_values ent = | (_,Lib.FrozenState _) -> None -let gallina_print_leaf_entry with_values c = - match gallina_print_leaf_entry with_values c with - | None -> mt () - | Some pp -> pp ++ fnl() - let gallina_print_context with_values = let rec prec n = function | h::rest when n = None or Option.get n > 0 -> @@ -487,7 +481,6 @@ let default_object_pr = { print_module = gallina_print_module; print_modtype = gallina_print_modtype; print_named_decl = gallina_print_named_decl; - print_leaf_entry = gallina_print_leaf_entry; print_library_entry = gallina_print_library_entry; print_context = gallina_print_context; print_typed_value_in_env = gallina_print_typed_value_in_env; @@ -504,7 +497,6 @@ let print_syntactic_def x = !object_pr.print_syntactic_def x let print_module x = !object_pr.print_module x let print_modtype x = !object_pr.print_modtype x let print_named_decl x = !object_pr.print_named_decl x -let print_leaf_entry x = !object_pr.print_leaf_entry x let print_library_entry x = !object_pr.print_library_entry x let print_context x = !object_pr.print_context x let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x @@ -583,16 +575,6 @@ let print_full_pure_context () = assume that the declaration of constructors and eliminations follows the definition of the inductive type *) -let list_filter_vec f vec = - let rec frec n lf = - if n < 0 then lf - else if f vec.(n) then - frec (n-1) (vec.(n)::lf) - else - frec (n-1) lf - in - frec (Array.length vec -1) [] - (* This is designed to print the contents of an opened section *) let read_sec_context r = let loc,qid = qualid_of_reference r in @@ -692,15 +674,6 @@ let print_impargs ref = (if has_impl then print_impl_args impl else (str "No implicit arguments" ++ fnl ())) -let unfold_head_fconst = - let rec unfrec k = match kind_of_term k with - | Const cst -> constant_value (Global.env ()) cst - | Lambda (na,t,b) -> mkLambda (na,t,unfrec b) - | App (f,v) -> appvect (unfrec f,v) - | _ -> k - in - unfrec - (* for debug *) let inspect depth = print_context false (Some depth) (Lib.contents_after None) diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index a7820e034..842fc4e89 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -74,7 +74,6 @@ type object_pr = { print_module : bool -> Names.module_path -> std_ppcmds; print_modtype : module_path -> std_ppcmds; print_named_decl : identifier * constr option * types -> std_ppcmds; - print_leaf_entry : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds; diff --git a/parsing/printer.ml b/parsing/printer.ml index 5d6837e13..34637b1e8 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -242,18 +242,6 @@ let pr_context_of env = match Flags.print_hyps_limit () with (* display goal parts (Proof mode) *) -let pr_restricted_named_context among env = - hv 0 (fold_named_context - (fun env ((id,_,_) as d) pps -> - if true || Idset.mem id among then - pps ++ - fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++ - pr_var_decl env d - else - pps) - env ~init:(mt ())) - - let pr_predicate pr_elt (b, elts) = let pr_elts = prlist_with_sep spc pr_elt elts in if b then @@ -269,13 +257,6 @@ let pr_transparent_state (ids, csts) = hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) -let pr_subgoal_metas metas env= - let pr_one (meta,typ) = - str "?" ++ int meta ++ str " : " ++ - hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253)) "") in - hv 0 (prlist_with_sep mt pr_one metas) - (* display complete goal *) let default_pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in -- cgit v1.2.3