diff options
| -rw-r--r-- | parsing/prettyp.ml | 44 | ||||
| -rw-r--r-- | parsing/prettyp.mli | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 10 |
3 files changed, 51 insertions, 4 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 64953592b..a95fb67f9 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -314,10 +314,10 @@ let print_mutual sp = let (mib,mip) = Global.lookup_inductive (sp,0) in let mipv = mib.mind_packets in let names = list_tabulate (fun x -> (sp,x)) (Array.length mipv) in - pr_mutual_inductive mib.mind_finite names ++ + pr_mutual_inductive mib.mind_finite names (* ++ print_inductive_implicit_args sp mipv ++ print_inductive_argument_scopes sp mipv - +*) let print_section_variable sp = let d = get_variable sp in print_named_decl d ++ @@ -328,7 +328,7 @@ let print_body = function | None -> (str"<no body>") let print_typed_body (val_0,typ) = - (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ ++ fnl ()) + (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ ++ fnl ()) let ungeneralized_type_of_constant_type = function | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level) @@ -421,6 +421,44 @@ let print_full_context () = let print_full_context_typ () = print_context false None (Lib.contents_after None) +let print_full_pure_context () = + let rec prec = function + | ((_,kn),Lib.Leaf lobj)::rest -> + let pp = match object_tag lobj with + | "CONSTANT" -> + let con = constant_of_kn kn in + let cb = Global.lookup_constant con in + let val_0 = cb.const_body in + let typ = ungeneralized_type_of_constant_type cb.const_type in + hov 0 ( + match val_0 with + | None -> + str (if cb.const_opaque then "Axiom " else "Parameter ") ++ + print_basename con ++ str " : " ++ cut () ++ pr_ltype typ + | Some v -> + if cb.const_opaque then + str "Theorem " ++ print_basename con ++ cut () ++ + str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ + str "Proof " ++ print_body val_0 + else + str "Definition " ++ print_basename con ++ cut () ++ + str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ + print_body val_0) ++ str "." ++ fnl () ++ fnl () + | "INDUCTIVE" -> + print_inductive kn ++ str "." ++ fnl () ++ fnl () + | "MODULE" -> + (* TODO: make it reparsable *) + let (mp,_,l) = repr_kn kn in + print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + | "MODULE TYPE" -> + (* TODO: make it reparsable *) + print_modtype kn ++ str "." ++ fnl () ++ fnl () + | _ -> mt () in + prec rest ++ pp + | _::rest -> prec rest + | _ -> mt () in + prec (Lib.contents_after None) + (* For printing an inductive definition with its constructors and elimination, assume that the declaration of constructors and eliminations diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index f23cc38ac..8cd2f9658 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -30,6 +30,7 @@ val print_context : bool -> int option -> Lib.library_segment -> std_ppcmds val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option val print_full_context : unit -> std_ppcmds val print_full_context_typ : unit -> std_ppcmds +val print_full_pure_context : unit -> std_ppcmds val print_sec_context : reference -> std_ppcmds val print_sec_context_typ : reference -> std_ppcmds val print_judgment : env -> unsafe_judgment -> std_ppcmds diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 763ed91f1..94c6ed1f5 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -32,6 +32,8 @@ let print_header () = Printf.printf "Welcome to Coq %s (%s)\n" ver rev; flush stdout +let output_context = ref false + let memory_stat = ref false let print_memory_stat () = @@ -272,6 +274,8 @@ let parse_args is_ide = | "-xml" :: rem -> Options.xml_export := true; parse rem + | "-output-context" :: rem -> output_context := true; parse rem + (* Scanned in Options! *) | "-v7" :: rem -> error "This version of Coq does not support v7 syntax" | "-v8" :: rem -> parse rem @@ -329,7 +333,11 @@ let init is_ide = msgnl (Toplevel.print_toplevel_error e); exit 1 end; - if !batch_mode then (flush_all(); Profile.print_profile (); exit 0); + if !batch_mode then + (flush_all(); + if !output_context then Pp.ppnl (Prettyp.print_full_pure_context ()); + Profile.print_profile (); + exit 0); Lib.declare_initial_state () let init_ide () = init true; List.rev !ide_args |