Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

The math package #1842

Closed
wants to merge 1 commit into from
Closed

The math package #1842

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 7 additions & 2 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ TEST_PREFIX ?= ${IDRIS2_CURDIR}/build/env
IDRIS2_BOOT_PREFIX := ${IDRIS2_CURDIR}/bootstrap-build

# These are the library path in the build dir to be used during build
export IDRIS2_BOOT_PATH := "${IDRIS2_CURDIR}/libs/prelude/build/ttc${SEP}${IDRIS2_CURDIR}/libs/base/build/ttc${SEP}${IDRIS2_CURDIR}/libs/contrib/build/ttc${SEP}${IDRIS2_CURDIR}/libs/network/build/ttc${SEP}${IDRIS2_CURDIR}/libs/test/build/ttc"
export IDRIS2_BOOT_PATH := "${IDRIS2_CURDIR}/libs/prelude/build/ttc${SEP}${IDRIS2_CURDIR}/libs/base/build/ttc${SEP}${IDRIS2_CURDIR}/libs/math/build/ttc${SEP}${IDRIS2_CURDIR}/libs/contrib/build/ttc${SEP}${IDRIS2_CURDIR}/libs/network/build/ttc${SEP}${IDRIS2_CURDIR}/libs/test/build/ttc"

export SCHEME

Expand Down Expand Up @@ -81,7 +81,10 @@ base: prelude
network: prelude
${MAKE} -C libs/network IDRIS2=${TARGET} IDRIS2_INC_CGS=${IDRIS2_CG} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

contrib: base
math: base
${MAKE} -C libs/math IDRIS2=${TARGET} IDRIS2_INC_CGS=${IDRIS2_CG} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

contrib: math
${MAKE} -C libs/contrib IDRIS2=${TARGET} IDRIS2_INC_CGS=${IDRIS2_CG} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

test-lib: contrib
Expand All @@ -103,6 +106,7 @@ ${TEST_PREFIX}/${NAME_VERSION} :
cp -rf ${IDRIS2_CURDIR}/libs/prelude/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/prelude-${IDRIS2_VERSION}
cp -rf ${IDRIS2_CURDIR}/libs/base/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/base-${IDRIS2_VERSION}
cp -rf ${IDRIS2_CURDIR}/libs/test/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/test-${IDRIS2_VERSION}
cp -rf ${IDRIS2_CURDIR}/libs/math/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/math-${IDRIS2_VERSION}
cp -rf ${IDRIS2_CURDIR}/libs/contrib/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/contrib-${IDRIS2_VERSION}
cp -rf ${IDRIS2_CURDIR}/libs/network/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/network-${IDRIS2_VERSION}
else
Expand All @@ -111,6 +115,7 @@ ${TEST_PREFIX}/${NAME_VERSION} :
ln -sf ${IDRIS2_CURDIR}/libs/prelude/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/prelude-${IDRIS2_VERSION}
ln -sf ${IDRIS2_CURDIR}/libs/base/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/base-${IDRIS2_VERSION}
ln -sf ${IDRIS2_CURDIR}/libs/test/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/test-${IDRIS2_VERSION}
ln -sf ${IDRIS2_CURDIR}/libs/math/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/math-${IDRIS2_VERSION}
ln -sf ${IDRIS2_CURDIR}/libs/contrib/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/contrib-${IDRIS2_VERSION}
ln -sf ${IDRIS2_CURDIR}/libs/network/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/network-${IDRIS2_VERSION}
endif
Expand Down
36 changes: 2 additions & 34 deletions libs/contrib/contrib.ipkg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@ version = 0.4.0

opts = "--ignore-missing-ipkg -Wno-shadowing"

depends = math

modules = Control.ANSI,
Control.ANSI.SGR,
Control.ANSI.CSI,
Expand All @@ -13,25 +15,13 @@ modules = Control.ANSI,

Control.Monad.Algebra,

Control.Algebra,
Control.Algebra.Laws,
Control.Algebra.Implementations,

Control.Arrow,
Control.Category,

Control.Validation,

Data.Binary.Digit,
Data.Binary,

Data.Bool.Algebra,
Data.Bool.Decidable,

Data.Container,

Data.Fin.Extra,

Data.Fun.Extra,
Data.Fun.Graph,

Expand Down Expand Up @@ -62,23 +52,8 @@ modules = Control.ANSI,

Data.Logic.Propositional,

Data.Monoid.Exponentiation,

Data.Morphisms.Algebra,

Data.Nat.Algebra,
Data.Nat.Ack,
Data.Nat.Division,
Data.Nat.Equational,
Data.Nat.Exponentiation,
Data.Nat.Fact,
Data.Nat.Factor,
Data.Nat.Fib,
Data.Nat.Order.Strict,
Data.Nat.Order.Properties,
Data.Nat.Order.Relation,
Data.Nat.Properties,

Data.Num.Implementations,

