aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Amin Timany <amintimany@gmail.com>2017-04-08 22:01:30 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-16 04:51:16 +0200
commit4385872b2d82fbad2be84f2423802e00e9d9575f (patch)
treed9ac9255860607bfb39cde77b7989c6463d9d8eb
parent0d884e0852ae388becc5b74c6a8cb30088f7b79b (diff)
Make unification use subtyping info of inductives
-rw-r--r--pretyping/evarconv.ml74
1 files changed, 64 insertions, 10 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3757ba7e6..882ea61a9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -350,6 +350,21 @@ let exact_ise_stack2 env evd f sk1 sk2 =
ise_stack2 evd (List.rev sk1) (List.rev sk2)
else UnifFailure (evd, (* Dummy *) NotSameHead)
+let check_leq_inductives evd uinfind u u' =
+ let u = EConstr.EInstance.kind evd u in
+ let u' = EConstr.EInstance.kind evd u' in
+ let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
+ let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+ if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
+ (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+ anomaly (Pp.str "Invalid inductive subtyping encountered!")
+ else
+ begin
+ let comp_subst = (Univ.Instance.append u u') in
+ let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in
+ Evd.add_constraints evd comp_cst
+ end
+
let rec evar_conv_x ts env evd pbty term1 term2 =
let term1 = whd_head_evar evd term1 in
let term2 = whd_head_evar evd term2 in
@@ -439,16 +454,55 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
else evar_eqappr_x ts env' evd CONV out2 out1
in
let rigids env evd sk term sk' term' =
- let univs = EConstr.eq_constr_universes evd term term' in
- match univs with
- | Some univs ->
- ise_and evd [(fun i ->
- let cstrs = Universes.to_constraints (Evd.universes i) univs in
- try Success (Evd.add_constraints i cstrs)
- with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
- (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
- | None ->
- UnifFailure (evd,NotSameHead)
+ let fall_back () =
+ let univs = EConstr.eq_constr_universes evd term term' in
+ match univs with
+ | Some univs ->
+ begin
+ let cstrs = Universes.to_constraints (Evd.universes evd) univs in
+ try Success (Evd.add_constraints evd cstrs)
+ with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p)
+ end
+ | None ->
+ UnifFailure (evd, NotSameHead)
+ in
+ let compare_heads evd =
+ match EConstr.kind evd term, EConstr.kind evd term' with
+ | Const (c, u), Const (c', u') ->
+ fall_back ()
+ | Ind (ind, u), Ind (ind', u') ->
+ let nparamsaplied = Stack.args_size sk in
+ let nparamsaplied' = Stack.args_size sk' in
+ if Names.eq_ind ind ind' then
+ begin
+ let mind = Environ.lookup_mind (fst ind) env in
+ if mind.Declarations.mind_polymorphic then
+ begin
+ let num_param_arity =
+ Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt)
+ in
+ if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then
+ fall_back ()
+ else
+ begin
+ let uinfind = mind.Declarations.mind_universes in
+ let evd' = check_leq_inductives evd uinfind u u' in
+ Success (check_leq_inductives evd' uinfind u' u)
+ end
+ end
+ else
+ fall_back ()
+ end
+ else UnifFailure (evd, NotSameHead)
+ | Construct (cons, u), Construct (cons', u') ->
+ fall_back ()
+ | _, _ -> anomaly (Pp.str "")
+ in
+ ise_and evd [(fun i ->
+ try compare_heads i
+ with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
+(* >>>>>>> Make unification use subtyping info of inductives *)
in
let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
let switch f a b = if on_left then f a b else f b a in