OMakefile_theories

########################################################################
# Theory building
#

#
# Unset NATIVE_ENABLED if we are in the mixed compilation mode.
#
NATIVE_ENABLED = $(mem $(COMPILATION_MODE), native both)

#
# When using native code profiling, no need to build theories to bytecode.
#
if $(NATIVE_PROFILING_ENABLED)
   BYTE_ENABLED = false
   export

#
# Commands to compile theory files
#
CAMLP5N = $(file $(LIB)/camlp5n$(EXE))
CAMLP5O = $(file $(LIB)/camlp5o$(EXE))
CONVERT = $(file $(BIN)/convert$(EXE))
PRLCN   = $(file $(BIN)/prlcn$(EXE))
PRLCO   = $(file $(BIN)/prlco$(EXE))
MPTIME =
CAMLP5FLAGS[] =

#
# Other helper files
#
declare THEORYDESCR THEORYNAME

include $(MK)/prlcomp

# Dependency analysis uses -prl flag by default
OCAMLDEPFLAGS += -prl

#
# Make sure we do not try falling back to an OCaml rule for an .ml without an .mli
# See also:
#   http://bugzilla.metaprl.org/show_bug.cgi?id=90
#   http://bugzilla.metaprl.org/show_bug.cgi?id=420
#

#
# XXX: JYH: disable this for now.  It is getting applied in too
# many places.
#
%.cmx %.o: %.ml disable-this-rule
   @echo $(quote *** Error: MetaPRL file $(in $(ROOT), $(file $<)) $'does not have
***        a corresponding' $(in $(ROOT), $(file $*.mli)))
   exit 1

#
# Reflected theories
#
reflect_%.ppo reflect_%.cmoz: %.cmoz reflect_%.cmiz $(PRLCN) :optional: reflect_%.prla :effects: reflect_%.prlb :scanner: scan-ocaml-%.ml
   $(WrapC $(PRLCN)) --reflect-impl -o $*.ppo $<

reflect_%.ppi reflect_%.cmiz: %.cmoz $(PRLCN) :scanner: scan-ocaml-%.mli
   $(WrapC $(PRLCN)) --reflect-intf -o $*.ppi $<

reflect_%.p4: %.cmoz reflect_%.cmiz $(PRLCO) :value: $(prlc-deps)
   $(WrapC $(PRLCO)) --reflect-impl -o $@ $(CAMLP5FLAGS) $<

reflect_%.p4i: %.cmoz $(PRLCO) :value: $(prlc-deps)
   $(WrapC $(PRLCO)) --reflect-intf -o $@ $(CAMLP5FLAGS) $<

reflect_%.cmi: reflect_%.ppi :scanner: scan-ocaml-%.ml
   $(OCAMLC) $(OCAMLFLAGS) $(OCAMLCFLAGS) $(PREFIXED_OCAMLINCLUDES) -c -intf $<

reflect_%.cmo: reflect_%.ppo reflect_%.cmi :scanner: scan-ocaml-%.ml
   $(OCAMLC) -intf-suffix .ppi $(OCAMLFLAGS) $(OCAMLCFLAGS) $(PREFIXED_OCAMLINCLUDES) -c -impl $<

reflect_%.cmx reflect_%$(EXT_OBJ): reflect_%.ppo reflect_%.cmi :scanner: scan-ocaml-%.ml
   $(OCAMLOPT) -intf-suffix .ppi $(OCAMLFLAGS) $(OCAMLOPTFLAGS) $(PREFIXED_OCAMLINCLUDES) -c -impl $<

#
# For theory files, generate intermediate .ppo files
#
%.ppo %.cmoz: %.ml %.cmiz :optional: %.prla :effects: %.prlb :scanner: scan-ocaml-%.ml :value: $(prlc-deps)
   $(WrapC $(CAMLP5N)) $(CAMLP5FLAGS) -o $*.ppo $*.ml

%.cmi %.cmiz: %.mli :scanner: scan-ocaml-%.mli
   $(PrlC $(OCAMLC)) $(OCAMLFLAGS) $(OCAMLCFLAGS) $(OCAMLPPFLAGS) $(PREFIXED_OCAMLINCLUDES) -c $<

%.cmo: %.ppo :squash: %.ml :scanner: scan-ocaml-%.ml
   $(OCAMLC) $(OCAMLFLAGS) $(OCAMLCFLAGS) $(PREFIXED_OCAMLINCLUDES) -c -impl $<

%.cmx %$(EXT_OBJ): %.ppo :squash: %.ml :scanner: scan-ocaml-%.ml
   $(OCAMLOPT) $(OCAMLFLAGS) $(OCAMLOPTFLAGS) $(PREFIXED_OCAMLINCLUDES) -c -impl $<

#
# Dependency management
#
if $(SLOPPY_DEPENDENCIES)
   %.cmi %.cmiz:  :squash: $(CAMLP5N)
   %.ppo %.cmoz:  :squash: $(CAMLP5N)

else
   %.cmi %.cmiz: $(CAMLP5N)
   %.ppo %.cmoz: $(CAMLP5N)

%.p4i: %.mli $(CAMLP5O) :value: $(prlc-deps)
   $(WrapC $(CAMLP5O)) $(CAMLP5FLAGS) $*.mli > $@

%.p4: %.ml $(CAMLP5O) :value: $(prlc-deps)
   $(WrapC $(CAMLP5O)) $(CAMLP5FLAGS) $*.ml > $@

if $(SPELLING_ENABLED)
    LIBWORDS = $(file $(addprefix $(LIB)/, $(SPELLING_DICTS)))
    %.ppo: $(LIBWORDS)
    %.p4: $(LIBWORDS)
    export

#
# Add the extra dependencies.  If sloppy dependencies
# is set, squash the dependency chain by using an
# intermediate file.
#
if $(SLOPPY_DEPENDENCIES)
   MPFILTER = $(file .sloppy)
   $(MPFILTER): $(CAMLP5N)
      echo "Sloppy filter dependencies" > $@

   %.cmi %.cmiz: $(MPFILTER)
   %.ppo %.cmoz: $(MPFILTER)

   export
else
   %.cmi %.cmiz: $(CAMLP5N)
   %.ppo %.cmoz: $(CAMLP5N)
   export

########################################################################
# LaTeX documentation
#

#
# Add the inputs directory to the search path.
#
INPUTSDIR = $(dir doc/latex/inputs)
TEXINPUTS += $(INPUTSDIR)

#
# Directory that store the .ps and .pdf files
#
DOCDIR = $(dir doc/ps/theories)

#
# Assume these files are always dependencies.
#
TEXDEPS += $(file $(INPUTSDIR)/rc.bib $(INPUTSDIR)/metaprl.tex)

#
# MetaPRL command
#
MP_SCRIPT = $(file $(EDITOR)/mp$(if $(equal $(OSTYPE), Win32), .bat))
MP_BIN = $(file $(EDITOR)/mp.$(if $(NATIVE_ENABLED), opt, top))

MP_DIRECT_SCRIPTS[] =

if $(NATIVE_ENABLED)
    MP_DIRECT_SCRIPTS[] +=
        mpopt
    export

if $(BYTE_ENABLED)
    MP_DIRECT_SCRIPTS[] +=
        mptop
    if $(MPRUN_ENABLED)
        MP_DIRECT_SCRIPTS[] +=
            mprun
        export
    export

if $(equal $(OSTYPE), Win32)
    MP_DIRECT_SCRIPTS = $(addsuffix .bat, $(MP_DIRECT_SCRIPTS))
    export

else
    MP_DIRECT_SCRIPTS[] +=
        mpxterm
        mpxterm-large
        mpkonsole
        mpkonsole-large
        mpshell
    if $(not $(equal $(ENSROOT), undefined))
        MP_DIRECT_SCRIPTS[] +=
            mpserver
            mpgossip
        export
    if $(BYTE_ENABLED)
        MP_DIRECT_SCRIPTS[] +=
            mpdebug-top
        if $(MPRUN_ENABLED)
            MP_DIRECT_SCRIPTS[] +=
                mpdebug
            export
        export
    export

MP_DIRECT_SCRIPTS[] = $(file $(addprefix $(EDITOR)/, $(MP_DIRECT_SCRIPTS)))

MP_PREREQS[] =
    $(MP_SCRIPT)
    $(MP_BIN)
    $(file $(EDITOR)/mpconfig)
    $(MP_DIRECT_SCRIPTS)
    $(THEORIES_PATH)
    $(MLDEBUG_PATH)

#
# Build a theory document locally.
# The main goal is to get MetaPRL to generate the TeX files.
#
TheoryDocument(docname, theories) =
    CMOZFILES = $(file $(addsuffix .cmoz, $(theories)))
    THEORIES = $(basename $(theories))

    CMDLINE = $"""set_tex_file "$(absname $(docname).tex)";;
$(concat $(nl), $(add-wrapper $'print_theory "', $'";;', $(THEORIES)))"""
    #
    # Contents of the print.ml file
    #
    $(docname)_print.ml:
        echo $(quote $(CMDLINE)) > $@

    #
    # Get MetaPRL to generate the .tex files
    #
    $(docname).tex $(docname)-body.tex: $(MP_PREREQS) $(CMOZFILES) $(docname)_print.ml
        $(MP_SCRIPT) -batch $(absname $(docname)_print.ml)

#
# Format the document and copy it to the DOCDIR directory.
#
TheoryDocumentInstall(name, theories) =
    TheoryDocument(theory, $(theories))
    LaTeXDocumentInstall(tex, $(DOCDIR), $(name), theory, theory-body)

#
# Also clean up the TeX files in the subdirectories
#
CLEAN += *.log *.aux *.idx *.ilg *.ind *.pdf *.ps *.dvi *.blg *.bbl *.out *.toc *.fls

########################################################################
# Subdirectories to build
#

THEORY_DIR = $(dir theories)

#
# the theories will install themselves.
#
InstallTheoryFiles(files) =
    DIR = theories/$(string $(in $(THEORY_DIR), $(CWD)))

    ExportInstallDir($(DIR))
    ExportSubInstall($(DIR), $(filter-targets $(addsuffixes .cmi .cmiz .cmoz .mli, $(files))))

    if $(NATIVE_ENABLED)
        ExportSubInstall($(DIR), theory.cmxa theory$(EXT_LIB))

    if $(BYTE_ENABLED)
        ExportSubInstall($(DIR), theory.cma)

    $(EXPORT)/$(DIR)/MetaprlInfo: MetaprlInfo $(EXPORT)/$(DIR)
        cat $< > $@
        echo "READONLY = true" >> $@

    $(MPINSTALL): $(EXPORT)/$(DIR)/MetaprlInfo

#
# These directories use prlc
#
THEORIES[] = $(split ' ', $(THEORIES))
THEORIES[] = $(if $(mem all, $(THEORIES)), $(THEORIES_ALL) $(filter-out all, $(THEORIES)), $(THEORIES))

THEORY_DEPS[] =

#
# Find a theory in the theory path
# XXX: JYH: we should probably build this kind of search into
# omake.
#
find-theory(name) =
    THEORYNAME = false
    foreach(d => ..., $(THEORYPATH))
        if $(and $(not $(THEORYNAME)), $(file-exists $(d)/$(name)/MetaprlInfo))
            THEORYNAME = $(d)/$(name)
            export
        export
    if $(not $(THEORYNAME))
        if $(not $(defined thydir))
           thydir = unknown
           export
        if $(not $(defined source))
           source = unknown
           export
        err[] =
            $"$(name) ($(in $(ROOT)/theories, $(thydir))) (referenced by the $(source)):"
            $"theory directory $(in $(ROOT), $(thydir)) does not exist")
            $(EMPTY)
            $"The current search path is the following:"
            $(concat $'; ', $(THEORYPATH))
        ConfMsgError($(err))
    return $(dir $(THEORYNAME))

