diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 30 |
1 files changed, 18 insertions, 12 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index bce5710d6..51735bc9e 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -150,10 +150,15 @@ let tag_var = tag Tag.variable 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] -> Name.print x - | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (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 "}" @@ -166,8 +171,9 @@ let tag_var = tag Tag.variable 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 (Name.print 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 @@ -192,8 +198,9 @@ let tag_var = tag Tag.variable tag_type (str "Set") | GType u -> (match u with - | Some (_,u) -> Name.print 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 @@ -279,7 +286,7 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator + hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator | CPatNotation ("( _ )",([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom @@ -304,11 +311,10 @@ let tag_var = tag Tag.variable 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 + hov 0 (prlist_with_sep pr_spcbar (prlist_with_sep sep_v (pr_patt ltop)) pl ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) @@ -395,7 +401,7 @@ let tag_var = tag Tag.variable | { 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))])} ) } + { 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 @@ -411,7 +417,7 @@ let tag_var = tag Tag.variable | CLambdaN ([],c) -> extract_lam_binders c | CLambdaN ([[_,Name id],bk,t], - { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) + { 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 @@ -643,7 +649,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],[(_,([(loc,[p])],b))]) -> + | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([[p]],b))]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ |