merging conflicts with the original "trunk__CLEANUP__Context__2" branch

1 files changed, 369 insertions, 193 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 3be1e83230..4e53b73a28 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -32,215 +32,391 @@ open Names
 (** Representation of contexts that can capture anonymous as well as non-anonymous variables.
     Individual declarations are then designated by de Bruijn indexes. *)
 module Rel =
+struct
+  (** Representation of {e local declarations}. *)
+  module Declaration =
   struct
-    (** Representation of {e local declarations}.
-
-        [(name, None, typ)] represents a {e local assumption}.
-        In the Reference Manual we denote them as [(name:typ)].
-
-        [(name, Some value, typ)] represents a {e local definition}.
-        In the Reference Manual we denote them as [(name := value : typ)].
-    *)
-    module Declaration =
-      struct
-	type t = Name.t * Constr.t option * Constr.t
-
-	(** Map all terms in a given declaration. *)
-	let map f (n, v, ty) = (n, Option.map f v, f ty)
-
-	(** Reduce all terms in a given declaration to a single value. *)
-	let fold f (_, v, ty) a = f ty (Option.fold_right f v a)
-
-	(** Check whether any term in a given declaration satisfies a given predicate. *)
-	let exists f (_, v, ty) = Option.cata f false v || f ty
-
-	(** Check whether all terms in a given declaration satisfy a given predicate. *)
-	let for_all f (_, v, ty) = Option.cata f true v && f ty
-
-	(** Check whether the two given declarations are equal. *)
-	let equal (n1, v1, ty1) (n2, v2, ty2) =
-	  Name.equal n1 n2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
-      end
-
-    (** Rel-context is represented as a list of declarations.
-        Inner-most declarations are at the beginning of the list.
-        Outer-most declarations are at the end of the list. *)
-    type t = Declaration.t list
-
-    (** empty rel-context *)
-    let empty = []
-
-    (** Return a new rel-context enriched by with a given inner-most declaration. *)
-    let add d ctx = d :: ctx
-
-    (** Return a declaration designated by a given de Bruijn index.
-        @raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *)
-    let rec lookup n ctx =
-      match n, ctx with
-      | 1, decl :: _ -> decl
-      | n, _ :: sign -> lookup (n-1) sign
-      | _, []        -> raise Not_found
-
-    (** Map all terms in a given rel-context. *)
-    let map f =
-      let map_decl (n, body_o, typ as decl) =
-	let body_o' = Option.smartmap f body_o in
-	let typ' = f typ in
-	if body_o' == body_o && typ' == typ then decl else
-          (n, body_o', typ')
-      in
-      List.smartmap map_decl
-
-    (** Reduce all terms in a given rel-context to a single value.
-        Innermost declarations are processed first. *)
-    let fold_inside f ~init = List.fold_left f init
-
-    (** Reduce all terms in a given rel-context to a single value.
-        Outermost declarations are processed first. *)
-    let fold_outside f l ~init = List.fold_right f l init
-
-    (** Perform a given action on every declaration in a given rel-context. *)
-    let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
-
-    (** Return the number of {e local declarations} in a given context. *)
-    let length = List.length
-
-    (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
-        with n = |Δ| and with the local definitions of [Γ] skipped in
-        [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
-    let nhyps =
-      let rec nhyps acc = function
-	| [] -> acc
-	| (_,None,_)::hyps -> nhyps (1+acc) hyps
-	| (_,Some _,_)::hyps -> nhyps acc hyps in
-      nhyps 0
-
-    (** Map a given rel-context to a list where each {e local assumption} is mapped to [true]
-        and each {e local definition} is mapped to [false]. *)
-    let to_tags =
-      let rec aux l = function
-	| [] -> l
-	| (_,Some _,_)::ctx -> aux (true::l) ctx
-	| (_,None,_)::ctx -> aux (false::l) ctx
-      in aux []
-
-    (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
-        with n = |Δ| and with the {e local definitions} of [Γ] skipped in
-        [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
-    let to_extended_list n =
-      let rec reln l p = function
-	| (_, None, _) :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
-	| (_, Some _, _) :: hyps -> reln l (p+1) hyps
-	| [] -> l
-      in
-      reln [] 1
-
-    (** [extended_vect n Γ] does the same, returning instead an array. *)
-    let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps)
+    (* local declaration *)
+    type t =
+      | LocalAssum of Name.t * Constr.t            (** name, type *)
+      | LocalDef of Name.t * Constr.t * Constr.t   (** name, value, type *)
+
+    (** Return the name bound by a given declaration. *)
+    let get_name = function
+      | LocalAssum (na,_)
+      | LocalDef (na,_,_) -> na
+
+    (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+    let get_value = function
+      | LocalAssum _ -> None
+      | LocalDef (_,v,_) -> Some v
+                                 
+    (** Return the type of the name bound by a given declaration. *)
+    let get_type = function
+      | LocalAssum (_,ty)
+      | LocalDef (_,_,ty) -> ty
+                               
+    (** Set the name that is bound by a given declaration. *)
+    let set_name na = function
+      | LocalAssum (_,ty) -> LocalAssum (na, ty)
+      | LocalDef (_,v,ty) -> LocalDef (na, v, ty)
+
+    (** Set the type of the bound variable in a given declaration. *)
+    let set_type ty = function
+      | LocalAssum (na,_) -> LocalAssum (na, ty)
+      | LocalDef (na,v,_) -> LocalDef (na, v, ty)
+
+    (** Return [true] iff a given declaration is a local assumption. *)
+    let is_local_assum = function
+      | LocalAssum _ -> true
+      | LocalDef _ -> false
+
+    (** Return [true] iff a given declaration is a local definition. *)
+    let is_local_def = function
+      | LocalAssum _ -> false
+      | LocalDef _ -> true
+
+    (** Check whether any term in a given declaration satisfies a given predicate. *)
+    let exists f = function
+      | LocalAssum (_, ty) -> f ty
+      | LocalDef (_, v, ty) -> f v || f ty
+
+      (** Check whether all terms in a given declaration satisfy a given predicate. *)
+    let for_all f = function
+      | LocalAssum (_, ty) -> f ty
+      | LocalDef (_, v, ty) -> f v && f ty
+
+    (** Check whether the two given declarations are equal. *)
+    let equal decl1 decl2 =
+      match decl1, decl2 with
+      | LocalAssum (n1,ty1), LocalAssum (n2, ty2) ->
+          Name.equal n1 n2 && Constr.equal ty1 ty2
+      | LocalDef (n1,v1,ty1), LocalDef (n2,v2,ty2) ->
+          Name.equal n1 n2 && Constr.equal v1 v2 && Constr.equal ty1 ty2
+      | _ ->
+          false
+
+    (** Map the name bound by a given declaration. *)
+    let map_name f = function
+      | LocalAssum (na, ty) as decl ->
+          let na' = f na in
+          if na == na' then decl else LocalAssum (na', ty)
+      | LocalDef (na, v, ty) as decl ->
+          let na' = f na in
+          if na == na' then decl else LocalDef (na', v, ty)
+
+    (** For local assumptions, this function returns the original local assumptions.
+        For local definitions, this function maps the value in the local definition. *)
+    let map_value f = function
+      | LocalAssum _ as decl -> decl
+      | LocalDef (na, v, t) as decl ->
+          let v' = f v in
+          if v == v' then decl else LocalDef (na, v', t)
+
+    (** Map the type of the name bound by a given declaration. *)
+    let map_type f = function
+      | LocalAssum (na, ty) as decl ->
+          let ty' = f ty in
+          if ty == ty' then decl else LocalAssum (na, ty')
+      | LocalDef (na, v, ty) as decl ->         
+          let ty' = f ty in
+          if ty == ty' then decl else LocalDef (na, v, ty')
+
+    (** Map all terms in a given declaration. *)
+    let map_constr f = function
+      | LocalAssum (na, ty) as decl ->
+          let ty' = f ty in
+          if ty == ty' then decl else LocalAssum (na, ty')
+      | LocalDef (na, v, ty) as decl ->
+          let v' = f v in
+          let ty' = f ty in
+          if v == v' && ty == ty' then decl else LocalDef (na, v', ty')
+
+    (** Perform a given action on all terms in a given declaration. *)
+    let iter_constr f = function
+      | LocalAssum (_,ty) -> f ty
+      | LocalDef (_,v,ty) -> f v; f ty
+
+    (** Reduce all terms in a given declaration to a single value. *)
+    let fold f decl acc =
+      match decl with
+      | LocalAssum (n,ty) -> f ty acc
+      | LocalDef (n,v,ty) -> f ty (f v acc)
+
+    let to_tuple = function
+      | LocalAssum (na, ty) -> na, None, ty
+      | LocalDef (na, v, ty) -> na, Some v, ty
+
+    let of_tuple = function
+      | n, None, ty -> LocalAssum (n,ty)
+      | n, Some v, ty -> LocalDef (n,v,ty)
   end
 
