From ee87c06f4dd78be89ff94c75093ed0b1c4100d09 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Sat, 23 Jan 2021 00:36:14 -0500
Subject: [PATCH 01/10] json first

---
 examples/json.dx  | 192 ++++++++++++++++++++++++++++++++++++++++++++++
 static/index.html |   2 +
 2 files changed, 194 insertions(+)
 create mode 100644 examples/json.dx

diff --git a/examples/json.dx b/examples/json.dx
new file mode 100644
index 000000000..9cdeb89f6
--- /dev/null
+++ b/examples/json.dx
@@ -0,0 +1,192 @@
+
+
+' ## Additional Prelude
+
+def join (extra: List a) (lists:n=>(List a)) : List a =
+    concat $ for i.
+        case ordinal i == (size n - 1) of
+             True -> lists.i
+             False -> lists.i <> extra
+
+interface Enum a
+         enum : List a
+
+
+' # JSON Implementation
+
+data JValue = AsJValue String
+-- TODO - once Dex supports recursive ADT JValue becomes Value.
+
+data Value = 
+     AsObject (List (String & JValue))
+     AsArray (List JValue)
+     AsString String
+     AsFloat Float
+     AsInt Int
+
+interface ToJSON a
+  toJSON : a -> Value
+
+
+-- These three are private methods. Users should use type classes.
+def escape (x:JValue) : String =
+    (AsJValue y) = x
+    y
+
+
+def collapse (x:Value) : JValue =
+    AsJValue $ case x of
+         AsString y ->  "\"" <> y <> "\""
+         AsFloat y -> show y
+         AsInt y -> show y
+         AsObject (AsList _ y) ->
+              ("{" <> (join ", " $ for i.
+                 (k, v) = y.i 
+                 "\"" <> k <> "\"" <> ":" <> (escape v)) <> "}")
+         AsArray (AsList _ y) -> ("[" <> (join ", " $ for i. escape y.i) <> "]")
+
+def hide [ToJSON a] (x:a) : JValue =
+    collapse $ toJSON x
+
+instance Show Value 
+  show = \x. escape $ collapse x
+
+instance ToJSON String
+  toJSON = AsString
+  
+instance ToJSON Int
+  toJSON = AsInt
+  
+instance ToJSON Float
+  toJSON = AsFloat
+  
+instance ToJSON Value
+  toJSON = id
+  
+instance [ToJSON v] ToJSON ((Fin n) => v)
+  toJSON = \x . AsArray $ AsList _ $ for i. hide x.i
+
+instance [ToJSON v] ToJSON ((Fin n) => (String & v))
+  toJSON = \x . AsObject $ AsList _ $ for i. (fst x.i, hide $ snd x.i)
+
+instance [ToJSON v] ToJSON (List (String & v))
+  toJSON = \(AsList _ x) . toJSON x
+
+
+' ## Data Frame
+
+data DataFrame key n value =
+     AsDataFrame (n => key => value) (key => String)
+
+a_data = ["A", "B", "C", "D", "E", "F", "G", "H", "I"]
+b_data = [28, 55, 43, 91, 81, 53, 19, 87, 52]
+
+bar : DataFrame (Fin 2) (Fin 9) Value = 
+    AsDataFrame  (for i. [toJSON a_data.i, toJSON b_data.i]) (["a", "b"])
+
+' VEGA LITE
+
+Options = List (String & String)
+
+data Mark =
+     AsMark String Options
+
+data EncodingType =
+     Quantitative
+     Nominal
+     Ordinal
+
+instance Show EncodingType
+         show = (\ x.
+              case x of
+                   Quantitative -> "quantitative"
+                   Nominal -> "nominal"
+                   Ordinal -> "ordinal")
+                   
+data Channel =
+     Y
+     X
+     Color
+     
+instance Show Channel
+         show = (\ x.
+              case x of
+                   Y -> "y"
+                   X -> "x"
+                   Color -> "color")
+
+data Encoding key =
+     AsEncoding Channel key EncodingType Options
+
+def enc (c:Channel) (k:Int) (et: EncodingType) : Encoding key =
+    AsEncoding c (k@_) et mempty
+
+def mark (m:String) : Mark =
+    AsMark m mempty
+
+def chart [ToJSON v] (x: DataFrame (Fin key) (Fin n) v)
+                     (mark: Mark)
+                     (encs : (Fin m) => Encoding (Fin key))
+             : Value =
+    
+    (AsMark mtype options) = mark
+    jmark = ("mark", toJSON ((AsList _ [("type", mtype)]) <> options))
+    (AsDataFrame df names) = x
+    jdf = toJSON $ for i. toJSON $ for k.
+                   ("field" <> (show $ ordinal k), toJSON df.i.k)
+    jdata = ("data", toJSON [("values", jdf)])
+    jencodings = toJSON $ for i.
+        (AsEncoding channel key type encoptions) = encs.i
+        (show channel, toJSON ((AsList _ [
+              ("field", "field" <> (show $ ordinal key)),
+              ("type", show type),
+              ("title", names.key)
+              ])
+                               <> encoptions))
+    jencode = ("encoding", jencodings)
+    toJSON [jdata, jmark, jencode]
+    
+
+
+def showVega (x: Value) : String =
+    "<iframe style=\"border:0\" height=\"300px\" width=\"700px\" srcdoc='<html>  <head><script src=\"https://cdn.jsdelivr.net/npm/vega@5.17.0\"></script>  <script src=\"https://cdn.jsdelivr.net/npm/vega-lite@4.17.0\"></script>  <script src=\"https://cdn.jsdelivr.net/npm/vega-embed@6.12.2\"></script> </head> <body> <div id=\"vis\"></div><script>vegaEmbed(\"#vis\"," <> (show x) <> ");</script></body></html>'</iframe>"
+
+c = chart bar (mark "bar") [enc X 0 Nominal,
+                            enc Y 1 Quantitative] 
+
+show c
+
+:html showVega $ c
+
+
+' ## More Examples
+
+data Class =
+     A
+     B
+     C
+
+instance Show Class
+         show = \x . case x of
+               A -> "Apples"
+               B -> "Bananas"
+               C -> "Cucumbers"
+
+keys : (Fin 5) => Key = splitKey $ newKey 1
+x1 : (Fin 100) => Float = arb $ keys.(0 @ _)
+x2 : (Fin 100) => Float = arb $ keys.(1 @ _)
+label : (Fin 100) => Class =
+      x = arb $ keys.(2 @ _)
+      for i. [A, B, C] (x.i)
+
+
+df = (AsDataFrame
+        (for i. [toJSON $ x1.i, toJSON $ x2.i, toJSON $ show label.i])
+        (["X1", "X2", "Label"]))
+
+
+:html showVega $ chart df (mark "point") [enc X 0 Quantitative,
+                                          enc Y 1 Quantitative,
+                                          enc Color 2 Nominal] 
+
+
diff --git a/static/index.html b/static/index.html
index d1774f2ec..93d8893db 100644
--- a/static/index.html
+++ b/static/index.html
@@ -10,6 +10,8 @@
   <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.12.0/dist/katex.min.css" integrity="sha384-AfEj0r4/OFrOo5t7NnNe46zW/tFgW6x/bCJG8FqQCEo3+Aro6EYUG4+cU+KJWu/X" crossorigin="anonymous">
   <script defer src="https://cdn.jsdelivr.net/npm/katex@0.12.0/dist/katex.min.js" integrity="sha384-g7c+Jr9ZivxKLnZTDUhnkOnsh30B4H0rpLUpJ4jAIKs4fnJI+sEnkvrMWph2EDg4" crossorigin="anonymous"></script>
   <script defer src="https://cdn.jsdelivr.net/npm/katex@0.12.0/dist/contrib/auto-render.min.js" integrity="sha384-mll67QQFJfxn0IYznZYonOWZ644AWYC+Pt2cHqMaRhXVrursRwvLnLaebdGIlYNa" crossorigin="anonymous"></script>
+
+
 </head>
 
 <body>

From 228bad600f3a610eb496a07ecd2cd9e012752804 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Sat, 23 Jan 2021 01:28:17 -0500
Subject: [PATCH 02/10] .

---
 examples/json.dx | 134 +++++++++++++++++++++++++++++++++++------------
 1 file changed, 100 insertions(+), 34 deletions(-)

diff --git a/examples/json.dx b/examples/json.dx
index 9cdeb89f6..d7abc583e 100644
--- a/examples/json.dx
+++ b/examples/json.dx
@@ -1,6 +1,9 @@
 
 
-' ## Additional Prelude
+' # Declarative Graphing
+
+
+' ## JSON Implementation
 
 def join (extra: List a) (lists:n=>(List a)) : List a =
     concat $ for i.
@@ -8,11 +11,6 @@ def join (extra: List a) (lists:n=>(List a)) : List a =
              True -> lists.i
              False -> lists.i <> extra
 
