From 44f462aa380de847452c0809d15c86649d5d6a7a Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 28 Mar 2017 19:24:02 +0200 Subject: Extend definition of inductives to include subtyping info --- vernac/command.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index 998e7803e1..5f95a42a37 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -656,7 +656,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; - mind_entry_universes = uctx; + mind_entry_universes = (uctx, Univ.UContext.empty); }, pl, impls -- 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. --- vernac/command.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index 5f95a42a37..b76c2247b3 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -656,7 +656,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; - mind_entry_universes = (uctx, Univ.UContext.empty); + mind_entry_universes = Universes.univ_inf_ind_from_universe_context uctx; }, pl, impls -- cgit v1.2.3 From d83a4a93202c91095c5528fe4b54c83737e5a151 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 4 Apr 2017 19:44:31 +0200 Subject: Add subtyping inference for inductive types --- vernac/command.ml | 54 +++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 53 insertions(+), 1 deletion(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index b76c2247b3..b23eb9e6bf 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -573,6 +573,32 @@ let check_param = function | CLocalAssum (nas, Generalized _, _) -> () | CLocalPattern _ -> assert false +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 interp_mutual_inductive (paramsl,indl) notations poly prv finite = check_all_names_different indl; List.iter check_param paramsl; @@ -649,6 +675,32 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in + let ground_uinfind = Universes.univ_inf_ind_from_universe_context uctx in + let uinfind = + 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_ar_params 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.mind_entry_arity true + in + List.fold_left + (fun ctxs cons -> + infer_inductive_subtyping_arity_constructor ctxs dosubst cons false) + ctxs' indentry.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)) + in (* Build the mutual inductive entry *) { mind_entry_params = List.map prepare_param ctx_params; mind_entry_record = None; @@ -656,7 +708,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; - mind_entry_universes = Universes.univ_inf_ind_from_universe_context uctx; + mind_entry_universes = uinfind; }, pl, impls -- 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 --- vernac/command.ml | 70 ++++++++----------------------------------------------- 1 file changed, 10 insertions(+), 60 deletions(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index b23eb9e6bf..35b75370e4 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -573,32 +573,6 @@ let check_param = function | CLocalAssum (nas, Generalized _, _) -> () | CLocalPattern _ -> assert false -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 interp_mutual_inductive (paramsl,indl) notations poly prv finite = check_all_names_different indl; List.iter check_param paramsl; @@ -676,41 +650,17 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in let ground_uinfind = Universes.univ_inf_ind_from_universe_context uctx in - let uinfind = - 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_ar_params 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.mind_entry_arity true - in - List.fold_left - (fun ctxs cons -> - infer_inductive_subtyping_arity_constructor ctxs dosubst cons false) - ctxs' indentry.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)) - in (* Build the mutual inductive entry *) - { mind_entry_params = List.map prepare_param ctx_params; - mind_entry_record = None; - mind_entry_finite = finite; - mind_entry_inds = entries; - mind_entry_polymorphic = poly; - mind_entry_private = if prv then Some false else None; - mind_entry_universes = uinfind; - }, - pl, impls + let mind_ent = + { mind_entry_params = List.map prepare_param ctx_params; + mind_entry_record = None; + mind_entry_finite = finite; + mind_entry_inds = entries; + mind_entry_polymorphic = poly; + mind_entry_private = if prv then Some false else None; + mind_entry_universes = ground_uinfind; + } + in (Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent), pl, impls (* Very syntactical equality *) let eq_local_binders bl1 bl2 = -- cgit v1.2.3 From c07215582ab75faeea864827b153eed80a28527a Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 6 Apr 2017 19:03:24 +0200 Subject: Change the place of inference after sect discharge --- vernac/command.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index 35b75370e4..2d4f051345 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -660,7 +660,10 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_private = if prv then Some false else None; mind_entry_universes = ground_uinfind; } - in (Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent), pl, impls + in + (if poly then + Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent + else mind_ent), pl, impls (* Very syntactical equality *) let eq_local_binders bl1 bl2 = -- 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. --- vernac/command.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index 2d4f051345..116a7aee16 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -106,7 +106,7 @@ let interp_definition pl bl p red_option c ctypopt = let c = EConstr.Unsafe.to_constr c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in - let vars = Universes.universes_of_constr body in + let vars = Univops.universes_of_constr body in let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in imps1@(Impargs.lift_implicits nb_args imps2), pl, @@ -131,8 +131,8 @@ let interp_definition pl bl p red_option c ctypopt = in if not (try List.for_all chk imps2 with Not_found -> false) then warn_implicits_in_term (); - let vars = Univ.LSet.union (Universes.universes_of_constr body) - (Universes.universes_of_constr typ) in + let vars = Univ.LSet.union (Univops.universes_of_constr body) + (Univops.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl ctx in imps1@(Impargs.lift_implicits nb_args impsty), pl, @@ -329,7 +329,7 @@ let do_assumptions_bound_univs coe kind nl id pl c = let nf, subst = Evarutil.e_nf_evars_and_universes evdref in let ty = EConstr.Unsafe.to_constr ty in let ty = nf ty in - let vars = Universes.universes_of_constr ty in + let vars = Univops.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in let uctx = Univ.ContextSet.of_context uctx in @@ -1213,7 +1213,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let env = Global.env() in let indexes = search_guard env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in + let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in @@ -1245,7 +1245,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Universes.universes_of_constr (List.hd fixdecls) in + let vars = Univops.universes_of_constr (List.hd fixdecls) in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in -- 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 --- vernac/command.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index 116a7aee16..6c59976232 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -662,7 +662,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = } in (if poly then - Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent + Inductiveops.infer_inductive_subtyping env_ar evd mind_ent else mind_ent), pl, impls (* Very syntactical equality *) -- 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 --- vernac/command.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index 6c59976232..2345cb4c51 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -573,7 +573,7 @@ let check_param = function | CLocalAssum (nas, Generalized _, _) -> () | CLocalPattern _ -> assert false -let interp_mutual_inductive (paramsl,indl) notations poly prv finite = +let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = check_all_names_different indl; List.iter check_param paramsl; let env0 = Global.env() in @@ -657,6 +657,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_finite = finite; mind_entry_inds = entries; mind_entry_polymorphic = poly; + mind_entry_cumulative = cum; mind_entry_private = if prv then Some false else None; mind_entry_universes = ground_uinfind; } @@ -747,10 +748,10 @@ type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) -let do_mutual_inductive indl poly prv finite = +let do_mutual_inductive indl cum poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in + let mie,pl,impls = interp_mutual_inductive indl ntns cum poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) -- 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 --- vernac/command.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'vernac/command.ml') diff --git a/vernac/command.ml b/vernac/command.ml index 2345cb4c51..4064773561 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -649,20 +649,25 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in - let ground_uinfind = Universes.univ_inf_ind_from_universe_context uctx in + let univs = + if poly then + if cum then + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) + else Polymorphic_ind_entry uctx + else + Monomorphic_ind_entry uctx + in (* Build the mutual inductive entry *) - let mind_ent = + let mind_ent = { mind_entry_params = List.map prepare_param ctx_params; mind_entry_record = None; mind_entry_finite = finite; mind_entry_inds = entries; - mind_entry_polymorphic = poly; - mind_entry_cumulative = cum; mind_entry_private = if prv then Some false else None; - mind_entry_universes = ground_uinfind; + mind_entry_universes = univs; } in - (if poly then + (if poly && cum then Inductiveops.infer_inductive_subtyping env_ar evd mind_ent else mind_ent), pl, impls -- cgit v1.2.3