diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-07 07:33:55 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-18 14:18:13 +0100 |
commit | df04191b48350b76a7650cccc68c9dfc60447787 (patch) | |
tree | d62408598005d93426eaa495c18e8552a94f9885 /kernel/indtypes.ml | |
parent | c71aa6bd368b801bb17d4da69d1ab1e2bd7cbf39 (diff) |
Slightly documenting code for building primitive projections.
Diffstat (limited to 'kernel/indtypes.ml')
-rw-r--r-- | kernel/indtypes.ml | 29 |
1 files changed, 25 insertions, 4 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f08f0b7bb..6c32626ad 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -690,15 +690,36 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) = match b with | Some c -> + (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) let c = liftn 1 j c in - (i, j+1, kns, pbs, substl subst c :: subst, - substl letsubst c :: letsubst) + (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params, x:I |- c(params,proj1 x,..,projj x)] *) + let c1 = substl subst c in + (* From [params, x:I |- subst:field1,..,fieldj] + to [params, x:I |- subst:field1,..,fieldj+1] where [subst] + is represented with instance of field1 last *) + let subst = c1 :: subst in + (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *) + let c2 = substl letsubst c in + (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)] + to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *) + let letsubst = c2 :: letsubst in + (i, j+1, kns, pbs, subst, letsubst) | None -> match na with | Name id -> let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in - let projty = substl letsubst (liftn 1 j t) in - let ty = substl subst (liftn 1 j t) in + (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *) + let t = liftn 1 j t in + (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *) + let projty = substl letsubst t in + (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] + to [params, x:I |- t(proj1 x,..,projj x)] *) + let ty = substl subst t in let term = mkProj (Projection.make kn true, mkRel 1) in let fterm = mkProj (Projection.make kn false, mkRel 1) in let compat = compat_body ty (j - 1) in |