From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [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 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 and other times it printed nothing as the caller checked for `is_ghost` upstream. --- printing/ppconstr.ml | 41 +++++++++++++++++++++-------------------- printing/pputils.ml | 5 +++-- printing/ppvernac.ml | 20 +++++++++----------- printing/prettyp.ml | 16 ++++++++-------- 4 files changed, 41 insertions(+), 41 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index fddd54a9fe..900bf2dafd 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 = { diff --git a/printing/pputils.ml b/printing/pputils.ml index 4ae5035a26..d1ba1a4a10 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -15,14 +15,15 @@ open Locus open Genredexpr let pr_located pr (loc, x) = - if !Flags.beautify && not (Loc.is_ghost loc) then + match loc with + | Some loc when !Flags.beautify -> let (b, e) = Loc.unloc loc in (* Side-effect: order matters *) let before = Pp.comment (CLexer.extract_comments b) in let x = pr x in let after = Pp.comment (CLexer.extract_comments e) in before ++ x ++ after - else pr x + | _ -> pr x let pr_or_var pr = function | ArgArg x -> pr x diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 27faa7c5c6..5b6c5580ad 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -32,11 +32,10 @@ open Decl_kinds let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr let pr_lident (loc,id) = - if 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_plident (lid, l) = pr_lident lid ++ @@ -50,11 +49,10 @@ open Decl_kinds let pr_fqid fqid = str (string_of_fqid fqid) let pr_lfqid (loc,fqid) = - if Loc.is_ghost loc then - let (b,_) = Loc.unloc loc in - pr_located pr_fqid (Loc.make_loc (b,b + String.length(string_of_fqid fqid)),fqid) - else - pr_fqid fqid + match loc with + | None -> pr_fqid fqid + | Some loc -> let (b,_) = Loc.unloc loc in + pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid let pr_lname = function | (loc,Name id) -> pr_lident (loc,id) @@ -296,7 +294,7 @@ open Decl_kinds let begin_of_inductive = function | [] -> 0 - | (_,((loc,_),_))::_ -> fst (Loc.unloc loc) + | (_,((loc,_),_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc let pr_class_rawexpr = function | FunClass -> keyword "Funclass" diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 025514902d..eb1124e738 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -711,7 +711,7 @@ let read_sec_context r = let dir = try Nametab.locate_section qid with Not_found -> - user_err ~loc ~hdr:"read_sec_context" (str "Unknown section.") in + user_err ?loc ~hdr:"read_sec_context" (str "Unknown section.") in let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest @@ -752,7 +752,7 @@ let print_any_name = function let print_name = function | ByNotation (loc,(ntn,sc)) -> print_any_name - (Term (Notation.interp_notation_as_global_reference ~loc (fun _ -> true) + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) | AN ref -> print_any_name (locate_any_name ref) @@ -776,11 +776,11 @@ let print_opaque_name qid = | VarRef id -> env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl -let print_about_any loc k = +let print_about_any ?loc k = match k with | Term ref -> let rb = Reductionops.ReductionBehaviour.print ref in - Dumpglob.add_glob loc ref; + Dumpglob.add_glob ?loc ref; pr_infos_list (print_ref false ref :: blankline :: print_name_infos ref @ @@ -789,7 +789,7 @@ let print_about_any loc k = [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> let () = match Syntax_def.search_syntactic_definition kn with - | [],Notation_term.NRef ref -> Dumpglob.add_glob loc ref + | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref | _ -> () in v 0 ( print_syntactic_def kn ++ fnl () ++ @@ -799,11 +799,11 @@ let print_about_any loc k = let print_about = function | ByNotation (loc,(ntn,sc)) -> - print_about_any loc - (Term (Notation.interp_notation_as_global_reference ~loc (fun _ -> true) + print_about_any ?loc + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) | AN ref -> - print_about_any (loc_of_reference ref) (locate_any_name ref) + print_about_any ?loc:(loc_of_reference ref) (locate_any_name ref) (* for debug *) let inspect depth = -- cgit v1.2.3