diff options
| -rw-r--r-- | pretyping/evarconv.ml | 208 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 15 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 18 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 48 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 37 |
5 files changed, 214 insertions, 112 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d0b724b755..4b0974ae03 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -127,9 +127,10 @@ let flex_kind_of_term flags env evd c sk = else Rigid | Evar ev -> if is_evar_allowed flags (fst ev) then Flexible ev else Rigid - | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid + | Lambda _ | Prod _ | Sort _ | Ind _ | Int _ | Float _ | Array _ -> Rigid + | Construct _ | CoFix _ (* Incorrect: should check only app in sk *) -> Rigid | Meta _ -> Rigid - | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) + | Fix _ -> Rigid (* happens when the fixpoint is partially applied (should check it?) *) | Cast _ | App _ | Case _ -> assert false let apprec_nohdbeta flags env evd c = @@ -328,12 +329,6 @@ let ise_and evd l = | UnifFailure _ as x -> x in ise_and evd l -let ise_exact ise x1 x2 = - match ise x1 x2 with - | None, out -> out - | _, (UnifFailure _ as out) -> out - | Some _, Success i -> UnifFailure (i,NotSameArgSize) - let ise_array2 evd f v1 v2 = let rec allrec i = function | -1 -> Success i @@ -355,37 +350,49 @@ let rec ise_inst2 evd f l1 l2 = match l1, l2 with (* Applicative node of stack are read from the outermost to the innermost but are unified the other way. *) -let rec ise_app_stack2 env f evd sk1 sk2 = - match sk1,sk2 with - | Stack.App node1 :: q1, Stack.App node2 :: q2 -> - let (t1,l1) = Stack.decomp_node_last node1 q1 in - let (t2,l2) = Stack.decomp_node_last node2 q2 in - begin match ise_app_stack2 env f evd l1 l2 with - |(_,UnifFailure _) as x -> x - |x,Success i' -> x,f env i' CONV t1 t2 +let rec ise_app_rev_stack2 env f evd revsk1 revsk2 = + match Stack.decomp_rev revsk1, Stack.decomp_rev revsk2 with + | Some (t1,revsk1), Some (t2,revsk2) -> + begin + match ise_app_rev_stack2 env f evd revsk1 revsk2 with + | (_, UnifFailure _) as x -> x + | x, Success i' -> x, f env i' CONV t1 t2 end - | _, _ -> (sk1,sk2), Success evd + | _, _ -> (revsk1,revsk2), Success evd (* This function tries to unify 2 stacks element by element. It works from the end to the beginning. If it unifies a non empty suffix of stacks but not the entire stacks, the first part of the answer is - Some(the remaining prefixes to tackle)) *) -let ise_stack2 no_app env evd f sk1 sk2 = - let rec ise_stack2 deep i sk1 sk2 = - let fail x = if deep then Some (List.rev sk1, List.rev sk2), Success i + Some(the remaining prefixes to tackle) + If [no_app] is set, situations like [match head u1 u2 with ... end] + will not try to match [u1] and [u2] (why?); but situations like + [match head u1 u2 with ... end v] will try to match [v] (??) *) +(* Input: E1[] =? E2[] where the E1, E2 are concatenations of + n-ary-app/case/fix/proj elimination rules + Output: + - either None if E1 = E2 is solved, + - or Some (E1'',E2'') such that there is a decomposition of + E1[] = E1'[E1''[]] and E2[] = E2'[E2''[]] s.t. E1' = E2' and + E1'' cannot be unified with E2'' + - UnifFailure if no such non-empty E1' = E2' exists *) +let rec ise_stack2 no_app env evd f sk1 sk2 = + let rec ise_rev_stack2 deep i revsk1 revsk2 = + let fail x = if deep then Some (List.rev revsk1, List.rev revsk2), Success i else None, x in - match sk1, sk2 with + match revsk1, revsk2 with | [], [] -> None, Success i | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 -> - (match f env i CONV t1 t2 with - | Success i' -> - (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with - | Success i'' -> ise_stack2 true i'' q1 q2 - | UnifFailure _ as x -> fail x) - | UnifFailure _ as x -> fail x) + begin + match ise_and i [ + (fun i -> f env i CONV t1 t2); + (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2)] + with + | Success i' -> ise_rev_stack2 true i' q1 q2 + | UnifFailure _ as x -> fail x + end | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 -> if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) - then ise_stack2 true i q1 q2 + then ise_rev_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 -> @@ -393,51 +400,51 @@ let ise_stack2 no_app env evd f sk1 sk2 = match ise_and i [ (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); - (fun i -> ise_exact (ise_stack2 false i) a1 a2)] with - | Success i' -> ise_stack2 true i' q1 q2 + (fun i -> snd (ise_stack2 no_app env i f a1 a2))] with + | Success i' -> ise_rev_stack2 true i' q1 q2 | UnifFailure _ as x -> fail x else fail (UnifFailure (i,NotSameHead)) | Stack.App _ :: _, Stack.App _ :: _ -> if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else - begin match ise_app_stack2 env f i sk1 sk2 with + begin match ise_app_rev_stack2 env f i revsk1 revsk2 with |_,(UnifFailure _ as x) -> fail x - |(l1, l2), Success i' -> ise_stack2 true i' l1 l2 + |(l1, l2), Success i' -> ise_rev_stack2 true i' l1 l2 end |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead)) - in ise_stack2 false evd (List.rev sk1) (List.rev sk2) + in ise_rev_stack2 false evd (List.rev sk1) (List.rev sk2) (* Make sure that the matching suffix is the all stack *) -let exact_ise_stack2 env evd f sk1 sk2 = - let rec ise_stack2 i sk1 sk2 = - match sk1, sk2 with +let rec exact_ise_stack2 env evd f sk1 sk2 = + let rec ise_rev_stack2 i revsk1 revsk2 = + match revsk1, revsk2 with | [], [] -> Success i | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 -> ise_and i [ - (fun i -> ise_stack2 i q1 q2); + (fun i -> ise_rev_stack2 i q1 q2); (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2); (fun i -> f env i CONV t1 t2)] | 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 ise_and i [ - (fun i -> ise_stack2 i q1 q2); + (fun i -> ise_rev_stack2 i q1 q2); (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); - (fun i -> ise_stack2 i a1 a2)] + (fun i -> exact_ise_stack2 env i f a1 a2)] else UnifFailure (i,NotSameHead) | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 -> if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) - then ise_stack2 i q1 q2 + then ise_rev_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) | Stack.App _ :: _, Stack.App _ :: _ -> - begin match ise_app_stack2 env f i sk1 sk2 with + begin match ise_app_rev_stack2 env f i revsk1 revsk2 with |_,(UnifFailure _ as x) -> x - |(l1, l2), Success i' -> ise_stack2 i' l1 l2 + |(l1, l2), Success i' -> ise_rev_stack2 i' l1 l2 end |_, _ -> UnifFailure (i,(* Maybe improve: *) NotSameHead) in if Reductionops.Stack.compare_shape sk1 sk2 then - ise_stack2 evd (List.rev sk1) (List.rev sk2) + ise_rev_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) (* Add equality constraints for covariant/invariant positions. For @@ -575,31 +582,35 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) in - let miller_pfenning on_left fallback ev lF tM evd = + let miller_pfenning l2r fallback ev lF tM evd = match is_unification_pattern_evar env evd ev lF tM with | None -> fallback () | Some l1' -> (* Miller-Pfenning's patterns unification *) let t2 = tM in let t2 = solve_pattern_eqn env evd l1' t2 in solve_simple_eqn (conv_fun evar_conv_x) flags env evd - (position_problem on_left pbty,ev,t2) + (position_problem l2r pbty,ev,t2) in - let consume_stack on_left (termF,skF) (termO,skO) evd = - let switch f a b = if on_left then f a b else f b a in + let consume_stack l2r (termF,skF) (termO,skO) evd = + let switch f a b = if l2r then f a b else f b a in let not_only_app = Stack.not_purely_applicative skO in match switch (ise_stack2 not_only_app env evd (evar_conv_x flags)) skF skO with - |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) -> + | Some (l,r), Success i' when l2r && (not_only_app || List.is_empty l) -> + (* E[?n]=E'[redex] reduces to either l[?n]=r[redex] with + case/fix/proj in E' (why?) or ?n=r[redex] *) switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) - |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) -> + | Some (r,l), Success i' when not l2r && (not_only_app || List.is_empty l) -> + (* E'[redex]=E[?n] reduces to either r[redex]=l[?n] with + case/fix/proj in E' (why?) or r[redex]=?n *) switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) - |None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO - |_, (UnifFailure _ as x) -> x - |Some _, _ -> UnifFailure (evd,NotSameArgSize) in - let eta env evd onleft sk term sk' term' = - assert (match sk with [] -> true | _ -> false); + | None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO + | _, (UnifFailure _ as x) -> x + | Some _, _ -> UnifFailure (evd,NotSameArgSize) in + let eta_lambda env evd onleft term (term',sk') = + (* Reduces an equation [env |- <(fun na:c1 => c'1)|empty> = <term'|sk'>] to + [env, na:c1 |- c'1 = sk'[term'] (with some additional reduction) *) let (na,c1,c'1) = destLambda evd term in - let c = nf_evar evd c1 in - let env' = push_rel (RelDecl.LocalAssum (na,c)) env in + let env' = push_rel (RelDecl.LocalAssum (na,c1)) env in let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env' evd (c'1, Stack.empty) in let out2 = whd_nored_state env' evd @@ -617,32 +628,39 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')] in - let consume on_left (_, skF as apprF) (_,skM as apprM) i = + let consume l2r (_, skF as apprF) (_,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then - consume_stack on_left apprF apprM i + consume_stack l2r apprF apprM i else quick_fail i in - let miller on_left ev (termF,skF as apprF) (termM, skM as apprM) i = - let switch f a b = if on_left then f a b else f b a in + let miller l2r ev (termF,skF as apprF) (termM, skM as apprM) i = + let switch f a b = if l2r then f a b else f b a in let not_only_app = Stack.not_purely_applicative skM in match Stack.list_of_app_stack skF with | None -> quick_fail evd | Some lF -> let tM = Stack.zip evd apprM in - miller_pfenning on_left + miller_pfenning l2r (fun () -> if not_only_app then (* Postpone the use of an heuristic *) switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM else quick_fail i) ev lF tM i in - let flex_maybeflex on_left ev (termF,skF as apprF) (termM, skM as apprM) vM = - let switch f a b = if on_left then f a b else f b a in + let flex_maybeflex l2r ev (termF,skF as apprF) (termM, skM as apprM) vM = + (* Problem: E[?n[inst]] = E'[redex] + Strategy, as far as I understand: + 1. if E[]=[]u1..un and ?n[inst] u1..un = E'[redex] is a Miller pattern: solve it now + 2a. if E'=E'1[E'2] and E=E'1 unifiable, recursively solve ?n[inst] = E'2[redex] + 2b. if E'=E'1[E'2] and E=E1[E2] and E=E'1 unifiable and E' contient app/fix/proj, + recursively solve E2[?n[inst]] = E'2[redex] + 3. reduce the redex into M and recursively solve E[?n[inst]] =? E'[M] *) + let switch f a b = if l2r then f a b else f b a in let delta i = switch (evar_eqappr_x flags env i pbty) apprF (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (vM,skM)) in - let default i = ise_try i [miller on_left ev apprF apprM; - consume on_left apprF apprM; + let default i = ise_try i [miller l2r ev apprF apprM; + consume l2r apprF apprM; delta] in match EConstr.kind evd termM with @@ -663,8 +681,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let delta' i = switch (evar_eqappr_x flags env i pbty) apprF apprM' in - fun i -> ise_try i [miller on_left ev apprF apprM'; - consume on_left apprF apprM'; delta'] + fun i -> ise_try i [miller l2r ev apprF apprM'; + consume l2r apprF apprM'; delta'] with Retyping.RetypeError _ -> (* Happens thanks to w_unify building ill-typed terms *) default @@ -672,21 +690,32 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty end | _ -> default evd in - let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = - let switch f a b = if on_left then f a b else f b a in + let flex_rigid l2r ev (termF, skF as apprF) (termR, skR as apprR) = + (* Problem: E[?n[inst]] = E'[M] with M blocking computation (in theory) + Strategy, as far as I understand: + 1. if E[]=[]u1..un and ?n[inst] u1..un = E'[M] is a Miller pattern: solve it now + 2a. if E'=E'1[E'2] and E=E'1 unifiable and E' contient app/fix/proj, + recursively solve ?n[inst] = E'2[M] + 2b. if E'=E'1[E'2] and E=E1[E2] and E=E'1 unifiable and E' contient app/fix/proj, + recursively solve E2[?n[inst]] = E'2[M] + 3a. if M a lambda or a constructor: eta-expand and recursively solve + 3b. if M a constructor C ..ui..: eta-expand and recursively solve proji[E[?n[inst]]]=ui + 4. fail if E purely applicative and ?n occurs rigidly in E'[M] + 5. absorb arguments if purely applicative and postpone *) + let switch f a b = if l2r then f a b else f b a in let eta evd = match EConstr.kind evd termR with | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> - eta env evd false skR termR skF termF - | Construct u -> eta_constructor flags env evd skR u skF termF + eta_lambda env evd false termR apprF + | Construct u -> eta_constructor flags env evd u skR apprF | _ -> UnifFailure (evd,NotSameHead) in match Stack.list_of_app_stack skF with | None -> - ise_try evd [consume_stack on_left apprF apprR; eta] + ise_try evd [consume_stack l2r apprF apprR; eta] | Some lF -> let tR = Stack.zip evd apprR in - miller_pfenning on_left + miller_pfenning l2r (fun () -> ise_try evd [eta;(* Postpone the use of an heuristic *) @@ -716,6 +745,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty solve_simple_eqn (conv_fun evar_conv_x) flags env i' (position_problem true pbty,destEvar i' ev1',term2) else + (* HH: Why not to drop sk1 and sk2 since they unified *) evar_eqappr_x flags env evd pbty (ev1', sk1) (term2, sk2) | Some (r,[]), Success i' -> @@ -736,7 +766,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty if isEvar i' ev1' then solve_simple_eqn (conv_fun evar_conv_x) flags env i' (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r)) - else evar_eqappr_x flags env evd pbty + else + (* HH: Why not to drop sk1 and sk2 since they unified *) + evar_eqappr_x flags env evd pbty (ev1', sk1) (term2, sk2) | None, (UnifFailure _ as x) -> (* sk1 and sk2 have no common outer part *) @@ -764,7 +796,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty else (* We could instead try Miller unification, then postpone to see if other equations help, as in: - [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *) + [Check fun a b c : unit => (eq_refl : _ a b = _ c a b)] *) UnifFailure (i,NotSameArgSize) | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") in @@ -776,7 +808,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty match (flex_kind_of_term flags env evd term1 sk1, flex_kind_of_term flags env evd term2 sk2) with | Flexible (sp1,al1), Flexible (sp2,al2) -> - (* sk1[?ev1] =? sk2[?ev2] *) + (* Notations: + - "sk" is a stack (or, more abstractly, an evaluation context, written E) + - "ev" is an evar "?ev", more precisely an evar ?n with an instance inst + - "al" is an evar instance + Problem: E₁[?n₁[inst₁]] = E₂[?n₂[inst₂]] (i.e. sk1[?ev1] =? sk2[?ev2] + Strategy is first-order unification + 1a. if E₁=E₂ unifiable, solve ?n₁[inst₁] = ?n₂[inst₂] + 1b. if E₂=E₂'[E₂''] and E₁=E₂' unifiable, recursively solve ?n₁[inst₁] = E₂''[?n₂[inst₂]] + 1b'. if E₁=E₁'[E₁''] and E₁'=E₂ unifiable, recursively solve E₁''[?n₁[inst₁]] = ?n₂[inst₂] + recursively solve E2[?n[inst]] = E'2[redex] + 2. fails if neither E₁ nor E₂ is a prefix of the other *) let f1 i = first_order env i term1 term2 sk1 sk2 and f2 i = if Evar.equal sp1 sp2 then @@ -976,10 +1018,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (* Eta-expansion *) | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 -> - eta env evd true sk1 term1 sk2 term2 + eta_lambda env evd true term1 (term2,sk2) | _, Rigid when isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 -> - eta env evd false sk2 term2 sk1 term1 + eta_lambda env evd false term2 (term1,sk1) | Rigid, Rigid -> begin match EConstr.kind evd term1, EConstr.kind evd term2 with @@ -1033,10 +1075,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty else UnifFailure (evd,NotSameHead) | Construct u, _ -> - eta_constructor flags env evd sk1 u sk2 term2 + eta_constructor flags env evd u sk1 (term2,sk2) | _, Construct u -> - eta_constructor flags env evd sk2 u sk1 term1 + eta_constructor flags env evd u sk2 (term1,sk1) | 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 @@ -1131,7 +1173,9 @@ and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk (fst (decompose_app_vect i (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) -and eta_constructor flags env evd sk1 ((ind, i), u) sk2 term2 = +and eta_constructor flags env evd ((ind, i), u) sk1 (term2,sk2) = + (* reduces an equation <Construct(ind,i)|sk1> == <term2|sk2> to the + equations [arg_i = Proj_i (sk2[term2])] where [sk1] is [params args] *) let open Declarations in let mib = lookup_mind (fst ind) env in match get_projections env ind with diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 44414aa6a0..f9f6f74a66 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1585,7 +1585,16 @@ let rec invert_definition unify flags choose imitate_defs imitate envk (subst1 b c) | Evar (evk',args' as ev') -> if Evar.equal evk evk' then raise (OccurCheckIn (evd,rhs)); - (* Evar/Evar problem (but left evar is virtual) *) + (* At this point, we imitated a context say, C[ ], and virtually + instantiated ?evk@{x₁..xn} with C[?evk''@{x₁..xn,y₁..yk}] + for y₁..yk the spine of variables of C[ ], now facing the + equation env, y₁...yk |- ?evk'@{args'} =?= ?evk''@{args,y1:=y1..yk:=yk} *) + (* Assume evk' is defined in context x₁'..xk'. + As a first step, we try to find a restriction ?evk'''@{xᵢ₁'..xᵢⱼ} of + ?evk' and an instance args''' in the environment of ?evk such that + env, y₁..yk |- args'''[args] = args' and thus such that + env, y₁..yk |- ?evk'''@{args'''[args]} = ?evk''@{args,y1:=y1..yk:=yk} *) + (* Note that we don't need to declare ?evk'' yet: it may remain virtual *) let aliases = lift_aliases k aliases in (try let ev = (evk,List.map (lift k) argsv) in @@ -1597,14 +1606,14 @@ let rec invert_definition unify flags choose imitate_defs | CannotProject (evd,ev') -> if not !progress then raise (NotEnoughInformationEvarEvar t); - (* Make the virtual left evar real *) + (* We could not invert args' in terms of args, so we now make ?evk'' real *) let ty = get_type_of env' evd t in let (evd,evar'',ev'') = materialize_evar (evar_define unify flags ~choose) env' evd k ev ty in (* materialize_evar may instantiate ev' by another evar; adjust it *) let (evk',args' as ev') = normalize_evar evd ev' in let evd = - (* Try to project (a restriction of) the left evar ... *) + (* Try now to invert args in terms of args' *) try let evd,body = project_evar_on_evar false unify flags env' evd aliases 0 None ev'' ev' in let evd = Evd.define evk' body evd in diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 094dae4828..d347f46637 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -136,6 +136,24 @@ val solve_evar_evar : ?force:bool -> (** The two evars are expected to be in inferably convertible types; if not, an exception IllTypedInstance is raised *) +(* [solve_simple_eqn unifier flags env evd (direction,?ev[inst],t)] + makes progresses on problems of the form [?ev[inst] := t] (or + [?ev[inst] :<= t], or [?ev[inst] :>= t]). It uses imitation and a + limited form of projection. At the time of writing this comment, + only rels/vars (possibly indirectly via a chain of evars) and + constructors are used for projection. For instance + [?e[x,S 0] := x + S 0] will be solved by imitating [+] and + projecting [x] and [S 0] (so that [?e[a,b]:=a+b]) but in + [?e[0+0] := 0+0], the possible imitation will not be seen. + + [choose] tells to make an irreversible choice when two valid + projections are competing. It is to be used when no more reversible + progress can be done. It is [false] by default. + + [imitate_defs] tells to expand local definitions if they cannot be + projected. It is [true] by default. +*) + val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option * existential * constr -> unification_result diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 9580825010..52f60fbc5e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -194,6 +194,7 @@ sig val append_app : 'a array -> 'a t -> 'a t val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) + val decomp_rev : 'a t -> ('a * 'a t) option val compare_shape : 'a t -> 'a t -> bool val map : ('a -> 'a) -> 'a t -> 'a t val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> @@ -214,13 +215,13 @@ end = struct open EConstr type 'a app_node = int * 'a array * int - (* first releavnt position, arguments, last relevant position *) + (* first relevant position, arguments, last relevant position *) (* - Invariant that this module must ensure : - (behare of direct access to app_node by the rest of Reductionops) + Invariant that this module must ensure: + (beware of direct access to app_node by the rest of Reductionops) - in app_node (i,_,j) i <= j - - There is no array realocation (outside of debug printing) + - There is no array reallocation (outside of debug printing) *) let pr_app_node pr (i,a,j) = @@ -267,12 +268,10 @@ struct let le = Array.length v in if Int.equal le 0 then s else App (0,v,pred le) :: s - let decomp_node (i,l,j) sk = - if i < j then (l.(i), App (succ i,l,j) :: sk) - else (l.(i), sk) - - let decomp = function - | App node::s -> Some (decomp_node node s) + let decomp_rev = function + | App (i,l,j) :: sk -> + if i < j then Some (l.(j), App (i,l,pred j) :: sk) + else Some (l.(j), sk) | _ -> None let decomp_node_last (i,l,j) sk = @@ -293,7 +292,7 @@ struct Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 | (Primitive(_,_,a1,_)::s1, Primitive(_,_,a2,_)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 - | ((Case _|Proj _|Fix _|Primitive _) :: _ | []) ,_ -> false in + | ((Case _ | Proj _ | Fix _ | Primitive _) :: _ | []) ,_ -> false in compare_rec 0 stk1 stk2 exception IncompatibleFold2 @@ -334,29 +333,35 @@ struct append_app a s let rec args_size = function - | App (i,_,j)::s -> j + 1 - i + args_size s - | (Case _|Fix _|Proj _|Primitive _)::_ | [] -> 0 + | App (i,_,j) :: s -> j + 1 - i + args_size s + | (Case _ | Fix _ | Proj _ | Primitive _) :: _ | [] -> 0 let strip_app s = let rec aux out = function | ( App _ as e) :: s -> aux (e :: out) s | s -> List.rev out,s in aux [] s + let strip_n_app n s = let rec aux n out = function | App (i,a,j) as e :: s -> - let nb = j - i + 1 in + let nb = j - i + 1 in if n >= nb then - aux (n - nb) (e::out) s + aux (n - nb) (e :: out) s else - let p = i+n in + let p = i + n in Some (CList.rev (if Int.equal n 0 then out else App (i,a,p-1) :: out), a.(p), - if j > p then App(succ p,a,j)::s else s) + if j > p then App (succ p,a,j) :: s else s) | s -> None in aux n [] s + let decomp s = + match strip_n_app 0 s with + | Some (_,a,s) -> Some (a,s) + | None -> None + let not_purely_applicative args = List.exists (function (Fix _ | Case _ | Proj _ ) -> true | App _ | Primitive _ -> false) args @@ -369,12 +374,11 @@ struct (Array.fold_right (fun x y -> x::y) a' args', s') | s -> ([],s) in let (out,s') = aux s in - let init = match s' with [] -> true | _ -> false in - Option.init init out + match s' with [] -> Some out | _ -> None let assign s p c = match strip_n_app p s with - | Some (pre,_,sk) -> pre @ (App (0,[|c|],0)::sk) + | Some (pre,_,sk) -> pre @ (App (0,[|c|],0) :: sk) | None -> assert false let tail n0 s0 = @@ -382,12 +386,12 @@ struct if Int.equal n 0 then s else match s with | App (i,a,j) :: s -> - let nb = j - i + 1 in + let nb = j - i + 1 in if n >= nb then aux (n - nb) s else let p = i+n in - if j >= p then App(p,a,j)::s else s + if j >= p then App (p,a,j) :: s else s | _ -> raise (Invalid_argument "Reductionops.Stack.tail") in aux n0 s0 diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 0b7f43f469..ae93eb48b4 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -69,10 +69,9 @@ module Stack : sig val empty : 'a t val is_empty : 'a t -> bool - val append_app : 'a array -> 'a t -> 'a t - val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) + [@@ocaml.deprecated "Use decomp_rev"] val compare_shape : 'a t -> 'a t -> bool @@ -84,23 +83,51 @@ module Stack : sig val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> constr t -> constr t -> 'a val map : ('a -> 'a) -> 'a t -> 'a t + + (** [append_app args sk] pushes array of arguments [args] on [sk] *) + val append_app : 'a array -> 'a t -> 'a t + + (** [append_app_list args sk] pushes list of arguments [args] on [sk] *) val append_app_list : 'a list -> 'a t -> 'a t - (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not - start by App *) + (** if [strip_app sk] = [(sk1,sk2)], then [sk = sk1 @ sk2] with + [sk1] purely applicative and [sk2] does not start with an argument *) val strip_app : 'a t -> 'a t * 'a t - (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) + (** @return (the nth first elements, the (n+1)th element, the remaining stack) + if there enough of those *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option + (** [decomp sk] extracts the first argument of [sk] is there is some *) + val decomp : 'a t -> ('a * 'a t) option + + (** [decomp sk] extracts the first argument of reversed stack [sk] is there is some *) + val decomp_rev : 'a t -> ('a * 'a t) option + + (** [not_purely_applicative sk] *) val not_purely_applicative : 'a t -> bool + + (** [list_of_app_stack sk] either returns [Some sk] turned into a list of + arguments if [sk] is purely applicative and [None] otherwise *) val list_of_app_stack : constr t -> constr list option + (** [assign sk n a] changes the [n]th argument of [sk] with [a], counting from 0 + @raise an anomaly if there is less that [n] arguments available *) val assign : 'a t -> int -> 'a -> 'a t + + (** [args_size sk] returns the number of arguments available at the + head of [sk] *) val args_size : 'a t -> int + + (** [tail n sk] drops the [n] first arguments of [sk] + @raise [Invalid_argument] if there are not enough arguments *) val tail : int -> 'a t -> 'a t + + (** [nth sk n] returns the [n]-th argument of [sk], counting from 0 + @raise [Not_found] if there is no [n]th argument *) val nth : 'a t -> int -> 'a + (** [zip sigma t sk] *) val zip : evar_map -> constr * constr t -> constr end |