+  (** Rel-context is represented as a list of declarations.
+      Inner-most declarations are at the beginning of the list.
+      Outer-most declarations are at the end of the list. *)
+  type t = Declaration.t list
+
+  (** empty rel-context *)
+  let empty = []
+
+  (** Return a new rel-context enriched by with a given inner-most declaration. *)
+  let add d ctx = d :: ctx
+
+  (** Return the number of {e local declarations} in a given context. *)
+  let length = List.length
+
+  (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+      with n = |Δ| and with the local definitions of [Γ] skipped in
+      [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+  let nhyps =
+    let open Declaration in
+    let rec nhyps acc = function
+      | [] -> acc
+      | LocalAssum _ :: hyps -> nhyps (succ acc) hyps
+      | LocalDef _ :: hyps -> nhyps acc hyps
+    in
+    nhyps 0
+
+  (** Return a declaration designated by a given de Bruijn index.
+      @raise Not_found if the designated de Bruijn index is not present in the designated rel-context. *)
+  let rec lookup n ctx =
+    match n, ctx with
+    | 1, decl :: _ -> decl
+    | n, _ :: sign -> lookup (n-1) sign
+    | _, []        -> raise Not_found
+
+  (** Check whether given two rel-contexts are equal. *)
+  let equal = List.equal Declaration.equal
+
+  (** Map all terms in a given rel-context. *)
+  let map f = List.smartmap (Declaration.map_constr f)
+
+  (** Perform a given action on every declaration in a given rel-context. *)
+  let iter f = List.iter (Declaration.iter_constr f)
+
+  (** Reduce all terms in a given rel-context to a single value.
+      Innermost declarations are processed first. *)
+  let fold_inside f ~init = List.fold_left f init
+
+  (** Reduce all terms in a given rel-context to a single value.
+      Outermost declarations are processed first. *)
+  let fold_outside f l ~init = List.fold_right f l init
+
+  (** Map a given rel-context to a list where each {e local assumption} is mapped to [true]
+      and each {e local definition} is mapped to [false]. *)
+  let to_tags =
+    let rec aux l = function
+      | [] -> l
+      | Declaration.LocalDef _ :: ctx -> aux (true::l) ctx
+      | Declaration.LocalAssum _ :: ctx -> aux (false::l) ctx
+    in aux []
+
+  (** [extended_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+      with n = |Δ| and with the {e local definitions} of [Γ] skipped in
+      [args]. Example: for [x:T, y:=c, z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+  let to_extended_list n =
+    let rec reln l p = function
+      | Declaration.LocalAssum _ :: hyps -> reln (Constr.mkRel (n+p) :: l) (p+1) hyps
+      | Declaration.LocalDef _ :: hyps -> reln l (p+1) hyps
+      | [] -> l
+    in
+    reln [] 1
+
+  (** [extended_vect n Γ] does the same, returning instead an array. *)
+  let to_extended_vect n hyps = Array.of_list (to_extended_list n hyps)
+end
+
 (** This module represents contexts that can capture non-anonymous variables.
     Individual declarations are then designated by the identifiers they bind. *)
 module Named =
+struct
+  (** Representation of {e local declarations}. *)
+  module Declaration =
   struct
-    (** Representation of {e local declarations}.
-
-        [(id, None, typ)] represents a {e local assumption}.
-        In the Reference Manual we denote them as [(name:typ)].
-
-        [(id, Some value, typ)] represents a {e local definition}.
-        In the Reference Manual we denote them as [(name := value : typ)].
-   *)
-    module Declaration =
-      struct
-	(** Named-context is represented as a list of declarations.
-            Inner-most declarations are at the beginning of the list.
-            Outer-most declarations are at the end of the list. *)
-	type t = Id.t * Constr.t option * Constr.t
-
-	(** Map all terms in a given declaration. *)
-	let map = Rel.Declaration.map
-
-	(** Reduce all terms in a given declaration to a single value. *)
-	let fold f (_, v, ty) a = f ty (Option.fold_right f v a)
-
-	(** Check whether any term in a given declaration satisfies a given predicate. *)
-	let exists f (_, v, ty) = Option.cata f false v || f ty
-
-	(** Check whether all terms in a given declaration satisfy a given predicate. *)
-	let for_all f (_, v, ty) = Option.cata f true v && f ty
-
-	(** Check whether the two given declarations are equal. *)
-	let equal (i1, v1, ty1) (i2, v2, ty2) =
-	  Id.equal i1 i2 && Option.equal Constr.equal v1 v2 && Constr.equal ty1 ty2
-      end
-
-    type t = Declaration.t list
+    (** local declaration *)
+    type t =
+      | LocalAssum of Id.t * Constr.t             (** identifier, type *)
+      | LocalDef of Id.t * Constr.t * Constr.t    (** identifier, value, type *)
+
+    (** Return the identifier bound by a given declaration. *)
+    let get_id = function
+      | LocalAssum (id,_) -> id
+      | LocalDef (id,_,_) -> id
+
+    (** Return [Some value] for local-declarations and [None] for local-assumptions. *)
+    let get_value = function
+      | LocalAssum _ -> None
+      | LocalDef (_,v,_) -> Some v
+
+    (** Return the type of the name bound by a given declaration. *)
+    let get_type = function
+      | LocalAssum (_,ty)
+      | LocalDef (_,_,ty) -> ty
+
+    (** Set the identifier that is bound by a given declaration. *)
+    let set_id id = function
+      | LocalAssum (_,ty) -> LocalAssum (id, ty)
+      | LocalDef (_, v, ty) -> LocalDef (id, v, ty)
+
+    (** Set the type of the bound variable in a given declaration. *)
+    let set_type ty = function
+      | LocalAssum (id,_) -> LocalAssum (id, ty)
+      | LocalDef (id,v,_) -> LocalDef (id, v, ty)
+
+    (** Return [true] iff a given declaration is a local assumption. *)
+    let is_local_assum = function
+      | LocalAssum _ -> true
+      | LocalDef _ -> false
+
+    (** Return [true] iff a given declaration is a local definition. *)
+    let is_local_def = function
+      | LocalDef _ -> true
+      | LocalAssum _ -> false
+
+    (** Check whether any term in a given declaration satisfies a given predicate. *)
+    let exists f = function
+      | LocalAssum (_, ty) -> f ty
+      | LocalDef (_, v, ty) -> f v || f ty
+
+    (** Check whether all terms in a given declaration satisfy a given predicate. *)
+    let for_all f = function
+      | LocalAssum (_, ty) -> f ty
+      | LocalDef (_, v, ty) -> f v && f ty
+
+    (** Check whether the two given declarations are equal. *)
+    let equal decl1 decl2 =
+      match decl1, decl2 with
+      | LocalAssum (id1, ty1), LocalAssum (id2, ty2) ->
+          Id.equal id1 id2 && Constr.equal ty1 ty2
+      | LocalDef (id1, v1, ty1), LocalDef (id2, v2, ty2) ->
+          Id.equal id1 id2 && Constr.equal v1 v2 && Constr.equal ty1 ty2
+      | _ ->
+          false
+
+    (** Map the identifier bound by a given declaration. *)
+    let map_id f = function
+      | LocalAssum (id, ty) as decl ->
+          let id' = f id in
+          if id == id' then decl else LocalAssum (id', ty)
+      | LocalDef (id, v, ty) as decl ->
+          let id' = f id in
+          if id == id' then decl else LocalDef (id', v, ty)
+
+    (** For local assumptions, this function returns the original local assumptions.
+        For local definitions, this function maps the value in the local definition. *)
+    let map_value f = function
+      | LocalAssum _ as decl -> decl
+      | LocalDef (na, v, t) as decl ->
+          let v' = f v in
+          if v == v' then decl else LocalDef (na, v', t)
+
+    (** Map the type of the name bound by a given declaration. *)
+    let map_type f = function
+      | LocalAssum (id, ty) as decl ->
+          let ty' = f ty in
+          if ty == ty' then decl else LocalAssum (id, ty')
+      | LocalDef (id, v, ty) as decl ->
+          let ty' = f ty in
+          if ty == ty' then decl else LocalDef (id, v, ty')
+
+    (** Map all terms in a given declaration. *)
+    let map_constr f = function
+      | LocalAssum (id, ty) as decl ->
+          let ty' = f ty in
+          if ty == ty' then decl else LocalAssum (id, ty')
+      | LocalDef (id, v, ty) as decl ->
+          let v' = f v in
+          let ty' = f ty in
+          if v == v' && ty == ty' then decl else LocalDef (id, v', ty')
+
+    (** Perform a given action on all terms in a given declaration. *)
+    let iter_constr f = function
+      | LocalAssum (_, ty) -> f ty
+      | LocalDef (_, v, ty) -> f v; f ty
+
+    (** Reduce all terms in a given declaration to a single value. *)
+    let fold f decl a =
+      match decl with
+      | LocalAssum (_, ty) -> f ty a
+      | LocalDef (_, v, ty) -> a |> f v |> f ty
+
+    let to_tuple = function
+      | LocalAssum (id, ty) -> id, None, ty
+      | LocalDef (id, v, ty) -> id, Some v, ty
+
+    let of_tuple = function
+      | id, None, ty -> LocalAssum (id, ty)
+      | id, Some v, ty -> LocalDef (id, v, ty)
+  end
 
