5 files changed, 190 insertions, 21 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 9bf743152f..c73fe7fbde 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -503,7 +503,79 @@ let fold_constr_with_binders g f n acc c =
    not recursive and the order with which subterms are processed is
    not specified *)
 
-let map f c = match kind c with
+let rec map_under_context f n d =
+  if n = 0 then f d else
+  match kind d with
+  | LetIn (na,b,t,c) ->
+    let b' = f b in
+    let t' = f t in
+    let c' = map_under_context f (n-1) c in
+    if b' == b && t' == t && c' == c then d
+    else mkLetIn (na,b',t',c')
+  | Lambda (na,t,b) ->
+    let t' = f t in
+    let b' = map_under_context f (n-1) b in
+    if t' == t && b' == b then d
+    else mkLambda (na,t',b')
+  | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
+
+let map_branches f ci bl =
+  let nl = Array.map List.length ci.ci_pp_info.cstr_tags in
+  let bl' = Array.map2 (map_under_context f) nl bl in
+  if Array.for_all2 (==) bl' bl then bl else bl'
+
+let map_return_predicate f ci p =
+  map_under_context f (List.length ci.ci_pp_info.ind_tags) p
+
+let rec map_under_context_with_binders g f l n d =
+  if n = 0 then f l d else
+  match kind d with
+  | LetIn (na,b,t,c) ->
+      let b' = f l b in
+      let t' = f l t in
+      let c' = map_under_context_with_binders g f (g l) (n-1) c in
+      if b' == b && t' == t && c' == c then d
+      else mkLetIn (na,b',t',c')
+  | Lambda (na,t,b) ->
+      let t' = f l t in
+      let b' = map_under_context_with_binders g f (g l) (n-1) b in
+      if t' == t && b' == b then d
+      else mkLambda (na,t',b')
+  | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
+
+let map_branches_with_binders g f l ci bl =
+  let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
+  let bl' = Array.map2 (map_under_context_with_binders g f l) tags bl in
+  if Array.for_all2 (==) bl' bl then bl else bl'
+
+let map_return_predicate_with_binders g f l ci p =
+  map_under_context_with_binders g f l (List.length ci.ci_pp_info.ind_tags) p
+
+let rec map_under_context_with_full_binders g f l n d =
+  if n = 0 then f l d else
+    match kind d with
+    | LetIn (na,b,t,c) ->
+       let b' = f l b in
+       let t' = f l t in
+       let c' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in
+       if b' == b && t' == t && c' == c then d
+       else mkLetIn (na,b',t',c')
+    | Lambda (na,t,b) ->
+       let t' = f l t in
+       let b' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in
+       if t' == t && b' == b then d
+       else mkLambda (na,t',b')
+    | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
+
+let map_branches_with_full_binders g f l ci bl =
+  let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
+  let bl' = Array.map2 (map_under_context_with_full_binders g f l) tags bl in
+  if Array.for_all2 (==) bl' bl then bl else bl'
+
+let map_return_predicate_with_full_binders g f l ci p =
+  map_under_context_with_full_binders g f l (List.length ci.ci_pp_info.ind_tags) p
+
+let map_gen userview f c = match kind c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
   | Cast (b,k,t) ->
@@ -540,6 +612,12 @@ let map f c = match kind c with
       let l' = Array.Smart.map f l in
       if l'==l then c
       else mkEvar (e, l')
+  | Case (ci,p,b,bl) when userview ->
+      let b' = f b in
+      let p' = map_return_predicate f ci p in
+      let bl' = map_branches f ci bl in
+      if b'==b && p'==p && bl'==bl then c
+      else mkCase (ci, p', b', bl')
   | Case (ci,p,b,bl) ->
       let b' = f b in
       let p' = f p in
@@ -557,6 +635,9 @@ let map f c = match kind c with
       if tl'==tl && bl'==bl then c
       else mkCoFix (ln,(lna,tl',bl'))
 
+let map_user_view = map_gen true
+let map = map_gen false
+
 (* Like {!map} but with an accumulator. *)
 
 let fold_map f accu c = match kind c with
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 70acf19328..9cc044316b 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -381,6 +381,85 @@ type rel_context = rel_declaration list
 type named_context = named_declaration list
 type compacted_context = compacted_declaration list
 
+(** {6 Functionals working on expressions canonically abstracted over
+       a local context (possibly with let-ins)} *)
+
+(** [map_under_context f l c] maps [f] on the immediate subterms of a
+    term abstracted over a context of length [n] (local definitions
+    are counted) *)
+
+val map_under_context : (constr -> constr) -> int -> constr -> constr
+
+(** [map_branches f br] maps [f] on the immediate subterms of an array
+   of "match" branches [br] in canonical eta-let-expanded form; it is
+   not recursive and the order with which subterms are processed is
+   not specified; it preserves sharing; the immediate subterms are the
+   types and possibly terms occurring in the context of each branch as
+   well as the body of each branch *)
+
+val map_branches : (constr -> constr) -> case_info -> constr array -> constr array
+
+(** [map_return_predicate f p] maps [f] on the immediate subterms of a
+   return predicate of a "match" in canonical eta-let-expanded form;
+   it is not recursive and the order with which subterms are processed
+   is not specified; it preserves sharing; the immediate subterms are
+   the types and possibly terms occurring in the context of each
+   branch as well as the body of the predicate *)
+
+val map_return_predicate : (constr -> constr) -> case_info -> constr -> constr
+
+(** [map_under_context_with_binders g f n l c] maps [f] on the
+    immediate subterms of a term abstracted over a context of length
+    [n] (local definitions are counted); it preserves sharing; it
+    carries an extra data [n] (typically a lift index) which is
+    processed by [g] (which typically add 1 to [n]) at each binder
+    traversal *)
+
+val map_under_context_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr
+
+(** [map_branches_with_binders f br] maps [f] on the immediate
+   subterms of an array of "match" branches [br] in canonical
+   eta-let-expanded form; it carries an extra data [n] (typically a
+   lift index) which is processed by [g] (which typically adds 1 to
+   [n]) at each binder traversal; it is not recursive and the order
+   with which subterms are processed is not specified; it preserves
+   sharing; the immediate subterms are the types and possibly terms
+   occurring in the context of the branch as well as the body of the
+   branch *)
+
+val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array
+
+(** [map_return_predicate_with_binders f p] maps [f] on the immediate
+   subterms of a return predicate of a "match" in canonical
+   eta-let-expanded form; it carries an extra data [n] (typically a
+   lift index) which is processed by [g] (which typically adds 1 to
+   [n]) at each binder traversal; it is not recursive and the order
+   with which subterms are processed is not specified; it preserves
+   sharing; the immediate subterms are the types and possibly terms
+   occurring in the context of each branch as well as the body of the
+   predicate *)
+
+val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr
+
+(** [map_under_context_with_full_binders g f n l c] is similar to
+    [map_under_context_with_binders] except that [g] takes also a full
+    binder as argument and that only the number of binders (and not
+    their signature) is required *)
+
+val map_under_context_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr
+
+(** [map_branches_with_full_binders g f l br] is equivalent to
+   [map_branches_with_binders] but using
+   [map_under_context_with_full_binders] *)
+
+val map_branches_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array
+
+(** [map_return_predicate_with_full_binders g f l p] is equivalent to
+   [map_return_predicate_with_binders] but using
+   [map_under_context_with_full_binders] *)
+
+val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr
+
 (** {6 Functionals working on the immediate subterm of a construction } *)
 
 (** [fold f acc c] folds [f] on the immediate subterms of [c]
@@ -395,6 +474,13 @@ val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
 
 val map : (constr -> constr) -> constr -> constr
 
+(** [map_user_view f c] maps [f] on the immediate subterms of [c]; it
+   differs from [map f c] in that the typing context and body of the
+   return predicate and of the branches of a [match] are considered as
+   immediate subterm of a [match] *)
+
+val map_user_view : (constr -> constr) -> constr -> constr
+
 (** Like {!map}, but also has an additional accumulator. *)
 
 val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 4d13a5fcb8..1d2f22b006 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -932,7 +932,7 @@ let check_one_fix renv recpos trees def =
             let case_spec = branches_specif renv 
 	      (lazy_subterm_specif renv [] c_0) ci in
 	    let stack' = push_stack_closures renv l stack in
-        let stack' = filter_stack_domain renv.env p stack' in
+            let stack' = filter_stack_domain renv.env p stack' in
               Array.iteri (fun k br' -> 
 			     let stack_br = push_stack_args case_spec.(k) stack' in
 			     check_rec_call renv stack_br br') lrest
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ad10c86945..eed25a4ca4 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -632,6 +632,14 @@ let mkMLapp f args =
     | MLapp(f,args') -> MLapp(f,Array.append args' args)
     | _ -> MLapp(f,args)
 
+let mkForceCofix prefix ind arg =
+  let name = fresh_lname Anonymous in
+  MLlet (name, arg,
+    MLif (
+      MLisaccu (prefix, ind, MLlocal name),
+      MLapp (MLprimitive Force_cofix, [|MLlocal name|]),
+      MLlocal name))
+
 let empty_params = [||]
 
 let decompose_MLlam c =
@@ -1143,7 +1151,7 @@ let ml_of_instance instance u =
       let arg = ml_of_lam env l a in
       let force =
 	if annot.asw_finite then arg
-	else MLapp(MLprimitive Force_cofix, [|arg|]) in
+        else mkForceCofix annot.asw_prefix annot.asw_ind arg in
       mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|]
   | Lif(t,bt,bf) -> 
       MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf)
@@ -1999,7 +2007,7 @@ let compile_mind mb mind stack =
       let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
       let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
       let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
-      let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in
+      let code = MLlet(cf_uid, mkForceCofix "" ind (MLlocal c_uid), code) in
       let gn = Gproj ("", ind, proj_arg) in
       Glet (gn, mkMLlam [|c_uid|] code) :: acc
     in
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 3bf23f1468..93e74af845 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -154,10 +154,6 @@ let args_of_accu (k:accumulator) =
   let acc = (get_accu k).acc_arg in
   (Obj.magic (Array.of_list acc) : t array)
 
-let is_accu x =
-  let o = Obj.repr x in
-  Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag
-
 let mk_fix_accu rec_pos pos types bodies =
   mk_accu (Afix(types,bodies,rec_pos, pos))
 
@@ -172,19 +168,17 @@ let upd_cofix (cofix :t) (cofix_fun : t) =
   | _ -> assert false
   
 let force_cofix (cofix : t) = 
-  if is_accu cofix then
-    let accu = (Obj.magic cofix : accumulator) in
-    let atom = atom_of_accu accu in
-    match atom with
-    | Acofix(typ,norm,pos,f) ->
-      let args = args_of_accu accu in
-      let f = Array.fold_right (fun arg f -> f arg) args f in
-      let v = f (Obj.magic ()) in
-      set_atom_of_accu accu (Acofixe(typ,norm,pos,v));
-	v
-    | Acofixe(_,_,_,v) -> v 
-    | _ -> cofix
-  else cofix
+  let accu = (Obj.magic cofix : accumulator) in
+  let atom = atom_of_accu accu in
+  match atom with
+  | Acofix(typ,norm,pos,f) ->
+    let args = args_of_accu accu in
+    let f = Array.fold_right (fun arg f -> f arg) args f in
+    let v = f (Obj.magic ()) in
+    set_atom_of_accu accu (Acofixe(typ,norm,pos,v));
+      v
+  | Acofixe(_,_,_,v) -> v
+  | _ -> cofix
 
 let mk_const tag = Obj.magic tag