#
# XXX: JYH: even more, this is very inefficient.
#
find-theories(names) =
    dirs =
        foreach(name => ..., $(names))
            find-theory($(name))
    return $(dirs)


#
# Compile an entire theory.
#
Theory(files) =
    if $(not $(THEORYNAME))
        ConfMsgError($"In $(in $(ROOT), $(CWD)) :$(nl)The THEORYNAME variable is not defined")
    if $(not $(THEORYDESCR))
        ConfMsgError($"In $(in $(ROOT), $(CWD)) :$(nl)The THEORYDESCR variable is not defined")

    OCAMLFLAGS += -rectypes
    OCAMLINCLUDES[] += $(find-theories $(THEORY_DEPS))
    OCamlLibrary(theory, $(files))

    .DEFAULT: $(addsuffix .cmoz, $(files))

    $(THEORIES_PATH): $(CWD)

    InstallTheoryFiles($(files))

    export

#
# Search the set of theories that are desired
#
section
    # Default theory for those directories that do not override it
    # Set to empty to force each theory to define its own values.
    THEORYNAME = misc
    THEORYDESCR = Miscellaneous Theories

    OCAMLINCLUDES[] += $(LIB)

    # Theories that we need, including recursive theory dependencies.
    COLLECTED_THEORIES[] =

    PENDING_THEORIES[] =

    # Always use -linkall on Theory libraries
    OCAML_LIB_FLAGS += -linkall

    # Collect the theories that need to be built, paying attention
    # to the value of the THEORY_DEPS variable in each theory.
    TheorySubDir(theories, source) =
        foreach(thy => ..., $(theories))
            thydir = $(find-theory $(thy))
            if $(not $(mem $(thydir), $(COLLECTED_THEORIES)))
                if $(not $(file-exists $(thydir)/MetaprlInfo))
                    err[] =
                        $"$(in $(ROOT)/theories, $(thydir)) (referenced by the $(source)):"
                        $"theory does not have a MetaprlInfo"
                    ConfMsgError($(err))
                public.VirtualTheory(subdirs) =
                    VIRTUAL_THEORY = true
                    THEORY_DEPS = $(addprefix $(thy)/, $(subdirs))
                    export

                # Every theory depends on the base theory
                THEORY_DEPS[] = meta/base
                VIRTUAL_THEORY = false

                # Actually include the theory.
                READONLY = false
                MLZFILES[] =
                PENDING_THEORIES[] += $(thydir)
                .SUBDIRS: $(thydir)
                    include MetaprlInfo
                    if $(READONLY)
                        # Do not include this directory in the build, but sitll include in the search path
                        $(THEORIES_PATH): $(CWD)
                        remove-project-directories(.)
                        export
                    elseif $(file-exists OMakefile)
                        include OMakefile
                        export
                    else
                        OCamlGeneratedFiles($(addsuffixes .ml .mli, $(MLZFILES)))
                        if $(defined MPFILES)
                            Theory($(MPFILES))
                            export
                        if $(defined PRINT_THEORIES)
                            TheoryDocumentInstall($(basename $(thy)), $(PRINT_THEORIES))
                            CLEAN += theory.tex theory-body.tex theory_print.ml
                            export CLEAN
                        all: theory$(LIB_SUFFIX)
                        clean:
                            $(CLEAN)
                        export
                    export READONLY THEORY_DEPS VIRTUAL_THEORY

                THEORY_DEPS_DIRS = $(dir $(addprefix $(THEORY_DIR)/, $(THEORY_DEPS)))
                if $(intersects $(PENDING_THEORIES), $(THEORY_DEPS_DIRS))
                    err[] =
                        $"ERROR: in $(in $(ROOT), $(thydir)):"
                        $"theory dependency ``$(thy): $(intersection $(PENDING_THEORIES), $(THEORY_DEPS_DIRS))''"
                        $"creates a dependency loop"
                    ConfMsgError($(err))
                TheorySubDir($(THEORY_DEPS), MetaprlInfo in $(in $(ROOT), $(thydir)))
                if $(not $(VIRTUAL_THEORY))
                    COLLECTED_THEORIES += $(thydir)
                    export COLLECTED_THEORIES
                export COLLECTED_THEORIES
            export COLLECTED_THEORIES
        export COLLECTED_THEORIES

    # Start the theory collection process with $(THEORIES)
    TheorySubDir($(THEORIES), THEORIES variable in $(MK)/config)
    export COLLECTED_THEORIES

MP_DIRS[] = $(COLLECTED_THEORIES)