From 6dc94fe5c1e02fccefbfedfcb1d4347274f3de0b Mon Sep 17 00:00:00 2001 From: filliatr Date: Mon, 28 May 2001 12:14:49 +0000 Subject: Pretty -> Prettyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1768 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 34 +-- Makefile | 4 +- contrib/interface/name_to_ast.ml | 2 +- parsing/pretty.ml | 595 --------------------------------------- parsing/pretty.mli | 59 ---- parsing/prettyp.ml | 595 +++++++++++++++++++++++++++++++++++++++ parsing/prettyp.mli | 59 ++++ parsing/search.ml | 1 - proofs/proof_trees.ml | 1 - tactics/tacticals.ml | 1 - toplevel/himsg.ml | 1 - toplevel/vernacentries.ml | 10 +- 12 files changed, 679 insertions(+), 683 deletions(-) delete mode 100644 parsing/pretty.ml delete mode 100644 parsing/pretty.mli create mode 100644 parsing/prettyp.ml create mode 100644 parsing/prettyp.mli diff --git a/.depend b/.depend index 2f9c529c10..8a2b81b565 100644 --- a/.depend +++ b/.depend @@ -69,7 +69,7 @@ parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/term.cmi parsing/g_zsyntax.cmi: parsing/coqast.cmi parsing/pcoq.cmi: parsing/coqast.cmi -parsing/pretty.cmi: kernel/environ.cmi kernel/inductive.cmi library/lib.cmi \ +parsing/prettyp.cmi: kernel/environ.cmi kernel/inductive.cmi library/lib.cmi \ kernel/names.cmi library/nametab.cmi lib/pp.cmi kernel/reduction.cmi \ kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi parsing/printer.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \ @@ -592,20 +592,20 @@ parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \ lib/util.cmi parsing/pcoq.cmi parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \ lib/util.cmx parsing/pcoq.cmi -parsing/pretty.cmo: pretyping/classops.cmi kernel/declarations.cmi \ +parsing/prettyp.cmo: pretyping/classops.cmi kernel/declarations.cmi \ library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \ library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \ library/lib.cmi library/libobject.cmi kernel/names.cmi \ library/nametab.cmi lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi \ kernel/safe_typing.cmi kernel/sign.cmi pretyping/syntax_def.cmi \ - kernel/term.cmi kernel/typeops.cmi lib/util.cmi parsing/pretty.cmi -parsing/pretty.cmx: pretyping/classops.cmx kernel/declarations.cmx \ + kernel/term.cmi kernel/typeops.cmi lib/util.cmi parsing/prettyp.cmi +parsing/prettyp.cmx: pretyping/classops.cmx kernel/declarations.cmx \ library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \ library/impargs.cmx kernel/inductive.cmx kernel/instantiate.cmx \ library/lib.cmx library/libobject.cmx kernel/names.cmx \ library/nametab.cmx lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx \ kernel/safe_typing.cmx kernel/sign.cmx pretyping/syntax_def.cmx \ - kernel/term.cmx kernel/typeops.cmx lib/util.cmx parsing/pretty.cmi + kernel/term.cmx kernel/typeops.cmx lib/util.cmx parsing/prettyp.cmi parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ kernel/environ.cmi parsing/esyntax.cmi parsing/extend.cmi \ library/global.cmi kernel/names.cmi lib/options.cmi pretyping/pattern.cmi \ @@ -622,14 +622,14 @@ parsing/search.cmo: parsing/astterm.cmi parsing/coqast.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ kernel/evd.cmi library/global.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ - parsing/pretty.cmi pretyping/pretyping.cmi parsing/printer.cmi \ + parsing/prettyp.cmi pretyping/pretyping.cmi parsing/printer.cmi \ pretyping/rawterm.cmi pretyping/retyping.cmi kernel/term.cmi \ pretyping/typing.cmi lib/util.cmi parsing/search.cmi parsing/search.cmx: parsing/astterm.cmx parsing/coqast.cmx \ kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ kernel/evd.cmx library/global.cmx library/libobject.cmx \ library/library.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ - parsing/pretty.cmx pretyping/pretyping.cmx parsing/printer.cmx \ + parsing/prettyp.cmx pretyping/pretyping.cmx parsing/printer.cmx \ pretyping/rawterm.cmx pretyping/retyping.cmx kernel/term.cmx \ pretyping/typing.cmx lib/util.cmx parsing/search.cmi parsing/termast.cmo: parsing/ast.cmi pretyping/classops.cmi \ @@ -835,14 +835,14 @@ proofs/pfedit.cmx: parsing/astterm.cmx kernel/declarations.cmx \ proofs/proof_trees.cmo: parsing/ast.cmi kernel/closure.cmi \ pretyping/detyping.cmi kernel/environ.cmi pretyping/evarutil.cmi \ kernel/evd.cmi library/global.cmi kernel/names.cmi library/nametab.cmi \ - lib/pp.cmi parsing/pretty.cmi parsing/printer.cmi proofs/proof_type.cmi \ + lib/pp.cmi parsing/prettyp.cmi parsing/printer.cmi proofs/proof_type.cmi \ kernel/sign.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \ parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \ proofs/proof_trees.cmi proofs/proof_trees.cmx: parsing/ast.cmx kernel/closure.cmx \ pretyping/detyping.cmx kernel/environ.cmx pretyping/evarutil.cmx \ kernel/evd.cmx library/global.cmx kernel/names.cmx library/nametab.cmx \ - lib/pp.cmx parsing/pretty.cmx parsing/printer.cmx proofs/proof_type.cmx \ + lib/pp.cmx parsing/prettyp.cmx parsing/printer.cmx proofs/proof_type.cmx \ kernel/sign.cmx lib/stamps.cmx pretyping/tacred.cmx kernel/term.cmx \ parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \ proofs/proof_trees.cmi @@ -1090,7 +1090,7 @@ tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi library/global.cmi library/indrec.cmi \ kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi \ - pretyping/pattern.cmi lib/pp.cmi parsing/pretty.cmi kernel/reduction.cmi \ + pretyping/pattern.cmi lib/pp.cmi parsing/prettyp.cmi kernel/reduction.cmi \ kernel/sign.cmi lib/stamps.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ kernel/term.cmi parsing/termast.cmi lib/util.cmi tactics/wcclausenv.cmi \ tactics/tacticals.cmi @@ -1098,7 +1098,7 @@ tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \ kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx library/global.cmx library/indrec.cmx \ kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx \ - pretyping/pattern.cmx lib/pp.cmx parsing/pretty.cmx kernel/reduction.cmx \ + pretyping/pattern.cmx lib/pp.cmx parsing/prettyp.cmx kernel/reduction.cmx \ kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ kernel/term.cmx parsing/termast.cmx lib/util.cmx tactics/wcclausenv.cmx \ tactics/tacticals.cmi @@ -1233,13 +1233,13 @@ toplevel/fhimsg.cmx: kernel/environ.cmx parsing/g_minicoq.cmx \ toplevel/himsg.cmo: parsing/ast.cmi pretyping/cases.cmi kernel/environ.cmi \ library/global.cmi kernel/indtypes.cmi kernel/inductive.cmi \ proofs/logic.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ - parsing/pretty.cmi pretyping/pretype_errors.cmi parsing/printer.cmi \ + parsing/prettyp.cmi pretyping/pretype_errors.cmi parsing/printer.cmi \ kernel/reduction.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ kernel/type_errors.cmi lib/util.cmi toplevel/himsg.cmi toplevel/himsg.cmx: parsing/ast.cmx pretyping/cases.cmx kernel/environ.cmx \ library/global.cmx kernel/indtypes.cmx kernel/inductive.cmx \ proofs/logic.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ - parsing/pretty.cmx pretyping/pretype_errors.cmx parsing/printer.cmx \ + parsing/prettyp.cmx pretyping/pretype_errors.cmx parsing/printer.cmx \ kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \ kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi toplevel/line_oriented_parser.cmo: toplevel/line_oriented_parser.cmi @@ -1320,7 +1320,7 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ library/impargs.cmi library/lib.cmi library/libobject.cmi \ library/library.cmi toplevel/metasyntax.cmi toplevel/mltop.cmi \ kernel/names.cmi library/nametab.cmi lib/options.cmi proofs/pfedit.cmi \ - lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi parsing/printer.cmi \ + lib/pp.cmi lib/pp_control.cmi parsing/prettyp.cmi parsing/printer.cmi \ proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \ toplevel/recordobj.cmi kernel/reduction.cmi proofs/refiner.cmi \ kernel/safe_typing.cmi parsing/search.cmi lib/stamps.cmi \ @@ -1337,7 +1337,7 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ library/impargs.cmx library/lib.cmx library/libobject.cmx \ library/library.cmx toplevel/metasyntax.cmx toplevel/mltop.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pfedit.cmx \ - lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx parsing/printer.cmx \ + lib/pp.cmx lib/pp_control.cmx parsing/prettyp.cmx parsing/printer.cmx \ proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \ toplevel/recordobj.cmx kernel/reduction.cmx proofs/refiner.cmx \ kernel/safe_typing.cmx parsing/search.cmx lib/stamps.cmx \ @@ -1734,7 +1734,7 @@ contrib/interface/name_to_ast.cmo: parsing/ast.cmi pretyping/classops.cmi \ parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ kernel/environ.cmi library/global.cmi library/impargs.cmi \ kernel/inductive.cmi library/lib.cmi library/libobject.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/pretty.cmi \ + kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/prettyp.cmi \ kernel/reduction.cmi kernel/sign.cmi pretyping/syntax_def.cmi \ kernel/term.cmi parsing/termast.cmi lib/util.cmi \ contrib/interface/name_to_ast.cmi @@ -1742,7 +1742,7 @@ contrib/interface/name_to_ast.cmx: parsing/ast.cmx pretyping/classops.cmx \ parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \ kernel/environ.cmx library/global.cmx library/impargs.cmx \ kernel/inductive.cmx library/lib.cmx library/libobject.cmx \ - kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/pretty.cmx \ + kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/prettyp.cmx \ kernel/reduction.cmx kernel/sign.cmx pretyping/syntax_def.cmx \ kernel/term.cmx parsing/termast.cmx lib/util.cmx \ contrib/interface/name_to_ast.cmi diff --git a/Makefile b/Makefile index 6a2fabb26a..2231746fa2 100644 --- a/Makefile +++ b/Makefile @@ -98,7 +98,7 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \ parsing/g_constr.cmo parsing/g_cases.cmo \ parsing/extend.cmo parsing/esyntax.cmo \ - parsing/printer.cmo parsing/pretty.cmo parsing/search.cmo \ + parsing/printer.cmo parsing/prettyp.cmo parsing/search.cmo \ parsing/egrammar.cmo \ parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo @@ -230,7 +230,7 @@ $(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) $(STRIP) $@ $(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) - $(COQMKTOP) -top $(INCLUDES) $(CAMLDEBUG) -o $@ + $(COQMKTOP) -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@ $(COQTOP): cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE) diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 09cefb2d92..20122d5762 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -10,7 +10,7 @@ open Reduction;; open Libobject;; open Environ;; open Declarations;; -open Pretty;; +open Prettyp;; open Inductive;; open Util;; open Pp;; diff --git a/parsing/pretty.ml b/parsing/pretty.ml deleted file mode 100644 index 6044767c2c..0000000000 --- a/parsing/pretty.ml +++ /dev/null @@ -1,595 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ] - -let print_typed_value x = print_typed_value_in_env (Global.env ()) x - -let pkprinters = function - | FW -> (fprterm,fprterm_env) - | CCI -> (prterm,prterm_env) - | _ -> anomaly "pkprinters" - -let print_impl_args = function - | [] -> [<>] - | [i] -> [< 'sTR"Position ["; 'iNT i; 'sTR"] is implicit" >] - | l -> - [< 'sTR"Positions ["; - prlist_with_sep (fun () -> [< 'sTR";" >]) (fun i -> [< 'iNT i >]) l; - 'sTR"] are implicit" >] - -(* To be improved; the type should be used to provide the types in the - abstractions. This should be done recursively inside prterm, so that - the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u) - synthesizes the type nat of the abstraction on u *) - -let print_named_def name body typ = - let pbody = prterm body in - let ptyp = prtype typ in - [< 'sTR "*** ["; 'sTR name ; 'sTR " "; - hOV 0 [< 'sTR ":="; 'bRK (1,2); pbody; 'sPC; - 'sTR ":"; 'bRK (1,2); ptyp >]; - 'sTR "]"; 'fNL >] - -let print_named_assum name typ = - [< 'sTR "*** [" ; 'sTR name ; 'sTR " : "; prtype typ; 'sTR "]"; 'fNL >] - -let print_named_decl (id,c,typ) = - let s = string_of_id id in - match c with - | Some body -> print_named_def s body typ - | None -> print_named_assum s typ - -let assumptions_for_print lna = - List.fold_right (fun na env -> add_name na env) lna empty_names_context - -let implicit_args_id id l = - if l = [] then - [<>] - else - [< 'sTR"For "; pr_id id; 'sTR": "; print_impl_args l ; 'fNL >] - -let implicit_args_msg sp mipv = - [< prvecti - (fun i mip -> - let imps = inductive_implicits_list (sp,i) in - [< (implicit_args_id mip.mind_typename imps); - prvecti - (fun j idc -> - let imps = constructor_implicits_list ((sp,i),succ j) in - (implicit_args_id idc imps)) - mip.mind_consnames - >]) - mipv >] - -let print_params env params = - if List.length params = 0 then - [<>] - else - [< 'sTR "["; pr_rel_context env params; 'sTR "]"; 'bRK(1,2) >] - -let print_constructors envpar names types = - let pc = - [< prvect_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >]) - (fun (id,c) -> [< pr_id id; 'sTR " : "; prterm_env envpar c >]) - (array_map2 (fun n t -> (n,t)) names types) >] - in hV 0 [< 'sTR " "; pc >] - -let build_inductive sp tyi = - let ctxt = context_of_global_reference (IndRef (sp,tyi)) in - let ctxt = Array.of_list (instance_from_section_context ctxt) in - let mis = Global.lookup_mind_specif ((sp,tyi),ctxt) in - let params = mis_params_ctxt mis in - let args = extended_rel_list 0 params in - let indf = make_ind_family (mis,args) in - let arity = get_arity_type indf in - let cstrtypes = get_constructors_types indf in - let cstrnames = mis_consnames mis in - (IndRef (sp,tyi), params, arity, cstrnames, cstrtypes) - -let print_one_inductive sp tyi = - let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in - let env = Global.env () in - let envpar = push_rels params env in - (hOV 0 - [< (hOV 0 - [< pr_global (IndRef (sp,tyi)) ; 'bRK(1,2); print_params env params; - 'sTR ": "; prterm_env envpar arity; 'sTR " :=" >]); - 'bRK(1,2); print_constructors envpar cstrnames cstrtypes >]) - -let print_mutual sp = - let mipv = (Global.lookup_mind sp).mind_packets in - if Array.length mipv = 1 then - let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp 0 in - let sfinite = - if mipv.(0).mind_finite then "Inductive " else "CoInductive " in - let env = Global.env () in - let envpar = push_rels params env in - (hOV 0 [< - 'sTR sfinite ; - pr_global (IndRef (sp,0)); 'bRK(1,2); - print_params env params; 'bRK(1,5); - 'sTR": "; prterm_env envpar arity; 'sTR" :="; - 'bRK(0,4); print_constructors envpar cstrnames cstrtypes; 'fNL; - implicit_args_msg sp mipv >] ) - (* Mutual [co]inductive definitions *) - else - let _,(mipli,miplc) = - Array.fold_right - (fun mi (n,(li,lc)) -> - if mi.mind_finite then (n+1,(n::li,lc)) else (n+1,(li,n::lc))) - mipv (0,([],[])) - in - let strind = - if mipli = [] then [<>] - else [< 'sTR "Inductive"; 'bRK(1,4); - (prlist_with_sep - (fun () -> [< 'fNL; 'sTR" with"; 'bRK(1,4) >]) - (print_one_inductive sp) mipli); 'fNL >] - and strcoind = - if miplc = [] then [<>] - else [< 'sTR "CoInductive"; 'bRK(1,4); - (prlist_with_sep - (fun () -> [<'fNL; 'sTR " with"; 'bRK(1,4) >]) - (print_one_inductive sp) miplc); 'fNL >] - in - (hV 0 [< 'sTR"Mutual " ; - if mipv.(0).mind_finite then - [< strind; strcoind >] - else - []; - implicit_args_msg sp mipv >]) - -(* - let env = Global.env () in - let evd = Evd.empty in - let {mind_packets=mipv} = mib in - (* On suppose que tous les inductifs ont les même paramètres *) - let nparams = mipv.(0).mind_nparams in - let (lpars,_) = decomp_n_prod env evd nparams - (body_of_type (mind_user_arity mipv.(0))) in - let arities = Array.map (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mipv in - let env_ar = push_rels lpars env in - let pr_constructor (id,c) = - [< pr_id id; 'sTR " : "; prterm_env env_ar c >] in - let print_constructors mis = - let (_,lC) = mis_type_mconstructs mis in - let lidC = - array_map2 (fun id c -> (id, snd (decomp_n_prod env evd nparams c))) - (mis_consnames mis) lC in - let plidC = - prvect_with_sep (fun () -> [<'bRK(0,0); 'sTR "| " >]) - pr_constructor - lidC - in - hV 0 [< 'sTR " "; plidC >] - in - let params = - if nparams = 0 then - [<>] - else - [< 'sTR "["; pr_rel_context env lpars; 'sTR "]"; 'bRK(1,2) >] in - let print_oneind tyi = - let mis = - build_mis - ((sp,tyi), - Array.of_list (instance_from_section_context mib.mind_hyps)) - mib in - let (_,arity) = decomp_n_prod env evd nparams - (body_of_type (mis_user_arity mis)) in - (hOV 0 - [< (hOV 0 - [< pr_global (IndRef (sp,tyi)) ; 'bRK(1,2); params; - 'sTR ": "; prterm_env env_ar arity; 'sTR " :=" >]); - 'bRK(1,2); print_constructors mis >]) - in - let mis0 = - build_mis - ((sp,0),Array.of_list (instance_from_section_context mib.mind_hyps)) - mib in - (* Case one [co]inductive *) - if Array.length mipv = 1 then - let (_,arity) = decomp_n_prod env evd nparams - (body_of_type (mis_user_arity mis0)) in - let sfinite = if mis_finite mis0 then "Inductive " else "CoInductive " in - (hOV 0 [< 'sTR sfinite ; pr_global (IndRef (sp,0)); - if nparams = 0 then - [<>] - else - [< 'sTR" ["; pr_rel_context env lpars; 'sTR "]">]; - 'bRK(1,5); 'sTR": "; prterm_env env_ar arity; 'sTR" :="; - 'bRK(0,4); print_constructors mis0; 'fNL; - implicit_args_msg sp mipv >] ) - (* Mutual [co]inductive definitions *) - else - let _,(mipli,miplc) = - List.fold_left - (fun (n,(li,lc)) mi -> - if mi.mind_finite then (n+1,(n::li,lc)) else (n+1,(li,n::lc))) - (0,([],[])) (Array.to_list mipv) - in - let strind = - if mipli = [] then [<>] - else [< 'sTR "Inductive"; 'bRK(1,4); - (prlist_with_sep - (fun () -> [< 'fNL; 'sTR" with"; 'bRK(1,4) >]) - print_oneind - (List.rev mipli)); 'fNL >] - and strcoind = - if miplc = [] then [<>] - else [< 'sTR "CoInductive"; 'bRK(1,4); - (prlist_with_sep - (fun () -> [<'fNL; 'sTR " with"; 'bRK(1,4) >]) - print_oneind (List.rev miplc)); 'fNL >] - in - (hV 0 [< 'sTR"Mutual " ; - if mis_finite mis0 then - [< strind; strcoind >] - else - []; - implicit_args_msg sp mipv >]) -*) -let print_section_variable sp = - let (d,_,_) = get_variable sp in - let l = implicits_of_var sp in - [< print_named_decl d; print_impl_args l; 'fNL >] - -let print_body = function - | Some c -> prterm c - | None -> [< 'sTR"" >] - -let print_typed_body (val_0,typ) = - [< print_body val_0; 'fNL; 'sTR " : "; prtype typ; 'fNL >] - -let print_constant with_values sep sp = - let cb = Global.lookup_constant sp in - if kind_of_path sp = CCI then - let val_0 = cb.const_body in - let typ = cb.const_type in - let impls = constant_implicits_list sp in - hOV 0 [< (match val_0 with - | None -> - [< 'sTR"*** [ "; - print_basename sp; - 'sTR " : "; 'cUT ; prtype typ ; 'sTR" ]"; 'fNL >] - | _ -> - [< print_basename sp; - 'sTR sep; 'cUT ; - if with_values then - print_typed_body (val_0,typ) - else - [< prtype typ ; 'fNL >] >]); - print_impl_args impls; 'fNL >] - else - hOV 0 [< 'sTR"Fw constant " ; - print_basename sp ; 'fNL>] - -let print_inductive sp = - if kind_of_path sp = CCI then - [< print_mutual sp; 'fNL >] - else - hOV 0 [< 'sTR"Fw inductive definition "; - print_basename sp; 'fNL >] - -let print_syntactic_def sep sp = - let id = basename sp in - let c = Syntax_def.search_syntactic_definition sp in - [< 'sTR" Syntactif Definition "; pr_id id ; 'sTR sep; pr_rawterm c; 'fNL >] - -let print_leaf_entry with_values sep (sp,lobj) = - let tag = object_tag lobj in - match (sp,tag) with - | (_,"VARIABLE") -> - print_section_variable sp - | (_,("CONSTANT"|"PARAMETER")) -> - print_constant with_values sep sp - | (_,"INDUCTIVE") -> - print_inductive sp - | (_,"AUTOHINT") -> - [< 'sTR" Hint Marker"; 'fNL >] - | (_,"GRAMMAR") -> - [< 'sTR" Grammar Marker"; 'fNL >] - | (_,"SYNTAXCONSTANT") -> - print_syntactic_def sep sp - | (_,"PPSYNTAX") -> - [< 'sTR" Syntax Marker"; 'fNL >] - | (_,"TOKEN") -> - [< 'sTR" Token Marker"; 'fNL >] - | (_,"CLASS") -> - [< 'sTR" Class Marker"; 'fNL >] - | (_,"COERCION") -> - [< 'sTR" Coercion Marker"; 'fNL >] - | (_,"REQUIRE") -> - [< 'sTR" Require Marker"; 'fNL >] - | (_,"END-SECTION") -> [< >] - | (_,s) -> - [< 'sTR(string_of_path sp); 'sTR" : "; - 'sTR"Unrecognized object "; 'sTR s; 'fNL >] - -let rec print_library_entry with_values ent = - let sep = if with_values then " = " else " : " in - match ent with - | (sp,Lib.Leaf lobj) -> - [< print_leaf_entry with_values sep (sp,lobj) >] - | (_,Lib.OpenedSection (str,_)) -> - [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >] - | (sp,Lib.ClosedSection _) -> - [< 'sTR(" >>>>>>> Closed Section " ^ (string_of_id (basename sp))); - 'fNL >] - | (_,Lib.Module dir) -> - [< 'sTR(" >>>>>>> Module " ^ (string_of_dirpath dir)); 'fNL >] - | (_,Lib.FrozenState _) -> - [< >] - -and print_context with_values = - let rec prec = function - | h::rest -> [< prec rest ; print_library_entry with_values h >] - | [] -> [< >] - in - prec - -let print_full_context () = print_context true (Lib.contents_after None) - -let print_full_context_typ () = print_context false (Lib.contents_after None) - -(* For printing an inductive definition with - its constructors and elimination, - assume that the declaration of constructors and eliminations - follows the definition of the inductive type *) - -let list_filter_vec f vec = - let rec frec n lf = - if n < 0 then lf - else if f vec.(n) then - frec (n-1) (vec.(n)::lf) - else - frec (n-1) lf - in - frec (Array.length vec -1) [] - -let read_sec_context qid = - let sp, _ = Nametab.locate_module qid in - let rec get_cxt in_cxt = function - | ((sp',Lib.OpenedSection (str,_)) as hd)::rest -> - if sp' = sp then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | [] -> [] - | hd::rest -> get_cxt (hd::in_cxt) rest - in - let cxt = (Lib.contents_after None) in - List.rev (get_cxt [] cxt) - -let print_sec_context sec = print_context true (read_sec_context sec) - -let print_sec_context_typ sec = print_context false (read_sec_context sec) - -let print_judgment env {uj_val=trm;uj_type=typ} = - print_typed_value_in_env env (trm, typ) - -let print_safe_judgment env j = - let trm = Safe_typing.j_val j in - let typ = Safe_typing.j_type j in - print_typed_value_in_env env (trm, typ) - -let print_eval red_fun env {uj_val=trm;uj_type=typ} = - let ntrm = red_fun env Evd.empty trm in - [< 'sTR " = "; print_judgment env {uj_val = ntrm; uj_type = typ} >] - -let print_name qid = - try - let sp,_ = Nametab.locate_obj qid in - let (sp,lobj) = - let (sp,entry) = - List.find (fun en -> (fst en) = sp) (Lib.contents_after None) - in - match entry with - | Lib.Leaf obj -> (sp,obj) - | _ -> raise Not_found - in - print_leaf_entry true " = " (sp,lobj) - with Not_found -> - try - match Nametab.locate qid with - | ConstRef sp -> print_constant true " = " sp - | IndRef (sp,_) -> print_inductive sp - | ConstructRef ((sp,_),_) -> print_inductive sp - | VarRef sp -> print_section_variable sp - with Not_found -> - try (* Var locale de but, pas var de section... donc pas d'implicits *) - let dir,str = repr_qualid qid in - if dir <> [] then raise Not_found; - let (c,typ) = Global.lookup_named str in - [< print_named_decl (str,c,typ) >] - with Not_found -> - try - let sp = Syntax_def.locate_syntactic_definition qid in - print_syntactic_def " = " sp - with Not_found -> - errorlabstrm "print_name" - [< pr_qualid qid; 'sPC; 'sTR "not a defined object" >] - -let print_opaque_name qid = - let sigma = Evd.empty in - let env = Global.env () in - let sign = Global.named_context () in - try - let x = global_qualified_reference qid in - match kind_of_term x with - | IsConst (sp,_ as cst) -> - let cb = Global.lookup_constant sp in - if is_defined cb then - print_constant true " = " sp - else - error "not a defined constant" - | IsMutInd ((sp,_),_) -> - print_mutual sp - | IsMutConstruct cstr -> - let ty = Typeops.type_of_constructor env sigma cstr in - print_typed_value (x, ty) - | IsVar id -> - let (c,ty) = lookup_named id env in - print_named_decl (id,c,ty) - | _ -> - assert false - with Not_found -> - errorlabstrm "print_opaque" [< pr_qualid qid; 'sPC; 'sTR "not declared" >] - -let print_local_context () = - let env = Lib.contents_after None in - let rec print_var_rec = function - | [] -> [< >] - | (sp,Lib.Leaf lobj)::rest -> - if "VARIABLE" = object_tag lobj then - let (d,_,_) = get_variable sp in - [< print_var_rec rest; - print_named_decl d >] - else - print_var_rec rest - | _::rest -> print_var_rec rest - - and print_last_const = function - | (sp,Lib.Leaf lobj)::rest -> - (match object_tag lobj with - | "CONSTANT" | "PARAMETER" -> - let {const_body=val_0;const_type=typ} = - Global.lookup_constant sp in - [< print_last_const rest; - print_basename sp ;'sTR" = "; - print_typed_body (val_0,typ) >] - | "INDUCTIVE" -> - [< print_last_const rest;print_mutual sp; 'fNL >] - | "VARIABLE" -> [< >] - | _ -> print_last_const rest) - | _ -> [< >] - in - [< print_var_rec env; print_last_const env >] - -let fprint_var name typ = - [< 'sTR ("*** [" ^ name ^ " :"); fprtype typ; 'sTR "]"; 'fNL >] - -let fprint_judge {uj_val=trm;uj_type=typ} = - [< fprterm trm; 'sTR" : " ; fprterm (body_of_type typ) >] - -let unfold_head_fconst = - let rec unfrec k = match kind_of_term k with - | IsConst cst -> constant_value (Global.env ()) cst - | IsLambda (na,t,b) -> mkLambda (na,t,unfrec b) - | IsApp (f,v) -> appvect (unfrec f,v) - | _ -> k - in - unfrec - -(* for debug *) -let inspect depth = - let rec inspectrec n res env = - if n=0 or env=[] then - res - else - inspectrec (n-1) (List.hd env::res) (List.tl env) - in - let items = List.rev (inspectrec depth [] (Lib.contents_after None)) in - print_context false items - - -(*************************************************************************) -(* Pretty-printing functions coming from classops.ml *) - -open Classops - -let string_of_strength = function - | NotDeclare -> "(temp)" - | NeverDischarge -> "(global)" - | DischargeAt sp -> "(disch@"^(string_of_dirpath sp) - -let print_coercion_value v = prterm (get_coercion_value v) - -let print_index_coercion c = - let _,v = coercion_info_from_index c in - print_coercion_value v - -let print_class i = - let cl,_ = class_info_from_index i in - [< 'sTR (string_of_class cl) >] - -let print_path ((i,j),p) = - [< 'sTR"["; - prlist_with_sep (fun () -> [< 'sTR"; " >]) - (fun c -> print_index_coercion c) p; - 'sTR"] : "; print_class i; 'sTR" >-> "; - print_class j >] - -let _ = Classops.install_path_printer print_path - -let print_graph () = - [< prlist_with_sep pr_fnl print_path (inheritance_graph()) >] - -let print_classes () = - [< prlist_with_sep pr_spc - (fun (_,(cl,x)) -> - [< 'sTR (string_of_class cl) - (*; 'sTR(string_of_strength x.cl_strength) *) >]) - (classes()) >] - -let print_coercions () = - [< prlist_with_sep pr_spc - (fun (_,(_,v)) -> [< print_coercion_value v >]) (coercions()) >] - -let cl_of_id id = - match string_of_id id with - | "FUNCLASS" -> CL_FUN - | "SORTCLASS" -> CL_SORT - | _ -> let v = Declare.global_reference CCI id in - let cl,_ = constructor_at_head v in - cl - -let index_cl_of_id id = - try - let cl = cl_of_id id in - let i,_ = class_info cl in - i - with _ -> - errorlabstrm "index_cl_of_id" - [< 'sTR(string_of_id id); 'sTR" is not a defined class" >] - -let print_path_between ids idt = - let i = (index_cl_of_id ids) in - let j = (index_cl_of_id idt) in - let p = - try - lookup_path_between (i,j) - with _ -> - errorlabstrm "index_cl_of_id" - [< 'sTR"No path between ";'sTR(string_of_id ids); - 'sTR" and ";'sTR(string_of_id ids) >] - in - print_path ((i,j),p) - -(*************************************************************************) diff --git a/parsing/pretty.mli b/parsing/pretty.mli deleted file mode 100644 index b84c566348..0000000000 --- a/parsing/pretty.mli +++ /dev/null @@ -1,59 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* names_context - -val print_closed_sections : bool ref -val print_impl_args : int list -> std_ppcmds -val print_context : bool -> Lib.library_segment -> std_ppcmds -val print_library_entry : bool -> (section_path * Lib.node) -> std_ppcmds -val print_full_context : unit -> std_ppcmds -val print_full_context_typ : unit -> std_ppcmds -val print_sec_context : Nametab.qualid -> std_ppcmds -val print_sec_context_typ : Nametab.qualid -> std_ppcmds -val print_judgment : env -> unsafe_judgment -> std_ppcmds -val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds -val print_eval : - 'a reduction_function -> env -> unsafe_judgment -> std_ppcmds -(* This function is exported for the graphical user-interface pcoq *) -val build_inductive : section_path -> int -> - global_reference * rel_context * types * identifier array * types array -val print_mutual : section_path -> std_ppcmds -val print_name : Nametab.qualid -> std_ppcmds -val print_opaque_name : Nametab.qualid -> std_ppcmds -val print_local_context : unit -> std_ppcmds - -(*i -val print_extracted_name : identifier -> std_ppcmds -val print_extraction : unit -> std_ppcmds -val print_extracted_vars : unit -> std_ppcmds -i*) - -(* Pretty-printing functions for classes and coercions *) -val print_graph : unit -> std_ppcmds -val print_classes : unit -> std_ppcmds -val print_coercions : unit -> std_ppcmds -val print_path_between : identifier -> identifier -> std_ppcmds - - -val inspect : int -> std_ppcmds - diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml new file mode 100644 index 0000000000..6044767c2c --- /dev/null +++ b/parsing/prettyp.ml @@ -0,0 +1,595 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ] + +let print_typed_value x = print_typed_value_in_env (Global.env ()) x + +let pkprinters = function + | FW -> (fprterm,fprterm_env) + | CCI -> (prterm,prterm_env) + | _ -> anomaly "pkprinters" + +let print_impl_args = function + | [] -> [<>] + | [i] -> [< 'sTR"Position ["; 'iNT i; 'sTR"] is implicit" >] + | l -> + [< 'sTR"Positions ["; + prlist_with_sep (fun () -> [< 'sTR";" >]) (fun i -> [< 'iNT i >]) l; + 'sTR"] are implicit" >] + +(* To be improved; the type should be used to provide the types in the + abstractions. This should be done recursively inside prterm, so that + the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u) + synthesizes the type nat of the abstraction on u *) + +let print_named_def name body typ = + let pbody = prterm body in + let ptyp = prtype typ in + [< 'sTR "*** ["; 'sTR name ; 'sTR " "; + hOV 0 [< 'sTR ":="; 'bRK (1,2); pbody; 'sPC; + 'sTR ":"; 'bRK (1,2); ptyp >]; + 'sTR "]"; 'fNL >] + +let print_named_assum name typ = + [< 'sTR "*** [" ; 'sTR name ; 'sTR " : "; prtype typ; 'sTR "]"; 'fNL >] + +let print_named_decl (id,c,typ) = + let s = string_of_id id in + match c with + | Some body -> print_named_def s body typ + | None -> print_named_assum s typ + +let assumptions_for_print lna = + List.fold_right (fun na env -> add_name na env) lna empty_names_context + +let implicit_args_id id l = + if l = [] then + [<>] + else + [< 'sTR"For "; pr_id id; 'sTR": "; print_impl_args l ; 'fNL >] + +let implicit_args_msg sp mipv = + [< prvecti + (fun i mip -> + let imps = inductive_implicits_list (sp,i) in + [< (implicit_args_id mip.mind_typename imps); + prvecti + (fun j idc -> + let imps = constructor_implicits_list ((sp,i),succ j) in + (implicit_args_id idc imps)) + mip.mind_consnames + >]) + mipv >] + +let print_params env params = + if List.length params = 0 then + [<>] + else + [< 'sTR "["; pr_rel_context env params; 'sTR "]"; 'bRK(1,2) >] + +let print_constructors envpar names types = + let pc = + [< prvect_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >]) + (fun (id,c) -> [< pr_id id; 'sTR " : "; prterm_env envpar c >]) + (array_map2 (fun n t -> (n,t)) names types) >] + in hV 0 [< 'sTR " "; pc >] + +let build_inductive sp tyi = + let ctxt = context_of_global_reference (IndRef (sp,tyi)) in + let ctxt = Array.of_list (instance_from_section_context ctxt) in + let mis = Global.lookup_mind_specif ((sp,tyi),ctxt) in + let params = mis_params_ctxt mis in + let args = extended_rel_list 0 params in + let indf = make_ind_family (mis,args) in + let arity = get_arity_type indf in + let cstrtypes = get_constructors_types indf in + let cstrnames = mis_consnames mis in + (IndRef (sp,tyi), params, arity, cstrnames, cstrtypes) + +let print_one_inductive sp tyi = + let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in + let env = Global.env () in + let envpar = push_rels params env in + (hOV 0 + [< (hOV 0 + [< pr_global (IndRef (sp,tyi)) ; 'bRK(1,2); print_params env params; + 'sTR ": "; prterm_env envpar arity; 'sTR " :=" >]); + 'bRK(1,2); print_constructors envpar cstrnames cstrtypes >]) + +let print_mutual sp = + let mipv = (Global.lookup_mind sp).mind_packets in + if Array.length mipv = 1 then + let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp 0 in + let sfinite = + if mipv.(0).mind_finite then "Inductive " else "CoInductive " in + let env = Global.env () in + let envpar = push_rels params env in + (hOV 0 [< + 'sTR sfinite ; + pr_global (IndRef (sp,0)); 'bRK(1,2); + print_params env params; 'bRK(1,5); + 'sTR": "; prterm_env envpar arity; 'sTR" :="; + 'bRK(0,4); print_constructors envpar cstrnames cstrtypes; 'fNL; + implicit_args_msg sp mipv >] ) + (* Mutual [co]inductive definitions *) + else + let _,(mipli,miplc) = + Array.fold_right + (fun mi (n,(li,lc)) -> + if mi.mind_finite then (n+1,(n::li,lc)) else (n+1,(li,n::lc))) + mipv (0,([],[])) + in + let strind = + if mipli = [] then [<>] + else [< 'sTR "Inductive"; 'bRK(1,4); + (prlist_with_sep + (fun () -> [< 'fNL; 'sTR" with"; 'bRK(1,4) >]) + (print_one_inductive sp) mipli); 'fNL >] + and strcoind = + if miplc = [] then [<>] + else [< 'sTR "CoInductive"; 'bRK(1,4); + (prlist_with_sep + (fun () -> [<'fNL; 'sTR " with"; 'bRK(1,4) >]) + (print_one_inductive sp) miplc); 'fNL >] + in + (hV 0 [< 'sTR"Mutual " ; + if mipv.(0).mind_finite then + [< strind; strcoind >] + else + []; + implicit_args_msg sp mipv >]) + +(* + let env = Global.env () in + let evd = Evd.empty in + let {mind_packets=mipv} = mib in + (* On suppose que tous les inductifs ont les même paramètres *) + let nparams = mipv.(0).mind_nparams in + let (lpars,_) = decomp_n_prod env evd nparams + (body_of_type (mind_user_arity mipv.(0))) in + let arities = Array.map (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mipv in + let env_ar = push_rels lpars env in + let pr_constructor (id,c) = + [< pr_id id; 'sTR " : "; prterm_env env_ar c >] in + let print_constructors mis = + let (_,lC) = mis_type_mconstructs mis in + let lidC = + array_map2 (fun id c -> (id, snd (decomp_n_prod env evd nparams c))) + (mis_consnames mis) lC in + let plidC = + prvect_with_sep (fun () -> [<'bRK(0,0); 'sTR "| " >]) + pr_constructor + lidC + in + hV 0 [< 'sTR " "; plidC >] + in + let params = + if nparams = 0 then + [<>] + else + [< 'sTR "["; pr_rel_context env lpars; 'sTR "]"; 'bRK(1,2) >] in + let print_oneind tyi = + let mis = + build_mis + ((sp,tyi), + Array.of_list (instance_from_section_context mib.mind_hyps)) + mib in + let (_,arity) = decomp_n_prod env evd nparams + (body_of_type (mis_user_arity mis)) in + (hOV 0 + [< (hOV 0 + [< pr_global (IndRef (sp,tyi)) ; 'bRK(1,2); params; + 'sTR ": "; prterm_env env_ar arity; 'sTR " :=" >]); + 'bRK(1,2); print_constructors mis >]) + in + let mis0 = + build_mis + ((sp,0),Array.of_list (instance_from_section_context mib.mind_hyps)) + mib in + (* Case one [co]inductive *) + if Array.length mipv = 1 then + let (_,arity) = decomp_n_prod env evd nparams + (body_of_type (mis_user_arity mis0)) in + let sfinite = if mis_finite mis0 then "Inductive " else "CoInductive " in + (hOV 0 [< 'sTR sfinite ; pr_global (IndRef (sp,0)); + if nparams = 0 then + [<>] + else + [< 'sTR" ["; pr_rel_context env lpars; 'sTR "]">]; + 'bRK(1,5); 'sTR": "; prterm_env env_ar arity; 'sTR" :="; + 'bRK(0,4); print_constructors mis0; 'fNL; + implicit_args_msg sp mipv >] ) + (* Mutual [co]inductive definitions *) + else + let _,(mipli,miplc) = + List.fold_left + (fun (n,(li,lc)) mi -> + if mi.mind_finite then (n+1,(n::li,lc)) else (n+1,(li,n::lc))) + (0,([],[])) (Array.to_list mipv) + in + let strind = + if mipli = [] then [<>] + else [< 'sTR "Inductive"; 'bRK(1,4); + (prlist_with_sep + (fun () -> [< 'fNL; 'sTR" with"; 'bRK(1,4) >]) + print_oneind + (List.rev mipli)); 'fNL >] + and strcoind = + if miplc = [] then [<>] + else [< 'sTR "CoInductive"; 'bRK(1,4); + (prlist_with_sep + (fun () -> [<'fNL; 'sTR " with"; 'bRK(1,4) >]) + print_oneind (List.rev miplc)); 'fNL >] + in + (hV 0 [< 'sTR"Mutual " ; + if mis_finite mis0 then + [< strind; strcoind >] + else + []; + implicit_args_msg sp mipv >]) +*) +let print_section_variable sp = + let (d,_,_) = get_variable sp in + let l = implicits_of_var sp in + [< print_named_decl d; print_impl_args l; 'fNL >] + +let print_body = function + | Some c -> prterm c + | None -> [< 'sTR"" >] + +let print_typed_body (val_0,typ) = + [< print_body val_0; 'fNL; 'sTR " : "; prtype typ; 'fNL >] + +let print_constant with_values sep sp = + let cb = Global.lookup_constant sp in + if kind_of_path sp = CCI then + let val_0 = cb.const_body in + let typ = cb.const_type in + let impls = constant_implicits_list sp in + hOV 0 [< (match val_0 with + | None -> + [< 'sTR"*** [ "; + print_basename sp; + 'sTR " : "; 'cUT ; prtype typ ; 'sTR" ]"; 'fNL >] + | _ -> + [< print_basename sp; + 'sTR sep; 'cUT ; + if with_values then + print_typed_body (val_0,typ) + else + [< prtype typ ; 'fNL >] >]); + print_impl_args impls; 'fNL >] + else + hOV 0 [< 'sTR"Fw constant " ; + print_basename sp ; 'fNL>] + +let print_inductive sp = + if kind_of_path sp = CCI then + [< print_mutual sp; 'fNL >] + else + hOV 0 [< 'sTR"Fw inductive definition "; + print_basename sp; 'fNL >] + +let print_syntactic_def sep sp = + let id = basename sp in + let c = Syntax_def.search_syntactic_definition sp in + [< 'sTR" Syntactif Definition "; pr_id id ; 'sTR sep; pr_rawterm c; 'fNL >] + +let print_leaf_entry with_values sep (sp,lobj) = + let tag = object_tag lobj in + match (sp,tag) with + | (_,"VARIABLE") -> + print_section_variable sp + | (_,("CONSTANT"|"PARAMETER")) -> + print_constant with_values sep sp + | (_,"INDUCTIVE") -> + print_inductive sp + | (_,"AUTOHINT") -> + [< 'sTR" Hint Marker"; 'fNL >] + | (_,"GRAMMAR") -> + [< 'sTR" Grammar Marker"; 'fNL >] + | (_,"SYNTAXCONSTANT") -> + print_syntactic_def sep sp + | (_,"PPSYNTAX") -> + [< 'sTR" Syntax Marker"; 'fNL >] + | (_,"TOKEN") -> + [< 'sTR" Token Marker"; 'fNL >] + | (_,"CLASS") -> + [< 'sTR" Class Marker"; 'fNL >] + | (_,"COERCION") -> + [< 'sTR" Coercion Marker"; 'fNL >] + | (_,"REQUIRE") -> + [< 'sTR" Require Marker"; 'fNL >] + | (_,"END-SECTION") -> [< >] + | (_,s) -> + [< 'sTR(string_of_path sp); 'sTR" : "; + 'sTR"Unrecognized object "; 'sTR s; 'fNL >] + +let rec print_library_entry with_values ent = + let sep = if with_values then " = " else " : " in + match ent with + | (sp,Lib.Leaf lobj) -> + [< print_leaf_entry with_values sep (sp,lobj) >] + | (_,Lib.OpenedSection (str,_)) -> + [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >] + | (sp,Lib.ClosedSection _) -> + [< 'sTR(" >>>>>>> Closed Section " ^ (string_of_id (basename sp))); + 'fNL >] + | (_,Lib.Module dir) -> + [< 'sTR(" >>>>>>> Module " ^ (string_of_dirpath dir)); 'fNL >] + | (_,Lib.FrozenState _) -> + [< >] + +and print_context with_values = + let rec prec = function + | h::rest -> [< prec rest ; print_library_entry with_values h >] + | [] -> [< >] + in + prec + +let print_full_context () = print_context true (Lib.contents_after None) + +let print_full_context_typ () = print_context false (Lib.contents_after None) + +(* For printing an inductive definition with + its constructors and elimination, + assume that the declaration of constructors and eliminations + follows the definition of the inductive type *) + +let list_filter_vec f vec = + let rec frec n lf = + if n < 0 then lf + else if f vec.(n) then + frec (n-1) (vec.(n)::lf) + else + frec (n-1) lf + in + frec (Array.length vec -1) [] + +let read_sec_context qid = + let sp, _ = Nametab.locate_module qid in + let rec get_cxt in_cxt = function + | ((sp',Lib.OpenedSection (str,_)) as hd)::rest -> + if sp' = sp then (hd::in_cxt) else get_cxt (hd::in_cxt) rest + | [] -> [] + | hd::rest -> get_cxt (hd::in_cxt) rest + in + let cxt = (Lib.contents_after None) in + List.rev (get_cxt [] cxt) + +let print_sec_context sec = print_context true (read_sec_context sec) + +let print_sec_context_typ sec = print_context false (read_sec_context sec) + +let print_judgment env {uj_val=trm;uj_type=typ} = + print_typed_value_in_env env (trm, typ) + +let print_safe_judgment env j = + let trm = Safe_typing.j_val j in + let typ = Safe_typing.j_type j in + print_typed_value_in_env env (trm, typ) + +let print_eval red_fun env {uj_val=trm;uj_type=typ} = + let ntrm = red_fun env Evd.empty trm in + [< 'sTR " = "; print_judgment env {uj_val = ntrm; uj_type = typ} >] + +let print_name qid = + try + let sp,_ = Nametab.locate_obj qid in + let (sp,lobj) = + let (sp,entry) = + List.find (fun en -> (fst en) = sp) (Lib.contents_after None) + in + match entry with + | Lib.Leaf obj -> (sp,obj) + | _ -> raise Not_found + in + print_leaf_entry true " = " (sp,lobj) + with Not_found -> + try + match Nametab.locate qid with + | ConstRef sp -> print_constant true " = " sp + | IndRef (sp,_) -> print_inductive sp + | ConstructRef ((sp,_),_) -> print_inductive sp + | VarRef sp -> print_section_variable sp + with Not_found -> + try (* Var locale de but, pas var de section... donc pas d'implicits *) + let dir,str = repr_qualid qid in + if dir <> [] then raise Not_found; + let (c,typ) = Global.lookup_named str in + [< print_named_decl (str,c,typ) >] + with Not_found -> + try + let sp = Syntax_def.locate_syntactic_definition qid in + print_syntactic_def " = " sp + with Not_found -> + errorlabstrm "print_name" + [< pr_qualid qid; 'sPC; 'sTR "not a defined object" >] + +let print_opaque_name qid = + let sigma = Evd.empty in + let env = Global.env () in + let sign = Global.named_context () in + try + let x = global_qualified_reference qid in + match kind_of_term x with + | IsConst (sp,_ as cst) -> + let cb = Global.lookup_constant sp in + if is_defined cb then + print_constant true " = " sp + else + error "not a defined constant" + | IsMutInd ((sp,_),_) -> + print_mutual sp + | IsMutConstruct cstr -> + let ty = Typeops.type_of_constructor env sigma cstr in + print_typed_value (x, ty) + | IsVar id -> + let (c,ty) = lookup_named id env in + print_named_decl (id,c,ty) + | _ -> + assert false + with Not_found -> + errorlabstrm "print_opaque" [< pr_qualid qid; 'sPC; 'sTR "not declared" >] + +let print_local_context () = + let env = Lib.contents_after None in + let rec print_var_rec = function + | [] -> [< >] + | (sp,Lib.Leaf lobj)::rest -> + if "VARIABLE" = object_tag lobj then + let (d,_,_) = get_variable sp in + [< print_var_rec rest; + print_named_decl d >] + else + print_var_rec rest + | _::rest -> print_var_rec rest + + and print_last_const = function + | (sp,Lib.Leaf lobj)::rest -> + (match object_tag lobj with + | "CONSTANT" | "PARAMETER" -> + let {const_body=val_0;const_type=typ} = + Global.lookup_constant sp in + [< print_last_const rest; + print_basename sp ;'sTR" = "; + print_typed_body (val_0,typ) >] + | "INDUCTIVE" -> + [< print_last_const rest;print_mutual sp; 'fNL >] + | "VARIABLE" -> [< >] + | _ -> print_last_const rest) + | _ -> [< >] + in + [< print_var_rec env; print_last_const env >] + +let fprint_var name typ = + [< 'sTR ("*** [" ^ name ^ " :"); fprtype typ; 'sTR "]"; 'fNL >] + +let fprint_judge {uj_val=trm;uj_type=typ} = + [< fprterm trm; 'sTR" : " ; fprterm (body_of_type typ) >] + +let unfold_head_fconst = + let rec unfrec k = match kind_of_term k with + | IsConst cst -> constant_value (Global.env ()) cst + | IsLambda (na,t,b) -> mkLambda (na,t,unfrec b) + | IsApp (f,v) -> appvect (unfrec f,v) + | _ -> k + in + unfrec + +(* for debug *) +let inspect depth = + let rec inspectrec n res env = + if n=0 or env=[] then + res + else + inspectrec (n-1) (List.hd env::res) (List.tl env) + in + let items = List.rev (inspectrec depth [] (Lib.contents_after None)) in + print_context false items + + +(*************************************************************************) +(* Pretty-printing functions coming from classops.ml *) + +open Classops + +let string_of_strength = function + | NotDeclare -> "(temp)" + | NeverDischarge -> "(global)" + | DischargeAt sp -> "(disch@"^(string_of_dirpath sp) + +let print_coercion_value v = prterm (get_coercion_value v) + +let print_index_coercion c = + let _,v = coercion_info_from_index c in + print_coercion_value v + +let print_class i = + let cl,_ = class_info_from_index i in + [< 'sTR (string_of_class cl) >] + +let print_path ((i,j),p) = + [< 'sTR"["; + prlist_with_sep (fun () -> [< 'sTR"; " >]) + (fun c -> print_index_coercion c) p; + 'sTR"] : "; print_class i; 'sTR" >-> "; + print_class j >] + +let _ = Classops.install_path_printer print_path + +let print_graph () = + [< prlist_with_sep pr_fnl print_path (inheritance_graph()) >] + +let print_classes () = + [< prlist_with_sep pr_spc + (fun (_,(cl,x)) -> + [< 'sTR (string_of_class cl) + (*; 'sTR(string_of_strength x.cl_strength) *) >]) + (classes()) >] + +let print_coercions () = + [< prlist_with_sep pr_spc + (fun (_,(_,v)) -> [< print_coercion_value v >]) (coercions()) >] + +let cl_of_id id = + match string_of_id id with + | "FUNCLASS" -> CL_FUN + | "SORTCLASS" -> CL_SORT + | _ -> let v = Declare.global_reference CCI id in + let cl,_ = constructor_at_head v in + cl + +let index_cl_of_id id = + try + let cl = cl_of_id id in + let i,_ = class_info cl in + i + with _ -> + errorlabstrm "index_cl_of_id" + [< 'sTR(string_of_id id); 'sTR" is not a defined class" >] + +let print_path_between ids idt = + let i = (index_cl_of_id ids) in + let j = (index_cl_of_id idt) in + let p = + try + lookup_path_between (i,j) + with _ -> + errorlabstrm "index_cl_of_id" + [< 'sTR"No path between ";'sTR(string_of_id ids); + 'sTR" and ";'sTR(string_of_id ids) >] + in + print_path ((i,j),p) + +(*************************************************************************) diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli new file mode 100644 index 0000000000..b84c566348 --- /dev/null +++ b/parsing/prettyp.mli @@ -0,0 +1,59 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* names_context + +val print_closed_sections : bool ref +val print_impl_args : int list -> std_ppcmds +val print_context : bool -> Lib.library_segment -> std_ppcmds +val print_library_entry : bool -> (section_path * Lib.node) -> std_ppcmds +val print_full_context : unit -> std_ppcmds +val print_full_context_typ : unit -> std_ppcmds +val print_sec_context : Nametab.qualid -> std_ppcmds +val print_sec_context_typ : Nametab.qualid -> std_ppcmds +val print_judgment : env -> unsafe_judgment -> std_ppcmds +val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds +val print_eval : + 'a reduction_function -> env -> unsafe_judgment -> std_ppcmds +(* This function is exported for the graphical user-interface pcoq *) +val build_inductive : section_path -> int -> + global_reference * rel_context * types * identifier array * types array +val print_mutual : section_path -> std_ppcmds +val print_name : Nametab.qualid -> std_ppcmds +val print_opaque_name : Nametab.qualid -> std_ppcmds +val print_local_context : unit -> std_ppcmds + +(*i +val print_extracted_name : identifier -> std_ppcmds +val print_extraction : unit -> std_ppcmds +val print_extracted_vars : unit -> std_ppcmds +i*) + +(* Pretty-printing functions for classes and coercions *) +val print_graph : unit -> std_ppcmds +val print_classes : unit -> std_ppcmds +val print_coercions : unit -> std_ppcmds +val print_path_between : identifier -> identifier -> std_ppcmds + + +val inspect : int -> std_ppcmds + diff --git a/parsing/search.ml b/parsing/search.ml index a4053757ff..2b9a5dd448 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -18,7 +18,6 @@ open Libobject open Declare open Coqast open Astterm -open Pretty open Environ open Pattern open Printer diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 43bd3c7497..18cd475cde 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -339,7 +339,6 @@ let pr_subgoals_existential sigma = function open Ast open Termast -open Pretty let ast_of_cvt_bind f = function | (NoDep n,c) -> ope ("BINDING", [(num n); ope ("COMMAND",[(f c)])]) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index e18887fa56..eaa6bcb31d 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -23,7 +23,6 @@ open Clenv open Pattern open Evar_refiner open Wcclausenv -open Pretty (******************************************) (* Basic Tacticals *) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e9194d8a85..d044232b6c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -22,7 +22,6 @@ open Type_errors open Reduction open Cases open Logic -open Pretty open Printer open Ast diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8d684633b8..1010ec1c38 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -27,7 +27,7 @@ open Vernacinterp open Coqast open Ast open Astterm -open Pretty +open Prettyp open Printer open Tacinterp open Tactic_debug @@ -1383,26 +1383,26 @@ let _ = let _ = add "PrintGRAPH" (function - | [] -> (fun () -> pPNL (Pretty.print_graph())) + | [] -> (fun () -> pPNL (Prettyp.print_graph())) | _ -> bad_vernac_args "PrintGRAPH") let _ = add "PrintCLASSES" (function - | [] -> (fun () -> pPNL (Pretty.print_classes())) + | [] -> (fun () -> pPNL (Prettyp.print_classes())) | _ -> bad_vernac_args "PrintCLASSES") let _ = add "PrintCOERCIONS" (function - | [] -> (fun () -> pPNL (Pretty.print_coercions())) + | [] -> (fun () -> pPNL (Prettyp.print_coercions())) | _ -> bad_vernac_args "PrintCOERCIONS") let _ = add "PrintPATH" (function | [VARG_IDENTIFIER ids;VARG_IDENTIFIER idt] -> - (fun () -> pPNL (Pretty.print_path_between ids idt)) + (fun () -> pPNL (Prettyp.print_path_between ids idt)) | _ -> bad_vernac_args "PrintPATH") (* Meta-syntax commands *) -- cgit v1.2.3