-interface Enum a
-         enum : List a
-
-
-' # JSON Implementation
 
 data JValue = AsJValue String
 -- TODO - once Dex supports recursive ADT JValue becomes Value.
@@ -73,18 +71,7 @@ instance [ToJSON v] ToJSON (List (String & v))
   toJSON = \(AsList _ x) . toJSON x
 
 
-' ## Data Frame
-
-data DataFrame key n value =
-     AsDataFrame (n => key => value) (key => String)
-
-a_data = ["A", "B", "C", "D", "E", "F", "G", "H", "I"]
-b_data = [28, 55, 43, 91, 81, 53, 19, 87, 52]
-
-bar : DataFrame (Fin 2) (Fin 9) Value = 
-    AsDataFrame  (for i. [toJSON a_data.i, toJSON b_data.i]) (["a", "b"])
-
-' VEGA LITE
+' ## Graph Grammars (Vega-Lite Spec)
 
 Options = List (String & String)
 
@@ -107,13 +94,23 @@ data Channel =
      Y
      X
      Color
+     Tooltip
+     HREF
+     Row
+     Col
+     Size
      
 instance Show Channel
          show = (\ x.
               case x of
                    Y -> "y"
                    X -> "x"
-                   Color -> "color")
+                   Color -> "color"
+                   Tooltip -> "tooltip"
+                   HREF -> "href"
+                   Size -> "size"
+                   Row -> "row"
+                   Col -> "col")
 
 data Encoding key =
      AsEncoding Channel key EncodingType Options
@@ -124,15 +121,26 @@ def enc (c:Channel) (k:Int) (et: EncodingType) : Encoding key =
 def mark (m:String) : Mark =
     AsMark m mempty
 
-def chart [ToJSON v] (x: DataFrame (Fin key) (Fin n) v)
+def optsList (x:Options) : List (String & Value) =
+    (AsList _  tab) = x
+    AsList _ $ for i. (fst tab.i, toJSON $ snd tab.i)
+
+
+data DataFrame key n value =
+     AsDataFrame (n => key => value) (key => String)
+
+
+def chart [ToJSON v] (x: DataFrame (Fin key) n v)
                      (mark: Mark)
                      (encs : (Fin m) => Encoding (Fin key))
+                     (opts : Options)
              : Value =
     
     (AsMark mtype options) = mark
     jmark = ("mark", toJSON ((AsList _ [("type", mtype)]) <> options))
     (AsDataFrame df names) = x
-    jdf = toJSON $ for i. toJSON $ for k.
+    finsize = (Fin $ size n)
+    jdf = toJSON $ unsafeCastTable finsize $ for i. toJSON $ for k.
                    ("field" <> (show $ ordinal k), toJSON df.i.k)
     jdata = ("data", toJSON [("values", jdf)])
     jencodings = toJSON $ for i.
@@ -144,22 +152,28 @@ def chart [ToJSON v] (x: DataFrame (Fin key) (Fin n) v)
               ])
                                <> encoptions))
     jencode = ("encoding", jencodings)
-    toJSON [jdata, jmark, jencode]
+    toJSON ((AsList _ [jdata, jmark, jencode]) <> optsList opts)
     
 
-
 def showVega (x: Value) : String =
     "<iframe style=\"border:0\" height=\"300px\" width=\"700px\" srcdoc='<html>  <head><script src=\"https://cdn.jsdelivr.net/npm/vega@5.17.0\"></script>  <script src=\"https://cdn.jsdelivr.net/npm/vega-lite@4.17.0\"></script>  <script src=\"https://cdn.jsdelivr.net/npm/vega-embed@6.12.2\"></script> </head> <body> <div id=\"vis\"></div><script>vegaEmbed(\"#vis\"," <> (show x) <> ");</script></body></html>'</iframe>"
 
-c = chart bar (mark "bar") [enc X 0 Nominal,
-                            enc Y 1 Quantitative] 
+' ## Example: Bar Chart
 
-show c
+a_data = ["A", "B", "C", "D", "E", "F", "G", "H", "I"]
+b_data = [28, 55, 43, 91, 81, 53, 19, 87, 52]
+
+df0 = AsDataFrame  (for i. [toJSON a_data.i, toJSON b_data.i]) (["a", "b"])
+
+c = (chart df0 (mark "bar")
+     [enc X 0 Nominal,
+      enc Y 1 Quantitative]
+      (toList [("title", "Bar Graph")]))
 
 :html showVega $ c
 
 
-' ## More Examples
+' ## Example: Scatter
 
 data Class =
      A
@@ -167,7 +181,7 @@ data Class =
      C
 
 instance Show Class
-         show = \x . case x of
+    show = \x . case x of
                A -> "Apples"
                B -> "Bananas"
                C -> "Cucumbers"
@@ -175,18 +189,70 @@ instance Show Class
 keys : (Fin 5) => Key = splitKey $ newKey 1
 x1 : (Fin 100) => Float = arb $ keys.(0 @ _)
 x2 : (Fin 100) => Float = arb $ keys.(1 @ _)
+weight : (Fin 100) => Float = arb $ keys.(2 @ _)
 label : (Fin 100) => Class =
-      x = arb $ keys.(2 @ _)
+      x = arb $ keys.(3 @ _)
       for i. [A, B, C] (x.i)
 
 
 df = (AsDataFrame
-        (for i. [toJSON $ x1.i, toJSON $ x2.i, toJSON $ show label.i])
-        (["X1", "X2", "Label"]))
+        (for i. [toJSON $ x1.i,
+                 toJSON $ x2.i,
+                 toJSON $ weight.i,
+                 toJSON $ show label.i])
+        (["X1", "X2", "Weight", "Label"]))
+
+
+:html showVega (chart df (mark "point")
+      [enc X 0 Quantitative,
+       enc Y 1 Quantitative,
+       enc Size 2 Quantitative,
+       enc Color 3 Nominal,
+       enc Tooltip 3 Nominal]
+       (toList [("title", "Scatter")]))
+
+' ## Example: Faceted Area plot
+
+y1 :  (Fin 3) => (Fin 10) => Float = arb $ keys.(0 @ _)
+y = for i. cumSum . for j. select (y1.i.j > 0.0) (-1.0) 1.0 
+
+df2 = (AsDataFrame
+        (for (i,j). [toJSON $ y.i.j,
+                     toJSON $ ["Run 1", "Run 2", "Run 3"].i,
+                     toJSON $ ordinal j])
+        (["density", "Runs", "Round"]))
+
+
+
+:html showVega (chart df2 (mark "area")
+                [enc Y 0 Quantitative,
+                 enc Row 1 Nominal,
+                 enc X 2 Quantitative]
+                 (toList [("title", "Area"), ("height", "100")]))
+
+
+' ## Example: Heatmap
+
+
+words = ["the", "dog", "walked", "to", "the", "store"]
+
+z :  (Fin 6) => (Fin 6) => Float = arb $ keys.(0 @ _)
+
+df3 = (AsDataFrame
+        (for (i,j). [toJSON $ z.i.j,
+                     toJSON $ words.i <> " - " <> words.j,
+                     toJSON $ ordinal i,
+                     toJSON $ ordinal j
+                     ])
+        (["match", "words", "X", "Y"]))
+
 
 
-:html showVega $ chart df (mark "point") [enc X 0 Quantitative,
-                                          enc Y 1 Quantitative,
-                                          enc Color 2 Nominal] 
+:html showVega (chart df3 (mark "rect")
+       [enc Color 0 Quantitative,
+        enc X 2 Ordinal,
+        enc Y 3 Ordinal,
+        enc Tooltip 1 Nominal]
+       (toList [("title", "HeatMap"), ("height", "100")]))
 
 

From 2336b2032a8dda45066064282e55cb7917314f6b Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Sat, 23 Jan 2021 01:45:49 -0500
Subject: [PATCH 03/10] ex

---
 examples/json.dx | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/examples/json.dx b/examples/json.dx
index d7abc583e..72bb9a686 100644
--- a/examples/json.dx
+++ b/examples/json.dx
@@ -156,7 +156,7 @@ def chart [ToJSON v] (x: DataFrame (Fin key) n v)
     
 
 def showVega (x: Value) : String =
-    "<iframe style=\"border:0\" height=\"300px\" width=\"700px\" srcdoc='<html>  <head><script src=\"https://cdn.jsdelivr.net/npm/vega@5.17.0\"></script>  <script src=\"https://cdn.jsdelivr.net/npm/vega-lite@4.17.0\"></script>  <script src=\"https://cdn.jsdelivr.net/npm/vega-embed@6.12.2\"></script> </head> <body> <div id=\"vis\"></div><script>vegaEmbed(\"#vis\"," <> (show x) <> ");</script></body></html>'</iframe>"
+    "<iframe style=\"border:0\" height=\"300px\" width=\"700px\" srcdoc='<html>  <head><script src=\"https://cdn.jsdelivr.net/npm/vega@5.17.0\"></script>  <script src=\"https://cdn.jsdelivr.net/npm/vega-lite@4.17.0\"></script>  <script src=\"https://cdn.jsdelivr.net/npm/vega-embed@6.12.2\"></script> </head> <body> <div id=\"vis\"></div><script>vegaEmbed(\"#vis\"," <> (show x) <> ");</script></body></html>'></iframe>"
 
 ' ## Example: Bar Chart
 
