aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml146
-rw-r--r--kernel/cClosure.mli6
-rw-r--r--kernel/constr.ml244
-rw-r--r--kernel/constr.mli70
-rw-r--r--kernel/cooking.ml34
-rw-r--r--kernel/inductive.ml117
-rw-r--r--kernel/inductive.mli17
-rw-r--r--kernel/inferCumulativity.ml9
-rw-r--r--kernel/mod_subst.ml17
-rw-r--r--kernel/nativecode.ml2
-rw-r--r--kernel/nativelambda.ml3
-rw-r--r--kernel/reduction.ml157
-rw-r--r--kernel/relevanceops.ml4
-rw-r--r--kernel/typeops.ml11
-rw-r--r--kernel/typeops.mli6
-rw-r--r--kernel/vars.ml37
-rw-r--r--kernel/vmlambda.ml3
17 files changed, 610 insertions, 273 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index d2256720c4..5613bf645e 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -34,6 +34,8 @@ open Environ
open Vars
open Esubst
+module RelDecl = Context.Rel.Declaration
+
let stats = ref false
(* Profiling *)
@@ -342,8 +344,8 @@ and fterm =
| FProj of Projection.t * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
- | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
- | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs
+ | FCaseT of case_info * Univ.Instance.t * constr array * case_return * fconstr * case_branch array * fconstr subs (* predicate and branches are closures *)
+ | FCaseInvert of case_info * Univ.Instance.t * constr array * case_return * finvert * fconstr * case_branch array * fconstr subs
| FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs
| FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs
| FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
@@ -410,7 +412,7 @@ type 'a next_native_args = (CPrimitives.arg_kind * 'a) list
type stack_member =
| Zapp of fconstr array
- | ZcaseT of case_info * constr * constr array * fconstr subs
+ | ZcaseT of case_info * Univ.Instance.t * constr array * case_return * case_branch array * fconstr subs
| Zproj of Projection.Repr.t
| Zfix of fconstr * stack
| Zprimitive of CPrimitives.t * pconstant * fconstr list * fconstr next_native_args
@@ -578,10 +580,11 @@ let rec to_constr lfts v =
| FFlex (ConstKey op) -> mkConstU op
| FInd op -> mkIndU op
| FConstruct op -> mkConstructU op
- | FCaseT (ci,p,c,ve,env) -> to_constr_case lfts ci p NoInvert c ve env
- | FCaseInvert (ci,p,(univs,args),c,ve,env) ->
+ | FCaseT (ci, u, pms, p, c, ve, env) ->
+ to_constr_case lfts ci u pms p NoInvert c ve env
+ | FCaseInvert (ci, u, pms, p, (univs, args), c, ve, env) ->
let iv = CaseInvert {univs;args=Array.map (to_constr lfts) args} in
- to_constr_case lfts ci p iv c ve env
+ to_constr_case lfts ci u pms p iv c ve env
| FFix ((op,(lna,tys,bds)) as fx, e) ->
if is_subs_id e && is_lift_id lfts then
mkFix fx
@@ -649,14 +652,20 @@ let rec to_constr lfts v =
subst_constr subs t
| FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*)
-and to_constr_case lfts ci p iv c ve env =
+and to_constr_case lfts ci u pms p iv c ve env =
if is_subs_id env && is_lift_id lfts then
- mkCase (ci, p, iv, to_constr lfts c, ve)
+ mkCase (ci, u, pms, p, iv, to_constr lfts c, ve)
else
let subs = comp_subs lfts env in
- mkCase (ci, subst_constr subs p, iv,
- to_constr lfts c,
- Array.map (fun b -> subst_constr subs b) ve)
+ let f_ctx (nas, c) =
+ let c = subst_constr (Esubst.subs_liftn (Array.length nas) subs) c in
+ (nas, c)
+ in
+ mkCase (ci, u, Array.map (fun c -> subst_constr subs c) pms,
+ f_ctx p,
+ iv,
+ to_constr lfts c,
+ Array.map f_ctx ve)
and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with
| Rel i ->
@@ -687,8 +696,8 @@ let rec zip m stk =
match stk with
| [] -> m
| Zapp args :: s -> zip {mark=Mark.neutr m.mark; term=FApp(m, args)} s
- | ZcaseT(ci,p,br,e)::s ->
- let t = FCaseT(ci, p, m, br, e) in
+ | ZcaseT(ci, u, pms, p, br, e)::s ->
+ let t = FCaseT(ci, u, pms, p, m, br, e) in
let mark = mark (neutr (Mark.red_state m.mark)) Unknown in
zip {mark; term=t} s
| Zproj p :: s ->
@@ -763,6 +772,9 @@ let rec subs_consn v i n s =
if Int.equal i n then s
else subs_consn v (i + 1) n (subs_cons v.(i) s)
+let subs_consv v s =
+ subs_consn v 0 (Array.length v) s
+
(* Beta reduction: look for an applied argument in the stack.
Since the encountered update marks are removed, h must be a whnf *)
let rec get_args n tys f e = function
@@ -870,6 +882,74 @@ let drop_parameters depth n argstk =
(* we know that n < stack_args_size(argstk) (if well-typed term) *)
anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor.")
+let inductive_subst (ind, _) mib u pms e =
+ let rec self i accu =
+ if Int.equal i mib.mind_ntypes then accu
+ else
+ let c = inject (mkIndU ((ind, i), u)) in
+ self (i + 1) (subs_cons c accu)
+ in
+ let self = self 0 (subs_id 0) in
+ let rec mk_pms i ctx = match ctx with
+ | [] -> self
+ | RelDecl.LocalAssum _ :: ctx ->
+ let c = mk_clos e pms.(i) in
+ let subs = mk_pms (i - 1) ctx in
+ subs_cons c subs
+ | RelDecl.LocalDef (_, c, _) :: ctx ->
+ let c = Vars.subst_instance_constr u c in
+ let subs = mk_pms i ctx in
+ subs_cons (mk_clos subs c) subs
+ in
+ mk_pms (Array.length pms - 1) mib.mind_params_ctxt
+
+(* Iota-reduction: feed the arguments of the constructor to the branch *)
+let get_branch infos depth ci u pms (ind, c) br e args =
+ let i = c - 1 in
+ let args = drop_parameters depth ci.ci_npar args in
+ let (_nas, br) = br.(i) in
+ if Int.equal ci.ci_cstr_ndecls.(i) ci.ci_cstr_nargs.(i) then
+ (* No let-bindings in the constructor, we don't have to fetch the
+ environment to know the value of the branch. *)
+ let rec push e stk = match stk with
+ | [] -> e
+ | Zapp v :: stk -> push (subs_consv v e) stk
+ | (Zshift _ | ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _) :: _ ->
+ assert false
+ in
+ let e = push e args in
+ (br, e)
+ else
+ (* The constructor contains let-bindings, but they are not physically
+ present in the match, so we fetch them in the environment. *)
+ let env = info_env infos in
+ let mib = Environ.lookup_mind (fst ind) env in
+ let mip = mib.mind_packets.(snd ind) in
+ let (ctx, _) = mip.mind_nf_lc.(i) in
+ let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in
+ let map = function
+ | Zapp args -> args
+ | Zshift _ | ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _ ->
+ assert false
+ in
+ let ind_subst = inductive_subst ind mib u pms e in
+ let args = Array.concat (List.map map args) in
+ let rec push i e = function
+ | [] -> []
+ | RelDecl.LocalAssum _ :: ctx ->
+ let ans = push (pred i) e ctx in
+ args.(i) :: ans
+ | RelDecl.LocalDef (_, b, _) :: ctx ->
+ let ans = push i e ctx in
+ let b = subst_instance_constr u b in
+ let s = Array.rev_of_list ans in
+ let e = subs_consv s ind_subst in
+ let v = mk_clos e b in
+ v :: ans
+ in
+ let ext = push (Array.length args - 1) [] ctx in
+ (br, subs_consv (Array.rev_of_list ext) e)
+
(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
to the conversion of the eta expansion of t, considered as an inhabitant
of ind, and the Constructor c of this inductive type applied to arguments
@@ -909,7 +989,6 @@ let rec project_nth_arg n = function
| (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _ | Zprimitive _) :: _ | [] -> assert false
(* After drop_parameters we have a purely applicative stack *)
-
(* Iota reduction: expansion of a fixpoint.
* Given a fixpoint and a substitution, returns the corresponding
* fixpoint body, and the substitution in which it should be
@@ -1269,7 +1348,7 @@ let rec knh info m stk =
| FCLOS(t,e) -> knht info e t (zupdate info m stk)
| FLOCKED -> assert false
| FApp(a,b) -> knh info a (append_stack b (zupdate info m stk))
- | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk)
+ | FCaseT(ci,u,pms,p,t,br,e) -> knh info t (ZcaseT(ci,u,pms,p,br,e)::zupdate info m stk)
| FFix(((ri,n),_),_) ->
(match get_nth_arg m ri.(n) stk with
(Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
@@ -1289,10 +1368,10 @@ and knht info e t stk =
match kind t with
| App(a,b) ->
knht info e a (append_stack (mk_clos_vect e b) stk)
- | Case(ci,p,NoInvert,t,br) ->
- knht info e t (ZcaseT(ci, p, br, e)::stk)
- | Case(ci,p,CaseInvert{univs;args},t,br) ->
- let term = FCaseInvert (ci, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in
+ | Case(ci,u,pms,p,NoInvert,t,br) ->
+ knht info e t (ZcaseT(ci, u, pms, p, br, e)::stk)
+ | Case(ci,u,pms,p,CaseInvert{univs;args},t,br) ->
+ let term = FCaseInvert (ci, u, pms, p, (univs,Array.map (mk_clos e) args), mk_clos e t, br, e) in
{ mark = mark Red Unknown; term }, stk
| Fix fx -> knh info { mark = mark Cstr Unknown; term = FFix (fx, e) } stk
| Cast(a,_,_) -> knht info e a stk
@@ -1347,15 +1426,15 @@ let rec knr info tab m stk =
| Def v -> kni info tab v stk
| Primitive _ -> assert false
| OpaqueDef _ | Undef _ -> (set_ntrl m; (m,stk)))
- | FConstruct((_ind,c),_u) ->
+ | FConstruct(c,_u) ->
let use_match = red_set info.i_flags fMATCH in
let use_fix = red_set info.i_flags fFIX in
if use_match || use_fix then
(match [@ocaml.warning "-4"] strip_update_shift_app m stk with
- | (depth, args, ZcaseT(ci,_,br,e)::s) when use_match ->
+ | (depth, args, ZcaseT(ci,u,pms,_,br,e)::s) when use_match ->
assert (ci.ci_npar>=0);
- let rargs = drop_parameters depth ci.ci_npar args in
- knit info tab e br.(c-1) (rargs@s)
+ let (br, e) = get_branch info depth ci u pms c br e args in
+ knit info tab e br s
| (_, cargs, Zfix(fx,par)::s) when use_fix ->
let rarg = fapp_stack(m,cargs) in
let stk' = par @ append_stack [|rarg|] s in
@@ -1399,7 +1478,7 @@ let rec knr info tab m stk =
kni info tab a (Zprimitive(op,c,rargs,nargs)::s)
end
| (_, _, s) -> (m, s))
- | FCaseInvert (ci,_p,iv,_c,v,env) when red_set info.i_flags fMATCH ->
+ | FCaseInvert (ci, _u, _pms, _p,iv,_c,v,env) when red_set info.i_flags fMATCH ->
begin match case_inversion info tab ci iv v with
| Some c -> knit info tab env c stk
| None -> (m, stk)
@@ -1419,7 +1498,12 @@ and knit info tab e t stk =
and case_inversion info tab ci (univs,args) v =
let open Declarations in
- if Array.is_empty args then Some v.(0)
+ (* No binders / lets at all in the unique branch *)
+ let v = match v with
+ | [| [||], v |] -> v
+ | _ -> assert false
+ in
+ if Array.is_empty args then Some v
else
let env = info_env info in
let ind = ci.ci_ind in
@@ -1437,7 +1521,7 @@ and case_inversion info tab ci (univs,args) v =
!conv {info with i_flags=all} tab expected index
in
if Array.for_all_i check_index 0 indices
- then Some v.(0) else None
+ then Some v else None
let kh info tab v stk = fapp_stack(kni info tab v stk)
@@ -1448,9 +1532,13 @@ let rec zip_term zfun m stk =
| [] -> m
| Zapp args :: s ->
zip_term zfun (mkApp(m, Array.map zfun args)) s
- | ZcaseT(ci,p,br,e)::s ->
- let t = mkCase(ci, zfun (mk_clos e p), NoInvert, m,
- Array.map (fun b -> zfun (mk_clos e b)) br) in
+ | ZcaseT(ci, u, pms, p, br, e) :: s ->
+ let zip_ctx (nas, c) =
+ let e = Esubst.subs_liftn (Array.length nas) e in
+ (nas, zfun (mk_clos e c))
+ in
+ let t = mkCase(ci, u, Array.map (fun c -> zfun (mk_clos e c)) pms, zip_ctx p,
+ NoInvert, m, Array.map zip_ctx br) in
zip_term zfun t s
| Zproj p::s ->
let t = mkProj (Projection.make p true, m) in
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 3e8916673d..bccbddb0fc 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -110,8 +110,8 @@ type fterm =
| FProj of Projection.t * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
- | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
- | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs
+ | FCaseT of case_info * Univ.Instance.t * constr array * case_return * fconstr * case_branch array * fconstr subs (* predicate and branches are closures *)
+ | FCaseInvert of case_info * Univ.Instance.t * constr array * case_return * finvert * fconstr * case_branch array * fconstr subs
| FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs
| FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs
| FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs
@@ -130,7 +130,7 @@ type 'a next_native_args = (CPrimitives.arg_kind * 'a) list
type stack_member =
| Zapp of fconstr array
- | ZcaseT of case_info * constr * constr array * fconstr subs
+ | ZcaseT of case_info * Univ.Instance.t * constr array * case_return * case_branch array * fconstr subs
| Zproj of Projection.Repr.t
| Zfix of fconstr * stack
| Zprimitive of CPrimitives.t * pconstant * fconstr list * fconstr next_native_args
diff --git a/kernel/constr.ml b/kernel/constr.ml
index bbaf95c9df..0dc72025af 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -83,10 +83,16 @@ type pconstant = Constant.t puniverses
type pinductive = inductive puniverses
type pconstructor = constructor puniverses
-type ('constr, 'univs) case_invert =
+type ('constr, 'univs) pcase_invert =
| NoInvert
| CaseInvert of { univs : 'univs; args : 'constr array }
+type 'constr pcase_branch = Name.t Context.binder_annot array * 'constr
+type 'types pcase_return = Name.t Context.binder_annot array * 'types
+
+type ('constr, 'types, 'univs) pcase =
+ case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
+
(* [Var] is used for named variables and [Rel] for variables as
de Bruijn indices. *)
type ('constr, 'types, 'sort, 'univs) kind_of_term =
@@ -103,7 +109,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Const of (Constant.t * 'univs)
| Ind of (inductive * 'univs)
| Construct of (constructor * 'univs)
- | Case of case_info * 'constr * ('constr, 'univs) case_invert * 'constr * 'constr array
+ | Case of case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
| Proj of Projection.t * 'constr
@@ -119,6 +125,10 @@ type existential = existential_key * constr list
type types = constr
+type case_invert = (constr, Instance.t) pcase_invert
+type case_return = types pcase_return
+type case_branch = constr pcase_branch
+type case = (constr, types, Instance.t) pcase
type rec_declaration = (constr, types) prec_declaration
type fixpoint = (constr, types) pfixpoint
type cofixpoint = (constr, types) pcofixpoint
@@ -194,7 +204,7 @@ let mkConstructU c = Construct c
let mkConstructUi ((ind,u),i) = Construct ((ind,i),u)
(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
-let mkCase (ci, p, iv, c, ac) = Case (ci, p, iv, c, ac)
+let mkCase (ci, u, params, p, iv, c, ac) = Case (ci, u, params, p, iv, c, ac)
(* If recindxs = [|i1,...in|]
funnames = [|f1,...fn|]
@@ -425,7 +435,7 @@ let destConstruct c = match kind c with
(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
let destCase c = match kind c with
- | Case (ci,p,iv,c,v) -> (ci,p,iv,c,v)
+ | Case (ci,u,params,p,iv,c,v) -> (ci,u,params,p,iv,c,v)
| _ -> raise DestKO
let destProj c = match kind c with
@@ -484,7 +494,8 @@ let fold f acc c = match kind c with
| App (c,l) -> Array.fold_left f (f acc c) l
| Proj (_p,c) -> f acc c
| Evar (_,l) -> List.fold_left f acc l
- | Case (_,p,iv,c,bl) -> Array.fold_left f (f (fold_invert f (f acc p) iv) c) bl
+ | Case (_,_,pms,(_,p),iv,c,bl) ->
+ Array.fold_left (fun acc (_, b) -> f acc b) (f (fold_invert f (f (Array.fold_left f acc pms) p) iv) c) bl
| Fix (_,(_lna,tl,bl)) ->
Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
| CoFix (_,(_lna,tl,bl)) ->
@@ -511,7 +522,8 @@ let iter f c = match kind c with
| App (c,l) -> f c; Array.iter f l
| Proj (_p,c) -> f c
| Evar (_,l) -> List.iter f l
- | Case (_,p,iv,c,bl) -> f p; iter_invert f iv; f c; Array.iter f bl
+ | Case (_,_,pms,p,iv,c,bl) ->
+ Array.iter f pms; f (snd p); iter_invert f iv; f c; Array.iter (fun (_, b) -> f b) bl
| Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
| CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
| Array(_u,t,def,ty) -> Array.iter f t; f def; f ty
@@ -531,7 +543,12 @@ let iter_with_binders g f n c = match kind c with
| LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
| App (c,l) -> f n c; Array.Fun1.iter f n l
| Evar (_,l) -> List.iter (fun c -> f n c) l
- | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
+ | Case (_,_,pms,p,iv,c,bl) ->
+ Array.Fun1.iter f n pms;
+ f (iterate g (Array.length (fst p)) n) (snd p);
+ iter_invert (f n) iv;
+ f n c;
+ Array.Fun1.iter (fun n (ctx, b) -> f (iterate g (Array.length ctx) n) b) n bl
| Proj (_p,c) -> f n c
| Fix (_,(_,tl,bl)) ->
Array.Fun1.iter f n tl;
@@ -560,7 +577,11 @@ let fold_constr_with_binders g f n acc c =
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
| Proj (_p,c) -> f n acc c
| Evar (_,l) -> List.fold_left (f n) acc l
- | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+ | Case (_,_,pms,p,iv,c,bl) ->
+ let fold_ctx n accu (nas, c) =
+ f (iterate g (Array.length nas) n) accu c
+ in
+ Array.fold_left (fold_ctx n) (f n (fold_invert (f n) (fold_ctx n (Array.fold_left (f n) acc pms) p) iv) c) bl
| Fix (_,(_,tl,bl)) ->
let n' = iterate g (Array.length tl) n in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
@@ -576,53 +597,30 @@ let fold_constr_with_binders g f n acc c =
not recursive and the order with which subterms are processed is
not specified *)
-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
+let map_under_context f d =
+ let (nas, p) = d in
+ let p' = f p in
+ if p' == p then d else (nas, p')
+
+let map_branches f bl =
+ let bl' = Array.map (map_under_context f) 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
+let map_return_predicate f p =
+ map_under_context f p
+
+let map_under_context_with_binders g f l d =
+ let (nas, p) = d in
+ let l = iterate g (Array.length nas) l in
+ let p' = f l p in
+ if p' == p then d else (nas, p')
+
+let map_branches_with_binders g f l bl =
+ let bl' = Array.map (map_under_context_with_binders g f l) 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 map_return_predicate_with_binders g f l p =
+ map_under_context_with_binders g f l p
let map_invert f = function
| NoInvert -> NoInvert
@@ -631,7 +629,7 @@ let map_invert f = function
if args == args' then orig
else CaseInvert {univs;args=args';}
-let map_gen userview f c = match kind c with
+let map f c = match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _ | Int _ | Float _) -> c
| Cast (b,k,t) ->
@@ -668,20 +666,14 @@ let map_gen userview f c = match kind c with
let l' = List.Smart.map f l in
if l'==l then c
else mkEvar (e, l')
- | Case (ci,p,iv,b,bl) when userview ->
- let b' = f b in
- let iv' = map_invert f iv in
- let p' = map_return_predicate f ci p in
- let bl' = map_branches f ci bl in
- if b'==b && iv'==iv && p'==p && bl'==bl then c
- else mkCase (ci, p', iv', b', bl')
- | Case (ci,p,iv,b,bl) ->
+ | Case (ci,u,pms,p,iv,b,bl) ->
+ let pms' = Array.Smart.map f pms in
let b' = f b in
let iv' = map_invert f iv in
- let p' = f p in
- let bl' = Array.Smart.map f bl in
- if b'==b && iv'==iv && p'==p && bl'==bl then c
- else mkCase (ci, p', iv', b', bl')
+ let p' = map_return_predicate f p in
+ let bl' = map_branches f bl in
+ if b'==b && iv'==iv && p'==p && bl'==bl && pms'==pms then c
+ else mkCase (ci, u, pms', p', iv', b', bl')
| Fix (ln,(lna,tl,bl)) ->
let tl' = Array.Smart.map f tl in
let bl' = Array.Smart.map f bl in
@@ -699,9 +691,6 @@ let map_gen userview f c = match kind c with
if def'==def && t==t' && ty==ty' then c
else mkArray(u,t',def',ty')
-let map_user_view = map_gen true
-let map = map_gen false
-
(* Like {!map} but with an accumulator. *)
let fold_map_invert f acc = function
@@ -711,6 +700,18 @@ let fold_map_invert f acc = function
if args==args' then acc, orig
else acc, CaseInvert {univs;args=args';}
+let fold_map_under_context f accu d =
+ let (nas, p) = d in
+ let accu, p' = f accu p in
+ if p' == p then accu, d else accu, (nas, p')
+
+let fold_map_branches f accu bl =
+ let accu, bl' = Array.Smart.fold_left_map (fold_map_under_context f) accu bl in
+ if Array.for_all2 (==) bl' bl then accu, bl else accu, bl'
+
+let fold_map_return_predicate f accu p =
+ fold_map_under_context f accu p
+
let fold_map f accu c = match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _ | Int _ | Float _) -> accu, c
@@ -749,13 +750,14 @@ let fold_map f accu c = match kind c with
let accu, l' = List.fold_left_map f accu l in
if l'==l then accu, c
else accu, mkEvar (e, l')
- | Case (ci,p,iv,b,bl) ->
- let accu, b' = f accu b in
+ | Case (ci,u,pms,p,iv,b,bl) ->
+ let accu, pms' = Array.Smart.fold_left_map f accu pms in
+ let accu, p' = fold_map_return_predicate f accu p in
let accu, iv' = fold_map_invert f accu iv in
- let accu, p' = f accu p in
- let accu, bl' = Array.Smart.fold_left_map f accu bl in
- if b'==b && iv'==iv && p'==p && bl'==bl then accu, c
- else accu, mkCase (ci, p', iv', b', bl')
+ let accu, b' = f accu b in
+ let accu, bl' = fold_map_branches f accu bl in
+ if pms'==pms && p'==p && iv'==iv && b'==b && bl'==bl then accu, c
+ else accu, mkCase (ci, u, pms', p', iv', b', bl')
| Fix (ln,(lna,tl,bl)) ->
let accu, tl' = Array.Smart.fold_left_map f accu tl in
let accu, bl' = Array.Smart.fold_left_map f accu bl in
@@ -816,13 +818,14 @@ let map_with_binders g f l c0 = match kind c0 with
let al' = List.Smart.map (fun c -> f l c) al in
if al' == al then c0
else mkEvar (e, al')
- | Case (ci, p, iv, c, bl) ->
- let p' = f l p in
+ | Case (ci, u, pms, p, iv, c, bl) ->
+ let pms' = Array.Fun1.Smart.map f l pms in
+ let p' = map_return_predicate_with_binders g f l p in
let iv' = map_invert (f l) iv in
let c' = f l c in
- let bl' = Array.Fun1.Smart.map f l bl in
- if p' == p && iv' == iv && c' == c && bl' == bl then c0
- else mkCase (ci, p', iv', c', bl')
+ let bl' = map_branches_with_binders g f l bl in
+ if pms' == pms && p' == p && iv' == iv && c' == c && bl' == bl then c0
+ else mkCase (ci, u, pms', p', iv', c', bl')
| Fix (ln, (lna, tl, bl)) ->
let tl' = Array.Fun1.Smart.map f l tl in
let l' = iterate g (Array.length tl) l in
@@ -886,6 +889,9 @@ let eq_invert eq leq_universes iv1 iv2 =
leq_universes univs iv2.univs
&& Array.equal eq args iv2.args
+let eq_under_context eq (_nas1, p1) (_nas2, p2) =
+ eq p1 p2
+
let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 =
match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with
| Cast _, _ | _, Cast _ -> assert false (* kind_nocast *)
@@ -911,8 +917,12 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
| Ind (c1,u1), Ind (c2,u2) -> Ind.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2
| Construct (c1,u1), Construct (c2,u2) ->
Construct.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2
- | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) ->
- eq 0 p1 p2 && eq_invert (eq 0) (leq_universes None) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2
+ | Case (ci1,u1,pms1,p1,iv1,c1,bl1), Case (ci2,u2,pms2,p2,iv2,c2,bl2) ->
+ (** FIXME: what are we doing with u1 = u2 ? *)
+ Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind && leq_universes (Some (GlobRef.IndRef ci1.ci_ind, 0)) u1 u2 &&
+ Array.equal (eq 0) pms1 pms2 && eq_under_context (eq 0) p1 p2 &&
+ eq_invert (eq 0) (leq_universes None) iv1 iv2 &&
+ eq 0 c1 c2 && Array.equal (eq_under_context (eq 0)) bl1 bl2
| Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
&& Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2
@@ -1063,6 +1073,9 @@ let constr_ord_int f t1 t2 =
let fix_cmp (a1, i1) (a2, i2) =
((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2
in
+ let ctx_cmp f (_n1, p1) (_n2, p2) =
+ f p1 p2
+ in
match kind t1, kind t2 with
| Cast (c1,_,_), _ -> f c1 t2
| _, Cast (c2,_,_) -> f t1 c2
@@ -1096,12 +1109,13 @@ let constr_ord_int f t1 t2 =
| Ind _, _ -> -1 | _, Ind _ -> 1
| Construct (ct1,_u1), Construct (ct2,_u2) -> Construct.CanOrd.compare ct1 ct2
| Construct _, _ -> -1 | _, Construct _ -> 1
- | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) ->
- let c = f p1 p2 in
+ | Case (_,_u1,pms1,p1,iv1,c1,bl1), Case (_,_u2,pms2,p2,iv2,c2,bl2) ->
+ let c = Array.compare f pms1 pms2 in
+ if Int.equal c 0 then let c = ctx_cmp f p1 p2 in
if Int.equal c 0 then let c = compare_invert f iv1 iv2 in
if Int.equal c 0 then let c = f c1 c2 in
- if Int.equal c 0 then Array.compare f bl1 bl2
- else c else c else c
+ if Int.equal c 0 then Array.compare (ctx_cmp f) bl1 bl2
+ else c else c else c else c
| Case _, _ -> -1 | _, Case _ -> 1
| Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
((fix_cmp =? (Array.compare f)) ==? (Array.compare f))
@@ -1180,6 +1194,9 @@ let invert_eqeq iv1 iv2 =
iv1.univs == iv2.univs
&& iv1.args == iv2.args
+let hasheq_ctx (nas1, c1) (nas2, c2) =
+ array_eqeq nas1 nas2 && c1 == c2
+
let hasheq t1 t2 =
match t1, t2 with
| Rel n1, Rel n2 -> n1 == n2
@@ -1197,8 +1214,11 @@ let hasheq t1 t2 =
| Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2
| Ind (ind1,u1), Ind (ind2,u2) -> ind1 == ind2 && u1 == u2
| Construct (cstr1,u1), Construct (cstr2,u2) -> cstr1 == cstr2 && u1 == u2
- | Case (ci1,p1,iv1,c1,bl1), Case (ci2,p2,iv2,c2,bl2) ->
- ci1 == ci2 && p1 == p2 && invert_eqeq iv1 iv2 && c1 == c2 && array_eqeq bl1 bl2
+ | Case (ci1,u1,pms1,p1,iv1,c1,bl1), Case (ci2,u2,pms2,p2,iv2,c2,bl2) ->
+ (** FIXME: use deeper equality for contexts *)
+ u1 == u2 && array_eqeq pms1 pms2 &&
+ ci1 == ci2 && hasheq_ctx p1 p2 &&
+ invert_eqeq iv1 iv2 && c1 == c2 && Array.equal hasheq_ctx bl1 bl2
| Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) ->
Int.equal i1 i2
&& Array.equal Int.equal ln1 ln2
@@ -1247,7 +1267,7 @@ let sh_instance = Univ.Instance.share
representation for [constr] using [hash_consing_functions] on
leaves. *)
let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
- let rec hash_term t =
+ let rec hash_term (t : t) =
match t with
| Var i ->
(Var (sh_id i), combinesmall 1 (Id.hash i))
@@ -1289,13 +1309,27 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
let u', hu = sh_instance u in
(Construct (sh_construct c, u'),
combinesmall 11 (combine (Construct.SyntacticOrd.hash c) hu))
- | Case (ci,p,iv,c,bl) ->
- let p, hp = sh_rec p
- and iv, hiv = sh_invert iv
- and c, hc = sh_rec c in
- let bl,hbl = hash_term_array bl in
- let hbl = combine4 hc hp hiv hbl in
- (Case (sh_ci ci, p, iv, c, bl), combinesmall 12 hbl)
+ | Case (ci,u,pms,p,iv,c,bl) ->
+ (** FIXME: use a dedicated hashconsing structure *)
+ let hcons_ctx (lna, c) =
+ let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in
+ let fold accu na = combine (hash_annot Name.hash na) accu in
+ let hna = Array.fold_left fold 0 lna in
+ let c, hc = sh_rec c in
+ (lna, c), combine hna hc
+ in
+ let u, hu = sh_instance u in
+ let pms,hpms = hash_term_array pms in
+ let p, hp = hcons_ctx p in
+ let iv, hiv = sh_invert iv in
+ let c, hc = sh_rec c in
+ let fold accu c =
+ let c, h = hcons_ctx c in
+ combine accu h, c
+ in
+ let hbl, bl = Array.fold_left_map fold 0 bl in
+ let hbl = combine (combine hc (combine hiv (combine hpms (combine hu hp)))) hbl in
+ (Case (sh_ci ci, u, pms, p, iv, c, bl), combinesmall 12 hbl)
| Fix (ln,(lna,tl,bl)) ->
let bl,hbl = hash_term_array bl in
let tl,htl = hash_term_array tl in
@@ -1400,8 +1434,8 @@ let rec hash t =
combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u))
| Construct (c,u) ->
combinesmall 11 (combine (Construct.CanOrd.hash c) (Instance.hash u))
- | Case (_ , p, iv, c, bl) ->
- combinesmall 12 (combine4 (hash c) (hash p) (hash_invert iv) (hash_term_array bl))
+ | Case (_ , u, pms, p, iv, c, bl) ->
+ combinesmall 12 (combine (combine (hash c) (combine (hash_invert iv) (combine (hash_term_array pms) (combine (Instance.hash u) (hash_under_context p))))) (hash_branches bl))
| Fix (_ln ,(_, tl, bl)) ->
combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl))
| CoFix(_ln, (_, tl, bl)) ->
@@ -1426,6 +1460,11 @@ and hash_term_array t =
and hash_term_list t =
List.fold_left (fun acc t -> combine (hash t) acc) 0 t
+and hash_under_context (_, t) = hash t
+
+and hash_branches bl =
+ Array.fold_left (fun acc t -> combine acc (hash_under_context t)) 0 bl
+
module CaseinfoHash =
struct
type t = case_info
@@ -1551,10 +1590,15 @@ let rec debug_print c =
| Construct (((sp,i),j),u) ->
str"Constr(" ++ pr_puniverses (MutInd.print sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
| Proj (p,c) -> str"Proj(" ++ Constant.debug_print (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ debug_print c ++ str")"
- | Case (_ci,p,iv,c,bl) -> v 0
- (hv 0 (str"<"++debug_print p++str">"++ cut() ++ str"Case " ++
- debug_print c ++ debug_invert iv ++ str"of") ++ cut() ++
- prlist_with_sep (fun _ -> brk(1,2)) debug_print (Array.to_list bl) ++
+ | Case (_ci,_u,pms,p,iv,c,bl) ->
+ let pr_ctx (nas, c) =
+ prvect_with_sep spc (fun na -> Name.print na.binder_name) nas ++ spc () ++ str "|-" ++ spc () ++
+ debug_print c
+ in
+ v 0 (hv 0 (str"Case " ++
+ debug_print c ++ cut () ++ str "as" ++ cut () ++ prlist_with_sep cut debug_print (Array.to_list pms) ++
+ cut () ++ str"return"++ cut () ++ pr_ctx p ++ debug_invert iv ++ cut () ++ str"with") ++ cut() ++
+ prlist_with_sep (fun _ -> brk(1,2)) pr_ctx (Array.to_list bl) ++
cut() ++ str"end")
| Fix f -> debug_print_fix debug_print f
| CoFix(i,(lna,tl,bl)) ->
diff --git a/kernel/constr.mli b/kernel/constr.mli
index ed63ac507c..17c7da1cf6 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -49,7 +49,7 @@ type case_info =
ci_pp_info : case_printing (* not interpreted by the kernel *)
}
-type ('constr, 'univs) case_invert =
+type ('constr, 'univs) pcase_invert =
| NoInvert
(** Normal reduction: match when the scrutinee is a constructor. *)
@@ -152,14 +152,30 @@ val mkRef : GlobRef.t Univ.puniverses -> constr
(** Constructs a destructor of inductive type.
- [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac]
+ [mkCase ci params p c ac] stand for match [c] as [x] in [I args] return [p] with [ac]
presented as describe in [ci].
- [p] structure is [fun args x -> "return clause"]
+
+ [p] structure is [args x |- "return clause"]
[ac]{^ ith} element is ith constructor case presented as
- {e lambda construct_args (without params). case_term } *)
-val mkCase : case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array -> constr
+ {e construct_args |- case_term } *)
+
+type 'constr pcase_branch = Name.t Context.binder_annot array * 'constr
+(** Names of the indices + name of self *)
+
+type 'types pcase_return = Name.t Context.binder_annot array * 'types
+(** Names of the branches *)
+
+type ('constr, 'types, 'univs) pcase =
+ case_info * 'univs * 'constr array * 'types pcase_return * ('constr, 'univs) pcase_invert * 'constr * 'constr pcase_branch array
+
+type case_invert = (constr, Univ.Instance.t) pcase_invert
+type case_return = types pcase_return
+type case_branch = constr pcase_branch
+type case = (constr, types, Univ.Instance.t) pcase
+
+val mkCase : case -> constr
(** If [recindxs = [|i1,...in|]]
[funnames = [|f1,.....fn|]]
@@ -243,7 +259,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Ind of (inductive * 'univs) (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
| Construct of (constructor * 'univs) (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *)
- | Case of case_info * 'constr * ('constr,'univs) case_invert * 'constr * 'constr array
+ | Case of case_info * 'univs * 'constr array * 'types pcase_return * ('constr,'univs) pcase_invert * 'constr * 'constr pcase_branch array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
| Proj of Projection.t * 'constr
@@ -351,7 +367,7 @@ Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args
return P in t1], or [if c then t1 else t2])
@return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])]
where [info] is pretty-printing information *)
-val destCase : constr -> case_info * constr * (constr,Univ.Instance.t) case_invert * constr * constr array
+val destCase : constr -> case
(** Destructs a projection *)
val destProj : constr -> Projection.t * constr
@@ -421,12 +437,6 @@ val lift : int -> constr -> constr
(** {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
@@ -434,7 +444,7 @@ val map_under_context : (constr -> constr) -> int -> constr -> constr
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
+val map_branches : (constr -> constr) -> case_branch array -> case_branch 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;
@@ -443,16 +453,7 @@ val map_branches : (constr -> constr) -> case_info -> constr array -> constr arr
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
+val map_return_predicate : (constr -> constr) -> case_return -> case_return
(** [map_branches_with_binders f br] maps [f] on the immediate
subterms of an array of "match" branches [br] in canonical
@@ -464,7 +465,7 @@ val map_under_context_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> '
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
+val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_branch array -> case_branch array
(** [map_return_predicate_with_binders f p] maps [f] on the immediate
subterms of a return predicate of a "match" in canonical
@@ -476,7 +477,7 @@ val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a ->
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
+val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_return -> case_return
(** {6 Functionals working on the immediate subterm of a construction } *)
@@ -486,7 +487,7 @@ val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -
val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
-val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a
+val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) pcase_invert -> 'a
(** [map f c] maps [f] on the immediate subterms of [c]; it is
not recursive and the order with which subterms are processed is
@@ -494,21 +495,14 @@ val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a
val map : (constr -> constr) -> constr -> constr
-val map_invert : ('a -> 'a) -> ('a, 'b) case_invert -> ('a, 'b) case_invert
-
-(** [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
+val map_invert : ('a -> 'a) -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert
(** Like {!map}, but also has an additional accumulator. *)
val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
val fold_map_invert : ('a -> 'b -> 'a * 'b) ->
- 'a -> ('b, 'c) case_invert -> 'a * ('b, 'c) case_invert
+ 'a -> ('b, 'c) pcase_invert -> 'a * ('b, 'c) pcase_invert
(** [map_with_binders g f n c] maps [f n] on the immediate
subterms of [c]; it carries an extra data [n] (typically a lift
@@ -525,7 +519,7 @@ val map_with_binders :
val iter : (constr -> unit) -> constr -> unit
-val iter_invert : ('a -> unit) -> ('a, 'b) case_invert -> unit
+val iter_invert : ('a -> unit) -> ('a, 'b) pcase_invert -> unit
(** [iter_with_binders g f n c] iters [f n] on the immediate
subterms of [c]; it carries an extra data [n] (typically a lift
@@ -604,7 +598,7 @@ val compare_head_gen_leq : Univ.Instance.t instance_compare_fn ->
constr constr_compare_fn
val eq_invert : ('a -> 'a -> bool) -> ('b -> 'b -> bool)
- -> ('a, 'b) case_invert -> ('a, 'b) case_invert -> bool
+ -> ('a, 'b) pcase_invert -> ('a, 'b) pcase_invert -> bool
(** {6 Hashconsing} *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 3707a75157..930efa5d36 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -75,30 +75,30 @@ let share_univs cache r u l =
let (u', args) = share cache r l in
mkApp (instantiate_my_gr r (Instance.append u' u), args)
-let update_case cache ci iv modlist =
- match share cache (IndRef ci.ci_ind) modlist with
- | exception Not_found -> ci, iv
- | u, l ->
- let iv = match iv with
- | NoInvert -> NoInvert
- | CaseInvert {univs; args;} ->
- let univs = Instance.append u univs in
- let args = Array.append l args in
- CaseInvert {univs; args;}
- in
- { ci with ci_npar = ci.ci_npar + Array.length l }, iv
-
let is_empty_modlist (cm, mm) =
Cmap.is_empty cm && Mindmap.is_empty mm
let expmod_constr cache modlist c =
let share_univs = share_univs cache in
- let update_case = update_case cache in
let rec substrec c =
match kind c with
- | Case (ci,p,iv,t,br) ->
- let ci,iv = update_case ci iv modlist in
- Constr.map substrec (mkCase (ci,p,iv,t,br))
+ | Case (ci, u, pms, p, iv, t, br) ->
+ begin match share cache (IndRef ci.ci_ind) modlist with
+ | (u', prefix) ->
+ let u = Instance.append u' u in
+ let pms = Array.append prefix pms in
+ let ci = { ci with ci_npar = ci.ci_npar + Array.length prefix } in
+ let iv = match iv with
+ | NoInvert -> NoInvert
+ | CaseInvert {univs; args;} ->
+ let univs = Instance.append u' univs in
+ let args = Array.append prefix args in
+ CaseInvert {univs; args;}
+ in
+ Constr.map substrec (mkCase (ci,u,pms,p,iv,t,br))
+ | exception Not_found ->
+ Constr.map substrec c
+ end
| Ind (ind,u) ->
(try
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ce12d65614..eb18d4b90e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -72,7 +72,7 @@ let constructor_instantiate mind u mib c =
let s = ind_subst mind mib u in
substl s (subst_instance_constr u c)
-let instantiate_params full t u args sign =
+let instantiate_params t u args sign =
let fail () =
anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in
let (rem_args, subs, ty) =
@@ -81,8 +81,7 @@ let instantiate_params full t u args sign =
match (decl, largs, kind ty) with
| (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
| (LocalDef (_,b,_), _, LetIn(_,_,_,t)) ->
- (largs, (substl subs (subst_instance_constr u b))::subs, t)
- | (_,[],_) -> if full then fail() else ([], subs, ty)
+ (largs, (substl subs (subst_instance_constr u b))::subs, t)
| _ -> fail ())
sign
~init:(args,[],t)
@@ -93,11 +92,11 @@ let instantiate_params full t u args sign =
let full_inductive_instantiate mib u params sign =
let dummy = Sorts.prop in
let t = Term.mkArity (Vars.subst_instance_context u sign,dummy) in
- fst (Term.destArity (instantiate_params true t u params mib.mind_params_ctxt))
+ fst (Term.destArity (instantiate_params t u params mib.mind_params_ctxt))
let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
let inst_ind = constructor_instantiate mind u mib t in
- instantiate_params true inst_ind u params mib.mind_params_ctxt
+ instantiate_params inst_ind u params mib.mind_params_ctxt
(************************************************************************)
(************************************************************************)
@@ -372,6 +371,91 @@ let check_correct_arity env c pj ind specif params =
with LocalArity kinds ->
error_elim_arity env ind c pj kinds
+(** {6 Changes of representation of Case nodes} *)
+
+(** Provided:
+ - a universe instance [u]
+ - a term substitution [subst]
+ - name replacements [nas]
+ [instantiate_context u subst nas ctx] applies both [u] and [subst] to [ctx]
+ while replacing names using [nas] (order reversed)
+*)
+let instantiate_context u subst nas ctx =
+ let rec instantiate i ctx = match ctx with
+ | [] -> assert (Int.equal i (-1)); []
+ | LocalAssum (_, ty) :: ctx ->
+ let ctx = instantiate (pred i) ctx in
+ let ty = substnl subst i (subst_instance_constr u ty) in
+ LocalAssum (nas.(i), ty) :: ctx
+ | LocalDef (_, ty, bdy) :: ctx ->
+ let ctx = instantiate (pred i) ctx in
+ let ty = substnl subst i (subst_instance_constr u ty) in
+ let bdy = substnl subst i (subst_instance_constr u bdy) in
+ LocalDef (nas.(i), ty, bdy) :: ctx
+ in
+ instantiate (Array.length nas - 1) ctx
+
+let expand_case_specif mib (ci, u, params, p, iv, c, br) =
+ (* Γ ⊢ c : I@{u} params args *)
+ (* Γ, indices, self : I@{u} params indices ⊢ p : Type *)
+ let mip = mib.mind_packets.(snd ci.ci_ind) in
+ let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in
+ let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list params) in
+ (* Expand the return clause *)
+ let ep =
+ let (nas, p) = p in
+ let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
+ let self =
+ let args = Context.Rel.to_extended_vect mkRel 0 mip.mind_arity_ctxt in
+ let inst = Instance.of_array (Array.init (Instance.length u) Level.var) in
+ mkApp (mkIndU (ci.ci_ind, inst), args)
+ in
+ let realdecls = LocalAssum (Context.anonR, self) :: realdecls in
+ let realdecls = instantiate_context u paramsubst nas realdecls in
+ Term.it_mkLambda_or_LetIn p realdecls
+ in
+ (* Expand the branches *)
+ let subst = paramsubst @ ind_subst (fst ci.ci_ind) mib u in
+ let ebr =
+ let build_one_branch i (nas, br) (ctx, _) =
+ let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in
+ let ctx = instantiate_context u subst nas ctx in
+ Term.it_mkLambda_or_LetIn br ctx
+ in
+ Array.map2_i build_one_branch br mip.mind_nf_lc
+ in
+ (ci, ep, iv, c, ebr)
+
+let expand_case env (ci, _, _, _, _, _, _ as case) =
+ let specif = Environ.lookup_mind (fst ci.ci_ind) env in
+ expand_case_specif specif case
+
+let contract_case env (ci, p, iv, c, br) =
+ let (mib, mip) = lookup_mind_specif env ci.ci_ind in
+ let (arity, p) = Term.decompose_lam_n_decls (mip.mind_nrealdecls + 1) p in
+ let (u, pms) = match arity with
+ | LocalAssum (_, ty) :: _ ->
+ (** Last binder is the self binder for the term being eliminated *)
+ let (ind, args) = decompose_appvect ty in
+ let (ind, u) = destInd ind in
+ let () = assert (Ind.CanOrd.equal ind ci.ci_ind) in
+ let pms = Array.sub args 0 mib.mind_nparams in
+ (** Unlift the parameters from under the index binders *)
+ let dummy = List.make mip.mind_nrealdecls mkProp in
+ let pms = Array.map (fun c -> Vars.substl dummy c) pms in
+ (u, pms)
+ | _ -> assert false
+ in
+ let p =
+ let nas = Array.of_list (List.rev_map get_annot arity) in
+ (nas, p)
+ in
+ let map i br =
+ let (ctx, br) = Term.decompose_lam_n_decls mip.mind_consnrealdecls.(i) br in
+ let nas = Array.of_list (List.rev_map get_annot ctx) in
+ (nas, br)
+ in
+ (ci, u, pms, p, iv, c, Array.mapi map br)
(************************************************************************)
(* Type of case branches *)
@@ -793,7 +877,8 @@ let rec subterm_specif renv stack t =
let f,l = decompose_app (whd_all renv.env t) in
match kind f with
| Rel k -> subterm_var k renv
- | Case (ci,p,_iv,c,lbr) -> (* iv ignored: it's just a cache *)
+ | Case (ci, u, pms, p, iv, c, lbr) -> (* iv ignored: it's just a cache *)
+ let (ci, p, _iv, c, lbr) = expand_case renv.env (ci, u, pms, p, iv, c, lbr) in
let stack' = push_stack_closures renv l stack in
let cases_spec =
branches_specif renv (lazy_subterm_specif renv [] c) ci
@@ -1018,7 +1103,8 @@ let check_one_fix renv recpos trees def =
check_rec_call renv stack (Term.applist(lift p c,l))
end
- | Case (ci,p,iv,c_0,lrest) -> (* iv ignored: it's just a cache *)
+ | Case (ci, u, pms, ret, iv, c_0, br) -> (* iv ignored: it's just a cache *)
+ let (ci, p, _iv, c_0, lrest) = expand_case renv.env (ci, u, pms, ret, iv, c_0, br) in
begin try
List.iter (check_rec_call renv []) (c_0::p::l);
(* compute the recarg info for the arguments of each branch *)
@@ -1040,7 +1126,7 @@ let check_one_fix renv recpos trees def =
(* the call to whd_betaiotazeta will reduce the
apparent iota redex away *)
check_rec_call renv []
- (Term.applist (mkCase (ci,p,iv,c_0,lrest), l))
+ (Term.applist (mkCase (ci, u, pms, ret, iv, c_0, br), l))
| _ -> Exninfo.iraise exn
end
@@ -1324,13 +1410,14 @@ let check_one_cofix env nbfix def deftype =
else
raise (CoFixGuardError (env,UnguardedRecursiveCall c))
- | Case (_,p,_,tm,vrest) -> (* iv ignored: just a cache *)
- begin
- let tree = match restrict_spec env (Subterm (Strict, tree)) p with
- | Dead_code -> assert false
- | Subterm (_, tree') -> tree'
- | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c))
- in
+ | Case (ci, u, pms, p, iv, tm, br) -> (* iv ignored: just a cache *)
+ begin
+ let (_, p, _iv, tm, vrest) = expand_case env (ci, u, pms, p, iv, tm, br) in
+ let tree = match restrict_spec env (Subterm (Strict, tree)) p with
+ | Dead_code -> assert false
+ | Subterm (_, tree') -> tree'
+ | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c))
+ in
if (noccur_with_meta n nbfix p) then
if (noccur_with_meta n nbfix tm) then
if (List.for_all (noccur_with_meta n nbfix) args) then
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 78658dc4de..5808a3fa65 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -79,6 +79,23 @@ val arities_of_specif : MutInd.t puniverses -> mind_specif -> types array
val inductive_params : mind_specif -> int
+(** Given a pattern-matching represented compactly, expands it so as to produce
+ lambda and let abstractions in front of the return clause and the pattern
+ branches. *)
+val expand_case : env -> case -> (case_info * constr * case_invert * constr * constr array)
+
+val expand_case_specif : mutual_inductive_body -> case -> (case_info * constr * case_invert * constr * constr array)
+
+(** Dual operation of the above. Fails if the return clause or branch has not
+ the expected form. *)
+val contract_case : env -> (case_info * constr * case_invert * constr * constr array) -> case
+
+(** [instantiate_context u subst nas ctx] applies both [u] and [subst]
+ to [ctx] while replacing names using [nas] (order reversed). In particular,
+ assumes that [ctx] and [nas] have the same length. *)
+val instantiate_context : Instance.t -> Vars.substl -> Name.t Context.binder_annot array ->
+ rel_context -> rel_context
+
(** [type_case_branches env (I,args) (p:A) c] computes useful types
about the following Cases expression:
<p>Cases (c :: (I args)) of b1..bn end
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index d02f92ef26..50c3ba1cc6 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -198,7 +198,9 @@ let rec infer_fterm cv_pb infos variances hd stk =
let variances = infer_vect infos variances elems in
infer_stack infos variances stk
- | FCaseInvert (_,p,_,_,br,e) ->
+ | FCaseInvert (ci, u, pms, p, _, _, br, e) ->
+ let mib = Environ.lookup_mind (fst ci.ci_ind) (info_env (fst infos)) in
+ let (_, p, _, _, br) = Inductive.expand_case_specif mib (ci, u, pms, p, NoInvert, mkProp, br) in
let infer c variances = infer_fterm CONV infos variances (mk_clos e c) [] in
let variances = infer p variances in
Array.fold_right infer br variances
@@ -217,7 +219,10 @@ and infer_stack infos variances (stk:CClosure.stack) =
| Zfix (fx,a) ->
let variances = infer_fterm CONV infos variances fx [] in
infer_stack infos variances a
- | ZcaseT (_, p, br, e) ->
+ | ZcaseT (ci,u,pms,p,br,e) ->
+ let dummy = mkProp in
+ let case = (ci, u, pms, p, NoInvert, dummy, br) in
+ let (_, p, _, _, br) = Inductive.expand_case (info_env (fst infos)) case in
let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
infer_vect infos variances (Array.map (mk_clos e) br)
| Zshift _ -> variances
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 4778bf1121..c5ac57a2cd 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -355,21 +355,26 @@ let rec map_kn f f' c =
| Construct (((kn,i),j),u) ->
let kn' = f kn in
if kn'==kn then c else mkConstructU (((kn',i),j),u)
- | Case (ci,p,iv,ct,l) ->
+ | Case (ci,u,pms,p,iv,ct,l) ->
let ci_ind =
let (kn,i) = ci.ci_ind in
let kn' = f kn in
if kn'==kn then ci.ci_ind else kn',i
in
- let p' = func p in
+ let f_ctx (nas, c as d) =
+ let c' = func c in
+ if c' == c then d else (nas, c')
+ in
+ let pms' = Array.Smart.map func pms in
+ let p' = f_ctx p in
let iv' = map_invert func iv in
let ct' = func ct in
- let l' = Array.Smart.map func l in
- if (ci.ci_ind==ci_ind && p'==p && iv'==iv
+ let l' = Array.Smart.map f_ctx l in
+ if (ci.ci_ind==ci_ind && pms'==pms && p'==p && iv'==iv
&& l'==l && ct'==ct)then c
else
- mkCase ({ci with ci_ind = ci_ind},
- p',iv',ct', l')
+ mkCase ({ci with ci_ind = ci_ind}, u,
+ pms',p',iv',ct', l')
| Cast (ct,k,t) ->
let ct' = func ct in
let t'= func t in
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 09db29d222..c19b883e3d 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2101,7 +2101,7 @@ let compile_deps env sigma prefix init t =
| Proj (p,c) ->
let init = compile_mind_deps env prefix init (Projection.mind p) in
aux env lvl init c
- | Case (ci, _p, _iv, _c, _ac) ->
+ | Case (ci, _u, _pms, _p, _iv, _c, _ac) ->
let mind = fst ci.ci_ind in
let init = compile_mind_deps env prefix init mind in
fold_constr_with_binders succ (aux env) lvl init t
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index b27c53ef0f..f3b483467d 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -535,7 +535,8 @@ let rec lambda_of_constr cache env sigma c =
let prefix = get_mind_prefix env (fst ind) in
mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|]
- | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *)
+ | Case (ci, u, pms, t, iv, a, br) -> (* XXX handle iv *)
+ let (ci, t, _iv, a, branches) = Inductive.expand_case env (ci, u, pms, t, iv, a, br) in
let (mind,i as ind) = ci.ci_ind in
let mib = lookup_mind mind env in
let oib = mib.mind_packets.(i) in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index cf40263f61..1e39756d47 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -56,7 +56,7 @@ let compare_stack_shape stk1 stk2 =
| (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
| (Zproj _p1::s1, Zproj _p2::s2) ->
Int.equal bal 0 && compare_rec 0 s1 s2
- | (ZcaseT(_c1,_,_,_)::s1, ZcaseT(_c2,_,_,_)::s2) ->
+ | (ZcaseT(_c1,_,_,_,_,_)::s1, ZcaseT(_c2,_,_,_,_,_)::s2) ->
Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
| (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -74,7 +74,7 @@ type lft_constr_stack_elt =
Zlapp of (lift * fconstr) array
| Zlproj of Projection.Repr.t * lift
| Zlfix of (lift * fconstr) * lft_constr_stack
- | Zlcase of case_info * lift * constr * constr array * fconstr subs
+ | Zlcase of case_info * lift * Univ.Instance.t * constr array * case_return * case_branch array * fconstr subs
| Zlprimitive of
CPrimitives.t * pconstant * lft_fconstr list * lft_fconstr next_native_args
and lft_constr_stack = lft_constr_stack_elt list
@@ -109,8 +109,8 @@ let pure_stack lfts stk =
| (Zfix(fx,a),(l,pstk)) ->
let (lfx,pa) = pure_rec l a in
(l, Zlfix((lfx,fx),pa)::pstk)
- | (ZcaseT(ci,p,br,e),(l,pstk)) ->
- (l,Zlcase(ci,l,p,br,e)::pstk)
+ | (ZcaseT(ci,u,pms,p,br,e),(l,pstk)) ->
+ (l,Zlcase(ci,l,u,pms,p,br,e)::pstk)
| (Zprimitive(op,c,rargs,kargs),(l,pstk)) ->
(l,Zlprimitive(op,c,List.map (fun t -> (l,t)) rargs,
List.map (fun (k,t) -> (k,(l,t))) kargs)::pstk))
@@ -233,6 +233,9 @@ let convert_instances ~flex u u' (s, check) =
exception MustExpand
+let convert_instances_cumul pb var u u' (s, check) =
+ (check.compare_cumul_instances pb var u u' s, check)
+
let get_cumulativity_constraints cv_pb variance u u' =
match cv_pb with
| CONV ->
@@ -294,8 +297,6 @@ let conv_table_key infos ~nargs k1 k2 cuniv =
| RelKey n, RelKey n' when Int.equal n n' -> cuniv
| _ -> raise NotConvertible
-exception IrregularPatternShape
-
let unfold_ref_with_args infos tab fl v =
match unfold_reference infos tab fl with
| Def def -> Some (def, v)
@@ -327,17 +328,6 @@ let push_relevance infos r =
let push_relevances infos nas =
{ infos with cnv_inf = CClosure.push_relevances infos.cnv_inf nas }
-let rec skip_pattern infos relevances n c1 c2 =
- if Int.equal n 0 then {infos with cnv_inf = CClosure.set_info_relevances infos.cnv_inf relevances}, c1, c2
- else match kind c1, kind c2 with
- | Lambda (x, _, c1), Lambda (_, _, c2) ->
- skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2
- | _ -> raise IrregularPatternShape
-
-let skip_pattern infos n c1 c2 =
- if Int.equal n 0 then infos, c1, c2
- else skip_pattern infos (info_relevances infos.cnv_inf) n c1 c2
-
let is_irrelevant infos lft c =
let env = info_env infos.cnv_inf in
try Relevanceops.relevance_of_fterm env (info_relevances infos.cnv_inf) lft c == Sorts.Irrelevant with _ -> false
@@ -364,6 +354,39 @@ let eta_expand_constructor env ((ind,ctor),u as pctor) =
let c = Term.it_mkLambda_or_LetIn c ctx in
inject c
+let inductive_subst (mind, _) mib u pms =
+ let open Context.Rel.Declaration in
+ let ntypes = mib.mind_ntypes in
+ let rec self i accu =
+ if Int.equal i ntypes then accu
+ else self (i + 1) (subs_cons (inject (mkIndU ((mind, i), u))) accu)
+ in
+ let accu = self 0 (subs_id 0) in
+ let rec mk_pms pms ctx = match ctx, pms with
+ | [], [] -> accu
+ | LocalAssum _ :: ctx, c :: pms ->
+ let subs = mk_pms pms ctx in
+ subs_cons c subs
+ | LocalDef (_, c, _) :: ctx, pms ->
+ let c = Vars.subst_instance_constr u c in
+ let subs = mk_pms pms ctx in
+ subs_cons (mk_clos subs c) subs
+ | LocalAssum _ :: _, [] | [], _ :: _ -> assert false
+ in
+ mk_pms (List.rev pms) mib.mind_params_ctxt
+
+let esubst_of_rel_context_instance ctx u args e =
+ let open Context.Rel.Declaration in
+ let rec aux lft e args ctx = match ctx with
+ | [] -> lft, e
+ | LocalAssum _ :: ctx -> aux (lft + 1) (subs_lift e) (subs_lift args) ctx
+ | LocalDef (_, c, _) :: ctx ->
+ let c = Vars.subst_instance_constr u c in
+ let c = mk_clos args c in
+ aux lft (subs_cons c e) (subs_cons c args) ctx
+ in
+ aux 0 e args (List.rev ctx)
+
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
@@ -672,13 +695,23 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
if Float64.equal f1 f2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
- | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) ->
+ | FCaseInvert (ci1,u1,pms1,p1,_,_,br1,e1), FCaseInvert (ci2,u2,pms2,p2,_,_,br2,e2) ->
(if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible);
let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in
- let ccnv = ccnv CONV l2r infos el1 el2 in
- let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in
- Array.fold_right2 (fun b1 b2 cuniv -> ccnv (mk_clos e1 b1) (mk_clos e2 b2) cuniv)
- br1 br2 cuniv
+ let fold c1 c2 cuniv = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
+ (** FIXME: cache the presence of let-bindings in the case_info *)
+ let mind = Environ.lookup_mind (fst ci1.ci_ind) (info_env infos.cnv_inf) in
+ let mip = mind.Declarations.mind_packets.(snd ci1.ci_ind) in
+ let cuniv =
+ let ind = (mind,snd ci1.ci_ind) in
+ let nargs = inductive_cumulativity_arguments ind in
+ convert_inductives CONV ind nargs u1 u2 cuniv
+ in
+ let pms1 = Array.map_to_list (fun c -> mk_clos e1 c) pms1 in
+ let pms2 = Array.map_to_list (fun c -> mk_clos e2 c) pms2 in
+ let cuniv = List.fold_right2 fold pms1 pms2 cuniv in
+ let cuniv = convert_return_clause ci1.ci_ind mind mip l2r infos e1 e2 el1 el2 u1 u2 pms1 pms2 p1 p2 cuniv in
+ convert_branches ci1.ci_ind mind mip l2r infos e1 e2 el1 el2 u1 u2 pms1 pms2 br1 br2 cuniv
| FArray (u1,t1,ty1), FArray (u2,t2,ty2) ->
let len = Parray.length_int t1 in
@@ -714,11 +747,27 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
| (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
let cu2 = f fx1 fx2 cu1 in
cmp_rec a1 a2 cu2
- | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) ->
+ | (Zlcase(ci1,l1,u1,pms1,p1,br1,e1),Zlcase(ci2,l2,u2,pms2,p2,br2,e2)) ->
if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then
raise NotConvertible;
- let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in
- convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2
+ let cu = cu1 in
+ (** FIXME: cache the presence of let-bindings in the case_info *)
+ let mind = Environ.lookup_mind (fst ci1.ci_ind) (info_env infos.cnv_inf) in
+ let mip = mind.Declarations.mind_packets.(snd ci1.ci_ind) in
+ let cu =
+ if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+ convert_instances ~flex:false u1 u2 cu
+ else
+ match mind.Declarations.mind_variance with
+ | None -> convert_instances ~flex:false u1 u2 cu
+ | Some variances -> convert_instances_cumul CONV variances u1 u2 cu
+ in
+ let pms1 = Array.map_to_list (fun c -> mk_clos e1 c) pms1 in
+ let pms2 = Array.map_to_list (fun c -> mk_clos e2 c) pms2 in
+ let fold_params c1 c2 accu = f (l1, c1) (l2, c2) accu in
+ let cu = List.fold_right2 fold_params pms1 pms2 cu in
+ let cu = convert_return_clause ci1.ci_ind mind mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 p1 p2 cu in
+ convert_branches ci1.ci_ind mind mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 br1 br2 cu
| (Zlprimitive(op1,_,rargs1,kargs1),Zlprimitive(op2,_,rargs2,kargs2)) ->
if not (CPrimitives.equal op1 op2) then raise NotConvertible else
let cu2 = List.fold_right2 f rargs1 rargs2 cu1 in
@@ -743,21 +792,55 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
fold 0 cuniv
else raise NotConvertible
-and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv =
- (** Skip comparison of the pattern types. We know that the two terms are
- living in a common type, thus this check is useless. *)
- let fold n c1 c2 cuniv = match skip_pattern infos n c1 c2 with
- | (infos, c1, c2) ->
- let lft1 = el_liftn n lft1 in
- let lft2 = el_liftn n lft2 in
+and convert_under_context l2r infos e1 e2 lft1 lft2 ctx (nas1, c1) (nas2, c2) cu =
+ let n = Array.length nas1 in
+ let () = assert (Int.equal n (Array.length nas2)) in
+ let n, e1, e2 = match ctx with
+ | None -> (* nolet *)
let e1 = subs_liftn n e1 in
let e2 = subs_liftn n e2 in
- ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
- | exception IrregularPatternShape ->
- (** Might happen due to a shape invariant that is not enforced *)
- ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
+ (n, e1, e2)
+ | Some (ctx, u1, u2, args1, args2) ->
+ let n1, e1 = esubst_of_rel_context_instance ctx u1 args1 e1 in
+ let n2, e2 = esubst_of_rel_context_instance ctx u2 args2 e2 in
+ let () = assert (Int.equal n1 n2) in
+ n1, e1, e2
+ in
+ let lft1 = el_liftn n lft1 in
+ let lft2 = el_liftn n lft2 in
+ let infos = push_relevances infos nas1 in
+ ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cu
+
+and convert_return_clause ind mib mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 p1 p2 cu =
+ let ctx =
+ if Int.equal mip.mind_nrealargs mip.mind_nrealdecls then None
+ else
+ let ctx, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
+ let pms1 = inductive_subst ind mib u1 pms1 in
+ let pms2 = inductive_subst ind mib u1 pms2 in
+ let open Context.Rel.Declaration in
+ (* Add the inductive binder *)
+ let dummy = mkProp in
+ let ctx = LocalAssum (Context.anonR, dummy) :: ctx in
+ Some (ctx, u1, u2, pms1, pms2)
+ in
+ convert_under_context l2r infos e1 e2 l1 l2 ctx p1 p2 cu
+
+and convert_branches ind mib mip l2r infos e1 e2 lft1 lft2 u1 u2 pms1 pms2 br1 br2 cuniv =
+ let fold i (ctx, _) cuniv =
+ let ctx =
+ if Int.equal mip.mind_consnrealdecls.(i) mip.mind_consnrealargs.(i) then None
+ else
+ let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in
+ let pms1 = inductive_subst ind mib u1 pms1 in
+ let pms2 = inductive_subst ind mib u2 pms2 in
+ Some (ctx, u1, u2, pms1, pms2)
+ in
+ let c1 = br1.(i) in
+ let c2 = br2.(i) in
+ convert_under_context l2r infos e1 e2 lft1 lft2 ctx c1 c2 cuniv
in
- Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv
+ Array.fold_right_i fold mip.mind_nf_lc cuniv
and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
| [], [] -> cuniv
diff --git a/kernel/relevanceops.ml b/kernel/relevanceops.ml
index f12b8cba37..986fc685d1 100644
--- a/kernel/relevanceops.ml
+++ b/kernel/relevanceops.ml
@@ -61,7 +61,7 @@ let rec relevance_of_fterm env extra lft f =
| FProj (p, _) -> relevance_of_projection env p
| FFix (((_,i),(lna,_,_)), _) -> (lna.(i)).binder_relevance
| FCoFix ((i,(lna,_,_)), _) -> (lna.(i)).binder_relevance
- | FCaseT (ci, _, _, _, _) | FCaseInvert (ci, _, _, _, _, _) -> ci.ci_relevance
+ | FCaseT (ci, _, _, _, _, _, _) | FCaseInvert (ci, _, _, _, _, _, _, _) -> ci.ci_relevance
| FLambda (len, tys, bdy, e) ->
let extra = List.fold_left (fun accu (x, _) -> Range.cons (binder_relevance x) accu) extra tys in
let lft = Esubst.el_liftn len lft in
@@ -97,7 +97,7 @@ and relevance_of_term_extra env extra lft subs c =
| App (c, _) -> relevance_of_term_extra env extra lft subs c
| Const (c,_) -> relevance_of_constant env c
| Construct (c,_) -> relevance_of_constructor env c
- | Case (ci, _, _, _, _) -> ci.ci_relevance
+ | Case (ci, _, _, _, _, _, _) -> ci.ci_relevance
| Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
| CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
| Proj (p, _) -> relevance_of_projection env p
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 802a32b0e7..83e41a63ec 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -548,7 +548,9 @@ let rec execute env cstr =
| Construct c ->
cstr, type_of_constructor env c
- | Case (ci,p,iv,c,lf) ->
+ | Case (ci, u, pms, p, iv, c, lf) ->
+ (** FIXME: change type_of_case to handle the compact form *)
+ let (ci, p, iv, c, lf) = expand_case env (ci, u, pms, p, iv, c, lf) in
let c', ct = execute env c in
let iv' = match iv with
| NoInvert -> NoInvert
@@ -563,7 +565,7 @@ let rec execute env cstr =
let lf', lft = execute_array env lf in
let ci', t = type_of_case env ci p' pt iv' c' ct lf' lft in
let cstr = if ci == ci' && c == c' && p == p' && iv == iv' && lf == lf' then cstr
- else mkCase(ci',p',iv',c',lf')
+ else mkCase (Inductive.contract_case env (ci',p',iv',c',lf'))
in
cstr, t
@@ -720,11 +722,6 @@ let judge_of_inductive env indu =
let judge_of_constructor env cu =
make_judge (mkConstructU cu) (type_of_constructor env cu)
-let judge_of_case env ci pj iv cj lfj =
- let lf, lft = dest_judgev lfj in
- let ci, t = type_of_case env ci pj.uj_val pj.uj_type iv cj.uj_val cj.uj_type lf lft in
- make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, iv, cj.uj_val, lft)) t
-
(* Building type of primitive operators and type *)
let type_of_prim_const env _u c =
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index d381e55dd6..5ea7163f72 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -92,12 +92,6 @@ val judge_of_cast :
val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment
val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment
-(** {6 Type of Cases. } *)
-val judge_of_case : env -> case_info
- -> unsafe_judgment -> (constr,Instance.t) case_invert -> unsafe_judgment
- -> unsafe_judgment array
- -> unsafe_judgment
-
(** {6 Type of global references. } *)
val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
diff --git a/kernel/vars.ml b/kernel/vars.ml
index a446fa413c..0f71057787 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -253,12 +253,21 @@ let subst_univs_level_constr subst c =
if u' == u then t else
(changed := true; mkSort (Sorts.sort_of_univ u'))
- | Case (ci,p,CaseInvert {univs;args},c,br) ->
- if Univ.Instance.is_empty univs then Constr.map aux t
+ | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
+ if Univ.Instance.is_empty u && Univ.Instance.is_empty univs then Constr.map aux t
else
+ let u' = f u in
let univs' = f univs in
- if univs' == univs then Constr.map aux t
- else (changed:=true; Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br)))
+ if u' == u && univs' == univs then Constr.map aux t
+ else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br)))
+
+ | Case (ci, u, pms, p, NoInvert, c, br) ->
+ if Univ.Instance.is_empty u then Constr.map aux t
+ else
+ let u' = f u in
+ if u' == u then Constr.map aux t
+ else
+ (changed := true; Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br)))
| Array (u,elems,def,ty) ->
let u' = f u in
@@ -305,10 +314,19 @@ let subst_instance_constr subst c =
if u' == u then t else
(mkSort (Sorts.sort_of_univ u'))
- | Case (ci,p,CaseInvert {univs;args},c,br) ->
+ | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
+ let u' = f u in
let univs' = f univs in
- if univs' == univs then Constr.map aux t
- else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br))
+ if u' == u && univs' == univs then Constr.map aux t
+ else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br))
+
+ | Case (ci, u, pms, p, NoInvert, c, br) ->
+ if Univ.Instance.is_empty u then Constr.map aux t
+ else
+ let u' = f u in
+ if u' == u then Constr.map aux t
+ else
+ Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br))
| Array (u,elems,def,ty) ->
let u' = f u in
@@ -348,8 +366,11 @@ let universes_of_constr c =
| Array (u,_,_,_) ->
let s = LSet.fold LSet.add (Instance.levels u) s in
Constr.fold aux s c
- | Case (_,_,CaseInvert {univs;args=_},_,_) ->
+ | Case (_, u, _, _, CaseInvert {univs;args=_},_ ,_) ->
+ let s = LSet.fold LSet.add (Instance.levels u) s in
let s = LSet.fold LSet.add (Instance.levels univs) s in
Constr.fold aux s c
+ | Case (_, u, _, _, NoInvert, _, _) ->
+ Constr.fold aux (LSet.fold LSet.add (Instance.levels u) s) c
| _ -> Constr.fold aux s c
in aux LSet.empty c
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index 390fa58883..91de58b0e6 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -674,7 +674,8 @@ let rec lambda_of_constr env c =
| Construct _ -> lambda_of_app env c empty_args
- | Case(ci,t,_iv,a,branches) -> (* XXX handle iv *)
+ | Case (ci, u, pms, t, iv, a, br) -> (* XXX handle iv *)
+ let (ci, t, _iv, a, branches) = Inductive.expand_case env.global_env (ci, u, pms, t, iv, a, br) in
let ind = ci.ci_ind in
let mib = lookup_mind (fst ind) env.global_env in
let oib = mib.mind_packets.(snd ind) in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:21:57 +0000