summaryrefslogtreecommitdiff
path: root/parsing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/printer.ml')
-rw-r--r--parsing/printer.ml249
1 files changed, 249 insertions, 0 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
new file mode 100644
index 00000000..dfacc764
--- /dev/null
+++ b/parsing/printer.ml
@@ -0,0 +1,249 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: printer.ml,v 1.58.2.1 2004/07/16 19:30:40 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Sign
+open Environ
+open Global
+open Declare
+open Coqast
+open Ast
+open Termast
+open Libnames
+open Extend
+open Nametab
+open Ppconstr
+
+let emacs_str s = if !Options.print_emacs then s else ""
+
+(**********************************************************************)
+(* Old Ast printing *)
+
+let constr_syntax_universe = "constr"
+(* This is starting precedence for printing constructions or tactics *)
+(* Level 9 means no parentheses except for applicative terms (at level 10) *)
+let constr_initial_prec_v7 = Some (9,Ppextend.L)
+let constr_initial_prec = Some (200,Ppextend.E)
+
+let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;
+
+let global_const_name kn =
+ try pr_global Idset.empty (ConstRef kn)
+ with Not_found -> (* May happen in debug *)
+ (str ("CONST("^(string_of_kn kn)^")"))
+
+let global_var_name id =
+ try pr_global Idset.empty (VarRef id)
+ with Not_found -> (* May happen in debug *)
+ (str ("SECVAR("^(string_of_id id)^")"))
+
+let global_ind_name (kn,tyi) =
+ try pr_global Idset.empty (IndRef (kn,tyi))
+ with Not_found -> (* May happen in debug *)
+ (str ("IND("^(string_of_kn kn)^","^(string_of_int tyi)^")"))
+
+let global_constr_name ((kn,tyi),i) =
+ try pr_global Idset.empty (ConstructRef ((kn,tyi),i))
+ with Not_found -> (* May happen in debug *)
+ (str ("CONSTRUCT("^(string_of_kn kn)^","^(string_of_int tyi)
+ ^","^(string_of_int i)^")"))
+
+let globpr gt = match gt with
+ | Nvar(_,s) -> (pr_id s)
+ | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
+ | Node(_,"CONST",[Path(_,sl)]) ->
+ global_const_name (section_path sl)
+ | Node(_,"SECVAR",[Nvar(_,s)]) ->
+ global_var_name s
+ | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
+ global_ind_name (section_path sl, tyi)
+ | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
+ global_constr_name ((section_path sl, tyi), i)
+ | Dynamic(_,d) ->
+ if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>")
+ else dfltpr gt
+ | gt -> dfltpr gt
+
+
+let wrap_exception = function
+ Anomaly (s1,s2) ->
+ warning ("Anomaly ("^s1^")"); pp s2;
+ str"<PP error: non-printable term>"
+ | Failure _ | UserError _ | Not_found ->
+ str"<PP error: non-printable term>"
+ | s -> raise s
+
+let gentermpr_fail gt =
+ let prec =
+ if !Options.v7 then constr_initial_prec_v7 else constr_initial_prec in
+ Esyntax.genprint globpr constr_syntax_universe prec gt
+
+let gentermpr gt =
+ try gentermpr_fail gt
+ with s -> wrap_exception s
+
+(**********************************************************************)
+(* Generic printing: choose old or new printers *)
+
+(* [at_top] means ids of env must be avoided in bound variables *)
+let gentermpr_core at_top env t =
+ if !Options.v7 then gentermpr (Termast.ast_of_constr at_top env t)
+ else Ppconstrnew.pr_lconstr (Constrextern.extern_constr at_top env t)
+let pr_cases_pattern t =
+ if !Options.v7 then gentermpr (Termast.ast_of_cases_pattern t)
+ else Ppconstrnew.pr_cases_pattern
+ (Constrextern.extern_cases_pattern Idset.empty t)
+let pr_pattern_env tenv env t =
+ if !Options.v7 then gentermpr (Termast.ast_of_pattern tenv env t)
+ else Ppconstrnew.pr_constr
+ (Constrextern.extern_pattern tenv env t)
+
+(**********************************************************************)
+(* Derived printers *)
+
+let prterm_env_at_top env = gentermpr_core true env
+let prterm_env env = gentermpr_core false env
+let prtype_env env typ = prterm_env env typ
+let prjudge_env env j =
+ (prterm_env env j.uj_val, prterm_env env j.uj_type)
+
+(* NB do not remove the eta-redexes! Global.env() has side-effects... *)
+let prterm t = prterm_env (Global.env()) t
+let prtype t = prtype_env (Global.env()) t
+let prjudge j = prjudge_env (Global.env()) j
+
+let pr_constant env cst = prterm_env env (mkConst cst)
+let pr_existential env ev = prterm_env env (mkEvar ev)
+let pr_inductive env ind = prterm_env env (mkInd ind)
+let pr_constructor env cstr = prterm_env env (mkConstruct cstr)
+let pr_global = pr_global Idset.empty
+
+let pr_rawterm t =
+ if !Options.v7 then gentermpr (Termast.ast_of_rawconstr t)
+ else Ppconstrnew.pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)
+
+open Pattern
+let pr_ref_label = function (* On triche sur le contexte *)
+ | ConstNode sp -> pr_constant (Global.env()) sp
+ | IndNode sp -> pr_inductive (Global.env()) sp
+ | CstrNode sp -> pr_constructor (Global.env()) sp
+ | VarNode id -> pr_id id
+
+let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t
+
+let pr_var_decl env (id,c,typ) =
+ let pbody = match c with
+ | None -> (mt ())
+ | Some c ->
+ (* Force evaluation *)
+ let pb = prterm_env env c in
+ (str" := " ++ pb ++ cut () ) in
+ let pt = prtype_env env typ in
+ let ptyp = (str" : " ++ pt) in
+ (pr_id id ++ hov 0 (pbody ++ ptyp))
+
+let pr_rel_decl env (na,c,typ) =
+ let pbody = match c with
+ | None -> mt ()
+ | Some c ->
+ (* Force evaluation *)
+ let pb = prterm_env env c in
+ (str":=" ++ spc () ++ pb ++ spc ()) in
+ let ptyp = prtype_env env typ in
+ match na with
+ | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+ | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+
+
+(* Prints out an "env" in a nice format. We print out the
+ * signature,then a horizontal bar, then the debruijn environment.
+ * It's printed out from outermost to innermost, so it's readable. *)
+
+(* Prints a signature, all declarations on the same line if possible *)
+let pr_named_context_of env =
+ hv 0 (fold_named_context
+ (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d)
+ env ~init:(mt ()))
+
+let pr_rel_context env rel_context =
+ let rec prec env = function
+ | [] -> (mt ())
+ | [b] ->
+ if !Options.v7 then pr_rel_decl env b
+ else str "(" ++ pr_rel_decl env b ++ str")"
+ | b::rest ->
+ let pb = pr_rel_decl env b in
+ let penvtl = prec (push_rel b env) rest in
+ if !Options.v7 then
+ (pb ++ str";" ++ spc () ++ penvtl)
+ else
+ (str "(" ++ pb ++ str")" ++ spc () ++ penvtl)
+ in
+ hov 0 (prec env (List.rev rel_context))
+
+(* Prints an env (variables and de Bruijn). Separator: newline *)
+let pr_context_unlimited env =
+ let sign_env =
+ fold_named_context
+ (fun env d pps ->
+ let pidt = pr_var_decl env d in (pps ++ fnl () ++ pidt))
+ env ~init:(mt ())
+ in
+ let db_env =
+ fold_rel_context
+ (fun env d pps ->
+ let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat))
+ env ~init:(mt ())
+ in
+ (sign_env ++ db_env)
+
+let pr_ne_context_of header env =
+ if Environ.rel_context env = empty_rel_context &
+ Environ.named_context env = empty_named_context then (mt ())
+ else let penv = pr_context_unlimited env in (header ++ penv ++ fnl ())
+
+let pr_context_limit n env =
+ let named_context = Environ.named_context env in
+ let lgsign = List.length named_context in
+ if n >= lgsign then
+ pr_context_unlimited env
+ else
+ let k = lgsign-n in
+ let _,sign_env =
+ fold_named_context
+ (fun env d (i,pps) ->
+ if i < k then
+ (i+1, (pps ++str "."))
+ else
+ let pidt = pr_var_decl env d in
+ (i+1, (pps ++ fnl () ++
+ str (emacs_str (String.make 1 (Char.chr 253))) ++
+ pidt)))
+ env ~init:(0,(mt ()))
+ in
+ let db_env =
+ fold_rel_context
+ (fun env d pps ->
+ let pnat = pr_rel_decl env d in
+ (pps ++ fnl () ++
+ str (emacs_str (String.make 1 (Char.chr 253))) ++
+ pnat))
+ env ~init:(mt ())
+ in
+ (sign_env ++ db_env)
+
+let pr_context_of env = match Options.print_hyps_limit () with
+ | None -> hv 0 (pr_context_unlimited env)
+ | Some n -> hv 0 (pr_context_limit n env)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-12 11:00:04 +0000