@@ -228,7 +228,7 @@ df2 = (AsDataFrame
                 [enc Y 0 Quantitative,
                  enc Row 1 Nominal,
                  enc X 2 Quantitative]
-                 (toList [("title", "Area"), ("height", "100")]))
+                 (toList [("title", "Area"), ("height", "50")]))
 
 
 ' ## Example: Heatmap
@@ -253,6 +253,6 @@ df3 = (AsDataFrame
         enc X 2 Ordinal,
         enc Y 3 Ordinal,
         enc Tooltip 1 Nominal]
-       (toList [("title", "HeatMap"), ("height", "100")]))
+       (toList [("title", "HeatMap"), ("height", "200")]))
 
 

From e84ce08c79d3962efe1eedee7049dfced946ca15 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Mon, 25 Jan 2021 14:09:08 -0500
Subject: [PATCH 04/10] update json demo

---
 examples/json.dx  | 294 +++++++++++++++++++++++++++++++---------------
 static/index.html |   6 +-
 2 files changed, 205 insertions(+), 95 deletions(-)

diff --git a/examples/json.dx b/examples/json.dx
index 72bb9a686..1079a9425 100644
--- a/examples/json.dx
+++ b/examples/json.dx
@@ -1,19 +1,26 @@
 
 
 ' # Declarative Graphing
-
+  This example shows how to use Dex to generate interactive
+  graphs using a declarative graph library known as Vega-Lite.
+  To do this we will first implement a small JSON serialization library
+  and then a Dex interface to produce graph outputs.
 
 ' ## JSON Implementation
 
-def join (extra: List a) (lists:n=>(List a)) : List a =
+def join (joiner: List a) (lists:n=>(List a)) : List a =
+    -- Join together lists with an intermediary joiner
     concat $ for i.
         case ordinal i == (size n - 1) of
              True -> lists.i
-             False -> lists.i <> extra
+             False -> lists.i <> joiner
 
+' A serialized JSON Value
 
-data JValue = AsJValue String
 -- TODO - once Dex supports recursive ADT JValue becomes Value.
+data JValue = AsJValue String
+
+' Simple JSON Data Type
 
 data Value = 
      AsObject (List (String & JValue))
@@ -21,18 +28,17 @@ data Value =
      AsString String
      AsFloat Float
      AsInt Int
-
+     AsNone
+     
 interface ToJSON a
   toJSON : a -> Value
 
+instance Show JValue
+  show = \ (AsJValue a). a
 
--- These three are private methods. Users should use type classes.
-def escape (x:JValue) : String =
-    (AsJValue y) = x
-    y
+' Serialization Methods
 
-
-def collapse (x:Value) : JValue =
+def toJValue (x:Value) : JValue =
     AsJValue $ case x of
          AsString y ->  "\"" <> y <> "\""
          AsFloat y -> show y
@@ -40,14 +46,17 @@ def collapse (x:Value) : JValue =
          AsObject (AsList _ y) ->
               ("{" <> (join ", " $ for i.
                  (k, v) = y.i 
-                 "\"" <> k <> "\"" <> ":" <> (escape v)) <> "}")
-         AsArray (AsList _ y) -> ("[" <> (join ", " $ for i. escape y.i) <> "]")
+                 "\"" <> k <> "\"" <> ":" <> (show v)) <> "}")
+         AsArray (AsList _ y) -> ("[" <> (join ", " $ for i. show y.i) <> "]")
+         AsNone -> ""
 
-def hide [ToJSON a] (x:a) : JValue =
-    collapse $ toJSON x
+def serialize [ToJSON a] (x:a) : JValue =
+    toJValue $ toJSON x
 
 instance Show Value 
-  show = \x. escape $ collapse x
+  show = \x. show $ toJValue x
+
+' Type classes for JSON conversion
 
 instance ToJSON String
   toJSON = AsString
@@ -62,21 +71,39 @@ instance ToJSON Value
   toJSON = id
   
 instance [ToJSON v] ToJSON ((Fin n) => v)
-  toJSON = \x . AsArray $ AsList _ $ for i. hide x.i
+  toJSON = \x . AsArray $ AsList _ $ for i. serialize x.i
+
+instance [ToJSON v] ToJSON (List v)
+  toJSON = \(AsList _ x) . toJSON x
 
 instance [ToJSON v] ToJSON ((Fin n) => (String & v))
-  toJSON = \x . AsObject $ AsList _ $ for i. (fst x.i, hide $ snd x.i)
+  toJSON = \x . AsObject $ AsList _ $ for i. (fst x.i, serialize $ snd x.i)
 
 instance [ToJSON v] ToJSON (List (String & v))
   toJSON = \(AsList _ x) . toJSON x
 
 
-' ## Graph Grammars (Vega-Lite Spec)
+' ## Declarative Graph Grammars
+Graph grammars are a style of graphing that aims to separate the data representation
+from the graph layout. The main idea is to represent the underlying data as a flat
+sequence of aligned rows (colloquially a `dataframe`) and separately describe the graph
+layout based on a grammar. 
+
+' Here we implement a subset of the Vega-Lite (https://vega.github.io/vega-lite/) specification for
+  graphing. Vega-Lite lets you make a large set of charts using a very small grammar. 
+  
 
-Options = List (String & String)
+' Our Dataframe will be Table that associates meta data with columns. 
+
+data DataFrame row col value meta =
+     AsDataFrame  (col => meta) (row => col => value) 
+
+
+' We will have two pieces of metadata. A header string and an encoding type that
+  describes the role of the column.
+
+Header = String
 
-data Mark =
-     AsMark String Options
 
 data EncodingType =
      Quantitative
@@ -84,12 +111,45 @@ data EncodingType =
      Ordinal
 
 instance Show EncodingType
+   show = (\ x.
+       case x of
+         Quantitative -> "quantitative"
+         Nominal -> "nominal"
+         Ordinal -> "ordinal")
+
+
+' The two main aspects of Vega-Lite are the Mark and the Channel.
+  The mark tells it what kind of graph to draw, and the channels
+  allow us to assign different columns to different roles.
+  We implement these as simple data types, ideally these would be
+  derived from the spec.
+
+
+data Mark =
+     Area
+     Bar
+     Circle
+     Line
+     Point
+     Rect
+     Rule
+     Square
+     Text
+     Tick
+     
+instance Show Mark
          show = (\ x.
               case x of
-                   Quantitative -> "quantitative"
-                   Nominal -> "nominal"
-                   Ordinal -> "ordinal")
-                   
+                   Area -> "area"
+                   Bar -> "bar"
+                   Circle -> "circle"
+                   Line -> "line"
+                   Point -> "point"
+                   Rect -> "rect"
+                   Rule-> "rule"
+                   Square -> "square"
+                   Tick -> "tick")
+
 data Channel =
      Y
      X
@@ -112,69 +172,101 @@ instance Show Channel
                    Row -> "row"
                    Col -> "col")
 
-data Encoding key =
-     AsEncoding Channel key EncodingType Options
-
-def enc (c:Channel) (k:Int) (et: EncodingType) : Encoding key =
-    AsEncoding c (k@_) et mempty
+' Most things in VL can take in extra visual options.
+  To avoid specifying these, we will take in as
+  JSON.
 
-def mark (m:String) : Mark =
-    AsMark m mempty
+data Opts a =
+     WithOpts a Value
 
