diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/genprint.ml | 6 | ||||
| -rw-r--r-- | printing/miscprint.ml | 4 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 30 | ||||
| -rw-r--r-- | printing/pptactic.ml | 378 | ||||
| -rw-r--r-- | printing/pptactic.mli | 8 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 56 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 37 | ||||
| -rw-r--r-- | printing/prettyp.ml | 31 | ||||
| -rw-r--r-- | printing/prettyp.mli | 2 | ||||
| -rw-r--r-- | printing/printer.ml | 34 | ||||
| -rw-r--r-- | printing/printer.mli | 13 | ||||
| -rw-r--r-- | printing/printmod.ml | 6 |
12 files changed, 284 insertions, 321 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml index d4f792b75..d8bd81c4c 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -40,6 +40,6 @@ let raw_print wit v = (Print.obj wit).raw v let glb_print wit v = (Print.obj wit).glb v let top_print wit v = (Print.obj wit).top v -let generic_raw_print v = unpack { unpacker = fun w v -> raw_print w (raw v); } v -let generic_glb_print v = unpack { unpacker = fun w v -> glb_print w (glb v); } v -let generic_top_print v = unpack { unpacker = fun w v -> top_print w (top v); } v +let generic_raw_print (GenArg (Rawwit w, v)) = raw_print w v +let generic_glb_print (GenArg (Glbwit w, v)) = glb_print w v +let generic_top_print (GenArg (Topwit w, v)) = top_print w v diff --git a/printing/miscprint.ml b/printing/miscprint.ml index 22db3d0bf..5e86c6bd7 100644 --- a/printing/miscprint.ml +++ b/printing/miscprint.ml @@ -33,9 +33,9 @@ and pr_intro_pattern_action prc = function | IntroRewrite false -> str "<-" and pr_or_and_intro_pattern prc = function - | [pl] -> + | IntroAndPattern pl -> str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")" - | pll -> + | IntroOrPattern pll -> str "[" ++ hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) ++ str "]" diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e21bfa007..8a0df18ca 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -136,8 +136,6 @@ end) = struct let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) - let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" - let pr_univ l = match l with | [_,x] -> str x @@ -153,11 +151,11 @@ end) = struct let pr_qualid sp = let (sl, id) = repr_qualid sp in - let id = tag_ref (str (Id.to_string id)) in + let id = tag_ref (pr_id id) in let sl = match List.rev (DirPath.repr sl) with | [] -> mt () | sl -> - let pr dir = tag_path (str (Id.to_string dir)) ++ str "." in + let pr dir = tag_path (pr_id dir) ++ str "." in prlist pr sl in sl ++ id @@ -182,7 +180,7 @@ end) = struct let pr_reference = function | Qualid (_, qid) -> pr_qualid qid - | Ident (_, id) -> tag_var (str (Id.to_string id)) + | Ident (_, id) -> tag_var (pr_id id) let pr_cref ref us = pr_reference ref ++ pr_universe_instance us @@ -457,7 +455,7 @@ end) = struct (pr_decl true) dl ++ fnl() ++ keyword "for" ++ spc () ++ pr_id id - let pr_asin pr (na,indnalopt) = + let pr_asin pr na indnalopt = (match na with (* Decision of printing "_" or not moved to constrextern.ml *) | Some na -> spc () ++ keyword "as" ++ spc () ++ pr_lname na | None -> mt ()) ++ @@ -465,8 +463,8 @@ end) = struct | None -> mt () | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t) - let pr_case_item pr (tm,asin) = - hov 0 (pr (lcast,E) tm ++ pr_asin pr asin) + let pr_case_item pr (tm,as_clause, in_clause) = + hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause) let pr_case_type pr po = match po with @@ -595,28 +593,20 @@ end) = struct return (p, lproj) | CApp (_,(None,a),l) -> return (pr_app (pr mt) a l, lapp) - | CRecord (_,w,l) -> - let beg = - match w with - | None -> - spc () - | Some t -> - spc () ++ pr spc ltop t ++ spc () - ++ keyword "with" ++ spc () - in + | CRecord (_,l) -> return ( - hv 0 (str"{|" ++ beg ++ + hv 0 (str"{|" ++ spc () ++ prlist_with_sep pr_semicolon (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l ++ str" |}"), latom ) - | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) -> + | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ hov 0 (pr_patt ltop p ++ - pr_asin (pr_dangling_with_for mt pr) asin ++ + pr_asin (pr_dangling_with_for mt pr) as_clause in_clause ++ str " :=" ++ pr spc ltop c ++ pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++ spc () ++ keyword "in" ++ pr spc ltop b)), diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7e903d2d3..c00036bb3 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -26,21 +26,22 @@ open Printer let pr_global x = Nametab.pr_global_env Id.Set.empty x -type grammar_terminals = string option list +type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list type pp_tactic = { - pptac_args : argument_type list; - pptac_prods : int * grammar_terminals; + pptac_level : int; + pptac_prods : grammar_terminals; } (* ML Extensions *) -let prtac_tab = Hashtbl.create 17 +let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t = + Hashtbl.create 17 (* Tactic notations *) let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty let declare_ml_tactic_pprule key pt = - Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods + Hashtbl.add prtac_tab key pt let declare_notation_tactic_pprule kn pt = prnotation_tab := KNmap.add kn pt !prnotation_tab @@ -264,149 +265,89 @@ module Make let with_evars ev s = if ev then "e" ^ s else s - let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = - match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x) - | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x) - | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x) - | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x) - | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) - | ConstrMayEvalArgType -> - pr_may_eval prc prlc (pr_or_by_notation prref) prpat - (out_gen (rawwit wit_constr_may_eval) x) - | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat) - (out_gen (rawwit wit_red_expr) x) - | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x) - | ListArgType _ -> - let list_unpacker wit l = - let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in - pr_sequence map (raw l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match raw o with + let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () - | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) - in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = raw o in - let p = in_gen (rawwit wit1) p in - let q = in_gen (rawwit wit2) q in - pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q] + | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in - hov 0 (pair_unpack { pair_unpacker } x) - | ExtraArgType s -> - try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genprint.generic_raw_print x - - - let rec pr_glb_generic prc prlc prtac prpat x = - match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x) - | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x) - | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x) - | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x) - | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) - | ConstrMayEvalArgType -> - pr_may_eval prc prlc - (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat - (out_gen (glbwit wit_constr_may_eval) x) - | QuantHypArgType -> - pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr - (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat) - (out_gen (glbwit wit_red_expr) x) - | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x) - | ListArgType _ -> - let list_unpacker wit l = - let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in - pr_sequence map (glb l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match glb o with + hov 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (rawwit wit1) p in + let q = in_gen (rawwit wit2) q in + hov 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q]) + | ExtraArg s -> + try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x) + with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x) + + + let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () - | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) - in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = glb o in - let p = in_gen (glbwit wit1) p in - let q = in_gen (glbwit wit2) q in - pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q] + | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in - hov 0 (pair_unpack { pair_unpacker } x) - | ExtraArgType s -> - try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genprint.generic_glb_print x - - let rec pr_top_generic prc prlc prtac prpat x = - match Genarg.genarg_tag x with - | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x) - | IdentArgType -> pr_id (out_gen (topwit wit_ident) x) - | VarArgType -> pr_id (out_gen (topwit wit_var) x) - | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x) - | ConstrArgType -> prc (out_gen (topwit wit_constr) x) - | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x) - | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr (prc,prlc,pr_evaluable_reference,prpat) - (out_gen (topwit wit_red_expr) x) - | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in - pr_with_bindings prc prlc (c,b) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it - | ListArgType _ -> - let list_unpacker wit l = - let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in - pr_sequence map (top l) - in - hov 0 (list_unpack { list_unpacker } x) - | OptArgType _ -> - let opt_unpacker wit o = match top o with + hov 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (glbwit wit1) p in + let q = in_gen (glbwit wit2) q in + let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in + hov 0 ans + | ExtraArg s -> + try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x) + with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x) + + let rec pr_top_generic_rec prc prlc prtac prpat (GenArg (Topwit wit, x)) = + match wit with + | ListArg wit -> + let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in + let ans = pr_sequence map x in + hov 0 ans + | OptArg wit -> + let ans = match x with | None -> mt () - | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) - in - hov 0 (opt_unpack { opt_unpacker } x) - | PairArgType _ -> - let pair_unpacker wit1 wit2 o = - let p, q = top o in - let p = in_gen (topwit wit1) p in - let q = in_gen (topwit wit2) q in - pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q] + | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in - hov 0 (pair_unpack { pair_unpacker } x) - | ExtraArgType s -> - try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x - with Not_found -> Genprint.generic_top_print x + hov 0 ans + | PairArg (wit1, wit2) -> + let p, q = x in + let p = in_gen (topwit wit1) p in + let q = in_gen (topwit wit2) q in + let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in + hov 0 ans + | ExtraArg s -> + try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x) + with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x) let rec tacarg_using_rule_token pr_gen = function - | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) - | None :: l, a :: al -> + | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) + | Egramml.GramNonTerminal _ :: l, a :: al -> let r = tacarg_using_rule_token pr_gen (l,al) in pr_gen a :: r | [], [] -> [] | _ -> failwith "Inconsistent arguments of extended tactic" + type any_arg = AnyArg : 'a Genarg.raw_abstract_argument_type -> any_arg + + let filter_arg = function + | Egramml.GramTerminal _ -> None + | Egramml.GramNonTerminal (_, t, _) -> Some (AnyArg t) + let pr_tacarg_using_rule pr_gen l = let l = match l with - | (Some s :: l, al) -> + | (Egramml.GramTerminal s :: l, al) -> (** First terminal token should be considered as the name of the tactic, so we tag it differently than the other terminal tokens. *) primitive s :: (tacarg_using_rule_token pr_gen (l, al)) @@ -414,42 +355,54 @@ module Make in pr_sequence (fun x -> x) l - let pr_extend_gen pr_gen lev s l = + let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l = try - let tags = List.map genarg_tag l in - let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in - let p = pr_tacarg_using_rule pr_gen (pl,l) in - if lev' > lev then surround p else p + let pp_rules = Hashtbl.find prtac_tab s in + let pp = pp_rules.(i) in + let args = List.map_filter filter_arg pp.pptac_prods in + let () = if not (List.for_all2eq check args l) then raise Not_found in + let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in + if pp.pptac_level > lev then surround p else p with Not_found -> - let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in + let name = + str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ + str "@" ++ int i + in let args = match l with | [] -> mt () | _ -> spc() ++ pr_sequence pr_gen l in str "<" ++ name ++ str ">" ++ args - let pr_alias_gen pr_gen lev key l = + let pr_alias_gen check pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in - let (lev', pl) = pp.pptac_prods in - let p = pr_tacarg_using_rule pr_gen (pl, l) in - if lev' > lev then surround p else p + let args = List.map_filter filter_arg pp.pptac_prods in + let () = if not (List.for_all2eq check args l) then raise Not_found in + let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in + if pp.pptac_level > lev then surround p else p with Not_found -> KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" - let pr_raw_extend prc prlc prtac prpat = - pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference) - let pr_glob_extend prc prlc prtac prpat = - pr_extend_gen (pr_glb_generic prc prlc prtac prpat) - let pr_extend prc prlc prtac prpat = - pr_extend_gen (pr_top_generic prc prlc prtac prpat) + let check_type t arg = match t, arg with + | AnyArg t, TacGeneric arg -> argument_type_eq (unquote t) (genarg_tag arg) + | _ -> false + + let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false + + let pr_raw_extend_rec prc prlc prtac prpat = + pr_extend_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)) + let pr_glob_extend_rec prc prlc prtac prpat = + pr_extend_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat)) + let pr_extend_rec prc prlc prtac prpat = + pr_extend_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat)) let pr_raw_alias prc prlc prtac prpat = - pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference) + pr_alias_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)) let pr_glob_alias prc prlc prtac prpat = - pr_alias_gen (pr_glb_generic prc prlc prtac prpat) + pr_alias_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat)) let pr_alias prc prlc prtac prpat = - pr_alias_gen (pr_top_generic prc prlc prtac prpat) + pr_alias_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat)) (**********************************************************************) (* The tactic printer *) @@ -716,11 +669,6 @@ module Make | l -> spc () ++ hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l) - let string_of_debug = function - | Off -> "" - | Debug -> "debug " - | Info -> "info_" - let pr_then () = str ";" let ltop = (5,E) @@ -755,8 +703,8 @@ module Make pr_reference : 'ref -> std_ppcmds; pr_name : 'nam -> std_ppcmds; pr_generic : 'lev generic_argument -> std_ppcmds; - pr_extend : int -> ml_tactic_name -> 'lev generic_argument list -> std_ppcmds; - pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds; + pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds; + pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds; } constraint 'a = < @@ -843,8 +791,6 @@ module Make let rec pr_atom0 a = tag_atom a (match a with | TacIntroPattern [] -> primitive "intros" | TacIntroMove (None,MoveLast) -> primitive "intro" - | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial" - | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto" | TacClear (true,[]) -> primitive "clear" | t -> str "(" ++ pr_atom1 t ++ str ")" ) @@ -953,23 +899,6 @@ module Make ++ pr_arg pr_quantified_hypothesis h2 ) - (* Automation tactics *) - | TacTrivial (_,[],Some []) as x -> - pr_atom0 x - | TacTrivial (d,lems,db) -> - hov 0 ( - str (string_of_debug d) ++ primitive "trivial" - ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db - ) - | TacAuto (_,None,[],Some []) as x -> - pr_atom0 x - | TacAuto (d,n,lems,db) -> - hov 0 ( - str (string_of_debug d) ++ primitive "auto" - ++ pr_opt (pr_or_var int) n - ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db - ) - (* Context management *) | TacClear (true,[]) as t -> pr_atom0 t @@ -1251,16 +1180,13 @@ module Make | TacML (loc,s,l) -> pr_with_comments loc (pr.pr_extend 1 s l), lcall | TacAlias (loc,kn,l) -> - pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom + pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom ) in if prec_less prec inherited then strm else str"(" ++ strm ++ str")" and pr_tacarg = function - | TacDynamic (loc,t) -> - pr_with_comments loc - (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>") | MetaIdArg (loc,true,s) -> pr_with_comments loc (str "$" ++ str s) | MetaIdArg (loc,false,s) -> @@ -1307,7 +1233,7 @@ module Make pr_reference = pr_reference; pr_name = pr_lident; pr_generic = Genprint.generic_raw_print; - pr_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; + pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; } in make_pr_tac @@ -1321,7 +1247,7 @@ module Make let pr_pat_and_constr_expr pr ((c,_),_) = pr c - let rec pr_glob_tactic_level env n t = + let pr_glob_tactic_level env n t = let glob_printers = (strip_prod_binders_glob_constr) in @@ -1338,7 +1264,7 @@ module Make pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; pr_generic = Genprint.generic_glb_print; - pr_extend = pr_glob_extend + pr_extend = pr_glob_extend_rec (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); pr_alias = pr_glob_alias @@ -1374,13 +1300,13 @@ module Make pr_uconstr = pr_closed_glob_env env Evd.empty; pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_lconstr_env env Evd.empty; - pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); - pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env); - pr_constant = pr_and_short_name (pr_evaluable_reference_env env); + pr_pattern = pr_constr_pattern_env env Evd.empty; + pr_lpattern = pr_lconstr_pattern_env env Evd.empty; + pr_constant = pr_evaluable_reference_env env; pr_reference = pr_located pr_ltac_constant; pr_name = pr_id; pr_generic = Genprint.generic_top_print; - pr_extend = pr_extend + pr_extend = pr_extend_rec (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) (pr_glob_tactic_level env) pr_constr_pattern; pr_alias = pr_alias @@ -1395,6 +1321,39 @@ module Make in prtac n t + let pr_raw_generic env = pr_raw_generic_rec + pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference + + let pr_glb_generic env = pr_glb_generic_rec + (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) + (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) + + let pr_top_generic env = pr_top_generic_rec + (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) + (pr_glob_tactic_level env) pr_constr_pattern + + let pr_raw_extend env = pr_raw_extend_rec + pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr + + let pr_glob_extend env = pr_glob_extend_rec + (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) + (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) + + let check_val_type t arg = + let AnyArg t = t in +(* let t = Genarg.val_tag (Obj.magic t) in *) +(* let Val.Dyn (t', _) = arg in *) +(* match Genarg.Val.eq t t' with *) +(* | None -> false *) +(* | Some _ -> true *) + true (** FIXME *) + + let pr_alias pr lev key args = + pr_alias_gen check_val_type pr lev key args + + let pr_extend pr lev ml args = + pr_extend_gen check_val_type pr lev ml args + let pr_tactic env = pr_tactic_level env ltop end @@ -1431,17 +1390,26 @@ end) (** Registering *) +let run_delayed c = + Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma } + let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in let pr_string s = str "\"" ++ str s ++ str "\"" in + Genprint.register_print0 Constrarg.wit_int_or_var + (pr_or_var int) (pr_or_var int) int; Genprint.register_print0 Constrarg.wit_ref pr_reference (pr_or_var (pr_located pr_global)) pr_global; + Genprint.register_print0 Constrarg.wit_ident + pr_id pr_id pr_id; + Genprint.register_print0 Constrarg.wit_var + (pr_located pr_id) (pr_located pr_id) pr_id; Genprint.register_print0 Constrarg.wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_constr (snd (c (Global.env()) Evd.empty)))); + (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c)))); Genprint.register_print0 Constrarg.wit_clause_dft_concl (pr_clauses (Some true) pr_lident) @@ -1451,11 +1419,41 @@ let () = Genprint.register_print0 Constrarg.wit_sort pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 + Constrarg.wit_constr + Ppconstr.pr_constr_expr + (fun (c, _) -> Printer.pr_glob_constr c) + Printer.pr_constr + ; + Genprint.register_print0 Constrarg.wit_uconstr Ppconstr.pr_constr_expr (fun (c,_) -> Printer.pr_glob_constr c) Printer.pr_closed_glob ; + Genprint.register_print0 + Constrarg.wit_open_constr + Ppconstr.pr_constr_expr + (fun (c, _) -> Printer.pr_glob_constr c) + Printer.pr_constr + ; + Genprint.register_print0 Constrarg.wit_red_expr + (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) + (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) + (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern)); + Genprint.register_print0 Constrarg.wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + Genprint.register_print0 Constrarg.wit_bindings + (pr_bindings_no_with pr_constr_expr pr_lconstr_expr) + (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it))); + Genprint.register_print0 Constrarg.wit_constr_may_eval + (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr) + (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr) + (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr)) + pr_constr; + Genprint.register_print0 Constrarg.wit_constr_with_bindings + (pr_with_bindings pr_constr_expr pr_lconstr_expr) + (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it))); Genprint.register_print0 Stdarg.wit_int int int int; Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 313465614..2bc64509f 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -41,14 +41,14 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit -type grammar_terminals = string option list +type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list type pp_tactic = { - pptac_args : argument_type list; - pptac_prods : int * grammar_terminals; + pptac_level : int; + pptac_prods : grammar_terminals; } -val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit +val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit (** The default pretty-printers produce {!Pp.std_ppcmds} that are diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index b2323acba..c5ec6bb09 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -8,11 +8,9 @@ open Pp open Genarg -open Constrexpr open Tacexpr open Ppextend open Environ -open Pattern open Misctypes module type Pp = sig @@ -32,46 +30,24 @@ module type Pp = sig val pr_clauses : bool option -> ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds - val pr_raw_generic : - (constr_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> - (tolerability -> raw_tactic_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> - (Libnames.reference -> std_ppcmds) -> rlevel generic_argument -> - std_ppcmds - - val pr_glb_generic : - (glob_constr_and_expr -> Pp.std_ppcmds) -> - (glob_constr_and_expr -> Pp.std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - (glob_constr_pattern_and_expr -> std_ppcmds) -> - glevel generic_argument -> std_ppcmds - - val pr_top_generic : - (Term.constr -> std_ppcmds) -> - (Term.constr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - (Pattern.constr_pattern -> std_ppcmds) -> - tlevel generic_argument -> - std_ppcmds - - val pr_raw_extend: - (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> - (tolerability -> raw_tactic_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> int -> - ml_tactic_name -> raw_generic_argument list -> std_ppcmds - - val pr_glob_extend: - (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - (glob_constr_pattern_and_expr -> std_ppcmds) -> int -> - ml_tactic_name -> glob_generic_argument list -> std_ppcmds + + val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds + + val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds + + val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds + + val pr_raw_extend: env -> int -> + ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds + + val pr_glob_extend: env -> int -> + ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds val pr_extend : - (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - (constr_pattern -> std_ppcmds) -> int -> - ml_tactic_name -> typed_generic_argument list -> std_ppcmds + (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds + + val pr_alias : (Val.t -> std_ppcmds) -> + int -> Names.KerName.t -> Val.t list -> std_ppcmds val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 38add9d2c..ffec926a8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -79,13 +79,7 @@ module Make | VernacEndSubproof -> str"" | _ -> str"." - let pr_gen t = - pr_raw_generic - pr_constr_expr - pr_lconstr_expr - pr_raw_tactic_level - pr_constr_expr - pr_reference t + let pr_gen t = pr_raw_generic (Global.env ()) t let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() @@ -111,10 +105,9 @@ module Make else id let pr_production_item = function - | TacNonTerm (loc,nt,Some (p,sep)) -> + | TacNonTerm (loc, nt, (p, sep)) -> let pp_sep = if not (String.is_empty sep) then str "," ++ quote (str sep) else mt () in str nt ++ str"(" ++ pr_id (strip_meta p) ++ pp_sep ++ str")" - | TacNonTerm (loc,nt,None) -> str nt | TacTerm s -> qs s let pr_comment pr_c = function @@ -641,10 +634,10 @@ module Make else spc() ++ qs s ) - | VernacTime v -> - return (keyword "Time" ++ spc() ++ pr_vernac_list v) - | VernacRedirect (s, v) -> - return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v) + | VernacTime (_,v) -> + return (keyword "Time" ++ spc() ++ pr_vernac v) + | VernacRedirect (s, (_,v)) -> + return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac v) | VernacTimeout(n,v) -> return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v) | VernacFail v -> @@ -1037,13 +1030,18 @@ module Make return (keyword "Cd" ++ pr_opt qs s) (* Commands *) - | VernacDeclareTacticDefinition (rc,l) -> - let pr_tac_body (id, redef, body) = + | VernacDeclareTacticDefinition l -> + let pr_tac_body tacdef_body = + let id, redef, body = + match tacdef_body with + | TacticDefinition ((_,id), body) -> pr_id id, false, body + | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body + in let idl, body = match body with | Tacexpr.TacFun (idl,b) -> idl,b | _ -> [], body in - pr_ltac_ref id ++ + id ++ prlist (function None -> str " _" | Some id -> spc () ++ pr_id id) idl ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ @@ -1231,8 +1229,6 @@ module Make (keyword "Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l) ) - | VernacNop -> - mt() (* Toplevel control *) | VernacToplevelControl exn -> @@ -1269,11 +1265,6 @@ module Make | VernacEndSubproof -> return (str "}") - and pr_vernac_list l = - hov 2 (str"[" ++ spc() ++ - prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l - ++ spc() ++ str"]") - and pr_extend s cl = let pr_arg a = try pr_gen a diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fd51fd6b0..b7b1d67f0 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -35,7 +35,7 @@ type object_pr = { print_syntactic_def : kernel_name -> std_ppcmds; print_module : bool -> Names.module_path -> std_ppcmds; print_modtype : module_path -> std_ppcmds; - print_named_decl : Id.t * constr option * types -> std_ppcmds; + print_named_decl : Context.Named.Declaration.t -> 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 -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; @@ -132,7 +132,8 @@ let print_renames_list prefix l = let need_expansion impl ref = let typ = Global.type_of_global_unsafe ref in let ctx = prod_assum typ in - let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in + let open Context.Rel.Declaration in + let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in List.exists is_status_implicit lastimpl @@ -168,8 +169,10 @@ type opacity = | FullyOpaque | TransparentMaybeOpacified of Conv_oracle.level -let opacity env = function - | VarRef v when not (Option.is_empty (pi2 (Environ.lookup_named v env))) -> +let opacity env = + let open Context.Named.Declaration in + function + | VarRef v when is_local_def (Environ.lookup_named v env) -> Some(TransparentMaybeOpacified (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) | ConstRef cst -> @@ -440,11 +443,13 @@ let print_named_def name body typ = let print_named_assum name typ = str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" -let gallina_print_named_decl (id,c,typ) = - let s = Id.to_string id in - match c with - | Some body -> print_named_def s body typ - | None -> print_named_assum s typ +let gallina_print_named_decl = + let open Context.Named.Declaration in + function + | LocalAssum (id, typ) -> + print_named_assum (Id.to_string id) typ + | LocalDef (id, body, typ) -> + print_named_def (Id.to_string id) body typ let assumptions_for_print lna = List.fold_right (fun na env -> add_name na env) lna empty_names_context @@ -721,8 +726,8 @@ let print_any_name = function try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - let (_,c,typ) = Global.lookup_named str in - (print_named_decl (str,c,typ)) + let open Context.Named.Declaration in + str |> Global.lookup_named |> set_id str |> print_named_decl with Not_found -> errorlabstrm "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") @@ -750,8 +755,8 @@ let print_opaque_name qid = let ty = Universes.unsafe_type_of_global gr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - let (_,c,ty) = lookup_named id env in - print_named_decl (id,c,ty) + let open Context.Named.Declaration in + lookup_named id env |> set_id id |> print_named_decl let print_about_any loc k = match k with diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 6f3556adb..0eab15579 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -66,7 +66,7 @@ type object_pr = { print_syntactic_def : kernel_name -> std_ppcmds; print_module : bool -> Names.module_path -> std_ppcmds; print_modtype : module_path -> std_ppcmds; - print_named_decl : Id.t * constr option * types -> std_ppcmds; + print_named_decl : Context.Named.Declaration.t -> 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 -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; diff --git a/printing/printer.ml b/printing/printer.ml index 63755d7ff..b89005887 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -262,16 +262,19 @@ let pr_var_decl_skel pr_id env sigma (id,c,typ) = let ptyp = (str" : " ++ pt) in (pr_id id ++ hov 0 (pbody ++ ptyp)) -let pr_var_decl env sigma (id,c,typ) = - pr_var_decl_skel pr_id env sigma (id,c,typ) +let pr_var_decl env sigma d = + pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d) let pr_var_list_decl env sigma (l,c,typ) = hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ)) -let pr_rel_decl env sigma (na,c,typ) = - let pbody = match c with - | None -> mt () - | Some c -> +let pr_rel_decl env sigma decl = + let open Context.Rel.Declaration in + let na = get_name decl in + let typ = get_type decl in + let pbody = match decl with + | LocalAssum _ -> mt () + | LocalDef (_,c,_) -> (* Force evaluation *) let pb = pr_lconstr_env env sigma c in let pb = if isCast c then surround pb else pb in @@ -293,7 +296,7 @@ let pr_named_context_of env sigma = hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) let pr_named_context env sigma ne_context = - hv 0 (Context.fold_named_context + hv 0 (Context.Named.fold_outside (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d) ne_context ~init:(mt ())) @@ -306,7 +309,7 @@ let pr_rel_context_of env sigma = (* Prints an env (variables and de Bruijn). Separator: newline *) let pr_context_unlimited env sigma = let sign_env = - Context.fold_named_list_context + Context.NamedList.fold (fun d pps -> let pidt = pr_var_list_decl env sigma d in (pps ++ fnl () ++ pidt)) @@ -333,7 +336,7 @@ let pr_context_limit n env sigma = else let k = lgsign-n in let _,sign_env = - Context.fold_named_list_context + Context.NamedList.fold (fun d (i,pps) -> if i < k then (i+1, (pps ++str ".")) @@ -420,7 +423,8 @@ let pr_evgl_sign sigma evi = | None -> [], [] | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi) in - let ids = List.rev_map pi1 l in + let open Context.Named.Declaration in + let ids = List.rev_map get_id l in let warn = if List.is_empty ids then mt () else (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") @@ -639,8 +643,8 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ - (match Proof_global.Bullet.suggest p - with None -> str"" | Some s -> fnl () ++ str s) ++ + (let s = Proof_global.Bullet.suggest p in + if Pp.is_empty s then s else fnl () ++ s) ++ fnl () in pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals @@ -726,7 +730,7 @@ let prterm = pr_lconstr type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of constant * (Label.t * Context.rel_context * types) list + | Axiom of constant * (Label.t * Context.Rel.t * types) list | Opaque of constant (* An opaque constant. *) | Transparent of constant @@ -777,7 +781,7 @@ let pr_assumptionset env s = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in + let var = pr_id id ++ str " : " ++ pr_ltype typ in (var :: v, a, o, tr) | Axiom (kn,[]) -> let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in @@ -786,7 +790,7 @@ let pr_assumptionset env s = let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++ cut() ++ prlist_with_sep cut (fun (lbl, ctx, ty) -> - str " used in " ++ str (Names.Label.to_string lbl) ++ + str " used in " ++ pr_label lbl ++ str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty)) l in (v, ax :: a, o, tr) diff --git a/printing/printer.mli b/printing/printer.mli index 3424c41dc..70993bb72 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -10,7 +10,6 @@ open Pp open Names open Globnames open Term -open Context open Environ open Pattern open Evd @@ -109,13 +108,13 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds val pr_context_unlimited : env -> evar_map -> std_ppcmds val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds -val pr_var_decl : env -> evar_map -> named_declaration -> std_ppcmds -val pr_var_list_decl : env -> evar_map -> named_list_declaration -> std_ppcmds -val pr_rel_decl : env -> evar_map -> rel_declaration -> std_ppcmds +val pr_var_decl : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds +val pr_var_list_decl : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds +val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds -val pr_named_context : env -> evar_map -> named_context -> std_ppcmds +val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds val pr_named_context_of : env -> evar_map -> std_ppcmds -val pr_rel_context : env -> evar_map -> rel_context -> std_ppcmds +val pr_rel_context : env -> evar_map -> Context.Rel.t -> std_ppcmds val pr_rel_context_of : env -> evar_map -> std_ppcmds val pr_context_of : env -> evar_map -> std_ppcmds @@ -165,7 +164,7 @@ val prterm : constr -> std_ppcmds (** = pr_lconstr *) type context_object = | Variable of Id.t (** A section variable or a Let definition *) (** An axiom and the type it inhabits (if an axiom of the empty type) *) - | Axiom of constant * (Label.t * Context.rel_context * types) list + | Axiom of constant * (Label.t * Context.Rel.t * types) list | Opaque of constant (** An opaque constant. *) | Transparent of constant (** A transparent constant *) diff --git a/printing/printmod.ml b/printing/printmod.ml index c154b0aaa..9354cd28d 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -89,7 +89,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in - let args = extended_rel_list 0 params in + let args = Context.Rel.to_extended_list 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in @@ -143,7 +143,7 @@ let print_record env mind mib = in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in - let args = extended_rel_list 0 params in + let args = Context.Rel.to_extended_list 0 params in let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in let cstrtype = hnf_prod_applist env cstrtypes.(0) args in @@ -263,7 +263,7 @@ let nametab_register_modparam mbid mtb = List.iter (nametab_register_body mp dir) struc let print_body is_impl env mp (l,body) = - let name = str (Label.to_string l) in + let name = pr_label l in hov 2 (match body with | SFBmodule _ -> keyword "Module" ++ spc () ++ name | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name |