From b06de08733bb01efcbb8b902fe3157b7045c8bb3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 22 Apr 2018 15:27:22 +0200 Subject: Infrastructure for ocamldebug on the checker --- Makefile.checker | 13 ++++++++- Makefile.dev | 2 +- checker/univ.ml | 8 +++++- checker/univ.mli | 12 +++++++- dev/checker.dbg | 5 ++++ dev/checker_db | 39 ++++++++++++++++++++++++++ dev/checker_printers.ml | 73 ++++++++++++++++++++++++++++++++++++++++++++++++ dev/checker_printers.mli | 54 +++++++++++++++++++++++++++++++++++ dev/ocamldebug-coq.run | 18 +++++++++++- 9 files changed, 219 insertions(+), 5 deletions(-) create mode 100644 dev/checker.dbg create mode 100644 dev/checker_db create mode 100644 dev/checker_printers.ml create mode 100644 dev/checker_printers.mli 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 *) +(* 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 *) +(* 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 -- cgit v1.2.3