diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 146 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 15 | ||||
| -rw-r--r-- | printing/pputils.ml | 4 | ||||
| -rw-r--r-- | printing/pputils.mli | 1 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 86 | ||||
| -rw-r--r-- | printing/ppvernac.mli | 2 | ||||
| -rw-r--r-- | printing/prettyp.mli | 4 | ||||
| -rw-r--r-- | printing/printmod.mli | 2 |
8 files changed, 109 insertions, 151 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 1146b42a0..3c7095505 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -10,6 +10,7 @@ open CErrors open Util open Pp +open CAst open Names open Nameops open Libnames @@ -86,8 +87,8 @@ let tag_var = tag Tag.variable open Notation - let print_hunks n pr pr_binders (terms, termlists, binders) unps = - let env = ref terms and envlist = ref termlists and bll = ref binders in + let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps = + let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in let pop r = let a = List.hd !r in r := List.tl !r; a in let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in (* Warning: @@ -102,6 +103,11 @@ let tag_var = tag Tag.variable let pp2 = aux l in let pp1 = pr (n, prec) c in return unp pp1 pp2 + | UnpBinderMetaVar (_, prec) as unp :: l -> + let c = pop bl in + let pp2 = aux l in + let pp1 = pr_patt (n, prec) c in + return unp pp1 pp2 | UnpListMetaVar (_, prec, sl) as unp :: l -> let cl = pop envlist in let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in @@ -127,9 +133,9 @@ let tag_var = tag Tag.variable in aux unps - let pr_notation pr pr_binders s env = + let pr_notation pr pr_patt pr_binders s env = let unpl, level = find_notation_printing_rule s in - print_hunks level pr pr_binders env unpl, level + print_hunks level pr pr_patt pr_binders env unpl, level let pr_delimiters key strm = strm ++ str ("%"^key) @@ -146,7 +152,7 @@ let tag_var = tag Tag.variable if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n) else mt() - let pr_with_comments ?loc pp = pr_located (fun x -> x) (Loc.tag ?loc pp) + let pr_with_comments ?loc pp = pr_located (fun x -> x) (loc, pp) let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c) @@ -215,28 +221,28 @@ let tag_var = tag Tag.variable let pr_expl_args pr (a,expl) = match expl with | None -> pr (lapp,L) a - | Some (_,ExplByPos (n,_id)) -> + | Some {v=ExplByPos (n,_id)} -> anomaly (Pp.str "Explicitation by position not implemented.") - | Some (_,ExplByName id) -> + | Some {v=ExplByName id} -> str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" let pr_opt_type_spc pr = function | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t - let pr_lident (loc,id) = + 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 @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id + pr_located pr_id (Some (Loc.make_loc (b,b + String.length (Id.to_string id))), id) let pr_lname = function - | (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located Name.print lna + | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id) + | x -> pr_ast Name.print x let pr_or_var pr = function | ArgArg x -> pr x - | ArgVar (loc,s) -> pr_lident (loc,s) + | ArgVar id -> pr_lident id let pr_prim_token = function | Numeral (n,s) -> str (if s then n else "-"^n) @@ -263,8 +269,8 @@ let tag_var = tag Tag.variable in str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec - | CPatAlias (p, id) -> - pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las + | CPatAlias (p, na) -> + pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las | CPatCstr (c, None, []) -> pr_reference c, latom @@ -292,7 +298,7 @@ let tag_var = tag Tag.variable pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom | CPatNotation (s,(l,ll),args) -> - let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) in + let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) s (l,ll,[],[]) in (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not) ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not @@ -310,7 +316,7 @@ let tag_var = tag Tag.variable let pr_patt = pr_patt mt - let pr_eqn pr (loc,(pl,rhs)) = + let pr_eqn pr {loc;v=(pl,rhs)} = spc() ++ hov 4 (pr_with_comments ?loc (str "| " ++ @@ -318,12 +324,12 @@ let tag_var = tag Tag.variable ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) - let begin_of_binder l_bi = + let begin_of_binder l_bi = let b_loc l = fst (Option.cata Loc.unloc (0,0) l) in match l_bi with - | CLocalDef((loc,_),_,_) -> b_loc loc - | CLocalAssum((loc,_)::_,_,_) -> b_loc loc - | CLocalPattern(loc,(_,_)) -> b_loc loc + | CLocalDef({loc},_,_) -> b_loc loc + | CLocalAssum({loc}::_,_,_) -> b_loc loc + | CLocalPattern{loc} -> b_loc loc | _ -> assert false let begin_of_binders = function @@ -345,12 +351,12 @@ let tag_var = tag Tag.variable | Generalized (b, b', t') -> assert (match b with Implicit -> true | _ -> false); begin match nal with - |[loc,Anonymous] -> + |[{loc; v=Anonymous}] -> hov 1 (str"`" ++ (surround_impl b' ((if t' then str "!" else mt ()) ++ pr t))) - |[loc,Name id] -> + |[{loc; v=Name id}] -> hov 1 (str "`" ++ (surround_impl b' - (pr_lident (loc,id) ++ str " : " ++ + (pr_lident CAst.(make ?loc id) ++ str " : " ++ (if t' then str "!" else mt()) ++ pr t))) |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.") end @@ -370,7 +376,7 @@ let tag_var = tag Tag.variable surround (pr_lname na ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++ str" :=" ++ spc() ++ pr_c c) - | CLocalPattern (loc,(p,tyo)) -> + | CLocalPattern {CAst.loc; v = p,tyo} -> let p = pr_patt lsimplepatt p in match tyo with | None -> @@ -394,68 +400,6 @@ let tag_var = tag Tag.variable if is_open then pr_delimited_binders pr_com_at sep pr_c else pr_undelimited_binders sep pr_c - let rec extract_prod_binders = let open CAst in function - (* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_prod_binders c in - if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) - | { v = CProdN ([],c) } -> - extract_prod_binders c - | { loc; v = CProdN ([[_,Name id],bk,t], - { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) } - when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> - let bl,c = extract_prod_binders b in - CLocalPattern (loc, (p,None)) :: bl, c - | { loc; v = CProdN ((nal,bk,t)::bl,c) } -> - let bl,c = extract_prod_binders (CAst.make ?loc @@ CProdN(bl,c)) in - CLocalAssum (nal,bk,t) :: bl, c - | c -> [], c - - let rec extract_lam_binders ce = let open CAst in match ce.v with - (* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_lam_binders c in - if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) - | CLambdaN ([],c) -> - extract_lam_binders c - | CLambdaN ([[_,Name id],bk,t], - { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) - when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> - let bl,c = extract_lam_binders b in - CLocalPattern (ce.loc,(p,None)) :: bl, c - | CLambdaN ((nal,bk,t)::bl,c) -> - let bl,c = extract_lam_binders (CAst.make ?loc:ce.loc @@ CLambdaN(bl,c)) in - CLocalAssum (nal,bk,t) :: bl, c - | _ -> [], ce - - let split_lambda = CAst.with_loc_val (fun ?loc -> function - | CLambdaN ([[na],bk,t],c) -> (na,t,c) - | CLambdaN (([na],bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN(bl,c)) - | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN((nal,bk,t)::bl,c)) - | _ -> anomaly (Pp.str "ill-formed fixpoint body.") - ) - - let rename na na' t c = - match (na,na') with - | (_,Name id), (_,Name id') -> - (na',t,replace_vars_constr_expr (Id.Map.singleton id id') c) - | (_,Name id), (_,Anonymous) -> (na,t,c) - | _ -> (na',t,c) - - let split_product na' = CAst.with_loc_val (fun ?loc -> function - | CProdN ([[na],bk,t],c) -> rename na na' t c - | CProdN (([na],bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN(bl,c)) - | CProdN ((na::nal,bk,t)::bl,c) -> - rename na na' t (CAst.make ?loc @@ CProdN((nal,bk,t)::bl,c)) - | _ -> anomaly (Pp.str "ill-formed fixpoint body.") - ) - - let rec split_fix n typ def = - if Int.equal n 0 then ([],typ,def) - else - let (na,_,def) = split_lambda def in - let (na,t,typ) = split_product na typ in - let (bl,typ,def) = split_fix (n-1) typ def in - (CLocalAssum ([na],default_binder_kind,t)::bl,typ,def) - let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_body = if dangling_with_for then pr_dangling else pr in @@ -467,7 +411,7 @@ let tag_var = tag Tag.variable let pr_guard_annot pr_aux bl (n,ro) = match n with | None -> mt () - | Some (loc, id) -> + | Some {loc; v = id} -> match (ro : Constrexpr.recursion_order_expr) with | CStructRec -> let names_of_binder = function @@ -484,11 +428,11 @@ let tag_var = tag Tag.variable spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++ (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" - let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) = + let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) = let annot = pr_guard_annot (pr lsimpleconstr) bl ro in pr_recursive_decl pr prd dangling_with_for id bl annot t c - let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) = + let pr_cofixdecl pr prd dangling_with_for ({v=id},bl,t,c) = pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c let pr_recursive pr_decl id = function @@ -518,7 +462,7 @@ let tag_var = tag Tag.variable let pr_simple_return_type pr na po = (match na with - | Some (_,Name id) -> + | Some {v=Name id} -> spc () ++ keyword "as" ++ spc () ++ pr_id id | _ -> mt ()) ++ pr_case_type pr po @@ -549,7 +493,7 @@ let tag_var = tag Tag.variable let pr_fun_sep = spc () ++ str "=>" let pr_dangling_with_for sep pr inherited a = - match a.CAst.v with + match a.v with | (CFix (_,[_])|CCoFix(_,[_])) -> pr sep (latom,E) a | _ -> @@ -564,18 +508,17 @@ let tag_var = tag Tag.variable return ( hov 0 (keyword "fix" ++ spc () ++ pr_recursive - (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix), + (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v fix), lfix ) | CCoFix (id,cofix) -> return ( hov 0 (keyword "cofix" ++ spc () ++ pr_recursive - (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), + (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v cofix), lfix ) - | CProdN _ -> - let (bl,a) = extract_prod_binders a in + | CProdN (bl,a) -> return ( hov 0 ( hov 2 (pr_delimited_binders pr_forall spc @@ -583,8 +526,7 @@ let tag_var = tag Tag.variable str "," ++ pr spc ltop a), lprod ) - | CLambdaN _ -> - let (bl,a) = extract_lam_binders a in + | CLambdaN (bl,a) -> return ( hov 0 ( hov 2 (pr_delimited_binders pr_fun spc @@ -592,8 +534,8 @@ let tag_var = tag Tag.variable pr_fun_sep ++ pr spc ltop a), llambda ) - | CLetIn ((_,Name x), ({ CAst.v = CFix((_,x'),[_])} - | { CAst.v = CCoFix((_,x'),[_]) } as fx), t, b) + | CLetIn ({v=Name x}, ({ v = CFix({v=x'},[_])} + | { v = CCoFix({v=x'},[_]) } as fx), t, b) when Id.equal x x' -> return ( hv 0 ( @@ -649,7 +591,7 @@ let tag_var = tag Tag.variable hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), latom ) - | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([[p]],b))]) -> + | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ @@ -722,10 +664,10 @@ let tag_var = tag Tag.variable | CastCoerce -> str ":>"), lcast ) - | CNotation ("( _ )",([t],[],[])) -> + | CNotation ("( _ )",([t],[],[],[])) -> return (pr (fun()->str"(") (max_int,L) t ++ str")", latom) | CNotation (s,env) -> - pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env + pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env | CGeneralization (bk,ak,c) -> return (pr_generalization bk ak (pr mt ltop c), latom) | CPrim p -> diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 1320cce9b..cedeed5f3 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -10,29 +10,20 @@ objects and their subcomponents. *) (** The default pretty-printers produce pretty-printing commands ({!Pp.t}). *) -open Loc open Libnames open Constrexpr open Names open Misctypes open Notation_term -val extract_lam_binders : - constr_expr -> local_binder_expr list * constr_expr -val extract_prod_binders : - constr_expr -> local_binder_expr list * constr_expr -val split_fix : - int -> constr_expr -> constr_expr -> - local_binder_expr list * constr_expr * constr_expr - val prec_less : precedence -> tolerability -> bool val pr_tight_coma : unit -> Pp.t val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t -val pr_lident : Id.t located -> Pp.t -val pr_lname : Name.t located -> 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 @@ -52,7 +43,7 @@ val pr_glob_level : glob_level -> Pp.t val pr_glob_sort : glob_sort -> Pp.t val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list -> - ('a * Names.Id.t) option * recursion_order_expr -> + lident option * recursion_order_expr -> Pp.t val pr_record_body : (reference * constr_expr) list -> Pp.t diff --git a/printing/pputils.ml b/printing/pputils.ml index a544b4762..e779fc5fc 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -24,9 +24,11 @@ let pr_located pr (loc, x) = before ++ x ++ after | _ -> pr x +let pr_ast pr { CAst.loc; v } = pr_located pr (loc, v) + let pr_or_var pr = function | ArgArg x -> pr x - | ArgVar (_,s) -> Names.Id.print s + | ArgVar {CAst.v=s} -> Names.Id.print s let pr_with_occurrences pr keyword (occs,c) = match occs with diff --git a/printing/pputils.mli b/printing/pputils.mli index f7f586b77..ec5c32fc4 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -12,6 +12,7 @@ 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 diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 950246c53..83cac7ddd 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -11,6 +11,8 @@ open Names open CErrors open Util +open CAst + open Extend open Vernacexpr open Pputils @@ -59,7 +61,7 @@ open Decl_kinds let pr_ident_decl (lid, l) = pr_lident lid ++ pr_universe_decl l - + let string_of_fqid fqid = String.concat "." (List.map Id.to_string fqid) @@ -93,16 +95,35 @@ open Decl_kinds let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() - let pr_set_entry_type = function + let pr_at_level = function + | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n + | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" + + let pr_constr_as_binder_kind = function + | AsIdent -> keyword "as ident" + | AsIdentOrPattern -> keyword "as pattern" + | AsStrictPattern -> keyword "as strict pattern" + + let pr_strict b = if b then str "strict " else mt () + + let pr_set_entry_type pr = function | ETName -> str"ident" | ETReference -> str"global" - | ETPattern -> str"pattern" - | ETConstr _ -> str"constr" + | ETPattern (b,None) -> pr_strict b ++ str"pattern" + | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n) + | ETConstr lev -> str"constr" ++ pr lev | ETOther (_,e) -> str e + | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk | ETBigint -> str "bigint" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" - | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" + + let pr_at_level_opt = function + | None -> mt () + | Some n -> spc () ++ pr_at_level n + + let pr_set_simple_entry_type = + pr_set_entry_type pr_at_level_opt let pr_comment pr_c = function | CommentConstr c -> pr_c c @@ -217,7 +238,7 @@ open Decl_kinds keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ pr_located pr_qualid qid - let rec pr_module_ast leading_space pr_c = let open CAst in function + let rec pr_module_ast leading_space pr_c = function | { loc ; v = CMident qid } -> if leading_space then spc () ++ pr_located pr_qualid (loc, qid) @@ -268,10 +289,10 @@ open Decl_kinds prlist_strict (pr_module_vardecls pr_c) l let pr_type_option pr_c = function - | { CAst.v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() + | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() | _ as c -> brk(0,2) ++ str" :" ++ pr_c c - let pr_decl_notation prc ((loc,ntn),c,scopt) = + let pr_decl_notation prc ({loc; v=ntn},c,scopt) = fnl () ++ keyword "where " ++ qs ntn ++ str " := " ++ Flags.without_option Flags.beautify prc c ++ pr_opt (fun sc -> str ": " ++ str sc) scopt @@ -310,7 +331,7 @@ open Decl_kinds let begin_of_inductive = function | [] -> 0 - | (_,((loc,_),_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc + | (_,({loc},_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc let pr_class_rawexpr = function | FunClass -> keyword "Funclass" @@ -360,22 +381,21 @@ open Decl_kinds let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k) let pr_syntax_modifier = function - | SetItemLevel (l,NextLevel) -> - prlist_with_sep sep_v2 str l ++ - spc() ++ keyword "at next level" - | SetItemLevel (l,NumLevel n) -> + | SetItemLevel (l,n) -> + prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n + | SetItemLevelAsBinder (l,bk,n) -> prlist_with_sep sep_v2 str l ++ - spc() ++ keyword "at level" ++ spc() ++ int n - | SetLevel n -> keyword "at level" ++ spc() ++ int n + spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk + | SetLevel n -> pr_at_level (NumLevel n) | SetAssoc LeftA -> keyword "left associativity" | SetAssoc RightA -> keyword "right associativity" | SetAssoc NonA -> keyword "no associativity" - | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ + | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ | SetOnlyPrinting -> keyword "only printing" | SetOnlyParsing -> keyword "only parsing" | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") - | SetFormat("text",s) -> keyword "format " ++ pr_located qs s - | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s + | SetFormat("text",s) -> keyword "format " ++ pr_ast qs s + | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s let pr_syntax_modifiers = function | [] -> mt() @@ -519,7 +539,7 @@ open Decl_kinds let rec aux = function | SsEmpty -> "()" | SsType -> "(Type)" - | SsSingl (_,id) -> "("^Id.to_string id^")" + | SsSingl { v=id } -> "("^Id.to_string id^")" | SsCompl e -> "-" ^ aux e^"" | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" @@ -643,7 +663,7 @@ open Decl_kinds ++ spc() ++ pr_smart_global q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" ) - | VernacInfix (((_,s),mv),q,sn) -> (* A Verifier *) + | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *) return ( hov 0 (hov 0 (keyword "Infix " ++ qs s ++ str " :=" ++ pr_constrarg q) ++ @@ -652,7 +672,7 @@ open Decl_kinds | None -> mt() | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) ) - | VernacNotation (c,((_,s),l),opt) -> + | VernacNotation (c,({v=s},l),opt) -> return ( hov 2 (keyword "Notation" ++ spc() ++ qs s ++ str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++ @@ -662,7 +682,7 @@ open Decl_kinds ) | VernacSyntaxExtension (_, (s, l)) -> return ( - keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++ + keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++ pr_syntax_modifiers l ) | VernacNotationAddFormat(s,k,v) -> @@ -674,7 +694,7 @@ open Decl_kinds | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *) let pr_def_token dk = keyword ( - if Name.is_anonymous (snd (fst id)) + if Name.is_anonymous (fst id).v then "Goal" else Kindops.string_of_definition_object_kind dk) in @@ -693,7 +713,7 @@ open Decl_kinds in (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) | ProveBody (bl,t) -> - let typ u = if snd (fst id) = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in + let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in let (binds,typ,c) = pr_def_body b in return ( @@ -871,16 +891,16 @@ open Decl_kinds return ( hov 1 ( (if abst then keyword "Declare" ++ spc () else mt ()) ++ - keyword "Instance" ++ - (match instid with - | (loc, Name id), l -> spc () ++ pr_ident_decl ((loc, id),l) ++ spc () - | (_, Anonymous), _ -> mt ()) ++ - pr_and_type_binders_arg sup ++ + keyword "Instance" ++ + (match instid with + | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc () + | { v = Anonymous }, _ -> mt ()) ++ + pr_and_type_binders_arg sup ++ str":" ++ spc () ++ (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with - | Some (true, { CAst.v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" + | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" | Some (true,_) -> assert false | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) @@ -1013,7 +1033,7 @@ open Decl_kinds hov 2 ( keyword "Arguments" ++ spc() ++ pr_smart_global q ++ - let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in + let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in let pr_if b x = if b then x else str "" in let pr_br imp x = match imp with | Vernacexpr.Implicit -> str "[" ++ x ++ str "]" @@ -1219,9 +1239,9 @@ let pr_vernac_flag = (fun f a -> pr_vernac_flag f ++ spc() ++ a) f (pr_vernac_expr v' ++ sep_end v') - | VernacTime (_,(_,v)) -> + | VernacTime (_,{v}) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) - | VernacRedirect (s, (_,v)) -> + | VernacRedirect (s, {v}) -> return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v) | VernacTimeout(n,v) -> return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v) diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index 34b4fb97f..603be6308 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -9,6 +9,8 @@ (** This module implements pretty-printers for vernac_expr syntactic objects and their subcomponents. *) +val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t + (** Prints a fixpoint body *) val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t diff --git a/printing/prettyp.mli b/printing/prettyp.mli index fd7f1f92b..c1d8f1d37 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -33,10 +33,10 @@ val print_eval : Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t val print_name : env -> Evd.evar_map -> reference or_by_notation -> - Vernacexpr.univ_name_list option -> Pp.t + Universes.univ_name_list option -> Pp.t val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t val print_about : env -> Evd.evar_map -> reference or_by_notation -> - Vernacexpr.univ_name_list option -> Pp.t + Universes.univ_name_list option -> Pp.t val print_impargs : reference or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) diff --git a/printing/printmod.mli b/printing/printmod.mli index 97ed063fe..4f15dd393 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -13,6 +13,6 @@ val printable_body : DirPath.t -> bool val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> - Vernacexpr.univ_name_list option -> Pp.t + Universes.univ_name_list option -> Pp.t val print_module : bool -> ModPath.t -> Pp.t val print_modtype : ModPath.t -> Pp.t |