From: Stefano Zacchiroli Date: Wed, 27 Apr 2005 17:21:01 +0000 (+0000) Subject: checked in new version of matita from svn X-Git-Tag: after_svn_merge~1 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git checked in new version of matita from svn --- diff --git a/helm/matita/.cvsignore b/helm/matita/.cvsignore new file mode 100644 index 000000000..004b4c5b8 --- /dev/null +++ b/helm/matita/.cvsignore @@ -0,0 +1,29 @@ +*.a +*.annot +autom4te.cache +buildTimeConf.ml +cicbrowser +cicbrowser.opt +*.cma +*.cmi +*.cmo +*.cmx +*.cmxa +config.log +config.status +configure +.depend +Makefile +matita +.matita +matitac +matitac.opt +matitaGeneratedGui.ml +matitaGeneratedGui.mli +matita.glade.bak +matita.gladep +matita.gladep.bak +matita.opt +matita.opt +*.o +*.swp diff --git a/helm/matita/.depend b/helm/matita/.depend new file mode 100644 index 000000000..618c44629 --- /dev/null +++ b/helm/matita/.depend @@ -0,0 +1,51 @@ +matitac.cmo: matitaTypes.cmo matitaLog.cmi matitaEngine.cmi matitaDb.cmi \ + buildTimeConf.cmo +matitac.cmx: matitaTypes.cmx matitaLog.cmx matitaEngine.cmx matitaDb.cmx \ + buildTimeConf.cmx +matitaDb.cmo: matitaDb.cmi +matitaDb.cmx: matitaDb.cmi +matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi +matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi +matitaEngine.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ + matitaDisambiguator.cmi matitaDb.cmi matitaEngine.cmi +matitaEngine.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \ + matitaDisambiguator.cmx matitaDb.cmx matitaEngine.cmi +matitaGeneratedGui.cmo: matitaGeneratedGui.cmi +matitaGeneratedGui.cmx: matitaGeneratedGui.cmi +matitaGtkMisc.cmo: matitaTypes.cmo matitaGeneratedGui.cmi matitaGtkMisc.cmi +matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi +matitaGui.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi matitaLog.cmi \ + matitaGtkMisc.cmi matitaGeneratedGui.cmi buildTimeConf.cmo matitaGui.cmi +matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaLog.cmx \ + matitaGtkMisc.cmx matitaGeneratedGui.cmx buildTimeConf.cmx matitaGui.cmi +matitaLog.cmo: matitaLog.cmi +matitaLog.cmx: matitaLog.cmi +matitaMathView.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \ + matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo matitaMathView.cmi +matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ + matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx matitaMathView.cmi +matitaMisc.cmo: matitaTypes.cmo buildTimeConf.cmo matitaMisc.cmi +matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi +matita.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \ + matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ + matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo +matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ + matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ + matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx +matitaScript.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ + matitaEngine.cmi matitaScript.cmi +matitaScript.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \ + matitaEngine.cmx matitaScript.cmi +matitaSync.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ + matitaSync.cmi +matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ + matitaSync.cmi +matitaTypes.cmo: matitaLog.cmi +matitaTypes.cmx: matitaLog.cmx +matitaDisambiguator.cmi: matitaTypes.cmo +matitaEngine.cmi: matitaTypes.cmo +matitaGtkMisc.cmi: matitaGeneratedGui.cmi +matitaGui.cmi: matitaLog.cmi matitaGeneratedGui.cmi matitaDisambiguator.cmi +matitaMisc.cmi: matitaTypes.cmo +matitaScript.cmi: matitaTypes.cmo +matitaSync.cmi: matitaTypes.cmo diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in new file mode 100644 index 000000000..f73436ba0 --- /dev/null +++ b/helm/matita/Makefile.in @@ -0,0 +1,103 @@ + +OCAMLFIND = @OCAMLFIND@ +CAMLP4O = @CAMLP4O@ +LABLGLADECC = @LABLGLADECC@ +REQUIRES = @FINDLIB_REQUIRES@ +CREQUIRES = @FINDLIB_CREQUIRES@ +HAVE_OCAMLOPT = @HAVE_OCAMLOPT@ + +OCAML_FLAGS = -pp $(CAMLP4O) +PKGS = -package "$(REQUIRES)" +CPKGS = -package "$(CREQUIRES)" +OCAML_THREADS_FLAGS = -thread +OCAML_DEBUG_FLAGS = -g +OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) +OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) +OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) +# objects for matita (GTK GUI) +CMOS = \ + buildTimeConf.cmo \ + matitaLog.cmo \ + matitaTypes.cmo \ + matitaMisc.cmo \ + matitaDb.cmo \ + matitaSync.cmo \ + matitaDisambiguator.cmo \ + matitaEngine.cmo \ + matitaScript.cmo \ + matitaGeneratedGui.cmo \ + matitaGtkMisc.cmo \ + matitaGui.cmo \ + matitaMathView.cmo +# objects for matitac (batch compiler) +CCMOS = \ + buildTimeConf.cmo \ + matitaLog.cmo \ + matitaTypes.cmo \ + matitaMisc.cmo \ + matitaDb.cmo \ + matitaSync.cmo \ + matitaDisambiguator.cmo \ + matitaEngine.cmo + +LIB_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES)) + +all: matita matitac cicbrowser + +ifeq ($(HAVE_OCAMLOPT),yes) +CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) +CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) +LIBX_DEPS = $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES)) +opt: matita.opt matitac.opt cicbrowser.opt +else +opt: + @echo "Native code compilation is disabled" +endif + +matita: $(LIB_DEPS) $(CMOS) matita.ml + $(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml +matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml + $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml + +matitac: $(LIB_DEPS) $(CCMOS) matitac.ml + $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) matitac.ml +matitac.opt: $(LIBX_DEPS) $(CMXS) matitac.ml + $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) matitac.ml + +cicbrowser: matita + @test -f $@ || ln -s $< $@ +cicbrowser.opt: matita.opt + @test -f $@ || ln -s $< $@ + +matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade + $(LABLGLADECC) -embed $< > matitaGeneratedGui.ml + $(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli + +%.cmi: %.mli + $(OCAMLC) $(PKGS) -c $< +%.cmo %.cmi: %.ml + $(OCAMLC) $(PKGS) -c $< +%.cmx: %.ml + $(OCAMLOPT) $(PKGS) -c $< +%.annot: %.ml + $(OCAMLC) -dtypes $(PKGS) -c $< + +clean: + rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ + matita matita.opt matitac matitac.opt \ + cicbrowser cicbrowser.opt +distclean: clean + rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli + rm -f config.log config.status Makefile buildTimeConf.ml + rm -f matita.glade.bak matita.gladep.bak + rm -rf autom4te.cache/ + +#.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli +.depend: + $(OCAMLDEP) *.ml *.mli > .depend + +include .depend + +.PHONY: all opt clean distclean depend + diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in new file mode 100644 index 000000000..98c033fdb --- /dev/null +++ b/helm/matita/buildTimeConf.ml.in @@ -0,0 +1,36 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let debug = @DEBUG@;; +let version = "0.0.1";; +let undo_history_size = 10;; +let console_history_size = 100;; +let browser_history_size = 100;; +let gtkrc = "@MATITA_GTKRC@";; +let base_uri = "cic:/matita";; +let phrase_sep = ".";; +let blank_uri = "about:blank";; +let current_proof_uri = "about:current_proof";; + diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac new file mode 100644 index 000000000..32759f12d --- /dev/null +++ b/helm/matita/configure.ac @@ -0,0 +1,104 @@ +AC_INIT(matitaTypes.ml) + +AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no) +if test $HAVE_OCAMLC = "no"; then + AC_MSG_ERROR(could not find ocamlc) +fi +AC_CHECK_PROG(HAVE_OCAMLOPT, ocamlopt, yes, no) +if test $HAVE_OCAMLOPT = "no"; then + AC_MSG_WARN(could not find ocamlopt: native code compilation disabled) +fi +AC_CHECK_PROG(HAVE_OCAMLFIND, ocamlfind, yes, no) +if test $HAVE_OCAMLFIND = "yes"; then + OCAMLFIND="ocamlfind" +else + AC_MSG_ERROR(could not find ocamlfind) +fi +AC_CHECK_PROG(HAVE_LABLGLADECC, lablgladecc2, yes, no) +if test $HAVE_LABLGLADECC = "yes"; then + LABLGLADECC="lablgladecc2" +else + AC_MSG_ERROR(could not find lablgladecc2) +fi +AC_CHECK_PROG(HAVE_CAMLP4O, camlp4o, yes, no) +if test $HAVE_CAMLP4O = "yes"; then + CAMLP4O="camlp4o" +else + AC_MSG_ERROR(could not find camlp4o) +fi + +FINDLIB_CREQUIRES="\ +pcre \ +mysql \ +unix \ +helm-cic_omdoc \ +helm-cic_transformations \ +helm-registry \ +helm-tactics \ +helm-xml \ +helm-cic_textual_parser2 \ +" +FINDLIB_REQUIRES="\ +$FINDLIB_CREQUIRES \ +lablgtk2.glade \ +lablgtkmathview \ +helm-xmldiff \ +" +for r in $FINDLIB_REQUIRES +do + AC_MSG_CHECKING(for $r ocaml library) + if $OCAMLFIND query $r &> /dev/null; then + AC_MSG_RESULT(yes) + else + AC_MSG_ERROR(could not find $r ocaml library) + fi +done + +OCAMLFIND_COMMANDS="" +AC_CHECK_PROG(HAVE_OCAMLC_OPT, ocamlc.opt, yes, no) +if test $HAVE_OCAMLC_OPT = "yes"; then + if test "$OCAMLFIND_COMMANDS" = ""; then + OCAMLFIND_COMMANDS="ocamlc=ocamlc.opt" + else + OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlc=ocamlc.opt" + fi +fi +AC_CHECK_PROG(HAVE_OCAMLOPT_OPT, ocamlopt.opt, yes, no) +if test $HAVE_OCAMLOPT_OPT = "yes"; then + if test "$OCAMLFIND_COMMANDS" = ""; then + OCAMLFIND_COMMANDS="ocamlopt=ocamlopt.opt" + else + OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlopt=ocamlopt.opt" + fi +fi +if test "$OCAMLFIND_COMMANDS" != ""; then + OCAMLFIND="OCAMLFIND_COMMANDS='$OCAMLFIND_COMMANDS' $OCAMLFIND" +fi +AC_ARG_ENABLE(debug, + [ --enable-debug Turn on debugging], + [case "${enableval}" in + yes) DEBUG=true ;; + no) DEBUG=false ;; + *) AC_MSG_ERROR(bad value ${enableval} for --enable-debug) ;; + esac], + [DEBUG=true]) +if test "$DEBUG" = "true"; then + echo "debugging enabled" +fi + +MATITA_GTKRC="matita.gtkrc" + +AC_SUBST(CAMLP4O) +AC_SUBST(DEBUG) +AC_SUBST(TRANSFORMER_MODULE) +AC_SUBST(FINDLIB_REQUIRES) +AC_SUBST(FINDLIB_CREQUIRES) +AC_SUBST(HAVE_OCAMLOPT) +AC_SUBST(LABLGLADECC) +AC_SUBST(OCAMLFIND) +AC_SUBST(MATITA_GTKRC) + +AC_OUTPUT([ + buildTimeConf.ml + Makefile +]) diff --git a/helm/matita/icons/matita-bulb-high.png b/helm/matita/icons/matita-bulb-high.png new file mode 100644 index 000000000..03b6e7f86 Binary files /dev/null and b/helm/matita/icons/matita-bulb-high.png differ diff --git a/helm/matita/icons/matita-bulb-low.png b/helm/matita/icons/matita-bulb-low.png new file mode 100644 index 000000000..f97302e48 Binary files /dev/null and b/helm/matita/icons/matita-bulb-low.png differ diff --git a/helm/matita/icons/matita-bulb-medium.png b/helm/matita/icons/matita-bulb-medium.png new file mode 100644 index 000000000..d3d449f93 Binary files /dev/null and b/helm/matita/icons/matita-bulb-medium.png differ diff --git a/helm/matita/matita.conf.xml b/helm/matita/matita.conf.xml new file mode 100644 index 000000000..93ec8c4b9 --- /dev/null +++ b/helm/matita/matita.conf.xml @@ -0,0 +1,26 @@ + + +
+ true + true + cic:/matita/ + .matita/xml + gares +
+
+ + mowgli.cs.unibo.it + helm + matita +
+
+ true + + file:///projects/helm/library/coq_contribs + + .matita/getter/cache + .matita/getter/maps + /projects/helm/xml/dtd + +
+ diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade new file mode 100644 index 000000000..362c6723a --- /dev/null +++ b/helm/matita/matita.glade @@ -0,0 +1,2744 @@ + + + + + + + Matita: about + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + False + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + <b>Matita @VERSION@</b> + +<tt>http://helm.cs.unibo.it</tt> + +Copyright (C) 2005, +<i>the HELM team</i> + False + True + GTK_JUSTIFY_CENTER + False + False + 0.5 + 0.5 + 5 + 5 + + + 0 + False + False + + + + + + + + 500 + 500 + True + Cic browser + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST + + + + True + True + False + + + + True + False + 0 + + + + True + GTK_SHADOW_OUT + GTK_POS_LEFT + GTK_POS_TOP + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + new browser win + True + True + GTK_RELIEF_NONE + True + + + + True + gtk-new + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + history back + True + True + GTK_RELIEF_NONE + True + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-go-back + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + + + False + False + + + + + + True + True + True + False + + + + True + history forward + True + True + GTK_RELIEF_NONE + True + + + + True + gtk-go-forward + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + refresh + True + True + GTK_RELIEF_NONE + True + + + + True + gtk-refresh + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + home + True + True + GTK_RELIEF_NONE + True + + + + True + gtk-home + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + + + + + False + False + + + + + + True + True + True + False + + + + True + cic uri + True + True + True + 0 + + True + * + False + 34 + + + + + False + False + + + + + + + 0 + False + True + + + + + + True + 0 + 0 + GTK_SHADOW_IN + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + + + + + + 0 + True + True + + + + + + + + + + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + False + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + DUMMY + False + False + GTK_JUSTIFY_CENTER + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + True + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + DUMMY + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + + + + 10 + Select File + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + + + + True + True + True + GTK_RELIEF_NORMAL + True + + + + + + True + True + True + GTK_RELIEF_NORMAL + True + + + + + + 200 + Interpretation choice + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + True + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-help + True + GTK_RELIEF_NORMAL + True + -11 + + + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + False + 0 + + + + True + some informative message here ... + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + + + + + 0 + True + True + + + + + 0 + True + True + + + + + + + + Matita + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + 800 + 600 + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST + + + + True + True + False + + + + True + False + 0 + + + + True + GTK_SHADOW_OUT + GTK_POS_LEFT + GTK_POS_TOP + + + + True + + + + True + _File + True + + + + + + + True + _New + True + + + + True + gtk-new + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + _Open... + True + + + + + True + gtk-open + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + _Save + True + + + + + True + gtk-save + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + Save _As ... + True + + + + True + gtk-save-as + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + + + + + + True + _Quit + True + + + + + True + gtk-quit + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + + + + + True + _Edit + True + + + + + + True + _View + True + + + + + + + True + New Cic Browser + True + + + + + + + + + + + True + Debug + True + + + + + + + True + + + + + + + + + + True + _Help + True + + + + + + + True + About... + True + + + + + + + + + + + 0 + False + False + + + + + + True + False + 0 + + + + True + GTK_SHADOW_OUT + GTK_POS_TOP + GTK_POS_TOP + + + + 102 + True + True + 0 + + + + True + False + 0 + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + 50 + True + Intros + True + intros + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + 50 + True + Apply + True + apply + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + 50 + True + Exact + True + exact + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + 50 + True + Elim + True + elim + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + 50 + True + ElimType + True + elimTy + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + 25 + True + Split + True + ∧ + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + 25 + True + Left + True + L + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + 25 + True + Right + True + R + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + 25 + True + Exists + True + ∃ + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + + True + False + 0 + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + 50 + True + Reflexivity + True + refl + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + 50 + True + Symmetry + True + sym + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + 50 + True + Transitivity + True + trans + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + 0 + False + False + + + + + + True + False + 0 + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + 50 + True + Simplify + True + simpl + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + 50 + True + Reduce + True + red + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + 50 + True + Whd + True + whd + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + 50 + True + Assumption + True + asum + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + 50 + True + Auto + True + auto + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + 50 + True + Cut + True + cut + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + 50 + True + Replace + True + repl + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + + + + + 0 + False + False + + + + + + True + True + + + + 400 + True + False + 0 + + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + True + restart + True + GTK_RELIEF_NONE + True + + + + True + gtk-goto-top + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + go back 1 phrase + True + GTK_RELIEF_NONE + True + + + + True + gtk-go-up + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + execute until point + True + GTK_RELIEF_NONE + True + + + + True + gtk-jump-to + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + go forward 1 phrase + True + GTK_RELIEF_NONE + True + + + + True + gtk-go-down + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + + True + True + True + False + + + + True + execute all + True + GTK_RELIEF_NONE + True + + + + True + gtk-goto-bottom + 4 + 0.5 + 0.5 + 0 + 0 + + + + + + + False + False + + + + + 0 + False + False + + + + + + True + True + True + True + GTK_POS_BOTTOM + False + False + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + True + True + False + True + GTK_JUSTIFY_LEFT + GTK_WRAP_NONE + True + 0 + 0 + 0 + 0 + 0 + 0 + + + + + + False + True + + + + + + True + script + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + + + + + False + True + + + + + + True + outline + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + + + + 0 + True + True + + + + + True + False + + + + + + 450 + 500 + True + True + 450 + + + + True + True + True + True + GTK_POS_TOP + False + False + + + True + False + + + + + + True + False + 0 + + + + True + True + GTK_POLICY_NEVER + GTK_POLICY_ALWAYS + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + True + GTK_JUSTIFY_LEFT + GTK_WRAP_CHAR + False + 0 + 0 + 0 + 0 + 0 + 0 + + + + + + 0 + True + True + + + + + True + True + + + + + False + True + + + + + 0 + True + True + + + + + 0 + True + True + + + + + + True + False + 0 + + + + True + True + + + 0 + True + True + + + + + + True + False + True + GTK_POS_TOP + False + False + + + + True + 0.5 + 0.5 + 0 + 0 + + + False + True + + + + + + True + label14 + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + + + + + True + 0.5 + 0.5 + 0 + 0 + + + False + True + + + + + + True + label15 + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + + + + + True + 0.5 + 0.5 + 0 + 0 + + + False + True + + + + + + True + label16 + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + + + + 0 + False + True + + + + + 0 + False + False + + + + + + + + + + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + True + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + DUMMY + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + True + False + True + GTK_JUSTIFY_LEFT + GTK_WRAP_NONE + True + 0 + 0 + 0 + 0 + 0 + 0 + + + + + + 0 + True + True + + + + + + + + 280 + Uri choice + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + GTK_RELIEF_NORMAL + True + 0 + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-index + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + Try _Selected + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + + + + True + False + True + True + Try Constants + True + GTK_RELIEF_NORMAL + True + 0 + + + + + + True + True + True + GTK_RELIEF_NORMAL + True + 0 + + + + True + 0.5 + 0.5 + 0 + 0 + 0 + 0 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-ok + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + _Auto + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + False + 0 + + + + True + some informative message here ... + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + + + + + 0 + True + True + + + + + + True + False + 0 + + + + True + URI: + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + True + True + True + 0 + + True + * + False + + + 0 + True + True + + + + + 0 + False + True + + + + + 0 + True + True + + + + + + + diff --git a/helm/matita/matita.gtkrc b/helm/matita/matita.gtkrc new file mode 100644 index 000000000..91081c311 --- /dev/null +++ b/helm/matita/matita.gtkrc @@ -0,0 +1,80 @@ +# Based on /usr/share/themes/Emacs/gtk-2.0-key/, +# modified by Zack for matita + +# +# A keybinding set implementing emacs-like keybindings +# + +# +# Bindings for GtkTextView and GtkEntry +# +binding "gtk-emacs-text-entry" +{ + bind "b" { "move-cursor" (logical-positions, -1, 0) } + bind "b" { "move-cursor" (logical-positions, -1, 1) } + bind "f" { "move-cursor" (logical-positions, 1, 0) } + bind "f" { "move-cursor" (logical-positions, 1, 1) } + + bind "b" { "move-cursor" (words, -1, 0) } + bind "b" { "move-cursor" (words, -1, 1) } + bind "f" { "move-cursor" (words, 1, 0) } + bind "f" { "move-cursor" (words, 1, 1) } + + bind "a" { "move-cursor" (paragraph-ends, -1, 0) } + bind "a" { "move-cursor" (paragraph-ends, -1, 1) } + bind "e" { "move-cursor" (paragraph-ends, 1, 0) } + bind "e" { "move-cursor" (paragraph-ends, 1, 1) } + + bind "w" { "cut-clipboard" () } + bind "y" { "paste-clipboard" () } + + bind "d" { "delete-from-cursor" (chars, 1) } + bind "d" { "delete-from-cursor" (word-ends, 1) } + bind "k" { "delete-from-cursor" (paragraph-ends, 1) } + bind "backslash" { "delete-from-cursor" (whitespace, 1) } + + bind "space" { "delete-from-cursor" (whitespace, 1) + "insert-at-cursor" (" ") } + bind "KP_Space" { "delete-from-cursor" (whitespace, 1) + "insert-at-cursor" (" ") } + + # + # Some non-Emacs keybindings people are attached to + # + bind "u" { + "move-cursor" (paragraph-ends, -1, 0) + "delete-from-cursor" (paragraph-ends, 1) + } + bind "h" { "delete-from-cursor" (chars, -1) } + bind "w" { "delete-from-cursor" (word-ends, -1) } +} + +# +# Bindings for GtkTextView +# +binding "gtk-emacs-text-view" +{ +# bind "p" { "move-cursor" (display-lines, -1, 0) } + bind "p" { "move-cursor" (display-lines, -1, 1) } +# bind "n" { "move-cursor" (display-lines, 1, 0) } + bind "n" { "move-cursor" (display-lines, 1, 1) } + + bind "space" { "set-anchor" () } + bind "KP_Space" { "set-anchor" () } +} + +# +# Bindings for GtkTreeView +# +binding "gtk-emacs-tree-view" +{ + bind "s" { "start-interactive-search" () } + bind "f" { "move-cursor" (logical-positions, 1) } + bind "b" { "move-cursor" (logical-positions, -1) } +} + +class "GtkEntry" binding "gtk-emacs-text-entry" +class "GtkTextView" binding "gtk-emacs-text-entry" +class "GtkTextView" binding "gtk-emacs-text-view" +class "GtkTreeView" binding "gtk-emacs-tree-view" + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml new file mode 100644 index 000000000..078ba00db --- /dev/null +++ b/helm/matita/matita.ml @@ -0,0 +1,150 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +open MatitaGtkMisc +open MatitaTypes +open MatitaMisc + +(** {2 Initialization} *) + +let _ = + Helm_registry.load_from "matita.conf.xml"; (* read conf *) + Http_getter.init (); + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + MatitaDb.clean_owner_environment (); + MatitaDb.create_owner_environment (); + GtkMain.Rc.add_default_file BuildTimeConf.gtkrc; (* loads gtk rc files *) + ignore (GMain.Main.init ()); + + (* environment trust *) + CicEnvironment.set_trust + (let trust = Helm_registry.get_bool "matita.environment_trust" in + fun _ -> trust) + +(** {2 GUI callbacks} *) + +let gui = MatitaGui.instance () + +let _ = + ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ -> + ignore (MatitaMathView.cicBrowser ()))); + (* disambiguator callback *) + MatitaDisambiguator.set_choose_uris_callback + (MatitaGui.interactive_uri_choice ()); + MatitaDisambiguator.set_choose_interp_callback + (MatitaGui.interactive_interp_choice ()) + +let script = + MatitaScript.script ~buffer:gui#main#scriptTextView#buffer + ~init:(Lazy.force MatitaEngine.initial_status) () + + (* math viewers *) +let _ = + let sequent_viewer = MatitaMathView.sequentViewer_instance () in + let sequents_viewer = MatitaMathView.sequentsViewer_instance () in + sequent_viewer#set_href_callback + (Some (fun uri -> (MatitaMathView.cicBrowser ())#loadUri uri)); + let browser_observer _ = MatitaMathView.refresh_all_browsers () in + let sequents_observer status = + sequents_viewer#reset; + match status.proof_status with + | Incomplete_proof ((proof, goal) as status) -> + sequents_viewer#load_sequents status; + sequents_viewer#goto_sequent goal + | _ -> () + in + script#addObserver sequents_observer; + script#addObserver browser_observer + + (** *) +let _ = + if BuildTimeConf.debug then begin + gui#main#debugMenu#misc#show (); + let addDebugItem ~label callback = + let item = + GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label () + in + ignore (item#connect#activate callback) + in + addDebugItem "dump environment to \"env.dump\"" (fun _ -> + let oc = open_out "env.dump" in + CicEnvironment.dump_to_channel oc; + close_out oc); + addDebugItem "print selected terms" (fun () -> + let i = ref 0 in + List.iter + (fun t -> + incr i; + MatitaLog.debug (sprintf "%d: %s" !i (CicPp.ppterm t))) + (MatitaMathView.sequentViewer_instance ())#get_selected_terms); + addDebugItem "dump getter settings" (fun _ -> + prerr_endline (Http_getter_env.env_to_string ())); + addDebugItem "getter: update" + (fun _ -> + ignore (Thread.create (fun () -> + MatitaLog.message "Rebuilding getter maps in background ..."; + Http_getter.update (); + MatitaLog.message "Getter maps successfully rebuilt.") ())); + addDebugItem "getter: getalluris" (fun _ -> + List.iter prerr_endline (Http_getter.getalluris ())); + addDebugItem "dump script status" script#dump; + addDebugItem "dump metasenv" + (fun _ -> + if script#onGoingProof () then + MatitaLog.debug (CicMetaSubst.ppmetasenv script#proofMetasenv [])); + addDebugItem "rotate light bulbs" + (fun _ -> + let nb = gui#main#hintNotebook in + nb#goto_page ((nb#current_page + 1) mod 3)); + end + + (** *) + +let _ = + at_exit + (fun () -> + Http_getter_logger.log "Sync map tree to disk..."; + Http_getter.sync_dump_file (); + print_endline "\nThanks for using Matita!\n"); + Sys.catch_break true; + (try + script#loadFrom Sys.argv.(1); + with Invalid_argument _ -> ()); + if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *) + Helm_registry.set "matita.mode" "cicbrowser"; + let browser = MatitaMathView.cicBrowser () in + try + browser#loadUri Sys.argv.(1) + with Invalid_argument _ -> () + end else begin (* matita *) + Helm_registry.set "matita.mode" "matita"; + gui#main#mainWin#show (); + end; + try + GtkThread.main () + with Sys.Break -> () + diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt new file mode 100644 index 000000000..30a8b5355 --- /dev/null +++ b/helm/matita/matita.txt @@ -0,0 +1,165 @@ + +(**********************************************************************) + +TODO +- implementare macro in matitaScript.ml (check, hint, ..) -> Gares +- script outline -> Zack +- cicBrowser: riagganciare(?) resa di termini scritti + nella URL(??) -> +- menu contestuale (tasto dx) nel sequent viewer -> +- controllo per script modificato o meno prima di uscire -> +- riattaccare hbugs (brrr...) -> Zack +- spostare il codice di creazione delle tabelle da + MatitaDb, al momento quelle create da matita possono + andare out of sync con quelle create dai file .sql + +DONE +- tree update in background -> Gares +- update del getter in background -> Zack +- agganciare href_callback del sequent_viewer -> Zack +- shortcut varie per script handling -> Zack +- operazioni rimanenti su script (top, bottom, jump) -> Zack +- lighting-ls-getter in matita -> Gares +- riagganciare toolbar -> Zack +- evitare che n-mila tattiche Goal siano nello script + (una per ogni cambio di tab) -> Zack +- implementazione comandi rimanenti in matitaEngine.ml -> Gares +- sintassi per gli alias -> Gares +- implementazione script handling (sopra engine) -> Zack +- matitaSync all'indietro -> Gares +- riagganciare GUI -> Zack + +(**********************************************************************) + +comandi: + - interattivi (solo da gui) + - Macro/Comandi (check, print, hint, undo, locate, match) + potrebbero anche non avere sintassi concreta, del tipo che + check e' solo un bottone che apre una finetra in cui puoi + scrivere un termine o selezionarlo dalla prova corrente + - batch (sono gli unici che stanno nel .ma) + - Tattiche, theorem, alias (cambiano la prova) + + + MOUSE +-------------------------------------------+ + gui (macro: hint) | SHELL + (disambiguatore) | + +-----------------+---------------+----------------------------------- + | matita (status) | | matitac + | (log) (sync) | but2log | fold ( fun s l -> engine l s) file + +-----------------+---------------+----------------------------------- + | lingua:/sintassi concreta non ambigua delle tattiche+Qed,Thm,alias/ + +---------------------------------------------------------- + | engine: TacticAst (cic) -> status -> status + | ma non usa il campo alias dello status +---------+---------------------------------------------------------- + ocaml +-------------------------------------------------------------------- + + +engine: + - accetta solo linee non ambigue + - alias: + alias ident nat = "cic:/matita/gares/nat.ind#(1/1)". + alias number = (natural|real|positive|integer). + + + +matita: + - mantiene uno stack di stati + - mantiene un log sync con gli stati + - offre delle api per generare la sintassi concreta che puo' servire + alla gui (la gui fa una chiamata a funzione e matita genera "auto." + cosi' la sintassi la gui non la vede mai e la tratta al massimo come un + testo semplice e basta (insomma, metterei in matita il generatore di + sintassi concreta) but2log + - ha il controllo... ovvero anche la gui viene usata da matita, o per sapere + la prossima azione o per chidere di scegliere il termine tra una lista + + (stato :: tl) (log , (start,end) :: tl) + + +----------+ + | | + +----------+ + +gui: + - step + - choose + +stato: + - alias + - proof status option + - metadati relativi allo script per il sync + - settings "baseuri/url/" eccc + - + +alias + - sintassi concreta + +engine prende in input + - AST di Cic (tactic ast) + +sync: + - presi 2 stati fa il diff e lo somma/sottrae al DB + +(**********************************************************************) + +script handling +- ad ogni script sul quale l'utente sta lavorando corrispondono + - un modello (vedi sotto) + - un buffer di testo gtk + attributi (usati principalmente per distinguere la + parte di testo immodificabile da quella modificabile) + - una lista di observer che vengono notificati ad ogni cambiamento di stato +- un modello di script e' composto da: + - una lista di stringhe (inizialmente vuota) detta "statement list". Ogni + elemento della lista corrisponde ad uno statement (nel senso di + TacticAst.statement) gia' valutato dall'engine. La parte immodificabile del + buffer di testo corrisponde con le stringhe contenute nella lista + - una lista di stati (inizialmente contenente lo stato vuoto) detta "state + list". Si ha l'invariante che la lunghezza di tale lista e' uguale alla + lunghezza della statements list + 1. Lo stato i-esimo della lista di stati + e' lo stato di matita _prima_ dell'esecuzione dell i-esimo statement + - una stringa, detta "future text", corrispondente alla parte di testo dello + script non ancora valutata. L'ultimo stato della state list e' lo stato + corrente di matita +- relazione tra modello e buffer di testo gtk + - le modifiche al testo del buffer sono possibili solo nella parta non ancora + valutata. Ognuna di esse viene apportata _anche_ al future text + - invariante: e' sempre possibile riscrivere ("redraw") l'intero contenuto del + buffer di testo a partire dal modello, attributi compresi +- oggetto script + - metodi + - new: gtk_text_buffer -> script + - redraw: unit (* ridisegna il contenuto del buffer di testo *) + - advance: ?statement:string -> unit -> unit + (* valuta il primo statement del future text (usando eval_statement + (puo' fallire con una eccezione)), rimuove il testo corrispondente dal + future text, aggiunge alla statement list una entry per ogni statement + ritornato da eval_statement, aggiunge il nuovo stato alla state list, + invoka tutti gli observer + Se c'e' l'argomento opzionale statement, quello e' il testo che viene + passato ad eval_statement, se ha successo nessuna rimozione dal future + text viene effettuata *) + - retract: unit -> unit + (* sposta l'ultimo statement della statement list al future text, toglie + l'ultimo stato della state list, MatitaSync.time_travel + ~present:ultimo_stato ~past:stato_precedente *) + - private eval_statement: string -> MatitaTypes.status * string list + (* parsa lo statement + - se e' un Command o un Tactical (vedi TacticAst) invoca MatitaEngine + passando lo stato corrente + - se e' una Macro la gestisce (= tutte le Macro sono implementate qua) + Ritorna una lista di coppie . La proiezione sulla + prima componente rappresenta gli stati da aggiungere alla state list; + quella sulla seconda gli statement da aggiungere alla statement list. + *) + (* gestione degli observer *) + - add_observer: (MatitaTypes.status -> unit) -> observer_id + - remove_observer: observer_id -> unit + (* gestione del salvataggio *) + - save_to: string -> unit (* ridisegna su file *) + - load_from: string -> unit + (* retract fino allo stato zero, nuovo stato con future text pari al + contenuto del file passato *) + diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml new file mode 100644 index 000000000..93a1abaa5 --- /dev/null +++ b/helm/matita/matitaDb.ml @@ -0,0 +1,198 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf ;; + +let instance = + let dbd = lazy ( + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + ()) + in + fun () -> Lazy.force dbd + + +let xpointer_RE = Pcre.regexp "#.*$" + +let clean_owner_environment () = + let dbd = instance () in + let owner = (Helm_registry.get "matita.owner") in + let obj_tbl = MetadataTypes.obj_tbl () in + let sort_tbl = MetadataTypes.sort_tbl () in + let rel_tbl = MetadataTypes.rel_tbl () in + let name_tbl = MetadataTypes.name_tbl () in + let conclno_tbl = MetadataTypes.conclno_tbl () in + let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in + let statements = [ + sprintf "DROP TABLE %s ;" obj_tbl; + sprintf "DROP TABLE %s ;" sort_tbl; + sprintf "DROP TABLE %s ;" rel_tbl; + sprintf "DROP TABLE %s ;" name_tbl; + sprintf "DROP TABLE %s ;" conclno_tbl; + sprintf "DROP TABLE %s ;" conclno_hyp_tbl ] in +(* +DROP INDEX refObj_source ON refObj (source); +DROP INDEX refObj_target ON refObj (h_occurrence); +DROP INDEX refObj_position ON refObj (h_position); +DROP INDEX refSort_source ON refSort (source); +DROP INDEX objectName_value ON objectName (value); +DROP INDEX no_inconcl_aux_source ON no_inconcl_aux (source); +DROP INDEX no_inconcl_aux_no ON no_inconcl_aux (no); +DROP INDEX no_concl_hyp_source ON no_concl_hyp (source); +DROP INDEX no_concl_hyp_no ON no_concl_hyp (no); +*) + let owned_uris = + try + MetadataDb.clean ~dbd + with Mysql.Error _ as exn -> + match Mysql.errno dbd with + | Mysql.No_such_table -> [] + | _ -> raise exn + in + List.iter + (fun uri -> + let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in + List.iter + (fun suffix -> Http_getter.unregister (uri ^ suffix)) + [""; ".body"; ".types"]) + owned_uris; + List.iter (fun statement -> + try + ignore (Mysql.exec dbd statement) + with Mysql.Error _ as exn -> + match Mysql.errno dbd with + | Mysql.Bad_table_error -> () + | _ -> raise exn + ) statements; +;; + +let create_owner_environment () = + let dbd = instance () in + let owner = (Helm_registry.get "matita.owner") in + let obj_tbl = MetadataTypes.obj_tbl () in + let sort_tbl = MetadataTypes.sort_tbl () in + let rel_tbl = MetadataTypes.rel_tbl () in + let name_tbl = MetadataTypes.name_tbl () in + let conclno_tbl = MetadataTypes.conclno_tbl () in + let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in + let statements = [ + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + h_occurrence varchar(255) binary not null, + h_position varchar(255) binary not null, + h_depth integer + );" obj_tbl; + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + h_position varchar(255) binary not null, + h_depth integer not null, + h_sort varchar(255) binary not null + );" sort_tbl; + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + h_position varchar(255) binary not null, + h_depth integer not null + );" rel_tbl; + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + value varchar(255) binary not null + );" name_tbl; + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + no tinyint(4) not null + );" conclno_tbl; + sprintf "CREATE TABLE %s ( + source varchar(255) binary not null, + no tinyint(4) not null + );" conclno_hyp_tbl ] in +(* +CREATE INDEX refObj_source ON refObj (source); +CREATE INDEX refObj_target ON refObj (h_occurrence); +CREATE INDEX refObj_position ON refObj (h_position); +CREATE INDEX refSort_source ON refSort (source); +CREATE INDEX objectName_value ON objectName (value); +CREATE INDEX no_inconcl_aux_source ON no_inconcl_aux (source); +CREATE INDEX no_inconcl_aux_no ON no_inconcl_aux (no); +CREATE INDEX no_concl_hyp_source ON no_concl_hyp (source); +CREATE INDEX no_concl_hyp_no ON no_concl_hyp (no); +*) + List.iter (fun statement -> + try + ignore (Mysql.exec dbd statement) + with + exn -> + let status = Mysql.status dbd in + match status with + | Mysql.StatusError Mysql.Table_exists_error -> () + | Mysql.StatusError _ -> raise exn + | _ -> () + ) statements +;; + +(* removes uri from the ownerized tables, and returns the list of other objects + * (theyr uris) that ref the one removed. + * AFAIK there is no need to return it, since the MatitaTypes.staus should + * contain all defined objects. but to double ckeck we do not garbage the + * metadata... + *) +let remove_uri uri = + let obj_tbl = MetadataTypes.obj_tbl () in + let sort_tbl = MetadataTypes.sort_tbl () in + let rel_tbl = MetadataTypes.rel_tbl () in + let name_tbl = MetadataTypes.name_tbl () in + let conclno_tbl = MetadataTypes.conclno_tbl () in + let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in + let dbd = instance () in + let suri = UriManager.string_of_uri uri in + let query table suri = sprintf + "DELETE FROM %s WHERE source LIKE '%s%%'" table (Mysql.escape suri) + in + List.iter (fun t -> + try + ignore (Mysql.exec dbd (query t suri)) + with + exn -> raise exn (* no errors should be accepted *) + ) [obj_tbl;sort_tbl;rel_tbl;name_tbl;conclno_tbl;conclno_hyp_tbl]; + (* and now the debug job *) + let dbg_q = + sprintf "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri + in + try + let rc = Mysql.exec dbd dbg_q in + let l = ref [] in + Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l); + let l = List.sort Pervasives.compare !l in + let rec uniq = function + | [] -> [] + | h::[] -> [h] + | h1::h2::tl when h1 = h2 -> uniq (h2 :: tl) + | h1::tl (* when h1 <> h2 *) -> h1 :: uniq tl + in + uniq l + with + exn -> raise exn (* no errors should be accepted *) + diff --git a/helm/matita/matitaDb.mli b/helm/matita/matitaDb.mli new file mode 100644 index 000000000..112b2d0b2 --- /dev/null +++ b/helm/matita/matitaDb.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val instance: unit -> Mysql.dbd + +val clean_owner_environment : unit -> unit +val create_owner_environment : unit -> unit + +val remove_uri: UriManager.uri -> string list diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml new file mode 100644 index 000000000..fcbcdea14 --- /dev/null +++ b/helm/matita/matitaDisambiguator.ml @@ -0,0 +1,65 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +open MatitaTypes + +exception Ambiguous_input + +type choose_uris_callback = id:string -> string list -> string list +type choose_interp_callback = (string * string) list list -> int list + +let mono_uris_callback ~id = raise Ambiguous_input +let mono_interp_callback _ = raise Ambiguous_input + +let _choose_uris_callback = ref mono_uris_callback +let _choose_interp_callback = ref mono_interp_callback +let set_choose_uris_callback f = _choose_uris_callback := f +let set_choose_interp_callback f = _choose_interp_callback := f + +module Callbacks = + struct + let interactive_user_uri_choice ~selection_mode ?ok + ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = + !_choose_uris_callback ~id uris + + let interactive_interpretation_choice interp = + !_choose_interp_callback interp + + let input_or_locate_uri ~(title:string) ?id = + (* Zack: I try to avoid using this callback. I therefore assume that + * the presence of an identifier that can't be resolved via "locate" + * query is a syntax error *) + let msg = match id with Some id -> id | _ -> "_" in + raise (Unbound_identifier msg) + end + +module Disambiguator = Disambiguate.Make (Callbacks) + +(* implement module's API *) + +let disambiguate_term = Disambiguator.disambiguate_term + diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli new file mode 100644 index 000000000..6d251cc7a --- /dev/null +++ b/helm/matita/matitaDisambiguator.mli @@ -0,0 +1,54 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open MatitaTypes + +(** raised when ambiguous input is found but not expected (e.g. in the batch + * compiler) *) +exception Ambiguous_input + +type choose_uris_callback = id:string -> string list -> string list +type choose_interp_callback = (string * string) list list -> int list + +val set_choose_uris_callback: choose_uris_callback -> unit +val set_choose_interp_callback: choose_interp_callback -> unit + +(** @raise Ambiguous_input if called, default value for internal + * choose_uris_callback if not set otherwise with set_choose_uris_callback + * above *) +val mono_uris_callback: choose_uris_callback + +(** @raise Ambiguous_input if called, default value for internal + * choose_interp_callback if not set otherwise with set_choose_interp_callback + * above *) +val mono_interp_callback: choose_interp_callback + +(** for GUI callbacks see MatitaGui.interactive_{interp,user_uri}_choice *) + +include Disambiguate.Disambiguator + (* + * val disambiguate_term: ... + *) + diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml new file mode 100644 index 000000000..f3ac49e16 --- /dev/null +++ b/helm/matita/matitaEngine.ml @@ -0,0 +1,479 @@ + +open Printf + +open MatitaTypes + + +(** create a ProofEngineTypes.mk_fresh_name_type function which uses given + * names as long as they are available, then it fallbacks to name generation + * using FreshNamesGenerator module *) +let namer_of names = + let len = List.length names in + let count = ref 0 in + fun metasenv context name ~typ -> + if !count < len then begin + let name = Cic.Name (List.nth names !count) in + incr count; + name + end else + FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ + +let tactic_of_ast = function + | TacticAst.Intros (_, _, names) -> + (* TODO Zack implement intros length *) + PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () + | TacticAst.Reflexivity _ -> Tactics.reflexivity + | TacticAst.Assumption _ -> Tactics.assumption + | TacticAst.Contradiction _ -> Tactics.contradiction + | TacticAst.Exists _ -> Tactics.exists + | TacticAst.Fourier _ -> Tactics.fourier + | TacticAst.Goal (_, n) -> Tactics.set_goal n + | TacticAst.Left _ -> Tactics.left + | TacticAst.Right _ -> Tactics.right + | TacticAst.Ring _ -> Tactics.ring + | TacticAst.Split _ -> Tactics.split + | TacticAst.Symmetry _ -> Tactics.symmetry + | TacticAst.Transitivity (_, term) -> Tactics.transitivity term + | TacticAst.Apply (_, term) -> Tactics.apply term + | TacticAst.Absurd (_, term) -> Tactics.absurd term + | TacticAst.Exact (_, term) -> Tactics.exact term + | TacticAst.Cut (_, term) -> Tactics.cut term + | TacticAst.Elim (_, term, _) -> + (* TODO Zack implement "using" argument *) + Tactics.elim_intros_simpl term + | TacticAst.ElimType (_, term) -> Tactics.elim_type term + | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what +(* | TacticAst.Auto _ -> Tactics.auto_new ~dbd *) + | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what +(* + (* TODO Zack a lot more of tactics to be implemented here ... *) + | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option + | TacticAst.Change of 'term * 'term * 'ident option + | TacticAst.Decompose of 'ident * 'ident list + | TacticAst.Discriminate of 'ident + | TacticAst.Fold of reduction_kind * 'term + | TacticAst.Injection of 'ident + | TacticAst.LetIn of 'term * 'ident + | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option + | TacticAst.Replace_pattern of 'term pattern * 'term + | TacticAst.Rewrite of direction * 'term * 'ident option +*) + | _ -> assert false + +let eval_tactical status tac = + let apply_tactic tactic = + let (proof, goals) = + ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status) + in + let new_status = + match goals with + | [] -> + let (_,metasenv,_,_) = proof in + (match metasenv with + | [] -> Proof proof + | (ng,_,_)::_ -> Incomplete_proof (proof,ng)) + | ng::_ -> Incomplete_proof (proof, ng) + in + { status with proof_status = new_status } + in + let rec tactical_of_ast = function + | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic + | TacticAst.Fail loc -> Tacticals.fail + | TacticAst.Do (loc, num, tactical) -> + Tacticals.do_tactic num (tactical_of_ast tactical) + | TacticAst.IdTac loc -> Tacticals.id_tac + | TacticAst.Repeat (loc, tactical) -> + Tacticals.repeat_tactic (tactical_of_ast tactical) + | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) + Tacticals.seq (List.map tactical_of_ast tacticals) + | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) + Tacticals.thens (tactical_of_ast tactical) + (List.map tactical_of_ast tacticals) + | TacticAst.Tries (loc, tacticals) -> + Tacticals.try_tactics + (List.map (fun t -> "", tactical_of_ast t) tacticals) + | TacticAst.Try (loc, tactical) -> + Tacticals.try_tactic (tactical_of_ast tactical) + in + apply_tactic (tactical_of_ast tac) + +let eval_command status cmd = + match cmd with + | TacticAst.Set (loc, name, value) -> set_option status name value + | TacticAst.Qed loc -> + let uri, metasenv, bo, ty = + match status.proof_status with + | Proof (Some uri, metasenv, body, ty) -> + uri, metasenv, body, ty + | Proof (None, metasenv, body, ty) -> + command_error + ("Someone allows to start a thm without giving the "^ + "name/uri. This should be fixed!") + | _-> command_error "You can't qed an uncomplete theorem" + in + let suri = UriManager.string_of_uri uri in + if metasenv <> [] then + command_error "Proof not completed! metasenv is not empty!"; + let proved_ty,ugraph = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph + in + let b,ugraph = + CicReduction.are_convertible [] proved_ty ty ugraph + in + if not b then + command_error + ("The type of your proof is not convertible with the "^ + "type you've declared!"); + MatitaLog.message (sprintf "%s defined" suri); + let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in + {status with proof_status = No_proof } + | TacticAst.Inductive (loc, dummy_params, types) -> + (* dummy_params are not real params, it is a list of nothing, and the only + * semantic content is the len, that is leftno (note: leftno and pamaters + * have nothing in common). + *) + let suri = + match types with + | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind" + | _ -> assert false + in + let uri = UriManager.uri_of_string suri in + let leftno = List.length dummy_params in + let obj = Cic.InductiveDefinition (types, [], leftno, []) in + let ugraph = + CicTypeChecker.typecheck_mutual_inductive_defs uri + (types, [], leftno) CicUniv.empty_ugraph + in + MatitaSync.add_inductive_def + ~uri ~types ~params:[] ~leftno ~ugraph status; + | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) -> + let uri = + UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") + in + let goalno = 1 in + let metasenv, body = + match status.proof_status with + | Intermediate metasenv -> + ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[]) + | _-> assert false + in + let initial_proof = (Some uri, metasenv, body, ty) in + { status with proof_status = Incomplete_proof (initial_proof,goalno)} + | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) -> + let uri = + UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") + in + let metasenv = MatitaMisc.get_proof_metasenv status in + let (body_type, ugraph) = + CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph + in + let (subst, metasenv, ugraph) = + CicUnification.fo_unif metasenv [] body_type ty ugraph + in + if metasenv <> [] then + command_error + "metasenv not empty while giving a definition with body"; + let body = CicMetaSubst.apply_subst subst body in + let ty = CicMetaSubst.apply_subst subst ty in + MatitaSync.add_constant ~uri ~body ~ty ~ugraph status + | TacticAst.Theorem (_, _, None, _, _) -> + command_error "The grammas should avoid having unnamed theorems!" + | TacticAst.Coercion (loc, term) -> assert false (** TODO *) + | TacticAst.Alias (loc, spec) -> + match spec with + | TacticAst.Ident_alias (id,uri) -> + {status with aliases = + DisambiguateTypes.Environment.add + (DisambiguateTypes.Id id) + ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri)) + status.aliases } + | TacticAst.Symbol_alias (symb, instance, desc) -> + {status with aliases = + DisambiguateTypes.Environment.add + (DisambiguateTypes.Symbol (symb,instance)) + (DisambiguateChoices.lookup_symbol_by_dsc symb desc) + status.aliases } + | TacticAst.Number_alias (instance,desc) -> + {status with aliases = + DisambiguateTypes.Environment.add + (DisambiguateTypes.Num instance) + (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases } + +let eval status st = + match st with + | TacticAst.Tactical (_, tac) -> eval_tactical status tac + | TacticAst.Command (_, cmd) -> eval_command status cmd + | TacticAst.Macro (_, mac) -> + command_error (sprintf "The macro %s can't be in a script" + (TacticAstPp.pp_macro_cic mac)) + +let disambiguate_term status term = + let (aliases, metasenv, cic, _) = + match + MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) + ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status) + ~metasenv:(MatitaMisc.get_proof_metasenv status) term + with + | [x] -> x + | _ -> assert false + in + let proof_status = + match status.proof_status with + | No_proof -> Intermediate metasenv + | Incomplete_proof ((uri, _, proof, ty), goal) -> + Incomplete_proof ((uri, metasenv, proof, ty), goal) + | Intermediate _ -> Intermediate metasenv + | Proof _ -> assert false + in + let status = + { status with + aliases = aliases; + proof_status = proof_status } + in + status, cic + +let disambiguate_terms status terms = + let term = CicAst.pack terms in + let status, term = disambiguate_term status term in + status, CicUtil.unpack term + +let disambiguate_tactic status = function + | TacticAst.Transitivity (loc, term) -> + let status, cic = disambiguate_term status term in + status, TacticAst.Transitivity (loc, cic) + | TacticAst.Apply (loc, term) -> + let status, cic = disambiguate_term status term in + status, TacticAst.Apply (loc, cic) + | TacticAst.Absurd (loc, term) -> + let status, cic = disambiguate_term status term in + status, TacticAst.Absurd (loc, cic) + | TacticAst.Exact (loc, term) -> + let status, cic = disambiguate_term status term in + status, TacticAst.Exact (loc, cic) + | TacticAst.Cut (loc, term) -> + let status, cic = disambiguate_term status term in + status, TacticAst.Cut (loc, cic) + | TacticAst.Elim (loc, term, Some term') -> + let status, cic1 = disambiguate_term status term in + let status, cic2 = disambiguate_term status term' in + status, TacticAst.Elim (loc, cic1, Some cic2) + | TacticAst.Elim (loc, term, None) -> + let status, cic = disambiguate_term status term in + status, TacticAst.Elim (loc, cic, None) + | TacticAst.ElimType (loc, term) -> + let status, cic = disambiguate_term status term in + status, TacticAst.ElimType (loc, cic) + | TacticAst.Replace (loc, what, with_what) -> + let status, cic1 = disambiguate_term status what in + let status, cic2 = disambiguate_term status with_what in + status, TacticAst.Replace (loc, cic1, cic2) + | TacticAst.Change (loc, what, with_what, ident) -> + let status, cic1 = disambiguate_term status what in + let status, cic2 = disambiguate_term status with_what in + status, TacticAst.Change (loc, cic1, cic2, ident) +(* + (* TODO Zack a lot more of tactics to be implemented here ... *) + | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option + | TacticAst.Change of 'term * 'term * 'ident option + | TacticAst.Decompose of 'ident * 'ident list + | TacticAst.Discriminate of 'ident + | TacticAst.Fold of reduction_kind * 'term + | TacticAst.Injection of 'ident + | TacticAst.LetIn of 'term * 'ident + | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option + | TacticAst.Replace_pattern of 'term pattern * 'term + | TacticAst.Rewrite of direction * 'term * 'ident option +*) + | TacticAst.Intros (loc, num, names) -> + status, TacticAst.Intros (loc, num, names) + | TacticAst.Auto loc -> status, TacticAst.Auto loc + | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc + | TacticAst.Assumption loc -> status, TacticAst.Assumption loc + | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc + | TacticAst.Exists loc -> status, TacticAst.Exists loc + | TacticAst.Fourier loc -> status, TacticAst.Fourier loc + | TacticAst.Left loc -> status, TacticAst.Left loc + | TacticAst.Right loc -> status, TacticAst.Right loc + | TacticAst.Ring loc -> status, TacticAst.Ring loc + | TacticAst.Split loc -> status, TacticAst.Split loc + | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc + | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g) + | x -> + print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x); + assert false + +let rec disambiguate_tactical status = function + | TacticAst.Tactic (loc, tactic) -> + let status, tac = disambiguate_tactic status tactic in + status, TacticAst.Tactic (loc, tac) + | TacticAst.Do (loc, num, tactical) -> + let status, tac = disambiguate_tactical status tactical in + status, TacticAst.Do (loc, num, tac) + | TacticAst.Repeat (loc, tactical) -> + let status, tac = disambiguate_tactical status tactical in + status, TacticAst.Repeat (loc, tac) + | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) + let status, tacticals = disambiguate_tacticals status tacticals in + let tacticals = List.rev tacticals in + status, TacticAst.Seq (loc, tacticals) + | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) + let status, tactical = disambiguate_tactical status tactical in + let status, tacticals = disambiguate_tacticals status tacticals in + status, TacticAst.Then (loc, tactical, tacticals) + | TacticAst.Tries (loc, tacticals) -> + let status, tacticals = disambiguate_tacticals status tacticals in + status, TacticAst.Tries (loc, tacticals) + | TacticAst.Try (loc, tactical) -> + let status, tactical = disambiguate_tactical status tactical in + status, TacticAst.Try (loc, tactical) + | (TacticAst.IdTac _ | TacticAst.Fail _) as tac -> + status, tac + +and disambiguate_tacticals status tacticals = + let status, tacticals = + List.fold_left + (fun (status, tacticals) tactical -> + let status, tac = disambiguate_tactical status tactical in + status, tac :: tacticals) + (status, []) + tacticals + in + let tacticals = List.rev tacticals in + status, tacticals + +let disambiguate_inddef status params indTypes = + let add_pi binders t = + List.fold_right + (fun (name, ast) acc -> + CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc)) + binders t + in + let ind_binders = + List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes + in + let binders = ind_binders @ params in + let asts = ref [] in + let add_ast ast = asts := ast :: !asts in + let paramsno = List.length params in + let indbindersno = List.length ind_binders in + List.iter + (fun (name, _, typ, constructors) -> + add_ast (add_pi params typ); + List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors) + indTypes; + let status, terms = disambiguate_terms status !asts in + let terms = ref (List.rev terms) in + let get_term () = + match !terms with [] -> assert false | hd :: tl -> terms := tl; hd + in + let uri = + match indTypes with + | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind" + | _ -> assert false + in + let mutinds = + let counter = ref 0 in + List.map + (fun _ -> + incr counter; + CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter)) + indTypes + in + let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in + let cicIndTypes = + List.fold_left + (fun acc (name, inductive, typ, constructors) -> + let cicTyp = get_term () in + let cicConstructors = + List.fold_left + (fun acc (name, _) -> + let typ = + subst_mutinds (CicUtil.strip_prods indbindersno (get_term ())) + in + (name, typ) :: acc) + [] constructors + in + (name, inductive, cicTyp, List.rev cicConstructors) :: acc) + [] indTypes + in + let cicIndTypes = List.rev cicIndTypes in + status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno)) + +let disambiguate_command status = function + | TacticAst.Inductive (loc, params, types) -> + let (status, (uri, (ind_types, vars, paramsno))) = + disambiguate_inddef status params types + in + let rec mk_list = function + | 0 -> [] + | n -> ("", Cic.Rel ~-117) :: mk_list (n-1) + in + (* once we've built the cic inductive types we no longer need terms + corresponding to parameters, but we need the leftno, and we encode + it as the length of dummy_params + *) + let dummy_params = mk_list paramsno in + status, TacticAst.Inductive (loc, dummy_params, ind_types) + | TacticAst.Theorem (loc, thm_flavour, name, ty, body) -> + let status, ty = disambiguate_term status ty in + let status, body = + match body with + | None -> status, None + | Some body -> + let status, body = disambiguate_term status body in + status, Some body + in + status, TacticAst.Theorem (loc, thm_flavour, name, ty, body) + | TacticAst.Coercion (loc, term) -> assert false (** TODO *) + | (TacticAst.Set _ | TacticAst.Qed _) as cmd -> + status, cmd + | TacticAst.Alias _ as x -> status, x + +let disambiguate_statement status statement = + match statement with + | TacticAst.Tactical (loc, tac) -> + let status, tac = disambiguate_tactical status tac in + status, (TacticAst.Tactical (loc, tac)) + | TacticAst.Command (loc, cmd) -> + let status, cmd = disambiguate_command status cmd in + status, (TacticAst.Command (loc, cmd)) + | TacticAst.Macro (_, mac) -> + command_error + (sprintf ("The engine is not allowed to disambiguate any macro, "^^ + "in particular %s") (TacticAstPp.pp_macro_ast mac)) + +let eval_ast status ast = + let status,st = disambiguate_statement status ast in + (* this disambiguation step should be deferred to support tacticals *) + eval status st + +let eval_from_stream status str = + let st = CicTextualParser2.parse_statement str in + eval_ast status st + +let eval_string status str = + eval_from_stream status (Stream.of_string str) + +let default_options () = + let options = + StringMap.add "baseuri" + (String + (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner")) + no_options + in + let options = + StringMap.add "basedir" + (String (Helm_registry.get "matita.basedir" )) + options + in + options + +let initial_status = + lazy { + aliases = DisambiguateTypes.empty_environment; + proof_status = No_proof; + options = default_options (); + coercions = []; + objects = []; + } + diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli new file mode 100644 index 000000000..3fcc4cc3e --- /dev/null +++ b/helm/matita/matitaEngine.mli @@ -0,0 +1,41 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(*val eval_ast:*) + +val eval_string: MatitaTypes.status -> string -> MatitaTypes.status + +val eval_from_stream: MatitaTypes.status -> char Stream.t -> MatitaTypes.status + +val eval_ast: + MatitaTypes.status -> (CicAst.term, string) TacticAst.statement -> + MatitaTypes.status + +val eval: + MatitaTypes.status -> (Cic.term, string) TacticAst.statement -> + MatitaTypes.status + +val initial_status: MatitaTypes.status lazy_t + diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml new file mode 100644 index 000000000..274ee123a --- /dev/null +++ b/helm/matita/matitaGtkMisc.ml @@ -0,0 +1,165 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +open MatitaTypes + +let wrap_callback f = f +(* +let wrap_callback f () = + try + f () + with exn -> + MatitaLog.error (sprintf "Uncaught exception: %s" (Printexc.to_string exn)) +*) + +let connect_button (button: #GButton.button) callback = + ignore (button#connect#clicked (wrap_callback callback)) + +let connect_menu_item (menu_item: #GMenu.menu_item) callback = + ignore (menu_item#connect#activate (wrap_callback callback)) + +let connect_key (ev:GObj.event_ops) ?(modifiers = []) ?(stop = false) key + callback += + ignore (ev#connect#key_press (fun key' -> + let modifiers' = GdkEvent.Key.state key' in + (match key' with + | key' when GdkEvent.Key.keyval key' = key + && List.for_all (fun m -> List.mem m modifiers') modifiers -> + callback (); + stop + | _ -> false))) + +let toggle_visibility ~(win: GWindow.window) ~(check: GMenu.check_menu_item) = + ignore (check#connect#toggled (fun _ -> + if check#active then win#show () else win#misc#hide ())); + ignore (win#event#connect#delete (fun _ -> + win#misc#hide (); + check#set_active false; + true)) + +let toggle_win ?(check: GMenu.check_menu_item option) (win: GWindow.window) () = + if win#is_active then win#misc#hide () else win#show (); + match check with + | None -> () + | Some check -> check#set_active (not check#active) + +let add_key_binding key callback (evbox: GBin.event_box) = + ignore (evbox#event#connect#key_press (function + | key' when GdkEvent.Key.keyval key' = key -> + callback (); + false + | _ -> false)) + +class stringListModel (tree_view: GTree.view) = + let column_list = new GTree.column_list in + let text_column = column_list#add Gobject.Data.string in + let list_store = GTree.list_store column_list in + object (self) + + initializer + let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in + let view_column = GTree.view_column ~renderer () in + tree_view#set_model (Some (list_store :> GTree.model)); + ignore (tree_view#append_column view_column) + + method list_store = list_store + + method easy_append s = + let tree_iter = list_store#append () in + list_store#set ~row:tree_iter ~column:text_column s + + method easy_insert pos s = + let tree_iter = list_store#insert pos in + list_store#set ~row:tree_iter ~column:text_column s + + method easy_selection () = + List.map + (fun tree_path -> + let iter = list_store#get_iter tree_path in + list_store#get ~row:iter ~column:text_column) + tree_view#selection#get_selected_rows + + end + +class type gui = + object + method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog + method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog + method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog + method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog + end + +let ask_confirmation ~(gui:#gui) ?(cancel = true) ?(title = "") ?(msg = "") () = + let dialog = gui#newConfirmationDialog () in + dialog#confirmationDialog#set_title title; + dialog#confirmationDialogLabel#set_label msg; + let result = ref None in + let return r _ = + result := Some r; + dialog#confirmationDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#confirmationDialogOkButton (return true); + connect_button dialog#confirmationDialogCancelButton (return false); + if not cancel then dialog#confirmationDialogCancelButton#misc#hide (); + dialog#confirmationDialog#show (); + GtkThread.main (); + (match !result with None -> assert false | Some r -> r) + +let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () = + let dialog = gui#newEmptyDialog () in + dialog#emptyDialog#set_title title; + dialog#emptyDialogLabel#set_label msg; + let result = ref None in + let return r = + result := r; + dialog#emptyDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#emptyDialog#event#connect#delete (fun _ -> true)); + if multiline then begin (* multiline input required: use a TextView widget *) + let win = + GBin.scrolled_window ~width:400 ~height:150 ~hpolicy:`NEVER + ~vpolicy:`ALWAYS ~packing:dialog#emptyDialogVBox#add () + in + let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in + view#misc#grab_focus (); + connect_button dialog#emptyDialogOkButton (fun _ -> + return (Some (view#buffer#get_text ()))) + end else begin (* monoline input required: use a TextEntry widget *) + let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in + entry#misc#grab_focus (); + connect_button dialog#emptyDialogOkButton (fun _ -> + return (Some entry#text)) + end; + connect_button dialog#emptyDialogCancelButton (fun _ ->return None); + dialog#emptyDialog#show (); + GtkThread.main (); + (match !result with None -> raise Cancel | Some r -> r) + diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli new file mode 100644 index 000000000..23f820f86 --- /dev/null +++ b/helm/matita/matitaGtkMisc.mli @@ -0,0 +1,96 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(** {2 Gtk helpers} *) + + (** given a window and a check menu item it links the two so that the former + * is only hidden on delete and the latter toggle show/hide of the former *) +val toggle_visibility: + win:GWindow.window -> check:GMenu.check_menu_item -> unit + +val toggle_win: + ?check:GMenu.check_menu_item -> GWindow.window -> unit -> unit + +val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit + +(** Connect a callback to the clicked signal of a button, ignoring its return + * value *) +val connect_button: #GButton.button -> (unit -> unit) -> unit + +(** Like connect_button above, but connects a callback to the activate signal of + * a menu item *) +val connect_menu_item: #GMenu.menu_item -> (unit -> unit) -> unit + + (** connect a unit -> unit callback to a particular key press event. Event can + * be specified using its keysym and a list of modifiers which must be in + * effect for the callback to be executed. Further signal processing of other + * key press events remains unchanged; further signal processing of the + * specified key press depends on the stop parameter *) +val connect_key: + GObj.event_ops -> + ?modifiers:Gdk.Tags.modifier list -> + ?stop:bool -> (* stop signal handling when the given key has been pressed? + * Defaults to false *) + Gdk.keysym -> (* (= int) the key, see GdkKeysyms.ml *) + (unit -> unit) -> (* callback *) + unit + + (** single string column list *) +class stringListModel: + GTree.view -> + object + method list_store: GTree.list_store (** list_store forwarding *) + + method easy_append: string -> unit (** append + set *) + method easy_insert: int -> string -> unit (** insert + set *) + method easy_selection: unit -> string list + end + +(** {2 Matita GUI components} *) + +class type gui = + object (* minimal gui object requirements *) + method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog + method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog + method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog + method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog + end + + (** {3 Dialogs} *) + + (** @return true if user hit "ok" button, false if user hit "cancel" button + * @param cancel if set to true a cancel button is shown to the user, otherwise + * it is not (and indeed the function will return true). Defaults to true *) +val ask_confirmation: + gui:#gui -> + ?cancel:bool -> ?title:string -> ?msg:string -> unit -> + bool + + (** @param multiline (default: false) if true a TextView widget will be used + * for prompting the user otherwise a TextEntry widget will be + * @return the string given by the user *) +val ask_text: + gui:#gui -> ?title:string -> ?msg:string -> ?multiline:bool -> unit -> string + diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml new file mode 100644 index 000000000..5a6377b3b --- /dev/null +++ b/helm/matita/matitaGui.ml @@ -0,0 +1,437 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +open MatitaGeneratedGui +open MatitaGtkMisc +open MatitaMisc + +let gui_instance = ref None ;; + +class console ~(buffer: GText.buffer) () = + object (self) + val error_tag = buffer#create_tag [ `FOREGROUND "red" ] + val warning_tag = buffer#create_tag [ `FOREGROUND "yellow" ] + val message_tag = buffer#create_tag [] + val debug_tag = buffer#create_tag [ `FOREGROUND "#888888" ] + method message s = buffer#insert ~iter:buffer#end_iter ~tags:[message_tag] s + method error s = buffer#insert ~iter:buffer#end_iter ~tags:[error_tag] s + method warning s = buffer#insert ~iter:buffer#end_iter ~tags:[warning_tag] s + method debug s = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s + method clear () = + buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter + method log_callback (tag: MatitaLog.log_tag) s = + match tag with + | `Debug -> self#debug (s ^ "\n") + | `Error -> self#error (s ^ "\n") + | `Message -> self#message (s ^ "\n") + | `Warning -> self#warning (s ^ "\n") + end + +class gui () = + (* creation order _is_ relevant for windows placement *) + let main = new mainWin () in + let about = new aboutWin () in + let fileSel = new fileSelectionWin () in + let keyBindingBoxes = (* event boxes which should receive global key events *) + [ main#mainWinEventBox ] + in + let console = new console ~buffer:main#logTextView#buffer () in + object (self) + val mutable chosen_file = None + val mutable _ok_not_exists = false + + initializer + (* glade's check widgets *) + List.iter (fun w -> w#check_widgets ()) + (let c w = (w :> unit>) in + [ c about; c fileSel; c main ]); + (* key bindings *) + List.iter (* global key bindings *) + (fun (key, callback) -> self#addKeyBinding key callback) +(* + [ GdkKeysyms._F3, + toggle_win ~check:main#showProofMenuItem proof#proofWin; + GdkKeysyms._F4, + toggle_win ~check:main#showCheckMenuItem check#checkWin; +*) + [ ]; + (* about win *) + ignore (about#aboutWin#event#connect#delete (fun _ -> true)); + ignore (main#aboutMenuItem#connect#activate (fun _ -> + about#aboutWin#show ())); + connect_button about#aboutDismissButton (fun _ -> + about#aboutWin#misc#hide ()); + about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@" + ~templ:BuildTimeConf.version about#aboutLabel#label); + (* file selection win *) + ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true)); + ignore (fileSel#fileSelectionWin#connect#response (fun event -> + let return r = + chosen_file <- r; + fileSel#fileSelectionWin#misc#hide (); + GMain.Main.quit () + in + match event with + | `OK -> + let fname = fileSel#fileSelectionWin#filename in + if Sys.file_exists fname then + (if is_regular fname then return (Some fname)) + else + (if _ok_not_exists then return (Some fname)) + | `CANCEL -> return None + | `HELP -> () + | `DELETE_EVENT -> return None)); + (* menus *) + List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ]; + main#helpMenu#set_right_justified true; + (* console *) + let adj = main#logScrolledWin#vadjustment in + ignore (adj#connect#changed + (fun _ -> adj#set_value (adj#upper -. adj#page_size))); + console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version); + (* toolbar *) + let module A = TacticAst in + let hole = CicAst.UserInput in + let loc = CicAst.dummy_floc in + let tac ast _ = + if (MatitaScript.instance ())#onGoingProof () then + (MatitaScript.instance ())#advance + ~statement:("\n" ^ TacticAstPp.pp_tactical (A.Tactic (loc, ast))) () + in + let tac_w_term ast _ = + if (MatitaScript.instance ())#onGoingProof () then + let (buf: GText.buffer) = self#main#scriptTextView#buffer in + buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) + ("\n" ^ TacticAstPp.pp_tactic ast) + in + let tbar = self#main in + connect_button tbar#introsButton (tac (A.Intros (loc, None, []))); + connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole))); + connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole))); + connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None))); + connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole))); + connect_button tbar#splitButton (tac (A.Split loc)); + connect_button tbar#leftButton (tac (A.Left loc)); + connect_button tbar#rightButton (tac (A.Right loc)); + connect_button tbar#existsButton (tac (A.Exists loc)); + connect_button tbar#reflexivityButton (tac (A.Reflexivity loc)); + connect_button tbar#symmetryButton (tac (A.Symmetry loc)); + connect_button tbar#transitivityButton + (tac_w_term (A.Transitivity (loc, hole))); + connect_button tbar#assumptionButton (tac (A.Assumption loc)); + connect_button tbar#cutButton (tac_w_term (A.Cut (loc, hole))); + connect_button tbar#autoButton (tac (A.Auto loc)); + (* quit *) + self#setQuitCallback (fun () -> exit 0); + (* log *) + MatitaLog.set_log_callback self#console#log_callback; + GtkSignal.user_handler := + (fun exn -> + MatitaLog.error + (sprintf "Uncaught exception: %s" (Printexc.to_string exn))); + (* script *) + let s () = MatitaScript.instance () in + let script_fname = ref None in + let enable_save_to f = + script_fname := Some f; + self#main#saveMenuItem#misc#set_sensitive true + in + let disable_save () = + script_fname := None; + self#main#saveMenuItem#misc#set_sensitive false + in + let loadScript () = + let script = s () in + match self#chooseFile () with + | Some f -> script#reset (); script#loadFrom f; enable_save_to f + | None -> () + in + let saveAsScript () = + let script = s () in + match self#chooseFile ~ok_not_exists:true () with + | Some f -> script#saveTo f; enable_save_to f + | None -> () + in + let saveScript () = + match !script_fname with + | None -> saveAsScript () + | Some f -> (s ())#saveTo f + in + let newScript () = (s ())#reset (); disable_save () in + let cursor () = + let buf = self#main#scriptTextView#buffer in + buf#place_cursor (buf#get_iter_at_mark (`NAME "locked")) + in + let advance _ = (MatitaScript.instance ())#advance (); cursor () in + let retract _ = (MatitaScript.instance ())#retract (); cursor () in + let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in + let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in + let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in + let connect_key sym f = + connect_key self#main#mainWinEventBox#event + ~modifiers:[`CONTROL] ~stop:true sym f; + connect_key self#main#scriptTextView#event + ~modifiers:[`CONTROL] ~stop:true sym f + in + connect_button self#main#scriptAdvanceButton advance; + connect_button self#main#scriptRetractButton retract; + connect_button self#main#scriptTopButton top; + connect_button self#main#scriptBottomButton bottom; + connect_key GdkKeysyms._Down advance; + connect_key GdkKeysyms._Up retract; + connect_key GdkKeysyms._Home top; + connect_key GdkKeysyms._End bottom; + connect_button self#main#scriptJumpButton jump; + connect_menu_item self#main#openMenuItem loadScript; + connect_menu_item self#main#saveMenuItem saveScript; + connect_menu_item self#main#saveAsMenuItem saveAsScript; + connect_menu_item self#main#newMenuItem newScript; + connect_key GdkKeysyms._period + (fun () -> + let buf = self#main#scriptTextView#buffer in + buf#insert ~iter:(buf#get_iter_at_mark `INSERT) ".\n"; + advance ()); + connect_key GdkKeysyms._Return + (fun () -> + let buf = self#main#scriptTextView#buffer in + buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n"; + advance ()); + (* debug menu *) + self#main#debugMenu#misc#hide (); + (* status bar *) + self#main#hintLowImage#set_file "icons/matita-bulb-low.png"; + self#main#hintMediumImage#set_file "icons/matita-bulb-medium.png"; + self#main#hintHighImage#set_file "icons/matita-bulb-high.png"; + (* focus *) + self#main#scriptTextView#misc#grab_focus () + + method console = console + + method about = about + method fileSel = fileSel + method main = main + + method newBrowserWin () = + let win = new browserWin () in + win#check_widgets (); + win + + method newUriDialog () = + let dialog = new uriChoiceDialog () in + dialog#check_widgets (); + dialog + + method newInterpDialog () = + let dialog = new interpChoiceDialog () in + dialog#check_widgets (); + dialog + + method newConfirmationDialog () = + let dialog = new confirmationDialog () in + dialog#check_widgets (); + dialog + + method newEmptyDialog () = + let dialog = new emptyDialog () in + dialog#check_widgets (); + dialog + + method private addKeyBinding key callback = + List.iter (fun evbox -> add_key_binding key callback evbox) + keyBindingBoxes + + method setQuitCallback callback = + ignore (main#toplevel#connect#destroy callback); + ignore (main#quitMenuItem#connect#activate callback); + self#addKeyBinding GdkKeysyms._q callback + + method chooseFile ?(ok_not_exists = false) () = + _ok_not_exists <- ok_not_exists; + fileSel#fileSelectionWin#show (); + GtkThread.main (); + chosen_file + + method askText ?(title = "") ?(msg = "") () = + let dialog = new textDialog () in + dialog#textDialog#set_title title; + dialog#textDialogLabel#set_label msg; + let text = ref None in + let return v = + text := v; + dialog#textDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#textDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#textDialogCancelButton (fun _ -> return None); + connect_button dialog#textDialogOkButton (fun _ -> + let text = dialog#textDialogTextView#buffer#get_text () in + return (Some text)); + dialog#textDialog#show (); + GtkThread.main (); + !text + + end + +let gui () = + let g = new gui () in + gui_instance := Some g; + g + +let instance = singleton gui + +let non p x = not (p x) + +let is_var_uri s = + try + String.sub s (String.length s - 4) 4 = ".var" + with Invalid_argument _ -> false + +let interactive_uri_choice + ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "") + ?(msg = "") ?(nonvars_button = false) () + ~id uris += + let gui = instance () in + let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in + if (selection_mode <> `SINGLE) && + (Helm_registry.get_bool "matita.auto_disambiguation") + then + Lazy.force nonvars_uris + else begin + let dialog = gui#newUriDialog () in + dialog#uriChoiceTreeView#selection#set_mode + (selection_mode :> Gtk.Tags.selection_mode); + let model = new stringListModel dialog#uriChoiceTreeView in + let choices = ref None in + let nonvars = ref false in + dialog#uriChoiceDialog#set_title title; + dialog#uriChoiceLabel#set_text msg; + List.iter model#easy_append uris; + dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; + let return v = + choices := v; + dialog#uriChoiceDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#uriChoiceConstantsButton (fun _ -> + return (Some (Lazy.force nonvars_uris))); + connect_button dialog#uriChoiceAutoButton (fun _ -> + Helm_registry.set_bool "matita.auto_disambiguation" true; + return (Some (Lazy.force nonvars_uris))); + connect_button dialog#uriChoiceSelectedButton (fun _ -> + match model#easy_selection () with + | [] -> () + | uris -> return (Some uris)); + connect_button dialog#uriChoiceAbortButton (fun _ -> return None); + dialog#uriChoiceDialog#show (); + GtkThread.main (); + (match !choices with + | None -> raise MatitaTypes.Cancel + | Some uris -> uris) + end + +class interpModel = + let cols = new GTree.column_list in + let id_col = cols#add Gobject.Data.string in + let dsc_col = cols#add Gobject.Data.string in + let interp_no_col = cols#add Gobject.Data.int in + let tree_store = GTree.tree_store cols in + let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in + let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in + let id_view_col = GTree.view_column ~renderer:id_renderer () in + let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in + fun tree_view choices -> + object + initializer + tree_view#set_model (Some (tree_store :> GTree.model)); + ignore (tree_view#append_column id_view_col); + ignore (tree_view#append_column dsc_view_col); + let name_of_interp = + (* try to find a reasonable name for an interpretation *) + let idx = ref 0 in + fun interp -> + try + List.assoc "0" interp + with Not_found -> + incr idx; string_of_int !idx + in + tree_store#clear (); + let idx = ref ~-1 in + List.iter + (fun interp -> + incr idx; + let interp_row = tree_store#append () in + tree_store#set ~row:interp_row ~column:id_col + (name_of_interp interp); + tree_store#set ~row:interp_row ~column:interp_no_col !idx; + List.iter + (fun (id, dsc) -> + let row = tree_store#append ~parent:interp_row () in + tree_store#set ~row ~column:id_col id; + tree_store#set ~row ~column:dsc_col dsc; + tree_store#set ~row ~column:interp_no_col !idx) + interp) + choices + + method get_interp_no tree_path = + let iter = tree_store#get_iter tree_path in + tree_store#get ~row:iter ~column:interp_no_col + end + +let interactive_interp_choice () choices = + let gui = instance () in + assert (choices <> []); + let dialog = gui#newInterpDialog () in + let model = new interpModel dialog#interpChoiceTreeView choices in + let interp_len = List.length (List.hd choices) in + dialog#interpChoiceDialog#set_title "Interpretation choice"; + dialog#interpChoiceDialogLabel#set_label "Choose an interpretation:"; + let interp_no = ref None in + let return _ = + dialog#interpChoiceDialog#destroy (); + GMain.Main.quit () + in + let fail _ = interp_no := None; return () in + ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#interpChoiceOkButton (fun _ -> + match !interp_no with None -> () | Some _ -> return ()); + connect_button dialog#interpChoiceCancelButton fail; + ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ -> + interp_no := Some (model#get_interp_no path); + return ())); + let selection = dialog#interpChoiceTreeView#selection in + ignore (selection#connect#changed (fun _ -> + match selection#get_selected_rows with + | [path] -> + MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path)); + interp_no := Some (model#get_interp_no path) + | _ -> assert false)); + dialog#interpChoiceDialog#show (); + GtkThread.main (); + (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel) + diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli new file mode 100644 index 000000000..aabcba1e8 --- /dev/null +++ b/helm/matita/matitaGui.mli @@ -0,0 +1,94 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +class type console = +object + method message: string -> unit + method error: string -> unit + method warning: string -> unit + method debug: string -> unit + method clear: unit -> unit + + method log_callback: MatitaLog.log_callback +end + + (** @param fname name of the Glade file describing the GUI *) +class type gui = +object + + method setQuitCallback : (unit -> unit) -> unit + + (** {2 Access to singleton instances of lower-level GTK widgets} *) + + method about : MatitaGeneratedGui.aboutWin + method fileSel : MatitaGeneratedGui.fileSelectionWin + method main : MatitaGeneratedGui.mainWin +(* method toolbar : MatitaGeneratedGui.toolBarWin *) + + method console: console + + (** {2 Dialogs instantiation} + * methods below create a new window on each invocation. You should + * remember to destroy windows after use *) + + method newBrowserWin: unit -> MatitaGeneratedGui.browserWin + method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog + method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog + method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog + method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog + + (** {2 Utility methods} *) + + (** ask the used to choose a file with the file chooser + * @param ok_not_exists if set to true returns also non existent files + * (useful for save). Defaults to false *) + method chooseFile: ?ok_not_exists:bool -> unit -> string option + + (** prompt the user for a (multiline) text entry *) + method askText: ?title:string -> ?msg:string -> unit -> string option + +end + + (** singleton instance of the gui *) +val instance: unit -> gui + + (** {2 Disambiguation callbacks} + * Use singleton gui instance. *) + + (** @param selection_mode selection mode in uri list, default to `MULTIPLE + * @param title window title, defaults to "" + * @param msg message for the user, defaults to "" + * @param nonvars_button enable button to exclude vars?, defaults to false + * @raise MatitaTypes.Cancel *) +val interactive_uri_choice: + ?selection_mode:([`SINGLE|`MULTIPLE]) -> ?title:string -> + ?msg:string -> ?nonvars_button:bool -> unit -> + MatitaDisambiguator.choose_uris_callback + + (** @raise MatitaTypes.Cancel *) +val interactive_interp_choice: + unit -> + MatitaDisambiguator.choose_interp_callback + diff --git a/helm/matita/matitaLog.ml b/helm/matita/matitaLog.ml new file mode 100644 index 000000000..0b55e8318 --- /dev/null +++ b/helm/matita/matitaLog.ml @@ -0,0 +1,50 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +type log_tag = [ `Debug | `Error | `Message | `Warning ] +type log_callback = log_tag -> string -> unit + +let default_callback tag s = + let prefix = + match tag with + | `Message -> "Info: " + | `Warning -> "Warning: " + | `Error -> "Error: " + | `Debug -> "Debug: " + in + print_endline (prefix ^ s); + flush stdout + +let callback = ref default_callback + +let set_log_callback f = callback := f + +let message s = !callback `Message s +let warn s = !callback `Warning s +let error s = !callback `Error s +let debug s = !callback `Debug s + diff --git a/helm/matita/matitaLog.mli b/helm/matita/matitaLog.mli new file mode 100644 index 000000000..8e789a700 --- /dev/null +++ b/helm/matita/matitaLog.mli @@ -0,0 +1,35 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +type log_tag = [ `Debug | `Error | `Message | `Warning ] +type log_callback = log_tag -> string -> unit + +val set_log_callback: log_callback -> unit + +val message : string -> unit +val warn : string -> unit +val error : string -> unit +val debug : string -> unit + diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml new file mode 100644 index 000000000..addf9763c --- /dev/null +++ b/helm/matita/matitaMathView.ml @@ -0,0 +1,513 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +open Printf + +open MatitaTypes + +let list_map_fail f = + let rec aux = function + | [] -> [] + | he::tl -> + try + let he' = f he in + he'::(aux tl) + with Exit -> + (aux tl) + in + aux + +(** inherit from this class if you want to access current script *) +class scriptAccessor = +object (self) + method private script = MatitaScript.instance () +end + +class clickableMathView obj = + let href = Gdome.domString "href" in + let xref = Gdome.domString "xref" in + object (self) + inherit GMathViewAux.multi_selection_math_view obj + + val mutable href_callback: (string -> unit) option = None + method set_href_callback f = href_callback <- f + + initializer + ignore (self#connect#selection_changed self#choose_selection); + ignore (self#connect#click (fun (gdome_elt, _, _, _) -> + match gdome_elt with + | Some elt (* element is an hyperlink, use href_callback on it *) + when elt#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href -> + (match href_callback with + | None -> () + | Some f -> + let uri = + elt#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href + in + f (uri#to_string)) + | Some elt -> ignore (self#action_toggle elt) + | None -> ())) + method private choose_selection gdome_elt = + let rec aux elt = + if elt#hasAttributeNS ~namespaceURI:Misc.helm_ns ~localName:xref then + self#set_selection (Some elt) + else + try + (match elt#get_parentNode with + | None -> assert false + | Some p -> aux (new Gdome.element_of_node p)) + with GdomeInit.DOMCastException _ -> () +(* debug_print "trying to select above the document root" *) + in + match gdome_elt with + | Some elt -> aux elt + | None -> self#set_selection None + end + +let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = + GtkBase.Widget.size_params + ~cont:(OgtkMathViewProps.pack_return (fun p -> + OgtkMathViewProps.set_params + (new clickableMathView (GtkMathViewProps.MathView_GMetaDOM.create p)) + ~font_size:None ~log_verbosity:None)) + [] + +class sequentViewer obj = + object(self) + + inherit clickableMathView obj + + val mutable current_infos = None + + method get_selected_terms = + let selections = self#get_selections in + list_map_fail + (fun node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helm_ns + ~localName:(Gdome.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + match current_infos with + | Some (ids_to_terms,_,_) -> + (try Hashtbl.find ids_to_terms xpath with _ -> raise Exit) + | None -> assert false) (* "ERROR: No current term!!!" *) + selections + + method get_selected_hypotheses = + let selections = self#get_selections in + list_map_fail + (fun node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helm_ns + ~localName:(Gdome.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + match current_infos with + | Some (_,_,ids_to_hypotheses) -> + (try Hashtbl.find ids_to_hypotheses xpath with _ -> raise Exit) + | None -> assert false) (* "ERROR: No current term!!!" *) + selections + + method load_sequent metasenv metano = + let sequent = CicUtil.lookup_meta metano metasenv in + let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) = + ApplyTransformation.mml_of_cic_sequent metasenv sequent + in + current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); +(* + debug_print "load_sequent: dumping MathML to ./prova"; + ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ()); +*) + self#load_root ~root:mathml#get_documentElement + end + +class sequentsViewer ~(notebook:GPack.notebook) + ~(sequentViewer:sequentViewer) () += + object (self) + inherit scriptAccessor + + val mutable pages = 0 + val mutable switch_page_callback = None + val mutable page2goal = [] (* associative list: page no -> goal no *) + val mutable goal2page = [] (* the other way round *) + val mutable goal2win = [] (* associative list: goal no -> scrolled win *) + val mutable _metasenv = [] + val mutable scrolledWin: GBin.scrolled_window option = None + (* scrolled window to which the sequentViewer is currently attached *) + + method private tab_label metano = + (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce + + method reset = + (match scrolledWin with + | Some w -> + (* removing page from the notebook will destroy all contained widget, + * we do not want the sequentViewer to be destroyed as well *) + w#remove sequentViewer#coerce; + scrolledWin <- None + | None -> ()); + for i = 1 to pages do notebook#remove_page 0 done; + pages <- 0; + page2goal <- []; + goal2page <- []; + goal2win <- []; + _metasenv <- []; + self#script#setGoal ~-1; + (match switch_page_callback with + | Some id -> + GtkSignal.disconnect notebook#as_widget id; + switch_page_callback <- None + | None -> ()) + + method load_sequents (status: ProofEngineTypes.status) = + let ((_, metasenv, _, _), goal) = status in + let sequents_no = List.length metasenv in + _metasenv <- metasenv; + pages <- sequents_no; + self#script#setGoal goal; + let win metano = + let w = + GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC + ~shadow_type:`IN ~show:true () + in + let reparent () = + scrolledWin <- Some w; + match sequentViewer#misc#parent with + | None -> w#add sequentViewer#coerce + | Some _ -> sequentViewer#misc#reparent w#coerce + in + goal2win <- (metano, reparent) :: goal2win; + w#coerce + in + let page = ref 0 in + List.iter + (fun (metano, _, _) -> + page2goal <- (!page, metano) :: page2goal; + goal2page <- (metano, !page) :: goal2page; + incr page; + notebook#append_page ~tab_label:(self#tab_label metano) (win metano)) + metasenv; + switch_page_callback <- + Some (notebook#connect#switch_page ~callback:(fun page -> + let goal = + try + List.assoc page page2goal + with Not_found -> assert false + in + self#script#setGoal goal; + self#render_page ~page ~goal)) + + method private render_page ~page ~goal = + sequentViewer#load_sequent _metasenv goal; + try + List.assoc goal goal2win (); + sequentViewer#set_selection None + with Not_found -> assert false + + method goto_sequent goal = + let page = + try + List.assoc goal goal2page + with Not_found -> assert false + in + notebook#goto_page page; + self#render_page page goal + + end + + (** constructors *) + +type 'widget constructor = + ?hadjustment:GData.adjustment -> + ?vadjustment:GData.adjustment -> + ?font_size:int -> + ?log_verbosity:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> + unit -> + 'widget + +let sequentViewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = + GtkBase.Widget.size_params + ~cont:(OgtkMathViewProps.pack_return (fun p -> + OgtkMathViewProps.set_params + (new sequentViewer (GtkMathViewProps.MathView_GMetaDOM.create p)) + ~font_size ~log_verbosity)) + [] + +let blank_uri = BuildTimeConf.blank_uri +let current_proof_uri = BuildTimeConf.current_proof_uri + +type term_source = + [ `Ast of DisambiguateTypes.term + | `Cic of Cic.term * Cic.metasenv + | `String of string + ] + +exception Browser_failure of string + +let cicBrowsers = ref [] + +class type cicBrowser = +object + method loadUri: string -> unit + method loadTerm: term_source -> unit +end + +class cicBrowser_impl ~(history:string MatitaMisc.history) () = + let term_RE = Pcre.regexp "^term:(.*)" in + let trailing_slash_RE = Pcre.regexp "/$" in + let gui = MatitaGui.instance () in + let win = gui#newBrowserWin () in + let toplevel = win#toplevel in + let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in + let fail msg = + ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ()) + ~title:"Cic browser" ~msg ~cancel:false ()); + in + let handle_error f = + try + f () + with exn -> + fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn)) + in + let handle_error' f = fun () -> handle_error f in (* used in callbacks *) + object (self) + inherit scriptAccessor + + initializer + ignore (win#browserUri#connect#activate (handle_error' (fun () -> + self#_loadUri win#browserUri#text))); + ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () -> + self#_loadUri current_proof_uri))); + ignore (win#browserRefreshButton#connect#clicked + (handle_error' self#refresh)); + ignore (win#browserBackButton#connect#clicked (handle_error' self#back)); + ignore (win#browserForwardButton#connect#clicked + (handle_error' self#forward)); + ignore (win#toplevel#event#connect#delete (fun _ -> + let my_id = Oo.id self in + cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers; + if !cicBrowsers = [] && + Helm_registry.get "matita.mode" = "cicbrowser" + then + GMain.quit (); + false)); + mathView#set_href_callback (Some (fun uri -> + handle_error (fun () -> self#_loadUri uri))); + self#_loadUri ~add_to_history:false blank_uri; + toplevel#show (); + + val mutable current_uri = "" + val mutable current_infos = None + val mutable current_mathml = None + + method private back () = + try + self#_loadUri ~add_to_history:false history#previous + with MatitaMisc.History_failure -> () + + method private forward () = + try + self#_loadUri ~add_to_history:false history#next + with MatitaMisc.History_failure -> () + + (* loads a uri which can be a cic uri or an about:* uri + * @param uri string *) + method private _loadUri ?(add_to_history = true) uri = + try + if current_uri <> uri || uri = current_proof_uri then begin + (match uri with + | uri when uri = blank_uri -> self#blank () + | uri when uri = current_proof_uri -> self#home () + | uri when Pcre.pmatch ~rex:term_RE uri -> + self#loadTerm (`String (Pcre.extract ~rex:term_RE uri).(1)) + | uri when Pcre.pmatch ~rex:trailing_slash_RE uri -> self#loadDir uri + | _ -> self#loadUriManagerUri (UriManager.uri_of_string uri)); + self#setUri uri; + if add_to_history then history#add uri + end + with + | UriManager.IllFormedUri _ -> fail (sprintf "invalid uri: %s" uri) + | CicEnvironment.Object_not_found _ -> + fail (sprintf "object not found: %s" uri) + | Browser_failure msg -> fail msg + + method loadUri uri = + handle_error (fun () -> self#_loadUri ~add_to_history:true uri) + + method private blank () = + mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement + + method private home () = + if self#script#onGoingProof () then + let ((uri, metasenv, bo, ty), _) = self#script#proofStatus in + let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in + let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in + self#loadObj obj + else + self#blank () + + (** loads a cic uri from the environment + * @param uri UriManager.uri *) + method private loadUriManagerUri uri = + let uri = UriManager.strip_xpointer uri in + let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + self#loadObj obj + + method private loadDir dir = + let mathml = MatitaMisc.empty_boxml () in + let content = Http_getter.ls dir in + let root = mathml#get_documentElement in + let new_box_elt name = + mathml#createElementNS ~namespaceURI:(Some Misc.boxml_ns) + ~qualifiedName:(Gdome.domString ("b:" ^ name)) + in + let new_text content = mathml#createTextNode (Gdome.domString content) in + let b_v = new_box_elt "v" in + List.iter + (fun item -> + let b_text = new_box_elt "text" in + let uri, elt = + match item with + | Http_getter_types.Ls_section subdir -> + (dir ^ subdir ^ "/"), (new_text (subdir ^ "/")) + | Http_getter_types.Ls_object obj -> + (dir ^ obj.Http_getter_types.uri), + (new_text obj.Http_getter_types.uri) + in + b_text#setAttributeNS ~namespaceURI:(Some Misc.xlink_ns) + ~qualifiedName:(Gdome.domString "xlink:href") + ~value:(Gdome.domString uri); + ignore (b_v#appendChild ~newChild:(b_text :> Gdome.node)); + ignore (b_text#appendChild ~newChild:(elt :> Gdome.node))) + content; + ignore (root#appendChild ~newChild:(b_v :> Gdome.node)); +(* Misc.domImpl#saveDocumentToFile ~doc:mathml ~name:"pippo" (); *) + mathView#load_root ~root:root + + method private setUri uri = + win#browserUri#set_text uri; + current_uri <- uri + + method private loadObj obj = + let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) + let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures, + ids_to_hypotheses,_,_))) = + ApplyTransformation.mml_of_cic_object obj + in + current_infos <- Some (ids_to_terms, ids_to_father_ids, + ids_to_conjectures, ids_to_hypotheses); + match current_mathml with + | Some current_mathml when use_diff -> + mathView#freeze; + XmlDiff.update_dom ~from:current_mathml mathml; + mathView#thaw + | _ -> + mathView#load_root ~root:mathml#get_documentElement; + current_mathml <- Some mathml + + method private _loadTerm s = failwith "not implemented _loadTerm" +(* TODO self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s)) *) + + method private _loadTermAst ast = failwith "not implemented _loadTermAst" +(* TODO + let (_, metasenv, term, _) = + MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast + in + self#_loadTermCic term metasenv +*) + + method private _loadTermCic term metasenv = + let context = self#script#proofContext in + let dummyno = CicMkImplicit.new_meta metasenv [] in + let sequent = (dummyno, context, term) in + mathView#load_sequent (sequent :: metasenv) dummyno + + method loadTerm (src:term_source) = + handle_error (fun () -> + (match src with + | `Ast ast -> self#_loadTermAst ast + | `Cic (cic, metasenv) -> self#_loadTermCic cic metasenv + | `String s -> self#_loadTerm s); + self#setUri "check") + + (** {2 methods used by constructor only} *) + + method win = win + method history = history + method currentUri = current_uri + method refresh () = + if current_uri = current_proof_uri then + self#_loadUri ~add_to_history:false current_proof_uri + + end + +let sequentsViewer ~(notebook:GPack.notebook) + ~(sequentViewer:sequentViewer) () += + new sequentsViewer ~notebook ~sequentViewer () + +let cicBrowser () = + let size = BuildTimeConf.browser_history_size in + let rec aux history = + let browser = new cicBrowser_impl ~history () in + let win = browser#win in + ignore (win#browserNewButton#connect#clicked (fun () -> + let history = + new MatitaMisc.browser_history ~memento:history#save size "" + in + let newBrowser = aux history in + newBrowser#loadUri browser#currentUri)); +(* + (* attempt (failed) to close windows on CTRL-W ... *) + MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL] + GdkKeysyms._W (fun () -> win#toplevel#destroy ()); +*) + cicBrowsers := browser :: !cicBrowsers; + (browser :> cicBrowser) + in + let history = new MatitaMisc.browser_history size blank_uri in + aux history + +let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers + +let default_sequentViewer () = sequentViewer ~show:true () +let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer + +let default_sequentsViewer () = + let gui = MatitaGui.instance () in + let sequentViewer = sequentViewer_instance () in + sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer () +let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer + diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli new file mode 100644 index 000000000..da187a7c5 --- /dev/null +++ b/helm/matita/matitaMathView.mli @@ -0,0 +1,107 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + + (** multi selection gtkMathView which handle mactions and hyperlinks. Mactions + * are handled internally. Hyperlinks are handled by calling an user provided + * callback *) +class type clickableMathView = + object + inherit GMathViewAux.multi_selection_math_view + + (** set hyperlink callback. None disable hyperlink handling *) + method set_href_callback: (string -> unit) option -> unit + end + +class type sequentViewer = + object + inherit clickableMathView + + (** @return the list of selected terms. Selections which are not terms are + * ignored *) + method get_selected_terms: Cic.term list + + (** @return the list of selected hypothese. Selections which are not + * hypotheses are ignored *) + method get_selected_hypotheses: Cic.hypothesis list + + (** load a sequent and render it into parent widget *) + method load_sequent: Cic.metasenv -> int -> unit + end + +class type sequentsViewer = + object + method reset: unit + method load_sequents: ProofEngineTypes.status -> unit + method goto_sequent: int -> unit (* to be called _after_ load_sequents *) + end + +exception Browser_failure of string + +type term_source = + [ `Ast of DisambiguateTypes.term + | `Cic of Cic.term * Cic.metasenv + | `String of string + ] + +class type cicBrowser = +object + method loadUri: string -> unit + method loadTerm: term_source -> unit +end + +(** {2 Constructors} *) + + (** meta constructor *) +type 'widget constructor = + ?hadjustment:GData.adjustment -> + ?vadjustment:GData.adjustment -> + ?font_size:int -> + ?log_verbosity:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> + unit -> + 'widget + +val clickableMathView: clickableMathView constructor + +val sequentViewer: sequentViewer constructor + +val sequentsViewer: + notebook:GPack.notebook -> + sequentViewer:sequentViewer -> + unit -> + sequentsViewer + +val cicBrowser: unit -> cicBrowser + +val refresh_all_browsers: unit -> unit + +(** {2 singleton instances} *) + +val sequentViewer_instance: unit -> sequentViewer +val sequentsViewer_instance: unit -> sequentsViewer + diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml new file mode 100644 index 000000000..58fa38809 --- /dev/null +++ b/helm/matita/matitaMisc.ml @@ -0,0 +1,176 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf +open MatitaTypes + +let is_dir fname = + try + (Unix.stat fname).Unix.st_kind = Unix.S_DIR + with Unix.Unix_error _ -> false + +let is_regular fname = + try + (Unix.stat fname).Unix.st_kind = Unix.S_REG + with Unix.Unix_error _ -> false + +let input_file fname = + let size = (Unix.stat fname).Unix.st_size in + let buf = Buffer.create size in + let ic = open_in fname in + Buffer.add_channel buf ic size; + close_in ic; + Buffer.contents buf + +let is_proof_script fname = true (** TODO Zack *) +let is_proof_object fname = true (** TODO Zack *) + +let append_phrase_sep s = + if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then + s ^ BuildTimeConf.phrase_sep + else + s + +let strip_trailing_blanks = + let rex = Pcre.regexp "\\s*$" in + fun s -> Pcre.replace ~rex s + +let empty_mathml () = + Misc.domImpl#createDocument ~namespaceURI:(Some Misc.mathml_ns) + ~qualifiedName:(Gdome.domString "math") ~doctype:None + +let empty_boxml () = + Misc.domImpl#createDocument ~namespaceURI:(Some Misc.boxml_ns) + ~qualifiedName:(Gdome.domString "box") ~doctype:None + +exception History_failure + +type 'a memento = 'a array * int * int * int (* data, hd, tl, cur *) + +class type ['a] history = + object + method add : 'a -> unit + method next : 'a + method previous : 'a + method load: 'a memento -> unit + method save: 'a memento + end + +class shell_history size = + let size = size + 1 in + let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in + let incr x = (x + 1) mod size in + object (self) + val data = Array.create size "" + val mutable hd = 0 (* insertion point *) + val mutable tl = -1 (* oldest inserted item *) + val mutable cur = -1 (* current item for the history *) + method add s = + data.(hd) <- s; + if tl = -1 then tl <- hd; + hd <- incr hd; + if hd = tl then tl <- incr tl; + cur <- hd + method previous = + if cur = tl then raise History_failure; + cur <- decr cur; + data.(cur) + method next = + if cur = hd then raise History_failure; + cur <- incr cur; + if cur = hd then "" else data.(cur) + method load (data', hd', tl', cur') = + assert (Array.length data = Array.length data'); + hd <- hd'; tl <- tl'; cur <- cur'; + Array.blit data' 0 data 0 (Array.length data') + method save = (Array.copy data, hd, tl, cur) + end + +class ['a] browser_history ?memento size init = + object (self) + initializer match memento with Some m -> self#load m | _ -> () + val data = Array.create size init + val mutable hd = 0 + val mutable tl = 0 + val mutable cur = 0 + method previous = + if cur = tl then raise History_failure; + cur <- cur - 1; + if cur = ~-1 then cur <- size - 1; + data.(cur) + method next = + if cur = hd then raise History_failure; + cur <- cur + 1; + if cur = size then cur <- 0; + data.(cur) + method add (e:'a) = + cur <- cur + 1; + if cur = size then cur <- 0; + if cur = tl then tl <- tl + 1; + if tl = size then tl <- 0; + hd <- cur; + data.(cur) <- e + method load (data', hd', tl', cur') = + assert (Array.length data = Array.length data'); + hd <- hd'; tl <- tl'; cur <- cur'; + Array.blit data' 0 data 0 (Array.length data') + method save = (Array.copy data, hd, tl, cur) + end + +let singleton f = + let instance = lazy (f ()) in + fun () -> Lazy.force instance + +let mkdir d = + let errmsg = sprintf "Unable to create directory \"%s\"" d in + try + (match Unix.system ("mkdir -p " ^ d) with + | Unix.WEXITED 0 -> () + | _ -> failwith errmsg) + with Unix.Unix_error _ -> failwith errmsg + +let get_proof_status status = + match status.proof_status with + | Incomplete_proof s -> s + | _ -> statement_error "no ongoing proof" + +let get_proof_metasenv status = + match status.proof_status with + | No_proof -> [] + | Incomplete_proof ((_, metasenv, _, _), _) -> metasenv + | Proof (_, metasenv, _, _) -> metasenv + | Intermediate m -> m + +let get_proof_context status = + match status.proof_status with + | Incomplete_proof ((_, metasenv, _, _), goal) -> + let (_, context, _) = CicUtil.lookup_meta goal metasenv in + context + | _ -> [] + +let qualify status name = get_string_option status "baseuri" ^ "/" ^ name + +let unopt = function None -> failwith "unopt: None" | Some v -> v + diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli new file mode 100644 index 000000000..1d51eca19 --- /dev/null +++ b/helm/matita/matitaMisc.mli @@ -0,0 +1,86 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val is_dir: string -> bool (** @return true if file is a directory *) +val is_regular: string -> bool (** @return true if file is a regular file *) + +val input_file: string -> string (** read all the contents of file to string *) + + (** @return true if file is a (textual) proof script *) +val is_proof_script: string -> bool + + (** @return true if file is a (binary) proof object *) +val is_proof_object: string -> bool + + (** given a phrase, if it doesn't end with BuildTimeConf.phrase_sep, append + * it *) +val append_phrase_sep: string -> string + +val strip_trailing_blanks: string -> string + + (** @raise Failure *) +val unopt: 'a option -> 'a + + (** Gdome.element of a MathML document whose rendering should be blank. Used + * by cicBrowser to render "about:blank" document *) +val empty_mathml: unit -> Gdome.document +val empty_boxml: unit -> Gdome.document + +exception History_failure + +type 'a memento + +class type ['a] history = + object ('b) + method add : 'a -> unit + method next : 'a (** @raise History_failure *) + method previous : 'a (** @raise History_failure *) + method load: 'a memento -> unit + method save: 'a memento + end + + (** shell like history: new items added at the end of the history + * @param size maximum history size *) +class shell_history : int -> [string] history + + (** browser like history: new items added at the current point of the history + * @param size maximum history size + * @param first element in history (this history is never empty) *) +class ['a] browser_history: ?memento:'a memento -> int -> 'a -> ['a] history + + (** create a singleton from a given function. Given function is invoked the + * first time it gets called. Next invocation will return first value *) +val singleton: (unit -> 'a) -> (unit -> 'a) + + (** create a directory, building also parents if needed + * @raise Failure when unable to create some directory *) +val mkdir: string -> unit + +val qualify: MatitaTypes.status -> string -> string + +val get_proof_status: MatitaTypes.status -> ProofEngineTypes.status +val get_proof_metasenv: MatitaTypes.status -> Cic.metasenv +val get_proof_context: MatitaTypes.status -> Cic.context + diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml new file mode 100644 index 000000000..94a7d1424 --- /dev/null +++ b/helm/matita/matitaScript.ml @@ -0,0 +1,266 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +open MatitaTypes + + (** raised when one of the script margins (top or bottom) is reached *) +exception Margin + +let safe_substring s i j = + try String.sub s i j with Invalid_argument _ -> assert false + +let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*" +let blanks_RE = Pcre.regexp "^\\s*$" + +let first_line s = + let s = Pcre.replace ~rex:heading_nl_RE s in + try + let nl_pos = String.index s '\n' in + String.sub s 0 nl_pos + with Not_found -> s + +let prepend_text header base = + if Pcre.pmatch ~rex:heading_nl_RE base then + sprintf "\n%s%s" header base + else + sprintf "%s\n%s" header base + + (** creates a statement AST for the Goal tactic, e.g. "goal 7" *) +let goal_ast n = + let module A = TacticAst in + let loc = CicAst.dummy_floc in + A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))) + +let eval_statement status user_goal s = + let st = CicTextualParser2.parse_statement (Stream.of_string s) in + match st with + | TacticAst.Command (loc, _) | TacticAst.Tactical (loc, _) -> + let parsed_text_length = snd (CicAst.loc_of_floc loc) in + let parsed_text = safe_substring s 0 parsed_text_length in + let goal_changed = ref false in + let status = + match status.proof_status with + | Incomplete_proof (_, goal) when goal <> user_goal -> + goal_changed := true; + MatitaEngine.eval_ast status (goal_ast user_goal) + | _ -> status + in + let new_status = MatitaEngine.eval_ast status st in + let new_aliases = + match st with + | TacticAst.Command (_, TacticAst.Alias _) -> + DisambiguateTypes.Environment.empty + | _ -> MatitaSync.alias_diff ~from:status new_status + in + let new_text = + if DisambiguateTypes.Environment.is_empty new_aliases then + parsed_text + else + prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases) + parsed_text + in + let new_text = + if !goal_changed then + prepend_text + (TacticAstPp.pp_tactic (TacticAst.Goal (loc, user_goal))(* ^ "\n"*)) + new_text + else + new_text + in + [ new_status, new_text ], parsed_text_length + | TacticAst.Macro (loc, mac) -> + (match mac with (* TODO *) + | _ -> failwith "not implemented") + +class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) () = +object (self) + initializer self#reset () + + val mutable statements = []; (** executed statements *) + val mutable history = [ init ]; + (** list of states before having executed statements. Head element of this + * list is the current state, last element is the state at the beginning of + * the script. + * Invariant: this list length is 1 + length of statements *) + + (** goal as seen by the user (i.e. metano corresponding to current tab) *) + val mutable userGoal = ~-1 + + (** text mark and tag representing locked part of a script *) + val locked_mark = + buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter + val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false] + + (* history can't be empty, the invariant above grant that it contains at + * least the init status *) + method status = match history with hd :: _ -> hd | _ -> assert false + + method private _advance ?statement () = + let s = match statement with Some s -> s | None -> self#getFuture in + if Pcre.pmatch ~rex:blanks_RE s then raise Margin; + MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); + let (entries, parsed_len) = eval_statement self#status userGoal s in + let (new_statuses, new_statements) = List.split entries in +(* +prerr_endline "evalStatement returned"; +List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; +*) + history <- List.rev new_statuses @ history; + statements <- List.rev new_statements @ statements; + let start = buffer#get_iter_at_mark (`MARK locked_mark) in + if statement = None then begin + let stop = start#copy#forward_chars parsed_len in + buffer#delete ~start ~stop + end; + let new_text = String.concat "" new_statements in + buffer#insert ~iter:start new_text; + self#moveMark (String.length new_text); + + method private _retract () = + match statements, history with + | last_statement :: _, cur_status :: prev_status :: _ -> + MatitaSync.time_travel ~present:cur_status ~past:prev_status; + statements <- List.tl statements; + history <- List.tl history; + self#moveMark (- (String.length last_statement)) + | _ -> raise Margin + + method advance ?statement () = + try + self#_advance ?statement () + with Margin -> () + + method retract () = try self#_retract () with Margin -> () + + method private getFuture = + buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark)) + ~stop:buffer#end_iter () + + (** @param rel_offset relative offset from current position of locked_mark *) + method private moveMark rel_offset = + let mark = `MARK locked_mark in + buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; + let current_mark_pos = buffer#get_iter_at_mark mark in + let new_mark_pos = + match rel_offset with + | 0 -> current_mark_pos + | n when n > 0 -> current_mark_pos#forward_chars n + | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n) + in + buffer#move_mark mark ~where:new_mark_pos; + buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos; + self#notify + + val mutable observers = [] + + method addObserver (o: MatitaTypes.status -> unit) = + observers <- o :: observers + + method private notify = + let status = self#status in + List.iter (fun o -> o status) observers + + method loadFrom fname = + buffer#set_text (MatitaMisc.input_file fname); + self#goto_top + + method saveTo fname = + let oc = open_out fname in + output_string oc (buffer#get_text ~start:buffer#start_iter + ~stop:buffer#end_iter ()); + close_out oc + + method private goto_top = + MatitaSync.time_travel ~present:self#status ~past:init; + statements <- []; + history <- [ init ]; + userGoal <- ~-1; + self#notify; + buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; + buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter + + method reset () = + self#goto_top; + buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter + + method goto (pos: [`Top | `Bottom | `Cursor]) () = + match pos with + | `Top -> self#goto_top + | `Bottom -> + (try while true do self#_advance () done with Margin -> ()) + | `Cursor -> + let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in + let cursor_iter () = buffer#get_iter_at_mark `INSERT in + let rec forward_until_cursor () = (* go forward until locked > cursor *) + self#_advance (); + if (locked_iter ())#compare (cursor_iter ()) < 0 then + forward_until_cursor () + in + let rec back_until_cursor () = (* go backward until locked < cursor *) + self#_retract (); + if (locked_iter ())#compare (cursor_iter ()) > 0 then + back_until_cursor () + in + let cmp = (locked_iter ())#compare (cursor_iter ()) in + (try + if cmp < 0 then (* locked < cursor *) + forward_until_cursor () + else if cmp > 0 then (* locked > cursor *) + back_until_cursor () + else (* cursor = locked *) + () + with Margin -> ()) + + method onGoingProof () = + match self#status.proof_status with + | No_proof | Proof _ -> false + | Incomplete_proof _ -> true + | Intermediate _ -> assert false + + method proofStatus = MatitaMisc.get_proof_status self#status + method proofMetasenv = MatitaMisc.get_proof_metasenv self#status + method proofContext = MatitaMisc.get_proof_context self#status + method setGoal n = userGoal <- n + + (* debug *) + method dump () = + MatitaLog.debug "script status:"; + MatitaLog.debug ("history size: " ^ string_of_int (List.length history)); + MatitaLog.debug (sprintf "%d statements:" (List.length statements)); + List.iter MatitaLog.debug statements; + +end + +let _script = ref None + +let script ~buffer ~init () = + let s = new script ~buffer ~init () in + _script := Some s; + s + +let instance () = match !_script with None -> assert false | Some s -> s + diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli new file mode 100644 index 000000000..2529376f1 --- /dev/null +++ b/helm/matita/matitaScript.mli @@ -0,0 +1,71 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +class type script = +object + + (** @return current status *) + method status: MatitaTypes.status + + (** {2 Observers} *) + + method addObserver : (MatitaTypes.status -> unit) -> unit + + (** {2 History} *) + + method advance : ?statement:string -> unit -> unit + method retract : unit -> unit + method goto: [`Top | `Bottom | `Cursor] -> unit -> unit + method reset: unit -> unit + + (** {2 Load/save} *) + + method loadFrom : string -> unit + method saveTo : string -> unit + + (** {2 Current proof} (if any) *) + + (** @return true if there is an ongoing proof, false otherise *) + method onGoingProof: unit -> bool + + method proofStatus: ProofEngineTypes.status (** @raise Statement_error *) + method proofMetasenv: Cic.metasenv (** @raise Statement_error *) + method proofContext: Cic.context (** @raise Statement_error *) + + method setGoal: int -> unit + + (* debug *) + method dump : unit -> unit + +end + +val script: buffer:GText.buffer -> init:MatitaTypes.status -> unit -> script + +(* each time script above is called an internal ref is set, instance will return + * the value of this ref *) +(* TODO Zack: orrible solution until we found a better one for having a single + * access point for the script *) +val instance: unit -> script + diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml new file mode 100644 index 000000000..f14e3d126 --- /dev/null +++ b/helm/matita/matitaSync.ml @@ -0,0 +1,225 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +open MatitaTypes + +let paths_and_uris_of_obj uri status = + let basedir = get_string_option status "basedir" in + let innertypesuri = UriManager.innertypesuri_of_uri uri in + let bodyuri = UriManager.bodyuri_of_uri uri in + let innertypesfilename = Str.replace_first (Str.regexp "^cic:") "" + (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in + let innertypespath = basedir ^ "/" ^ innertypesfilename in + let xmlfilename = Str.replace_first (Str.regexp "^cic:/") "" + (UriManager.string_of_uri uri) ^ ".xml.gz" in + let xmlpath = basedir ^ "/" ^ xmlfilename in + let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") "" + (UriManager.string_of_uri uri) ^ ".body.xml.gz" in + let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in + xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri + +let save_object_to_disk status uri obj = + let ensure_path_exists path = + let dir = Filename.dirname path in + MatitaMisc.mkdir dir + in + (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *) + let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = + Cic2acic.acic_object_of_cic_object ~eta_fix:false obj + in + (* prepare XML *) + let xml, bodyxml = + Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false + annobj + in + let xmlinnertypes = + Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types + ~ask_dtd_to_the_getter:false + in + let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri = + paths_and_uris_of_obj uri status + in + let path_scheme_of path = "file://" ^ path in + List.iter MatitaMisc.mkdir + (List.map Filename.dirname [innertypespath; xmlpath]); + (* now write to disk *) + ensure_path_exists innertypespath; + Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ; + ensure_path_exists xmlpath; + Xml.pp ~gzip:true xml (Some xmlpath) ; + (* now register to the getter *) + Http_getter.register' innertypesuri (path_scheme_of innertypespath); + Http_getter.register' uri (path_scheme_of xmlpath); + (* we return a list of uri,path we registered/created *) + (uri,xmlpath) :: (innertypesuri,innertypespath) :: + (* now the optional body, both write and register *) + (match bodyxml,bodyuri with + None,None -> [] + | Some bodyxml,Some bodyuri-> + ensure_path_exists xmlbodypath; + Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ; + Http_getter.register' bodyuri (path_scheme_of xmlbodypath); + [bodyuri,xmlbodypath] + | _-> assert false) + +let unregister_if_some = function + | Some u -> Http_getter.unregister' u | None -> () + +let remove_object_from_disk uri path = + Sys.remove path; + Http_getter.unregister' uri + +let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status = + let dbd = MatitaDb.instance () in + let suri = UriManager.string_of_uri uri in + if CicEnvironment.in_library uri then + command_error (sprintf "%s constant already defined" suri) + else begin + let name = UriManager.name_of_uri uri in + let obj = Cic.Constant (name, body, ty, params, attrs) in + let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in + CicEnvironment.add_type_checked_term uri (obj, ugraph); + MetadataDb.index_constant ~dbd ~uri ~body ~ty; + let new_stuff = save_object_to_disk status uri obj in + MatitaLog.message (sprintf "%s constant defined" suri); + { status with objects = new_stuff @ status.objects } + end + +let split_obj = function + | Cic.Constant (name, body, ty, _, attrs) + | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs) + | _ -> assert false + +let add_inductive_def + ~uri ~types ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph status += + let dbd = MatitaDb.instance () in + let suri = UriManager.string_of_uri uri in + if CicEnvironment.in_library uri then + command_error (sprintf "%s inductive type already defined" suri) + else begin + let name = UriManager.name_of_uri uri in + let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in + let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in + CicEnvironment.put_inductive_definition uri (obj, ugraph); + MetadataDb.index_inductive_def ~dbd ~uri ~types:types; + let new_stuff = save_object_to_disk status uri obj in + MatitaLog.message (sprintf "%s inductive type defined" suri); + let status = { status with objects = new_stuff @ status.objects } in + let elim sort status = + try + let obj = CicElim.elim_of ~sort uri 0 in + let (name, body, ty, attrs) = split_obj obj in + let suri = MatitaMisc.qualify status name ^ ".con" in + let uri = UriManager.uri_of_string suri in + (* TODO Zack: make CicElim returns a universe *) + let ugraph = CicUniv.empty_ugraph in + add_constant ~uri ?body ~ty ~attrs ~ugraph status; + with CicElim.Can_t_eliminate -> status + in + List.fold_left + (fun status sort -> elim sort status) + status + [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; + end + +module OrderedUri = +struct + type t = UriManager.uri * string + let compare (u1, _) (u2, _) = UriManager.compare u1 u2 +end + +module UriSet = Set.Make (OrderedUri) + +(* returns the uri of objects that were added in the meanwhile... + * status1 ----> status2 + * assumption: objects defined in status2 are a superset of those defined in + * status1 + *) +let delta_status status1 status2 = + let module S = UriSet in + let diff l1 l2 = + let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in + let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in + let diff = S.diff s2 s1 in + S.fold (fun uri uris -> uri :: uris) diff [] + in + diff status1.objects status2.objects + +let time_travel ~present ~past = + let list_of_objs_to_remove = List.rev (delta_status past present) in + (* List.rev is just for the debugging code, which otherwise may list both + * something.ind and something.ind#xpointer ... (ask Enrico :-) *) + let debug_list = ref [] in + List.iter (fun (x,p) -> + remove_object_from_disk x p; + (try + CicEnvironment.remove_obj x + with CicEnvironment.Object_not_found _ -> + MatitaLog.debug + (sprintf "time_travel removes from cache %s that is not in" + (UriManager.string_of_uri x))); + let l = MatitaDb.remove_uri x in + debug_list := UriManager.string_of_uri x :: !debug_list @ l) + list_of_objs_to_remove; + + (* this is debug code + * idea: debug_list is the list of objects to be removed as computed from the + * db, while list_of_objs_to_remove is the same list but computer from the + * differences between statuses *) + let l1 = List.sort Pervasives.compare !debug_list in + let l2 = List.sort Pervasives.compare + (List.map (fun (x,_) -> UriManager.string_of_uri x) list_of_objs_to_remove) + in + let rec uniq = function + | [] -> [] + | h::[] -> [h] + | h1::h2::tl when h1 = h2 -> uniq (h2 :: tl) + | h1::tl (* when h1 <> h2 *) -> h1 :: uniq tl + in + let l1 = uniq l1 in + let l2 = uniq l2 in + try + List.iter2 (fun x y -> if x <> y then raise Exit) l1 l2 + with + | Invalid_argument _ | Exit -> + MatitaLog.debug "It seems you garbaged something..."; + MatitaLog.debug "l1:"; + List.iter MatitaLog.debug l1; + MatitaLog.debug "l2:"; + List.iter MatitaLog.debug l2 + +let alias_diff ~from status = + let module Map = DisambiguateTypes.Environment in + Map.fold + (fun domain_item codomain_item acc -> + if not (Map.mem domain_item from.aliases) then + Map.add domain_item codomain_item acc + else + acc) + status.aliases Map.empty + diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli new file mode 100644 index 000000000..8e85c4186 --- /dev/null +++ b/helm/matita/matitaSync.mli @@ -0,0 +1,49 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val add_constant: + uri:UriManager.uri -> + ?body:Cic.term -> ty:Cic.term -> + ugraph:CicUniv.universe_graph -> + ?params:UriManager.uri list -> ?attrs:Cic.attribute list -> + MatitaTypes.status -> MatitaTypes.status + +val add_inductive_def: + uri:UriManager.uri -> + types:Cic.inductiveType list -> + ?params:UriManager.uri list -> ?leftno:int -> ?attrs:Cic.attribute list -> + ugraph:CicUniv.universe_graph -> + MatitaTypes.status -> MatitaTypes.status + +val time_travel: + present:MatitaTypes.status -> past:MatitaTypes.status -> unit + + (** perform a diff between the aliases contained in two statuses, assuming + * that the second one can only have more aliases than the first one + * @return the list of aliases that should be added to aliases of from in + * order to be equal to aliases of the second argument *) +val alias_diff: from:MatitaTypes.status -> MatitaTypes.status -> + DisambiguateTypes.environment + diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml new file mode 100644 index 000000000..48d419341 --- /dev/null +++ b/helm/matita/matitaTypes.ml @@ -0,0 +1,147 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + + (** user hit the cancel button *) +exception Cancel + + (** statement invoked in the wrong context (e.g. tactic with no ongoing proof) + *) +exception Statement_error of string +let statement_error msg = raise (Statement_error msg) + +exception Command_error of string +let command_error msg = raise (Command_error msg) + + (** parameters are: option name, error message *) +exception Option_error of string * string + +exception Unbound_identifier of string + +type proof_status = + | No_proof + | Incomplete_proof of ProofEngineTypes.status + | Proof of ProofEngineTypes.proof + | Intermediate of Cic.metasenv + (* Status in which the proof could be while it is being processed by the + * engine. No status entering/exiting the engine could be in it. *) + +module StringMap = Map.Make (String) + +type option_value = + | String of string + | Int of int +type options = option_value StringMap.t +let no_options = StringMap.empty + +type status = { + aliases: DisambiguateTypes.environment; (** disambiguation aliases *) + proof_status: proof_status; + options: options; + coercions: CoercGraph.coercions; + objects: (UriManager.uri * string) list; + (** in-scope objects, with their paths *) +} + +let dump_status status = + MatitaLog.message "status.aliases:\n"; + MatitaLog.message + (CicTextualParser2.EnvironmentP3.to_string status.aliases ^ "\n"); + MatitaLog.message "status.proof_status:"; + MatitaLog.message + (match status.proof_status with + | No_proof -> "no proof\n" + | Incomplete_proof _ -> "incomplete proof\n" + | Proof _ -> "proof\n" + | Intermediate _ -> "Intermediate\n"); + MatitaLog.message "status.options\n"; + StringMap.iter (fun k v -> + let v = + match v with + | String s -> s + | Int i -> string_of_int i + in + MatitaLog.message (k ^ "::=" ^ v)) status.options; + MatitaLog.message "status.coercions\n"; + List.iter + (fun (u1,u2,u3) -> MatitaLog.message + ((UriManager.string_of_uri u1) ^ + (UriManager.string_of_uri u2) ^ + (UriManager.string_of_uri u3))) status.coercions; + MatitaLog.message "status.objects:\n"; + List.iter + (fun (u,_) -> + MatitaLog.message (UriManager.string_of_uri u)) status.objects + + +let get_option status name = + try + StringMap.find name status.options + with Not_found -> raise (Option_error (name, "not found")) + +let get_string_option status name = + match get_option status name with + | String s -> s + | _ -> raise (Option_error (name, "not a string value")) + +let set_option status name value = + let mangle_dir s = + let s = Str.global_replace (Str.regexp "//+") "/" s in + let s = Str.global_replace (Str.regexp "/$") "" s in + s + in + let types = + [ "baseuri", (`String, mangle_dir); + "basedir", (`String, mangle_dir); + ] + in + let ty_and_mangler = + try + List.assoc name types + with Not_found -> command_error (sprintf "Unknown option \"%s\"" name) + in + let value = + match ty_and_mangler with + | `String, f -> String (f value) + | `Int, f -> + (try + Int (int_of_string (f value)) + with Failure _ -> + command_error (sprintf "Not an integer value \"%s\"" value)) + in + { status with options = StringMap.add name value status.options } + + (* subset of MatitaConsole.console methods needed by MatitaInterpreter *) +class type console = + object + method clear : unit -> unit + method echo_error : string -> unit + method echo_message : string -> unit + method wrap_exn : 'a. (unit -> 'a) -> 'a option + method choose_uri : string list -> string + method show : ?msg:string -> unit -> unit + end + diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml new file mode 100644 index 000000000..4dbac3653 --- /dev/null +++ b/helm/matita/matitac.ml @@ -0,0 +1,89 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +open MatitaTypes + +(** {2 Initialization} *) + +let arg_spec = [ +(* "-opt", Arg...., "set bla bla bla"; *) +] +let usage = + sprintf "MatitaC v%s\nUsage: matitac [option ...] file ...\nOptions:" + BuildTimeConf.version + +let _ = + Helm_registry.load_from "matita.conf.xml"; + Http_getter.init (); + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + MatitaDb.clean_owner_environment (); + MatitaDb.create_owner_environment () + +let scripts = + let acc = ref [] in + let add_script fname = acc := fname :: !acc in + Arg.parse arg_spec add_script usage; + List.rev !acc + +let run_script fname = + MatitaLog.message (sprintf "execution of %s started:" fname); + let is = + Stream.of_channel + (match fname with + | "stdin" -> stdin + | fname -> open_in fname) + in + let status = ref (Lazy.force MatitaEngine.initial_status) in + try + while true do + dump_status !status; + try + status := MatitaEngine.eval_from_stream !status is + with + | CicTextualParser2.Parse_error _ as exn -> + try + Stream.empty is; + raise End_of_file + with Stream.Failure -> raise exn + | exn -> + MatitaLog.error (Printexc.to_string exn); + raise exn + done + with + | End_of_file -> + MatitaLog.message (sprintf "execution of %s completed." fname); + Http_getter.sync_dump_file (); + exit(0) + | CicTextualParser2.Parse_error (floc,err) -> + let (x, y) = CicAst.loc_of_floc floc in + MatitaLog.message (sprintf "Parse error at %d-%d: %s" x y err); + Http_getter.sync_dump_file (); + exit 1 + + +let _ = List.iter run_script scripts + diff --git a/helm/matita/tests/test1.ma b/helm/matita/tests/test1.ma new file mode 100644 index 000000000..6c3646409 --- /dev/null +++ b/helm/matita/tests/test1.ma @@ -0,0 +1,6 @@ +set "baseuri" "cic:/matita/zack/aaa/". +inductive nat:Set \def O:nat | S:nat \to nat. +set "baseuri" "cic:/matita/zack/bbb/". +inductive nat:Set \def O:nat | S:nat \to nat. +alias id "nat" = "cic:/matita/zack/bbb/nat.ind#xpointer(1/1)". +inductive c:Set \def c1: nat \to c. diff --git a/helm/matita/tests/test2.ma b/helm/matita/tests/test2.ma new file mode 100644 index 000000000..29c694d5f --- /dev/null +++ b/helm/matita/tests/test2.ma @@ -0,0 +1,7 @@ +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias symbol "and" (instance 0) = "logical and". +alias symbol "eq" (instance 0) = "leibnitz's equality". +theorem a:\forall x:nat.x=x\land x=x. +intro. +split. +goal 6. \ No newline at end of file diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma new file mode 100644 index 000000000..c4aafaf3c --- /dev/null +++ b/helm/matita/tests/test3.ma @@ -0,0 +1,8 @@ +alias symbol "eq" (instance 0) = "leibnitz's equality". +theorem a:\forall x.x=x. +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +goal 5. +exact nat. +intro. +reflexivity. +qed. \ No newline at end of file