diff options
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 154 |
1 files changed, 89 insertions, 65 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 72fe499e6..df2aabdf8 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -28,15 +28,91 @@ open Ppconstr let emacs_str s = if !Options.print_emacs then s else "" -(* These are the names of the universes where the pp rules for constr and - tactic are put (must be consistent with files PPConstr.v and PPTactic.v *) - -let tactic_syntax_universe = "tactic" +(**********************************************************************) +(* 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 tactic_initial_prec = Some ((tactic_syntax_universe,(9,0,0)),Ppextend.L) - +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_constr (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 @@ -48,25 +124,14 @@ 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 fprterm_env a = - warning "Fw printing not implemented, use CCI printing 1"; prterm_env a -let fprterm a = - warning "Fw printing not implemented, use CCI printing 2"; prterm a - -let fprtype_env env typ = - warning "Fw printing not implemented, use CCI printing 3"; prtype_env env typ -let fprtype a = - warning "Fw printing not implemented, use CCI printing 4"; prtype a +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 -(* For compatibility *) -let fterm0 = fprterm_env - -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 env cstr) - -let pr_global = pr_global +let pr_rawterm t = + pr_constr (Constrextern.extern_rawconstr Idset.empty t) open Pattern let pr_ref_label = function (* On triche sur le contexte *) @@ -75,49 +140,8 @@ let pr_ref_label = function (* On triche sur le contexte *) | CstrNode sp -> pr_constructor (Global.env()) sp | VarNode id -> pr_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_rawterm t = pr_constr (Constrextern.extern_rawconstr t) -let pr_pattern_env tenv env t = gentermpr (Termast.ast_of_pattern tenv env t) let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t -(* -let gentacpr x = Pptactic.prtac x -*) - -(* -and default_tacpr = function - | Nvar(_,s) -> (pr_id s) - - (* constr's may occur inside tac expressions ! *) - | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev))) - | Node(_,"CONST",[Path(_,sl)]) -> - let sp = section_path sl in - pr_global (ConstRef sp) - | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) -> - let sp = section_path sl in - pr_global (IndRef (sp,tyi)) - | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) -> - let sp = section_path sl in - pr_global (ConstructRef ((sp,tyi),i)) - - (* This should be tactics *) - | Node(_,s,[]) -> (str s) -(* TODO - | Node(_,s,ta) -> - (str s ++ brk(1,2) ++ hov 0 (prlist_with_sep pr_spc gentacpr ta)) -*) - | Dynamic(_,d) as gt -> - let tg = Dyn.tag d in - if tg = "tactic" then (str"<dynamic [tactic]>") - else if tg = "value" then (str"<dynamic [value]>") - else if tg = "constr" then (str"<dynamic [constr]>") - else dfltpr gt - | gt -> dfltpr gt -*) - let pr_var_decl env (id,c,typ) = let pbody = match c with | None -> (mt ()) |