diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 15 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 5 | ||||
| -rw-r--r-- | printing/pputils.ml | 99 | ||||
| -rw-r--r-- | printing/pputils.mli | 24 | ||||
| -rw-r--r-- | printing/printer.ml | 14 | ||||
| -rw-r--r-- | printing/printer.mli | 2 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 6 |
7 files changed, 31 insertions, 134 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 6d53349fa1..26202ef4ca 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -14,7 +14,6 @@ open Util open Pp open CAst open Names -open Nameops open Libnames open Pputils open Ppextend @@ -230,20 +229,6 @@ let tag_var = tag Tag.variable | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t - let pr_lident {loc; v=id} = - match loc with - | None -> pr_id id - | Some loc -> let (b,_) = Loc.unloc loc in - pr_located pr_id (Some (Loc.make_loc (b,b + String.length (Id.to_string id))), id) - - let pr_lname = function - | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id) - | x -> pr_ast Name.print x - - let pr_or_var pr = function - | Locus.ArgArg x -> pr x - | Locus.ArgVar id -> pr_lident id - let pr_prim_token = function | Numeral (n,s) -> str (if s then n else "-"^n) | String s -> qs s diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index e7f71849a5..1cb3aa6d7a 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -21,11 +21,6 @@ val prec_less : precedence -> tolerability -> bool val pr_tight_coma : unit -> Pp.t -val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t - -val pr_lident : lident -> Pp.t -val pr_lname : lname -> Pp.t - val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t val pr_com_at : int -> Pp.t val pr_sep_com : diff --git a/printing/pputils.ml b/printing/pputils.ml index 59e5f68f22..e6daf9544c 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -12,7 +12,6 @@ open Util open Pp open Genarg open Locus -open Genredexpr let beautify_comments = ref [] @@ -39,91 +38,25 @@ let pr_located pr (loc, x) = let pr_ast pr { CAst.loc; v } = pr_located pr (loc, v) -let pr_or_var pr = function - | ArgArg x -> pr x - | ArgVar {CAst.v=s} -> Names.Id.print s - -let pr_with_occurrences pr keyword (occs,c) = - match occs with - | AllOccurrences -> - pr c - | NoOccurrences -> - failwith "pr_with_occurrences: no occurrences" - | OnlyOccurrences nl -> - hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++ - hov 0 (prlist_with_sep spc (pr_or_var int) nl)) - | AllOccurrencesBut nl -> - hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++ - hov 0 (prlist_with_sep spc (pr_or_var int) nl)) - -exception ComplexRedFlag - -let pr_short_red_flag pr r = - if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then - raise ComplexRedFlag - else if List.is_empty r.rConst then - if r.rDelta then mt () else raise ComplexRedFlag - else (if r.rDelta then str "-" else mt ()) ++ - hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]") - -let pr_red_flag pr r = - try pr_short_red_flag pr r - with ComplexRedFlag -> - (if r.rBeta then pr_arg str "beta" else mt ()) ++ - (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else - (if r.rMatch then pr_arg str "match" else mt ()) ++ - (if r.rFix then pr_arg str "fix" else mt ()) ++ - (if r.rCofix then pr_arg str "cofix" else mt ())) ++ - (if r.rZeta then pr_arg str "zeta" else mt ()) ++ - (if List.is_empty r.rConst then - if r.rDelta then pr_arg str "delta" - else mt () - else - pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ - hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) - -let pr_union pr1 pr2 = function - | Inl a -> pr1 a - | Inr b -> pr2 b - -let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function - | Red false -> keyword "red" - | Hnf -> keyword "hnf" - | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f) - ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o - | Cbv f -> - if f.rBeta && f.rMatch && f.rFix && f.rCofix && - f.rZeta && f.rDelta && List.is_empty f.rConst then - keyword "compute" - else - hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f) - | Lazy f -> - hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f) - | Cbn f -> - hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f) - | Unfold l -> - hov 1 (keyword "unfold" ++ spc() ++ - prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l) - | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l) - | Pattern l -> - hov 1 (keyword "pattern" ++ - pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l) +let pr_lident { CAst.loc; v=id } = + let open Names.Id in + match loc with + | None -> print id + | Some loc -> let (b,_) = Loc.unloc loc in + pr_located print + (Some (Loc.make_loc (b,b + String.length (to_string id))), id) - | Red true -> - CErrors.user_err Pp.(str "Shouldn't be accessible from user.") - | ExtraRedExpr s -> - str s - | CbvVm o -> - keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o - | CbvNative o -> - keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o +let pr_lname = let open Names in function + | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id) + | x -> pr_ast Name.print x -let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) = - pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma) +let pr_or_var pr = function + | ArgArg x -> pr x + | ArgVar id -> pr_lident id -let pr_or_by_notation f = let open Constrexpr in function - | {CAst.loc; v=AN v} -> f v - | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc +let pr_or_by_notation f = let open Constrexpr in CAst.with_val (function + | AN v -> f v + | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc) let hov_if_not_empty n p = if Pp.ismt p then p else hov n p diff --git a/printing/pputils.mli b/printing/pputils.mli index 5b1969e232..ea554355bc 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -8,33 +8,17 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Genarg -open Locus -open Genredexpr val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t (** Prints an object surrounded by its commented location *) -val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t +val pr_lident : lident -> Pp.t +val pr_lname : lname -> Pp.t +val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t -val pr_with_occurrences : - ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t - -val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t -val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t - -val pr_red_expr : - ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> - (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t - -val pr_red_expr_env : Environ.env -> Evd.evar_map -> - (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * - (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * - ('b -> Pp.t) * - (Environ.env -> Evd.evar_map -> 'c -> Pp.t) -> - (string -> Pp.t) -> - ('a,'b,'c) red_expr_gen -> Pp.t val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t diff --git a/printing/printer.ml b/printing/printer.ml index b80133b171..be0139da06 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -546,10 +546,10 @@ let rec pr_evars_int_hd pr sigma i = function (hov 0 (pr i evk evi)) ++ (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd pr sigma (i+1) rest) -let pr_evars_int sigma ~shelf ~givenup i evs = +let pr_evars_int sigma ~shelf ~given_up i evs = let pr_status i = if List.mem i shelf then str " (shelved)" - else if List.mem i givenup then str " (given up)" + else if List.mem i given_up then str " (given up)" else mt () in pr_evars_int_hd (fun i evk evi -> @@ -761,7 +761,7 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map if Evar.Map.is_empty exl then (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else - let pei = pr_evars_int sigma ~shelf ~givenup:[] 1 exl in + let pei = pr_evars_int sigma ~shelf ~given_up:[] 1 exl in v 0 ((str "No more subgoals," ++ str " but there are non-instantiated existential variables:" ++ cut () ++ (hov 0 pei) @@ -789,7 +789,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = straightforward, but seriously, [Proof.proof] should return [evar_info]-s instead. *) let p = proof in - let (goals , stack , shelf, given_up, sigma ) = Proof.proof p in + let Proof.{goals; stack; shelf; given_up; sigma} = Proof.data p in let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in let seeds = Proof.V82.top_evars p in begin match goals with @@ -821,7 +821,7 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in let os_map = match oproof with | Some op when diffs -> - let (_,_,_,_, osigma) = Proof.proof op in + let Proof.{sigma=osigma} = Proof.data op in let diff_goal_map = Proof_diffs.make_goal_map oproof proof in Some (osigma, diff_goal_map) | _ -> None @@ -834,8 +834,8 @@ let pr_open_subgoals ~proof = pr_open_subgoals_diff proof let pr_nth_open_subgoal ~proof n = - let gls,_,_,_,sigma = Proof.proof proof in - pr_subgoal n sigma gls + let Proof.{goals;sigma} = Proof.data proof in + pr_subgoal n sigma goals let pr_goal_by_id ~proof id = try diff --git a/printing/printer.mli b/printing/printer.mli index 357f30d1f4..fd4682a086 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -182,7 +182,7 @@ val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Pr val pr_open_subgoals : proof:Proof.t -> Pp.t val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t -val pr_evars_int : evar_map -> shelf:Goal.goal list -> givenup:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t +val pr_evars_int : evar_map -> shelf:Goal.goal list -> given_up:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index a381266976..b280ce909b 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -553,7 +553,7 @@ open Goal.Set let db_goal_map op np ng_to_og = let pr_goals title prf = Printf.printf "%s: " title; - let (goals,_,_,_,sigma) = Proof.proof prf in + let Proof.{goals;sigma} = Proof.data prf in List.iter (fun g -> Printf.printf "%d -> %s " (Evar.repr g) (goal_to_evar g sigma)) goals; let gs = diff (Proof.all_goals prf) (List.fold_left (fun s g -> add g s) empty goals) in List.iter (fun g -> Printf.printf "%d " (Evar.repr g)) (elements gs); @@ -626,11 +626,11 @@ let make_goal_map_i op np = let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in let oevar_to_og = ref StringMap.empty in - let (_,_,_,_,osigma) = Proof.proof op 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) (Goal.Set.elements rem_gs); - let (_,_,_,_,nsigma) = Proof.proof np in + 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 |