aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml23
-rw-r--r--checker/check.mllib13
-rw-r--r--checker/check_stat.ml7
-rw-r--r--checker/checker.ml12
-rw-r--r--checker/closure.ml2
-rw-r--r--checker/declarations.ml58
-rw-r--r--checker/environ.ml20
l---------checker/esubst.ml1
l---------checker/esubst.mli1
-rw-r--r--checker/indtypes.ml8
-rw-r--r--checker/mod_checking.ml6
-rw-r--r--checker/modops.ml2
l---------checker/names.ml1
l---------checker/names.mli1
-rw-r--r--checker/print.ml8
-rw-r--r--checker/safe_typing.ml4
-rw-r--r--checker/subtyping.ml2
-rw-r--r--checker/typeops.ml8
-rw-r--r--checker/votour.ml48
19 files changed, 127 insertions, 98 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 3a5c91217d..93eb2a0d25 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -111,15 +111,14 @@ let check_one_lib admit (dir,m) =
also check if it carries a validation certificate (yet to
be implemented). *)
if LibrarySet.mem dir admit then
- (Flags.if_verbose ppnl
+ (Flags.if_verbose Feedback.msg_notice
(str "Admitting library: " ++ pr_dirpath dir);
Safe_typing.unsafe_import file md m.library_extra_univs dig)
else
- (Flags.if_verbose ppnl
+ (Flags.if_verbose Feedback.msg_notice
(str "Checking library: " ++ pr_dirpath dir);
Safe_typing.import file md m.library_extra_univs dig);
- Flags.if_verbose pp (fnl());
- pp_flush ();
+ Flags.if_verbose Feedback.msg_notice (fnl());
register_loaded_library m
(*************************************************************************)
@@ -173,7 +172,7 @@ let remove_load_path dir =
let add_load_path (phys_path,coq_path) =
if !Flags.debug then
- ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+ Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
str phys_path);
let phys_path = canonical_path_name phys_path in
let physical, logical = !load_paths in
@@ -188,7 +187,7 @@ let add_load_path (phys_path,coq_path) =
begin
(* Assume the user is concerned by library naming *)
if dir <> default_root_prefix then
- msg_warning
+ Feedback.msg_warning
(str phys_path ++ strbrk " was previously bound to " ++
pr_dirpath dir ++ strbrk "; it is remapped to " ++
pr_dirpath coq_path);
@@ -299,7 +298,7 @@ let name_clash_message dir mdir f =
let depgraph = ref LibraryMap.empty
let intern_from_file (dir, f) =
- Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
+ Flags.if_verbose Feedback.msg_notice(str"[intern "++str f++str" ...");
let (sd,md,table,opaque_csts,digest) =
try
let ch = System.with_magic_number_check raw_intern_library f in
@@ -323,7 +322,7 @@ let intern_from_file (dir, f) =
errorlabstrm "intern_from_file"
(str "The file "++str f++str " contains unfinished tasks");
if opaque_csts <> None then begin
- pp (str " (was a vio file) ");
+ Feedback.msg_notice(str " (was a vio file) ");
Option.iter (fun (_,_,b) -> if not b then
errorlabstrm "intern_from_file"
(str "The file "++str f++str " is still a .vio"))
@@ -334,12 +333,12 @@ let intern_from_file (dir, f) =
Validate.validate !Flags.debug Values.v_libsum sd;
Validate.validate !Flags.debug Values.v_lib md;
Validate.validate !Flags.debug Values.v_opaques table;
- Flags.if_verbose ppnl (str" done]"); pp_flush ();
+ Flags.if_verbose Feedback.msg_notice (str" done]");
let digest =
if opaque_csts <> None then Cic.Dviovo (digest,udg)
else (Cic.Dvo digest) in
sd,md,table,opaque_csts,digest
- with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in
+ with e -> Flags.if_verbose Feedback.msg_notice (str" failed!]"); raise e in
depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
Option.iter (fun (opaque_csts,_,_) ->
@@ -407,11 +406,11 @@ let recheck_library ~norec ~admit ~check =
let nochk =
List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in
(* *)
- Flags.if_verbose ppnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
+ Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
prlist
(fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
List.iter (check_one_lib nochk) needed;
- Flags.if_verbose ppnl (str"Modules were successfully checked")
+ Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked")
open Printf
diff --git a/checker/check.mllib b/checker/check.mllib
index 900cfe0c82..2fa4d57977 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -22,21 +22,24 @@ CList
CString
Serialize
Stateid
-Feedback
-Pp
-Segmenttree
-Unicodetable
-Unicode
CObj
CArray
CStack
Util
+Pp
Ppstyle
+Xml_datatype
+Richpp
+Feedback
+Segmenttree
+Unicodetable
+Unicode
Errors
CEphemeron
Future
CUnix
+Minisys
System
Profile
RemoteCounter
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index d031975d79..a26c93a30d 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -28,7 +28,7 @@ let pr_engagement (impr_set,type_in_type) =
match impr_set with
| ImpredicativeSet -> str "Theory: Set is impredicative"
| PredicativeSet -> str "Theory: Set is predicative"
- end ++
+ end ++ fnl() ++
begin
match type_in_type with
| StratifiedType -> str "Theory: Stratified type hierarchy"
@@ -57,12 +57,13 @@ let print_context env =
env_modules=mods; env_modtypes=mtys};
env_stratification=
{env_universes=univ; env_engagement=engt}} = env in
- ppnl(hov 0
+ Feedback.msg_notice
+ (hov 0
(fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
str"===============" ++ fnl() ++ fnl() ++
str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
str "* " ++ hov 0 (pr_ax csts) ++
- fnl())); pp_flush()
+ fnl()));
end
let stats () =
diff --git a/checker/checker.ml b/checker/checker.ml
index 91a207a60c..61b13c60bb 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -17,7 +17,7 @@ open Check
let () = at_exit flush_all
let fatal_error info anomaly =
- flush_all (); pperrnl info; flush_all ();
+ flush_all (); Feedback.msg_error info; flush_all ();
exit (if anomaly then 129 else 1)
let coq_root = Id.of_string "Coq"
@@ -67,12 +67,12 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
Check.add_load_path (dir,coq_dirpath)
end
else
- msg_warning (str "Cannot open " ++ str dir)
+ Feedback.msg_warning (str "Cannot open " ++ str dir)
let convert_string d =
try Id.of_string d
with Errors.UserError _ ->
- if_verbose msg_warning
+ if_verbose Feedback.msg_warning
(str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
raise Exit
@@ -90,7 +90,7 @@ let add_rec_path ~unix_path ~coq_root =
List.iter Check.add_load_path dirs;
Check.add_load_path (unix_path, coq_root)
else
- msg_warning (str "Cannot open " ++ str unix_path)
+ Feedback.msg_warning (str "Cannot open " ++ str unix_path)
(* By the option -include -I or -R of the command line *)
let includes = ref []
@@ -123,7 +123,7 @@ let init_load_path () =
add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
(* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix)
- (xdg_dirs ~warn:(fun x -> msg_warning (str x)));
+ (xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)));
(* then directories in COQPATH *)
List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
(* then current directory *)
@@ -288,7 +288,7 @@ let rec explain_exn = function
Format.printf "@\nis not convertible with@\n";
Print.print_pure_constr a;
Format.printf "@\n====== universes ====@\n";
- Pp.pp (Univ.pr_universes
+ Feedback.msg_notice (Univ.pr_universes
(ctx.Environ.env_stratification.Environ.env_universes));
str "\nCantApplyBadType at argument " ++ int n
| CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
diff --git a/checker/closure.ml b/checker/closure.ml
index c2708e97d2..cef1d31a68 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -29,7 +29,7 @@ let reset () =
beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0
let stop() =
- msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+ Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++
str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]")
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 3ce3125337..1fe02c8b60 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -73,32 +73,32 @@ let solve_delta_kn resolve kn =
| Equiv kn1 -> kn1
| Inline _ -> raise Not_found
with Not_found ->
- let mp,dir,l = repr_kn kn in
+ let mp,dir,l = KerName.repr kn in
let new_mp = find_prefix resolve mp in
if mp == new_mp then
kn
else
- make_kn new_mp dir l
+ KerName.make new_mp dir l
let gen_of_delta resolve x kn fix_can =
let new_kn = solve_delta_kn resolve kn in
if kn == new_kn then x else fix_can new_kn
let constant_of_delta resolve con =
- let kn = user_con con in
- gen_of_delta resolve con kn (constant_of_kn_equiv kn)
+ let kn = Constant.user con in
+ gen_of_delta resolve con kn (Constant.make kn)
let constant_of_delta2 resolve con =
- let kn, kn' = canonical_con con, user_con con in
- gen_of_delta resolve con kn (constant_of_kn_equiv kn')
+ let kn, kn' = Constant.canonical con, Constant.user con in
+ gen_of_delta resolve con kn (Constant.make kn')
let mind_of_delta resolve mind =
- let kn = user_mind mind in
- gen_of_delta resolve mind kn (mind_of_kn_equiv kn)
+ let kn = MutInd.user mind in
+ gen_of_delta resolve mind kn (MutInd.make kn)
let mind_of_delta2 resolve mind =
- let kn, kn' = canonical_mind mind, user_mind mind in
- gen_of_delta resolve mind kn (mind_of_kn_equiv kn')
+ let kn, kn' = MutInd.canonical mind, MutInd.user mind in
+ gen_of_delta resolve mind kn (MutInd.make kn')
let find_inline_of_delta kn resolve =
match Deltamap.find_kn kn resolve with
@@ -106,7 +106,7 @@ let find_inline_of_delta kn resolve =
| _ -> raise Not_found
let constant_of_delta_with_inline resolve con =
- let kn1,kn2 = canonical_con con,user_con con in
+ let kn1,kn2 = Constant.canonical con, Constant.user con in
try find_inline_of_delta kn2 resolve
with Not_found ->
try find_inline_of_delta kn1 resolve
@@ -137,17 +137,17 @@ let subst_mp sub mp =
| Some (mp',_) -> mp'
let subst_kn_delta sub kn =
- let mp,dir,l = repr_kn kn in
+ let mp,dir,l = KerName.repr kn in
match subst_mp0 sub mp with
Some (mp',resolve) ->
- solve_delta_kn resolve (make_kn mp' dir l)
+ solve_delta_kn resolve (KerName.make mp' dir l)
| None -> kn
let subst_kn sub kn =
- let mp,dir,l = repr_kn kn in
+ let mp,dir,l = KerName.repr kn in
match subst_mp0 sub mp with
Some (mp',_) ->
- make_kn mp' dir l
+ KerName.make mp' dir l
| None -> kn
exception No_subst
@@ -165,14 +165,14 @@ let gen_subst_mp f sub mp1 mp2 =
| Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2
let make_mind_equiv mpu mpc dir l =
- let knu = make_kn mpu dir l in
- if mpu == mpc then mind_of_kn knu
- else mind_of_kn_equiv knu (make_kn mpc dir l)
+ let knu = KerName.make mpu dir l in
+ if mpu == mpc then MutInd.make1 knu
+ else MutInd.make knu (KerName.make mpc dir l)
let subst_ind sub mind =
- let kn1,kn2 = user_mind mind, canonical_mind mind in
- let mp1,dir,l = repr_kn kn1 in
- let mp2,_,_ = repr_kn kn2 in
+ 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
try
let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in
@@ -182,14 +182,14 @@ let subst_ind sub mind =
with No_subst -> mind
let make_con_equiv mpu mpc dir l =
- let knu = make_kn mpu dir l in
- if mpu == mpc then constant_of_kn knu
- else constant_of_kn_equiv knu (make_kn mpc dir l)
+ let knu = KerName.make mpu dir l in
+ if mpu == mpc then Constant.make1 knu
+ else Constant.make knu (KerName.make mpc dir l)
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 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 dup con = con, Const (con, u) in
let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in
@@ -304,7 +304,9 @@ let subset_prefixed_by mp resolver =
match hint with
| Inline _ -> rslv
| Equiv _ ->
- if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv
+ if mp_in_mp mp (KerName.modpath kn)
+ then Deltamap.add_kn kn hint rslv
+ else rslv
in
Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver
diff --git a/checker/environ.ml b/checker/environ.ml
index 7040fdda46..9352f71ef7 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -112,7 +112,7 @@ let anomaly s = anomaly (Pp.str s)
let add_constant kn cs env =
if Cmap_env.mem kn env.env_globals.env_constants then
Printf.ksprintf anomaly ("Constant %s is already defined")
- (string_of_con kn);
+ (Constant.to_string kn);
let new_constants =
Cmap_env.add kn cs env.env_globals.env_constants in
let new_globals =
@@ -172,12 +172,14 @@ let lookup_projection p env =
let scrape_mind env kn=
try
KNmap.find kn env.env_globals.env_inductives_eq
- with
- Not_found -> kn
+ with
+ Not_found -> kn
let mind_equiv env (kn1,i1) (kn2,i2) =
Int.equal i1 i2 &&
- KerName.equal (scrape_mind env (user_mind kn1)) (scrape_mind env (user_mind kn2))
+ KerName.equal
+ (scrape_mind env (MutInd.user kn1))
+ (scrape_mind env (MutInd.user kn2))
let lookup_mind kn env =
@@ -186,9 +188,9 @@ 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")
- (string_of_mind kn);
+ (MutInd.to_string kn);
let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
- let kn1,kn2 = user_mind kn,canonical_mind kn in
+ let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in
let new_inds_eq = if KerName.equal kn1 kn2 then
env.env_globals.env_inductives_eq
else
@@ -205,7 +207,7 @@ let add_mind kn mib env =
let add_modtype ln mtb env =
if MPmap.mem ln env.env_globals.env_modtypes then
Printf.ksprintf anomaly ("Module type %s is already defined")
- (string_of_mp ln);
+ (ModPath.to_string ln);
let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
let new_globals =
{ env.env_globals with
@@ -215,7 +217,7 @@ let add_modtype ln mtb env =
let shallow_add_module mp mb env =
if MPmap.mem mp env.env_globals.env_modules then
Printf.ksprintf anomaly ("Module %s is already defined")
- (string_of_mp mp);
+ (ModPath.to_string mp);
let new_mods = MPmap.add mp mb env.env_globals.env_modules in
let new_globals =
{ env.env_globals with
@@ -225,7 +227,7 @@ let shallow_add_module mp mb env =
let shallow_remove_module mp env =
if not (MPmap.mem mp env.env_globals.env_modules) then
Printf.ksprintf anomaly ("Module %s is unknown")
- (string_of_mp mp);
+ (ModPath.to_string mp);
let new_mods = MPmap.remove mp env.env_globals.env_modules in
let new_globals =
{ env.env_globals with
diff --git a/checker/esubst.ml b/checker/esubst.ml
new file mode 120000
index 0000000000..b82bd24f1e
--- /dev/null
+++ b/checker/esubst.ml
@@ -0,0 +1 @@
+../kernel/esubst.ml \ No newline at end of file
diff --git a/checker/esubst.mli b/checker/esubst.mli
new file mode 120000
index 0000000000..e30eaae5d3
--- /dev/null
+++ b/checker/esubst.mli
@@ -0,0 +1 @@
+../kernel/esubst.mli \ No newline at end of file
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 566df673c1..a667bb8a3e 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -32,11 +32,11 @@ 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) = repr_kn kn in
+ let (mp,_,l) = KerName.repr kn in
str(string_of_mp mp ^ "." ^ Label.to_string l)
let prcon c =
- let ck = canonical_con c in
- let uk = user_con c in
+ let ck = Constant.canonical c in
+ let uk = Constant.user c in
if KerName.equal ck uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")")
(* Same as noccur_between but may perform reductions.
@@ -528,7 +528,7 @@ let check_positivity env_ar mind params nrecp inds =
(************************************************************************)
let check_inductive env kn mib =
- Flags.if_verbose ppnl (str " checking ind: " ++ pr_mind kn); pp_flush ();
+ Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn);
(* check mind_constraints: should be consistent with env *)
let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in
(* check mind_record : TODO ? check #constructor = 1 ? *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 3ea5ed0d34..7f93e15609 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -18,7 +18,7 @@ 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 empty_dirpath 1 in
+ 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
@@ -26,7 +26,7 @@ let refresh_arity ar =
| _ -> ar, Univ.ContextSet.empty
let check_constant_declaration env kn cb =
- Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); pp_flush ();
+ Flags.if_verbose Feedback.msg_notice (str " checking cst: " ++ prcon kn);
let env' =
if cb.const_polymorphic then
let inst = Univ.make_abstract_instance cb.const_universes in
@@ -70,7 +70,7 @@ let check_constant_declaration env kn cb =
let lookup_module mp env =
try Environ.lookup_module mp env
with Not_found ->
- failwith ("Unknown module: "^string_of_mp mp)
+ failwith ("Unknown module: "^ModPath.to_string mp)
let mk_mtb mp sign delta =
{ mod_mp = mp;
diff --git a/checker/modops.ml b/checker/modops.ml
index 9f43752620..442f999bb3 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -28,7 +28,7 @@ let error_not_match l _ =
let error_no_such_label l = error ("No such label "^Label.to_string l)
let error_no_such_label_sub l l1 =
- let l1 = string_of_mp l1 in
+ let l1 = ModPath.to_string l1 in
error ("The field "^
Label.to_string l^" is missing in "^l1^".")
diff --git a/checker/names.ml b/checker/names.ml
new file mode 120000
index 0000000000..f0bf2f83f6
--- /dev/null
+++ b/checker/names.ml
@@ -0,0 +1 @@
+../kernel/names.ml \ No newline at end of file
diff --git a/checker/names.mli b/checker/names.mli
new file mode 120000
index 0000000000..10459f3b29
--- /dev/null
+++ b/checker/names.mli
@@ -0,0 +1 @@
+../kernel/names.mli \ No newline at end of file
diff --git a/checker/print.ml b/checker/print.ml
index 9cd8fda5dc..c0d1ac3688 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -10,7 +10,7 @@ open Format
open Cic
open Names
-let print_instance i = Pp.pp (Univ.Instance.pr i)
+let print_instance i = Feedback.msg_notice (Univ.Instance.pr i)
let print_pure_constr csr =
let rec term_display c = match c with
@@ -108,7 +108,7 @@ let print_pure_constr csr =
and sort_display = function
| Prop(Pos) -> print_string "Set"
| Prop(Null) -> print_string "Prop"
- | Type u -> print_string "Type("; Pp.pp (Univ.pr_uni u); print_string ")"
+ | Type u -> print_string "Type("; Feedback.msg_notice (Univ.pr_uni u); print_string ")"
and name_display = function
| Name id -> print_string (Id.to_string id)
@@ -122,7 +122,7 @@ let print_pure_constr csr =
| ("Coq"::_::l) -> l
| l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
- print_string (debug_string_of_mind sp)
+ print_string (MutInd.debug_to_string sp)
and sp_con_display sp =
(* let dir,l = decode_kn sp in
let ls =
@@ -131,7 +131,7 @@ let print_pure_constr csr =
| ("Coq"::_::l) -> l
| l -> l
in List.iter (fun x -> print_string x; print_string ".") ls;*)
- print_string (debug_string_of_con sp)
+ print_string (Constant.debug_to_string sp)
in
try
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 7f9ed92f95..1071e2f930 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -81,7 +81,7 @@ let stamp_library file digest = ()
warning is issued in case of mismatch *)
let import file clib univs digest =
let env = !genv in
- check_imports msg_warning clib.comp_name env clib.comp_deps;
+ check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps;
check_engagement env clib.comp_enga;
let mb = clib.comp_mod in
Mod_checking.check_module
@@ -93,7 +93,7 @@ let import file clib univs digest =
(* When the module is admitted, digests *must* match *)
let unsafe_import file clib univs digest =
let env = !genv in
- if !Flags.debug then check_imports msg_warning clib.comp_name env clib.comp_deps
+ if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps
else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps;
check_engagement env clib.comp_enga;
full_add_module clib.comp_name clib.comp_mod univs digest
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index e41922573f..46d21f6ccb 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -103,7 +103,7 @@ 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 eq_mind (fun x -> x.proj_ind);
+ check MutInd.equal (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);
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 64afd21b2a..da9842a8db 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -92,7 +92,7 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp =
let _cb =
try lookup_constant kn env
with Not_found ->
- failwith ("Cannot find constant: "^string_of_con kn)
+ failwith ("Cannot find constant: "^Constant.to_string kn)
in
let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in
let () = check_constraints cu env in
@@ -178,7 +178,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: "^string_of_mind (fst ind))
+ failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
in
type_of_inductive_knowing_parameters env (specif,u) paramstyp
@@ -192,7 +192,7 @@ let judge_of_constructor env (c,u) =
let specif =
try lookup_mind_specif env ind
with Not_found ->
- failwith ("Cannot find inductive: "^string_of_mind (fst ind))
+ failwith ("Cannot find inductive: "^MutInd.to_string (fst ind))
in
type_of_constructor (c,u) specif
@@ -223,7 +223,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(eq_mind pb.proj_ind (fst ind));
+ assert(MutInd.equal pb.proj_ind (fst ind));
let ty = subst_instance_constr u pb.proj_type in
substl (c :: List.rev args) ty
diff --git a/checker/votour.ml b/checker/votour.ml
index 79755da4ad..48f9f45e7e 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -10,6 +10,26 @@ open Values
(** {6 Interactive visit of a vo} *)
+let rec read_num max =
+ let quit () =
+ Printf.printf "\nGoodbye!\n%!";
+ exit 0 in
+ Printf.printf "# %!";
+ let l = try read_line () with End_of_file -> quit () in
+ if l = "u" then None
+ else if l = "x" then quit ()
+ else
+ try
+ let v = int_of_string l in
+ if v < 0 || v >= max then
+ let () =
+ Printf.printf "Out-of-range input! (only %d children)\n%!" max in
+ read_num max
+ else Some v
+ with Failure "int_of_string" ->
+ Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!";
+ read_num max
+
type 'a repr =
| INT of int
| STRING of string
@@ -255,15 +275,13 @@ let rec visit v o pos =
(fun i vop -> Printf.printf " %d: %s\n" i (node_info vop))
children;
Printf.printf "-------------\n";
- Printf.printf ("# %!");
- let l = read_line () in
try
- if l = "u" then let info = pop () in visit info.typ info.obj info.pos
- else if l = "x" then (Printf.printf "\nGoodbye!\n\n";exit 0)
- else
- let v',o',pos' = children.(int_of_string l) in
- push (get_name v) v o pos;
- visit v' o' pos'
+ match read_num (Array.length children) with
+ | None -> let info = pop () in visit info.typ info.obj info.pos
+ | Some child ->
+ let v',o',pos' = children.(child) in
+ push (get_name v) v o pos;
+ visit v' o' pos'
with
| Failure "empty stack" -> ()
| Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos
@@ -350,13 +368,13 @@ let visit_vo f =
let size = if Sys.word_size = 64 then header.size64 else header.size32 in
Printf.printf " %d: %s, starting at byte %d (size %iw)\n" i name pos size)
segments;
- Printf.printf "# %!";
- let l = read_line () in
- let seg = int_of_string l in
- seek_in ch segments.(seg).pos;
- let o = Repr.input ch in
- let () = Visit.init () in
- Visit.visit segments.(seg).typ o []
+ match read_num (Array.length segments) with
+ | Some seg ->
+ seek_in ch segments.(seg).pos;
+ let o = Repr.input ch in
+ let () = Visit.init () in
+ Visit.visit segments.(seg).typ o []
+ | None -> ()
done
let main =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 05:33:13 +0000