diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 499 |
1 files changed, 194 insertions, 305 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index aa94fb7b..4c5d955c 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -1,38 +1,55 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) open CErrors open Util open Pp +open CAst open Names open Nameops open Libnames open Pputils open Ppextend +open Notation_term open Constrexpr open Constrexpr_ops open Decl_kinds open Misctypes (*i*) -module Make (Taggers : sig - val tag_keyword : std_ppcmds -> std_ppcmds - val tag_evar : std_ppcmds -> std_ppcmds - val tag_type : std_ppcmds -> std_ppcmds - val tag_path : std_ppcmds -> std_ppcmds - val tag_ref : std_ppcmds -> std_ppcmds - val tag_var : std_ppcmds -> std_ppcmds - val tag_constr_expr : constr_expr -> std_ppcmds -> std_ppcmds - val tag_unparsing : unparsing -> std_ppcmds -> std_ppcmds -end) = struct +module Tag = +struct + let keyword = "constr.keyword" + let evar = "constr.evar" + let univ = "constr.type" + let notation = "constr.notation" + let variable = "constr.variable" + let reference = "constr.reference" + let path = "constr.path" + +end + +let do_not_tag _ x = x +let tag t s = Pp.tag t s +let tag_keyword = tag Tag.keyword +let tag_evar = tag Tag.evar +let tag_type = tag Tag.univ +let tag_unparsing = function +| UnpTerminal s -> tag Tag.notation +| _ -> do_not_tag () +let tag_constr_expr = do_not_tag +let tag_path = tag Tag.path +let tag_ref = tag Tag.reference +let tag_var = tag Tag.variable - open Taggers let keyword s = tag_keyword (str s) let sep_v = fun _ -> str"," ++ spc() @@ -67,13 +84,13 @@ end) = struct | Any -> true let prec_of_prim_token = function - | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint + | Numeral (_,b) -> if b then lposint else lnegint | String _ -> latom 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: @@ -88,6 +105,11 @@ end) = struct 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 @@ -103,7 +125,7 @@ end) = struct let pp1 = str s in return unp pp1 pp2 | UnpBox (b,sub) as unp :: l -> - let pp1 = ppcmd_of_box b (aux sub) in + let pp1 = ppcmd_of_box b (aux (List.map snd sub)) in let pp2 = aux l in return unp pp1 pp2 | UnpCut cut as unp :: l -> @@ -113,9 +135,9 @@ end) = struct 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) @@ -129,17 +151,22 @@ end) = struct str "`" ++ str hd ++ c ++ str tl let pr_com_at n = - if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n) + if !Flags.beautify && not (Int.equal n 0) then comment (Pputils.extract_comments n) else mt() - let pr_with_comments loc pp = pr_located (fun x -> x) (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 (constr_loc c) (sep() ++ f c) + let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c) + + let pr_univ_expr = function + | Some (x,n) -> + pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) + | None -> str"_" let pr_univ l = match l with - | [_,x] -> str x - | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> str (snd x)) l ++ str")" + | [x] -> pr_univ_expr x + | l -> str"max(" ++ prlist_with_sep (fun () -> str",") pr_univ_expr l ++ str")" let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" @@ -152,22 +179,23 @@ end) = struct let pr_glob_level = function | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") - | GType None -> tag_type (str "Type") - | GType (Some (_, u)) -> tag_type (str u) + | GType UUnknown -> tag_type (str "Type") + | GType UAnonymous -> tag_type (str "_") + | GType (UNamed u) -> tag_type (pr_reference u) let pr_qualid sp = let (sl, id) = repr_qualid sp in - let id = tag_ref (pr_id id) in + let id = tag_ref (Id.print id) in let sl = match List.rev (DirPath.repr sl) with | [] -> mt () | sl -> - let pr dir = tag_path (pr_id dir) ++ str "." in + let pr dir = tag_path (Id.print dir) ++ str "." in prlist pr sl in sl ++ id - let pr_id = pr_id - let pr_name = pr_name + let pr_id = Id.print + let pr_name = Name.print let pr_qualid = pr_qualid let pr_patvar = pr_id @@ -178,15 +206,16 @@ end) = struct tag_type (str "Set") | GType u -> (match u with - | Some (_,u) -> str u - | None -> tag_type (str "Type")) + | UNamed u -> pr_reference u + | UAnonymous -> tag_type (str "Type") + | UUnknown -> tag_type (str "_")) let pr_universe_instance l = pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l - let pr_reference = function - | Qualid (_, qid) -> pr_qualid qid - | Ident (_, id) -> tag_var (pr_id id) + let pr_reference = CAst.with_val (function + | Qualid qid -> pr_qualid qid + | Ident id -> tag_var (pr_id id)) let pr_cref ref us = pr_reference ref ++ pr_universe_instance us @@ -194,36 +223,31 @@ end) = struct let pr_expl_args pr (a,expl) = match expl with | None -> pr (lapp,L) a - | Some (_,ExplByPos (n,_id)) -> - anomaly (Pp.str "Explicitation by position not implemented") - | Some (_,ExplByName id) -> + | Some {v=ExplByPos (n,_id)} -> + anomaly (Pp.str "Explicitation by position not implemented.") + | Some {v=ExplByName id} -> str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" - let pr_opt_type pr = function - | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () - | t -> cut () ++ str ":" ++ pr t - let pr_opt_type_spc pr = function - | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () + | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t - let pr_lident (loc,id) = - if not (Loc.is_ghost loc) then - let (b,_) = Loc.unloc loc in - pr_located pr_id (Loc.make_loc (b,b + String.length (Id.to_string id)), id) - else - pr_id 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 (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 pr_name 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 -> str (Bigint.to_string n) + | Numeral (n,s) -> str (if s then n else "-"^n) | String s -> qs s let pr_evar pr id l = @@ -240,73 +264,74 @@ end) = struct let lpatrec = 0 let rec pr_patt sep inh p = - let (strm,prec) = match p with - | CPatRecord (_, l) -> + let (strm,prec) = match CAst.(p.v) with + | CPatRecord l -> let pp (c, p) = pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p 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, []) -> + | CPatCstr (c, None, []) -> pr_reference c, latom - | CPatCstr (_, c, None, args) -> + | CPatCstr (c, None, args) -> pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp - | CPatCstr (_, c, Some args, []) -> + | CPatCstr (c, Some args, []) -> str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp - | CPatCstr (_, c, Some expl_args, extra_args) -> + | CPatCstr (c, Some expl_args, extra_args) -> surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args) ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp - | CPatAtom (_, None) -> + | CPatAtom (None) -> str "_", latom - | CPatAtom (_,Some r) -> + | CPatAtom (Some r) -> pr_reference r, latom - | CPatOr (_,pl) -> - hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator + | CPatOr pl -> + hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator - | CPatNotation (_,"( _ )",([p],[]),[]) -> + | CPatNotation ("( _ )",([p],[]),[]) -> 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 + | CPatNotation (s,(l,ll),args) -> + 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 - | CPatPrim (_,p) -> + | CPatPrim p -> pr_prim_token p, latom - | CPatDelimiters (_,k,p) -> + | CPatDelimiters (k,p) -> pr_delimiters k (pr_patt mt lsimplepatt p), 1 | CPatCast _ -> assert false in - let loc = cases_pattern_expr_loc p in - pr_with_comments loc + let loc = p.CAst.loc in + pr_with_comments ?loc (sep() ++ if prec_less prec inh then strm else surround strm) let pr_patt = pr_patt mt - let pr_eqn pr (loc,pl,rhs) = - let pl = List.map snd pl in + let pr_eqn pr {loc;v=(pl,rhs)} = spc() ++ hov 4 - (pr_with_comments loc + (pr_with_comments ?loc (str "| " ++ - hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl + hov 0 (prlist_with_sep pr_spcbar (prlist_with_sep sep_v (pr_patt ltop)) pl ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) - let begin_of_binder = function - LocalRawDef((loc,_),_) -> fst (Loc.unloc loc) - | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) - | LocalPattern(loc,_,_) -> fst (Loc.unloc loc) + 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 | _ -> assert false let begin_of_binders = function @@ -328,18 +353,18 @@ end) = struct | 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 | Default b -> match t with - | CHole (_,_,Misctypes.IntroAnonymous,_) -> + | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> let s = prlist_with_sep spc pr_lname nal in hov 1 (surround_implicit b s) | _ -> @@ -347,15 +372,13 @@ end) = struct hov 1 (if many then surround_impl b s else surround_implicit b s) let pr_binder_among_many pr_c = function - | LocalRawAssum (nal,k,t) -> + | CLocalAssum (nal,k,t) -> pr_binder true pr_c (nal,k,t) - | LocalRawDef (na,c) -> - let c,topt = match c with - | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t - | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in - surround (pr_lname na ++ pr_opt_type pr_c topt ++ - str":=" ++ cut() ++ pr_c c) - | LocalPattern (loc,p,tyo) -> + | CLocalDef (na,c,topt) -> + surround (pr_lname na ++ + pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++ + str" :=" ++ spc() ++ pr_c c) + | CLocalPattern {CAst.loc; v = p,tyo} -> let p = pr_patt lsimplepatt p in match tyo with | None -> @@ -369,80 +392,20 @@ end) = struct let pr_delimited_binders kw sep pr_c bl = let n = begin_of_binders bl in match bl with - | [LocalRawAssum (nal,k,t)] -> + | [CLocalAssum (nal,k,t)] -> kw n ++ pr_binder false pr_c (nal,k,t) - | (LocalRawAssum _ | LocalPattern _) :: _ as bdl -> + | (CLocalAssum _ | CLocalPattern _ | CLocalDef _) :: _ as bdl -> kw n ++ pr_undelimited_binders sep pr_c bdl - | _ -> assert false + | [] -> assert false let pr_binders_gen pr_c sep is_open = 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 = function - (* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_prod_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) - | CProdN (loc,[],c) -> - extract_prod_binders c - | CProdN (loc,[[_,Name id],bk,t], - CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) - when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> - let bl,c = extract_prod_binders b in - LocalPattern (loc,p,None) :: bl, c - | CProdN (loc,(nal,bk,t)::bl,c) -> - let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in - LocalRawAssum (nal,bk,t) :: bl, c - | c -> [], c - - let rec extract_lam_binders = function - (* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_lam_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) - | CLambdaN (loc,[],c) -> - extract_lam_binders c - | CLambdaN (loc,[[_,Name id],bk,t], - CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) - when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> - let bl,c = extract_lam_binders b in - LocalPattern (loc,p,None) :: bl, c - | CLambdaN (loc,(nal,bk,t)::bl,c) -> - let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in - LocalRawAssum (nal,bk,t) :: bl, c - | c -> [], c - - let split_lambda = function - | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c) - | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c)) - | CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(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,Topconstr.replace_vars_constr_expr (Id.Map.singleton id id') c) - | (_,Name id), (_,Anonymous) -> (na,t,c) - | _ -> (na',t,c) - - let split_product na' = function - | CProdN (loc,[[na],bk,t],c) -> rename na na' t c - | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c)) - | CProdN (loc,(na::nal,bk,t)::bl,c) -> - rename na na' t (CProdN(loc,(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 - (LocalRawAssum ([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 - pr_id id ++ str" " ++ + pr_id id ++ (if bl = [] then mt () else str" ") ++ hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++ pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c @@ -450,13 +413,13 @@ end) = struct 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 - | LocalRawAssum (nal,_,_) -> nal - | LocalRawDef (_,_) -> [] - | LocalPattern _ -> assert false + | CLocalAssum (nal,_,_) -> nal + | CLocalDef (_,_,_) -> [] + | CLocalPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" @@ -467,15 +430,15 @@ end) = struct 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 - | [] -> anomaly (Pp.str "(co)fixpoint with no definition") + | [] -> anomaly (Pp.str "(co)fixpoint with no definition.") | [d1] -> pr_decl false d1 | dl -> prlist_with_sep (fun () -> fnl() ++ keyword "with" ++ spc ()) @@ -495,13 +458,13 @@ end) = struct let pr_case_type pr po = match po with - | None | Some (CHole (_,_,Misctypes.IntroAnonymous,_)) -> mt() + | None | Some { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt() | Some p -> spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p) 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 @@ -532,33 +495,32 @@ end) = struct let pr_fun_sep = spc () ++ str "=>" let pr_dangling_with_for sep pr inherited a = - match a with - | (CFix (_,_,[_])|CCoFix(_,_,[_])) -> + match a.v with + | (CFix (_,[_])|CCoFix(_,[_])) -> pr sep (latom,E) a | _ -> pr sep inherited a let pr pr sep inherited a = let return (cmds, prec) = (tag_constr_expr a cmds, prec) in - let (strm, prec) = match a with + let (strm, prec) = match CAst.(a.v) with | CRef (r, us) -> return (pr_cref r us, latom) - | CFix (_,id,fix) -> + | CFix (id,fix) -> 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) -> + | 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 @@ -566,8 +528,7 @@ end) = struct 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 @@ -575,7 +536,8 @@ end) = struct pr_fun_sep ++ pr spc ltop a), llambda ) - | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), 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 ( @@ -585,16 +547,17 @@ end) = struct pr spc ltop b), lletin ) - | CLetIn (_,x,a,b) -> + | CLetIn (x,a,t,b) -> return ( hv 0 ( - hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :=" - ++ pr spc ltop a ++ spc () + hov 2 (keyword "let" ++ spc () ++ pr_lname x + ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr mt ltop t) t + ++ str " :=" ++ pr spc ltop a ++ spc () ++ keyword "in") ++ pr spc ltop b), lletin ) - | CAppExpl (_,(Some i,f,us),l) -> + | CAppExpl ((Some i,f,us),l) -> let l1,l2 = List.chop i l in let c,l1 = List.sep_last l1 in let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in @@ -602,16 +565,16 @@ end) = struct return (p ++ prlist (pr spc (lapp,L)) l2, lapp) else return (p, lproj) - | CAppExpl (_,(None,Ident (_,var),us),[t]) - | CApp (_,(_,CRef(Ident(_,var),us)),[t,None]) + | CAppExpl ((None,{v=Ident var},us),[t]) + | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None]) when Id.equal var Notation_ops.ldots_var -> return ( hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg ) - | CAppExpl (_,(None,f,us),l) -> + | CAppExpl ((None,f,us),l) -> return (pr_appexpl (pr mt) (f,us) l, lapp) - | CApp (_,(Some i,f),l) -> + | CApp ((Some i,f),l) -> let l1,l2 = List.chop i l in let c,l1 = List.sep_last l1 in assert (Option.is_empty (snd c)); @@ -623,14 +586,14 @@ end) = struct ) else return (p, lproj) - | CApp (_,(None,a),l) -> + | CApp ((None,a),l) -> return (pr_app (pr mt) a l, lapp) - | CRecord (_,l) -> + | CRecord l -> return ( hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), latom ) - | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) -> + | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ @@ -641,7 +604,7 @@ end) = struct spc () ++ keyword "in" ++ pr spc ltop b)), lletpattern ) - | CCases(_,_,rtntypopt,c,eqns) -> + | CCases(_,rtntypopt,c,eqns) -> return ( v 0 (hv 0 (keyword "match" ++ brk (1,2) ++ @@ -654,7 +617,7 @@ end) = struct ++ keyword "end"), latom ) - | CLetTuple (_,nal,(na,po),c,b) -> + | CLetTuple (nal,(na,po),c,b) -> return ( hv 0 ( hov 2 (keyword "let" ++ spc () ++ @@ -667,7 +630,7 @@ end) = struct pr spc ltop b), lletin ) - | CIf (_,c,(na,po),b1,b2) -> + | CIf (c,(na,po),b1,b2) -> (* On force les parenthèses autour d'un "if" sous-terme (même si le parsing est lui plus tolérant) *) return ( @@ -681,19 +644,19 @@ end) = struct lif ) - | CHole (_,_,Misctypes.IntroIdentifier id,_) -> + | CHole (_,Misctypes.IntroIdentifier id,_) -> return (str "?[" ++ pr_id id ++ str "]", latom) - | CHole (_,_,Misctypes.IntroFresh id,_) -> + | CHole (_,Misctypes.IntroFresh id,_) -> return (str "?[?" ++ pr_id id ++ str "]", latom) - | CHole (_,_,_,_) -> + | CHole (_,_,_) -> return (str "_", latom) - | CEvar (_,n,l) -> + | CEvar (n,l) -> return (pr_evar (pr mt) n l, latom) - | CPatVar (_,p) -> - return (str "?" ++ pr_patvar p, latom) - | CSort (_,s) -> + | CPatVar p -> + return (str "@?" ++ pr_patvar p, latom) + | CSort s -> return (pr_glob_sort s, latom) - | CCast (_,a,b) -> + | CCast (a,b) -> return ( hv 0 (pr mt (lcast,L) a ++ spc () ++ match b with @@ -703,56 +666,65 @@ end) = struct | 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 - | CGeneralization (_,bk,ak,c) -> + | CNotation (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) -> + | CPrim p -> return (pr_prim_token p, prec_of_prim_token p) - | CDelimiters (_,sc,a) -> + | CDelimiters (sc,a) -> return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim) in let loc = constr_loc a in - pr_with_comments loc + pr_with_comments ?loc (sep() ++ if prec_less prec inherited then strm else surround strm) type term_pr = { - pr_constr_expr : constr_expr -> std_ppcmds; - pr_lconstr_expr : constr_expr -> std_ppcmds; - pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; - pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds + pr_constr_expr : constr_expr -> Pp.t; + pr_lconstr_expr : constr_expr -> Pp.t; + pr_constr_pattern_expr : constr_pattern_expr -> Pp.t; + pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t } - type precedence = Ppextend.precedence * Ppextend.parenRelation let modular_constr_pr = pr let rec fix rf x = rf (fix rf) x let pr = fix modular_constr_pr mt - let transf env c = + let pr prec = function + (* A toplevel printer hack mimicking parsing, incidentally meaning + that we cannot use [pr] correctly anymore in a recursive loop + if the current expr is followed by other exprs which would be + interpreted as arguments *) + | { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us + | c -> pr prec c + + let transf env sigma c = if !Flags.beautify_file then - let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in + let r = Constrintern.for_grammar (Constrintern.intern_constr env sigma) c in Constrextern.extern_glob_constr (Termops.vars_of_env env) r else c - let pr prec c = pr prec (transf (Global.env()) c) + let pr_expr prec c = + let env = Global.env () in + let sigma = Evd.from_env env in + pr prec (transf env sigma c) - let pr_simpleconstr = function - | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us - | c -> pr lsimpleconstr c + let pr_simpleconstr = pr_expr lsimpleconstr let default_term_pr = { pr_constr_expr = pr_simpleconstr; - pr_lconstr_expr = pr ltop; + pr_lconstr_expr = pr_expr ltop; pr_constr_pattern_expr = pr_simpleconstr; - pr_lconstr_pattern_expr = pr ltop + pr_lconstr_pattern_expr = pr_expr ltop } let term_pr = ref default_term_pr let set_term_pr = (:=) term_pr + let pr_constr_expr_n n c = pr_expr n c let pr_constr_expr c = !term_pr.pr_constr_expr c let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c @@ -762,88 +734,5 @@ end) = struct let pr_record_body = pr_record_body_gen pr - let pr_binders = pr_undelimited_binders spc (pr ltop) - -end - -module Tag = -struct - let keyword = - let style = Terminal.make ~bold:true () in - Ppstyle.make ~style ["constr"; "keyword"] - - let evar = - let style = Terminal.make ~fg_color:`LIGHT_BLUE () in - Ppstyle.make ~style ["constr"; "evar"] - - let univ = - let style = Terminal.make ~bold:true ~fg_color:`YELLOW () in - Ppstyle.make ~style ["constr"; "type"] - - let notation = - let style = Terminal.make ~fg_color:`WHITE () in - Ppstyle.make ~style ["constr"; "notation"] - - let variable = - Ppstyle.make ["constr"; "variable"] - - let reference = - let style = Terminal.make ~fg_color:`LIGHT_GREEN () in - Ppstyle.make ~style ["constr"; "reference"] - - let path = - let style = Terminal.make ~fg_color:`LIGHT_MAGENTA () in - Ppstyle.make ~style ["constr"; "path"] - -end - -let do_not_tag _ x = x - -let split_token tag s = - let len = String.length s in - let rec parse_string off i = - if Int.equal i len then - if Int.equal off i then mt () else tag (str (String.sub s off (i - off))) - else if s.[i] == ' ' then - if Int.equal off i then parse_space 1 (succ i) - else tag (str (String.sub s off (i - off))) ++ parse_space 1 (succ i) - else parse_string off (succ i) - and parse_space spc i = - if Int.equal i len then str (String.make spc ' ') - else if s.[i] == ' ' then parse_space (succ spc) (succ i) - else str (String.make spc ' ') ++ parse_string i (succ i) - in - parse_string 0 0 - -(** Instantiating Make with tagging functions that only add style - information. *) -include Make (struct - let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s - let tag_keyword = tag Tag.keyword - let tag_evar = tag Tag.evar - let tag_type = tag Tag.univ - let tag_unparsing = function - | UnpTerminal s -> fun _ -> split_token (fun pp -> tag Tag.notation pp) s - | _ -> do_not_tag () - let tag_constr_expr = do_not_tag - let tag_path = tag Tag.path - let tag_ref = tag Tag.reference - let tag_var = tag Tag.variable -end) - -module Richpp = struct - - include Make (struct - open Ppannotation - let tag_keyword = Pp.tag (Pp.Tag.inj AKeyword tag) - let tag_type = Pp.tag (Pp.Tag.inj AKeyword tag) - let tag_evar = do_not_tag () - let tag_unparsing unp = Pp.tag (Pp.Tag.inj (AUnparsing unp) tag) - let tag_constr_expr e = Pp.tag (Pp.Tag.inj (AConstrExpr e) tag) - let tag_path = do_not_tag () - let tag_ref = do_not_tag () - let tag_var = do_not_tag () - end) - -end + let pr_binders = pr_undelimited_binders spc (pr_expr ltop) |