aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/checkFlags.ml1
-rw-r--r--checker/checkInductive.ml10
-rw-r--r--checker/checker.ml22
-rw-r--r--checker/values.ml17
4 files changed, 25 insertions, 25 deletions
diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml
index 1f5e76bd83..369623e8c5 100644
--- a/checker/checkFlags.ml
+++ b/checker/checkFlags.ml
@@ -18,6 +18,7 @@ let set_local_flags flags env =
check_universes = flags.check_universes;
conv_oracle = flags.conv_oracle;
cumulative_sprop = flags.cumulative_sprop;
+ allow_uip = flags.allow_uip;
}
in
Environ.set_typing_flags flags env
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index c370a77ea0..ef606c9a75 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -101,11 +101,17 @@ let check_kelim k1 k2 = Sorts.family_leq k1 k2
(* Use [eq_ind_chk] because when we rebuild the recargs we have lost
the knowledge of who is the canonical version.
Try with to see test-suite/coqchk/include.v *)
+let eq_nested_types ty1 ty2 = match ty1, ty2 with
+| NestedInd ind1, NestedInd ind2 -> eq_ind_chk ind1 ind2
+| NestedInd _, _ -> false
+| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2
+| NestedPrimitive _, _ -> false
+
let eq_recarg a1 a2 = match a1, a2 with
| Norec, Norec -> true
| Mrec i1, Mrec i2 -> eq_ind_chk i1 i2
- | Imbr i1, Imbr i2 -> eq_ind_chk i1 i2
- | (Norec | Mrec _ | Imbr _), _ -> false
+ | Nested ty1, Nested ty2 -> eq_nested_types ty1 ty2
+ | (Norec | Mrec _ | Nested _), _ -> false
let eq_reloc_tbl = Array.equal (fun x y -> Int.equal (fst x) (fst y) && Int.equal (snd x) (snd y))
diff --git a/checker/checker.ml b/checker/checker.ml
index 086acc482c..e2c90e2b93 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -95,12 +95,10 @@ let add_rec_path ~unix_path ~coq_root =
else
Feedback.msg_warning (str "Cannot open " ++ str unix_path)
-(* By the option -include -I or -R of the command line *)
+(* By the option -R/-Q of the command line *)
let includes = ref []
let push_include (s, alias) = includes := (s,alias) :: !includes
-let set_default_include d =
- push_include (d, Check.default_root_prefix)
let set_include d p =
let p = dirpath_of_string p in
push_include (d,p)
@@ -127,7 +125,7 @@ let init_load_path () =
List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
(* then current directory *)
add_path ~unix_path:"." ~coq_root:Check.default_root_prefix;
- (* additional loadpath, given with -I -include -R options *)
+ (* additional loadpath, given with -R/-Q options *)
List.iter
(fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root)
(List.rev !includes);
@@ -299,6 +297,7 @@ let explain_exn = function
| UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
| DisallowedSProp -> str"DisallowedSProp"
| BadRelevance -> str"BadRelevance"
+ | BadInvert -> str"BadInvert"
| UndeclaredUniverse _ -> str"UndeclaredUniverse"))
| InductiveError e ->
@@ -320,9 +319,6 @@ let explain_exn = function
report ())
| e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
-let deprecated flag =
- Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag))
-
let parse_args argv =
let rec parse = function
| [] -> ()
@@ -338,16 +334,8 @@ let parse_args argv =
Envars.set_user_coqlib s;
parse rem
- | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem
- | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
- | ("-I"|"-include") :: d :: rem -> deprecated "-I"; set_default_include d; parse rem
- | ("-I"|"-include") :: [] -> usage ()
-
- | "-Q" :: d :: p :: rem -> set_include d p;parse rem
- | "-Q" :: ([] | [_]) -> usage ()
-
- | "-R" :: d :: p :: rem -> set_include d p;parse rem
- | "-R" :: ([] | [_]) -> usage ()
+ | ("-Q"|"-R") :: d :: p :: rem -> set_include d p;parse rem
+ | ("-Q"|"-R") :: ([] | [_]) -> usage ()
| "-debug" :: rem -> set_debug (); parse rem
diff --git a/checker/values.ml b/checker/values.ml
index cce0ce7203..38cb243f80 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -147,18 +147,20 @@ let rec v_constr =
[|v_puniverses v_cst|]; (* Const *)
[|v_puniverses v_ind|]; (* Ind *)
[|v_puniverses v_cons|]; (* Construct *)
- [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
+ [|v_caseinfo;v_constr;v_case_invert;v_constr;Array v_constr|]; (* Case *)
[|v_fix|]; (* Fix *)
[|v_cofix|]; (* CoFix *)
[|v_proj;v_constr|]; (* Proj *)
[|v_uint63|]; (* Int *)
- [|Float64|] (* Int *)
+ [|Float64|]; (* Float *)
+ [|v_instance;Array v_constr;v_constr;v_constr|] (* Array *)
|])
and v_prec = Tuple ("prec_declaration",
[|Array (v_binder_annot v_name); Array v_constr; Array v_constr|])
and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
+and v_case_invert = Sum ("case_inversion", 1, [|[|v_instance;Array v_constr|]|])
let v_rdecl = v_sum "rel_declaration" 0
[| [|v_binder_annot v_name; v_constr|]; (* LocalAssum *)
@@ -234,7 +236,7 @@ let v_template_universes =
v_tuple "template_universes" [|List(Opt v_level);v_context_set|]
let v_primitive =
- v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *)
+ v_enum "primitive" 50 (* Number of "Primitive" in Int63.v and PrimFloat.v *)
let v_cst_def =
v_sum "constant_def" 0
@@ -244,7 +246,7 @@ let v_typing_flags =
v_tuple "typing_flags"
[|v_bool; v_bool; v_bool;
v_oracle; v_bool; v_bool;
- v_bool; v_bool; v_bool|]
+ v_bool; v_bool; v_bool; v_bool|]
let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
@@ -258,8 +260,11 @@ let v_cb = v_tuple "constant_body"
v_bool;
v_typing_flags|]
+let v_nested = v_sum "nested" 0
+ [|[|v_ind|] (* NestedInd *);[|v_cst|] (* NestedPrimitive *)|]
+
let v_recarg = v_sum "recarg" 1 (* Norec *)
- [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|]
+ [|[|v_ind|] (* Mrec *);[|v_nested|] (* Nested *)|]
let rec v_wfp = Sum ("wf_paths",0,
[|[|Int;Int|]; (* Rtree.Param *)
@@ -316,7 +321,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
let v_prim_ind = v_enum "prim_ind" 6
(* Number of "Register ... as kernel.ind_..." in Int63.v and PrimFloat.v *)
-let v_prim_type = v_enum "prim_type" 2
+let v_prim_type = v_enum "prim_type" 3
(* Number of constructors of prim_type in "kernel/cPrimitives.ml" *)
let v_retro_action =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 08:15:42 +0000