diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/genprint.ml | 4 | ||||
| -rw-r--r-- | printing/genprint.mli | 4 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 11 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 4 | ||||
| -rw-r--r-- | printing/pputils.ml | 4 | ||||
| -rw-r--r-- | printing/pputils.mli | 4 | ||||
| -rw-r--r-- | printing/printer.ml | 8 | ||||
| -rw-r--r-- | printing/printer.mli | 12 | ||||
| -rw-r--r-- | printing/printmod.ml | 4 | ||||
| -rw-r--r-- | printing/printmod.mli | 4 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 55 | ||||
| -rw-r--r-- | printing/proof_diffs.mli | 15 |
12 files changed, 61 insertions, 68 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml index a673cbd933..0157c066b6 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/genprint.mli b/printing/genprint.mli index 59e36baeb6..64ec8a57df 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 59972f8bdb..b285c0abcc 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -77,8 +77,8 @@ let tag_var = tag Tag.variable | LevelSome -> true let prec_of_prim_token = function - | Numeral (SPlus,_) -> lposint - | Numeral (SMinus,_) -> lnegint + | Numeral (NumTok.SPlus,_) -> lposint + | Numeral (NumTok.SMinus,_) -> lnegint | String _ -> latom let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps = @@ -222,8 +222,7 @@ let tag_var = tag Tag.variable | t -> str " :" ++ pr_sep_com (fun()->brk(1,4)) (pr ltop) t let pr_prim_token = function - | Numeral (SPlus,n) -> str (NumTok.to_string n) - | Numeral (SMinus,n) -> str ("-"^NumTok.to_string n) + | Numeral n -> NumTok.Signed.print n | String s -> qs s let pr_evar pr id l = diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 288fb251c4..2850e4bfa0 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/pputils.ml b/printing/pputils.ml index 5ec2f93cd8..896d38523a 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/pputils.mli b/printing/pputils.mli index f260c4a373..479db15fff 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/printer.ml b/printing/printer.ml index b376616b61..32dc4bb0f0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -106,8 +106,8 @@ let pr_letype_env = Proof_diffs.pr_letype_env let pr_type_env ?lax ?goal_concl_style env sigma c = pr_etype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c) -let pr_ltype_env ?lax ?goal_concl_style env sigma c = - pr_letype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c) +let pr_ltype_env ?lax ?goal_concl_style env sigma ?impargs c = + pr_letype_env ?lax ?goal_concl_style env sigma ?impargs (EConstr.of_constr c) let pr_ljudge_env env sigma j = (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) diff --git a/printing/printer.mli b/printing/printer.mli index 24d0a8cf6a..936426949c 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -45,6 +45,10 @@ val enable_goal_names_printing : bool ref intended to be printed in scope [some_scope_name]. It defaults to [None]. + [~impargs:some_list_of_binding_kind] indicates the implicit arguments + of the external quatification. Only used for printing types (not + terms), and at toplevel (only "l" versions). It defaults to [None]. + [~lax:true] is for debugging purpose. It defaults to [~lax:false]. *) @@ -66,7 +70,7 @@ val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env - val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t val pr_etype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t -val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t +val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t val pr_open_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t val pr_open_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t @@ -97,7 +101,7 @@ val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp [~lax:true] is for debugging purpose. *) -val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t +val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> ?impargs:Glob_term.binding_kind list -> types -> Pp.t val pr_type_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> closed_glob_constr -> Pp.t diff --git a/printing/printmod.ml b/printing/printmod.ml index b84113bde2..eec2fe86ac 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/printmod.mli b/printing/printmod.mli index 4c9245ee27..c7f056063b 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index c3ee5968dc..3a6424ba9f 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -85,8 +85,6 @@ let log_out_ch = ref stdout let cprintf s = cfprintf !log_out_ch s [@@@ocaml.warning "+32"] -module StringMap = Map.Make(String);; - let tokenize_string s = (* todo: cLexer changes buff as it proceeds. Seems like that should be saved, too. But I don't understand how it's used--it looks like things get appended to it but @@ -98,18 +96,17 @@ let tokenize_string s = else stream_tok ((Tok.extract_string true e) :: acc) str in - let st = CLexer.get_lexer_state () in + let st = CLexer.Lexer.State.get () in try let istr = Stream.of_string s in let lex = CLexer.LexerDiff.tok_func istr in let toks = stream_tok [] (fst lex) in - CLexer.set_lexer_state st; + CLexer.Lexer.State.set st; toks with exn -> - CLexer.set_lexer_state st; + CLexer.Lexer.State.set st; raise (Diff_Failure "Input string is not lexable");; - type hyp_info = { idents: string list; rhs_pp: Pp.t; @@ -124,22 +121,22 @@ type hyp_info = { let diff_hyps o_line_idents o_map n_line_idents n_map = let rv : Pp.t list ref = ref [] in - let is_done ident map = (StringMap.find ident map).done_ in + let is_done ident map = (CString.Map.find ident map).done_ in let exists ident map = - try let _ = StringMap.find ident map in true + try let _ = CString.Map.find ident map in true with Not_found -> false in let contains l ident = try [List.find (fun x -> x = ident) l] with Not_found -> [] in let output old_ids_uo new_ids = (* use the order from the old line in case it's changed in the new *) let old_ids = if old_ids_uo = [] then [] else - let orig = (StringMap.find (List.hd old_ids_uo) o_map).idents in + let orig = (CString.Map.find (List.hd old_ids_uo) o_map).idents in List.concat (List.map (contains orig) old_ids_uo) in let setup ids map = if ids = [] then ("", Pp.mt ()) else let open Pp in - let rhs_pp = (StringMap.find (List.hd ids) map).rhs_pp in + let rhs_pp = (CString.Map.find (List.hd ids) map).rhs_pp in let pp_ids = List.map (fun x -> str x) ids in let hyp_pp = List.fold_left (fun l1 l2 -> l1 ++ str ", " ++ l2) (List.hd pp_ids) (List.tl pp_ids) ++ rhs_pp in (string_of_ppcmds hyp_pp, hyp_pp) @@ -151,11 +148,11 @@ let diff_hyps o_line_idents o_map n_line_idents n_map = let hyp_diffs = diff_str ~tokenize_string o_line n_line in let (has_added, has_removed) = has_changes hyp_diffs in if show_removed () && has_removed then begin - List.iter (fun x -> (StringMap.find x o_map).done_ <- true) old_ids; + List.iter (fun x -> (CString.Map.find x o_map).done_ <- true) old_ids; rv := (add_diff_tags `Removed o_pp hyp_diffs) :: !rv; end; if n_line <> "" then begin - List.iter (fun x -> (StringMap.find x n_map).done_ <- true) new_ids; + List.iter (fun x -> (CString.Map.find x n_map).done_ <- true) new_ids; rv := (add_diff_tags `Added n_pp hyp_diffs) :: !rv end in @@ -166,14 +163,14 @@ let diff_hyps o_line_idents o_map n_line_idents n_map = match dtype with | `Removed -> if dtype = `Removed then begin - let o_idents = (StringMap.find ident o_map).idents in + let o_idents = (CString.Map.find ident o_map).idents in (* only show lines that have all idents removed here; other removed idents appear later *) if show_removed () && not (is_done ident o_map) && List.for_all (fun x -> not (exists x n_map)) o_idents then output (List.rev o_idents) [] end | _ -> begin (* Added or Common case *) - let n_idents = (StringMap.find ident n_map).idents in + let n_idents = (CString.Map.find ident n_map).idents in (* Process a new hyp line, possibly splitting it. Duplicates some of process_ident iteration, but easier to understand this way *) @@ -184,13 +181,13 @@ let diff_hyps o_line_idents o_map n_line_idents n_map = let fst_omap_idents = ref None in let add ids id map = ids := id :: !ids; - (StringMap.find id map).done_ <- true in + (CString.Map.find id map).done_ <- true in (* get identifiers shared by one old and one new line, plus other Added in new and other Removed in old *) let process_split ident3 = if not (is_done ident3 n_map) then begin - let this_omap_idents = try Some (StringMap.find ident3 o_map).idents + let this_omap_idents = try Some (CString.Map.find ident3 o_map).idents with Not_found -> None in if !fst_omap_idents = None then fst_omap_idents := this_omap_idents; @@ -244,9 +241,9 @@ let process_goal sigma g : EConstr.t reified_goal = let hyps = List.map to_tuple hyps in { name; ty; hyps; env; sigma };; -let pr_letype_env ?lax ?goal_concl_style env sigma t = +let pr_letype_env ?lax ?goal_concl_style env sigma ?impargs t = Ppconstr.pr_lconstr_expr env sigma - (Constrextern.extern_type ?lax ?goal_concl_style env sigma t) + (Constrextern.extern_type ?lax ?goal_concl_style env sigma ?impargs t) let pp_of_type env sigma ty = pr_letype_env ~goal_concl_style:true env sigma ty @@ -290,7 +287,7 @@ map will contain: concl_pp is the conclusion as a Pp.t *) let goal_info goal sigma = - let map = ref StringMap.empty in + let map = ref CString.Map.empty in let line_idents = ref [] in let build_hyp_info env sigma hyp = let (names, body, ty) = hyp in @@ -308,7 +305,7 @@ let goal_info goal sigma = let rhs_pp = mid ++ str " : " ++ ts in let make_entry () = { idents; rhs_pp; done_ = false } in - List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents + List.iter (fun ident -> map := (CString.Map.add ident (make_entry ()) !map); ()) idents in try @@ -339,7 +336,7 @@ let unwrap g_s = let goal = Evd.sig_it g_s in let sigma = Refiner.project g_s in goal_info goal sigma - | None -> ([], StringMap.empty, Pp.mt ()) + | None -> ([], CString.Map.empty, Pp.mt ()) let diff_goal_ide og_s ng nsigma = diff_goal_info (unwrap og_s) (goal_info ng nsigma) @@ -405,7 +402,7 @@ the call to db_goal_map and entering the following: (conj (conj ?Goal0 ?Goal1) ?Goal) <--- goal 4 is still the rightmost goal in the proof *) let match_goals ot nt = - let nevar_to_oevar = ref StringMap.empty in + let nevar_to_oevar = ref CString.Map.empty in (* ogname is "" when there is no difference on the current path. It's set to the old goal's evar name once a rewritten goal is found, at which point the code only searches for the replacing goals @@ -514,7 +511,7 @@ let match_goals ot nt = | CPatVar _, CPatVar _ -> () | CEvar (n,l), CEvar (n2,l2) -> let oevar = if ogname = "" then Id.to_string n else ogname in - nevar_to_oevar := StringMap.add (Id.to_string n2) oevar !nevar_to_oevar; + nevar_to_oevar := CString.Map.add (Id.to_string n2) oevar !nevar_to_oevar; iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2 | CEvar (n,l), nt' -> (* pass down the old goal evar name *) @@ -641,16 +638,16 @@ let make_goal_map_i op np = (* >= 2 removals, >= 1 addition, need to match *) let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in - let oevar_to_og = ref StringMap.empty in + let oevar_to_og = ref CString.Map.empty in let Proof.{sigma=osigma} = Proof.data op in - List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og) + List.iter (fun og -> oevar_to_og := CString.Map.add (goal_to_evar og osigma) og !oevar_to_og) (Goal.Set.elements rem_gs); let Proof.{sigma=nsigma} = Proof.data np in let get_og ng = let nevar = goal_to_evar ng nsigma in - let oevar = StringMap.find nevar nevar_to_oevar in - let og = StringMap.find oevar !oevar_to_og in + let oevar = CString.Map.find nevar nevar_to_oevar in + let og = CString.Map.find oevar !oevar_to_og in og in Goal.Set.iter (fun ng -> diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index eebdaccd32..24b171770a 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -57,7 +57,7 @@ val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t (** Convert a string to a list of token strings using the lexer *) val tokenize_string : string -> string list -val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t +val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> EConstr.types -> Pp.t val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> env -> evar_map -> constr -> Pp.t @@ -83,11 +83,4 @@ type hyp_info = { mutable done_: bool; } -module StringMap : -sig - type +'a t - val empty: hyp_info t - val add : string -> hyp_info -> hyp_info t -> hyp_info t -end - -val diff_hyps : string list list -> hyp_info StringMap.t -> string list list -> hyp_info StringMap.t -> Pp.t list +val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list |