Remove where syntax (#1674)

Closes #1640 #1354

src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs

@@ -211,21 +211,13 @@ goFunctionClause ::
 goFunctionClause FunctionClause {..} = do
   _clausePatterns' <- mapM goPatternArg _clausePatterns
   _clauseBody' <- goExpression _clauseBody
-  goWhereBlock _clauseWhere
   return
     Abstract.FunctionClause
       { _clauseName = goSymbol _clauseOwnerFunction,
         _clausePatterns = _clausePatterns',
         _clauseBody = _clauseBody'
       }
 
-goWhereBlock ::
-  Maybe (WhereBlock 'Scoped) ->
-  Sem r ()
-goWhereBlock w = case w of
-  Just _ -> unsupported "where block"
-  Nothing -> return ()
-
 goInductiveParameter ::
   Member (Error ScoperError) r =>
   InductiveParameter 'Scoped ->

src/Juvix/Compiler/Concrete/Language.hs

@@ -351,8 +351,7 @@ type FunctionName s = SymbolType s
 data FunctionClause (s :: Stage) = FunctionClause
   { _clauseOwnerFunction :: FunctionName s,
     _clausePatterns :: [PatternType s],
-    _clauseBody :: ExpressionType s,
-    _clauseWhere :: Maybe (WhereBlock s)
+    _clauseBody :: ExpressionType s
   }
 
 deriving stock instance
@@ -623,73 +622,6 @@ deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (Functi
 
 deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Function s)
 
---------------------------------------------------------------------------------
--- Where block clauses
---------------------------------------------------------------------------------
-
-newtype WhereBlock (s :: Stage) = WhereBlock
-  { whereClauses :: NonEmpty (WhereClause s)
-  }
-
-deriving stock instance
-  ( Show (PatternType s),
-    Show (IdentifierType s),
-    Show (ModuleRefType s),
-    Show (SymbolType s),
-    Show (ExpressionType s)
-  ) =>
-  Show (WhereBlock s)
-
-deriving stock instance
-  ( Eq (PatternType s),
-    Eq (IdentifierType s),
-    Eq (ModuleRefType s),
-    Eq (SymbolType s),
-    Eq (ExpressionType s)
-  ) =>
-  Eq (WhereBlock s)
-
-deriving stock instance
-  ( Ord (PatternType s),
-    Ord (IdentifierType s),
-    Ord (ModuleRefType s),
-    Ord (SymbolType s),
-    Ord (ExpressionType s)
-  ) =>
-  Ord (WhereBlock s)
-
-data WhereClause (s :: Stage)
-  = WhereOpenModule (OpenModule s)
-  | WhereTypeSig (TypeSignature s)
-  | WhereFunClause (FunctionClause s)
-
-deriving stock instance
-  ( Show (PatternType s),
-    Show (IdentifierType s),
-    Show (ModuleRefType s),
-    Show (SymbolType s),
-    Show (ExpressionType s)
-  ) =>
-  Show (WhereClause s)
-
-deriving stock instance
-  ( Eq (PatternType s),
-    Eq (IdentifierType s),
-    Eq (ModuleRefType s),
-    Eq (SymbolType s),
-    Eq (ExpressionType s)
-  ) =>
-  Eq (WhereClause s)
-
-deriving stock instance
-  ( Ord (PatternType s),
-    Ord (IdentifierType s),
-    Ord (ModuleRefType s),
-    Ord (SymbolType s),
-    Ord (ExpressionType s)
-  ) =>
-  Ord (WhereClause s)
-
 --------------------------------------------------------------------------------
 -- Lambda expression
 --------------------------------------------------------------------------------

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

@@ -493,25 +493,11 @@ instance SingI s => PrettyCode (FunctionClause s) where
       Nothing -> return Nothing
       Just ne -> Just . hsep <$> mapM ppPatternAtom ne
     clauseBody' <- ppExpression _clauseBody
-    clauseWhere' <- mapM ppCode _clauseWhere
     return $
       clauseOwnerFunction'
         <+?> clausePatterns'
         <+> kwAssign
-        <+> nest
-          2
-          ( clauseBody'
-              <+?> ((line <>) <$> clauseWhere')
-          )
-
-instance SingI s => PrettyCode (WhereBlock s) where
-  ppCode WhereBlock {..} = indent' . (kwWhere <+>) <$> ppBlock whereClauses
-
-instance SingI s => PrettyCode (WhereClause s) where
-  ppCode c = case c of
-    WhereOpenModule o -> ppCode o
-    WhereTypeSig sig -> ppCode sig
-    WhereFunClause fun -> ppCode fun
+        <+> nest 2 clauseBody'
 
 instance SingI s => PrettyCode (AxiomDef s) where
   ppCode AxiomDef {..} = do

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

@@ -796,31 +796,6 @@ checkOpenModule op
   | op ^. openModuleImport = checkOpenImportModule op
   | otherwise = checkOpenModuleNoImport op
 
-checkWhereBlock ::
-  forall r.
-  Members
-    '[ Error ScoperError,
-       State Scope,
-       State ScoperState,
-       Reader LocalVars,
-       InfoTableBuilder,
-       NameIdGen
-     ]
-    r =>
-  WhereBlock 'Parsed ->
-  Sem r (WhereBlock 'Scoped)
-checkWhereBlock WhereBlock {..} = WhereBlock <$> mapM checkWhereClause whereClauses
-
-checkWhereClause ::
-  forall r.
-  Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r =>
-  WhereClause 'Parsed ->
-  Sem r (WhereClause 'Scoped)
-checkWhereClause c = case c of
-  WhereOpenModule o -> WhereOpenModule <$> checkOpenModuleNoImport o
-  WhereTypeSig s -> WhereTypeSig <$> checkTypeSignature s
-  WhereFunClause f -> WhereFunClause <$> checkFunctionClause f
-
 checkFunctionClause ::
   forall r.
   Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r =>
@@ -829,20 +804,18 @@ checkFunctionClause ::
 checkFunctionClause clause@FunctionClause {..} = do
   clauseOwnerFunction' <- checkTypeSigInScope
   registerName (S.unqualifiedSymbol clauseOwnerFunction')
-  (clausePatterns', clauseWhere', clauseBody') <- do
+  (clausePatterns', clauseBody') <- do
     clp <- mapM checkParsePatternAtom _clausePatterns
     withBindCurrentGroup $ do
       s <- get @Scope
-      clw <- mapM checkWhereBlock _clauseWhere
       clb <- checkParseExpressionAtoms _clauseBody
       put s
-      return (clp, clw, clb)
+      return (clp, clb)
   registerFunctionClause'
     FunctionClause
       { _clauseOwnerFunction = clauseOwnerFunction',
         _clausePatterns = clausePatterns',
-        _clauseBody = clauseBody',
-        _clauseWhere = clauseWhere'
+        _clauseBody = clauseBody'
       }
   where
     fun = _clauseOwnerFunction

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

@@ -470,23 +470,6 @@ function = do
   _funReturn <- parseExpressionAtoms
   return Function {..}
 
---------------------------------------------------------------------------------
--- Where block clauses
---------------------------------------------------------------------------------
-
-whereBlock :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (WhereBlock 'Parsed)
-whereBlock = do
-  kw kwWhere
-  WhereBlock <$> braces (P.sepEndBy1 whereClause (kw kwSemicolon))
-
-whereClause :: forall r. Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (WhereClause 'Parsed)
-whereClause =
-  (WhereOpenModule <$> openModule)
-    <|> sigOrFun
-  where
-    sigOrFun :: ParsecS r (WhereClause 'Parsed)
-    sigOrFun = either WhereTypeSig WhereFunClause <$> auxTypeSigFunClause
-
 --------------------------------------------------------------------------------
 -- Lambda expression
 --------------------------------------------------------------------------------
@@ -574,7 +557,6 @@ functionClause _clauseOwnerFunction = do
   _clausePatterns <- P.many patternAtom
   kw kwAssign
   _clauseBody <- parseExpressionAtoms
-  _clauseWhere <- optional whereBlock
   return FunctionClause {..}
 
 --------------------------------------------------------------------------------

tests/positive/StdlibList/Data/List.juvix

@@ -39,12 +39,12 @@ length _ (nil _) := zero;
 length a (∷ _ _ l) := suc (length a l);
 
 reverse : (a : Type) → List a → List a;
-reverse a l := rev l (nil a)
-  where {
+reverse a l := 
+  let  {
   rev : List a → List a → List a;
   rev (nil _) a := a;
   rev (∷ _ x xs) a := rev xs (∷ a x a)
-  };
+  } in rev l (nil a);
 
 replicate : (a : Type) → ℕ → a → List a;
 replicate a zero _ := nil a;
@@ -85,16 +85,18 @@ quickSort : (a : Type) → (a → a → Ordering) → List a → List a;
 quickSort a _ (nil _) := nil a;
 quickSort a _ (∷ _ x (nil _)) := ∷ a x (nil a);
 quickSort a cmp (∷ _ x ys) :=
-  ++ a (quickSort a (filter a ltx) ys)
-  (++ a (∷ a x (nil a)) (quickSort a (filter a gex) ys))
-  where {
+  let {
     ltx : a → Bool;
     ltx y := match (cmp y x) λ{
       LT := true;
       _  := false;
     };
     gex : a → Bool;
     gex y := not (ltx y)
+  } in 
+  {
+     ++ a (quickSort a (filter a ltx) ys)
+    (++ a (∷ a x (nil a)) (quickSort a (filter a gex) ys))
   };
 
 end;