aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/ppconstr.ml')
-rw-r--r--printing/ppconstr.ml41
1 files changed, 21 insertions, 20 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index fddd54a9f..900bf2daf 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -147,7 +147,7 @@ let tag_var = tag Tag.variable
let pr_with_comments ?loc pp = pr_located (fun x -> x) (Loc.tag ?loc pp)
- let pr_sep_com sep f c = pr_with_comments ~loc:(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 l =
match l with
@@ -221,11 +221,10 @@ let tag_var = tag Tag.variable
| 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
+ 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
let pr_lname = function
| (loc,Name id) -> pr_lident (loc,id)
@@ -302,7 +301,7 @@ let tag_var = tag Tag.variable
assert false
in
let loc = cases_pattern_expr_loc (loc, p) in
- pr_with_comments ~loc
+ pr_with_comments ?loc
(sep() ++ if prec_less prec inh then strm else surround strm)
let pr_patt = pr_patt mt
@@ -310,16 +309,18 @@ let tag_var = tag Tag.variable
let pr_eqn pr (loc,(pl,rhs)) =
let pl = List.map snd pl in
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
++ str " =>") ++
pr_sep_com spc (pr ltop) rhs))
- let begin_of_binder = function
- | CLocalDef((loc,_),_,_) -> fst (Loc.unloc loc)
- | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
- | CLocalPattern(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
@@ -420,12 +421,12 @@ let tag_var = tag Tag.variable
| CLambdaN ((nal,bk,t)::bl,c) ->
let bl,c = extract_lam_binders (loc, CLambdaN(bl,c)) in
CLocalAssum (nal,bk,t) :: bl, c
- | c -> [], Loc.tag ~loc c
+ | c -> [], Loc.tag ?loc c
- let split_lambda = Loc.with_loc (fun ~loc -> function
+ let split_lambda = Loc.with_loc (fun ?loc -> function
| CLambdaN ([[na],bk,t],c) -> (na,t,c)
- | CLambdaN (([na],bk,t)::bl,c) -> (na,t,Loc.tag ~loc @@ CLambdaN(bl,c))
- | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t,Loc.tag ~loc @@ CLambdaN((nal,bk,t)::bl,c))
+ | CLambdaN (([na],bk,t)::bl,c) -> (na,t,Loc.tag ?loc @@ CLambdaN(bl,c))
+ | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t,Loc.tag ?loc @@ CLambdaN((nal,bk,t)::bl,c))
| _ -> anomaly (Pp.str "ill-formed fixpoint body")
)
@@ -436,11 +437,11 @@ let tag_var = tag Tag.variable
| (_,Name id), (_,Anonymous) -> (na,t,c)
| _ -> (na',t,c)
- let split_product na' = Loc.with_loc (fun ~loc -> function
+ let split_product na' = Loc.with_loc (fun ?loc -> function
| CProdN ([[na],bk,t],c) -> rename na na' t c
- | CProdN (([na],bk,t)::bl,c) -> rename na na' t (Loc.tag ~loc @@ CProdN(bl,c))
+ | CProdN (([na],bk,t)::bl,c) -> rename na na' t (Loc.tag ?loc @@ CProdN(bl,c))
| CProdN ((na::nal,bk,t)::bl,c) ->
- rename na na' t (Loc.tag ~loc @@ CProdN((nal,bk,t)::bl,c))
+ rename na na' t (Loc.tag ?loc @@ CProdN((nal,bk,t)::bl,c))
| _ -> anomaly (Pp.str "ill-formed fixpoint body")
)
@@ -730,7 +731,7 @@ let tag_var = tag Tag.variable
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 = {