diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include.ml | 60 | ||||
| -rw-r--r-- | dev/include.ml | 21 | ||||
| -rw-r--r-- | dev/top_printers.ml | 109 |
3 files changed, 190 insertions, 0 deletions
diff --git a/dev/base_include.ml b/dev/base_include.ml new file mode 100644 index 0000000000..8964873eb0 --- /dev/null +++ b/dev/base_include.ml @@ -0,0 +1,60 @@ + +(* File to include to get some Coq facilities under the ocaml toplevel. + This file is loaded by include.ml *) + +(* We only assume that the variable COQTOP is set *) +let src_dir = + let coqtop = try Sys.getenv "COQTOP" with Not_found -> "." in + let coqtop = + if Sys.file_exists coqtop then + coqtop + else begin + print_endline ("Cannot find the sources in "^coqtop); + print_string "Where are they ? "; + read_line () + end + in + let add_dir dl = + Topdirs.dir_directory (List.fold_left Filename.concat "" dl) + in + List.iter add_dir + [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; + [ "pretyping" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ]; + [ "toplevel" ] ]; + coqtop +;; +(* Now Coq_config.cmi is accessible *) +Topdirs.dir_directory Coq_config.camlp4lib;; + +#use "top_printers.ml";; + +#install_printer (* identifier *) prid;; +#install_printer (* section_path *) prsp;; + +(* parsing of terms *) + +let parse_com = Pcoq.parse_string Pcoq.Command.command;; +let parse_tac = Pcoq.parse_string Pcoq.Tactic.tactic;; + +(* For compatibility reasons *) +let parse_ast = parse_com;; + +(* build a term of type constr without type-checking or resolution of + implicit syntax *) + +let raw_constr_of_string s = + Astterm.dbize_cci Evd.empty (unitize_env (Global.context())) + (parse_ast s);; + +let e s = + constr_of_com Evd.empty (Global.env()) (parse_ast s);; + +(* Get the current goal *) + +let getgoal x = top_goal_of_pftreestate (get_pftreestate x);; + +let get_nth_goal n = nth_goal_of_pftreestate n (get_pftreestate ());; +let current_goal () = get_nth_goal 1;; + +let pf_e gl s = + constr_of_com (project gl) (pf_env gl) (parse_ast s);; diff --git a/dev/include.ml b/dev/include.ml new file mode 100644 index 0000000000..ae7b8b90a9 --- /dev/null +++ b/dev/include.ml @@ -0,0 +1,21 @@ + +(* File to include to install the pretty-printers in the ocaml toplevel *) + +#use "base_include.ml";; + +#install_printer (* ast *) prast;; +#install_printer (* pat *) prastpat;; +#install_printer (* patlist *) prastpatl;; +#install_printer (* constr *) ppterm0;; +#install_printer (* type_judgement*) pptype;; +#install_printer (* judgement*) prj;; +#install_printer (* goal *) prgoal;; +#install_printer (* sigma goal *) prsigmagoal;; +#install_printer (* ctxt *) prctxt;; +#install_printer (* proof *) pproof;; +#install_printer (* global_constraints *) prevd;; +#install_printer (* readable_constraints *) prevc;; +#install_printer (* walking_constraints *) prwc;; +#install_printer (* universe *) print_uni;; +#install_printer (* universes *) pp_universes;; +#install_printer (* clenv *) prclenv;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml new file mode 100644 index 0000000000..a63be4447d --- /dev/null +++ b/dev/top_printers.ml @@ -0,0 +1,109 @@ + +(* Printers for the ocaml toplevel. *) + +open System +open Pp +open Coqast +open Ast +open Lexer +open Egrammar +open Names +open Sign +open Univ +open Generic +open Term +open Sosub +open Proof_trees +open Summary +open Libobject +open Library +open Environ +open Termast +open Printer +open Closure +open Reduction +open Typing +open Astterm +open States +open Constant +open Inductive +open Discharge +open Command +open Pretty +open Refiner +open Tacmach +open Pfedit +open Clenv +open Tactics +open Tacticals +open Elim +open Tacinterp +open Tacentries +open Vernacinterp +open Vernacentries +open Vernac +open Toplevel +open Mltop +open Esyntax +open Metasyntax + + +let pP s = pP (hOV 0 s) + +let prast c = pP(print_ast c) + +let prastpat c = pP(print_astpat c) +let prastpatl c = pP(print_astlpat c) +let ppterm0 = (fun x -> pP(term0 (gLOB nil_sign) x)) +let pptype = (fun x -> pP(prtype x)) + +let prid id = pP [< 'sTR"#" ; 'sTR(string_of_id id) >] + +let prconst (sp,j) = + pP [< 'sTR"#"; 'sTR(string_of_path sp); + 'sTR"="; term0 (gLOB nil_sign) j.uj_val >] + +let prvar ((id,a)) = + pP [< 'sTR"#" ; 'sTR(string_of_id id) ; 'sTR":" ; + term0 (gLOB nil_sign) a >] + +let genprj f j = [< (f (gLOB nil_sign)j.uj_val); + 'sTR " : "; + (f (gLOB nil_sign)j.uj_type); + 'sTR " : "; + (f (gLOB nil_sign)j.uj_kind)>] + +let prj j = pP (genprj term0 j) + + +let prsp sp = pP[< 'sTR(string_of_path sp) >] + +let prgoal g = pP(prgl g) + +let prsigmagoal g = pP(prgl (sig_it g)) + +let prgls gls = pP(pr_gls gls) + +let prglls glls = pP(pr_glls glls) + +let prctxt ctxt = pP(pr_ctxt ctxt) + +let pproof p = pP(print_proof Evd.empty nil_sign p) + +let prevd evd = pP(pr_decls evd) + +let prevc evc = pP(pr_evc evc) + +let prwc wc = pP(pr_evc wc) + +let prclenv clenv = pP(pr_clenv clenv) + +let p_uni u = + [< 'sTR(string_of_path u.u_sp) ; + 'sTR "." ; + 'iNT u.u_num >] + +let print_uni u = (pP (p_uni u)) + +let pp_universes u = pP [< 'sTR"[" ; pr_universes u ; 'sTR"]" >] + |