Skip to content
Browse files

First part of the big changes to the kernel:

- Const, Ind, Construct now come with a universe level instance
- It is used for type inference in the kernel, which now also takes
a graph as input: actually a set of local universe variables and their
constraints. Type inference just checks that the constraints are enough
to satisfy its own rules.
- Remove polymorphic_arity and _knowing_parameters everywhere: we
don't need full applications for polymorphism to apply anymore, as
we generate fresh variables at each constant/inductive/constructor
application. However knowing_parameters variants might be reinstated
later for optimization.
- New structures exported in univ.mli:
  - universe_list for universe level instances
  - universe_context(_set) for the local universe constraints, also
recording which variables will be local and hence generalized after
inference if defining a polymorphic ind/constant.
- this patch makes coq stop compiling at indtypes.ml
  • Loading branch information...
1 parent 318301c commit 68ec29f109f18fa8c2d74de77fad635884dca807 @mattam82 mattam82 committed
View
16 Makefile
@@ -237,7 +237,21 @@ devdocclean:
.PHONY: tags
tags:
- echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \
+ echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \
+ etags --language=none\
+ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/type[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
+ "--regex=/module[ \t]+\([^ \t]+\)/\1/"
+ echo $(ML4FILES) | sort -r | xargs \
+ etags --append --language=none\
+ "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"
+
+checker-tags:
+ echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \
etags --language=none\
"--regex=/let[ \t]+\([^ \t]+\)/\1/" \
"--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
View
22 checker/declarations.ml
@@ -14,20 +14,7 @@ type retroknowledge
type engagement = ImpredicativeSet
let val_eng = val_enum "eng" 1
-
-type polymorphic_arity = {
- poly_param_levels : Univ.universe option list;
- poly_level : Univ.universe;
-}
-let val_pol_arity =
- val_tuple ~name:"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
-
-type constant_type =
- | NonPolymorphicType of constr
- | PolymorphicArity of rel_context * polymorphic_arity
-
-let val_cst_type =
- val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
+let val_cst_type = val_constr
(** Substitutions, code imported from kernel/mod_subst *)
@@ -513,12 +500,15 @@ let subst_constant_def sub = function
| Def c -> Def (subst_constr_subst sub c)
| OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+(** Local variables and graph *)
+type universe_context = Univ.UniverseLSet.t * Univ.constraints
+
type constant_body = {
const_hyps : section_context; (* New: younger hyp at top *)
const_body : constant_def;
- const_type : constant_type;
+ const_type : types;
const_body_code : to_patch_substituted;
- const_constraints : Univ.constraints }
+ const_constraints : universe_context }
let body_of_constant cb = match cb.const_body with
| Undef _ -> None
View
16 checker/declarations.mli
@@ -15,15 +15,6 @@ type engagement = ImpredicativeSet
(* Constants *)
-type polymorphic_arity = {
- poly_param_levels : Univ.universe option list;
- poly_level : Univ.universe;
-}
-
-type constant_type =
- | NonPolymorphicType of constr
- | PolymorphicArity of rel_context * polymorphic_arity
-
type constr_substituted
val force_constr : constr_substituted -> constr
val from_val : constr -> constr_substituted
@@ -52,12 +43,15 @@ type constant_def =
| Def of constr_substituted
| OpaqueDef of lazy_constr
+(** Local variables and graph *)
+type universe_context = Univ.UniverseLSet.t * Univ.constraints
+
type constant_body = {
const_hyps : section_context; (* New: younger hyp at top *)
const_body : constant_def;
- const_type : constant_type;
+ const_type : types;
const_body_code : to_patch_substituted;
- const_constraints : Univ.constraints }
+ const_constraints : universe_context }
val body_of_constant : constant_body -> constr_substituted option
val constant_has_body : constant_body -> bool
View
2 checker/environ.mli
@@ -52,7 +52,7 @@ val lookup_constant : constant -> env -> Declarations.constant_body
val add_constant : constant -> Declarations.constant_body -> env -> env
type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
-val constant_value : env -> constant -> constr
+val constant_value : env -> constant puniverses -> constr
val evaluable_constant : constant -> env -> bool
(* Inductives *)
View
6 checker/inductive.mli
@@ -23,10 +23,10 @@ type mind_specif = mutual_inductive_body * one_inductive_body
Raises [Not_found] if the inductive type is not found. *)
val lookup_mind_specif : env -> inductive -> mind_specif
-val type_of_inductive : env -> mind_specif -> constr
+val type_of_inductive : env -> mind_specif -> constr * Univ.constraints
(* Return type as quoted by the user *)
-val type_of_constructor : constructor -> mind_specif -> constr
+val type_of_constructor : constructor -> mind_specif -> constr * Univ.constraints
val arities_of_specif : mutual_inductive -> mind_specif -> constr array
@@ -37,7 +37,7 @@ val arities_of_specif : mutual_inductive -> mind_specif -> constr array
introduced by products) and the type for the whole expression.
*)
val type_case_branches :
- env -> inductive * constr list -> constr * constr -> constr
+ env -> inductive puniverses * constr list -> constr * constr -> constr
-> constr array * constr
(* Check a [case_info] actually correspond to a Case expression on the
View
18 kernel/cbytegen.ml
@@ -353,7 +353,7 @@ let rec str_const c =
| App(f,args) ->
begin
match kind_of_term f with
- | Construct((kn,j),i) ->
+ | Construct(((kn,j),i),u) ->
begin
let oib = lookup_mind kn !global_env in
let oip = oib.mind_packets.(j) in
@@ -422,8 +422,8 @@ let rec str_const c =
end
| _ -> Bconstr c
end
- | Ind ind -> Bstrconst (Const_ind ind)
- | Construct ((kn,j),i) ->
+ | Ind (ind,u) -> Bstrconst (Const_ind ind)
+ | Construct (((kn,j),i),u) ->
begin
(* spiwack: tries first to apply the run-time compilation
behavior of the constructor, as in 2/ above *)
@@ -657,7 +657,7 @@ let rec compile_constr reloc c sz cont =
in
compile_constr reloc a sz
(try
- let entry = Term.Ind ind in
+ let entry = Term.Ind (ind,[]) in
Retroknowledge.get_vm_before_match_info (!global_env).retroknowledge
entry code_sw
with Not_found ->
@@ -689,13 +689,13 @@ and compile_const =
falls back on its normal behavior *)
try
Retroknowledge.get_vm_compiling_info (!global_env).retroknowledge
- (kind_of_term (mkConst kn)) reloc args sz cont
+ (kind_of_term (mkConstU kn)) reloc args sz cont
with Not_found ->
if Int.equal nargs 0 then
- Kgetglobal (get_allias !global_env kn) :: cont
+ Kgetglobal (get_allias !global_env (Univ.out_punivs kn)) :: cont
else
comp_app (fun _ _ _ cont ->
- Kgetglobal (get_allias !global_env kn) :: cont)
+ Kgetglobal (get_allias !global_env (Univ.out_punivs kn)) :: cont)
compile_constr reloc () args sz cont
let compile env c =
@@ -723,7 +723,7 @@ let compile_constant_body env = function
match kind_of_term body with
| Const kn' ->
(* we use the canonical name of the constant*)
- let con= constant_of_kn (canonical_con kn') in
+ let con= constant_of_kn (canonical_con (Univ.out_punivs kn')) in
BCallias (get_allias env con)
| _ ->
let res = compile env body in
@@ -751,7 +751,7 @@ let compile_structured_int31 fc args =
Const_b0
(Array.fold_left
(fun temp_i -> fun t -> match kind_of_term t with
- | Construct (_,d) -> 2*temp_i+d-1
+ | Construct ((_,d),_) -> 2*temp_i+d-1
| _ -> raise NotClosed)
0 args
)
View
4 kernel/cemitcodes.ml
@@ -330,7 +330,7 @@ let subst_patch s (ri,pos) =
let ci = {a.ci with ci_ind = (subst_ind s kn,i)} in
(Reloc_annot {a with ci = ci},pos)
| Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
- | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con s kn)), pos)
+ | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con_kn s kn)), pos)
let subst_to_patch s (code,pl,fv) =
code,List.rev_map (subst_patch s) pl,fv
@@ -342,7 +342,7 @@ type body_code =
let subst_body_code s = function
| BCdefined tp -> BCdefined (subst_to_patch s tp)
- | BCallias kn -> BCallias (fst (subst_con s kn))
+ | BCallias kn -> BCallias (fst (subst_con_kn s kn))
| BCconstant -> BCconstant
type to_patch_substituted = body_code substituted
View
20 kernel/closure.ml
@@ -206,7 +206,7 @@ let unfold_red kn =
* instantiations (cbv or lazy) are.
*)
-type table_key = id_key
+type table_key = (inv_rel_key, constant puniverses) tableKey
module IdKeyHash =
struct
@@ -246,7 +246,7 @@ let ref_value_cache info ref =
| Some t -> lift n t
end
| VarKey id -> List.assoc id info.i_vars
- | ConstKey cst -> constant_value info.i_env cst
+ | ConstKey cst -> constant_value_unsafe info.i_env cst
in
let v = info.i_repr info body in
KeyTable.add info.i_tab ref v;
@@ -329,8 +329,8 @@ and fterm =
| FAtom of constr (* Metas and Sorts *)
| FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
- | FInd of inductive
- | FConstruct of constructor
+ | FInd of inductive puniverses
+ | FConstruct of constructor puniverses
| FApp of fconstr * fconstr array
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
@@ -616,9 +616,9 @@ let rec to_constr constr_fun lfts v =
| FAtom c -> exliftn lfts c
| FCast (a,k,b) ->
mkCast (constr_fun lfts a, k, constr_fun lfts b)
- | FFlex (ConstKey op) -> mkConst op
- | FInd op -> mkInd op
- | FConstruct op -> mkConstruct op
+ | FFlex (ConstKey op) -> mkConstU op
+ | FInd op -> mkIndU op
+ | FConstruct op -> mkConstructU op
| FCases (ci,p,c,ve) ->
mkCase (ci, constr_fun lfts p,
constr_fun lfts c,
@@ -872,8 +872,8 @@ let rec knr info m stk =
(match get_args n tys f e stk with
Inl e', s -> knit info e' f s
| Inr lam, s -> (lam,s))
- | FFlex(ConstKey kn) when red_set info.i_flags (fCONST kn) ->
- (match ref_value_cache info (ConstKey kn) with
+ | FFlex(ConstKey (kn,_ as c)) when red_set info.i_flags (fCONST kn) ->
+ (match ref_value_cache info (ConstKey c) with
Some v -> kni info v stk
| None -> (set_norm m; (m,stk)))
| FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
@@ -884,7 +884,7 @@ let rec knr info m stk =
(match ref_value_cache info (RelKey k) with
Some v -> kni info v stk
| None -> (set_norm m; (m,stk)))
- | FConstruct(ind,c) when red_set info.i_flags fIOTA ->
+ | FConstruct((ind,c),u) when red_set info.i_flags fIOTA ->
(match strip_update_shift_app m stk with
(depth, args, Zcase(ci,_,br)::s) ->
assert (ci.ci_npar>=0);
View
6 kernel/closure.mli
@@ -81,7 +81,7 @@ val unfold_side_red : reds
val unfold_red : evaluable_global_reference -> reds
(***********************************************************************)
-type table_key = id_key
+type table_key = (inv_rel_key, constant puniverses) tableKey
type 'a infos
val ref_value_cache: 'a infos -> table_key -> 'a option
@@ -105,8 +105,8 @@ type fterm =
| FAtom of constr (** Metas and Sorts *)
| FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
- | FInd of inductive
- | FConstruct of constructor
+ | FInd of inductive puniverses
+ | FConstruct of constructor puniverses
| FApp of fconstr * fconstr array
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
View
6 kernel/conv_oracle.mli
@@ -12,7 +12,7 @@ open Names
If [oracle_order kn1 kn2] is true, then unfold kn1 first.
Note: the oracle does not introduce incompleteness, it only
tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : bool -> 'a tableKey -> 'a tableKey -> bool
+val oracle_order : bool -> ('a,constant) tableKey -> ('a,constant) tableKey -> bool
(** Priority for the expansion of constant in the conversion test.
* Higher levels means that the expansion is less prioritary.
@@ -25,11 +25,11 @@ val transparent : level
(** Check whether a level is transparent *)
val is_transparent : level -> bool
-val get_strategy : 'a tableKey -> level
+val get_strategy : ('a,constant) tableKey -> level
(** Sets the level of a constant.
* Level of RelKey constant cannot be set. *)
-val set_strategy : 'a tableKey -> level -> unit
+val set_strategy : ('a,constant) tableKey -> level -> unit
val get_transp_state : unit -> transparent_state
View
2 kernel/cooking.ml
@@ -151,4 +151,4 @@ let cook_constant env r =
let j = make_judge (constr_of_def body) typ in
Typeops.make_polymorphic env j
in
- (body, typ, cb.const_constraints, const_hyps)
+ (body, typ, cb.const_universes, const_hyps)
View
2 kernel/cooking.mli
@@ -23,7 +23,7 @@ type recipe = {
val cook_constant :
env -> recipe ->
- constant_def * constant_type * constraints * Sign.section_context
+ constant_def * constant_type * universe_context * Sign.section_context
(** {6 Utility functions used in module [Discharge]. } *)
View
64 kernel/declarations.ml
@@ -32,14 +32,7 @@ type engagement = ImpredicativeSet
(*s Constants (internal representation) (Definition/Axiom) *)
-type polymorphic_arity = {
- poly_param_levels : universe option list;
- poly_level : universe;
-}
-
-type constant_type =
- | NonPolymorphicType of types
- | PolymorphicArity of rel_context * polymorphic_arity
+type constant_type = types
type constr_substituted = constr substituted
@@ -88,7 +81,7 @@ type constant_body = {
const_body : constant_def;
const_type : constant_type;
const_body_code : Cemitcodes.to_patch_substituted;
- const_constraints : constraints }
+ const_universes : universe_context }
let body_of_constant cb = match cb.const_body with
| Undef _ -> None
@@ -117,9 +110,7 @@ let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
let subst_const_type sub arity =
if is_empty_subst sub then arity
- else match arity with
- | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
- | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
+ else subst_mps sub arity
let subst_const_def sub = function
| Undef inl -> Undef inl
@@ -131,7 +122,7 @@ let subst_const_body sub cb = {
const_body = subst_const_def sub cb.const_body;
const_type = subst_const_type sub cb.const_type;
const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
- const_constraints = cb.const_constraints}
+ const_universes = cb.const_universes}
(* Hash-consing of [constant_body] *)
@@ -143,16 +134,7 @@ let hcons_rel_decl ((n,oc,t) as d) =
let hcons_rel_context l = List.smartmap hcons_rel_decl l
-let hcons_polyarity ar =
- { poly_param_levels =
- List.smartmap (Option.smartmap hcons_univ) ar.poly_param_levels;
- poly_level = hcons_univ ar.poly_level }
-
-let hcons_const_type = function
- | NonPolymorphicType t ->
- NonPolymorphicType (hcons_constr t)
- | PolymorphicArity (ctx,s) ->
- PolymorphicArity (hcons_rel_context ctx, hcons_polyarity s)
+let hcons_const_type = hcons_constr
let hcons_const_def = function
| Undef inl -> Undef inl
@@ -168,8 +150,8 @@ let hcons_const_def = function
let hcons_const_body cb =
{ cb with
const_body = hcons_const_def cb.const_body;
- const_type = hcons_const_type cb.const_type;
- const_constraints = hcons_constraints cb.const_constraints }
+ const_type = hcons_constr cb.const_type;
+ const_universes = hcons_universe_context cb.const_universes }
(*s Inductive types (internal representation with redundant
@@ -227,15 +209,11 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
*)
-type monomorphic_inductive_arity = {
+type inductive_arity = {
mind_user_arity : constr;
mind_sort : sorts;
}
-type inductive_arity =
-| Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_arity
-
type one_inductive_body = {
(* Primitive datas *)
@@ -246,9 +224,12 @@ type one_inductive_body = {
(* Arity context of [Ii] with parameters: [forall params, Ui] *)
mind_arity_ctxt : rel_context;
- (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *)
+ (* Arity sort, original user arity *)
mind_arity : inductive_arity;
+ (* Local universe variables and constraints *)
+ mind_universes : universe_context;
+
(* Names of the constructors: [cij] *)
mind_consnames : identifier array;
@@ -319,13 +300,9 @@ type mutual_inductive_body = {
}
-let subst_indarity sub = function
-| Monomorphic s ->
- Monomorphic {
- mind_user_arity = subst_mps sub s.mind_user_arity;
- mind_sort = s.mind_sort;
- }
-| Polymorphic s as x -> x
+let subst_indarity sub s =
+ { mind_user_arity = subst_mps sub s.mind_user_arity;
+ mind_sort = s.mind_sort }
let subst_mind_packet sub mbp =
{ mind_consnames = mbp.mind_consnames;
@@ -334,6 +311,9 @@ let subst_mind_packet sub mbp =
mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
mind_arity = subst_indarity sub mbp.mind_arity;
+ (* FIXME: Really? No need to substitute in universe levels?
+ copying mind_constraints below *)
+ mind_universes = mbp.mind_universes;
mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
mind_nrealargs = mbp.mind_nrealargs;
mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
@@ -355,11 +335,9 @@ let subst_mind sub mib =
mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
mind_constraints = mib.mind_constraints }
-let hcons_indarity = function
- | Monomorphic a ->
- Monomorphic { mind_user_arity = hcons_constr a.mind_user_arity;
- mind_sort = hcons_sorts a.mind_sort }
- | Polymorphic a -> Polymorphic (hcons_polyarity a)
+let hcons_indarity a =
+ { mind_user_arity = hcons_constr a.mind_user_arity;
+ mind_sort = hcons_sorts a.mind_sort }
let hcons_mind_packet oib =
{ oib with
View
25 kernel/declarations.mli
@@ -21,14 +21,7 @@ type engagement = ImpredicativeSet
(** {6 Representation of constants (Definition/Axiom) } *)
-type polymorphic_arity = {
- poly_param_levels : universe option list;
- poly_level : universe;
-}
-
-type constant_type =
- | NonPolymorphicType of types
- | PolymorphicArity of rel_context * polymorphic_arity
+type constant_type = types
type constr_substituted
@@ -65,9 +58,9 @@ type constant_def =
type constant_body = {
const_hyps : section_context; (** New: younger hyp at top *)
const_body : constant_def;
- const_type : constant_type;
+ const_type : types;
const_body_code : to_patch_substituted;
- const_constraints : constraints }
+ const_universes : universe_context }
val subst_const_def : substitution -> constant_def -> constant_def
val subst_const_body : substitution -> constant_body -> constant_body
@@ -111,15 +104,11 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
v}
*)
-type monomorphic_inductive_arity = {
- mind_user_arity : constr;
+type inductive_arity = {
+ mind_user_arity : types;
mind_sort : sorts;
}
-type inductive_arity =
-| Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_arity
-
type one_inductive_body = {
(** {8 Primitive datas } *)
@@ -127,7 +116,9 @@ type one_inductive_body = {
mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
- mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *)
+ mind_arity : inductive_arity; (** Arity sort and original user arity *)
+
+ mind_universes : universe_context; (** Local universe variables and constraints *)
mind_consnames : identifier array; (** Names of the constructors: [cij] *)
View
1 kernel/entries.mli
@@ -55,6 +55,7 @@ type definition_entry = {
const_entry_secctx : section_context option;
const_entry_type : types option;
const_entry_polymorphic : bool;
+ const_entry_universes : universe_context;
const_entry_opaque : bool }
type inline = int option (* inlining level, None for no inlining *)
View
75 kernel/environ.ml
@@ -163,18 +163,23 @@ let add_constant kn cs env =
{ env with env_globals = new_globals }
(* constant_type gives the type of a constant *)
-let constant_type env kn =
+let constant_type env (kn,u) =
let cb = lookup_constant kn env in
- cb.const_type
+ let subst = make_universe_subst u cb.const_universes in
+ (subst_univs_constr subst cb.const_type,
+ instantiate_univ_context subst cb.const_universes)
type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
-let constant_value env kn =
+let constant_value env (kn,u) =
let cb = lookup_constant kn env in
match cb.const_body with
- | Def l_body -> Declarations.force l_body
+ | Def l_body ->
+ let subst = make_universe_subst u cb.const_universes in
+ (subst_univs_constr subst (Declarations.force l_body),
+ instantiate_univ_context subst cb.const_universes)
| OpaqueDef _ -> raise (NotEvaluableConst Opaque)
| Undef _ -> raise (NotEvaluableConst NoBody)
@@ -182,10 +187,44 @@ let constant_opt_value env cst =
try Some (constant_value env cst)
with NotEvaluableConst _ -> None
+let constant_value_and_type env (kn, u) =
+ let cb = lookup_constant kn env in
+ let subst = make_universe_subst u cb.const_universes in
+ let cst = instantiate_univ_context subst cb.const_universes in
+ let b' = match cb.const_body with
+ | Def l_body -> Some (subst_univs_constr subst (Declarations.force l_body))
+ | OpaqueDef _ -> None
+ | Undef _ -> None
+ in b', subst_univs_constr subst cb.const_type, cst
+
+(* TODO remove *)
+
+(* constant_type gives the type of a constant *)
+let constant_type_unsafe env (kn,u) =
+ let cb = lookup_constant kn env in
+ let subst = make_universe_subst u cb.const_universes in
+ subst_univs_constr subst cb.const_type
+
+let constant_value_unsafe env (kn,u) =
+ let cb = lookup_constant kn env in
+ match cb.const_body with
+ | Def l_body ->
+ let subst = make_universe_subst u cb.const_universes in
+ subst_univs_constr subst (Declarations.force l_body)
+ | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
+ | Undef _ -> raise (NotEvaluableConst NoBody)
+
+let constant_opt_value_unsafe env cst =
+ try Some (constant_value_unsafe env cst)
+ with NotEvaluableConst _ -> None
+
(* A global const is evaluable if it is defined and not opaque *)
-let evaluable_constant cst env =
- try let _ = constant_value env cst in true
- with NotEvaluableConst _ -> false
+let evaluable_constant (kn,_) env =
+ let cb = lookup_constant kn env in
+ match cb.const_body with
+ | Def _ -> true
+ | OpaqueDef _ -> false
+ | Undef _ -> false
(* Mutual Inductives *)
let lookup_mind = lookup_mind
@@ -228,9 +267,9 @@ let lookup_constructor_variables (ind,_) env =
let vars_of_global env constr =
match kind_of_term constr with
Var id -> [id]
- | Const kn -> lookup_constant_variables kn env
- | Ind ind -> lookup_inductive_variables ind env
- | Construct cstr -> lookup_constructor_variables cstr env
+ | Const (kn,_) -> lookup_constant_variables kn env
+ | Ind (ind,_) -> lookup_inductive_variables ind env
+ | Construct (cstr,_) -> lookup_constructor_variables cstr env
| _ -> raise Not_found
let global_vars_set env constr =
@@ -401,7 +440,7 @@ let unregister env field =
is abstract, and that the only function which add elements to the
retroknowledge is Environ.register which enforces this shape *)
(match retroknowledge find env field with
- | Ind i31t -> let i31c = Construct (i31t, 1) in
+ | Ind (i31t,u) -> let i31c = Construct ((i31t, 1),u) in
{env with retroknowledge =
remove (retroknowledge clear_info env i31c) field}
| _ -> assert false)
@@ -458,13 +497,13 @@ fun env field value ->
operators to the reactive retroknowledge. *)
let add_int31_binop_from_const op =
match value with
- | Const kn -> retroknowledge add_int31_op env value 2
+ | Const (kn,_) -> retroknowledge add_int31_op env value 2
op kn
| _ -> anomaly "Environ.register: should be a constant"
in
let add_int31_unop_from_const op =
match value with
- | Const kn -> retroknowledge add_int31_op env value 1
+ | Const (kn,_) -> retroknowledge add_int31_op env value 1
op kn
| _ -> anomaly "Environ.register: should be a constant"
in
@@ -476,9 +515,9 @@ fun env field value ->
match field with
| KInt31 (grp, Int31Type) ->
(match Retroknowledge.find rk (KInt31 (grp,Int31Bits)) with
- | Ind i31bit_type ->
+ | Ind (i31bit_type,u) ->
(match value with
- | Ind i31t ->
+ | Ind (i31t,u) ->
Retroknowledge.add_vm_decompile_constant_info rk
value (constr_of_int31 i31t i31bit_type)
| _ -> anomaly "Environ.register: should be an inductive type")
@@ -490,7 +529,7 @@ fun env field value ->
match field with
| KInt31 (_, Int31Type) ->
let i31c = match value with
- | Ind i31t -> (Construct (i31t, 1))
+ | Ind (i31t,u) -> (Construct ((i31t, 1),u))
| _ -> anomaly "Environ.register: should be an inductive type"
in
add_int31_decompilation_from_type
@@ -508,14 +547,14 @@ fun env field value ->
| KInt31 (_, Int31TimesC) -> add_int31_binop_from_const Cbytecodes.Kmulcint31
| KInt31 (_, Int31Div21) -> (* this is a ternary operation *)
(match value with
- | Const kn ->
+ | Const (kn,u) ->
retroknowledge add_int31_op env value 3
Cbytecodes.Kdiv21int31 kn
| _ -> anomaly "Environ.register: should be a constant")
| KInt31 (_, Int31Div) -> add_int31_binop_from_const Cbytecodes.Kdivint31
| KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *)
(match value with
- | Const kn ->
+ | Const (kn,u) ->
retroknowledge add_int31_op env value 3
Cbytecodes.Kaddmuldivint31 kn
| _ -> anomaly "Environ.register: should be a constant")
View
16 kernel/environ.mli
@@ -119,7 +119,7 @@ val add_constant : constant -> constant_body -> env -> env
(** Looks up in the context of global constant names
raises [Not_found] if the required path is not found *)
val lookup_constant : constant -> env -> constant_body
-val evaluable_constant : constant -> env -> bool
+val evaluable_constant : constant puniverses -> env -> bool
(** {6 ... } *)
(** [constant_value env c] raises [NotEvaluableConst Opaque] if
@@ -129,9 +129,17 @@ val evaluable_constant : constant -> env -> bool
type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
-val constant_value : env -> constant -> constr
-val constant_type : env -> constant -> constant_type
-val constant_opt_value : env -> constant -> constr option
+val constant_value : env -> constant puniverses -> constr * Univ.constraints
+val constant_type : env -> constant puniverses -> types * Univ.constraints
+val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option
+val constant_value_and_type : env -> constant puniverses ->
+ types option * constr * Univ.constraints
+
+(* FIXME: remove *)
+val constant_value_unsafe : env -> constant puniverses -> constr
+val constant_type_unsafe : env -> constant puniverses -> types
+val constant_opt_value_unsafe : env -> constant puniverses -> constr option
+
(** {5 Inductive types } *)
View
5 kernel/indtypes.ml
@@ -108,6 +108,10 @@ let is_unit constrsinfos =
| [] -> (* type without constructors *) true
| _ -> false
+let infer_type env t =
+ (* TODO next *)
+ infer_type env empty_universe_context_set t
+
let rec infos_and_sort env t =
let t = whd_betadeltaiota env t in
match kind_of_term t with
@@ -173,7 +177,6 @@ let infer_constructor_packet env_ar_par params lc =
let level = max_inductive_sort (Array.map (fun j -> j.utj_type) jlc) in
(* compute *)
let info = small_unit (List.map (infos_and_sort env_ar_par) lc) in
-
(info,lc'',level,cst)
(* Type-check an inductive definition. Does not check positivity
View
160 kernel/inductive.ml
@@ -35,14 +35,14 @@ let find_inductive env c =
let (t, l) = decompose_app (whd_betadeltaiota env c) in
match kind_of_term t with
| Ind ind
- when (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
+ when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite -> (ind, l)
| _ -> raise Not_found
let find_coinductive env c =
let (t, l) = decompose_app (whd_betadeltaiota env c) in
match kind_of_term t with
| Ind ind
- when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
+ when not (fst (lookup_mind_specif env (out_punivs ind))).mind_finite -> (ind, l)
| _ -> raise Not_found
let inductive_params (mib,_) = mib.mind_nparams
@@ -123,81 +123,70 @@ let cons_subst u su subst =
try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst
with Not_found -> (u, su) :: subst
-let actualize_decl_level env lev t =
- let sign,s = dest_arity env t in
- mkArity (sign,lev)
-
-let polymorphism_on_non_applied_parameters = false
-
-(* Bind expected levels of parameters to actual levels *)
-(* Propagate the new levels in the signature *)
-let rec make_subst env = function
- | (_,Some _,_ as t)::sign, exp, args ->
- let ctx,subst = make_subst env (sign, exp, args) in
- t::ctx, subst
- | d::sign, None::exp, args ->
- let args = match args with _::args -> args | [] -> [] in
- let ctx,subst = make_subst env (sign, exp, args) in
- d::ctx, subst
- | d::sign, Some u::exp, a::args ->
- (* We recover the level of the argument, but we don't change the *)
- (* level in the corresponding type in the arity; this level in the *)
- (* arity is a global level which, at typing time, will be enforce *)
- (* to be greater than the level of the argument; this is probably *)
- (* a useless extra constraint *)
- let s = sort_as_univ (snd (dest_arity env a)) in
- let ctx,subst = make_subst env (sign, exp, args) in
- d::ctx, cons_subst u s subst
- | (na,None,t as d)::sign, Some u::exp, [] ->
- (* No more argument here: we instantiate the type with a fresh level *)
- (* which is first propagated to the corresponding premise in the arity *)
- (* (actualize_decl_level), then to the conclusion of the arity (via *)
- (* the substitution) *)
- let ctx,subst = make_subst env (sign, exp, []) in
- if polymorphism_on_non_applied_parameters then
- let s = fresh_local_univ () in
- let t = actualize_decl_level env (Type s) t in
- (na,None,t)::ctx, cons_subst u s subst
- else
- d::ctx, subst
- | sign, [], _ ->
- (* Uniform parameters are exhausted *)
- sign,[]
- | [], _, _ ->
- assert false
-
-let instantiate_universes env ctx ar argsorts =
- let args = Array.to_list argsorts in
- let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in
- let level = subst_large_constraints subst ar.poly_level in
- ctx,
- (* Singleton type not containing types are interpretable in Prop *)
- if is_type0m_univ level then prop_sort
- (* Non singleton type not containing types are interpretable in Set *)
- else if is_type0_univ level then set_sort
- (* This is a Type with constraints *)
- else Type level
+(* let actualize_decl_level env lev t = *)
+(* let sign,s = dest_arity env t in *)
+(* mkArity (sign,lev) *)
+
+(* let polymorphism_on_non_applied_parameters = false *)
+
+(* (\* Bind expected levels of parameters to actual levels *\) *)
+(* (\* Propagate the new levels in the signature *\) *)
+(* let rec make_subst env = function *)
+(* | (_,Some _,_ as t)::sign, exp, args -> *)
+(* let ctx,subst = make_subst env (sign, exp, args) in *)
+(* t::ctx, subst *)
+(* | d::sign, None::exp, args -> *)
+(* let args = match args with _::args -> args | [] -> [] in *)
+(* let ctx,subst = make_subst env (sign, exp, args) in *)
+(* d::ctx, subst *)
+(* | d::sign, Some u::exp, a::args -> *)
+(* (\* We recover the level of the argument, but we don't change the *\) *)
+(* (\* level in the corresponding type in the arity; this level in the *\) *)
+(* (\* arity is a global level which, at typing time, will be enforce *\) *)
+(* (\* to be greater than the level of the argument; this is probably *\) *)
+(* (\* a useless extra constraint *\) *)
+(* let s = sort_as_univ (snd (dest_arity env a)) in *)
+(* let ctx,subst = make_subst env (sign, exp, args) in *)
+(* d::ctx, cons_subst u s subst *)
+(* | (na,None,t as d)::sign, Some u::exp, [] -> *)
+(* (\* No more argument here: we instantiate the type with a fresh level *\) *)
+(* (\* which is first propagated to the corresponding premise in the arity *\) *)
+(* (\* (actualize_decl_level), then to the conclusion of the arity (via *\) *)
+(* (\* the substitution) *\) *)
+(* let ctx,subst = make_subst env (sign, exp, []) in *)
+(* if polymorphism_on_non_applied_parameters then *)
+(* let s = fresh_local_univ () in *)
+(* let t = actualize_decl_level env (Type s) t in *)
+(* (na,None,t)::ctx, cons_subst u s subst *)
+(* else *)
+(* d::ctx, subst *)
+(* | sign, [], _ -> *)
+(* (\* Uniform parameters are exhausted *\) *)
+(* sign,[] *)
+(* | [], _, _ -> *)
+(* assert false *)
+
+(* let instantiate_universes env ctx ar argsorts = *)
+(* let args = Array.to_list argsorts in *)
+(* let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in *)
+(* let level = subst_large_constraints subst ar.poly_level in *)
+(* ctx, *)
+(* (\* Singleton type not containing types are interpretable in Prop *\) *)
+(* if is_type0m_univ level then prop_sort *)
+(* (\* Non singleton type not containing types are interpretable in Set *\) *)
+(* else if is_type0_univ level then set_sort *)
+(* (\* This is a Type with constraints *\) *)
+(* else Type level *)
exception SingletonInductiveBecomesProp of identifier
-let type_of_inductive_knowing_parameters ?(polyprop=true) env mip paramtyps =
- match mip.mind_arity with
- | Monomorphic s ->
- s.mind_user_arity
- | Polymorphic ar ->
- let ctx = List.rev mip.mind_arity_ctxt in
- let ctx,s = instantiate_universes env ctx ar paramtyps in
- (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
- the situation where a non-Prop singleton inductive becomes Prop
- when applied to Prop params *)
- if not polyprop && not (is_type0m_univ ar.poly_level) && is_prop_sort s
- then raise (SingletonInductiveBecomesProp mip.mind_typename);
- mkArity (List.rev ctx,s)
-
-(* Type of a (non applied) inductive type *)
-
-let type_of_inductive env (_,mip) =
- type_of_inductive_knowing_parameters env mip [||]
+(* Type of an inductive type *)
+
+let type_of_inductive env ((_,mip),u) =
+ let subst = make_universe_subst u mip.mind_universes in
+ let cst = instantiate_univ_context subst mip.mind_universes in
+ (subst_univs_constr subst mip.mind_arity.mind_user_arity,
+ cst)
(* The max of an array of universes *)
@@ -212,13 +201,16 @@ let max_inductive_sort =
(************************************************************************)
(* Type of a constructor *)
-let type_of_constructor cstr (mib,mip) =
+let type_of_constructor (cstr,u) (mib,mip) =
let ind = inductive_of_constructor cstr in
let specif = mip.mind_user_lc in
let i = index_of_constructor cstr in
let nconstr = Array.length mip.mind_consnames in
if i > nconstr then error "Not enough constructors in the type.";
- constructor_instantiate (fst ind) mib specif.(i-1)
+ let subst = make_universe_subst u mip.mind_universes in
+ let cst = instantiate_univ_context subst mip.mind_universes in
+ let c = constructor_instantiate (fst ind) mib specif.(i-1) in
+ (subst_univs_constr subst c, cst)
let arities_of_specif kn (mib,mip) =
let specif = mip.mind_nf_lc in
@@ -250,9 +242,7 @@ let local_rels ctxt =
(* Get type of inductive, with parameters instantiated *)
let inductive_sort_family mip =
- match mip.mind_arity with
- | Monomorphic s -> family_of_sort s.mind_sort
- | Polymorphic _ -> InType
+ family_of_sort mip.mind_arity.mind_sort
let mind_arity mip =
mip.mind_arity_ctxt, inductive_sort_family mip
@@ -344,7 +334,7 @@ let build_branches_type ind (_,mip as specif) params p =
let build_case_type n p c realargs =
whd_betaiota (betazeta_appvect (n+1) p (Array.of_list (realargs@[c])))
-let type_case_branches env (ind,largs) pj c =
+let type_case_branches env ((ind,u),largs) pj c =
let specif = lookup_mind_specif env ind in
let nparams = inductive_params specif in
let (params,realargs) = List.chop nparams largs in
@@ -440,7 +430,7 @@ type guard_env =
genv : subterm_spec Lazy.t list;
}
-let make_renv env recarg (kn,tyi) =
+let make_renv env recarg ((kn,tyi),u) =
let mib = Environ.lookup_mind kn env in
let mind_recvec =
Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
@@ -563,7 +553,7 @@ let rec subterm_specif renv stack t =
with Not_found -> None in
(match oind with
None -> Not_subterm (* happens if fix is polymorphic *)
- | Some ind ->
+ | Some (ind,u) ->
let nbfix = Array.length typarray in
let recargs = lookup_subterms renv.env ind in
(* pushing the fixpoints *)
@@ -725,7 +715,7 @@ let check_one_fix renv recpos def =
if evaluable_constant kn renv.env then
try List.iter (check_rec_call renv []) l
with (FixGuardError _ ) ->
- let value = (applist(constant_value renv.env kn, l)) in
+ let value = (applist(constant_value_unsafe renv.env kn, l)) in
check_rec_call renv stack value
else List.iter (check_rec_call renv []) l
@@ -870,7 +860,7 @@ let check_one_cofix env nbfix def deftype =
else if not(List.for_all (noccur_with_meta n nbfix) args) then
raise (CoFixGuardError (env,NestedRecursiveOccurrences))
- | Construct (_,i as cstr_kn) ->
+ | Construct ((_,i as cstr_kn),u) ->
let lra = vlra.(i-1) in
let mI = inductive_of_constructor cstr_kn in
let (mib,mip) = lookup_mind_specif env mI in
@@ -929,7 +919,7 @@ let check_one_cofix env nbfix def deftype =
| _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
- let (mind, _) = codomain_is_coind env deftype in
+ let ((mind, _),_) = codomain_is_coind env deftype in
let vlra = lookup_subterms env mind in
check_rec_call env false 1 (dest_subterms vlra) def
View
20 kernel/inductive.mli
@@ -20,9 +20,9 @@ open Environ
only a coinductive type.
They raise [Not_found] if not convertible to a recursive type. *)
-val find_rectype : env -> types -> inductive * constr list
-val find_inductive : env -> types -> inductive * constr list
-val find_coinductive : env -> types -> inductive * constr list
+val find_rectype : env -> types -> inductive puniverses * constr list
+val find_inductive : env -> types -> inductive puniverses * constr list
+val find_coinductive : env -> types -> inductive puniverses * constr list
type mind_specif = mutual_inductive_body * one_inductive_body
@@ -34,12 +34,12 @@ val lookup_mind_specif : env -> inductive -> mind_specif
(** {6 Functions to build standard types related to inductive } *)
val ind_subst : mutual_inductive -> mutual_inductive_body -> constr list
-val type_of_inductive : env -> mind_specif -> types
+val type_of_inductive : env -> mind_specif puniverses -> types * Univ.constraints
val elim_sorts : mind_specif -> sorts_family list
(** Return type as quoted by the user *)
-val type_of_constructor : constructor -> mind_specif -> types
+val type_of_constructor : constructor puniverses -> mind_specif -> types * Univ.constraints
(** Return constructor types in normal form *)
val arities_of_constructors : inductive -> mind_specif -> types array
@@ -60,7 +60,7 @@ val inductive_params : mind_specif -> int
the universe constraints generated.
*)
val type_case_branches :
- env -> inductive * constr list -> unsafe_judgment -> constr
+ env -> inductive puniverses * constr list -> unsafe_judgment -> constr
-> types array * types * constraints
val build_branches_type :
@@ -91,13 +91,13 @@ val check_cofix : env -> cofixpoint -> unit
exception SingletonInductiveBecomesProp of identifier
-val type_of_inductive_knowing_parameters : ?polyprop:bool ->
- env -> one_inductive_body -> types array -> types
+(* val type_of_inductive_knowing_parameters : ?polyprop:bool -> *)
+(* env -> one_inductive_body -> types array -> types *)
val max_inductive_sort : sorts array -> universe
-val instantiate_universes : env -> rel_context ->
- polymorphic_arity -> types array -> rel_context * sorts
+(* val instantiate_universes : env -> rel_context -> *)
+(* inductive_arity -> types array -> rel_context * sorts *)
(** {6 Debug} *)
View
19 kernel/mod_subst.ml
@@ -290,12 +290,12 @@ let subst_ind sub mind =
| Canonical -> mind_of_delta2 resolve mind'
with No_subst -> mind
-let subst_con0 sub con =
+let subst_con0 sub (con,u) =
let kn1,kn2 = user_con con,canonical_con con in
let mp1,dir,l = repr_kn kn1 in
let mp2,_,_ = repr_kn kn2 in
let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in
- let dup con = con, mkConst con in
+ let dup con = con, mkConstU (con,u) in
let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
match constant_of_delta_with_inline resolve con' with
| Some t ->
@@ -310,7 +310,10 @@ let subst_con0 sub con =
let subst_con sub con =
try subst_con0 sub con
- with No_subst -> con, mkConst con
+ with No_subst -> fst con, mkConstU con
+
+let subst_con_kn sub con =
+ subst_con sub (con,[])
(* Here the semantics is completely unclear.
What does "Hint Unfold t" means when "t" is a parameter?
@@ -319,18 +322,18 @@ let subst_con sub con =
interpretation (i.e. an evaluable reference is never expanded). *)
let subst_evaluable_reference subst = function
| EvalVarRef id -> EvalVarRef id
- | EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn))
+ | EvalConstRef kn -> EvalConstRef (fst (subst_con_kn subst kn))
let rec map_kn f f' c =
let func = map_kn f f' in
match kind_of_term c with
| Const kn -> (try snd (f' kn) with No_subst -> c)
- | Ind (kn,i) ->
+ | Ind ((kn,i),u) ->
let kn' = f kn in
- if kn'==kn then c else mkInd (kn',i)
- | Construct ((kn,i),j) ->
+ if kn'==kn then c else mkIndU ((kn',i),u)
+ | Construct (((kn,i),j),u) ->
let kn' = f kn in
- if kn'==kn then c else mkConstruct ((kn',i),j)
+ if kn'==kn then c else mkConstructU (((kn',i),j),u)
| Case (ci,p,ct,l) ->
let ci_ind =
let (kn,i) = ci.ci_ind in
View
3 kernel/mod_subst.mli
@@ -116,6 +116,9 @@ val subst_kn :
substitution -> kernel_name -> kernel_name
val subst_con :
+ substitution -> constant puniverses -> constant * constr
+
+val subst_con_kn :
substitution -> constant -> constant * constr
(** Here the semantics is completely unclear.
View
4 kernel/modops.ml
@@ -242,8 +242,8 @@ let add_retroknowledge mp =
| Retroknowledge.RKRegister (f, e) ->
Environ.register env f
(match e with
- | Const kn -> kind_of_term (mkConst kn)
- | Ind ind -> kind_of_term (mkInd ind)
+ | Const kn -> kind_of_term (mkConstU kn)
+ | Ind ind -> kind_of_term (mkIndU ind)
| _ -> anomaly "Modops.add_retroknowledge: had to import an unsupported kind of term")
in
fun lclrk env ->
View
10 kernel/names.ml
@@ -516,8 +516,7 @@ let hcons_mind = Hashcons.simple_hcons Hcn.generate hcons_kn
let hcons_ind = Hashcons.simple_hcons Hind.generate hcons_mind
let hcons_construct = Hashcons.simple_hcons Hconstruct.generate hcons_ind
-
-(*******)
+(*****************)
type transparent_state = Idpred.t * Cpred.t
@@ -525,9 +524,10 @@ let empty_transparent_state = (Idpred.empty, Cpred.empty)
let full_transparent_state = (Idpred.full, Cpred.full)
let var_full_transparent_state = (Idpred.full, Cpred.empty)
let cst_full_transparent_state = (Idpred.empty, Cpred.full)
+(******************)
-type 'a tableKey =
- | ConstKey of constant
+type ('a,'b) tableKey =
+ | ConstKey of 'b
| VarKey of identifier
| RelKey of 'a
@@ -536,7 +536,7 @@ type inv_rel_key = int (* index in the [rel_context] part of environment
starting by the end, {\em inverse}
of de Bruijn indice *)
-type id_key = inv_rel_key tableKey
+type id_key = (inv_rel_key, constant) tableKey
let eq_id_key ik1 ik2 =
if ik1 == ik2 then true
View
16 kernel/names.mli
@@ -229,13 +229,7 @@ val hcons_mind : mutual_inductive -> mutual_inductive
val hcons_ind : inductive -> inductive
val hcons_construct : constructor -> constructor
-(******)
-
-type 'a tableKey =
- | ConstKey of constant
- | VarKey of identifier
- | RelKey of 'a
-
+(** Sets of names *)
type transparent_state = Idpred.t * Cpred.t
val empty_transparent_state : transparent_state
@@ -243,11 +237,17 @@ val full_transparent_state : transparent_state
val var_full_transparent_state : transparent_state
val cst_full_transparent_state : transparent_state
+
+type ('a,'b) tableKey =
+ | ConstKey of 'b
+ | VarKey of identifier
+ | RelKey of 'a
+
type inv_rel_key = int (** index in the [rel_context] part of environment
starting by the end, {e inverse}
of de Bruijn indice *)
-type id_key = inv_rel_key tableKey
+type id_key = (inv_rel_key,constant) tableKey
val eq_id_key : id_key -> id_key -> bool
View
14 kernel/reduction.ml
@@ -27,9 +27,15 @@ open Esubst
let unfold_reference ((ids, csts), infos) k =
match k with
| VarKey id when not (Idpred.mem id ids) -> None
- | ConstKey cst when not (Cpred.mem cst csts) -> None
+ | ConstKey (cst,_) when not (Cpred.mem cst csts) -> None
| _ -> unfold_reference infos k
+let conv_key k =
+ match k with
+ | VarKey id -> VarKey id
+ | ConstKey (cst,_) -> ConstKey cst
+ | RelKey n -> RelKey n
+
let rec is_empty_stack = function
[] -> true
| Zupdate _::s -> is_empty_stack s
@@ -297,7 +303,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
with NotConvertible ->
(* else the oracle tells which constant is to be expanded *)
let (app1,app2) =
- if Conv_oracle.oracle_order l2r fl1 fl2 then
+ if Conv_oracle.oracle_order l2r (conv_key fl1) (conv_key fl2) then
match unfold_reference infos fl1 with
| Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
| None ->
@@ -365,13 +371,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* Inductive types: MutInd MutConstruct Fix Cofix *)
- | (FInd ind1, FInd ind2) ->
+ | (FInd (ind1,u1), FInd (ind2,u2)) ->
if eq_ind ind1 ind2
then
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
- | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
+ | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
if Int.equal j1 j2 && eq_ind ind1 ind2
then
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
View
68 kernel/term.ml
@@ -100,6 +100,7 @@ type ('constr, 'types) pfixpoint =
(int array * int) * ('constr, 'types) prec_declaration
type ('constr, 'types) pcofixpoint =
int * ('constr, 'types) prec_declaration
+type 'a puniverses = 'a * universe_level list
(* [Var] is used for named variables and [Rel] for variables as
de Bruijn indices. *)
@@ -114,9 +115,9 @@ type ('constr, 'types) kind_of_term =
| Lambda of name * 'types * 'constr
| LetIn of name * 'constr * 'types * 'constr
| App of 'constr * 'constr array
- | Const of constant
- | Ind of inductive
- | Construct of constructor
+ | Const of constant puniverses
+ | Ind of inductive puniverses
+ | Construct of constructor puniverses
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
@@ -177,22 +178,27 @@ let mkApp (f, a) =
| _ -> App (f, a)
(* Constructs a constant *)
-let mkConst c = Const c
+let mkConst c = Const (c, [])
+let mkConstU c = Const c
(* Constructs an existential variable *)
let mkEvar e = Evar e
(* Constructs the ith (co)inductive type of the block named kn *)
-let mkInd m = Ind m
+let mkInd m = Ind (m, [])
+let mkIndU m = Ind m
(* Constructs the jth constructor of the ith (co)inductive type of the
block named kn. The array of terms correspond to the variables
introduced in the section *)
-let mkConstruct c = Construct c
+let mkConstruct c = Construct (c, [])
+let mkConstructU c = Construct c
(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
let mkCase (ci, p, c, ac) = Case (ci, p, c, ac)
+let out_punivs (a, _) = a
+
(* If recindxs = [|i1,...in|]
funnames = [|f1,...fn|]
typarray = [|t1,...tn|]
@@ -591,9 +597,9 @@ let compare_constr f t1 t2 =
Int.equal (Array.length l1) (Array.length l2) &&
f c1 c2 && Array.equal f l1 l2
| Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
- | Const c1, Const c2 -> eq_constant c1 c2
- | Ind c1, Ind c2 -> eq_ind c1 c2
- | Construct c1, Construct c2 -> eq_constructor c1 c2
+ | Const (c1,_), Const (c2,_) -> eq_constant c1 c2
+ | Ind (c1,_), Ind (c2,_) -> eq_ind c1 c2
+ | Construct (c1,_), Construct (c2,_) -> eq_constructor c1 c2
| Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
f p1 p2 & f c1 c2 && Array.equal f bl1 bl2
| Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
@@ -638,11 +644,11 @@ let constr_ord_int f t1 t2 =
| App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
| Evar (e1,l1), Evar (e2,l2) ->
((-) =? (Array.compare f)) e1 e2 l1 l2
- | Const c1, Const c2 -> kn_ord (canonical_con c1) (canonical_con c2)
- | Ind (spx, ix), Ind (spy, iy) ->
+ | Const (c1,u1), Const (c2,u2) -> kn_ord (canonical_con c1) (canonical_con c2)
+ | Ind ((spx, ix), ux), Ind ((spy, iy), uy) ->
let c = Int.compare ix iy in
if Int.equal c 0 then kn_ord (canonical_mind spx) (canonical_mind spy) else c
- | Construct ((spx, ix), jx), Construct ((spy, iy), jy) ->
+ | Construct (((spx, ix), jx), ux), Construct (((spy, iy), jy), uy) ->
let c = Int.compare jx jy in
if Int.equal c 0 then
(let c = Int.compare ix iy in
@@ -1143,6 +1149,30 @@ let strip_lam_assum t = snd (decompose_lam_assum t)
let strip_lam t = snd (decompose_lam t)
let strip_lam_n n t = snd (decompose_lam_n n t)
+let subst_univs_constr subst c =
+ if subst = [] then c
+ else
+ let f = List.map (Univ.subst_univs_level subst) in
+ let changed = ref false in
+ let rec aux t =
+ match kind_of_term t with
+ | Const (c, u) ->
+ let u' = f u in
+ if u' = u then t
+ else (changed := true; mkConstU (c, u'))
+ | Ind (i, u) ->
+ let u' = f u in
+ if u' = u then t
+ else (changed := true; mkIndU (i, u'))
+ | Construct (c, u) ->
+ let u' = f u in
+ if u' = u then t
+ else (changed := true; mkConstructU (c, u'))
+ | _ -> map_constr aux t
+ in
+ let c' = aux c in
+ if !changed then c' else c
+
(***************************)
(* Arities *)
(***************************)
@@ -1314,9 +1344,9 @@ let hcons_term (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
(t, combinesmall 8 (combine (Hashtbl.hash e) hl))
| Const c ->
(Const (sh_con c), combinesmall 9 (Hashtbl.hash c))
- | Ind ((kn,i) as ind) ->
+ | Ind ((kn,i),u as ind) ->
(Ind (sh_ind ind), combinesmall 9 (combine (Hashtbl.hash kn) i))
- | Construct (((kn,i),j) as c)->
+ | Construct ((((kn,i),j),u) as c)->
(Construct (sh_construct c), combinesmall 10 (combine3 (Hashtbl.hash kn) i j))
| Case (ci,p,c,bl) ->
let p, hp = sh_rec p
@@ -1371,11 +1401,11 @@ let rec hash_constr t =
combinesmall 7 (combine (hash_term_array l) (hash_constr c))
| Evar (e,l) ->
combinesmall 8 (combine (Hashtbl.hash e) (hash_term_array l))
- | Const c ->
+ | Const (c,u) ->
combinesmall 9 (Hashtbl.hash c) (* TODO: proper hash function for constants *)
- | Ind (kn,i) ->
+ | Ind ((kn,i),u) ->
combinesmall 9 (combine (Hashtbl.hash kn) i)
- | Construct ((kn,i),j) ->
+ | Construct (((kn,i),j),u) ->
combinesmall 10 (combine3 (Hashtbl.hash kn) i j)
| Case (_ , p, c, bl) ->
combinesmall 11 (combine3 (hash_constr c) (hash_constr p) (hash_term_array bl))
@@ -1425,6 +1455,10 @@ module Hcaseinfo =
let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ
let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
+let hcons_construct (c,u) = (hcons_construct c,u)
+let hcons_ind (i,u) = (hcons_ind i,u)
+let hcons_con (c,u) = (hcons_con c,u)
+
let hcons_constr =
hcons_term
(hcons_sorts,
View
20 kernel/term.mli
@@ -17,6 +17,8 @@ type sorts =
| Prop of contents (** Prop and Set *)
| Type of Univ.universe (** Type *)
+type 'a puniverses = 'a Univ.puniverses
+
val set_sort : sorts
val prop_sort : sorts
val type1_sort : sorts
@@ -127,17 +129,20 @@ val mkApp : constr * constr array -> constr
(** Constructs a constant
The array of terms correspond to the variables introduced in the section *)
val mkConst : constant -> constr
+val mkConstU : constant puniverses -> constr
(** Inductive types *)
(** Constructs the ith (co)inductive type of the block named kn
The array of terms correspond to the variables introduced in the section *)
val mkInd : inductive -> constr
+val mkIndU : inductive puniverses -> constr
(** Constructs the jth constructor of the ith (co)inductive type of the
block named kn. The array of terms correspond to the variables
introduced in the section *)
val mkConstruct : constructor -> constr
+val mkConstructU : constructor puniverses -> constr
(** Constructs a destructor of inductive type.
@@ -206,9 +211,9 @@ type ('constr, 'types) kind_of_term =
| Lambda of name * 'types * 'constr
| LetIn of name * 'constr * 'types * 'constr
| App of 'constr * 'constr array
- | Const of constant
- | Ind of inductive
- | Construct of constructor
+ | Const of constant puniverses
+ | Ind of inductive puniverses
+ | Construct of constructor puniverses
| Case of case_info * 'constr * 'constr * 'constr array
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
@@ -299,16 +304,16 @@ val destApplication : constr -> constr * constr array
val decompose_app : constr -> constr * constr list
(** Destructs a constant *)
-val destConst : constr -> constant
+val destConst : constr -> constant puniverses
(** Destructs an existential variable *)
val destEvar : constr -> existential
(** Destructs a (co)inductive type *)
-val destInd : constr -> inductive
+val destInd : constr -> inductive puniverses
(** Destructs a constructor *)
-val destConstruct : constr -> constructor
+val destConstruct : constr -> constructor puniverses
(** Destructs a [match c as x in I args return P with ... |
Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args
@@ -629,6 +634,9 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
val constr_ord : constr -> constr -> int
val hash_constr : constr -> int
+val subst_univs_constr : Univ.universe_subst -> constr -> constr
+
+
(*********************************************************************)
val hcons_sorts : sorts -> sorts
View
15 kernel/term_typing.ml
@@ -23,7 +23,7 @@ open Entries
open Indtypes
open Typeops
-let constrain_type env j cst1 = function
+let constrain_type env j cst1 poly = function
| None ->
make_polymorphic env j, cst1
| Some t ->
@@ -31,7 +31,10 @@ let constrain_type env j cst1 = function
let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
assert (eq_constr t tj.utj_val);
let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
- NonPolymorphicType t, cstrs
+ if poly then
+ make_polymorphic env { j with uj_type = tj.utj_val }, cstrs
+ else
+ NonPolymorphicType t, cstrs
let local_constrain_type env j cst1 = function
| None ->
@@ -93,7 +96,8 @@ let infer_declaration env dcl =
let j =
{uj_val = hcons_constr j.uj_val;
uj_type = hcons_constr j.uj_type} in
- let (typ,cst) = constrain_type env j cst c.const_entry_type in
+ let (typ,cst) = constrain_type env j cst
+ c.const_entry_polymorphic c.const_entry_type in
let def =
if c.const_entry_opaque
then OpaqueDef (Declarations.opaque_from_val j.uj_val)
@@ -103,6 +107,7 @@ let infer_declaration env dcl =
| ParameterEntry (ctx,t,nl) ->
let (j,cst) = infer env t in
let t = hcons_constr (Typeops.assumption_of_judgment env j) in
+ (* TODO: polymorphic parameters *)
Undef nl, NonPolymorphicType t, cst, ctx
let global_vars_set_constant_type env = function
@@ -113,7 +118,7 @@ let global_vars_set_constant_type env = function
(fun t c -> Idset.union (global_vars_set env t) c))
ctx ~init:Idset.empty
-let build_constant_declaration env kn (def,typ,cst,ctx) =
+let build_constant_declaration env kn (def,typ,univs,ctx) =
let hyps =
let inferred =
let ids_typ = global_vars_set_constant_type env typ in
@@ -138,7 +143,7 @@ let build_constant_declaration env kn (def,typ,cst,ctx) =
const_body = def;
const_type = typ;
const_body_code = tps;
- const_constraints = cst }
+ const_universes = univs }
(*s Global and local constant declaration. *)
View
4 kernel/term_typing.mli
@@ -22,10 +22,10 @@ val translate_local_assum : env -> types ->
types * Univ.constraints
val infer_declaration : env -> constant_entry ->
- constant_def * constant_type * constraints * Sign.section_context option
+ constant_def * constant_type * universe_context * Sign.section_context option
val build_constant_declaration : env -> 'a ->
- constant_def * constant_type * constraints * Sign.section_context option ->
+ constant_def * constant_type * universe_context * Sign.section_context option ->
constant_body
val translate_constant : env -> constant -> constant_entry -> constant_body
View
167 kernel/typeops.ml
@@ -18,6 +18,8 @@ open Reduction
open Inductive
open Type_errors
+type constrained_unsafe_judgment = unsafe_judgment * Univ.constraints
+
let conv_leq l2r = default_conv CUMUL ~l2r
let conv_leq_vecti env v1 v2 =
@@ -122,53 +124,14 @@ let check_hyps id env hyps =
(* Make a type polymorphic if an arity *)
-let extract_level env p =
- let _,c = dest_prod_assum env p in
- match kind_of_term c with Sort (Type u) -> Some u | _ -> None
-
-let extract_context_levels env l =
- let fold l (_, b, p) = match b with
- | None -> extract_level env p :: l
- | _ -> l
- in
- List.fold_left fold [] l
-
-let make_polymorphic env {uj_val = c; uj_type = t} =
- let params, ccl = dest_prod_assum env t in
- match kind_of_term ccl with
- | Sort (Type u) ->
- let param_ccls = extract_context_levels env params in
- let s = { poly_param_levels = param_ccls; poly_level = u} in
- PolymorphicArity (params,s)
- | _ ->
- NonPolymorphicType t
-
(* Type of constants *)
-let type_of_constant_knowing_parameters env t paramtyps =
- match t with
- | NonPolymorphicType t -> t
- | PolymorphicArity (sign,ar) ->
- let ctx = List.rev sign in
- let ctx,s = instantiate_universes env ctx ar paramtyps in
- mkArity (List.rev ctx,s)
-
-let type_of_constant_type env t =
- type_of_constant_knowing_parameters env t [||]
-
-let type_of_constant env cst =
- type_of_constant_type env (constant_type env cst)
-
-let judge_of_constant_knowing_parameters env cst jl =
- let c = mkConst cst in
- let cb = lookup_constant cst env in
- let _ = check_args env c cb.const_hyps in
- let paramstyp = Array.map (fun j -> j.uj_type) jl in
- let t = type_of_constant_knowing_parameters env cb.const_type paramstyp in
- make_judge c t
+let type_of_constant env cst = constant_type env cst
let judge_of_constant env cst =
- judge_of_constant_knowing_parameters env cst [||]
+ let c = mkConstU cst in
+ let ty, cu = type_of_constant env cst in
+ make_judge c ty, cu
(* Type of a lambda-abstraction. *)
@@ -205,8 +168,8 @@ let judge_of_apply env funj argjv =
| Prod (_,c1,c2) ->
(try
let c = conv_leq false env hj.uj_type c1 in
- let cst' = union_constraints cst c in
- apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl
+ let ctx' = union_constraints cst c in
+ apply_rec (n+1) (subst1 hj.uj_val c2) ctx' restjl
with NotConvertible ->
error_cant_apply_bad_type env
(n,c1, hj.uj_type)
@@ -283,7 +246,7 @@ let judge_of_cast env cj k tj =
conv_leq true env cj.uj_type expected_type in
{ uj_val = c;
uj_type = expected_type },
- cst
+ cst
with NotConvertible ->
error_actual_type env cj expected_type
@@ -301,27 +264,32 @@ let judge_of_cast env cj k tj =
the App case of execute; from this constraints, the expected
dynamic constraints of the form u<=v are enforced *)
-let judge_of_inductive_knowing_parameters env ind jl =
- let c = mkInd ind in
- let (mib,mip) = lookup_mind_specif env ind in
- check_args env c mib.mind_hyps;
- let paramstyp = Array.map (fun j -> j.uj_type) jl in
- let t = Inductive.type_of_inductive_knowing_parameters env mip paramstyp in
- make_judge c t
+(* let judge_of_inductive_knowing_parameters env ind jl = *)
+(* let c = mkInd ind in *)
+(* let (mib,mip) = lookup_mind_specif env ind in *)
+(* check_args env c mib.mind_hyps; *)
+(* let paramstyp = Array.map (fun j -> j.uj_type) jl in *)
+(* let t = in *)
+(* make_judge c t *)
let judge_of_inductive env ind =
- judge_of_inductive_knowing_parameters env ind [||]
+ let c = mkIndU ind in
+ let (mib,mip) = lookup_mind_specif env (fst ind) in
+ let t,u = Inductive.type_of_inductive env ((mib,mip),snd ind) in
+ make_judge c t, u
+
(* Constructors. *)
let judge_of_constructor env c =
- let constr = mkConstruct c in
+ let constr = mkConstructU c in
let _ =
- let ((kn,_),_) = c in
+ let (((kn,_),_),_) = c in
let mib = lookup_mind kn env in
check_args env constr mib.mind_hyps in
- let specif = lookup_mind_specif env (inductive_of_constructor c) in
- make_judge constr (type_of_constructor c specif)
+ let specif = lookup_mind_specif env (inductive_of_constructor (fst c)) in
+ let t,u = type_of_constructor c specif in
+ make_judge constr t, u
(* Case. *)
@@ -334,17 +302,17 @@ let check_branch_types env ind cj (lfj,explft) =
error_number_branches env cj (Array.length explft)
let judge_of_case env ci pj cj lfj =
- let indspec =
+ let ((ind, u), _ as indspec) =
try find_rectype env cj.uj_type
with Not_found -> error_case_not_inductive env cj in
- let _ = check_case_info env (fst indspec) ci in
+ let _ = check_case_info env ind ci in
let (bty,rslty,univ) =
type_case_branches env indspec pj cj.uj_val in
- let univ' = check_branch_types env (fst indspec) cj (lfj,bty) in
+ let univ' = check_branch_types env ind cj (lfj,bty) in
({ uj_val = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val,
Array.map j_val lfj);
uj_type = rslty },
- union_constraints univ univ')
+ (union_constraints univ univ'))
(* Fixpoints. *)
@@ -365,8 +333,11 @@ let type_fixpoint env lna lar vdefj =
(* This combinator adds the universe constraints both in the local
graph and in the universes of the environment. This is to ensure
that the infered local graph is satisfiable. *)
-let univ_combinator (cst,univ) (j,c') =
- (j,(union_constraints cst c', merge_constraints c' univ))
+let univ_combinator (ctx,univ) (j,ctx') =
+ (j,(union_universe_context_set ctx ctx', merge_constraints (snd ctx') univ))
+
+let univ_combinator_cst (ctx,univ) (j,cst) =
+ (j,(union_universe_context_set ctx (empty_universe_set, cst), merge_constraints cst univ))
(* The typing machine. *)
(* ATTENTION : faudra faire le typage du contexte des Const,
@@ -388,24 +359,24 @@ let rec execute env cstr cu =
(judge_of_variable env id, cu)
| Const c ->
- (judge_of_constant env c, cu)
+ univ_combinator_cst cu (judge_of_constant env c)
(* Lambda calculus operators *)
| App (f,args) ->
let (jl,cu1) = execute_array env args cu in
let (j,cu2) =
- match kind_of_term f with
- | Ind ind ->
- (* Sort-polymorphism of inductive types *)
- judge_of_inductive_knowing_parameters env ind jl, cu1
- | Const cst ->
- (* Sort-polymorphism of constant *)
- judge_of_constant_knowing_parameters env cst jl, cu1
- | _ ->
- (* No sort-polymorphism *)
+ (* match kind_of_term f with *)
+ (* | Ind ind -> *)
+ (* (\* Sort-polymorphism of inductive types *\) *)
+ (* judge_of_inductive_knowing_parameters env ind jl, cu1 *)
+ (* | Const cst -> *)
+ (* (\* Sort-polymorphism of constant *\) *)
+ (* judge_of_constant_knowing_parameters env cst jl, cu1 *)
+ (* | _ -> *)
+ (* (\* No sort-polymorphism *\) *)
execute env f cu1
in
- univ_combinator cu2 (judge_of_apply env j jl)
+ univ_combinator_cst cu2 (judge_of_apply env j jl)
| Lambda (name,c1,c2) ->