From c71aa6bd368b801bb17d4da69d1ab1e2bd7cbf39 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 7 Nov 2015 07:20:34 +0100 Subject: Fixing logical bugs in the presence of let-ins in computiong primitive projections. - lift accounting for the record missing in computing the subst from fields to projections of the record - substitution for parameters should not lift the local definitions - typo in building the latter (subst -> letsubst) --- kernel/indtypes.ml | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 351de9ee88..f08f0b7bbb 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -654,13 +654,12 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params matching with a parameter context. *) let indty, paramsletsubst = let subst, inst = - List.fold_right - (fun (na, b, t) (subst, inst) -> + List.fold_right_i + (fun i (na, b, t) (subst, inst) -> match b with - | None -> (mkRel 1 :: List.map (lift 1) subst, - mkRel 1 :: List.map (lift 1) inst) - | Some b -> (substl subst b) :: subst, List.map (lift 1) inst) - paramslet ([], []) + | None -> (mkRel i :: subst, mkRel i :: inst) + | Some b -> (substl subst b) :: subst, inst) + 1 paramslet ([], []) in let subst = (* For the record parameter: *) mkRel 1 :: List.map (lift 1) subst @@ -690,8 +689,10 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params in let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) = match b with - | Some c -> (i, j+1, kns, pbs, substl subst c :: subst, - substl letsubst c :: subst) + | Some c -> + let c = liftn 1 j c in + (i, j+1, kns, pbs, substl subst c :: subst, + substl letsubst c :: letsubst) | None -> match na with | Name id -> -- cgit v1.2.3 From df04191b48350b76a7650cccc68c9dfc60447787 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 7 Nov 2015 07:33:55 +0100 Subject: Slightly documenting code for building primitive projections. --- kernel/indtypes.ml | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f08f0b7bbb..6c32626ad9 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 -- cgit v1.2.3 From 6ababf42b3f03926c30cfbd209436ec83a21769e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 18 Nov 2015 17:04:12 +0100 Subject: Fixing fix c71aa6b to primitive projections. - Introduced an error: fold was counting in the wrong direction and I did not test it. Sorry. - Substitution from params-with-let to params-without-let was still not correct. Hopefully everything ok now. Eventually, we should use canonical combinators for that: extended_rel_context to built the instance and and a combinator apparently yet to define for building a substitution contracting the let-ins. --- kernel/indtypes.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 6c32626ad9..a46c33bf03 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -653,13 +653,13 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params that typechecking projections requires just a substitution and not matching with a parameter context. *) let indty, paramsletsubst = - let subst, inst = - List.fold_right_i - (fun i (na, b, t) (subst, inst) -> + let _, _, subst, inst = + List.fold_right + (fun (na, b, t) (i, j, subst, inst) -> match b with - | None -> (mkRel i :: subst, mkRel i :: inst) - | Some b -> (substl subst b) :: subst, inst) - 1 paramslet ([], []) + | None -> (i-1, j-1, mkRel i :: subst, mkRel j :: inst) + | Some b -> (i, j-1, substl subst b :: subst, inst)) + paramslet (nparamargs, List.length paramslet, [], []) in let subst = (* For the record parameter: *) mkRel 1 :: List.map (lift 1) subst -- cgit v1.2.3