-def optsList (x:Options) : List (String & Value) =
-    (AsList _  tab) = x
-    AsList _ $ for i. (fst tab.i, toJSON $ snd tab.i)
-
-
-data DataFrame key n value =
-     AsDataFrame (n => key => value) (key => String)
+def pure (x:a) : Opts a =
+    WithOpts x AsNone
+    
+def pureLs (x:a) : List (Opts a) =
+   AsList 1 [WithOpts x AsNone]
+
+def mergeOpts [ToJSON a, ToJSON b] (x : a) (y : b) : Value =
+     case toJSON x of 
+         (AsObject x') -> case toJSON y of
+                  (AsObject y') -> AsObject $ x' <> y'
+                  (AsNone) -> AsObject x'
+         (AsNone) -> toJSON y
+ 
+def VLDataFrame (row:Type) (col:Type) (value:Type): Type =
+    DataFrame row col value (Header & EncodingType) 
+
+
+def chart [ToJSON v, ToJSON o] (x: VLDataFrame n (Fin key) v)
+                     (mark: Opts Mark)
+                     (encs : (Fin key) => List (Opts Channel))
+                     (opts : o)
+             : Value =
 
+    -- Make the mark
+    (WithOpts mtype options) = mark
+    jmark = ("mark", mergeOpts options [("type", show mtype)])
 
-def chart [ToJSON v] (x: DataFrame (Fin key) n v)
-                     (mark: Mark)
-                     (encs : (Fin m) => Encoding (Fin key))
-                     (opts : Options)
-             : Value =
-    
-    (AsMark mtype options) = mark
-    jmark = ("mark", toJSON ((AsList _ [("type", mtype)]) <> options))
-    (AsDataFrame df names) = x
-    finsize = (Fin $ size n)
-    jdf = toJSON $ unsafeCastTable finsize $ for i. toJSON $ for k.
-                   ("field" <> (show $ ordinal k), toJSON df.i.k)
+    -- Make the data
+    (AsDataFrame meta df) = x
+    finsize = Fin $ size n
+    jdf = toJSON $ castTable finsize $ for i. toJSON $ for k.
+                   ("field" <> (show $ ordinal k),
+                   toJSON df.i.k)
     jdata = ("data", toJSON [("values", jdf)])
-    jencodings = toJSON $ for i.
-        (AsEncoding channel key type encoptions) = encs.i
-        (show channel, toJSON ((AsList _ [
-              ("field", "field" <> (show $ ordinal key)),
+
+    -- Make the encodings
+    jencodings = toJSON $ concat $ for i.
+        (AsList v encopts) = encs.i
+        AsList _ $ for c : (Fin v). 
+           (WithOpts channel encoptions) = encopts.c
+           (title, type):(String & EncodingType) = meta.i
+           (show channel,
+            mergeOpts encoptions 
+            [
+              ("field", "field" <> (show $ ordinal i)),
               ("type", show type),
-              ("title", names.key)
-              ])
-                               <> encoptions))
+              ("title", title)
+              ])           
     jencode = ("encoding", jencodings)
-    toJSON ((AsList _ [jdata, jmark, jencode]) <> optsList opts)
+    mergeOpts opts [jdata, jmark, jencode]
     
 
 def showVega (x: Value) : String =
-    "<iframe style=\"border:0\" height=\"300px\" width=\"700px\" srcdoc='<html>  <head><script src=\"https://cdn.jsdelivr.net/npm/vega@5.17.0\"></script>  <script src=\"https://cdn.jsdelivr.net/npm/vega-lite@4.17.0\"></script>  <script src=\"https://cdn.jsdelivr.net/npm/vega-embed@6.12.2\"></script> </head> <body> <div id=\"vis\"></div><script>vegaEmbed(\"#vis\"," <> (show x) <> ");</script></body></html>'></iframe>"
+    "<iframe width=\"100%\" frameborder=\"0\" scrolling=\"no\" onload=\"resizeIframe(this)\" srcdoc='<html> 
+    <head><script src=\"https://cdn.jsdelivr.net/npm/vega@5.17.0\"></script>  
+          <script src=\"https://cdn.jsdelivr.net/npm/vega-lite@4.17.0\"></script>  
+          <script src=\"https://cdn.jsdelivr.net/npm/vega-embed@6.12.2\"></script> 
+    </head> 
+    <body> 
+           <div id=\"vis\"></div>
+           <script>vegaEmbed(\"#vis\"," <> (show x) <> ");</script>
+    </body>
+    </html>'>
+    </iframe>"
 
 ' ## Example: Bar Chart
 
 a_data = ["A", "B", "C", "D", "E", "F", "G", "H", "I"]
 b_data = [28, 55, 43, 91, 81, 53, 19, 87, 52]
 
-df0 = AsDataFrame  (for i. [toJSON a_data.i, toJSON b_data.i]) (["a", "b"])
+df0 = (AsDataFrame [("a", Nominal), ("b", Quantitative)]
+                   (for i. [toJSON a_data.i, toJSON b_data.i]))
+
 
-c = (chart df0 (mark "bar")
-     [enc X 0 Nominal,
-      enc Y 1 Quantitative]
-      (toList [("title", "Bar Graph")]))
+c = (chart df0 (pure Bar)
+     [pureLs X, pureLs Y]
+     [("title", "Bar Graph")])
 
 :html showVega $ c
 
 
 ' ## Example: Scatter
 
+' This example constructs a scatter plot with several different variables. 
+
+
+' First we will construct a Nominal variable for a class.
+
 data Class =
      A
      B
@@ -186,6 +278,8 @@ instance Show Class
                B -> "Bananas"
                C -> "Cucumbers"
 
+' Then we will generate some random data. 
+
 keys : (Fin 5) => Key = splitKey $ newKey 1
 x1 : (Fin 100) => Float = arb $ keys.(0 @ _)
 x2 : (Fin 100) => Float = arb $ keys.(1 @ _)
@@ -194,65 +288,77 @@ label : (Fin 100) => Class =
       x = arb $ keys.(3 @ _)
       for i. [A, B, C] (x.i)
 
+' The data frame has a mapping between the variable names and their encoding type.
 
 df = (AsDataFrame
-        (for i. [toJSON $ x1.i,
+        [("X1", Quantitative), ("X2", Quantitative), ("Weight", Quantitative), ("Label", Nominal)]
+         (for i. [toJSON $ x1.i,
                  toJSON $ x2.i,
                  toJSON $ weight.i,
-                 toJSON $ show label.i])
-        (["X1", "X2", "Weight", "Label"]))
+                 toJSON $ show label.i]))
+
 
+' We use a different mark `Bar` and pass in multiple Channels for some variables.
 
-:html showVega (chart df (mark "point")
-      [enc X 0 Quantitative,
-       enc Y 1 Quantitative,
-       enc Size 2 Quantitative,
-       enc Color 3 Nominal,
-       enc Tooltip 3 Nominal]
-       (toList [("title", "Scatter")]))
+:html showVega (chart df (pure Point)
+         [pureLs X, pureLs Y, pureLs Size,
+          AsList _ [pure Color, pure Tooltip]]
+          [("title", "Scatter")])
 
 ' ## Example: Faceted Area plot
 
+' This example show three different random walks. In particular in demonstrates how
+  VL can auto-facet the chart based on Nominal variables.
+
 y1 :  (Fin 3) => (Fin 10) => Float = arb $ keys.(0 @ _)
 y = for i. cumSum . for j. select (y1.i.j > 0.0) (-1.0) 1.0 
 
 df2 = (AsDataFrame
+    [("density", Quantitative), ("Runs", Nominal), ("Round", Ordinal)]
         (for (i,j). [toJSON $ y.i.j,
                      toJSON $ ["Run 1", "Run 2", "Run 3"].i,
-                     toJSON $ ordinal j])
-        (["density", "Runs", "Round"]))
-
-
+                     toJSON $ ordinal j]))
+     
 
-:html showVega (chart df2 (mark "area")
-                [enc Y 0 Quantitative,
-                 enc Row 1 Nominal,
-                 enc X 2 Quantitative]
-                 (toList [("title", "Area"), ("height", "50")]))
+:html showVega (chart df2 (pure Area)
+                [pureLs Y,
+                 pureLs Row,
+                 pureLs X]
+                 [("title", "Area"), ("height", "75")])
 
 
 ' ## Example: Heatmap
 
-
 words = ["the", "dog", "walked", "to", "the", "store"]
 
 z :  (Fin 6) => (Fin 6) => Float = arb $ keys.(0 @ _)
 
 df3 = (AsDataFrame
+        [("match", Quantitative) , ("words", Nominal), ("row", Ordinal), ("col", Ordinal)]
         (for (i,j). [toJSON $ z.i.j,
                      toJSON $ words.i <> " - " <> words.j,
                      toJSON $ ordinal i,
                      toJSON $ ordinal j
-                     ])
-        (["match", "words", "X", "Y"]))
+                     ]))
 
+' Default heat map
 
+:html showVega (chart df3 (pure Rect)
+       [pureLs Color,
+        pureLs Tooltip,
+        pureLs X,
+        pureLs Y] AsNone)
 
