Jan/let patterns

src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs

@@ -541,12 +541,12 @@ goAxiom axiom = do
 goDeriving :: forall r. (Members '[Reader HtmlOptions] r) => Deriving 'Scoped -> Sem r Html
 goDeriving def = do
   sig <- ppHelper (ppCode def)
-  defHeader (def ^. derivingFunLhs . funLhsName) sig Nothing
+  defHeader (def ^. derivingFunLhs . funLhsName . functionDefName) sig Nothing
 
 goFunctionDef :: forall r. (Members '[Reader HtmlOptions] r) => FunctionDef 'Scoped -> Sem r Html
 goFunctionDef def = do
   sig <- ppHelper (ppCode (functionDefLhs def))
-  defHeader (def ^. signName) sig (def ^. signDoc)
+  defHeader (def ^. signName . functionDefName) sig (def ^. signDoc)
 
 goInductive :: forall r. (Members '[Reader HtmlOptions] r) => InductiveDef 'Scoped -> Sem r Html
 goInductive def = do

src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs

@@ -60,11 +60,11 @@ runInfoTableBuilder ini = reinterpret (runState ini) $ \case
      in do
           modify' (over infoInductives (HashMap.insert (ity ^. inductiveName . nameId) ity))
           highlightDoc (ity ^. inductiveName . nameId) j
-  RegisterFunctionDef f ->
+  RegisterFunctionDef f -> do
     let j = f ^. signDoc
-     in do
-          modify' (over infoFunctions (HashMap.insert (f ^. signName . nameId) f))
-          highlightDoc (f ^. signName . nameId) j
+        fid = f ^. signName . functionDefName . nameId
+    modify' (over infoFunctions (HashMap.insert fid f))
+    highlightDoc fid j
   RegisterName n -> highlightName (S.anameFromName n)
   RegisterScopedIden n -> highlightName (anameFromScopedIden n)
   RegisterModuleDoc uid doc -> highlightDoc uid doc

src/Juvix/Compiler/Concrete/Gen.hs

@@ -28,7 +28,6 @@ simplestFunctionDef :: forall s. (SingI s) => FunctionName s -> ExpressionType s
 simplestFunctionDef funName funBody =
   FunctionDef
     { _signName = name,
-      _signPattern = Nothing,
       _signBody = SigBodyExpression funBody,
       _signTypeSig =
         TypeSig
@@ -46,8 +45,12 @@ simplestFunctionDef funName funBody =
   where
     name :: FunctionSymbolType s
     name = case sing :: SStage s of
-      SParsed -> Just funName
-      SScoped -> funName
+      SParsed -> FunctionDefName funName
+      SScoped ->
+        FunctionDefNameScoped
+          { _functionDefName = funName,
+            _functionDefNamePattern = Nothing
+          }
 
 smallUniverseExpression :: forall s r. (SingI s) => (Members '[Reader Interval] r) => Sem r (ExpressionType s)
 smallUniverseExpression = do
@@ -290,7 +293,7 @@ mkTypeSigType ts = do
 
 mkTypeSigType' :: forall s. (SingI s) => ExpressionType s -> TypeSig s -> (ExpressionType s)
 mkTypeSigType' wildcard TypeSig {..} =
-  foldr mkFun rty (map mkFunctionParameters _typeSigArgs)
+  foldr (mkFun . mkFunctionParameters) rty _typeSigArgs
   where
     rty = fromMaybe wildcard _typeSigRetType
 
@@ -303,7 +306,7 @@ mkTypeSigType' wildcard TypeSig {..} =
         { _paramNames = getSigArgNames arg,
           _paramImplicit = _sigArgImplicit,
           _paramDelims = fmap Just _sigArgDelims,
-          _paramColon = Irrelevant $ maybe Nothing (Just . (^. unIrrelevant)) _sigArgColon,
+          _paramColon = Irrelevant $ fmap (^. unIrrelevant) _sigArgColon,
           _paramType = fromMaybe (univ (getLoc arg)) _sigArgType
         }
 

src/Juvix/Compiler/Concrete/Language/Base.hs

@@ -83,8 +83,8 @@ type family SymbolType s = res | res -> s where
 
 type FunctionSymbolType :: Stage -> GHCType
 type family FunctionSymbolType s = res | res -> s where
-  FunctionSymbolType 'Parsed = Maybe Symbol
-  FunctionSymbolType 'Scoped = S.Symbol
+  FunctionSymbolType 'Parsed = FunctionDefNameParsed
+  FunctionSymbolType 'Scoped = FunctionDefNameScoped
 
 type IdentifierType :: Stage -> GHCType
 type family IdentifierType s = res | res -> s where
@@ -706,11 +706,27 @@ deriving stock instance Ord (Deriving 'Parsed)
 
 deriving stock instance Ord (Deriving 'Scoped)
 
+data FunctionDefNameParsed
+  = FunctionDefNamePattern (PatternAtom 'Parsed)
+  | FunctionDefName Symbol
+  deriving stock (Eq, Ord, Show, Generic)
+
+instance Serialize FunctionDefNameParsed
+
+instance NFData FunctionDefNameParsed
+
+data FunctionDefNameScoped = FunctionDefNameScoped
+  { _functionDefName :: S.Symbol,
+    _functionDefNamePattern :: Maybe PatternArg
+  }
+  deriving stock (Eq, Ord, Show, Generic)
+
+instance Serialize FunctionDefNameScoped
+
+instance NFData FunctionDefNameScoped
+
 data FunctionDef (s :: Stage) = FunctionDef
-  { -- When s = 'Parsed, _signName must be present if the definition is
-    -- function-like. One of _signName or _signPattern must be present.
-    _signName :: FunctionSymbolType s,
-    _signPattern :: Maybe (PatternAtomType s),
+  { _signName :: FunctionSymbolType s,
     _signTypeSig :: TypeSig s,
     _signDoc :: Maybe (Judoc s),
     _signPragmas :: Maybe ParsedPragmas,
@@ -2869,7 +2885,6 @@ data FunctionLhs (s :: Stage) = FunctionLhs
     _funLhsInstance :: Maybe KeywordRef,
     _funLhsCoercion :: Maybe KeywordRef,
     _funLhsName :: FunctionSymbolType s,
-    _funLhsPattern :: Maybe (PatternAtomType s),
     _funLhsTypeSig :: TypeSig s
   }
   deriving stock (Generic)
@@ -2895,6 +2910,7 @@ deriving stock instance Ord (FunctionLhs 'Parsed)
 deriving stock instance Ord (FunctionLhs 'Scoped)
 
 makeLenses ''SideIfs
+makeLenses ''FunctionDefNameScoped
 makeLenses ''TypeSig
 makeLenses ''FunctionLhs
 makeLenses ''Statements
@@ -2984,6 +3000,7 @@ makeLenses ''MarkdownInfo
 makeLenses ''Deriving
 
 makePrisms ''NamedArgumentNew
+makePrisms ''FunctionDefNameParsed
 
 functionDefLhs :: FunctionDef s -> FunctionLhs s
 functionDefLhs FunctionDef {..} =
@@ -2993,7 +3010,6 @@ functionDefLhs FunctionDef {..} =
       _funLhsInstance = _signInstance,
       _funLhsCoercion = _signCoercion,
       _funLhsName = _signName,
-      _funLhsPattern = _signPattern,
       _funLhsTypeSig = _signTypeSig
     }
 
@@ -3156,17 +3172,33 @@ instance HasLoc (OpenModule s short) where
 instance HasLoc (ProjectionDef s) where
   getLoc = getLoc . (^. projectionConstructor)
 
-getFunLhsLoc :: (SingI s) => FunctionLhs s -> Maybe Interval
-getFunLhsLoc FunctionLhs {..} =
-  (Just . getLoc <$> _funLhsBuiltin)
-    ?<> (Just . getLoc <$> _funLhsTerminating)
-    ?<> (Just . getLocPatternAtomType <$> _funLhsPattern)
-    ?<> (getLocExpressionType <$> _funLhsTypeSig ^. typeSigRetType)
+getLocFunctionSymbolType :: forall s. (SingI s) => FunctionSymbolType s -> Interval
+getLocFunctionSymbolType = case sing :: SStage s of
+  SParsed -> getLoc
+  SScoped -> getLoc
+
+instance HasLoc FunctionDefNameScoped where
+  getLoc FunctionDefNameScoped {..} =
+    getLoc _functionDefName
+      <>? (getLoc <$> _functionDefNamePattern)
+
+instance HasLoc FunctionDefNameParsed where
+  getLoc = \case
+    FunctionDefNamePattern a -> getLoc a
+    FunctionDefName s -> getLoc s
+
+instance (SingI s) => HasLoc (FunctionLhs s) where
+  getLoc FunctionLhs {..} =
+    (getLoc <$> _funLhsBuiltin)
+      ?<> (getLoc <$> _funLhsTerminating)
+      ?<> ( getLocFunctionSymbolType _funLhsName
+              <>? (getLocExpressionType <$> _funLhsTypeSig ^. typeSigRetType)
+          )
 
 instance (SingI s) => HasLoc (Deriving s) where
   getLoc Deriving {..} =
     getLoc _derivingKw
-      <>? getFunLhsLoc _derivingFunLhs
+      <> getLoc _derivingFunLhs
 
 instance HasLoc (Statement 'Scoped) where
   getLoc :: Statement 'Scoped -> Interval
@@ -3405,8 +3437,8 @@ instance (SingI s) => HasLoc (FunctionDef s) where
       ?<> (getLoc <$> _signPragmas)
       ?<> (getLoc <$> _signBuiltin)
       ?<> (getLoc <$> _signTerminating)
-      ?<> (getLocPatternAtomType <$> _signPattern)
-      ?<> getLoc _signBody
+      ?<> (getLocFunctionSymbolType _signName)
+      <> getLoc _signBody
 
 instance HasLoc (Example s) where
   getLoc e = e ^. exampleLoc
@@ -3597,13 +3629,20 @@ symbolParsed sym = case sing :: SStage s of
 
 getFunctionSymbol :: forall s. (SingI s) => FunctionSymbolType s -> SymbolType s
 getFunctionSymbol sym = case sing :: SStage s of
-  SParsed -> fromJust sym
-  SScoped -> sym
+  SParsed -> case sym of
+    FunctionDefName p -> p
+    FunctionDefNamePattern {} -> impossibleError "invalid call"
+  SScoped -> sym ^. functionDefName
+
+functionSymbolPattern :: forall s. (SingI s) => FunctionSymbolType s -> Maybe (PatternAtomType s)
+functionSymbolPattern f = case sing :: SStage s of
+  SParsed -> f ^? _FunctionDefNamePattern
+  SScoped -> f ^. functionDefNamePattern
 
 withFunctionSymbol :: forall s a. (SingI s) => a -> (SymbolType s -> a) -> FunctionSymbolType s -> a
 withFunctionSymbol a f sym = case sing :: SStage s of
-  SParsed -> maybe a f sym
-  SScoped -> f sym
+  SParsed -> maybe a f (sym ^? _FunctionDefName)
+  SScoped -> f (sym ^. functionDefName)
 
 namedArgumentNewSymbolParsed :: (SingI s) => SimpleGetter (NamedArgumentNew s) Symbol
 namedArgumentNewSymbolParsed = to $ \case
@@ -3614,8 +3653,8 @@ namedArgumentNewSymbol :: Lens' (NamedArgumentNew 'Parsed) Symbol
 namedArgumentNewSymbol f = \case
   NamedArgumentItemPun a -> NamedArgumentItemPun <$> (namedArgumentPunSymbol f a)
   NamedArgumentNewFunction a -> do
-    a' <- f (fromJust (a ^. namedArgumentFunctionDef . signName))
-    return $ NamedArgumentNewFunction (over namedArgumentFunctionDef (set signName (Just a')) a)
+    a' <- f (a ^?! namedArgumentFunctionDef . signName . _FunctionDefName)
+    return $ NamedArgumentNewFunction (over namedArgumentFunctionDef (set signName (FunctionDefName a')) a)
 
 scopedIdenSrcName :: Lens' ScopedIden S.Name
 scopedIdenSrcName f n = case n ^. scopedIdenAlias of

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -1168,7 +1168,8 @@ instance (SingI s) => PrettyPrint (FunctionLhs s) where
         coercion' = (<> if isJust instance' then space else line) . ppCode <$> _funLhsCoercion
         instance' = (<> line) . ppCode <$> _funLhsInstance
         builtin' = (<> line) . ppCode <$> _funLhsBuiltin
-        name' = case _funLhsPattern of
+        mpat :: Maybe (PatternAtomType s) = functionSymbolPattern _funLhsName
+        name' = case mpat of
           Just pat -> withFunctionSymbol id annDef _funLhsName (ppPatternAtomType pat)
           Nothing -> annDef (getFunctionSymbol _funLhsName) (ppSymbolType (getFunctionSymbol _funLhsName))
         sig' = ppCode _funLhsTypeSig

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -412,7 +412,7 @@ reserveFunctionSymbol ::
   FunctionLhs 'Parsed ->
   Sem r S.Symbol
 reserveFunctionSymbol f =
-  reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. funLhsBuiltin) (fromJust (f ^. funLhsName))
+  reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. funLhsBuiltin) (f ^?! funLhsName . _FunctionDefName)
 
 reserveAxiomSymbol ::
   (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
@@ -1118,17 +1118,24 @@ checkDeriving ::
   Sem r (Deriving 'Scoped)
 checkDeriving Deriving {..} = do
   let lhs@FunctionLhs {..} = _derivingFunLhs
-  massert (isNothing _funLhsPattern)
+  massert (isJust (_funLhsName ^? _FunctionDefName))
+  let name = case _funLhsName of
+        FunctionDefName n -> n
+        FunctionDefNamePattern {} -> impossible
   typeSig' <- withLocalScope (checkTypeSig _funLhsTypeSig)
   name' <-
     if
-        | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol (fromJust _funLhsName)
+        | P.isLhsFunctionLike lhs -> getReservedDefinitionSymbol name
         | otherwise -> reserveFunctionSymbol lhs
+  let defname' =
+        FunctionDefNameScoped
+          { _functionDefName = name',
+            _functionDefNamePattern = Nothing
+          }
   let lhs' =
         FunctionLhs
-          { _funLhsName = name',
+          { _funLhsName = defname',
             _funLhsTypeSig = typeSig',
-            _funLhsPattern = Nothing,
             ..
           }
   return
@@ -1190,33 +1197,36 @@ checkFunctionDef fdef@FunctionDef {..} = do
     a' <- checkTypeSig _signTypeSig
     b' <- checkBody
     return (a', b')
-  whenJust _signPattern $
-    reservePatternFunctionSymbols
+  whenJust (functionSymbolPattern _signName) reservePatternFunctionSymbols
   sigName' <- case _signName of
-    Just name'
-      | P.isFunctionLike fdef ->
-          getReservedDefinitionSymbol name'
-      | otherwise ->
-          reserveFunctionSymbol (functionDefLhs fdef)
-    Nothing ->
-      freshSymbol KNameFunction KNameFunction (WithLoc (getLoc (fromJust _signPattern)) "__pattern__")
-  sigPattern' <-
-    case _signPattern of
-      Just pat ->
-        fmap Just
-          . runReader PatternNamesKindFunctions
-          $ checkParsePatternAtom pat
-      Nothing -> return Nothing
+    FunctionDefName name -> do
+      name' <-
+        if
+            | P.isFunctionLike fdef -> getReservedDefinitionSymbol name
+            | otherwise -> reserveFunctionSymbol (functionDefLhs fdef)
+      return
+        FunctionDefNameScoped
+          { _functionDefName = name',
+            _functionDefNamePattern = Nothing
+          }
+    FunctionDefNamePattern p -> do
+      name' <- freshSymbol KNameFunction KNameFunction (WithLoc (getLoc p) "__pattern__")
+      p' <- runReader PatternNamesKindFunctions (checkParsePatternAtom p)
+      return
+        FunctionDefNameScoped
+          { _functionDefName = name',
+            _functionDefNamePattern = Just p'
+          }
   let def =
         FunctionDef
           { _signName = sigName',
-            _signPattern = sigPattern',
+            -- _signPattern = sigPattern',
             _signDoc = sigDoc',
             _signBody = sigBody',
             _signTypeSig = sig',
             ..
           }
-  registerNameSignature (sigName' ^. S.nameId) def
+  registerNameSignature (sigName' ^. functionDefName . S.nameId) def
   registerFunctionDef @$> def
   where
     checkBody :: Sem r (FunctionDefBody 'Scoped)

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -481,7 +481,7 @@ derivingInstance = do
   _derivingFunLhs <- functionDefinitionLhs opts Nothing
   unless (isJust (_derivingFunLhs ^. funLhsInstance)) $
     parseFailure off "Expected `deriving instance`"
-  unless (isNothing (_derivingFunLhs ^. funLhsPattern)) $
+  when (has _FunctionDefNamePattern (_derivingFunLhs ^. funLhsName)) $
     parseFailure off "Patterns not allowed for `deriving instance`"
   return Deriving {..}
 
@@ -1334,27 +1334,26 @@ functionDefinitionLhs opts _funLhsBuiltin = P.label "<function definition>" $ do
     parseFailure off0 "instance not allowed here"
   when (isJust _funLhsCoercion && isNothing _funLhsInstance) $
     parseFailure off0 "expected: instance"
-  _funLhsName <- optional $ P.try $ do
+  mname <- optional . P.try $ do
     n <- symbol
     P.notFollowedBy (kw kwAt)
     return n
-  _funLhsPattern <- case _funLhsName of
-    Nothing -> Just <$> patternAtom
-    Just {} -> return Nothing
+  _funLhsName <- case mname of
+    Nothing -> FunctionDefNamePattern <$> patternAtom
+    Just fname -> return (FunctionDefName fname)
   let sigOpts =
         SigOptions
           { _sigAllowDefault = True,
             _sigAllowOmitType = allowOmitType
           }
   _funLhsTypeSig <- typeSig sigOpts
-  when (isNothing _funLhsName && not (null (_funLhsTypeSig ^. typeSigArgs))) $
+  when (isNothing (_funLhsName ^? _FunctionDefName) && notNull (_funLhsTypeSig ^. typeSigArgs)) $
     parseFailure off "expected function name"
   return
     FunctionLhs
       { _funLhsInstance,
         _funLhsBuiltin,
         _funLhsCoercion,
-        _funLhsPattern,
         _funLhsName,
         _funLhsTypeSig,
         _funLhsTerminating
@@ -1424,7 +1423,6 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
   let fdef =
         FunctionDef
           { _signName = _funLhsName,
-            _signPattern = _funLhsPattern,
             _signTypeSig = _funLhsTypeSig,
             _signTerminating = _funLhsTerminating,
             _signInstance = _funLhsInstance,
@@ -1434,7 +1432,7 @@ functionDefinition opts _signBuiltin = P.label "<function definition>" $ do
             _signPragmas,
             _signBody
           }
-  when (isNothing _funLhsName && P.isFunctionLike fdef) $
+  when (isNothing (_funLhsName ^? _FunctionDefName) && P.isFunctionLike fdef) $
     parseFailure off0 "expected function name"
   return fdef
   where