diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 109 |
1 files changed, 73 insertions, 36 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e21bfa00..aa94fb7b 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Pp open Names @@ -129,15 +129,13 @@ end) = struct str "`" ++ str hd ++ c ++ str tl let pr_com_at n = - if Flags.do_beautify() && not (Int.equal n 0) then comment n + 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,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 @@ -151,13 +149,19 @@ end) = struct | GType [] -> tag_type (str "Type") | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) + 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) + let pr_qualid sp = let (sl, id) = repr_qualid sp in - let id = tag_ref (str (Id.to_string id)) in + let id = tag_ref (pr_id id) in let sl = match List.rev (DirPath.repr sl) with | [] -> mt () | sl -> - let pr dir = tag_path (str (Id.to_string dir)) ++ str "." in + let pr dir = tag_path (pr_id dir) ++ str "." in prlist pr sl in sl ++ id @@ -182,7 +186,7 @@ end) = struct let pr_reference = function | Qualid (_, qid) -> pr_qualid qid - | Ident (_, id) -> tag_var (str (Id.to_string id)) + | Ident (_, id) -> tag_var (pr_id id) let pr_cref ref us = pr_reference ref ++ pr_universe_instance us @@ -246,16 +250,16 @@ end) = struct | CPatAlias (_, p, id) -> pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las - | CPatCstr (_,c, [], []) -> + | CPatCstr (_,c, None, []) -> pr_reference c, latom - | CPatCstr (_, c, [], args) -> + | CPatCstr (_, c, None, args) -> pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp - | CPatCstr (_, c, args, []) -> + | CPatCstr (_, c, Some args, []) -> str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp - | CPatCstr (_, c, 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 @@ -281,6 +285,8 @@ end) = struct | 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 @@ -300,6 +306,7 @@ end) = struct let begin_of_binder = function LocalRawDef((loc,_),_) -> fst (Loc.unloc loc) | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) + | LocalPattern(loc,_,_) -> fst (Loc.unloc loc) | _ -> assert false let begin_of_binders = function @@ -348,6 +355,13 @@ end) = struct | _ -> 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) -> + let p = pr_patt lsimplepatt p in + match tyo with + | None -> + str "'" ++ p + | Some ty -> + str "'" ++ surround (p ++ spc () ++ str ":" ++ ws 1 ++ pr_c ty) let pr_undelimited_binders sep pr_c = prlist_with_sep sep (pr_binder_among_many pr_c) @@ -356,13 +370,13 @@ end) = struct 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 + kw n ++ pr_binder false pr_c (nal,k,t) + | (LocalRawAssum _ | LocalPattern _) :: _ as bdl -> + kw n ++ 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 + 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 @@ -371,6 +385,11 @@ end) = struct 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 @@ -382,6 +401,11 @@ end) = struct 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 @@ -432,6 +456,7 @@ end) = struct let names_of_binder = function | LocalRawAssum (nal,_,_) -> nal | LocalRawDef (_,_) -> [] + | LocalPattern _ -> 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"}" @@ -457,7 +482,7 @@ end) = struct (pr_decl true) dl ++ fnl() ++ keyword "for" ++ spc () ++ pr_id id - let pr_asin pr (na,indnalopt) = + let pr_asin pr na indnalopt = (match na with (* Decision of printing "_" or not moved to constrextern.ml *) | Some na -> spc () ++ keyword "as" ++ spc () ++ pr_lname na | None -> mt ()) ++ @@ -465,8 +490,8 @@ end) = struct | None -> mt () | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t) - let pr_case_item pr (tm,asin) = - hov 0 (pr (lcast,E) tm ++ pr_asin pr asin) + let pr_case_item pr (tm,as_clause, in_clause) = + hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause) let pr_case_type pr po = match po with @@ -495,9 +520,14 @@ end) = struct pr (lapp,L) a ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l) - let pr_forall () = keyword "forall" ++ spc () + let pr_record_body_gen pr l = + spc () ++ + prlist_with_sep pr_semicolon + (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l - let pr_fun () = keyword "fun" ++ spc () + let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc () + + let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc () let pr_fun_sep = spc () ++ str "=>" @@ -595,28 +625,17 @@ end) = struct return (p, lproj) | CApp (_,(None,a),l) -> return (pr_app (pr mt) a l, lapp) - | CRecord (_,w,l) -> - let beg = - match w with - | None -> - spc () - | Some t -> - spc () ++ pr spc ltop t ++ spc () - ++ keyword "with" ++ spc () - in + | CRecord (_,l) -> return ( - hv 0 (str"{|" ++ beg ++ - prlist_with_sep pr_semicolon - (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l - ++ str" |}"), + hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), latom ) - | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) -> + | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ hov 0 (pr_patt ltop p ++ - pr_asin (pr_dangling_with_for mt pr) asin ++ + pr_asin (pr_dangling_with_for mt pr) as_clause in_clause ++ str " :=" ++ pr spc ltop c ++ pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++ spc () ++ keyword "in" ++ pr spc ltop b)), @@ -741,6 +760,8 @@ end) = struct let pr_cases_pattern_expr = pr_patt ltop + let pr_record_body = pr_record_body_gen pr + let pr_binders = pr_undelimited_binders spc (pr ltop) end @@ -778,6 +799,22 @@ 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 @@ -786,7 +823,7 @@ include Make (struct let tag_evar = tag Tag.evar let tag_type = tag Tag.univ let tag_unparsing = function - | UnpTerminal s -> tag Tag.notation + | 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 |