add first-class functions to brush language

src/app/MetaBrush/Application.hs

@@ -102,7 +102,7 @@ import Math.Vector2D
 import MetaBrush.Action
   ( ActionOrigin(..) )
 import qualified MetaBrush.Asset.Brushes as Asset.Brushes
-  ( circle )
+  ( EllipseBrushFields, ellipse )
 import MetaBrush.Asset.Colours
   ( getColours )
 import MetaBrush.Asset.Logo
@@ -164,7 +164,7 @@ runApplication application = do
 
   uniqueSupply <- newUniqueSupply
 
-  circleBrush  <- Asset.Brushes.circle uniqueSupply
+  ellipseBrush <- Asset.Brushes.ellipse uniqueSupply
   docUnique    <- runReaderT freshUnique uniqueSupply
   strokeUnique <- runReaderT freshUnique uniqueSupply
 
@@ -179,14 +179,14 @@ runApplication application = do
             { strokeName    = "Stroke 1"
             , strokeVisible = True
             , strokeUnique  = strokeUnique
-            , strokeBrush   = Just $ adaptBrush @'[ "r" SuperRecord.:= Double ] circleBrush
+            , strokeBrush   = Just $ adaptBrush @Asset.Brushes.EllipseBrushFields ellipseBrush
             , strokeSpline  =
               Spline
-                { splineStart  = mkPoint ( Point2D 10 -20 ) 2
+                { splineStart  = mkPoint ( Point2D 10 -20 ) 2 1 0
                 , splineCurves = OpenCurves $ Seq.fromList
-                  [ LineTo { curveEnd = NextPoint ( mkPoint ( Point2D  10  10 ) 10 ), curveData = invalidateCache undefined }
+                  [ LineTo { curveEnd = NextPoint ( mkPoint ( Point2D  10  10 ) 10 5 ( pi / 4 ) ), curveData = invalidateCache undefined }
-                  , LineTo { curveEnd = NextPoint ( mkPoint ( Point2D -10  10 )  5 ), curveData = invalidateCache undefined }
+                  , LineTo { curveEnd = NextPoint ( mkPoint ( Point2D -10  10 )  8 5 ( pi / 4 ) ), curveData = invalidateCache undefined }
-                  , LineTo { curveEnd = NextPoint ( mkPoint ( Point2D -10 -20 ) 15 ), curveData = invalidateCache undefined }
+                  , LineTo { curveEnd = NextPoint ( mkPoint ( Point2D -10 -20 ) 10 7 ( pi / 2 ) ), curveData = invalidateCache undefined }
                   ]
                 }
             }
@@ -194,8 +194,9 @@ runApplication application = do
         )
       ]
         where
