Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
(* Printers for the ocaml toplevel. *)
open Sortsopen Utilopen Ppopen Namesopen Libnamesopen Univopen UVarsopen Environopen Printeropen Constropen Contextopen Genargopen Clenv
let with_env_evm f x = let env = Global.env() in let sigma = Evd.from_env env in f env sigma x
(* std_ppcmds *)let pp x = Pp.pp_with !Topfmt.std_ft x
let ppexninfo e = let loc = Loc.get_loc e |> Option.map Pp.(fun loc -> str "exn loc: " ++ Loc.pr loc ++ fnl()) |> Option.default (mt()) in pp (loc ++ CErrors.print_extra e)
(** Future printer *)
let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
(* name printers *)let ppid id = pp (Id.print id)let ppmbid mbid = pp (str (MBId.debug_to_string mbid))let ppdir dir = pp (DirPath.print dir)let ppmp mp = pp(str (ModPath.debug_to_string mp))let ppcon con = pp(Constant.debug_print con)let ppprojrepr con = pp(Projection.Repr.print con)let ppproj p = pp(Projection.debug_print p)let ppkn kn = pp(str (KerName.to_string kn))let ppmind kn = pp(MutInd.debug_print kn)let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)let ppsp sp = pp(pr_path sp)let ppqualid qid = pp(pr_qualid qid)let ppscheme k = pp (Ind_tables.pr_scheme_kind k)
let pprecarg r = pp (Declareops.pr_recarg r)let ppwf_paths x = pp (Declareops.pr_wf_paths x)
let get_current_context () = try Vernacstate.Declare.get_current_context () with Vernacstate.Declare.NoCurrentProof -> let env = Global.env() in Evd.from_env env, env [@@ocaml.warning "-3"]
(* term printers *)let envpp pp = let sigma,env = get_current_context () in pp env sigmalet ppevar evk = pp (Evar.print evk)let pr_constr t = let sigma, env = get_current_context () in Printer.pr_constr_env env sigma tlet pr_econstr t = let sigma, env = get_current_context () in Printer.pr_econstr_env env sigma tlet ppconstr x = pp (pr_constr x)let ppeconstr x = pp (pr_econstr x)let ppconstr_expr x = let sigma,env = get_current_context () in let flags = Ppconstr.current_flags() in pp (Ppconstr.pr_constr_expr ~flags env sigma x)let ppconstr_univ x = Flags.with_option PrintingFlags.print_universes ppconstr xlet ppglob_constr = (fun x -> pp(with_env_evm pr_lglob_constr_env x))let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
(* XXX we could also try to have a printer which shows which parts are shared, but this is probably better for most uses (ie stepping through typeops and wanting to print the current constr) *)let pphconstr c = ppconstr (HConstr.self c)
let ppuint63 i = pp (str (Uint63.to_string i))
let pp_parray pr a = let a, def = Parray.to_array a in let a = Array.to_list a in pp (str "[|" ++ prlist_with_sep (fun () -> str ";" ++ spc()) pr a ++ spc() ++ str "|" ++ spc() ++ pr def ++ str "|]")
let pp_constr_parray = pp_parray pr_constrlet pp_fconstr_parray = pp_parray (fun f -> pr_constr (CClosure.term_of_fconstr f))
let pplift el = pp @@ Esubst.Internal.pp_lift el
let ppfsubst s = let (s, k) = Esubst.Internal.repr s in let sep () = str ";" ++ spc () in let pr = function | Esubst.Internal.REL n -> str "<#" ++ int n ++ str ">" | Esubst.Internal.VAL (k, x) -> pr_constr (Vars.lift k (CClosure.term_of_fconstr x)) in pp @@ str "[" ++ prlist_with_sep sep pr s ++ str "| " ++ int k ++ str "]"
let ppnumtokunsigned n = pp (NumTok.Unsigned.print n)let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n)
let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"let ppintset l = pp (prset int (Int.Set.elements l))let ppidset l = pp (prset Id.print (Id.Set.elements l))
let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
let pridmap pr l = let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])let ppidmap pr l = pp (pridmap pr l)
let prmapgen pr dom = if dom = [] then str "[]" else str "[domain= " ++ hov 0 (prlist_with_sep spc pr dom) ++ str "]"let pridmapgen l = prmapgen Id.print (Id.Set.elements (Id.Map.domain l))let ppidmapgen l = pp (pridmapgen l)let printmapgen l = prmapgen int (Int.Set.elements (Int.Map.domain l))let ppintmapgen l = pp (printmapgen l)
let ppmpmapgen l = pp (prmapgen (fun mp -> str (ModPath.debug_to_string mp)) (ModPath.Set.elements (ModPath.Map.domain l)))
let ppdpmapgen l = pp (prmapgen (fun mp -> str (DirPath.to_string mp)) (DirPath.Set.elements (DirPath.Map.domain l)))
let ppconmapenvgen l = pp (prmapgen (fun mp -> str (Constant.debug_to_string mp)) (Cset.elements (Cmap.domain l)))
let ppmindmapenvgen l = pp (prmapgen (fun mp -> str (MutInd.debug_to_string mp)) (Mindset.elements (Mindmap.domain l)))
let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> hov 0 (pr_constr c ++ (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++ pr_constr c ++ str">") ++ (if id = id0 then mt () else spc () ++ str "<canonical: " ++ Id.print id ++ str ">"))))
let prididmap = pridmap (fun _ -> Id.print)let ppididmap = ppidmap (fun _ -> Id.print)
let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]") ++ str "," ++ spc () ++ pr_econstr c)
let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l)
let ppgenlam l = pp (Genlambda.pp_lam l)
let ppunbound_ltac_var_map l = ppidmap (fun _ arg -> str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">") l
open Ltac_pretypelet rec pr_closure {idents=idents;typed=typed;untyped=untyped} = hov 1 (str"{idents=" ++ prididmap idents ++ str";" ++ spc() ++ str"typed=" ++ prconstrunderbindersidmap typed ++ str";" ++ spc() ++ str"untyped=" ++ pr_closed_glob_constr_idmap untyped ++ str"}")and pr_closed_glob_constr_idmap x = pridmap (fun _ -> pr_closed_glob_constr) xand pr_closed_glob_constr {closure=closure;term=term} = pr_closure closure ++ with_env_evm pr_lglob_constr_env term
let ppclosure x = pp (pr_closure x)let ppclosedglobconstr x = pp (pr_closed_glob_constr x)let ppclosedglobconstridmap x = pp (pr_closed_glob_constr_idmap x)
let pP s = pp (hov 0 s)
let pp_as_format s = let fmt, args = pp_as_format s in let pr_escaped s = str ("\"" ^ String.escaped s ^ "\"") in pp (hov 0 (str "printf" ++ spc() ++ str "\"" ++ str fmt ++ str "\"" ++ pr_non_empty_arg (prlist_with_sep spc pr_escaped) args))
let safe_pr_global = let open GlobRef in function | ConstRef kn -> pp (str "CONSTREF(" ++ Constant.debug_print kn ++ str ")") | IndRef (kn,i) -> pp (str "INDREF(" ++ MutInd.debug_print kn ++ str "," ++ int i ++ str ")") | ConstructRef ((kn,i),j) -> pp (str "CONSTRUCTREF(" ++ MutInd.debug_print kn ++ str "," ++ int i ++ str "," ++ int j ++ str ")") | VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")")
let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x
let ppconst (sp,j) = pp (str"#" ++ KerName.print sp ++ str"=" ++ envpp pr_lconstr_env j.uj_val)
let ppvar ((id,a)) = pp (str"#" ++ Id.print id ++ str":" ++ envpp pr_lconstr_env a)
let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
let ppj j = pp (genppj (envpp pr_ljudge_env) j)
let ppsubst s = pp (Mod_subst.debug_pr_subst s)let ppdelta s = pp (Mod_subst.debug_pr_delta (fun c -> pr_constr c.UVars.univ_abstracted_value) s)
let pp_idpred s = pp (pr_idpred s)let pp_cpred s = pp (pr_cpred s)let pp_transparent_state s = pp (pr_transparent_state s)let pp_estack_t n = pp (Reductionops.Stack.pr pr_econstr n)let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
(* proof printers *)let pr_evar ev = Pp.int (Evar.repr ev)let ppmetas metas = pp (Unification.Meta.pr_metaset metas)let ppmetamap metas = let env = Global.env () in let sigma = Evd.from_env env in pp (Unification.Meta.pr_metamap env sigma metas)let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!PrintingFlags.print_universes (Some 2) (Global.env ()) evd)let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!PrintingFlags.print_universes None (Global.env ()) evd)let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars)let ppexistentialset evars = pp (pr_existentialset evars)let ppexistentialfilter filter = match Evd.Filter.repr filter with| None -> pp (Pp.str "ø")| Some f -> pp (prlist_with_sep spc bool f)let pr_goal e = Pp.(str "GOAL:" ++ int (Evar.repr e))let ppclenv clenv = pp(pr_clenv clenv)let ppgoal g = pp(Printer.Debug.pr_goal g)let ppgoal_with_state g = ppevar (Proofview_monad.drop_state g)let pphintdb db = pp(envpp Hints.pr_hint_db_env db)let ppproofview p = let gls,sigma = Proofview.proofview p in pp(pr_enum pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) (Global.env ()) sigma)
let ppseff seff = pp (Safe_typing.debug_print_private_constants seff)
(* spiwack: deactivated until a replacement is foundlet pppftreestate p = pp(print_pftreestate p)*)
(* let ppgoal g = pp(db_pr_goal g) *)(* let pr_gls gls = *)(* hov 0 (pr_evar_defs (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) *)
(* let pr_glls glls = *)(* hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ *)(* prlist_with_sep fnl db_pr_goal (sig_it glls)) *)
(* let ppsigmagoal g = pp(pr_goal (sig_it g)) *)(* let prgls gls = pp(pr_gls gls) *)(* let prglls glls = pp(pr_glls glls) *)
let pproof p = pp(Proof.pr_proof p)
let ppuni u = pp(Universe.raw_pr u)let ppuni_level u = pp (Level.raw_pr u)let ppqvar q = pp (QVar.raw_pr q)let ppesorts s = pp (Sorts.debug_print (EConstr.Unsafe.to_sorts s))
(* pprelevance not directly useful since it's transparent, but used for pperelevance *)let pprelevance (r:Sorts.relevance) = match r with | Relevant -> pp (str "Relevant") | Irrelevant -> pp (str "Irrelevant") | RelevanceVar q -> pp (surround (str "RelevanceVar " ++ spc() ++ Sorts.QVar.raw_pr q))let pperelevance r = pprelevance (EConstr.Unsafe.to_relevance r)
let qprinter = UnivNames.quality_printer UnivNames.empty_binderslet sprinter = UnivNames.sort_printer UnivNames.empty_binderslet prlev l = UnivNames.pr_level_with_global_universes llet prqvar q = UnivNames.pr_quality_with_global_universes (QVar q)let prquality q = UnivNames.pr_quality_with_global_universes qlet ppqvarset l = pp (hov 1 (str "{" ++ prlist_with_sep spc prqvar (QVar.Set.elements l) ++ str "}"))let ppqset qs = pp (hov 1 (str "{" ++ prlist_with_sep spc prquality (Quality.Set.elements qs) ++ str "}"))let ppuniverse_set l = pp (Level.Set.pr prlev l)let ppuniverse_instance l = pp (Instance.pr sprinter l)let ppuniverse_einstance l = ppuniverse_instance (EConstr.Unsafe.to_instance l)let ppuniverse_context l = pp (UVars.UContext.pr sprinter l)let ppuniverse_subst l = pp (UnivSubst.pr_universe_subst Level.raw_pr l)let ppuniverse_opt_subst l = pp (UnivFlex.pr Level.raw_pr l)let ppqvar_subst l = pp (UVars.pr_quality_level_subst Quality.raw_printer l)let ppuniverse_level_subst l = pp (UVars.pr_universe_level_subst Level.raw_pr l)let pppoly_flags f = pp (PolyFlags.pr f)let ppustate l = pp (UState.pr l)let ppconstraints c = pp (UnivConstraints.pr Level.raw_pr c)let ppqconstraints c = pp (ElimConstraints.pr qprinter c)let ppuniverseconstraints c = pp (UnivProblem.Set.pr c)let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctxlet ppuniverses u = pp (UGraph.pr_universes Level.raw_pr (UGraph.repr u))let ppqualities q = pp (QGraph.pr_qualities Quality.raw_printer q)let ppelim_constraints cstrs = pp (Sorts.ElimConstraints.pr qprinter cstrs)let ppnamedcontextval e = let env = Global.env () in let sigma = Evd.from_env env in pp (pr_named_context_of (Environ.reset_with_named_context e env) sigma)
let ppaucontext auctx = let {quals = qnas; univs = unas} = AbstractContext.names auctx in let prgen pr var_index nas l = match var_index l with | Some n -> (match nas.(n) with | Anonymous -> pr l | Name id -> Id.print id) | None -> pr l in let prqvar l = prgen prqvar Sorts.QVar.var_index qnas l in let prlev l = prgen prlev Level.var_index unas l in let prqglobal q = prquality (QGlobal q) in pp (UContext.pr { pru = prlev; prq = { prvar = prqvar; prglobal = prqglobal } } (AbstractContext.repr auctx))
let pp_partialfsubst psubst = pp (Partial_subst.pr (fun f -> pr_constr (CClosure.term_of_fconstr f)) prquality (Universe.pr prlev) psubst)
let pp_partialsubst psubst = pp (Partial_subst.pr pr_econstr prquality (Universe.pr prlev) psubst)
let ppenv e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]")
let ppglobenv e = ppenv (GlobEnv.env e)
let ppenvwithcst e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ str "{" ++ Environ.fold_constants (fun a _ s -> Constant.print a ++ spc () ++ s) e (mt ()) ++ str "}")
let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
let ppobj obj = let Libobject.Dyn.Dyn (tag, _) = obj in Format.print_string (Libobject.Dyn.repr tag)
let cnt = ref 0
let cast_kind_display k = match k with | VMcast -> "VMcast" | DEFAULTcast -> "DEFAULTcast" | NATIVEcast -> "NATIVEcast"
let constr_display csr = let rec term_display c = match kind c with | Rel n -> "Rel("^(string_of_int n)^")" | Meta n -> "Meta("^(string_of_int n)^")" | Var id -> "Var("^(Id.to_string id)^")" | Sort s -> "Sort("^(sort_display s)^")" | Cast (c,k, t) -> "Cast("^(term_display c)^","^(cast_kind_display k)^","^(term_display t)^")" | Prod (na,t,c) -> "Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n" | Lambda (na,t,c) -> "Lambda("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n" | LetIn (na,b,t,c) -> "LetIn("^(name_display na)^","^(term_display b)^"," ^(term_display t)^","^(term_display c)^")" | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n" | Evar (e,l) -> let l = SList.to_list l in let map = function None -> "?" | Some t -> term_display t in let l = List.map map l in "Evar("^(Pp.string_of_ppcmds (Evar.print e))^", [|"^(String.concat "; " l)^"|])" | Const (c,u) -> "Const("^(Constant.to_string c)^","^(universes_display u)^")" | Ind ((sp,i),u) -> "MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^","^(universes_display u)^")" | Construct (((sp,i),j),u) -> "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^")," ^","^(universes_display u)^(string_of_int j)^")" | Proj (p, r, c) -> "Proj("^(Projection.to_string p)^","^term_display c ^")" | Case (ci,u,pms,((_,p),_),iv,c,bl) -> "MutCase(<abs>,"^(term_display p)^","^(term_display c)^"," ^(array_display (Array.map snd bl))^")" | Fix ((t,i),(lna,tl,bl)) -> "Fix(([|"^(Array.fold_right (fun x i -> (string_of_int x)^(if not(i="") then (";"^i) else "")) t "")^"|],"^(string_of_int i)^")," ^(array_display tl)^",[|" ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="") then (";"^i) else "")) lna "")^"|]," ^(array_display bl)^")" | CoFix(i,(lna,tl,bl)) -> "CoFix("^(string_of_int i)^")," ^(array_display tl)^"," ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="") then (";"^i) else "")) lna "")^"," ^(array_display bl)^")" | Int i -> "Int("^(Uint63.to_string i)^")" | Float f -> "Float("^(Float64.to_string f)^")" | String s -> Printf.sprintf "String(%S)" (Pstring.to_string s) | Array (u,t,def,ty) -> "Array("^(array_display t)^","^(term_display def)^","^(term_display ty)^")@{" ^universes_display u^"\n"
and array_display v = "[|"^ (Array.fold_right (fun x i -> (term_display x)^(if not(i="") then (";"^i) else "")) v "")^"|]"
and univ_display u = incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Universe.raw_pr u ++ fnl ())
and quality_display q = incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Sorts.Quality.raw_pr q ++ fnl ())
and level_display u = incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.raw_pr u ++ fnl ())
and sort_display = function | SProp -> "SProp" | Set -> "Set" | Prop -> "Prop" | Type u -> univ_display u; "Type("^(string_of_int !cnt)^")" | GSort (q, u) -> univ_display u; Printf.sprintf "GSort(%s, %i)" (Sorts.QGlobal.to_string q) !cnt | VSort (q, u) -> univ_display u; Printf.sprintf "VSort(%s, %i)" (Sorts.QVar.to_string q) !cnt
and universes_display l = let qs, us = Instance.to_array l in let qs = Array.fold_right (fun x i -> quality_display x; (string_of_int !cnt)^ (if not(i="") then (" "^i) else "")) qs "" in Array.fold_right (fun x i -> level_display x; (string_of_int !cnt)^(if not(i="") then (" "^i) else "")) us (if qs = "" then "" else (qs^" | "))
and name_display x = match x.binder_name with | Name id -> "Name("^(Id.to_string id)^")" | Anonymous -> "Anonymous"
in pp (str (term_display csr) ++fnl ())
let econstr_display c = constr_display EConstr.Unsafe.(to_constr c) ;;
open Format;;
let print_pure_constr csr = let rec term_display c = match Constr.kind c with | Rel n -> print_string "#"; print_int n | Meta n -> print_string "Meta("; print_int n; print_string ")" | Var id -> print_string (Id.to_string id) | Sort s -> sort_display s | Cast (c,_, t) -> open_hovbox 1; print_string "("; (term_display c); print_cut(); print_string "::"; (term_display t); print_string ")"; close_box() | Prod ({binder_name=Name(id)},t,c) -> open_hovbox 1; print_string"("; print_string (Id.to_string id); print_string ":"; box_display t; print_string ")"; print_cut(); box_display c; close_box() | Prod ({binder_name=Anonymous},t,c) -> print_string"("; box_display t; print_cut(); print_string "->"; box_display c; print_string ")"; | Lambda (na,t,c) -> print_string "["; name_display na; print_string ":"; box_display t; print_string "]"; print_cut(); box_display c; | LetIn (na,b,t,c) -> print_string "["; name_display na; print_string "="; box_display b; print_cut(); print_string ":"; box_display t; print_string "]"; print_cut(); box_display c; | App (c,l) -> print_string "("; box_display c; Array.iter (fun x -> print_space (); box_display x) l; print_string ")" | Evar (e,l) -> print_string "Evar#"; print_int (Evar.repr e); print_string "{"; let iter = function None -> print_space (); print_string "?" | Some t -> print_space (); box_display t in List.iter iter (SList.to_list l); print_string"}" | Const (c,u) -> print_string "Cons("; sp_con_display c; print_string ","; universes_display u; print_string ")" | Proj (p,_,c') -> print_string "Proj("; sp_prj_display p; print_string ","; box_display c'; print_string ")" | Ind ((sp,i),u) -> print_string "Ind("; sp_display sp; print_string ","; print_int i; print_string ","; universes_display u; print_string ")" | Construct (((sp,i),j),u) -> print_string "Constr("; sp_display sp; print_string ","; print_int i; print_string ","; print_int j; print_string ","; universes_display u; print_string ")" | Case (ci,u,pms,(p,_),iv,c,bl) -> let pr_ctx (nas, c) = Array.iter (fun na -> print_cut (); name_display na) nas; print_string " |- "; box_display c in open_vbox 0; print_cut(); print_string "Case"; print_space(); box_display c; print_space (); print_cut(); print_string "in"; print_cut(); print_string "Ind("; sp_display (fst ci.ci_ind); print_string ","; print_int (snd ci.ci_ind); print_string ")"; print_string "@{"; universes_display u; print_string "}"; Array.iter (fun x -> print_space (); box_display x) pms; print_cut(); print_string "return <"; pr_ctx p; print_string ">"; print_cut(); print_string "with"; open_vbox 0; Array.iter (fun x -> print_cut(); pr_ctx x) bl; close_box(); print_cut(); print_string "end"; close_box() | Fix ((t,i),(lna,tl,bl)) -> print_string "Fix("; print_int i; print_string ")"; print_cut(); open_vbox 0; let print_fix () = for k = 0 to (Array.length tl) - 1 do open_vbox 0; name_display lna.(k); print_string "/"; print_int t.(k); print_cut(); print_string ":"; box_display tl.(k) ; print_cut(); print_string ":="; box_display bl.(k); close_box (); print_cut() done in print_string"{"; print_fix(); print_string"}" | CoFix(i,(lna,tl,bl)) -> print_string "CoFix("; print_int i; print_string ")"; print_cut(); open_vbox 0; let print_fix () = for k = 0 to (Array.length tl) - 1 do open_vbox 1; name_display lna.(k); print_cut(); print_string ":"; box_display tl.(k) ; print_cut(); print_string ":="; box_display bl.(k); close_box (); print_cut(); done in print_string"{"; print_fix (); print_string"}" | Int i -> print_string ("Int("^(Uint63.to_string i)^")") | Float f -> print_string ("Float("^(Float64.to_string f)^")") | String s -> print_string (Printf.sprintf "String(%S)" (Pstring.to_string s)) | Array (u,t,def,ty) -> print_string "Array("; Array.iter (fun x -> box_display x; print_space()) t; print_string "|"; box_display def; print_string ":"; box_display ty; print_string ")@{"; universes_display u; print_string "}"
and box_display c = open_hovbox 1; term_display c; close_box()
and universes_display u = let qs, us = Instance.to_array u in Array.iter (fun u -> print_space (); pp (Sorts.Quality.raw_pr u)) qs; Array.iter (fun u -> print_space (); pp (Level.raw_pr u)) us
and sort_display = function | SProp -> print_string "SProp" | Set -> print_string "Set" | Prop -> print_string "Prop" | Type u -> open_hbox(); print_string "Type("; pp (Universe.raw_pr u); print_string ")"; close_box() | GSort (q, u) -> open_hbox(); print_string "GSort("; pp (str @@ QGlobal.to_string q); print_string ", "; pp (Universe.raw_pr u); print_string ")"; close_box() | VSort (q, u) -> open_hbox(); print_string "VSort("; pp (QVar.raw_pr q); print_string ", "; pp (Universe.raw_pr u); print_string ")"; close_box()
and name_display x = match x.binder_name with | Name id -> print_string (Id.to_string id) | Anonymous -> print_string "_"(* Remove the top names for library and Scratch to avoid long names *) and sp_display sp =(* let dir,l = decode_kn sp in let ls = match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Stdlib"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) print_string (MutInd.debug_to_string sp) and sp_con_display sp =(* let dir,l = decode_kn sp in let ls = match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Stdlib"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) print_string (Constant.debug_to_string sp) and sp_prj_display sp = print_string (Projection.debug_to_string sp) in try box_display csr; print_flush() with e -> print_string (Printexc.to_string e);print_flush (); raise e
let print_pure_econstr c = print_pure_constr EConstr.Unsafe.(to_constr c) ;;
let pploc x = let (l,r) = Loc.unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")"
let pp_argument_type t = pp (pr_argument_type t)
let pp_generic_argument arg = pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">")
let prgenarginfo arg = let Geninterp.Val.Dyn (tag, _) = arg in let tpe = Geninterp.Val.pr tag in (* FIXME *)(* try *)(* let data = Pptactic.pr_top_generic (Global.env ()) arg in *)(* str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" *)(* with _any -> *) str "<genarg:" ++ tpe ++ str ">"
let ppgenarginfo arg = pp (prgenarginfo arg)
let ppgenargargt arg = pp (str (Genarg.ArgT.repr arg))
let ppist ist = let pr id arg = prgenarginfo arg in pp (pridmap pr ist.Ltac_plugin.Tacinterp.lfun)
(**********************************************************************)(* Vernac-level debugging commands *)
let in_current_context f c = let (evmap,sign) = get_current_context () in f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*)
(* We expand the result of preprocessing to be independent of camlp5
VERNAC COMMAND EXTEND PrintPureConstr| [ "PrintPureConstr" constr(c) ] -> [ in_current_context print_pure_constr c ]ENDVERNAC COMMAND EXTEND PrintConstr [ "PrintConstr" constr(c) ] -> [ in_current_context constr_display c ]END*)
let () = let open Vernacextend in let open Vernactypes in let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in let cmd_fn c ?loc:_ ~atts () = vtdefault (fun () -> in_current_context econstr_display c) in let cmd_class _ ~atts:_ = VtQuery in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in static_vernac_extend ~ignore_kw:false ~plugin:None ~command:"PrintConstr" [cmd]
let () = let open Vernacextend in let open Vernactypes in let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in let cmd_fn c ?loc:_ ~atts () = vtdefault (fun () -> in_current_context print_pure_econstr c) in let cmd_class _ ~atts:_ = VtQuery in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in static_vernac_extend ~ignore_kw:false ~plugin:None ~command:"PrintPureConstr" [cmd]
(* Setting printer of unbound global reference *)open Namesopen Libnames
let encode_path ?loc prefix mpdir suffix id = let dir = match mpdir with | None -> [] | Some mp -> DirPath.repr (dirpath_of_string (ModPath.to_string mp)) in make_qualid ?loc (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id
let raw_string_of_ref ?loc _ = let open GlobRef in function | ConstRef cst -> let (mp,id) = KerName.repr (Constant.user cst) in encode_path ?loc "CST" (Some mp) [] id | IndRef (kn,i) -> let (mp,id) = KerName.repr (MutInd.user kn) in encode_path ?loc "IND" (Some mp) [id] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> let (mp,id) = KerName.repr (MutInd.user kn) in encode_path ?loc "CSTR" (Some mp) [id;Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) | VarRef id -> encode_path ?loc "SECVAR" None [] id
let short_string_of_ref ?loc _ = let open GlobRef in function | VarRef id -> qualid_of_ident ?loc id | ConstRef cst -> qualid_of_ident ?loc (Constant.label cst) | IndRef (kn,0) -> qualid_of_ident ?loc (MutInd.label kn) | IndRef (kn,i) -> encode_path ?loc "IND" None [MutInd.label kn] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> encode_path ?loc "CSTR" None [MutInd.label kn; Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j))