aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r--pretyping/evarconv.ml242
1 files changed, 166 insertions, 76 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a0542cbb2..594481af3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -27,41 +27,52 @@ let debug_unification = ref (false)
let _ = Goptions.declare_bool_option {
Goptions.optsync = true; Goptions.optdepr = false;
Goptions.optname =
- "Print states sended to Evarconv unification";
+ "Print states sent to Evarconv unification";
Goptions.optkey = ["Debug";"Unification"];
Goptions.optread = (fun () -> !debug_unification);
Goptions.optwrite = (fun a -> debug_unification:=a);
}
-let eval_flexible_term ts env c =
+let unfold_projection env p c stk =
+ (match try Some (lookup_projection p env) with Not_found -> None with
+ | Some pb ->
+ let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) in
+ Some (c, s :: stk)
+ | None -> None)
+
+let eval_flexible_term ts env c stk =
match kind_of_term c with
- | Const c ->
+ | Const (c,u as cu) ->
if is_transparent_constant ts c
- then constant_opt_value env c
+ then Option.map (fun x -> x, stk) (constant_opt_value_in env cu)
else None
| Rel n ->
- (try let (_,v,_) = lookup_rel n env in Option.map (lift n) v
+ (try let (_,v,_) = lookup_rel n env in Option.map (fun t -> lift n t, stk) v
with Not_found -> None)
| Var id ->
(try
if is_transparent_variable ts id then
- let (_,v,_) = lookup_named id env in v
+ let (_,v,_) = lookup_named id env in Option.map (fun t -> t, stk) v
else None
with Not_found -> None)
- | LetIn (_,b,_,c) -> Some (subst1 b c)
- | Lambda _ -> Some c
+ | LetIn (_,b,_,c) -> Some (subst1 b c, stk)
+ | Lambda _ -> Some (c, stk)
+ | Proj (p, c) ->
+ if is_transparent_constant ts p
+ then unfold_projection env p c stk
+ else None
| _ -> assert false
type flex_kind_of_term =
| Rigid
- | MaybeFlexible of Constr.t (* reducible but not necessarily reduced *)
+ | MaybeFlexible of Constr.t * Constr.t Stack.t (* reducible but not necessarily reduced *)
| Flexible of existential
let flex_kind_of_term ts env c sk =
match kind_of_term c with
- | LetIn _ | Rel _ | Const _ | Var _ ->
- Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env c)
- | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c
+ | LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
+ Option.cata (fun (x,y) -> MaybeFlexible (x,y)) Rigid (eval_flexible_term ts env c sk)
+ | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible (c, sk)
| Evar ev -> Flexible ev
| Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ -> Rigid
| Meta _ -> Rigid
@@ -100,36 +111,43 @@ let position_problem l2r = function
projection would have been reduced) *)
let check_conv_record (t1,sk1) (t2,sk2) =
- let proji = global_of_constr t1 in
- let canon_s,sk2_effective =
- try
- match kind_of_term t2 with
- Prod (_,a,b) -> (* assert (l2=[]); *)
+ let (proji, u), arg = Universes.global_app_of_constr t1 in
+ let canon_s,sk2_effective =
+ try
+ match kind_of_term t2 with
+ Prod (_,a,b) -> (* assert (l2=[]); *)
if dependent (mkRel 1) b then raise Not_found
else lookup_canonical_conversion (proji, Prod_cs),(Stack.append_app [|a;pop b|] Stack.empty)
- | Sort s ->
- lookup_canonical_conversion
- (proji, Sort_cs (family_of_sort s)),[]
- | _ ->
- let c2 = global_of_constr t2 in
- lookup_canonical_conversion (proji, Const_cs c2),sk2
- with Not_found ->
- lookup_canonical_conversion (proji,Default_cs),[]
- in
- let { o_DEF = c; o_INJ=n; o_TABS = bs;
- o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
- let params1, c1, extra_args1 =
+ | Sort s ->
+ lookup_canonical_conversion
+ (proji, Sort_cs (family_of_sort s)),[]
+ | _ ->
+ let c2 = global_of_constr t2 in
+ lookup_canonical_conversion (proji, Const_cs c2),sk2
+ with Not_found ->
+ lookup_canonical_conversion (proji,Default_cs),[]
+ in
+ let { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
+ o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
+ let params1, c1, extra_args1 =
+ match arg with
+ | Some c -> (* A primitive projection applied to c *)
+ [], c, sk1
+ | None ->
match Stack.strip_n_app nparams sk1 with
| Some (params1, c1,extra_args1) -> params1, c1, extra_args1
| _ -> raise Not_found in
- let us2,extra_args2 =
- let l_us = List.length us in
+ let us2,extra_args2 =
+ let l_us = List.length us in
if Int.equal l_us 0 then Stack.empty,sk2_effective
else match (Stack.strip_n_app (l_us-1) sk2_effective) with
- | None -> raise Not_found
- | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
- (c,bs,(Stack.append_app_list params Stack.empty,params1),(Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
- (n,Stack.zip(t2,sk2)))
+ | None -> raise Not_found
+ | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
+ let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
+ let c' = subst_univs_level_constr subst c in
+ let bs' = List.map (subst_univs_level_constr subst) bs in
+ ctx',c',bs',(Stack.append_app_list params Stack.empty,params1),(Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
+ (n,Stack.zip(t2,sk2))
(* Precondition: one of the terms of the pb is an uninstantiated evar,
* possibly applied to arguments. *)
@@ -206,6 +224,9 @@ let ise_stack2 no_app env evd f sk1 sk2 =
| Success i'' -> ise_stack2 true i'' q1 q2
| UnifFailure _ as x -> fail x)
| UnifFailure _ as x -> fail x)
+ | Stack.Proj (n1,a1,p1)::q1, Stack.Proj (n2,a2,p2)::q2 ->
+ if eq_constant p1 p2 then ise_stack2 true i q1 q2
+ else fail (UnifFailure (i, NotSameHead))
| Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
@@ -259,6 +280,13 @@ let exact_ise_stack2 env evd f sk1 sk2 =
ise_stack2 evd (List.rev sk1) (List.rev sk2)
else UnifFailure (evd, (* Dummy *) NotSameHead)
+let eq_puniverses evd pbty f (x,u) (y,v) =
+ if f x y then
+ try
+ Success (Evd.set_eq_instances evd u v)
+ with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
+ else UnifFailure (evd, NotSameHead)
+
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
@@ -266,15 +294,19 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
could have found, we do it only if the terms are free of evar.
Note: incomplete heuristic... *)
let ground_test =
- if is_ground_term evd term1 && is_ground_term evd term2 then
- if is_trans_fconv pbty ts env evd term1 term2 then
- Some true
- else if is_ground_env evd env then Some false
- else None
- else None in
+ if is_ground_term evd term1 && is_ground_term evd term2 then (
+ let evd, b =
+ try infer_conv ~pb:pbty ~ts env evd term1 term2
+ with Univ.UniverseInconsistency _ -> evd, false
+ in
+ if b then Some (evd, true)
+ else if is_ground_env evd env then Some (evd, false)
+ else None)
+ else None
+ in
match ground_test with
- | Some true -> Success evd
- | Some false -> UnifFailure (evd,ConversionFailed (env,term1,term2))
+ | Some (evd, true) -> Success evd
+ | Some (evd, false) -> UnifFailure (evd,ConversionFailed (env,term1,term2))
| None ->
(* Until pattern-unification is used consistently, use nohdbeta to not
destroy beta-redexes that can be used for 1st-order unification *)
@@ -392,11 +424,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in
ise_try evd [f1; f2]
- | Flexible ev1, MaybeFlexible v2 -> flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2
+ | Flexible ev1, MaybeFlexible (v2,sk2) ->
+ flex_maybeflex true ev1 (appr1,csts1) ((term2,sk2),csts2) v2
- | MaybeFlexible v1, Flexible ev2 -> flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1
+ | MaybeFlexible (v1,sk1), Flexible ev2 ->
+ flex_maybeflex false ev2 (appr2,csts2) ((term1,sk1),csts1) v1
- | MaybeFlexible v1, MaybeFlexible v2 -> begin
+ | MaybeFlexible (v1,sk1), MaybeFlexible (v2,sk2) -> begin
match kind_of_term term1, kind_of_term term2 with
| LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) ->
let f1 i =
@@ -414,12 +448,37 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in
ise_try evd [f1; f2]
+ | Proj (p, c), Proj (p', c') when eq_constant p p' ->
+ let f1 i =
+ ise_and i
+ [(fun i -> evar_conv_x ts env i CONV c c');
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
+ and f2 i =
+ if is_transparent_constant ts p then
+ match unfold_projection env p c sk1 with
+ | Some (c, sk1) ->
+ let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (c,sk1) in
+ evar_eqappr_x ts env i pbty out1 (appr2, csts2)
+ | None -> assert false
+ else UnifFailure (i, NotSameHead)
+ in
+ ise_try evd [f1; f2]
+
| _, _ ->
- let f1 i =
- if eq_constr term1 term2 then
- exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2
- else
- UnifFailure (i,NotSameHead)
+ let f1 i =
+ (* Gather the universe constraints that would make term1 and term2 equal.
+ If these only involve unifications of flexible universes to other universes,
+ allow this identification (first-order unification of universes). Otherwise
+ fallback to unfolding.
+ *)
+ let b,univs = eq_constr_universes term1 term2 in
+ if b then
+ ise_and i [(fun i ->
+ try Success (Evd.add_universe_constraints i univs)
+ with UniversesDiffer -> UnifFailure (i,NotSameHead)
+ | Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
+ else UnifFailure (i,NotSameHead)
and f2 i =
(try conv_record ts env i
(try check_conv_record appr1 appr2
@@ -438,9 +497,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(* false (* immediate solution without Canon Struct *)*)
| Lambda _ -> assert (match args with [] -> true | _ -> false); true
| LetIn (_,b,_,c) -> is_unnamed
- (fst (whd_betaiota_deltazeta_for_iota_state
+ (fst (whd_betaiota_deltazeta_for_iota_state
ts env i Cst_stack.empty (subst1 b c, args)))
- | Case _| Fix _| App _| Cast _ -> assert false in
+ | Fix _ -> true (* Partially applied fix can be the result of a whd call *)
+ | Proj (p, c) -> true
+ | Case _ | App _| Cast _ -> assert false in
let rhs_is_stuck_and_unnamed () =
let applicative_stack = fst (Stack.strip_app sk2) in
is_unnamed
@@ -475,7 +536,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
| Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1
- | MaybeFlexible v1, Rigid ->
+ | MaybeFlexible (v1,sk1), Rigid ->
let f3 i =
(try conv_record ts env i (check_conv_record appr1 appr2)
with Not_found -> UnifFailure (i,NoCanonicalStructure))
@@ -487,14 +548,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in
ise_try evd [f3; f4]
- | Rigid, MaybeFlexible v2 ->
+ | Rigid, MaybeFlexible (v2,sk2) ->
let f3 i =
(try conv_record ts env i (check_conv_record appr2 appr1)
with Not_found -> UnifFailure (i,NoCanonicalStructure))
and f4 i =
- evar_eqappr_x ts env i pbty (appr1,csts1)
- (whd_betaiota_deltazeta_for_iota_state
- ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+ evar_eqappr_x ts env i pbty (appr1,csts1)
+ (whd_betaiota_deltazeta_for_iota_state
+ ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
in
ise_try evd [f3; f4]
@@ -515,8 +576,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
then Evd.set_eq_sort evd s1 s2
else Evd.set_leq_sort evd s1 s2
in Success evd'
- with Univ.UniverseInconsistency _ ->
- UnifFailure (evd,UnifUnivInconsistency)
+ with Univ.UniverseInconsistency p ->
+ UnifFailure (evd,UnifUnivInconsistency p)
| e when Errors.noncritical e -> UnifFailure (evd,NotSameHead))
| Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty ->
@@ -537,19 +598,19 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
else UnifFailure (evd,NotSameHead)
| Const c1, Const c2 ->
- if eq_constant c1 c2 then
- exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2
- else UnifFailure (evd,NotSameHead)
+ ise_and evd
+ [(fun i -> eq_puniverses i pbty eq_constant c1 c2);
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
| Ind sp1, Ind sp2 ->
- if eq_ind sp1 sp2 then
- exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2
- else UnifFailure (evd,NotSameHead)
+ ise_and evd
+ [(fun i -> eq_puniverses i pbty eq_ind sp1 sp2);
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
| Construct sp1, Construct sp2 ->
- if eq_constructor sp1 sp2 then
- exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2
- else UnifFailure (evd,NotSameHead)
+ ise_and evd
+ [(fun i -> eq_puniverses i pbty eq_constructor sp1 sp2);
+ (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
| Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *)
if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
@@ -583,13 +644,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _) ->
UnifFailure (evd,NotSameHead)
- | (App _ | Cast _ | Case _), _ -> assert false
+ | (App _ | Cast _ | Case _ | Proj _), _ -> assert false
| (LetIn _| Evar _), _ -> assert false
| (Lambda _), _ -> assert false
end
-and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
+and conv_record trs env evd (ctx,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
+ let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
if Reductionops.Stack.compare_shape ts ts1 then
let (evd',ks,_) =
List.fold_left
@@ -614,6 +676,28 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2))
(fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1)]
else UnifFailure(evd,(*dummy*)NotSameHead)
+and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) =
+ let mib = lookup_mind (fst ind) env in
+ match mib.Declarations.mind_record with
+ | Some (exp,projs) when Array.length projs > 0 ->
+ let pars = mib.Declarations.mind_nparams in
+ (try
+ let l1' = Stack.tail pars l1 in
+ if Environ.is_projection projs.(0) env then
+ let sk2 =
+ let term = Stack.zip c in
+ List.map (fun p -> mkProj (p, term)) (Array.to_list projs)
+ in
+ exact_ise_stack2 env evd (evar_conv_x ts) l1'
+ (Stack.append_app_list sk2 Stack.empty)
+ else raise (Failure "")
+ with Failure _ -> UnifFailure(evd,NotSameHead))
+ | _ -> UnifFailure (evd,NotSameHead)
+
+(* Profiling *)
+(* let evar_conv_xkey = Profile.declare_profile "evar_conv_x";; *)
+(* let evar_conv_x = Profile.profile6 evar_conv_xkey evar_conv_x *)
+
(* We assume here |l1| <= |l2| *)
let first_order_unification ts env evd (ev1,l1) (term2,l2) =
@@ -846,7 +930,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
(* Some head evar have been instantiated, or unknown kind of problem *)
evar_conv_x ts env evd pbty t1 t2
-let check_problems_are_solved evd =
+let check_problems_are_solved env evd =
match snd (extract_all_conv_pbs evd) with
| (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2)
| _ -> ()
@@ -890,10 +974,16 @@ let rec solve_unconstrained_evars_with_canditates ts evd =
let evd = aux (List.rev l) in
solve_unconstrained_evars_with_canditates ts evd
-let solve_unconstrained_impossible_cases evd =
+let solve_unconstrained_impossible_cases env evd =
Evd.fold_undefined (fun evk ev_info evd' ->
match ev_info.evar_source with
- | _,Evar_kinds.ImpossibleCase -> Evd.define evk (j_type (coq_unit_judge ())) evd'
+ | _,Evar_kinds.ImpossibleCase ->
+ let j, ctx = coq_unit_judge () in
+ let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd' ctx in
+ let ty = j_type j in
+ let conv_algo = evar_conv_x full_transparent_state in
+ let evd' = check_evar_instance evd' evk ty conv_algo in
+ Evd.define evk ty evd'
| _ -> evd') evd evd
let consider_remaining_unif_problems env
@@ -925,8 +1015,8 @@ let consider_remaining_unif_problems env
in
let (evd,pbs) = extract_all_conv_pbs evd in
let heuristic_solved_evd = aux evd pbs false [] in
- check_problems_are_solved heuristic_solved_evd;
- solve_unconstrained_impossible_cases heuristic_solved_evd
+ check_problems_are_solved env heuristic_solved_evd;
+ solve_unconstrained_impossible_cases env heuristic_solved_evd
(* Main entry points *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 08:56:14 +0000