From 1a638acc6d83eea44228bf371d24f02e7dfc7d5b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Dennis=20M=C3=BCller?= <d.mueller@jacobs-university.de>
Date: Tue, 16 Oct 2018 21:27:56 +0200
Subject: [PATCH] update
---
.../mitm/prim.omdoc.xz | Bin 0 -> 416 bytes
narration/primitives.omdoc | 2 +
.../http..www.gap-system.org/mitm/prim.rel | 5 +
relational/primitives.rel | 2 +
source/alignment.mmt | 6 +-
source/primitives.mmt | 90 ++++++++++++++++++
6 files changed, 104 insertions(+), 1 deletion(-)
create mode 100644 content/http..www.gap-system.org/mitm/prim.omdoc.xz
create mode 100644 narration/primitives.omdoc
create mode 100644 relational/http..www.gap-system.org/mitm/prim.rel
create mode 100644 relational/primitives.rel
create mode 100644 source/primitives.mmt
diff --git a/content/http..www.gap-system.org/mitm/prim.omdoc.xz b/content/http..www.gap-system.org/mitm/prim.omdoc.xz
new file mode 100644
index 0000000000000000000000000000000000000000..72d0bdafee404bd1bec725e28aea363e788cc94b
GIT binary patch
literal 416
zcmV;R0bl<8H+ooF000E$*0e?f03iVu0001VFXf})0~!HcT>u^%$);Gjm;(V8!D4R=
zvOFp-REWkEE1f>j;I%&DeXXhUOC=fH*0Ejij1i?$h>zE3%J*;?T3^ss2<$DwDDq;t
znLacvhsM>}k5K=+9PUNhTk`SD2w2L9{?_Qf4j#~H7}06jPiIZPjJp`-{|a^CraRo|
zEdMMl;!nZu$L584E;HG?cMH{-;WE=&Tc<g5xe36I9IB15A85(Mm{nP7aE9X-cWq9x
zJ!GAN+#~oe4A7JL4cYW9TpEfM(IFqlSIO`E$th2-c<f^c@AwI;Yt)Ywy@Hfyg<@D#
z3*&nU&@<W;)AENvV?|CL;xh?K90O;6rqXva%kPR=!dxvZ3+_$6YdgPXV+K+-az77V
zs?#^3>|<Z6L?auzm&15Ut0}zkQ>fV452&}Gg3}z7_k2mXVr`UCZOFllF}1FyQUfkC
zNW`$nHY{K-pCrWeRMFydFOhoQsG_L=0001&$vb7NTF7<)0r>)(1^@ti)x_no#Ao{g
K000001X)^|8^q!O
literal 0
HcmV?d00001
diff --git a/narration/primitives.omdoc b/narration/primitives.omdoc
new file mode 100644
index 0000000..af023ba
--- /dev/null
+++ b/narration/primitives.omdoc
@@ -0,0 +1,2 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<omdoc base="http://www.gap-system.org/primitives.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://www.gap-system.org/primitives.mmt#0.0.0:3045.89.0"/></metadata><mref name="[http://www.gap-system.org/mitm?prim]" target="http://www.gap-system.org/mitm?prim"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://www.gap-system.org/primitives.mmt#44.2.0:54.2.10"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/relational/http..www.gap-system.org/mitm/prim.rel b/relational/http..www.gap-system.org/mitm/prim.rel
new file mode 100644
index 0000000..a2fe1f9
--- /dev/null
+++ b/relational/http..www.gap-system.org/mitm/prim.rel
@@ -0,0 +1,5 @@
+untypedconstant http://www.gap-system.org/mitm?prim?ListConstr
+theory http://www.gap-system.org/mitm?prim
+HasMeta http://www.gap-system.org/mitm?prim http://www.gap-system.org?Types
+Declares http://www.gap-system.org/mitm?prim http://www.gap-system.org/mitm?prim?ListConstr
+constant http://www.gap-system.org/mitm?prim?ListConstr
diff --git a/relational/primitives.rel b/relational/primitives.rel
new file mode 100644
index 0000000..b680eac
--- /dev/null
+++ b/relational/primitives.rel
@@ -0,0 +1,2 @@
+document http://www.gap-system.org/primitives.omdoc
+Declares http://www.gap-system.org/primitives.omdoc http://www.gap-system.org/mitm?prim
diff --git a/source/alignment.mmt b/source/alignment.mmt
index b444533..1c5d5ed 100644
--- a/source/alignment.mmt
+++ b/source/alignment.mmt
@@ -1 +1,5 @@
-namespace http://www.gap-system.org âš
\ No newline at end of file
+namespace http://www.gap-system.org âš
+
+theory Alignments : mitm?lib =
+ DihedralGroup = [d] `lib?DihedralGroup `lib?IsPermGroup d â™
+âš
\ No newline at end of file
diff --git a/source/primitives.mmt b/source/primitives.mmt
new file mode 100644
index 0000000..caff728
--- /dev/null
+++ b/source/primitives.mmt
@@ -0,0 +1,90 @@
+namespace http://www.gap-system.org/mitm âš
+
+theory prim : ../?Types =
+ ListConstr â™
+âš
+
+// theory Types : ur:?PLF =
+ object : type â™
+ category : type â™
+
+ booleans : type â™
+ integers : type â™
+ floats : type â™
+
+ filter = object ⟶ type â™
+
+ hastp : object ⟶ filter ⟶ type ☠// = [o][f] f o ☠# 1 $ 2 â™
+
+ filter_and : filter ⟶ filter ⟶ filter ☠# 1 and 2 â™
+ filter_and_hasFilter1 : {x : object,f : filter,g : filter} x $ f ⟶ x $ g ⟶ x $ (f and g) â™
+ filter_and_hasFilter2 : {x : object,f : filter,g : filter} x $ (f and g) ⟶ x $ f â™
+ filter_and_hasFilter3 : {x : object,f : filter,g : filter} x $ (f and g) ⟶ x $ g â™
+
+ ded : object ⟶ type â™
+
+ rule rules?Booleans â™
+ rule rules?Integers â™
+ rule rules?Floats â™
+
+ gapbool : booleans ⟶ object â™
+ gapint : integers ⟶ object â™
+ gapfloat : floats ⟶ object â™
+
+ trueI : ded (gapbool true) â™
+ catFilter : category ⟶ filter â™
+ propertyFilter : (object ⟶ object) ⟶ filter ☠= [p] [o] ded (p o) â™
+
+ Has : (object ⟶ object) ⟶ filter â™
+ CategoryCollection : filter ⟶ category â™
+ Set : filter ⟶ (object ⟶ object) â™
+ IsBool : category â™
+ IsObject : category â™
+ // HasIsProperty : {o,x} x # (propertyFilter o) ⟶ ((Has o) x) # catFilter IsBool â™
+
+âš
+
+// theory Types : odk:?Math =
+ Object : tp â™
+
+ Family : tp â™
+ Family_Of_Families : tm Family â™
+ Families_are_Objects : Family < Object â™
+ Family_Of_Object : tm Object ⟶ tm Family ☠# FamilyOfObj 1 â™
+ Family_Of_Family_is_Family_of_Families : {F:tm Family} ⊦ eq Family (FamilyOfObj (tpCast Families_are_Objects F)) Family_Of_Families â™
+
+ Filter : tp â™
+ Elementary_Filter : tp â™
+ Elementary_Filter_Is_Filter : Elementary_Filter < Filter â™
+
+ Filter_applies : tm Filter ⟶ tm Object ⟶ prop ☠# 1 _ 2 â™
+
+ filter_conj : tm Filter ⟶ tm Filter ⟶ tm Filter ☠# 1 + 2 prec 5â™
+ filter_conj_is_Conjunction : {F1,F2,O} ⊦ ((F1 + F2) _ O) ≠((F1 _ O) ∧ (F2 _ O)) ☠role Simplify â™
+ filter_conj_is_associative : {F1,F2,F3} ⊦ F1 + (F2 + F3) ≠(F1 + F2) + F3 â™
+ filter_conj_is_commutative : {F1,F2} ⊦ F1 + F2 ≠F2 + F1 â™
+
+ filter_def : (tm Object ⟶ prop) ⟶ tm Filter ☠# MakeFilter 1 â™
+ filter_def_application : {F,O} ⊦ ((MakeFilter F) _ O) ≠F O â™
+
+ GAPtype : tp â™
+ Family_of_GAPtype : tm GAPtype ⟶ tm Family ☠# FamilyOfTp 1 â™
+ Filter_of_GAPtype : tm GAPtype ⟶ tm list Elementary_Filter ☠# FilterOf 1 â™
+ GAPtype_Constructor : tm Family ⟶ tm list Elementary_Filter ⟶ tm GAPtype ☠# GAPtp 1 2 â™
+ // Filter_applies_to_type_object : {O} ⊦ (FilterOf O) _ O â™
+
+ Operation : tp â™
+ Name_of_Operation : tm Operation ⟶ tm string â™
+ Arglength_of_Operation : tm Operation ⟶ tm â„• â™
+ Filter_of_Operation : {op: tm Operation} tm vector Filter (Arglength_of_Operation op) â™
+ Operation_Constructor : {name: tm string, args: tm â„•} tm vector Filter args ⟶ tm Operation â™
+
+ Category : tp â™
+ Category_is_elementary_Filter : Category < Elementary_Filter â™
+
+ Property : tp â™
+ Property_is_elementary_Filter : Property < Elementary_Filter â™
+ Has : tm Property ⟶ tm Elementary_Filter â™
+ OperationFromProperty : tm Property ⟶ tm Operation â™
+ OperationSet : tm Property ⟶ tm Operation ☠# Set 1 â™
+âš
\ No newline at end of file
--
GitLab