Skip to content

Commit

Permalink
Languages example. Work on the viewer.
Browse files Browse the repository at this point in the history
  • Loading branch information
@ericfinster
ericfinster committed Apr 15, 2015
1 parent bcb500a commit 87c7d57
Show file tree
Hide file tree
Showing 4 changed files with 72 additions and 29 deletions.
1 change: 1 addition & 0 deletions examples/languages.xml
View file

Large diffs are not rendered by default.

42 changes: 35 additions & 7 deletions orchard-javafx/src/main/scala/orchard/ui/javafx/OrchardEditor.scala
View file
Expand Up @@ -334,7 +334,7 @@ object OrchardEditor extends PopupManager(new VBox)
case KeyCode.M => if (ev.isControlDown) onNewModule
case KeyCode.I => if (ev.isControlDown) onImportSubstitution
case KeyCode.V => if (ev.isControlDown) { if (ev.isShiftDown) onNewSubstInShell else onNewSubstitution }
// case KeyCode.X => if (ev.isControlDown) onCloseWorkspace
case KeyCode.X => if (ev.isControlDown) onExtend
case KeyCode.L => if (ev.isControlDown) onAbstract
case KeyCode.W => if (ev.isControlDown) onCancelSubstitution
case KeyCode.R => if (ev.isControlDown) onRename
Expand All @@ -353,18 +353,36 @@ object OrchardEditor extends PopupManager(new VBox)
}
})

def onExtend =
for {
wksp <- activeWorkspace
sheet <- wksp.activeSheet
} {
sheet.extend
}

