diff options
Diffstat (limited to 'pretyping')
32 files changed, 957 insertions, 575 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a793e217d4..6370bd4f9a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -46,8 +46,10 @@ module NamedDecl = Context.Named.Declaration type pattern_matching_error = | BadPattern of constructor * constr | BadConstructor of constructor * inductive - | WrongNumargConstructor of constructor * int - | WrongNumargInductive of inductive * int + | WrongNumargConstructor of + {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int} + | WrongNumargInductive of + {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int} | UnusedClause of cases_pattern list | NonExhaustive of cases_pattern list | CannotInferPredicate of (constr * types) array @@ -65,11 +67,13 @@ let error_bad_constructor ?loc env cstr ind = raise_pattern_matching_error ?loc (env, Evd.empty, BadConstructor (cstr,ind)) -let error_wrong_numarg_constructor ?loc env c n = - raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargConstructor(c,n)) +let error_wrong_numarg_constructor ?loc env ~cstr ~expanded ~nargs ~expected_nassums ~expected_ndecls = + raise_pattern_matching_error ?loc (env, Evd.empty, + WrongNumargConstructor {cstr; expanded; nargs; expected_nassums; expected_ndecls}) -let error_wrong_numarg_inductive ?loc env c n = - raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,n)) +let error_wrong_numarg_inductive ?loc env ~ind ~expanded ~nargs ~expected_nassums ~expected_ndecls = + raise_pattern_matching_error ?loc (env, Evd.empty, + WrongNumargInductive {ind; expanded; nargs; expected_nassums; expected_ndecls}) let list_try_compile f l = let rec aux errors = function @@ -519,13 +523,18 @@ let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with (* Check the constructor has the right number of args *) let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in - if Int.equal (List.length args) nb_args_constr then pat + let nargs = List.length args in + if Int.equal nargs nb_args_constr then pat else try let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args) in DAst.make ?loc @@ PatCstr (cstr, args', alias) with NotAdjustable -> - error_wrong_numarg_constructor ?loc env cstr nb_args_constr + let nlet = List.count (function LocalDef _ -> true | _ -> false) ci.cs_args in + (* In practice, this is already checked at interning *) + error_wrong_numarg_constructor ?loc env ~cstr + (* as if not expanded: *) ~expanded:false ~nargs ~expected_nassums:nb_args_constr + ~expected_ndecls:(nb_args_constr + nlet) else (* Try to insert a coercion *) try @@ -1156,17 +1165,16 @@ let rec ungeneralize sigma n ng body = | LetIn (na,b,t,c) -> (* We traverse an alias *) mkLetIn (na,b,t,ungeneralize sigma (n+1) ng c) - | Case (ci,p,iv,c,brs) -> + | Case (ci,u,pms,p,iv,c,brs) -> (* We traverse a split *) let p = - let sign,p = decompose_lam_assum sigma p in + let (nas, p) = p in let sign2,p = decompose_prod_n_assum sigma ng p in - let p = prod_applist sigma p [mkRel (n+List.length sign+ng)] in - it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in - mkCase (ci,p,iv,c,Array.map2 (fun q c -> - let sign,b = decompose_lam_n_decls sigma q c in - it_mkLambda_or_LetIn (ungeneralize sigma (n+q) ng b) sign) - ci.ci_cstr_ndecls brs) + let p = prod_applist sigma p [mkRel (n+Array.length nas+ng)] in + nas, it_mkProd_or_LetIn p sign2 + in + let map (nas, br) = nas, ungeneralize sigma (n + Array.length nas) ng br in + mkCase (ci, u, pms, p, iv, c, Array.map map brs) | App (f,args) -> (* We traverse an inner generalization *) assert (isCase sigma f); @@ -1186,12 +1194,9 @@ let rec is_dependent_generalization sigma ng body = | LetIn (na,b,t,c) -> (* We traverse an alias *) is_dependent_generalization sigma ng c - | Case (ci,p,iv,c,brs) -> + | Case (ci,u,pms,p,iv,c,brs) -> (* We traverse a split *) - Array.exists2 (fun q c -> - let _,b = decompose_lam_n_decls sigma q c in - is_dependent_generalization sigma ng b) - ci.ci_cstr_ndecls brs + Array.exists (fun (_, b) -> is_dependent_generalization sigma ng b) brs | App (g,args) -> (* We traverse an inner generalization *) assert (isCase sigma g); @@ -1750,7 +1755,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = let good = List.filter (fun (_,u,_) -> is_conv_leq !!env sigma t u) subst in match good with | [] -> - map_constr_with_full_binders sigma (push_binder sigma) aux x t + map_constr_with_full_binders !!env sigma (push_binder sigma) aux x t | (_, _, u) :: _ -> (* u is in extenv *) let vl = List.map pi1 good in let ty = diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 9a986bc14c..ade1fbf3d3 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -23,17 +23,21 @@ open Evardefine type pattern_matching_error = | BadPattern of constructor * constr | BadConstructor of constructor * inductive - | WrongNumargConstructor of constructor * int - | WrongNumargInductive of inductive * int + | WrongNumargConstructor of + {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int} + | WrongNumargInductive of + {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int} | UnusedClause of cases_pattern list | NonExhaustive of cases_pattern list | CannotInferPredicate of (constr * types) array exception PatternMatchingError of env * evar_map * pattern_matching_error -val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> int -> 'a +val error_wrong_numarg_constructor : + ?loc:Loc.t -> env -> cstr:constructor -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a -val error_wrong_numarg_inductive : ?loc:Loc.t -> env -> inductive -> int -> 'a +val error_wrong_numarg_inductive : + ?loc:Loc.t -> env -> ind:inductive -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a val irrefutable : env -> cases_pattern -> bool diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 2661000a39..7930c3d634 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -76,8 +76,7 @@ type cbv_value = and cbv_stack = | TOP | APP of cbv_value array * cbv_stack - | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert - * case_info * cbv_value subs * cbv_stack + | CASE of Univ.Instance.t * constr array * case_return * case_branch array * Constr.case_invert * case_info * cbv_value subs * cbv_stack | PROJ of Projection.t * cbv_stack (* les vars pourraient etre des constr, @@ -111,15 +110,20 @@ let shift_value n v = * (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1})) * -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti) *) + +let rec mk_fix_subs make_body n env i = + if Int.equal i n then env + else mk_fix_subs make_body n (subs_cons (make_body i) env) (i + 1) + let contract_fixp env ((reci,i),(_,_,bds as bodies)) = let make_body j = FIXP(((reci,j),bodies), env, [||]) in let n = Array.length bds in - subs_cons(Array.init n make_body, env), bds.(i) + mk_fix_subs make_body n env 0, bds.(i) let contract_cofixp env (i,(_,_,bds as bodies)) = let make_body j = COFIXP((j,bodies), env, [||]) in let n = Array.length bds in - subs_cons(Array.init n make_body, env), bds.(i) + mk_fix_subs make_body n env 0, bds.(i) let make_constr_ref n k t = match k with @@ -138,7 +142,7 @@ let rec stack_concat stk1 stk2 = match stk1 with TOP -> stk2 | APP(v,stk1') -> APP(v,stack_concat stk1' stk2) - | CASE(c,b,iv,i,s,stk1') -> CASE(c,b,iv,i,s,stack_concat stk1' stk2) + | CASE(u,pms,c,b,iv,i,s,stk1') -> CASE(u,pms,c,b,iv,i,s,stack_concat stk1' stk2) | PROJ (p,stk1') -> PROJ (p,stack_concat stk1' stk2) (* merge stacks when there is no shifts in between *) @@ -352,9 +356,9 @@ let rec reify_stack t = function | TOP -> t | APP (args,st) -> reify_stack (mkApp(t,Array.map reify_value args)) st - | CASE (ty,br,iv,ci,env,st) -> + | CASE (u,pms,ty,br,iv,ci,env,st) -> reify_stack - (mkCase (ci, ty, iv, t, br)) + (mkCase (ci, u, pms, ty, iv, t,br)) st | PROJ (p, st) -> reify_stack (mkProj (p, t)) st @@ -401,6 +405,33 @@ let rec strip_app = function | APP (args,st) -> APP (args,strip_app st) | s -> TOP +let rec subs_consn v i n s = + if Int.equal i n then s + else subs_consn v (i + 1) n (subs_cons v.(i) s) + +(* TODO: share the common parts with EConstr *) +let expand_branch env u pms (ind, i) br = + let open Declarations in + let nas, _br = br.(i - 1) in + let (mib, mip) = Inductive.lookup_mind_specif env ind in + let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in + let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list pms) in + let subst = paramsubst @ Inductive.ind_subst (fst ind) mib u in + let (ctx, _) = mip.mind_nf_lc.(i - 1) in + let (ctx, _) = List.chop mip.mind_consnrealdecls.(i - 1) ctx in + Inductive.instantiate_context u subst nas ctx + +let cbv_subst_of_rel_context_instance mkclos sign args env = + let rec aux subst sign l = + let open Context.Rel.Declaration in + match sign, l with + | LocalAssum _ :: sign', a::args' -> aux (subs_cons a subst) sign' args' + | LocalDef (_,c,_)::sign', args' -> + aux (subs_cons (mkclos subst c) subst) sign' args' + | [], [] -> subst + | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.") + in aux env (List.rev sign) (Array.to_list args) + (* The main recursive functions * * Go under applications and cases/projections (pushed in the stack), @@ -420,7 +451,7 @@ let rec norm_head info env t stack = they could be computed when getting out of the stack *) let nargs = Array.map (cbv_stack_term info TOP env) args in norm_head info env head (stack_app nargs stack) - | Case (ci,p,iv,c,v) -> norm_head info env c (CASE(p,v,iv,ci,env,stack)) + | Case (ci,u,pms,p,iv,c,v) -> norm_head info env c (CASE(u,pms,p,v,iv,ci,env,stack)) | Cast (ct,_,_) -> norm_head info env ct stack | Proj (p, c) -> @@ -456,7 +487,7 @@ let rec norm_head info env t stack = (* New rule: for Cbv, Delta does not apply to locally bound variables or red_set info.reds fDELTA *) - let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in + let env' = subs_cons (cbv_stack_term info TOP env b) env in norm_head info env' c stack else (CBN(t,env), stack) (* Should we consider a commutative cut ? *) @@ -526,14 +557,14 @@ and cbv_stack_value info env = function when red_set info.reds fBETA -> let nargs = Array.length args in if nargs == nlams then - cbv_stack_term info stk (subs_cons(args,env)) b + cbv_stack_term info stk (subs_consn args 0 nargs env) b else if nlams < nargs then - let env' = subs_cons(Array.sub args 0 nlams, env) in + let env' = subs_consn args 0 nlams env in let eargs = Array.sub args nlams (nargs-nlams) in cbv_stack_term info (APP(eargs,stk)) env' b else let ctxt' = List.skipn nargs ctxt in - LAM(nlams-nargs,ctxt', b, subs_cons(args,env)) + LAM(nlams-nargs,ctxt', b, subs_consn args 0 nargs env) (* a Fix applied enough -> IOTA *) | (FIXP(fix,env,[||]), stk) @@ -548,16 +579,33 @@ and cbv_stack_value info env = function cbv_stack_term info stk envf redfix (* constructor in a Case -> IOTA *) - | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,iv,ci,env,stk))) + | (CONSTR(((sp,n),_),[||]), APP(args,CASE(u,pms,_p,br,iv,ci,env,stk))) when red_set info.reds fMATCH -> + let nargs = Array.length args - ci.ci_npar in let cargs = - Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in - cbv_stack_term info (stack_app cargs stk) env br.(n-1) + Array.sub args ci.ci_npar nargs in + let env = + if (Int.equal ci.ci_cstr_ndecls.(n - 1) ci.ci_cstr_nargs.(n - 1)) then (* no lets *) + subs_consn cargs 0 nargs env + else + let mkclos env c = cbv_stack_term info TOP env c in + let ctx = expand_branch info.env u pms (sp, n) br in + cbv_subst_of_rel_context_instance mkclos ctx cargs env + in + cbv_stack_term info stk env (snd br.(n-1)) (* constructor of arity 0 in a Case -> IOTA *) - | (CONSTR(((_,n),u),[||]), CASE(_,br,_,_,env,stk)) + | (CONSTR(((sp, n), _),[||]), CASE(u,pms,_,br,_,ci,env,stk)) when red_set info.reds fMATCH -> - cbv_stack_term info stk env br.(n-1) + let env = + if (Int.equal ci.ci_cstr_ndecls.(n - 1) ci.ci_cstr_nargs.(n - 1)) then (* no lets *) + env + else + let mkclos env c = cbv_stack_term info TOP env c in + let ctx = expand_branch info.env u pms (sp, n) br in + cbv_subst_of_rel_context_instance mkclos ctx [||] env + in + cbv_stack_term info stk env (snd br.(n-1)) (* constructor in a Projection -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,stk))) @@ -631,10 +679,31 @@ let rec apply_stack info t = function | TOP -> t | APP (args,st) -> apply_stack info (mkApp(t,Array.map (cbv_norm_value info) args)) st - | CASE (ty,br,iv,ci,env,st) -> + | CASE (u,pms,ty,br,iv,ci,env,st) -> + (* FIXME: Prevent this expansion by caching whether an inductive contains let-bindings *) + let (_, ty, _, _, br) = Inductive.expand_case info.env (ci, u, pms, ty, iv, mkProp, br) in + let ty = + let (_, mip) = Inductive.lookup_mind_specif info.env ci.ci_ind in + Term.decompose_lam_n_decls (mip.Declarations.mind_nrealdecls + 1) ty + in + let mk_br c n = Term.decompose_lam_n_decls n c in + let br = Array.map2 mk_br br ci.ci_cstr_ndecls in + let map_ctx (nas, c) = + let open Context.Rel.Declaration in + let fold decl e = match decl with + | LocalAssum _ -> subs_lift e + | LocalDef (_, b, _) -> + let b = cbv_stack_term info TOP e b in + (* The let-binding persists, so we have to shift *) + subs_shft (1, subs_cons b e) + in + let env = List.fold_right fold nas env in + let nas = Array.of_list (List.rev_map get_annot nas) in + (nas, cbv_norm_term info env c) + in apply_stack info - (mkCase (ci, cbv_norm_term info env ty, iv, t, - Array.map (cbv_norm_term info env) br)) + (mkCase (ci, u, Array.map (cbv_norm_term info env) pms, map_ctx ty, iv, t, + Array.map map_ctx br)) st | PROJ (p, st) -> apply_stack info (mkProj (p, t)) st diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 409f4c0f70..4d81678200 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -42,8 +42,7 @@ type cbv_value = and cbv_stack = | TOP | APP of cbv_value array * cbv_stack - | CASE of constr * constr array * (constr,Univ.Instance.t) case_invert - * case_info * cbv_value subs * cbv_stack + | CASE of Univ.Instance.t * constr array * case_return * case_branch array * Constr.case_invert * case_info * cbv_value subs * cbv_stack | PROJ of Projection.t * cbv_stack val shift_value : int -> cbv_value -> cbv_value diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index a3f1c0b004..c77feeafbb 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -351,7 +351,9 @@ let matches_core env sigma allow_bound_rels sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 - | PIf (a1,b1,b1'), Case (ci,_,_,a2,[|b2;b2'|]) -> + | PIf (a1,b1,b1'), Case (ci, u2, pms2, p2, iv, a2, ([|b2;b2'|] as br2)) -> + let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in + let b2, b2' = match br2 with [|b2; b2'|] -> b2, b2' | _ -> assert false in let ctx_b2,b2 = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(0) b2 in let ctx_b2',b2' = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(1) b2' in let n = Context.Rel.length ctx_b2 in @@ -367,7 +369,8 @@ let matches_core env sigma allow_bound_rels else raise PatternMatchingFailure - | PCase (ci1,p1,a1,br1), Case (ci2,p2,_,a2,br2) -> + | PCase (ci1, p1, a1, br1), Case (ci2, u2, pms2, p2, iv, a2, br2) -> + let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in let n2 = Array.length br2 in let () = match ci1.cip_ind with | None -> () @@ -504,12 +507,30 @@ let sub_match ?(closed=true) env sigma pat c = | [app';c] -> mk_ctx (mkApp (app',[|c|])) | _ -> assert false in try_aux [(env, app); (env, Array.last lc)] mk_ctx next - | Case (ci,hd,iv,c1,lc) -> + | Case (ci,u,pms,hd0,iv,c1,lc0) -> + let (mib, mip) = Inductive.lookup_mind_specif env ci.ci_ind in + let (_, hd, _, _, br) = expand_case env sigma (ci, u, pms, hd0, iv, c1, lc0) in + let hd = + let (ctx, hd) = decompose_lam_assum sigma hd in + (push_rel_context ctx env, hd) + in + let map i br = + let decls = mip.Declarations.mind_consnrealdecls.(i) in + let (ctx, c) = decompose_lam_n_decls sigma decls br in + (push_rel_context ctx env, c) + in + let lc = Array.to_list (Array.mapi map br) in let next_mk_ctx = function - | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,iv,c1,Array.of_list lc)) + | c1 :: rem -> + let pms, rem = List.chop (Array.length pms) rem in + let pms = Array.of_list pms in + let hd, lc = match rem with [] -> assert false | x :: l -> (x, l) in + let hd = (fst hd0, hd) in + let map_br (nas, _) br = (nas, br) in + mk_ctx (mkCase (ci,u,pms,hd,iv,c1,Array.map2 map_br lc0 (Array.of_list lc))) | _ -> assert false in - let sub = (env, c1) :: (env, hd) :: subargs env lc in + let sub = (env, c1) :: Array.fold_right (fun c accu -> (env, c) :: accu) pms (hd :: lc) in try_aux sub next_mk_ctx next | Fix (indx,(names,types,bodies as recdefs)) -> let nb_fix = Array.length types in @@ -528,10 +549,9 @@ let sub_match ?(closed=true) env sigma pat c = let sub = subargs env types @ subargs env' bodies in try_aux sub next_mk_ctx next | Proj (p,c') -> - begin try - let term = Retyping.expand_projection env sigma p c' [] in - aux env term mk_ctx next - with Retyping.RetypeError _ -> next () + begin match Retyping.expand_projection env sigma p c' [] with + | term -> aux env term mk_ctx next + | exception Retyping.RetypeError _ -> next () end | Array(u, t, def, ty) -> let next_mk_ctx = function diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 402a6f6ed3..bb5125f5ed 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +module CVars = Vars + open Pp open CErrors open Util @@ -33,6 +35,78 @@ type detyping_flags = { flg_isgoal : bool; } +(** Reimplementation of kernel case expansion functions in more lenient way *) +module RobustExpand : +sig +val return_clause : Environ.env -> Evd.evar_map -> Ind.t -> + EInstance.t -> EConstr.t array -> EConstr.case_return -> rel_context * EConstr.t +val branch : Environ.env -> Evd.evar_map -> Construct.t -> + EInstance.t -> EConstr.t array -> EConstr.case_branch -> rel_context * EConstr.t +end = +struct +open CVars +open Declarations +open Univ +open Constr + +let instantiate_context u subst nas ctx = + let rec instantiate i ctx = match ctx with + | [] -> [] + | LocalAssum (_, ty) :: ctx -> + let ctx = instantiate (pred i) ctx in + let ty = substnl subst i (subst_instance_constr u ty) in + LocalAssum (nas.(i), ty) :: ctx + | LocalDef (_, ty, bdy) :: ctx -> + let ctx = instantiate (pred i) ctx in + let ty = substnl subst i (subst_instance_constr u ty) in + let bdy = substnl subst i (subst_instance_constr u bdy) in + LocalDef (nas.(i), ty, bdy) :: ctx + in + let () = if not (Int.equal (Array.length nas) (List.length ctx)) then raise Exit in + instantiate (Array.length nas - 1) ctx + +let return_clause env sigma ind u params (nas, p) = + try + let u = EConstr.Unsafe.to_instance u in + let params = EConstr.Unsafe.to_constr_array params in + let () = if not @@ Environ.mem_mind (fst ind) env then raise Exit in + let mib = Environ.lookup_mind (fst ind) env in + let mip = mib.mind_packets.(snd ind) in + let paramdecl = subst_instance_context u mib.mind_params_ctxt in + let paramsubst = subst_of_rel_context_instance paramdecl (Array.to_list params) in + let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in + let self = + let args = Context.Rel.to_extended_vect mkRel 0 mip.mind_arity_ctxt in + let inst = Instance.of_array (Array.init (Instance.length u) Level.var) in + mkApp (mkIndU (ind, inst), args) + in + let realdecls = LocalAssum (Context.anonR, self) :: realdecls in + let realdecls = instantiate_context u paramsubst nas realdecls in + List.map EConstr.of_rel_decl realdecls, p + with e when CErrors.noncritical e -> + let dummy na = LocalAssum (na, EConstr.mkProp) in + List.rev (Array.map_to_list dummy nas), p + +let branch env sigma (ind, i) u params (nas, br) = + try + let u = EConstr.Unsafe.to_instance u in + let params = EConstr.Unsafe.to_constr_array params in + let () = if not @@ Environ.mem_mind (fst ind) env then raise Exit in + let mib = Environ.lookup_mind (fst ind) env in + let mip = mib.mind_packets.(snd ind) in + let paramdecl = subst_instance_context u mib.mind_params_ctxt in + let paramsubst = subst_of_rel_context_instance paramdecl (Array.to_list params) in + let subst = paramsubst @ Inductive.ind_subst (fst ind) mib u in + let (ctx, _) = mip.mind_nf_lc.(i - 1) in + let ctx, _ = List.chop mip.mind_consnrealdecls.(i - 1) ctx in + let ctx = instantiate_context u subst nas ctx in + List.map EConstr.of_rel_decl ctx, br + with e when CErrors.noncritical e -> + let dummy na = LocalAssum (na, EConstr.mkProp) in + List.rev (Array.map_to_list dummy nas), br + +end + module Avoid : sig type t @@ -241,16 +315,9 @@ let print_primproj_params = (* Auxiliary function for MutCase printing *) (* [computable] tries to tell if the predicate typing the result is inferable*) -let computable sigma p k = +let computable sigma (nas, ccl) = (* We first remove as many lambda as the arity, then we look - if it remains a lambda for a dependent elimination. This function - works for normal eta-expanded term. For non eta-expanded or - non-normal terms, it may affirm the pred is synthetisable - because of an undetected ultimate dependent variable in the second - clause, or else, it may affirm the pred non synthetisable - because of a non normal term in the fourth clause. - A solution could be to store, in the MutCase, the eta-expanded - normal form of pred to decide if it depends on its variables + if it remains a lambda for a dependent elimination. Lorsque le prédicat est dépendant de manière certaine, on ne déclare pas le prédicat synthétisable (même si la @@ -258,10 +325,7 @@ let computable sigma p k = sinon on perd la réciprocité de la synthèse (qui, lui, engendrera un prédicat non dépendant) *) - let sign,ccl = decompose_lam_assum sigma p in - Int.equal (Context.Rel.length sign) (k + 1) - && - noccur_between sigma 1 (k+1) ccl + noccur_between sigma 1 (Array.length nas) ccl let lookup_name_as_displayed env sigma t s = let rec lookup avoid n c = match EConstr.kind sigma c with @@ -393,30 +457,27 @@ let update_name sigma na ((_,(e,_)),c) = | _ -> na -let get_domain env sigma c = - let (_,t,_) = EConstr.destProd sigma (Reductionops.whd_all env sigma (Retyping.get_type_of env sigma c)) in - t - -let rec decomp_branch tags nal flags (avoid,env as e) sigma c = - match tags with - | [] -> (List.rev nal,(e,c)) - | b::tags -> +let decomp_branch flags e sigma (ctx, c) = + let n = List.length ctx in + let rec aux i nal (avoid, env as e) c = + if Int.equal i 0 then (List.rev nal,(e,c)) + else let decl, c, let_in = - match EConstr.kind sigma (strip_outer_cast sigma c), b with - | Lambda (na,t,c),false -> LocalAssum (na,t), c, true - | LetIn (na,b,t,c),true -> LocalDef (na,b,t), c, false - | _, false -> - let na = make_annot (Name default_dependent_ident) Sorts.Relevant (* dummy *) in - LocalAssum (na, get_domain (snd env) sigma c), applist (lift 1 c, [mkRel 1]), false - | _, true -> - let na = make_annot Anonymous Sorts.Relevant (* dummy *) in - LocalDef (na, mkProp (* dummy *), type1), lift 1 c, false + match EConstr.kind sigma c with + | Lambda (na,t,c) -> LocalAssum (na,t), c, true + | LetIn (na,b,t,c) -> LocalDef (na,b,t), c, false + | _ -> assert false in let na',avoid' = compute_name sigma ~let_in ~pattern:true flags avoid env (get_name decl) c in - decomp_branch tags (na'::nal) flags - (avoid', add_name (set_name na' decl) env) sigma c + aux (i - 1) (na'::nal) (avoid', add_name (set_name na' decl) env) c + in + aux n [] e (EConstr.it_mkLambda_or_LetIn c ctx) -let rec build_tree na isgoal e sigma ci cl = +let rec build_tree na isgoal e sigma (ci, u, pms, cl) = + let map i br = + RobustExpand.branch (snd (snd e)) sigma (ci.ci_ind, i + 1) u pms br + in + let cl = Array.mapi map cl in let mkpat n rhs pl = let na = update_name sigma na rhs in na, DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,na) in @@ -429,12 +490,12 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with | [] -> [Id.Set.empty,[],rhs] | na::nal -> match EConstr.kind sigma c with - | Case (ci,p,iv,c,cl) when + | Case (ci,u,pms,p,iv,c,cl) when eq_constr sigma c (mkRel (List.index Name.equal na (fst (snd e)))) && not (Int.equal (Array.length cl) 0) && (* don't contract if p dependent *) - computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> - let clauses = build_tree na isgoal e sigma ci cl in + computable sigma p (* FIXME: can do better *) -> + let clauses = build_tree na isgoal e sigma (ci, u, pms, cl) in List.flatten (List.map (fun (ids,pat,rhs) -> let lines = align_tree nal isgoal rhs sigma in @@ -447,7 +508,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with List.map (fun (ids,hd,rest) -> Nameops.Name.fold_right Id.Set.add na ids,pat::hd,rest) mat and contract_branch isgoal e sigma (cdn,mkpat,rhs) = - let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in + let nal,rhs = decomp_branch isgoal e sigma rhs in let mat = align_tree nal isgoal rhs sigma in List.map (fun (ids,hd,rhs) -> let na, pat = mkpat rhs hd in @@ -457,15 +518,10 @@ and contract_branch isgoal e sigma (cdn,mkpat,rhs) = (* Transform internal representation of pattern-matching into list of *) (* clauses *) -let is_nondep_branch sigma c l = - try - (* FIXME: do better using tags from l *) - let sign,ccl = decompose_lam_n_decls sigma (List.length l) c in - noccur_between sigma 1 (Context.Rel.length sign) ccl - with e when CErrors.noncritical e -> (* Not eta-expanded or not reduced *) - false +let is_nondep_branch sigma (nas, ccl) = + noccur_between sigma 1 (Array.length nas) ccl -let extract_nondep_branches test c b l = +let extract_nondep_branches b l = let rec strip l r = match DAst.get r, l with | r', [] -> r @@ -473,7 +529,7 @@ let extract_nondep_branches test c b l = | GLetIn (_,_,_,t), true::l -> strip l t (* FIXME: do we need adjustment? *) | _,_ -> assert false in - if test c l then Some (strip l b) else None + strip l b let it_destRLambda_or_LetIn_names l c = let rec aux l nal c = @@ -498,13 +554,14 @@ let it_destRLambda_or_LetIn_names l c = | _ -> DAst.make @@ GApp (c,[a])) in aux l [] c -let detype_case computable detype detype_eqns testdep avoid ci p iv c bl = +let detype_case computable detype detype_eqns avoid env sigma (ci, univs, params, p, iv, c, bl) = let synth_type = synthetize_type () in let tomatch = detype c in let tomatch = match iv with | NoInvert -> tomatch - | CaseInvert {univs;args} -> - let t = mkApp (mkIndU (ci.ci_ind,univs), args) in + | CaseInvert {indices} -> + (* XXX use holes instead of params? *) + let t = mkApp (mkIndU (ci.ci_ind,univs), Array.append params indices) in DAst.make @@ GCast (tomatch, CastConv (detype t)) in let alias, aliastyp, pred= @@ -512,6 +569,8 @@ let detype_case computable detype detype_eqns testdep avoid ci p iv c bl = then Anonymous, None, None else + let (ctx, p) = RobustExpand.return_clause (snd env) sigma ci.ci_ind univs params p in + let p = EConstr.it_mkLambda_or_LetIn p ctx in let p = detype p in let nl,typ = it_destRLambda_or_LetIn_names ci.ci_pp_info.ind_tags p in let n,typ = match DAst.get typ with @@ -540,21 +599,29 @@ let detype_case computable detype detype_eqns testdep avoid ci p iv c bl = let constagsl = ci.ci_pp_info.cstr_tags in match tag, aliastyp with | LetStyle, None -> + let map i br = + let (ctx, body) = RobustExpand.branch (snd env) sigma (ci.ci_ind, i + 1) univs params br in + EConstr.it_mkLambda_or_LetIn body ctx + in + let bl = Array.mapi map bl in let bl' = Array.map detype bl in let (nal,d) = it_destRLambda_or_LetIn_names constagsl.(0) bl'.(0) in GLetTuple (nal,(alias,pred),tomatch,d) | IfStyle, None -> - let bl' = Array.map detype bl in - let nondepbrs = - Array.map3 (extract_nondep_branches testdep) bl bl' constagsl in - if Array.for_all ((!=) None) nondepbrs then - GIf (tomatch,(alias,pred), - Option.get nondepbrs.(0),Option.get nondepbrs.(1)) + if Array.for_all (fun br -> is_nondep_branch sigma br) bl then + let map i br = + let ctx, body = RobustExpand.branch (snd env) sigma (ci.ci_ind, i + 1) univs params br in + EConstr.it_mkLambda_or_LetIn body ctx + in + let bl = Array.mapi map bl in + let bl' = Array.map detype bl in + let nondepbrs = Array.map2 extract_nondep_branches bl' constagsl in + GIf (tomatch,(alias,pred), nondepbrs.(0), nondepbrs.(1)) else - let eqnl = detype_eqns constructs constagsl bl in + let eqnl = detype_eqns constructs constagsl (ci, univs, params, bl) in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) | _ -> - let eqnl = detype_eqns constructs constagsl bl in + let eqnl = detype_eqns constructs constagsl (ci, univs, params, bl) in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) let rec share_names detype flags n l avoid env sigma c t = @@ -788,12 +855,12 @@ and detype_r d flags avoid env sigma t = GRef (GlobRef.IndRef ind_sp, detype_instance sigma u) | Construct (cstr_sp,u) -> GRef (GlobRef.ConstructRef cstr_sp, detype_instance sigma u) - | Case (ci,p,iv,c,bl) -> - let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in + | Case (ci,u,pms,p,iv,c,bl) -> + let comp = computable sigma p in + let case = (ci, u, pms, p, iv, c, bl) in detype_case comp (detype d flags avoid env sigma) - (detype_eqns d flags avoid env sigma ci comp) - (is_nondep_branch sigma) avoid - ci p iv c bl + (detype_eqns d flags avoid env sigma comp) + avoid env sigma case | Fix (nvn,recdef) -> detype_fix (detype d) flags avoid env sigma nvn recdef | CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef | Int i -> GInt i @@ -805,18 +872,21 @@ and detype_r d flags avoid env sigma t = let u = detype_instance sigma u in GArray(u, t, def, ty) -and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = +and detype_eqns d flags avoid env sigma computable constructs consnargsl bl = try if !Flags.raw_print || not (reverse_matching ()) then raise Exit; - let mat = build_tree Anonymous flags (avoid,env) sigma ci bl in + let mat = build_tree Anonymous flags (avoid,env) sigma bl in List.map (fun (ids,pat,((avoid,env),c)) -> CAst.make (Id.Set.elements ids,[pat],detype d flags avoid env sigma c)) mat with e when CErrors.noncritical e -> + let (ci, u, pms, bl) = bl in Array.to_list - (Array.map3 (detype_eqn d flags avoid env sigma) constructs consnargsl bl) + (Array.map3 (detype_eqn d flags avoid env sigma u pms) constructs consnargsl bl) -and detype_eqn d flags avoid env sigma constr construct_nargs branch = +and detype_eqn d flags avoid env sigma u pms constr construct_nargs br = + let ctx, body = RobustExpand.branch (snd env) sigma constr u pms br in + let branch = EConstr.it_mkLambda_or_LetIn body ctx in let make_pat decl avoid env b ids = if force_wildcard () && noccurn sigma 1 b then DAst.make @@ PatVar Anonymous,avoid,(add_name (set_name Anonymous decl) env),ids @@ -824,39 +894,24 @@ and detype_eqn d flags avoid env sigma constr construct_nargs branch = let na,avoid' = compute_name sigma ~let_in:false ~pattern:true flags avoid env (get_name decl) b in DAst.make (PatVar na),avoid',(add_name (set_name na decl) env),add_vname ids na in - let rec buildrec ids patlist avoid env l b = - match EConstr.kind sigma b, l with - | _, [] -> CAst.make @@ + let rec buildrec ids patlist avoid env n b = + if Int.equal n 0 then + CAst.make @@ (Id.Set.elements ids, [DAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], detype d flags avoid env sigma b) - | Lambda (x,t,b), false::l -> + else match EConstr.kind sigma b with + | Lambda (x,t,b) -> let pat,new_avoid,new_env,new_ids = make_pat (LocalAssum (x,t)) avoid env b ids in - buildrec new_ids (pat::patlist) new_avoid new_env l b + buildrec new_ids (pat::patlist) new_avoid new_env (pred n) b - | LetIn (x,b,t,b'), true::l -> + | LetIn (x,b,t,b') -> let pat,new_avoid,new_env,new_ids = make_pat (LocalDef (x,b,t)) avoid env b' ids in - buildrec new_ids (pat::patlist) new_avoid new_env l b' - - | Cast (c,_,_), l -> (* Oui, il y a parfois des cast *) - buildrec ids patlist avoid env l c - - | _, true::l -> - let pat = DAst.make @@ PatVar Anonymous in - buildrec ids (pat::patlist) avoid env l b - - | _, false::l -> - (* eta-expansion : n'arrivera plus lorsque tous les - termes seront construits à partir de la syntaxe Cases *) - (* nommage de la nouvelle variable *) - let new_b = applist (lift 1 b, [mkRel 1]) in - let typ = get_domain (snd env) sigma b in - let pat,new_avoid,new_env,new_ids = - make_pat (LocalAssum (make_annot Anonymous Sorts.Relevant (* dummy *),typ)) avoid env new_b ids in - buildrec new_ids (pat::patlist) new_avoid new_env l new_b + buildrec new_ids (pat::patlist) new_avoid new_env (pred n) b' + | _ -> assert false in - buildrec Id.Set.empty [] avoid env construct_nargs branch + buildrec Id.Set.empty [] avoid env (List.length ctx) branch and detype_binder d flags bk avoid env sigma decl c = let na = get_name decl in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d0b724b755..990e84e5a7 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 = @@ -205,7 +206,7 @@ let occur_rigidly flags env evd (evk,_) t = if rigid_normal_occ b' || rigid_normal_occ t' then Rigid true else Reducible | Rel _ | Var _ -> Reducible - | Case (_,_,_,c,_) -> + | Case (_,_,_,_,_,c,_) -> (match aux c with | Rigid b -> Rigid b | _ -> Reducible) @@ -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,52 @@ 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) + | Stack.Case (ci1,u1,pms1,t1,iv1,c1)::q1, Stack.Case (ci2,u2,pms2,t2,iv2,c2)::q2 -> + let dummy = mkProp in + let (_, t1, _, _, c1) = EConstr.expand_case env evd (ci1,u1,pms1,t1,iv1,dummy,c1) in + let (_, t2, _, _, c2) = EConstr.expand_case env evd (ci2,u2,pms2,t2,iv2,dummy,c2) in + 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 +403,54 @@ 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 -> + | Stack.Case (ci1,u1,pms1,t1,iv1,c1)::q1, Stack.Case (ci2,u2,pms2,t2,iv2,c2)::q2 -> + let dummy = mkProp in + let (_, t1, _, _, c1) = EConstr.expand_case env evd (ci1,u1,pms1,t1,iv1,dummy,c1) in + let (_, t2, _, _, c2) = EConstr.expand_case env evd (ci2,u2,pms2,t2,iv2,dummy,c2) in 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 +588,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 +634,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 +687,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 +696,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 +751,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 +772,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 +802,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 +814,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 +1024,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 +1081,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 +1179,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 @@ -1234,7 +1284,7 @@ let apply_on_subterm env evd fixed f test c t = if occur_evars !evdref !fixedref t then match EConstr.kind !evdref t with | Evar (ev, args) when Evar.Set.mem ev !fixedref -> t - | _ -> map_constr_with_binders_left_to_right !evdref + | _ -> map_constr_with_binders_left_to_right env !evdref (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t else @@ -1249,7 +1299,7 @@ let apply_on_subterm env evd fixed f test c t = evdref := evd'; t') else ( if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed"); - map_constr_with_binders_left_to_right !evdref + map_constr_with_binders_left_to_right env !evdref (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t)) in @@ -1339,7 +1389,7 @@ let thin_evars env sigma sign c = if not (Id.Set.mem id ctx) then raise (TypingFailed !sigma) else t | _ -> - map_constr_with_binders_left_to_right !sigma + map_constr_with_binders_left_to_right env !sigma (fun d (env,acc) -> (push_rel d env, acc+1)) applyrec (env,acc) t in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 44414aa6a0..cb3eef9df0 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -232,7 +232,7 @@ let recheck_applications unify flags env evdref t = else () in aux 0 fty | _ -> - iter_with_full_binders !evdref (fun d env -> push_rel d env) aux env t + iter_with_full_binders env !evdref (fun d env -> push_rel d env) aux env t in aux env t @@ -304,7 +304,7 @@ let noccur_evar env evd evk c = | LocalAssum _ -> () | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (EConstr.of_constr b))) | Proj (p,c) -> occur_rec true acc c - | _ -> iter_with_full_binders evd (fun rd (k,env) -> (succ k, push_rel rd env)) + | _ -> iter_with_full_binders env evd (fun rd (k,env) -> (succ k, push_rel rd env)) (occur_rec check_types) acc c in try occur_rec false (0,env) c; true with Occur -> false @@ -490,14 +490,14 @@ let expansion_of_var sigma aliases x = | Some a, _ -> (true, Alias.repr sigma a) | None, a :: _ -> (true, Some a) -let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t with +let rec expand_vars_in_term_using env sigma aliases t = match EConstr.kind sigma t with | Rel n -> of_alias (normalize_alias sigma aliases (RelAlias n)) | Var id -> of_alias (normalize_alias sigma aliases (VarAlias id)) | _ -> - let self aliases c = expand_vars_in_term_using sigma aliases c in - map_constr_with_full_binders sigma (extend_alias sigma) self aliases t + let self aliases c = expand_vars_in_term_using env sigma aliases c in + map_constr_with_full_binders env sigma (extend_alias sigma) self aliases t -let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env sigma) +let expand_vars_in_term env sigma = expand_vars_in_term_using env sigma (make_alias_map env sigma) let free_vars_and_rels_up_alias_expansion env sigma aliases c = let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in @@ -533,7 +533,7 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c = | Const _ | Ind _ | Construct _ -> acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2 | _ -> - iter_with_full_binders sigma + iter_with_full_binders env sigma (fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1)) frec (aliases,depth) c in @@ -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 @@ -1636,7 +1645,7 @@ let rec invert_definition unify flags choose imitate_defs let candidates = try let t = - map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) + map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1) imitate envk t in (* Less dependent solutions come last *) l@[t] @@ -1650,7 +1659,7 @@ let rec invert_definition unify flags choose imitate_defs evar'') | None -> (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *) - map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) + map_constr_with_full_binders env' !evdref (fun d (env,k) -> push_rel d env, k+1) imitate envk t in let rhs = whd_beta env evd rhs (* heuristic *) 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/find_subterm.ml b/pretyping/find_subterm.ml index bd717e2d1f..9f84b7683f 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -21,42 +21,15 @@ module NamedDecl = Context.Named.Declaration (** Processing occurrences *) -type occurrence_error = - | InvalidOccurrence of int list - | IncorrectInValueOccurrence of Id.t - -let explain_invalid_occurrence l = - let l = List.sort_uniquize Int.compare l in - str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ") - ++ prlist_with_sep spc int l ++ str "." - let explain_incorrect_in_value_occurrence id = Id.print id ++ str " has no value." -let explain_occurrence_error = function - | InvalidOccurrence l -> explain_invalid_occurrence l - | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id - -let error_occurrences_error e = - user_err (explain_occurrence_error e) - -let error_invalid_occurrence occ = - error_occurrences_error (InvalidOccurrence occ) - -let check_used_occurrences nbocc (nowhere_except_in,locs) = - let rest = List.filter (fun o -> o >= nbocc) locs in - match rest with - | [] -> () - | _ -> error_occurrences_error (InvalidOccurrence rest) - let proceed_with_occurrences f occs x = match occs with | NoOccurrences -> x | occs -> - let plocs = Locusops.convert_occs occs in - assert (List.for_all (fun x -> x >= 0) (snd plocs)); - let (nbocc,x) = f 1 x in - check_used_occurrences nbocc plocs; + let (occs,x) = f (Locusops.initialize_occurrence_counter occs) x in + Locusops.check_used_occurrences occs; x (** Applying a function over a named_declaration with an hypothesis @@ -70,7 +43,7 @@ let map_named_declaration_with_hyploc f hyploc acc decl = in match decl,hyploc with | LocalAssum (id,_), InHypValueOnly -> - error_occurrences_error (IncorrectInValueOccurrence id.Context.binder_name) + user_err (explain_incorrect_in_value_occurrence id.Context.binder_name) | LocalAssum (id,typ), _ -> let acc,typ = f acc typ in acc, LocalAssum (id,typ) | LocalDef (id,body,typ), InHypTypeOnly -> @@ -100,57 +73,57 @@ type 'a testing_function = { (b,l), b=true means no occurrence except the ones in l and b=false, means all occurrences except the ones in l *) -let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t = - let (nowhere_except_in,locs) = Locusops.convert_occs occs in - let maxocc = List.fold_right max locs 0 in - let pos = ref occ in +let replace_term_occ_gen_modulo env sigma occs like_first test bywhat cl occ t = + let count = ref (Locusops.initialize_occurrence_counter occs) in let nested = ref false in - let add_subst t subst = + let add_subst pos t subst = try test.testing_state <- test.merge_fun subst test.testing_state; - test.last_found <- Some ((cl,!pos),t) + test.last_found <- Some ((cl,pos),t) with NotUnifiable e when not like_first -> let lastpos = Option.get test.last_found in - raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in + raise (SubtermUnificationError (!nested,((cl,pos),t),lastpos,e)) in let rec substrec k t = - if nowhere_except_in && !pos > maxocc then t else + if Locusops.occurrences_done !count then t else try let subst = test.match_fun test.testing_state t in - if Locusops.is_selected !pos occs then + let selected, count' = Locusops.update_occurrence_counter !count in count := count'; + if selected then + let pos = Locusops.current_occurrence !count in (if !nested then begin (* in case it is nested but not later detected as unconvertible, as when matching "id _" in "id (id 0)" *) let lastpos = Option.get test.last_found in - raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,None)) + raise (SubtermUnificationError (!nested,((cl,pos),t),lastpos,None)) end; - add_subst t subst; incr pos; + add_subst pos t subst; (* Check nested matching subterms *) - if not (Locusops.is_all_occurrences occs) && occs != Locus.NoOccurrences then + if Locusops.more_specific_occurrences !count then begin nested := true; ignore (subst_below k t); nested := false end; (* Do the effective substitution *) Vars.lift k (bywhat ())) else - (incr pos; subst_below k t) + subst_below k t with NotUnifiable _ -> subst_below k t and subst_below k t = - map_constr_with_binders_left_to_right sigma (fun d k -> k+1) substrec k t + map_constr_with_binders_left_to_right env sigma (fun d k -> k+1) substrec k t in let t' = substrec 0 t in - (!pos, t') + (!count, t') -let replace_term_occ_modulo evd occs test bywhat t = +let replace_term_occ_modulo env evd occs test bywhat t = let occs',like_first = match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in proceed_with_occurrences - (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t + (replace_term_occ_gen_modulo env evd occs' like_first test bywhat None) occs' t -let replace_term_occ_decl_modulo evd occs test bywhat d = +let replace_term_occ_decl_modulo env evd occs test bywhat d = let (plocs,hyploc),like_first = match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in proceed_with_occurrences (map_named_declaration_with_hyploc - (replace_term_occ_gen_modulo evd plocs like_first test bywhat) + (replace_term_occ_gen_modulo env evd plocs like_first test bywhat) hyploc) plocs d @@ -172,7 +145,7 @@ let make_eq_univs_test env evd c = let subst_closed_term_occ env evd occs c t = let test = make_eq_univs_test env evd c in let bywhat () = mkRel 1 in - let t' = replace_term_occ_modulo evd occs test bywhat t in + let t' = replace_term_occ_modulo env evd occs test bywhat t in t', test.testing_state let subst_closed_term_occ_decl env evd occs c d = @@ -182,6 +155,6 @@ let subst_closed_term_occ_decl env evd occs c d = let bywhat () = mkRel 1 in proceed_with_occurrences (map_named_declaration_with_hyploc - (fun _ -> replace_term_occ_gen_modulo evd plocs like_first test bywhat None) + (fun _ -> replace_term_occ_gen_modulo env evd plocs like_first test bywhat None) hyploc) plocs d, test.testing_state diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index 436b730a88..c71cb207ab 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -43,13 +43,13 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function matching subterms at the indicated occurrences [occl] with [mk ()]; it turns a NotUnifiable exception raised by the testing function into a SubtermUnificationError. *) -val replace_term_occ_modulo : evar_map -> occurrences or_like_first -> +val replace_term_occ_modulo : env -> evar_map -> occurrences or_like_first -> 'a testing_function -> (unit -> constr) -> constr -> constr (** [replace_term_occ_decl_modulo] is similar to [replace_term_occ_modulo] but for a named_declaration. *) val replace_term_occ_decl_modulo : - evar_map -> + env -> evar_map -> (occurrences * hyp_location_flag) or_like_first -> 'a testing_function -> (unit -> constr) -> named_declaration -> named_declaration @@ -65,6 +65,3 @@ val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first -> val subst_closed_term_occ_decl : env -> evar_map -> (occurrences * hyp_location_flag) or_like_first -> constr -> named_declaration -> named_declaration * evar_map - -(** Miscellaneous *) -val error_invalid_occurrence : int list -> 'a diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index a957bc0fcd..9f93e5e6c1 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -137,7 +137,7 @@ type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g type 'a extended_glob_local_binder_r = | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g - | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option + | GLocalDef of Name.t * 'a glob_constr_g * 'a glob_constr_g option | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t diff --git a/pretyping/heads.ml b/pretyping/heads.ml index d1ac0862ed..f6e45613e1 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -32,31 +32,29 @@ type head_approximation = | FlexibleHead of int * int * int * bool (* [true] if a surrounding case *) | NotImmediatelyComputableHead -(* FIXME: maybe change interface here *) -let rec compute_head env = function - | EvalConstRef cst -> - let body = Environ.constant_opt_value_in env (cst,Univ.Instance.empty) in - (match body with - | None -> RigidHead (RigidParameter cst) - | Some c -> kind_of_head env c) - | EvalVarRef id -> - (match lookup_named id env with - | LocalDef (_,c,_) -> kind_of_head env c - | _ -> RigidHead RigidOther) +let rec compute_head_const env cst = + let body = Environ.constant_opt_value_in env (cst,Univ.Instance.empty) in + match body with + | None -> RigidHead (RigidParameter cst) + | Some c -> kind_of_head env c + +and compute_head_var env id = match lookup_named id env with +| LocalDef (_,c,_) -> kind_of_head env c +| _ -> RigidHead RigidOther and kind_of_head env t = let rec aux k l t b = match kind (Reduction.whd_betaiotazeta env t) with | Rel n when n > k -> NotImmediatelyComputableHead | Rel n -> FlexibleHead (k,k+1-n,List.length l,b) | Var id -> - (try on_subterm k l b (compute_head env (EvalVarRef id)) + (try on_subterm k l b (compute_head_var env id) with Not_found -> (* a goal variable *) match lookup_named id env with | LocalDef (_,c,_) -> aux k l c b | LocalAssum _ -> NotImmediatelyComputableHead) | Const (cst,_) -> - (try on_subterm k l b (compute_head env (EvalConstRef cst)) + (try on_subterm k l b (compute_head_const env cst) with Not_found -> CErrors.anomaly Pp.(str "constant not found in kind_of_head: " ++ @@ -78,7 +76,7 @@ and kind_of_head env t = | App (c,al) -> aux k (Array.to_list al @ l) c b | Proj (p,c) -> RigidHead RigidOther - | Case (_,_,_,c,_) -> aux k [] c true + | Case (_,_,_,_,_,c,_) -> aux k [] c true | Int _ | Float _ | Array _ -> ConstructorHead | Fix ((i,j),_) -> let n = i.(j) in diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 5ffd919312..dd7cf8abaa 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -122,12 +122,24 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = | None -> let iv = make_case_invert env (find_rectype env sigma (EConstr.of_constr (lift 1 depind))) ci in let iv = EConstr.Unsafe.to_case_invert iv in - mkCase (ci, lift ndepar p, iv, mkRel 1, Termops.rel_vect ndepar k) + let ncons = Array.length mip.mind_consnames in + let mk_branch i = + (* eta-expansion to please branch contraction *) + let ft = get_type (lookup_rel (ncons - i) env) in + (* we need that to get the generated names for the branch *) + let (ctx, _) = decompose_prod_assum ft in + let n = mkRel (List.length ctx + 1) in + let args = Context.Rel.to_extended_vect mkRel 0 ctx in + let br = it_mkLambda_or_LetIn (mkApp (n, args)) ctx in + lift (ndepar + ncons - i - 1) br + in + let br = Array.init ncons mk_branch in + mkCase (Inductive.contract_case env (ci, lift ndepar p, iv, mkRel 1, br)) | Some ps -> let term = mkApp (mkRel 2, - Array.map - (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in + Array.map + (fun p -> mkProj (Projection.make p true, mkRel 1)) ps) in if dep then let ty = mkApp (mkRel 3, [| mkRel 1 |]) in mkCast (term, DEFAULTcast, ty) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 23145b1629..d02b015604 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -245,6 +245,14 @@ let inductive_alldecls env (ind,u) = let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u) [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"] +let inductive_alltags env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + Context.Rel.to_tags mip.mind_arity_ctxt + +let constructor_alltags env (ind,j) = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + Context.Rel.to_tags (fst mip.mind_nf_lc.(j-1)) + let constructor_has_local_defs env (indsp,j) = let (mib,mip) = Inductive.lookup_mind_specif env indsp in let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in @@ -336,11 +344,7 @@ let get_projections = Environ.get_projections let make_case_invert env (IndType (((ind,u),params),indices)) ci = if Typeops.should_invert_case env ci - then - let univs = EConstr.EInstance.make u in - let params = Array.map_of_list EConstr.of_constr params in - let args = Array.append params (Array.of_list indices) in - CaseInvert {univs;args} + then CaseInvert {indices=Array.of_list indices} else NoInvert let make_case_or_project env sigma indt ci pred c branches = @@ -348,8 +352,7 @@ let make_case_or_project env sigma indt ci pred c branches = let IndType (((ind,_),_),_) = indt in let projs = get_projections env ind in match projs with - | None -> - mkCase (ci, pred, make_case_invert env indt ci, c, branches) + | None -> (mkCase (EConstr.contract_case env sigma (ci, pred, make_case_invert env indt ci, c, branches))) | Some ps -> assert(Array.length branches == 1); let na, ty, t = destLambda sigma pred in @@ -741,6 +744,6 @@ let control_only_guard env sigma c = in let rec iter env c = check_fix_cofix env c; - EConstr.iter_with_full_binders sigma EConstr.push_rel iter env c + EConstr.iter_with_full_binders env sigma EConstr.push_rel iter env c in iter env c diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1e2bba9f73..8e83814fa0 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -138,6 +138,10 @@ val constructor_nrealdecls : env -> constructor -> int val constructor_nrealdecls_env : env -> constructor -> int [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"] +(** @return tags of all decls: true = assumption, false = letin *) +val inductive_alltags : env -> inductive -> bool list +val constructor_alltags : env -> constructor -> bool list + (** Is there local defs in params or args ? *) val constructor_has_local_defs : env -> constructor -> bool val inductive_has_local_defs : env -> inductive -> bool @@ -209,7 +213,7 @@ val make_case_or_project : (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr val make_case_invert : env -> inductive_type -> case_info - -> (EConstr.constr,EConstr.EInstance.t) case_invert + -> EConstr.case_invert (*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 86352eb79a..256d61a32b 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Util open Locus (** Utilities on or_var *) @@ -27,12 +28,43 @@ let occurrences_map f = function if l' = [] then AllOccurrences else AllOccurrencesBut l' | (NoOccurrences|AllOccurrences|AtLeastOneOccurrence) as o -> o -let convert_occs = function - | AtLeastOneOccurrence -> (false,[]) - | AllOccurrences -> (false,[]) - | AllOccurrencesBut l -> (false,l) - | NoOccurrences -> (true,[]) - | OnlyOccurrences l -> (true,l) +type occurrences_count = {current: int; remaining: int list; where: (bool * int)} + +let error_invalid_occurrence l = + CErrors.user_err Pp.(str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ") + ++ prlist_with_sep spc int l ++ str ".") + +let initialize_occurrence_counter occs = + let (nowhere_except_in,occs) = + match occs with + | AtLeastOneOccurrence -> (false,[]) + | AllOccurrences -> (false,[]) + | AllOccurrencesBut l -> (false,List.sort_uniquize Int.compare l) + | NoOccurrences -> (true,[]) + | OnlyOccurrences l -> (true,List.sort_uniquize Int.compare l) in + let max = + match occs with + | n::_ when n <= 0 -> error_invalid_occurrence [n] + | [] -> 0 + | _ -> Util.List.last occs in + {current = 0; remaining = occs; where = (nowhere_except_in,max)} + +let update_occurrence_counter {current; remaining; where = (nowhere_except_in,_ as where)} = + let current = succ current in + match remaining with + | occ::remaining when Int.equal current occ -> (nowhere_except_in,{current;remaining;where}) + | _ -> (not nowhere_except_in,{current;remaining;where}) + +let check_used_occurrences {remaining} = + if not (Util.List.is_empty remaining) then error_invalid_occurrence remaining + +let occurrences_done {current; where = (nowhere_except_in,max)} = + nowhere_except_in && current > max + +let current_occurrence {current} = current + +let more_specific_occurrences {current; where = (_,max)} = + current <= max let is_selected occ = function | AtLeastOneOccurrence -> true diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index 911ccc1a38..748bfbc252 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -20,13 +20,44 @@ val or_var_map : ('a -> 'b) -> 'a or_var -> 'b or_var val occurrences_map : ('a list -> 'b list) -> 'a occurrences_gen -> 'b occurrences_gen -(** From occurrences to a list of positions (or complement of positions) *) -val convert_occs : occurrences -> bool * int list +(** {6 Counting occurrences} *) + +type occurrences_count + (** A counter of occurrences associated to a list of occurrences *) + +(** Three basic functions to initialize, count, and conclude a loop + browsing over subterms *) + +val initialize_occurrence_counter : occurrences -> occurrences_count + (** Initialize an occurrence_counter *) + +val update_occurrence_counter : occurrences_count -> bool * occurrences_count + (** Increase the occurrence counter by one and tell if the current occurrence is selected *) + +val check_used_occurrences : occurrences_count -> unit + (** Increase the occurrence counter and tell if the current occurrence is selected *) + +(** Auxiliary functions about occurrence counters *) + +val current_occurrence : occurrences_count -> int + (** Tell the value of the current occurrence *) + +val occurrences_done : occurrences_count -> bool + (** Tell if there are no more occurrences to select and if the loop + can be shortcut *) + +val more_specific_occurrences : occurrences_count -> bool + (** Tell if there are no more occurrences to select (or unselect) + and if an inner loop can be shortcut *) + +(** {6 Miscellaneous} *) val is_selected : int -> occurrences -> bool val is_all_occurrences : 'a occurrences_gen -> bool +val error_invalid_occurrence : int list -> 'a + (** Usual clauses *) val allHypsAndConcl : 'a clause_expr diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index d06d6e01d1..92e412a537 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -320,13 +320,13 @@ and nf_atom_type env sigma atom = | Acase(ans,accu,p,bs) -> let a,ta = nf_accu_type env sigma accu in let ((mind,_),u as ind),allargs = find_rectype_a env ta in - let iv = if Typeops.should_invert_case env ans.asw_ci then - CaseInvert {univs=u; args=allargs} - else NoInvert - in let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in let nparams = mib.mind_nparams in let params,realargs = Array.chop nparams allargs in + let iv = if Typeops.should_invert_case env ans.asw_ci then + CaseInvert {indices=realargs} + else NoInvert + in let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = hnf_prod_applist_assum env nparamdecls @@ -343,7 +343,8 @@ and nf_atom_type env sigma atom = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs a in - mkCase(ans.asw_ci, p, iv, a, branchs), tcase + let ci = ans.asw_ci in + mkCase (Inductive.contract_case env (ci, p, iv, a, branchs)), tcase | Afix(tt,ft,rp,s) -> let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in let tt = Array.map fst tt and rt = Array.map snd tt in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b259945d9e..47097a0e32 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -202,7 +202,8 @@ let pattern_of_constr env sigma t = | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> PMeta None) - | Case (ci,p,_,a,br) -> + | Case (ci, u, pms, p, iv, a, br) -> + let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p, iv, a, br) in let cip = { cip_style = ci.ci_pp_info.style; cip_ind = Some ci.ci_ind; @@ -213,7 +214,7 @@ let pattern_of_constr env sigma t = (i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c) in PCase (cip, pattern_of_constr env p, pattern_of_constr env a, - Array.to_list (Array.mapi branch_of_constr br)) + Array.to_list (Array.mapi branch_of_constr br)) | Fix (lni,(lna,tl,bl)) -> let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in let env' = Array.fold_left2 push env lna tl in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9dbded75ba..e86a8a28c9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1043,7 +1043,7 @@ struct if not record then let f = it_mkLambda_or_LetIn f fsign in let ci = make_case_info !!env (ind_of_ind_type indt) rci LetStyle in - mkCase (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|]) + mkCase (EConstr.contract_case !!env sigma (ci, p, make_case_invert !!env indt ci, cj.uj_val,[|f|])) else it_mkLambda_or_LetIn f fsign in (* Make dependencies from arity signature impossible *) @@ -1159,7 +1159,7 @@ struct let pred = nf_evar sigma pred in let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val pred in let ci = make_case_info !!env (fst ind) rci IfStyle in - mkCase (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|]) + mkCase (EConstr.contract_case !!env sigma (ci, pred, make_case_invert !!env indty ci, cj.uj_val, [|b1;b2|])) in let cj = { uj_val = v; uj_type = p } in discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma cj tycon diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index b6e44265ae..aa862a912e 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -323,23 +323,32 @@ let check_and_decompose_canonical_structure env sigma ref = let lookup_canonical_conversion env (proj,pat) = assoc_pat env pat (GlobRef.Map.find proj !object_table) -let decompose_projection sigma c args = +let rec get_nth n = function +| [] -> raise Not_found +| arg :: args -> + let len = Array.length arg in + if n < len then arg.(n) + else get_nth (n - len) args + +let rec decompose_projection sigma c args = match EConstr.kind sigma c with + | Meta mv -> decompose_projection sigma (Evd.meta_value sigma mv) args + | Cast (c, _, _) -> decompose_projection sigma c args + | App (c, arg) -> decompose_projection sigma c (arg :: args) | Const (c, u) -> let n = find_projection_nparams (GlobRef.ConstRef c) in (* Check if there is some canonical projection attached to this structure *) let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in - let arg = Stack.nth args n in - arg + get_nth n args | Proj (p, c) -> let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in c | _ -> raise Not_found -let is_open_canonical_projection env sigma (c,args) = +let is_open_canonical_projection env sigma c = let open EConstr in try - let arg = decompose_projection sigma c args in + let arg = decompose_projection sigma c [] in try let arg = whd_all env sigma arg in let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 5b8dc8184a..83927085e9 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -94,7 +94,7 @@ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> cs -> unit val subst_canonical_structure : Mod_subst.substitution -> cs -> cs val is_open_canonical_projection : - Environ.env -> Evd.evar_map -> Reductionops.state -> bool + Environ.env -> Evd.evar_map -> EConstr.t -> bool val canonical_projections : unit -> ((GlobRef.t * cs_pattern) * obj_typ) list diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3352bfce38..3da75f67b9 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -177,9 +177,12 @@ sig type 'a app_node val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t + type 'a case_stk = + case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array + type 'a member = | App of 'a app_node - | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array + | Case of 'a case_stk | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red @@ -194,6 +197,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 +218,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) = @@ -229,9 +233,12 @@ struct ) + type 'a case_stk = + case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array + type 'a member = | App of 'a app_node - | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array + | Case of 'a case_stk | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red @@ -244,9 +251,9 @@ struct let pr_c x = hov 1 (pr_c x) in match member with | App app -> str "ZApp" ++ pr_app_node pr_c app - | Case (_,_,_,br) -> + | Case (_,_,_,_,_,br) -> str "ZCase(" ++ - prvect_with_sep (pr_bar) pr_c br + prvect_with_sep (pr_bar) (fun (_, c) -> pr_c c) br ++ str ")" | Proj p -> str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")" @@ -267,12 +274,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 = @@ -285,7 +290,7 @@ struct ([],[]) -> Int.equal bal 0 | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2 | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 - | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> + | (Case _ :: s1, Case _::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Proj (p)::s1, Proj(p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 @@ -293,7 +298,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 @@ -305,8 +310,9 @@ struct let t1,l1 = decomp_node_last n1 q1 in let t2,l2 = decomp_node_last n2 q2 in aux (f o t1 t2) l1 l2 - | Case (_,t1,_,a1) :: q1, Case (_,t2,_,a2) :: q2 -> - aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2 + | Case ((_,_,pms1,(_, t1),_,a1)) :: q1, Case ((_,_,pms2, (_, t2),_,a2)) :: q2 -> + let f' o (_, t1) (_, t2) = f o t1 t2 in + aux (Array.fold_left2 f' (f (Array.fold_left2 f o pms1 pms2) t1 t2) a1 a2) q1 q2 | Proj (p1) :: q1, Proj (p2) :: q2 -> aux o q1 q2 | Fix ((_,(_,a1,b1)),s1) :: q1, Fix ((_,(_,a2,b2)),s2) :: q2 -> @@ -321,8 +327,8 @@ struct | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) - | Case (info,ty,iv,br) -> - Case (info, f ty, map_invert f iv, Array.map f br) + | Case (info,u,pms,ty,iv,br) -> + Case (info, u, Array.map f pms, on_snd f ty, iv, Array.map (on_snd f) br) | Fix ((r,(na,ty,bo)),arg) -> Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg) | Primitive (p,c,args,kargs) -> @@ -334,29 +340,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 +381,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 +393,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 @@ -404,7 +415,7 @@ struct then a else Array.sub a i (j - i + 1) in zip (mkApp (f, a'), s) - | f, (Case (ci,rt,iv,br)::s) -> zip (mkCase (ci,rt,iv,f,br), s) + | f, (Case (ci,u,pms,rt,iv,br)::s) -> zip (mkCase (ci,u,pms,rt,iv,f,br), s) | f, (Fix (fix,st)::s) -> zip (mkFix fix, st @ (append_app [|f|] s)) | f, (Proj (p)::s) -> zip (mkProj (p,f),s) @@ -465,13 +476,13 @@ let strong_with_flags whdfun flags env sigma t = | d -> d in push_rel d env in let rec strongrec env t = - map_constr_with_full_binders sigma + map_constr_with_full_binders env sigma push_rel_check_zeta strongrec env (whdfun flags env sigma t) in strongrec env t let strong whdfun env sigma t = let rec strongrec env t = - map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in + map_constr_with_full_binders env sigma push_rel strongrec env (whdfun env sigma t) in strongrec env t (*************************************) @@ -698,6 +709,20 @@ let debug_RAKAM = ~key:["Debug";"RAKAM"] ~value:false +let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) = + let args = Stack.tail ci.ci_npar args in + let args = Option.get (Stack.list_of_app_stack args) in + let br = lf.(i - 1) in + if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then + (* No let-bindings *) + let subst = List.rev args in + Vars.substl subst (snd br) + else + (* For backwards compat with unification, we do not reduce the let-bindings + upfront. *) + let ctx = expand_branch env sigma u pms (ind, i) br in + applist (it_mkLambda_or_LetIn (snd br) ctx, args) + let rec whd_state_gen flags env sigma = let open Context.Named.Declaration in let rec whrec (x, stack) : state = @@ -781,8 +806,8 @@ let rec whd_state_gen flags env sigma = | _ -> fold ()) | _ -> fold ()) - | Case (ci,p,iv,d,lf) -> - whrec (d, Stack.Case (ci,p,iv,lf) :: stack) + | Case (ci,u,pms,p,iv,d,lf) -> + whrec (d, Stack.Case (ci,u,pms,p,iv,lf) :: stack) | Fix ((ri,n),_ as f) -> (match Stack.strip_n_app ri.(n) stack with @@ -790,13 +815,14 @@ let rec whd_state_gen flags env sigma = |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,bef)::s')) - | Construct ((ind,c),u) -> + | Construct (cstr ,u) -> let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, _, lf)::s') when use_match -> - whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') + |args, (Stack.Case case::s') when use_match -> + let r = apply_branch env sigma cstr args case in + whrec (r, s') |args, (Stack.Proj (p)::s') when use_match -> whrec (Stack.nth args (Projection.npars p + Projection.arg p), s') |args, (Stack.Fix (f,s')::s'') when use_fix -> @@ -846,7 +872,7 @@ let rec whd_state_gen flags env sigma = whrec (** reduction machine without global env and refold machinery *) -let local_whd_state_gen flags _env sigma = +let local_whd_state_gen flags env sigma = let rec whrec (x, stack) = let c0 = EConstr.kind sigma x in let s = (EConstr.of_kind c0, stack) in @@ -878,8 +904,8 @@ let local_whd_state_gen flags _env sigma = | Proj (p,c) when CClosure.RedFlags.red_projection flags p -> (whrec (c, Stack.Proj (p) :: stack)) - | Case (ci,p,iv,d,lf) -> - whrec (d, Stack.Case (ci,p,iv,lf) :: stack) + | Case (ci,u,pms,p,iv,d,lf) -> + whrec (d, Stack.Case (ci,u,pms,p,iv,lf) :: stack) | Fix ((ri,n),_ as f) -> (match Stack.strip_n_app ri.(n) stack with @@ -892,13 +918,14 @@ let local_whd_state_gen flags _env sigma = Some c -> whrec (c,stack) | None -> s) - | Construct ((ind,c),u) -> + | Construct (cstr, u) -> let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, _, lf)::s') when use_match -> - whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') + |args, (Stack.Case case :: s') when use_match -> + let r = apply_branch env sigma cstr args case in + whrec (r, s') |args, (Stack.Proj (p) :: s') when use_match -> whrec (Stack.nth args (Projection.npars p + Projection.arg p), s') |args, (Stack.Fix (f,s')::s'') when use_fix -> @@ -930,14 +957,6 @@ let stack_red_of_state_red f = let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in f -(* Drops the Cst_stack *) -let iterate_whd_gen flags env sigma s = - let rec aux t = - let (hd,sk) = whd_state_gen flags env sigma (t,Stack.empty) in - let whd_sk = Stack.map aux sk in - Stack.zip sigma (hd,whd_sk) - in aux s - let red_of_state_red f env sigma x = Stack.zip sigma (f env sigma (x,Stack.empty)) @@ -1192,11 +1211,15 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 = let default_plain_instance_ident = Id.of_string "H" +type subst_fun = { sfun : metavariable -> EConstr.t } + (* Try to replace all metas. Does not replace metas in the metas' values * Differs from (strong whd_meta). *) -let plain_instance sigma s c = +let plain_instance sigma s c = match s with +| None -> c +| Some s -> let rec irec n u = match EConstr.kind sigma u with - | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u) + | Meta p -> (try lift n (s.sfun p) with Not_found -> u) | App (f,l) when isCast sigma f -> let (f,_,t) = destCast sigma f in let l' = Array.Fun1.Smart.map irec n l in @@ -1205,7 +1228,7 @@ let plain_instance sigma s c = (* Don't flatten application nodes: this is used to extract a proof-term from a proof-tree and we want to keep the structure of the proof-tree *) - (try let g = Metamap.find p s in + (try let g = s.sfun p in match EConstr.kind sigma g with | App _ -> let l' = Array.Fun1.Smart.map lift 1 l' in @@ -1216,12 +1239,11 @@ let plain_instance sigma s c = with Not_found -> mkApp (f,l')) | _ -> mkApp (irec n f,l')) | Cast (m,_,_) when isMeta sigma m -> - (try lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u) + (try lift n (s.sfun (destMeta sigma m)) with Not_found -> u) | _ -> map_with_binders sigma succ irec n u in - if Metamap.is_empty s then c - else irec 0 c + irec 0 c (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota] has (unfortunately) different subtle side effects: @@ -1423,23 +1445,41 @@ let is_arity env sigma c = (*************************************) (* Metas *) -let meta_value env evd mv = - let rec valrec mv = - match meta_opt_fvalue evd mv with - | Some (b,_) -> - let metas = Metamap.bind valrec b.freemetas in - instance env evd metas b.rebus - | None -> mkMeta mv +type meta_instance_subst = { + sigma : Evd.evar_map; + mutable cache : EConstr.t Metamap.t; +} + +let create_meta_instance_subst sigma = { + sigma; + cache = Metamap.empty; +} + +let eval_subst env subst = + let rec ans mv = + try Metamap.find mv subst.cache + with Not_found -> + match meta_opt_fvalue subst.sigma mv with + | None -> mkMeta mv + | Some (b, _) -> + let metas = + if Metaset.is_empty b.freemetas then None + else Some { sfun = ans } + in + let res = instance env subst.sigma metas b.rebus in + let () = subst.cache <- Metamap.add mv res subst.cache in + res in - valrec mv + { sfun = ans } -let meta_instance env sigma b = +let meta_instance env subst b = let fm = b.freemetas in if Metaset.is_empty fm then b.rebus else - let c_sigma = Metamap.bind (fun mv -> meta_value env sigma mv) fm in - instance env sigma c_sigma b.rebus + let sfun = eval_subst env subst in + instance env subst.sigma (Some sfun) b.rebus let nf_meta env sigma c = + let sigma = create_meta_instance_subst sigma in let cl = mk_freelisted c in meta_instance env sigma { cl with rebus = cl.rebus } diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index d404a7e414..59bc4a8b72 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -57,9 +57,12 @@ module Stack : sig val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t + type 'a case_stk = + case_info * EInstance.t * 'a array * 'a pcase_return * 'a pcase_invert * 'a pcase_branch array + type 'a member = | App of 'a app_node - | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array + | Case of 'a case_stk | Proj of Projection.t | Fix of ('a, 'a) pfixpoint * 'a t | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red @@ -69,10 +72,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,30 +86,56 @@ 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 (************************************************************************) -type state = constr * constr Stack.t - type reduction_function = env -> evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr @@ -115,11 +143,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -type state_reduction_function = - env -> evar_map -> state -> state - -val pr_state : env -> evar_map -> state -> Pp.t - (** {6 Reduction Function Operators } *) val strong_with_flags : @@ -127,12 +150,6 @@ val strong_with_flags : (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function -val whd_state_gen : - CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state - -val iterate_whd_gen : CClosure.RedFlags.reds -> - Environ.env -> Evd.evar_map -> constr -> constr - (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function @@ -166,24 +183,13 @@ val whd_all_stack : stack_reduction_function val whd_allnolet_stack : stack_reduction_function val whd_betalet_stack : stack_reduction_function -val whd_nored_state : state_reduction_function -val whd_beta_state : state_reduction_function -val whd_betaiota_state : state_reduction_function -val whd_betaiotazeta_state : state_reduction_function -val whd_all_state : state_reduction_function -val whd_allnolet_state : state_reduction_function -val whd_betalet_state : state_reduction_function - (** {6 Head normal forms } *) val whd_delta_stack : stack_reduction_function -val whd_delta_state : state_reduction_function val whd_delta : reduction_function val whd_betadeltazeta_stack : stack_reduction_function -val whd_betadeltazeta_state : state_reduction_function val whd_betadeltazeta : reduction_function val whd_zeta_stack : stack_reduction_function -val whd_zeta_state : state_reduction_function val whd_zeta : reduction_function val shrink_eta : Environ.env -> constr -> constr @@ -269,11 +275,24 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t -> (** {6 Heuristic for Conversion with Evar } *) +type state = constr * constr Stack.t + +type state_reduction_function = + env -> evar_map -> state -> state + +val pr_state : env -> evar_map -> state -> Pp.t + +val whd_nored_state : state_reduction_function + val whd_betaiota_deltazeta_for_iota_state : - TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state + TransparentState.t -> state_reduction_function (** {6 Meta-related reduction functions } *) -val meta_instance : env -> evar_map -> constr freelisted -> constr +type meta_instance_subst + +val create_meta_instance_subst : Evd.evar_map -> meta_instance_subst + +val meta_instance : env -> meta_instance_subst -> constr freelisted -> constr val nf_meta : env -> evar_map -> constr -> constr exception AnomalyInConversion of exn diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 34bcd0982c..064990f6bf 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -129,7 +129,8 @@ let retype ?(polyprop=true) sigma = | Evar ev -> existential_type sigma ev | Ind (ind, u) -> EConstr.of_constr (rename_type_of_inductive env (ind, EInstance.kind sigma u)) | Construct (cstr, u) -> EConstr.of_constr (rename_type_of_constructor env (cstr, EInstance.kind sigma u)) - | Case (_,p,_iv,c,lf) -> + | Case (ci,u,pms,p,iv,c,lf) -> + let (_,p,iv,c,lf) = EConstr.expand_case env sigma (ci,u,pms,p,iv,c,lf) in let Inductiveops.IndType(indf,realargs) = let t = type_of env c in try Inductiveops.find_rectype env sigma t @@ -309,7 +310,7 @@ let relevance_of_term env sigma c = | Const (c,_) -> Relevanceops.relevance_of_constant env c | Ind _ -> Sorts.Relevant | Construct (c,_) -> Relevanceops.relevance_of_constructor env c - | Case (ci, _, _, _, _) -> ci.ci_relevance + | Case (ci, _, _, _, _, _, _) -> ci.ci_relevance | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance | Proj (p, _) -> Relevanceops.relevance_of_projection env p diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 9cf7119709..01819a650b 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -43,6 +43,25 @@ exception ReductionTacticError of reduction_tactic_error exception Elimconst exception Redelimination +type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t + +(* Better to have it here that in closure, since used in grammar.cma *) +let eq_egr e1 e2 = match e1, e2 with + EvalConstRef con1, EvalConstRef con2 -> Constant.CanOrd.equal con1 con2 + | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 + | _, _ -> false + +(* Here the semantics is completely unclear. + What does "Hint Unfold t" means when "t" is a parameter? + Does the user mean "Unfold X.t" or does she mean "Unfold y" + where X.t is later on instantiated with y? I choose the first + interpretation (i.e. an evaluable reference is never expanded). *) +let subst_evaluable_reference subst = function + | EvalVarRef id -> EvalVarRef id + | EvalConstRef kn -> EvalConstRef (Mod_subst.subst_constant subst kn) + let error_not_evaluable r = user_err ~hdr:"error_not_evaluable" (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ @@ -277,8 +296,8 @@ let compute_consteval_direct env sigma ref = | Fix fix when not onlyproj -> (try check_fix_reversibility sigma labs l fix with Elimconst -> NotAnElimination) - | Case (_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n - | Case (_,_,_,d,_) -> srec env n labs true d + | Case (_,_,_,_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n + | Case (_,_,_,_,_,d,_) -> srec env n labs true d | Proj (p, d) when isRel sigma d -> EliminationProj n | _ -> NotAnElimination in @@ -459,29 +478,36 @@ let contract_cofix_use_function env sigma f sigma (nf_beta env sigma bodies.(bodynum)) type 'a miota_args = { - mP : constr; (** the result type *) + mU : EInstance.t; (* Universe instance of the return clause *) + mParams : constr array; (* Parameters of the inductive *) + mP : case_return; (* the result type *) mconstr : constr; (** the constructor *) mci : case_info; (** special info to re-build pattern *) mcargs : 'a list; (** the constructor's arguments *) - mlf : 'a array } (** the branch code vector *) + mlf : 'a pcase_branch array } (** the branch code vector *) -let reduce_mind_case sigma mia = +let reduce_mind_case env sigma mia = match EConstr.kind sigma mia.mconstr with - | Construct ((ind_sp,i),u) -> -(* let ncargs = (fst mia.mci).(i-1) in*) + | Construct ((_, i as cstr), u) -> let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in - applist (mia.mlf.(i-1),real_cargs) + let br = mia.mlf.(i - 1) in + let ctx = EConstr.expand_branch env sigma mia.mU mia.mParams cstr br in + let br = it_mkLambda_or_LetIn (snd br) ctx in + applist (br, real_cargs) | CoFix cofix -> let cofix_def = contract_cofix sigma cofix in (* XXX Is NoInvert OK here? *) - mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) + mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false let reduce_mind_case_use_function func env sigma mia = match EConstr.kind sigma mia.mconstr with - | Construct ((ind_sp,i),u) -> + | Construct ((_, i as cstr),u) -> let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in - applist (mia.mlf.(i-1), real_cargs) + let br = mia.mlf.(i - 1) in + let ctx = EConstr.expand_branch env sigma mia.mU mia.mParams cstr br in + let br = it_mkLambda_or_LetIn (snd br) ctx in + applist (br, real_cargs) | CoFix (bodynum,(names,_,_) as cofix) -> let build_cofix_name = if isConst sigma func then @@ -507,8 +533,7 @@ let reduce_mind_case_use_function func env sigma mia = fun _ -> None in let cofix_def = contract_cofix_use_function env sigma build_cofix_name cofix in - (* Is NoInvert OK here? *) - mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) + mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false @@ -709,9 +734,9 @@ and whd_simpl_stack env sigma = | LetIn (n,b,t,c) -> redrec (Vars.substl [b] c, stack) | App (f,cl) -> assert false (* see push_app above *) | Cast (c,_,_) -> redrec (c, stack) - | Case (ci,p,iv,c,lf) -> + | Case (ci,u,pms,p,iv,c,lf) -> (try - redrec (special_red_case env sigma (ci,p,iv,c,lf), stack) + redrec (special_red_case env sigma (ci,u,pms,p,iv,c,lf), stack) with Redelimination -> s') | Fix fix -> @@ -823,15 +848,15 @@ and reduce_proj env sigma c = let proj_narg = Projection.npars proj + Projection.arg proj in List.nth cargs proj_narg | _ -> raise Redelimination) - | Case (n,p,iv,c,brs) -> + | Case (n,u,pms,p,iv,c,brs) -> let c' = redrec c in - let p = (n,p,iv,c',brs) in + let p = (n,u,pms,p,iv,c',brs) in (try special_red_case env sigma p with Redelimination -> mkCase p) | _ -> raise Redelimination in redrec c -and special_red_case env sigma (ci, p, iv, c, lf) = +and special_red_case env sigma (ci, u, pms, p, iv, c, lf) = let rec redrec s = let (constr, cargs) = whd_simpl_stack env sigma s in match match_eval_ref env sigma constr cargs with @@ -841,14 +866,14 @@ and special_red_case env sigma (ci, p, iv, c, lf) = | Some gvalue -> if reducible_mind_case sigma gvalue then reduce_mind_case_use_function constr env sigma - {mP=p; mconstr=gvalue; mcargs=cargs; + {mP=p; mU = u; mParams = pms; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf} else redrec (gvalue, cargs)) | None -> if reducible_mind_case sigma constr then - reduce_mind_case sigma - {mP=p; mconstr=constr; mcargs=cargs; + reduce_mind_case env sigma + {mP=p; mU = u; mParams = pms; mconstr=constr; mcargs=cargs; mci=ci; mlf=lf} else raise Redelimination @@ -896,7 +921,7 @@ let try_red_product env sigma c = let open Context.Rel.Declaration in mkProd (x, a, redrec (push_rel (LocalAssum (x, a)) env) b) | LetIn (x,a,b,t) -> redrec env (Vars.subst1 a t) - | Case (ci,p,iv,d,lf) -> simpfun (mkCase (ci,p,iv,redrec env d,lf)) + | Case (ci,u,pms,p,iv,d,lf) -> simpfun (mkCase (ci,u,pms,p,iv,redrec env d,lf)) | Proj (p, c) -> let c' = match EConstr.kind sigma c with @@ -1043,31 +1068,26 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = (* Still the same projection, we ignore the change in parameters *) mkProj (p, a') else mkApp (app', [| a' |]) - | _ -> map_constr_with_binders_left_to_right sigma g f acc c + | _ -> map_constr_with_binders_left_to_right env sigma g f acc c let e_contextually byhead (occs,c) f = begin fun env sigma t -> - let (nowhere_except_in,locs) = Locusops.convert_occs occs in - let maxocc = List.fold_right max locs 0 in - let pos = ref 1 in + let count = ref (Locusops.initialize_occurrence_counter occs) in (* FIXME: we do suspicious things with this evarmap *) let evd = ref sigma in let rec traverse nested (env,c as envc) t = - if nowhere_except_in && (!pos > maxocc) then (* Shortcut *) t + if Locusops.occurrences_done !count then (* Shortcut *) t else try let subst = if byhead then matches_head env sigma c t else Constr_matching.matches env sigma c t in - let ok = - if nowhere_except_in then Int.List.mem !pos locs - else not (Int.List.mem !pos locs) in - incr pos; + let ok, count' = Locusops.update_occurrence_counter !count in count := count'; if ok then begin if Option.has_some nested then - user_err (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str "."); + user_err (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (Locusops.current_occurrence !count) ++ str "."); (* Skip inner occurrences for stable counting of occurrences *) - if locs != [] then - ignore (traverse_below (Some (!pos-1)) envc t); + if Locusops.more_specific_occurrences !count then + ignore (traverse_below (Some (Locusops.current_occurrence !count)) envc t); let (evm, t) = (f subst) env !evd t in (evd := evm; t) end @@ -1087,7 +1107,7 @@ let e_contextually byhead (occs,c) f = begin fun env sigma t -> (traverse nested) envc sigma t in let t' = traverse None (env,c) t in - if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs; + Locusops.check_used_occurrences !count; (!evd, t') end @@ -1105,28 +1125,25 @@ let match_constr_evaluable_ref sigma c evref = | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty | _, _ -> None -let substlin env sigma evalref n (nowhere_except_in,locs) c = - let maxocc = List.fold_right max locs 0 in - let pos = ref n in - assert (List.for_all (fun x -> x >= 0) locs); +let substlin env sigma evalref occs c = + let count = ref (Locusops.initialize_occurrence_counter occs) in let value u = value_of_evaluable_ref env evalref u in let rec substrec () c = - if nowhere_except_in && !pos > maxocc then c + if Locusops.occurrences_done !count then c else match match_constr_evaluable_ref sigma c evalref with | Some u -> - let ok = - if nowhere_except_in then Int.List.mem !pos locs - else not (Int.List.mem !pos locs) in - incr pos; - if ok then value u else c + let ok, count' = Locusops.update_occurrence_counter !count in + count := count'; + if ok then value u else c | None -> - map_constr_with_binders_left_to_right sigma + map_constr_with_binders_left_to_right env sigma (fun _ () -> ()) substrec () c in let t' = substrec () c in - (!pos, t') + Locusops.check_used_occurrences !count; + (Locusops.current_occurrence !count, t') let string_of_evaluable_ref env = function | EvalVarRef id -> Id.to_string id @@ -1154,23 +1171,14 @@ let unfold env sigma name c = * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences. * Performs a betaiota reduction after unfolding. *) let unfoldoccs env sigma (occs,name) c = - let unfo nowhere_except_in locs = - let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in - if Int.equal nbocc 1 then + match occs with + | NoOccurrences -> c + | AllOccurrences -> unfold env sigma name c + | OnlyOccurrences _ | AllOccurrencesBut _ | AtLeastOneOccurrence -> + let (occ,uc) = substlin env sigma name occs c in + if Int.equal occ 0 then user_err Pp.(str ((string_of_evaluable_ref env name)^" does not occur.")); - let rest = List.filter (fun o -> o >= nbocc) locs in - let () = match rest with - | [] -> () - | _ -> error_invalid_occurrence rest - in nf_betaiotazeta env sigma uc - in - match occs with - | NoOccurrences -> c - | AllOccurrences -> unfold env sigma name c - | OnlyOccurrences l -> unfo true l - | AllOccurrencesBut l -> unfo false l - | AtLeastOneOccurrence -> unfo false [] (* Unfold reduction tactic: *) let unfoldn loccname env sigma c = @@ -1293,9 +1301,9 @@ let one_step_reduce env sigma c = | App (f,cl) -> redrec (f, (Array.to_list cl)@stack) | LetIn (_,f,_,cl) -> (Vars.subst1 f cl,stack) | Cast (c,_,_) -> redrec (c,stack) - | Case (ci,p,iv,c,lf) -> + | Case (ci,u,pms,p,iv,c,lf) -> (try - (special_red_case env sigma (ci,p,iv,c,lf), stack) + (special_red_case env sigma (ci,u,pms,p,iv,c,lf), stack) with Redelimination -> raise NotStepReducible) | Fix fix -> (try match reduce_fix env sigma fix stack with diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 65e3421736..aa232175bb 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -18,6 +18,21 @@ open Locus open Univ open Ltac_pretype +(* XXX: Move to a module *) +type evaluable_global_reference = + | EvalVarRef of Id.t + | EvalConstRef of Constant.t + +val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool + +(** Here the semantics is completely unclear. + What does "Hint Unfold t" means when "t" is a parameter? + Does the user mean "Unfold X.t" or does she mean "Unfold y" + where X.t is later on instantiated with y? I choose the first + interpretation (i.e. an evaluable reference is never expanded). *) +val subst_evaluable_reference : + Mod_subst.substitution -> evaluable_global_reference -> evaluable_global_reference + type reduction_tactic_error = InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index aeb3873de7..5b8b367ff2 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -33,7 +33,7 @@ let meta_type env evd mv = let ty = try Evd.meta_ftype evd mv with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in - meta_instance env evd ty + meta_instance env (create_meta_instance_subst evd) ty let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in @@ -178,7 +178,7 @@ let type_case_branches env sigma (ind,largs) pj c = let ty = whd_betaiota env sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in sigma, (lc, ty, Sorts.relevance_of_sort ps) -let judge_of_case env sigma ci pj iv cj lfj = +let judge_of_case env sigma case ci pj iv cj lfj = let ((ind, u), spec) = try find_mrectype env sigma cj.uj_type with Not_found -> error_case_not_inductive env sigma cj in @@ -189,7 +189,7 @@ let judge_of_case env sigma ci pj iv cj lfj = let () = if (match iv with | NoInvert -> false | CaseInvert _ -> true) != should_invert_case env ci then Type_errors.error_bad_invert env in - sigma, { uj_val = mkCase (ci, pj.uj_val, iv, cj.uj_val, Array.map j_val lfj); + sigma, { uj_val = mkCase case; uj_type = rslty } let check_type_fixpoint ?loc env sigma lna lar vdefj = @@ -383,20 +383,23 @@ let rec execute env sigma cstr = let sigma, ty = type_of_constructor env sigma ctor in sigma, make_judge cstr ty - | Case (ci,p,iv,c,lf) -> + | Case (ci, u, pms, p, iv, c, lf) -> + let case = (ci, u, pms, p, iv, c, lf) in + let (ci, p, iv, c, lf) = EConstr.expand_case env sigma case in let sigma, cj = execute env sigma c in let sigma, pj = execute env sigma p in let sigma, lfj = execute_array env sigma lf in let sigma = match iv with | NoInvert -> sigma - | CaseInvert {univs;args} -> - let t = mkApp (mkIndU (ci.ci_ind,univs), args) in + | CaseInvert {indices} -> + let args = Array.append pms indices in + let t = mkApp (mkIndU (ci.ci_ind,u), args) in let sigma, tj = execute env sigma t in let sigma, tj = type_judgment env sigma tj in let sigma = check_actual_type env sigma cj tj.utj_val in sigma in - judge_of_case env sigma ci pj iv cj lfj + judge_of_case env sigma case ci pj iv cj lfj | Fix ((vn,i as vni),recdef) -> let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 1c24578a1c..83e46e3295 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -563,7 +563,7 @@ let is_rigid_head sigma flags t = | Construct _ | Int _ | Float _ | Array _ -> true | Fix _ | CoFix _ -> true | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _ - | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _, _) + | Lambda _ | LetIn _ | App (_, _) | Case _ | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) let force_eqs c = @@ -652,7 +652,7 @@ let rec is_neutral env sigma ts t = not (TransparentState.is_transparent_variable ts id) | Rel n -> true | Evar _ | Meta _ -> true - | Case (_, p, _, c, _) -> is_neutral env sigma ts c + | Case (_, _, _, _, _, c, _) -> is_neutral env sigma ts c | Proj (p, c) -> is_neutral env sigma ts c | Lambda _ | LetIn _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> false | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *) @@ -698,6 +698,16 @@ let careful_infer_conv ~pb ~ts env sigma m n = (fun sigma -> infer_conv ~pb ~ts env sigma m n) else infer_conv ~pb ~ts env sigma m n +type maybe_ground = Ground | NotGround | Unknown + +let error_cannot_unify_local env sigma (m, n, p) = + error_cannot_unify_local env sigma (fst m, fst n, p) + +let fast_occur_meta_or_undefined_evar sigma (c, gnd) = match gnd with +| Unknown -> occur_meta_or_undefined_evar sigma c +| Ground -> false +| NotGround -> true + let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top env cv_pb flags m n = let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn : subst0) curm curn = let cM = Evarutil.whd_head_evar sigma curm @@ -795,7 +805,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else Evd.set_eq_sort curenv sigma s1 s2 in (sigma', metasubst, evarsubst) with e when CErrors.noncritical e -> - error_cannot_unify curenv sigma (m,n)) + error_cannot_unify curenv sigma (fst m,fst n)) | Lambda (na,t1,c1), Lambda (__,t2,c2) -> unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} @@ -853,7 +863,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e unify_app_pattern true curenvnb pb opt substn cM f1 l1 cN f2 l2 | _ -> raise ex) - | Case (ci1,p1,_,c1,cl1), Case (ci2,p2,_,c2,cl2) -> + | Case (ci1, u1, pms1, p1, iv1, c1, cl1), Case (ci2, u2, pms2, p2, iv2, c2, cl2) -> + let (ci1, p1, iv1, c1, cl1) = EConstr.expand_case env sigma (ci1, u1, pms1, p1, iv1, c1, cl1) in + let (ci2, p2, iv2, c2, cl2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv2, c2, cl2) in (try if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN); let opt' = {opt with at_top = true; with_types = false} in @@ -963,7 +975,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e modulo_delta = TransparentState.full; modulo_eta = true; modulo_betaiota = true } - ty1 ty2 + (ty1, Unknown) (ty2, Unknown) with RetypeError _ -> substn and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN = @@ -1070,10 +1082,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) = let f1 () = if isApp_or_Proj sigma cM then - let f1l1 = whd_nored_state curenv sigma (cM,Stack.empty) in - if is_open_canonical_projection curenv sigma f1l1 then - let f2l2 = whd_nored_state curenv sigma (cN,Stack.empty) in - solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn + if is_open_canonical_projection curenv sigma cM then + solve_canonical_projection curenvnb pb opt cM cN substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) in @@ -1086,14 +1096,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else try f1 () with e when precatchable_exception e -> if isApp_or_Proj sigma cN then - let f2l2 = whd_nored_state curenv sigma (cN, Stack.empty) in - if is_open_canonical_projection curenv sigma f2l2 then - let f1l1 = whd_nored_state curenv sigma (cM, Stack.empty) in - solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn + if is_open_canonical_projection curenv sigma cN then + solve_canonical_projection curenvnb pb opt cN cM substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) - and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) = + and solve_canonical_projection curenvnb pb opt cM cN (sigma,ms,es) = + let f1l1 = whd_nored_state (fst curenvnb) sigma (cM,Stack.empty) in + let f2l2 = whd_nored_state (fst curenvnb) sigma (cN,Stack.empty) in let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2 with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -1133,10 +1143,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e try let res = if subterm_restriction opt flags || - occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n + fast_occur_meta_or_undefined_evar sigma m || fast_occur_meta_or_undefined_evar sigma n then None else + let (m, _) = m in + let (n, _) = n in let ans = match flags.modulo_conv_on_closed_terms with | Some convflags -> careful_infer_conv ~pb:cv_pb ~ts:convflags env sigma m n | _ -> constr_cmp cv_pb env sigma flags m n in @@ -1152,7 +1164,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e in let a = match res with | Some sigma -> sigma, ms, es - | None -> unirec_rec (env,0) cv_pb opt subst m n in + | None -> unirec_rec (env,0) cv_pb opt subst (fst m) (fst n) in if debug_unification () then Feedback.msg_debug (str "Leaving unification with success"); a with e -> @@ -1160,7 +1172,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e if debug_unification () then Feedback.msg_debug (str "Leaving unification with failure"); Exninfo.iraise e -let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env +let unify_0 env sigma pb flags c1 c2 = + unify_0_with_initial_metas (sigma,[],[]) true env pb flags (c1, Unknown) (c2, Unknown) let left = true let right = false @@ -1494,13 +1507,13 @@ let check_types env flags (sigma,_,_ as subst) m n = if isEvar_or_Meta sigma (head_app env sigma m) then unify_0_with_initial_metas subst true env CUMUL flags - (get_type_of env sigma n) - (get_type_of env sigma m) + (get_type_of env sigma n, Unknown) + (get_type_of env sigma m, Unknown) else if isEvar_or_Meta sigma (head_app env sigma n) then unify_0_with_initial_metas subst true env CUMUL flags - (get_type_of env sigma m) - (get_type_of env sigma n) + (get_type_of env sigma m, Unknown) + (get_type_of env sigma n, Unknown) else subst let try_resolve_typeclasses env evd flag m n = @@ -1511,7 +1524,7 @@ let try_resolve_typeclasses env evd flag m n = let w_unify_core_0 env evd with_types cv_pb flags m n = let (mc1,evd') = retract_coercible_metas evd in - let (sigma,ms,es) = check_types env (set_flags_for_type flags.core_unify_flags) (evd',mc1,[]) m n in + let (sigma,ms,es) = check_types env (set_flags_for_type flags.core_unify_flags) (evd',mc1,[]) (fst m) (fst n) in let subst2 = unify_0_with_initial_metas (sigma,ms,es) false env cv_pb flags.core_unify_flags m n @@ -1524,7 +1537,7 @@ let w_typed_unify env evd = w_unify_core_0 env evd true let w_typed_unify_array env evd flags f1 l1 f2 l2 = let f1,l1,f2,l2 = adjust_app_array_size f1 l1 f2 l2 in let (mc1,evd') = retract_coercible_metas evd in - let fold_subst subst m n = unify_0_with_initial_metas subst true env CONV flags.core_unify_flags m n in + let fold_subst subst m n = unify_0_with_initial_metas subst true env CONV flags.core_unify_flags (m, Unknown) (n, Unknown) in let subst = fold_subst (evd', [], []) f1 f2 in let subst = Array.fold_left2 fold_subst subst l1 l2 in let evd = w_merge env true flags.merge_unify_flags subst in @@ -1611,6 +1624,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = restrict_conv_on_strict_subterms = true } } else default_matching_flags pending in let n = Array.length (snd (decompose_app_vect sigma c)) in + let cgnd = if occur_meta_or_undefined_evar sigma c then NotGround else Ground in let matching_fun _ t = try let t',l2 = @@ -1624,7 +1638,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = else applist (t,l1), l2 else t, [] in - let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in + let sigma = w_typed_unify env sigma Reduction.CONV flags (c, cgnd) (t', Unknown) in let ty = Retyping.get_type_of env sigma t in if not (is_correct_type ty) then raise (NotUnifiable None); Some(sigma, t, l2) @@ -1680,7 +1694,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = (push_named_context_val d sign,depdecls) | (AllOccurrences | AtLeastOneOccurrence), InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in - let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in + let newdecl = replace_term_occ_decl_modulo env sigma occ test mkvarid d in if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl && not (indirectly_dependent sigma c d depdecls) then @@ -1691,7 +1705,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = (push_named_context_val newdecl sign, newdecl :: depdecls) | occ -> (* There are specific occurrences, hence not like first *) - let newdecl = replace_term_occ_decl_modulo sigma (AtOccs occ) test mkvarid d in + let newdecl = replace_term_occ_decl_modulo env sigma (AtOccs occ) test mkvarid d in (push_named_context_val newdecl sign, newdecl :: depdecls) in try let sign,depdecls = @@ -1701,7 +1715,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = | NoOccurrences -> concl | occ -> let occ = if likefirst then LikeFirst else AtOccs occ in - replace_term_occ_modulo sigma occ test mkvarid concl + replace_term_occ_modulo env sigma occ test mkvarid concl in let lastlhyp = if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in @@ -1765,6 +1779,7 @@ let keyed_unify env evd kop = let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = let bestexn = ref None in let kop = Keys.constr_key (fun c -> EConstr.kind evd c) op in + let opgnd = if occur_meta_or_undefined_evar evd op then NotGround else Ground in let rec matchrec cl = let cl = strip_outer_cast evd cl in (try @@ -1774,7 +1789,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = let f1, l1 = decompose_app_vect evd op in let f2, l2 = decompose_app_vect evd cl in w_typed_unify_array env evd flags f1 l1 f2 l2,cl - else w_typed_unify env evd CONV flags op cl,cl + else w_typed_unify env evd CONV flags (op, opgnd) (cl, Unknown),cl with ex when Pretype_errors.unsatisfiable_exception ex -> bestexn := Some ex; user_err Pp.(str "Unsat")) else user_err Pp.(str "Bound 1") @@ -1789,11 +1804,11 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = matchrec c1 with ex when precatchable_exception ex -> matchrec c2) - | Case(_,_,_,c,lf) -> (* does not search in the predicate *) + | Case(_,_,_,_,_,c,lf) -> (* does not search in the predicate *) (try matchrec c with ex when precatchable_exception ex -> - iter_fail matchrec lf) + iter_fail matchrec (Array.map snd lf)) | LetIn(_,c1,_,c2) -> (try matchrec c1 @@ -1869,11 +1884,12 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = else bind (f a.(i)) (ffail (i+1)) in ffail 0 in + let opgnd = if occur_meta_or_undefined_evar evd op then NotGround else Ground in let rec matchrec cl = let cl = strip_outer_cast evd cl in (bind (if closed0 evd cl - then return (fun () -> w_typed_unify env evd CONV flags op cl,cl) + then return (fun () -> w_typed_unify env evd CONV flags (op, opgnd) (cl, Unknown),cl) else fail "Bound 1") (match EConstr.kind evd cl with | App (f,args) -> @@ -1883,8 +1899,8 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = let c2 = args.(n-1) in bind (matchrec c1) (matchrec c2) - | Case(_,_,_,c,lf) -> (* does not search in the predicate *) - bind (matchrec c) (bind_iter matchrec lf) + | Case(_,_,_,_,_,c,lf) -> (* does not search in the predicate *) + bind (matchrec c) (bind_iter matchrec (Array.map snd lf)) | Proj (p,c) -> matchrec c @@ -2052,7 +2068,7 @@ let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = raise ex) (* General case: try first order *) - | _ -> w_typed_unify env evd cv_pb flags ty1 ty2 + | _ -> w_typed_unify env evd cv_pb flags (ty1, Unknown) (ty2, Unknown) (* Profiling *) diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 077597c278..c4de353d18 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -116,13 +116,3 @@ val unify_0 : Environ.env -> types -> types -> subst0 - -val unify_0_with_initial_metas : - subst0 -> - bool -> - Environ.env -> - Evd.conv_pb -> - core_unify_flags -> - types -> - types -> - subst0 diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 1420401875..cf6d581066 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -284,10 +284,10 @@ and nf_stk ?from:(from=0) env sigma c t stk = let tcase = build_case_type p realargs c in let ci = Inductiveops.make_case_info env ind relevance RegularStyle in let iv = if Typeops.should_invert_case env ci then - CaseInvert {univs=u; args=allargs} + CaseInvert {indices=realargs} else NoInvert in - nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk + nf_stk env sigma (mkCase (Inductive.contract_case env (ci, p, iv, c, branchs))) tcase stk | Zproj p :: stk -> assert (from = 0) ; let p' = Projection.make p true in |