aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.checker13
-rw-r--r--Makefile.dev2
-rw-r--r--checker/univ.ml8
-rw-r--r--checker/univ.mli12
-rw-r--r--dev/checker.dbg5
-rw-r--r--dev/checker_db39
-rw-r--r--dev/checker_printers.ml73
-rw-r--r--dev/checker_printers.mli54
-rw-r--r--dev/ocamldebug-coq.run18
9 files changed, 219 insertions, 5 deletions
diff --git a/Makefile.checker b/Makefile.checker
index dd1f6d514..0ec565d61 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -73,9 +73,12 @@ checker/check.cmxa: checker/check.mllib | md5chk
CHECKGENFILES:=$(addprefix checker/, names.mli names.ml esubst.mli esubst.ml)
+CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) $(CHECKGENFILES) \
+ $(filter dev/checker_%, $(MLFILES) $(MLIFILES))
+
$(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES) $(CHECKGENFILES))
$(SHOW)'OCAMLDEP checker/MLFILES checker/MLIFILES'
- $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(filter checker/%, $(MLFILES) $(MLIFILES) $(CHECKGENFILES)) $(TOTARGET)
+ $(HIDE)$(OCAMLFIND) ocamldep -slash $(CHKLIBS) $(CHECKMLFILES) $(TOTARGET)
$(CHECKMLLIBFILE).d: $(filter checker/%, $(MLLIBFILES) $(MLPACKFILES) $(CHECKGENFILES)) | $(OCAMLLIBDEP)
$(SHOW)'OCAMLLIBDEP checker/MLLIBFILES checker/MLPACKFILES'
@@ -93,6 +96,14 @@ checker/%.cmx: checker/%.ml
$(SHOW)'OCAMLOPT $<'
$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $<
+dev/checker_%.cmo: dev/checker_%.ml
+ $(SHOW)'OCAMLC $<'
+ $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $<
+
+dev/checker_%.cmi: dev/checker_%.mli
+ $(SHOW)'OCAMLC $<'
+ $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $<
+
md5chk:
$(SHOW)'MD5SUM cic.mli'
$(HIDE)if grep -q "^MD5 $$($(OCAML) tools/md5sum.ml checker/cic.mli)$$" checker/values.ml; \
diff --git a/Makefile.dev b/Makefile.dev
index 0461fe072..8f7d21694 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -17,7 +17,7 @@
.PHONY: devel printers
-DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo
+DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo
devel: printers
printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp5.dbg
diff --git a/checker/univ.ml b/checker/univ.ml
index fc0764077..7d285b6fe 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -142,7 +142,13 @@ end
(** Level sets and maps *)
module LMap = HMap.Make (Level)
-module LSet = LMap.Set
+module LSet = struct
+ include LMap.Set
+
+ let pr s =
+ str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}"
+
+end
type 'a universe_map = 'a LMap.t
diff --git a/checker/univ.mli b/checker/univ.mli
index 935f0a2b8..6cd3b3638 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -49,6 +49,7 @@ sig
val make : Level.t -> t
(** Create a universe representing the given level. *)
+ val pr : t -> Pp.t
end
type universe = Universe.t
@@ -140,7 +141,14 @@ val check_constraints : constraints -> universes -> bool
(** Polymorphic maps from universe levels to 'a *)
module LMap : CSig.MapS with type key = universe_level
-module LSet : CSig.SetS with type elt = universe_level
+module LSet :
+sig
+ include CSig.SetS with type elt = Level.t
+
+ val pr : t -> Pp.t
+ (** Pretty-printing *)
+end
+
type 'a universe_map = 'a LMap.t
(** {6 Substitution} *)
@@ -216,6 +224,8 @@ sig
val instantiate : Instance.t -> t -> Constraint.t
val repr : t -> UContext.t
+ val pr : (Level.t -> Pp.t) -> t -> Pp.t
+
end
type abstract_universe_context = AUContext.t
diff --git a/dev/checker.dbg b/dev/checker.dbg
new file mode 100644
index 000000000..9c9ab29e0
--- /dev/null
+++ b/dev/checker.dbg
@@ -0,0 +1,5 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer clib.cma
+load_printer lib.cma
+load_printer check.cma
diff --git a/dev/checker_db b/dev/checker_db
new file mode 100644
index 000000000..327e636c5
--- /dev/null
+++ b/dev/checker_db
@@ -0,0 +1,39 @@
+source checker.dbg
+
+load_printer checker_printers.cmo
+
+install_printer Checker_printers.pP
+
+install_printer Checker_printers.ppfuture
+
+install_printer Checker_printers.ppid
+install_printer Checker_printers.pplab
+install_printer Checker_printers.ppmbid
+install_printer Checker_printers.ppdir
+install_printer Checker_printers.ppmp
+install_printer Checker_printers.ppcon
+install_printer Checker_printers.ppproj
+install_printer Checker_printers.ppkn
+install_printer Checker_printers.ppmind
+install_printer Checker_printers.ppind
+
+install_printer Checker_printers.ppbigint
+
+install_printer Checker_printers.ppintset
+install_printer Checker_printers.ppidset
+
+install_printer Checker_printers.ppidmapgen
+
+install_printer Checker_printers.ppididmap
+
+install_printer Checker_printers.ppuni
+install_printer Checker_printers.ppuni_level
+install_printer Checker_printers.ppuniverse_set
+install_printer Checker_printers.ppuniverse_instance
+install_printer Checker_printers.ppauniverse_context
+install_printer Checker_printers.ppuniverse_context
+install_printer Checker_printers.ppconstraints
+install_printer Checker_printers.ppuniverse_context_future
+install_printer Checker_printers.ppuniverses
+
+install_printer Checker_printers.pploc
diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml
new file mode 100644
index 000000000..40ae1a7b0
--- /dev/null
+++ b/dev/checker_printers.ml
@@ -0,0 +1,73 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pp
+open Names
+open Univ
+
+let pp x = Pp.pp_with Format.std_formatter x
+
+(** Future printer *)
+
+let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
+
+(* name printers *)
+let ppid id = pp (Id.print id)
+let pplab l = pp (Label.print l)
+let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
+let ppdir dir = pp (DirPath.print dir)
+let ppmp mp = pp(str (ModPath.debug_to_string mp))
+let ppcon con = pp(Constant.debug_print con)
+let ppproj con = pp(Constant.debug_print (Projection.constant con))
+let ppkn kn = pp(str (KerName.to_string kn))
+let ppmind kn = pp(MutInd.debug_print kn)
+let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
+
+(* term printers *)
+let ppbigint n = pp (str (Bigint.to_string n));;
+
+let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
+let ppintset l = pp (prset int (Int.Set.elements l))
+let ppidset l = pp (prset Id.print (Id.Set.elements l))
+
+let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
+
+let pridmap pr l =
+ let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in
+ prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])
+let ppidmap pr l = pp (pridmap pr l)
+
+let pridmapgen l =
+ let dom = Id.Set.elements (Id.Map.domain l) in
+ if dom = [] then str "[]" else
+ str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]"
+let ppidmapgen l = pp (pridmapgen l)
+
+let prididmap = pridmap (fun _ -> Id.print)
+let ppididmap = ppidmap (fun _ -> Id.print)
+
+let pP s = pp (hov 0 s)
+
+(* proof printers *)
+let ppuni u = pp(Universe.pr u)
+let ppuni_level u = pp (Level.pr u)
+
+let ppuniverse_set l = pp (LSet.pr l)
+let ppuniverse_instance l = pp (Instance.pr l)
+let ppauniverse_context l = pp (AUContext.pr Level.pr l)
+let ppuniverse_context l = pp (pr_universe_context Level.pr l)
+let ppconstraints c = pp (pr_constraints Level.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 pploc x = let (l,r) = Loc.unloc x in
+ print_string"(";print_int l;print_string",";print_int r;print_string")"
diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli
new file mode 100644
index 000000000..2f9500c5c
--- /dev/null
+++ b/dev/checker_printers.mli
@@ -0,0 +1,54 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** Printers for the ocaml toplevel. *)
+
+val pp : Pp.t -> unit
+val pP : Pp.t -> unit (* with surrounding box *)
+
+val ppfuture : 'a Future.computation -> unit
+
+val ppid : Names.Id.t -> unit
+val pplab : Names.Label.t -> unit
+val ppmbid : Names.MBId.t -> unit
+val ppdir : Names.DirPath.t -> unit
+val ppmp : Names.ModPath.t -> unit
+val ppcon : Names.Constant.t -> unit
+val ppproj : Names.Projection.t -> unit
+val ppkn : Names.KerName.t -> unit
+val ppmind : Names.MutInd.t -> unit
+val ppind : Names.inductive -> unit
+
+val ppbigint : Bigint.bigint -> unit
+
+val ppintset : Int.Set.t -> unit
+val ppidset : Names.Id.Set.t -> unit
+
+val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t
+val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit
+
+val pridmapgen : 'a Names.Id.Map.t -> Pp.t
+val ppidmapgen : 'a Names.Id.Map.t -> unit
+
+val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t
+val ppididmap : Names.Id.t Names.Id.Map.t -> unit
+
+(* Universes *)
+val ppuni : Univ.Universe.t -> unit
+val ppuni_level : Univ.Level.t -> unit (* raw *)
+val ppuniverse_set : Univ.LSet.t -> unit
+val ppuniverse_instance : Univ.Instance.t -> unit
+val ppauniverse_context : Univ.AUContext.t -> unit
+val ppuniverse_context : Univ.UContext.t -> unit
+val ppconstraints : Univ.Constraint.t -> unit
+val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
+val ppuniverses : Univ.universes -> unit
+
+val pploc : Loc.t -> unit
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 8f1c165dd..2bec09de2 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -14,7 +14,15 @@
export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
-exec $OCAMLDEBUG \
+GUESS_CHECKER=
+for arg in "$@"; do
+ if [ "${arg##*/}" = coqchk.byte ]; then
+ GUESS_CHECKER=1
+ fi
+done
+
+if [ -z "$GUESS_CHECKER" ]; then
+ exec $OCAMLDEBUG \
-I $CAMLP5LIB -I +threads \
-I $COQTOP \
-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
@@ -35,3 +43,11 @@ exec $OCAMLDEBUG \
-I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \
-I $COQTOP/ide \
"$@"
+else
+ exec $OCAMLDEBUG \
+ -I $CAMLP5LIB -I +threads \
+ -I $COQTOP \
+ -I $COQTOP/config -I $COQTOP/clib \
+ -I $COQTOP/lib -I $COQTOP/checker \
+ "$@"
+fi
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 05:36:24 +0000