...
 
Commits (2)
  • Florian Rabe's avatar
    no message · a90ccfb3
    Florian Rabe authored
    a90ccfb3
  • Florian Rabe's avatar
    no message · 74af6271
    Florian Rabe authored
    Merge branch 'master' of gl.mathhub.info:ODK/DiscreteZoo
    
    # Conflicts:
    #	source/mathdata.mmt
    74af6271
commit your sources in this folder
\ No newline at end of file
namespace http://data.mathhub.info/schemas❚
// list of collections: [('matrix', id, ...)] ❚
theory Example : ?SchemaLang =
ID: uuid❘
meta ?Codecs?codec UUIDIdent❘
tag ?SchemaLang?primaryKey❘
tag ?SchemaLang?opaque❘
tag ?SchemaLang?hidden❘
mat: matrix int 2 2❘
meta ?Codecs?codec MatrixAsArray IntIdent❘
tag ?SchemaLang?opaque❘
trace: int❘
meta ?Codecs?codec IntIdent❘
orthogonal: bool❙
meta ?Codecs?codec BoolIdent❘
eigenvalues: list int❘
meta ?Codecs?codec ListAsArray IntIdent❘
characteristic: Polynomial IntegerRing❘
meta ?Codecs?codec PolynomialAsSparseArray IntIdent❘
namespace http://data.mathhub.info/schemas❚
theory MathData : ur:/?PLF =
include ?Equality❙
boolean: type❙
true: boolean❙
false: boolean❙
int: type❙
leq : int ⟶ int ⟶ boolean❘# 1 ≤ 2❙
geq : int ⟶ int ⟶ boolean❘# 1 ≥ 2❙
lt : int ⟶ int ⟶ boolean❘# 1 < 2❙
gt : int ⟶ int ⟶ boolean❘# 1 > 2❙
eq : int ⟶ int ⟶ boolean❘# 1 = 2❙
neq : int ⟶ int ⟶ boolean❘# 1 ≠ 2❙
string: type❙
concat: string ⟶ string ⟶ string ❘ # 1 @ 2❙
uuid: type❙
// opaque type ❙
array : type ⟶ type❙
theory Codecs : ur:/?PLF =
namespace http://data.mathhub.info/schemas❚
theory MatrixExample : ur:/?PLF =
include ?MathData❙
// list of collections: [('matrix', id, ...)] ❙
id: uuid ❙ // primary key, opaque, not displayed by default ❙
matrix : array array int ❙ // opaque, displayed by default ❙
trace : int ❙ // not opaque, displayed by default ❙
orthogonal : boolean ❙ // not opaque, displayed by default ❙
eigenvalues : array int ❙ // not opaque, displayed by default ❙
\ No newline at end of file
namespace http://data.mathhub.info/schemas❚
import lfrules scala://lf.mmt.kwarc.info/❚
import stdlit scala://uom.api.mmt.kwarc.info/❚
theory MathData : ur:/?PLF =
bool : type❙
rule lfrules?Realize bool stdlit?StandardBool❙
int : type❙
plus : int ⟶ int ⟶ int❘# 1 + 2❙
minus : int ⟶ int ⟶ int❘# 1 - 2❙
times : int ⟶ int ⟶ int❘# 1 ⋅ 2❙
rule lfrules?Realize int stdlit?StandardInt❙
rule lfrules?Realize plus stdlit?Arithmetic/Plus❙
eq : {a: type} a ⟶ a ⟶ bool❘# 2 = 3❙
leq : int ⟶ int ⟶ bool❘# 1 ≤ 2❙
geq : int ⟶ int ⟶ bool❘# 1 ≥ 2❙
string: type❙
concat : string ⟶ string ⟶ string ❘# 1 @ 2❙
rule lfrules?Realize string stdlit?StandardString❙
rule lfrules?Realize concat stdlit?StringOperations/Concat❙
uuid: type❙
rule lfrules?Realize uuid stdlit?UUIDLiteral❙
list : type ⟶ type❘# list 1 prec 10❙
nil : {a} list a❙
cons : {a} a ⟶ list a ⟶ list a❙
concat : {a} list a ⟶ list a ⟶ list a❘# 2 ++ 3❙
map : {a,b} list a ⟶ (a ⟶ b) ⟶ list b❙
length : {a} list a ⟶ int❙
vector : type ⟶ int ⟶ type❘# vector 1 2 prec 10❙
empty : {a} vector a 0❙
single : {a} a ⟶ vector a 1❙
stack : {a,m,n} vector a m ⟶ vector a n ⟶ vector a (m+n)❘# 4 ; 5❙
matrix : type ⟶ int ⟶ int ⟶ type ❘= [a,m,n] vector (vector a m) n❙
option : type ⟶ type❙
some : {a} a ⟶ option a❙
none : {a} option a❙
getOrElse : {a} option a ⟶ a ⟶ a❙
product : type ⟶ type ⟶ type❘# 1 * 2❙
pair : {a,b} a ⟶ b ⟶ product a b❘# 3 , 4❙
left : {a,b} product a b ⟶ a ❘# 3 _1❙
right : {a,b} product a b ⟶ b❘# 3 _2❙
Ring: type❙
ring: {a: type, plus: a ⟶ a ⟶ a, minus: a ⟶ a, zero: a, times: a ⟶ a ⟶ a, one: a} Ring❙
univ: Ring ⟶ type❙
IntegerRing: Ring❘= ring int plus ([x] 0-x) 0 times 1❙
var: type ❘ = string❙
PolynomialRing : Ring ⟶ Ring❘# PolyRing 1 prec 10❙
Polynomial : Ring ⟶ type❘ = [r] univ (PolyRing r)❘ # Poly 1 prec 10❙
polynomial : {r} var ⟶ list (univ r) ⟶ Poly r❙
coeffs : {r} Poly r ⟶ list (univ r)❙
degree : {r} Poly r ⟶ int❙
theory DbData : ur:?PLF =
db_tp : type❙
db_val : db_tp ⟶ type❘# V 1 prec -5❙
db_null : {a} V a❙
db_int : db_tp❙
db_bool : db_tp❙
db_string: db_tp❙
db_uuid : db_tp❙
db_array : db_tp ⟶ db_tp❙
eq : {a} V a ⟶ V a ⟶ V db_bool❙
neq : {a} V a ⟶ V a ⟶ V db_bool❙
leq : V db_int ⟶ V db_int ⟶ V db_bool❘# 1 ≤ 2❙
lt : V db_int ⟶ V db_int ⟶ V db_bool❘# 1 < 2❙
geq : V db_int ⟶ V db_int ⟶ V db_bool❘# 1 ≥ 2❙
gt : V db_int ⟶ V db_int ⟶ V db_bool❘# 1 > 2❙
elemAt : {a} V db_array a ⟶ V db_int ⟶ V a❙
length : {a} V db_array a ⟶ V db_int❙
lengthDim: {a} V db_array a ⟶ V db_int ⟶ V db_int❙
contains : {a} V db_array a ⟶ V db_array a ⟶ V db_bool❙
containedIn : {a} V db_array a ⟶ V db_array a ⟶ V db_bool❙
hasCommonElem : {a} V db_array a ⟶ V db_array a ⟶ V db_bool❙
theory Codecs : ur:?PLF =
include ?MathData❙
include ?DbData❙
codec : type ⟶ db_tp ⟶ type❙
BoolIdent : codec bool db_bool❙
IntIdent : codec int db_int❙
StringIdent : codec string db_string❙
UUIDIdent : codec uuid db_uuid❙
IntAsString : codec int db_string❙
ListAsArray : {A,a} codec A a ⟶ codec (list A) (db_array a)❘# ListAsArray 3❙
VectorAsArray : {A,a,n} codec A a ⟶ codec (vector A n) (db_array a)❘# VectorAsArray 3 4❙
OptionAsNullable : {A,a} codec A a ⟶ codec (option A) a❘# OptionAsNullable 3❙
ProductAsArray: {A,B,e} codec A e ⟶ codec B e ⟶ codec (A * B) e❙
MatrixAsArray : {A,a,m,n} codec A a ⟶ codec (matrix A m n) (db_array (db_array a))❘
= [A,a,m,n,C] VectorAsArray n (VectorAsArray m C)❘# MatrixAsArray 5❙
PolynomialAsSparseArray : {r, e} codec (univ r) e ⟶ codec (Poly r) (db_array (db_array e))❘# %%prefix 2❙
PolynomialAsDenseArray : {r, e} codec (univ r) e ⟶ codec (Poly r) (db_array e)❘# %%prefix 2❙
theory CommutingOps : ur:?PLF =
include ?Codecs❙
commute0 : {A,a} codec A a ⟶ A ⟶ db_val a ⟶ type❘
# 4 ~ 5 @ 3 prec -5❙
commute1 : {A,a,B,b} codec A a ⟶ codec B b ⟶ (A ⟶ B) ⟶ (db_val a ⟶ db_val b) ⟶ type❘
# 7 ~ 8 @ 5 ⟹ 6 prec -10❙
commute2 : {A,a,B,b,C,c} codec A a ⟶ codec B b ⟶ codec C c ⟶
(A ⟶ B ⟶ C) ⟶ (db_val a ⟶ db_val b ⟶ db_val c) ⟶ type❘
# 10 ~ 11 @ 7 ⟹ 8 ⟹ 9 prec -15❙
eq : {A,a,C} MathData?eq A ~ DbData?eq a @ C ⟹ C ⟹ BoolIdent❙
arrayLen: {A, a, C} MathData?length A ~ DbData?length a @ ListAsArray C ⟹ IntIdent ❙
theory SchemaLang : ur:?PLF =
include ?MathData❙
include ?DbData❙
include ?Codecs❙
include ?CommutingOps❙
primaryKey❙
opaque❙
hidden❙
namespace http://www.discretezoo.xyz/prototyper❚
theory dzgraph : http://www.discretezoo.xyz/odz?DZGraph =
meta /?Metadata?implements ugraph❙
meta /?Metadata?constructor from_record❙
meta /?Metadata?key "label"❙
sparse6 : string ❘ meta /?Metadata?codec standardString
❘ link /?Metadata?implements http://www.discretezoo.xyz/odz?DZGraph?sparse6 ❙
order : pos_lit ❘ meta /?Metadata?codec standardPos
❘ link /?Metadata?implements http://www.discretezoo.xyz/odz?DZGraph?order ❙
\ No newline at end of file