diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constr_matching.ml | 38 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 33 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 8 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 5 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 68 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 24 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 8 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 177 | ||||
| -rw-r--r-- | pretyping/unification.ml | 46 | ||||
| -rw-r--r-- | pretyping/unification.mli | 10 |
10 files changed, 215 insertions, 202 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index c77feeafbb..15d1ddb4ec 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -352,10 +352,9 @@ let matches_core env sigma allow_bound_rels (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | 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 (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in + let ctx_b2,b2 = br2.(0) in + let ctx_b2',b2' = br2.(1) in let n = Context.Rel.length ctx_b2 in let n' = Context.Rel.length ctx_b2' in if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then @@ -370,7 +369,7 @@ let matches_core env sigma allow_bound_rels raise PatternMatchingFailure | 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 (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in let n2 = Array.length br2 in let () = match ci1.cip_ind with | None -> () @@ -383,14 +382,37 @@ let matches_core env sigma allow_bound_rels if not ci1.cip_extensible && not (Int.equal (List.length br1) n2) then raise PatternMatchingFailure in + let sorec_under_ctx subst (n, c1) (decls, c2) = + let env = push_rel_context decls env in + let rec fold (ctx, subst) nas decls = match nas, decls with + | [], _ -> + (* Historical corner case: less bound variables are allowed in + destructuring let-bindings. See #13735. *) + (ctx, subst) + | na1 :: nas, d :: decls -> + let na2 = Context.Rel.Declaration.get_annot d in + let t = Context.Rel.Declaration.get_type d in + let ctx = push_binder na1 na2 t ctx in + let subst = add_binders na1 na2 binding_vars subst in + fold (ctx, subst) nas decls + | _, [] -> + assert false + in + let ctx, subst = fold (ctx, subst) (Array.to_list n) (List.rev decls) in + sorec ctx env subst c1 c2 + in let chk_branch subst (j,n,c) = (* (ind,j+1) is normally known to be a correct constructor and br2 a correct match over the same inductive *) assert (j < n2); - sorec ctx env subst c br2.(j) + sorec_under_ctx subst (n, c) br2.(j) + in + let subst = sorec ctx env subst a1 a2 in + let subst = match p1 with + | None -> subst + | Some p1 -> sorec_under_ctx subst p1 p2 in - let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in - List.fold_left chk_branch chk_head br1 + List.fold_left chk_branch subst br1 | PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2)) when Array.equal Int.equal ln1 ln2 && i1 = i2 -> diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index bb5125f5ed..48f34e7c6b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -744,9 +744,11 @@ let detype_level sigma l = UNamed (detype_level_name sigma l) let detype_instance sigma l = - let l = EInstance.kind sigma l in - if Univ.Instance.is_empty l then None - else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) + if not !print_universes then None + else + let l = EInstance.kind sigma l in + if Univ.Instance.is_empty l then None + else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) let delay (type a) (d : a delay) (f : a delay -> _ -> _ -> _ -> _ -> _ -> a glob_constr_r) flags env avoid sigma t : a glob_constr_g = match d with @@ -928,10 +930,12 @@ and detype_binder d flags bk avoid env sigma decl c = let c = detype d { flags with flg_isgoal = false } avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) let s = - (* It can fail if ty is an evar, or if run inside ocamldebug or the - OCaml toplevel since their printers don't have access to the proper sigma/env *) - try Retyping.get_sort_family_of (snd env) sigma ty - with Retyping.RetypeError _ -> InType + if !Flags.in_debugger then InType + else + (* It can fail if ty is an evar, or if run inside ocamldebug or the + OCaml toplevel since their printers don't have access to the proper sigma/env *) + try Retyping.get_sort_family_of (snd env) sigma ty + with Retyping.RetypeError _ -> InType in let t = if s != InProp && not !Flags.raw_print then None else Some (detype d { flags with flg_isgoal = false } avoid env sigma ty) in GLetIn (na', c, t, r) @@ -1160,18 +1164,3 @@ let rec subst_glob_constr env subst = DAst.map (function GArray(u,t',def',ty') ) - -(* Utilities to transform kernel cases to simple pattern-matching problem *) - -let simple_cases_matrix_of_branches ind brs = - List.map (fun (i,n,b) -> - let nal,c = it_destRLambda_or_LetIn_names n b in - let mkPatVar na = DAst.make @@ PatVar na in - let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in - let ids = List.map_filter Nameops.Name.to_option nal in - CAst.make @@ (ids,[p],c)) - brs - -let return_type_of_predicate ind nrealargs_tags pred = - let nal,p = it_destRLambda_or_LetIn_names (nrealargs_tags@[false]) pred in - (List.hd nal, Some (CAst.make (ind, List.tl nal))), Some p diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 254f772ff8..6d6f7fa97b 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -72,14 +72,6 @@ val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option val force_wildcard : unit -> bool val synthetize_type : unit -> bool -(** Utilities to transform kernel cases to simple pattern-matching problem *) - -val it_destRLambda_or_LetIn_names : bool list -> glob_constr -> Name.t list * glob_constr -val simple_cases_matrix_of_branches : - inductive -> (int * bool list * glob_constr) list -> cases_clauses -val return_type_of_predicate : - inductive -> bool list -> glob_constr -> predicate_pattern * glob_constr option - val subst_genarg_hook : (substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument) Hook.t diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index f6d61f4892..553511f1bf 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -18,7 +18,6 @@ type patvar = Id.t type case_info_pattern = { cip_style : Constr.case_style; cip_ind : inductive option; - cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) cip_extensible : bool (** does this match end with _ => _ ? *) } type constr_pattern = @@ -35,8 +34,8 @@ type constr_pattern = | PSort of Sorts.family | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern - | PCase of case_info_pattern * constr_pattern * constr_pattern * - (int * bool list * constr_pattern) list (** index of constructor, nb of args *) + | PCase of case_info_pattern * (Name.t array * constr_pattern) option * constr_pattern * + (int * Name.t array * constr_pattern) list (** index of constructor, nb of args *) | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array) | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) | PInt of Uint63.t diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 47097a0e32..0c4bbf71e2 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -24,7 +24,6 @@ open Environ let case_info_pattern_eq i1 i2 = i1.cip_style == i2.cip_style && Option.equal Ind.CanOrd.equal i1.cip_ind i2.cip_ind && - Option.equal (List.equal (==)) i1.cip_ind_tags i2.cip_ind_tags && i1.cip_extensible == i2.cip_extensible let rec constr_pattern_eq p1 p2 = match p1, p2 with @@ -51,7 +50,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2 | PCase (info1, p1, r1, l1), PCase (info2, p2, r2, l2) -> case_info_pattern_eq info1 info2 && - constr_pattern_eq p1 p2 && + Option.equal (fun (nas1, p1) (nas2, p2) -> Array.equal Name.equal nas1 nas2 && constr_pattern_eq p1 p2) p1 p2 && constr_pattern_eq r1 r2 && List.equal pattern_eq l1 l2 | PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) -> @@ -74,7 +73,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with (** FIXME: fixpoint and cofixpoint should be relativized to pattern *) and pattern_eq (i1, j1, p1) (i2, j2, p2) = - Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2 + Int.equal i1 i2 && Array.equal Name.equal j1 j2 && constr_pattern_eq p1 p2 and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = Array.equal Name.equal n1 n2 && @@ -92,8 +91,8 @@ let rec occur_meta_pattern = function | PIf (c,c1,c2) -> (occur_meta_pattern c) || (occur_meta_pattern c1) || (occur_meta_pattern c2) - | PCase(_,p,c,br) -> - (occur_meta_pattern p) || + | PCase(_, p,c,br) -> + Option.cata (fun (_, p) -> occur_meta_pattern p) false p || (occur_meta_pattern c) || (List.exists (fun (_,_,p) -> occur_meta_pattern p) br) | PArray (t,def,ty) -> @@ -115,10 +114,10 @@ let rec occurn_pattern n = function | PIf (c,c1,c2) -> (occurn_pattern n c) || (occurn_pattern n c1) || (occurn_pattern n c2) - | PCase(_,p,c,br) -> - (occurn_pattern n p) || + | PCase(_, p, c, br) -> + Option.cata (fun (nas, p) -> occurn_pattern (Array.length nas + n) p) false p || (occurn_pattern n c) || - (List.exists (fun (_,_,p) -> occurn_pattern n p) br) + (List.exists (fun (_, nas, p) -> occurn_pattern (Array.length nas + n) p) br) | PMeta _ | PSoApp _ -> true | PEvar (_,args) -> List.exists (occurn_pattern n) args | PVar _ | PRef _ | PSort _ | PInt _ | PFloat _ -> false @@ -202,18 +201,25 @@ let pattern_of_constr env sigma t = | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> PMeta None) - | 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 + | Case (ci, u, pms, p0, iv, a, br0) -> + let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p0, iv, a, br0) in + let pattern_of_ctx c (nas, c0) = + let ctx, c = Term.decompose_lam_n_decls (Array.length nas) c in + let env = push_rel_context ctx env in + let c = pattern_of_constr env c in + (Array.map Context.binder_name nas, c) + in + let p = pattern_of_ctx p p0 in let cip = { cip_style = ci.ci_pp_info.style; cip_ind = Some ci.ci_ind; - cip_ind_tags = Some ci.ci_pp_info.ind_tags; cip_extensible = false } in let branch_of_constr i c = - (i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c) + let nas, c = pattern_of_ctx c br0.(i) in + (i, nas, c) in - PCase (cip, pattern_of_constr env p, pattern_of_constr env a, + PCase (cip, Some p, pattern_of_constr env a, 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 @@ -242,7 +248,10 @@ let map_pattern_with_binders g f l = function | PLetIn (n,a,t,b) -> PLetIn (n,f l a,Option.map (f l) t,f (g n l) b) | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2) | PCase (ci,po,p,pl) -> - PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl) + let fold nas l = Array.fold_left (fun l na -> g na l) l nas in + let map_branch (i, n, c) = (i, n, f (fold n l) c) in + let po = Option.map (fun (nas, po) -> nas, (f (fold nas l) po)) po in + PCase (ci,po,f l p, List.map map_branch pl) | PProj (p,pc) -> PProj (p, f l pc) | PFix (lni,(lna,tl,bl)) -> let l' = Array.fold_left (fun l na -> g na l) l lna in @@ -352,7 +361,11 @@ let rec subst_pattern env sigma subst pat = let ind = cip.cip_ind in let ind' = Option.Smart.map (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in - let typ' = subst_pattern env sigma subst typ in + let map ((nas, typ) as t) = + let typ' = subst_pattern env sigma subst typ in + if typ' == typ then t else (nas, typ') + in + let typ' = Option.Smart.map map typ in let c' = subst_pattern env sigma subst c in let subst_branch ((i,n,c) as br) = let c' = subst_pattern env sigma subst c in @@ -382,8 +395,6 @@ let rec subst_pattern env sigma subst pat = let mkPLetIn na b t c = PLetIn(na,b,t,c) let mkPProd na t u = PProd(na,t,u) let mkPLambda na t b = PLambda(na,t,b) -let mkPLambdaUntyped na b = PLambda(na,PMeta None,b) -let rev_it_mkPLambdaUntyped = List.fold_right mkPLambdaUntyped let mkPProd_or_LetIn (na,_,bo,t) c = match bo with @@ -446,18 +457,14 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> - let mkGLambda na c = DAst.make ?loc @@ - GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None),c) in - let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; cip_ind = None; - cip_ind_tags = None; cip_extensible = false } in - let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in - PCase (cip, PMeta None, pat_of_raw metas vars b, - [0,tags,pat_of_raw metas vars c]) + let tags = Array.of_list nal (* Approximation which can be without let-ins... *) in + PCase (cip, None, pat_of_raw metas vars b, + [0,tags,pat_of_raw metas (List.rev_append (Array.to_list tags) vars) c]) | GCases (sty,p,[c,(na,indnames)],brs) -> let get_ind p = match DAst.get p with | PatCstr((ind,_),_,_) -> Some ind @@ -476,18 +483,17 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function let pred = match p,indnames with | Some p, Some {CAst.v=(_,nal)} -> let nvars = na :: List.rev nal @ vars in - rev_it_mkPLambdaUntyped nal (mkPLambdaUntyped na (pat_of_raw metas nvars p)) - | None, _ -> PMeta None + Some (Array.rev_of_list (na :: List.rev nal), pat_of_raw metas nvars p) + | None, _ -> None | Some p, None -> match DAst.get p with - | GHole _ -> PMeta None + | GHole _ -> None | _ -> user_err ?loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = { cip_style = sty; cip_ind = ind; - cip_ind_tags = None; cip_extensible = ext } in (* Nota : when we have a non-trivial predicate, @@ -556,10 +562,10 @@ and pats_of_glob_branches loc metas vars ind brs = err ?loc (str "No unique branch for " ++ int j ++ str"-th constructor."); let lna = List.map get_arg lv in - let vars' = List.rev lna @ vars in - let pat = rev_it_mkPLambdaUntyped lna (pat_of_raw metas vars' br) in + let vars' = List.rev_append lna vars in + let tags = Array.of_list lna in + let pat = pat_of_raw metas vars' br in let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in - let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in ext, ((j-1, tags, pat) :: pats) | _ -> err ?loc:loc' (Pp.str "Non supported pattern.") diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3da75f67b9..54a47a252d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -468,23 +468,6 @@ let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) with Not_found -> None -let strong_with_flags whdfun flags env sigma t = - let push_rel_check_zeta d env = - let open CClosure.RedFlags in - let d = match d with - | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t) - | d -> d in - push_rel d env in - let rec strongrec env t = - 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 env sigma push_rel strongrec env (whdfun env sigma t) in - strongrec env t - (*************************************) (*** Reduction using bindingss ***) (*************************************) @@ -978,6 +961,9 @@ let whd_betalet = red_of_state_red whd_betalet_state (* 2. Delta Reduction Functions *) +let whd_const_state c e = raw_whd_state_gen CClosure.RedFlags.(mkflags [fCONST c]) e +let whd_const c = red_of_state_red (whd_const_state c) + let whd_delta_state e = raw_whd_state_gen CClosure.delta e let whd_delta_stack = stack_red_of_state_red whd_delta_state let whd_delta = red_of_state_red whd_delta_state @@ -1281,7 +1267,9 @@ let plain_instance sigma s c = match s with let instance env sigma s c = (* if s = [] then c else *) - strong whd_betaiota env sigma (plain_instance sigma s c) + (* No need to compute contexts under binders as whd_betaiota is local *) + let rec strongrec t = EConstr.map sigma strongrec (whd_betaiota env sigma t) in + strongrec (plain_instance sigma s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 59bc4a8b72..41d16f1c3c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -143,13 +143,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -(** {6 Reduction Function Operators } *) - -val strong_with_flags : - (CClosure.RedFlags.reds -> reduction_function) -> - (CClosure.RedFlags.reds -> reduction_function) -val strong : reduction_function -> reduction_function - (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function @@ -185,6 +178,7 @@ val whd_betalet_stack : stack_reduction_function (** {6 Head normal forms } *) +val whd_const : Constant.t -> reduction_function val whd_delta_stack : stack_reduction_function val whd_delta : reduction_function val whd_betadeltazeta_stack : stack_reduction_function diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 01819a650b..430813e874 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -68,8 +68,7 @@ let error_not_evaluable r = spc () ++ str "to an evaluable reference.") let is_evaluable_const env cst = - is_transparent env (ConstKey cst) && - (evaluable_constant cst env || is_primitive env cst) + is_transparent env (ConstKey cst) && evaluable_constant cst env let is_evaluable_var env id = is_transparent env (VarKey id) && evaluable_named id env @@ -163,6 +162,10 @@ let reference_value env sigma c u = | None -> raise NotEvaluable | Some d -> d +let is_primitive_val sigma c = match EConstr.kind sigma c with + | Int _ | Float _ | Array _ -> true + | _ -> false + (************************************************************************) (* Reduction of constants hiding a fixpoint (e.g. for "simpl" tactic). *) (* One reuses the name of the function after reduction of the fixpoint *) @@ -381,11 +384,6 @@ let x = Name default_dependent_ident do so that the reduction uses this extra information *) let dummy = mkProp -let vfx = Id.of_string "_expanded_fix_" -let vfun = Id.of_string "_eliminator_function_" -let venv = let open Context.Named.Declaration in - val_of_named_context [LocalAssum (make_annot vfx Sorts.Relevant, dummy); - LocalAssum (make_annot vfun Sorts.Relevant, dummy)] (* Mark every occurrence of substituted vars (associated to a function) as a problem variable: an evar that can be instantiated either by @@ -400,10 +398,10 @@ let substl_with_function subst sigma constr = match v.(i-k-1) with | (fx, Some (min, ref)) -> let sigma = !evd in - let (sigma, evk) = Evarutil.new_pure_evar venv sigma dummy in + let (sigma, evk) = Evarutil.new_pure_evar empty_named_context_val sigma dummy in evd := sigma; - minargs := Evar.Map.add evk min !minargs; - Vars.lift k (mkEvar (evk, [fx; ref])) + minargs := Evar.Map.add evk (min, fx, ref) !minargs; + mkEvar (evk, []) | (fx, None) -> Vars.lift k fx else mkRel (i - Array.length v) | _ -> @@ -416,14 +414,14 @@ exception Partial (* each problem variable that cannot be made totally applied even by reduction is solved by the expanded fix term. *) let solve_arity_problem env sigma fxminargs c = - let evm = ref sigma in - let set_fix i = evm := Evd.define i (mkVar vfx) !evm in + let set = ref Evar.Set.empty in + let set_fix i = set := Evar.Set.add i !set in let rec check strict c = let c' = whd_betaiotazeta env sigma c in let (h,rcargs) = decompose_app_vect sigma c' in match EConstr.kind sigma h with - Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) -> - let minargs = Evar.Map.find i fxminargs in + Evar(i,_) when Evar.Map.mem i fxminargs && not (Evar.Set.mem i !set) -> + let minargs, _, _ = Evar.Map.find i fxminargs in if Array.length rcargs < minargs then if strict then set_fix i else raise Partial; @@ -432,45 +430,95 @@ let solve_arity_problem env sigma fxminargs c = (let ev, u = destEvalRefU sigma h in match reference_opt_value env sigma ev u with | Some h' -> - let bak = !evm in + let bak = !set in (try Array.iter (check false) rcargs with Partial -> - evm := bak; + set := bak; check strict (mkApp(h',rcargs))) | None -> Array.iter (check strict) rcargs) | _ -> EConstr.iter sigma (check strict) c' in check true c; - !evm + !set let substl_checking_arity env subst sigma c = (* we initialize the problem: *) let body,sigma,minargs = substl_with_function subst sigma c in (* we collect arity constraints *) - let sigma' = solve_arity_problem env sigma minargs body in + let ans = solve_arity_problem env sigma minargs body in (* we propagate the constraints: solved problems are substituted; the other ones are replaced by the function symbol *) - let rec nf_fix c = match EConstr.kind sigma c with - | Evar (i,[fx;f]) when Evar.Map.mem i minargs -> + let rec nf_fix k c = match EConstr.kind sigma c with + | Evar (i, []) -> (* FIXME: find a less hackish way of doing this *) - begin match EConstr.kind sigma' c with - | Evar _ -> f - | c -> EConstr.of_kind c + begin match Evar.Map.find i minargs with + | (_, fx, ref) -> + if Evar.Set.mem i ans then Vars.lift k fx + else Vars.lift k ref + | exception Not_found -> + (* An argumentless evar that was not generated by substl_with_function *) + c end - | _ -> EConstr.map sigma nf_fix c + | _ -> EConstr.map_with_binders sigma succ nf_fix k c in - nf_fix body + nf_fix 0 body type fix_reduction_result = NotReducible | Reduced of (constr * constr list) let contract_fix_use_function env sigma f ((recindices,bodynum),(_names,_types,bodies as typedbodies)) = + let (names, (nbfix, lv, n)), u, largs = f in + let lu = List.firstn n largs in + let p = List.length lv in + let lyi = List.map fst lv in + let la = + List.map_i (fun q aq -> + (* k from the comment is q+1 *) + try mkRel (p+1-(List.index Int.equal (n-q) lyi)) + with Not_found -> Vars.lift p aq) + 0 lu + in + let f i = match names.(i) with + | None -> None + | Some (minargs,ref) -> + let body = applist (mkEvalRef ref u, la) in + let g = + List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> + let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in + let tij' = Vars.substl (List.rev subst) tij in + let x = make_annot x Sorts.Relevant in (* TODO relevance *) + mkLambda (x,tij',c)) 1 body (List.rev lv) + in Some (minargs,g) + in let nbodies = Array.length recindices in let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in let lbodies = List.init nbodies make_Fi in - substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum)) + let c = substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum)) in + nf_beta env sigma c let contract_cofix_use_function env sigma f - (bodynum,(_names,_,bodies as typedbodies)) = + (bodynum,(names,_,bodies as typedbodies)) args = + let f = + if isConst sigma f then + let minargs = List.length args in + fun i -> + if Int.equal i bodynum then Some (minargs, f) + else match names.(i).binder_name with + | Anonymous -> None + | Name id -> + (* In case of a call to another component of a block of + mutual inductive, try to reuse the global name if + the block was indeed initially built as a global + definition *) + let (kn, u) = destConst sigma f in + let kn = Constant.change_label kn (Label.of_id id) in + let cst = (kn, EInstance.kind sigma u) in + try match constant_opt_value_in env cst with + | None -> None + (* TODO: check kn is correct *) + | Some _ -> Some (minargs,mkConstU (kn, u)) + with Not_found -> None + else + fun _ -> None in let nbodies = Array.length bodies in let make_Fi j = (mkCoFix(j,typedbodies), f j) in let subbodies = List.init nbodies make_Fi in @@ -500,7 +548,7 @@ let reduce_mind_case env sigma mia = 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 = +let reduce_mind_case_use_function f env sigma mia = match EConstr.kind sigma mia.mconstr with | Construct ((_, i as cstr),u) -> let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in @@ -509,30 +557,8 @@ let reduce_mind_case_use_function func env sigma mia = 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 - let minargs = List.length mia.mcargs in - fun i -> - if Int.equal i bodynum then Some (minargs,func) - else match names.(i).binder_name with - | Anonymous -> None - | Name id -> - (* In case of a call to another component of a block of - mutual inductive, try to reuse the global name if - the block was indeed initially built as a global - definition *) - let (kn, u) = destConst sigma func in - let kn = Constant.change_label kn (Label.of_id id) in - let cst = (kn, EInstance.kind sigma u) in - try match constant_opt_value_in env cst with - | None -> None - (* TODO: check kn is correct *) - | Some _ -> Some (minargs,mkConstU (kn, u)) - with Not_found -> None - else - fun _ -> None in let cofix_def = - contract_cofix_use_function env sigma build_cofix_name cofix in + contract_cofix_use_function env sigma f cofix mia.mcargs in mkCase (mia.mci, mia.mU, mia.mParams, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false @@ -683,7 +709,7 @@ let rec red_elim_const env sigma ref u largs = let f = ([|Some (minfxargs,ref)|],infos), u, largs in (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) + | Reduced (c,rest) -> (c, rest), nocase) | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min -> let rec descend (ref,u) args = let c = reference_value env sigma ref u in @@ -697,7 +723,7 @@ let rec red_elim_const env sigma ref u largs = let f = refinfos, u, midargs in (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) + | Reduced (c,rest) -> (c, rest), nocase) | NotAnElimination when unfold_nonelim -> let c = reference_value env sigma ref u in (whd_betaiotazeta env sigma (applist (c, largs)), []), nocase @@ -714,7 +740,8 @@ and reduce_params env sigma stack l = let arg = List.nth stack i in let rarg = whd_construct_stack env sigma arg in match EConstr.kind sigma (fst rarg) with - | Construct _ -> List.assign stack i (applist rarg) + | Construct _ | Int _ | Float _ | Array _ -> + List.assign stack i (applist rarg) | _ -> raise Redelimination) stack l @@ -770,6 +797,16 @@ and whd_simpl_stack env sigma = else s' with Redelimination -> s') + | Const (cst, _) when is_primitive env cst -> + (try + let args = + List.map_filter_i (fun i a -> + match a with CPrimitives.Kwhnf -> Some i | _ -> None) + (CPrimitives.kind (Option.get (get_primitive env cst))) in + let stack = reduce_params env sigma stack args in + whd_const cst env sigma (applist (x, stack)), [] + with Redelimination -> s') + | _ -> match match_eval_ref env sigma x stack with | Some (ref, u) -> @@ -811,29 +848,6 @@ and reduce_fix_use_function env sigma f fix stack = let stack' = List.assign stack recargnum (applist recarg') in (match EConstr.kind sigma recarg'hd with | Construct _ -> - let (names, (nbfix, lv, n)), u, largs = f in - let lu = List.firstn n largs in - let p = List.length lv in - let lyi = List.map fst lv in - let la = - List.map_i (fun q aq -> - (* k from the comment is q+1 *) - try mkRel (p+1-(List.index Int.equal (n-q) lyi)) - with Not_found -> Vars.lift p aq) - 0 lu - in - let f i = match names.(i) with - | None -> None - | Some (minargs,ref) -> - let body = applist (mkEvalRef ref u, la) in - let g = - List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> - let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in - let tij' = Vars.substl (List.rev subst) tij in - let x = make_annot x Sorts.Relevant in (* TODO relevance *) - mkLambda (x,tij',c)) 1 body (List.rev lv) - in Some (minargs,g) - in Reduced (contract_fix_use_function env sigma f fix,stack') | _ -> NotReducible) @@ -880,11 +894,11 @@ and special_red_case env sigma (ci, u, pms, p, iv, c, lf) = in redrec (push_app sigma (c, [])) -(* reduce until finding an applied constructor or fail *) +(* reduce until finding an applied constructor (or primitive value) or fail *) and whd_construct_stack env sigma s = let (constr, cargs as s') = whd_simpl_stack env sigma (s, []) in - if reducible_mind_case sigma constr then s' + if reducible_mind_case sigma constr || is_primitive_val sigma constr then s' else match match_eval_ref env sigma constr cargs with | Some (ref, u) -> (match reference_opt_value env sigma ref u with @@ -1040,7 +1054,10 @@ let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, []) let whd_simpl env sigma c = applist (whd_simpl_stack env sigma (c, [])) -let simpl env sigma c = strong whd_simpl env sigma c +let simpl env sigma c = + let rec strongrec env t = + map_constr_with_full_binders env sigma push_rel strongrec env (whd_simpl env sigma t) in + strongrec env c (* Reduction at specific subterms *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a845fc3246..83e46e3295 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -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} @@ -965,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 = @@ -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) @@ -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") @@ -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) -> @@ -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 |