Skip to content

Commit 6efa064

Browse files
adamAndMathadamAndMath
committed
Added parsing and construction of functions
1 parent cf0b6ef commit 6efa064

9 files changed

+127
-35
lines changed

‎src/algebraic/manipulator/function/AssumedFunction.scala

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
package algebraic.manipulator.function
2+
3+
import algebraic.manipulator.{Environment, Path, Type}
4+
5+
case class AssumedFunction(params: List[Type]) extends FunctionElement {
6+
override def paramTypes: List[Type] = params
7+
8+
override def dependencies(env: Environment): Set[Path] = env.dependencies(params)
9+
}

‎src/algebraic/manipulator/function/Function.scala

Lines changed: 0 additions & 7 deletions
This file was deleted.

‎src/algebraic/manipulator/function/FunctionElement.scala

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
package algebraic.manipulator.function
2+
3+
import algebraic.manipulator.{Element, Type}
4+
5+
trait FunctionElement extends Element {
6+
def paramTypes: List[Type]
7+
}

‎src/algebraic/manipulator/function/InductiveFunction.scala

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2,18 +2,18 @@ package algebraic.manipulator.function
22

33
import algebraic.manipulator._
44

5-
case class InductiveFunction(params: List[Definition], base: InductiveBase, steps: List[InductiveStep]) extends Function {
6-
override def paramTypes: List[Type] = params.map(_.varType)
5+
case class InductiveFunction(header: Header, base: InductiveBase, steps: List[InductiveStep]) extends FunctionElement {
6+
override def paramTypes: List[Type] = header.parameters.map(_.varType)
77

88
override def dependencies(env: Environment): Set[Path] =
9-
env.dependencies(params) ++ env.bind(params).dependencies(base :: steps)
9+
env.dependencies(header) ++ header.bind(env).dependencies(base :: steps)
1010
}
1111

12-
case class InductiveBase(inductives: Map[Variable, Exp], exp: Exp) extends Depending {
13-
override def dependencies(env: Environment): Set[Path] = env.dependencies(exp :: inductives.values.toList)
12+
case class InductiveBase(inductive: Variable, value: Exp, exp: Exp) extends Depending {
13+
override def dependencies(env: Environment): Set[Path] = env.dependencies(List(value, exp))
1414
}
1515

16-
case class InductiveStep(v: Variable, params: List[Definition], exp: Exp) extends Depending {
16+
case class InductiveStep(params: List[Definition], step: Exp, exp: Exp) extends Depending {
1717
override def dependencies(env: Environment): Set[Path] =
18-
env.dependencies(params) ++ env.bind(params).dependencies(params)
18+
env.dependencies(params) ++ env.bind(params).dependencies(List(step, exp))
1919
}

‎src/algebraic/manipulator/function/SimpleFunction.scala

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,9 @@ package algebraic.manipulator.function
22

33
import algebraic.manipulator._
44

5-
case class SimpleFunction(params: List[Definition], exp: Exp) extends Function {
6-
override def paramTypes: List[Type] = params.map(_.varType)
5+
case class SimpleFunction(header: Header, exp: Exp) extends FunctionElement {
6+
override def paramTypes: List[Type] = header.parameters.map(_.varType)
77

88
override def dependencies(env: Environment): Set[Path] =
9-
env.dependencies(params) ++ env.bind(params).dependencies(exp)
9+
env.dependencies(header) ++ header.bind(env).dependencies(exp)
1010
}

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

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ object LatexWriter {
6868
case InductiveStructure(_, _) => true
6969
case SimpleStructure => false
7070
case _: ObjectElement => true
71-
case _: Function => true
71+
case _: FunctionElement => true
7272
case _: Identity => false
7373
}
7474

@@ -81,6 +81,13 @@ object LatexWriter {
8181
s"$$${writeDefinition(Header(Nil, base.params))}: ${writeExp(base.exp)} \\in $typeOut$$" +
8282
steps.map(step => s" and $$${writeDefinition(Header(Nil, Definition(SimpleType(name), step.v.name) :: step.params))}: ${writeExp(step.exp)} \\in $typeOut$$").mkString +
8383
"\\\\\n"
84+
case SimpleFunction(header, exp) => s"Let $$${writeExp(Operation(name, header.dummies, header.parameters.map(_.variable)))} = ${writeExp(exp)}\\\n"
85+
case InductiveFunction(header, base, steps) =>
86+
s"Let $$${writeExp(Operation(name, header.dummies, header.parameters.map(_.variable)))} = \n" +
87+
" \\begin{cases}\n" +
88+
s" ${base.exp} & \\quad ${base.inductive} = ${base.value}" +
89+
s"${steps.map(s => s"\\\\\n ${s.exp} & \\quad ${s.step}").mkString}" +
90+
"\n \\end{cases}$\\\\\n"
8491
}
8592

8693
def writeAssumption(assumption: Assumption): String =

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

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
package algebraic.manipulator.read
2+
3+
import algebraic.manipulator.{Environment, Exp, Header, Path, Type}
4+
import algebraic.manipulator.function._
5+
import algebraic.manipulator.read.ProofReader._
6+
import algebraic.manipulator.read.Tokens._
7+
8+
trait FunctionTemplate extends ElementTemplate {
9+
override def apply(env: Environment): FunctionElement
10+
}
11+
12+
object FunctionTemplate {
13+
var readers: Map[String, Tokens => Read[FunctionTemplate]] = Map.empty +
14+
("assume" -> (readAssumption(_: Tokens))) +
15+
("define" -> (readDefine(_: Tokens))) +
16+
("inductive" -> (readInductive(_: Tokens)))
17+
18+
def readAssumption(tokens: Tokens.Tokens): Read[AssumedFunctionTemplate] = {
19+
val (params, tail) = tokens.expect(PARENTHESES, _.readList(COMMA, readType))
20+
21+
(AssumedFunctionTemplate(params), tail)
22+
}
23+
24+
def readDefine(tokens: Tokens.Tokens): Read[SimpleFunctionTemplate] = {
25+
val (header, t1) = readHeader(tokens)
26+
val (exp, t2) = readExp(t1)
27+
28+
(SimpleFunctionTemplate(header, exp), t2)
29+
}
30+
31+
def readInductive(tokens: Tokens.Tokens): Read[InductiveFunctionTemplate] = {
32+
val (header, tail) = readHeader(tokens)
33+
tail.expect(BLOCK, tokens => {
34+
val (base, t1) = readInductiveBase(tokens)
35+
val (steps, t2) = t1.whileNot(CLOSE_BLOCK, readInductiveStep)
36+
37+
(InductiveFunctionTemplate(header, base, steps), t2)
38+
})
39+
}
40+
41+
def readInductiveBase(tokens: Tokens): Read[InductiveBase] = {
42+
val (inductive, t1) = readVariable(tokens.expect("base"))
43+
val (value, t2) = readExp(t1.expect(EQUAL))
44+
val (exp, t3) = readExp(t2.expect(IMPLY))
45+
46+
(InductiveBase(inductive, value, exp), t3.ignore(SEMI))
47+
}
48+
49+
def readInductiveStep(tokens: Tokens): Read[InductiveStep] = {
50+
val (params, t1) = tokens.expect("step").whenBlock(PARENTHESES, _.readList(COMMA, readDefinition))
51+
val (step, t2) = readExp(t1)
52+
val (exp, t3) = readExp(t2.expect(IMPLY))
53+
54+
(InductiveStep(params.getOrElse(Nil), step, exp), t3.ignore(SEMI))
55+
}
56+
57+
case class AssumedFunctionTemplate(params: List[Type]) extends FunctionTemplate {
58+
override def apply(env: Environment): FunctionElement = AssumedFunction(params)
59+
60+
override def dependencies(env: Environment): Set[Path] = env.dependencies(params)
61+
}
62+
63+
case class SimpleFunctionTemplate(header: Header, exp: Exp) extends FunctionTemplate {
64+
override def apply(env: Environment): FunctionElement = SimpleFunction(header, exp)
65+
66+
override def dependencies(env: Environment): Set[Path] =
67+
env.dependencies(header) ++ header.bind(env).dependencies(exp)
68+
}
69+
70+
case class InductiveFunctionTemplate(header: Header, base: InductiveBase, steps: List[InductiveStep]) extends FunctionTemplate {
71+
override def apply(env: Environment): FunctionElement = InductiveFunction(header, base, steps)
72+
73+
override def dependencies(env: Environment): Set[Path] =
74+
env.dependencies(header) ++ header.bind(env).dependencies(base :: steps)
75+
}
76+
}

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

Lines changed: 10 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,11 @@ object ProofReader {
1717
("toeval" -> (readToEval(_: Tokens))) +
1818
("fromeval" -> (readFromEval(_: Tokens)))
1919

20+
var elementReaders: Map[String, Map[String, Tokens => Read[ElementTemplate]]] = Map.empty +
21+
("struct" -> StructureTemplate.readers) +
22+
("object" -> ObjectTemplate.readers) +
23+
("fn" -> FunctionTemplate.readers)
24+
2025
def readTree(tokens: Tokens): Read[Tree] = {
2126
val (tree, t1) = {
2227
if (tokens is OPEN_BRAC) readTreeBrac(tokens)
@@ -160,26 +165,16 @@ object ProofReader {
160165

161166
def readElement(tokens: Tokens): Read[(String, ElementTemplate)] = {
162167
tokens.tail.token match {
163-
case STRING("struct") =>
164-
val (typeName, t1) = tokens.string()
165-
val (name, t2) = t1.tail.string()
166-
167-
if (!StructureTemplate.readers.contains(typeName))
168-
throw new TokenException(tokens, s"$typeName is not a valid structure type")
169-
170-
val (structure, t3) = StructureTemplate.readers(typeName)(t2)
171-
172-
((name, structure), t3)
173-
case STRING("object") =>
168+
case STRING(t) if elementReaders.contains(t) =>
174169
val (typeName, t1) = tokens.string()
175170
val (name, t2) = t1.tail.string()
176171

177-
if (!ObjectTemplate.readers.contains(typeName))
178-
throw new TokenException(tokens, s"$typeName is not a valid structure type")
172+
if (!elementReaders(t).contains(typeName))
173+
throw new TokenException(tokens, s"$typeName is not a valid $t type")
179174

180-
val (obj, t3) = ObjectTemplate.readers(typeName)(t2)
175+
val (elm, t3) = elementReaders(t)(typeName)(t2)
181176

182-
((name, obj), t3)
177+
((name, elm), t3)
183178
case _ =>
184179
val (typeName, t1) = tokens.string()
185180
val (name, t2) = t1.string()

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

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,12 @@ object Tokens {
3939
} else
4040
go(Token(pos, line, SLASH, prev), pos + 1, line, code.tail)
4141
case '\\' => go(Token(pos, line, BACKSLASH, prev), pos + 1, line, code.tail)
42-
case '=' => go(Token(pos, line, EQUAL, prev), pos + 1, line, code.tail)
4342
case '+' => go(Token(pos, line, PLUS, prev), pos + 1, line, code.tail)
43+
case '=' =>
44+
if (code.tail.head == '>')
45+
go(Token(pos, line, IMPLY, prev), pos + 2, line, code.tail.tail)
46+
else
47+
go(Token(pos, line, EQUAL, prev), pos + 1, line, code.tail)
4448
case '-' =>
4549
if (code.tail.head == '>')
4650
go(Token(pos, line, ARROW, prev), pos + 2, line, code.tail.tail)
@@ -205,8 +209,9 @@ object Tokens {
205209
case object SEMI extends ProofToken
206210
case object SLASH extends ProofToken
207211
case object BACKSLASH extends ProofToken
208-
case object EQUAL extends ProofToken
209212
case object PLUS extends ProofToken
213+
case object EQUAL extends ProofToken
214+
case object IMPLY extends ProofToken
210215
case object DASH extends ProofToken
211216
case object ARROW extends ProofToken
212217
case object TILDE extends ProofToken

0 commit comments

Comments
 (0)