Merge branch 'dev-2023'

dex.cabal

@@ -48,7 +48,6 @@ library
                      , Algebra
                      , Builder
                      , CUDA
-                     , Cat
                      , CheapReduction
                      , CheckType
                      , ConcreteSyntax
@@ -58,6 +57,7 @@ library
                      , Generalize
                      , Imp
                      , ImpToLLVM
+                     , IncState
                      , Inference
                      , Inline
                      , IRVariants
@@ -70,39 +70,38 @@ library
                      , LLVM.Shims
                      , Lexing
                      , Linearize
-                     , Logging
                      , Lower
+                     , MonadUtil
                      , MTL1
                      , Name
                      , Occurrence
                      , OccAnalysis
                      , Optimize
+                     , PeepholeOptimize
                      , PPrint
                      , RawName
                      , Runtime
                      , RuntimePrint
                      , Serialize
                      , Simplify
                      , Subst
-                     , SourceInfo
                      , SourceRename
+                     , SourceIdTraversal
                      , TopLevel
                      , Transpose
-                     , TraverseSourceInfo
                      , Types.Core
                      , Types.Imp
-                     , Types.Misc
                      , Types.Primitives
                      , Types.OpNames
                      , Types.Source
+                     , Types.Top
                      , QueryType
                      , QueryTypePure
                      , Util
                      , Vectorize
   if flag(live)
     exposed-modules:   Actor
                      , Live.Eval
-                     , Live.Terminal
                      , Live.Web
                      , RenderHtml
   other-modules:       Paths_dex
@@ -126,7 +125,6 @@ library
                      , prettyprinter
                      , text
                        -- Portable system utilities
-                     , ansi-terminal
                      , directory
                      , filepath
                      , haskeline
@@ -135,11 +133,13 @@ library
                        -- Serialization
                      , aeson
                      , store
+                     , time
                        -- Floating-point pedanticness (correcting for GHC < 9.2.2)
                      , floating-bits
   if flag(live)
     build-depends:     binary
                      , blaze-html
+                     , blaze-markup
                      , cmark
                      , http-types
                      , wai
@@ -234,6 +234,7 @@ executable dex
   main-is:             dex.hs
   build-depends:       dex
                      , ansi-wl-pprint
+                     , ansi-terminal
                      , base
                      , bytestring
                      , containers

examples/raytrace.dx

@@ -15,7 +15,7 @@ def Vec(n:Nat) -> Type = Fin n => Float
 def Mat(n:Nat, m:Nat) -> Type = Fin n => Fin m => Float
 
 def relu(x:Float) -> Float = max x 0.0
-def length(x: d=>Float) -> Float given (d|Ix) = sqrt $ sum for i. sq x[i]
+def length(x: d=>Float) -> Float given (d|Ix) = sqrt $ sum for i:d. sq x[i]
 -- TODO: make a newtype for normal vectors
 def normalize(x: d=>Float) -> d=>Float given (d|Ix) = x / (length x)
 def directionAndLength(x: d=>Float) -> (d=>Float, Float) given (d|Ix) =
@@ -68,7 +68,7 @@ def rotateZ(p:Vec 3, angle:Angle) -> Vec 3 =
   [c*px - s*py, s*px+c*py, pz]
 
 def sampleCosineWeightedHemisphere(normal: Vec 3, k:Key) -> Vec 3 =
-  [k1, k2] = split_key k
+  [k1, k2] = split_key(n=2, k)
   u1 = rand k1
   u2 = rand k2
   uu = normalize $ cross normal [0.0, 1.1, 1.1]
@@ -152,21 +152,21 @@ def sdObject(pos:Position, obj:Object) -> Distance =
       Wall(nor, d) -> d + dot nor pos
       Block(blockPos, halfWidths, angle) ->
         pos' = rotateY (pos - blockPos) angle
