aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/termops.ml31
-rw-r--r--ide/ide_slave.ml5
-rw-r--r--kernel/context.ml24
-rw-r--r--kernel/context.mli6
-rw-r--r--printing/printer.ml39
5 files changed, 65 insertions, 40 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index 7afd7a038..3f36059dd 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -17,6 +17,7 @@ open Environ
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
+module NamedListDecl = Context.NamedList.Declaration
(* Sorts and sort family *)
@@ -983,17 +984,25 @@ let rec mem_named_context id ctxt =
let compact_named_context_reverse sign =
let compact l decl =
- let (i1,c1,t1) = match decl with
- | NamedDecl.LocalAssum (i,t) -> i,None,t
- | NamedDecl.LocalDef (i,c,t) -> i,Some c,t
- in
- 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.Named.fold_inside compact ~init:[] sign
+ match decl, l with
+ | NamedDecl.LocalAssum (i,t), [] ->
+ [NamedListDecl.LocalAssum ([i],t)]
+ | NamedDecl.LocalDef (i,c,t), [] ->
+ [NamedListDecl.LocalDef ([i],c,t)]
+ | NamedDecl.LocalAssum (i1,t1), NamedListDecl.LocalAssum (li,t2) :: q ->
+ if Constr.equal t1 t2
+ then NamedListDecl.LocalAssum (i1::li, t2) :: q
+ else NamedListDecl.LocalAssum ([i1],t1) :: NamedListDecl.LocalAssum (li,t2) :: q
+ | NamedDecl.LocalDef (i1,c1,t1), NamedListDecl.LocalDef (li,c2,t2) :: q ->
+ if Constr.equal c1 c2 && Constr.equal t1 t2
+ then NamedListDecl.LocalDef (i1::li, c2, t2) :: q
+ else NamedListDecl.LocalDef ([i1],c1,t1) :: NamedListDecl.LocalDef (li,c2,t2) :: q
+ | NamedDecl.LocalAssum (i,t), q ->
+ NamedListDecl.LocalAssum ([i],t) :: q
+ | NamedDecl.LocalDef (i,c,t), q ->
+ NamedListDecl.LocalDef ([i],c,t) :: q
+ in
+ Context.Named.fold_inside compact ~init:[] sign
let compact_named_context sign = List.rev (compact_named_context_reverse sign)
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 01e37c7c1..36d676f5d 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -195,10 +195,7 @@ let process_goal sigma g =
in
let process_hyp d (env,l) =
let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in
- let d' = List.map (fun name -> match pi2 d with
- | None -> NamedDecl.LocalAssum (name, pi3 d)
- | Some value -> NamedDecl.LocalDef (name, value, pi3 d))
- (pi1 d) in
+ let d' = Context.NamedList.Declaration.to_named_context d in
(List.fold_right Environ.push_named d' env,
(Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in
let (_env, hyps) =
diff --git a/kernel/context.ml b/kernel/context.ml
index 94fcfb486..fed6a5feb 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -416,12 +416,24 @@ module NamedList =
struct
module Declaration =
struct
- type t = Id.t list * Constr.t option * Constr.t
-
- let map_constr f (ids, copt, ty as decl) =
- let copt' = Option.map f copt in
- let ty' = f ty in
- if copt == copt' && ty == ty' then decl else (ids, copt', ty')
+ type t =
+ | LocalAssum of Id.t list * Constr.t
+ | LocalDef of Id.t list * Constr.t * Constr.t
+
+ let map_constr f = function
+ | LocalAssum (ids, ty) as decl ->
+ let ty' = f ty in
+ if ty == ty' then decl else LocalAssum (ids, ty')
+ | LocalDef (ids, c, ty) as decl ->
+ let ty' = f ty in
+ let c' = f c in
+ if c == c' && ty == ty' then decl else LocalDef (ids,c',ty')
+
+ let to_named_context = function
+ | LocalAssum (ids, t) ->
+ List.map (fun id -> Named.Declaration.LocalAssum (id,t)) ids
+ | LocalDef (ids, v, t) ->
+ List.map (fun id -> Named.Declaration.LocalDef (id,v,t)) ids
end
type t = Declaration.t list
diff --git a/kernel/context.mli b/kernel/context.mli
index c5da51381..72fbfb540 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -255,8 +255,12 @@ module NamedList :
sig
module Declaration :
sig
- type t = Id.t list * Constr.t option * Constr.t
+ type t =
+ | LocalAssum of Id.t list * Constr.t
+ | LocalDef of Id.t list * Constr.t * Constr.t
+
val map_constr : (Constr.t -> Constr.t) -> t -> t
+ val to_named_context : t -> Named.t
end
type t = Declaration.t list
diff --git a/printing/printer.ml b/printing/printer.ml
index 977746837..5c62c2af0 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -24,6 +24,7 @@ open Declarations
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
+module NamedListDecl = Context.NamedList.Declaration
let emacs_str s =
if !Flags.print_emacs then s else ""
@@ -251,27 +252,29 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
(**********************************************************************)
(* Contexts and declarations *)
-let pr_var_decl_skel pr_id env sigma (id,c,typ) =
- let pbody = match c with
- | None -> (mt ())
- | Some c ->
- (* Force evaluation *)
- let pb = pr_lconstr_env env sigma c in
- let pb = if isCast c then surround pb else pb in
- (str" := " ++ pb ++ cut () ) in
+let pr_var_list_decl env sigma decl =
+ let ids, pbody, typ = match decl with
+ | NamedListDecl.LocalAssum (ids, typ) ->
+ ids, mt (), typ
+ | NamedListDecl.LocalDef (ids,c,typ) ->
+ (* Force evaluation *)
+ let pb = pr_lconstr_env env sigma c in
+ let pb = if isCast c then surround pb else pb in
+ ids, (str" := " ++ pb ++ cut ()), typ
+ in
+ let pids = prlist_with_sep pr_comma pr_id ids in
let pt = pr_ltype_env env sigma typ in
let ptyp = (str" : " ++ pt) in
- (pr_id id ++ hov 0 (pbody ++ ptyp))
-
-let pr_var_decl env sigma d =
- let d = match d with
- | NamedDecl.LocalAssum (id,typ) -> id, None, typ
- | NamedDecl.LocalDef (id,c,typ) -> id, Some c, typ
+ hov 0 (pids ++ pbody ++ ptyp)
+
+let pr_var_decl env sigma decl =
+ let decl = match decl with
+ | NamedDecl.LocalAssum (id, t) ->
+ NamedListDecl.LocalAssum ([id], t)
+ | NamedDecl.LocalDef (id,c,t) ->
+ NamedListDecl.LocalDef ([id],c,t)
in
- pr_var_decl_skel pr_id env sigma d
-
-let pr_var_list_decl env sigma (l,c,typ) =
- hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ))
+ pr_var_list_decl env sigma decl
let pr_rel_decl env sigma decl =
let na = RelDecl.get_name decl in
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 14:10:44 +0000