diff options
Diffstat (limited to 'pretyping')
45 files changed, 1801 insertions, 1045 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 08df9a2460..3b3de33d8e 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -13,6 +13,7 @@ open Names open Globnames open Term open Constr +open Context open Environ open Util open Libobject @@ -72,7 +73,7 @@ let arguments_names r = GlobRef.Map.find r !name_table let rename_type ty ref = let name_override old_name override = match override with - | Name _ as x -> x + | Name _ as x -> {old_name with binder_name=x} | Anonymous -> old_name in let rec rename_type_aux c = function | [] -> c diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 1ad90b2953..e22368d5e5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -16,6 +16,7 @@ open Util open Names open Nameops open Constr +open Context open Termops open Environ open EConstr @@ -321,9 +322,9 @@ let inh_coerce_to_ind env sigma0 loc ty tyi = constructor and renounce if not able to give more information *) (* devrait être indifférent d'exiger leq ou pas puisque pour un inductif cela doit être égal *) - match cumul env sigma expected_typ ty with - | Some sigma -> sigma - | None -> sigma0 + match Evarconv.unify_leq_delay env sigma expected_typ ty with + | sigma -> sigma + | exception Evarconv.UnableToUnify _ -> sigma0 let binding_vars_of_inductive sigma = function | NotInd _ -> [] @@ -431,9 +432,9 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = let sigma, current = if List.is_empty deps && isEvar sigma typ then (* Don't insert coercions if dependent; only solve evars *) - match cumul !!(pb.env) sigma indt typ with - | None -> sigma, current - | Some sigma -> sigma, current + match Evarconv.unify_leq_delay !!(pb.env) sigma indt typ with + | exception Evarconv.UnableToUnify _ -> sigma, current + | sigma -> sigma, current else let sigma, j = Coercion.inh_conv_coerce_to ?loc ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in sigma, j.uj_val @@ -472,7 +473,8 @@ let push_current_pattern ~program_mode sigma (cur,ty) eqn = let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in match eqn.patterns with | pat::pats -> - let _,rhs_env = push_rel ~hypnaming sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in + let r = Sorts.Relevant in (* TODO relevance *) + let _,rhs_env = push_rel ~hypnaming sigma (LocalDef (make_annot (alias_of_pat pat) r,cur,ty)) eqn.rhs.rhs_env in { eqn with rhs = { eqn.rhs with rhs_env = rhs_env }; patterns = pats } @@ -762,7 +764,10 @@ let get_names avoid env sigma sign eqns = (fun (l,avoid) d na -> let na = merge_name - (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid)) + (fun decl -> + let na = get_name decl in + let t = get_type decl in + Name (next_name_away (named_hd env sigma t na) avoid)) d na in (na::l,Id.Set.add (Name.get_id na) avoid)) @@ -782,10 +787,10 @@ let recover_and_adjust_alias_names (_,avoid) names sign = let rec aux = function | [],[] -> [] - | x::names, LocalAssum (_,t)::sign -> - (x, LocalAssum (alias_of_pat x,t)) :: aux (names,sign) + | x::names, LocalAssum (x',t)::sign -> + (x, LocalAssum ({x' with binder_name=alias_of_pat x},t)) :: aux (names,sign) | names, (LocalDef (na,_,_) as decl)::sign -> - (DAst.make @@ PatVar na, decl) :: aux (names,sign) + (DAst.make @@ PatVar na.binder_name, decl) :: aux (names,sign) | _ -> assert false in List.split (aux (names,sign)) @@ -1247,7 +1252,7 @@ let rec generalize_problem names sigma pb = function let pb',deps = generalize_problem names sigma pb l in let d = map_constr (lift i) (lookup_rel i !!(pb.env)) in begin match d with - | LocalDef (Anonymous,_,_) -> pb', deps + | LocalDef ({binder_name=Anonymous},_,_) -> pb', deps | _ -> (* for better rendering *) let d = RelDecl.map_type (fun c -> whd_betaiota sigma c) d in @@ -1436,16 +1441,15 @@ let compile ~program_mode sigma pb = brvals pb.tomatch pb.pred deps cstrs in let brvals = Array.map (fun (sign,body) -> it_mkLambda_or_LetIn body sign) brvals in - let (pred,typ) = + let (pred,typ) = find_predicate pb.caseloc pb.env sigma - pred current indt (names,dep) tomatch in - let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in + pred current indt (names,dep) tomatch + in + let rci = Typing.check_allowed_sort !!(pb.env) sigma mind current pred in + let ci = make_case_info !!(pb.env) (fst mind) rci pb.casestyle in let pred = nf_betaiota !!(pb.env) sigma pred in - let case = - make_case_or_project !!(pb.env) sigma indf ci pred current brvals - in + let case = make_case_or_project !!(pb.env) sigma indf ci pred current brvals in let sigma, _ = Typing.type_of !!(pb.env) sigma pred in - Typing.check_allowed_sort !!(pb.env) sigma mind current pred; sigma, { uj_val = applist (case, inst); uj_type = prod_applist sigma typ inst } @@ -1460,7 +1464,7 @@ let compile ~program_mode sigma pb = let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let pb = { pb with - env = snd (push_rel ~hypnaming sigma (LocalDef (na,current,ty)) env); + env = snd (push_rel ~hypnaming sigma (LocalDef (annotR na,current,ty)) env); tomatch = tomatch; pred = lift_predicate 1 pred tomatch; history = pop_history pb.history; @@ -1511,7 +1515,8 @@ let compile ~program_mode sigma pb = and compile_alias initial sigma pb (na,orig,(expanded,expanded_typ)) rest = let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let f c t = - let alias = LocalDef (na,c,t) in + let r = Retyping.relevance_of_type !!(pb.env) sigma t in + let alias = LocalDef (make_annot na r,c,t) in let pb = { pb with env = snd (push_rel ~hypnaming sigma alias pb.env); @@ -1524,7 +1529,7 @@ let compile ~program_mode sigma pb = if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then subst1 c j.uj_val else - mkLetIn (na,c,t,j.uj_val); + mkLetIn (make_annot na r,c,t,j.uj_val); uj_type = subst1 c j.uj_type } in (* spiwack: when an alias appears on a deep branch, its non-expanded form is automatically a variable of the same name. We avoid @@ -1707,9 +1712,11 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context !!env) in let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in - begin match solve_simple_eqn (evar_conv_x TransparentState.full) !!env sigma (None,ev,substl inst ev') with - | Success evd -> evdref := evd - | UnifFailure _ -> assert false + begin + let flags = (default_flags_of TransparentState.full) in + match solve_simple_eqn evar_unify flags !!env sigma (None,ev,substl inst ev') with + | Success evd -> evdref := evd + | UnifFailure _ -> assert false end; ev' | _ -> @@ -1765,9 +1772,9 @@ let build_tycon ?loc env tycon_env s subst tycon extenv sigma t = let sigma, t = abstract_tycon ?loc tycon_env sigma subst tycon extenv t in let sigma, tt = Typing.type_of !!extenv sigma t in (sigma, t, tt) in - match cumul !!env sigma tt (mkSort s) with - | None -> anomaly (Pp.str "Build_tycon: should be a type."); - | Some sigma -> + match unify_leq_delay !!env sigma tt (mkSort s) with + | exception Evarconv.UnableToUnify _ -> anomaly (Pp.str "Build_tycon: should be a type."); + | sigma -> sigma, { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return @@ -1810,7 +1817,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t = List.rev_append patl patl',acc_sign,acc | (t, NotInd (bo,typ)) :: tms -> let pat,acc = make_patvar t acc in - let d = LocalAssum (alias_of_pat pat,typ) in + let d = LocalAssum (annotR (alias_of_pat pat),typ) in let patl,acc_sign,acc = aux (n+1) (snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env)) (d::acc_sign) tms acc in pat::patl,acc_sign,acc in let avoid0 = GlobEnv.vars_of_env env in @@ -1911,9 +1918,11 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = match tm with | NotInd (bo,typ) -> (match t with - | None -> let sign = match bo with - | None -> [LocalAssum (na, lift n typ)] - | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign + | None -> + let r = Sorts.Relevant in (* TODO relevance *) + let sign = match bo with + | None -> [LocalAssum (make_annot na r, lift n typ)] + | Some b -> [LocalDef (make_annot na r, lift n b, lift n typ)] in sign | Some {CAst.loc} -> user_err ?loc (str"Unexpected type annotation for a term of non inductive type.")) @@ -1921,7 +1930,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let indf' = if dolift then lift_inductive_family n indf else indf in let ((ind,u),_) = dest_ind_family indf' in let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in - let arsign = fst (get_arity env0 indf') in + let arsign, inds = get_arity env0 indf' in let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in let realnal = match t with @@ -1933,8 +1942,9 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = List.rev realnal | None -> List.make nrealargs_ctxt Anonymous in + let r = Sorts.relevance_of_sort_family inds in let t = EConstr.of_constr (build_dependent_inductive env0 indf') in - LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in + LocalAssum (make_annot na r, t) :: List.map2 RelDecl.set_name realnal arsign in let rec buildrec n = function | [],[] -> [] | (_,tm)::ltm, (_,x)::tmsign -> @@ -1945,7 +1955,8 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon = match tycon with - | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma j p + | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma + ~flags:(default_flags_of TransparentState.full) j p | None -> sigma, j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) @@ -2140,9 +2151,10 @@ let constr_of_pat env sigma arsign pat avoid = | Anonymous -> let previd, id = prime avoid (Name (Id.of_string "wildcard")) in Name id, Id.Set.add id avoid - in - (sigma, (DAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, - (List.map (fun x -> mkRel 1) realargs), 1, avoid) + in + let r = Sorts.Relevant in (* TODO relevance *) + (sigma, (DAst.make ?loc @@ PatVar name), [LocalAssum (make_annot name r, ty)] @ realargs, mkRel 1, ty, + (List.map (fun x -> mkRel 1) realargs), 1, avoid) | PatCstr (((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in let IndType (indf, _) = @@ -2181,23 +2193,26 @@ let constr_of_pat env sigma arsign pat avoid = match alias with Anonymous -> sigma, pat', sign, app, apptype, realargs, n, avoid - | Name id -> - let sign = LocalAssum (alias, lift m ty) :: sign in - let avoid = Id.Set.add id avoid in + | Name id -> + let _, inds = get_arity env indf in + let r = Sorts.relevance_of_sort_family inds in + let sign = LocalAssum (make_annot alias r, lift m ty) :: sign in + let avoid = Id.Set.add id avoid in let sigma, sign, i, avoid = try let env = EConstr.push_rel_context sign env in - let sigma = the_conv_x_leq (EConstr.push_rel_context sign env) - (lift (succ m) ty) (lift 1 apptype) sigma in + let sigma = unify_leq_delay (EConstr.push_rel_context sign env) sigma + (lift (succ m) ty) (lift 1 apptype) in let sigma, eq_t = mk_eq sigma (lift (succ m) ty) (mkRel 1) (* alias *) (lift 1 app) (* aliased term *) in - let neq = eq_id avoid id in - sigma, LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid - with Reduction.NotConvertible -> sigma, sign, 1, avoid + let neq = eq_id avoid id in + (* if we ever allow using a SProp-typed coq_eq_ind this relevance will be wrong *) + sigma, LocalDef (nameR neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid + with Evarconv.UnableToUnify _ -> sigma, sign, 1, avoid in - (* Mark the equality as a hole *) + (* Mark the equality as a hole *) sigma, pat', sign, lift i app, lift i apptype, realargs, n + i, avoid in let sigma, pat', sign, patc, patty, args, z, avoid = typ env sigma (RelDecl.get_type (List.hd arsign), List.tl arsign) pat avoid in @@ -2219,18 +2234,18 @@ match EConstr.kind sigma t with let rels_of_patsign sigma = List.map (fun decl -> match decl with - | LocalDef (na,t',t) when is_topvar sigma t' -> LocalAssum (na,t) + | LocalDef (na,t',t) when is_topvar sigma t' -> LocalAssum (na,t) | _ -> decl) let vars_of_ctx sigma ctx = let _, y = List.fold_right (fun decl (prev, vars) -> match decl with - | LocalDef (na,t',t) when is_topvar sigma t' -> + | LocalDef (na,t',t) when is_topvar sigma t' -> prev, (DAst.make @@ GApp ( (DAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), - [hole na; DAst.make @@ GVar prev])) :: vars + [hole na.binder_name; DAst.make @@ GVar prev])) :: vars | _ -> match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" @@ -2340,12 +2355,13 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity = let args = List.rev args in substl args (liftn signlen (succ nargs) arity) in - let rhs_rels', tycon = + let r = Sorts.Relevant in (* TODO relevance *) + let rhs_rels', tycon = let neqs_rels, arity = match ineqs with | None -> [], arity | Some ineqs -> - [LocalAssum (Anonymous, ineqs)], lift 1 arity + [LocalAssum (make_annot Anonymous r, ineqs)], lift 1 arity in let eqs_rels, arity = decompose_prod_n_assum sigma neqs arity in eqs_rels @ neqs_rels @ rhs_rels', arity @@ -2356,7 +2372,7 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity = and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in let sigma, _btype = Typing.type_of !!env sigma bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in - let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in + let branch_decl = LocalDef (make_annot (Name branch_name) r, lift !i bbody, lift !i btype) in let branch = let bref = DAst.make @@ GVar branch_name in match vars_of_ctx sigma rhs_rels with @@ -2404,9 +2420,10 @@ let abstract_tomatch env sigma tomatchs tycon = | _ -> let tycon = Option.map (fun t -> subst_term sigma (lift 1 c) (lift 1 t)) tycon in - let name = next_ident_away (Id.of_string "filtered_var") names in + let name = next_ident_away (Id.of_string "filtered_var") names in + let r = Sorts.Relevant in (* TODO relevance *) (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, - LocalDef (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx, + LocalDef (make_annot (Name name) r, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx, Id.Set.add name names, tycon) ([], [], Id.Set.empty, tycon) tomatchs in List.rev prev, ctx, tycon @@ -2468,8 +2485,8 @@ let build_dependent_signature env sigma avoid tomatchs arsign = make_prime avoid name in (sigma, env, succ nargeqs, - (LocalAssum (Name (eq_id avoid previd), eq)) :: argeqs, - refl_arg :: refl_args, + (LocalAssum (make_annot (Name (eq_id avoid previd)) Sorts.Relevant, eq)) :: argeqs, + refl_arg :: refl_args, pred slift, RelDecl.set_name (Name id) decl :: argsign')) (sigma, env, neqs, [], [], slift, []) args argsign @@ -2483,8 +2500,8 @@ let build_dependent_signature env sigma avoid tomatchs arsign = in let sigma, refl_eq = mk_JMeq_refl sigma ty tm in let previd, id = make_prime avoid appn in - (sigma, (LocalAssum (Name (eq_id avoid previd), eq) :: argeqs) :: eqs, - succ nargeqs, + (sigma, (LocalAssum (make_annot (Name (eq_id avoid previd)) Sorts.Relevant, eq) :: argeqs) :: eqs, + succ nargeqs, refl_eq :: refl_args, pred slift, ((RelDecl.set_name (Name id) app_decl :: argsign') :: arsigns)) @@ -2500,8 +2517,9 @@ let build_dependent_signature env sigma avoid tomatchs arsign = (mkRel slift) (lift nar tm) in let sigma, refl = mk_eq_refl sigma tomatch_ty tm in + let na = make_annot (Name (eq_id avoid previd)) Sorts.Relevant in (sigma, - [LocalAssum (Name (eq_id avoid previd), eq)] :: eqs, succ neqs, + [LocalAssum (na, eq)] :: eqs, succ neqs, refl :: refl_args, pred slift, (arsign' :: []) :: arsigns)) (sigma, [], 0, [], nar, []) tomatchs arsign @@ -2577,11 +2595,12 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env (* We push the initial terms to match and push their alias to rhs' envs *) (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t) - | NotInd (Some b, t) -> LocalDef (na,b,t) - | IsInd (typ,_,_) -> LocalAssum (na,typ) in + (* TODO relevance *) + let out_tmt na = function NotInd (None,t) -> LocalAssum (make_annot na Sorts.Relevant,t) + | NotInd (Some b, t) -> LocalDef (make_annot na Sorts.Relevant,b,t) + | IsInd (typ,_,_) -> LocalAssum (make_annot na Sorts.Relevant,typ) in let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in - + let typs = List.map (fun (c,d) -> (c,extract_inductive_data !!env sigma d,d)) typs in @@ -2651,10 +2670,11 @@ let compile_cases ?loc ~program_mode style (typing_fun, sigma) tycon env (predop (* names of aliases will be recovered from patterns (hence Anonymous *) (* here) *) + (* TODO relevance *) let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t) | NotInd (Some b,t) -> LocalDef (na,b,t) | IsInd (typ,_,_) -> LocalAssum (na,typ) in - let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in + let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt (make_annot na Sorts.Relevant) tmt)) nal tomatchs in let typs = List.map (fun (c,d) -> (c,extract_inductive_data !!env sigma d,d)) typs in diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index e27fc536eb..c9f18d89be 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -48,7 +48,7 @@ type cbv_value = | VAL of int * constr | STACK of int * cbv_value * cbv_stack | CBN of constr * cbv_value subs - | LAM of int * (Name.t * constr) list * constr * cbv_value subs + | LAM of int * (Name.t Context.binder_annot * constr) list * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array | CONSTR of constructor Univ.puniverses * cbv_value array @@ -281,11 +281,11 @@ and reify_value = function (* reduction under binders *) apply_env env @@ List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) b ctxt - | FIXP ((lij,(names,lty,bds)),env,args) -> - let fix = mkFix (lij, (names, lty, bds)) in + | FIXP ((lij,fix),env,args) -> + let fix = mkFix (lij, fix) in mkApp (apply_env env fix, Array.map reify_value args) - | COFIXP ((j,(names,lty,bds)),env,args) -> - let cofix = mkCoFix (j, (names,lty,bds)) in + | COFIXP ((j,cofix),env,args) -> + let cofix = mkCoFix (j, cofix) in mkApp (apply_env env cofix, Array.map reify_value args) | CONSTR (c,args) -> mkApp(mkConstructU c, Array.map reify_value args) @@ -550,7 +550,7 @@ and cbv_norm_value info = function (* reduction under binders *) | FIXP ((lij,(names,lty,bds)),env,args) -> mkApp (mkFix (lij, - (names, + (names, Array.map (cbv_norm_term info env) lty, Array.map (cbv_norm_term info (subs_liftn (Array.length lty) env)) bds)), @@ -558,7 +558,7 @@ and cbv_norm_value info = function (* reduction under binders *) | COFIXP ((j,(names,lty,bds)),env,args) -> mkApp (mkCoFix (j, - (names,Array.map (cbv_norm_term info env) lty, + (names,Array.map (cbv_norm_term info env) lty, Array.map (cbv_norm_term info (subs_liftn (Array.length lty) env)) bds)), Array.map (cbv_norm_value info) args) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 0a1e771921..d6c2ad146e 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -32,7 +32,7 @@ type cbv_value = | VAL of int * constr | STACK of int * cbv_value * cbv_stack | CBN of constr * cbv_value subs - | LAM of int * (Name.t * constr) list * constr * cbv_value subs + | LAM of int * (Name.t Context.binder_annot * constr) list * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array | CONSTR of constructor Univ.puniverses * cbv_value array diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 306a76e35e..54a1aa9aa0 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -179,7 +179,7 @@ let find_class_type sigma t = | Proj (p, c) when not (Projection.unfolded p) -> CL_PROJ (Projection.repr p), EInstance.empty, (c :: args) | Ind (ind_sp,u) -> CL_IND ind_sp, u, args - | Prod (_,_,_) -> CL_FUN, EInstance.empty, [] + | Prod _ -> CL_FUN, EInstance.empty, [] | Sort _ -> CL_SORT, EInstance.empty, [] | _ -> raise Not_found diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 2329b87acc..82411ba2ef 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -21,6 +21,7 @@ open Util open Names open Term open Constr +open Context open Environ open EConstr open Vars @@ -64,9 +65,9 @@ let apply_coercion_args env sigma check isproj argl funj = | Prod (_,c1,c2) -> let sigma = if check then - begin match cumul env sigma (Retyping.get_type_of env sigma h) c1 with - | None -> raise NoCoercion - | Some sigma -> sigma + begin match Evarconv.unify_leq_delay env sigma (Retyping.get_type_of env sigma h) c1 with + | exception Evarconv.UnableToUnify _ -> raise NoCoercion + | sigma -> sigma end else sigma in @@ -157,7 +158,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let rec coerce_unify env x y = let x = hnf env !evdref x and y = hnf env !evdref y in try - evdref := the_conv_x_leq env x y !evdref; + evdref := Evarconv.unify_leq_delay env !evdref x y; None with UnableToUnify _ -> coerce' env x y and coerce' env x y : (EConstr.constr -> EConstr.constr) option = @@ -172,26 +173,26 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let rec aux tele typ typ' i co = if i < len then let hdx = l.(i) and hdy = l'.(i) in - try evdref := the_conv_x_leq env hdx hdy !evdref; + try evdref := unify_leq_delay env !evdref hdx hdy; let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in - aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co + aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co with UnableToUnify _ -> - let (n, eqT), restT = dest_prod typ in + let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in let () = - try evdref := the_conv_x_leq env eqT eqT' !evdref - with UnableToUnify _ -> raise NoSubtacCoercion - in + try evdref := unify_leq_delay env !evdref eqT eqT' + with UnableToUnify _ -> raise NoSubtacCoercion + in (* Disallow equalities on arities *) if Reductionops.is_arity env !evdref eqT then raise NoSubtacCoercion; let restargs = lift_args 1 (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) in let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in - let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in + let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in - let evar = make_existential ?loc n env evdref eq in + let evar = make_existential ?loc n.binder_name env evdref eq in let eq_app x = papp evdref coq_eq_rect [| eqT; hdx; pred; x; hdy; evar|] in @@ -216,9 +217,12 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) | _ -> subco ()) | Prod (name, a, b), Prod (name', a', b') -> let name' = - Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.vars_of_env env)) - in - let env' = push_rel (LocalAssum (name', a')) env in + {name' with + binder_name = + Name (Namegen.next_ident_away + Namegen.default_dependent_ident (Termops.vars_of_env env))} + in + let env' = push_rel (LocalAssum (name', a')) env in let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) let coec1 = app_opt env' evdref c1 (mkRel 1) in @@ -230,7 +234,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) | _, _ -> Some (fun f -> - mkLambda (name', a', + mkLambda (name', a', app_opt env' evdref c2 (mkApp (lift 1 f, [| coec1 |]))))) @@ -253,11 +257,11 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let c1 = coerce_unify env a a' in let remove_head a c = match EConstr.kind !evdref c with - | Lambda (n, t, t') -> c, t' + | Lambda (n, t, t') -> c, t' | Evar (k, args) -> let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in evdref := evs; - let (n, dom, rng) = destLambda !evdref t in + let (n, dom, rng) = destLambda !evdref t in if isEvar !evdref dom then let (domk, args) = destEvar !evdref dom in evdref := define domk a !evdref; @@ -265,8 +269,12 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) t, rng | _ -> raise NoSubtacCoercion in - let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in - let env' = push_rel (LocalAssum (Name Namegen.default_dependent_ident, a)) env in + let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in + let ra = Retyping.relevance_of_type env !evdref a in + let env' = push_rel + (LocalAssum (make_annot (Name Namegen.default_dependent_ident) ra, a)) + env + in let c2 = coerce_unify env' b b' in match c1, c2 with | None, None -> None @@ -396,9 +404,9 @@ let apply_coercion env sigma p hj typ_cl = let inh_app_fun_core ~program_mode env evd j = let t = whd_all env evd j.uj_type in match EConstr.kind evd t with - | Prod (_,_,_) -> (evd,j) + | Prod _ -> (evd,j) | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product evd ev in + let (evd',t) = Evardefine.define_evar_as_product env evd ev in (evd',{ uj_val = j.uj_val; uj_type = t }) | _ -> try let t,p = @@ -466,7 +474,7 @@ let inh_coerce_to_prod ?loc ~program_mode env evd t = !evdref, typ' else (evd, t) -let inh_coerce_to_fail env evd rigidonly v t c1 = +let inh_coerce_to_fail flags env evd rigidonly v t c1 = if rigidonly && not (Heads.is_rigid env (EConstr.Unsafe.to_constr c1) && Heads.is_rigid env (EConstr.Unsafe.to_constr t)) then raise NoCoercion @@ -483,13 +491,16 @@ let inh_coerce_to_fail env evd rigidonly v t c1 = | None -> evd, None, t with Not_found -> raise NoCoercion in - try (the_conv_x_leq env t' c1 evd, v') + try (unify_leq_delay ~flags env evd t' c1, v') with UnableToUnify _ -> raise NoCoercion -let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 = - try (the_conv_x_leq env t c1 evd, v) +let default_flags_of env = + default_flags_of TransparentState.full + +let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigidonly v t c1 = + try (unify_leq_delay ~flags env evd t c1, v) with UnableToUnify (best_failed_evd,e) -> - try inh_coerce_to_fail env evd rigidonly v t c1 + try inh_coerce_to_fail flags env evd rigidonly v t c1 with NoCoercion -> match EConstr.kind evd (whd_all env evd t), @@ -502,11 +513,11 @@ let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 = (* has type forall (x:u1), u2 (with v' recursively obtained) *) (* Note: we retype the term because template polymorphism may have *) (* weakened its type *) - let name = match name with + let name = map_annot (function | Anonymous -> Name Namegen.default_dependent_ident - | _ -> name in + | na -> na) name in let open Context.Rel.Declaration in - let env1 = push_rel (LocalAssum (name,u1)) env in + let env1 = push_rel (LocalAssum (name,u1)) env in let (evd', v1) = inh_conv_coerce_to_fail ?loc env1 evd rigidonly (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in @@ -516,14 +527,14 @@ let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 = | None -> subst_term evd' v1 t2 | Some v2 -> Retyping.get_type_of env1 evd' v2 in let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in - (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') + (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) -let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly env evd cj t = +let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd cj t = let (evd', val') = try - inh_conv_coerce_to_fail ?loc env evd rigidonly (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (best_failed_evd,e) -> try if program_mode then @@ -545,15 +556,14 @@ let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly env evd cj t let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) -let inh_conv_coerce_to ?loc ~program_mode resolve_tc = - inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false - -let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc = - inh_conv_coerce_to_gen ~program_mode resolve_tc ?loc true +let inh_conv_coerce_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = + inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env evd +let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = + inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc true flags env evd -let inh_conv_coerces_to ?loc env evd t t' = +let inh_conv_coerces_to ?loc env evd ?(flags=default_flags_of env) t t' = try - fst (inh_conv_coerce_to_fail ?loc env evd true None t t') + fst (inh_conv_coerce_to_fail ?loc env evd ~flags true None t t') with NoCoercion -> evd (* Maybe not enough information to unify *) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index a941391125..43d4059785 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -45,17 +45,21 @@ val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool -> a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable. resolve_tc=false disables resolving type classes (as the last resort before failing) *) + val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool -> - env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment + env -> evar_map -> ?flags:Evarconv.unify_flags -> + unsafe_judgment -> types -> evar_map * unsafe_judgment val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool -> - env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment + env -> evar_map -> ?flags:Evarconv.unify_flags -> + unsafe_judgment -> types -> evar_map * unsafe_judgment (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; it fails if no coercion exists *) val inh_conv_coerces_to : ?loc:Loc.t -> - env -> evar_map -> types -> types -> evar_map + env -> evar_map -> ?flags:Evarconv.unify_flags -> + types -> types -> evar_map (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 94257fedd7..bc083ed9d9 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -14,6 +14,7 @@ open CErrors open Util open Names open Constr +open Context open Globnames open Termops open Term @@ -70,7 +71,7 @@ let constrain sigma n (ids, m) ((names,seen as names_seen), terms as subst) = (names_seen, Id.Map.add n (ids, m) terms) let add_binders na1 na2 binding_vars ((names,seen), terms as subst) = - match na1, na2 with + match na1, na2.binder_name with | Name id1, Name id2 when Id.Set.mem id1 binding_vars -> if Id.Map.mem id1 names then let () = Glob_ops.warn_variable_collision id1 in @@ -94,7 +95,7 @@ let rec build_lambda sigma vars ctx m = match vars with let (na, t, suf) = match suf with | [] -> assert false | (_, id, t) :: suf -> - (Name id, t, suf) + (map_annot Name.mk_name id, t, suf) in (* Check that the abstraction is legal by generating a transitive closure of its dependencies. *) @@ -178,11 +179,12 @@ let make_renaming ids = function | _ -> dummy_constr let push_binder na1 na2 t ctx = - let id2 = match na2 with - | Name id2 -> id2 - | Anonymous -> - let avoid = Id.Set.of_list (List.map pi2 ctx) in - Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in + let id2 = map_annot (function + | Name id2 -> id2 + | Anonymous -> + let avoid = Id.Set.of_list (List.map (fun (_,id,_) -> id.binder_name) ctx) in + Namegen.next_ident_away Namegen.default_non_dependent_ident avoid) na2 + in (na1, id2, t) :: ctx (* This is an optimization of the main pattern-matching which shares @@ -341,19 +343,19 @@ let matches_core env sigma allow_bound_rels sorec ctx env subst c1 c2 | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) + sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> - sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) + sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) -> - sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) + sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2 | PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) -> - sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) + 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'|]) -> diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 99cd89cc2a..ac7c3d30d5 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -13,6 +13,7 @@ open CErrors open Util open Names open Constr +open Context open Term open EConstr open Vars @@ -40,9 +41,12 @@ let print_evar_arguments = ref false let add_name na b t (nenv, env) = let open Context.Rel.Declaration in + (* Is this just a dummy? Be careful, printing doesn't always give us + a correct env. *) + let r = Sorts.Relevant in add_name na nenv, push_rel (match b with - | None -> LocalAssum (na,t) - | Some b -> LocalDef (na,b,t) + | None -> LocalAssum (make_annot na r,t) + | Some b -> LocalDef (make_annot na r,b,t) ) env @@ -202,11 +206,11 @@ let computable sigma p k = let lookup_name_as_displayed env sigma t s = let rec lookup avoid n c = match EConstr.kind sigma c with | Prod (name,_,c') -> - (match compute_displayed_name_in sigma RenamingForGoal avoid name c' with + (match compute_displayed_name_in sigma RenamingForGoal avoid name.binder_name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | LetIn (name,_,_,c') -> - (match compute_displayed_name_in sigma RenamingForGoal avoid name c' with + (match compute_displayed_name_in sigma RenamingForGoal avoid name.binder_name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | Cast (c,_,_) -> lookup avoid n c @@ -216,7 +220,7 @@ let lookup_name_as_displayed env sigma t s = let lookup_index_as_renamed env sigma t n = let rec lookup n d c = match EConstr.kind sigma c with | Prod (name,_,c') -> - (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name c' with + (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name.binder_name c' with (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if Int.equal n 0 then @@ -226,7 +230,7 @@ let lookup_index_as_renamed env sigma t n = else lookup (n-1) (d+1) c') | LetIn (name,_,_,c') -> - (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name c' with + (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name.binder_name c' with | (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if Int.equal n 0 then @@ -342,9 +346,9 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = | b::tags -> let na,c,f,body,t = match EConstr.kind sigma (strip_outer_cast sigma c), b with - | Lambda (na,t,c),false -> na,c,compute_displayed_let_name_in,None,Some t - | LetIn (na,b,t,c),true -> - na,c,compute_displayed_name_in,Some b,Some t + | Lambda (na,t,c),false -> na.binder_name,c,compute_displayed_let_name_in,None,Some t + | LetIn (na,b,t,c),true -> + na.binder_name,c,compute_displayed_name_in,Some b,Some t | _, false -> Name default_dependent_ident,(applist (lift 1 c, [mkRel 1])), compute_displayed_name_in,None,None @@ -490,19 +494,16 @@ let rec share_names detype n l avoid env sigma c t = match EConstr.kind sigma c, EConstr.kind sigma t with (* factorize even when not necessary to have better presentation *) | Lambda (na,t,c), Prod (na',t',c') -> - let na = match (na,na') with - Name _, _ -> na - | _, Name _ -> na' - | _ -> na in + let na = Nameops.Name.pick_annot na na' in let t' = detype avoid env sigma t in - let id = next_name_away na avoid in + let id = next_name_away na.binder_name avoid in let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in share_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' (* May occur for fix built interactively *) | LetIn (na,b,t',c), _ when n > 0 -> let t'' = detype avoid env sigma t' in let b' = detype avoid env sigma b in - let id = next_name_away na avoid in + let id = next_name_away na.binder_name avoid in let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in share_names detype n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) (* Only if built with the f/n notation or w/o let-expansion in types *) @@ -511,7 +512,7 @@ let rec share_names detype n l avoid env sigma c t = (* If it is an open proof: we cheat and eta-expand *) | _, Prod (na',t',c') when n > 0 -> let t'' = detype avoid env sigma t' in - let id = next_name_away na' avoid in + let id = next_name_away na'.binder_name avoid in let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in let appc = mkApp (lift 1 c,[|mkRel 1|]) in share_names detype (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' @@ -549,7 +550,7 @@ let detype_fix detype avoid env sigma (vn,_ as nvn) (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left2 (fun (avoid, env, l) na ty -> - let id = next_name_away na avoid in + let id = next_name_away na.binder_name avoid in (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) (avoid, env, []) names tys in let n = Array.length tys in @@ -565,7 +566,7 @@ let detype_cofix detype avoid env sigma n (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left2 (fun (avoid, env, l) na ty -> - let id = next_name_away na avoid in + let id = next_name_away na.binder_name avoid in (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) (avoid, env, []) names tys in let ntys = Array.length tys in @@ -597,6 +598,7 @@ let detype_universe sigma u = Univ.Universe.map fn u let detype_sort sigma = function + | SProp -> GSProp | Prop -> GProp | Set -> GSet | Type u -> @@ -702,9 +704,9 @@ and detype_r d flags avoid env sigma t = match decl with | LocalDef _ -> true | LocalAssum (id,_) -> - try let n = List.index Name.equal (Name id) (fst env) in + try let n = List.index Name.equal (Name id.binder_name) (fst env) in isRelN sigma n c - with Not_found -> isVarId sigma id c + with Not_found -> isVarId sigma id.binder_name c in let id,l = try @@ -765,11 +767,11 @@ and detype_eqn d (lax,isgoal as flags) avoid env sigma constr construct_nargs br [DAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], detype d flags avoid env sigma b) | Lambda (x,t,b), false::l -> - let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in + let pat,new_avoid,new_env,new_ids = make_pat x.binder_name avoid env b None t ids in buildrec new_ids (pat::patlist) new_avoid new_env l b | LetIn (x,b,t,b'), true::l -> - let pat,new_avoid,new_env,new_ids = make_pat x avoid env b' (Some b) t ids in + let pat,new_avoid,new_env,new_ids = make_pat x.binder_name avoid env b' (Some b) t ids in buildrec new_ids (pat::patlist) new_avoid new_env l b' | Cast (c,_,_), l -> (* Oui, il y a parfois des cast *) @@ -791,7 +793,7 @@ and detype_eqn d (lax,isgoal as flags) avoid env sigma constr construct_nargs br in buildrec Id.Set.empty [] avoid env construct_nargs branch -and detype_binder d (lax,isgoal as flags) bk avoid env sigma na body ty c = +and detype_binder d (lax,isgoal as flags) bk avoid env sigma {binder_name=na} body ty c = let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in let na',avoid' = match bk with | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c @@ -827,7 +829,7 @@ let detype_rel_context d ?(lax=false) where avoid env sigma sign = (RenamingElsewhereFor (fst env,c)) avoid na c in let b = match decl with | LocalAssum _ -> None - | LocalDef (_,b,_) -> Some b + | LocalDef (_,b,_) -> Some b in let b' = Option.map (detype d (lax,false) avoid env sigma) b in let t' = detype d (lax,false) avoid env sigma t in @@ -864,7 +866,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = (* spiwack: I'm not sure it is the right thing to do, but I'm computing the detyping environment like [Printer.pr_constr_under_binders_env] does. *) - let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in + let assums = List.map (fun id -> LocalAssum (make_annot (Name id) Sorts.Relevant,(* dummy *) mkProp)) b in let env = push_rel_context assums env in DAst.get (detype Now ?lax isgoal avoid env sigma c) (* if [id] is bound to a [closed_glob_constr]. *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index bb163ddaee..28a97bb91a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -15,6 +15,7 @@ open Constr open Termops open Environ open EConstr +open Context open Vars open Reduction open Reductionops @@ -24,14 +25,28 @@ open Evardefine open Evarsolve open Evd open Pretype_errors -open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -type unify_fun = TransparentState.t -> +type unify_flags = Evarsolve.unify_flags + +type unify_fun = unify_flags -> env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result +let default_transparent_state env = TransparentState.full +(* Conv_oracle.get_transp_state (Environ.oracle env) *) + +let default_flags_of ?(subterm_ts=TransparentState.empty) ts = + { modulo_betaiota = true; + open_ts = ts; closed_ts = ts; subterm_ts; + frozen_evars = Evar.Set.empty; with_cs = true; + allow_K_at_toplevel = true } + +let default_flags env = + let ts = default_transparent_state env in + default_flags_of ts + let debug_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; @@ -42,6 +57,16 @@ let () = Goptions.(declare_bool_option { optwrite = (fun a -> debug_unification:=a); }) +let debug_ho_unification = ref (false) +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = + "Print higher-order unification debug information"; + optkey = ["Debug";"HO";"Unification"]; + optread = (fun () -> !debug_ho_unification); + optwrite = (fun a -> debug_ho_unification:=a); +}) + (*******************************************) (* Functions to deal with impossible cases *) (*******************************************) @@ -54,8 +79,8 @@ let impossible_default_case env = let coq_unit_judge = let open Environ in let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in - let na1 = Name (Id.of_string "A") in - let na2 = Name (Id.of_string "H") in + let na1 = make_annot (Name (Id.of_string "A")) Sorts.Relevant in + let na2 = make_annot (Name (Id.of_string "H")) Sorts.Relevant in fun env -> match impossible_default_case env with | Some (id, type_of_id, ctx) -> @@ -63,7 +88,7 @@ let coq_unit_judge = | None -> (* In case the constants id/ID are not defined *) Environ.make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) - (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), + (mkProd (na1,mkProp,mkArrow (mkRel 1) Sorts.Relevant (mkRel 2))), Univ.ContextSet.empty let unfold_projection env evd ts p c = @@ -101,42 +126,106 @@ type flex_kind_of_term = | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *) | Flexible of EConstr.existential -let flex_kind_of_term ts env evd c sk = +let is_frozen flags (evk, _) = Evar.Set.mem evk flags.frozen_evars + +let flex_kind_of_term flags env evd c sk = match EConstr.kind evd c with | LetIn _ | Rel _ | Const _ | Var _ | Proj _ -> - Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c) - | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c - | Evar ev -> Flexible ev + Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term flags.open_ts env evd c) + | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> + if flags.modulo_betaiota then MaybeFlexible c + else Rigid + | Evar ev -> + if is_frozen flags ev then Rigid + else Flexible ev | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ -> Rigid | Meta _ -> Rigid | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) | Cast _ | App _ | Case _ -> assert false -let apprec_nohdbeta ts env evd c = +let apprec_nohdbeta flags env evd c = let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in - if Stack.not_purely_applicative sk + if flags.modulo_betaiota && Stack.not_purely_applicative sk then Stack.zip evd (fst (whd_betaiota_deltazeta_for_iota_state - ts env evd Cst_stack.empty appr)) + flags.open_ts env evd Cst_stack.empty appr)) else c let position_problem l2r = function | CONV -> None | CUMUL -> Some l2r -let occur_rigidly (evk,_ as ev) evd t = +(* [occur_rigidly ev evd t] tests if the evar ev occurs in a rigid + context in t. Precondition: t has a rigid head and is not reducible. + + That function is an under approximation of occur-check, it can return + false even if the occur-check would succeed on the normal form. This + means we might postpone unsolvable constraints which will ultimately + result in an occur-check after reductions. If it returns true, we + know that the occur-check would also return true on the normal form. + + [t] is assumed to have a rigid head, which can + appear under a elimination context (e.g. application, match or projection). + + In the inner recursive function, the result indicates if the term is + rigid (irreducible), normal (succession of constructors) or + potentially reducible. For applications, this means than an + occurrence of the evar in arguments should be looked at to find an + occur-check if the head is rigid or normal. For inductive + eliminations, only an occurrence in a rigid context of the + discriminee counts as a rigid occurrence overall, not a normal + occurrence which might disappear after reduction. *) + +type result = Rigid of bool | Normal of bool | Reducible + +let rigid_normal_occ = function Rigid b -> b | Normal b -> b | _ -> false + +let occur_rigidly flags env evd (evk,_) t = let rec aux t = match EConstr.kind evd t with - | App (f, c) -> if aux f then Array.exists aux c else false - | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ | Int _ -> true - | Proj (p, c) -> not (aux c) - | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false + | App (f, c) -> + (match aux f with + | Rigid b -> Rigid (b || Array.exists (fun x -> rigid_normal_occ (aux x)) c) + | Normal b -> Normal (b || Array.exists (fun x -> rigid_normal_occ (aux x)) c) + | Reducible -> Reducible) + | Construct _ -> Normal false + | Ind _ | Sort _ -> Rigid false + | Proj (p, c) -> + let cst = Projection.constant p in + let rigid = not (TransparentState.is_transparent_constant flags.open_ts cst) in + if rigid then aux c + else (* if the evar appears rigidly in c then this elimination + cannot reduce and we have a rigid occurrence, otherwise + we don't know. *) + (match aux c with + | Rigid _ as res -> res + | Normal b -> Reducible + | Reducible -> Reducible) + | Evar (evk',l as ev) -> + if Evar.equal evk evk' then Rigid true + else if is_frozen flags ev then + Rigid (Array.exists (fun x -> rigid_normal_occ (aux x)) l) + else Reducible | Cast (p, _, _) -> aux p - | Lambda _ | LetIn _ -> false - | Const _ -> false - | Prod (_, b, t) -> ignore(aux b || aux t); true - | Rel _ | Var _ -> false - | Case (_,_,c,_) -> if eq_constr evd (mkEvar ev) c then raise Occur else false - in try ignore(aux t); false with Occur -> true + | Lambda (na, t, b) -> aux b + | LetIn (na, _, _, b) -> aux b + | Const (c,_) -> + if TransparentState.is_transparent_constant flags.open_ts c then Reducible + else Rigid false + | Prod (_, b, t) -> + let b' = aux b and t' = aux t in + if rigid_normal_occ b' || rigid_normal_occ t' then Rigid true + else Reducible + | Rel _ | Var _ -> Reducible + | Case (_,_,c,_) -> + (match aux c with + | Rigid b -> Rigid b + | _ -> Reducible) + | Meta _ | Fix _ | CoFix _ | Int _ -> Reducible + in + match aux t with + | Rigid b -> b + | Normal b -> b + | Reducible -> false (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose the problem (t1 stack1) = (t2 stack2) into a problem @@ -163,8 +252,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let canon_s,sk2_effective = try match EConstr.kind sigma t2 with - Prod (_,a,b) -> (* assert (l2=[]); *) - let _, a, b = destProd sigma t2 in + Prod (_,a,b) -> (* assert (l2=[]); *) + let _, a, b = destProd sigma t2 in if noccurn sigma 1 b then lookup_canonical_conversion (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) @@ -365,7 +454,21 @@ let compare_cumulative_instances evd variances u u' = Success evd | Inr p -> UnifFailure (evd, UnifUnivInconsistency p) -let rec evar_conv_x ts env evd pbty term1 term2 = +let conv_fun f flags on_types = + let typefn env evd pbty term1 term2 = + let flags = { (default_flags env) with + with_cs = flags.with_cs; + frozen_evars = flags.frozen_evars } + in f flags env evd pbty term1 term2 + in + let termfn env evd pbty term1 term2 = + f flags env evd pbty term1 term2 + in + match on_types with + | TypeUnification -> typefn + | TermUnification -> termfn + +let rec evar_conv_x flags env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in (* Maybe convertible but since reducing can erase evars which [evar_apprec] @@ -374,7 +477,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( let e = - match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with + match infer_conv ~catch_incon:false ~pb:pbty ~ts:flags.closed_ts env evd term1 term2 with | Some evd -> Success evd | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)) | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) @@ -389,30 +492,30 @@ let rec evar_conv_x ts env evd pbty term1 term2 = | None -> (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) - let term1 = apprec_nohdbeta (fst ts) env evd term1 in - let term2 = apprec_nohdbeta (fst ts) env evd term2 in + let term1 = apprec_nohdbeta flags env evd term1 in + let term2 = apprec_nohdbeta flags env evd term2 in let default () = - evar_eqappr_x ts env evd pbty + evar_eqappr_x flags env evd pbty (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty) (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty) in begin match EConstr.kind evd term1, EConstr.kind evd term2 with - | Evar ev, _ when Evd.is_undefined evd (fst ev) -> - (match solve_simple_eqn (evar_conv_x ts) env evd - (position_problem true pbty,ev, term2) with + | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> + (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd + (position_problem true pbty,ev,term2) with | UnifFailure (_,OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) - | _, Evar ev when Evd.is_undefined evd (fst ev) -> - (match solve_simple_eqn (evar_conv_x ts) env evd - (position_problem false pbty,ev, term1) with + | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> + (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd + (position_problem false pbty,ev,term1) with | UnifFailure (_, OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) | _ -> default () end -and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty +and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) @@ -423,18 +526,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Some l1' -> (* Miller-Pfenning's patterns unification *) let t2 = tM in let t2 = solve_pattern_eqn env evd l1' t2 in - solve_simple_eqn (evar_conv_x ts) env evd + solve_simple_eqn (conv_fun evar_conv_x) flags env evd (position_problem on_left 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 not_only_app = Stack.not_purely_applicative skO in - match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with + 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) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) + 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) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) - |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO + 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' = @@ -443,12 +546,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let c = nf_evar evd c1 in let env' = push_rel (RelDecl.LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state - (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in + flags.open_ts env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in - if onleft then evar_eqappr_x ts env' evd CONV out1 out2 - else evar_eqappr_x ts env' evd CONV out2 out1 + if onleft then evar_eqappr_x flags env' evd CONV out1 out2 + else evar_eqappr_x flags env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = let check_strict evd u u' = @@ -504,12 +607,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_and evd [(fun i -> try compare_heads i with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')] in - let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM = + let consume on_left (_, 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 + 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 not_only_app = Stack.not_purely_applicative skM in - let f1 i = match Stack.list_of_app_stack skF with | None -> quick_fail evd | Some lF -> @@ -518,17 +625,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (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 - and consume (termF,skF as apprF) (termM,skM as apprM) i = - if not (Stack.is_empty skF && Stack.is_empty skM) then - consume_stack on_left apprF apprM i - else quick_fail i - and delta i = - switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) - (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i cstsM (vM,skM)) + ev lF tM i + in + let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM = + let switch f a b = if on_left then f a b else f b a in + let delta i = + switch (evar_eqappr_x flags env i pbty) (apprF,cstsF) + (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i cstsM (vM,skM)) in - let default i = ise_try i [f1; consume apprF apprM; delta] + let default i = ise_try i [miller on_left ev apprF apprM; + consume on_left apprF apprM; + delta] in match EConstr.kind evd termM with | Proj (p, c) when not (Stack.is_empty skF) -> @@ -543,13 +650,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty try let termM' = Retyping.expand_projection env evd p c [] in let apprM', cstsM' = - whd_betaiota_deltazeta_for_iota_state - (fst ts) env evd cstsM (termM',skM) + whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd cstsM (termM',skM) in let delta' i = - switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM') + switch (evar_eqappr_x flags env i pbty) (apprF,cstsF) (apprM',cstsM') in - fun i -> ise_try i [f1; consume apprF apprM'; delta'] + fun i -> ise_try i [miller on_left ev apprF apprM'; + consume on_left apprF apprM'; delta'] with Retyping.RetypeError _ -> (* Happens thanks to w_unify building ill-typed terms *) default @@ -563,7 +670,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty 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 ts env evd skR u skF termF + | Construct u -> eta_constructor flags env evd skR u skF termF | _ -> UnifFailure (evd,NotSameHead) in match Stack.list_of_app_stack skF with @@ -571,12 +678,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [consume_stack on_left apprF apprR; eta] | Some lF -> let tR = Stack.zip evd apprR in - miller_pfenning on_left - (fun () -> - ise_try evd - [eta;(* Postpone the use of an heuristic *) - (fun i -> - if not (occur_rigidly ev i tR) then + miller_pfenning on_left + (fun () -> + ise_try evd + [eta;(* Postpone the use of an heuristic *) + (fun i -> + if not (occur_rigidly flags env i ev tR) then let i,tF = if isRel i tR || isVar i tR then (* Optimization so as to generate candidates *) @@ -585,95 +692,111 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else i,Stack.zip evd apprF in switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) - tF tR - else + tF tR + else UnifFailure (evd,OccurCheck (fst ev,tR)))]) - ev lF tR evd + ev lF tR evd + in + let first_order env i t1 t2 sk1 sk2 = + (* Try first-order unification *) + match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with + | None, Success i' -> + (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) + (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) + let ev1' = whd_evar i' t1 in + if isEvar i' ev1' then + solve_simple_eqn (conv_fun evar_conv_x) flags env i' + (position_problem true pbty,destEvar i' ev1',term2) + else + evar_eqappr_x flags env evd pbty + ((ev1', sk1), csts1) ((term2, sk2), csts2) + | Some (r,[]), Success i' -> + (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) + (* we now unify r[?ev1] and ?ev2 *) + let ev2' = whd_evar i' t2 in + if isEvar i' ev2' then + solve_simple_eqn (conv_fun evar_conv_x) flags env i' + (position_problem false pbty,destEvar i' ev2',Stack.zip i' (term1,r)) + else + evar_eqappr_x flags env evd pbty + ((ev2', sk1), csts1) ((term2, sk2), csts2) + | Some ([],r), Success i' -> + (* Symmetrically *) + (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) + (* we now unify ?ev1 and r[?ev2] *) + let ev1' = whd_evar i' t1 in + 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 + ((ev1', sk1), csts1) ((term2, sk2), csts2) + | None, (UnifFailure _ as x) -> + (* sk1 and sk2 have no common outer part *) + if Stack.not_purely_applicative sk2 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid true (destEvar evd t1) appr1 appr2 + else + if Stack.not_purely_applicative sk1 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid false (destEvar evd t2) appr2 appr1 + else + (* We could instead try Miller unification, then + postpone to see if other equations help, as in: + [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *) + x + | Some _, Success _ -> + (* sk1 and sk2 have a common outer part *) + if Stack.not_purely_applicative sk2 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid true (destEvar evd t1) appr1 appr2 + else + if Stack.not_purely_applicative sk1 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid false (destEvar evd t2) appr2 appr1 + 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)] *) + UnifFailure (i,NotSameArgSize) + | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in - match (flex_kind_of_term (fst ts) env evd term1 sk1, - flex_kind_of_term (fst ts) env evd term2 sk2) with - | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> + 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] *) - let f1 i = - (* Try first-order unification *) - match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with - | None, Success i' -> - (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) - (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) - let ev1' = whd_evar i' (mkEvar ev1) in - if isEvar i' ev1' then - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar i' ev1', term2) - else - evar_eqappr_x ts env evd pbty - ((ev1', sk1), csts1) ((term2, sk2), csts2) - | Some (r,[]), Success i' -> - (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) - (* we now unify r[?ev1] and ?ev2 *) - let ev2' = whd_evar i' (mkEvar ev2) in - if isEvar i' ev2' then - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem false pbty,destEvar i' ev2',Stack.zip evd (term1,r)) - else - evar_eqappr_x ts env evd pbty - ((ev2', sk1), csts1) ((term2, sk2), csts2) - | Some ([],r), Success i' -> - (* Symmetrically *) - (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) - (* we now unify ?ev1 and r[?ev2] *) - let ev1' = whd_evar i' (mkEvar ev1) in - if isEvar i' ev1' then - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar i' ev1',Stack.zip evd (term2,r)) - else evar_eqappr_x ts env evd pbty - ((ev1', sk1), csts1) ((term2, sk2), csts2) - | None, (UnifFailure _ as x) -> - (* sk1 and sk2 have no common outer part *) - if Stack.not_purely_applicative sk2 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid true ev1 appr1 appr2 - else - if Stack.not_purely_applicative sk1 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid false ev2 appr2 appr1 - else - (* We could instead try Miller unification, then - postpone to see if other equations help, as in: - [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *) - x - | Some _, Success _ -> - (* sk1 and sk2 have a common outer part *) - if Stack.not_purely_applicative sk2 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid true ev1 appr1 appr2 - else - if Stack.not_purely_applicative sk1 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid false ev2 appr2 appr1 - 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)] *) - UnifFailure (i,NotSameArgSize) - | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") - + let f1 i = first_order env i term1 term2 sk1 sk2 and f2 i = if Evar.equal sp1 sp2 then - match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with + match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with |None, Success i' -> - Success (solve_refl (fun env i pbty a1 a2 -> - is_success (evar_conv_x ts env i pbty a1 a2)) + Success (solve_refl (fun flags p env i pbty a1 a2 -> + let flags = + match p with + | TypeUnification -> default_flags env + | TermUnification -> flags + in + is_success (evar_conv_x flags env i pbty a1 a2)) flags env i' (position_problem true pbty) sp1 al1 al2) |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (i,NotSameArgSize) else UnifFailure (i,NotSameHead) - in - ise_try evd [f1; f2] + and f3 i = miller true (sp1,al1) appr1 appr2 i + and f4 i = miller false (sp2,al2) appr2 appr1 i + and f5 i = + (* We ensure failure of consuming the stacks does not + propagate an error about unification of the stacks while + the heads themselves cannot be unified, so we return + NotSameHead. *) + match consume true appr1 appr2 i with + | Success _ as x -> x + | UnifFailure _ -> quick_fail i + in + ise_try evd [f1; f2; f3; f4; f5] | Flexible ev1, MaybeFlexible v2 -> flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2 @@ -687,31 +810,31 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let f1 i = (* FO *) ise_and i [(fun i -> ise_try i - [(fun i -> evar_conv_x ts env i CUMUL t1 t2); - (fun i -> evar_conv_x ts env i CUMUL t2 t1)]); - (fun i -> evar_conv_x ts env i CONV b1 b2); + [(fun i -> evar_conv_x flags env i CUMUL t1 t2); + (fun i -> evar_conv_x flags env i CUMUL t2 t1)]); + (fun i -> evar_conv_x flags env i CONV b1 b2); (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in - let na = Nameops.Name.pick na1 na2 in - evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] - and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) - and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2) - in evar_eqappr_x ts env i pbty out1 out2 + let na = Nameops.Name.pick_annot na1 na2 in + evar_conv_x flags (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] + and f2 i = + let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts1 (v1,sk1) + and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts2 (v2,sk2) + in evar_eqappr_x flags env i pbty out1 out2 in ise_try evd [f1; f2] | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' -> let f1 i = ise_and i - [(fun i -> evar_conv_x ts env i CONV c c'); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] + [(fun i -> evar_conv_x flags env i CONV c c'); + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) - and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2) - in evar_eqappr_x ts env i pbty out1 out2 + let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts1 (v1,sk1) + and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts2 (v2,sk2) + in evar_eqappr_x flags env i pbty out1 out2 in ise_try evd [f1; f2] @@ -723,7 +846,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in (match res with | Some (f1,args1) -> - evar_eqappr_x ts env evd pbty ((f1,Stack.append_app args1 sk1),csts1) + evar_eqappr_x flags env evd pbty ((f1,Stack.append_app args1 sk1),csts1) (appr2,csts2) | None -> UnifFailure (evd,NotSameHead)) @@ -734,7 +857,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in (match res with | Some (f2,args2) -> - evar_eqappr_x ts env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2) + evar_eqappr_x flags env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2) | None -> UnifFailure (evd,NotSameHead)) | _, _ -> @@ -751,13 +874,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty try Success (Evd.add_universe_constraints i univs) with UniversesDiffer -> UnifFailure (i,NotSameHead) | Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] | None -> UnifFailure (i,NotSameHead) and f2 i = (try - if not (snd ts) then raise Not_found - else conv_record ts env i + if not flags.with_cs then raise Not_found + else conv_record flags env i (try check_conv_record env i appr1 appr2 with Not_found -> check_conv_record env i appr2 appr1) with Not_found -> UnifFailure (i,NoCanonicalStructure)) @@ -775,7 +898,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Lambda _ -> assert (match args with [] -> true | _ -> false); true | LetIn (_,b,_,c) -> is_unnamed (fst (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i Cst_stack.empty (subst1 b c, args))) + flags.open_ts env i Cst_stack.empty (subst1 b c, args))) | Fix _ -> true (* Partially applied fix can be the result of a whd call *) | Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args | Case _ | App _| Cast _ -> assert false in @@ -783,20 +906,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let applicative_stack = fst (Stack.strip_app sk2) in is_unnamed (fst (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i Cst_stack.empty (v2, applicative_stack))) in + flags.open_ts env i Cst_stack.empty (v2, applicative_stack))) in let rhs_is_already_stuck = rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in if (EConstr.isLambda i term1 || rhs_is_already_stuck) && (not (Stack.not_purely_applicative sk1)) then - evar_eqappr_x ~rhs_is_already_stuck ts env i pbty + evar_eqappr_x ~rhs_is_already_stuck flags env i pbty (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) + flags.open_ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) (appr2,csts2) else - evar_eqappr_x ts env i pbty (appr1,csts1) + evar_eqappr_x flags env i pbty (appr1,csts1) (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) + flags.open_ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) in ise_try evd [f1; f2; f3] end @@ -804,13 +927,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 -> let (na1,c1,c'1) = EConstr.destLambda evd term1 in let (na2,c2,c'2) = EConstr.destLambda evd term2 in - assert app_empty; ise_and evd - [(fun i -> evar_conv_x ts env i CONV c1 c2); + [(fun i -> evar_conv_x flags env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.Name.pick na1 na2 in - evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] + let na = Nameops.Name.pick_annot na1 na2 in + evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2); + (* When in modulo_betaiota = false case, lambda's are not reduced *) + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1 @@ -818,13 +942,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | MaybeFlexible v1, Rigid -> let f3 i = (try - if not (snd ts) then raise Not_found - else conv_record ts env i (check_conv_record env i appr1 appr2) + if not flags.with_cs then raise Not_found + else conv_record flags env i (check_conv_record env i appr1 appr2) with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = - evar_eqappr_x ts env i pbty + evar_eqappr_x flags env i pbty (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) + flags.open_ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) (appr2,csts2) in ise_try evd [f3; f4] @@ -832,13 +956,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Rigid, MaybeFlexible v2 -> let f3 i = (try - if not (snd ts) then raise Not_found - else conv_record ts env i (check_conv_record env i appr2 appr1) + if not flags.with_cs then raise Not_found + else conv_record flags env i (check_conv_record env i appr2 appr1) with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = - evar_eqappr_x ts env i pbty (appr1,csts1) + evar_eqappr_x flags env i pbty (appr1,csts1) (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) + flags.open_ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) in ise_try evd [f3; f4] @@ -865,22 +989,22 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty UnifFailure (evd,UnifUnivInconsistency p) | e when CErrors.noncritical e -> UnifFailure (evd,NotSameHead)) - | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> + | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> ise_and evd - [(fun i -> evar_conv_x ts env i CONV c1 c2); + [(fun i -> evar_conv_x flags env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.Name.pick n1 n2 in - evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] + let na = Nameops.Name.pick_annot n1 n2 in + evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> if Int.equal x1 x2 then - exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2 + exact_ise_stack2 env evd (evar_conv_x flags) sk1 sk2 else UnifFailure (evd,NotSameHead) | Var var1, Var var2 -> if Id.equal var1 var2 then - exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2 + exact_ise_stack2 env evd (evar_conv_x flags) sk1 sk2 else UnifFailure (evd,NotSameHead) | Const _, Const _ @@ -889,49 +1013,59 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Int _, Int _ -> rigids env evd sk1 term1 sk2 term2 + | Evar (sp1,al1), Evar (sp2,al2) -> (* Frozen evars *) + if Evar.equal sp1 sp2 then + match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with + |None, Success i' -> + ise_array2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2 + |_, (UnifFailure _ as x) -> x + |Some _, _ -> UnifFailure (evd,NotSameArgSize) + else UnifFailure (evd,NotSameHead) + | Construct u, _ -> - eta_constructor ts env evd sk1 u sk2 term2 + eta_constructor flags env evd sk1 u sk2 term2 | _, Construct u -> - eta_constructor ts env evd sk2 u sk1 term1 + eta_constructor flags env evd sk2 u sk1 term1 - | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) + | 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 ise_and evd [ - (fun i -> ise_array2 i (fun i' -> evar_conv_x ts env i' CONV) tys1 tys2); - (fun i -> ise_array2 i (fun i' -> evar_conv_x ts (push_rec_types recdef1 env) i' CONV) bds1 bds2); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] + (fun i -> ise_array2 i (fun i' -> evar_conv_x flags env i' CONV) tys1 tys2); + (fun i -> ise_array2 i (fun i' -> evar_conv_x flags (push_rec_types recdef1 env) i' CONV) bds1 bds2); + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] else UnifFailure (evd, NotSameHead) - | CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) -> + | CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) -> if Int.equal i1 i2 then ise_and evd [(fun i -> ise_array2 i - (fun i -> evar_conv_x ts env i CONV) tys1 tys2); + (fun i -> evar_conv_x flags env i CONV) tys1 tys2); (fun i -> ise_array2 i - (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV) + (fun i -> evar_conv_x flags (push_rec_types recdef1 env) i CONV) bds1 bds2); (fun i -> exact_ise_stack2 env i - (evar_conv_x ts) sk1 sk2)] + (evar_conv_x flags) sk1 sk2)] else UnifFailure (evd,NotSameHead) | (Meta _, _) | (_, Meta _) -> - begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with + begin match ise_stack2 true env evd (evar_conv_x flags) sk1 sk2 with |_, (UnifFailure _ as x) -> x - |None, Success i' -> evar_conv_x ts env i' CONV term1 term2 - |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2')) + |None, Success i' -> evar_conv_x flags env i' CONV term1 term2 + |Some (sk1',sk2'), Success i' -> evar_conv_x flags env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2')) end - | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _), _ -> + | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _), _ -> UnifFailure (evd,NotSameHead) - - | (App _ | Cast _ | Case _ | Proj _), _ -> assert false - | (LetIn _| Evar _), _ -> assert false - | (Lambda _), _ -> assert false - + | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _) -> + UnifFailure (evd,NotSameHead) + | Case _, _ -> UnifFailure (evd,NotSameHead) + | Proj _, _ -> UnifFailure (evd,NotSameHead) + | (App _ | Cast _), _ -> assert false + | LetIn _, _ -> assert false end -and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) = +and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) = (* Tries to unify the states (proji params1 c1 | sk1) = (proji params2 (c (?xs:bs)) | sk2) @@ -962,7 +1096,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fun (i,ks,m,test) b -> if match n with Some n -> Int.equal m n | None -> false then let ty = Retyping.get_type_of env i t2 in - let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in + let test i = evar_conv_x flags env i CUMUL ty (substl ks b) in (i,t2::ks, m-1, test) else let dloc = Loc.tag Evar_kinds.InternalHole in @@ -974,20 +1108,20 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) ise_and evd' [(fun i -> exact_ise_stack2 env i - (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x)) + (fun env' i' cpb x1 x -> evar_conv_x flags env' i' cpb x1 (substl ks x)) params1 params); (fun i -> exact_ise_stack2 env i - (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u)) + (fun env' i' cpb u1 u -> evar_conv_x flags env' i' cpb u1 (substl ks u)) us2 us); - (fun i -> evar_conv_x trs env i CONV c1 app); - (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2); + (fun i -> evar_conv_x flags env i CONV c1 app); + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2); test; - (fun i -> evar_conv_x trs env i CONV h2 + (fun i -> evar_conv_x flags env i CONV h2 (fst (decompose_app_vect i (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) -and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = +and eta_constructor flags env evd sk1 ((ind, i), u) sk2 term2 = let open Declarations in let mib = lookup_mind (fst ind) env in match get_projections env ind with @@ -999,15 +1133,17 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let term = Stack.zip evd (term2,sk2) in List.map (fun p -> EConstr.mkProj (Projection.make p false, term)) (Array.to_list projs) in - exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1' + exact_ise_stack2 env evd (evar_conv_x { flags with with_cs = false}) l1' (Stack.append_app_list l2' Stack.empty) - with + with | Invalid_argument _ -> (* Stack.tail: partially applied constructor *) UnifFailure(evd,NotSameHead)) | _ -> UnifFailure (evd,NotSameHead) -let evar_conv_x ts = evar_conv_x (ts, true) +let evar_conv_x flags = evar_conv_x flags + +let evar_unify = conv_fun evar_conv_x (* Profiling *) let evar_conv_x = @@ -1018,25 +1154,26 @@ let evar_conv_x = let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () -let evar_conv_x ts = Hook.get evar_conv_hook_get ts +let evar_conv_x flags = Hook.get evar_conv_hook_get flags let set_evar_conv f = Hook.set evar_conv_hook_set f (* We assume here |l1| <= |l2| *) -let first_order_unification ts env evd (ev1,l1) (term2,l2) = +let first_order_unification flags env evd (ev1,l1) (term2,l2) = let (deb2,rest2) = Array.chop (Array.length l2-Array.length l1) l2 in ise_and evd (* First compare extra args for better failure message *) - [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1); + [(fun i -> ise_array2 i (fun i -> evar_conv_x flags env i CONV) rest2 l1); (fun i -> (* Then instantiate evar unless already done by unifying args *) let t2 = mkApp(term2,deb2) in if is_defined i (fst ev1) then - evar_conv_x ts env i CONV t2 (mkEvar ev1) + evar_conv_x flags env i CONV t2 (mkEvar ev1) else - solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))] + solve_simple_eqn ~choose:true ~imitate_defs:false + evar_unify flags env i (None,ev1,t2))] let choose_less_dependent_instance evk evd term args = let evi = Evd.find_undefined evd evk in @@ -1046,30 +1183,57 @@ let choose_less_dependent_instance evk evd term args = | [] -> None | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd) -let apply_on_subterm env evdref f c t = +type occurrence_match_test = + env -> evar_map -> constr -> + env -> evar_map -> int -> constr -> constr -> bool * evar_map + +type occurrence_selection = + | AtOccurrences of Locus.occurrences + | Unspecified of Abstraction.abstraction + +type occurrences_selection = + occurrence_match_test * occurrence_selection list + +let default_occurrence_selection = Unspecified Abstraction.Imitate + +let default_occurrence_test ~frozen_evars ts _ origsigma _ env sigma _ c pat = + let flags = { (default_flags_of ~subterm_ts:ts ts) with frozen_evars } in + match evar_conv_x flags env sigma CONV c pat with + | Success sigma -> true, sigma + | UnifFailure _ -> false, sigma + +let default_occurrences_selection ?(frozen_evars=Evar.Set.empty) ts n = + (default_occurrence_test ~frozen_evars ts, + List.init n (fun _ -> default_occurrence_selection)) + +let apply_on_subterm env evd fixedref f test c t = + let test = test env evd c in + let prc env evd = Termops.Internal.print_constr_env env evd in + let evdref = ref evd in let rec applyrec (env,(k,c) as acc) t = - (* By using eq_constr, we make an approximation, for instance, we *) - (* could also be interested in finding a term u convertible to t *) - (* such that c occurs in u *) - let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with - | None -> false - | Some cstr -> - try ignore (Evd.add_universe_constraints !evdref cstr); true - with UniversesDiffer -> false - in - if eq_constr c t then f k - else + if Evar.Set.exists (fun fixed -> occur_evar !evdref fixed t) !fixedref then match EConstr.kind !evdref t with - | Evar (evk,args) -> - let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in - let g decl a = if is_local_assum decl then applyrec acc a else a in - mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) - | _ -> - map_constr_with_binders_left_to_right !evdref - (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) - applyrec acc t + | Evar (ev, args) when Evar.Set.mem ev !fixedref -> t + | _ -> map_constr_with_binders_left_to_right !evdref + (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) + applyrec acc t + else + (if !debug_ho_unification then + Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t); + let b, evd = + try test env !evdref k c t + with e when CErrors.noncritical e -> assert false in + if b then (if !debug_ho_unification then Feedback.msg_debug (Pp.str "succeeded"); + let evd', t' = f !evdref k t in + evdref := evd'; t') + else ( + if !debug_ho_unification then Feedback.msg_debug (Pp.str "failed"); + map_constr_with_binders_left_to_right !evdref + (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) + applyrec acc t)) in - applyrec (env,(0,c)) t + let t' = applyrec (env,(0,c)) t in + !evdref, t' let filter_possible_projections evd c ty ctxt args = (* Since args in the types will be replaced by holes, we count the @@ -1114,117 +1278,284 @@ let set_solve_evars f = solve_evars := f * proposition from Dan Grayson] *) +let check_selected_occs env sigma c occ occs = + let notfound = + match occs with + | AtOccurrences occs -> + (match occs with + | Locus.AtLeastOneOccurrence -> occ == 1 + | Locus.AllOccurrences -> false + | Locus.AllOccurrencesBut l -> List.last l > occ + | Locus.OnlyOccurrences l -> List.last l > occ + | Locus.NoOccurrences -> false) + | Unspecified abstract -> false + in if notfound then + raise (PretypeError (env,sigma,NoOccurrenceFound (c,None))) + else () + exception TypingFailed of evar_map -let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = +let set_of_evctx l = + List.fold_left (fun s decl -> Id.Set.add (NamedDecl.get_id decl) s) Id.Set.empty l + +(** Weaken the existentials so that they can be typed in sign and raise + an error if the term otherwise mentions variables not bound in sign. *) +let thin_evars env sigma sign c = + let evdref = ref sigma in + let ctx = set_of_evctx sign in + let rec applyrec (env,acc) t = + match kind sigma t with + | Evar (ev, args) -> + let evi = Evd.find_undefined sigma ev in + let filter = Array.map (fun c -> Id.Set.subset (collect_vars sigma c) ctx) args in + let filter = Filter.make (Array.to_list filter) in + let candidates = Option.map (List.map EConstr.of_constr) (evar_candidates evi) in + let evd, ev = restrict_evar !evdref ev filter candidates in + evdref := evd; whd_evar !evdref t + | Var id -> + if not (Id.Set.mem id ctx) then raise (TypingFailed sigma) + else t + | _ -> + map_constr_with_binders_left_to_right !evdref + (fun d (env,acc) -> (push_rel d env, acc+1)) + applyrec (env,acc) t + in + let c' = applyrec (env,0) c in + (!evdref, c') + +let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = try let evi = Evd.find_undefined evd evk in + let evi = nf_evar_info evd evi in + let env_evar_unf = evar_env evi in let env_evar = evar_filtered_env evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - let instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in - + if !debug_ho_unification then + (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs); + Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar)); + let args = Array.map (nf_evar evd) args in + let vars = List.map NamedDecl.get_id ctxt in + let argsubst = List.map2 (fun id c -> (id, c)) vars (Array.to_list args) in + let instance = List.map mkVar vars in + let rhs = nf_evar evd rhs in + if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd); + (* Ensure that any progress made by Typing.e_solve_evars will not contradict + the solution we are trying to build here by adding the problem as a constraint. *) + let evd = Evarutil.add_unification_pb (CONV,env_rhs,mkEvar (evk,args),rhs) evd in + let prc env evd c = Termops.Internal.print_constr_env env evd c in let rec make_subst = function - | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> + | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> begin match occs with - | Some _ -> - user_err Pp.(str "Cannot force abstraction on identity instance.") - | None -> - make_subst (ctxt',l,occsl) + | AtOccurrences loc when not (Locusops.is_all_occurrences loc) -> + user_err Pp.(str "Cannot force abstraction on identity instance.") + | _ -> + make_subst (ctxt',l,occsl) end - | decl'::ctxt', c::l, occs::occsl -> - let id = NamedDecl.get_id decl' in + | decl'::ctxt', c::l, occs::occsl -> + let id = NamedDecl.get_annot decl' in let t = NamedDecl.get_type decl' in let evs = ref [] in - let ty = Retyping.get_type_of env_rhs evd c in - let filter' = filter_possible_projections evd c ty ctxt args in + let c = nf_evar evd c in + (* ty is in env_rhs now *) + let ty = replace_vars argsubst t in + let filter' = filter_possible_projections evd c (nf_evar evd ty) ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) - | _, _, [] -> [] - | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in - - let rec set_holes evdref rhs = function - | (id,_,c,cty,evsref,filter,occs)::subst -> - let set_var k = - match occs with - | Some Locus.AllOccurrences -> mkVar id - | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported") - | None -> - let evty = set_holes evdref cty subst in - let instance = Filter.filter_list filter instance in - let evd = !evdref in - let (evd, ev) = new_evar_instance sign evd evty ~filter instance in - evdref := evd; - evsref := (fst (destEvar !evdref ev),evty)::!evsref; - ev in - set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst - | [] -> rhs in + | _, _, [] -> [] + | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") + in + let fixed = ref Evar.Set.empty in + let rec set_holes env_rhs evd rhs = function + | (id,idty,c,cty,evsref,filter,occs)::subst -> + let c = nf_evar evd c in + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"set holes for: " ++ + prc env_rhs evd (mkVar id.binder_name) ++ spc () ++ + prc env_rhs evd c ++ str" in " ++ + prc env_rhs evd rhs); + let occ = ref 1 in + let set_var evd k inst = + let oc = !occ in + if !debug_ho_unification then + (Feedback.msg_debug Pp.(str"Found one occurrence"); + Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c)); + incr occ; + match occs with + | AtOccurrences occs -> + if Locusops.is_selected oc occs then evd, mkVar id.binder_name + else evd, inst + | Unspecified prefer_abstraction -> + let evd, evty = set_holes env_rhs evd cty subst in + let evty = nf_evar evd evty in + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++ + str" of type: " ++ prc env_evar evd evty ++ + str " for " ++ prc env_rhs evd c); + let instance = Filter.filter_list filter instance in + (* Allow any type lower than the variable's type as the + abstracted subterm might have a smaller type, which could be + crucial to make the surrounding context typecheck. *) + let evd, evty = + if isArity evd evty then + refresh_universes ~status:Evd.univ_flexible (Some true) + env_evar_unf evd evty + else evd, evty in + let (evd, ev) = new_evar_instance sign evd evty ~filter instance in + let evk = fst (destEvar evd ev) in + evsref := (evk,evty,inst,prefer_abstraction)::!evsref; + fixed := Evar.Set.add evk !fixed; + evd, ev + in + let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs'); + let () = check_selected_occs env_rhs evd c !occ occs in + let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in + set_holes env_rhs' evd rhs' subst + | [] -> evd, rhs in let subst = make_subst (ctxt,Array.to_list args,argoccs) in - let evd, rhs = - let evdref = ref evd in - let rhs = set_holes evdref rhs subst in - !evdref, rhs - in - + let evd, rhs' = set_holes env_rhs evd rhs subst in + let rhs' = nf_evar evd rhs' in + (* Thin evars making the term typable in env_evar *) + let evd, rhs' = thin_evars env_evar evd ctxt rhs' in (* We instantiate the evars of which the value is forced by typing *) - let evd,rhs = - try !solve_evars env_evar evd rhs + if !debug_ho_unification then + (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs'); + Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); + let evd,rhs' = + try !solve_evars env_evar evd rhs' with e when Pretype_errors.precatchable_exception e -> (* Could not revert all subterms *) raise (TypingFailed evd) in + let rhs' = nf_evar evd rhs' in + (* We instantiate the evars of which the value is forced by typing *) + if !debug_ho_unification then + (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs'); + Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); let rec abstract_free_holes evd = function - | (id,idty,c,_,evsref,_,_)::l -> - let rec force_instantiation evd = function - | (evk,evty)::evs -> - let evd = - if is_undefined evd evk then - (* We force abstraction over this unconstrained occurrence *) - (* and we use typing to propagate this instantiation *) - (* This is an arbitrary choice *) - let evd = Evd.define evk (mkVar id) evd in - match evar_conv_x ts env_evar evd CUMUL idty evty with - | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") - | Success evd -> - match reconsider_unif_constraints (evar_conv_x ts) evd with - | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") - | Success evd -> - evd - else - evd - in - force_instantiation evd evs - | [] -> - abstract_free_holes evd l - in - force_instantiation evd !evsref - | [] -> - let evd = - try Evarsolve.check_evar_instance evd evk rhs - (evar_conv_x TransparentState.full) - with IllTypedInstance _ -> raise (TypingFailed evd) - in - Evd.define evk rhs evd + | (id,idty,c,cty,evsref,_,_)::l -> + let id = id.binder_name in + let c = nf_evar evd c in + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"abstracting: " ++ + prc env_rhs evd (mkVar id) ++ spc () ++ + prc env_rhs evd c); + let rec force_instantiation evd = function + | (evk,evty,inst,abstract)::evs -> + let evk = Option.default evk (Evarutil.advance evd evk) in + let evd = + if is_undefined evd evk then + (* We try abstraction or concretisation for *) + (* this unconstrained occurrence *) + (* and we use typing to propagate this instantiation *) + (* We avoid making an arbitrary choice by leaving candidates *) + (* if both can work *) + let evi = Evd.find_undefined evd evk in + let vid = mkVar id in + let candidates = [inst; vid] in + try + let evd, ev = Evarutil.restrict_evar evd evk (Evd.evar_filter evi) (Some candidates) in + let evi = Evd.find evd ev in + (match evar_candidates evi with + | Some [t] -> + if not (noccur_evar env_rhs evd ev (EConstr.of_constr t)) then + raise (TypingFailed evd); + instantiate_evar evar_unify flags evd ev (EConstr.of_constr t) + | Some l when abstract = Abstraction.Abstract && + List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> + instantiate_evar evar_unify flags evd ev vid + | _ -> evd) + with e -> user_err (Pp.str "Cannot find an instance") + else + ((if !debug_ho_unification then + let evi = Evd.find evd evk in + let env = Evd.evar_env evi in + Feedback.msg_debug Pp.(str"evar is defined: " ++ + int (Evar.repr evk) ++ spc () ++ + prc env evd (match evar_body evi with Evar_defined c -> c + | Evar_empty -> assert false))); + evd) + in force_instantiation evd evs + | [] -> abstract_free_holes evd l + in force_instantiation evd !evsref + | [] -> + if Evd.is_defined evd evk then + (* Can happen due to dependencies: instantiating evars in the arguments of evk might + instantiate evk itself. *) + (if !debug_ho_unification then + begin + let evi = Evd.find evd evk in + let evenv = evar_env evi in + let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in + Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv evd body) + end; + evd) + else + try + let evi = Evd.find_undefined evd evk in + let evenv = evar_env evi in + let rhs' = nf_evar evd rhs' in + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++ + prc evenv evd rhs'); + (* solve_evars is not commuting with nf_evar, because restricting + an evar might provide a more specific type. *) + let evd, _ = !solve_evars evenv evd rhs' in + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs')); + let flags = default_flags_of TransparentState.full in + Evarsolve.instantiate_evar evar_unify flags evd evk rhs' + with IllTypedInstance _ -> raise (TypingFailed evd) in - abstract_free_holes evd subst, true + let evd = abstract_free_holes evd subst in + evd, true with TypingFailed evd -> evd, false -let second_order_matching_with_args ts env evd pbty ev l t = -(* - let evd,ev = evar_absorb_arguments env evd ev l in - let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in - let evd, b = second_order_matching ts env evd ev argoccs t in - if b then Success evd - else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) - if b then Success evd else - *) - let pb = (pbty,env,mkApp(mkEvar ev,l),t) in - UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) - -let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = - let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in - let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in +let default_evar_selection flags evd (ev,args) = + let evi = Evd.find_undefined evd ev in + let rec aux args abs = + match args, abs with + | _ :: args, a :: abs -> + let spec = + if not flags.allow_K_at_toplevel then + (* [evar_absorb_arguments] puts an Abstract flag for the + toplevel binders that were absorbed. *) + let occs = + if a == Abstraction.Abstract then Locus.AtLeastOneOccurrence + else Locus.AllOccurrences + in AtOccurrences occs + else Unspecified a + in spec :: aux args abs + | l, [] -> List.map (fun _ -> default_occurrence_selection) l + | [], _ :: _ -> assert false + in aux (Array.to_list args) evi.evar_abstract_arguments + +let second_order_matching_with_args flags env evd with_ho pbty ev l t = + if with_ho then + let evd,ev = evar_absorb_arguments env evd ev (Array.to_list l) in + let argoccs = default_evar_selection flags evd ev in + let test = default_occurrence_test ~frozen_evars:flags.frozen_evars flags.subterm_ts in + let evd, b = + try second_order_matching flags env evd ev (test,argoccs) t + with PretypeError (_, _, NoOccurrenceFound _) -> evd, false + in + if b then Success evd + else + UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) + else + let pb = (pbty,env,mkApp(mkEvar ev,l),t) in + UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) + +let is_beyond_capabilities = function + | CannotSolveConstraint (pb,ProblemBeyondCapabilities) -> true + | _ -> false + +let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = + let t1 = apprec_nohdbeta flags env evd (whd_head_evar evd t1) in + let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in let () = if !debug_unification then @@ -1234,7 +1565,8 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = Termops.Internal.print_constr_env env evd t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match EConstr.kind evd term1, EConstr.kind evd term2 with - | Evar (evk1,args1), (Rel _|Var _) when app_empty + | Evar (evk1,args1 as ev1), (Rel _|Var _) when app_empty + && not (is_frozen flags ev1) && List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a) (remove_instance_local_defs evd evk1 args1) -> (* The typical kind of constraint coming from pattern-matching return @@ -1244,8 +1576,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = | None -> let reason = ProblemBeyondCapabilities in UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) - | (Rel _|Var _), Evar (evk2,args2) when app_empty - && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a) + | (Rel _|Var _), Evar (evk2,args2 as ev2) when app_empty + && not (is_frozen flags ev2) + && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a) (remove_instance_local_defs evd evk2 args2) -> (* The typical kind of constraint coming from pattern-matching return type inference *) @@ -1255,36 +1588,44 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let reason = ProblemBeyondCapabilities in UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> - let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in - Success (solve_refl ~can_drop:true f env evd + let f flags ontype env evd pbty x y = + let reds = + match ontype with + | TypeUnification -> TransparentState.full + | TermUnification -> flags.open_ts + in is_fconv ~reds pbty env evd x y + in + Success (solve_refl ~can_drop:true f flags env evd (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 when app_empty -> + (* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *) Success (solve_evar_evar ~force:true - (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd - (position_problem true pbty) ev1 ev2) - | Evar ev1,_ when Array.length l1 <= Array.length l2 -> + (evar_define evar_unify flags ~choose:true) + evar_unify flags env evd + (position_problem true pbty) ev1 ev2) + | Evar ev1,_ when not (is_frozen flags ev1) && Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) (* and otherwise second-order matching *) ise_try evd - [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2); + [(fun evd -> first_order_unification flags env evd (ev1,l1) appr2); (fun evd -> - second_order_matching_with_args ts env evd pbty ev1 l1 t2)] - | _,Evar ev2 when Array.length l2 <= Array.length l1 -> + second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2)] + | _,Evar ev2 when not (is_frozen flags ev2) && Array.length l2 <= Array.length l1 -> (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) (* and otherwise second-order matching *) ise_try evd - [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1); + [(fun evd -> first_order_unification flags env evd (ev2,l2) appr1); (fun evd -> - second_order_matching_with_args ts env evd pbty ev2 l2 t1)] - | Evar ev1,_ -> + second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1)] + | Evar ev1,_ when not (is_frozen flags ev1) -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd pbty ev1 l1 t2 - | _,Evar ev2 -> + second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2 + | _,Evar ev2 when not (is_frozen flags ev2) -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd pbty ev2 l2 t1 + second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1 | _ -> (* Some head evar have been instantiated, or unknown kind of problem *) - evar_conv_x ts env evd pbty t1 t2 + evar_conv_x flags env evd pbty t1 t2 let error_cannot_unify env evd pb ?reason t1 t2 = Pretype_errors.error_cannot_unify @@ -1313,7 +1654,7 @@ let max_undefined_with_candidates evd = with MaxUndefined ans -> Some ans -let rec solve_unconstrained_evars_with_candidates ts evd = +let rec solve_unconstrained_evars_with_candidates flags evd = (* max_undefined is supposed to return the most recent, hence possibly most dependent evar *) match max_undefined_with_candidates evd with @@ -1324,11 +1665,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd = | a::l -> (* In case of variables, most recent ones come first *) try - let conv_algo = evar_conv_x ts in - let evd = check_evar_instance evd evk a conv_algo in - let evd = Evd.define evk a evd in - match reconsider_unif_constraints conv_algo evd with - | Success evd -> solve_unconstrained_evars_with_candidates ts evd + let evd = instantiate_evar evar_unify flags evd evk a in + match reconsider_unif_constraints evar_unify flags evd with + | Success evd -> solve_unconstrained_evars_with_candidates flags evd | UnifFailure _ -> aux l with | IllTypedInstance _ -> aux l @@ -1336,7 +1675,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = (* Expected invariant: most dependent solutions come first *) (* so as to favor progress when used with the refine tactics *) let evd = aux l in - solve_unconstrained_evars_with_candidates ts evd + solve_unconstrained_evars_with_candidates flags evd let solve_unconstrained_impossible_cases env evd = Evd.fold_undefined (fun evk ev_info evd' -> @@ -1345,35 +1684,40 @@ let solve_unconstrained_impossible_cases env evd = let j, ctx = coq_unit_judge env in let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in let ty = j_type j in - let conv_algo = evar_conv_x TransparentState.full in - let evd' = check_evar_instance evd' evk ty conv_algo in - Evd.define evk ty evd' + let flags = default_flags env in + instantiate_evar evar_unify flags evd' evk ty | _ -> evd') evd evd let solve_unif_constraints_with_heuristics env - ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd = - let evd = solve_unconstrained_evars_with_candidates ts evd in + ?(flags=default_flags env) ?(with_ho=false) evd = + let evd = solve_unconstrained_evars_with_candidates flags evd in let rec aux evd pbs progress stuck = match pbs with | (pbty,env,t1,t2 as pb) :: pbs -> - (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with + (match apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 with | Success evd' -> - let (evd', rest) = extract_all_conv_pbs evd' in - begin match rest with + let evd' = solve_unconstrained_evars_with_candidates flags evd' in + let (evd', rest) = extract_all_conv_pbs evd' in + begin match rest with | [] -> aux evd' pbs true stuck - | _ -> (* Unification got actually stuck, postpone *) - aux evd pbs progress (pb :: stuck) + | l -> + (* Unification got actually stuck, postpone *) + let reason = CannotSolveConstraint (pb,ProblemBeyondCapabilities) in + aux evd pbs progress ((pb, reason):: stuck) end | UnifFailure (evd,reason) -> - error_cannot_unify env evd pb ~reason t1 t2) + if is_beyond_capabilities reason then + aux evd pbs progress ((pb,reason) :: stuck) + else aux evd [] false ((pb,reason) :: stuck)) | _ -> - if progress then aux evd stuck false [] + if progress then aux evd (List.map fst stuck) false [] else match stuck with | [] -> (* We're finished *) evd - | (pbty,env,t1,t2 as pb) :: _ -> - (* There remains stuck problems *) - error_cannot_unify env evd pb t1 t2 + | ((pbty,env,t1,t2 as pb), reason) :: _ -> + (* There remains stuck problems *) + Pretype_errors.error_cannot_unify ?loc:(loc_of_conv_pb evd pb) + env evd ~reason (t1, t2) in let (evd,pbs) = extract_all_conv_pbs evd in let heuristic_solved_evd = aux evd pbs false [] in @@ -1384,16 +1728,49 @@ let solve_unif_constraints_with_heuristics env exception UnableToUnify of evar_map * unification_error -let default_transparent_state env = TransparentState.full -(* Conv_oracle.get_transp_state (Environ.oracle env) *) +let unify_delay ?flags env evd t1 t2 = + let flags = + match flags with + | None -> default_flags_of (default_transparent_state env) + | Some flags -> flags + in + match evar_conv_x flags env evd CONV t1 t2 with + | Success evd' -> evd' + | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) +let unify_leq_delay ?flags env evd t1 t2 = + let flags = + match flags with + | None -> default_flags_of (default_transparent_state env) + | Some flags -> flags + in + match evar_conv_x flags env evd CUMUL t1 t2 with + | Success evd' -> evd' + | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) + +let unify ?flags ?(with_ho=true) env evd cv_pb ty1 ty2 = + let flags = + match flags with + | None -> default_flags_of (default_transparent_state env) + | Some flags -> flags + in + let res = evar_conv_x flags env evd cv_pb ty1 ty2 in + match res with + | Success evd -> + solve_unif_constraints_with_heuristics ~flags ~with_ho env evd + | UnifFailure (evd, reason) -> + raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason))) + +(* deprecated *) let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd = - match evar_conv_x ts env evd CONV t1 t2 with + let flags = default_flags_of ts in + match evar_conv_x flags env evd CONV t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = - match evar_conv_x ts env evd CUMUL t1 t2 with + let flags = default_flags_of ts in + match evar_conv_x flags env evd CUMUL t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) @@ -1402,7 +1779,9 @@ let make_opt = function | UnifFailure _ -> None let conv env ?(ts=default_transparent_state env) evd t1 t2 = - make_opt(evar_conv_x ts env evd CONV t1 t2) + let flags = default_flags_of ts in + make_opt(evar_conv_x flags env evd CONV t1 t2) let cumul env ?(ts=default_transparent_state env) evd t1 t2 = - make_opt(evar_conv_x ts env evd CUMUL t1 t2) + let flags = default_flags_of ts in + make_opt(evar_conv_x flags env evd CUMUL t1 t2) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 4585fac252..0fe47c2a48 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -16,28 +16,74 @@ open Locus (** {4 Unification for type inference. } *) +type unify_flags = Evarsolve.unify_flags + +(** The default subterm transparent state is no unfoldings *) +val default_flags_of : ?subterm_ts:TransparentState.t -> TransparentState.t -> unify_flags + +type unify_fun = unify_flags -> + env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result + +val conv_fun : unify_fun -> Evarsolve.unifier + exception UnableToUnify of evar_map * Pretype_errors.unification_error (** {6 Main unification algorithm for type inference. } *) -(** returns exception NotUnifiable with best known evar_map if not unifiable *) +(** There are two variants for unification: one that delays constraints outside its capabilities + ([unify_delay]) and another that tries to solve such remaining constraints using + heuristics ([unify]). *) + +(** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints. + In case the flags are not specified, they default to + [default_flags_of TransparentState.full] currently. + + In case of success, the two terms are hence unifiable only if the remaining constraints + can be solved or [check_problems_are_solved] is true. + + @raises UnableToUnify in case the two terms do not unify *) + +val unify_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map +val unify_leq_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map + +(** returns exception UnableToUnify with best known evar_map if not unifiable *) val the_conv_x : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map +[@@ocaml.deprecated "Use Evarconv.unify_delay instead"] val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map - +[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"] (** The same function resolving evars by side-effect and catching the exception *) + val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option +[@@ocaml.deprecated "Use Evarconv.unify_delay instead"] val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option +[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"] + +(** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining + constraints. In case of success the two terms are unified without condition. + + The with_ho option tells if higher-order unification should be tried to resolve the + constraints. + + @raises a PretypeError if it cannot unify *) +val unify : ?flags:unify_flags -> ?with_ho:bool -> + env -> evar_map -> conv_pb -> constr -> constr -> evar_map (** {6 Unification heuristics. } *) (** Try heuristics to solve pending unification problems and to solve - evars with candidates *) + evars with candidates. + + The with_ho option tells if higher-order unification should be tried + to resolve the constraints. -val solve_unif_constraints_with_heuristics : env -> ?ts:TransparentState.t -> evar_map -> evar_map + @raises a PretypeError if it fails to resolve some problem *) -(** Check all pending unification problems are solved and raise an - error otherwise *) +val solve_unif_constraints_with_heuristics : + env -> ?flags:unify_flags -> ?with_ho:bool -> evar_map -> evar_map + +(** Check all pending unification problems are solved and raise a + PretypeError otherwise *) val check_problems_are_solved : env -> evar_map -> unit @@ -54,28 +100,55 @@ val check_conv_record : env -> evar_map -> (** Try to solve problems of the form ?x[args] = c by second-order matching, using typing to select occurrences *) -val second_order_matching : TransparentState.t -> env -> evar_map -> - EConstr.existential -> occurrences option list -> constr -> evar_map * bool +type occurrence_match_test = + env -> evar_map -> constr -> (* Used to precompute the local tests *) + env -> evar_map -> int -> constr -> constr -> bool * evar_map + +(** When given the choice of abstracting an occurrence or leaving it, + force abstration. *) + +type occurrence_selection = + | AtOccurrences of occurrences + | Unspecified of Abstraction.abstraction + +(** By default, unspecified, not preferring abstraction. + This provides the most general solutions. *) +val default_occurrence_selection : occurrence_selection + +type occurrences_selection = + occurrence_match_test * occurrence_selection list + +val default_occurrence_test : frozen_evars:Evar.Set.t -> TransparentState.t -> occurrence_match_test + +(** [default_occurrence_selection n] + Gives the default test and occurrences for [n] arguments *) +val default_occurrences_selection : ?frozen_evars:Evar.Set.t (* By default, none *) -> + TransparentState.t -> int -> occurrences_selection + +val second_order_matching : unify_flags -> env -> evar_map -> + EConstr.existential -> occurrences_selection -> constr -> evar_map * bool (** Declare function to enforce evars resolution by using typing constraints *) val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit -type unify_fun = TransparentState.t -> - env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result - (** Override default [evar_conv_x] algorithm. *) val set_evar_conv : unify_fun -> unit (** The default unification algorithm with evars and universes. *) val evar_conv_x : unify_fun +val evar_unify : Evarsolve.unifier + (**/**) (* For debugging *) -val evar_eqappr_x : ?rhs_is_already_stuck:bool -> TransparentState.t * bool -> +val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags -> env -> evar_map -> conv_pb -> state * Cst_stack.t -> state * Cst_stack.t -> Evarsolve.unification_result + +val occur_rigidly : Evarsolve.unify_flags -> + 'a -> Evd.evar_map -> Evar.t * 'b -> EConstr.t -> bool (**/**) (** {6 Functions to deal with impossible cases } *) diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 571be7466c..a51cb22c20 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -13,6 +13,7 @@ open Util open Pp open Names open Constr +open Context open Termops open EConstr open Vars @@ -72,7 +73,7 @@ let idx = Namegen.default_dependent_ident (* Refining an evar to a product *) -let define_pure_evar_as_product evd evk = +let define_pure_evar_as_product env evd evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in @@ -84,11 +85,12 @@ let define_pure_evar_as_product evd evk = let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~src ~filter:(evar_filter evi) in + let rdom = Sorts.Relevant in (* TODO relevance *) let evd2,rng = - let newenv = push_named (LocalAssum (id, dom)) evenv in + let newenv = push_named (LocalAssum (make_annot id rdom, dom)) evenv in let src = subterm_source evk ~where:Codomain evksrc in let filter = Filter.extend 1 (evar_filter evi) in - if Sorts.is_prop (ESorts.kind evd1 s) then + if Environ.is_impredicative_sort env (ESorts.kind evd1 s) then (* Impredicative product, conclusion must fall in [Prop]. *) new_evar newenv evd1 concl ~src ~filter else @@ -97,17 +99,17 @@ let define_pure_evar_as_product evd evk = new_type_evar newenv evd1 status ~src ~filter in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in - let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) (ESorts.kind evd1 s) in + let evd3 = Evd.set_leq_sort evenv evd3 (Sorts.sort_of_univ prods) (ESorts.kind evd1 s) in evd3, rng in - let prod = mkProd (Name id, dom, subst_var id rng) in + let prod = mkProd (make_annot (Name id) rdom, dom, subst_var id rng) in let evd3 = Evd.define evk prod evd2 in evd3,prod (* Refine an applied evar to a product and returns its instantiation *) -let define_evar_as_product evd (evk,args) = - let evd,prod = define_pure_evar_as_product evd evk in +let define_evar_as_product env evd (evk,args) = + let evd,prod = define_pure_evar_as_product env evd evk in (* Quick way to compute the instantiation of evk with args *) let na,dom,rng = destProd evd prod in let evdom = mkEvar (fst (destEvar evd dom), args) in @@ -131,16 +133,19 @@ let define_pure_evar_as_lambda env evd evk = let typ = Reductionops.whd_all evenv evd (evar_concl evi) in let evd1,(na,dom,rng) = match EConstr.kind evd typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) - | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ + | Evar ev' -> let evd,typ = define_evar_as_product env evd ev' in evd,destProd evd typ | _ -> error_not_product env evd typ in let avoid = Environ.ids_of_named_context_val evi.evar_hyps in let id = - next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in + map_annot (fun na -> next_name_away_with_default_using_types "x" na avoid + (Reductionops.whd_evar evd dom)) na + in let newenv = push_named (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = subterm_source evk ~where:Body (evar_source evk evd1) in - let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in - let lam = mkLambda (Name id, dom, subst_var id body) in + let abstract_arguments = Abstraction.abstract_last evi.evar_abstract_arguments in + let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id.binder_name) rng) ~filter ~abstract_arguments in + let lam = mkLambda (map_annot Name.mk_name id, dom, subst_var id.binder_name body) in Evd.define evk lam evd2, lam let define_evar_as_lambda env evd (evk,args) = @@ -163,13 +168,12 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function (* Refining an evar to a sort *) let define_evar_as_sort env evd (ev,args) = - let evd, u = new_univ_variable univ_rigid evd in + let evd, s = new_sort_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in - let s = Type u in let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in let sort = destSort evd concl in let evd' = Evd.define ev (mkSort s) evd in - Evd.set_leq_sort env evd' (Type (Univ.super u)) (ESorts.kind evd' sort), s + Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' sort), s (* Propagation of constraints through application and abstraction: Given a type constraint on a functional term, returns the type @@ -180,21 +184,22 @@ let split_tycon ?loc env evd tycon = let rec real_split evd c = let t = Reductionops.whd_all env evd c in match EConstr.kind evd t with - | Prod (na,dom,rng) -> evd, (na, dom, rng) + | Prod (na,dom,rng) -> evd, (na, dom, rng) | Evar ev (* ev is undefined because of whd_all *) -> - let (evd',prod) = define_evar_as_product evd ev in - let (_,dom,rng) = destProd evd prod in - evd',(Anonymous, dom, rng) - | App (c,args) when isEvar evd c -> - let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in + let (evd',prod) = define_evar_as_product env evd ev in + let (na,dom,rng) = destProd evd prod in + let anon = {na with binder_name = Anonymous} in + evd',(anon, dom, rng) + | App (c,args) when isEvar evd c -> + let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in real_split evd' (mkApp (lam,args)) | _ -> error_not_product ?loc env evd c in match tycon with - | None -> evd,(Anonymous,None,None) + | None -> evd,(make_annot Anonymous Relevant,None,None) | Some c -> - let evd', (n, dom, rng) = real_split evd c in - evd', (n, mk_tycon dom, mk_tycon rng) + let evd', (n, dom, rng) = real_split evd c in + evd', (n, mk_tycon dom, mk_tycon rng) let valcon_of_tycon x = x let lift_tycon n = Option.map (lift n) diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index cd23f9c601..8ff113196b 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -33,12 +33,12 @@ val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> val split_tycon : ?loc:Loc.t -> env -> evar_map -> type_constraint -> - evar_map * (Name.t * type_constraint * type_constraint) + evar_map * (Name.t Context.binder_annot * type_constraint * type_constraint) val valcon_of_tycon : type_constraint -> val_constraint val lift_tycon : int -> type_constraint -> type_constraint -val define_evar_as_product : evar_map -> existential -> evar_map * types +val define_evar_as_product : env -> evar_map -> existential -> evar_map * types val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4c4a236620..a4a078bfa0 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -12,6 +12,7 @@ open Sorts open Util open CErrors open Names +open Context open Constr open Environ open Termops @@ -24,6 +25,49 @@ open Reductionops open Evarutil open Pretype_errors +type unify_flags = { + modulo_betaiota: bool; + open_ts : TransparentState.t; + closed_ts : TransparentState.t; + subterm_ts : TransparentState.t; + frozen_evars : Evar.Set.t; + allow_K_at_toplevel : bool; + with_cs : bool } + +type unification_kind = + | TypeUnification + | TermUnification + +(************************) +(* Unification results *) +(************************) + +type unification_result = + | Success of evar_map + | UnifFailure of evar_map * unification_error + +let is_success = function Success _ -> true | UnifFailure _ -> false + +let test_success unify flags b env evd c c' rhs = + is_success (unify flags b env evd c c' rhs) + +(** A unification function parameterized by: + - unification flags + - the kind of unification + - environment + - sigma + - conversion problem + - the two terms to unify. *) + +type unifier = unify_flags -> unification_kind -> + env -> evar_map -> conv_pb -> constr -> constr -> unification_result + +(** A conversion function: parameterized by the kind of unification, + environment, sigma, conversion problem and the two terms to convert. + Conversion is not allowed to instantiate evars contrary to unification. *) +type conversion_check = unify_flags -> unification_kind -> + env -> evar_map -> conv_pb -> constr -> constr -> bool + let normalize_evar evd ev = match EConstr.kind evd (mkEvar ev) with | Evar (evk,args) -> (evk,args) @@ -129,20 +173,6 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c = let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in refresh_universes (Some false) env sigma ty - - -(************************) -(* Unification results *) -(************************) - -type unification_result = - | Success of evar_map - | UnifFailure of evar_map * unification_error - -let is_success = function Success _ -> true | UnifFailure _ -> false - -let test_success conv_algo env evd c c' rhs = - is_success (conv_algo env evd c c' rhs) let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = match pbty with @@ -154,7 +184,7 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = exception IllTypedInstance of env * EConstr.types * EConstr.types -let recheck_applications conv_algo env evdref t = +let recheck_applications unify flags env evdref t = let rec aux env t = match EConstr.kind !evdref t with | App (f, args) -> @@ -164,9 +194,9 @@ let recheck_applications conv_algo env evdref t = let rec aux i ty = if i < Array.length argsty then match EConstr.kind !evdref (whd_all env !evdref ty) with - | Prod (na, dom, codom) -> - (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with - | Success evd -> evdref := evd; + | Prod (na, dom, codom) -> + (match unify flags TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with + | Success evd -> evdref := evd; aux (succ i) (subst1 args.(i) codom) | UnifFailure (evd, reason) -> Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom)) @@ -324,7 +354,7 @@ let compute_rel_aliases var_aliases rels sigma = (fun decl (n,aliases) -> (n-1, match decl with - | LocalDef (_,t,u) -> + | LocalDef (_,t,u) -> (match EConstr.kind sigma t with | Var id' -> let aliases_of_n = @@ -611,7 +641,7 @@ let make_projectable_subst aliases sigma evi args = List.fold_right_i (fun i decl (args,all,cstrs,revmap) -> match decl,args with - | LocalAssum (id,c), a::rest -> + | LocalAssum ({binder_name=id},c), a::rest -> let revmap = Id.Map.add id i revmap in let cstrs = let a',args = decompose_app_vect sigma a in @@ -622,7 +652,7 @@ let make_projectable_subst aliases sigma evi args = | _ -> cstrs in let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in (rest,all,cstrs,revmap) - | LocalDef (id,c,_), a::rest -> + | LocalDef ({binder_name=id},c,_), a::rest -> let revmap = Id.Map.add id i revmap in (match EConstr.kind sigma c with | Var id' -> @@ -698,7 +728,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) = List.fold_right (fun d (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) -> let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in - let id = next_name_away na avoid in + let id = map_annot (fun na -> next_name_away na avoid) na in let evd,t_in_sign = let s = Retyping.get_sort_of env evd t_in_env in let evd,ty_t_in_sign = refresh_universes @@ -714,7 +744,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = (push_named_context_val d' sign, Filter.extend 1 filter, (mkRel 1)::(List.map (lift 1) inst_in_env), (mkRel 1)::(List.map (lift 1) inst_in_sign), - push_rel d env,evd,Id.Set.add id avoid)) + push_rel d env,evd,Id.Set.add id.binder_name avoid)) rel_sign (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,avoid) in @@ -734,6 +764,19 @@ let restrict_upon_filter evd evk p args = let len = Array.length args in Filter.restrict_upon oldfullfilter len (fun i -> p (Array.unsafe_get args i)) +let check_evar_instance unify flags evd evk1 body = + let evi = Evd.find evd evk1 in + let evenv = evar_env evi in + (* FIXME: The body might be ill-typed when this is called from w_merge *) + (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) + let ty = + try Retyping.get_type_of ~lax:true evenv evd body + with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance")) + in + match unify flags TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with + | Success evd -> evd + | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl)) + (***************) (* Unification *) @@ -869,12 +912,13 @@ let rec find_solution_type evarenv = function * pass [define] to [do_projection_effects] as a parameter. *) -let rec do_projection_effects define_fun env ty evd = function +let rec do_projection_effects unify flags define_fun env ty evd = function | ProjectVar -> evd | ProjectEvar ((evk,argsv),evi,id,p) -> - let evd = Evd.define evk (mkVar id) evd in + let evd = check_evar_instance unify flags evd evk (mkVar id) in + let evd = Evd.define evk (EConstr.mkVar id) evd in (* TODO: simplify constraints involving evk *) - let evd = do_projection_effects define_fun env ty evd p in + let evd = do_projection_effects unify flags define_fun env ty evd p in let ty = whd_all env evd (Lazy.force ty) in if not (isSort evd ty) then (* Don't try to instantiate if a sort because if evar_concl is an @@ -1110,9 +1154,9 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = * Note: argument f is the function used to instantiate evars. *) -let filter_compatible_candidates conv_algo env evd evi args rhs c = +let filter_compatible_candidates unify flags env evd evi args rhs c = let c' = instantiate_evar_array evi c args in - match conv_algo env evd Reduction.CONV rhs c' with + match unify flags TermUnification env evd Reduction.CONV rhs c' with | Success evd -> Some (c,evd) | UnifFailure _ -> None @@ -1122,7 +1166,7 @@ let filter_compatible_candidates conv_algo env evd evi args rhs c = exception DoesNotPreserveCandidateRestriction -let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) = +let restrict_candidates unify flags env evd filter1 (evk1,argsv1) (evk2,argsv2) = let evi1 = Evd.find evd evk1 in let evi2 = Evd.find evd evk2 in match evi1.evar_candidates, evi2.evar_candidates with @@ -1133,7 +1177,7 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) = let l1' = List.filter (fun c1 -> let c1' = instantiate_evar_array evi1 c1 argsv1 in let filter c2 = - let compatibility = filter_compatible_candidates conv_algo env evd evi2 argsv2 c1' c2 in + let compatibility = filter_compatible_candidates unify flags env evd evi2 argsv2 c1' c2 in match compatibility with | None -> false | Some _ -> true @@ -1200,14 +1244,14 @@ exception EvarSolvedOnTheFly of evar_map * EConstr.constr (* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on the common domain of definition *) -let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) = +let project_evar_on_evar force unify flags env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) = (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *) let fvs2 = free_vars_and_rels_up_alias_expansion env evd aliases (mkEvar ev2) in let filter1 = restrict_upon_filter evd evk1 (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2) argsv1 in let candidates1 = - try restrict_candidates g env evd filter1 ev1 ev2 + try restrict_candidates unify flags env evd filter1 ev1 ev2 with DoesNotPreserveCandidateRestriction -> let evd,ev1' = do_restrict_hyps evd ev1 filter1 NoUpdate in raise (CannotProject (evd,ev1')) in @@ -1225,35 +1269,22 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e else raise (CannotProject (evd,ev1')) -let check_evar_instance evd evk1 body conv_algo = - let evi = Evd.find evd evk1 in - let evenv = evar_env evi in - (* FIXME: The body might be ill-typed when this is called from w_merge *) - (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) - let ty = - try Retyping.get_type_of ~lax:true evenv evd body - with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance") - in - match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with - | Success evd -> evd - | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl)) - let update_evar_info ev1 ev2 evd = (* We update the source of obligation evars during evar-evar unifications. *) let loc, evs1 = evar_source ev1 evd in let evi = Evd.find evd ev2 in Evd.add evd ev2 {evi with evar_source = loc, evs1} -let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = +let solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 (evk2,_ as ev2) = try - let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in + let evd,body = project_evar_on_evar force unify flags env evd aliases 0 pbty ev1 ev2 in let evd' = Evd.define_with_evar evk2 body evd in let evd' = if is_obligation_evar evd evk2 then update_evar_info evk2 (fst (destEvar evd' body)) evd' else evd' in - check_evar_instance evd' evk2 body g + check_evar_instance unify flags evd' evk2 body with EvarSolvedOnTheFly (evd,c) -> f env evd pbty ev2 c @@ -1264,22 +1295,33 @@ let preferred_orientation evd evk1 evk2 = else if is_obligation_evar evd evk2 then false else true -let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = +let solve_evar_evar_aux force f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env evd in + let frozen_ev1 = Evar.Set.mem evk1 flags.frozen_evars in + let frozen_ev2 = Evar.Set.mem evk2 flags.frozen_evars in if preferred_orientation evd evk1 evk2 then - try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 + try if not frozen_ev1 then + solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 + else raise (CannotProject (evd,ev2)) with CannotProject (evd,ev2) -> - try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 - with CannotProject (evd,ev1) -> - add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd + try if not frozen_ev2 then + solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 + else raise (CannotProject (evd,ev1)) + with CannotProject (evd,ev1) -> + add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd else - try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 + try if not frozen_ev2 then + solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 + else raise (CannotProject (evd,ev1)) with CannotProject (evd,ev1) -> - try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 + try if not frozen_ev1 then + solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 + else raise (CannotProject (evd,ev2)) with CannotProject (evd,ev2) -> - add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd + add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd -let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = +(** Precondition: evk1 is not frozen *) +let solve_evar_evar ?(force=false) f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let pbty = if force then None else pbty in let evi = Evd.find evd evk1 in let downcast evk t evd = downcast evk t evd in @@ -1314,25 +1356,19 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar downcast evk2 t2 (downcast evk1 t1 evd) with Reduction.NotArity -> evd in - solve_evar_evar_aux force f g env evd pbty ev1 ev2 - -type conv_fun = - env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> unification_result - -type conv_fun_bool = - env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> bool + solve_evar_evar_aux force f unify flags env evd pbty ev1 ev2 (* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint * definitions. We try to unify the ti with the ui pairwise. The pairs * that don't unify are discarded (i.e. ?e is redefined so that it does not * depend on these args). *) -let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 = +let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 = let evdref = ref evd in let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with | None -> false | Some cstr -> - try ignore (Evd.add_universe_constraints !evdref cstr); true + try evdref := Evd.add_universe_constraints !evdref cstr; true with UniversesDiffer -> false in if Array.equal eq_constr argsv1 argsv2 then !evdref else @@ -1340,19 +1376,26 @@ let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 = let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in let untypedfilter = restrict_upon_filter evd evk - (fun (a1,a2) -> conv_algo env evd Reduction.CONV a1 a2) args in + (fun (a1,a2) -> unify flags TermUnification env evd Reduction.CONV a1 a2) args in let candidates = filter_candidates evd evk untypedfilter NoUpdate in let filter = closure_of_filter evd evk untypedfilter in - let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in - if Evar.equal (fst ev1) evk && can_drop then (* No refinement *) evd else + let evd',ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in + let frozen = Evar.Set.mem evk flags.frozen_evars in + if Evar.equal (fst ev1) evk && (frozen || can_drop) then + (* No refinement needed *) evd' + else (* either progress, or not allowed to drop, e.g. to preserve possibly *) (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *) (* if e can depend on x until ?y is not resolved, or, conversely, we *) (* don't know if ?y has to be unified with ?y, until e is resolved *) - let argsv2 = restrict_instance evd evk filter argsv2 in - let ev2 = (fst ev1,argsv2) in - (* Leave a unification problem *) - add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd + if frozen then + (* We cannot prune a frozen evar *) + add_conv_oriented_pb (pbty,env,mkEvar (evk, argsv1),mkEvar (evk,argsv2)) evd + else + let argsv2 = restrict_instance evd' evk filter argsv2 in + let ev2 = (fst ev1,argsv2) in + (* Leave a unification problem *) + add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd' (* If the evar can be instantiated by a finite set of candidates known in advance, we check which of them apply *) @@ -1360,14 +1403,14 @@ let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 = exception NoCandidates exception IncompatibleCandidates -let solve_candidates conv_algo env evd (evk,argsv) rhs = +let solve_candidates unify flags env evd (evk,argsv) rhs = let evi = Evd.find evd evk in match evi.evar_candidates with | None -> raise NoCandidates | Some l -> let l' = List.map_filter - (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs c) l in + (fun c -> filter_compatible_candidates unify flags env evd evi argsv rhs c) l in match l' with | [] -> raise IncompatibleCandidates | [c,evd] -> @@ -1375,7 +1418,7 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = (* time and the evar been solved by the filtering process *) if Evd.is_undefined evd evk then let evd' = Evd.define evk c evd in - check_evar_instance evd' evk c conv_algo + check_evar_instance unify flags evd' evk c else evd | l when List.length l < List.length l' -> let candidates = List.map fst l in @@ -1399,6 +1442,13 @@ let occur_evar_upto_types sigma n c = in try occur_rec c; false with Occur -> true +let instantiate_evar unify flags evd evk body = + (* Check instance freezing the evar to be defined, as + checking could involve the same evar definition problem again otherwise *) + let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in + let evd' = check_evar_instance unify flags evd evk body in + Evd.define evk body evd' + (* We try to instantiate the evar assuming the body won't depend * on arguments that are not Rels or Vars, or appearing several times * (i.e. we tackle a generalization of Miller-Pfenning patterns unification) @@ -1428,7 +1478,8 @@ exception NotEnoughInformationEvarEvar of EConstr.constr exception OccurCheckIn of evar_map * EConstr.constr exception MetaOccurInBodyInternal -let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = +let rec invert_definition unify flags choose imitate_defs + env evd pbty (evk,argsv as ev) rhs = let aliases = make_alias_map env evd in let evdref = ref evd in let progress = ref false in @@ -1447,7 +1498,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = if choose then (mkVar id, p) else raise (NotUniqueInType sols) in let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in - let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in + let evd = do_projection_effects unify flags (evar_define unify flags ~choose) env ty !evdref p in evdref := evd; c with @@ -1460,7 +1511,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let ty = find_solution_type (evar_filtered_env evi) sols in let ty' = instantiate_evar_array evi ty argsv in let (evd,evar,(evk',argsv' as ev')) = - materialize_evar (evar_define conv_algo ~choose) env !evdref 0 ev ty' in + materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty' in let ts = expansions_of_var evd aliases t in let test c = isEvar evd c || List.exists (is_alias evd c) ts in let filter = restrict_upon_filter evd evk test argsv' in @@ -1484,13 +1535,15 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | LocalAssum _ -> project_variable (RelAlias (i-k)) | LocalDef (_,b,_) -> try project_variable (RelAlias (i-k)) - with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i (EConstr.of_constr b))) + with NotInvertibleUsingOurAlgorithm _ when imitate_defs -> + imitate envk (lift i (EConstr.of_constr b))) | Var id -> (match Environ.lookup_named id env' with | LocalAssum _ -> project_variable (VarAlias id) | LocalDef (_,b,_) -> try project_variable (VarAlias id) - with NotInvertibleUsingOurAlgorithm _ -> imitate envk (EConstr.of_constr b)) + with NotInvertibleUsingOurAlgorithm _ when imitate_defs -> + imitate envk (EConstr.of_constr b)) | LetIn (na,b,u,c) -> imitate envk (subst1 b c) | Evar (evk',args' as ev') -> @@ -1499,7 +1552,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let aliases = lift_aliases k aliases in (try let ev = (evk,Array.map (lift k) argsv) in - let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in + let evd,body = project_evar_on_evar false unify flags env' !evdref aliases k None ev' ev in evdref := evd; body with @@ -1510,15 +1563,15 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = (* Make the virtual left evar real *) let ty = get_type_of env' evd t in let (evd,evar'',ev'') = - materialize_evar (evar_define conv_algo ~choose) env' evd k ev ty in + 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 - let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in + 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 - check_evar_instance evd evk' body conv_algo + check_evar_instance unify flags evd evk' body with | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *) | CannotProject (evd,ev'') -> @@ -1555,7 +1608,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | [x] -> x | _ -> let (evd,evar'',ev'') = - materialize_evar (evar_define conv_algo ~choose) env' !evdref k ev ty in + materialize_evar (evar_define unify flags ~choose) env' !evdref k ev ty in evdref := restrict_evar evd (fst ev'') None (UpdateWith candidates); evar'') | None -> @@ -1585,7 +1638,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = else let t' = imitate (env,0) rhs in if !progress then - (recheck_applications conv_algo (evar_env evi) evdref t'; t') + (recheck_applications unify flags (evar_env evi) evdref t'; t') else t' in (!evdref,body) @@ -1594,46 +1647,30 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = * [define] tries to find an instance lhs such that * "lhs [hyps:=args]" unifies to rhs. The term "lhs" must be closed in * context "hyps" and not referring to itself. + * ev is assumed not to be frozen. *) -and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = +and evar_define unify flags ?(choose=false) ?(imitate_defs=true) env evd pbty (evk,argsv as ev) rhs = match EConstr.kind evd rhs with | Evar (evk2,argsv2 as ev2) -> if Evar.equal evk evk2 then solve_refl ~can_drop:choose - (test_success conv_algo) env evd pbty evk argsv argsv2 + (test_success unify) flags env evd pbty evk argsv argsv2 else solve_evar_evar ~force:choose - (evar_define conv_algo) conv_algo env evd pbty ev ev2 + (evar_define unify flags) unify flags env evd pbty ev ev2 | _ -> - try solve_candidates conv_algo env evd ev rhs + try solve_candidates unify flags env evd ev rhs with NoCandidates -> try - let (evd',body) = invert_definition conv_algo choose env evd pbty ev rhs in + let (evd',body) = invert_definition unify flags choose imitate_defs env evd pbty ev rhs in if occur_meta evd' body then raise MetaOccurInBodyInternal; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body)); (* needed only if an inferred type *) let evd', body = refresh_universes pbty env evd' body in -(* Cannot strictly type instantiations since the unification algorithm - * does not unify applications from left to right. - * e.g problem f x == g y yields x==y and f==g (in that order) - * Another problem is that type variables are evars of type Type - let _ = - try - let env = evar_filtered_env evi in - let ty = evi.evar_concl in - Typing.check env evd' body ty - with e -> - msg_info - (str "Ill-typed evar instantiation: " ++ fnl() ++ - pr_evar_map evd' ++ fnl() ++ - str "----> " ++ int ev ++ str " := " ++ - print_constr body); - raise e in*) - let evd' = check_evar_instance evd' evk body conv_algo in - Evd.define evk body evd' + instantiate_evar unify flags evd' evk body with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd pbty ev sols rhs @@ -1648,8 +1685,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = let c = whd_all env evd rhs in match EConstr.kind evd c with | Evar (evk',argsv2) when Evar.equal evk evk' -> - solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c') - env evd pbty evk argsv argsv2 + solve_refl (fun flags _b env sigma pb c c' -> is_fconv pb env sigma c c') flags + env evd pbty evk argsv argsv2 | _ -> raise (OccurCheckIn (evd,rhs)) @@ -1683,13 +1720,13 @@ let status_changed evd lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar evd t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar evd t2) lev with NoHeadEvar -> false) -let reconsider_unif_constraints conv_algo evd = +let reconsider_unif_constraints unify flags evd = let (evd,pbs) = extract_changed_conv_pbs evd (status_changed evd) in List.fold_left (fun p (pbty,env,t1,t2 as x) -> match p with | Success evd -> - (match conv_algo env evd pbty t1 t2 with + (match unify flags TermUnification env evd pbty t1 t2 with | Success _ as x -> x | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e))) | UnifFailure _ as x -> x) @@ -1702,11 +1739,12 @@ let reconsider_unif_constraints conv_algo evd = * if the problem couldn't be solved. *) (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) -let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) = +let solve_simple_eqn unify flags ?(choose=false) ?(imitate_defs=true) + env evd (pbty,(evk1,args1 as ev1),t2) = try let t2 = whd_betaiota evd t2 in (* includes whd_evar *) - let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in - reconsider_unif_constraints conv_algo evd + let evd = evar_define unify flags ~choose ~imitate_defs env evd pbty ev1 t2 in + reconsider_unif_constraints unify flags evd with | NotInvertibleUsingOurAlgorithm t -> UnifFailure (evd,NotClean (ev1,env,t)) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 4665ed29a2..ebf8230bbd 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -16,6 +16,25 @@ type alias val of_alias : alias -> EConstr.t +type unify_flags = { + modulo_betaiota : bool; + (* Enable beta-iota reductions during unification *) + open_ts : TransparentState.t; + (* Enable delta reduction according to open_ts for open terms *) + closed_ts : TransparentState.t; + (* Enable delta reduction according to closed_ts for closed terms (when calling conversion) *) + subterm_ts : TransparentState.t; + (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order + unifications. *) + frozen_evars : Evar.Set.t; + (* Frozen evars are treated like rigid variables during unification: they can not be instantiated. *) + allow_K_at_toplevel : bool; + (* During higher-order unifications, allow to produce K-redexes: i.e. to produce + an abstraction for an unused argument *) + with_cs : bool + (* Enable canonical structure resolution during unification *) +} + type unification_result = | Success of evar_map | UnifFailure of evar_map * Pretype_errors.unification_error @@ -26,19 +45,49 @@ val is_success : unification_result -> bool their representative that is most ancient in the context *) val expand_vars_in_term : env -> evar_map -> constr -> constr +(** One might want to use different conversion strategies for types and terms: + e.g. preventing delta reductions when doing term unifications but allowing + arbitrary delta conversion when checking the types of evar instances. *) + +type unification_kind = + | TypeUnification + | TermUnification + +(** A unification function parameterized by: + - unification flags + - the kind of unification + - environment + - sigma + - conversion problem + - the two terms to unify. *) +type unifier = unify_flags -> unification_kind -> + env -> evar_map -> conv_pb -> constr -> constr -> unification_result + +(** A conversion function: parameterized by the kind of unification, + environment, sigma, conversion problem and the two terms to convert. + Conversion is not allowed to instantiate evars contrary to unification. *) +type conversion_check = unify_flags -> unification_kind -> + env -> evar_map -> conv_pb -> constr -> constr -> bool + +(** [instantiate_evar unify flags env sigma ev c] defines the evar [ev] with [c], + checking that the type of [c] is unifiable with [ev]'s declared type first. + + Preconditions: + - [ev] does not occur in [c]. + - [c] does not contain any Meta(_) + *) + +val instantiate_evar : unifier -> unify_flags -> evar_map -> + Evar.t -> constr -> evar_map + (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is true); fails if the instance is not valid for the given [ev] *) -type conv_fun = - env -> evar_map -> conv_pb -> constr -> constr -> unification_result - -type conv_fun_bool = - env -> evar_map -> conv_pb -> constr -> constr -> bool +val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> + env -> evar_map -> bool option -> existential -> constr -> evar_map -val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> - bool option -> existential -> constr -> evar_map val refresh_universes : ?status:Evd.rigid -> @@ -49,18 +98,18 @@ val refresh_universes : bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types -val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> +val solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> env -> evar_map -> bool option -> Evar.t -> constr array -> constr array -> evar_map val solve_evar_evar : ?force:bool -> (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> - conv_fun -> + unifier -> unify_flags -> env -> evar_map -> bool option -> existential -> existential -> evar_map -val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> +val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option * existential * constr -> unification_result -val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result +val reconsider_unif_constraints : unifier -> unify_flags -> evar_map -> unification_result val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> constr -> alias list option @@ -75,8 +124,8 @@ val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool exception IllTypedInstance of env * types * types (* May raise IllTypedInstance if types are not convertible *) -val check_evar_instance : - evar_map -> Evar.t -> constr -> conv_fun -> evar_map +val check_evar_instance : unifier -> unify_flags -> + evar_map -> Evar.t -> constr -> evar_map val remove_instance_local_defs : evar_map -> Evar.t -> 'a array -> 'a list diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index b16087031b..7019cdf046 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -70,7 +70,7 @@ let map_named_declaration_with_hyploc f hyploc acc decl = in match decl,hyploc with | LocalAssum (id,_), InHypValueOnly -> - error_occurrences_error (IncorrectInValueOccurrence id) + error_occurrences_error (IncorrectInValueOccurrence id.Context.binder_name) | LocalAssum (id,typ), _ -> let acc,typ = f acc typ in acc, LocalAssum (id,typ) | LocalDef (id,body,typ), InHypTypeOnly -> @@ -125,7 +125,7 @@ let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t = end; add_subst t subst; incr pos; (* Check nested matching subterms *) - if occs != Locus.AllOccurrences && occs != Locus.NoOccurrences then + if not (Locusops.is_all_occurrences occs) && occs != Locus.NoOccurrences then begin nested := true; ignore (subst_below k t); nested := false end; (* Do the effective substitution *) Vars.lift k (bywhat ())) diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index d6b204561e..cd82b1993b 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -92,7 +92,7 @@ let push_rec_types ~hypnaming sigma (lna,typarray) env = let open Context.Rel.Declaration in let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e ~hypnaming in (e,d)) env ctxt in - Array.map get_name ctx, env + Array.map get_annot ctx, env let new_evar env sigma ?src ?naming typ = let open Context.Named.Declaration in diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index 63f72e60bd..65ae495135 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -50,7 +50,7 @@ val vars_of_env : t -> Id.Set.t val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t -val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t array * constr array -> t -> Name.t array * t +val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t Context.binder_annot array * constr array -> t -> Name.t Context.binder_annot array * t (** Declare an evar using renaming information *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 68626597fc..affed5389f 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -514,12 +514,11 @@ let rec cases_pattern_of_glob_constr na c = ) c open Declarations -open Term open Context (* Keep only patterns which are not bound to a local definitions *) -let drop_local_defs typi args = - let (decls,_) = decompose_prod_assum typi in +let drop_local_defs params decls args = + let decls = List.skipn (Rel.length params) (List.rev decls) in let rec aux decls args = match decls, args with | [], [] -> [] @@ -531,7 +530,7 @@ let drop_local_defs typi args = end | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args | _ -> assert false in - aux (List.rev decls) args + aux decls args let add_patterns_for_params_remove_local_defs (ind,j) l = let (mib,mip) = Global.lookup_inductive ind in @@ -540,9 +539,8 @@ let add_patterns_for_params_remove_local_defs (ind,j) l = if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then (* Optimisation *) l else - let typi = mip.mind_nf_lc.(j-1) in - let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in - drop_local_defs typi l in + let (ctx, _) = mip.mind_nf_lc.(j - 1) in + drop_local_defs mib.mind_params_ctxt ctx l in Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l let add_alias ?loc na c = diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 8670c1d964..c57cf88cc6 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -24,6 +24,7 @@ type existential_name = Id.t (** Sorts *) type 'a glob_sort_gen = + | GSProp (** representation of [SProp] literal *) | GProp (** representation of [Prop] literal *) | GSet (** representation of [Set] literal *) | GType of 'a (** representation of [Type] literal *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index bd321d5886..4f940fa16a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -21,6 +21,7 @@ open Globnames open Nameops open Term open Constr +open Context open Vars open Namegen open Declarations @@ -43,8 +44,8 @@ exception RecursionSchemeError of env * recursion_scheme_error let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na let name_assumption env = function -| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) -| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) +| LocalAssum (na,t) -> LocalAssum (map_annot (named_hd env t) na, t) +| LocalDef (na,c,t) -> LocalDef (map_annot (named_hd env c) na, c, t) let mkLambda_or_LetIn_name env d b = mkLambda_or_LetIn (name_assumption env d) b let mkProd_or_LetIn_name env d b = mkProd_or_LetIn (name_assumption env d) b @@ -54,7 +55,7 @@ let it_mkProd_or_LetIn_name env b l = List.fold_left (fun c d -> mkProd_or_LetIn let it_mkLambda_or_LetIn_name env b l = List.fold_left (fun c d -> mkLambda_or_LetIn_name env d c) b l let make_prod_dep dep env = if dep then mkProd_name env else mkProd -let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c) +let mkLambda_string s r t c = mkLambda (make_annot (Name (Id.of_string s)) r, t, c) (*******************************************) @@ -79,6 +80,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let indf = make_ind_family(pind, Context.Rel.to_extended_list mkRel 0 lnamespar) in let constrs = get_constructors env indf in let projs = get_projections env ind in + let relevance = Sorts.relevance_of_sort_family kind in let () = if Option.is_empty projs then check_privacy_block mib in let () = @@ -98,11 +100,13 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let nbprod = k+1 in let indf' = lift_inductive_family nbprod indf in - let arsign,_ = get_arity env indf' in + let arsign,sort = get_arity env indf' in + let r = Sorts.relevance_of_sort_family sort in let depind = build_dependent_inductive env indf' in - let deparsign = LocalAssum (Anonymous,depind)::arsign in + let deparsign = LocalAssum (make_annot Anonymous r,depind)::arsign in - let ci = make_case_info env (fst pind) RegularStyle in + let rci = relevance in + let ci = make_case_info env (fst pind) rci RegularStyle in let pbody = appvect (mkRel (ndepar + nbprod), @@ -111,7 +115,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let p = it_mkLambda_or_LetIn_name env' ((if dep then mkLambda_name env' else mkLambda) - (Anonymous,depind,pbody)) + (make_annot Anonymous r,depind,pbody)) arsign in let obj = @@ -132,16 +136,16 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = else let cs = lift_constructor (k+1) constrs.(k) in let t = build_branch_type env sigma dep (mkRel (k+1)) cs in - mkLambda_string "f" t - (add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1)) + mkLambda_string "f" relevance t + (add_branch (push_rel (LocalAssum (make_annot Anonymous relevance, t)) env) (k+1)) in let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg sigma kind in let typP = make_arity env' sigma dep indf s in let typP = EConstr.Unsafe.to_constr typP in let c = it_mkLambda_or_LetIn_name env - (mkLambda_string "P" typP - (add_branch (push_rel (LocalAssum (Anonymous,typP)) env') 0)) lnamespar + (mkLambda_string "P" Sorts.Relevant typP + (add_branch (push_rel (LocalAssum (make_annot Anonymous Sorts.Relevant,typP)) env') 0)) lnamespar in (sigma, c) @@ -171,12 +175,12 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let p' = EConstr.Unsafe.to_constr p' in let largs = List.map EConstr.Unsafe.to_constr largs in match kind p' with - | Prod (n,t,c) -> - let d = LocalAssum (n,t) in - make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c) - | LetIn (n,b,t,c) when List.is_empty largs -> - let d = LocalDef (n,b,t) in - mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c) + | Prod (n,t,c) -> + let d = LocalAssum (n,t) in + make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c) + | LetIn (n,b,t,c) when List.is_empty largs -> + let d = LocalDef (n,b,t) in + mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c) | Ind (_,_) -> let realargs = List.skipn nparams largs in let base = applist (lift i pk,realargs) in @@ -208,23 +212,24 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = (match optionpos with | None -> make_prod env - (n,t, - process_constr (push_rel (LocalAssum (n,t)) env) (i+1) c_0 rest + (n,t, + process_constr (push_rel (LocalAssum (n,t)) env) (i+1) c_0 rest (nhyps-1) (i::li)) | Some(dep',p) -> let nP = lift (i+1+decP) p in let env' = push_rel (LocalAssum (n,t)) env in - let t_0 = process_pos env' dep' nP (lift 1 t) in + let t_0 = process_pos env' dep' nP (lift 1 t) in + let r_0 = Retyping.relevance_of_type env' sigma (EConstr.of_constr t_0) in make_prod_dep (dep || dep') env (n,t, - mkArrow t_0 + mkArrow t_0 r_0 (process_constr - (push_rel (LocalAssum (Anonymous,t_0)) env') + (push_rel (LocalAssum (make_annot Anonymous n.binder_relevance,t_0)) env') (i+2) (lift 1 c_0) rest (nhyps-1) (i::li)))) | LetIn (n,b,t,c_0) -> - mkLetIn (n,b,t, + mkLetIn (n,b,t, process_constr - (push_rel (LocalDef (n,b,t)) env) + (push_rel (LocalDef (n,b,t)) env) (i+1) c_0 recargs (nhyps-1) li) | _ -> assert false else @@ -250,12 +255,12 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let p' = EConstr.Unsafe.to_constr p' in let largs = List.map EConstr.Unsafe.to_constr largs in match kind p' with - | Prod (n,t,c) -> - let d = LocalAssum (n,t) in - mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c) - | LetIn (n,b,t,c) when List.is_empty largs -> - let d = LocalDef (n,b,t) in - mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c) + | Prod (n,t,c) -> + let d = LocalAssum (n,t) in + mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c) + | LetIn (n,b,t,c) when List.is_empty largs -> + let d = LocalDef (n,b,t) in + mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c) | Ind _ -> let realargs = List.skipn nparrec largs and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect mkRel 0 hyps) in @@ -280,7 +285,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = (match optionpos with | None -> mkLambda_name env - (n,t,process_constr (push_rel d env) (i+1) + (n,t,process_constr (push_rel d env) (i+1) (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)]))))) (cprest,rest)) | Some(_,f_0) -> @@ -288,12 +293,12 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let env' = push_rel d env in let arg = process_pos env' nF (lift 1 t) in mkLambda_name env - (n,t,process_constr env' (i+1) + (n,t,process_constr env' (i+1) (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg]))))) (cprest,rest))) | (LocalDef (n,c,t) as d)::cprest, rest -> mkLetIn - (n,c,t, + (n,c,t, process_constr (push_rel d env) (i+1) (lift 1 f) (cprest,rest)) | [],[] -> f @@ -329,25 +334,26 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = let recargpar = recargparn [] (nparams-nparrec) in let make_one_rec p = let makefix nbconstruct = - let rec mrec i ln ltyp ldef = function - | ((indi,u),mibi,mipi,dep,_)::rest -> - let tyi = snd indi in - let nctyi = - Array.length mipi.mind_consnames in (* nb constructeurs du type*) + let rec mrec i ln lrelevance ltyp ldef = function + | ((indi,u),mibi,mipi,dep,target_sort)::rest -> + let tyi = snd indi in + let nctyi = + Array.length mipi.mind_consnames in (* nb constructeurs du type*) - (* arity in the context of the fixpoint, i.e. + (* arity in the context of the fixpoint, i.e. P1..P_nrec f1..f_nbconstruct *) - let args = Context.Rel.to_extended_list mkRel (nrec+nbconstruct) lnamesparrec in - let indf = make_ind_family((indi,u),args) in + let args = Context.Rel.to_extended_list mkRel (nrec+nbconstruct) lnamesparrec in + let indf = make_ind_family((indi,u),args) in - let arsign,_ = get_arity env indf in - let depind = build_dependent_inductive env indf in - let deparsign = LocalAssum (Anonymous,depind)::arsign in + let arsign,s = get_arity env indf in + let r = Sorts.relevance_of_sort_family s in + let depind = build_dependent_inductive env indf in + let deparsign = LocalAssum (make_annot Anonymous r,depind)::arsign in - let nonrecpar = Context.Rel.length lnonparrec in - let larsign = Context.Rel.length deparsign in - let ndepar = larsign - nonrecpar in - let dect = larsign+nrec+nbconstruct in + let nonrecpar = Context.Rel.length lnonparrec in + let larsign = Context.Rel.length deparsign in + let ndepar = larsign - nonrecpar in + let dect = larsign+nrec+nbconstruct in (* constructors in context of the Cases expr, i.e. P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *) @@ -375,9 +381,10 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = (* Predicate in the context of the case *) - let depind' = build_dependent_inductive env indf' in - let arsign',_ = get_arity env indf' in - let deparsign' = LocalAssum (Anonymous,depind')::arsign' in + let depind' = build_dependent_inductive env indf' in + let arsign',s = get_arity env indf' in + let r = Sorts.relevance_of_sort_family s in + let deparsign' = LocalAssum (make_annot Anonymous r,depind')::arsign' in let pargs = let nrpar = Context.Rel.to_extended_list mkRel (2*ndepar) lnonparrec @@ -388,13 +395,15 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = in (* body of i-th component of the mutual fixpoint *) + let target_relevance = Sorts.relevance_of_sort_family target_sort in let deftyi = - let ci = make_case_info env indi RegularStyle in + let rci = target_relevance in + let ci = make_case_info env indi rci RegularStyle in let concl = applist (mkRel (dect+j+ndepar),pargs) in let pred = it_mkLambda_or_LetIn_name env ((if dep then mkLambda_name env else mkLambda) - (Anonymous,depind',concl)) + (make_annot Anonymous r,depind',concl)) arsign' in let obj = @@ -416,20 +425,21 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = in it_mkProd_or_LetIn_name env concl deparsign - in - mrec (i+nctyi) (Context.Rel.nhyps arsign ::ln) (typtyi::ltyp) + in + mrec (i+nctyi) (Context.Rel.nhyps arsign ::ln) (target_relevance::lrelevance) (typtyi::ltyp) (deftyi::ldef) rest | [] -> let fixn = Array.of_list (List.rev ln) in let fixtyi = Array.of_list (List.rev ltyp) in let fixdef = Array.of_list (List.rev ldef) in - let names = Array.make nrec (Name(Id.of_string "F")) in - mkFix ((fixn,p),(names,fixtyi,fixdef)) + let lrelevance = CArray.rev_of_list lrelevance in + let names = Array.map (fun r -> make_annot (Name(Id.of_string "F")) r) lrelevance in + mkFix ((fixn,p),(names,fixtyi,fixdef)) in - mrec 0 [] [] [] + mrec 0 [] [] [] [] in let rec make_branch env i = function - | ((indi,u),mibi,mipi,dep,_)::rest -> + | ((indi,u),mibi,mipi,dep,sfam)::rest -> let tyi = snd indi in let nconstr = Array.length mipi.mind_consnames in let rec onerec env j = @@ -443,9 +453,10 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = let p_0 = type_rec_branch true dep env !evdref (vargs,depPvec,i+j) tyi cs recarg - in - mkLambda_string "f" p_0 - (onerec (push_rel (LocalAssum (Anonymous,p_0)) env) (j+1)) + in + let r_0 = Sorts.relevance_of_sort_family sfam in + mkLambda_string "f" r_0 p_0 + (onerec (push_rel (LocalAssum (make_annot Anonymous r_0,p_0)) env) (j+1)) in onerec env 0 | [] -> makefix i listdepkind @@ -458,9 +469,9 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = evdref := sigma; res in let typP = make_arity env !evdref dep indf s in - let typP = EConstr.Unsafe.to_constr typP in - mkLambda_string "P" typP - (put_arity (push_rel (LocalAssum (Anonymous,typP)) env) (i+1) rest) + let typP = EConstr.Unsafe.to_constr typP in + mkLambda_string "P" Sorts.Relevant typP + (put_arity (push_rel (LocalAssum (anonR,typP)) env) (i+1) rest) | [] -> make_branch env 0 listdepkind in @@ -530,7 +541,7 @@ let weaken_sort_scheme env evd set sort npars term ty = mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) else let c',term' = drec (np-1) c in - mkProd (n, t, c'), mkLambda (n, t, term') + mkProd (n, t, c'), mkLambda (n, t, term') | LetIn (n,b,t,c) -> let c',term' = drec np c in mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.") @@ -588,6 +599,7 @@ let build_induction_scheme env sigma pind dep kind = (*s Eliminations. *) let elimination_suffix = function + | InSProp -> "_sind" | InProp -> "_ind" | InSet -> "_rec" | InType -> "_rect" diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 4c02dc0f09..678aebfbe6 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -15,6 +15,7 @@ open Univ open Term open Constr open Vars +open Context open Termops open Declarations open Declareops @@ -60,6 +61,8 @@ let lift_inductive_family n = liftn_inductive_family n 1 let substnl_ind_family l n = map_ind_family (substnl l n) +let relevance_of_inductive_family env ((ind,_),_ : inductive_family) = + Inductive.relevance_of_inductive env ind type inductive_type = IndType of inductive_family * EConstr.constr list @@ -75,6 +78,9 @@ let lift_inductive_type n = liftn_inductive_type n 1 let substnl_ind_type l n = map_inductive_type (EConstr.Vars.substnl l n) +let relevance_of_inductive_type env (IndType (indf, _)) = + relevance_of_inductive_family env indf + let mkAppliedInd (IndType ((ind,params), realargs)) = let open EConstr in let ind = on_snd EInstance.make ind in @@ -101,7 +107,8 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in if j > nconstr then user_err Pp.(str "Not enough constructors in the type."); - substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1)) + let (ctx, cty) = specif.(j - 1) in + substl (List.init ntypes make_Ik) (subst_instance_constr u (Term.it_mkProd_or_LetIn cty ctx)) (* Number of constructors *) @@ -275,13 +282,12 @@ let has_dependent_elim mib = | NotRecord | FakeRecord -> true (* Annotation for cases *) -let make_case_info env ind style = +let make_case_info env ind r style = let (mib,mip) = Inductive.lookup_mind_specif env ind in let ind_tags = Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in let cstr_tags = - Array.map2 (fun c n -> - let d,_ = decompose_prod_assum c in + Array.map2 (fun (d, _) n -> Context.Rel.to_tags (List.firstn n d)) mip.mind_nf_lc mip.mind_consnrealdecls in let print_info = { ind_tags; cstr_tags; style } in @@ -289,6 +295,7 @@ let make_case_info env ind style = ci_npar = mib.mind_nparams; ci_cstr_ndecls = mip.mind_consnrealdecls; ci_cstr_nargs = mip.mind_consnrealargs; + ci_relevance = r; ci_pp_info = print_info } (*s Useful functions *) @@ -419,12 +426,14 @@ let build_dependent_inductive env ((ind, params) as indf) = (* builds the arity of an elimination predicate in sort [s] *) let make_arity_signature env sigma dep indf = - let (arsign,_) = get_arity env indf in + let (arsign,s) = get_arity env indf in + let r = Sorts.relevance_of_sort_family s in + let anon = make_annot Anonymous r in let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in if dep then (* We need names everywhere *) Namegen.name_context env sigma - ((LocalAssum (Anonymous,EConstr.of_constr (build_dependent_inductive env indf)))::arsign) + ((LocalAssum (anon,EConstr.of_constr (build_dependent_inductive env indf)))::arsign) (* Costly: would be better to name once for all at definition time *) else (* No need to enforce names *) @@ -457,12 +466,15 @@ let compute_projections env (kn, i as ind) = let x = match mib.mind_record with | NotRecord | FakeRecord -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") - | PrimRecord info-> Name (pi1 (info.(i))) + | PrimRecord info -> + let id, _, _, _ = info.(i) in + make_annot (Name id) mib.mind_packets.(i).mind_relevance in let pkt = mib.mind_packets.(i) in let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in + let ctx, cty = pkt.mind_nf_lc.(0) in + let rctx, _ = decompose_prod_assum (substl subst (Term.it_mkProd_or_LetIn cty ctx)) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in (* We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not @@ -490,7 +502,7 @@ let compute_projections env (kn, i as ind) = let subst = c1 :: subst in (proj_arg, j+1, pbs, subst) | LocalAssum (na,t) -> - match na with + match na.binder_name with | Name id -> let lab = Label.of_id id in let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab in @@ -600,7 +612,7 @@ let is_predicate_explicitly_dep env sigma pred arsign = From Coq > 8.2, using or not the effective dependency of the predicate is parametrable! *) - begin match na with + begin match na.binder_name with | Anonymous -> false | Name _ -> true end @@ -622,9 +634,7 @@ let set_pattern_names env sigma ind brv = let (mib,mip) = Inductive.lookup_mind_specif env ind in let arities = Array.map - (fun c -> - Context.Rel.length ((prod_assum c)) - - mib.mind_nparams) + (fun (d, _) -> List.length d - mib.mind_nparams) mip.mind_nf_lc in Array.map2 (set_names env sigma) arities brv @@ -644,9 +654,10 @@ let type_case_branches_with_names env sigma indspec p c = (* Type of Case predicates *) let arity_of_case_predicate env (ind,params) dep k = - let arsign,_ = get_arity env (ind,params) in + let arsign,s = get_arity env (ind,params) in + let r = Sorts.relevance_of_sort_family s in let mind = build_dependent_inductive env (ind,params) in - let concl = if dep then mkArrow mind (mkSort k) else mkSort k in + let concl = if dep then mkArrow mind r (mkSort k) else mkSort k in Term.it_mkProd_or_LetIn concl arsign (***********************************************) @@ -721,7 +732,7 @@ let control_only_guard env sigma c = match kind c with | CoFix (_,(_,_,_) as cofix) -> Inductive.check_cofix e cofix - | Fix (_,(_,_,_) as fix) -> + | Fix fix -> Inductive.check_fix e fix | _ -> () in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 5a4257e175..c74bbfe98b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -38,6 +38,8 @@ val lift_inductive_family : int -> inductive_family -> inductive_family val substnl_ind_family : constr list -> int -> inductive_family -> inductive_family +val relevance_of_inductive_family : env -> inductive_family -> Sorts.relevance + (** An inductive type with its parameters and real arguments *) type inductive_type = IndType of inductive_family * EConstr.constr list val make_ind_type : inductive_family * EConstr.constr list -> inductive_type @@ -47,6 +49,8 @@ val liftn_inductive_type : int -> int -> inductive_type -> inductive_type val lift_inductive_type : int -> inductive_type -> inductive_type val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type +val relevance_of_inductive_type : env -> inductive_type -> Sorts.relevance + val mkAppliedInd : inductive_type -> EConstr.constr val mis_is_recursive_subset : int list -> wf_paths -> bool val mis_is_recursive : @@ -176,7 +180,7 @@ val type_case_branches_with_names : env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types (** Annotation for cases *) -val make_case_info : env -> inductive -> case_style -> case_info +val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_info (** Make a case or substitute projections if the inductive type is a record with primitive projections. diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index bf8a38a353..fefc15dfb2 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -201,7 +201,7 @@ let infer_inductive env mie = Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) LMap.empty uarray in - let env = Typeops.check_context env params in + let env, params = Typeops.check_context env params in let variances = List.fold_left (fun variances entry -> let variances = infer_arity_constructor true env variances entry.mind_entry_arity diff --git a/pretyping/locus.ml b/pretyping/locus.ml index 37dd120c1a..087a6b9174 100644 --- a/pretyping/locus.ml +++ b/pretyping/locus.ml @@ -20,6 +20,7 @@ type 'a or_var = type 'a occurrences_gen = | AllOccurrences + | AtLeastOneOccurrence | AllOccurrencesBut of 'a list (** non-empty *) | NoOccurrences | OnlyOccurrences of 'a list (** non-empty *) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 6b6a3f8a9f..aaa4ce684d 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -19,15 +19,17 @@ let occurrences_map f = function | AllOccurrencesBut l -> let l' = f l in if l' = [] then AllOccurrences else AllOccurrencesBut l' - | (NoOccurrences|AllOccurrences) as o -> o + | (NoOccurrences|AllOccurrences|AtLeastOneOccurrence) as o -> o let convert_occs = function + | AtLeastOneOccurrence -> (false,[]) | AllOccurrences -> (false,[]) | AllOccurrencesBut l -> (false,l) | NoOccurrences -> (true,[]) | OnlyOccurrences l -> (true,l) let is_selected occ = function + | AtLeastOneOccurrence -> true | AllOccurrences -> true | AllOccurrencesBut l -> not (Int.List.mem occ l) | OnlyOccurrences l -> Int.List.mem occ l @@ -46,6 +48,11 @@ let is_nowhere = function | { onhyps=Some[]; concl_occs=NoOccurrences } -> true | _ -> false +let is_all_occurrences = function + | AtLeastOneOccurrence + | AllOccurrences -> true + | _ -> false + (** Clause conversion functions, parametrized by a hyp enumeration function *) (** From [clause] to [simple_clause] *) @@ -61,12 +68,12 @@ let simple_clause_of enum_hyps cl = List.map Option.make (enum_hyps ()) | Some l -> List.map (fun ((occs,id),w) -> - if occs <> AllOccurrences then error_occurrences (); + if not (is_all_occurrences occs) then error_occurrences (); if w = InHypValueOnly then error_body_selection (); Some id) l in if cl.concl_occs = NoOccurrences then hyps else - if cl.concl_occs <> AllOccurrences then error_occurrences () + if not (is_all_occurrences cl.concl_occs) then error_occurrences () else None :: hyps (** From [clause] to [concrete_clause] *) @@ -111,7 +118,7 @@ let clause_with_generic_occurrences cls = List.for_all (function ((AllOccurrences,_),_) -> true | _ -> false) hyps in let concl = match cls.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in hyps && concl @@ -122,6 +129,6 @@ let clause_with_generic_context_selection cls = List.for_all (function ((AllOccurrences,_),InHyp) -> true | _ -> false) hyps in let concl = match cls.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in hyps && concl diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index a07c018c32..ac15fe1018 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -21,6 +21,8 @@ val convert_occs : occurrences -> bool * int list val is_selected : int -> occurrences -> bool +val is_all_occurrences : 'a occurrences_gen -> bool + (** Usual clauses *) val allHypsAndConcl : 'a clause_expr diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index b7090e69da..0b2d760ca8 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -10,6 +10,7 @@ open CErrors open Term open Constr +open Context open Vars open Environ open Reduction @@ -89,10 +90,12 @@ let invert_tag cst tag reloc_tbl = with Find_at j -> (j+1) let decompose_prod env t = - let (name,dom,codom as res) = destProd (whd_all env t) in - match name with - | Anonymous -> (Name (Id.of_string "x"),dom,codom) - | _ -> res + let (name,dom,codom) = destProd (whd_all env t) in + let name = map_annot (function + | Anonymous -> Name (Id.of_string "x") + | na -> na) name + in + (name,dom,codom) let app_type env c = let t = whd_all env c in @@ -107,7 +110,8 @@ let find_rectype_a env c = (* Instantiate inductives and parameters in constructor type *) -let type_constructor mind mib u typ params = +let type_constructor mind mib u (ctx, typ) params = + let typ = it_mkProd_or_LetIn typ ctx in let s = ind_subst mind mib u in let ctyp = substl s typ in let nparams = Array.length params in @@ -193,7 +197,7 @@ let rec nf_val env sigma v typ = | Vaccu accu -> nf_accu env sigma accu | Vfun f -> let lvl = nb_rel env in - let name,dom,codom = + let name,dom,codom = try decompose_prod env typ with DestKO -> CErrors.anomaly @@ -274,11 +278,13 @@ and nf_atom env sigma atom = | Asort s -> mkSort s | Avar id -> mkVar id | Aprod(n,dom,codom) -> - let dom = nf_type env sigma dom in - let vn = mk_rel_accu (nb_rel env) in - let env = push_rel (LocalAssum (n,dom)) env in - let codom = nf_type env sigma (codom vn) in - mkProd(n,dom,codom) + let dom, sdom = nf_type_sort env sigma dom in + let rdom = Sorts.relevance_of_sort sdom in + let n = make_annot n rdom in + let vn = mk_rel_accu (nb_rel env) in + let env = push_rel (LocalAssum (n,dom)) env in + let codom = nf_type env sigma (codom vn) in + mkProd(n,dom,codom) | Ameta (mv,_) -> mkMeta mv | Aproj (p, c) -> let c = nf_accu env sigma c in @@ -324,28 +330,34 @@ and nf_atom_type env sigma atom = let ci = ans.asw_ci in mkCase(ci, p, a, branchs), tcase | Afix(tt,ft,rp,s) -> - let tt = Array.map (fun t -> nf_type env sigma t) tt in - let name = Array.map (fun _ -> (Name (Id.of_string "Ffix"))) tt in + 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 + let name = Name (Id.of_string "Ffix") in + let names = Array.map (fun s -> make_annot name (Sorts.relevance_of_sort s)) rt in let lvl = nb_rel env in let nbfix = Array.length ft in let fargs = mk_rels_accu lvl (Array.length ft) in - (* Third argument of the tuple is ignored by push_rec_types *) - let env = push_rec_types (name,tt,[||]) env in + (* Body argument of the tuple is ignored by push_rec_types *) + let env = push_rec_types (names,tt,[||]) env in (* We lift here because the types of arguments (in tt) will be evaluated in an environment where the fixpoints have been pushed *) let norm_body i v = nf_val env sigma (napply v fargs) (lift nbfix tt.(i)) in let ft = Array.mapi norm_body ft in - mkFix((rp,s),(name,tt,ft)), tt.(s) + mkFix((rp,s),(names,tt,ft)), tt.(s) | Acofix(tt,ft,s,_) | Acofixe(tt,ft,s,_) -> - let tt = Array.map (nf_type env sigma) tt in - let name = Array.map (fun _ -> (Name (Id.of_string "Fcofix"))) tt in + 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 + let name = Name (Id.of_string "Fcofix") in let lvl = nb_rel env in + let names = Array.map (fun s -> make_annot name (Sorts.relevance_of_sort s)) rt in let fargs = mk_rels_accu lvl (Array.length ft) in - let env = push_rec_types (name,tt,[||]) env in + let env = push_rec_types (names,tt,[||]) env in let ft = Array.mapi (fun i v -> nf_val env sigma (napply v fargs) tt.(i)) ft in - mkCoFix(s,(name,tt,ft)), tt.(s) + mkCoFix(s,(names,tt,ft)), tt.(s) | Aprod(n,dom,codom) -> let dom,s1 = nf_type_sort env sigma dom in + let r1 = Sorts.relevance_of_sort s1 in + let n = make_annot n r1 in let vn = mk_rel_accu (nb_rel env) in let env = push_rel (LocalAssum (n,dom)) env in let codom,s2 = nf_type_sort env sigma (codom vn) in @@ -389,6 +401,8 @@ and nf_predicate env sigma ind mip params v pT = let rargs = Array.init n (fun i -> mkRel (n-i)) in let params = if Int.equal n 0 then params else Array.map (lift n) params in let dom = mkApp(mkIndU ind,Array.append params rargs) in + let r = Inductive.relevance_of_inductive env (fst ind) in + let name = make_annot name r in let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in mkLambda(name,dom,body) | _ -> nf_type env sigma v diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 6803ea7d9b..13034d078a 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -15,6 +15,7 @@ open Globnames open Nameops open Term open Constr +open Context open Glob_term open Pp open Mod_subst @@ -153,16 +154,20 @@ let pattern_of_constr env sigma t = | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) | Var id -> PVar id + | Sort SProp -> PSort GSProp | Sort Prop -> PSort GProp | Sort Set -> PSort GSet | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr env c - | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t), - pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b) - | Prod (na,c,b) -> PProd (na,pattern_of_constr env c, - pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) - | Lambda (na,c,b) -> PLambda (na,pattern_of_constr env c, - pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) + | LetIn (na,c,t,b) -> PLetIn (na.binder_name, + pattern_of_constr env c,Some (pattern_of_constr env t), + pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b) + | Prod (na,c,b) -> PProd (na.binder_name, + pattern_of_constr env c, + pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) + | Lambda (na,c,b) -> PLambda (na.binder_name, + pattern_of_constr env c, + pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | App (f,a) -> (match match kind f with @@ -206,12 +211,12 @@ let pattern_of_constr env sigma t = | 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 - PFix (lni,(lna,Array.map (pattern_of_constr env) tl, + PFix (lni,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl, Array.map (pattern_of_constr env') bl)) | CoFix (ln,(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 - PCoFix (ln,(lna,Array.map (pattern_of_constr env) tl, + PCoFix (ln,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl, Array.map (pattern_of_constr env') bl)) | Int i -> PInt i in pattern_of_constr env t diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index dc6607557d..35a7036af4 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -60,6 +60,7 @@ type pretype_error = | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of (Evar.t * Evar_kinds.t) option * Evar.Set.t option + | DisallowedSProp exception PretypeError of env * Evd.evar_map * pretype_error @@ -107,9 +108,9 @@ let error_ill_typed_rec_body ?loc env sigma i na jl tys = raise_type_error ?loc (env, sigma, IllTypedRecBody (i, na, jl, tys)) -let error_elim_arity ?loc env sigma pi s c j a = +let error_elim_arity ?loc env sigma pi c j a = raise_type_error ?loc - (env, sigma, ElimArity (pi, s, c, j, a)) + (env, sigma, ElimArity (pi, c, j, a)) let error_not_a_type ?loc env sigma j = raise_type_error ?loc (env, sigma, NotAType j) @@ -171,6 +172,9 @@ let error_var_not_found ?loc env sigma s = let error_evar_not_found ?loc env sigma id = raise_pretype_error ?loc (env, sigma, EvarNotFound id) +let error_disallowed_sprop env sigma = + raise (PretypeError (env, sigma, DisallowedSProp)) + (*s Typeclass errors *) let unsatisfiable_constraints env evd ev comp = diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index a0d459fe6b..a9e2b0ea8f 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -67,6 +67,7 @@ type pretype_error = | UnsatisfiableConstraints of (Evar.t * Evar_kinds.t) option * Evar.Set.t option (** unresolvable evar, connex component *) + | DisallowedSProp exception PretypeError of env * Evd.evar_map * pretype_error @@ -101,12 +102,12 @@ val error_number_branches : val error_ill_typed_rec_body : ?loc:Loc.t -> env -> Evd.evar_map -> - int -> Name.t array -> unsafe_judgment array -> types array -> 'b + int -> Name.t Context.binder_annot array -> unsafe_judgment array -> types array -> 'b val error_elim_arity : ?loc:Loc.t -> env -> Evd.evar_map -> - pinductive -> Sorts.family list -> constr -> - unsafe_judgment -> (Sorts.family * Sorts.family * arity_error) option -> 'b + pinductive -> constr -> + unsafe_judgment -> (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'b val error_not_a_type : ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b @@ -158,6 +159,8 @@ val error_var_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b val error_evar_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b +val error_disallowed_sprop : env -> Evd.evar_map -> 'a + (** {6 Typeclass errors } *) val unsatisfiable_constraints : env -> Evd.evar_map -> Evar.t option -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a92b245b91..8e9a2e114b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -29,7 +29,7 @@ open Util open Names open Evd open Constr -open Term +open Context open Termops open Environ open EConstr @@ -266,7 +266,7 @@ let apply_inference_hook hook env sigma frozen = match frozen with let apply_heuristics env sigma fail_evar = (* Resolve eagerly, potentially making wrong choices *) try solve_unif_constraints_with_heuristics - ~ts:(Typeclasses.classes_transparent_state ()) env sigma + ~flags:(default_flags_of (Typeclasses.classes_transparent_state ())) env sigma with e when CErrors.noncritical e -> let e = CErrors.push e in if fail_evar then iraise e else sigma @@ -399,11 +399,13 @@ let pretype_id pretype k0 loc env sigma id = (* Main pretyping function *) let interp_known_glob_level ?loc evd = function + | GSProp -> Univ.Level.sprop | GProp -> Univ.Level.prop | GSet -> Univ.Level.set | GType s -> interp_known_level_info ?loc evd s let interp_glob_level ?loc evd : glob_level -> _ = function + | GSProp -> evd, Univ.Level.sprop | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set | GType s -> interp_level_info ?loc evd s @@ -448,11 +450,12 @@ let pretype_ref ?loc sigma env ref us = let judge_of_Type ?loc evd s = let evd, s = interp_universe ?loc evd s in let judge = - { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } + { uj_val = mkType s; uj_type = mkType (Univ.super s) } in evd, judge let pretype_sort ?loc sigma = function + | GSProp -> sigma, judge_of_sprop | GProp -> sigma, judge_of_prop | GSet -> sigma, judge_of_set | GType s -> judge_of_Type ?loc sigma s @@ -473,8 +476,8 @@ let mark_obligation_evar sigma k evc = let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t = let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc in - let pretype_type = pretype_type k0 resolve_tc in - let pretype = pretype k0 resolve_tc in + let pretype_type = pretype_type ~program_mode k0 resolve_tc in + let pretype = pretype ~program_mode k0 resolve_tc in let open Context.Rel.Declaration in let loc = t.CAst.loc in match DAst.get t with @@ -483,7 +486,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo inh_conv_coerce_to_tycon ?loc env sigma t_ref tycon | GVar id -> - let sigma, t_id = pretype_id (fun e r t -> pretype ~program_mode tycon e r t) k0 loc env sigma id in + let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) k0 loc env sigma id in inh_conv_coerce_to_tycon ?loc env sigma t_id tycon | GEvar (id, inst) -> @@ -535,21 +538,23 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo let rec type_bl env sigma ctxt = function | [] -> sigma, ctxt | (na,bk,None,ty)::bl -> - let sigma, ty' = pretype_type ~program_mode empty_valcon env sigma ty in - let dcl = LocalAssum (na, ty'.utj_val) in + let sigma, ty' = pretype_type empty_valcon env sigma ty in + let rty' = Sorts.relevance_of_sort ty'.utj_type in + let dcl = LocalAssum (make_annot na rty', ty'.utj_val) in let dcl', env = push_rel ~hypnaming sigma dcl env in type_bl env sigma (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> - let sigma, ty' = pretype_type ~program_mode empty_valcon env sigma ty in - let sigma, bd' = pretype ~program_mode (mk_tycon ty'.utj_val) env sigma bd in - let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in + let sigma, ty' = pretype_type empty_valcon env sigma ty in + let rty' = Sorts.relevance_of_sort ty'.utj_type in + let sigma, bd' = pretype (mk_tycon ty'.utj_val) env sigma bd in + let dcl = LocalDef (make_annot na rty', bd'.uj_val, ty'.utj_val) in let dcl', env = push_rel ~hypnaming sigma dcl env in type_bl env sigma (Context.Rel.add dcl' ctxt) bl in let sigma, ctxtv = Array.fold_left_map (fun sigma -> type_bl env sigma Context.Rel.empty) sigma bl in let sigma, larj = Array.fold_left2_map (fun sigma e ar -> - pretype_type ~program_mode empty_valcon (snd (push_rel_context ~hypnaming sigma e env)) sigma ar) + pretype_type empty_valcon (snd (push_rel_context ~hypnaming sigma e env)) sigma ar) sigma ctxtv lar in let lara = Array.map (fun a -> a.utj_val) larj in let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in @@ -562,12 +567,16 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo | GFix (vn,i) -> i | GCoFix i -> i in - begin match conv !!env sigma ftys.(fixi) t with - | None -> sigma - | Some sigma -> sigma + begin match Evarconv.unify_delay !!env sigma ftys.(fixi) t with + | exception Evarconv.UnableToUnify _ -> sigma + | sigma -> sigma end | None -> sigma in + let names = Array.map2 (fun na t -> + make_annot na (Retyping.relevance_of_type !!(env) sigma t)) + names ftys + in (* Note: bodies are not used by push_rec_types, so [||] is safe *) let names,newenv = push_rec_types ~hypnaming sigma (names,ftys) env in let sigma, vdefj = @@ -579,7 +588,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo decompose_prod_n_assum sigma (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in let ctxt,nenv = push_rel_context ~hypnaming sigma ctxt newenv in - let sigma, j = pretype ~program_mode (mk_tycon ty) nenv sigma def in + let sigma, j = pretype (mk_tycon ty) nenv sigma def in sigma, { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) sigma ctxtv vdef in @@ -602,10 +611,10 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i)) vn) in - let fixdecls = (names,ftys,fdefs) in + let fixdecls = (names,ftys,fdefs) in let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) - | GCoFix i -> + | GCoFix i -> let fixdecls = (names,ftys,fdefs) in let cofix = (i, fixdecls) in (try check_cofix !!env (i, nf_fix sigma fixdecls) @@ -622,7 +631,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo inh_conv_coerce_to_tycon ?loc env sigma j tycon | GApp (f,args) -> - let sigma, fj = pretype ~program_mode empty_tycon env sigma f in + let sigma, fj = pretype empty_tycon env sigma f in let floc = loc_of_glob_constr f in let length = List.length args in let candargs = @@ -665,24 +674,24 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo match EConstr.kind sigma resty with | Prod (na,c1,c2) -> let tycon = Some c1 in - let sigma, hj = pretype ~program_mode tycon env sigma c in + let sigma, hj = pretype tycon env sigma c in let sigma, candargs, ujval = match candargs with | [] -> sigma, [], j_val hj | arg :: args -> - begin match conv !!env sigma (j_val hj) arg with - | Some sigma -> - sigma, args, nf_evar sigma (j_val hj) - | None -> + begin match Evarconv.unify_delay !!env sigma (j_val hj) arg with + | exception Evarconv.UnableToUnify _ -> sigma, [], j_val hj + | sigma -> + sigma, args, nf_evar sigma (j_val hj) end in - let sigma, ujval = adjust_evar_source sigma na ujval in - let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in + let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in + let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in let j = { uj_val = value; uj_type = typ } in apply_rec env sigma (n+1) j candargs rest | _ -> - let sigma, hj = pretype ~program_mode empty_tycon env sigma c in + let sigma, hj = pretype empty_tycon env sigma c in error_cant_apply_not_functional ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|] in @@ -712,26 +721,28 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo in let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in let dom_valcon = valcon_of_tycon dom in - let sigma, j = pretype_type ~program_mode dom_valcon env sigma c1 in + let sigma, j = pretype_type dom_valcon env sigma c1 in + let name = {binder_name=name; binder_relevance=Sorts.relevance_of_sort j.utj_type} in let var = LocalAssum (name, j.utj_val) in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let var',env' = push_rel ~hypnaming sigma var env in - let sigma, j' = pretype ~program_mode rng env' sigma c2 in + let sigma, j' = pretype rng env' sigma c2 in let name = get_name var' in - let resj = judge_of_abstraction !!env (orelse_name name name') j j' in + let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in inh_conv_coerce_to_tycon ?loc env sigma resj tycon | GProd(name,bk,c1,c2) -> - let sigma, j = pretype_type ~program_mode empty_valcon env sigma c1 in + let sigma, j = pretype_type empty_valcon env sigma c1 in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let sigma, name, j' = match name with | Anonymous -> - let sigma, j = pretype_type ~program_mode empty_valcon env sigma c2 in + let sigma, j = pretype_type empty_valcon env sigma c2 in sigma, name, { j with utj_val = lift 1 j.utj_val } | Name _ -> - let var = LocalAssum (name, j.utj_val) in + let r = Sorts.relevance_of_sort j.utj_type in + let var = LocalAssum (make_annot name r, j.utj_val) in let var, env' = push_rel ~hypnaming sigma var env in - let sigma, c2_j = pretype_type ~program_mode empty_valcon env' sigma c2 in + let sigma, c2_j = pretype_type empty_valcon env' sigma c2 in sigma, get_name var, c2_j in let resj = @@ -747,24 +758,25 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo let sigma, tycon1 = match t with | Some t -> - let sigma, t_j = pretype_type ~program_mode empty_valcon env sigma t in + let sigma, t_j = pretype_type empty_valcon env sigma t in sigma, mk_tycon t_j.utj_val | None -> sigma, empty_tycon in - let sigma, j = pretype ~program_mode tycon1 env sigma c1 in + let sigma, j = pretype tycon1 env sigma c1 in let sigma, t = Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma j.uj_type in - let var = LocalDef (name, j.uj_val, t) in + let r = Retyping.relevance_of_term !!env sigma j.uj_val in + let var = LocalDef (make_annot name r, j.uj_val, t) in let tycon = lift_tycon 1 tycon in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let var, env = push_rel ~hypnaming sigma var env in - let sigma, j' = pretype ~program_mode tycon env sigma c2 in + let sigma, j' = pretype tycon env sigma c2 in let name = get_name var in - sigma, { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; + sigma, { uj_val = mkLetIn (make_annot name r, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } | GLetTuple (nal,(na,po),c,d) -> - let sigma, cj = pretype ~program_mode empty_tycon env sigma c in + let sigma, cj = pretype empty_tycon env sigma c in let (IndType (indf,realargs)) = try find_rectype !!env sigma cj.uj_type with Not_found -> @@ -788,10 +800,11 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo | Some ps -> let rec aux n k names l = match names, l with - | na :: names, (LocalAssum (_,t) :: l) -> + | na :: names, (LocalAssum (na', t) :: l) -> let t = EConstr.of_constr t in let proj = Projection.make ps.(cs.cs_nargs - k) true in - LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) + LocalDef ({na' with binder_name = na}, + lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) :: aux (n+1) (k + 1) names l | na :: names, (decl :: l) -> set_name na decl :: aux (n+1) k names l @@ -801,27 +814,27 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo let fsign = Context.Rel.map (whd_betaiota sigma) fsign in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in - let obj ind p v f = + let obj ind rci p v f = if not record then - let f = it_mkLambda_or_LetIn f fsign in - let ci = make_case_info !!env (fst ind) LetStyle in - mkCase (ci, p, cj.uj_val,[|f|]) + let f = it_mkLambda_or_LetIn f fsign in + let ci = make_case_info !!env (fst ind) rci LetStyle in + mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in (* Make dependencies from arity signature impossible *) - let arsgn = - let arsgn,_ = get_arity !!env indf in - List.map (set_name Anonymous) arsgn + let arsgn, indr = + let arsgn,s = get_arity !!env indf in + List.map (set_name Anonymous) arsgn, Sorts.relevance_of_sort_family s in let indt = build_dependent_inductive !!env indf in - let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) + let psign = LocalAssum (make_annot na indr, indt) :: arsgn in (* For locating names in [po] *) let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in let nar = List.length arsgn in let psign',env_p = push_rel_context ~hypnaming ~force_names:true sigma psign predenv in (match po with | Some p -> - let sigma, pj = pretype_type ~program_mode empty_valcon env_p sigma p in + let sigma, pj = pretype_type empty_valcon env_p sigma p in let ccl = nf_evar sigma pj.utj_val in let p = it_mkLambda_or_LetIn ccl psign' in let inst = @@ -829,17 +842,17 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo @[EConstr.of_constr (build_dependent_constructor cs)] in let lp = lift cs.cs_nargs p in let fty = hnf_lam_applist !!env sigma lp inst in - let sigma, fj = pretype ~program_mode (mk_tycon fty) env_f sigma d in + let sigma, fj = pretype (mk_tycon fty) env_f sigma d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort !!env sigma ind cj.uj_val p; - obj ind p cj.uj_val fj.uj_val - in + let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in + obj ind rci p cj.uj_val fj.uj_val + in sigma, { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) } | None -> let tycon = lift_tycon cs.cs_nargs tycon in - let sigma, fj = pretype ~program_mode tycon env_f sigma d in + let sigma, fj = pretype tycon env_f sigma d in let ccl = nf_evar sigma fj.uj_type in let ccl = if noccur_between sigma 1 cs.cs_nargs ccl then @@ -851,12 +864,12 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign' in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort !!env sigma ind cj.uj_val p; - obj ind p cj.uj_val fj.uj_val + let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in + obj ind rci p cj.uj_val fj.uj_val in sigma, { uj_val = v; uj_type = ccl }) | GIf (c,(na,po),b1,b2) -> - let sigma, cj = pretype ~program_mode empty_tycon env sigma c in + let sigma, cj = pretype empty_tycon env sigma c in let (IndType (indf,realargs)) = try find_rectype !!env sigma cj.uj_type with Not_found -> @@ -867,21 +880,21 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo user_err ?loc (str "If is only for inductive types with two constructors."); - let arsgn = - let arsgn,_ = get_arity !!env indf in + let arsgn, indr = + let arsgn,s = get_arity !!env indf in (* Make dependencies from arity signature impossible *) - List.map (set_name Anonymous) arsgn + List.map (set_name Anonymous) arsgn, Sorts.relevance_of_sort_family s in let nar = List.length arsgn in let indt = build_dependent_inductive !!env indf in - let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) + let psign = LocalAssum (make_annot na indr, indt) :: arsgn in (* For locating names in [po] *) let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let psign,env_p = push_rel_context ~hypnaming sigma psign predenv in let sigma, pred, p = match po with | Some p -> - let sigma, pj = pretype_type ~program_mode empty_valcon env_p sigma p in + let sigma, pj = pretype_type empty_valcon env_p sigma p in let ccl = nf_evar sigma pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in let typ = lift (- nar) (beta_applist sigma (pred,[cj.uj_val])) in @@ -904,38 +917,38 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo List.map (set_name Anonymous) cs_args in let _,env_c = push_rel_context ~hypnaming sigma csgn env in - let sigma, bj = pretype ~program_mode (mk_tycon pi) env_c sigma b in + let sigma, bj = pretype (mk_tycon pi) env_c sigma b in sigma, it_mkLambda_or_LetIn bj.uj_val cs_args in let sigma, b1 = f sigma cstrs.(0) b1 in let sigma, b2 = f sigma cstrs.(1) b2 in let v = let ind,_ = dest_ind_family indf in - let ci = make_case_info !!env (fst ind) IfStyle in let pred = nf_evar sigma pred in - Typing.check_allowed_sort !!env sigma ind cj.uj_val pred; - mkCase (ci, pred, cj.uj_val, [|b1;b2|]) + 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, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in inh_conv_coerce_to_tycon ?loc env sigma cj tycon | GCases (sty,po,tml,eqns) -> - Cases.compile_cases ?loc ~program_mode sty (pretype ~program_mode, sigma) tycon env (po,tml,eqns) + Cases.compile_cases ?loc ~program_mode sty (pretype, sigma) tycon env (po,tml,eqns) | GCast (c,k) -> let sigma, cj = match k with | CastCoerce -> - let sigma, cj = pretype ~program_mode empty_tycon env sigma c in + let sigma, cj = pretype empty_tycon env sigma c in Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in - let sigma, tj = pretype_type ~program_mode empty_valcon env sigma t in + let sigma, tj = pretype_type empty_valcon env sigma t in let sigma, tval = Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma tj.utj_val in let tval = nf_evar sigma tval in let (sigma, cj), tval = match k with | VMcast -> - let sigma, cj = pretype ~program_mode empty_tycon env sigma c in + let sigma, cj = pretype empty_tycon env sigma c in let cty = nf_evar sigma cj.uj_type and tval = nf_evar sigma tval in if not (occur_existential sigma cty || occur_existential sigma tval) then match Reductionops.vm_infer_conv !!env sigma cty tval with @@ -946,7 +959,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo else user_err ?loc (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> - let sigma, cj = pretype ~program_mode empty_tycon env sigma c in + let sigma, cj = pretype empty_tycon env sigma c in let cty = nf_evar sigma cj.uj_type and tval = nf_evar sigma tval in begin match Nativenorm.native_infer_conv !!env sigma cty tval with @@ -956,7 +969,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo (ConversionFailed (!!env,cty,tval)) end | _ -> - pretype ~program_mode (mk_tycon tval) env sigma c, tval + pretype (mk_tycon tval) env sigma c, tval in let v = mkCast (cj.uj_val, k, tval) in sigma, { uj_val = v; uj_type = tval } @@ -1060,9 +1073,9 @@ and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match valcon with | None -> sigma, tj | Some v -> - begin match cumul !!env sigma v tj.utj_val with - | Some sigma -> sigma, tj - | None -> + begin match Evarconv.unify_leq_delay !!env sigma v tj.utj_val with + | sigma -> sigma, tj + | exception Evarconv.UnableToUnify _ -> error_unexpected_type ?loc:(loc_of_glob_constr c) !!env sigma tj.utj_val v end diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index d0359b43f4..34a6cecc95 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -5,10 +5,10 @@ Pretype_errors Reductionops Inductiveops InferCumulativity -Vnorm Arguments_renaming -Nativenorm Retyping +Vnorm +Nativenorm Cbv Find_subterm Evardefine diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 98ca329117..71fbfe8716 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -12,6 +12,7 @@ open CErrors open Util open Names open Constr +open Context open Termops open Univ open Evd @@ -479,10 +480,10 @@ 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,br,alt) -> Case (info, f ty, Array.map f br, alt) - | Fix ((r,(na,ty,bo)),arg,alt) -> - Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg,alt) - | Cst (cst,curr,remains,params,alt) -> + | Case (info,ty,br,alt) -> Case (info, f ty, Array.map f br, alt) + | Fix ((r,(na,ty,bo)),arg,alt) -> + Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg,alt) + | Cst (cst,curr,remains,params,alt) -> Cst (cst,curr,remains,map f params,alt) | Primitive (p,c,args,kargs,cst_l) -> Primitive(p,c, map f args, kargs, cst_l) @@ -775,7 +776,7 @@ let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbo | Some e -> match reference with | None -> bd - | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in + | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -817,7 +818,7 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies | Some e -> match reference with | None -> bd - | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in + | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -1062,7 +1063,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> - let env' = push_rel (LocalAssum (na, t)) env in + let env' = push_rel (LocalAssum (na, t)) env in let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with | App (f,cl) -> @@ -1520,7 +1521,9 @@ let plain_instance sigma s c = match EConstr.kind sigma g with | App _ -> let l' = Array.Fun1.Smart.map lift 1 l' in - mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l')) + let r = Sorts.Relevant in (* TODO fix relevance *) + let na = make_annot (Name default_plain_instance_ident) r in + mkLetIn (na,g,t,mkApp(mkRel 1, l')) | _ -> mkApp (g,l') with Not_found -> mkApp (f,l')) | _ -> mkApp (irec n f,l')) @@ -1623,11 +1626,11 @@ let splay_prod_assum env sigma = let t = whd_allnolet env sigma c in match EConstr.kind sigma t with | Prod (x,t,c) -> - prodec_rec (push_rel (LocalAssum (x,t)) env) - (Context.Rel.add (LocalAssum (x,t)) l) c + prodec_rec (push_rel (LocalAssum (x,t)) env) + (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> - prodec_rec (push_rel (LocalDef (x,b,t)) env) - (Context.Rel.add (LocalDef (x,b,t)) l) c + prodec_rec (push_rel (LocalDef (x,b,t)) env) + (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> let t' = whd_all env sigma t in @@ -1648,8 +1651,8 @@ let splay_prod_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match EConstr.kind sigma (whd_all env sigma c) with | Prod (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 + decrec (push_rel (LocalAssum (n,a)) env) + (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 | _ -> invalid_arg "splay_prod_n" in decrec env n Context.Rel.empty @@ -1658,8 +1661,8 @@ let splay_lam_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match EConstr.kind sigma (whd_all env sigma c) with | Lambda (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 + decrec (push_rel (LocalAssum (n,a)) env) + (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 | _ -> invalid_arg "splay_lam_n" in decrec env n Context.Rel.empty diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index fae0b23b83..5938d9b367 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -235,9 +235,9 @@ val hnf_lam_app : env -> evar_map -> constr -> constr -> constr val hnf_lam_appvect : env -> evar_map -> constr -> constr array -> constr val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr -val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr -val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr -val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * ESorts.t +val splay_prod : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr +val splay_lam : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr +val splay_arity : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * ESorts.t val sort_of_arity : env -> evar_map -> constr -> ESorts.t val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index a76a203e37..20120f4182 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -13,6 +13,7 @@ open CErrors open Util open Term open Constr +open Context open Inductive open Inductiveops open Names @@ -79,7 +80,8 @@ let rec subst_type env sigma typ = function let sort_of_atomic_type env sigma ft args = let rec concl_of_arity env n ar args = match EConstr.kind sigma (whd_all env sigma ar), args with - | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l + | Prod (na, t, b), h::l -> + concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l | Sort s, [] -> ESorts.kind sigma s | _ -> retype_error NotASort in concl_of_arity env 0 ft (Array.to_list args) @@ -150,8 +152,8 @@ let retype ?(polyprop=true) sigma = | Cast (c,_, s) when isSort sigma s -> destSort sigma s | Sort s -> begin match ESorts.kind sigma s with - | Prop | Set -> Sorts.type1 - | Type u -> Type (Univ.super u) + | SProp | Prop | Set -> Sorts.type1 + | Type u -> Sorts.sort_of_univ (Univ.super u) end | Prod (name,t,c2) -> let dom = sort_of env t in @@ -188,7 +190,7 @@ let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s) | Sort _ -> InType | Prod (name,t,c2) -> - let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in + let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in if not (is_impredicative_set env) && s2 == InSet && sort_family_of env t == InType then InType else s2 | App(f,args) when Termops.is_template_polymorphic_ind env sigma f -> @@ -256,3 +258,41 @@ let expand_projection env sigma pr c args = in mkApp (mkConstU (Projection.constant pr,u), Array.of_list (ind_args @ (c :: args))) + +let relevance_of_term env sigma c = + if Environ.sprop_allowed env then + let rec aux rels c = + match kind sigma c with + | Rel n -> Retypeops.relevance_of_rel_extra env rels n + | Var x -> Retypeops.relevance_of_var env x + | Sort _ -> Sorts.Relevant + | Cast (c, _, _) -> aux rels c + | Prod ({binder_relevance=r}, _, codom) -> + aux (r::rels) codom + | Lambda ({binder_relevance=r}, _, bdy) -> + aux (r::rels) bdy + | LetIn ({binder_relevance=r}, _, _, bdy) -> + aux (r::rels) bdy + | App (c, _) -> aux rels c + | Const (c,_) -> Retypeops.relevance_of_constant env c + | Ind _ -> Sorts.Relevant + | Construct (c,_) -> Retypeops.relevance_of_constructor env c + | Case (ci, _, _, _) -> ci.ci_relevance + | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance + | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance + | Proj (p, _) -> Retypeops.relevance_of_projection env p + | Int _ -> Sorts.Relevant + + | Meta _ | Evar _ -> Sorts.Relevant + + in + aux [] c + else Sorts.Relevant + +let relevance_of_type env sigma t = + let s = get_sort_family_of env sigma t in + Sorts.relevance_of_sort_family s + +let relevance_of_sort s = Sorts.relevance_of_sort (EConstr.Unsafe.to_sorts s) + +let relevance_of_sort_family f = Sorts.relevance_of_sort_family f diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 2aff0c7775..252bfb1a84 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -53,3 +53,8 @@ val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list val expand_projection : env -> evar_map -> Names.Projection.t -> constr -> constr list -> constr val print_retype_error : retype_error -> Pp.t + +val relevance_of_term : env -> evar_map -> constr -> Sorts.relevance +val relevance_of_type : env -> evar_map -> types -> Sorts.relevance +val relevance_of_sort : ESorts.t -> Sorts.relevance +val relevance_of_sort_family : Sorts.family -> Sorts.relevance diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2308a541fb..bcc20a41b4 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -13,6 +13,7 @@ open CErrors open Util open Names open Constr +open Context open Libnames open Globnames open Termops @@ -229,7 +230,8 @@ let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) = (* Heuristic to look if global names are associated to other components of a mutual fixpoint *) -let invert_name labs l na0 env sigma ref = function +let invert_name labs l {binder_name=na0} env sigma ref na = + match na.binder_name with | Name id -> let minfxargs = List.length l in begin match na0 with @@ -249,7 +251,7 @@ let invert_name labs l na0 env sigma ref = function | Some c -> let labs',ccl = decompose_lam sigma c in let _, l' = whd_betalet_stack sigma ccl in - let labs' = List.map snd labs' in + let labs' = List.map snd labs' in (* ppedrot: there used to be generic equality on terms here *) let eq_constr c1 c2 = EConstr.eq_constr sigma c1 c2 in if List.equal eq_constr labs' labs && @@ -269,7 +271,7 @@ let compute_consteval_direct env sigma ref = match EConstr.kind sigma c' with | Lambda (id,t,g) when List.is_empty l && not onlyproj -> let open Context.Rel.Declaration in - srec (push_rel (LocalAssum (id,t)) env) (n+1) (t::labs) onlyproj g + srec (push_rel (LocalAssum (id,t)) env) (n+1) (t::labs) onlyproj g | Fix fix when not onlyproj -> (try check_fix_reversibility sigma labs l fix with Elimconst -> NotAnElimination) @@ -289,7 +291,7 @@ let compute_consteval_mutual_fix env sigma ref = match EConstr.kind sigma c' with | Lambda (na,t,g) when List.is_empty l -> let open Context.Rel.Declaration in - srec (push_rel (LocalAssum (na,t)) env) (minarg+1) (t::labs) ref g + srec (push_rel (LocalAssum (na,t)) env) (minarg+1) (t::labs) ref g | Fix ((lv,i),(names,_,_)) -> (* Last known constant wrapping Fix is ref = [labs](Fix l) *) (match compute_consteval_direct env sigma ref with @@ -374,7 +376,8 @@ let make_elim_fun (names,(nbfix,lv,n)) u largs = 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 - mkLambda (x,tij',c)) 1 body (List.rev lv) + let x = make_annot x Sorts.Relevant in (* TODO relevance *) + mkLambda (x,tij',c)) 1 body (List.rev lv) in Some (minargs,g) (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]: @@ -384,7 +387,8 @@ 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 (vfx, dummy); LocalAssum (vfun, dummy)] + 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 @@ -513,7 +517,7 @@ let reduce_mind_case_use_function func env sigma mia = let minargs = List.length mia.mcargs in fun i -> if Int.equal i bodynum then Some (minargs,func) - else match names.(i) with + else match names.(i).binder_name with | Anonymous -> None | Name id -> (* In case of a call to another component of a block of @@ -627,12 +631,12 @@ let whd_nothing_for_iota env sigma s = | Rel n -> let open Context.Rel.Declaration in (match lookup_rel n env with - | LocalDef (_,body,_) -> whrec (lift n body, stack) + | LocalDef (_,body,_) -> whrec (lift n body, stack) | _ -> s) | Var id -> let open Context.Named.Declaration in (match lookup_named id env with - | LocalDef (_,body,_) -> whrec (body, stack) + | LocalDef (_,body,_) -> whrec (body, stack) | _ -> s) | Evar ev -> s | Meta ev -> @@ -838,10 +842,10 @@ let try_red_product env sigma c = | Cast (c,_,_) -> redrec env c | Prod (x,a,b) -> let open Context.Rel.Declaration in - mkProd (x, a, redrec (push_rel (LocalAssum (x, a)) env) b) + 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,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf)) - | Proj (p, c) -> + | Proj (p, c) -> let c' = match EConstr.kind sigma c with | Construct _ -> c @@ -1105,6 +1109,7 @@ let unfoldoccs env sigma (occs,name) 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 = @@ -1149,6 +1154,7 @@ let compute = cbv_betadeltaiota let abstract_scheme env sigma (locc,a) (c, sigma) = let ta = Retyping.get_type_of env sigma a in let na = named_hd env sigma ta Anonymous in + let na = make_annot na Sorts.Relevant in (* TODO relevance *) if occur_meta sigma ta then user_err Pp.(str "Cannot find a type for the generalisation."); if occur_meta sigma a then mkLambda (na,ta,c), sigma @@ -1191,7 +1197,7 @@ let reduce_to_ind_gen allow_product env sigma t = | Prod (n,ty,t') -> let open Context.Rel.Declaration in if allow_product then - elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l) + elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l) else user_err (str"Not an inductive definition.") | _ -> @@ -1269,7 +1275,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = | Prod (n,ty,t') -> if allow_product then let open Context.Rel.Declaration in - elimrec (push_rel (LocalAssum (n,t)) env) t' ((LocalAssum (n,ty))::l) + elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l) else error_cannot_recognize ref | _ -> diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d732544c5c..1496712bbc 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -124,12 +124,14 @@ let typeclass_univ_instance (cl, u) = let class_info c = try GlobRef.Map.find c !classes - with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c)) + with Not_found -> + let env = Global.env() in + not_a_class env (Evd.from_env env) (EConstr.of_constr (printable_constr_of_global c)) let global_class_of_constr env sigma c = try let gr, u = Termops.global_of_constr sigma c in - class_info gr, u - with Not_found -> not_a_class env c + GlobRef.Map.find gr !classes, u + with Not_found -> not_a_class env sigma c let dest_class_app env sigma c = let cl, args = EConstr.decompose_app sigma c in diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 2720a3e4de..af5b3016c9 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -20,10 +20,10 @@ type typeclass_error = | NotAClass of constr | UnboundMethod of GlobRef.t * lident (* Class name, method *) -exception TypeClassError of env * typeclass_error +exception TypeClassError of env * Evd.evar_map * typeclass_error -let typeclass_error env err = raise (TypeClassError (env, err)) +let typeclass_error env sigma err = raise (TypeClassError (env, sigma, err)) -let not_a_class env c = typeclass_error env (NotAClass c) +let not_a_class env sigma c = typeclass_error env sigma (NotAClass c) -let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id)) +let unbound_method env sigma cid id = typeclass_error env sigma (UnboundMethod (cid, id)) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 9831627a9a..fd75781ed5 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -18,9 +18,10 @@ type typeclass_error = | NotAClass of constr | UnboundMethod of GlobRef.t * lident (** Class name, method *) -exception TypeClassError of env * typeclass_error +exception TypeClassError of env * Evd.evar_map * typeclass_error -val not_a_class : env -> constr -> 'a +val typeclass_error : env -> Evd.evar_map -> typeclass_error -> 'a -val unbound_method : env -> GlobRef.t -> lident -> 'a +val not_a_class : env -> Evd.evar_map -> constr -> 'a +val unbound_method : env -> Evd.evar_map -> GlobRef.t -> lident -> 'a diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 2e50e1ab3f..89f72c874b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -15,6 +15,7 @@ open CErrors open Util open Term open Constr +open Context open Environ open EConstr open Vars @@ -65,16 +66,16 @@ let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv = match EConstr.kind sigma (whd_all env sigma typ) with | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in let (_,c1,c2) = destProd sigma t in sigma, (c1,c2) | _ -> error_cant_apply_not_functional env sigma funj argjv in - begin match Evarconv.cumul env sigma hj.uj_type c1 with - | Some sigma -> + begin match Evarconv.unify_leq_delay env sigma hj.uj_type c1 with + | sigma -> apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl - | None -> + | exception Evarconv.UnableToUnify _ -> error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv end in @@ -90,16 +91,16 @@ let judge_of_apply env sigma funj argjv = match EConstr.kind sigma (whd_all env sigma typ) with | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in let (_,c1,c2) = destProd sigma t in sigma, (c1,c2) | _ -> error_cant_apply_not_functional env sigma funj argjv in - begin match Evarconv.cumul env sigma hj.uj_type c1 with - | Some sigma -> + begin match Evarconv.unify_leq_delay env sigma hj.uj_type c1 with + | sigma -> apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl - | None -> + | exception Evarconv.UnableToUnify _ -> error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv end in @@ -109,9 +110,9 @@ let check_branch_types env sigma (ind,u) cj (lfj,explft) = if not (Int.equal (Array.length lfj) (Array.length explft)) then error_number_branches env sigma cj (Array.length explft); Array.fold_left2_i (fun i sigma lfj explft -> - match Evarconv.cumul env sigma lfj.uj_type explft with - | Some sigma -> sigma - | None -> + match Evarconv.unify_leq_delay env sigma lfj.uj_type explft with + | sigma -> sigma + | exception Evarconv.UnableToUnify _ -> error_ill_formed_branch env sigma cj.uj_val ((ind,i+1),u) lfj.uj_type explft) sigma lfj explft @@ -122,25 +123,25 @@ let max_sort l = let is_correct_arity env sigma c pj ind specif params = let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in let allowed_sorts = elim_sorts specif in - let error () = Pretype_errors.error_elim_arity env sigma ind allowed_sorts c pj None in + let error () = Pretype_errors.error_elim_arity env sigma ind c pj None in let rec srec env sigma pt ar = let pt' = whd_all env sigma pt in match EConstr.kind sigma pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> - begin match Evarconv.cumul env sigma a1 a1' with - | None -> error () - | Some sigma -> + begin match Evarconv.unify_leq_delay env sigma a1 a1' with + | exception Evarconv.UnableToUnify _ -> error () + | sigma -> srec (push_rel (LocalAssum (na1,a1)) env) sigma t ar' end | Sort s, [] -> let s = ESorts.kind sigma s in if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () - else sigma + else sigma, s | Evar (ev,_), [] -> let sigma, s = Evd.fresh_sort_in_family sigma (max_sort allowed_sorts) in let sigma = Evd.define ev (mkSort s) sigma in - sigma + sigma, s | _, (LocalDef _ as d)::ar' -> srec (push_rel d env) sigma (lift 1 pt') ar' | _ -> @@ -165,20 +166,20 @@ let type_case_branches env sigma (ind,largs) pj c = let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in let params = List.map EConstr.Unsafe.to_constr params in - let sigma = is_correct_arity env sigma c pj ind specif params in + let sigma, ps = is_correct_arity env sigma c pj ind specif params in let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in let lc = Array.map EConstr.of_constr lc in let n = (snd specif).Declarations.mind_nrealdecls in let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in - sigma, (lc, ty) + sigma, (lc, ty, Sorts.relevance_of_sort ps) let judge_of_case env sigma ci pj 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 let indspec = ((ind, EInstance.kind sigma u), spec) in - let _ = check_case_info env (fst indspec) ci in - let sigma, (bty,rslty) = type_case_branches env sigma indspec pj cj.uj_val in + let sigma, (bty,rslty,rci) = type_case_branches env sigma indspec pj cj.uj_val in + let () = check_case_info env (fst indspec) rci ci in let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in sigma, { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } @@ -187,9 +188,9 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj = let lt = Array.length vdefj in assert (Int.equal (Array.length lar) lt); Array.fold_left2_i (fun i sigma defj ar -> - match Evarconv.cumul env sigma defj.uj_type (lift lt ar) with - | Some sigma -> sigma - | None -> + match Evarconv.unify_leq_delay env sigma defj.uj_type (lift lt ar) with + | sigma -> sigma + | exception Evarconv.UnableToUnify _ -> error_ill_typed_rec_body ?loc env sigma i lna vdefj lar) sigma vdefj lar @@ -203,18 +204,20 @@ let check_allowed_sort env sigma ind c p = let _, s = splay_prod env sigma pj.uj_type in let ksort = match EConstr.kind sigma s with | Sort s -> Sorts.family (ESorts.kind sigma s) - | _ -> error_elim_arity env sigma ind sorts c pj None in + | _ -> error_elim_arity env sigma ind c pj None in if not (List.exists ((==) ksort) sorts) then let s = inductive_sort_family (snd specif) in - error_elim_arity env sigma ind sorts c pj - (Some(ksort,s,Type_errors.error_elim_explain ksort s)) + error_elim_arity env sigma ind c pj + (Some(sorts,ksort,s,Type_errors.error_elim_explain ksort s)) + else + Sorts.relevance_of_sort_family ksort let judge_of_cast env sigma cj k tj = let expected_type = tj.utj_val in - match Evarconv.cumul env sigma cj.uj_type expected_type with - | None -> + match Evarconv.unify_leq_delay env sigma cj.uj_type expected_type with + | exception Evarconv.UnableToUnify _ -> error_actual_type_core env sigma cj expected_type; - | Some sigma -> + | sigma -> sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); uj_type = expected_type } @@ -230,6 +233,10 @@ let check_cofix env sigma pcofix = (* The typing machine with universes and existential variables. *) +let judge_of_sprop = + { uj_val = EConstr.mkSProp; + uj_type = EConstr.type1 } + let judge_of_prop = { uj_val = EConstr.mkProp; uj_type = EConstr.mkSort Sorts.type1 } @@ -262,16 +269,19 @@ let judge_of_projection env sigma p cj = uj_type = ty} let judge_of_abstraction env name var j = - { uj_val = mkLambda (name, var.utj_val, j.uj_val); - uj_type = mkProd (name, var.utj_val, j.uj_type) } + let r = Sorts.relevance_of_sort var.utj_type in + { uj_val = mkLambda (make_annot name r, var.utj_val, j.uj_val); + uj_type = mkProd (make_annot name r, var.utj_val, j.uj_type) } let judge_of_product env name t1 t2 = + let r = Sorts.relevance_of_sort t1.utj_type in let s = sort_of_product env t1.utj_type t2.utj_type in - { uj_val = mkProd (name, t1.utj_val, t2.utj_val); + { uj_val = mkProd (make_annot name r, t1.utj_val, t2.utj_val); uj_type = mkSort s } let judge_of_letin env name defj typj j = - { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ; + let r = Sorts.relevance_of_sort typj.utj_type in + { uj_val = mkLetIn (make_annot name r, defj.uj_val, typj.utj_val, j.uj_val) ; uj_type = subst1 defj.uj_val j.uj_type } let check_hyps_inclusion env sigma f x hyps = @@ -349,7 +359,7 @@ let rec execute env sigma cstr = | Fix ((vn,i as vni),recdef) -> let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in - let fix = (vni,recdef') in + let fix = (vni,recdef') in check_fix env sigma fix; sigma, make_judge (mkFix fix) tys.(i) @@ -361,6 +371,9 @@ let rec execute env sigma cstr = | Sort s -> begin match ESorts.kind sigma s with + | SProp -> + if Environ.sprop_allowed env then sigma, judge_of_sprop + else error_disallowed_sprop env sigma | Prop -> sigma, judge_of_prop | Set -> sigma, judge_of_set | Type u -> sigma, judge_of_type u @@ -384,26 +397,29 @@ let rec execute env sigma cstr = | Lambda (name,c1,c2) -> let sigma, j = execute env sigma c1 in let sigma, var = type_judgment env sigma j in - let env1 = push_rel (LocalAssum (name, var.utj_val)) env in + let name = check_binder_annot var.utj_type name in + let env1 = push_rel (LocalAssum (name, var.utj_val)) env in let sigma, j' = execute env1 sigma c2 in - sigma, judge_of_abstraction env1 name var j' + sigma, judge_of_abstraction env1 name.binder_name var j' | Prod (name,c1,c2) -> let sigma, j = execute env sigma c1 in let sigma, varj = type_judgment env sigma j in - let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in + let name = check_binder_annot varj.utj_type name in + let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in let sigma, j' = execute env1 sigma c2 in let sigma, varj' = type_judgment env1 sigma j' in - sigma, judge_of_product env name varj varj' + sigma, judge_of_product env name.binder_name varj varj' | LetIn (name,c1,c2,c3) -> let sigma, j1 = execute env sigma c1 in let sigma, j2 = execute env sigma c2 in let sigma, j2 = type_judgment env sigma j2 in let sigma, _ = judge_of_cast env sigma j1 DEFAULTcast j2 in + let name = check_binder_annot j2.utj_type name in let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in let sigma, j3 = execute env1 sigma c3 in - sigma, judge_of_letin env name j1 j2 j3 + sigma, judge_of_letin env name.binder_name j1 j2 j3 | Cast (c,k,t) -> let sigma, cj = execute env sigma c in @@ -427,10 +443,10 @@ and execute_array env = Array.fold_left_map (execute env) let check env sigma c t = let sigma, j = execute env sigma c in - match Evarconv.cumul env sigma j.uj_type t with - | None -> + match Evarconv.unify_leq_delay env sigma j.uj_type t with + | exception Evarconv.UnableToUnify _ -> error_actual_type_core env sigma j t - | Some sigma -> sigma + | sigma -> sigma (* Type of a constr *) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1ea16bbf34..f68820429b 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -39,13 +39,14 @@ val solve_evars : env -> evar_map -> constr -> evar_map * constr (** Raise an error message if incorrect elimination for this inductive (first constr is term to match, second is return predicate) *) val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> - unit + Sorts.relevance (** Raise an error message if bodies have types not unifiable with the expected ones *) val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map -> - Names.Name.t array -> types array -> unsafe_judgment array -> evar_map + Names.Name.t Context.binder_annot array -> types array -> unsafe_judgment array -> evar_map +val judge_of_sprop : unsafe_judgment val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment val judge_of_apply : env -> evar_map -> unsafe_judgment -> unsafe_judgment array -> diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ac0b58b92b..9ba51dcfa9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -13,6 +13,7 @@ open Pp open Util open Names open Constr +open Context open Termops open Environ open EConstr @@ -103,13 +104,13 @@ let occur_meta_evd sigma mv c = let abstract_scheme env evd c l lname_typ = let mkLambda_name env (n,a,b) = - mkLambda (named_hd env evd a n, a, b) + mkLambda (map_annot (named_hd env evd a) n, a, b) in List.fold_left2 (fun (t,evd) (locc,a) decl -> - let na = RelDecl.get_name decl in + let na = RelDecl.get_annot decl in let ta = RelDecl.get_type decl in - let na = match EConstr.kind evd a with Var id -> Name id | _ -> na in + let na = match EConstr.kind evd a with Var id -> {na with binder_name=Name id} | _ -> na in (* [occur_meta ta] test removed for support of eelim/ecase but consequences are unclear... if occur_meta ta then error "cannot find a type for the generalisation" @@ -117,7 +118,7 @@ let abstract_scheme env evd c l lname_typ = if occur_meta evd a then mkLambda_name env (na,ta,t), evd else let t', evd' = Find_subterm.subst_closed_term_occ env evd locc a t in - mkLambda_name env (na,ta,t'), evd') + mkLambda_name env (na,ta,t'), evd') (c,evd) (List.rev l) lname_typ @@ -141,7 +142,15 @@ let abstract_list_all env evd typ c l = evd,(p,typp) let set_occurrences_of_last_arg args = - Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args) + Evarconv.AtOccurrences AllOccurrences :: + List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified Abstraction.Abstract) args) + +let occurrence_test _ _ _ env sigma _ c1 c2 = + match EConstr.eq_constr_universes env sigma c1 c2 with + | None -> false, sigma + | Some cstr -> + try true, Evd.add_universe_constraints sigma cstr + with UniversesDiffer -> false, sigma let abstract_list_all_with_dependencies env evd typ c l = let (evd, ev) = new_evar env evd typ in @@ -149,8 +158,9 @@ let abstract_list_all_with_dependencies env evd typ c l = let n = List.length l in let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in let evd,b = - Evarconv.second_order_matching TransparentState.empty - env evd ev' argoccs c in + Evarconv.second_order_matching + (Evarconv.default_flags_of TransparentState.empty) + env evd ev' (occurrence_test, argoccs) c in if b then let p = nf_evar evd ev in evd, p @@ -552,8 +562,8 @@ let is_rigid_head sigma flags t = | Ind (i,u) -> true | Construct _ | Int _ -> true | Fix _ | CoFix _ -> true - | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod (_, _, _) - | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _) + | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _ + | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _) | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) let force_eqs c = @@ -653,7 +663,7 @@ let is_eta_constructor_app env sigma ts f l1 term = let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite && - let (_, projs, _) = info.(i) in + let (_, projs, _, _) = info.(i) in Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (* Check that the other term is neutral *) is_neutral env sigma ts term @@ -773,14 +783,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e with e when CErrors.noncritical e -> error_cannot_unify curenv sigma (m,n)) - | Lambda (na,t1,c1), Lambda (_,t2,c2) -> - unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} + | Lambda (na,t1,c1), Lambda (__,t2,c2) -> + unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2 - | Prod (na,t1,c1), Prod (_,t2,c2) -> - unirec_rec (push (na,t1) curenvnb) pb {opt with at_top = true} + | Prod (na,t1,c1), Prod (_,t2,c2) -> + unirec_rec (push (na,t1) curenvnb) pb {opt with at_top = true} (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2 - | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt substn (subst1 a c) cN - | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c) + | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt substn (subst1 a c) cN + | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c) (* Fast path for projections. *) | Proj (p1,c1), Proj (p2,c2) when Constant.equal @@ -791,11 +801,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e unify_not_same_head curenvnb pb opt substn cM cN) (* eta-expansion *) - | Lambda (na,t1,c1), _ when flags.modulo_eta -> - unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} substn + | Lambda (na,t1,c1), _ when flags.modulo_eta -> + unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} substn c1 (mkApp (lift 1 cN,[|mkRel 1|])) - | _, Lambda (na,t2,c2) when flags.modulo_eta -> - unirec_rec (push (na,t2) curenvnb) CONV {opt with at_top = true} substn + | _, Lambda (na,t2,c2) when flags.modulo_eta -> + unirec_rec (push (na,t2) curenvnb) CONV {opt with at_top = true} substn (mkApp (lift 1 cM,[|mkRel 1|])) c2 (* For records *) @@ -1315,8 +1325,8 @@ let order_metas metas = (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) -let solve_simple_evar_eqn ts env evd ev rhs = - match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with +let solve_simple_evar_eqn flags env evd ev rhs = + match solve_simple_eqn Evarconv.evar_unify flags env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); | Success evd -> evd @@ -1326,6 +1336,7 @@ let solve_simple_evar_eqn ts env evd ev rhs = is true, unification of types of metas is required *) let w_merge env with_types flags (evd,metas,evars : subst0) = + let eflags = Evarconv.default_flags_of flags.modulo_delta_types in let rec w_merge_rec evd metas evars eqns = (* Process evars *) @@ -1350,14 +1361,14 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = else let evd' = let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in - try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'' + try solve_simple_evar_eqn eflags curenv evd' ev rhs'' with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev,rhs'') in w_merge_rec evd' metas evars' eqns | _ -> let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in let evd' = - try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'' + try solve_simple_evar_eqn eflags curenv evd' ev rhs'' with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev, rhs'') in w_merge_rec evd' metas evars' eqns @@ -1649,7 +1660,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> (push_named_context_val d sign,depdecls) - | AllOccurrences, InHyp as occ -> + | (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 if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl @@ -1765,7 +1776,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = matchrec c with ex when precatchable_exception ex -> iter_fail matchrec lf) - | LetIn(_,c1,_,c2) -> + | LetIn(_,c1,_,c2) -> (try matchrec c1 with ex when precatchable_exception ex -> @@ -1773,13 +1784,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = | Proj (p,c) -> matchrec c - | Fix(_,(_,types,terms)) -> + | Fix(_,(_,types,terms)) -> (try iter_fail matchrec types with ex when precatchable_exception ex -> iter_fail matchrec terms) - | CoFix(_,(_,types,terms)) -> + | CoFix(_,(_,types,terms)) -> (try iter_fail matchrec types with ex when precatchable_exception ex -> @@ -1850,13 +1861,13 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = | Proj (p,c) -> matchrec c - | LetIn(_,c1,_,c2) -> + | LetIn(_,c1,_,c2) -> bind (matchrec c1) (matchrec c2) - | Fix(_,(_,types,terms)) -> + | Fix(_,(_,types,terms)) -> bind (bind_iter matchrec types) (bind_iter matchrec terms) - | CoFix(_,(_,types,terms)) -> + | CoFix(_,(_,types,terms)) -> bind (bind_iter matchrec types) (bind_iter matchrec terms) | Prod (_,t,c) -> diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 083661a64b..62e9e477f7 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -13,6 +13,7 @@ open Names open Declarations open Term open Constr +open Context open Vars open Environ open Inductive @@ -31,10 +32,12 @@ module NamedDecl = Context.Named.Declaration let crazy_type = mkSet let decompose_prod env t = - let (name,dom,codom as res) = destProd (whd_all env t) in - match name with - | Anonymous -> (Name (Id.of_string "x"), dom, codom) - | Name _ -> res + let (name,dom,codom) = destProd (whd_all env t) in + let name = map_annot (function + | Anonymous -> Name (Id.of_string "x") + | Name _ as na -> na) name + in + (name,dom,codom) exception Find_at of int @@ -61,7 +64,8 @@ let find_rectype_a env c = (* Instantiate inductives and parameters in constructor type *) -let type_constructor mind mib u typ params = +let type_constructor mind mib u (ctx, typ) params = + let typ = it_mkProd_or_LetIn typ ctx in let s = ind_subst mind mib u in let ctyp = substl s typ in let ctyp = subst_instance_constr u ctyp in @@ -137,6 +141,8 @@ and nf_whd env sigma whd typ = let dom = nf_vtype env sigma (dom p) in let name = Name (Id.of_string "x") in let vc = reduce_fun (nb_rel env) (codom p) in + let r = Retyping.relevance_of_type env sigma (EConstr.of_constr dom) in + let name = make_annot name r in let codom = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vc in mkProd(name,dom,codom) | Vfun f -> nf_fun env sigma f typ @@ -306,6 +312,8 @@ and nf_predicate env sigma ind mip params v pT = let rargs = Array.init n (fun i -> mkRel (n-i)) in let params = if Int.equal n 0 then params else Array.map (lift n) params in let dom = mkApp(mkIndU ind,Array.append params rargs) in + let r = Inductive.relevance_of_inductive env (fst ind) in + let name = make_annot name r in let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in mkLambda(name,dom,body) | _ -> assert false @@ -316,7 +324,7 @@ and nf_args env sigma vargs ?from:(f=0) t = let args = Array.init len (fun i -> - let _,dom,codom = decompose_prod env !t in + let _,dom,codom = decompose_prod env !t in let c = nf_val env sigma (arg vargs (f+i)) dom in t := subst1 c codom; c) in !t,args @@ -327,7 +335,7 @@ and nf_bargs env sigma b ofs t = let args = Array.init len (fun i -> - let _,dom,codom = decompose_prod env !t in + let _,dom,codom = decompose_prod env !t in let c = nf_val env sigma (bfield b (i+ofs)) dom in t := subst1 c codom; c) in args @@ -352,14 +360,17 @@ and nf_fix env sigma f = let vb, vt = reduce_fix k f in let ndef = Array.length vt in let ft = Array.map (fun v -> nf_val env sigma v crazy_type) vt in - let name = Array.init ndef (fun _ -> (Name (Id.of_string "Ffix"))) in - (* Third argument of the tuple is ignored by push_rec_types *) - let env = push_rec_types (name,ft,ft) env in + let name = Name (Id.of_string "Ffix") in + let names = Array.map (fun t -> + make_annot name @@ + Retyping.relevance_of_type env sigma (EConstr.of_constr t)) ft in + (* Body argument of the tuple is ignored by push_rec_types *) + let env = push_rec_types (names,ft,ft) env in (* We lift here because the types of arguments (in tt) will be evaluated in an environment where the fixpoints have been pushed *) let norm_vb v t = nf_fun env sigma v (lift ndef t) in let fb = Util.Array.map2 norm_vb vb ft in - mkFix ((rec_args,init),(name,ft,fb)) + mkFix ((rec_args,init),(names,ft,fb)) and nf_fix_app env sigma f vargs = let fd = nf_fix env sigma f in @@ -372,12 +383,14 @@ and nf_cofix env sigma cf = let init = current_cofix cf in let k = nb_rel env in let vb,vt = reduce_cofix k cf in - let ndef = Array.length vt in let cft = Array.map (fun v -> nf_val env sigma v crazy_type) vt in - let name = Array.init ndef (fun _ -> (Name (Id.of_string "Fcofix"))) in - let env = push_rec_types (name,cft,cft) env in + let name = Name (Id.of_string "Fcofix") in + let names = Array.map (fun t -> + make_annot name @@ + Retyping.relevance_of_type env sigma (EConstr.of_constr t)) cft in + let env = push_rec_types (names,cft,cft) env in let cfb = Util.Array.map2 (fun v t -> nf_val env sigma v t) vb cft in - mkCoFix (init,(name,cft,cfb)) + mkCoFix (init,(names,cft,cfb)) let cbv_vm env sigma c t = if Termops.occur_meta sigma c then |