diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 7 | ||||
| -rw-r--r-- | kernel/environ.mli | 5 | ||||
| -rw-r--r-- | kernel/reduction.ml | 51 |
3 files changed, 53 insertions, 10 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index e75ccbb252..03c9cb4be6 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -87,6 +87,7 @@ let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) type named_context_val = { env_named_ctx : Constr.named_context; env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t; + env_named_var : Constr.t list; } type rel_context_val = { @@ -109,6 +110,7 @@ type env = { let empty_named_context_val = { env_named_ctx = []; env_named_map = Id.Map.empty; + env_named_var = []; } let empty_rel_context_val = { @@ -183,6 +185,7 @@ let push_named_context_val_val d rval ctxt = { env_named_ctx = Context.Named.add d ctxt.env_named_ctx; env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; + env_named_var = mkVar (NamedDecl.get_id d) :: ctxt.env_named_var; } let push_named_context_val d ctxt = @@ -193,7 +196,7 @@ let match_named_context_val c = match c.env_named_ctx with | decl :: ctx -> let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in - let cval = { env_named_ctx = ctx; env_named_map = map } in + let cval = { env_named_ctx = ctx; env_named_map = map; env_named_var = List.tl c.env_named_var } in Some (decl, v, cval) let map_named_val f ctxt = @@ -208,7 +211,7 @@ let map_named_val f ctxt = in let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in if map == ctxt.env_named_map then ctxt - else { env_named_ctx = ctx; env_named_map = map } + else { env_named_ctx = ctx; env_named_map = map; env_named_var = ctxt.env_named_var } let push_named d env = {env with env_named_context = push_named_context_val d env.env_named_context} diff --git a/kernel/environ.mli b/kernel/environ.mli index 5cb56a2a29..974e794c6b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -69,6 +69,11 @@ type stratification = { type named_context_val = private { env_named_ctx : Constr.named_context; env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t; + (** Identifier-indexed version of [env_named_ctx] *) + env_named_var : Constr.t list; + (** List of identifiers in [env_named_ctx], in the same order, including + let-ins. This is not used in the kernel, but is critical to preserve + sharing of evar instances in the proof engine. *) } type rel_context_val = private { diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 0754e9d4cc..7c6b869b4a 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -234,6 +234,8 @@ let sort_cmp_universes env pb s0 s1 (u, check) = let convert_instances ~flex u u' (s, check) = (check.compare_instances ~flex u u' s, check) +exception MustExpand + let get_cumulativity_constraints cv_pb variance u u' = match cv_pb with | CONV -> @@ -251,7 +253,8 @@ let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 | Some variances -> let num_param_arity = inductive_cumulativity_arguments (mind,ind) in if not (Int.equal num_param_arity nargs) then - cmp_instances u1 u2 s + (* shortcut, not sure if worth doing, could use perf data *) + if Univ.Instance.equal u1 u2 then s else raise MustExpand else cmp_cumul cv_pb variances u1 u2 s @@ -269,7 +272,7 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u | Some _ -> let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in if not (Int.equal num_cnstr_args nargs) then - cmp_instances u1 u2 s + if Univ.Instance.equal u1 u2 then s else raise MustExpand else (** By invariant, both constructors have a common supertype, so they are convertible _at that type_. *) @@ -336,6 +339,28 @@ 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 +let identity_of_ctx (ctx:Constr.rel_context) = + Context.Rel.to_extended_vect mkRel 0 ctx + +(* ind -> fun args => ind args *) +let eta_expand_ind env (ind,u as pind) = + let mib = Environ.lookup_mind (fst ind) env in + let mip = mib.mind_packets.(snd ind) in + let ctx = Vars.subst_instance_context u mip.mind_arity_ctxt in + let args = identity_of_ctx ctx in + let c = mkApp (mkIndU pind, args) in + let c = Term.it_mkLambda_or_LetIn c ctx in + inject c + +let eta_expand_constructor env ((ind,ctor),u as pctor) = + let mib = Environ.lookup_mind (fst ind) env in + let mip = mib.mind_packets.(snd ind) in + let ctx = Vars.subst_instance_context u (fst mip.mind_nf_lc.(ctor-1)) in + let args = identity_of_ctx ctx in + let c = mkApp (mkConstructU pctor, args) in + let c = Term.it_mkLambda_or_LetIn c ctx in + inject c + (* 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 @@ -545,7 +570,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = end (* Inductive types: MutInd MutConstruct Fix Cofix *) - | (FInd (ind1,u1), FInd (ind2,u2)) -> + | (FInd (ind1,u1 as pind1), FInd (ind2,u2 as pind2)) -> if eq_ind ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in @@ -556,11 +581,16 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if not (Int.equal nargs (CClosure.stack_args_size v2)) then raise NotConvertible else - let cuniv = convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with + | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + | exception MustExpand -> + let env = info_env infos.cnv_inf in + let hd1 = eta_expand_ind env pind1 in + let hd2 = eta_expand_ind env pind2 in + eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv else raise NotConvertible - | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> + | (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) -> if Int.equal j1 j2 && eq_ind ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in @@ -571,8 +601,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if not (Int.equal nargs (CClosure.stack_args_size v2)) then raise NotConvertible else - let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with + | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + | exception MustExpand -> + let env = info_env infos.cnv_inf in + let hd1 = eta_expand_constructor env pctor1 in + let hd2 = eta_expand_constructor env pctor2 in + eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv else raise NotConvertible (* Eta expansion of records *) |