Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
10 changes: 10 additions & 0 deletions research/p104-designer-toolkit-v2/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
# scratch state written by the tools (TK_WORK defaults to this directory)
.cache/
out/
jobs/
ext/
*.so
__pycache__/
k2/bin/
*.tmp
phi.net.snap*
252 changes: 252 additions & 0 deletions research/p104-designer-toolkit-v2/MAP.md

Large diffs are not rendered by default.

534 changes: 534 additions & 0 deletions research/p104-designer-toolkit-v2/P104-LEMMAS.md

Large diffs are not rendered by default.

606 changes: 606 additions & 0 deletions research/p104-designer-toolkit-v2/P104-THEORY.md

Large diffs are not rendered by default.

1,593 changes: 1,593 additions & 0 deletions research/p104-designer-toolkit-v2/PRIMMINE-RULES.tsv

Large diffs are not rendered by default.

52 changes: 52 additions & 0 deletions research/p104-designer-toolkit-v2/PRIMMINE-SCALE-RULES.tsv
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
table LHS(A) RHS(B) class
3pub/SCALE ADD 0<-1 -1; ADD 0<-2 -1 INIT 3; COPY 3<-2 -1; ADD 3<-1 -1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P8
3pub/SCALE ADD 0<-1 -1; ADD 0<-2 -1; ADD 1<-2 -1 INIT 3; COPY 3<-2 -1; ADD 3<-1 -1; ADD 0<-3 1; ADD 1<-2 -1; CLEAR 3 DECOMP(CLSFIX fwd) P8
3pub/SCALE ADD 0<-1 -1; ADD 0<-2 -1; ADD 2<-1 -1 ADD 0<-1 -1; ADD 2<-1 -1; ADD 0<-2 -1; SCALE 1 -1; ADD 0<-1 1; SCALE 1 -1 DECOMP(CLSFIX rev) P1c+P9
3pub/SCALE ADD 0<-1 -1; ADD 0<-2 -1; ADD 2<-1 -1 ADD 0<-1 -1; ADD 2<-1 -1; SCALE 0 -1; ADD 0<-1 1; ADD 0<-2 1; SCALE 0 -1 DECOMP(CLSFIX rev) P9+P1c+P9
3pub/SCALE ADD 0<-1 -1; ADD 0<-2 -1; ADD 2<-1 -1 ADD 0<-1 -1; SCALE 2 -1; ADD 2<-1 1; ADD 0<-1 -1; ADD 0<-2 1; SCALE 2 -1 DECOMP(CLSFIX rev) P9+P9+P9+P1c
3pub/SCALE ADD 0<-1 -1; ADD 0<-2 -1; ADD 2<-1 -1 INIT 3; COPY 3<-2 -1; ADD 2<-1 -1; ADD 3<-1 -1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P8
3pub/SCALE ADD 0<-1 -1; ADD 0<-2 -1; SCALE 0 -1 SCALE 0 -1; INIT 3; COPY 3<-2 -1; ADD 3<-1 -1; ADD 0<-3 -1; CLEAR 3 DECOMP(CLSFIX fwd) P8+P9
3pub/SCALE ADD 0<-1 -1; ADD 0<-2 -1; SCALE 1 -1 SCALE 1 -1; INIT 3; COPY 3<-1 -1; ADD 3<-2 1; ADD 0<-3 -1; CLEAR 3 DECOMP(CLSFIX fwd) P9+P8
3pub/SCALE ADD 0<-1 -1; ADD 0<-2 -1; SCALE 1 -1 SCALE 1 -1; INIT 3; COPY 3<-2 -1; ADD 3<-1 1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P9+P8
3pub/SCALE ADD 0<-1 -1; ADD 0<-2 -1; SCALE 2 -1 SCALE 2 -1; INIT 3; COPY 3<-1 -1; ADD 3<-2 1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P9+P8
3pub/SCALE ADD 0<-1 -1; ADD 0<-2 -1; SCALE 2 -1 SCALE 2 -1; INIT 3; COPY 3<-2 -1; ADD 3<-1 1; ADD 0<-3 -1; CLEAR 3 DECOMP(CLSFIX fwd) P9+P8
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1 INIT 3; COPY 3<-2 -1; ADD 1<-3 1; ADD 3<-1 -1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P1c+P8+P6
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-1 -1 ADD 0<-1 -1; ADD 0<-2 1; SCALE 1 -1; ADD 0<-1 1; ADD 1<-2 1; SCALE 1 -1 DECOMP(CLSFIX rev) P9+P9+P9+P3
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-1 -1 ADD 0<-2 -1; ADD 1<-2 -1; ADD 0<-1 -1; SCALE 1 -1; ADD 0<-1 1; SCALE 1 -1 DECOMP(CLSFIX rev) P1c+P9+P9
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-1 -1 ADD 0<-2 1; ADD 0<-1 -1; SCALE 1 -1; ADD 0<-1 1; ADD 1<-2 1; SCALE 1 -1 DECOMP(CLSFIX rev) P9+P9+P9+P3
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-1 -1 ADD 1<-2 -1; ADD 0<-1 -1; ADD 0<-2 -1; SCALE 1 -1; ADD 0<-1 1; SCALE 1 -1 DECOMP(CLSFIX rev) P1c+P9+P9
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-1 -1 ADD 1<-2 -1; ADD 0<-2 -1; ADD 0<-1 -1; SCALE 1 -1; ADD 0<-1 1; SCALE 1 -1 DECOMP(CLSFIX rev) P1c+P9+P9
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-1 -1 ADD 1<-2 -1; ADD 2<-1 1; ADD 1<-2 1; ADD 0<-1 -1; ADD 1<-2 -1; ADD 2<-1 -1 DECOMP(CLSFIX fwd) P1c+P3+P3
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-1 -1 ADD 2<-1 -1; ADD 1<-2 -1; ADD 0<-1 -1; ADD 2<-1 1; ADD 1<-2 -1; ADD 2<-1 -1 UNRESOLVED-CAP (CLSFIX: all linearisations, fwd+rev, cap 2500, depth 6)
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-1 -1 ADD 2<-1 -1; ADD 1<-2 -1; ADD 2<-1 1; ADD 0<-1 -1; ADD 1<-2 -1; ADD 2<-1 -1 UNRESOLVED-CAP (CLSFIX: all linearisations, fwd+rev, cap 2500, depth 6)
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-1 -1 INIT 3; COPY 3<-1 -1; ADD 1<-2 -1; ADD 3<-1 -1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX rev) P8
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-2 -1 ADD 0<-2 -1; SCALE 1 -1; ADD 1<-2 1; ADD 0<-2 -1; ADD 0<-1 1; SCALE 1 -1 DECOMP(CLSFIX rev) P1c+P9+P9+P9
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-2 -1 ADD 1<-2 -1; ADD 0<-2 -1; SCALE 1 -1; ADD 0<-1 1; ADD 0<-2 -1; SCALE 1 -1 DECOMP(CLSFIX rev) P9+P1c+P9
3pub/SCALE ADD 0<-1 -1; ADD 1<-2 -1; ADD 0<-2 -1 INIT 3; COPY 3<-2 -1; ADD 3<-1 -1; ADD 1<-2 -1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P8
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1 INIT 3; COPY 3<-0 -1; ADD 0<-1 -1; ADD 3<-1 1; ADD 2<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P1c+P8
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1 INIT 3; COPY 3<-1 -1; ADD 3<-0 1; ADD 0<-1 -1; ADD 2<-3 -1; CLEAR 3 DECOMP(CLSFIX fwd) P1c+P8
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1 INIT 3; COPY 3<-1 -1; ADD 3<-0 1; ADD 2<-3 -1; ADD 0<-1 -1; CLEAR 3 DECOMP(CLSFIX fwd) P1c+P8
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 0<-1 -1 ADD 0<-1 -1; ADD 2<-1 -1; SCALE 0 -1; ADD 0<-1 1; ADD 2<-0 1; SCALE 0 -1 DECOMP(CLSFIX rev) P9+P9+P9+P3
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 0<-1 -1 ADD 0<-2 -1; ADD 2<-0 -1; ADD 0<-1 -1; ADD 0<-2 1; ADD 2<-0 -1; ADD 0<-2 -1 UNRESOLVED-CAP (CLSFIX: all linearisations, fwd+rev, cap 2500, depth 6)
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 0<-1 -1 ADD 0<-2 -1; ADD 2<-0 -1; ADD 0<-2 1; ADD 0<-1 -1; ADD 2<-0 -1; ADD 0<-2 -1 UNRESOLVED-CAP (CLSFIX: all linearisations, fwd+rev, cap 2500, depth 6)
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 0<-1 -1 ADD 2<-0 -1; ADD 0<-1 -1; ADD 2<-1 1; SCALE 0 -1; ADD 0<-1 1; SCALE 0 -1 DECOMP(CLSFIX rev) P1c+P9+P9
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 0<-1 -1 ADD 2<-0 -1; ADD 0<-2 1; ADD 2<-0 1; ADD 0<-1 -1; ADD 2<-0 -1; ADD 0<-2 -1 DECOMP(CLSFIX fwd) P1c+P3+P3
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 0<-1 -1 ADD 2<-0 -1; ADD 2<-1 1; ADD 0<-1 -1; SCALE 0 -1; ADD 0<-1 1; SCALE 0 -1 DECOMP(CLSFIX rev) P1c+P9+P9
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 0<-1 -1 ADD 2<-1 -1; ADD 0<-1 -1; SCALE 0 -1; ADD 0<-1 1; ADD 2<-0 1; SCALE 0 -1 DECOMP(CLSFIX rev) P9+P9+P9+P3
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 0<-1 -1 ADD 2<-1 1; ADD 2<-0 -1; ADD 0<-1 -1; SCALE 0 -1; ADD 0<-1 1; SCALE 0 -1 DECOMP(CLSFIX rev) P1c+P9+P9
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 2<-1 1 ADD 0<-2 1; ADD 2<-1 1; ADD 0<-2 -1; ADD 2<-0 -1 DECOMP(CLSFIX fwd) P3
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 2<-1 1 ADD 2<-0 -1; ADD 2<-1 1; SCALE 0 -1; ADD 0<-1 1; ADD 2<-1 1; SCALE 0 -1 DECOMP(CLSFIX rev) P9+P1c+P9
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 2<-1 1 ADD 2<-1 1; SCALE 0 -1; ADD 2<-0 1; ADD 2<-1 1; ADD 0<-1 1; SCALE 0 -1 DECOMP(CLSFIX rev) P1c+P9+P9+P9
3pub/SCALE ADD 0<-1 -1; ADD 2<-0 -1; ADD 2<-1 1 INIT 3; COPY 3<-1 -1; ADD 0<-3 1; ADD 3<-0 1; ADD 2<-3 -1; CLEAR 3 DECOMP(CLSFIX rev) P6+P8
3pub/SCALE ADD 0<-1 -1; ADD 2<-1 -1; ADD 0<-2 1 ADD 0<-1 -1; ADD 0<-2 1; ADD 2<-1 -1; SCALE 0 -1; ADD 0<-1 1; SCALE 0 -1 DECOMP(CLSFIX rev) P1c+P9
3pub/SCALE ADD 0<-1 -1; ADD 2<-1 -1; ADD 0<-2 1 ADD 0<-1 -1; ADD 0<-2 1; SCALE 1 -1; ADD 0<-1 1; ADD 2<-1 1; SCALE 1 -1 DECOMP(CLSFIX rev) P9+P1c+P9
3pub/SCALE ADD 0<-1 -1; ADD 2<-1 -1; ADD 0<-2 1 ADD 0<-1 -1; SCALE 2 -1; ADD 0<-2 -1; ADD 0<-1 -1; ADD 2<-1 1; SCALE 2 -1 DECOMP(CLSFIX rev) P9+P9+P9+P1c
3pub/SCALE ADD 0<-1 -1; ADD 2<-1 -1; ADD 0<-2 1 INIT 3; COPY 3<-1 -1; ADD 2<-3 1; ADD 3<-2 1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P8+P6
3pub/SCALE ADD 0<-1 -1; ADD 2<-1 -1; ADD 2<-0 1 ADD 0<-2 -1; ADD 2<-1 -1; ADD 0<-2 1; ADD 2<-0 1 DECOMP(CLSFIX fwd) P3
3pub/SCALE ADD 0<-1 -1; ADD 2<-1 -1; ADD 2<-0 1 INIT 3; COPY 3<-1 -1; ADD 0<-3 1; ADD 3<-0 1; ADD 2<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P8+P6
3pub/SCALE ADD 0<-1 -1; SCALE 0 -1; ADD 0<-2 -1 SCALE 0 -1; INIT 3; COPY 3<-2 -1; ADD 3<-1 1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P9+P8
3pub/SCALE ADD 0<-1 -1; SCALE 2 -1; ADD 0<-2 -1 SCALE 2 -1; INIT 3; COPY 3<-1 -1; ADD 3<-2 -1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P8
3pub/SCALE ADD 0<-1 -1; SCALE 2 -1; ADD 0<-2 -1 SCALE 2 -1; INIT 3; COPY 3<-2 -1; ADD 3<-1 -1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P8
3pub/SCALE SCALE 0 -1; ADD 0<-1 -1; ADD 0<-2 -1 SCALE 0 -1; INIT 3; COPY 3<-2 -1; ADD 3<-1 -1; ADD 0<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P8
3pub/SCALE SCALE 0 -1; ADD 1<-0 -1; ADD 1<-2 -1 SCALE 0 -1; INIT 3; COPY 3<-0 -1; ADD 3<-2 -1; ADD 1<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P8
3pub/SCALE SCALE 0 -1; ADD 1<-0 -1; ADD 1<-2 -1 SCALE 0 -1; INIT 3; COPY 3<-2 -1; ADD 3<-0 -1; ADD 1<-3 1; CLEAR 3 DECOMP(CLSFIX fwd) P8
Loading