-          mkPoint :: Point2D Double -> Double -> PointData ( Super.Rec '[ "r" SuperRecord.:= Double ] )
+          mkPoint :: Point2D Double -> Double -> Double -> Double -> PointData ( Super.Rec Asset.Brushes.EllipseBrushFields )
-          mkPoint pt r = PointData pt Normal ( #r SuperRecord.:= r SuperRecord.& SuperRecord.rnil )
+          mkPoint pt a b phi = PointData pt Normal
+            ( #a SuperRecord.:= a SuperRecord.& #b SuperRecord.:= b SuperRecord.& #phi SuperRecord.:= phi SuperRecord.&  SuperRecord.rnil )
 
   recomputeStrokesTVar <- STM.newTVarIO @Bool                                    False
   documentRenderTVar   <- STM.newTVarIO @( ( Int32, Int32 ) -> Cairo.Render () ) ( const $ pure () )

src/app/MetaBrush/Asset/Brushes.hs

@@ -39,11 +39,10 @@ import MetaBrush.Unique
 
 --------------------------------------------------------------------------------
 
-circle
+type CircleBrushFields = '[ "r" SuperRecord.:= Double ]
-  :: forall circleBrushFields
+
-  .  ( circleBrushFields ~ '[ "r" SuperRecord.:= Double ] )
+circle :: UniqueSupply -> IO ( Brush CircleBrushFields )
-  => UniqueSupply -> IO ( Brush circleBrushFields )
+circle uniqueSupply = mkBrush @CircleBrushFields uniqueSupply name code
-circle uniqueSupply = mkBrush @circleBrushFields uniqueSupply name code
   where
     name, code :: Text
     name = "Circle"
@@ -59,11 +58,8 @@ circle uniqueSupply = mkBrush @circleBrushFields uniqueSupply name code
      \          -- (-r  ,-r*c) -- (-r*c,-r  ) -> ( 0,-r)\n\
      \          -- ( r*c,-r  ) -- ( r  ,-r*c) ->   .   ]"
 
-circleCW
+circleCW :: UniqueSupply -> IO ( Brush CircleBrushFields )
-  :: forall circleBrushFields
+circleCW uniqueSupply = mkBrush @CircleBrushFields uniqueSupply name code
-  .  ( circleBrushFields ~ '[ "r" SuperRecord.:= Double ] )
-  => UniqueSupply -> IO ( Brush circleBrushFields )
-circleCW uniqueSupply = mkBrush @circleBrushFields uniqueSupply name code
   where
     name, code :: Text
     name = "Circle CW"
@@ -79,6 +75,31 @@ circleCW uniqueSupply = mkBrush @circleBrushFields uniqueSupply name code
      \          -- (-r  , r*c) -- (-r*c, r  ) -> ( 0, r)\n\
      \          -- ( r*c, r  ) -- ( r  , r*c) ->   .   ]"
 
+type EllipseBrushFields = '[ "a" SuperRecord.:= Double, "b" SuperRecord.:= Double, "phi" SuperRecord.:= Double ]
+
+ellipse :: UniqueSupply -> IO ( Brush EllipseBrushFields )
+ellipse uniqueSupply = mkBrush @EllipseBrushFields uniqueSupply name code
+  where
+    name, code :: Text
+    name = "Ellipse"
+    code =
+     "with\n\
+     \  a = 1\n\
+     \  b = 1\n\
+     \  phi = 0\n\
+     \satisfying\n\
+     \  a > 0 && b > 0\n\
+     \define\n\
+     \  let\n\
+     \    c = kappa\n\
+     \    applyRotation pt = rotate pt CCW by phi\n\
+     \  in\n\
+     \    map applyRotation over\n\
+     \      [ (a,0) -- ( a  , b*c) -- ( a*c, b  ) -> ( 0, b)\n\
+     \              -- (-a*c, b  ) -- (-a  , b*c) -> (-a, 0)\n\
+     \              -- (-a  ,-b*c) -- (-a*c,-b  ) -> ( 0,-b)\n\
+     \              -- ( a*c,-b  ) -- ( a  ,-b*c) ->   .   ]"
+
 {-
 rounded
   :: forall roundedBrushFields

src/app/MetaBrush/MetaParameter/AST.hs

@@ -370,10 +370,19 @@ data Term ( p :: Pass ) ( kind :: K p ) where
   CExt :: !( X_Ext p ( T p a ) ) -> Term p ( T p a )
 
 data Decl ( p :: Pass ) where
-  Decl  :: C p ( STypeI a )
+  ValDecl
-        => !( Loc p () )
+    :: C p ( STypeI a )
-        -> !( Pat p ( T p a ) ) -> !( Term p ( T p a ) )
+    => !( Pat p ( T p a ) )
-        -> Decl p
+    -> !( Loc p () )
+    -> !( Term p ( T p a ) )
+    -> Decl p
+  FunDecl
+    :: ( C p ( STypeI a ), C p ( STypeI b ) )
+    => !( Loc p ( Name p ) )
+    -> !( Pat p ( T p a ) )
+    -> !( Loc p () )
+    -> !( Term p ( T p b ) )
+    -> Decl p
 
 data Pat ( p :: Pass ) ( kind :: K p ) where
   PName :: { patName :: !( Loc p ( Name p ) ) }
@@ -550,7 +559,7 @@ instance Ext Tc a where
 -------------------
 
 termSpan :: Term p a -> Span
-termSpan ( f :$ a ) = termSpan f <> termSpan a
+termSpan ( f :$ a )                = termSpan f <> termSpan a
 termSpan ( Var ( Located l _ ) )   = l
 termSpan ( Let locs _ body )       = foldMap ( \ ( Located l _ ) -> l ) locs <> termSpan body
 termSpan ( With locs _ _ body )    = foldMap ( \ ( Located l _ ) -> l ) locs <> termSpan body
@@ -561,7 +570,7 @@ termSpan ( Line locs _ _ )         = foldMap ( \ ( Located l _ ) -> l ) locs
 termSpan ( Bez2 locs _ _ _ )       = foldMap ( \ ( Located l _ ) -> l ) locs
 termSpan ( Bez3 locs _ _ _ _ )     = foldMap ( \ ( Located l _ ) -> l ) locs
 termSpan ( PolyBez locs _ )        = foldMap ( \ ( Located l _ ) -> l ) locs
-termSpan ( CExt _ ) = mempty
+termSpan ( CExt _ )                = mempty
 
 
 toTreeTerm
@@ -617,7 +626,8 @@ toTreeDecl
   .  ( Show ( Name p ), forall x. Ext p x, forall (kvs :: Ks p). Ext_With p kvs )
   => Decl p
   -> Tree String
-toTreeDecl ( Decl _ lhs rhs ) = Node "(=)" [ toTreePat lhs, toTreeTerm rhs ]
+toTreeDecl ( ValDecl lhs _ rhs ) = Node "(=)" [ toTreePat lhs, toTreeTerm rhs ]
+toTreeDecl ( FunDecl nm arg _ rhs ) = Node "(=)" [ Node ( show nm ) [ toTreePat arg ], toTreeTerm rhs ]
 
 toTreePat :: Show ( Name p ) => Pat p a -> Tree String
 toTreePat ( PName   nm       ) = Node ( show nm ) [ ]

src/app/MetaBrush/MetaParameter/Eval.hs

@@ -6,6 +6,7 @@
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE LambdaCase            #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns        #-}
 {-# LANGUAGE OverloadedStrings     #-}
@@ -20,7 +21,7 @@ module MetaBrush.MetaParameter.Eval
 
 -- base
 import Data.Foldable
-  ( for_ )
+  ( for_, traverse_ )
 import Data.Functor.Compose
   ( Compose(..) )
 import Data.Type.Equality
@@ -107,7 +108,7 @@ eval ( PolyBez _ spline ) =
     ( const $ bitraverseCurve ( const $ pure () ) ( const eval ) )
     eval
     spline
-eval ( Let _ decls a ) = declare decls *> eval a
+eval ( Let _ decls a ) = traverse_ declare decls *> eval a
 eval ( With _ ( Tc_With ( withDeclsRecord :: Super.Rec ( MapFields UniqueTerm brushFields ) ) ) _ ( body :: Term Tc r ) ) = do
   defaultParamsRecord <-
     SuperRecord.traverseC @IsUniqueTerm2 @( State EvalState ) @( MapFields UniqueTerm brushFields ) @( MapFields UniqueField brushFields )
@@ -154,56 +155,72 @@ eval ( Var var@( Located _ ( UniqueName _ varUniq ) ) ) = do
           )
 eval ( CExt ( Val v ) ) = pure v
 
-declare :: [ Decl Tc ] -> State EvalState ()
+declare :: Decl Tc -> State EvalState ( Maybe UniqueName )
-declare [] = pure ()
+declare ( ValDecl pat _ t ) =
-declare ( Decl _ pat t : next ) = go pat t *> declare next
+  declareVal pat t
-  where
+declare ( FunDecl ( Located { located = nm } ) args _ t ) =
-    go :: forall a. STypeI a => Pat Tc a -> Term Tc a -> State EvalState ( Maybe UniqueName )
+  Just <$> declareFun nm args t
-    go ( PName ( Located _ patUniqName@( UniqueName _ patUniq ) ) ) r = do
+
+declareVal :: forall a. STypeI a => Pat Tc a -> Term Tc a -> State EvalState ( Maybe UniqueName )
+declareVal ( PName ( Located { located = patUniqName@( UniqueName { nameUnique = patUniq } ) } ) ) r = do
+  modifying ( field' @"evalHeap" )
+    ( Map.insert patUniq $ TypedTerm r )
+  pure ( Just patUniqName )
+declareVal ( PPoint _ lpat rpat ) r = do
+  case sTypeI @a of
+    sTyPoint@STyPoint
+      | ( _ :: SType ( Point2D x ) ) <- sTyPoint
+      -> do
+      nextUnique <- use ( field' @"nextUnique" )
+      let
+        uniq1, uniq2, uniq3, nextUnique' :: Unique
+        uniq1       = nextUnique
+        uniq2       = succ uniq1
+        uniq3       = succ uniq2
+        nextUnique' = succ uniq3
+      assign ( field' @"nextUnique" ) nextUnique'
+      let
+        pairText :: Text
+        pairText = "$pair%" <> Text.pack ( show uniq1 )
+        pairName, fstName, sndName :: UniqueName
+        pairName = UniqueName pairText               uniq1
+        fstName  = UniqueName ( pairText <> "$fst" ) uniq2
+        sndName  = UniqueName ( pairText <> "$snd" ) uniq3
+        var_l, var_r :: Term Tc x
+        var_l = Var ( Located noSpan fstName )
+        var_r = Var ( Located noSpan sndName )
       modifying ( field' @"evalHeap" )
-        ( Map.insert patUniq $ TypedTerm r )
+        ( Map.union
-      pure ( Just patUniqName )
+        $ Map.fromList
-    go ( PPoint _ lpat rpat ) r = do
+            [ ( uniq1, TypedTerm $ Point [] var_l var_r )
-      case sTypeI @a of
+            , ( uniq2, TypedTerm $ ( Op @( a -> x ) [] "fst" ( \ ~( Point2D x _ ) -> x ) ) :$ r )
-        sTyPoint@STyPoint
+            , ( uniq3, TypedTerm $ ( Op @( a -> x ) [] "snd" ( \ ~( Point2D _ y ) -> y ) ) :$ r )
-          | ( _ :: SType ( Point2D x ) ) <- sTyPoint
+            ]
-          -> do
+        )
-          nextUnique <- use ( field' @"nextUnique" )
+      _ <- declareVal lpat var_l
-          let
+      _ <- declareVal rpat var_r
-            uniq1, uniq2, uniq3, nextUnique' :: Unique
+      pure ( Just pairName )
-            uniq1       = nextUnique
+declareVal ( AsPat _ ( Located { located = asUniqName@( UniqueName { nameUnique = asUniq } ) } ) patt ) r = do
-            uniq2       = succ uniq1
+  mbNm <- declareVal patt r
-            uniq3       = succ uniq2
+  for_ mbNm \ nm ->
-            nextUnique' = succ uniq3
+    modifying ( field' @"evalHeap" )
-          assign ( field' @"nextUnique" ) nextUnique'
+      ( Map.insert asUniq ( TypedTerm $ Var @Tc @a ( Located noSpan nm ) ) )
-          let
+  pure ( Just asUniqName )
-            pairText :: Text
+declareVal ( PWild _ ) _ = pure Nothing
-            pairText = "$pair%" <> Text.pack ( show uniq1 ) 
+
-            pairName, fstName, sndName :: UniqueName
+declareFun
-            pairName = UniqueName pairText               uniq1
+  :: forall a b. ( STypeI a, STypeI b )
-            fstName  = UniqueName ( pairText <> "$fst" ) uniq2
+  => UniqueName -> Pat Tc a -> Term Tc b -> State EvalState UniqueName
-            sndName  = UniqueName ( pairText <> "$snd" ) uniq3
+declareFun uniq@( UniqueName { nameUnique = funUnique } ) argPat rhs = do
-            var_l, var_r :: Term Tc x
+  st <- get
-            var_l = Var ( Located noSpan fstName )
+  let
-            var_r = Var ( Located noSpan sndName )
+    fun :: a -> b
-          modifying ( field' @"evalHeap" )
+    fun arg = ( `evalState` st ) do
-            ( Map.union
+      _ <- declareVal argPat ( CExt @Tc @a ( Val arg ) )
-            $ Map.fromList
+      eval rhs
-                [ ( uniq1, TypedTerm $ Point [] var_l var_r )
+  modifying ( field' @"evalHeap" )
-                , ( uniq2, TypedTerm $ ( Op @( a -> x ) [] "fst" ( \ ~( Point2D x _ ) -> x ) ) :$ r )
+    ( Map.insert funUnique ( TypedTerm $ CExt @Tc @( a -> b ) ( Val fun ) ) )
-                , ( uniq3, TypedTerm $ ( Op @( a -> x ) [] "snd" ( \ ~( Point2D _ y ) -> y ) ) :$ r )
+  pure uniq
-                ]
-            )
-          go lpat var_l
-          go rpat var_r
-          pure ( Just pairName )
-    go ( AsPat _ ( Located _ asUniqName@( UniqueName _ asUniq ) ) patt ) r = do
-      mbNm <- go patt r
-      for_ mbNm \ nm ->
-        modifying ( field' @"evalHeap" )
-          ( Map.insert asUniq ( TypedTerm $ Var @Tc @a ( Located noSpan nm ) ) )
-      pure ( Just asUniqName )
-    go ( PWild _ ) _ = pure Nothing
 
 bindRecordValues
   :: forall brushFields usedFields defaultFields

src/app/MetaBrush/MetaParameter/Parse.hs

@@ -80,6 +80,7 @@ import MetaBrush.MetaParameter.PrimOp
   , scale_around_by, scale_by
   , shear_from_by, shear_by
   , translate_by
+  , map_over
   )
   
 --------------------------------------------------------------------------------
@@ -101,61 +102,6 @@ showParses x = do
       tree = toTreeTerm expr
     drawTree tree
 
-examples :: [ Located Token ] -> Int -> IO ()
-examples inputToks n =
-  for_ ( Earley.exactly n ( Earley.generator grammar inputToks ) ) \ ( expr, toks ) -> do
-    for_ toks ( located >>> showToken >>> ( <> " " ) >>> putStr )
-    putStrLn ""
-    drawTree ( toTreeTerm expr )
-    putStrLn "\n\n"
-
-someToks :: [ Located Token ]
-someToks = map ( Located mempty )
-  [ TokAlphabetic "x"
-  , TokAlphabetic "let"
-  , TokAlphabetic "in"
-  , TokSpecial '['
-  , TokSpecial ']'
-  , TokSpecial '('
-  , TokSpecial ')'
-  , TokSymbolic "="
-  , TokSymbolic "--"
-  , TokSymbolic "->"
-  , TokSymbolic "."
-  ]
-
-test1 :: Text
-test1 =
-  "  let\n\
-  \    q = rotate p around c CW by theta + 3 * theta2\n\
-  \    r = scale ( translate q by t ) by (7,11)\n\
-  \  in rotate q around p CW by phi"
-
-test2 :: Text
-test2 =
-  "  let\n\
-  \    p = (3,3)\n\
-  \    q = (1,1)\n\
-  \  in\n\
-  \    rotate p\n\
-  \      around q\n\
-  \      CCW by\n\
-  \        let\n\
-  \          q = pi / 2 \n\
-  \        in q"
-
-test3 :: Text
-test3 =
-  "  let\n\
-  \    p = (1,1)\n\
-  \  in\n\
-  \    [ p -- c1 -- c2 -> q\n\
-  \        -- c3 -- c4 -> r\n\
-  \        -> s  -> .\n\
-  \      ]"
-
-
-
 --------------------------------------------------------------------------------
 -- Language grammar.
 
@@ -227,14 +173,24 @@ grammar = mdo
   anyPattern <- Earley.rule ( ( basicPattern <|> asPattern ) <?> "pattern" )
 
   declaration <-
-    Earley.rule
+    Earley.rule $
       ( do
-        p <- anyPattern
+        funName <- alphabeticName
+        anyWhitespace
+        argPat <- anyPattern
         anyWhitespace
         eqLoc <- symbol "="
-        e <- expr
+        rhs <- expr
-        pure ( Location ( location eqLoc ), p, e )
+        pure ( FunDecl funName argPat ( Location ( location eqLoc ) ) rhs )
-      <?> "declaration"
+      <?> "function declaration"
+      ) <|>
+      ( do
+        lhs <- anyPattern
+        anyWhitespace
+        eqLoc <- symbol "="
+        rhs <- expr
+        pure ( ValDecl lhs ( Location ( location eqLoc ) ) rhs )
+      <?> "variable declaration"
       )
 
   moreDeclarations <- Earley.rule
@@ -242,7 +198,7 @@ grammar = mdo
         separator
         decl <- declaration
         more <- moreDeclarations
-        pure $ ( \ ( l, p, e ) -> Decl l p e : more ) decl
+        pure ( decl : more )
     <|> pure []
     )
 
@@ -251,7 +207,7 @@ grammar = mdo
       ( do
           decl <- declaration
           more <- moreDeclarations
-          pure $ ( \ ( l, p, e ) -> Decl l p e : more ) decl
+          pure ( decl : more )
       <|> pure []
       )
 
@@ -361,6 +317,7 @@ reserved
   [ "let", "in"
   , "with", "set", "satisfying"
   , "around", "by", "rotate", "scale", "shear", "translate", "transform"
+  , "map", "over"
   , "cw", "ccw"
   , "pi", "tau", "kappa"
   ]
@@ -520,6 +477,13 @@ mixfixTable
           "translate_by_" translate_by
             :$ p :$ t
       )
+    , ( [ Just $ ws_tokAlpha "map", Nothing, Just $ ws_tokAlpha "over", Nothing ]
+      , Earley.NonAssoc
+      , \ [ Just ( Located lt _ ), _, Just ( Located lb _ ), _ ] [ f, v ] ->
+        Op [ Location lt, Location lb ]
+          "map_over_" map_over
+            :$ f :$ v
+      )
     ]
   , [ ( [ Nothing, Just $ ws_tokSymbol "||", Nothing ]
       , Earley.RightAssoc

src/app/MetaBrush/MetaParameter/PrimOp.hs

@@ -1,8 +1,11 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DerivingStrategies #-}
 
 module MetaBrush.MetaParameter.PrimOp where
 
 -- MetaBrush
+import Math.Bezier.Spline
+  ( SplineType(Closed), SplinePts )
 import Math.Vector2D
   ( Point2D(..) )
 
@@ -19,15 +22,15 @@ kappa = 0.5519150244935105707435627227925
 rotate_around_by :: Orientation -> Point2D Double -> Point2D Double -> Double -> Point2D Double
 rotate_around_by ori ( Point2D px py ) ( Point2D cx cy ) theta =
   translate_by ( rotate_by ori ( Point2D ( px - cx ) ( py - cy ) ) theta ) ( Point2D cx cy )
-rotate_by :: Orientation -> Point2D Double  -> Double -> Point2D Double
+rotate_by :: Orientation -> Point2D Double -> Double -> Point2D Double
 rotate_by CCW ( Point2D px py ) theta = Point2D ( c * px - s * py ) ( c * py + s * px )
   where
     c, s :: Double
     c = cos theta
     s = sin theta
-rotate_by CW  p theta = rotate_by CCW p ( -theta ) 
+rotate_by CW p theta = rotate_by CCW p ( -theta )
 
-scale_around_by :: Point2D Double -> Point2D Double -> Point2D Double  -> Point2D Double
+scale_around_by :: Point2D Double -> Point2D Double -> Point2D Double -> Point2D Double
 scale_around_by ( Point2D px py ) ( Point2D cx cy ) ( Point2D rx ry ) = Point2D ( rx * ( px - cx ) + cx ) ( ry * ( py - cy ) + cy )
 scale_by :: Point2D Double -> Point2D Double -> Point2D Double
 scale_by ( Point2D px py ) ( Point2D rx ry ) = Point2D ( rx * px ) ( ry * py )
@@ -40,3 +43,6 @@ shear_by ( Point2D px py ) ( Point2D vx vy ) = undefined
 
 translate_by :: Point2D Double -> Point2D Double -> Point2D Double
 translate_by ( Point2D px py ) ( Point2D tx ty ) = Point2D ( px + tx ) ( py + ty )
+
+map_over :: ( Point2D Double -> Point2D Double ) -> ( SplinePts Closed -> SplinePts Closed )
+map_over = fmap

src/app/MetaBrush/MetaParameter/Rename.hs

@@ -117,13 +117,22 @@ renameDecls decls = do
   where
 
     go :: Map Text Unique -> [ Decl P ] -> m [ Decl Rn ]
-    go outerLocalVars ( Decl loc lhs rhs : next ) = do
+    go outerLocalVars ( ValDecl lhs eqLoc rhs : next ) = do
       -- Collect all the declarations from the left-hand sides.
       lhs'  <- renameLhs outerLocalVars lhs
       next' <- go outerLocalVars next
-      -- Now rename each right-hand side with the full LHS info.
+      -- Now rename the right-hand side with the full LHS info.
       rhs'  <- locally ( rename rhs )
-      pure $ Decl loc lhs' rhs' : next'
+      pure $ ValDecl lhs' eqLoc rhs' : next'
+    go outerLocalVars ( FunDecl funName argPat eqLoc rhs : next ) = do
+      -- Collect all the declarations from the left-hand sides.
+      funName' <- patName <$> renameLhs outerLocalVars ( PName funName )
+      next'    <- go outerLocalVars next
+      -- Now rename the right-hand side with the full LHS info,
+      -- taking care to bring into scope the names bound by the function
+      -- when renaming the RHS.
+      ( lhs', rhs' ) <- locally ( (,) <$> renameLhs outerLocalVars argPat <*> rename rhs )
+      pure $ FunDecl funName' lhs' eqLoc rhs' : next'
     go outerLocalVars [] = do
       -- Finished handling all the left-hand sides:
       --   add all the declared names to the existing (outer) names,

src/app/MetaBrush/MetaParameter/TypeCheck.hs

@@ -263,10 +263,20 @@ typeCheckDecls = go []
     catchOutOfScope _    err                   = throwError err
 
 typeCheckDecl :: MonadTc m => Decl Rn -> m ( Decl Tc )
-typeCheckDecl ( Decl loc lhs rhs ) = do
+typeCheckDecl ( ValDecl lhs eqLoc rhs ) = do
   TypedTerm ( rhs' :: Term Tc a ) <- typeCheck rhs
   lhs' <- typeCheckPatAt @a lhs
-  pure ( Decl loc lhs' rhs' )
+  pure ( ValDecl lhs' eqLoc rhs' )
+-- TODO: this assumes all user-declared functions are of type @ Point2D Double -> Point2D Double @.
+-- A better solution would be to introduce a unification variable for the argument type,
+-- and throw an error (or default) if there remain uninstantiated unification variables after typechecking the RHS.
+typeCheckDecl ( FunDecl funName@( Located _ ( UniqueName _ uniq ) ) argPat eqLoc rhs ) = do
+  argPat' <- typeCheckPatAt @( Point2D Double ) argPat
+  rhs'    <- typeCheckAt @( Point2D Double ) "Expected function of type `Point2D Double -> Point2D Double'"  rhs
+  assign
+    ( field' @"globalEnv" . field' @"tcGlobalVarTys" . at uniq )
+    ( Just $ SomeSType ( proxy# :: Proxy# ( Point2D Double -> Point2D Double ) ) )
+  pure ( FunDecl funName argPat' eqLoc rhs' )
 
 typeCheckPatAt :: forall ( a :: Type ) m. ( STypeI a, MonadTc m ) => Pat Rn '() -> m ( Pat Tc a )
 typeCheckPatAt ( PName nm@( Located _ ( UniqueName _ uniq ) ) ) = do
@@ -307,10 +317,11 @@ withDeclsRecord decls f = do
     revSortDecls :: [ Decl Tc ] -> m [ ( Text, ( UniqueName, TypedTerm ) ) ]
     revSortDecls = fmap ( sortOn ( Down . fst ) ) . traverse getDeclName
     getDeclName :: Decl Tc -> m ( Text, ( UniqueName, TypedTerm ) )
-    getDeclName ( Decl ( Located loc _ ) pat term ) = case pat of
+    getDeclName ( ValDecl pat ( Located eqLoc _ ) term ) = case pat of
       PName   ( Located _ uniq@( UniqueName nm _ ) )   -> pure ( nm, ( uniq, TypedTerm term ) )
       AsPat _ ( Located _ uniq@( UniqueName nm _ ) ) _ -> pure ( nm, ( uniq, TypedTerm term ) )
-      _                                                -> tcError $ NoPatternName loc
+      _                                                -> tcError $ NoPatternName eqLoc
+    getDeclName ( FunDecl funName _ _ _ ) = tcError $ UnexpectedFunDecl funName
     go :: TypedTermsRecord -> [ ( Text, ( UniqueName, TypedTerm ) ) ] -> TypedTermsRecord
     go record [] = record
     go  ( TypedTermsRecord ( record :: Super.Rec ( MapFields UniqueTerm kvs ) ) )
@@ -413,6 +424,8 @@ data TcError
   }
   | OutOfScope
   { outOfScopeVar :: !( Located UniqueName ) }
+  | UnexpectedFunDecl
+  { funDeclLoc :: !( Located UniqueName ) }
   deriving stock ( Show, Generic )
 
 data TcWarning = TcWarning