From 9bebbb96e58b3c1b0f7f88ba2af45462eae69b0f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 10 Dec 2017 09:26:25 +0100 Subject: [ast] Improve precision of Ast location recognition in serialization. We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way. --- printing/ppconstr.ml | 55 ++++++++++++++++++++++++++------------------------- printing/ppconstr.mli | 7 +++---- printing/pputils.ml | 4 +++- printing/pputils.mli | 1 + printing/ppvernac.ml | 46 +++++++++++++++++++++--------------------- printing/prettyp.mli | 4 ++-- printing/printmod.mli | 2 +- 7 files changed, 62 insertions(+), 57 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 873505940..3c7095505 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -10,6 +10,7 @@ open CErrors open Util open Pp +open CAst open Names open Nameops open Libnames @@ -151,7 +152,7 @@ let tag_var = tag Tag.variable 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.tag ?loc pp) + let pr_with_comments ?loc pp = pr_located (fun x -> x) (loc, pp) let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c) @@ -220,28 +221,28 @@ let tag_var = tag Tag.variable let pr_expl_args pr (a,expl) = match expl with | None -> pr (lapp,L) a - | Some (_,ExplByPos (n,_id)) -> + | Some {v=ExplByPos (n,_id)} -> anomaly (Pp.str "Explicitation by position not implemented.") - | Some (_,ExplByName id) -> + | Some {v=ExplByName id} -> str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" let pr_opt_type_spc pr = function | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t - let pr_lident (loc,id) = + let pr_lident {loc; v=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 + pr_located pr_id (Some (Loc.make_loc (b,b + String.length (Id.to_string id))), id) let pr_lname = function - | (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located Name.print lna + | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id) + | x -> pr_ast Name.print x let pr_or_var pr = function | ArgArg x -> pr x - | ArgVar (loc,s) -> pr_lident (loc,s) + | ArgVar id -> pr_lident id let pr_prim_token = function | Numeral (n,s) -> str (if s then n else "-"^n) @@ -315,7 +316,7 @@ let tag_var = tag Tag.variable let pr_patt = pr_patt mt - let pr_eqn pr (loc,(pl,rhs)) = + let pr_eqn pr {loc;v=(pl,rhs)} = spc() ++ hov 4 (pr_with_comments ?loc (str "| " ++ @@ -323,12 +324,12 @@ let tag_var = tag Tag.variable ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) - let begin_of_binder l_bi = + 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 + | CLocalDef({loc},_,_) -> b_loc loc + | CLocalAssum({loc}::_,_,_) -> b_loc loc + | CLocalPattern{loc} -> b_loc loc | _ -> assert false let begin_of_binders = function @@ -350,12 +351,12 @@ let tag_var = tag Tag.variable | Generalized (b, b', t') -> assert (match b with Implicit -> true | _ -> false); begin match nal with - |[loc,Anonymous] -> + |[{loc; v=Anonymous}] -> hov 1 (str"`" ++ (surround_impl b' ((if t' then str "!" else mt ()) ++ pr t))) - |[loc,Name id] -> + |[{loc; v=Name id}] -> hov 1 (str "`" ++ (surround_impl b' - (pr_lident (loc,id) ++ str " : " ++ + (pr_lident CAst.(make ?loc id) ++ str " : " ++ (if t' then str "!" else mt()) ++ pr t))) |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.") end @@ -375,7 +376,7 @@ let tag_var = tag Tag.variable surround (pr_lname na ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++ str" :=" ++ spc() ++ pr_c c) - | CLocalPattern (loc,(p,tyo)) -> + | CLocalPattern {CAst.loc; v = p,tyo} -> let p = pr_patt lsimplepatt p in match tyo with | None -> @@ -410,7 +411,7 @@ let tag_var = tag Tag.variable let pr_guard_annot pr_aux bl (n,ro) = match n with | None -> mt () - | Some (loc, id) -> + | Some {loc; v = id} -> match (ro : Constrexpr.recursion_order_expr) with | CStructRec -> let names_of_binder = function @@ -427,11 +428,11 @@ let tag_var = tag Tag.variable spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++ (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" - let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) = + let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) = let annot = pr_guard_annot (pr lsimpleconstr) bl ro in pr_recursive_decl pr prd dangling_with_for id bl annot t c - let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) = + let pr_cofixdecl pr prd dangling_with_for ({v=id},bl,t,c) = pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c let pr_recursive pr_decl id = function @@ -461,7 +462,7 @@ let tag_var = tag Tag.variable let pr_simple_return_type pr na po = (match na with - | Some (_,Name id) -> + | Some {v=Name id} -> spc () ++ keyword "as" ++ spc () ++ pr_id id | _ -> mt ()) ++ pr_case_type pr po @@ -492,7 +493,7 @@ let tag_var = tag Tag.variable let pr_fun_sep = spc () ++ str "=>" let pr_dangling_with_for sep pr inherited a = - match a.CAst.v with + match a.v with | (CFix (_,[_])|CCoFix(_,[_])) -> pr sep (latom,E) a | _ -> @@ -507,14 +508,14 @@ let tag_var = tag Tag.variable return ( hov 0 (keyword "fix" ++ spc () ++ pr_recursive - (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix), + (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v fix), lfix ) | CCoFix (id,cofix) -> return ( hov 0 (keyword "cofix" ++ spc () ++ pr_recursive - (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), + (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v cofix), lfix ) | CProdN (bl,a) -> @@ -533,8 +534,8 @@ let tag_var = tag Tag.variable pr_fun_sep ++ pr spc ltop a), llambda ) - | CLetIn ((_,Name x), ({ CAst.v = CFix((_,x'),[_])} - | { CAst.v = CCoFix((_,x'),[_]) } as fx), t, b) + | CLetIn ({v=Name x}, ({ v = CFix({v=x'},[_])} + | { v = CCoFix({v=x'},[_]) } as fx), t, b) when Id.equal x x' -> return ( hv 0 ( @@ -590,7 +591,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],[(_,([[p]],b))]) -> + | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 158906dd2..cedeed5f3 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -10,7 +10,6 @@ objects and their subcomponents. *) (** The default pretty-printers produce pretty-printing commands ({!Pp.t}). *) -open Loc open Libnames open Constrexpr open Names @@ -23,8 +22,8 @@ val pr_tight_coma : unit -> Pp.t val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t -val pr_lident : Id.t located -> Pp.t -val pr_lname : Name.t located -> Pp.t +val pr_lident : lident -> Pp.t +val pr_lname : lname -> Pp.t val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t val pr_com_at : int -> Pp.t @@ -44,7 +43,7 @@ val pr_glob_level : glob_level -> Pp.t val pr_glob_sort : glob_sort -> Pp.t val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list -> - ('a * Names.Id.t) option * recursion_order_expr -> + lident option * recursion_order_expr -> Pp.t val pr_record_body : (reference * constr_expr) list -> Pp.t diff --git a/printing/pputils.ml b/printing/pputils.ml index a544b4762..e779fc5fc 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -24,9 +24,11 @@ let pr_located pr (loc, x) = before ++ x ++ after | _ -> pr x +let pr_ast pr { CAst.loc; v } = pr_located pr (loc, v) + let pr_or_var pr = function | ArgArg x -> pr x - | ArgVar (_,s) -> Names.Id.print s + | ArgVar {CAst.v=s} -> Names.Id.print s let pr_with_occurrences pr keyword (occs,c) = match occs with diff --git a/printing/pputils.mli b/printing/pputils.mli index f7f586b77..ec5c32fc4 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -12,6 +12,7 @@ open Locus open Genredexpr val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t +val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t (** Prints an object surrounded by its commented location *) val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 31c0d20f3..83cac7ddd 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -11,6 +11,8 @@ open Names open CErrors open Util +open CAst + open Extend open Vernacexpr open Pputils @@ -59,7 +61,7 @@ open Decl_kinds let pr_ident_decl (lid, l) = pr_lident lid ++ pr_universe_decl l - + let string_of_fqid fqid = String.concat "." (List.map Id.to_string fqid) @@ -236,7 +238,7 @@ open Decl_kinds keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ pr_located pr_qualid qid - let rec pr_module_ast leading_space pr_c = let open CAst in function + let rec pr_module_ast leading_space pr_c = function | { loc ; v = CMident qid } -> if leading_space then spc () ++ pr_located pr_qualid (loc, qid) @@ -287,10 +289,10 @@ open Decl_kinds prlist_strict (pr_module_vardecls pr_c) l let pr_type_option pr_c = function - | { CAst.v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() + | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() | _ as c -> brk(0,2) ++ str" :" ++ pr_c c - let pr_decl_notation prc ((loc,ntn),c,scopt) = + let pr_decl_notation prc ({loc; v=ntn},c,scopt) = fnl () ++ keyword "where " ++ qs ntn ++ str " := " ++ Flags.without_option Flags.beautify prc c ++ pr_opt (fun sc -> str ": " ++ str sc) scopt @@ -329,7 +331,7 @@ open Decl_kinds let begin_of_inductive = function | [] -> 0 - | (_,((loc,_),_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc + | (_,({loc},_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc let pr_class_rawexpr = function | FunClass -> keyword "Funclass" @@ -392,8 +394,8 @@ open Decl_kinds | SetOnlyPrinting -> keyword "only printing" | SetOnlyParsing -> keyword "only parsing" | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") - | SetFormat("text",s) -> keyword "format " ++ pr_located qs s - | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s + | SetFormat("text",s) -> keyword "format " ++ pr_ast qs s + | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s let pr_syntax_modifiers = function | [] -> mt() @@ -537,7 +539,7 @@ open Decl_kinds let rec aux = function | SsEmpty -> "()" | SsType -> "(Type)" - | SsSingl (_,id) -> "("^Id.to_string id^")" + | SsSingl { v=id } -> "("^Id.to_string id^")" | SsCompl e -> "-" ^ aux e^"" | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" @@ -661,7 +663,7 @@ open Decl_kinds ++ spc() ++ pr_smart_global q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" ) - | VernacInfix (((_,s),mv),q,sn) -> (* A Verifier *) + | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *) return ( hov 0 (hov 0 (keyword "Infix " ++ qs s ++ str " :=" ++ pr_constrarg q) ++ @@ -670,7 +672,7 @@ open Decl_kinds | None -> mt() | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) ) - | VernacNotation (c,((_,s),l),opt) -> + | VernacNotation (c,({v=s},l),opt) -> return ( hov 2 (keyword "Notation" ++ spc() ++ qs s ++ str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++ @@ -680,7 +682,7 @@ open Decl_kinds ) | VernacSyntaxExtension (_, (s, l)) -> return ( - keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++ + keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++ pr_syntax_modifiers l ) | VernacNotationAddFormat(s,k,v) -> @@ -692,7 +694,7 @@ open Decl_kinds | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *) let pr_def_token dk = keyword ( - if Name.is_anonymous (snd (fst id)) + if Name.is_anonymous (fst id).v then "Goal" else Kindops.string_of_definition_object_kind dk) in @@ -711,7 +713,7 @@ open Decl_kinds in (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) | ProveBody (bl,t) -> - let typ u = if snd (fst id) = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in + let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in let (binds,typ,c) = pr_def_body b in return ( @@ -889,16 +891,16 @@ open Decl_kinds return ( hov 1 ( (if abst then keyword "Declare" ++ spc () else mt ()) ++ - keyword "Instance" ++ - (match instid with - | (loc, Name id), l -> spc () ++ pr_ident_decl ((loc, id),l) ++ spc () - | (_, Anonymous), _ -> mt ()) ++ - pr_and_type_binders_arg sup ++ + keyword "Instance" ++ + (match instid with + | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc () + | { v = Anonymous }, _ -> mt ()) ++ + pr_and_type_binders_arg sup ++ str":" ++ spc () ++ (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with - | Some (true, { CAst.v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" + | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" | Some (true,_) -> assert false | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) @@ -1031,7 +1033,7 @@ open Decl_kinds hov 2 ( keyword "Arguments" ++ spc() ++ pr_smart_global q ++ - let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in + let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in let pr_if b x = if b then x else str "" in let pr_br imp x = match imp with | Vernacexpr.Implicit -> str "[" ++ x ++ str "]" @@ -1237,9 +1239,9 @@ let pr_vernac_flag = (fun f a -> pr_vernac_flag f ++ spc() ++ a) f (pr_vernac_expr v' ++ sep_end v') - | VernacTime (_,(_,v)) -> + | VernacTime (_,{v}) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) - | VernacRedirect (s, (_,v)) -> + | VernacRedirect (s, {v}) -> return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v) | VernacTimeout(n,v) -> return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index fd7f1f92b..c1d8f1d37 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -33,10 +33,10 @@ val print_eval : Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t val print_name : env -> Evd.evar_map -> reference or_by_notation -> - Vernacexpr.univ_name_list option -> Pp.t + Universes.univ_name_list option -> Pp.t val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t val print_about : env -> Evd.evar_map -> reference or_by_notation -> - Vernacexpr.univ_name_list option -> Pp.t + Universes.univ_name_list option -> Pp.t val print_impargs : reference or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) diff --git a/printing/printmod.mli b/printing/printmod.mli index 97ed063fe..4f15dd393 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -13,6 +13,6 @@ val printable_body : DirPath.t -> bool val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> - Vernacexpr.univ_name_list option -> Pp.t + Universes.univ_name_list option -> Pp.t val print_module : bool -> ModPath.t -> Pp.t val print_modtype : ModPath.t -> Pp.t -- cgit v1.2.3