-:html showVega (chart df3 (mark "rect")
-       [enc Color 0 Quantitative,
-        enc X 2 Ordinal,
-        enc Y 3 Ordinal,
-        enc Tooltip 1 Nominal]
-       (toList [("title", "HeatMap"), ("height", "200")]))
+' Customization through JSON options.
 
 
+:html showVega (chart df3 (pure Rect)
+       [pureLs Color,
+        pureLs Tooltip,
+        pureLs X,
+        pureLs Y] $
+       mergeOpts [("title",  "HeatMap"), ("height",  "200"), ("width",  "200")]
+         [("config", toJSON [
+          ("axis", [("grid", toJSON  1), ("tickBand", toJSON  "extent")])
+          ])]
+       )
\ No newline at end of file
diff --git a/static/index.html b/static/index.html
index 93d8893db..05a282ede 100644
--- a/static/index.html
+++ b/static/index.html
@@ -11,7 +11,11 @@
   <script defer src="https://cdn.jsdelivr.net/npm/katex@0.12.0/dist/katex.min.js" integrity="sha384-g7c+Jr9ZivxKLnZTDUhnkOnsh30B4H0rpLUpJ4jAIKs4fnJI+sEnkvrMWph2EDg4" crossorigin="anonymous"></script>
   <script defer src="https://cdn.jsdelivr.net/npm/katex@0.12.0/dist/contrib/auto-render.min.js" integrity="sha384-mll67QQFJfxn0IYznZYonOWZ644AWYC+Pt2cHqMaRhXVrursRwvLnLaebdGIlYNa" crossorigin="anonymous"></script>
 
-
+<script>
+  function resizeIframe(obj) {
+    obj.style.height = obj.contentWindow.document.documentElement.scrollHeight + 'px';
+  }
+</script>
 </head>
 
 <body>

From 95cf9a58c8702065abc0a87a352f967f27dd56d4 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Tue, 26 Jan 2021 12:26:34 -0500
Subject: [PATCH 05/10] remove the dataframe requirement

---
 examples/{json.dx => vega.dx} | 244 +++++++++++++++++-----------------
 makefile                      |   2 +-
 static/dynamic.js             |   6 +
 3 files changed, 129 insertions(+), 123 deletions(-)
 rename examples/{json.dx => vega.dx} (56%)

diff --git a/examples/json.dx b/examples/vega.dx
similarity index 56%
rename from examples/json.dx
rename to examples/vega.dx
index 1079a9425..783b84cbc 100644
--- a/examples/json.dx
+++ b/examples/vega.dx
@@ -70,19 +70,31 @@ instance ToJSON Float
 instance ToJSON Value
   toJSON = id
   
-instance [ToJSON v] ToJSON ((Fin n) => v)
-  toJSON = \x . AsArray $ AsList _ $ for i. serialize x.i
+instance [ToJSON v] ToJSON (n => v)
+  toJSON = \x .
+    sizen = (size n)
+    tab = castTable (Fin sizen) $ for i. serialize x.i
+    AsArray $ AsList sizen tab
 
 instance [ToJSON v] ToJSON (List v)
   toJSON = \(AsList _ x) . toJSON x
 
-instance [ToJSON v] ToJSON ((Fin n) => (String & v))
-  toJSON = \x . AsObject $ AsList _ $ for i. (fst x.i, serialize $ snd x.i)
+instance [ToJSON v] ToJSON (n => (String & v))
+
+  toJSON = \x .
+     sizen = (size n)
+     tab = castTable (Fin sizen) $ for i. (fst x.i, serialize $ snd x.i)
+     AsObject $ AsList _ tab
 
 instance [ToJSON v] ToJSON (List (String & v))
   toJSON = \(AsList _ x) . toJSON x
 
 
+def wrapCol [ToJSON d]  (iso: Iso a ((n=>d) & c)) (x:a) : n=> Value =
+    -- Helper function. Returns JSON of a column of a record
+    y = getAt iso x
+    for i. toJSON y.i
+
 ' ## Declarative Graph Grammars
 Graph grammars are a style of graphing that aims to separate the data representation
 from the graph layout. The main idea is to represent the underlying data as a flat
@@ -93,14 +105,8 @@ layout based on a grammar.
   graphing. Vega-Lite lets you make a large set of charts using a very small grammar. 
   
 
-' Our Dataframe will be Table that associates meta data with columns. 
-
-data DataFrame row col value meta =
-     AsDataFrame  (col => meta) (row => col => value) 
-
-
-' We will have two pieces of metadata. A header string and an encoding type that
-  describes the role of the column.
+' We will have several pieces of metadata. A header string, encoding type, and the
+  channels that the data is displayed with.
 
 Header = String
 
@@ -118,7 +124,30 @@ instance Show EncodingType
          Ordinal -> "ordinal")
 
 
-' The two main aspects of Vega-Lite are the Mark and the Channel.
+data Channel =
+     Y
+     X
+     Color
+     Tooltip
+     HREF
+     Row
+     Col
+     Size
+     
+instance Show Channel
+         show = (\ x.
+              case x of
+                   Y -> "y"
+                   X -> "x"
+                   Color -> "color"
+                   Tooltip -> "tooltip"
+                   HREF -> "href"
+                   Size -> "size"
+                   Row -> "row"
+                   Col -> "col")
+
+
+' The final aspect of Vega-Lite is the Mark.
   The mark tells it what kind of graph to draw, and the channels
   allow us to assign different columns to different roles.
   We implement these as simple data types, ideally these would be
@@ -150,28 +179,6 @@ instance Show Mark
                    Square -> "square"
                    Tick -> "tick")
 
-data Channel =
-     Y
-     X
-     Color
-     Tooltip
-     HREF
-     Row
-     Col
-     Size
-     
-instance Show Channel
-         show = (\ x.
-              case x of
-                   Y -> "y"
-                   X -> "x"
-                   Color -> "color"
-                   Tooltip -> "tooltip"
-                   HREF -> "href"
-                   Size -> "size"
-                   Row -> "row"
-                   Col -> "col")
-
 ' Most things in VL can take in extra visual options.
   To avoid specifying these, we will take in as
   JSON.
