Permalink
Browse files

- Fix bug preventing apply from unfolding Fixpoints.

- Remove Universe Polymorphism flags everywhere.
- Properly infer, discharge template arities and fix substitution inside them
(kernel code to check for correctness).
- Fix tactics that were supposing universe polymorphic constants/inductives to
be parametric on that status. Required to make interp_constr* return the whole evar
universe context now.
- Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing,
sadly losing most of its benefits.
Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting
all serialization code.

Conflicts:
	kernel/univ.ml
	tactics/tactics.ml
	theories/Logic/EqdepFacts.v
  • Loading branch information...
1 parent 62fb849 commit 1ed00e4f8cded2a2024b66c3f7f4deee6ecd7c83 @mattam82 mattam82 committed Nov 8, 2013
Showing with 525 additions and 358 deletions.
  1. +1 −1 checker/mod_checking.ml
  2. +1 −0 dev/include
  3. +2 −1 dev/top_printers.ml
  4. +5 −4 interp/constrintern.mli
  5. +4 −2 kernel/declareops.ml
  6. +1 −1 kernel/entries.mli
  7. +26 −18 kernel/environ.ml
  8. +8 −4 kernel/environ.mli
  9. +2 −2 kernel/fast_typeops.ml
  10. +90 −29 kernel/indtypes.ml
  11. +2 −2 kernel/opaqueproof.ml
  12. +4 −4 kernel/opaqueproof.mli
  13. +26 −20 kernel/safe_typing.ml
  14. +1 −1 kernel/safe_typing.mli
  15. +15 −8 kernel/term_typing.ml
  16. +2 −0 kernel/term_typing.mli
  17. +2 −2 kernel/typeops.ml
  18. +15 −20 kernel/univ.ml
  19. +2 −0 kernel/univ.mli
  20. +5 −4 library/declare.ml
  21. +1 −1 library/declaremods.mli
  22. +28 −8 library/global.ml
  23. +5 −1 library/global.mli
  24. +7 −7 library/library.ml
  25. +1 −1 library/library.mli
  26. +4 −5 library/universes.ml
  27. +3 −0 library/universes.mli
  28. +1 −1 plugins/cc/cctac.ml
  29. +2 −2 plugins/funind/functional_principles_types.ml
  30. +1 −1 plugins/funind/invfun.ml
  31. +1 −1 plugins/funind/recdef.ml
  32. +9 −4 plugins/romega/const_omega.ml
  33. +0 −40 plugins/setoid_ring/Field_theory.v
  34. +19 −10 pretyping/evd.ml
  35. +3 −1 pretyping/evd.mli
  36. +1 −1 pretyping/pretyping.ml
  37. +1 −1 pretyping/pretyping.mli
  38. +3 −0 pretyping/reductionops.ml
  39. +2 −2 pretyping/termops.ml
  40. +1 −1 pretyping/termops.mli
  41. +2 −2 pretyping/typing.ml
  42. +1 −1 pretyping/unification.ml
  43. +14 −1 printing/prettyp.ml
  44. +12 −3 proofs/logic.ml
  45. +3 −2 proofs/pfedit.ml
  46. +2 −1 proofs/pfedit.mli
  47. +5 −4 proofs/proof_global.ml
  48. +4 −4 stm/lemmas.ml
  49. +2 −2 stm/stm.ml
  50. +11 −5 tactics/auto.ml
  51. +1 −1 tactics/eauto.ml4
  52. +19 −10 tactics/equality.ml
  53. +6 −3 tactics/extratactics.ml4
  54. +4 −5 tactics/leminv.ml
  55. +54 −35 tactics/rewrite.ml
  56. +10 −0 tactics/rewrite.mli
  57. +1 −1 tactics/tacinterp.ml
  58. +6 −4 tactics/tactics.ml
  59. +1 −1 theories/Classes/RelationPairs.v
  60. +2 −2 theories/Init/Datatypes.v
  61. +6 −6 theories/Init/Specif.v
  62. +2 −2 theories/Lists/List.v
  63. +1 −1 theories/Lists/SetoidList.v
  64. +1 −1 theories/Lists/SetoidPermutation.v
  65. +1 −1 theories/Logic/ChoiceFacts.v
  66. +1 −1 theories/Logic/EqdepFacts.v
  67. +1 −1 theories/Logic/Eqdep_dec.v
  68. +1 −1 theories/MSets/MSetRBT.v
  69. +1 −1 theories/Program/Basics.v
  70. +1 −1 theories/Sorting/Permutation.v
  71. +1 −1 theories/Sorting/Sorted.v
  72. +1 −1 theories/Vectors/VectorDef.v
  73. +3 −3 toplevel/auto_ind_decl.ml
  74. +3 −3 toplevel/classes.ml
  75. +16 −15 toplevel/command.ml
  76. +4 −10 toplevel/discharge.ml
  77. +1 −1 toplevel/ind_tables.ml
  78. +2 −2 toplevel/indschemes.ml
  79. +7 −5 toplevel/obligations.ml
  80. +1 −1 toplevel/record.ml
  81. +3 −2 toplevel/vernacentries.ml
