summaryrefslogtreecommitdiff
path: root/parsing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/printer.ml')
-rw-r--r--parsing/printer.ml377
1 files changed, 253 insertions, 124 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
index dfacc764..82676b79 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: printer.ml,v 1.58.2.1 2004/07/16 19:30:40 herbelin Exp $ *)
+(* $Id: printer.ml 7855 2006-01-12 08:21:57Z herbelin $ *)
open Pp
open Util
@@ -18,139 +18,100 @@ open Sign
open Environ
open Global
open Declare
-open Coqast
-open Ast
-open Termast
open Libnames
-open Extend
open Nametab
open Ppconstr
+open Evd
+open Proof_type
+open Refiner
+open Pfedit
+open Ppconstr
+open Constrextern
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
+(** Terms *)
-(**********************************************************************)
-(* Generic printing: choose old or new printers *)
+ (* [at_top] means ids of env must be avoided in bound variables *)
+let pr_constr_core at_top env t =
+ pr_constr_expr (extern_constr at_top env t)
+let pr_lconstr_core at_top env t =
+ pr_lconstr_expr (extern_constr at_top env t)
+
+let pr_lconstr_env_at_top env = pr_lconstr_core true env
+let pr_lconstr_env env = pr_lconstr_core false env
+let pr_constr_env env = pr_constr_core false env
+
+ (* NB do not remove the eta-redexes! Global.env() has side-effects... *)
+let pr_lconstr t = pr_lconstr_env (Global.env()) t
+let pr_constr t = pr_constr_env (Global.env()) t
+
+let pr_type_core at_top env t =
+ pr_constr_expr (extern_type at_top env t)
+let pr_ltype_core at_top env t =
+ pr_lconstr_expr (extern_type at_top env t)
+
+let pr_ltype_env_at_top env = pr_ltype_core true env
+let pr_ltype_env env = pr_ltype_core false env
+let pr_type_env env = pr_type_core false env
+
+let pr_ltype t = pr_ltype_env (Global.env()) t
+let pr_type t = pr_type_env (Global.env()) t
+
+let pr_ljudge_env env j =
+ (pr_lconstr_env env j.uj_val, pr_lconstr_env env j.uj_type)
+
+let pr_ljudge j = pr_ljudge_env (Global.env()) j
+
+let pr_lrawconstr_env env c =
+ pr_lconstr_expr (extern_rawconstr (vars_of_env env) c)
+let pr_rawconstr_env env c =
+ pr_constr_expr (extern_rawconstr (vars_of_env env) c)
+
+let pr_lrawconstr c =
+ pr_lconstr_expr (extern_rawconstr Idset.empty c)
+let pr_rawconstr c =
+ pr_constr_expr (extern_rawconstr Idset.empty c)
-(* [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)
+ pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
+
+let pr_constr_pattern_env env c =
+ pr_constr_expr (extern_constr_pattern (names_of_rel_context env) c)
+let pr_constr_pattern t =
+ pr_constr_expr (extern_constr_pattern empty_names_context t)
+
+let _ = Termops.set_print_constr pr_lconstr_env
(**********************************************************************)
-(* 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
+(* Global references *)
+
+let pr_global_env = pr_global_env
+let pr_global = pr_global_env Idset.empty
+
+let pr_constant env cst = pr_global_env (vars_of_env env) (ConstRef cst)
+let pr_existential env ev = pr_lconstr_env env (mkEvar ev)
+let pr_inductive env ind = pr_lconstr_env env (mkInd ind)
+let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
+
+let pr_evaluable_reference ref =
+ let ref' = match ref with
+ | EvalConstRef const -> ConstRef const
+ | EvalVarRef sp -> VarRef sp in
+ pr_global ref'
+
+(**********************************************************************)
+(* Contexts and declarations *)
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
+ let pb = pr_lconstr_env env c in
(str" := " ++ pb ++ cut () ) in
- let pt = prtype_env env typ in
+ let pt = pr_ltype_env env typ in
let ptyp = (str" : " ++ pt) in
(pr_id id ++ hov 0 (pbody ++ ptyp))
@@ -159,9 +120,9 @@ let pr_rel_decl env (na,c,typ) =
| None -> mt ()
| Some c ->
(* Force evaluation *)
- let pb = prterm_env env c in
+ let pb = pr_lconstr_env env c in
(str":=" ++ spc () ++ pb ++ spc ()) in
- let ptyp = prtype_env env typ in
+ let ptyp = pr_ltype_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)
@@ -177,22 +138,25 @@ let pr_named_context_of env =
(fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d)
env ~init:(mt ()))
+let pr_named_context env ne_context =
+ hv 0 (Sign.fold_named_context
+ (fun d pps -> pps ++ ws 2 ++ pr_var_decl env d)
+ ne_context ~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] -> 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)
+ str "(" ++ pb ++ str")" ++ spc () ++ penvtl
in
hov 0 (prec env (List.rev rel_context))
+let pr_rel_context_of env =
+ pr_rel_context env (rel_context env)
+
(* Prints an env (variables and de Bruijn). Separator: newline *)
let pr_context_unlimited env =
let sign_env =
@@ -247,3 +211,168 @@ let pr_context_limit n 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)
+
+
+(* display complete goal *)
+let pr_goal g =
+ let env = evar_env g in
+ let penv = pr_context_of env in
+ let pc = pr_ltype_env_at_top env g.evar_concl in
+ str" " ++ hv 0 (penv ++ fnl () ++
+ str (emacs_str (String.make 1 (Char.chr 253))) ++
+ str "============================" ++ fnl () ++
+ str" " ++ pc) ++ fnl ()
+
+(* display the conclusion of a goal *)
+let pr_concl n g =
+ let env = evar_env g in
+ let pc = pr_ltype_env_at_top env g.evar_concl in
+ str (emacs_str (String.make 1 (Char.chr 253))) ++
+ str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc
+
+(* display evar type: a context and a type *)
+let pr_evgl_sign gl =
+ let ps = pr_named_context_of (evar_env gl) in
+ let pc = pr_lconstr gl.evar_concl in
+ hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]")
+
+(* Print an enumerated list of existential variables *)
+let rec pr_evars_int i = function
+ | [] -> (mt ())
+ | (ev,evd)::rest ->
+ let pegl = pr_evgl_sign evd in
+ let pei = pr_evars_int (i+1) rest in
+ (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
+ str (string_of_existential ev) ++ str " : " ++ pegl)) ++
+ fnl () ++ pei
+
+let pr_subgoal n =
+ let rec prrec p = function
+ | [] -> error "No such goal"
+ | g::rest ->
+ if p = 1 then
+ let pg = pr_goal g in
+ v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg)
+ else
+ prrec (p-1) rest
+ in
+ prrec n
+
+(* Print open subgoals. Checks for uninstantiated existential variables *)
+let pr_subgoals sigma = function
+ | [] ->
+ let exl = Evarutil.non_instantiated sigma in
+ if exl = [] then
+ (str"Proof completed." ++ fnl ())
+ else
+ let pei = pr_evars_int 1 exl in
+ (str "No more subgoals but non-instantiated existential " ++
+ str "variables :" ++fnl () ++ (hov 0 pei))
+ | [g] ->
+ let pg = pr_goal g in
+ v 0 (str ("1 "^"subgoal") ++cut () ++ pg)
+ | g1::rest ->
+ let rec pr_rec n = function
+ | [] -> (mt ())
+ | g::rest ->
+ let pc = pr_concl n g in
+ let prest = pr_rec (n+1) rest in
+ (cut () ++ pc ++ prest)
+ in
+ let pg1 = pr_goal g1 in
+ let prest = pr_rec 2 rest in
+ v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut ()
+ ++ pg1 ++ prest ++ fnl ())
+
+
+let pr_subgoals_of_pfts pfts =
+ let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in
+ let sigma = (top_goal_of_pftreestate pfts).sigma in
+ pr_subgoals sigma gls
+
+let pr_open_subgoals () =
+ let pfts = get_pftreestate () in
+ match focus() with
+ | 0 ->
+ pr_subgoals_of_pfts pfts
+ | n ->
+ let pf = proof_of_pftreestate pfts in
+ let gls = fst (frontier pf) in
+ assert (n > List.length gls);
+ if List.length gls < 2 then
+ pr_subgoal n gls
+ else
+ v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
+ pr_subgoal n gls)
+
+let pr_nth_open_subgoal n =
+ let pf = proof_of_pftreestate (get_pftreestate ()) in
+ pr_subgoal n (fst (frontier pf))
+
+(* Elementary tactics *)
+
+let pr_prim_rule = function
+ | Intro id ->
+ str"intro " ++ pr_id id
+
+ | Intro_replacing id ->
+ (str"intro replacing " ++ pr_id id)
+
+ | Cut (b,id,t) ->
+ if b then
+ (str"assert " ++ pr_constr t)
+ else
+ (str"cut " ++ pr_constr t ++ str ";[intro " ++ pr_id id ++ str "|idtac]")
+
+ | FixRule (f,n,[]) ->
+ (str"fix " ++ pr_id f ++ str"/" ++ int n)
+
+ | FixRule (f,n,others) ->
+ let rec print_mut = function
+ | (f,n,ar)::oth ->
+ pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
+ | [] -> mt () in
+ (str"fix " ++ pr_id f ++ str"/" ++ int n ++
+ str" with " ++ print_mut others)
+
+ | Cofix (f,[]) ->
+ (str"cofix " ++ pr_id f)
+
+ | Cofix (f,others) ->
+ let rec print_mut = function
+ | (f,ar)::oth ->
+ (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
+ | [] -> mt () in
+ (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others)
+
+ | Refine c ->
+ str(if occur_meta c then "refine " else "exact ") ++
+ Constrextern.with_meta_as_hole pr_constr c
+
+ | Convert_concl (c,_) ->
+ (str"change " ++ pr_constr c)
+
+ | Convert_hyp (id,None,t) ->
+ (str"change " ++ pr_constr t ++ spc () ++ str"in " ++ pr_id id)
+
+ | Convert_hyp (id,Some c,t) ->
+ (str"change " ++ pr_constr c ++ spc () ++ str"in "
+ ++ pr_id id ++ str" (type of " ++ pr_id id ++ str ")")
+
+ | Thin ids ->
+ (str"clear " ++ prlist_with_sep pr_spc pr_id ids)
+
+ | ThinBody ids ->
+ (str"clearbody " ++ prlist_with_sep pr_spc pr_id ids)
+
+ | Move (withdep,id1,id2) ->
+ (str (if withdep then "dependent " else "") ++
+ str"move " ++ pr_id id1 ++ str " after " ++ pr_id id2)
+
+ | Rename (id1,id2) ->
+ (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
+
+(* Backwards compatibility *)
+
+let prterm = pr_lconstr
+