@@ -191,48 +198,47 @@ def mergeOpts [ToJSON a, ToJSON b] (x : a) (y : b) : Value =
                   (AsObject y') -> AsObject $ x' <> y'
                   (AsNone) -> AsObject x'
          (AsNone) -> toJSON y
- 
-def VLDataFrame (row:Type) (col:Type) (value:Type): Type =
-    DataFrame row col value (Header & EncodingType) 
 
 
-def chart [ToJSON v, ToJSON o] (x: VLDataFrame n (Fin key) v)
-                     (mark: Opts Mark)
-                     (encs : (Fin key) => List (Opts Channel))
-                     (opts : o)
-             : Value =
 
+data VLChart row col v =
+     AsVLDescriptor (Opts Mark) v (col => ({title: Header &
+                              encType: EncodingType &
+                              encodings: List (Opts Channel) &
+                              rows: row => Value
+                              })) 
+
+instance [ToJSON v] ToJSON (VLChart r c v)
+   toJSON = \ x.
+    (AsVLDescriptor mark opts df) = x
     -- Make the mark
     (WithOpts mtype options) = mark
     jmark = ("mark", mergeOpts options [("type", show mtype)])
 
     -- Make the data
-    (AsDataFrame meta df) = x
-    finsize = Fin $ size n
-    jdf = toJSON $ castTable finsize $ for i. toJSON $ for k.
-                   ("field" <> (show $ ordinal k),
-                   toJSON df.i.k)
+    jdf = toJSON $ for row : r. toJSON $ for col : c.
+                   ("col" <> (show $ ordinal col),
+                    toJSON (getAt #rows df.col).row)
     jdata = ("data", toJSON [("values", jdf)])
 
     -- Make the encodings
-    jencodings = toJSON $ concat $ for i.
-        (AsList v encopts) = encs.i
-        AsList _ $ for c : (Fin v). 
-           (WithOpts channel encoptions) = encopts.c
-           (title, type):(String & EncodingType) = meta.i
+    jencodings = toJSON $ concat $ for col : c.
+        (AsList v encopts) = getAt #encodings df.col
+        AsList v $ for f. 
+           (WithOpts channel encoptions) = encopts.f
            (show channel,
             mergeOpts encoptions 
             [
-              ("field", "field" <> (show $ ordinal i)),
-              ("type", show type),
-              ("title", title)
-              ])           
+              ("field", "col" <> (show $ ordinal col)),
+              ("type",  show $ getAt #encType df.col),
+              ("title", getAt #title df.col)
+              ])
     jencode = ("encoding", jencodings)
     mergeOpts opts [jdata, jmark, jencode]
     
 
 def showVega (x: Value) : String =
-    "<iframe width=\"100%\" frameborder=\"0\" scrolling=\"no\" onload=\"resizeIframe(this)\" srcdoc='<html> 
+    "<iframe width=\"100%\" frameborder=\"0\" scrolling=\"no\" onload=\"resize_iframe(this)\" srcdoc='<html> 
     <head><script src=\"https://cdn.jsdelivr.net/npm/vega@5.17.0\"></script>  
           <script src=\"https://cdn.jsdelivr.net/npm/vega-lite@4.17.0\"></script>  
           <script src=\"https://cdn.jsdelivr.net/npm/vega-embed@6.12.2\"></script> 
@@ -246,18 +252,20 @@ def showVega (x: Value) : String =
 
 ' ## Example: Bar Chart
 
-a_data = ["A", "B", "C", "D", "E", "F", "G", "H", "I"]
-b_data = [28, 55, 43, 91, 81, 53, 19, 87, 52]
+' Start with a well type and useful Dex record
 
-df0 = (AsDataFrame [("a", Nominal), ("b", Quantitative)]
-                   (for i. [toJSON a_data.i, toJSON b_data.i]))
+df1 = {a = ["A", "B", "C", "D", "E", "F", "G", "H", "I"],
+       b = [28, 55, 43, 91, 81, 53, 19, 87, 52]}
 
 
-c = (chart df0 (pure Bar)
-     [pureLs X, pureLs Y]
-     [("title", "Bar Graph")])
+chart1 = (AsVLDescriptor (pure Bar) [("title", "Bar Graph")]
+    [{title="a axis", encodings=pureLs X,
+      encType=Nominal, rows=wrapCol #a df1},
+     {title="b axis", encodings=pureLs Y,
+     encType=Quantitative, rows=wrapCol #b df1}]
+)
 
-:html showVega $ c
+:html showVega $ toJSON chart1
 
 
 ' ## Example: Scatter
@@ -278,87 +286,79 @@ instance Show Class
                B -> "Bananas"
                C -> "Cucumbers"
 
+instance Arbitrary Class
+    arb = \key. [A, B, C].(arb key)
+
+instance ToJSON Class
+    toJSON = \x. AsString $ show x
+
 ' Then we will generate some random data. 
 
-keys : (Fin 5) => Key = splitKey $ newKey 1
-x1 : (Fin 100) => Float = arb $ keys.(0 @ _)
-x2 : (Fin 100) => Float = arb $ keys.(1 @ _)
-weight : (Fin 100) => Float = arb $ keys.(2 @ _)
-label : (Fin 100) => Class =
-      x = arb $ keys.(3 @ _)
-      for i. [A, B, C] (x.i)
+key : (Fin 5) => Key = splitKey $ newKey 1
 
-' The data frame has a mapping between the variable names and their encoding type.
+df2 : {x1: (Fin 100) => Float &
+       x2: (Fin 100) => Float &
+       weight: (Fin 100) => Float &
+       label : (Fin 100) => Class} =
+            [k1, k2, k3, k4] = splitKey $ newKey 1
+            {x1=arb k1,
+             x2=arb k2,
+             weight=arb k3,
+             label=arb k4}
 
-df = (AsDataFrame
-        [("X1", Quantitative), ("X2", Quantitative), ("Weight", Quantitative), ("Label", Nominal)]
-         (for i. [toJSON $ x1.i,
-                 toJSON $ x2.i,
-                 toJSON $ weight.i,
-                 toJSON $ show label.i]))
+' The descriptor has a mapping between the variable names and their encoding type.
 
+' We use a different mark `Point` and pass in multiple Channels for some variables.
 
-' We use a different mark `Bar` and pass in multiple Channels for some variables.
+chart2 = (AsVLDescriptor (pure Point) [("title", "Scatter")]
+            [{title="X1", encodings=pureLs X, encType=Quantitative, rows=wrapCol #x1 df2},
+             {title="X2", encodings=pureLs Y, encType=Quantitative, rows=wrapCol #x2 df2},
+             {title="Weight", encodings=pureLs Size, encType=Quantitative, rows=wrapCol #weight df2},
+             {title="Label", encodings=toList [pure Color, pure Tooltip], encType=Nominal, rows=wrapCol #label df2}])
+
+                 
+:html showVega $ toJSON chart2
 
-:html showVega (chart df (pure Point)
-         [pureLs X, pureLs Y, pureLs Size,
-          AsList _ [pure Color, pure Tooltip]]
-          [("title", "Scatter")])
 
 ' ## Example: Faceted Area plot
 
 ' This example show three different random walks. In particular in demonstrates how
   VL can auto-facet the chart based on Nominal variables.
 
-y1 :  (Fin 3) => (Fin 10) => Float = arb $ keys.(0 @ _)
-y = for i. cumSum . for j. select (y1.i.j > 0.0) (-1.0) 1.0 
 
-df2 = (AsDataFrame
-    [("density", Quantitative), ("Runs", Nominal), ("Round", Ordinal)]
-        (for (i,j). [toJSON $ y.i.j,
-                     toJSON $ ["Run 1", "Run 2", "Run 3"].i,
-                     toJSON $ ordinal j]))
-     
+y1 :  (Fin 3) => (Fin 10) => Float = arb $ newKey 0
+df3 = for i. cumSum . for j. select (y1.i.j > 0.0) (-1.0) 1.0 
 
-:html showVega (chart df2 (pure Area)
-                [pureLs Y,
-                 pureLs Row,
-                 pureLs X]
-                 [("title", "Area"), ("height", "75")])
+:t df3
+
+chart3 = (AsVLDescriptor (pure Area) [("title", "Area"), ("height", "75")]
+            [{title="density", encodings=pureLs Y, encType=Quantitative, rows=for (i,j). toJSON df3.i.j},
+             {title="Runs", encodings=pureLs Row, encType=Nominal, rows= for (i,_). toJSON $ ["Run 1", "Run 2", "Run 3"].i},
+             {title="Round", encodings=pureLs X, encType=Ordinal, rows=for (_,j). toJSON $ ordinal j}]
+)
+
+:html showVega $ toJSON chart3
 
 
 ' ## Example: Heatmap
 
 words = ["the", "dog", "walked", "to", "the", "store"]
+z :  (Fin 6) => (Fin 6) => Float = arb $ newKey 0
 
-z :  (Fin 6) => (Fin 6) => Float = arb $ keys.(0 @ _)
-
-df3 = (AsDataFrame
-        [("match", Quantitative) , ("words", Nominal), ("row", Ordinal), ("col", Ordinal)]
-        (for (i,j). [toJSON $ z.i.j,
-                     toJSON $ words.i <> " - " <> words.j,
-                     toJSON $ ordinal i,
-                     toJSON $ ordinal j
-                     ]))
+def showChart4 [ToJSON o] (opts:o) : Value  = toJSON (AsVLDescriptor (pure Rect) opts
+            [{title="match", encodings=pureLs Color, encType=Quantitative, rows=for (i,j). toJSON z.i.j},
+            {title="words", encodings=pureLs Tooltip, encType=Nominal, rows=for (i,j). toJSON (words.i <> " - " <> words.j)},
+            {title="row", encodings=pureLs X, encType=Ordinal, rows=for (i,_). toJSON (ordinal i)},
+            {title="col", encodings=pureLs Y, encType=Ordinal, rows=for (_,j). toJSON (ordinal j)}]  
+        )
 
 ' Default heat map
 
-:html showVega (chart df3 (pure Rect)
-       [pureLs Color,
-        pureLs Tooltip,
-        pureLs X,
-        pureLs Y] AsNone)
+:html showVega $ showChart4 AsNone
 
 ' Customization through JSON options.
 
 
-:html showVega (chart df3 (pure Rect)
-       [pureLs Color,
-        pureLs Tooltip,
-        pureLs X,
-        pureLs Y] $
-       mergeOpts [("title",  "HeatMap"), ("height",  "200"), ("width",  "200")]
-         [("config", toJSON [
-          ("axis", [("grid", toJSON  1), ("tickBand", toJSON  "extent")])
-          ])]
-       )
\ No newline at end of file
+:html showVega $ showChart4 $ mergeOpts [("title",  "HeatMap"), ("height", "200"), ("width",  "200")] [("config", toJSON [
+          ("axis", [("grid", "1"), ("tickBand",  "extent")])
+          ])]<
\ No newline at end of file
diff --git a/makefile b/makefile
index 13157df5e..c0714dfff 100644
--- a/makefile
+++ b/makefile
@@ -89,7 +89,7 @@ example-names = mandelbrot pi sierpinski rejection-sampler \
                 regression brownian_motion particle-swarm-optimizer \
                 ode-integrator mcmc ctc raytrace particle-filter \
                 isomorphisms ode-integrator linear_algebra fluidsim \
-                sgd chol
+                sgd chol vega
 
 test-names = uexpr-tests adt-tests type-tests eval-tests show-tests \
              shadow-tests monad-tests io-tests exception-tests \
diff --git a/static/dynamic.js b/static/dynamic.js
index 7aeeb9524..41d567b79 100644
--- a/static/dynamic.js
+++ b/static/dynamic.js
@@ -83,3 +83,9 @@ source.onmessage = function(event) {
         renderMathInElement(proseBlock, katexOptions)
     );
 };
+
+
+// Needed to resize dynamic iframe heights.
+function resize_iframe(obj) {
+    obj.style.height = obj.contentWindow.document.documentElement.scrollHeight + 'px';
+}

From 4bc91e38d1d7527f4d9098369064d7804f344b27 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Tue, 26 Jan 2021 12:30:13 -0500
Subject: [PATCH 06/10] remove js from static page

---
 examples/vega.dx  | 2 +-
 static/index.html | 6 ------
 2 files changed, 1 insertion(+), 7 deletions(-)

diff --git a/examples/vega.dx b/examples/vega.dx
index 783b84cbc..b03b9a35c 100644
--- a/examples/vega.dx
+++ b/examples/vega.dx
@@ -361,4 +361,4 @@ def showChart4 [ToJSON o] (opts:o) : Value  = toJSON (AsVLDescriptor (pure Rect)
 
 :html showVega $ showChart4 $ mergeOpts [("title",  "HeatMap"), ("height", "200"), ("width",  "200")] [("config", toJSON [
           ("axis", [("grid", "1"), ("tickBand",  "extent")])
-          ])]<
\ No newline at end of file
+          ])]
\ No newline at end of file
diff --git a/static/index.html b/static/index.html
index 05a282ede..d1774f2ec 100644
--- a/static/index.html
+++ b/static/index.html
@@ -10,12 +10,6 @@
   <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.12.0/dist/katex.min.css" integrity="sha384-AfEj0r4/OFrOo5t7NnNe46zW/tFgW6x/bCJG8FqQCEo3+Aro6EYUG4+cU+KJWu/X" crossorigin="anonymous">
   <script defer src="https://cdn.jsdelivr.net/npm/katex@0.12.0/dist/katex.min.js" integrity="sha384-g7c+Jr9ZivxKLnZTDUhnkOnsh30B4H0rpLUpJ4jAIKs4fnJI+sEnkvrMWph2EDg4" crossorigin="anonymous"></script>
   <script defer src="https://cdn.jsdelivr.net/npm/katex@0.12.0/dist/contrib/auto-render.min.js" integrity="sha384-mll67QQFJfxn0IYznZYonOWZ644AWYC+Pt2cHqMaRhXVrursRwvLnLaebdGIlYNa" crossorigin="anonymous"></script>
-
-<script>
-  function resizeIframe(obj) {
-    obj.style.height = obj.contentWindow.document.documentElement.scrollHeight + 'px';
-  }
-</script>
 </head>
 
 <body>

From fb7259617c9117e35e81933f457aa27c467bad4f Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Tue, 26 Jan 2021 12:35:58 -0500
Subject: [PATCH 07/10] change name of file

---
 examples/{vega.dx => vega-plotting.dx} | 0
 makefile                               | 2 +-
 2 files changed, 1 insertion(+), 1 deletion(-)
 rename examples/{vega.dx => vega-plotting.dx} (100%)

diff --git a/examples/vega.dx b/examples/vega-plotting.dx
similarity index 100%
rename from examples/vega.dx
rename to examples/vega-plotting.dx
diff --git a/makefile b/makefile
index c0714dfff..cdf5e2b78 100644
--- a/makefile
+++ b/makefile
@@ -89,7 +89,7 @@ example-names = mandelbrot pi sierpinski rejection-sampler \
                 regression brownian_motion particle-swarm-optimizer \
                 ode-integrator mcmc ctc raytrace particle-filter \
                 isomorphisms ode-integrator linear_algebra fluidsim \
-                sgd chol vega
+                sgd chol vega-plotting
 
 test-names = uexpr-tests adt-tests type-tests eval-tests show-tests \
              shadow-tests monad-tests io-tests exception-tests \

From b4a2a06050d7d7eb0c0e174a8f10353948554b8c Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Wed, 27 Jan 2021 08:39:48 -0500
Subject: [PATCH 08/10] move to rows

---
 examples/vega-plotting.dx | 29 +++++++++++++----------------
 1 file changed, 13 insertions(+), 16 deletions(-)

diff --git a/examples/vega-plotting.dx b/examples/vega-plotting.dx
index b03b9a35c..6e9a674ae 100644
--- a/examples/vega-plotting.dx
+++ b/examples/vega-plotting.dx
@@ -90,10 +90,9 @@ instance [ToJSON v] ToJSON (List (String & v))
   toJSON = \(AsList _ x) . toJSON x
 
 
-def wrapCol [ToJSON d]  (iso: Iso a ((n=>d) & c)) (x:a) : n=> Value =
+def wrapCol [ToJSON d]  (iso: Iso a (d & c)) (x:n=>a) : n=> Value =
     -- Helper function. Returns JSON of a column of a record
-    y = getAt iso x
-    for i. toJSON y.i
+    for i. toJSON $ getAt iso x.i
 
 ' ## Declarative Graph Grammars
 Graph grammars are a style of graphing that aims to separate the data representation
@@ -254,8 +253,8 @@ def showVega (x: Value) : String =
 
 ' Start with a well type and useful Dex record
 
-df1 = {a = ["A", "B", "C", "D", "E", "F", "G", "H", "I"],
-       b = [28, 55, 43, 91, 81, 53, 19, 87, 52]}
+df1 = for i. {a = ["A", "B", "C", "D", "E", "F", "G", "H", "I"].i,
+              b = [28, 55, 43, 91, 81, 53, 19, 87, 52].i}
 
 
 chart1 = (AsVLDescriptor (pure Bar) [("title", "Bar Graph")]
@@ -294,17 +293,15 @@ instance ToJSON Class
 
 ' Then we will generate some random data. 
 
-key : (Fin 5) => Key = splitKey $ newKey 1
-
-df2 : {x1: (Fin 100) => Float &
-       x2: (Fin 100) => Float &
-       weight: (Fin 100) => Float &
-       label : (Fin 100) => Class} =
-            [k1, k2, k3, k4] = splitKey $ newKey 1
-            {x1=arb k1,
-             x2=arb k2,
-             weight=arb k3,
-             label=arb k4}
+key : Key = newKey 1
+
+
+df2 :(Fin 100) => {x1:Float & x2:Float & weight:Float & label:Class}  =  for i: (Fin 100).
+              [k1, k2, k3, k4] = splitKey $ ixkey key i
+              {x1=(arb k1),
+               x2=arb k2,
+               weight=arb k3,
+               label=arb k4}
 
 ' The descriptor has a mapping between the variable names and their encoding type.
 

From de59579a3add95fd23a7aeda4fa1cfe43b66ea96 Mon Sep 17 00:00:00 2001
From: srush <srush.research@gmail.com>
Date: Wed, 27 Jan 2021 09:44:54 -0500
Subject: [PATCH 09/10] add last line because tests break

---
 examples/vega-plotting.dx | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/examples/vega-plotting.dx b/examples/vega-plotting.dx
index 6e9a674ae..a06402feb 100644
--- a/examples/vega-plotting.dx
+++ b/examples/vega-plotting.dx
@@ -265,6 +265,7 @@ chart1 = (AsVLDescriptor (pure Bar) [("title", "Bar Graph")]
 )
 
 :html showVega $ toJSON chart1
+> <html output>
 
 
 ' ## Example: Scatter
@@ -315,6 +316,7 @@ chart2 = (AsVLDescriptor (pure Point) [("title", "Scatter")]
 
                  
 :html showVega $ toJSON chart2
+> <html output>
 
 
 ' ## Example: Faceted Area plot
@@ -327,6 +329,7 @@ y1 :  (Fin 3) => (Fin 10) => Float = arb $ newKey 0
 df3 = for i. cumSum . for j. select (y1.i.j > 0.0) (-1.0) 1.0 
 
 :t df3
+> ((Fin 3) => (Fin 10) => Float32)
 
 chart3 = (AsVLDescriptor (pure Area) [("title", "Area"), ("height", "75")]
             [{title="density", encodings=pureLs Y, encType=Quantitative, rows=for (i,j). toJSON df3.i.j},
@@ -335,6 +338,7 @@ chart3 = (AsVLDescriptor (pure Area) [("title", "Area"), ("height", "75")]
 )
 
 :html showVega $ toJSON chart3
+> <html output>
 
 
 ' ## Example: Heatmap
@@ -352,10 +356,15 @@ def showChart4 [ToJSON o] (opts:o) : Value  = toJSON (AsVLDescriptor (pure Rect)
 ' Default heat map
 
 :html showVega $ showChart4 AsNone
+> <html output>
 
 ' Customization through JSON options.
 
 
 :html showVega $ showChart4 $ mergeOpts [("title",  "HeatMap"), ("height", "200"), ("width",  "200")] [("config", toJSON [
           ("axis", [("grid", "1"), ("tickBand",  "extent")])
-          ])]
\ No newline at end of file
+          ])]
+> <html output>
+
+
+' (end)
\ No newline at end of file

From 50693ae77729b4c732e137a7bd690e229c90e66c Mon Sep 17 00:00:00 2001
From: Adam Paszke <apaszke@google.com>
Date: Mon, 1 Feb 2021 16:20:41 +0000
Subject: [PATCH 10/10] Don't modify compiler JS sources

---
 examples/vega-plotting.dx | 64 ++++++++++++++++++++-------------------
 static/dynamic.js         |  6 ----
 2 files changed, 33 insertions(+), 37 deletions(-)

diff --git a/examples/vega-plotting.dx b/examples/vega-plotting.dx
index a06402feb..10a5d890d 100644
--- a/examples/vega-plotting.dx
+++ b/examples/vega-plotting.dx
@@ -22,14 +22,14 @@ data JValue = AsJValue String
 
 ' Simple JSON Data Type
 
-data Value = 
+data Value =
      AsObject (List (String & JValue))
      AsArray (List JValue)
      AsString String
      AsFloat Float
      AsInt Int
      AsNone
-     
+
 interface ToJSON a
   toJSON : a -> Value
 
@@ -45,7 +45,7 @@ def toJValue (x:Value) : JValue =
          AsInt y -> show y
          AsObject (AsList _ y) ->
               ("{" <> (join ", " $ for i.
-                 (k, v) = y.i 
+                 (k, v) = y.i
                  "\"" <> k <> "\"" <> ":" <> (show v)) <> "}")
          AsArray (AsList _ y) -> ("[" <> (join ", " $ for i. show y.i) <> "]")
          AsNone -> ""
@@ -53,23 +53,23 @@ def toJValue (x:Value) : JValue =
 def serialize [ToJSON a] (x:a) : JValue =
     toJValue $ toJSON x
 
-instance Show Value 
+instance Show Value
   show = \x. show $ toJValue x
 
 ' Type classes for JSON conversion
 
 instance ToJSON String
   toJSON = AsString
-  
+
 instance ToJSON Int
   toJSON = AsInt
-  
+
 instance ToJSON Float
   toJSON = AsFloat
-  
+
 instance ToJSON Value
   toJSON = id
-  
+
 instance [ToJSON v] ToJSON (n => v)
   toJSON = \x .
     sizen = (size n)
@@ -98,11 +98,11 @@ def wrapCol [ToJSON d]  (iso: Iso a (d & c)) (x:n=>a) : n=> Value =
 Graph grammars are a style of graphing that aims to separate the data representation
 from the graph layout. The main idea is to represent the underlying data as a flat
 sequence of aligned rows (colloquially a `dataframe`) and separately describe the graph
-layout based on a grammar. 
+layout based on a grammar.
 
 ' Here we implement a subset of the Vega-Lite (https://vega.github.io/vega-lite/) specification for
-  graphing. Vega-Lite lets you make a large set of charts using a very small grammar. 
-  
+  graphing. Vega-Lite lets you make a large set of charts using a very small grammar.
+
 
 ' We will have several pieces of metadata. A header string, encoding type, and the
   channels that the data is displayed with.
@@ -132,7 +132,7 @@ data Channel =
      Row
      Col
      Size
-     
+
 instance Show Channel
          show = (\ x.
               case x of
@@ -164,7 +164,7 @@ data Mark =
      Square
      Text
      Tick
-     
+
 instance Show Mark
          show = (\ x.
               case x of
@@ -187,12 +187,12 @@ data Opts a =
 
 def pure (x:a) : Opts a =
     WithOpts x AsNone
-    
+
 def pureLs (x:a) : List (Opts a) =
    AsList 1 [WithOpts x AsNone]
 
 def mergeOpts [ToJSON a, ToJSON b] (x : a) (y : b) : Value =
-     case toJSON x of 
+     case toJSON x of
          (AsObject x') -> case toJSON y of
                   (AsObject y') -> AsObject $ x' <> y'
                   (AsNone) -> AsObject x'
@@ -205,7 +205,7 @@ data VLChart row col v =
                               encType: EncodingType &
                               encodings: List (Opts Channel) &
                               rows: row => Value
-                              })) 
+                              }))
 
 instance [ToJSON v] ToJSON (VLChart r c v)
    toJSON = \ x.
@@ -223,10 +223,10 @@ instance [ToJSON v] ToJSON (VLChart r c v)
     -- Make the encodings
     jencodings = toJSON $ concat $ for col : c.
         (AsList v encopts) = getAt #encodings df.col
-        AsList v $ for f. 
+        AsList v $ for f.
            (WithOpts channel encoptions) = encopts.f
            (show channel,
-            mergeOpts encoptions 
+            mergeOpts encoptions
             [
               ("field", "col" <> (show $ ordinal col)),
               ("type",  show $ getAt #encType df.col),
@@ -234,15 +234,17 @@ instance [ToJSON v] ToJSON (VLChart r c v)
               ])
     jencode = ("encoding", jencodings)
     mergeOpts opts [jdata, jmark, jencode]
-    
+
 
 def showVega (x: Value) : String =
-    "<iframe width=\"100%\" frameborder=\"0\" scrolling=\"no\" onload=\"resize_iframe(this)\" srcdoc='<html> 
-    <head><script src=\"https://cdn.jsdelivr.net/npm/vega@5.17.0\"></script>  
-          <script src=\"https://cdn.jsdelivr.net/npm/vega-lite@4.17.0\"></script>  
-          <script src=\"https://cdn.jsdelivr.net/npm/vega-embed@6.12.2\"></script> 
-    </head> 
-    <body> 
+    "<iframe width=\"100%\" frameborder=\"0\" scrolling=\"no\"
+             onload=\"this.style.height=this.contentWindow.document.body.scrollHeight+'px'\";
+             srcdoc='<html>
+    <head><script src=\"https://cdn.jsdelivr.net/npm/vega@5.17.0\"></script>
+          <script src=\"https://cdn.jsdelivr.net/npm/vega-lite@4.17.0\"></script>
+          <script src=\"https://cdn.jsdelivr.net/npm/vega-embed@6.12.2\"></script>
+    </head>
+    <body>
            <div id=\"vis\"></div>
            <script>vegaEmbed(\"#vis\"," <> (show x) <> ");</script>
     </body>
@@ -270,7 +272,7 @@ chart1 = (AsVLDescriptor (pure Bar) [("title", "Bar Graph")]
 
 ' ## Example: Scatter
 
-' This example constructs a scatter plot with several different variables. 
+' This example constructs a scatter plot with several different variables.
 
 
 ' First we will construct a Nominal variable for a class.
@@ -292,7 +294,7 @@ instance Arbitrary Class
 instance ToJSON Class
     toJSON = \x. AsString $ show x
 
-' Then we will generate some random data. 
+' Then we will generate some random data.
 
 key : Key = newKey 1
 
@@ -314,7 +316,7 @@ chart2 = (AsVLDescriptor (pure Point) [("title", "Scatter")]
              {title="Weight", encodings=pureLs Size, encType=Quantitative, rows=wrapCol #weight df2},
              {title="Label", encodings=toList [pure Color, pure Tooltip], encType=Nominal, rows=wrapCol #label df2}])
 
-                 
+
 :html showVega $ toJSON chart2
 > <html output>
 
@@ -326,7 +328,7 @@ chart2 = (AsVLDescriptor (pure Point) [("title", "Scatter")]
 
 
 y1 :  (Fin 3) => (Fin 10) => Float = arb $ newKey 0
-df3 = for i. cumSum . for j. select (y1.i.j > 0.0) (-1.0) 1.0 
+df3 = for i. cumSum . for j. select (y1.i.j > 0.0) (-1.0) 1.0
 
 :t df3
 > ((Fin 3) => (Fin 10) => Float32)
@@ -350,7 +352,7 @@ def showChart4 [ToJSON o] (opts:o) : Value  = toJSON (AsVLDescriptor (pure Rect)
             [{title="match", encodings=pureLs Color, encType=Quantitative, rows=for (i,j). toJSON z.i.j},
             {title="words", encodings=pureLs Tooltip, encType=Nominal, rows=for (i,j). toJSON (words.i <> " - " <> words.j)},
             {title="row", encodings=pureLs X, encType=Ordinal, rows=for (i,_). toJSON (ordinal i)},
-            {title="col", encodings=pureLs Y, encType=Ordinal, rows=for (_,j). toJSON (ordinal j)}]  
+            {title="col", encodings=pureLs Y, encType=Ordinal, rows=for (_,j). toJSON (ordinal j)}]
         )
 
 ' Default heat map
@@ -367,4 +369,4 @@ def showChart4 [ToJSON o] (opts:o) : Value  = toJSON (AsVLDescriptor (pure Rect)
 > <html output>
 
 
-' (end)
\ No newline at end of file
+' (end)
diff --git a/static/dynamic.js b/static/dynamic.js
index 41d567b79..7aeeb9524 100644
--- a/static/dynamic.js
+++ b/static/dynamic.js
@@ -83,9 +83,3 @@ source.onmessage = function(event) {
         renderMathInElement(proseBlock, katexOptions)
     );
 };
-
-
-// Needed to resize dynamic iframe heights.
-function resize_iframe(obj) {
-    obj.style.height = obj.contentWindow.document.documentElement.scrollHeight + 'px';
-}