Remove old function syntax (#2305)

* Enables new function syntax in local let-declarations
* Closes #2251

Makefile

@@ -116,7 +116,7 @@ JUVIXFILESTOFORMAT=$(shell find  \
 	-type d \( -name ".juvix-build" -o -name "FancyPaths" \) -prune -o \
 	-type f -name "*.juvix" -print)
 
-JUVIXFORMATFLAGS?=--in-place --new-function-syntax
+JUVIXFORMATFLAGS?=--in-place
 JUVIXTYPECHECKFLAGS?=--only-errors
 
 .PHONY: format-juvix-files

app/Commands/Format.hs

@@ -49,9 +49,8 @@ targetFromOptions opts = do
 runCommand :: forall r. Members '[Embed IO, App, Resource, Files] r => FormatOptions -> Sem r ()
 runCommand opts = do
   target <- targetFromOptions opts
-  let newSyntax = NewSyntax (opts ^. formatNewSyntax)
   runOutputSem (renderFormattedOutput target opts) $ runScopeFileApp $ do
-    res <- runReader newSyntax $ case target of
+    res <- case target of
       TargetFile p -> format p
       TargetProject p -> formatProject p
       TargetStdin -> formatStdin

app/Commands/Format/Options.hs

@@ -5,7 +5,6 @@ import CommonOptions
 data FormatOptions = FormatOptions
   { _formatInput :: Maybe (Prepath FileOrDir),
     _formatCheck :: Bool,
-    _formatNewSyntax :: Bool,
     _formatInPlace :: Bool
   }
   deriving stock (Data)
@@ -29,11 +28,6 @@ parseFormat = do
       ( long "check"
           <> help "Do not print reformatted sources or unformatted file paths to standard output."
       )
-  _formatNewSyntax <-
-    switch
-      ( long "new-function-syntax"
-          <> help "Format the file using the new function syntax."
-      )
   _formatInPlace <-
     switch
       ( long "in-place"

examples/milestone/Bank/Bank.juvix

@@ -83,8 +83,7 @@ calculateInterest : Nat -> Nat -> Nat -> Nat
   | principal rate periods :=
     let
       amount : Nat := principal;
-      incrAmount : Nat -> Nat;
-      incrAmount a := div (a * rate) 10000;
+      incrAmount (a : Nat) : Nat := div (a * rate) 10000;
     in iterate (min 100 periods) incrAmount amount;
 
 --- Asserts some ;Bool; condition.

examples/milestone/Collatz/Collatz.juvix

@@ -3,19 +3,18 @@ module Collatz;
 import Stdlib.Prelude open;
 import Stdlib.Data.Nat.Ord open;
 
-collatzNext : Nat → Nat
-  | n := if (mod n 2 == 0) (div n 2) (3 * n + 1);
+collatzNext (n : Nat) : Nat :=
+  if (mod n 2 == 0) (div n 2) (3 * n + 1);
 
 collatz : Nat → Nat
   | zero := zero
   | (suc zero) := suc zero
   | n := collatzNext n;
 
 terminating
-run : (Nat → Nat) → Nat → IO
-  | _ (suc zero) :=
-    printNatLn 1 >> printStringLn "Finished!"
-  | f n := printNatLn n >> run f (f n);
+run (f : Nat → Nat) : Nat → IO
+  | (suc zero) := printNatLn 1 >> printStringLn "Finished!"
+  | n := printNatLn n >> run f (f n);
 
 welcome : String :=
   "Collatz calculator\n------------------\n\nType a number then ENTER";

examples/milestone/Fibonacci/Fibonacci.juvix

@@ -6,7 +6,6 @@ fib : Nat → Nat → Nat → Nat
   | zero x1 _ := x1
   | (suc n) x1 x2 := fib n x2 (x1 + x2);
 
-fibonacci : Nat → Nat
-  | n := fib n 0 1;
+fibonacci (n : Nat) : Nat := fib n 0 1;
 
 main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat);

examples/milestone/PascalsTriangle/PascalsTriangle.juvix

@@ -7,38 +7,35 @@ module PascalsTriangle;
 import Stdlib.Prelude open;
 
 --- Return a list of repeated applications of a given function
-scanIterate : {A : Type} → Nat → (A → A) → A → List A
+scanIterate {A} : Nat → (A → A) → A → List A
   | zero _ _ := nil
   | (suc n) f a := a :: scanIterate n f (f a);
 
 --- Produce a singleton List
-singleton : {A : Type} → A → List A
-  | a := a :: nil;
+singleton {A} (a : A) : List A := a :: nil;
 
 --- Concatenates a list of strings
 --- ;concat (("a" :: nil) :: "b" :: nil); evaluates to ;"a"
   :: "b"
   :: nil;
 concat : List String → String := foldl (++str) "";
 
-intercalate : String → List String → String
-  | sep xs := concat (intersperse sep xs);
+intercalate (sep : String) (xs : List String) : String :=
+  concat (intersperse sep xs);
 
-showList : List Nat → String
-  | xs :=
-    "[" ++str intercalate "," (map natToString xs) ++str "]";
+showList (xs : List Nat) : String :=
+  "[" ++str intercalate "," (map natToString xs) ++str "]";
 
 --- Compute the next row of Pascal's triangle
-pascalNextRow : List Nat → List Nat
-  | row :=
-    zipWith
-      (+)
-      (singleton zero ++ row)
-      (row ++ singleton zero);
+pascalNextRow (row : List Nat) : List Nat :=
+  zipWith
+    (+)
+    (singleton zero ++ row)
+    (row ++ singleton zero);
 
 --- Produce Pascal's triangle to a given depth
-pascal : Nat → List (List Nat)
-  | rows := scanIterate rows pascalNextRow (singleton 1);
+pascal (rows : Nat) : List (List Nat) :=
+  scanIterate rows pascalNextRow (singleton 1);
 
 main : IO :=
   printStringLn (unlines (map showList (pascal 10)));

examples/milestone/TicTacToe/CLI/TicTacToe.juvix

@@ -10,16 +10,15 @@ import Stdlib.Prelude open;
 import Logic.Game open;
 
 --- A ;String; that prompts the user for their input
-prompt : GameState → String
-  | x :=
-    "\n"
-      ++str showGameState x
-      ++str "\nPlayer "
-      ++str showSymbol (player x)
-      ++str ": ";
+prompt (x : GameState) : String :=
+  "\n"
+    ++str showGameState x
+    ++str "\nPlayer "
+    ++str showSymbol (player x)
+    ++str ": ";
 
-nextMove : GameState → String → GameState
-  | s := flip playMove s ∘ validMove ∘ stringToNat;
+nextMove (s : GameState) : String → GameState :=
+  flip playMove s ∘ validMove ∘ stringToNat;
 
 --- Main loop
 terminating

examples/milestone/TicTacToe/Logic/Board.juvix

@@ -35,8 +35,8 @@ columns : List (List Square) → List (List Square) :=
 rows : List (List Square) → List (List Square) := id;
 
 --- Textual representation of a ;List Square;
-showRow : List Square → String
-  | xs := concat (surround "|" (map showSquare xs));
+showRow (xs : List Square) : String :=
+  concat (surround "|" (map showSquare xs));
 
 showBoard : Board → String
   | (board squares) :=

examples/milestone/TicTacToe/Logic/Extra.juvix

@@ -11,9 +11,9 @@ import Stdlib.Prelude open;
 concat : List String → String := foldl (++str) "";
 
 --- It inserts the first ;String; at the beginning, in between, and at the end of the second list
-surround : String → List String → List String
-  | x xs := (x :: intersperse x xs) ++ x :: nil;
+surround (x : String) (xs : List String) : List String :=
+  (x :: intersperse x xs) ++ x :: nil;
 
 --- It inserts the first ;String; in between the ;String;s in the second list and concatenates the result
-intercalate : String → List String → String
-  | sep xs := concat (intersperse sep xs);
+intercalate (sep : String) (xs : List String) : String :=
+  concat (intersperse sep xs);

examples/milestone/TicTacToe/Logic/Game.juvix

@@ -43,5 +43,5 @@ playMove : Maybe Nat → GameState → GameState
           noError));
 
 --- Returns ;just; if the given ;Nat; is in range of 1..9
