diff options
| -rw-r--r-- | ide/ide_slave.ml | 19 | ||||
| -rw-r--r-- | kernel/context.ml | 6 | ||||
| -rw-r--r-- | kernel/context.mli | 4 | ||||
| -rw-r--r-- | printing/printer.ml | 8 | ||||
| -rw-r--r-- | printing/printer.mli | 1 |
5 files changed, 32 insertions, 6 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 6b2c52123..42bc939b5 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -168,17 +168,28 @@ let concl_next_tac sigma concl = "right" ]) +let compact_named_context c = + let compact l (i1,c1,t1) = + match l with + | [] -> [[i1],c1,t1] + | (l2,c2,t2)::q -> + if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 + then (i1::l2,c2,t2)::q + else ([i1],c1,t1)::l + in Context.fold_named_context_reverse compact ~init:[] c + let process_goal sigma g = let env = Goal.V82.env sigma g in + let min_env = Environ.reset_context env in let id = Goal.uid g in let ccl = let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in - let process_hyp h_env d acc = - let d = Context.map_named_declaration (Reductionops.nf_evar sigma) d in - (string_of_ppcmds (pr_var_decl h_env d)) :: acc in + let process_hyp d = + let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in + (string_of_ppcmds (pr_var_list_decl min_env d)) in let hyps = - List.rev (Environ.fold_named_context process_hyp env ~init: []) in + List.map process_hyp (compact_named_context (Environ.named_context env)) in { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } let goals () = diff --git a/kernel/context.ml b/kernel/context.ml index bdc4c067a..5256ee417 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -23,10 +23,13 @@ open Names (***************************************************************************) type named_declaration = Id.t * Constr.t option * Constr.t +type named_list_declaration = Id.t list * Constr.t option * Constr.t type rel_declaration = Name.t * Constr.t option * Constr.t -let map_named_declaration f (id, (v : Constr.t option), ty) = +let map_named_declaration_skel f (id, (v : Constr.t option), ty) = (id, Option.map f v, f ty) +let map_named_list_declaration = map_named_declaration_skel +let map_named_declaration = map_named_declaration_skel let map_rel_declaration = map_named_declaration @@ -77,6 +80,7 @@ let rel_context_nhyps hyps = goal assumptions. *) type named_context = named_declaration list +type compacted_named_context = named_list_declaration list let empty_named_context = [] diff --git a/kernel/context.mli b/kernel/context.mli index 048edef95..1d732d273 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -19,10 +19,13 @@ open Names purpose) *) type named_declaration = Id.t * Constr.t option * Constr.t +type named_list_declaration = Id.t list * Constr.t option * Constr.t type rel_declaration = Name.t * Constr.t option * Constr.t val map_named_declaration : (Constr.t -> Constr.t) -> named_declaration -> named_declaration +val map_named_list_declaration : + (Constr.t -> Constr.t) -> named_list_declaration -> named_list_declaration val map_rel_declaration : (Constr.t -> Constr.t) -> rel_declaration -> rel_declaration @@ -51,6 +54,7 @@ val eq_rel_declaration : type named_context = named_declaration list type section_context = named_context +type compacted_named_context = named_list_declaration list type rel_context = rel_declaration list (** In [rel_context], more recent declaration is on top *) diff --git a/printing/printer.ml b/printing/printer.ml index ed872afc6..7938b7bb0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -219,7 +219,7 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) (**********************************************************************) (* Contexts and declarations *) -let pr_var_decl env (id,c,typ) = +let pr_var_decl_skel pr_id env (id,c,typ) = let pbody = match c with | None -> (mt ()) | Some c -> @@ -231,6 +231,12 @@ let pr_var_decl env (id,c,typ) = let ptyp = (str" : " ++ pt) in (pr_id id ++ hov 0 (pbody ++ ptyp)) +let pr_var_decl env (id,c,typ) = + pr_var_decl_skel pr_id env (id,c,typ) + +let pr_var_list_decl env (l,c,typ) = + hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env (l,c,typ)) + let pr_rel_decl env (na,c,typ) = let pbody = match c with | None -> mt () diff --git a/printing/printer.mli b/printing/printer.mli index aa949232a..6be208053 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -106,6 +106,7 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds val pr_var_decl : env -> named_declaration -> std_ppcmds +val pr_var_list_decl : env -> named_list_declaration -> std_ppcmds val pr_rel_decl : env -> rel_declaration -> std_ppcmds val pr_named_context : env -> named_context -> std_ppcmds |