summaryrefslogtreecommitdiff
path: root/parsing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/printer.ml')
-rw-r--r--parsing/printer.ml470
1 files changed, 344 insertions, 126 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 75cdead9..29ebe4fa 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -1,19 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: printer.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
open Util
open Names
open Nameops
open Term
-open Termops
open Sign
open Environ
open Global
@@ -22,29 +19,36 @@ open Libnames
open Nametab
open Evd
open Proof_type
-open Decl_mode
open Refiner
open Pfedit
open Ppconstr
open Constrextern
open Tacexpr
+open Declarations
+
+open Store.Field
-let emacs_str s alts =
- match !Flags.print_emacs, !Flags.print_emacs_safechar with
- | true, true -> alts
- | true , false -> s
- | false,_ -> ""
+let emacs_str s =
+ if !Flags.print_emacs then s else ""
+let delayed_emacs_cmd s =
+ if !Flags.print_emacs then s () else str ""
(**********************************************************************)
(** Terms *)
- (* [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)
+(* [goal_concl_style] means that all names of goal/section variables
+ and all names of rel variables (if any) in the given env and all short
+ names of global definitions of the current module must be avoided while
+ printing bound variables.
+ Otherwise, short names of global definitions are printed qualified
+ and only names of goal/section variables and rel names that do
+ _not_ occur in the scope of the binder to be printed are avoided. *)
+
+let pr_constr_core goal_concl_style env t =
+ pr_constr_expr (extern_constr goal_concl_style env t)
+let pr_lconstr_core goal_concl_style env t =
+ pr_lconstr_expr (extern_constr goal_concl_style 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
@@ -63,7 +67,7 @@ let pr_constr_under_binders_env_gen pr env (ids,c) =
(* we also need to preserve the actual names of the patterns *)
(* So what to do? *)
let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) ids in
- pr (push_rels_assum assums env) c
+ pr (Termops.push_rels_assum assums env) c
let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_constr_env
let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_env
@@ -71,12 +75,12 @@ let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_en
let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c
let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c
-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_type_core goal_concl_style env t =
+ pr_constr_expr (extern_type goal_concl_style env t)
+let pr_ltype_core goal_concl_style env t =
+ pr_lconstr_expr (extern_type goal_concl_style env t)
-let pr_ltype_env_at_top env = pr_ltype_core true env
+let pr_goal_concl_style_env 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
@@ -88,40 +92,97 @@ let pr_ljudge_env env j =
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_lglob_constr_env env c =
+ pr_lconstr_expr (extern_glob_constr (Termops.vars_of_env env) c)
+let pr_glob_constr_env env c =
+ pr_constr_expr (extern_glob_constr (Termops.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)
+let pr_lglob_constr c =
+ pr_lconstr_expr (extern_glob_constr Idset.empty c)
+let pr_glob_constr c =
+ pr_constr_expr (extern_glob_constr Idset.empty c)
let pr_cases_pattern t =
pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
let pr_lconstr_pattern_env env c =
- pr_lconstr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c)
+ pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) c)
let pr_constr_pattern_env env c =
- pr_constr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c)
+ pr_constr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) c)
let pr_lconstr_pattern t =
- pr_lconstr_pattern_expr (extern_constr_pattern empty_names_context t)
+ pr_lconstr_pattern_expr (extern_constr_pattern Termops.empty_names_context t)
let pr_constr_pattern t =
- pr_constr_pattern_expr (extern_constr_pattern empty_names_context t)
+ pr_constr_pattern_expr (extern_constr_pattern Termops.empty_names_context t)
-let pr_sort s = pr_rawsort (extern_sort s)
+let pr_sort s = pr_glob_sort (extern_sort s)
let _ = Termops.set_print_constr pr_lconstr_env
+
+(** Term printers resilient to [Nametab] errors *)
+
+(** When the nametab isn't up-to-date, the term printers above
+ could raise [Not_found] during [Nametab.shortest_qualid_of_global].
+ In this case, we build here a fully-qualified name based upon
+ the kernel modpath and label of constants, and the idents in
+ the [mutual_inductive_body] for the inductives and constructors
+ (needs an environment for this). *)
+
+let id_of_global env = function
+ | ConstRef kn -> id_of_label (con_label kn)
+ | IndRef (kn,0) -> id_of_label (mind_label kn)
+ | IndRef (kn,i) ->
+ (Environ.lookup_mind kn env).mind_packets.(i).mind_typename
+ | ConstructRef ((kn,i),j) ->
+ (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1)
+ | VarRef v -> v
+
+let cons_dirpath id dp = make_dirpath (id :: repr_dirpath dp)
+
+let rec dirpath_of_mp = function
+ | MPfile sl -> sl
+ | MPbound uid -> make_dirpath [id_of_mbid uid]
+ | MPdot (mp,l) -> cons_dirpath (id_of_label l) (dirpath_of_mp mp)
+
+let dirpath_of_global = function
+ | ConstRef kn -> dirpath_of_mp (con_modpath kn)
+ | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+ dirpath_of_mp (mind_modpath kn)
+ | VarRef _ -> empty_dirpath
+
+let qualid_of_global env r =
+ Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
+
+let safe_gen f env c =
+ let orig_extern_ref = Constrextern.get_extern_reference () in
+ let extern_ref loc vars r =
+ try orig_extern_ref loc vars r
+ with e when Errors.noncritical e ->
+ Libnames.Qualid (loc, qualid_of_global env r)
+ in
+ Constrextern.set_extern_reference extern_ref;
+ try
+ let p = f env c in
+ Constrextern.set_extern_reference orig_extern_ref;
+ p
+ with e when Errors.noncritical e ->
+ Constrextern.set_extern_reference orig_extern_ref;
+ str "??"
+
+let safe_pr_lconstr_env = safe_gen pr_lconstr_env
+let safe_pr_constr_env = safe_gen pr_constr_env
+let safe_pr_lconstr t = safe_pr_lconstr_env (Global.env()) t
+let safe_pr_constr t = safe_pr_constr_env (Global.env()) 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_constant env cst = pr_global_env (Termops.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)
@@ -129,8 +190,8 @@ let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr)
let pr_evaluable_reference ref =
pr_global (Tacred.global_of_evaluable_reference ref)
-(*let pr_rawterm t =
- pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)*)
+(*let pr_glob_constr t =
+ pr_lconstr (Constrextern.extern_glob_constr Idset.empty t)*)
(*open Pattern
@@ -222,7 +283,7 @@ let pr_context_limit n env =
else
let pidt = pr_var_decl env d in
(i+1, (pps ++ fnl () ++
- str (emacs_str (String.make 1 (Char.chr 253)) "") ++
+ str (emacs_str "") ++
pidt)))
env ~init:(0,(mt ()))
in
@@ -231,7 +292,7 @@ let pr_context_limit n env =
(fun env d pps ->
let pnat = pr_rel_decl env d in
(pps ++ fnl () ++
- str (emacs_str (String.make 1 (Char.chr 253)) "") ++
+ str (emacs_str "") ++
pnat))
env ~init:(mt ())
in
@@ -243,18 +304,6 @@ let pr_context_of env = match Flags.print_hyps_limit () with
(* display goal parts (Proof mode) *)
-let pr_restricted_named_context among env =
- hv 0 (fold_named_context
- (fun env ((id,_,_) as d) pps ->
- if true || Idset.mem id among then
- pps ++
- fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++
- pr_var_decl env d
- else
- pps)
- env ~init:(mt ()))
-
-
let pr_predicate pr_elt (b, elts) =
let pr_elts = prlist_with_sep spc pr_elt elts in
if b then
@@ -270,39 +319,34 @@ let pr_transparent_state (ids, csts) =
hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
-let pr_subgoal_metas metas env=
- let pr_one (meta,typ) =
- str "?" ++ int meta ++ str " : " ++
- hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++
- str (emacs_str (String.make 1 (Char.chr 253)) "") in
- hv 0 (prlist_with_sep mt pr_one metas)
-
(* display complete goal *)
-let default_pr_goal g =
- let env = evar_unfiltered_env g in
+let default_pr_goal gs =
+ let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
+ let env = Goal.V82.unfiltered_env sigma g in
let preamb,thesis,penv,pc =
- if g.evar_extra = None then
- mt (), mt (),
- pr_context_of env,
- pr_ltype_env_at_top env g.evar_concl
- else
- (str " *** Declarative Mode ***" ++ fnl ()++fnl ()),
- (str "thesis := " ++ fnl ()),
- pr_context_of env,
- pr_ltype_env_at_top env g.evar_concl
+ mt (), mt (),
+ pr_context_of env,
+ pr_goal_concl_style_env env (Goal.V82.concl sigma g)
in
preamb ++
str" " ++ hv 0 (penv ++ fnl () ++
- str (emacs_str (String.make 1 (Char.chr 253)) "") ++
+ str (emacs_str "") ++
str "============================" ++ fnl () ++
thesis ++ str " " ++ pc) ++ fnl ()
+(* display a goal tag *)
+let pr_goal_tag g =
+ let s = " (ID " ^ Goal.uid g ^ ")" in
+ str (emacs_str s)
+
(* 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
+let pr_concl n sigma g =
+ let (g,sigma) = Goal.V82.nf_evar sigma g in
+ let env = Goal.V82.env sigma g in
+ let pc = pr_goal_concl_style_env env (Goal.V82.concl sigma g) in
+ str (emacs_str "") ++
+ str "subgoal " ++ int n ++ pr_goal_tag g ++
+ str " is:" ++ cut () ++ str" " ++ pc
(* display evar type: a context and a type *)
let pr_evgl_sign gl =
@@ -316,6 +360,12 @@ let pr_evgl_sign gl =
let pc = pr_lconstr gl.evar_concl in
hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ spc () ++ warn)
+(* Print an existential variable *)
+
+let pr_evar (ev, evd) =
+ let pegl = pr_evgl_sign evd in
+ (hov 0 (str (string_of_existential ev) ++ str " : " ++ pegl))
+
(* Print an enumerated list of existential variables *)
let rec pr_evars_int i = function
| [] -> (mt ())
@@ -326,21 +376,69 @@ let rec pr_evars_int i = function
str (string_of_existential ev) ++ str " : " ++ pegl)) ++
fnl () ++ pei
-let default_pr_subgoal n =
+let default_pr_subgoal n sigma =
let rec prrec p = function
| [] -> error "No such goal."
| g::rest ->
if p = 1 then
- let pg = default_pr_goal g in
- v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg)
+ let pg = default_pr_goal { sigma=sigma ; it=g } in
+ v 0 (str "subgoal " ++ int n ++ pr_goal_tag g
+ ++ str " is:" ++ cut () ++ pg)
else
prrec (p-1) rest
in
prrec n
+let emacs_print_dependent_evars sigma seeds =
+ let evars () =
+ let evars = Evarutil.gather_dependent_evars sigma seeds in
+ let evars =
+ Intmap.fold begin fun e i s ->
+ let e' = str (string_of_existential e) in
+ match i with
+ | None -> s ++ str" " ++ e' ++ str " open,"
+ | Some i ->
+ s ++ str " " ++ e' ++ str " using " ++
+ Intset.fold begin fun d s ->
+ str (string_of_existential d) ++ str " " ++ s
+ end i (str ",")
+ end evars (str "")
+ in
+ cut () ++
+ str "(dependent evars:" ++ evars ++ str ")" ++ fnl ()
+ in
+ delayed_emacs_cmd evars
+
(* Print open subgoals. Checks for uninstantiated existential variables *)
-let default_pr_subgoals close_cmd sigma = function
- | [] ->
+(* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
+(* spiwack: [pr_first] is true when the first goal must be singled out
+ and printed in its entirety. *)
+(* courtieu: in emacs mode, even less cases where the first goal is printed
+ in its entirety *)
+let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
+ let rec print_stack a = function
+ | [] -> Pp.int a
+ | b::l -> Pp.int a ++ str"-" ++ print_stack b l
+ in
+ let print_unfocused a l =
+ str"unfocused: " ++ print_stack a l
+ in
+ let rec pr_rec n = function
+ | [] -> (mt ())
+ | g::rest ->
+ let pc = pr_concl n sigma g in
+ let prest = pr_rec (n+1) rest in
+ (cut () ++ pc ++ prest)
+ in
+ let print_multiple_goals g l =
+ if pr_first then
+ default_pr_goal { it = g ; sigma = sigma } ++
+ pr_rec 2 l
+ else
+ pr_rec 1 (g::l)
+ in
+ match goals,stack with
+ | [],_ ->
begin
match close_cmd with
Some cmd ->
@@ -348,38 +446,54 @@ let default_pr_subgoals close_cmd sigma = function
str "." ++ fnl ())
| None ->
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))
+ if exl = [] then
+ (str"No more subgoals." ++ fnl ()
+ ++ emacs_print_dependent_evars sigma seeds)
+ else
+ let pei = pr_evars_int 1 exl in
+ (str "No more subgoals but non-instantiated existential " ++
+ str "variables:" ++ fnl () ++ (hov 0 pei)
+ ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
+ str "You can use Grab Existential Variables.")
end
- | [g] ->
- let pg = default_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 = default_pr_goal g1 in
- let prest = pr_rec 2 rest in
- v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut ()
- ++ pg1 ++ prest ++ fnl ())
-
+ | [g],[] when not !Flags.print_emacs ->
+ let pg = default_pr_goal { it = g ; sigma = sigma } in
+ v 0 (
+ str "1 subgoal" ++ pr_goal_tag g ++ cut () ++ pg
+ ++ emacs_print_dependent_evars sigma seeds
+ )
+ | [g],a::l when not !Flags.print_emacs ->
+ let pg = default_pr_goal { it = g ; sigma = sigma } in
+ v 0 (
+ str "1 focused subgoal (" ++ print_unfocused a l ++ str")" ++ pr_goal_tag g ++ cut () ++ pg
+ ++ emacs_print_dependent_evars sigma seeds
+ )
+ | g1::rest,[] ->
+ let goals = print_multiple_goals g1 rest in
+ v 0 (
+ int(List.length rest+1) ++ str" subgoals" ++
+ str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
+ ++ goals ++ fnl ()
+ ++ emacs_print_dependent_evars sigma seeds
+ )
+ | g1::rest,a::l ->
+ let goals = print_multiple_goals g1 rest in
+ v 0 (
+ int(List.length rest+1) ++ str" focused subgoals (" ++
+ print_unfocused a l ++ str")" ++ cut () ++
+ str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
+ ++ goals
+ ++ emacs_print_dependent_evars sigma seeds
+ )
(**********************************************************************)
(* Abstraction layer *)
type printer_pr = {
- pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds;
- pr_subgoal : int -> goal list -> std_ppcmds;
- pr_goal : goal -> std_ppcmds;
+ pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> int list -> goal list -> std_ppcmds;
+ pr_subgoal : int -> evar_map -> goal list -> std_ppcmds;
+ pr_goal : goal sigma -> std_ppcmds;
}
let default_printer_pr = {
@@ -392,7 +506,7 @@ let printer_pr = ref default_printer_pr
let set_printer_pr = (:=) printer_pr
-let pr_subgoals x = !printer_pr.pr_subgoals x
+let pr_subgoals ?pr_first x = !printer_pr.pr_subgoals ?pr_first x
let pr_subgoal x = !printer_pr.pr_subgoal x
let pr_goal x = !printer_pr.pr_goal x
@@ -400,25 +514,43 @@ let pr_goal x = !printer_pr.pr_goal x
(**********************************************************************)
let pr_open_subgoals () =
- let pfts = get_pftreestate () in
- let gls = fst (frontier (proof_of_pftreestate pfts)) in
- match focus() with
- | 0 ->
- let sigma = (top_goal_of_pftreestate pfts).sigma in
- let close_cmd = Decl_mode.get_end_command pfts in
- pr_subgoals close_cmd sigma gls
- | n ->
- assert (n > List.length gls);
- if List.length gls < 2 then
- pr_subgoal n gls
- else
- (* LEM TODO: this way of saying how many subgoals has to be abstracted out*)
- v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++
- pr_subgoal n gls)
+ (* spiwack: it shouldn't be the job of the printer to look up stuff
+ in the [evar_map], I did stuff that way because it was more
+ straightforward, but seriously, [Proof.proof] should return
+ [evar_info]-s instead. *)
+ let p = Proof_global.give_me_the_proof () in
+ let (goals , stack , sigma ) = Proof.proof p in
+ let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in
+ let seeds = Proof.V82.top_evars p in
+ begin match goals with
+ | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
+ begin match bgoals with
+ | [] -> pr_subgoals None sigma seeds stack goals
+ | _ ->
+ (* emacs mode: xml-like flag for detecting information message *)
+ str (emacs_str "<infomsg>") ++
+ str"This subproof is complete, but there are still unfocused goals."
+ ++ str (emacs_str "</infomsg>")
+ ++ fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] bgoals
+ end
+ | _ -> pr_subgoals None sigma seeds stack goals
+ end
let pr_nth_open_subgoal n =
- let pf = proof_of_pftreestate (get_pftreestate ()) in
- pr_subgoal n (fst (frontier pf))
+ let pf = get_pftreestate () in
+ let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
+ pr_subgoal n sigma gls
+
+let pr_goal_by_id id =
+ let p = Proof_global.give_me_the_proof () in
+ let g = Goal.get_by_uid id in
+ let pr gs =
+ v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut ()
+ ++ pr_goal gs)
+ in
+ try
+ Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma})
+ with Not_found -> error "Invalid goal identifier."
(* Elementary tactics *)
@@ -458,7 +590,7 @@ let pr_prim_rule = function
| [] -> mt () in
(str"cofix " ++ pr_id f ++ str" with " ++ print_mut others)
| Refine c ->
- str(if occur_meta c then "refine " else "exact ") ++
+ str(if Termops.occur_meta c then "refine " else "exact ") ++
Constrextern.with_meta_as_hole pr_constr c
| Convert_concl (c,_) ->
@@ -515,7 +647,7 @@ let pr_assumptionset env s =
str (string_of_mp mp ^ "." ^ string_of_label lab)
in
let safe_pr_ltype typ =
- try str " : " ++ pr_ltype typ with _ -> mt ()
+ try str " : " ++ pr_ltype typ with e when Errors.noncritical e -> mt ()
in
let (vars,axioms,opaque) =
ContextObjectMap.fold (fun t typ r ->
@@ -570,3 +702,89 @@ let pr_instance_gmap insts =
prlist_with_sep fnl (fun (gr, insts) ->
prlist_with_sep fnl pr_instance (cmap_to_list insts))
(Gmap.to_list insts)
+
+(** Inductive declarations *)
+
+open Termops
+open Reduction
+open Inductive
+open Inductiveops
+
+let print_params env params =
+ if params = [] then mt () else pr_rel_context env params ++ brk(1,2)
+
+let print_constructors envpar names types =
+ let pc =
+ prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
+ (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c)
+ (Array.to_list (array_map2 (fun n t -> (n,t)) names types))
+ in
+ hv 0 (str " " ++ pc)
+
+let build_ind_type env mip =
+ match mip.mind_arity with
+ | Monomorphic ar -> ar.mind_user_arity
+ | Polymorphic ar ->
+ it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt
+
+let print_one_inductive env mib ((_,i) as ind) =
+ let mip = mib.mind_packets.(i) in
+ let params = mib.mind_params_ctxt in
+ let args = extended_rel_list 0 params in
+ let arity = hnf_prod_applist env (build_ind_type env mip) args in
+ let cstrtypes = Inductive.type_of_constructors ind (mib,mip) in
+ let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
+ let envpar = push_rel_context params env in
+ hov 0 (
+ pr_id mip.mind_typename ++ brk(1,4) ++ print_params env params ++
+ str ": " ++ pr_lconstr_env envpar arity ++ str " :=") ++
+ brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes
+
+let print_mutual_inductive env mind mib =
+ let inds = list_tabulate (fun x -> (mind,x)) (Array.length mib.mind_packets)
+ in
+ hov 0 (
+ str (if mib.mind_finite then "Inductive " else "CoInductive ") ++
+ prlist_with_sep (fun () -> fnl () ++ str" with ")
+ (print_one_inductive env mib) inds)
+
+let get_fields =
+ let rec prodec_rec l subst c =
+ match kind_of_term c with
+ | Prod (na,t,c) ->
+ let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
+ prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c
+ | LetIn (na,b,_,c) ->
+ let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
+ prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c
+ | _ -> List.rev l
+ in
+ prodec_rec [] []
+
+let print_record env mind mib =
+ let mip = mib.mind_packets.(0) in
+ let params = mib.mind_params_ctxt in
+ let args = extended_rel_list 0 params in
+ let arity = hnf_prod_applist env (build_ind_type env mip) args in
+ let cstrtypes = Inductive.type_of_constructors (mind,0) (mib,mip) in
+ let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
+ let fields = get_fields cstrtype in
+ let envpar = push_rel_context params env in
+ hov 0 (
+ hov 0 (
+ str "Record " ++ pr_id mip.mind_typename ++ brk(1,4) ++
+ print_params env params ++
+ str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++
+ str ":= " ++ pr_id mip.mind_consnames.(0)) ++
+ brk(1,2) ++
+ hv 2 (str "{ " ++
+ prlist_with_sep (fun () -> str ";" ++ brk(2,0))
+ (fun (id,b,c) ->
+ pr_id id ++ str (if b then " : " else " := ") ++
+ pr_lconstr_env envpar c) fields) ++ str" }")
+
+let pr_mutual_inductive_body env mind mib =
+ if mib.mind_record & not !Flags.raw_print then
+ print_record env mind mib
+ else
+ print_mutual_inductive env mind mib
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 08:15:31 +0000