[location] Make location optional in Loc.located

This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.

We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.

The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.

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 = {