diff options
author | 2014-10-30 18:48:22 +0100 | |
---|---|---|
committer | 2014-11-04 22:51:35 +0100 | |
commit | 00bb36da0696b1442bf4e0bb1a657e3de8c92b1e (patch) | |
tree | 4c1465b0b6fc6093dff8f21da83ae509d6e671b6 | |
parent | 7f40ab12d4ff5ecceccbeb72555e7c4421bd9dd0 (diff) |
printing/Ppconstr.Make:
- Functorize Ppconstr with respect to a set of tagging functions.
- These functions are meant to introduce tags to produce semistructured
pretty printings.
printing/Ppconstr:
Preserve the previous behaviour of this module by instantiating Make
with tagging functions that do nothing.
-rw-r--r-- | printing/ppconstr.ml | 1270 |
1 files changed, 665 insertions, 605 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index d8d144628..fe8b582b1 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -23,46 +23,54 @@ open Locus open Genredexpr (*i*) -let sep_v = fun _ -> str"," ++ spc() -let pr_tight_coma () = str "," ++ cut () - -let latom = 0 -let lprod = 200 -let llambda = 200 -let lif = 200 -let lletin = 200 -let lletpattern = 200 -let lfix = 200 -let lcast = 100 -let larg = 9 -let lapp = 10 -let lposint = 0 -let lnegint = 35 (* must be consistent with Notation "- x" *) -let ltop = (200,E) -let lproj = 1 -let ldelim = 1 -let lsimpleconstr = (8,E) -let lsimplepatt = (1,E) - -let prec_less child (parent,assoc) = - if parent < 0 && Int.equal child lprod then true - else - let parent = abs parent in - match assoc with - | E -> (<=) child parent - | L -> (<) child parent - | Prec n -> child<=n - | Any -> true - -let prec_of_prim_token = function - | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint - | String _ -> latom - -open Notation - -let print_hunks n pr pr_binders (terms, termlists, binders) unps = +module Make (Taggers : sig + val tag_constr_expr : constr_expr -> std_ppcmds -> std_ppcmds + val tag_unparsing : unparsing -> std_ppcmds -> std_ppcmds +end) = struct + + open Taggers + + let sep_v = fun _ -> str"," ++ spc() + let pr_tight_coma () = str "," ++ cut () + + let latom = 0 + let lprod = 200 + let llambda = 200 + let lif = 200 + let lletin = 200 + let lletpattern = 200 + let lfix = 200 + let lcast = 100 + let larg = 9 + let lapp = 10 + let lposint = 0 + let lnegint = 35 (* must be consistent with Notation "- x" *) + let ltop = (200,E) + let lproj = 1 + let ldelim = 1 + let lsimpleconstr = (8,E) + let lsimplepatt = (1,E) + + let prec_less child (parent,assoc) = + if parent < 0 && Int.equal child lprod then true + else + let parent = abs parent in + match assoc with + | E -> (<=) child parent + | L -> (<) child parent + | Prec n -> child<=n + | Any -> true + + let prec_of_prim_token = function + | Numeral p -> if Bigint.is_pos_or_zero p 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 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: The following function enforces a very precise order of evaluation of subcomponent. @@ -70,638 +78,690 @@ let print_hunks n pr pr_binders (terms, termlists, binders) unps = let rec aux = function | [] -> mt () - | UnpMetaVar (_, prec) :: l -> + | UnpMetaVar (_, prec) as unp :: l -> let c = pop env in let pp2 = aux l in let pp1 = pr (n, prec) c in - (pp1 ++ pp2) - | UnpListMetaVar (_, prec, sl) :: l -> + 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 let pp2 = aux l in - (pp1 ++ pp2) - | UnpBinderListMetaVar (_, isopen, sl) :: l -> + return unp pp1 pp2 + | UnpBinderListMetaVar (_, isopen, sl) as unp :: l -> let cl = pop bll in let pp2 = aux l in let pp1 = pr_binders (fun () -> aux sl) isopen cl in - (pp1 ++ pp2) - | UnpTerminal s :: l -> + return unp pp1 pp2 + | UnpTerminal s as unp :: l -> let pp2 = aux l in let pp1 = str s in - (pp1 ++ pp2) - | UnpBox (b,sub) :: l -> + return unp pp1 pp2 + | UnpBox (b,sub) as unp :: l -> let pp1 = ppcmd_of_box b (aux sub) in let pp2 = aux l in - (pp1 ++ pp2) - | UnpCut cut :: l -> + return unp pp1 pp2 + | UnpCut cut as unp :: l -> let pp2 = aux l in let pp1 = ppcmd_of_cut cut in - (pp1 ++ pp2) + return unp pp1 pp2 in aux unps -let pr_notation pr pr_binders s env = - let unpl, level = find_notation_printing_rule s in - print_hunks level pr pr_binders env unpl, level + let pr_notation pr pr_binders s env = + let unpl, level = find_notation_printing_rule s in + print_hunks level pr pr_binders env unpl, level -let pr_delimiters key strm = - strm ++ str ("%"^key) + let pr_delimiters key strm = + strm ++ str ("%"^key) -let pr_generalization bk ak c = - let hd, tl = - match bk with - | Implicit -> "{", "}" - | Explicit -> "(", ")" - in (* TODO: syntax Abstraction Kind *) + let pr_generalization bk ak c = + let hd, tl = + match bk with + | Implicit -> "{", "}" + | Explicit -> "(", ")" + in (* TODO: syntax Abstraction Kind *) str "`" ++ str hd ++ c ++ str tl -let pr_com_at n = - if Flags.do_beautify() && not (Int.equal n 0) then comment n - else mt() - -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_in_comment pr x = str "(* " ++ pr x ++ str " *)" - -let pr_univ l = - match l with - | [x] -> str x - | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")" - -let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" - -let pr_glob_sort = function - | GProp -> str "Prop" - | GSet -> str "Set" - | GType [] -> str "Type" - | GType u -> hov 0 (str "Type" ++ pr_univ_annot pr_univ u) - -let pr_id = pr_id -let pr_name = pr_name -let pr_qualid = pr_qualid -let pr_patvar = pr_id - -let pr_glob_sort_instance = function - | GProp -> str "Prop" - | GSet -> str "Set" - | GType u -> - (match u with - | Some u -> str u - | None -> str "Type") - -let pr_universe_instance l = - pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l - -let pr_cref ref us = - pr_reference ref ++ pr_universe_instance us - -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) -> - 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 () - | 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_lname = function - (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located pr_name lna - -let pr_or_var pr = function - | ArgArg x -> pr x - | ArgVar (loc,s) -> pr_lident (loc,s) - -let pr_prim_token = function - | Numeral n -> str (Bigint.to_string n) - | String s -> qs s - -let pr_evar pr id l = - hov 0 (str "?" ++ pr_id id ++ - (match l with - | [] -> mt() - | l -> - let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in - str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) - -let las = lapp -let lpator = 100 -let lpatrec = 0 - -let rec pr_patt sep inh p = - let (strm,prec) = match p 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 - | CPatCstr (_,c,[],[]) -> pr_reference c, latom - | CPatCstr (_,c,[],args) -> - pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp - | CPatCstr (_,c,args,[]) -> - str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp - | CPatCstr (_,c,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) -> str "_", latom - | CPatAtom (_,Some r) -> pr_reference r, latom - | CPatOr (_,pl) -> - hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator - | 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 - (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) -> pr_prim_token p, latom - | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimplepatt p), 1 - in - let loc = cases_pattern_expr_loc p 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 - spc() ++ hov 4 - (pr_with_comments loc - (str "| " ++ - hov 0 (prlist_with_sep pr_bar (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) - | _ -> assert false - -let begin_of_binders = function - | b::_ -> begin_of_binder b - | _ -> 0 - -let surround_impl k p = - match k with - | Explicit -> str"(" ++ p ++ str")" - | Implicit -> str"{" ++ p ++ str"}" - -let surround_implicit k p = - match k with - | Explicit -> p - | Implicit -> (str"{" ++ p ++ str"}") - -let pr_binder many pr (nal,k,t) = - match k with - | Generalized (b, b', t') -> - assert (match b with Implicit -> true | _ -> false); - begin match nal with - |[loc,Anonymous] -> - hov 1 (str"`" ++ (surround_impl b' - ((if t' then str "!" else mt ()) ++ pr t))) - |[loc,Name id] -> - hov 1 (str "`" ++ (surround_impl b' - (pr_lident (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,_) -> - let s = prlist_with_sep spc pr_lname nal in - hov 1 (surround_implicit b s) - | _ -> - let s = prlist_with_sep spc pr_lname nal ++ str " : " ++ pr t in - 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) -> + let pr_com_at n = + if Flags.do_beautify() && not (Int.equal n 0) then comment n + else mt() + + 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_in_comment pr x = str "(* " ++ pr x ++ str " *)" + + let pr_univ l = + match l with + | [x] -> str x + | l -> str"max(" ++ prlist_with_sep (fun () -> str",") str l ++ str")" + + let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" + + let pr_glob_sort = function + | GProp -> str "Prop" + | GSet -> str "Set" + | GType [] -> str "Type" + | GType u -> hov 0 (str "Type" ++ pr_univ_annot pr_univ u) + + let pr_id = pr_id + let pr_name = pr_name + let pr_qualid = pr_qualid + let pr_patvar = pr_id + + let pr_glob_sort_instance = function + | GProp -> str "Prop" + | GSet -> str "Set" + | GType u -> + (match u with + | Some u -> str u + | None -> str "Type") + + let pr_universe_instance l = + pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l + + let pr_cref ref us = + pr_reference ref ++ pr_universe_instance us + + 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) -> + 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 () + | 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_lname = function + (loc,Name id) -> pr_lident (loc,id) + | lna -> pr_located pr_name lna + + let pr_or_var pr = function + | ArgArg x -> pr x + | ArgVar (loc,s) -> pr_lident (loc,s) + + let pr_prim_token = function + | Numeral n -> str (Bigint.to_string n) + | String s -> qs s + + let pr_evar pr id l = + hov 0 (str "?" ++ pr_id id ++ + (match l with + | [] -> mt() + | l -> + let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in + str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) + + let las = lapp + let lpator = 100 + let lpatrec = 0 + + let rec pr_patt sep inh p = + let (strm,prec) = match p 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 + | CPatCstr (_,c,[],[]) -> pr_reference c, latom + | CPatCstr (_,c,[],args) -> + pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp + | CPatCstr (_,c,args,[]) -> + str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp + | CPatCstr (_,c,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) -> str "_", latom + | CPatAtom (_,Some r) -> pr_reference r, latom + | CPatOr (_,pl) -> + hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator + | 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 + (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) -> pr_prim_token p, latom + | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimplepatt p), 1 + in + let loc = cases_pattern_expr_loc p 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 + spc() ++ hov 4 + (pr_with_comments loc + (str "| " ++ + hov 0 (prlist_with_sep pr_bar (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) + | _ -> assert false + + let begin_of_binders = function + | b::_ -> begin_of_binder b + | _ -> 0 + + let surround_impl k p = + match k with + | Explicit -> str"(" ++ p ++ str")" + | Implicit -> str"{" ++ p ++ str"}" + + let surround_implicit k p = + match k with + | Explicit -> p + | Implicit -> (str"{" ++ p ++ str"}") + + let pr_binder many pr (nal,k,t) = + match k with + | Generalized (b, b', t') -> + assert (match b with Implicit -> true | _ -> false); + begin match nal with + |[loc,Anonymous] -> + hov 1 (str"`" ++ (surround_impl b' + ((if t' then str "!" else mt ()) ++ pr t))) + |[loc,Name id] -> + hov 1 (str "`" ++ (surround_impl b' + (pr_lident (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,_) -> + let s = prlist_with_sep spc pr_lname nal in + hov 1 (surround_implicit b s) + | _ -> + let s = prlist_with_sep spc pr_lname nal ++ str " : " ++ pr t in + 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) -> pr_binder true pr_c (nal,k,t) - | LocalRawDef (na,c) -> + | 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) - -let pr_undelimited_binders sep pr_c = - prlist_with_sep sep (pr_binder_among_many pr_c) - -let pr_delimited_binders kw sep pr_c bl = - let n = begin_of_binders bl in - match bl with - | [LocalRawAssum (nal,k,t)] -> - pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t) - | LocalRawAssum _ :: _ as bdl -> - pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl - | _ -> assert false - -let pr_binders_gen pr_c sep is_open = - if is_open then pr_delimited_binders mt sep pr_c - else pr_undelimited_binders sep pr_c - -let rec extract_prod_binders = function -(* | CLetIn (loc,na,b,c) as x -> + str":=" ++ cut() ++ pr_c c) + + let pr_undelimited_binders sep pr_c = + prlist_with_sep sep (pr_binder_among_many pr_c) + + let pr_delimited_binders kw sep pr_c bl = + let n = begin_of_binders bl in + match bl with + | [LocalRawAssum (nal,k,t)] -> + pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t) + | LocalRawAssum _ :: _ as bdl -> + pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl + | _ -> assert false + + let pr_binders_gen pr_c sep is_open = + if is_open then pr_delimited_binders mt 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) -> + | CProdN (loc,[],c) -> extract_prod_binders c - | CProdN (loc,(nal,bk,t)::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 + | c -> [], c -let rec extract_lam_binders = function -(* | CLetIn (loc,na,b,c) as x -> + 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) -> + | CLambdaN (loc,[],c) -> extract_lam_binders c - | CLambdaN (loc,(nal,bk,t)::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) -> + | 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" " ++ - 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 - -let pr_guard_annot pr_aux bl (n,ro) = - match n with - | None -> mt () - | Some (loc, id) -> - match (ro : Constrexpr.recursion_order_expr) with - | CStructRec -> - let names_of_binder = function - | LocalRawAssum (nal,_,_) -> nal - | LocalRawDef (_,_) -> [] - in let ids = List.flatten (List.map names_of_binder bl) in - if List.length ids > 1 then - spc() ++ str "{struct " ++ pr_id id ++ str"}" - else mt() - | CWfRec c -> - spc() ++ str "{wf " ++ pr_aux c ++ spc() ++ pr_id id ++ str"}" - | CMeasureRec (m,r) -> - spc() ++ str "{measure " ++ 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 annot = pr_guard_annot (pr lsimpleconstr) bl ro in + | _ -> 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" " ++ + 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 + + let pr_guard_annot pr_aux bl (n,ro) = + match n with + | None -> mt () + | Some (loc, id) -> + match (ro : Constrexpr.recursion_order_expr) with + | CStructRec -> + let names_of_binder = function + | LocalRawAssum (nal,_,_) -> nal + | LocalRawDef (_,_) -> [] + in let ids = List.flatten (List.map names_of_binder bl) in + if List.length ids > 1 then + spc() ++ str "{struct " ++ pr_id id ++ str"}" + else mt() + | CWfRec c -> + spc() ++ str "{wf " ++ pr_aux c ++ spc() ++ pr_id id ++ str"}" + | CMeasureRec (m,r) -> + spc() ++ str "{measure " ++ 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 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) = - pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c + let pr_cofixdecl pr prd dangling_with_for ((_,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") - | [d1] -> pr_decl false d1 - | dl -> + let pr_recursive pr_decl id = function + | [] -> anomaly (Pp.str "(co)fixpoint with no definition") + | [d1] -> pr_decl false d1 + | dl -> prlist_with_sep (fun () -> fnl() ++ str "with ") (pr_decl true) dl ++ - fnl() ++ str "for " ++ pr_id id - -let pr_asin pr (na,indnalopt) = - (match na with (* Decision of printing "_" or not moved to constrextern.ml *) - | Some na -> spc () ++ str "as " ++ pr_lname na - | None -> mt ()) ++ - (match indnalopt with - | None -> mt () - | Some t -> spc () ++ str "in " ++ pr_patt lsimplepatt t) - -let pr_case_item pr (tm,asin) = - hov 0 (pr (lcast,E) tm ++ pr_asin pr asin) - -let pr_case_type pr po = - match po with - | None | Some (CHole (_,_,Misctypes.IntroAnonymous,_)) -> mt() - | Some p -> + fnl() ++ str "for " ++ pr_id id + + let pr_asin pr (na,indnalopt) = + (match na with (* Decision of printing "_" or not moved to constrextern.ml *) + | Some na -> spc () ++ str "as " ++ pr_lname na + | None -> mt ()) ++ + (match indnalopt with + | None -> mt () + | Some t -> spc () ++ str "in " ++ pr_patt lsimplepatt t) + + let pr_case_item pr (tm,asin) = + hov 0 (pr (lcast,E) tm ++ pr_asin pr asin) + + let pr_case_type pr po = + match po with + | None | Some (CHole (_,_,Misctypes.IntroAnonymous,_)) -> mt() + | Some p -> spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimpleconstr) p) -let pr_simple_return_type pr na po = - (match na with - | Some (_,Name id) -> + let pr_simple_return_type pr na po = + (match na with + | Some (_,Name id) -> spc () ++ str "as " ++ pr_id id - | _ -> mt ()) ++ - pr_case_type pr po + | _ -> mt ()) ++ + pr_case_type pr po -let pr_proj pr pr_app a f l = - hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") + let pr_proj pr pr_app a f l = + hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") -let pr_appexpl pr (f,us) l = - hov 2 ( - str "@" ++ pr_reference f ++ + let pr_appexpl pr (f,us) l = + hov 2 ( + str "@" ++ pr_reference f ++ pr_universe_instance us ++ prlist (pr_sep_com spc (pr (lapp,L))) l) -let pr_app pr a l = - hov 2 ( - pr (lapp,L) a ++ - prlist (fun a -> spc () ++ pr_expl_args pr a) l) - -let pr_forall () = str"forall" ++ spc () - -let pr_fun () = str"fun" ++ spc () - -let pr_fun_sep = str " =>" - - -let pr_dangling_with_for sep pr inherited a = - match a with - | (CFix (_,_,[_])|CCoFix(_,_,[_])) -> pr sep (latom,E) a - | _ -> pr sep inherited a - -let pr pr sep inherited a = - let (strm,prec) = match a with - | CRef (r,us) -> pr_cref r us, latom - | CFix (_,id,fix) -> - hov 0 (str"fix " ++ - pr_recursive - (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix), - lfix - | CCoFix (_,id,cofix) -> - hov 0 (str "cofix " ++ - pr_recursive - (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), - lfix - | CProdN _ -> - let (bl,a) = extract_prod_binders a in - hov 0 ( - hov 2 (pr_delimited_binders pr_forall spc - (pr mt ltop) bl) ++ - str "," ++ pr spc ltop a), - lprod - | CLambdaN _ -> - let (bl,a) = extract_lam_binders a in - hov 0 ( - hov 2 (pr_delimited_binders pr_fun spc - (pr mt ltop) bl) ++ - pr_fun_sep ++ pr spc ltop a), - llambda - | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b) - when Id.equal x x' -> - hv 0 ( - hov 2 (str "let " ++ pr mt ltop fx ++ str " in") ++ - pr spc ltop b), - lletin - | CLetIn (_,x,a,b) -> - hv 0 ( - hov 2 (str "let " ++ pr_lname x ++ str " :=" ++ - pr spc ltop a ++ str " in") ++ - pr spc ltop b), - lletin - | 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 - if not (List.is_empty l2) then - p ++ prlist (pr spc (lapp,L)) l2, lapp - else - p, lproj - | CAppExpl (_,(None,Ident (_,var),us),[t]) - | CApp (_,(_,CRef(Ident(_,var),us)),[t,None]) - when Id.equal var Notation_ops.ldots_var -> - hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg - | CAppExpl (_,(None,f,us),l) -> pr_appexpl (pr mt) (f,us) l, lapp - | 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)); - let p = pr_proj (pr mt) pr_app (fst c) f l1 in - if not (List.is_empty l2) then - p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2, lapp - else - p, lproj - | CApp (_,(None,a),l) -> 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 () ++ str"with" ++ spc () - in - hv 0 (str"{|" ++ beg ++ - 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)]) -> - hv 0 ( - str "let '" ++ - hov 0 (pr_patt ltop p ++ - pr_asin (pr_dangling_with_for mt pr) asin ++ - str " :=" ++ pr spc ltop c ++ - pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++ - str " in" ++ pr spc ltop b)), - lletpattern - | CCases(_,_,rtntypopt,c,eqns) -> - v 0 - (hv 0 (str "match" ++ brk (1,2) ++ - hov 0 ( - prlist_with_sep sep_v - (pr_case_item (pr_dangling_with_for mt pr)) c - ++ pr_case_type (pr_dangling_with_for mt pr) rtntypopt) ++ - spc () ++ str "with") ++ - prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"), - latom - | CLetTuple (_,nal,(na,po),c,b) -> - hv 0 ( - str "let " ++ - hov 0 (str "(" ++ - prlist_with_sep sep_v pr_lname nal ++ - str ")" ++ - pr_simple_return_type (pr mt) na po ++ str " :=" ++ - pr spc ltop c ++ str " in") ++ - pr spc ltop b), - lletin - | CIf (_,c,(na,po),b1,b2) -> + let pr_app pr a l = + hov 2 ( + pr (lapp,L) a ++ + prlist (fun a -> spc () ++ pr_expl_args pr a) l) + + let pr_forall () = str"forall" ++ spc () + + let pr_fun () = str"fun" ++ spc () + + let pr_fun_sep = str " =>" + + + let pr_dangling_with_for sep pr inherited a = + match a 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 + | CRef (r, us) -> + return (pr_cref r us, latom) + | CFix (_,id,fix) -> + return ( + hov 0 (str"fix " ++ + pr_recursive + (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix), + lfix + ) + | CCoFix (_,id,cofix) -> + return ( + hov 0 (str "cofix " ++ + pr_recursive + (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), + lfix + ) + | CProdN _ -> + let (bl,a) = extract_prod_binders a in + return ( + hov 0 ( + hov 2 (pr_delimited_binders pr_forall spc + (pr mt ltop) bl) ++ + str "," ++ pr spc ltop a), + lprod + ) + | CLambdaN _ -> + let (bl,a) = extract_lam_binders a in + return ( + hov 0 ( + hov 2 (pr_delimited_binders pr_fun spc + (pr mt ltop) bl) ++ + pr_fun_sep ++ pr spc ltop a), + llambda + ) + | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b) + when Id.equal x x' -> + return ( + hv 0 ( + hov 2 (str "let " ++ pr mt ltop fx ++ str " in") ++ + pr spc ltop b), + lletin + ) + | CLetIn (_,x,a,b) -> + return ( + hv 0 ( + hov 2 (str "let " ++ pr_lname x ++ str " :=" ++ + pr spc ltop a ++ str " in") ++ + pr spc ltop b), + lletin + ) + | 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 + if not (List.is_empty l2) then + 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]) + 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) -> + return (pr_appexpl (pr mt) (f,us) l, lapp) + | 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)); + let p = pr_proj (pr mt) pr_app (fst c) f l1 in + if not (List.is_empty l2) then + return ( + p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2, + lapp + ) + else + 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 () ++ str"with" ++ spc () + in + return ( + hv 0 (str"{|" ++ beg ++ + 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)]) -> + return ( + hv 0 ( + str "let '" ++ + hov 0 (pr_patt ltop p ++ + pr_asin (pr_dangling_with_for mt pr) asin ++ + str " :=" ++ pr spc ltop c ++ + pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++ + str " in" ++ pr spc ltop b)), + lletpattern + ) + | CCases(_,_,rtntypopt,c,eqns) -> + return ( + v 0 + (hv 0 (str "match" ++ brk (1,2) ++ + hov 0 ( + prlist_with_sep sep_v + (pr_case_item (pr_dangling_with_for mt pr)) c + ++ pr_case_type (pr_dangling_with_for mt pr) rtntypopt) ++ + spc () ++ str "with") ++ + prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"), + latom + ) + | CLetTuple (_,nal,(na,po),c,b) -> + return ( + hv 0 ( + str "let " ++ + hov 0 (str "(" ++ + prlist_with_sep sep_v pr_lname nal ++ + str ")" ++ + pr_simple_return_type (pr mt) na po ++ str " :=" ++ + pr spc ltop c ++ str " in") ++ + pr spc ltop b), + lletin + ) + | 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) *) - hv 0 ( - hov 1 (str "if " ++ pr mt ltop c ++ pr_simple_return_type (pr mt) na po) ++ - spc () ++ - hov 0 (str "then" ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++ - hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)), - lif - - | CHole (_,_,Misctypes.IntroIdentifier id,_) -> - str "?[" ++ pr_id id ++ str "]", latom - | CHole (_,_,Misctypes.IntroFresh id,_) -> - str "?[?" ++ pr_id id ++ str "]", latom - | CHole (_,_,_,_) -> str "_", latom - | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom - | CPatVar (_,p) -> str "?" ++ pr_patvar p, latom - | CSort (_,s) -> pr_glob_sort s, latom - | CCast (_,a,b) -> - hv 0 (pr mt (lcast,L) a ++ cut () ++ - match b with - | CastConv b -> str ":" ++ pr mt (-lcast,E) b - | CastVM b -> str "<:" ++ pr mt (-lcast,E) b - | CastNative b -> str "<<:" ++ pr mt (-lcast,E) b - | CastCoerce -> str ":>"), lcast - | CNotation (_,"( _ )",([t],[],[])) -> - 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) -> pr_generalization bk ak (pr mt ltop c), latom - | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p - | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt (ldelim,E) a), ldelim - in - let loc = constr_loc a in - 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 -} - -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 = - if !Flags.beautify_file then - let r = Constrintern.for_grammar (Constrintern.intern_constr env) 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_simpleconstr = function - | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us - | c -> pr lsimpleconstr c - -let default_term_pr = { - pr_constr_expr = pr_simpleconstr; - pr_lconstr_expr = pr ltop; - pr_constr_pattern_expr = pr_simpleconstr; - pr_lconstr_pattern_expr = pr ltop -} - -let term_pr = ref default_term_pr - -let set_term_pr = (:=) term_pr - -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 -let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c - -let pr_cases_pattern_expr = pr_patt ltop - -let pr_binders = pr_undelimited_binders spc (pr ltop) - -let pr_with_occurrences pr (occs,c) = - match occs with - | AllOccurrences -> pr c - | NoOccurrences -> failwith "pr_with_occurrences: no occurrences" - | OnlyOccurrences nl -> - hov 1 (pr c ++ spc() ++ str"at " ++ - hov 0 (prlist_with_sep spc (pr_or_var int) nl)) - | AllOccurrencesBut nl -> - hov 1 (pr c ++ spc() ++ str"at - " ++ - hov 0 (prlist_with_sep spc (pr_or_var int) nl)) - -let pr_red_flag pr r = - (if r.rBeta then pr_arg str "beta" else mt ()) ++ - (if r.rIota then pr_arg str "iota" else mt ()) ++ - (if r.rZeta then pr_arg str "zeta" else mt ()) ++ - (if List.is_empty r.rConst then - if r.rDelta then pr_arg str "delta" - else mt () - else - pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ - hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) - -let pr_metaid id = str"?" ++ pr_id id - -let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function - | Red false -> str "red" - | Hnf -> str "hnf" - | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_pattern) o - | Cbv f -> + return ( + hv 0 ( + hov 1 (str "if " ++ pr mt ltop c ++ pr_simple_return_type (pr mt) na po) ++ + spc () ++ + hov 0 (str "then" ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++ + hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)), + lif + ) + + | CHole (_,_,Misctypes.IntroIdentifier id,_) -> + return (str "?[" ++ pr_id id ++ str "]", latom) + | CHole (_,_,Misctypes.IntroFresh id,_) -> + return (str "?[?" ++ pr_id id ++ str "]", latom) + | CHole (_,_,_,_) -> + return (str "_", latom) + | CEvar (_,n,l) -> + return (pr_evar (pr mt) n l, latom) + | CPatVar (_,p) -> + return (str "?" ++ pr_patvar p, latom) + | CSort (_,s) -> + return (pr_glob_sort s, latom) + | CCast (_,a,b) -> + return ( + hv 0 (pr mt (lcast,L) a ++ cut () ++ + match b with + | CastConv b -> str ":" ++ pr mt (-lcast,E) b + | CastVM b -> str "<:" ++ pr mt (-lcast,E) b + | CastNative b -> str "<<:" ++ pr mt (-lcast,E) b + | CastCoerce -> str ":>"), + lcast + ) + | 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) -> + return (pr_generalization bk ak (pr mt ltop c), latom) + | CPrim (_,p) -> + return (pr_prim_token p, prec_of_prim_token p) + | CDelimiters (_,sc,a) -> + return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim) + in + let loc = constr_loc a in + 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 + } + + 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 = + if !Flags.beautify_file then + let r = Constrintern.for_grammar (Constrintern.intern_constr env) 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_simpleconstr = function + | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us + | c -> pr lsimpleconstr c + + let default_term_pr = { + pr_constr_expr = pr_simpleconstr; + pr_lconstr_expr = pr ltop; + pr_constr_pattern_expr = pr_simpleconstr; + pr_lconstr_pattern_expr = pr ltop + } + + let term_pr = ref default_term_pr + + let set_term_pr = (:=) term_pr + + 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 + let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c + + let pr_cases_pattern_expr = pr_patt ltop + + let pr_binders = pr_undelimited_binders spc (pr ltop) + + let pr_with_occurrences pr (occs,c) = + match occs with + | AllOccurrences -> pr c + | NoOccurrences -> failwith "pr_with_occurrences: no occurrences" + | OnlyOccurrences nl -> + hov 1 (pr c ++ spc() ++ str"at " ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) + | AllOccurrencesBut nl -> + hov 1 (pr c ++ spc() ++ str"at - " ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) + + let pr_red_flag pr r = + (if r.rBeta then pr_arg str "beta" else mt ()) ++ + (if r.rIota then pr_arg str "iota" else mt ()) ++ + (if r.rZeta then pr_arg str "zeta" else mt ()) ++ + (if List.is_empty r.rConst then + if r.rDelta then pr_arg str "delta" + else mt () + else + pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ + hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) + + let pr_metaid id = str"?" ++ pr_id id + + let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function + | Red false -> str "red" + | Hnf -> str "hnf" + | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_pattern) o + | Cbv f -> if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then str "compute" else hov 1 (str "cbv" ++ pr_red_flag pr_ref f) - | Lazy f -> + | Lazy f -> hov 1 (str "lazy" ++ pr_red_flag pr_ref f) - | Cbn f -> + | Cbn f -> hov 1 (str "cbn" ++ pr_red_flag pr_ref f) - | Unfold l -> + | Unfold l -> hov 1 (str "unfold" ++ spc() ++ - prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l) - | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l) - | Pattern l -> + prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l) + | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l) + | Pattern l -> hov 1 (str "pattern" ++ - pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l) + pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr)) l) - | Red true -> error "Shouldn't be accessible from user." - | ExtraRedExpr s -> str s - | CbvVm o -> str "vm_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o - | CbvNative o -> str "native_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o + | Red true -> error "Shouldn't be accessible from user." + | ExtraRedExpr s -> str s + | CbvVm o -> str "vm_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o + | CbvNative o -> str "native_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o -let pr_may_eval test prc prlc pr2 pr3 = function - | ConstrEval (r,c) -> + let pr_may_eval test prc prlc pr2 pr3 = function + | ConstrEval (r,c) -> hov 0 (str "eval" ++ brk (1,1) ++ - pr_red_expr (prc,prlc,pr2,pr3) r ++ - str " in" ++ spc() ++ prc c) - | ConstrContext ((_,id),c) -> + pr_red_expr (prc,prlc,pr2,pr3) r ++ + str " in" ++ spc() ++ prc c) + | ConstrContext ((_,id),c) -> hov 0 (str "context " ++ pr_id id ++ spc () ++ - str "[" ++ prlc c ++ str "]") - | ConstrTypeOf c -> hov 1 (str "type of" ++ spc() ++ prc c) - | ConstrTerm c when test c -> h 0 (str "(" ++ prc c ++ str ")") - | ConstrTerm c -> prc c - -let pr_may_eval a = pr_may_eval (fun _ -> false) a + str "[" ++ prlc c ++ str "]") + | ConstrTypeOf c -> hov 1 (str "type of" ++ spc() ++ prc c) + | ConstrTerm c when test c -> h 0 (str "(" ++ prc c ++ str ")") + | ConstrTerm c -> prc c + + let pr_may_eval a = pr_may_eval (fun _ -> false) a + +end + +(** Preserve the initial behaviour of Ppconstr by instantiating Make + with tagging functions that do nothing. *) +include Make (struct + let do_not_tag _ x = x + let tag_unparsing = do_not_tag + let tag_constr_expr = do_not_tag +end) |