Skip to content

Commit d14494d

Browse files
adamAndMathadamAndMath
committed
Added wrapping and unwrapping of objects and functions
1 parent 6efa064 commit d14494d

File tree

13 files changed

+141
-22
lines changed

13 files changed

+141
-22
lines changed

‎src/algebraic/manipulator/latex/LatexWriter.scala

Lines changed: 21 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -43,16 +43,22 @@ object LatexWriter {
4343
def writeFile(project: Project, file: WorkFile): String = {
4444
val env = file.env(project)
4545

46+
val assumptions = file.names.filter(file.get(_).isInstanceOf[Assumption])
47+
4648
s"\\chapter{${file.path.last}}\n" +
4749
file.names.filter(n => isDefinition(file.get(n))).map(name =>
4850
writeElementDefinition(name, file.get(name))
4951
).mkString +
50-
"Given the following assumptions:\n" +
51-
file.names.filter(file.get(_).isInstanceOf[Assumption]).map(name =>
52-
"\\\\\n" +
53-
s"\\label{${(file.path + name).mkString(":")}}\n" +
54-
writeAssumption(file.get(name).asInstanceOf[Assumption])
55-
).mkString +
52+
{
53+
if (assumptions.nonEmpty)
54+
"Given the following assumptions:\n" +
55+
assumptions.map(name =>
56+
"\\\\\n" +
57+
s"\\label{${(file.path + name).mkString(":")}}\n" +
58+
writeAssumption(file.get(name).asInstanceOf[Assumption])
59+
).mkString
60+
else ""
61+
} +
5662
file.names
5763
.filterNot(file.get(_).isInstanceOf[Assumption])
5864
.filterNot(n => isDefinition(file.get(n)))
@@ -74,7 +80,7 @@ object LatexWriter {
7480

7581
def writeElementDefinition(name: String, element: Element): String = element match {
7682
case AssumedObject => s"Let $name be an object\\\\\n"
77-
case SimpleObject(exp) => s"Let $$${writeExp(Variable(name))} = ${writeExp(exp)}$$"
83+
case SimpleObject(exp) => s"Let $$${writeExp(Variable(name))} = ${writeExp(exp)}$$\\\\\n"
7884
case InductiveStructure(base, steps) =>
7985
val typeOut = writeType(SimpleType(name))
8086
s"Let $$$typeOut$$ be the smallest set that satisfies " +
@@ -151,6 +157,8 @@ object LatexWriter {
151157
positions :: (parameters.indices zip parameters.map(_.positions)).map{case (i, p) => p.map(_ :> colors(i)).getOrElse(PathTree.empty)}.fold(PathTree.empty)(_|_)
152158
case FromEval(positions) => positions :> colors.head
153159
case Rename(positions, _, _) => positions :> colors.head
160+
case Wrap(Variable(_), positions) => positions :> colors.head
161+
case Unwrap(positions) => positions :> colors.head
154162
}
155163

156164
def getOutputColors(env: Environment, exps: List[Exp], manipulation: Manipulation): PathTree[String] = manipulation match {
@@ -165,6 +173,8 @@ object LatexWriter {
165173
| parameters.indices.map(i => Tree.edge(i+1) :> colors(i)).fold(PathTree.empty)(_|_))
166174
case FromEval(positions) => positions :> colors.head
167175
case Rename(positions, _, _) => positions :> colors.head
176+
case Wrap(Variable(_), positions) => positions :> colors.head
177+
case Unwrap(positions) => positions :> colors.head
168178
}
169179

170180
def writeManipulation(env: Environment, manipulation: Manipulation): String = manipulation match {
@@ -175,6 +185,10 @@ object LatexWriter {
175185
case ToEval(_, _) => "Convert to function call"
176186
case FromEval(_) => "Convert from function call"
177187
case Rename(_, from, to) => s"Renaming $from to $to"
188+
case Wrap(Variable(name), _) => env(Path(name)) match {
189+
case SimpleObject(exp) => writeIdentityReference(env.toFull(Path(name)), Header(Nil, Nil), List(Variable(name), exp))
190+
}
191+
case Unwrap(_) => "Unwrapping"
178192
}
179193

180194
def writeIdentityReference(path: Path, header: Header, exps: List[Exp]): String = {

‎src/algebraic/manipulator/manipulation/Unwrap.scala

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
package algebraic.manipulator.manipulation
2+
3+
import algebraic.manipulator._
4+
import algebraic.manipulator.function.{InductiveFunction, SimpleFunction}
5+
import algebraic.manipulator.objects.SimpleObject
6+
7+
case class Unwrap(positions: Tree) extends PathManipulation(positions) {
8+
override def dependencies(env: Environment): Set[Path] = Set.empty
9+
10+
override def replace(env: Environment, exp: Exp): Exp = exp match {
11+
case Variable(name) => env(Path(name)) match {
12+
case SimpleObject(value) => value
13+
}
14+
case Operation(name, dummies, parameters) => env(Path(name)) match {
15+
case SimpleFunction(header, value) =>
16+
if (header.dummies.length != dummies.length)
17+
throw new IllegalArgumentException(s"Expected ${header.dummies.length} dummies, but recieved ${dummies.length}")
18+
if (header.parameters.length != parameters.length)
19+
throw new IllegalArgumentException(s"Expected ${header.parameters.length} arguments, but recieved ${parameters.length}")
20+
21+
val dumMap = header.dummies.zip(dummies).toMap
22+
val parMap = header.parameters.map(_.variable).zip(parameters).toMap
23+
value.setAll(dumMap, v => parMap.getOrElse(v, v))
24+
case InductiveFunction(header, base, steps) =>
25+
if (header.dummies.length != dummies.length)
26+
throw new IllegalArgumentException(s"Expected ${header.dummies.length} dummies, but recieved ${dummies.length}")
27+
if (header.parameters.length != parameters.length)
28+
throw new IllegalArgumentException(s"Expected ${header.parameters.length} arguments, but recieved ${parameters.length}")
29+
30+
val dumMap = header.dummies.zip(dummies).toMap
31+
val parMap = header.parameters.map(_.variable).zip(parameters).toMap
32+
val inductive = parMap(base.inductive)
33+
34+
if (base.value == inductive)
35+
return base.exp.setAll(dumMap, v => parMap.getOrElse(v, v))
36+
for (step <- steps) {
37+
val inner = inductive.get(step.step.tree.filter((base.inductive :: step.params.map(_.variable)).contains)).toMap
38+
if ((base.inductive :: step.params.map(_.variable)).forall(inner.contains)) {
39+
val indPar = step.step.set(v => inner.getOrElse(v, v))
40+
if (indPar == inductive) {
41+
val newParMap = parMap + (base.inductive -> indPar)
42+
return step.exp.setAll(dumMap, v => newParMap.getOrElse(v, v))
43+
}
44+
}
45+
}
46+
47+
throw new IllegalArgumentException(s"No case in $name matches $exp")
48+
}
49+
}
50+
}

‎src/algebraic/manipulator/manipulation/Wrap.scala

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
package algebraic.manipulator.manipulation
2+
import algebraic.manipulator._
3+
import algebraic.manipulator.function.{InductiveFunction, SimpleFunction}
4+
import algebraic.manipulator.objects.SimpleObject
5+
6+
case class Wrap(wrapper: Exp, positions: Tree) extends PathManipulation(positions) {
7+
override def dependencies(env: Environment): Set[Path] = env.dependencies(wrapper)
8+
9+
override def replace(env: Environment, exp: Exp): Exp = wrapper match {
10+
case Operation(name, dummies, parameters) => env(Path(name)) match {
11+
case SimpleFunction(header, value) =>
12+
if (header.dummies.length != dummies.length)
13+
throw new IllegalArgumentException(s"Expected ${header.dummies.length} dummies, but recieved ${dummies.length}")
14+
if (header.parameters.length != parameters.length)
15+
throw new IllegalArgumentException(s"Expected ${header.parameters.length} arguments, but recieved ${parameters.length}")
16+
val dumMap = header.dummies.zip(dummies).toMap
17+
val parMap = header.parameters.map(_.variable).zip(parameters).toMap
18+
val expect = value.setAll(dumMap, v => parMap.getOrElse(v, v))
19+
if (expect != exp)
20+
throw new IllegalArgumentException(s"Expected $expect, but recieved $exp")
21+
wrapper
22+
case InductiveFunction(header, base, steps) => ???
23+
}
24+
case Variable(name) => env(Path(name)) match {
25+
case SimpleObject(value) =>
26+
if (value != exp)
27+
throw new IllegalArgumentException(s"Expected $value, but recieved $exp")
28+
wrapper
29+
}
30+
}
31+
}

‎src/algebraic/manipulator/read/ProofReader.scala

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,9 @@ object ProofReader {
1515
("substitute" -> (readSubstitution(_: Tokens))) +
1616
("rename" -> (readRename(_: Tokens))) +
1717
("toeval" -> (readToEval(_: Tokens))) +
18-
("fromeval" -> (readFromEval(_: Tokens)))
18+
("fromeval" -> (readFromEval(_: Tokens))) +
19+
("wrap" -> (readWrap(_: Tokens))) +
20+
("unwrap" -> (readUnwrap(_: Tokens)))
1921

2022
var elementReaders: Map[String, Map[String, Tokens => Read[ElementTemplate]]] = Map.empty +
2123
("struct" -> StructureTemplate.readers) +
@@ -156,6 +158,18 @@ object ProofReader {
156158
(FromEval(pos), tail)
157159
}
158160

161+
def readWrap(tokens: Tokens.Tokens): Read[Wrap] = {
162+
val (exp, t1) = readExp(tokens)
163+
val (pos, t2) = readTree(t1.expect(COLON))
164+
165+
(Wrap(exp, pos), t2)
166+
}
167+
168+
def readUnwrap(tokens: Tokens.Tokens): Read[Unwrap] = {
169+
val (pos, tail) = readTree(tokens.expect(COLON))
170+
(Unwrap(pos), tail)
171+
}
172+
159173
def readHeader(tokens: Tokens): Read[Header] = {
160174
val (dum, t1) = tokens.whenBlock(LESSGREAT, _.readList(COMMA, readVariable))
161175
val (par, t2) = t1.readList(COMMA, PARENTHESES, readDefinition)

‎work/base/Add.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
import Numbers
22

3+
assume fn add(Complex, Complex)
4+
35
assume Commute(Complex a, Complex b)
46
add(a,b)=add(b,a);
57

‎work/base/Div.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
import Numbers
22

3+
assume div(Complex, Complex)
4+
35
assume Mult1(Complex a, Complex b)
46
a=div(mult(a,b),b)=mult(div(a,b),b);
57

‎work/base/Log.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
import Numbers
22

3+
assume Pow(Complex a, Complex b)
4+
35
assume Pow(Complex a, Complex b)
46
b=log(a,pow(a,b))=pow(a,log(a,b));
57

‎work/base/Mult.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
import Numbers
22

3+
assume fn mult(Complex, Complex)
4+
35
assume Identity(Complex a)
46
a=mult(a,1)=mult(1,a);
57

‎work/base/Pow.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
import Numbers
22

3+
assume pow(Complex, Complex)
4+
35
assume Definition(Complex a, Complex n, Complex m)
46
pow(a,add(n,m))=mult(pow(a,n),pow(a,m));
57

‎work/base/Sub.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
import Numbers
22

3+
assume fn sub(Complex a, Complex b)
4+
35
assume Add1(Complex a, Complex b)
46
a=sub(add(a,b),b)=add(sub(a,b),b);
57

‎work/calculus/Diff.txt

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,10 @@ using base.Div;
77
using base.Pow;
88
using base.Log;
99

10+
define diff(Complex -> Complex f) = func<x>(lim<h>(0,div(sub(eval(f,add(x,h)),eval(f,x)),h)))
11+
1012
assume Lim<h>(Complex -> Complex f, Complex x)
11-
diff(eval(f,x),x)=lim<h>(0,div(sub(eval(f,add(x,h)),eval(f,x)),h));
13+
diff(eval(f,x),x) = lim<h>(0,div(sub(eval(f,add(x,h)),eval(f,x)),h));
1214

1315
work Factor(Complex -> Complex f, Complex a, Complex x) {
1416
let 2 diff(mult(a,eval(f,x)),x);
@@ -202,7 +204,7 @@ work Ln(Complex x) {
202204
substitute Lim.Func[0->2]<h>:1,0,0;
203205
fromeval:1,0,0,[0|1];
204206
substitute ~Div.Singularity:1,0,0,0;
205-
substitute ~Euler<h>:1,0,0;
207+
wrap e:1,0,0;
206208
substitute Ln.Inverse:1,0;
207209
} result {
208210
diff(ln(x),x)=div(1,x)

‎work/calculus/Euler.txt

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,2 @@
11

22
define object e=lim<h>(0,pow(add(1,h),div(1,h)))
3-
4-
assume Euler<h>()
5-
e=lim<h>(0,pow(add(1,h),div(1,h)));

‎work/calculus/Ln.txt

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,46 +2,45 @@ import Numbers
22
import calculus.Euler
33
using base.Log
44

5-
assume Ln(Complex a)
6-
ln(a)=log(e,a);
5+
define ln(Complex a) = log(e, a);
76

87
work Pow(Complex a) {
98
let 3 a;
109
substitute Log.Pow[0->1](e,-):1;
1110
substitute Log.Pow[0->2](e,-):2;
12-
substitute ~Ln:[1|2,1];
11+
wrap ln:[1|2,1];
1312
} result {
1413
a=ln(pow(e,a))=pow(e,ln(a))
1514
}
1615

1716
work Inverse() {
1817
let 2 log(e,e);
1918
substitute Log.Inverse:1;
20-
substitute ~Ln:0;
19+
wrap ln:0;
2120
} result {
2221
ln(e)=1
2322
}
2423

2524
work Singularity() {
2625
let 2 log(e,1);
2726
substitute Log.Singularity:1;
28-
substitute ~Ln:0;
27+
wrap ln:0;
2928
} result {
3029
ln(1)=0
3130
}
3231

3332
work Distribute(Complex a, Complex b) {
3433
let 2 log(e,mult(a,b));
3534
substitute Log.Distribute:1;
36-
substitute ~Ln:[0|1,[0|1]];
35+
wrap ln:[0|1,[0|1]];
3736
} result {
3837
ln(mult(a,b))=add(ln(a),ln(b))
3938
}
4039

4140
work DistributeSub(Complex a, Complex b) {
4241
let 2 log(e,div(a,b));
4342
substitute Log.DistributeSub:1;
44-
substitute ~Ln:[0|1,[0|1]];
43+
wrap ln:[0|1,[0|1]];
4544
} result {
4645
ln(div(a,b))=sub(ln(a),ln(b))
4746
}
@@ -50,15 +49,15 @@ work Mult(Complex a, Complex p) {
5049
let 3 log(e,pow(a,p));
5150
substitute Log.Mult[0->1]:1;
5251
substitute Log.Mult[0->2]:2;
53-
substitute ~Ln:[0|1,0|2,1];
52+
wrap ln:[0|1,0|2,1];
5453
} result {
5554
ln(pow(a,p))=mult(ln(a),p)=mult(p,ln(a))
5655
}
5756

5857
work ChangeBase(Complex a, Complex b) {
5958
let 2 log(a,b);
6059
substitute Log.ChangeBase(-,-,e):1;
61-
substitute ~Ln:1,[0|1];
60+
wrap ln:1,[0|1];
6261
} result {
6362
log(a,b)=div(ln(b),ln(a))
6463
}

0 commit comments

Comments
 (0)