CLEANUP: changing the definition of the "Context.NamedList.Declaration" type

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