aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.mllib1
-rw-r--r--checker/cic.mli21
-rw-r--r--checker/closure.ml3
-rw-r--r--checker/environ.ml14
-rw-r--r--checker/environ.mli1
-rw-r--r--checker/indtypes.ml10
-rw-r--r--checker/inductive.ml14
-rw-r--r--checker/mod_checking.ml27
-rw-r--r--checker/print.ml4
-rw-r--r--checker/reduction.ml41
-rw-r--r--checker/subtyping.ml106
-rw-r--r--checker/term.ml20
-rw-r--r--checker/typeops.ml16
-rw-r--r--checker/univ.ml42
-rw-r--r--checker/univ.mli2
-rw-r--r--checker/values.ml19
16 files changed, 94 insertions, 247 deletions
diff --git a/checker/check.mllib b/checker/check.mllib
index f79ba66e35..139fa765b4 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -3,7 +3,6 @@ Coq_config
Analyze
Hook
Terminal
-Canary
Hashset
Hashcons
CSet
diff --git a/checker/cic.mli b/checker/cic.mli
index 7ec3457686..4846a9af8c 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -33,11 +33,10 @@ open Names
(** {6 The sorts of CCI. } *)
-type contents = Pos | Null
-
type sorts =
- | Prop of contents (** Prop and Set *)
- | Type of Univ.universe (** Type *)
+ | Prop
+ | Set
+ | Type of Univ.universe
(** {6 The sorts family of CCI. } *)
@@ -207,12 +206,10 @@ type inline = int option
always transparent. *)
type projection_body = {
- proj_ind : MutInd.t;
+ proj_ind : inductive;
proj_npars : int;
proj_arg : int;
proj_type : constr; (* Type under params *)
- proj_eta : constr * constr; (* Eta-expanded term and type *)
- proj_body : constr; (* For compatibility, the match version *)
}
type constant_def =
@@ -241,7 +238,6 @@ type constant_body = {
const_type : constr;
const_body_code : to_patch_substituted;
const_universes : constant_universes;
- const_proj : bool;
const_inline_code : bool;
const_typing_flags : typing_flags;
}
@@ -255,9 +251,10 @@ type recarg =
type wf_paths = recarg Rtree.t
-type record_body = (Id.t * Constant.t array * projection_body array) option
- (* The body is empty for non-primitive records, otherwise we get its
- binder name in projections and list of projections if it is primitive. *)
+type record_info =
+| NotRecord
+| FakeRecord
+| PrimRecord of (Id.t * Constant.t array * projection_body array) array
type regular_inductive_arity = {
mind_user_arity : constr;
@@ -325,7 +322,7 @@ type mutual_inductive_body = {
mind_packets : one_inductive_body array; (** The component of the mutual inductive block *)
- mind_record : record_body option; (** Whether the inductive type has been declared as a record. *)
+ mind_record : record_info; (** Whether the inductive type has been declared as a record. *)
mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *)
diff --git a/checker/closure.ml b/checker/closure.ml
index b9ae4daa86..2dcc1a9840 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -619,7 +619,8 @@ let drop_parameters depth n argstk =
let eta_expand_ind_stack env ind m s (f, s') =
let mib = lookup_mind (fst ind) env in
match mib.mind_record with
- | Some (Some (_,projs,pbs)) when mib.mind_finite <> CoFinite ->
+ | PrimRecord info when mib.mind_finite <> CoFinite ->
+ let (_, projs, pbs) = info.(snd ind) in
(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
let pars = mib.mind_nparams in
diff --git a/checker/environ.ml b/checker/environ.ml
index 809150cea9..ba1eb0ddb4 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -166,9 +166,6 @@ let evaluable_constant cst env =
try let _ = constant_value env (cst, Univ.Instance.empty) in true
with Not_found | NotEvaluableConst _ -> false
-let is_projection cst env =
- (lookup_constant cst env).const_proj
-
let lookup_projection p env =
Cmap_env.find (Projection.constant p) env.env_globals.env_projections
@@ -195,11 +192,12 @@ let add_mind kn mib env =
(MutInd.to_string kn);
let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
let new_projections = match mib.mind_record with
- | None | Some None -> env.env_globals.env_projections
- | Some (Some (id, kns, pbs)) ->
- Array.fold_left2 (fun projs kn pb ->
- Cmap_env.add kn pb projs)
- env.env_globals.env_projections kns pbs
+ | NotRecord | FakeRecord -> env.env_globals.env_projections
+ | PrimRecord projs ->
+ Array.fold_left (fun accu (id, kns, pbs) ->
+ Array.fold_left2 (fun accu kn pb ->
+ Cmap_env.add kn pb accu) accu kns pbs)
+ env.env_globals.env_projections projs
in
let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in
let new_inds_eq = if KerName.equal kn1 kn2 then
diff --git a/checker/environ.mli b/checker/environ.mli
index 4a7597249d..acb29d7d2d 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -58,7 +58,6 @@ exception NotEvaluableConst of const_evaluation_result
val constant_value : env -> Constant.t puniverses -> constr
val evaluable_constant : Constant.t -> env -> bool
-val is_projection : Constant.t -> env -> bool
val lookup_projection : Projection.t -> env -> projection_body
(* Inductives *)
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 916934a81f..bcb71fe55f 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -107,11 +107,11 @@ let rec sorts_of_constr_args env t =
(* Prop and Set are small *)
let is_small_sort = function
- | Prop _ -> true
+ | Prop | Set -> true
| _ -> false
let is_logic_sort = function
-| Prop Null -> true
+| Prop -> true
| _ -> false
(* [infos] is a sequence of pair [islogic,issmall] for each type in
@@ -186,10 +186,10 @@ let check_predicativity env s small level =
(* (universes env) in *)
if not (Univ.check_leq (universes env) level u) then
failwith "impredicative Type inductive type"
- | Prop Pos, ImpredicativeSet -> ()
- | Prop Pos, _ ->
+ | Set, ImpredicativeSet -> ()
+ | Set, _ ->
if not small then failwith "impredicative Set inductive type"
- | Prop Null,_ -> ()
+ | Prop,_ -> ()
let sort_of_ind = function
diff --git a/checker/inductive.ml b/checker/inductive.ml
index e1c6b135d7..b1edec5568 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -101,7 +101,7 @@ let instantiate_params full t u args sign =
substl subs ty
let full_inductive_instantiate mib u params sign =
- let dummy = Prop Null in
+ let dummy = Prop in
let t = mkArity (Term.subst_instance_context u sign,dummy) in
fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
@@ -137,8 +137,8 @@ Remark: Set (predicative) is encoded as Type(0)
let sort_as_univ = function
| Type u -> u
-| Prop Null -> Univ.type0m_univ
-| Prop Pos -> Univ.type0_univ
+| Prop -> Univ.type0m_univ
+| Set -> Univ.type0_univ
(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
(* in the domain or add [u |-> sup x su] if [u] is already mapped *)
@@ -195,9 +195,9 @@ let instantiate_universes env ctx ar argsorts =
let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
let ty =
(* Singleton type not containing types are interpretable in Prop *)
- if Univ.is_type0m_univ level then Prop Null
+ if Univ.is_type0m_univ level then Prop
(* Non singleton type not containing types are interpretable in Set *)
- else if Univ.is_type0_univ level then Prop Pos
+ else if Univ.is_type0_univ level then Set
(* This is a Type with constraints *)
else Type level
in
@@ -226,8 +226,8 @@ let type_of_inductive env mip =
(* The max of an array of universes *)
let cumulate_constructor_univ u = function
- | Prop Null -> u
- | Prop Pos -> Univ.sup Univ.type0_univ u
+ | Prop -> u
+ | Set -> Univ.sup Univ.type0_univ u
| Type u' -> Univ.sup u u'
let max_inductive_sort =
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ca9581167f..6b2af71f33 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -2,7 +2,6 @@ open Pp
open Util
open Names
open Cic
-open Term
open Reduction
open Typeops
open Indtypes
@@ -13,17 +12,6 @@ open Environ
(** {6 Checking constants } *)
-let refresh_arity ar =
- let ctxt, hd = decompose_prod_assum ar in
- match hd with
- Sort (Type u) when not (Univ.is_univ_variable u) ->
- let ul = Univ.Level.make DirPath.empty 1 in
- let u' = Univ.Universe.make ul in
- let cst = Univ.enforce_leq u u' Univ.empty_constraint in
- let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
- mkArity (ctxt,Prop Null), ctx
- | _ -> ar, Univ.ContextSet.empty
-
let check_constant_declaration env kn cb =
Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn);
(** Locally set the oracle for further typechecking *)
@@ -37,18 +25,13 @@ let check_constant_declaration env kn cb =
let ctx = Univ.AUContext.repr auctx in
push_context ~strict:false ctx env
in
- let envty, ty =
- let ty = cb.const_type in
- let ty', cu = refresh_arity ty in
- let envty = push_context_set cu env' in
- let _ = infer_type envty ty' in
- envty, ty
- in
- let () =
+ let ty = cb.const_type in
+ let _ = infer_type env' ty in
+ let () =
match body_of_constant cb with
| Some bd ->
- let j = infer envty bd in
- conv_leq envty j ty
+ let j = infer env' bd in
+ conv_leq env' j ty
| None -> ()
in
let env =
diff --git a/checker/print.ml b/checker/print.ml
index fc9cd687e8..247c811f80 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -57,8 +57,8 @@ let print_pure_constr fmt csr =
fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c
and pp_sort fmt = function
- | Prop(Pos) -> pp_print_string fmt "Set"
- | Prop(Null) -> pp_print_string fmt "Prop"
+ | Set -> pp_print_string fmt "Set"
+ | Prop -> pp_print_string fmt "Prop"
| Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u)
and pp_name fmt = function
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 4e508dc772..16c7012138 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -210,29 +210,26 @@ let convert_constructors
let sort_cmp env univ pb s0 s1 =
match (s0,s1) with
- | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
- | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
- | (Prop c1, Type u) ->
+ | Prop, Prop | Set, Set -> ()
+ | Prop, (Set | Type _) | Set, Type _ ->
+ if not (pb = CUMUL) then raise NotConvertible
+ | Type u1, Type u2 ->
+ (** FIXME: handle type-in-type option here *)
+ if (* snd (engagement env) == StratifiedType && *)
+ not
(match pb with
- CUMUL -> ()
- | _ -> raise NotConvertible)
- | (Type u1, Type u2) ->
- (** FIXME: handle type-in-type option here *)
- if (* snd (engagement env) == StratifiedType && *)
- not
- (match pb with
- | CONV -> Univ.check_eq univ u1 u2
- | CUMUL -> Univ.check_leq univ u1 u2)
- then begin
- if !Flags.debug then begin
- let op = match pb with CONV -> "=" | CUMUL -> "<=" in
- Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
- str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
- ++ Univ.pr_universes univ)
- end;
- raise NotConvertible
- end
- | (_, _) -> raise NotConvertible
+ | CONV -> Univ.check_eq univ u1 u2
+ | CUMUL -> Univ.check_leq univ u1 u2)
+ then begin
+ if !Flags.debug then begin
+ let op = match pb with CONV -> "=" | CUMUL -> "<=" in
+ Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.(
+ str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
+ ++ Univ.pr_universes univ)
+ end;
+ raise NotConvertible
+ end
+ | Set, Prop | Type _, (Prop | Set) -> raise NotConvertible
let rec no_arg_available = function
| [] -> true
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 5c672d04a6..6d0d6f6c6d 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -9,7 +9,6 @@
(************************************************************************)
(*i*)
-open CErrors
open Util
open Names
open Cic
@@ -126,48 +125,13 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
in
let eq_projection_body p1 p2 =
let check eq f = if not (eq (f p1) (f p2)) then error () in
- check MutInd.equal (fun x -> x.proj_ind);
+ check eq_ind (fun x -> x.proj_ind);
check (==) (fun x -> x.proj_npars);
check (==) (fun x -> x.proj_arg);
check (eq_constr) (fun x -> x.proj_type);
- check (eq_constr) (fun x -> fst x.proj_eta);
- check (eq_constr) (fun x -> snd x.proj_eta);
- check (eq_constr) (fun x -> x.proj_body); true
- in
- let check_inductive_type t1 t2 =
-
- (* Due to template polymorphism, the conclusions of
- t1 and t2, if in Type, are generated as the least upper bounds
- of the types of the constructors.
-
- By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U
- |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each
- universe in the conclusion of t1 has an bounding universe in
- the conclusion of t2, so that we don't need to check the
- subtyping of the conclusions of t1 and t2.
-
- Even if we'd like to recheck it, the inference of constraints
- is not designed to deal with algebraic constraints of the form
- max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy
- to recheck it (in short, we would need the actual graph of
- constraints as input while type checking is currently designed
- to output a set of constraints instead) *)
-
- (* So we cheat and replace the subtyping problem on algebraic
- constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n)
- (that we know are necessary true) by trivial constraints that
- the constraint generator knows how to deal with *)
-
- let (ctx1,s1) = dest_arity env t1 in
- let (ctx2,s2) = dest_arity env t2 in
- let s1,s2 =
- match s1, s2 with
- | Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null
- | (Prop _, Type _) | (Type _,Prop _) -> error ()
- | _ -> (s1, s2) in
- check_conv conv_leq env
- (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+ true
in
+ let check_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in
let check_packet p1 p2 =
let check eq f = if not (eq (f p1) (f p2)) then error () in
@@ -220,16 +184,19 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
(* we check that records and their field names are preserved. *)
let record_equal x y =
match x, y with
- | None, None -> true
- | Some None, Some None -> true
- | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) ->
- Id.equal id1 id2 &&
- Array.for_all2 Constant.UserOrd.equal p1 p2 &&
- Array.for_all2 eq_projection_body pb1 pb2
+ | NotRecord, NotRecord -> true
+ | FakeRecord, FakeRecord -> true
+ | PrimRecord info1, PrimRecord info2 ->
+ let check (id1, p1, pb1) (id2, p2, pb2) =
+ Id.equal id1 id2 &&
+ Array.for_all2 Constant.UserOrd.equal p1 p2 &&
+ Array.for_all2 eq_projection_body pb1 pb2
+ in
+ Array.equal check info1 info2
| _, _ -> false
in
check record_equal (fun mib -> mib.mind_record);
- if mib1.mind_record != None then begin
+ if mib1.mind_record != NotRecord then begin
let rec names_prod_letin t = match t with
| Prod(n,_,t) -> n::(names_prod_letin t)
| LetIn(n,_,_,t) -> n::(names_prod_letin t)
@@ -253,52 +220,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
let error () = error_not_match l spec2 in
let check_conv f = check_conv_error error f in
- let check_type env t1 t2 =
-
- (* If the type of a constant is generated, it may mention
- non-variable algebraic universes that the general conversion
- algorithm is not ready to handle. Anyway, generated types of
- constants are functions of the body of the constant. If the
- bodies are the same in environments that are subtypes one of
- the other, the types are subtypes too (i.e. if Gamma <= Gamma',
- Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
- Hence they don't have to be checked again *)
-
- let t1,t2 =
- if isArity t2 then
- let (ctx2,s2) = destArity t2 in
- match s2 with
- | Type v when not (Univ.is_univ_variable v) ->
- (* The type in the interface is inferred and is made of algebraic
- universes *)
- begin try
- let (ctx1,s1) = dest_arity env t1 in
- match s1 with
- | Type u when not (Univ.is_univ_variable u) ->
- (* Both types are inferred, no need to recheck them. We
- cheat and collapse the types to Prop *)
- mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
- | Prop _ ->
- (* The type in the interface is inferred, it may be the case
- that the type in the implementation is smaller because
- the body is more reduced. We safely collapse the upper
- type to Prop *)
- mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
- | Type _ ->
- (* The type in the interface is inferred and the type in the
- implementation is not inferred or is inferred but from a
- more reduced body so that it is just a variable. Since
- constraints of the form "univ <= max(...)" are not
- expressible in the system of algebraic universes: we fail
- (the user has to use an explicit type in the interface *)
- error ()
- with UserError _ (* "not an arity" *) ->
- error () end
- | _ -> t1,t2
- else
- (t1,t2) in
- check_conv conv_leq env t1 t2
- in
+ let check_type env t1 t2 = check_conv conv_leq env t1 t2 in
match info1 with
| Constant cb1 ->
let cb1 = subst_const_body subst1 cb1 in
diff --git a/checker/term.ml b/checker/term.ml
index 509634bdba..d84491b38f 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -20,15 +20,15 @@ open Cic
(* Sorts. *)
let family_of_sort = function
- | Prop Null -> InProp
- | Prop Pos -> InSet
+ | Prop -> InProp
+ | Set -> InSet
| Type _ -> InType
let family_equal = (==)
let sort_of_univ u =
- if Univ.is_type0m_univ u then Prop Null
- else if Univ.is_type0_univ u then Prop Pos
+ if Univ.is_type0m_univ u then Prop
+ else if Univ.is_type0_univ u then Set
else Type u
(********************************************************************)
@@ -356,15 +356,11 @@ let rec isArity c =
(* alpha conversion : ignore print names and casts *)
let compare_sorts s1 s2 = match s1, s2 with
-| Prop c1, Prop c2 ->
- begin match c1, c2 with
- | Pos, Pos | Null, Null -> true
- | Pos, Null -> false
- | Null, Pos -> false
- end
+| Prop, Prop | Set, Set -> true
| Type u1, Type u2 -> Univ.Universe.equal u1 u2
-| Prop _, Type _ -> false
-| Type _, Prop _ -> false
+| Prop, Set | Set, Prop -> false
+| (Prop | Set), Type _ -> false
+| Type _, (Prop | Set) -> false
let eq_puniverses f (c1,u1) (c2,u2) =
Univ.Instance.equal u1 u2 && f c1 c2
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 18f07dc0b7..19ede4b9a2 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -103,11 +103,11 @@ let judge_of_apply env (f,funj) argjv =
let sort_of_product env domsort rangsort =
match (domsort, rangsort) with
(* Product rule (s,Prop,Prop) *)
- | (_, Prop Null) -> rangsort
+ | _, Prop -> rangsort
(* Product rule (Prop/Set,Set,Set) *)
- | (Prop _, Prop Pos) -> rangsort
+ | (Prop | Set), Set -> rangsort
(* Product rule (Type,Set,?) *)
- | (Type u1, Prop Pos) ->
+ | Type u1, Set ->
if engagement env = ImpredicativeSet then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
@@ -115,11 +115,11 @@ let sort_of_product env domsort rangsort =
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
Type (Univ.sup u1 Univ.type0_univ)
(* Product rule (Prop,Type_i,Type_i) *)
- | (Prop Pos, Type u2) -> Type (Univ.sup Univ.type0_univ u2)
+ | Set, Type u2 -> Type (Univ.sup Univ.type0_univ u2)
(* Product rule (Prop,Type_i,Type_i) *)
- | (Prop Null, Type _) -> rangsort
+ | Prop, Type _ -> rangsort
(* Product rule (Type_i,Type_i,Type_i) *)
- | (Type u1, Type u2) -> Type (Univ.sup u1 u2)
+ | Type u1, Type u2 -> Type (Univ.sup u1 u2)
(* Type of a type cast *)
@@ -203,7 +203,7 @@ let judge_of_projection env p c ct =
try find_rectype env ct
with Not_found -> error_case_not_inductive env (c, ct)
in
- assert(MutInd.equal pb.proj_ind (fst ind));
+ assert(eq_ind pb.proj_ind ind);
let ty = subst_instance_constr u pb.proj_type in
substl (c :: List.rev args) ty
@@ -239,7 +239,7 @@ let type_fixpoint env lna lar lbody vdefj =
let rec execute env cstr =
match cstr with
(* Atomic terms *)
- | Sort (Prop _) -> judge_of_prop
+ | Sort (Prop | Set) -> judge_of_prop
| Sort (Type u) -> judge_of_type u
diff --git a/checker/univ.ml b/checker/univ.ml
index 15673736f2..e50e883adf 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -190,13 +190,6 @@ struct
(let (u,n) = x and (v,n') = y in
Int.equal n n' && Level.equal u v)
- let leq (u,n) (v,n') =
- let cmp = Level.compare u v in
- if Int.equal cmp 0 then n <= n'
- else if n <= n' then
- (Level.is_prop u && Level.is_small v)
- else false
-
let successor (u,n) =
if Level.is_prop u then type1
else (u, n + 1)
@@ -833,41 +826,6 @@ type 'a constrained = 'a * constraints
type 'a constraint_function = 'a -> 'a -> constraints -> constraints
-let constraint_add_leq v u c =
- (* We just discard trivial constraints like u<=u *)
- if Expr.equal v u then c
- else
- match v, u with
- | (x,n), (y,m) ->
- let j = m - n in
- if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
- Constraint.add (x,Lt,y) c
- else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
- if Level.equal x y then (* u+(k+1) <= u *)
- raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u))
- else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
- else if j = 0 then
- Constraint.add (x,Le,y) c
- else (* j >= 1 *) (* m = n + k, u <= v+k *)
- if Level.equal x y then c (* u <= u+k, trivial *)
- else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
- else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints.")
-
-let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
-
-let check_univ_leq u v =
- Universe.for_all (fun u -> check_univ_leq_one u v) u
-
-let enforce_leq u v c =
- match v with
- | [v] ->
- List.fold_right (fun u -> constraint_add_leq u v) u c
- | _ -> anomaly (Pp.str"A universe bound can only be a variable.")
-
-let enforce_leq u v c =
- if check_univ_leq u v then c
- else enforce_leq u v c
-
let check_constraint g (l,d,r) =
match d with
| Eq -> check_equal g l r
diff --git a/checker/univ.mli b/checker/univ.mli
index 6cd3b36382..3b29b158f2 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -109,8 +109,6 @@ type 'a constrained = 'a * constraints
type 'a constraint_function = 'a -> 'a -> constraints -> constraints
-val enforce_leq : universe constraint_function
-
(** {6 ... } *)
(** Merge of constraints in a universes graph.
The function [merge_constraints] merges a set of constraints in a given
diff --git a/checker/values.ml b/checker/values.ml
index 67032bd1b7..88cdb644db 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 fb80632357e3ffa988c6bba3fa6ade64 checker/cic.mli
+MD5 c395aa2dbfc18794b3b7192f3dc5b2e5 checker/cic.mli
*)
@@ -91,7 +91,7 @@ let rec v_mp = Sum("module_path",0,
[|[|v_dp|];
[|v_uid|];
[|v_mp;v_id|]|])
-let v_kn = v_tuple "kernel_name" [|Any;v_mp;v_dp;v_id;Int|]
+let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id;Int|]
let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|]
let v_ind = v_tuple "inductive" [|v_cst;Int|]
let v_cons = v_tuple "constructor" [|v_ind;Int|]
@@ -122,7 +122,7 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
(** kernel/term *)
-let v_sort = v_sum "sort" 0 [|[|v_enum "cnt" 2|];[|v_univ|]|]
+let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|]
let v_sortfam = v_enum "sorts_family" 3
let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
@@ -225,9 +225,7 @@ let v_cst_def =
let v_projbody =
v_tuple "projection_body"
- [|v_cst;Int;Int;v_constr;
- v_tuple "proj_eta" [|v_constr;v_constr|];
- v_constr|]
+ [|v_ind;Int;Int;v_constr|]
let v_typing_flags =
v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
@@ -241,7 +239,6 @@ let v_cb = v_tuple "constant_body"
Any;
v_const_univs;
v_bool;
- v_bool;
v_typing_flags|]
let v_recarg = v_sum "recarg" 1 (* Norec *)
@@ -277,8 +274,10 @@ let v_one_ind = v_tuple "one_inductive_body"
Any|]
let v_finite = v_enum "recursivity_kind" 3
-let v_mind_record = Annot ("mind_record",
- Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |])))
+
+let v_record_info =
+ v_sum "record_info" 2
+ [| [| Array (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]) |] |]
let v_ind_pack_univs =
v_sum "abstract_inductive_universes" 0
@@ -286,7 +285,7 @@ let v_ind_pack_univs =
let v_ind_pack = v_tuple "mutual_inductive_body"
[|Array v_one_ind;
- v_mind_record;
+ v_record_info;
v_finite;
Int;
v_section_ctxt;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 04:27:39 +0000