diff options
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 151 |
1 files changed, 74 insertions, 77 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 89bbdb2e9a..da78f8352e 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -86,28 +86,28 @@ let gentermpr gt = (* [at_top] means ids of env must be avoided in bound variables *) let gentermpr_core at_top env t = - gentermpr (Termast.ast_of_constr at_top (unitize_env env) t) + gentermpr (Termast.ast_of_constr at_top env t) let prterm_env_at_top env = gentermpr_core true env let prterm_env env = gentermpr_core false env -let prterm = prterm_env (gLOB nil_sign) +let prterm = prterm_env empty_env let prtype_env env typ = prterm_env env (incast_type typ) -let prtype = prtype_env (gLOB nil_sign) +let prtype = prtype_env empty_env let prjudge_env env j = (prterm_env env j.uj_val, prterm_env env (incast_type j.uj_type)) -let prjudge = prjudge_env (gLOB nil_sign) +let prjudge = prjudge_env empty_env (* Plus de "k"... let gentermpr k = gentermpr_core false let gentermpr_at_top k = gentermpr_core true let fprterm_env a = gentermpr FW a -let fprterm = fprterm_env (gLOB nil_sign) +let fprterm = fprterm_env empty_env let fprtype_env env typ = fprterm_env env (incast_type typ) -let fprtype = fprtype_env (gLOB nil_sign) +let fprtype = fprtype_env empty_env *) let fprterm_env a = @@ -123,27 +123,23 @@ let fprtype a = (* For compatibility *) let fterm0 = fprterm_env -let pr_constant env cst = gentermpr (ast_of_constant (unitize_env env) cst) -let pr_existential env ev = gentermpr (ast_of_existential (unitize_env env) ev) -let pr_inductive env ind = gentermpr (ast_of_inductive (unitize_env env) ind) +let pr_constant env cst = gentermpr (ast_of_constant env cst) +let pr_existential env ev = gentermpr (ast_of_existential env ev) +let pr_inductive env ind = gentermpr (ast_of_inductive env ind) let pr_constructor env cstr = - gentermpr (ast_of_constructor (unitize_env env) cstr) + gentermpr (ast_of_constructor env cstr) open Pattern let pr_ref_label = function (* On triche sur le contexte *) - | ConstNode sp -> pr_constant (Global.context()) (sp,[||]) - | IndNode sp -> pr_inductive (Global.context()) (sp,[||]) - | CstrNode sp -> pr_constructor (Global.context()) (sp,[||]) + | ConstNode sp -> pr_constant (Global.env()) (sp,[||]) + | IndNode sp -> pr_inductive (Global.env()) (sp,[||]) + | CstrNode sp -> pr_constructor (Global.env()) (sp,[||]) | VarNode id -> print_id id let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t) let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t) -let pr_pattern_env env t = - gentermpr (Termast.ast_of_pattern (unitize_env env) t) -let pr_pattern t = pr_pattern_env (gLOB nil_sign) t - -(* For compatibility *) -let term0 = prterm_env +let pr_pattern_env env t = gentermpr (Termast.ast_of_pattern env t) +let pr_pattern t = pr_pattern_env empty_names_context t let rec gentacpr gt = Esyntax.genprint default_tacpr tactic_syntax_universe tactic_initial_prec gt @@ -155,86 +151,87 @@ and default_tacpr = function [< 'sTR s; 'bRK(1,2); hOV 0 (prlist_with_sep pr_spc gentacpr ta) >] | gt -> dfltpr gt -let print_decl sign (s,typ) = - let ptyp = prterm_env (gLOB sign) (body_of_type typ) in - [< print_id s ; 'sTR" : "; ptyp >] - -let print_binding env (na,typ) = - let ptyp = prterm_env env (body_of_type typ) in +let pr_var_decl env (id,c,typ) = + let pbody = match c with + | None -> [< >] + | Some c -> [< 'sTR" := "; prterm_env env c >] in + let ptyp = [< 'sTR" : "; prtype_env env typ >] in + [< print_id id ; hOV 0 [< pbody; ptyp >] >] + +let pr_rel_decl env (na,c,typ) = + let pbody = match c with + | None -> [< >] + | Some c -> [< 'sTR" :="; 'sPC; prterm_env env c >] in + let ptyp = prtype_env env typ in match na with - | Anonymous -> [< 'sTR"<>" ; 'sTR" : " ; ptyp >] - | Name id -> [< print_id id ; 'sTR" : "; ptyp >] + | Anonymous -> [< 'sTR"<>" ; 'sPC; pbody; 'sTR" :"; 'sPC; ptyp >] + | Name id -> [< print_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. *) -let sign_it_with f sign e = - snd (sign_it (fun id t (sign,e) -> (add_sign (id,t) sign, f id t sign e)) - sign (nil_sign,e)) - -let sign_it_with_i f sign e = - let (_,_,e') = - (sign_it (fun id t (i,sign,e) -> (i+1,add_sign (id,t) sign, - f i id t sign e)) - sign (0,nil_sign,e)) - in - e' - -let dbenv_it_with f env e = - snd (dbenv_it (fun na t (env,e) -> (add_rel (na,t) env, f na t env e)) - env (gLOB(get_globals env),e)) - (* Prints a signature, all declarations on the same line if possible *) -let pr_sign sign = - hV 0 [< (sign_it_with (fun id t sign pps -> - [< pps; 'wS 2; print_decl sign (id,t) >]) - sign) [< >] >] +let pr_var_context_of env = + hV 0 [< (fold_var_context + (fun env d pps -> [< pps; 'wS 2; pr_var_decl env d >]) + env) [< >] >] + +let pr_rel_context env rel_context = + let rec prec env = function + | [] -> [<>] + | [b] -> pr_rel_decl env b + | b::rest -> + let pb = pr_rel_decl env b in + let penvtl = prec (push_rel b env) rest in + [< pb; 'sTR";"; 'sPC; penvtl >] + in + prec env (List.rev rel_context) (* Prints an env (variables and de Bruijn). Separator: newline *) -let pr_env env = +let pr_context_unlimited env = let sign_env = - sign_it_with - (fun id t sign pps -> - let pidt = print_decl sign (id,t) in [< pps; 'fNL; pidt >]) - (get_globals env) [< >] + fold_var_context + (fun env d pps -> + let pidt = pr_var_decl env d in [< pps; 'fNL; pidt >]) + env [< >] in let db_env = - dbenv_it_with - (fun na t env pps -> - let pnat = print_binding env (na,t) in [< pps; 'fNL; pnat >]) + fold_rel_context + (fun env d pps -> + let pnat = pr_rel_decl env d in [< pps; 'fNL; pnat >]) env [< >] in [< sign_env; db_env >] -let pr_ne_env header k = function - | ENVIRON (sign,_) as env when isnull_sign sign & isnull_rel_env env -> [< >] - | env -> let penv = pr_env env in [< header; penv >] +let pr_ne_context_of header k env = + if Environ.context env = empty_context then [< >] + else let penv = pr_context_unlimited env in [< header; penv >] -let pr_env_limit n env = - let sign = get_globals env in - let lgsign = sign_length sign in +let pr_context_limit n env = + let var_context = Environ.var_context env in + let lgsign = List.length var_context in if n >= lgsign then - pr_env env + pr_context_unlimited env else let k = lgsign-n in - let sign_env = - sign_it_with_i - (fun i id t sign pps -> + let _,sign_env = + fold_var_context + (fun env d (i,pps) -> if i < k then - [< pps ;'sTR "." >] + (i+1, [< pps ;'sTR "." >]) else - let pidt = print_decl sign (id,t) in - [< pps ; 'fNL ; - 'sTR (emacs_str (String.make 1 (Char.chr 253))); - pidt >]) - (get_globals env) [< >] + let pidt = pr_var_decl env d in + (i+1, [< pps ; 'fNL ; + 'sTR (emacs_str (String.make 1 (Char.chr 253))); + pidt >])) + env (0,[< >]) in let db_env = - dbenv_it_with - (fun na t env pps -> - let pnat = print_binding env (na,t) in + 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 >]) @@ -242,6 +239,6 @@ let pr_env_limit n env = in [< sign_env; db_env >] -let pr_env_opt env = match Options.print_hyps_limit () with - | None -> hV 0 (pr_env env) - | Some n -> hV 0 (pr_env_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) |