diff options
| -rw-r--r-- | parsing/g_basevernac.ml4 | 6 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 76 | ||||
| -rw-r--r-- | parsing/pptactic.mli | 11 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 | ||||
| -rw-r--r-- | translate/ppconstrnew.ml | 63 | ||||
| -rw-r--r-- | translate/ppconstrnew.mli | 1 | ||||
| -rw-r--r-- | translate/pptacticnew.ml | 29 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 44 | ||||
| -rw-r--r-- | translate/ppvernacnew.mli | 2 |
10 files changed, 167 insertions, 75 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 13d4a623b..581726891 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -281,8 +281,10 @@ GEXTEND Gram | IDENT "Distfix"; local = locality; a = entry_prec; n = natural; s = STRING; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (local,a,n,s,p,sc) - | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr -> - VernacNotation (local,"'"^s^"'",c,[],None,None) + | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr; + l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing] + | -> [] ] -> + VernacNotation (local,"'"^s^"'",c,l,None,None) | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ]; diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 9b11b58ac..7b1ccb511 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -113,19 +113,25 @@ let pr_quantified_hypothesis = function 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) + | 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) -let pr_bindings prc = function +let pr_bindings prc prlc = function | ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ prlist_with_sep spc prc l | ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - prlist_with_sep spc (pr_binding prc) l + prlist_with_sep spc + (fun b -> if Options.do_translate () then + str"(" ++ pr_binding prlc b ++ str")" + else + pr_binding prc b) + l | NoBindings -> mt () -let pr_with_bindings prc (c,bl) = prc c ++ hv 0 (pr_bindings prc bl) +let pr_with_bindings prc prlc (c,bl) = + prc c ++ hv 0 (pr_bindings prc prlc bl) let pr_with_names = function | [] -> mt () @@ -231,7 +237,7 @@ let pr_autoarg_usingTDB = function | true -> spc () ++ str "Using TDB" | false -> mt () -let rec pr_raw_generic prc prtac x = +let rec pr_raw_generic prc prlc prtac x = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false") | IntArgType -> pr_arg int (out_gen rawwit_int x) @@ -254,17 +260,17 @@ let rec pr_raw_generic prc prtac x = | CastedOpenConstrArgType -> pr_arg prc (out_gen rawwit_casted_open_constr x) | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings prc) (out_gen rawwit_constr_with_bindings x) + pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x) | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prtac x ++ a) x (mt())) + hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prlc prtac x ++ a) x (mt())) | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_raw_generic prc prtac x ++ a) x (mt())) - | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prtac) (mt()) x) + hov 0 (fold_list1 (fun x a -> pr_raw_generic prc prlc prtac x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac) (mt()) x) | PairArgType _ -> hov 0 (fold_pair - (fun a b -> pr_raw_generic prc prtac a ++ spc () ++ - pr_raw_generic prc prtac b) + (fun a b -> pr_raw_generic prc prlc prtac a ++ spc () ++ + pr_raw_generic prc prlc prtac b) x) | ExtraArgType s -> let tab = if Options.do_translate() then !genarg_pprule @@ -273,7 +279,7 @@ let rec pr_raw_generic prc prtac x = with Not_found -> str " [no printer for " ++ str s ++ str "] " -let rec pr_glob_generic prc prtac x = +let rec pr_glob_generic prc prlc prtac x = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen globwit_bool x then "true" else "false") | IntArgType -> pr_arg int (out_gen globwit_int x) @@ -296,17 +302,17 @@ let rec pr_glob_generic prc prtac x = | CastedOpenConstrArgType -> pr_arg prc (out_gen globwit_casted_open_constr x) | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings prc) (out_gen globwit_constr_with_bindings x) + pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x) | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_glob_generic prc prtac x ++ a) x (mt())) + hov 0 (fold_list0 (fun x a -> pr_glob_generic prc prlc prtac x ++ a) x (mt())) | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_glob_generic prc prtac x ++ a) x (mt())) - | OptArgType _ -> hov 0 (fold_opt (pr_glob_generic prc prtac) (mt()) x) + hov 0 (fold_list1 (fun x a -> pr_glob_generic prc prlc prtac x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_glob_generic prc prlc prtac) (mt()) x) | PairArgType _ -> hov 0 (fold_pair - (fun a b -> pr_glob_generic prc prtac a ++ spc () ++ - pr_glob_generic prc prtac b) + (fun a b -> pr_glob_generic prc prlc prtac a ++ spc () ++ + pr_glob_generic prc prlc prtac b) x) | ExtraArgType s -> let tab = if Options.do_translate() then !genarg_pprule @@ -316,7 +322,7 @@ let rec pr_glob_generic prc prtac x = open Closure -let rec pr_generic prc prtac x = +let rec pr_generic prc prlc prtac x = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen wit_bool x then "true" else "false") | IntArgType -> pr_arg int (out_gen wit_int x) @@ -337,17 +343,17 @@ let rec pr_generic prc prtac x = | CastedOpenConstrArgType -> pr_arg prc (snd (out_gen wit_casted_open_constr x)) | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings prc) (out_gen wit_constr_with_bindings x) + pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x) | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_generic prc prtac x ++ a) x (mt())) + hov 0 (fold_list0 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt())) | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_generic prc prtac x ++ a) x (mt())) - | OptArgType _ -> hov 0 (fold_opt (pr_generic prc prtac) (mt()) x) + hov 0 (fold_list1 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_generic prc prlc prtac) (mt()) x) | PairArgType _ -> hov 0 (fold_pair - (fun a b -> pr_generic prc prtac a ++ spc () ++ - pr_generic prc prtac b) + (fun a b -> pr_generic prc prlc prtac a ++ spc () ++ + pr_generic prc prlc prtac b) x) | ExtraArgType s -> let tab = if Options.do_translate() then !genarg_pprule @@ -373,8 +379,8 @@ let pr_extend_gen proj prgen s l = let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) = -let pr_bindings = pr_bindings pr_constr in -let pr_with_bindings = pr_with_bindings pr_constr in +let pr_bindings = pr_bindings pr_constr pr_constr in +let pr_with_bindings = pr_with_bindings pr_constr pr_constr in let pr_eliminator cb = str "using" ++ pr_arg (pr_with_bindings) cb in let pr_constrarg c = spc () ++ pr_constr c in let pr_intarg n = spc () ++ int n in @@ -395,8 +401,9 @@ let rec pr_atom0 = function (* Main tactic printer *) and pr_atom1 = function - | TacExtend (_,s,l) -> pr_extend pr_constr pr_tac s l - | TacAlias (_,s,l,_) -> pr_extend pr_constr pr_tac s (List.map snd l) + | TacExtend (_,s,l) -> pr_extend pr_constr pr_constr pr_tac s l + | TacAlias (_,s,l,_) -> + pr_extend pr_constr pr_constr pr_tac s (List.map snd l) (* Basic tactics *) | TacIntroPattern [] as t -> pr_atom0 t @@ -658,9 +665,12 @@ and prtac x = pr6 x in (prtac,pr0,pr_match_rule false pr_pat pr_tac) -let pr_raw_extend prc prtac = pr_extend_gen pi1 (pr_raw_generic prc prtac) -let pr_glob_extend prc prtac = pr_extend_gen pi2 (pr_glob_generic prc prtac) -let pr_extend prc prtac = pr_extend_gen pi3 (pr_generic prc prtac) +let pr_raw_extend prc prlc prtac = + pr_extend_gen pi1 (pr_raw_generic prc prlc prtac) +let pr_glob_extend prc prlc prtac = + pr_extend_gen pi2 (pr_glob_generic prc prlc prtac) +let pr_extend prc prlc prtac = + pr_extend_gen pi3 (pr_generic prc prlc prtac) let pr_and_constr_expr pr (c,_) = pr c diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 055b5adf2..728c8f8cd 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -59,25 +59,28 @@ val pr_glob_tactic : glob_tactic_expr -> std_ppcmds val pr_tactic : Proof_type.tactic_expr -> std_ppcmds val pr_glob_generic: - (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + (rawconstr_and_expr -> std_ppcmds) -> + (rawconstr_and_expr -> std_ppcmds) -> + (glob_tactic_expr -> std_ppcmds) -> glob_generic_argument -> std_ppcmds val pr_raw_generic : (constr_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> (constr_expr, raw_tactic_expr) generic_argument -> std_ppcmds val pr_raw_extend: - (constr_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> string -> raw_generic_argument list -> std_ppcmds val pr_glob_extend: - (rawconstr_and_expr -> std_ppcmds) -> + (rawconstr_and_expr -> std_ppcmds) -> (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> string -> glob_generic_argument list -> std_ppcmds val pr_extend : - (Term.constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> string -> closed_generic_argument list -> std_ppcmds diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 86cbe3654..7cc7a67e0 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -171,6 +171,12 @@ let parse_args is_ide = translate_file := true; parse rem + | "-translate2" :: rem -> make_translate true; p1:=false; parse rem + | "-ftranslate2" :: rem -> + make_translate true; p1:= false; + translate_file := true; + parse rem + | "-unsafe" :: f :: rem -> add_unsafe f; parse rem | "-unsafe" :: [] -> usage () diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 3285c3db0..1deed459d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -142,11 +142,11 @@ let rec vernac_com interpfun (loc,com) = | _ -> if !translate_file then msgnl - (pr_comments !comments ++ hov 0 (pr_vernac com) ++ sep_end) + (pr_comments !comments ++ hov 0 (pr_vernac com) ++ sep_end()) else msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pr_comments !comments ++ - pr_vernac com ++ sep_end))); + pr_vernac com ++ sep_end()))); Constrintern.set_temporary_implicits_in []; Constrextern.set_temporary_implicits_out []; comments := None; diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 96c65b54c..aa1c3af11 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -92,7 +92,7 @@ let pr_expl_args pr (a,expl) = let pr_opt_type pr = function | CHole _ -> mt () - | t -> cut () ++ str ":" ++ pr ltop t + | t -> cut () ++ str ":" ++ pr (if !Options.p1 then ltop else (latom,E)) t let pr_opt_type_spc pr = function | CHole _ -> mt () @@ -136,16 +136,64 @@ let pr_binder pr (nal,t) = prlist_with_sep sep (pr_located pr_name) nal ++ pr_opt_type pr t) *) +(* Option 1a *) let pr_oneb pr t na = match t with CHole _ -> pr_located pr_name na | _ -> hov 1 (str "(" ++ pr_located pr_name na ++ pr_opt_type pr t ++ str ")") -let pr_binder pr (nal,t) = +let pr_binder1 pr (nal,t) = hov 0 (prlist_with_sep sep (pr_oneb pr t) nal) -let pr_binders pr bl = - hv 0 (prlist_with_sep sep (pr_binder pr) bl) +let pr_binders1 pr bl = + hv 0 (prlist_with_sep sep (pr_binder1 pr) bl) + +(* Option 1b *) +let pr_binder1 pr (nal,t) = + match t with + CHole _ -> prlist_with_sep sep (pr_located pr_name) nal + | _ -> hov 1 + (str "(" ++ prlist_with_sep sep (pr_located pr_name) nal ++ str ":" ++ + pr ltop t ++ str ")") + +let pr_binders1 pr bl = + hv 0 (prlist_with_sep sep (pr_binder1 pr) bl) + +let pr_opt_type' pr = function + | CHole _ -> mt () + | t -> cut () ++ str ":" ++ pr (latom,E) t + +let pr_prod_binders1 pr = function +(* | [nal,t] -> hov 1 (prlist_with_sep sep (pr_located pr_name) nal ++ pr_opt_type' pr t)*) + | bl -> pr_binders1 pr bl + +(* Option 2 *) +let pr_let_binder pr x a = + hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++ brk(0,1) ++ pr ltop a) + +let pr_binder2 pr (nal,t) = + hov 0 ( + prlist_with_sep sep (pr_located pr_name) nal ++ + pr_opt_type pr t) + +let pr_binders2 pr bl = + hv 0 (prlist_with_sep sep (pr_binder2 pr) bl) + +let pr_prod_binder2 pr (nal,t) = + str "for " ++ hov 0 ( + prlist_with_sep sep (pr_located pr_name) nal ++ + pr_opt_type pr t) ++ str "," + +let pr_prod_binders2 pr bl = + hv 0 (prlist_with_sep sep (pr_prod_binder2 pr) bl) + +(**) +let pr_binders pr = (if !Options.p1 then pr_binders1 else pr_binders2) pr +let pr_prod_binders pr bl = + if !Options.p1 then + str "!" ++ pr_prod_binders1 pr bl ++ str "." + else + pr_prod_binders2 pr bl let pr_arg_binders pr bl = if bl = [] then mt() else (spc() ++ pr_binders pr bl) @@ -369,13 +417,14 @@ let rec pr inherited a = larrow | CProdN _ -> let (bl,a) = extract_prod_binders a in - hv 0 (str "!" ++ pr_binders pr bl ++ str "." ++ spc() ++ pr ltop a), + hv 0 (pr_prod_binders pr bl ++ spc() ++ pr ltop a), lprod | CLambdaN _ -> let (bl,a) = extract_lam_binders a in + let left, mid = str"fun" ++ spc(), " =>" in hov 2 ( - str "fun" ++ spc () ++ pr_binders pr bl ++ - str " =>" ++ spc() ++ pr ltop a), + left ++ pr_binders pr bl ++ + str mid ++ spc() ++ pr ltop a), llambda | CLetIn (_,x,a,b) -> let (bl,a) = extract_lam_binders a in diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli index 9cd75607b..5f7cc2c07 100644 --- a/translate/ppconstrnew.mli +++ b/translate/ppconstrnew.mli @@ -36,6 +36,7 @@ val prec_less : int -> int * Ppextend.parenRelation -> bool val pr_global : Idset.t -> global_reference -> std_ppcmds +val pr_tight_coma : unit -> std_ppcmds val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds val pr_name : name -> std_ppcmds val pr_qualid : qualid -> std_ppcmds diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index acff5e164..3ee8e0d76 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -39,28 +39,31 @@ let pr_quantified_hypothesis = function let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h +(* let pr_binding prc = function - | NamedHyp id, c -> hov 1 (pr_id id ++ str ":=" ++ cut () ++ prc c) - | AnonHyp n, c -> hov 1 (int n ++ str ":=" ++ cut () ++ prc c) + | NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) + | AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) +*) let pr_esubst prc l = let pr_qhyp = function - (_,AnonHyp n,c) -> int n ++ str":=" ++ prc c - | (_,NamedHyp id,c) -> pr_id id ++ str":=" ++ prc c in + (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" + | (_,NamedHyp id,c) -> str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")" + in prlist_with_sep spc pr_qhyp l -let pr_bindings_gen for_ex prc = function +let pr_bindings_gen for_ex prlc prc = function | ImplicitBindings l -> spc () ++ (if for_ex then mt() else str "with ") ++ hv 0 (prlist_with_sep spc prc l) | ExplicitBindings l -> spc () ++ (if for_ex then mt() else str "with ") ++ - hv 0 (pr_esubst prc l) + hv 0 (pr_esubst prlc l) | NoBindings -> mt () -let pr_bindings prc = pr_bindings_gen false prc +let pr_bindings prlc prc = pr_bindings_gen false prlc prc -let pr_with_bindings prc (c,bl) = prc c ++ pr_bindings prc bl +let pr_with_bindings prlc prc (c,bl) = prc c ++ pr_bindings prlc prc bl let pr_with_names = function | [] -> mt () @@ -175,9 +178,9 @@ open Closure let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) = -let pr_bindings env = pr_bindings (pr_constr env) in -let pr_ex_bindings env = pr_bindings_gen true (pr_constr env) in -let pr_with_bindings env = pr_with_bindings (pr_constr env) in +let pr_bindings env = pr_bindings (pr_lconstr env) (pr_constr env) in +let pr_ex_bindings env = pr_bindings_gen true (pr_lconstr env) (pr_constr env) in +let pr_with_bindings env = pr_with_bindings (pr_lconstr env) (pr_constr env) in let pr_eliminator env cb = str "using" ++ pr_arg (pr_with_bindings env) cb in let pr_constrarg env c = spc () ++ pr_constr env c in let pr_lconstrarg env c = spc () ++ pr_lconstr env c in @@ -201,9 +204,9 @@ let rec pr_atom0 env = function (* Main tactic printer *) and pr_atom1 env = function | TacExtend (_,s,l) -> - pr_extend (pr_constr env) (pr_tac env) s l + pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s l | TacAlias (_,s,l,_) -> - pr_extend (pr_constr env) (pr_tac env) s (List.map snd l) + pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s (List.map snd l) (* Basic tactics *) | TacIntroPattern [] as t -> pr_atom0 env t diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 1480c765c..161232a5f 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -34,6 +34,7 @@ let pr_raw_tactic_env l env t = let pr_gen env t = Pptactic.pr_raw_generic (Ppconstrnew.pr_constr_env env) + (Ppconstrnew.pr_lconstr_env env) (Pptacticnew.pr_raw_tactic env) t let pr_raw_tactic tac = @@ -241,20 +242,23 @@ let anonymize_binder na c = (Constrintern.interp_rawconstr Evd.empty (Global.env())) c)) else c +let surround_binder p = + if !Options.p1 then str"(" ++ p ++ str")" else p + let pr_binder pr_c ty na = match anonymize_binder (snd na) ty with CHole _ -> pr_located pr_name na | _ -> hov 1 - (str "(" ++ pr_located pr_name na ++ str ":" ++ cut() ++ - pr_c ty ++ str")") + (surround_binder (pr_located pr_name na ++ str":" ++ cut() ++ pr_c ty)) let pr_valdecls pr_c = function | LocalRawAssum (na,c) -> - prlist_with_sep spc (pr_binder pr_c c) na + let sep = if !Options.p1 then spc else pr_tight_coma in + prlist_with_sep sep (pr_binder pr_c c) na | LocalRawDef (na,c) -> - hov 1 (str"(" ++ pr_located pr_name na ++ str":=" ++ cut() ++ - pr_c c ++ str")") + hov 1 + (surround_binder (pr_located pr_name na ++ str":=" ++ cut() ++ pr_c c)) let pr_vbinders pr_c l = hv 0 (prlist_with_sep spc (pr_valdecls pr_c) l) @@ -280,12 +284,21 @@ let pr_assumption_token = function | (Decl_kinds.Global,Decl_kinds.Logical) -> str"Axiom" | (Decl_kinds.Global,Decl_kinds.Definitional) -> str"Parameter" -let pr_params pr_c (a,(b,c)) = - hov 2 (str"(" ++ pr_id b ++ spc() ++ - (if a then str":>" else str":") ++ - spc() ++ pr_c c ++ str")") +let pr_params pr_c (xl,(c,t)) = + hov 2 (surround_binder (prlist_with_sep sep pr_id xl ++ spc() ++ + (if c then str":>" else str":") ++ + spc() ++ pr_c t)) + +let rec factorize = function + | [] -> [] + | (c,(x,t))::l -> + match factorize l with + | (xl,t')::l' when t' = (c,t) & not !Options.p1 -> (x::xl,t')::l' + | l' -> ([x],(c,t))::l' -let pr_ne_params_list pr_c l = prlist_with_sep spc (pr_params pr_c) l +let pr_ne_params_list pr_c l = + let sep = if !Options.p1 then spc else pr_coma in + prlist_with_sep sep (pr_params pr_c) (factorize l) let pr_thm_token = function | Decl_kinds.Theorem -> str"Theorem" @@ -354,7 +367,7 @@ let pr_syntax_entry (p,rl) = str"level" ++ spc() ++ int p ++ str" :" ++ fnl() ++ prlist_with_sep (fun _ -> fnl() ++ str"| ") pr_syntax_rule rl -let sep_end = str";" +let sep_end () = if !Options.p1 then str";" else str"." (**************************************) (* Pretty printer for vernac commands *) @@ -411,7 +424,7 @@ let rec pr_vernac = function | VernacRestoreState s -> str"Restore State" ++ spc() ++ qs s (* Control *) - | VernacList l -> hov 2 (str"[" ++ spc() ++ prlist_with_sep (fun _ -> sep_end ++ fnl() ) (pr_located pr_vernac) l ++ spc() ++ str"]") + | VernacList l -> hov 2 (str"[" ++ spc() ++ prlist_with_sep (fun _ -> sep_end () ++ fnl() ) (pr_located pr_vernac) l ++ spc() ++ str"]") | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc() ++ str s | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v | VernacVar id -> pr_id id @@ -447,7 +460,12 @@ let rec pr_vernac = function let (s,l) = match mv8 with None -> (s,l) | Some ml -> ml in - hov 2( str"Notation" ++ spc() ++ pr_locality local ++ qs s ++ + let ps = + let n = String.length s in + if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' + then str (String.sub s 1 (n-2)) + else qs s in + hov 2( str"Notation" ++ spc() ++ pr_locality local ++ ps ++ str " :=" ++ pr_constrarg c ++ (match l with | [] -> mt() diff --git a/translate/ppvernacnew.mli b/translate/ppvernacnew.mli index 0e4bde50e..a444bb537 100644 --- a/translate/ppvernacnew.mli +++ b/translate/ppvernacnew.mli @@ -26,6 +26,6 @@ open Libnames open Ppextend open Topconstr -val sep_end : std_ppcmds +val sep_end : unit -> std_ppcmds val pr_vernac : vernac_expr -> std_ppcmds |