View
@@ -28,7 +28,7 @@ let check_constant_declaration env kn cb =
(* let env = add_constraints cb.const_constraints env in*)
(match cb.const_type with
ty ->
- let env' = add_constraints (Future.force cb.const_constraints) env in
+ let env' = add_constraints cb.const_constraints env in (*MS: FIXME*)
let _ = infer_type env' ty in
(match body_of_constant cb with
| Some bd ->
View
@@ -35,6 +35,7 @@
#install_printer (* constraints *) ppconstraints;;
#install_printer (* univ constraints *) ppuniverseconstraints;;
#install_printer (* universe *) ppuni;;
+#install_printer (* universes *) ppuniverse;;
#install_printer (* universes *) ppuniverses;;
#install_printer (* univ level *) ppuni_level;;
#install_printer (* univ context *) ppuniverse_context;;
View
@@ -179,7 +179,7 @@ let pppftreestate p = pp(print_pftreestate p)
let ppuni u = pp(pr_uni u)
let ppuni_level u = pp (Level.pr u)
-let ppuniverses u = pp (str"[" ++ Universe.pr u ++ str"]")
+let ppuniverse u = pp (str"[" ++ Universe.pr u ++ str"]")
let ppuniverse_set l = pp (LSet.pr l)
let ppuniverse_instance l = pp (Instance.pr l)
@@ -195,6 +195,7 @@ let ppuniverseconstraints c = pp (UniverseConstraints.pr c)
let ppuniverse_context_future c =
let ctx = Future.force c in
ppuniverse_context ctx
+let ppuniverses u = pp (Univ.pr_universes u)
let ppenv e = pp
(str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++
View
@@ -91,13 +91,13 @@ val intern_context : bool -> env -> internalization_env -> local_binder list ->
(** Main interpretation functions expecting evars to be all resolved *)
val interp_constr : evar_map -> env -> ?impls:internalization_env ->
- constr_expr -> constr Univ.in_universe_context_set
+ constr_expr -> constr Evd.in_evar_universe_context
val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
- constr_expr -> types -> constr Univ.in_universe_context_set
+ constr_expr -> types -> constr Evd.in_evar_universe_context
val interp_type : evar_map -> env -> ?impls:internalization_env ->
- constr_expr -> types Univ.in_universe_context_set
+ constr_expr -> types Evd.in_evar_universe_context
(** Main interpretation function expecting evars to be all resolved *)
@@ -142,7 +142,8 @@ val interp_reference : ltac_sign -> reference -> glob_constr
(** Interpret binders *)
-val interp_binder : evar_map -> env -> Name.t -> constr_expr -> types Univ.in_universe_context_set
+val interp_binder : evar_map -> env -> Name.t -> constr_expr ->
+ types Evd.in_evar_universe_context
val interp_binder_evars : evar_map ref -> env -> Name.t -> constr_expr -> types
View
@@ -47,12 +47,14 @@ let constraints_of_constant cb = Univ.Constraint.union
(match cb.const_body with
| Undef _ -> Univ.empty_constraint
| Def c -> Univ.empty_constraint
- | OpaqueDef o -> Univ.UContext.constraints (Opaqueproof.force_constraints o))
+ | OpaqueDef o -> Univ.ContextSet.constraints (Opaqueproof.force_constraints o))
let universes_of_constant cb =
match cb.const_body with
| Undef _ | Def _ -> cb.const_universes
- | OpaqueDef o -> Opaqueproof.force_constraints o
+ | OpaqueDef o ->
+ Univ.UContext.union cb.const_universes
+ (Univ.ContextSet.to_context (Opaqueproof.force_constraints o))
let universes_of_polymorphic_constant cb =
if cb.const_polymorphic then universes_of_constant cb
View
@@ -50,7 +50,7 @@ type mutual_inductive_entry = {
mind_entry_private : bool option }
(** {6 Constants (Definition/Axiom) } *)
-type proof_output = constr * Declareops.side_effects
+type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects
type const_entry_body = proof_output Future.computation
type projection = mutual_inductive * int * int * types
View
@@ -311,17 +311,21 @@ let evaluable_constant kn env =
| OpaqueDef _ -> false
| Undef _ -> false
-let template_polymorphic_constant (cst,u) env =
- if not (Univ.Instance.is_empty u) then false
- else
- match (lookup_constant cst env).const_type with
- | TemplateArity _ -> true
- | RegularArity _ -> false
+let polymorphic_constant cst env =
+ (lookup_constant cst env).const_polymorphic
-let polymorphic_constant (cst,u) env =
+let polymorphic_pconstant (cst,u) env =
if Univ.Instance.is_empty u then false
- else
- (lookup_constant cst env).const_polymorphic
+ else polymorphic_constant cst env
+
+let template_polymorphic_constant cst env =
+ match (lookup_constant cst env).const_type with
+ | TemplateArity _ -> true
+ | RegularArity _ -> false
+
+let template_polymorphic_pconstant (cst,u) env =
+ if not (Univ.Instance.is_empty u) then false
+ else template_polymorphic_constant cst env
let lookup_projection cst env =
match (lookup_constant cst env).const_proj with
@@ -336,17 +340,21 @@ let is_projection cst env =
(* Mutual Inductives *)
let lookup_mind = lookup_mind
-let template_polymorphic_ind ((mind,i),u) env =
- if not (Univ.Instance.is_empty u) then false
- else
- match (lookup_mind mind env).mind_packets.(i).mind_arity with
- | TemplateArity _ -> true
- | RegularArity _ -> false
+let polymorphic_ind (mind,i) env =
+ (lookup_mind mind env).mind_polymorphic
-let polymorphic_ind ((mind,i),u) env =
+let polymorphic_pind (ind,u) env =
if Univ.Instance.is_empty u then false
- else
- (lookup_mind mind env).mind_polymorphic
+ else polymorphic_ind ind env
+
+let template_polymorphic_ind (mind,i) env =
+ match (lookup_mind mind env).mind_packets.(i).mind_arity with
+ | TemplateArity _ -> true
+ | RegularArity _ -> false
+
+let template_polymorphic_pind (ind,u) env =
+ if not (Univ.Instance.is_empty u) then false
+ else template_polymorphic_ind ind env
let add_mind_key kn mind_key env =
let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
View
@@ -128,10 +128,12 @@ val lookup_constant : constant -> env -> constant_body
val evaluable_constant : constant -> env -> bool
(** New-style polymorphism *)
-val polymorphic_constant : pconstant -> env -> bool
+val polymorphic_constant : constant -> env -> bool
+val polymorphic_pconstant : pconstant -> env -> bool
(** Old-style polymorphism *)
-val template_polymorphic_constant : pconstant -> env -> bool
+val template_polymorphic_constant : constant -> env -> bool
+val template_polymorphic_pconstant : pconstant -> env -> bool
(** {6 ... } *)
(** [constant_value env c] raises [NotEvaluableConst Opaque] if
@@ -173,10 +175,12 @@ val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
(** New-style polymorphism *)
-val polymorphic_ind : pinductive -> env -> bool
+val polymorphic_ind : inductive -> env -> bool
+val polymorphic_pind : pinductive -> env -> bool
(** Old-style polymorphism *)
-val template_polymorphic_ind : pinductive -> env -> bool
+val template_polymorphic_ind : inductive -> env -> bool
+val template_polymorphic_pind : pinductive -> env -> bool
(** {5 Modules } *)
View
@@ -384,11 +384,11 @@ let rec execute env cstr =
let argst = execute_array env args in
let ft =
match kind_of_term f with
- | Ind ind when Environ.template_polymorphic_ind ind env ->
+ | Ind ind when Environ.template_polymorphic_pind ind env ->
(* Template sort-polymorphism of inductive types *)
let args = Array.map (fun t -> lazy t) argst in
judge_of_inductive_knowing_parameters env ind args
- | Const cst when Environ.template_polymorphic_constant cst env ->
+ | Const cst when Environ.template_polymorphic_pconstant cst env ->
(* Template sort-polymorphism of constants *)
let args = Array.map (fun t -> lazy t) argst in
judge_of_constant_knowing_parameters env cst args
View
@@ -193,6 +193,34 @@ let cumulate_arity_large_levels env sign =
let is_impredicative env u =
is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
+let param_ccls params =
+ let has_some_univ u = function
+ | Some v when Universe.equal u v -> true
+ | _ -> false
+ in
+ let remove_some_univ u = function
+ | Some v when Universe.equal u v -> None
+ | x -> x
+ in
+ let fold l (_, b, p) = match b with
+ | None ->
+ (* Parameter contributes to polymorphism only if explicit Type *)
+ let c = strip_prod_assum p in
+ (* Add Type levels to the ordered list of parameters contributing to *)
+ (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
+ begin match kind_of_term c with
+ | Sort (Type u) ->
+ if List.exists (has_some_univ u) l then
+ None :: List.map (remove_some_univ u) l
+ else
+ Some u :: l
+ | _ ->
+ None :: l
+ end
+ | _ -> l
+ in
+ List.fold_left fold [] params
+
(* Type-check an inductive definition. Does not check positivity
conditions. *)
(* TODO check that we don't overgeneralize construcors/inductive arities with
@@ -215,7 +243,7 @@ let typecheck_inductive env ctx mie =
List.fold_left
(fun (env_ar,l) ind ->
(* Arities (without params) are typed-checked here *)
- let arity =
+ let arity, expltype =
if isArity ind.mind_entry_arity then
let (ctx,s) = destArity ind.mind_entry_arity in
match s with
@@ -226,11 +254,12 @@ let typecheck_inductive env ctx mie =
let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in
let (cctx, _) = destArity proparity.utj_val in
(* Any universe is well-formed, we don't need to check [s] here *)
- mkArity (cctx, s)
- | _ -> let arity = infer_type env_params ind.mind_entry_arity in
- arity.utj_val
+ mkArity (cctx, s), not (Sorts.is_small s)
+ | _ ->
+ let arity = infer_type env_params ind.mind_entry_arity in
+ arity.utj_val, not (Sorts.is_small s)
else let arity = infer_type env_params ind.mind_entry_arity in
- arity.utj_val
+ arity.utj_val, false
in
let (sign, deflev) = dest_arity env_params arity in
let inflev =
@@ -249,7 +278,7 @@ let typecheck_inductive env ctx mie =
let env_ar' =
push_rel (Name id, None, full_arity) env_ar in
(* (add_constraints cst2 env_ar) in *)
- (env_ar', (id,full_arity,sign @ params,deflev,inflev)::l))
+ (env_ar', (id,full_arity,sign @ params,expltype,deflev,inflev)::l))
(env',[])
mie.mind_entry_inds in
@@ -277,30 +306,60 @@ let typecheck_inductive env ctx mie =
(* Compute/check the sorts of the inductive types *)
let inds =
- Array.map (fun ((id,full_arity,sign,def_level,inf_level),cn,lc,(is_unit,clev)) ->
- let defu = Term.univ_of_sort def_level in
- let infu =
- (** Inferred level, with parameters and constructors. *)
- match inf_level with
- | Some alev -> Universe.sup clev alev
- | None -> clev
+ Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,(is_unit,clev)) ->
+ let full_polymorphic () =
+ let defu = Term.univ_of_sort def_level in
+ let infu =
+ (** Inferred level, with parameters and constructors. *)
+ match inf_level with
+ | Some alev -> Universe.sup clev alev
+ | None -> clev
+ in
+ let is_natural =
+ check_leq (universes env') infu defu &&
+ not (is_type0m_univ defu && not is_unit)
+ in
+ let _ =
+ (** Impredicative sort, always allow *)
+ if is_impredicative env defu then ()
+ else (** Predicative case: the inferred level must be lower or equal to the
+ declared level. *)
+ if not is_natural then
+ anomaly ~label:"check_inductive"
+ (Pp.str"Incorrect universe " ++
+ Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is "
+ ++ Universe.pr infu)
+ in
+ RegularArity (not is_natural,full_arity,defu)
in
- let is_natural =
- check_leq (universes env') infu defu &&
- not (is_type0m_univ defu && not is_unit)
+ let template_polymorphic () =
+ let sign, s =
+ try dest_arity env full_arity
+ with NotArity -> raise (InductiveError (NotAnArity (env, full_arity)))
+ in
+ match s with
+ | Type u when expltype (* Explicitly polymorphic *) ->
+ (* && no_upper_constraints u (Univ.UContext.constraints mie.mind_entry_universes) -> *)
+ (* The polymorphic level is a function of the level of the *)
+ (* conclusions of the parameters *)
+ (* We enforce [u >= lev] in case [lev] has a strict upper *)
+ (* constraints over [u] *)
+ let b = check_leq (universes env') clev u in
+ if not b then
+ anomaly ~label:"check_inductive"
+ (Pp.str"Incorrect universe " ++
+ Universe.pr u ++ Pp.str " declared for inductive type, inferred level is "
+ ++ Universe.pr clev)
+ else
+ TemplateArity (param_ccls params, clev)
+ | _ (* Not an explicit occurrence of Type *) ->
+ full_polymorphic ()
in
- let _ =
- (** Impredicative sort, always allow *)
- if is_impredicative env defu then ()
- else (** Predicative case: the inferred level must be lower or equal to the
- declared level. *)
- if not is_natural then
- anomaly ~label:"check_inductive"
- (Pp.str"Incorrect universe " ++
- Universe.pr defu ++ Pp.str " declared for inductive type, inferred level is "
- ++ Universe.pr infu)
+ let arity =
+ if mie.mind_entry_polymorphic then full_polymorphic ()
+ else template_polymorphic ()
in
- (id,cn,lc,(sign,RegularArity (not is_natural,full_arity,defu))))
+ (id,cn,lc,(sign,arity)))
inds
in (env_arities, params, inds)
@@ -617,7 +676,7 @@ let allowed_sorts is_smashed s =
let arity_conclusion = function
| RegularArity (_, c, _) -> c
- | TemplateArity s -> mkType s.template_level
+ | TemplateArity (_, s) -> mkType s
let fold_inductive_blocks f =
Array.fold_left (fun acc (_,_,lc,(arsign,ar)) ->
@@ -681,7 +740,9 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
(* Elimination sorts *)
let arkind,kelim =
match ar_kind with
- | TemplateArity ar -> TemplateArity ar, all_sorts
+ | TemplateArity (paramlevs, lev) ->
+ let ar = {template_param_levels = paramlevs; template_level = lev} in
+ TemplateArity ar, all_sorts
| RegularArity (info,ar,defs) ->
let s = sort_of_univ defs in
let kelim = allowed_sorts info s in
View
@@ -17,7 +17,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
abstract : Context.named_context in_universe_context }
-type proofterm = (constr * Univ.universe_context) Future.computation
+type proofterm = (constr * Univ.universe_context_set) Future.computation
type opaque =
| Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
| Direct of cooking_info list * proofterm
@@ -99,7 +99,7 @@ let force_constraints = function
| NoIndirect(_,cu) -> snd(Future.force cu)
| Indirect (_,dp,i) ->
match !get_univ dp i with
- | None -> Univ.UContext.empty
+ | None -> Univ.ContextSet.empty
| Some u -> Future.force u
let get_constraints = function
Oops, something went wrong.

0 comments on commit 1ed00e4

Please sign in to comment.