-        length $ for i. max ((abs pos'[i]) - halfWidths[i]) 0.0
+        length $ for i:(Fin 3). max ((abs pos'[i]) - halfWidths[i]) 0.0
       Sphere(spherePos, r) ->
         pos' = pos - spherePos
         max (length pos' - r) 0.0
     Light(squarePos, hw, _) ->
       pos' = pos - squarePos
       halfWidths = [hw, 0.01, hw]
-      length $ for i. max ((abs pos'[i]) - halfWidths[i]) 0.0
+      length $ for i:(Fin 3). max ((abs pos'[i]) - halfWidths[i]) 0.0
 
 def sdScene(scene:Scene n, pos:Position) -> (Object, Distance) given (n|Ix) =
-  (i, d) = minimum_by snd $ for i. (i, sdObject pos scene.objects[i])
+  (i, d) = minimum_by(for i:n. (i, sdObject pos scene.objects[i]), snd)
   (scene.objects[i], d)
 
 def calcNormal(obj:Object, pos:Position) -> Direction =
-  normalize (grad (\pos. sdObject pos obj) pos)
+  grad(\p:Position. sdObject(p, obj)) pos | normalize
 
 data RayMarchResult =
   -- incident ray, surface normal, surface properties
@@ -176,7 +176,7 @@ data RayMarchResult =
   HitNothing
 
 def raymarch(scene:Scene n, ray:Ray) -> RayMarchResult given (n|Ix) =
-  maxIters = 100
+  maxIters : Nat = 100
   tol = 0.01
   startLength = 10.0 * tol  -- trying to escape the current surface
   with_state (10.0 * tol) \rayLength.
@@ -209,7 +209,7 @@ def rayDirectRadiance(scene:Scene n, ray:Ray) -> Radiance given (n|Ix) =
     HitObj(_, _) -> zero
 
 def sampleSquare(hw:Float, k:Key) -> Position =
- [kx, kz] = split_key k
+ [kx, kz] : Fin 2 => Key = split_key k
  x = randuniform (- hw) hw kx
  z = randuniform (- hw) hw kz
  [x, 0.0, z]
@@ -220,7 +220,7 @@ def sampleLightRadiance(
     inRay:Ray,
     k:Key) -> Radiance given (n|Ix) =
   yield_accum (AddMonoid Float) \radiance.
-    for i. case scene.objects[i] of
+    each scene.objects \obj. case obj of
       PassiveObject(_, _) -> ()
       Light(lightPos, hw, _) ->
         (dirToLight, distToLight) = directionAndLength $
@@ -244,7 +244,7 @@ def trace(params:Params, scene:Scene n, initRay:Ray, k:Key) -> Color given (n|Ix
             if i == 0 then radiance += intensity   -- TODO: scale etc
             Done ()
           HitObj(incidentRay, osurf) ->
-            [k1, k2] = split_key $ hash k i
+            [k1, k2] = split_key(n=2, hash k i)
             lightRadiance = sampleLightRadiance scene osurf incidentRay k1
             ray    := sampleReflection osurf incidentRay k2
             filter := surfaceFilter (get filter) osurf.surface
@@ -265,27 +265,24 @@ def cameraRays(n:Nat, camera:Camera) -> Fin n => Fin n => ((Key) -> Ray) =
   pixHalfWidth = halfWidth / n_to_f n
   ys = reverse $ linspace (Fin n) (neg halfWidth) halfWidth
   xs =           linspace (Fin n) (neg halfWidth) halfWidth
-  for i j. \key.
-    [kx, ky] = split_key key
+  for i:(Fin n) j:(Fin n). \key.
+    [kx, ky] = split_key(n=2, key)
     x = xs[j] + randuniform (-pixHalfWidth) pixHalfWidth kx
     y = ys[i] + randuniform (-pixHalfWidth) pixHalfWidth ky
     Ray(camera.pos, normalize [x, y, neg camera.sensorDist])
 
 def takePicture(params:Params, scene:Scene m, camera:Camera) -> Image given (m|Ix) =
-  n = camera.numPix
-  rays = cameraRays n camera
+  rays = cameraRays camera.numPix camera
   rootKey = new_key 0
-  image = for i j.
+  image = for i:(Fin camera.numPix) j:(Fin camera.numPix).
     pixKey = if params.shareSeed
       then rootKey
       else ixkey (ixkey rootKey i) j
     def sampleRayColor(k:Key) -> Color =
-      [k1, k2] = split_key k
+      [k1, k2] = split_key(n=2, k)
       trace params scene (rays[i,j] k1) k2
     sampleAveraged sampleRayColor params.numSamples pixKey
-  MkImage _ _ $ image / mean (for ixs.
-                                (i,j,k) = ixs
-                                image[i,j,k])
+  MkImage _ _ $ image / mean(flatten3D(image))
 
 '## Define the scene and render it
 

lib/diagram.dx

@@ -35,15 +35,16 @@ struct GeomStyle =
 default_geom_style = GeomStyle Nothing (Just black) 1
 
 -- TODO: consider sharing attributes among a set of objects for efficiency
+Object : Type = (GeomStyle, Point, Geom)
 struct Diagram =
-  val : (List (GeomStyle, Point, Geom))
+  val : (List Object)
 
 instance Monoid(Diagram)
   mempty = Diagram mempty
   def (<>)(d1, d2) = Diagram $ d1.val <> d2.val
 
 def concat_diagrams(diagrams:n=>Diagram) -> Diagram given (n|Ix) =
-  Diagram $ concat for i. diagrams[i].val
+  Diagram $ concat $ each diagrams \d. d.val
 
 -- TODO: arbitrary affine transformations. Our current representation of
 -- rectangles and circles means we can only do scale/flip/rotate90.
@@ -54,8 +55,8 @@ def apply_transformation(
     d:Diagram
     ) -> Diagram =
   AsList(_, objs) = d.val
-  Diagram $ to_list for i.
-    (attr, p, geom) = objs[i]
+  Diagram $ to_list $ each objs \obj.
+    (attr, p, geom) = obj
     (attr, transformPoint p, transformGeom geom)
 
 def flip_y(d:Diagram) -> Diagram =
@@ -92,8 +93,8 @@ def text(x:String)         -> Diagram = singleton_default $ Text x
 
 def update_geom(update: (GeomStyle) -> GeomStyle, d:Diagram) -> Diagram =
   AsList(_, objs) = d.val
-  Diagram $ to_list for i.
-    (       attr, point, geoms) = objs[i]
+  Diagram $ to_list $ each objs \obj.
+    (       attr, point, geoms) = obj
     (update attr, point, geoms)
 
 -- TODO: these would be better if we had field-access-based ref projections, so we could
@@ -149,7 +150,7 @@ def (<=>)(attr:String, val:b) -> String given (b|Show) =
   attr <.> "=" <.> quote (show val)
 
 def html_color(cs:HtmlColor) -> String =
-  "#" <> (concat $ for i. showHex cs[i])
+  "#" <> (concat $ each cs showHex)
 
 def optional_html_color(c: Maybe HtmlColor) -> String =
   case c of
@@ -166,7 +167,7 @@ def attr_string(attr:GeomStyle) -> String =
 def render_geom(attr:GeomStyle, p:Point, geom:Geom) -> String =
   -- For things that are solid. SVG says they have fill=stroke.
   solidAttr = GeomStyle attr.strokeColor attr.strokeColor attr.strokeWidth
-  groupEle = \attr s. tag_brackets_attr "g" (attr_string attr) s
+  groupEle = \attr:GeomStyle s:String. tag_brackets_attr "g" (attr_string attr) s
   case geom of
     PointGeom ->
       groupEle solidAttr $ self_closing_brackets $
@@ -188,7 +189,7 @@ def render_geom(attr:GeomStyle, p:Point, geom:Geom) -> String =
          "x"      <=> (p.x - (w/2.0)) <.>
          "y"      <=> (p.y - (h/2.0)))
     Text content ->
-      textEle = \s. tag_brackets_attr("text",
+      textEle = \s:String. tag_brackets_attr("text",
         ("x" <=> p.x <.>
          "y" <=> p.y <.>
          "text-anchor" <=> "middle" <.>    -- horizontal center
@@ -200,8 +201,8 @@ BoundingBox : Type = (Point, Point)
 
 @noinline
 def compute_bounds(d:Diagram) -> BoundingBox =
-  computeSubBound = \sel op.
-    \triple.
+  computeSubBound = \sel:((Point) -> Float) op:((Float) -> Float).
+    \triple:Object.
       (_, p, geom) = triple
       sel p + case geom of
         PointGeom       -> 0.0
@@ -213,12 +214,12 @@ def compute_bounds(d:Diagram) -> BoundingBox =
   AsList(_, objs) = d.val
   (
     Point(
-      minimum $ map (computeSubBound (\p. p.x) neg) objs,
-      minimum $ map (computeSubBound (\p. p.y) neg) objs
+      minimum $ each objs (computeSubBound (\p. p.x) neg),
+      minimum $ each objs (computeSubBound (\p. p.y) neg)
     ),
     Point(
-      maximum $ map (computeSubBound (\p. p.x) id)  objs,
-      maximum $ map (computeSubBound (\p. p.y) id)  objs
+      maximum $ each objs (computeSubBound (\p. p.x) id),
+      maximum $ each objs (computeSubBound (\p. p.y) id)
     )
   )
 
@@ -235,11 +236,11 @@ def render_svg(d:Diagram, bounds:BoundingBox) -> String =
                 <+> "height"  <=> imgHeight
                 <+> "viewBox" <=> (imgXMin <+> imgYMin <+> imgWidth <+> imgHeight))
   tag_brackets_attr "svg" svgAttrStr $
-    concat for i.
-      (attr, pos, geom) = objs[i]
+    concat $ each objs \obj.
+      (attr, pos, geom) = obj
       render_geom attr pos geom
 
-render_scaled_svg = \d. render_svg d (compute_bounds d)
+render_scaled_svg = \d:Diagram. render_svg d (compute_bounds d)
 
 '## Derived convenience methods and combinators