diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 70 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 5 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 41 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 71 |
5 files changed, 84 insertions, 105 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ddaf69676..a8ab0666d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -33,27 +33,33 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_unification:=a); } -let unfold_projection env ts p c stk = +let unfold_projection env evd ts p c stk = (match try Some (lookup_projection p env) with Not_found -> None with | Some pb -> let cst = Projection.constant p in let unfold () = let s = Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, - Projection.constant p) in + p, Cst_stack.empty) in Some (c, s :: stk) in + let unfold_app () = + let t' = Retyping.expand_projection env evd p c [] in + let f, args = destApp t' in + let stk = Stack.append_app args stk in + Some (f, stk) + in if Projection.unfolded p then unfold () else if is_transparent_constant ts cst then (match ReductionBehaviour.get (Globnames.ConstRef cst) with - | None -> unfold () + | None -> unfold_app () | Some (recargs, nargs, flags) -> if (List.mem `ReductionNeverUnfold flags) then None - else unfold ()) + else unfold_app ()) else None | None -> None) -let eval_flexible_term ts env c stk = +let eval_flexible_term ts env evd c stk = match kind_of_term c with | Const (c,u as cu) -> if is_transparent_constant ts c @@ -70,7 +76,7 @@ let eval_flexible_term ts env c stk = with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c, stk) | Lambda _ -> Some (c, stk) - | Proj (p, c) -> unfold_projection env ts p c stk + | Proj (p, c) -> unfold_projection env evd ts p c stk | _ -> assert false type flex_kind_of_term = @@ -78,10 +84,10 @@ type flex_kind_of_term = | 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 = +let flex_kind_of_term ts env evd c sk = match kind_of_term c with | LetIn _ | Rel _ | Const _ | Var _ | Proj _ -> - Option.cata (fun (x,y) -> MaybeFlexible (x,y)) Rigid (eval_flexible_term ts env c sk) + Option.cata (fun (x,y) -> MaybeFlexible (x,y)) Rigid (eval_flexible_term ts env evd 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 @@ -143,7 +149,8 @@ let check_conv_record (t1,sk1) (t2,sk2) = 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) + 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)),[] @@ -254,8 +261,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 + | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> + if eq_constant (Projection.constant p1) (Projection.constant 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 -> @@ -297,8 +305,9 @@ let exact_ise_stack2 env evd f sk1 sk2 = (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); (fun i -> ise_stack2 i a1 a2)] else UnifFailure (i,NotSameHead) - | Stack.Proj (n1,a1,p1)::q1, Stack.Proj (n2,a2,p2)::q2 -> - if eq_constant p1 p2 then ise_stack2 i q1 q2 + | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> + if eq_constant (Projection.constant p1) (Projection.constant p2) + then ise_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false @@ -394,7 +403,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd - (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), Cst_stack.empty in + (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), + Cst_stack.empty in if onleft then evar_eqappr_x ts env' evd CONV out1 out2 else evar_eqappr_x ts env' evd CONV out2 out1 in @@ -461,7 +471,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let open Pp in pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in - match (flex_kind_of_term (fst ts) env term1 sk1, flex_kind_of_term (fst ts) env term2 sk2) with + match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> let f1 i = match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with @@ -541,36 +551,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in evar_eqappr_x ts env i pbty out1 out2 in ise_try evd [f1; f2] - - | Proj (p, t), Const (p',_) when eq_constant (Projection.constant p) p' -> - let f1 i = - let pb = Environ.lookup_projection p env in - (match Stack.strip_n_app pb.Declarations.proj_npars sk2' with - | Some (pars, t', rest) -> - ise_and i - [(fun i -> evar_conv_x ts env i CONV t t'); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 rest)] - | None -> UnifFailure (evd, NotSameHead)) - and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1') - and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2') - in evar_eqappr_x ts env i pbty out1 out2 - in ise_try evd [f1;f2] - - | Const (p',_), Proj (p, t) when eq_constant (Projection.constant p) p' -> - let f1 i = - let pb = Environ.lookup_projection p env in - (match Stack.strip_n_app pb.Declarations.proj_npars sk1' with - | Some (pars, t', rest) -> - ise_and i - [(fun i -> evar_conv_x ts env i CONV t t'); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) rest sk2)] - | None -> UnifFailure (evd, NotSameHead)) - and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1') - and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2') - in evar_eqappr_x ts env i pbty out1 out2 - in ise_try evd [f1;f2] | _, _ -> let f1 i = diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f02d7623d..7b1fee543 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -705,7 +705,8 @@ let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in - let s = destSort evi.evar_concl in + let concl = whd_evar evd evi.evar_concl in + let s = destSort concl in let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in let evd2,rng = let newenv = push_named (id, None, dom) evenv in @@ -713,7 +714,7 @@ let define_pure_evar_as_product evd evk = let filter = Filter.extend 1 (evar_filter evi) in if is_prop_sort s then (* Impredicative product, conclusion must fall in [Prop]. *) - new_evar newenv evd1 evi.evar_concl ~src ~filter + new_evar newenv evd1 concl ~src ~filter else let evd3, (rng, srng) = new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 4761f824e..58d309997 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -208,7 +208,7 @@ sig type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * constant + | Proj of int * int * projection * Cst_stack.t | Fix of fixpoint * 'a t * Cst_stack.t | Cst of 'a cst_member * int * int list * 'a t * Cst_stack.t | Shift of int @@ -262,7 +262,7 @@ struct type 'a member = | App of 'a app_node | Case of Term.case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * constant + | Proj of int * int * projection * Cst_stack.t | Fix of fixpoint * 'a t * Cst_stack.t | Cst of 'a cst_member * int * int list * 'a t * Cst_stack.t | Shift of int @@ -278,9 +278,9 @@ struct str "ZCase(" ++ prvect_with_sep (pr_bar) pr_c br ++ str ")" - | Proj (n,m,p) -> + | Proj (n,m,p,cst) -> str "ZProj(" ++ int n ++ pr_comma () ++ int m ++ - pr_comma () ++ pr_con p ++ str ")" + pr_comma () ++ pr_con (Projection.constant p) ++ str ")" | Fix (f,args,cst) -> str "ZFix(" ++ Termops.pr_fix Termops.print_constr f ++ pr_comma () ++ pr pr_c args ++ str ")" @@ -346,8 +346,9 @@ struct if f (t1,lft1) (t2,lft2) && CArray.equal (fun x y -> f (x,lft1) (y,lft2)) a1 a2 then equal_rec s1 lft1 s2 lft2 else None - | (Proj (n1,m1,p)::s1, Proj(n2,m2,p2)::s2) -> - if Int.equal n1 n2 && Int.equal m1 m2 && Constant.equal p p2 + | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) -> + if Int.equal n1 n2 && Int.equal m1 m2 + && Constant.equal (Projection.constant p) (Projection.constant p2) then equal_rec s1 lft1 s2 lft2 else None | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' -> @@ -375,7 +376,7 @@ struct | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 - | (Proj (n1,m1,p)::s1, Proj(n2,m2,p2)::s2) -> + | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 | (Fix(_,a1,_)::s1, Fix(_,a2,_)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -402,7 +403,7 @@ struct aux (fold_array (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) a1 a2) lft1 q1 lft2 q2 - | Proj (n1,m1,p1) :: q1, Proj (n2,m2,p2) :: q2 -> + | Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 -> aux o lft1 q1 lft2 q2 | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 -> let (o',lft1',lft2') = aux (fold_array (fold_array o b1 b2) a1 a2) @@ -418,7 +419,7 @@ struct let rec map f x = List.map (function | Update _ -> assert false - | (Proj (_,_,_) | Shift _) as e -> e + | (Proj (_,_,_,_) | Shift _) as e -> e | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) @@ -537,7 +538,9 @@ struct | f, (Cst (cst,_,_,params,_)::s) -> zip ~refold (constr_of_cst_member cst (params @ (append_app [|f|] s))) | f, (Shift n::s) -> zip ~refold (lift n f, s) - | f, (Proj (n,m,p)::s) -> zip ~refold (mkProj (Projection.make p true,f),s) + | f, (Proj (n,m,p,cst_l)::s) when refold -> + zip ~refold (best_state (mkProj (p,f),s) cst_l) + | f, (Proj (n,m,p,_)::s) -> zip ~refold (mkProj (p,f),s) | _, (Update _::_) -> assert false end @@ -837,7 +840,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = and arg = pb.Declarations.proj_arg in match ReductionBehaviour.get (Globnames.ConstRef kn) with | None -> - let stack' = (c, Stack.Proj (npars, arg, kn) :: stack) in + let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in let stack'', csts = whrec Cst_stack.empty stack' in if equal_stacks stack' stack'' then fold () else stack'', csts @@ -854,7 +857,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = |[] -> (* if nargs has been specified *) (* CAUTION : the constant is NEVER refold (even when it hides a (co)fix) *) - let stack' = (c, Stack.Proj (npars, arg, kn) :: stack) in + let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in whrec Cst_stack.empty(* cst_l *) stack' | curr::remains -> if curr == 0 then (* Try to reduce the record argument *) @@ -910,7 +913,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = match Stack.strip_app stack with |args, (Stack.Case(ci, _, lf,_)::s') -> whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') - |args, (Stack.Proj (n,m,p)::s') -> + |args, (Stack.Proj (n,m,p,_)::s') -> whrec Cst_stack.empty (Stack.nth args (n+m), s') |args, (Stack.Fix (f,s',cst_l)::s'') -> let x' = Stack.zip(x,args) in @@ -935,7 +938,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = match Stack.strip_n_app 0 stack with | None -> assert false | Some (_,arg,s'') -> - whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,Projection.constant p) :: s'')) + whrec Cst_stack.empty (arg, Stack.Proj (npars,narg,p,cst_l) :: s'')) | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with | None -> fold () | Some (bef,arg,s''') -> @@ -991,7 +994,7 @@ let local_whd_state_gen flags sigma = | Proj (p,c) when Closure.RedFlags.red_projection flags p -> (let pb = lookup_projection p (Global.env ()) in whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, - Projection.constant p) + p, Cst_stack.empty) :: stack)) | Case (ci,p,d,lf) -> @@ -1017,7 +1020,7 @@ let local_whd_state_gen flags sigma = match Stack.strip_app stack with |args, (Stack.Case(ci, _, lf,_)::s') -> whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') - |args, (Stack.Proj (n,m,p) :: s') -> + |args, (Stack.Proj (n,m,p,_) :: s') -> whrec (Stack.nth args (n+m), s') |args, (Stack.Fix (f,s',cst)::s'') -> let x' = Stack.zip(x,args) in @@ -1465,12 +1468,12 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' - |args, (Stack.Proj (n,m,p) :: stack'' as stack') -> + |args, (Stack.Proj (n,m,p,_) :: stack'' as stack') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in if isConstruct t_o then - if Closure.is_transparent_constant ts p then - whrec Cst_stack.empty (* csts_o *) (Stack.nth stack_o (n+m), stack'') + if Projection.unfolded p || Closure.is_transparent_constant ts (Projection.constant p) + then whrec Cst_stack.empty (* csts_o *) (Stack.nth stack_o (n+m), stack'') else (* Won't unfold *) (whd_betaiota_state sigma (t_o, stack_o@stack'),csts') else s,csts' |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts' diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 9a9b34751..3335f0023 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -57,7 +57,7 @@ module Stack : sig type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * constant + | Proj of int * int * projection * Cst_stack.t | Fix of fixpoint * 'a t * Cst_stack.t | Cst of 'a cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 735d4b68a..f99ea9a52 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -390,7 +390,7 @@ let unfold_projection env p 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, - Projection.constant p) in + p, Cst_stack.empty) in s :: stk | None -> assert false) @@ -519,9 +519,10 @@ let eta_constructor_app env f l1 term = let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with | Some (projs, _) -> - let pars = mib.Declarations.mind_nparams in - let l1' = Array.sub l1 pars (Array.length l1 - pars) in - let l2 = Array.map (fun p -> mkProj (Projection.make p false, term)) projs in + let npars = mib.Declarations.mind_nparams in + let pars, l1' = Array.chop npars l1 in + let arg = Array.append pars [|term|] in + let l2 = Array.map (fun p -> mkApp (mkConstU (p,u), arg)) projs in l1', l2 | _ -> assert false) | _ -> assert false @@ -653,6 +654,33 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb with ex when precatchable_exception ex -> reduce curenvnb pb b wt substn cM cN) + | Proj (p1,c1), Proj (p2,c2) -> + if eq_constant (Projection.constant p1) (Projection.constant p2) then + try + let substn = unirec_rec curenvnb CONV true wt substn c1 c2 in + try (* Force unification of the types to fill in parameters *) + let ty1 = get_type_of curenv ~lax:true sigma c1 in + let ty2 = get_type_of curenv ~lax:true sigma c2 in + unify_0_with_initial_metas substn true env cv_pb + { flags with modulo_conv_on_closed_terms = Some full_transparent_state; + modulo_delta = full_transparent_state; + modulo_eta = true; + modulo_betaiota = true } + ty1 ty2 + with RetypeError _ -> substn + with ex when precatchable_exception ex -> + unify_not_same_head curenvnb pb b wt substn cM cN + else + unify_not_same_head curenvnb pb b wt substn cM cN + + | Proj (p1,c1), _ when not (Projection.unfolded p1) -> + let cM' = Retyping.expand_projection curenv sigma p1 c1 [] in + unirec_rec curenvnb CONV true false substn cM' cN + + | _, Proj (p2,c2) when not (Projection.unfolded p2) -> + let cN' = Retyping.expand_projection curenv sigma p2 c2 [] in + unirec_rec curenvnb CONV true false substn cM cN' + | App (f1,l1), _ when (isMeta f1 && use_metas_pattern_unification flags nb l1 || use_evars_pattern_unification flags && isAllowedEvar flags f1) -> @@ -679,41 +707,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | Some l -> solve_pattern_eqn_array curenvnb f2 l cM substn) - | Proj (p1,c1), Proj (p2,c2) -> - if eq_constant (Projection.constant p1) (Projection.constant p2) then - try - let substn = unirec_rec curenvnb CONV true wt substn c1 c2 in - try (* Force unification of the types to fill in parameters *) - let ty1 = get_type_of curenv ~lax:true sigma c1 in - let ty2 = get_type_of curenv ~lax:true sigma c2 in - unify_0_with_initial_metas substn true env cv_pb - { flags with modulo_conv_on_closed_terms = Some full_transparent_state; - modulo_delta = full_transparent_state; - modulo_eta = true; - modulo_betaiota = true } - ty1 ty2 - with RetypeError _ -> substn - with ex when precatchable_exception ex -> - unify_not_same_head curenvnb pb b wt substn cM cN - else - unify_not_same_head curenvnb pb b wt substn cM cN - - | App (f1, l1), Proj (p', c) when isConst f1 && - eq_constant (fst (destConst f1)) (Projection.constant p') -> - expand curenvnb pb b false substn cM f1 l1 cN cN [||] - - | Proj (p', c), App (f1, l1) when isConst f1 && - eq_constant (fst (destConst f1)) (Projection.constant p') -> - expand curenvnb pb b false substn cM f1 l1 cN cN [||] - | App (f1,l1), App (f2,l2) -> - (match kind_of_term f1, kind_of_term f2 with - | Const (p, u), Proj (p', c) when eq_constant p (Projection.constant p') -> - expand curenvnb pb b false substn cM f1 l1 cN f2 l2 - | Proj (p', _), Const (p, _) when eq_constant p (Projection.constant p') -> - expand curenvnb pb b false substn cM f1 l1 cN f2 l2 - | _ -> - unify_app curenvnb pb b substn cM f1 l1 cN f2 l2) + unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 | _ -> unify_not_same_head curenvnb pb b wt substn cM cN |