aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.mllib2
-rw-r--r--checker/checker.ml7
-rw-r--r--checker/closure.ml80
-rw-r--r--checker/closure.mli4
-rw-r--r--checker/coqchk.ml (renamed from checker/main.ml)0
-rw-r--r--checker/coqchk.mli (renamed from checker/main.mli)0
-rw-r--r--checker/declarations.ml36
-rw-r--r--checker/dune26
-rw-r--r--checker/environ.ml2
-rw-r--r--checker/indtypes.ml61
-rw-r--r--checker/inductive.ml35
-rw-r--r--checker/modops.ml2
-rw-r--r--checker/reduction.ml20
-rw-r--r--checker/subtyping.ml8
-rw-r--r--checker/typeops.ml4
-rw-r--r--checker/univ.ml5
-rw-r--r--checker/validate.ml1
-rw-r--r--checker/values.ml17
-rw-r--r--checker/values.mli1
-rw-r--r--checker/votour.ml2
20 files changed, 176 insertions, 137 deletions
diff --git a/checker/check.mllib b/checker/check.mllib
index 139fa765b4..173ad1e325 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,5 +1,3 @@
-Coq_config
-
Analyze
Hook
Terminal
diff --git a/checker/checker.ml b/checker/checker.ml
index fd2725c859..8a5220c9ca 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -243,7 +243,9 @@ let explain_exn = function
| Invalid_argument s ->
hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ())
| Sys.Break ->
- hov 0 (fnl () ++ str "User interrupt.")
+ hov 0 (fnl () ++ str "User interrupt.")
+ | Univ.AlreadyDeclared ->
+ hov 0 (str "Error: Multiply declared universe.")
| Univ.UniverseInconsistency (o,u,v) ->
let msg =
if !Flags.debug (*!Constrextern.print_universes*) then
@@ -321,8 +323,7 @@ let parse_args argv =
| "-coqlib" :: s :: rem ->
if not (exists_dir s) then
fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
- Flags.coqlib := s;
- Flags.coqlib_spec := true;
+ Envars.set_user_coqlib s;
parse rem
| ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem
diff --git a/checker/closure.ml b/checker/closure.ml
index 5706011607..138499b0e6 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -121,9 +121,6 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
* abstractions, storing a representation (of type 'a) of the body of
* this constant or abstraction.
* * i_tab is the cache table of the results
- * * i_repr is the function to get the representation from the current
- * state of the cache and the body of the constant. The result
- * is stored in the table.
* * i_rels = (4,[(1,c);(3,d)]) means there are 4 free rel variables
* and only those with index 1 and 3 have bodies which are c and d resp.
*
@@ -156,33 +153,6 @@ end
module KeyTable = Hashtbl.Make(KeyHash)
-type 'a infos = {
- i_flags : reds;
- i_repr : 'a infos -> constr -> 'a;
- i_env : env;
- i_rels : int * (int * constr) list;
- i_tab : 'a KeyTable.t }
-
-let ref_value_cache info ref =
- try
- Some (KeyTable.find info.i_tab ref)
- with Not_found ->
- try
- let body =
- match ref with
- | RelKey n ->
- let (s,l) = info.i_rels in lift n (Int.List.assoc (s-n) l)
- | VarKey id -> raise Not_found
- | ConstKey cst -> constant_value info.i_env cst
- in
- let v = info.i_repr info body in
- KeyTable.add info.i_tab ref v;
- Some v
- with
- | Not_found (* List.assoc *)
- | NotEvaluableConst _ (* Const *)
- -> None
-
let defined_rels flags env =
(* if red_local_const (snd flags) then*)
fold_rel_context
@@ -193,16 +163,6 @@ let defined_rels flags env =
(rel_context env) ~init:(0,[])
(* else (0,[])*)
-let mind_equiv_infos info = mind_equiv info.i_env
-
-let create mk_cl flgs env =
- { i_flags = flgs;
- i_repr = mk_cl;
- i_env = env;
- i_rels = defined_rels flgs env;
- i_tab = KeyTable.create 17 }
-
-
(**********************************************************************)
(* Lazy reduction: the one used in kernel operations *)
@@ -255,6 +215,12 @@ and fterm =
| FCLOS of constr * fconstr subs
| FLOCKED
+type clos_infos = {
+ i_flags : reds;
+ i_env : env;
+ i_rels : int * (int * constr) list;
+ i_tab : fconstr KeyTable.t }
+
let fterm_of v = v.term
let set_norm v = v.norm <- Norm
@@ -372,6 +338,30 @@ let mk_clos e t =
let mk_clos_vect env v = Array.map (mk_clos env) v
+let inject = mk_clos (subs_id 0)
+
+let ref_value_cache info ref =
+ try
+ Some (KeyTable.find info.i_tab ref)
+ with Not_found ->
+ try
+ let body =
+ match ref with
+ | RelKey n ->
+ let (s,l) = info.i_rels in lift n (Int.List.assoc (s-n) l)
+ | VarKey id -> raise Not_found
+ | ConstKey cst -> constant_value info.i_env cst
+ in
+ let v = inject body in
+ KeyTable.add info.i_tab ref v;
+ Some v
+ with
+ | Not_found (* List.assoc *)
+ | NotEvaluableConst _ (* Const *)
+ -> None
+
+let mind_equiv_infos info = mind_equiv info.i_env
+
(* Translate the head constructor of t from constr to fconstr. This
function is parameterized by the function to apply on the direct
subterms.
@@ -783,21 +773,19 @@ let kh info v stk = fapp_stack(kni info v stk)
let whd_val info v =
with_stats (lazy (term_of_fconstr (kh info v [])))
-let inject = mk_clos (subs_id 0)
-
let whd_stack infos m stk =
let k = kni infos m stk in
let _ = fapp_stack k in (* to unlock Zupdates! *)
k
-(* cache of constants: the body is computed only when needed. *)
-type clos_infos = fconstr infos
-
let infos_env x = x.i_env
let infos_flags x = x.i_flags
let oracle_of_infos x = x.i_env.env_conv_oracle
let create_clos_infos flgs env =
- create (fun _ -> inject) flgs env
+ { i_flags = flgs;
+ i_env = env;
+ i_rels = defined_rels flgs env;
+ i_tab = KeyTable.create 17 }
let unfold_reference = ref_value_cache
diff --git a/checker/closure.mli b/checker/closure.mli
index cec785699d..4c6643754b 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -61,10 +61,6 @@ val betadeltaiotanolet : reds
type table_key = Constant.t puniverses tableKey
-type 'a infos
-val ref_value_cache: 'a infos -> table_key -> 'a option
-val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
-
(************************************************************************)
(*s Lazy reduction. *)
diff --git a/checker/main.ml b/checker/coqchk.ml
index 83b4ddd2d5..83b4ddd2d5 100644
--- a/checker/main.ml
+++ b/checker/coqchk.ml
diff --git a/checker/main.mli b/checker/coqchk.mli
index 9db9ecd12e..9db9ecd12e 100644
--- a/checker/main.mli
+++ b/checker/coqchk.mli
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 03fee1ab51..93d5f8bfa2 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -70,12 +70,12 @@ let solve_delta_kn resolve kn =
| Equiv kn1 -> kn1
| Inline _ -> raise Not_found
with Not_found ->
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
let new_mp = find_prefix resolve mp in
if mp == new_mp then
kn
else
- KerName.make new_mp dir l
+ KerName.make new_mp l
let gen_of_delta resolve x kn fix_can =
let new_kn = solve_delta_kn resolve kn in
@@ -129,17 +129,17 @@ let subst_mp sub mp =
| Some (mp',_) -> mp'
let subst_kn_delta sub kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
match subst_mp0 sub mp with
Some (mp',resolve) ->
- solve_delta_kn resolve (KerName.make mp' dir l)
+ solve_delta_kn resolve (KerName.make mp' l)
| None -> kn
let subst_kn sub kn =
- let mp,dir,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
match subst_mp0 sub mp with
Some (mp',_) ->
- KerName.make mp' dir l
+ KerName.make mp' l
| None -> kn
exception No_subst
@@ -156,16 +156,16 @@ let gen_subst_mp f sub mp1 mp2 =
| None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve
| Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2
-let make_mind_equiv mpu mpc dir l =
- let knu = KerName.make mpu dir l in
+let make_mind_equiv mpu mpc l =
+ let knu = KerName.make mpu l in
if mpu == mpc then MutInd.make1 knu
- else MutInd.make knu (KerName.make mpc dir l)
+ else MutInd.make knu (KerName.make mpc l)
let subst_ind sub mind =
let kn1,kn2 = MutInd.user mind, MutInd.canonical mind in
- let mp1,dir,l = KerName.repr kn1 in
- let mp2,_,_ = KerName.repr kn2 in
- let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in
+ let mp1,l = KerName.repr kn1 in
+ let mp2,_ = KerName.repr kn2 in
+ let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 l in
try
let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in
match side with
@@ -173,16 +173,16 @@ let subst_ind sub mind =
| Canonical -> mind_of_delta2 resolve mind'
with No_subst -> mind
-let make_con_equiv mpu mpc dir l =
- let knu = KerName.make mpu dir l in
+let make_con_equiv mpu mpc l =
+ let knu = KerName.make mpu l in
if mpu == mpc then Constant.make1 knu
- else Constant.make knu (KerName.make mpc dir l)
+ else Constant.make knu (KerName.make mpc l)
let subst_con0 sub con u =
let kn1,kn2 = Constant.user con, Constant.canonical con in
- let mp1,dir,l = KerName.repr kn1 in
- let mp2,_,_ = KerName.repr kn2 in
- let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in
+ let mp1,l = KerName.repr kn1 in
+ let mp2,_ = KerName.repr kn2 in
+ let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 l in
let dup con = con, Const (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
diff --git a/checker/dune b/checker/dune
index d918f853dd..5aff9211d7 100644
--- a/checker/dune
+++ b/checker/dune
@@ -3,24 +3,32 @@
(rule (copy %{project_root}/kernel/esubst.ml esubst.ml))
(rule (copy %{project_root}/kernel/esubst.mli esubst.mli))
+; Careful with bug https://github.com/ocaml/odoc/issues/148
+;
+; If we don't pack checker we will have a problem here due to
+; duplicate module names in the whole build.
(library
- (name checker)
- (public_name coq.checker)
+ (name checklib)
+ (public_name coq.checklib)
(synopsis "Coq's Standalone Proof Checker")
- (modules values analyze names esubst)
- (wrapped false)
+ (modules :standard \ coqchk votour)
+ (modules_without_implementation cic)
+ (wrapped true)
(libraries coq.lib))
(executable
- (name main)
+ (name coqchk)
(public_name coqchk)
- (modules :standard \ votour values analyze names esubst)
- (modules_without_implementation cic)
- (libraries coq.checker))
+ (package coq)
+ (modules coqchk)
+ (flags :standard -open Checklib)
+ (libraries coq.checklib))
(executable
(name votour)
(public_name votour)
+ (package coq)
(modules votour)
- (libraries coq.checker))
+ (flags :standard -open Checklib)
+ (libraries coq.checklib))
diff --git a/checker/environ.ml b/checker/environ.ml
index 74cf237763..b172acb126 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -183,7 +183,7 @@ let lookup_mind kn env =
let add_mind kn mib env =
if Mindmap_env.mem kn env.env_globals.env_inductives then
- Printf.ksprintf anomaly ("Inductive %s is already defined.")
+ Printf.ksprintf anomaly ("Mutual inductive block %s is already defined.")
(MutInd.to_string kn);
let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 8f11e01c33..f6c510ee1c 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -34,7 +34,7 @@ let string_of_mp mp =
if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
let prkn kn =
- let (mp,_,l) = KerName.repr kn in
+ let (mp,l) = KerName.repr kn in
str(string_of_mp mp ^ "." ^ Label.to_string l)
let prcon c =
let ck = Constant.canonical c in
@@ -310,25 +310,31 @@ let failwith_non_pos_list n ntypes l =
List.iter (failwith_non_pos n ntypes) l;
anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.")
-(* Conclusion of constructors: check the inductive type is called with
- the expected parameters *)
-let check_correct_par (env,n,ntypes,_) hyps l largs =
- let nparams = rel_context_nhyps hyps in
- let largs = Array.of_list largs in
- if Array.length largs < nparams then
- raise (IllFormedInd (LocalNotEnoughArgs l));
- let (lpar,largs') = Array.chop nparams largs in
- let nhyps = List.length hyps in
- let rec check k index = function
+(* Check the inductive type is called with the expected parameters *)
+(* [n] is the index of the last inductive type in [env] *)
+let check_correct_par (env,n,ntypes,_) paramdecls ind_index args =
+ let nparams = rel_context_nhyps paramdecls in
+ let args = Array.of_list args in
+ if Array.length args < nparams then
+ raise (IllFormedInd (LocalNotEnoughArgs ind_index));
+ let (params,realargs) = Array.chop nparams args in
+ let nparamdecls = List.length paramdecls in
+ let rec check param_index paramdecl_index = function
| [] -> ()
- | LocalDef _ :: hyps -> check k (index+1) hyps
- | _::hyps ->
- match whd_all env lpar.(k) with
- | Rel w when w = index -> check (k-1) (index+1) hyps
- | _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l)))
- in check (nparams-1) (n-nhyps) hyps;
- if not (Array.for_all (noccur_between n ntypes) largs') then
- failwith_non_pos_vect n ntypes largs'
+ | LocalDef _ :: paramdecls ->
+ check param_index (paramdecl_index+1) paramdecls
+ | _::paramdecls ->
+ match whd_all env params.(param_index) with
+ | Rel w when Int.equal w paramdecl_index ->
+ check (param_index-1) (paramdecl_index+1) paramdecls
+ | _ ->
+ let paramdecl_index_in_env = paramdecl_index-n+nparamdecls+1 in
+ let err =
+ LocalNonPar (param_index+1, paramdecl_index_in_env, ind_index) in
+ raise (IllFormedInd err)
+ in check (nparams-1) (n-nparamdecls) paramdecls;
+ if not (Array.for_all (noccur_between n ntypes) realargs) then
+ failwith_non_pos_vect n ntypes realargs
(* Arguments of constructor: check the number of recursive parameters nrecp.
the first parameters which are constant in recursive arguments
@@ -412,8 +418,8 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
| Some b ->
check_pos (ienv_push_var ienv (na, b, mk_norec)) d)
| Rel k ->
- (try
- let (ra,rarg) = List.nth ra_env (k-1) in
+ (try let (ra,rarg) = List.nth ra_env (k-1) in
+ let largs = List.map (whd_all env) largs in
(match ra with
Mrec _ -> check_rec_par ienv hyps nrecp largs
| _ -> ());
@@ -525,10 +531,11 @@ let check_positivity env_ar mind params nrecp inds =
Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in
let lra_ind = List.rev (Array.to_list rc) in
let lparams = rel_context_length params in
+ let ra_env =
+ List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
+ let env_ar_par = push_rel_context params env_ar in
let check_one i mip =
- let ra_env =
- List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
- let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
+ let ienv = (env_ar_par, 1+lparams, ntypes, ra_env) in
check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
in
let irecargs = Array.mapi check_one inds in
@@ -595,8 +602,12 @@ let check_subtyping cumi paramsctxt env inds =
(************************************************************************)
(************************************************************************)
+let print_mutind ind =
+ let kn = MutInd.user ind in
+ str (ModPath.to_string (KerName.modpath kn) ^ "." ^ Label.to_string (KerName.label kn))
+
let check_inductive env kn mib =
- Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn);
+ Flags.if_verbose Feedback.msg_notice (str " checking mutind block: " ++ print_mutind kn);
(* check mind_constraints: should be consistent with env *)
let env0 =
match mib.mind_universes with
diff --git a/checker/inductive.ml b/checker/inductive.ml
index d15380643f..269a98cb0e 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -282,6 +282,11 @@ let get_instantiated_arity (ind,u) (mib,mip) params =
let elim_sorts (_,mip) = mip.mind_kelim
+let is_primitive_record (mib,_) =
+ match mib.mind_record with
+ | PrimRecord _ -> true
+ | NotRecord | FakeRecord -> false
+
let extended_rel_list n hyps =
let rec reln l p = function
| LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps
@@ -381,12 +386,13 @@ let type_case_branches env (pind,largs) (p,pj) c =
(* Checking the case annotation is relevant *)
let check_case_info env indsp ci =
- let (mib,mip) = lookup_mind_specif env indsp in
+ let mib, mip as spec = lookup_mind_specif env indsp in
if
- not (eq_ind_chk indsp ci.ci_ind) ||
+ not (mind_equiv env indsp ci.ci_ind) ||
(mib.mind_nparams <> ci.ci_npar) ||
(mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
- (mip.mind_consnrealargs <> ci.ci_cstr_nargs)
+ (mip.mind_consnrealargs <> ci.ci_cstr_nargs) ||
+ is_primitive_record spec
then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
(************************************************************************)
@@ -801,10 +807,23 @@ let rec subterm_specif renv stack t =
subterm_specif (push_var renv (x,a,spec)) stack' b
(* Metas and evars are considered OK *)
- | (Meta _|Evar _) -> Dead_code
-
- (* Other terms are not subterms *)
- | _ -> Not_subterm
+ | (Meta _|Evar _) -> Dead_code
+
+ | Proj (p, c) ->
+ let subt = subterm_specif renv stack c in
+ (match subt with
+ | Subterm (_s, wf) ->
+ (* We take the subterm specs of the constructor of the record *)
+ let wf_args = (dest_subterms wf).(0) in
+ (* We extract the tree of the projected argument *)
+ let n = Projection.arg p in
+ spec_of_tree (List.nth wf_args n)
+ | Dead_code -> Dead_code
+ | Not_subterm -> Not_subterm)
+
+ (* Other terms are not subterms *)
+ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _
+ | Construct _ | CoFix _ -> Not_subterm
and lazy_subterm_specif renv stack t =
lazy (subterm_specif renv stack t)
@@ -856,6 +875,8 @@ let filter_stack_domain env p stack =
match stack, t with
| elt :: stack', Prod (n,a,c0) ->
let d = LocalAssum (n,a) in
+ let ctx, a = dest_prod_assum env a in
+ let env = push_rel_context ctx env in
let ty, args = decompose_app (whd_all env a) in
let elt = match ty with
| Ind ind ->
diff --git a/checker/modops.ml b/checker/modops.ml
index b92d7bbf1f..541d009ff9 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -55,7 +55,7 @@ let module_body_of_type mp mtb =
let rec add_structure mp sign resolver env =
let add_one env (l,elem) =
- let kn = KerName.make2 mp l in
+ let kn = KerName.make mp l in
let con = Constant.make1 kn in
let mind = mind_of_delta resolver (MutInd.make1 kn) in
match elem with
diff --git a/checker/reduction.ml b/checker/reduction.ml
index d36c0ef2c9..1158152f63 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -192,10 +192,7 @@ let convert_constructors
| Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2
| Cumulative_ind cumi ->
let num_cnstr_args =
- let nparamsctxt =
- mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
- in
- nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
+ mind.mind_nparams + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
in
if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
convert_universes univs u1 u2
@@ -280,17 +277,26 @@ let get_strategy { var_opacity; cst_opacity } = function
with Not_found -> default_level)
| RelKey _ -> Expand
+let dep_order l2r k1 k2 = match k1, k2 with
+| RelKey _, RelKey _ -> l2r
+| RelKey _, (VarKey _ | ConstKey _) -> true
+| VarKey _, RelKey _ -> false
+| VarKey _, VarKey _ -> l2r
+| VarKey _, ConstKey _ -> true
+| ConstKey _, (RelKey _ | VarKey _) -> false
+| ConstKey _, ConstKey _ -> l2r
+
let oracle_order infos l2r k1 k2 =
let o = Closure.oracle_of_infos infos in
match get_strategy o k1, get_strategy o k2 with
- | Expand, Expand -> l2r
+ | Expand, Expand -> dep_order l2r k1 k2
| Expand, (Opaque | Level _) -> true
| (Opaque | Level _), Expand -> false
- | Opaque, Opaque -> l2r
+ | Opaque, Opaque -> dep_order l2r k1 k2
| Level _, Opaque -> true
| Opaque, Level _ -> false
| Level n1, Level n2 ->
- if Int.equal n1 n2 then l2r
+ if Int.equal n1 n2 then dep_order l2r k1 k2
else n1 < n2
let eq_table_key univ =
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 0916d98ddf..e2c605dde8 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -198,9 +198,11 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
assert (Array.length mib2.mind_packets = 1);
assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1);
assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1);
- check
- (fun l1 l2 -> List.equal Name.equal l1 l2)
- (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
+ check (List.equal Name.equal)
+ (fun mib ->
+ let nparamdecls = List.length mib.mind_params_ctxt in
+ let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in
+ snd (List.chop nparamdecls names))
end;
(* we first check simple things *)
Array.iter2 check_packet mib1.mind_packets mib2.mind_packets;
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 138fe8bc95..e4c3f4ae4b 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -158,7 +158,7 @@ let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) =
let specif =
try lookup_mind_specif env ind
with Not_found ->
- failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
+ failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind))
in
type_of_inductive_knowing_parameters env (specif,u) paramstyp
@@ -172,7 +172,7 @@ let judge_of_constructor env (c,u) =
let specif =
try lookup_mind_specif env ind
with Not_found ->
- failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
+ failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind))
in
type_of_constructor (c,u) specif
diff --git a/checker/univ.ml b/checker/univ.ml
index e50e883adf..a0511ad21b 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1088,14 +1088,13 @@ let subst_univs_universe fn ul =
let merge_context strict ctx g =
let g = Array.fold_left
- (* Be lenient, module typing reintroduces universes and
- constraints due to includes *)
- (fun g v -> try add_universe v strict g with AlreadyDeclared -> g)
+ (fun g v -> add_universe v strict g)
g (UContext.instance ctx)
in merge_constraints (UContext.constraints ctx) g
let merge_context_set strict ctx g =
let g = LSet.fold
+ (* Include and side effects still have double-declared universes *)
(fun v g -> try add_universe v strict g with AlreadyDeclared -> g)
(ContextSet.levels ctx) g
in merge_constraints (ContextSet.constraints ctx) g
diff --git a/checker/validate.ml b/checker/validate.ml
index f831875dd4..c214409a2c 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -85,6 +85,7 @@ let rec val_gen v ctx o = match v with
| Fail s -> fail ctx o ("unexpected object " ^ s)
| Annot (s,v) -> val_gen v (ctx/CtxAnnot s) o
| Dyn -> val_dyn ctx o
+ | Proxy { contents = v } -> val_gen v ctx o
(* Check that an object is a tuple (or a record). vs is an array of
value representation for each field. Its size corresponds to the
diff --git a/checker/values.ml b/checker/values.ml
index 801874773a..24f10b7a87 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -45,6 +45,13 @@ type value =
| String
| Annot of string * value
| Dyn
+ | Proxy of value ref
+
+let fix (f : value -> value) : value =
+ let self = ref Any in
+ let ans = f (Proxy self) in
+ let () = self := ans in
+ ans
(** Some pseudo-constructors *)
@@ -91,7 +98,7 @@ let rec v_mp = Sum("module_path",0,
[|[|v_dp|];
[|v_uid|];
[|v_mp;v_id|]|])
-let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id;Int|]
+let v_kn = v_tuple "kernel_name" [|v_mp;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|]
@@ -347,18 +354,16 @@ let v_states = v_pair Any v_frozen
let v_state = Tuple ("state", [|v_states; Any; v_bool|])
let v_vcs =
- let data = Opt Any in
- let vcs =
+ let vcs self =
Tuple ("vcs",
[|Any; Any;
Tuple ("dag",
[|Any; Any; v_map Any (Tuple ("state_info",
- [|Any; Any; Opt v_state; v_pair data Any|]))
+ [|Any; Any; Opt v_state; v_pair (Opt self) Any|]))
|])
|])
in
- let () = Obj.set_field (Obj.magic data) 0 (Obj.magic vcs) in
- vcs
+ fix vcs
let v_uuid = Any
let v_request id doc =
diff --git a/checker/values.mli b/checker/values.mli
index 20b9d54a68..1b1437a469 100644
--- a/checker/values.mli
+++ b/checker/values.mli
@@ -20,6 +20,7 @@ type value =
| String
| Annot of string * value
| Dyn
+ | Proxy of value ref
val v_univopaques : value
val v_libsum : value
diff --git a/checker/votour.ml b/checker/votour.ml
index bc820e23dd..1ea0de456e 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -152,6 +152,7 @@ let rec get_name ?(extra=false) = function
|String -> "string"
|Annot (s,v) -> s^"/"^get_name ~extra v
|Dyn -> "<dynamic>"
+ | Proxy v -> get_name ~extra !v
(** For tuples, its quite handy to display the inner 1st string (if any).
Cf. [structure_body] for instance *)
@@ -255,6 +256,7 @@ let rec get_children v o pos = match v with
| _ -> raise Exit
end
|Fail s -> raise Forbidden
+ | Proxy v -> get_children !v o pos
let get_children v o pos =
try get_children v o pos
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 04:47:59 +0000