Makefile.coq_modules

#
# Copyright 2015-2016 IBM Corporation
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
# http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
#

QCERT_LIB_UTILS = LibUtilsAssoc LibUtilsBag LibUtilsBindings LibUtilsBindingsNat \
		  LibUtilsClosure LibUtilsCompat LibUtilsCoqLibAdd LibUtilsDigits \
		  LibUtilsFresh LibUtilsGroupByDomain LibUtilsInterleaved \
		  LibUtilsLattice LibUtilsLift LibUtilsLiftIterators LibUtilsListAdd \
		  LibUtilsResult LibUtilsSortingAdd LibUtilsStringAdd LibUtilsSublist \
		  LibUtils

ELFIC_UTILS	= R_compl check_sub_structure compatible continuous_linear_map fixed_point \
		  hierarchyD hilbert linear_map logic_tricks lax_milgram lax_milgram_cea


UTILS = BasicUtils \
	Assoc \
	ClassicUtils \
	CoquelicotAdd \
	ELim_Seq \
	ExtrFloatishIEEE \
	improper_integrals \
	Isomorphism \
	ListAdd \
	FiniteType \
	FiniteTypeVector \
	NumberIso \
	PairEncoding \
	Quotient \
	quotient_space \
	RealAdd \
	RbarAdd \
	RiemannAdd \
	StreamAdd \
	StreamLimits \
	Sums \
	nvector \
	Vector \
	PushNeg \
	DVector \
	Utils \
	Floatish/FloatishDef \
	Floatish/FloatishOps \
	Floatish/FloatishRealOps \
	Floatish/FloatishInterval \
	Floatish/FloatishIEEE \
	Floatish/FloatishReal \
	Floatish

NEURAL_NETWORKS = AxiomaticNormedRealVectorSpace \
		DefinedFunctions \
		derivlemmas \
		Gen_NN
		

CERTRL = pmf_monad \
	qvalues \
	mdp \
	mdp_turtle \
	finite_time \
	cond_expt \
	pmf_prob

PROB_THEORY = \
	Almost \
	BorelSigmaAlgebra \
	DiscreteProbSpace \
	Dynkin \
	Event \
	Independence \
	ProbSpace \
	FunctionsToReal \
	Measures \
	RandomVariable \
	RealRandomVariable \
	RandomVariableFinite \
	RandomVariableL2 \
	RandomVariableLpNat \
	RandomVariableLpR \
	RandomVariableLinf \
	OrthoProject \
	RealVectorHilbert \
	SimpleExpectation \
	ConditionalExpectation \
	Expectation \
	RbarExpectation \
	VectorConditionalExpectation \
	SigmaAlgebras \
	VectorRandomVariable \
	Martingale \
	MartingaleConvergence \
	MartingaleStopped \
	Gaussian \
	ProductSpace \
	ProductSpaceDep


QLEARN = \
	Dvoretzky \
	Bellman \
	qlearn_aux \
	qlearn \
	qlearn_redux \
	infprod \
	sumtest \
   	slln \
	vecslln \
	Tsitsiklis

FHE = \
      nth_root \
      encode \
      encrypt \
      zp_prim_root \
      arith

MODULES =  $(addprefix lib_utils/,$(QCERT_LIB_UTILS)) \
	$(addprefix CertRL/LM/,$(ELFIC_UTILS)) \
	$(addprefix utils/,$(UTILS)) \
	$(addprefix NeuralNetworks/,$(NEURAL_NETWORKS)) \
	$(addprefix ProbTheory/,$(PROB_THEORY)) \
	$(addprefix CertRL/,$(CERTRL)) \
	$(addprefix QLearn/,$(QLEARN)) \
	$(addprefix FHE/,$(FHE)) \
	API