-    (** empty named-context *)
-    let empty = []
-
-    (** empty named-context *)
-    let add d ctx = d :: ctx
-
-    (** Return a declaration designated by a given de Bruijn index.
-        @raise Not_found if the designated identifier is not present in the designated named-context. *)
-    let rec lookup id = function
-      | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
-      | _ :: sign -> lookup id sign
-      | [] -> raise Not_found
-
-    (** Map all terms in a given named-context. *)
-    let map f =
-      let map_decl (n, body_o, typ as decl) =
-	let body_o' = Option.smartmap f body_o in
-	let typ' = f typ in
-	if body_o' == body_o && typ' == typ then decl else
-          (n, body_o', typ')
-      in
-      List.smartmap map_decl
-
-    (** Reduce all terms in a given named-context to a single value.
-        Innermost declarations are processed first. *)
-    let fold_inside f ~init = List.fold_left f init
-
-    (** Reduce all terms in a given named-context to a single value.
-        Outermost declarations are processed first. *)
-    let fold_outside f l ~init = List.fold_right f l init
-
-    (** Perform a given action on every declaration in a given named-context. *)
-    let iter f = List.iter (fun (_,b,t) -> f t; Option.iter f b)
-
-    (** Return the number of {e local declarations} in a given named-context. *)
-    let length = List.length
-
-    (** Check whether given two named-contexts are equal. *)
-    let equal = List.equal Declaration.equal
-
-    (** Return the set of all identifiers bound in a given named-context. *)
-    let to_vars =
-      List.fold_left (fun accu (id, _, _) -> Id.Set.add id accu) Id.Set.empty
-
-    (** [instance_from_named_context Ω] builds an instance [args] such
-        that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
-        definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
-        gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
-    let to_instance =
-      let filter = function
-	| (id, None, _) -> Some (Constr.mkVar id)
-	| (_, Some _, _) -> None
-      in
-      List.map_filter filter
+  (** Named-context is represented as a list of declarations.
+      Inner-most declarations are at the beginning of the list.
+      Outer-most declarations are at the end of the list. *)
+  type t = Declaration.t list
+
+  (** empty named-context *)
+  let empty = []
+
+  (** empty named-context *)
+  let add d ctx = d :: ctx
+
+  (** Return the number of {e local declarations} in a given named-context. *)
+  let length = List.length
+
+(** Return a declaration designated by a given de Bruijn index.
+    @raise Not_found if the designated identifier is not present in the designated named-context. *)   let rec lookup id = function
+    | decl :: _ when Id.equal id (Declaration.get_id decl) -> decl
+    | _ :: sign -> lookup id sign
+    | [] -> raise Not_found
+
+  (** Check whether given two named-contexts are equal. *)
+  let equal = List.equal Declaration.equal
+
+  (** Map all terms in a given named-context. *)
+  let map f = List.smartmap (Declaration.map_constr f)
+
+  (** Perform a given action on every declaration in a given named-context. *)
+  let iter f = List.iter (Declaration.iter_constr f)
+
+  (** Reduce all terms in a given named-context to a single value.
+      Innermost declarations are processed first. *)
+  let fold_inside f ~init = List.fold_left f init
+
+  (** Reduce all terms in a given named-context to a single value.
+      Outermost declarations are processed first. *)
+  let fold_outside f l ~init = List.fold_right f l init
+
+  (** Return the set of all identifiers bound in a given named-context. *)
+  let to_vars =
+    List.fold_left (fun accu decl -> Id.Set.add (Declaration.get_id decl) accu) Id.Set.empty
+
+  (** [instance_from_named_context Ω] builds an instance [args] such
+      that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
+      definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
+      gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
+  let to_instance =
+    let filter = function
+      | Declaration.LocalAssum (id, _) -> Some (Constr.mkVar id)
+      | _ -> None
+    in
+    List.map_filter filter
   end
 
 module NamedList =
   struct
     module Declaration =
       struct
-	type t = Id.t list * Constr.t option * Constr.t
-	let map = Named.Declaration.map
+        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')
       end
+
     type t = Declaration.t list
+
     let fold f l ~init = List.fold_right f l init
   end