def onDumpAgda =
for {
wksp <- activeWorkspace
sheet <- wksp.activeSheet
selectedCell <- sheet.selectionBase
} {
val dumpCell : NCell[String] = selectedCell.neutralNCell map {
case None => "None"
case Some(expr) => expr.id
// val dumpCell : NCell[String] = selectedCell.neutralNCell map {
// case None => "None"
// case Some(expr) => expr.id
// }

import orchard.core.complex._

val dumpCell = sheet.toCell map {
case Positive => "pos"
case Negative => "neg"
case Neutral(None) => "(neutral nothing)"
case Neutral(Some(expr)) => "(neutral (just " ++ expr.id ++ "))"
}

println(NCell.agdaSyntax(dumpCell))

}

def onDumpScala =
Expand All @@ -373,9 +391,19 @@ object OrchardEditor extends PopupManager(new VBox)
sheet <- wksp.activeSheet
selectedCell <- sheet.selectionBase
} {
val dumpCell : NCell[String] = selectedCell.neutralNCell map {
case None => "None"
case Some(expr) => expr.id
// val dumpCell : NCell[String] = selectedCell.neutralNCell map {
// case None => "None"
// case Some(expr) => expr.id
// }


import orchard.core.complex._

val dumpCell = sheet.toCell map {
case Positive => "Positive()"
case Negative => "Negative()"
case Neutral(None) => "Neutral(None)"
case Neutral(Some(expr)) => "Neutral(Some(" ++ expr.id ++ "))"
}

println(NCell.scalaSyntax(dumpCell))
Expand Down
35 changes: 21 additions & 14 deletions orchard-javafx/src/main/scala/orchard/ui/javafx/OrchardViewer.scala
View file
Expand Up @@ -20,6 +20,10 @@ import javafx.event.EventHandler
import javafx.scene.input.KeyCode
import javafx.scene.input.KeyEvent

import javax.imageio.ImageIO
import javafx.scene.SnapshotParameters
import javafx.embed.swing.SwingFXUtils

import javafx.scene.{layout => jfxsl}

import orchard.core.cell._
Expand Down Expand Up @@ -269,6 +273,7 @@ class OrchardViewer(implicit pm : PopupManager) extends Dialog {
def handle(ev : KeyEvent) {
ev.getCode match {
// case KeyCode.X => close
case KeyCode.W => onWrite
case _ => ()
}
}
Expand All @@ -278,23 +283,25 @@ class OrchardViewer(implicit pm : PopupManager) extends Dialog {
def onShow = ()
def onHide = ()

// def onWrite = {
// fileChooser.setTitle("Export Snapshot")
def onWrite = {

val fc = OrchardEditor.fileChooser
fc.setTitle("Export Snapshot")

// val file = fileChooser.showSaveDialog(getScene.getWindow)
val file = fc.showSaveDialog(getScene.getWindow)

// if (file != null) {
if (file != null) {

// val image = viewerArea.content.head.snapshot(new SnapshotParameters, null)
val image = viewerArea.content.head.snapshot(new SnapshotParameters, null)

// try {
// ImageIO.write(SwingFXUtils.fromFXImage(image, null), "png", file)
// } catch {
// case e : java.io.IOException => {
// println("There was an error writing to the file!.")
// }
// }
// }
// }
try {
ImageIO.write(SwingFXUtils.fromFXImage(image, null), "png", file)
} catch {
case e : java.io.IOException => {
println("There was an error writing to the file!.")
}
}
}
}

}
23 changes: 15 additions & 8 deletions orchard-lib/src/main/scala/orchard/core/cell/Cell.scala
View file
Expand Up @@ -301,18 +301,25 @@ object NCell {
}
}

def addParens(str : String) : String =
if (str.contains(' ')) {
"(" ++ str ++ ")"
} else {
str
}

def verticalTraverse(t : CellTree[D, String]) : String =
t match {
case Seed(obj, _) => "pt (" ++ obj.toString ++ ")"
case Leaf(shape, _) => { index += 1 ; "leaf " ++ addresses(perm(index)).toAgda }
case Seed(obj, _) => "pt " ++ addParens(obj.toString)
case Leaf(shape, _) => { index += 1 ; "leaf" } // ++ addresses(perm(index)).toAgda }
case Graft(cell, branches, _) => {
// Recurse on the branches, getting their string. then "plug these into" the result
// by traversing the cells source tree.

val verticalExprs = new Stack ++ (branches map (verticalTraverse(_)))

cell match {
case Object(value, _) => "node (" ++ value.toString ++ ") (" ++ verticalExprs.pop ++ ")"
case Object(value, _) => "node " ++ addParens(value.toString) ++ " " ++ addParens(verticalExprs.pop)
case Composite(value, srcTree, tgtValue, _) => {

def horizontalTraverse(tr : CellTree[D#Pred, String]) : CellTree[D#Pred, String] =
Expand All @@ -333,7 +340,7 @@ object NCell {
}
}

"node (" ++ value.toString ++ ") (" ++ cellTreeAgdaSyntax(horizontalTraverse(srcTree)) ++ ")"
"node " ++ addParens(value.toString) ++ " " ++ addParens(cellTreeAgdaSyntax(horizontalTraverse(srcTree)))
}
}
}
Expand All @@ -345,7 +352,7 @@ object NCell {

def cellScalaSyntax[D <: Nat](cell : Cell[D, String]) : String =
cell match {
case Object(value, ev) => "Pointt(" ++ value.toString ++ ")"
case Object(value, ev) => "Point(" ++ value.toString ++ ")"
case Composite(value, srcTree, tgtValue, ev) => cellTreeScalaSyntax(srcTree)
}

Expand All @@ -366,7 +373,7 @@ object NCell {
def verticalTraverse(t : CellTree[D, String]) : String =
t match {
case Seed(obj, _) => "Pt(" ++ obj.toString ++ ")"
case Leaf(shape, _) => { index += 1 ; "Leaf(" ++ addresses(perm(index)).toScala ++ ")" }
case Leaf(shape, _) => { index += 1 ; "Leaf(__" ++ S(shape.dim).toInt.toString ++ ")" }
case Graft(cell, branches, _) => {
// Recurse on the branches, getting their string. then "plug these into" the result
// by traversing the cells source tree.
Expand Down Expand Up @@ -499,7 +506,7 @@ object NCell {

def generateCell[D <: Nat : HasPred](cellLbl : A, srcs : CellTree[D#Pred, String], tgtLbl : A) = {

val lblString = "ext " ++ cellLbl.toString ++ " (" ++ cellTreeAgdaSyntax(srcs.addrTree map (_.toAgda)) ++ ")"
val lblString = "ext " ++ cellLbl.toString // ++ " (" ++ cellTreeAgdaSyntax(srcs.addrTree map (_.toAgda)) ++ ")"
val tgtString = "int " ++ tgtLbl.toString ++ " (" ++ cellTreeAgdaSyntax(srcs) ++ ")"

CompositeCell(lblString, srcs, tgtString)
Expand All @@ -515,7 +522,7 @@ object NCell {

def generateCell[D <: Nat : HasPred](cellLbl : A, srcs : CellTree[D#Pred, String], tgtLbl : A) = {

val lblString = "Dot(" ++ cellLbl.toString ++ ", " ++ cellTreeScalaSyntax(srcs.addrTree map (_.toScala)) ++ ")"
val lblString = "Dot(" ++ cellLbl.toString ++ ", __" ++ S(srcs.dimension).toInt.toString ++ ")" // ", " ++ cellTreeScalaSyntax(srcs.addrTree map (_.toScala)) ++ ")"
val tgtString = "Box(" ++ tgtLbl.toString ++ ", " ++ cellTreeScalaSyntax(srcs) ++ ")"

CompositeCell(lblString, srcs, tgtString)
Expand Down

0 comments on commit 87c7d57

Please sign in to comment.