From f713e6c195d1de177b43cab7c2902f5160f6af9f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 24 Mar 2017 02:18:53 +0100 Subject: A fix to #5414 (ident bound by ltac names now known for "match"). Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let". --- pretyping/cases.ml | 96 +++++++++++++++++++++++++++++++++---------------- pretyping/cases.mli | 13 ++++--- pretyping/glob_ops.ml | 24 +++++++++++++ pretyping/glob_ops.mli | 3 ++ pretyping/pretyping.ml | 61 +++++++++++-------------------- pretyping/pretyping.mli | 18 ---------- 6 files changed, 123 insertions(+), 92 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c3f392980a..b88532e1b9 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -245,6 +245,7 @@ let push_history_pattern n pci cont = type 'a pattern_matching_problem = { env : env; + lvar : Glob_term.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; @@ -346,25 +347,45 @@ let find_tomatch_tycon evdref env loc = function | None -> empty_tycon,None -let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = +let make_return_predicate_ltac_lvar sigma na tm c lvar = + match na, tm.CAst.v with + | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' -> + if Id.Map.mem id lvar.ltac_genargs then + let ltac_genargs = Id.Map.remove id lvar.ltac_genargs in + let ltac_idents = match kind sigma c with + | Var id' -> Id.Map.add id id' lvar.ltac_idents + | _ -> lvar.ltac_idents in + { lvar with ltac_genargs; ltac_idents } + else lvar + | _ -> lvar + +let ltac_interp_realnames lvar = function + | t, IsInd (ty,ind,realnal) -> t, IsInd (ty,ind,List.map (ltac_interp_name lvar) realnal) + | _ as x -> x + +let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = let loc = loc_of_glob_constr tomatch in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in - let j = typing_fun tycon env evdref tomatch in + let j = typing_fun tycon env evdref !lvar tomatch in let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in evdref := evd; let typ = nf_evar !evdref j.uj_type in + lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar; let t = try try_find_ind env !evdref typ realnames with Not_found -> unify_tomatch_with_patterns evdref env loc typ pats realnames in (j.uj_val,t) -let coerce_to_indtype typing_fun evdref env matx tomatchl = +let coerce_to_indtype typing_fun evdref env lvar matx tomatchl = let pats = List.map (fun r -> r.patterns) matx in let matx' = match matrix_transpose pats with | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *) | m -> m in - List.map2 (coerce_row typing_fun evdref env) matx' tomatchl + let lvar = ref lvar in + let tms = List.map2 (coerce_row typing_fun evdref env lvar) matx' tomatchl in + let tms = List.map (ltac_interp_realnames !lvar) tms in + !lvar,tms (************************************************************************) (* Utils *) @@ -1392,6 +1413,7 @@ and match_current pb (initial,tomatch) = postprocess_dependencies !(pb.evdref) depstocheck brvals pb.tomatch pb.pred deps cstrs in let brvals = Array.map (fun (sign,body) -> + let sign = List.map (map_name (ltac_interp_name pb.lvar)) sign in it_mkLambda_or_LetIn body sign) brvals in let (pred,typ) = find_predicate pb.caseloc pb.env pb.evdref @@ -1824,6 +1846,7 @@ let build_inversion_problem loc env sigma tms t = let evdref = ref sigma in let pb = { env = pb_env; + lvar = empty_lvar; evdref = evdref; pred = (*ty *) mkSort s; tomatch = sub_tms; @@ -1847,15 +1870,15 @@ let build_initial_predicate arsign pred = | _ -> assert false in buildrec 0 pred [] (List.rev arsign) -let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = +let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = let lift = if dolift then lift else fun n t -> t in let get_one_sign n tm (na,t) = match tm with | NotInd (bo,typ) -> (match t with - | None -> (match bo with + | None -> let sign = match bo with | None -> [LocalAssum (na, lift n typ)] - | Some b -> [LocalDef (na, lift n b, lift n typ)]) + | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign,sign | Some (loc,_) -> user_err ?loc (str"Unexpected type annotation for a term of non inductive type.")) @@ -1865,22 +1888,31 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in let arsign = fst (get_arity env0 indf') in let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in - let realnal = + let realnal, realnal' = match t with | Some (loc,(ind',realnal)) -> if not (eq_ind ind ind') then user_err ?loc (str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then anomaly (Pp.str "Ill-formed 'in' clause in cases."); - List.rev realnal - | None -> List.make nrealargs_ctxt Anonymous in - LocalAssum (na, EConstr.of_constr (build_dependent_inductive env0 indf')) - ::(List.map2 RelDecl.set_name realnal arsign) in + let realnal = List.rev realnal in + let realnal' = List.map (ltac_interp_name lvar) realnal in + realnal,realnal' + | None -> + let realnal = List.make nrealargs_ctxt Anonymous in + realnal, realnal in + let na' = ltac_interp_name lvar na in + let t = EConstr.of_constr (build_dependent_inductive env0 indf') in + (* Context with names for typing *) + let arsign1 = LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in + (* Context with names for building the term *) + let arsign2 = LocalAssum (na', t) :: List.map2 RelDecl.set_name realnal' arsign in + arsign1,arsign2 in let rec buildrec n = function | [],[] -> [] | (_,tm)::ltm, (_,x)::tmsign -> let l = get_one_sign n tm x in - l :: buildrec (n + List.length l) (ltm,tmsign) + l :: buildrec (n + List.length (fst l)) (ltm,tmsign) | _ -> assert false in List.rev (buildrec 0 (tomatchl,tmsign)) @@ -1970,7 +2002,7 @@ let noccur_with_meta sigma n m term = in try (occur_rec n term; true) with LocalOccur -> false -let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = +let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred = let refresh_tycon sigma t = (** If we put the typing constraint in the term, it has to be refreshed to preserve the invariant that no algebraic universe @@ -1978,6 +2010,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true) env sigma t in + let typing_arsign,building_arsign = List.split arsign in let preds = match pred, tycon with (* No return clause *) @@ -1987,7 +2020,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = (* First strategy: we abstract the tycon wrt to the dependencies *) let sigma, t = refresh_tycon sigma t in let p1 = - prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in + prepare_predicate_from_arsign_tycon env sigma loc tomatchs typing_arsign t in (* Second strategy: we build an "inversion" predicate *) let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in (match p1 with @@ -2006,22 +2039,22 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = (* First strategy: we build an "inversion" predicate *) let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in (* Second strategy: we directly use the evar as a non dependent pred *) - let pred2 = lift (List.length (List.flatten arsign)) t in + let pred2 = lift (List.length (List.flatten typing_arsign)) t in [sigma1, pred1; sigma, pred2] (* Some type annotation *) | Some rtntyp, _ -> (* We extract the signature of the arity *) - let envar = List.fold_right push_rel_context arsign env in + let envar = List.fold_right push_rel_context typing_arsign env in let sigma, newt = new_sort_variable univ_flexible_alg sigma in let evdref = ref sigma in - let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in + let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref lvar rtntyp in let sigma = !evdref in let predccl = nf_evar sigma predcclj.uj_val in [sigma, predccl] in List.map (fun (sigma,pred) -> - let (nal,pred) = build_initial_predicate arsign pred in + let (nal,pred) = build_initial_predicate building_arsign pred in sigma,nal,pred) preds @@ -2441,10 +2474,10 @@ let context_of_arsign l = l ([], 0) in x -let compile_program_cases ?loc style (typing_function, evdref) tycon env +let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar (predopt, tomatchl, eqns) = let typing_fun tycon env = function - | Some t -> typing_function tycon env evdref t + | Some t -> typing_function tycon env evdref lvar t | None -> Evarutil.evd_comb0 use_unit_judge evdref in (* We build the matrix of patterns and right-hand side *) @@ -2452,14 +2485,15 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env (* We build the vector of terms to match consistently with the *) (* constructors found in patterns *) - let tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in + let predlvar,tomatchs = coerce_to_indtype typing_function evdref env lvar matx tomatchl in let tycon = valcon_of_tycon tycon in let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env !evdref tomatchs tycon in let env = push_rel_context tomatchs_lets env in let len = List.length eqns in let sign, allnames, signlen, eqs, neqs, args = (* The arity signature *) - let arsign = extract_arity_signature ~dolift:false env tomatchs tomatchl in + let arsign = extract_arity_signature ~dolift:false env predlvar tomatchs tomatchl in + let arsign = List.map fst arsign in (* Because no difference between the arity for typing and the arity for building *) (* Build the dependent arity signature, the equalities which makes the first part of the predicate and their instantiations. *) let avoid = [] in @@ -2522,11 +2556,12 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env let initial_pushed = List.map (fun x -> Pushed (true,x)) typs' in let typing_function tycon env evdref = function - | Some t -> typing_function tycon env evdref t + | Some t -> typing_function tycon env evdref lvar t | None -> evd_comb0 use_unit_judge evdref in let pb = { env = env; + lvar = lvar; evdref = evdref; pred = pred; tomatch = initial_pushed; @@ -2548,10 +2583,10 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env (**************************************************************************) (* Main entry of the matching compilation *) -let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) = +let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomatchl, eqns) = if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then compile_program_cases ?loc style (typing_fun, evdref) - tycon env (predopt, tomatchl, eqns) + tycon env lvar (predopt, tomatchl, eqns) else (* We build the matrix of patterns and right-hand side *) @@ -2559,15 +2594,15 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, (* We build the vector of terms to match consistently with the *) (* constructors found in patterns *) - let tomatchs = coerce_to_indtype typing_fun evdref env matx tomatchl in + let predlvar,tomatchs = coerce_to_indtype typing_fun evdref env lvar matx tomatchl in (* If an elimination predicate is provided, we check it is compatible with the type of arguments to match; if none is provided, we build alternative possible predicates *) - let arsign = extract_arity_signature env tomatchs tomatchl in - let preds = prepare_predicate ?loc typing_fun env !evdref tomatchs arsign tycon predopt in + let arsign = extract_arity_signature env predlvar tomatchs tomatchl in + let preds = prepare_predicate ?loc typing_fun env !evdref predlvar tomatchs arsign tycon predopt in let compile_for_one_predicate (sigma,nal,pred) = (* We push the initial terms to match and push their alias to rhs' envs *) @@ -2598,13 +2633,14 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, (* A typing function that provides with a canonical term for absurd cases*) let typing_fun tycon env evdref = function - | Some t -> typing_fun tycon env evdref t + | Some t -> typing_fun tycon env evdref lvar t | None -> evd_comb0 use_unit_judge evdref in let myevdref = ref sigma in let pb = { env = env; + lvar = lvar; evdref = myevdref; pred = pred; tomatch = initial_pushed; diff --git a/pretyping/cases.mli b/pretyping/cases.mli index b16342db4b..4b1fde25a8 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -39,9 +39,9 @@ val irrefutable : env -> cases_pattern -> bool val compile_cases : ?loc:Loc.t -> case_style -> - (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> + (type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) * evar_map ref -> type_constraint -> - env -> glob_constr option * tomatch_tuples * cases_clauses -> + env -> ltac_var_map -> glob_constr option * tomatch_tuples * cases_clauses -> unsafe_judgment val constr_of_pat : @@ -101,6 +101,7 @@ and pattern_continuation = type 'a pattern_matching_problem = { env : env; + lvar : Glob_term.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; @@ -115,10 +116,14 @@ val compile : 'a pattern_matching_problem -> unsafe_judgment val prepare_predicate : ?loc:Loc.t -> (Evarutil.type_constraint -> - Environ.env -> Evd.evar_map ref -> glob_constr -> unsafe_judgment) -> + Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) -> Environ.env -> Evd.evar_map -> + Glob_term.ltac_var_map -> (types * tomatch_type) list -> - rel_context list -> + (rel_context * rel_context) list -> constr option -> glob_constr option -> (Evd.evar_map * Names.name list * constr) list + +val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name -> + Glob_term.glob_constr -> constr -> Glob_term.ltac_var_map -> Glob_term.ltac_var_map diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 62ff9ac708..9c09396ccc 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -504,3 +504,27 @@ let glob_constr_of_closed_cases_pattern = function na,glob_constr_of_closed_cases_pattern_aux (CAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found + +(**********************************************************************) +(* Interpreting ltac variables *) + +open Pp +open CErrors + +let ltac_interp_name { ltac_idents ; ltac_genargs } = function + | Anonymous -> Anonymous + | Name id as n -> + try Name (Id.Map.find id ltac_idents) + with Not_found -> + if Id.Map.mem id ltac_genargs then + user_err (str"Ltac variable"++spc()++ pr_id id ++ + spc()++str"is not bound to an identifier."++spc()++ + str"It cannot be used in a binder.") + else n + +let empty_lvar : ltac_var_map = { + ltac_constrs = Id.Map.empty; + ltac_uconstrs = Id.Map.empty; + ltac_idents = Id.Map.empty; + ltac_genargs = Id.Map.empty; +} diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 75db04f77f..6bb421e732 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -83,3 +83,6 @@ val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list + +val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name +val empty_lvar : Glob_term.ltac_var_map diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 92e728683d..7488f35bfe 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -42,21 +42,11 @@ open Pretype_errors open Glob_term open Glob_ops open Evarconv -open Pattern open Misctypes module NamedDecl = Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type var_map = constr_under_binders Id.Map.t -type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t -type ltac_var_map = { - ltac_constrs : var_map; - ltac_uconstrs : uconstr_var_map; - ltac_idents: Id.t Id.Map.t; - ltac_genargs : unbound_ltac_var_map; -} type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * EConstr.constr @@ -419,17 +409,6 @@ let orelse_name name name' = match name with | Anonymous -> name' | _ -> name -let ltac_interp_name { ltac_idents ; ltac_genargs } = function - | Anonymous -> Anonymous - | Name id as n -> - try Name (Id.Map.find id ltac_idents) - with Not_found -> - if Id.Map.mem id ltac_genargs then - user_err (str"Ltac variable"++spc()++ pr_id id ++ - spc()++str"is not bound to an identifier."++spc()++ - str"It cannot be used in a binder.") - else n - let ltac_interp_name_env k0 lvar env sigma = (* envhd is the initial part of the env when pretype was called first *) (* (in practice is is probably 0, but we have to grant the @@ -943,16 +922,20 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre List.map (set_name Anonymous) arsgn else arsgn in - let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in + let indt = build_dependent_inductive env.ExtraEnv.env indf in + let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) + let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in + let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in + let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in + let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *) let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let nar = List.length arsgn in (match po with | Some p -> let env_p = push_rel_context !evdref psign env in - let pj = pretype_type empty_valcon env_p evdref lvar p in + let pj = pretype_type empty_valcon env_p evdref predlvar p in let ccl = nf_evar !evdref pj.utj_val in - let psign = make_arity_signature env.ExtraEnv.env !evdref true indf in (* with names *) - let p = it_mkLambda_or_LetIn ccl psign in + let p = it_mkLambda_or_LetIn ccl psign' in let inst = (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs) @[EConstr.of_constr (build_dependent_constructor cs)] in @@ -968,7 +951,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | None -> let tycon = lift_tycon cs.cs_nargs tycon in - let fj = pretype tycon env_f evdref lvar d in + let fj = pretype tycon env_f evdref predlvar d in let ccl = nf_evar !evdref fj.uj_type in let ccl = if noccur_between !evdref 1 cs.cs_nargs ccl then @@ -977,7 +960,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre error_cant_find_case_type ?loc env.ExtraEnv.env !evdref cj.uj_val in (* let ccl = refresh_universes ccl in *) - let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in + 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.ExtraEnv.env !evdref ind cj.uj_val p; @@ -1004,14 +987,19 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre else arsgn in let nar = List.length arsgn in - let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in + let indt = build_dependent_inductive env.ExtraEnv.env indf in + let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) + let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in + let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in + let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in + let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *) let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let pred,p = match po with | Some p -> let env_p = push_rel_context !evdref psign env in - let pj = pretype_type empty_valcon env_p evdref lvar p in + let pj = pretype_type empty_valcon env_p evdref predlvar p in let ccl = nf_evar !evdref pj.utj_val in - let pred = it_mkLambda_or_LetIn ccl psign in + let pred = it_mkLambda_or_LetIn ccl psign' in let typ = lift (- nar) (beta_applist !evdref (pred,[cj.uj_val])) in pred, typ | None -> @@ -1021,7 +1009,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let env = ltac_interp_name_env k0 lvar env !evdref in new_type_evar env evdref loc in - it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in + it_mkLambda_or_LetIn (lift (nar+1) p) psign', p in let pred = nf_evar !evdref pred in let p = nf_evar !evdref p in let f cs b = @@ -1054,8 +1042,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | GCases (sty,po,tml,eqns) -> Cases.compile_cases ?loc sty - ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref) - tycon env.ExtraEnv.env (* loc *) (po,tml,eqns) + ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref),evdref) + tycon env.ExtraEnv.env (* loc *) lvar (po,tml,eqns) | GCast (c,k) -> let cj = @@ -1198,13 +1186,6 @@ let no_classes_no_fail_inference_flags = { let all_and_fail_flags = default_inference_flags true let all_no_fail_flags = default_inference_flags false -let empty_lvar : ltac_var_map = { - ltac_constrs = Id.Map.empty; - ltac_uconstrs = Id.Map.empty; - ltac_idents = Id.Map.empty; - ltac_genargs = Id.Map.empty; -} - let on_judgment sigma f j = let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in let (c,_,t) = destCast sigma (f c) in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index dcacd07209..e17468ef83 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -12,7 +12,6 @@ into elementary ones, insertion of coercions and resolution of implicit arguments. *) -open Names open Term open Environ open Evd @@ -28,23 +27,6 @@ val search_guard : type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type var_map = Pattern.constr_under_binders Id.Map.t -type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t - -type ltac_var_map = { - ltac_constrs : var_map; - (** Ltac variables bound to constrs *) - ltac_uconstrs : uconstr_var_map; - (** Ltac variables bound to untyped constrs *) - ltac_idents: Id.t Id.Map.t; - (** Ltac variables bound to identifiers *) - ltac_genargs : unbound_ltac_var_map; - (** Ltac variables bound to other kinds of arguments *) -} - -val empty_lvar : ltac_var_map - type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr -- cgit v1.2.3 From 571c319ed536cb2757176d3ae4007a75f5d3b04d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:08:14 +0100 Subject: Remove support for Coq 8.2. --- pretyping/classops.ml | 8 ++------ pretyping/unification.ml | 1 - 2 files changed, 2 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 9a973cff55..627a9c9cc7 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -454,15 +454,11 @@ let cache_coercion (_, c) = add_coercion_in_graph (xf,is,it) let load_coercion _ o = - if - !automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2 - then + if !automatically_import_coercions then cache_coercion o let open_coercion i o = - if Int.equal i 1 && not - (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2) - then + if Int.equal i 1 && not !automatically_import_coercions then cache_coercion o let subst_coercion (subst, c) = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0fb48ed8cf..3e0eb9d91b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -481,7 +481,6 @@ let set_flags_for_type flags = { flags with let use_evars_pattern_unification flags = !global_pattern_unification_flag && flags.use_pattern_unification - && Flags.version_strictly_greater Flags.V8_2 let use_metas_pattern_unification sigma flags nb l = !global_pattern_unification_flag && flags.use_pattern_unification -- cgit v1.2.3 From daf5335b18c926d7130cd28e50f00cc49c4011f6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:12:58 +0100 Subject: Remove support for Coq 8.3. --- pretyping/unification.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3e0eb9d91b..ef4f7f7545 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -484,8 +484,7 @@ let use_evars_pattern_unification flags = let use_metas_pattern_unification sigma flags nb l = !global_pattern_unification_flag && flags.use_pattern_unification - || (Flags.version_less_or_equal Flags.V8_3 || - flags.use_meta_bound_pattern_unification) && + || flags.use_meta_bound_pattern_unification && Array.for_all (fun c -> isRel sigma c && destRel sigma c <= nb) l type key = @@ -608,9 +607,6 @@ let do_reduce ts (env, nb) sigma c = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, Stack.empty))) -let use_full_betaiota flags = - flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3 - let isAllowedEvar sigma flags c = match EConstr.kind sigma c with | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars) | _ -> false @@ -948,7 +944,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e expand curenvnb pb opt substn cM f1 l1 cN f2 l2 and reduce curenvnb pb opt (sigma, metas, evars as substn) cM cN = - if use_full_betaiota flags && not (subterm_restriction opt flags) then + if flags.modulo_betaiota && not (subterm_restriction opt flags) then let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in if not (EConstr.eq_constr sigma cM cM') then unirec_rec curenvnb pb opt substn cM' cN -- cgit v1.2.3 From 376da97be60957b25e59afb5791fae665127b17b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:48:14 +0100 Subject: Remove options deprecated since 8.4. --- pretyping/unification.ml | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ef4f7f7545..b4964c1f36 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -248,20 +248,9 @@ let sort_eqns = unify_r2l let global_pattern_unification_flag = ref true -(* Compatibility option introduced and activated in Coq 8.3 whose - syntax is now deprecated. *) - open Goptions -let _ = - declare_bool_option - { optdepr = true; - optname = "pattern-unification for existential variables in tactics"; - optkey = ["Tactic";"Evars";"Pattern";"Unification"]; - optread = (fun () -> !global_pattern_unification_flag); - optwrite = (:=) global_pattern_unification_flag } -(* Compatibility option superseding the previous one, introduced and - activated in Coq 8.4 *) +(* Compatibility option introduced and activated in Coq 8.4 *) let _ = declare_bool_option -- cgit v1.2.3 From 5e93f1e95853c3614df813845b94051a45f1a749 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:51:32 +0100 Subject: Deprecate options that were introduced for compatibility with 8.2. --- pretyping/classops.ml | 2 +- pretyping/unification.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 627a9c9cc7..8d87f6e99c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -428,7 +428,7 @@ let automatically_import_coercions = ref false open Goptions let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "automatic import of coercions"; optkey = ["Automatic";"Coercions";"Import"]; optread = (fun () -> !automatically_import_coercions); diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b4964c1f36..67c8b07e78 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -254,7 +254,7 @@ open Goptions let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "pattern-unification for existential variables in tactics"; optkey = ["Tactic";"Pattern";"Unification"]; optread = (fun () -> !global_pattern_unification_flag); -- cgit v1.2.3 From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 1 Apr 2017 17:35:39 +0200 Subject: Using UInfoInd for universes in inductive types It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. --- pretyping/typeclasses.ml | 2 +- pretyping/vnorm.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d7b4842810..152ccb0798 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -123,7 +123,7 @@ let typeclass_univ_instance (cl,u') = else Univ.Instance.empty | IndRef c -> let mib,oib = Global.lookup_inductive c in - if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes + if mib.mind_polymorphic then Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty | _ -> Univ.Instance.empty in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b08666483e..074b7373c7 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -174,7 +174,7 @@ and nf_whd env sigma whd typ = | Vatom_stk(Aind ((mi,i) as ind), stk) -> let mib = Environ.lookup_mind mi env in let nb_univs = - if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes + if mib.mind_polymorphic then Univ.UContext.size (Univ.UInfoInd.univ_context mib.mind_universes) else 0 in let mk u = -- cgit v1.2.3 From bef2e53ae2286d0a7c61697f7a7a71bfdc0a3c99 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 5 Apr 2017 14:49:13 +0200 Subject: Subtyping inference for inductoves and records Also reinferred after sections discharge --- pretyping/inductiveops.ml | 65 ++++++++++++++++++++++++++++++++++++++++++++++ pretyping/inductiveops.mli | 5 ++++ 2 files changed, 70 insertions(+) (limited to 'pretyping') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d8252ea9bb..1f8600dc2c 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -655,3 +655,68 @@ let control_only_guard env c = iter_constr_with_full_binders push_rel iter env c in iter env c + +(* inference of subtyping condition for inductive types *) + +let infer_inductive_subtyping_arity_constructor + (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity = + let update_contexts (env, evd, csts) csts' = + (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts') + in + let basic_check (env, evd, csts) tp = + let csts' = + Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp) + in update_contexts (env, evd, csts) csts' + in + let infer_typ typ ctxs = + match typ with + | LocalAssum (_, typ') -> + begin + try + let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts) + with Reduction.NotConvertible -> + anomaly ~label:"inference of record/inductive subtyping relation failed" + (Pp.str "Can't infer subtyping for record/inductive type") + end + | _ -> anomaly (Pp.str "") + in + let typs, codom = Reduction.dest_prod env arcn in + let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in + if not is_arity then basic_check last_contexts codom else last_contexts + +let infer_inductive_subtyping env evd mind_ent = + let { Entries.mind_entry_inds = entries; + Entries.mind_entry_polymorphic = poly; + Entries.mind_entry_universes = ground_uinfind; + } = mind_ent + in + let uinfind = + if poly then + begin + let uctx = Univ.UInfoInd.univ_context ground_uinfind in + let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in + let dosubst = subst_univs_level_constr sbsubst in + let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in + let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in + let uctx_other = Univ.UContext.make (instance_other, constraints_other) in + let env' = Environ.push_context uctx env in + let env' = Environ.push_context uctx_other env' in + let evd' = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in + let (_, _, subtyp_constraints) = + List.fold_left + (fun ctxs indentry -> + let ctxs' = infer_inductive_subtyping_arity_constructor + ctxs dosubst indentry.Entries.mind_entry_arity true + in + List.fold_left + (fun ctxs cons -> + infer_inductive_subtyping_arity_constructor ctxs dosubst cons false) + ctxs' indentry.Entries.mind_entry_lc + ) (env', evd', Univ.Constraint.empty) entries + in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind, + Univ.UContext.make + (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind), + subtyp_constraints)) + end + else ground_uinfind + in {mind_ent with Entries.mind_entry_universes = uinfind;} diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index bdb6f996b9..7d89b1b2bd 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -199,3 +199,8 @@ val type_of_inductive_knowing_conclusion : (********************) val control_only_guard : env -> types -> unit + +(* inference of subtyping condition for inductive types *) + +val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry -- cgit v1.2.3 From ab86b9b3999f3860bdb69824f585b9cf461ff295 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Fri, 7 Apr 2017 12:44:12 +0200 Subject: Use inductive subtyping for conv/cumul --- pretyping/reductionops.ml | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c2a6483012..971ad78e67 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1361,9 +1361,24 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible +let sigma_leq_inductives ~flex uinfind i0 i1 sigma = + let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in + let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + if not ((Univ.Instance.length ind_instance = Univ.Instance.length i0) && + (Univ.Instance.length ind_instance = Univ.Instance.length i1)) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + let comp_subst = (Univ.Instance.append i0 i1) in + let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in + try Evd.add_constraints sigma comp_cst + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible + let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances } + Reduction.compare_instances = sigma_compare_instances; + Reduction.leq_inductives = sigma_leq_inductives } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = -- cgit v1.2.3 From 4385872b2d82fbad2be84f2423802e00e9d9575f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 8 Apr 2017 22:01:30 +0200 Subject: Make unification use subtyping info of inductives --- pretyping/evarconv.ml | 74 ++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 64 insertions(+), 10 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3757ba7e6d..882ea61a9d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -350,6 +350,21 @@ let exact_ise_stack2 env evd f sk1 sk2 = ise_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) +let check_leq_inductives evd uinfind u u' = + let u = EConstr.EInstance.kind evd u in + let u' = EConstr.EInstance.kind evd u' in + let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in + let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && + (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + begin + let comp_subst = (Univ.Instance.append u u') in + let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in + Evd.add_constraints evd comp_cst + end + let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in @@ -439,16 +454,55 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else evar_eqappr_x ts env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = - let univs = EConstr.eq_constr_universes evd term term' in - match univs with - | Some univs -> - ise_and evd [(fun i -> - let cstrs = Universes.to_constraints (Evd.universes i) univs in - try Success (Evd.add_constraints i cstrs) - with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] - | None -> - UnifFailure (evd,NotSameHead) + let fall_back () = + let univs = EConstr.eq_constr_universes evd term term' in + match univs with + | Some univs -> + begin + let cstrs = Universes.to_constraints (Evd.universes evd) univs in + try Success (Evd.add_constraints evd cstrs) + with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) + end + | None -> + UnifFailure (evd, NotSameHead) + in + let compare_heads evd = + match EConstr.kind evd term, EConstr.kind evd term' with + | Const (c, u), Const (c', u') -> + fall_back () + | Ind (ind, u), Ind (ind', u') -> + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + if Names.eq_ind ind ind' then + begin + let mind = Environ.lookup_mind (fst ind) env in + if mind.Declarations.mind_polymorphic then + begin + let num_param_arity = + Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) + in + if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then + fall_back () + else + begin + let uinfind = mind.Declarations.mind_universes in + let evd' = check_leq_inductives evd uinfind u u' in + Success (check_leq_inductives evd' uinfind u' u) + end + end + else + fall_back () + end + else UnifFailure (evd, NotSameHead) + | Construct (cons, u), Construct (cons', u') -> + fall_back () + | _, _ -> anomaly (Pp.str "") + in + 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')] +(* >>>>>>> Make unification use subtyping info of inductives *) 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 -- cgit v1.2.3 From 40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sun, 21 May 2017 14:46:30 +0200 Subject: Squashed commit of the following: Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints. --- pretyping/evarconv.ml | 94 +++++++++++++++++++++++++++++++++-------------- pretyping/reductionops.ml | 4 +- 2 files changed, 69 insertions(+), 29 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 882ea61a9d..eb8a0c85a0 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -454,48 +454,88 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else evar_eqappr_x ts env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = - let fall_back () = + let check_strict () = let univs = EConstr.eq_constr_universes evd term term' in + match univs with + | Some univs -> + begin + let cstrs = Universes.to_constraints (Evd.universes evd) univs in + try Success (Evd.add_constraints evd cstrs) + with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) + end + | None -> + UnifFailure (evd, NotSameHead) + in + let first_try_strict_check cond u u' try_subtyping_constraints = + if cond then + let univs = EConstr.eq_constr_universes evd term term' in match univs with | Some univs -> begin let cstrs = Universes.to_constraints (Evd.universes evd) univs in try Success (Evd.add_constraints evd cstrs) - with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) + with Univ.UniverseInconsistency p -> try_subtyping_constraints () end | None -> UnifFailure (evd, NotSameHead) + else + UnifFailure (evd, NotSameHead) in let compare_heads evd = match EConstr.kind evd term, EConstr.kind evd term' with | Const (c, u), Const (c', u') -> - fall_back () + check_strict () | Ind (ind, u), Ind (ind', u') -> - let nparamsaplied = Stack.args_size sk in - let nparamsaplied' = Stack.args_size sk' in - if Names.eq_ind ind ind' then - begin - let mind = Environ.lookup_mind (fst ind) env in - if mind.Declarations.mind_polymorphic then - begin - let num_param_arity = - Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) - in - if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then - fall_back () - else - begin - let uinfind = mind.Declarations.mind_universes in - let evd' = check_leq_inductives evd uinfind u u' in - Success (check_leq_inductives evd' uinfind u' u) - end - end - else - fall_back () - end - else UnifFailure (evd, NotSameHead) + let check_subtyping_constraints () = + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + begin + let mind = Environ.lookup_mind (fst ind) env in + if mind.Declarations.mind_polymorphic then + begin + let num_param_arity = + Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) + in + if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then + UnifFailure (evd, NotSameHead) + else + begin + let uinfind = mind.Declarations.mind_universes in + let evd' = check_leq_inductives evd uinfind u u' in + Success (check_leq_inductives evd' uinfind u' u) + end + end + else + UnifFailure (evd, NotSameHead) + end + in + first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints | Construct (cons, u), Construct (cons', u') -> - fall_back () + let check_subtyping_constraints () = + let ind, ind' = fst cons, fst cons' in + let j, j' = snd cons, snd cons' in + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + let mind = Environ.lookup_mind (fst ind) env in + if mind.Declarations.mind_polymorphic then + begin + let num_cnstr_args = + let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in + nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1) + in + if not (num_cnstr_args = nparamsaplied && num_cnstr_args = nparamsaplied') then + UnifFailure (evd, NotSameHead) + else + begin + let uinfind = mind.Declarations.mind_universes in + let evd' = check_leq_inductives evd uinfind u u' in + Success (check_leq_inductives evd' uinfind u' u) + end + end + else + UnifFailure (evd, NotSameHead) + in + first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints | _, _ -> anomaly (Pp.str "") in ise_and evd [(fun i -> diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 971ad78e67..e374f7b3bb 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1313,8 +1313,8 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV -let report_anomaly _ = - let e = UserError (None, Pp.str "Conversion test raised an anomaly") in +let report_anomaly e = + let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in let e = CErrors.push e in iraise e -- cgit v1.2.3 From 7b5fcef8a0fb3b97a3980f10596137234061990f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 26 Apr 2017 15:24:35 +0200 Subject: Fix bugs --- pretyping/evarconv.ml | 6 ++++-- pretyping/inductiveops.ml | 41 ++++++++++++++++++++++++++--------------- pretyping/inductiveops.mli | 4 ++++ 3 files changed, 34 insertions(+), 17 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index eb8a0c85a0..ea22c3708f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -494,7 +494,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if mind.Declarations.mind_polymorphic then begin let num_param_arity = - Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs in if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then UnifFailure (evd, NotSameHead) @@ -520,7 +520,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if mind.Declarations.mind_polymorphic then begin let num_cnstr_args = - let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in + let nparamsctxt = + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs + in nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1) in if not (num_cnstr_args = nparamsaplied && num_cnstr_args = nparamsaplied') then diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1f8600dc2c..ebfb1f8a7c 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -659,14 +659,22 @@ let control_only_guard env c = (* inference of subtyping condition for inductive types *) let infer_inductive_subtyping_arity_constructor - (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity = + (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) = + let numchecked = ref 0 in + let numparams = Context.Rel.nhyps params in let update_contexts (env, evd, csts) csts' = (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts') in let basic_check (env, evd, csts) tp = - let csts' = - Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp) - in update_contexts (env, evd, csts) csts' + let result = + if !numchecked >= numparams then + let csts' = + Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp) + in update_contexts (env, evd, csts) csts' + else + (env, evd, csts) + in + numchecked := !numchecked + 1; result in let infer_typ typ ctxs = match typ with @@ -680,12 +688,14 @@ let infer_inductive_subtyping_arity_constructor end | _ -> anomaly (Pp.str "") in - let typs, codom = Reduction.dest_prod env arcn in + let arcn' = Term.it_mkProd_or_LetIn arcn params in + let typs, codom = Reduction.dest_prod env arcn' in let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in if not is_arity then basic_check last_contexts codom else last_contexts let infer_inductive_subtyping env evd mind_ent = - let { Entries.mind_entry_inds = entries; + let { Entries.mind_entry_params = params; + Entries.mind_entry_inds = entries; Entries.mind_entry_polymorphic = poly; Entries.mind_entry_universes = ground_uinfind; } = mind_ent @@ -704,15 +714,16 @@ let infer_inductive_subtyping env evd mind_ent = let evd' = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in let (_, _, subtyp_constraints) = List.fold_left - (fun ctxs indentry -> - let ctxs' = infer_inductive_subtyping_arity_constructor - ctxs dosubst indentry.Entries.mind_entry_arity true - in - List.fold_left - (fun ctxs cons -> - infer_inductive_subtyping_arity_constructor ctxs dosubst cons false) - ctxs' indentry.Entries.mind_entry_lc - ) (env', evd', Univ.Constraint.empty) entries + (fun ctxs indentry -> + let _, params = Typeops.infer_local_decls env params in + let ctxs' = infer_inductive_subtyping_arity_constructor + ctxs dosubst indentry.Entries.mind_entry_arity true params + in + List.fold_left + (fun ctxs cons -> + infer_inductive_subtyping_arity_constructor ctxs dosubst cons false params) + ctxs' indentry.Entries.mind_entry_lc + ) (env', evd', Univ.Constraint.empty) entries in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind, Univ.UContext.make (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind), diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7d89b1b2bd..811f47f39a 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -201,6 +201,10 @@ val type_of_inductive_knowing_conclusion : val control_only_guard : env -> types -> unit (* inference of subtyping condition for inductive types *) +(* for debugging purposes only to be removed *) +val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t -> +(Term.constr -> Term.constr) -> +Term.types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> Entries.mutual_inductive_entry -- cgit v1.2.3 From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- pretyping/evarconv.ml | 2 ++ pretyping/reductionops.ml | 64 +++++++++++++++++++++++++++++++++++++++-------- 2 files changed, 56 insertions(+), 10 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ea22c3708f..be2fd81290 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -494,6 +494,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if mind.Declarations.mind_polymorphic then begin let num_param_arity = + (* Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) *) mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs in if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then @@ -521,6 +522,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty begin let num_cnstr_args = let nparamsctxt = + (* Context.Rel.length mind.Declarations.mind_params_ctxt *) mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs in nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e374f7b3bb..2040acba79 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1361,24 +1361,68 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible -let sigma_leq_inductives ~flex uinfind i0 i1 sigma = +let sigma_check_inductive_instances cv_pb uinfind u u' sigma = let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in - if not ((Univ.Instance.length ind_instance = Univ.Instance.length i0) && - (Univ.Instance.length ind_instance = Univ.Instance.length i1)) then + if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && + (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else - let comp_subst = (Univ.Instance.append i0 i1) in - let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in - try Evd.add_constraints sigma comp_cst - with Evd.UniversesDiffer - | Univ.UniverseInconsistency _ -> - raise Reduction.NotConvertible + let comp_cst = + let comp_subst = (Univ.Instance.append u u') in + Univ.subst_instance_constraints comp_subst ind_sbcst + in + let comp_cst = + match cv_pb with + Reduction.CONV -> + let comp_subst = (Univ.Instance.append u' u) in + let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in + Univ.Constraint.union comp_cst comp_cst' + | Reduction.CUMUL -> comp_cst + in + try Evd.add_constraints sigma comp_cst + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible + +let sigma_conv_inductives + cv_pb (mind, ind) u1 sv1 u2 sv2 sigma = + try sigma_compare_instances ~flex:false u1 u2 sigma with + Reduction.NotConvertible -> + if mind.Declarations.mind_polymorphic then + let num_param_arity = + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + in + if not (num_param_arity = sv1 && num_param_arity = sv2) then + raise Reduction.NotConvertible + else + let uinfind = mind.Declarations.mind_universes in + sigma_check_inductive_instances cv_pb uinfind u1 u2 sigma + else raise Reduction.NotConvertible + +let sigma_conv_constructors + (mind, ind, cns) u1 sv1 u2 sv2 sigma = + try sigma_compare_instances ~flex:false u1 u2 sigma with + Reduction.NotConvertible -> + if mind.Declarations.mind_polymorphic then + let num_cnstr_args = + let nparamsctxt = + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in + nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) + in + if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then + raise Reduction.NotConvertible + else + let uinfind = mind.Declarations.mind_universes in + sigma_check_inductive_instances Reduction.CONV uinfind u1 u2 sigma + else raise Reduction.NotConvertible let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; Reduction.compare_instances = sigma_compare_instances; - Reduction.leq_inductives = sigma_leq_inductives } + Reduction.conv_inductives = sigma_conv_inductives; + Reduction.conv_constructors = sigma_conv_constructors} let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = -- cgit v1.2.3 From fece24ec8aa88950477ccfed70b511f05b438718 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Fri, 28 Apr 2017 12:49:38 +0200 Subject: Fix a bug Incorrect environment was used when checking subtyping information of inductive types. --- pretyping/inductiveops.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'pretyping') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ebfb1f8a7c..1ef4a9f5e7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -697,11 +697,12 @@ let infer_inductive_subtyping env evd mind_ent = let { Entries.mind_entry_params = params; Entries.mind_entry_inds = entries; Entries.mind_entry_polymorphic = poly; + Entries.mind_entry_cumulative = cum; Entries.mind_entry_universes = ground_uinfind; } = mind_ent in let uinfind = - if poly then + if poly && cum then begin let uctx = Univ.UInfoInd.univ_context ground_uinfind in let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in @@ -709,9 +710,9 @@ let infer_inductive_subtyping env evd mind_ent = let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env' = Environ.push_context uctx env in - let env' = Environ.push_context uctx_other env' in - let evd' = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in + let env = Environ.push_context uctx env in + let env = Environ.push_context uctx_other env in + let evd = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in let (_, _, subtyp_constraints) = List.fold_left (fun ctxs indentry -> @@ -723,7 +724,7 @@ let infer_inductive_subtyping env evd mind_ent = (fun ctxs cons -> infer_inductive_subtyping_arity_constructor ctxs dosubst cons false params) ctxs' indentry.Entries.mind_entry_lc - ) (env', evd', Univ.Constraint.empty) entries + ) (env, evd, Univ.Constraint.empty) entries in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind, Univ.UContext.make (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind), -- cgit v1.2.3 From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- pretyping/arguments_renaming.ml | 2 +- pretyping/evarconv.ml | 55 ++++++++++++++++------------- pretyping/inductiveops.ml | 77 ++++++++++++++++++++++++----------------- pretyping/recordops.ml | 5 ++- pretyping/reductionops.ml | 45 +++++++++++++++--------- pretyping/typeclasses.ml | 8 ++--- pretyping/vnorm.ml | 6 ++-- 7 files changed, 112 insertions(+), 86 deletions(-) (limited to 'pretyping') diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 1bd03491a7..c7b37aba5c 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -43,7 +43,7 @@ let section_segment_of_reference = function | ConstRef con -> Lib.section_segment_of_constant con | IndRef (kn,_) | ConstructRef ((kn,_),_) -> Lib.section_segment_of_mutual_inductive kn - | _ -> [], Univ.LMap.empty, Univ.UContext.empty + | _ -> [], Univ.LMap.empty, Univ.AUContext.empty let discharge_rename_args = function | _, (ReqGlobal (c, names), _ as req) -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index be2fd81290..b15dde5d79 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -350,18 +350,22 @@ let exact_ise_stack2 env evd f sk1 sk2 = ise_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) -let check_leq_inductives evd uinfind u u' = +let check_leq_inductives evd cumi u u' = let u = EConstr.EInstance.kind evd u in let u' = EConstr.EInstance.kind evd u' in - let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in - let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + let ind_instance = + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + in + let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else begin let comp_subst = (Univ.Instance.append u u') in - let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in + let comp_cst = + Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst) + in Evd.add_constraints evd comp_cst end @@ -491,23 +495,24 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let nparamsaplied' = Stack.args_size sk' in begin let mind = Environ.lookup_mind (fst ind) env in - if mind.Declarations.mind_polymorphic then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + UnifFailure (evd, NotSameHead) + | Declarations.Cumulative_ind cumi -> begin let num_param_arity = - (* Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) *) - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs in - if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then + if not (num_param_arity = nparamsaplied + && num_param_arity = nparamsaplied') then UnifFailure (evd, NotSameHead) else begin - let uinfind = mind.Declarations.mind_universes in - let evd' = check_leq_inductives evd uinfind u u' in - Success (check_leq_inductives evd' uinfind u' u) + let evd' = check_leq_inductives evd cumi u u' in + Success (check_leq_inductives evd' cumi u' u) end end - else - UnifFailure (evd, NotSameHead) end in first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints @@ -518,26 +523,29 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let nparamsaplied = Stack.args_size sk in let nparamsaplied' = Stack.args_size sk' in let mind = Environ.lookup_mind (fst ind) env in - if mind.Declarations.mind_polymorphic then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + UnifFailure (evd, NotSameHead) + | Declarations.Cumulative_ind cumi -> begin let num_cnstr_args = let nparamsctxt = - (* Context.Rel.length mind.Declarations.mind_params_ctxt *) - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs in - nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1) + nparamsctxt + + mind.Declarations.mind_packets.(snd ind). + Declarations.mind_consnrealargs.(j - 1) in - if not (num_cnstr_args = nparamsaplied && num_cnstr_args = nparamsaplied') then + if not (num_cnstr_args = nparamsaplied + && num_cnstr_args = nparamsaplied') then UnifFailure (evd, NotSameHead) else begin - let uinfind = mind.Declarations.mind_universes in - let evd' = check_leq_inductives evd uinfind u u' in - Success (check_leq_inductives evd' uinfind u' u) + let evd' = check_leq_inductives evd cumi u u' in + Success (check_leq_inductives evd' cumi u' u) end end - else - UnifFailure (evd, NotSameHead) in first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints | _, _ -> anomaly (Pp.str "") @@ -546,7 +554,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty 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')] -(* >>>>>>> Make unification use subtyping info of inductives *) 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 diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1ef4a9f5e7..2ae7c0f809 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -696,39 +696,52 @@ let infer_inductive_subtyping_arity_constructor let infer_inductive_subtyping env evd mind_ent = let { Entries.mind_entry_params = params; Entries.mind_entry_inds = entries; - Entries.mind_entry_polymorphic = poly; - Entries.mind_entry_cumulative = cum; - Entries.mind_entry_universes = ground_uinfind; + Entries.mind_entry_universes = ground_univs; } = mind_ent in let uinfind = - if poly && cum then - begin - let uctx = Univ.UInfoInd.univ_context ground_uinfind in - let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in - let dosubst = subst_univs_level_constr sbsubst in - let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in - let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx env in - let env = Environ.push_context uctx_other env in - let evd = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in - let (_, _, subtyp_constraints) = - List.fold_left - (fun ctxs indentry -> - let _, params = Typeops.infer_local_decls env params in - let ctxs' = infer_inductive_subtyping_arity_constructor - ctxs dosubst indentry.Entries.mind_entry_arity true params - in - List.fold_left - (fun ctxs cons -> - infer_inductive_subtyping_arity_constructor ctxs dosubst cons false params) - ctxs' indentry.Entries.mind_entry_lc - ) (env, evd, Univ.Constraint.empty) entries - in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind, - Univ.UContext.make - (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind), - subtyp_constraints)) - end - else ground_uinfind + match ground_univs with + | Entries.Monomorphic_ind_entry _ + | Entries.Polymorphic_ind_entry _ -> ground_univs + | Entries.Cumulative_ind_entry cumi -> + begin + let uctx = Univ.CumulativityInfo.univ_context cumi in + let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in + let dosubst = subst_univs_level_constr sbsubst in + let instance_other = + Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) + in + let constraints_other = + Univ.subst_univs_level_constraints + sbsubst (Univ.UContext.constraints uctx) + in + let uctx_other = Univ.UContext.make (instance_other, constraints_other) in + let env = Environ.push_context uctx env in + let env = Environ.push_context uctx_other env in + let evd = + Evd.merge_universe_context + evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) + in + let (_, _, subtyp_constraints) = + List.fold_left + (fun ctxs indentry -> + let _, params = Typeops.infer_local_decls env params in + let ctxs' = infer_inductive_subtyping_arity_constructor + ctxs dosubst indentry.Entries.mind_entry_arity true params + in + List.fold_left + (fun ctxs cons -> + infer_inductive_subtyping_arity_constructor + ctxs dosubst cons false params + ) + ctxs' indentry.Entries.mind_entry_lc + ) (env, evd, Univ.Constraint.empty) entries + in + Entries.Cumulative_ind_entry + (Univ.CumulativityInfo.make + (Univ.CumulativityInfo.univ_context cumi, + Univ.UContext.make + (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi), + subtyp_constraints))) + end in {mind_ent with Entries.mind_entry_universes = uinfind;} diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index bc9e3a1f46..283a1dcd18 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -197,7 +197,7 @@ let warn_projection_no_head_constant = (* Intended to always succeed *) let compute_canonical_projections warn (con,ind) = let env = Global.env () in - let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in + let ctx = Environ.constant_context env con in let u = Univ.UContext.instance ctx in let v = (mkConstU (con,u)) in let ctx = Univ.ContextSet.of_context ctx in @@ -298,8 +298,7 @@ let error_not_structure ref = let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in let env = Global.env () in - let ctx = Environ.constant_context env sp in - let u = Univ.UContext.instance ctx in + let u = Environ.constant_instance env sp in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2040acba79..123c610166 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1362,21 +1362,25 @@ let sigma_compare_instances ~flex i0 i1 sigma = raise Reduction.NotConvertible let sigma_check_inductive_instances cv_pb uinfind u u' sigma = - let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in - let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + let ind_instance = + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind) + in + let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.subst_instance_constraints comp_subst ind_sbcst + Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbctx) in let comp_cst = match cv_pb with Reduction.CONV -> let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in + let comp_cst' = + Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx) + in Univ.Constraint.union comp_cst comp_cst' | Reduction.CUMUL -> comp_cst in @@ -1389,34 +1393,43 @@ let sigma_conv_inductives cv_pb (mind, ind) u1 sv1 u2 sv2 sigma = try sigma_compare_instances ~flex:false u1 u2 sigma with Reduction.NotConvertible -> - if mind.Declarations.mind_polymorphic then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Polymorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Cumulative_ind cumi -> let num_param_arity = - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs in if not (num_param_arity = sv1 && num_param_arity = sv2) then raise Reduction.NotConvertible else - let uinfind = mind.Declarations.mind_universes in - sigma_check_inductive_instances cv_pb uinfind u1 u2 sigma - else raise Reduction.NotConvertible + sigma_check_inductive_instances cv_pb cumi u1 u2 sigma let sigma_conv_constructors (mind, ind, cns) u1 sv1 u2 sv2 sigma = try sigma_compare_instances ~flex:false u1 u2 sigma with Reduction.NotConvertible -> - if mind.Declarations.mind_polymorphic then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Polymorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Cumulative_ind cumi -> let num_cnstr_args = let nparamsctxt = - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in - nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + in + nparamsctxt + + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) in if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then raise Reduction.NotConvertible else - let uinfind = mind.Declarations.mind_universes in - sigma_check_inductive_instances Reduction.CONV uinfind u1 u2 sigma - else raise Reduction.NotConvertible + sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 152ccb0798..f883e647b5 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -111,20 +111,16 @@ let new_instance cl info glob poly impl = let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes" let instances : instances ref = Summary.ref Refmap.empty ~name:"instances" -open Declarations - let typeclass_univ_instance (cl,u') = let subst = let u = match cl.cl_impl with | ConstRef c -> let cb = Global.lookup_constant c in - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes - else Univ.Instance.empty + Declareops.constant_polymorphic_instance cb | IndRef c -> let mib,oib = Global.lookup_inductive c in - if mib.mind_polymorphic then Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) - else Univ.Instance.empty + Declareops.inductive_polymorphic_instance mib | _ -> Univ.Instance.empty in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 074b7373c7..9e151fea25 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -174,8 +174,7 @@ and nf_whd env sigma whd typ = | Vatom_stk(Aind ((mi,i) as ind), stk) -> let mib = Environ.lookup_mind mi env in let nb_univs = - if mib.mind_polymorphic then Univ.UContext.size (Univ.UInfoInd.univ_context mib.mind_universes) - else 0 + Univ.Instance.length (Declareops.inductive_polymorphic_instance mib) in let mk u = let pind = (ind, u) in (mkIndU pind, type_of_ind env pind) @@ -204,8 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk = | ConstKey cst -> let cbody = Environ.lookup_constant cst env in let nb_univs = - if cbody.const_polymorphic then Univ.UContext.size cbody.const_universes - else 0 + Univ.Instance.length (Declareops.constant_polymorphic_instance cbody) in let mk u = let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst) -- cgit v1.2.3 From 15b1856edd593b39d63d23584a4f5acec0eeb592 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 15 Jun 2017 16:50:05 +0200 Subject: Fix a bug in cumulativity --- pretyping/evarconv.ml | 9 +++++---- pretyping/reductionops.mli | 1 - 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b15dde5d79..d84363089d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -353,12 +353,13 @@ let exact_ise_stack2 env evd f sk1 sk2 = let check_leq_inductives evd cumi u u' = let u = EConstr.EInstance.kind evd u in let u' = EConstr.EInstance.kind evd u' in - let ind_instance = - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + let length_ind_instance = + Univ.Instance.length + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) in let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && - (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + if not ((length_ind_instance = Univ.Instance.length u) && + (length_ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else begin diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index af4ea3ac53..a4da19de75 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -66,7 +66,6 @@ module Cst_stack : sig val pr : t -> Pp.std_ppcmds end - module Stack : sig type 'a app_node -- cgit v1.2.3