Data.OpenUnion,
Expand Down Expand Up @@ -125,13 +100,10 @@ modules = Control.ANSI,
Data.Vect.Sort,
Data.Vect.Views.Extra,

Data.Void,

Data.HVect,

Debug.Buffer,

Decidable.Order.Strict,
Decidable.Decidable.Extra,

Language.JSON,
Expand All @@ -149,10 +121,6 @@ modules = Control.ANSI,
Search.Negation,
Search.Properties,

Syntax.WithProof,
Syntax.PreorderReasoning,
Syntax.PreorderReasoning.Generic,

System.Console.GetOpt,
System.Directory.Tree,
System.Future,
Expand Down
0 libs/contrib/Control/Algebra.idr → libs/math/Control/Algebra.idr
View file
Open in desktop
File renamed without changes.
0 ...ntrib/Control/Algebra/Implementations.idr → .../math/Control/Algebra/Implementations.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Control/Algebra/Laws.idr → libs/math/Control/Algebra/Laws.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Binary.idr → libs/math/Data/Binary.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Binary/Digit.idr → libs/math/Data/Binary/Digit.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Bool/Algebra.idr → libs/math/Data/Bool/Algebra.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Bool/Decidable.idr → libs/math/Data/Bool/Decidable.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Fin/Extra.idr → libs/math/Data/Fin/Extra.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Monoid/Exponentiation.idr → libs/math/Data/Monoid/Exponentiation.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Nat/Ack.idr → libs/math/Data/Nat/Ack.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Nat/Algebra.idr → libs/math/Data/Nat/Algebra.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Nat/Division.idr → libs/math/Data/Nat/Division.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Nat/Equational.idr → libs/math/Data/Nat/Equational.idr
View file
Open in desktop
File renamed without changes.
1 change: 0 additions & 1 deletion libs/contrib/Data/Nat/Exponentiation.idr → libs/math/Data/Nat/Exponentiation.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ module Data.Nat.Exponentiation
import Data.Nat as Nat
import Data.Nat.Properties
import Data.Monoid.Exponentiation as Mon
import Data.Num.Implementations as Num
import Data.Nat.Views
import Data.Nat.Order
import Syntax.PreorderReasoning
Expand Down
0 libs/contrib/Data/Nat/Fact.idr → libs/math/Data/Nat/Fact.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Nat/Factor.idr → libs/math/Data/Nat/Factor.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Nat/Fib.idr → libs/math/Data/Nat/Fib.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Nat/Order/Properties.idr → libs/math/Data/Nat/Order/Properties.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Nat/Order/Relation.idr → libs/math/Data/Nat/Order/Relation.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Nat/Order/Strict.idr → libs/math/Data/Nat/Order/Strict.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Nat/Properties.idr → libs/math/Data/Nat/Properties.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Data/Void.idr → libs/math/Data/Void.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Decidable/Order/Strict.idr → libs/math/Decidable/Order/Strict.idr
View file
Open in desktop
File renamed without changes.
14 changes: 14 additions & 0 deletions libs/math/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
all:
${IDRIS2} --build math.ipkg

install:
${IDRIS2} --install math.ipkg

install-with-src:
${IDRIS2} --install-with-src math.ipkg

docs:
${IDRIS2} --mkdoc math.ipkg

clean:
$(RM) -r build
0 libs/contrib/Syntax/PreorderReasoning.idr → libs/math/Syntax/PreorderReasoning.idr
View file
Open in desktop
File renamed without changes.
0 ...trib/Syntax/PreorderReasoning/Generic.idr → ...math/Syntax/PreorderReasoning/Generic.idr
View file
Open in desktop
File renamed without changes.
0 libs/contrib/Syntax/WithProof.idr → libs/math/Syntax/WithProof.idr
View file
Open in desktop
File renamed without changes.
39 changes: 39 additions & 0 deletions libs/math/math.ipkg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
package math
version = 0.4.0

-- opts = "--ignore-missing-ipkg -Wno-shadowing"

modules = Control.Algebra,
Control.Algebra.Laws,
Control.Algebra.Implementations,

Data.Binary.Digit,
Data.Binary,

Data.Bool.Algebra,
Data.Bool.Decidable,

Data.Fin.Extra,

Data.Monoid.Exponentiation,

Data.Nat.Algebra,
Data.Nat.Ack,
Data.Nat.Division,
Data.Nat.Equational,
Data.Nat.Exponentiation,
Data.Nat.Fact,
Data.Nat.Factor,
Data.Nat.Fib,
Data.Nat.Order.Strict,
Data.Nat.Order.Properties,
Data.Nat.Order.Relation,
Data.Nat.Properties,

Data.Void,

Decidable.Order.Strict,

Syntax.WithProof,
Syntax.PreorderReasoning,
Syntax.PreorderReasoning.Generic
3 changes: 1 addition & 2 deletions tests/idris2/interface024/run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
rm -rf build

$1 --no-banner --no-color --check EH.idr -p contrib

$1 --no-banner --no-color --check EH.idr -p math