-validMove : Nat → Maybe Nat
-  | n := if (n <= 9 && n >= 1) (just n) nothing;
+validMove (n : Nat) : Maybe Nat :=
+  if (n <= 9 && n >= 1) (just n) nothing;

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -23,10 +23,10 @@ showSquare : Square → String
   | (empty n) := " " ++str natToString n ++str " "
   | (occupied s) := " " ++str showSymbol s ++str " ";
 
-replace : Symbol → Nat → Square → Square
-  | player k (empty n) :=
+replace (player : Symbol) (k : Nat) : Square → Square
+  | (empty n) :=
     if
       (n Stdlib.Data.Nat.Ord.== k)
       (occupied player)
       (empty n)
-  | _ _ s := s;
+  | s := s;

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

@@ -397,7 +397,6 @@ goJudoc (Judoc bs) = mconcatMapM goGroup bs
 
 goStatement :: (Members '[Reader HtmlOptions, Reader NormalizedTable] r) => Statement 'Scoped -> Sem r Html
 goStatement = \case
-  StatementTypeSignature t -> goTypeSignature t
   StatementAxiom t -> goAxiom t
   StatementInductive t -> goInductive t
   StatementOpenModule t -> goOpen t
@@ -483,20 +482,6 @@ defHeader tmp uid sig mjudoc = do
       sourceLink' <- sourceAndSelfLink tmp uid
       return $ noDefHeader (sig <> sourceLink')
 
-goTypeSignature :: forall r. (Members '[Reader HtmlOptions, Reader NormalizedTable] r) => TypeSignature 'Scoped -> Sem r Html
-goTypeSignature sig = do
-  sig' <- typeSig
-  defHeader tmp uid sig' (sig ^. sigDoc)
-  where
-    tmp :: TopModulePath
-    tmp = sig ^. sigName . S.nameDefinedIn . S.absTopModulePath
-    uid :: NameId
-    uid = sig ^. sigName . S.nameId
-    typeSig :: Sem r Html
-    typeSig = ppCodeHtml opts (set sigDoc Nothing sig)
-    opts :: Options
-    opts = set optPrintPragmas False defaultOptions
-
 sourceAndSelfLink :: (Members '[Reader HtmlOptions] r) => TopModulePath -> NameId -> Sem r Html
 sourceAndSelfLink tmp name = do
   ref' <- local (set htmlOptionsKind HtmlSrc) (nameIdAttrRef tmp (Just name))

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

@@ -4,15 +4,7 @@ import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Language
 import Juvix.Prelude
 
-data OldFunctionInfo = OldFunctionInfo
-  { _oldFunctionInfoType :: TypeSignature 'Scoped,
-    _oldFunctionInfoClauses :: [FunctionClause 'Scoped]
-  }
-  deriving stock (Eq, Show)
-
-data FunctionInfo
-  = FunctionInfoOld OldFunctionInfo
-  | FunctionInfoNew (FunctionDef 'Scoped)
+newtype FunctionInfo = FunctionInfo (FunctionDef 'Scoped)
   deriving stock (Eq, Show)
 
 data ConstructorInfo = ConstructorInfo
@@ -61,25 +53,13 @@ makeLenses ''InfoTable
 makeLenses ''InductiveInfo
 makeLenses ''ConstructorInfo
 makeLenses ''AxiomInfo
-makeLenses ''OldFunctionInfo
-
-_FunctionInfoOld :: Traversal' FunctionInfo OldFunctionInfo
-_FunctionInfoOld f = \case
-  FunctionInfoOld x -> FunctionInfoOld <$> f x
-  r@FunctionInfoNew {} -> pure r
 
 functionInfoDoc :: Lens' FunctionInfo (Maybe (Judoc 'Scoped))
 functionInfoDoc f = \case
-  FunctionInfoOld i -> do
-    i' <- traverseOf (oldFunctionInfoType . sigDoc) f i
-    pure (FunctionInfoOld i')
-  FunctionInfoNew i -> do
+  FunctionInfo i -> do
     i' <- traverseOf signDoc f i
-    pure (FunctionInfoNew i')
+    pure (FunctionInfo i')
 
 instance HasLoc FunctionInfo where
   getLoc = \case
-    FunctionInfoOld f ->
-      getLoc (f ^. oldFunctionInfoType)
-        <>? (getLocSpan <$> nonEmpty (f ^. oldFunctionInfoClauses))
-    FunctionInfoNew f -> getLoc f
+    FunctionInfo f -> getLoc f

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

@@ -14,9 +14,7 @@ data InfoTableBuilder m a where
   RegisterAxiom :: AxiomDef 'Scoped -> InfoTableBuilder m ()
   RegisterConstructor :: S.Symbol -> ConstructorDef 'Scoped -> InfoTableBuilder m ()
   RegisterInductive :: InductiveDef 'Scoped -> InfoTableBuilder m ()
-  RegisterTypeSignature :: TypeSignature 'Scoped -> InfoTableBuilder m ()
   RegisterFunctionDef :: FunctionDef 'Scoped -> InfoTableBuilder m ()
-  RegisterFunctionClause :: FunctionClause 'Scoped -> InfoTableBuilder m ()
   RegisterName :: HasLoc c => S.Name' c -> InfoTableBuilder m ()
   RegisterModule :: Module 'Scoped 'ModuleTop -> InfoTableBuilder m ()
   RegisterFixity :: FixityDef -> InfoTableBuilder m ()
@@ -54,27 +52,11 @@ toState = reinterpret $ \case
           registerDoc (ity ^. inductiveName . nameId) j
   RegisterFunctionDef f ->
     let ref = f ^. signName . S.nameId
-        info = FunctionInfoNew f
+        info = FunctionInfo f
         j = f ^. signDoc
      in do
           modify (set (infoFunctions . at ref) (Just info))
           registerDoc (f ^. signName . nameId) j
-  RegisterTypeSignature f ->
-    let ref = f ^. sigName . S.nameId
-        info =
-          FunctionInfoOld
-            OldFunctionInfo
-              { _oldFunctionInfoType = f,
-                _oldFunctionInfoClauses = []
-              }
-        j = f ^. sigDoc
-     in do
-          modify (set (infoFunctions . at ref) (Just info))
-          registerDoc (f ^. sigName . nameId) j
-  RegisterFunctionClause c ->
-    -- assumes the signature has already been registered
-    let key = c ^. clauseOwnerFunction . S.nameId
-     in modify (over (infoFunctions . at key . _Just . _FunctionInfoOld . oldFunctionInfoClauses) (`snoc` c))
   RegisterName n -> modify (over highlightNames (cons (S.AName n)))
   RegisterModule m -> do
     let j = m ^. moduleDoc