Merge branch 'main' into check-geb

examples/midsquare/MidSquareHash.juvix

@@ -0,0 +1,91 @@
+--- This file implements the mid-square hashing function in Juvix. See:
+--- https://research.cs.vt.edu/AVresearch/hashing/midsquare.php
+---
+--- The implementation is for hashing natural numbers with maximum 16 bits into 6
+--- bits. In order to facilitate the translation to the current version of the
+--- GEB backend, no recursion is used (it is manually unrolled).
+---
+module MidSquareHash;
+
+open import Stdlib.Prelude;
+open import Stdlib.Data.Nat.Ord;
+
+--- `powN` is 2 ^ N
+pow0 : Nat := 1;
+pow1 : Nat := 2 * pow0;
+pow2 : Nat := 2 * pow1;
+pow3 : Nat := 2 * pow2;
+pow4 : Nat := 2 * pow3;
+pow5 : Nat := 2 * pow4;
+pow6 : Nat := 2 * pow5;
+pow7 : Nat := 2 * pow6;
+pow8 : Nat := 2 * pow7;
+pow9 : Nat := 2 * pow8;
+pow10 : Nat := 2 * pow9;
+pow11 : Nat := 2 * pow10;
+pow12 : Nat := 2 * pow11;
+pow13 : Nat := 2 * pow12;
+pow14 : Nat := 2 * pow13;
+pow15 : Nat := 2 * pow14;
+pow16 : Nat := 2 * pow15;
+
+--- `hashN` hashes a number with max N bits (i.e. smaller than 2^N) into 6 bits
+--- (i.e. smaller than 64) using the mid-square algorithm.
+hash0 : Nat -> Nat;
+hash0 x := 0;
+
+hash1 : Nat -> Nat;
+hash1 x := x * x;
+
+hash2 : Nat -> Nat;
+hash2 x := x * x;
+
+hash3 : Nat -> Nat;
+hash3 x := x * x;
+
+hash4 : Nat -> Nat;
+hash4 x := if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
+
+hash5 : Nat -> Nat;
+hash5 x := if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
+
+hash6 : Nat -> Nat;
+hash6 x := if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
+
+hash7 : Nat -> Nat;
+hash7 x := if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
+
+hash8 : Nat -> Nat;
+hash8 x := if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
+
+hash9 : Nat -> Nat;
+hash9 x := if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
+
+hash10 : Nat -> Nat;
+hash10 x := if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
+
+hash11 : Nat -> Nat;
+hash11 x := if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
+
+hash12 : Nat -> Nat;
+hash12 x := if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
+
+hash13 : Nat -> Nat;
+hash13 x := if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
+
+hash14 : Nat -> Nat;
+hash14 x := if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
+
+hash15 : Nat -> Nat;
+hash15 x := if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
+
+hash16 : Nat -> Nat;
+hash16 x := if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
+
+hash : Nat -> Nat := hash16;
+
+main : Nat;
+main := hash 1367;
+-- result: 3
+
+end;

examples/midsquare/MidSquareHash.jvc

@@ -7,45 +7,45 @@
 --
 
 -- `powN` is 2 ^ N
-def pow0 : int := 1;
-def pow1 : int := 2 * pow0;
-def pow2 : int := 2 * pow1;
-def pow3 : int := 2 * pow2;
-def pow4 : int := 2 * pow3;
-def pow5 : int := 2 * pow4;
-def pow6 : int := 2 * pow5;
-def pow7 : int := 2 * pow6;
-def pow8 : int := 2 * pow7;
-def pow9 : int := 2 * pow8;
-def pow10 : int := 2 * pow9;
-def pow11 : int := 2 * pow10;
-def pow12 : int := 2 * pow11;
-def pow13 : int := 2 * pow12;
-def pow14 : int := 2 * pow13;
-def pow15 : int := 2 * pow14;
-def pow16 : int := 2 * pow15;
+def pow0 : Int := 1;
+def pow1 : Int := 2 * pow0;
+def pow2 : Int := 2 * pow1;
+def pow3 : Int := 2 * pow2;
+def pow4 : Int := 2 * pow3;
+def pow5 : Int := 2 * pow4;
+def pow6 : Int := 2 * pow5;
+def pow7 : Int := 2 * pow6;
+def pow8 : Int := 2 * pow7;
+def pow9 : Int := 2 * pow8;
+def pow10 : Int := 2 * pow9;
+def pow11 : Int := 2 * pow10;
+def pow12 : Int := 2 * pow11;
+def pow13 : Int := 2 * pow12;
+def pow14 : Int := 2 * pow13;
+def pow15 : Int := 2 * pow14;
+def pow16 : Int := 2 * pow15;
 
 -- `hashN` hashes a number with max N bits (i.e. smaller than 2^N) into 6 bits
 -- (i.e. smaller than 64) using the mid-square algorithm.
-def hash0 : int -> int := \(x : int) 0;
-def hash1 : int -> int := \(x : int) x * x;
-def hash2 : int -> int := \(x : int) x * x;
-def hash3 : int -> int := \(x : int) x * x;
-def hash4 : int -> int := \(x : int) if x < pow3 then hash3 x else ((x * x) / pow1) % pow6;
-def hash5 : int -> int := \(x : int) if x < pow4 then hash4 x else ((x * x) / pow2) % pow6;
-def hash6 : int -> int := \(x : int) if x < pow5 then hash5 x else ((x * x) / pow3) % pow6;
-def hash7 : int -> int := \(x : int) if x < pow6 then hash6 x else ((x * x) / pow4) % pow6;
-def hash8 : int -> int := \(x : int) if x < pow7 then hash7 x else ((x * x) / pow5) % pow6;
-def hash9 : int -> int := \(x : int) if x < pow8 then hash8 x else ((x * x) / pow6) % pow6;
-def hash10 : int -> int := \(x : int) if x < pow9 then hash9 x else ((x * x) / pow7) % pow6;
-def hash11 : int -> int := \(x : int) if x < pow10 then hash10 x else ((x * x) / pow8) % pow6;
-def hash12 : int -> int := \(x : int) if x < pow11 then hash11 x else ((x * x) / pow9) % pow6;
-def hash13 : int -> int := \(x : int) if x < pow12 then hash12 x else ((x * x) / pow10) % pow6;
-def hash14 : int -> int := \(x : int) if x < pow13 then hash13 x else ((x * x) / pow11) % pow6;
-def hash15 : int -> int := \(x : int) if x < pow14 then hash14 x else ((x * x) / pow12) % pow6;
-def hash16 : int -> int := \(x : int) if x < pow15 then hash15 x else ((x * x) / pow13) % pow6;
+def hash0 : Int -> Int := \(x : Int) 0;
+def hash1 : Int -> Int := \(x : Int) x * x;
+def hash2 : Int -> Int := \(x : Int) x * x;
+def hash3 : Int -> Int := \(x : Int) x * x;
+def hash4 : Int -> Int := \(x : Int) if x < pow3 then hash3 x else ((x * x) / pow1) % pow6;
+def hash5 : Int -> Int := \(x : Int) if x < pow4 then hash4 x else ((x * x) / pow2) % pow6;
+def hash6 : Int -> Int := \(x : Int) if x < pow5 then hash5 x else ((x * x) / pow3) % pow6;
+def hash7 : Int -> Int := \(x : Int) if x < pow6 then hash6 x else ((x * x) / pow4) % pow6;
+def hash8 : Int -> Int := \(x : Int) if x < pow7 then hash7 x else ((x * x) / pow5) % pow6;
+def hash9 : Int -> Int := \(x : Int) if x < pow8 then hash8 x else ((x * x) / pow6) % pow6;
+def hash10 : Int -> Int := \(x : Int) if x < pow9 then hash9 x else ((x * x) / pow7) % pow6;
+def hash11 : Int -> Int := \(x : Int) if x < pow10 then hash10 x else ((x * x) / pow8) % pow6;
+def hash12 : Int -> Int := \(x : Int) if x < pow11 then hash11 x else ((x * x) / pow9) % pow6;
+def hash13 : Int -> Int := \(x : Int) if x < pow12 then hash12 x else ((x * x) / pow10) % pow6;
+def hash14 : Int -> Int := \(x : Int) if x < pow13 then hash13 x else ((x * x) / pow11) % pow6;
+def hash15 : Int -> Int := \(x : Int) if x < pow14 then hash14 x else ((x * x) / pow12) % pow6;
+def hash16 : Int -> Int := \(x : Int) if x < pow15 then hash15 x else ((x * x) / pow13) % pow6;
 
-def hash : int -> int := hash16;
+def hash : Int -> Int := hash16;
 
 hash 1367
 -- result: 3

src/Juvix/Compiler/Concrete/Language.hs

@@ -102,6 +102,11 @@ type family ModulePathType s t = res | res -> t s where
   ModulePathType 'Parsed 'ModuleLocal = Symbol
   ModulePathType 'Scoped 'ModuleLocal = S.Symbol
 
+type ModuleEndType :: ModuleIsTop -> GHC.Type
+type family ModuleEndType t = res | res -> t where
+  ModuleEndType 'ModuleTop = ()
+  ModuleEndType 'ModuleLocal = KeywordRef
+
 --------------------------------------------------------------------------------
 -- Top level statement
 --------------------------------------------------------------------------------
@@ -396,7 +401,8 @@ data Module (s :: Stage) (t :: ModuleIsTop) = Module
   { _moduleKw :: KeywordRef,
     _modulePath :: ModulePathType s t,
     _moduleDoc :: Maybe (Judoc s),
-    _moduleBody :: [Statement s]
+    _moduleBody :: [Statement s],
+    _moduleKwEnd :: ModuleEndType t
   }
 
 deriving stock instance
@@ -407,6 +413,7 @@ deriving stock instance
     Show (IdentifierType s),
     Show (ModuleRefType s),
     Show (SymbolType s),
+    Show (ModuleEndType t),
     Show (ExpressionType s)
   ) =>
   Show (Module s t)
@@ -419,6 +426,7 @@ deriving stock instance
     Eq (IdentifierType s),
     Eq (ModuleRefType s),
     Eq (SymbolType s),
+    Eq (ModuleEndType t),
     Eq (ExpressionType s)
   ) =>
   Eq (Module s t)
@@ -431,6 +439,7 @@ deriving stock instance
     Ord (IdentifierType s),
     Ord (ModuleRefType s),
     Ord (SymbolType s),
+    Ord (ModuleEndType t),
     Ord (ExpressionType s)
   ) =>
   Ord (Module s t)

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

@@ -168,8 +168,9 @@ ppInductiveParameters ps
   | otherwise = Just <$> ppCode ps
 
 instance (SingI s, SingI t) => PrettyCode (Module s t) where
+  ppCode :: (Members '[Reader Options] r) => Module s t -> Sem r (Doc Ann)
   ppCode Module {..} = do
-    moduleBody' <- indent' <$> ppCode _moduleBody
+    moduleBody' <- localIndent <$> ppCode _moduleBody
     modulePath' <- ppModulePathType _modulePath
     moduleDoc' <- mapM ppCode _moduleDoc
     return $
@@ -178,14 +179,24 @@ instance (SingI s, SingI t) => PrettyCode (Module s t) where
         <+> modulePath'
           <> kwSemicolon
           <> line
+          <> topSpace
           <> moduleBody'
-          <> line
-          <> kwEnd
-          <>? lastSemicolon
+          <>? ending
     where
-      lastSemicolon = case sing :: SModuleIsTop t of
-        SModuleLocal -> Nothing
-        SModuleTop -> Just (kwSemicolon <> line)
+      topSpace :: Doc Ann
+      topSpace = case sing :: SModuleIsTop t of
+        SModuleLocal -> mempty
+        SModuleTop -> line
+
+      localIndent :: Doc Ann -> Doc Ann
+      localIndent = case sing :: SModuleIsTop t of
+        SModuleLocal -> indent'
+        SModuleTop -> id
+
+      ending :: Maybe (Doc Ann)
+      ending = case sing :: SModuleIsTop t of
+        SModuleLocal -> Just (line <> kwEnd)
+        SModuleTop -> Nothing
 
 instance PrettyCode Precedence where
   ppCode p = return $ case p of

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

@@ -59,23 +59,33 @@ ppModulePathType x = case sing :: SStage s of
 instance SingI t => PrettyPrint (Module 'Scoped t) where
   ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => Module 'Scoped t -> Sem r ()
   ppCode Module {..} = do
-    let moduleBody' = indent (ppCode _moduleBody)
+    let moduleBody' = localIndent (ppCode _moduleBody)
         modulePath' = ppModulePathType _modulePath
         moduleDoc' :: Sem r () = maybe (return ()) ppCode _moduleDoc
     moduleDoc'
       <> ppCode _moduleKw
       <+> modulePath'
         <> ppCode kwSemicolon
         <> line
+        <> topSpace
         <> moduleBody'
         <> line
-        <> ppCode kwEnd
-        <> lastSemicolon
+        <> ending
     where
-      lastSemicolon :: Sem r ()
-      lastSemicolon = case sing :: SModuleIsTop t of
-        SModuleLocal -> return ()
-        SModuleTop -> semicolon <> line <> end
+      topSpace :: Sem r ()
+      topSpace = case sing :: SModuleIsTop t of
+        SModuleLocal -> mempty
+        SModuleTop -> line
+
+      localIndent :: Sem r () -> Sem r ()
+      localIndent = case sing :: SModuleIsTop t of
+        SModuleLocal -> indent
+        SModuleTop -> id
+
+      ending :: Sem r ()
+      ending = case sing :: SModuleIsTop t of
+        SModuleLocal -> ppCode _moduleKwEnd
+        SModuleTop -> end
 
 instance PrettyPrint [Statement 'Scoped] where
   ppCode :: forall r. Members '[ExactPrint, Reader Options] r => [Statement 'Scoped] -> Sem r ()

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

@@ -532,9 +532,9 @@ checkTopModule ::
   (Members '[Error ScoperError, Reader ScopeParameters, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
   Module 'Parsed 'ModuleTop ->
   Sem r (ModuleRef'' 'S.NotConcrete 'ModuleTop)
-checkTopModule m@(Module _moduleKw path doc body) = do
+checkTopModule m@Module {..} = do
   r <- checkedModule
-  modify (over (scoperModulesCache . cachedModules) (HashMap.insert path r))
+  modify (over (scoperModulesCache . cachedModules) (HashMap.insert _modulePath r))
   registerModule (r ^. moduleRefModule)
   return r
   where
@@ -544,16 +544,16 @@ checkTopModule m@(Module _moduleKw path doc body) = do
       Sem s S.TopModulePath
     freshTopModulePath = do
       _nameId <- freshNameId
-      let _nameDefinedIn = S.topModulePathToAbsPath path
-          _nameConcrete = path
-          _nameDefined = getLoc (path ^. modulePathName)
+      let _nameDefinedIn = S.topModulePathToAbsPath _modulePath
+          _nameConcrete = _modulePath
+          _nameDefined = getLoc (_modulePath ^. modulePathName)
           _nameKind = S.KNameTopModule
           _nameFixity :: Maybe Fixity
           _nameFixity = Nothing
           -- This visibility annotation is not relevant
           _nameVisibilityAnn = VisPublic
           _nameWhyInScope = S.BecauseDefined
-          _nameVerbatim = N.topModulePathToDottedPath path
+          _nameVerbatim = N.topModulePathToDottedPath _modulePath
           moduleName = S.Name' {..}
       return moduleName
 
@@ -565,14 +565,15 @@ checkTopModule m@(Module _moduleKw path doc body) = do
       (s, (m', p)) <- runState iniScope $ do
         path' <- freshTopModulePath
         withTopScope $ do
-          (_moduleExportInfo, body') <- topBindings (checkModuleBody body)
-          doc' <- mapM checkJudoc doc
+          (_moduleExportInfo, body') <- topBindings (checkModuleBody _moduleBody)
+          doc' <- mapM checkJudoc _moduleDoc
           let _moduleRefModule =
                 Module
                   { _modulePath = path',
                     _moduleBody = body',
                     _moduleDoc = doc',
-                    _moduleKw
+                    _moduleKw,
+                    _moduleKwEnd
                   }
               _moduleRefName = S.unConcrete path'
           return (ModuleRef'' {..}, path')
@@ -632,7 +633,8 @@ checkLocalModule Module {..} = do
           { _modulePath = _modulePath',
             _moduleBody = moduleBody',
             _moduleDoc = moduleDoc',
-            _moduleKw
+            _moduleKw,
+            _moduleKwEnd
           }
       entry :: ModuleRef' 'S.NotConcrete
       entry = mkModuleRef' @'ModuleLocal ModuleRef'' {..}

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

@@ -614,16 +614,21 @@ pmodulePath = case sing :: SModuleIsTop t of
   SModuleTop -> topModulePath
   SModuleLocal -> symbol
 
-moduleDef :: (SingI t, Members '[Error ParserError, Files, PathResolver, InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (Module 'Parsed t)
+moduleDef :: forall t r. (SingI t, Members '[Error ParserError, Files, PathResolver, InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (Module 'Parsed t)
 moduleDef = P.label "<module definition>" $ do
   _moduleKw <- kw kwModule
   _moduleDoc <- getJudoc
   _modulePath <- pmodulePath
   _moduleParameters <- many inductiveParams
   kw kwSemicolon
   _moduleBody <- P.sepEndBy statement (kw kwSemicolon)
-  kw kwEnd
+  _moduleKwEnd <- endModule
   return Module {..}
+  where
+    endModule :: ParsecS r (ModuleEndType t)
+    endModule = case sing :: SModuleIsTop t of
+      SModuleLocal -> kw kwEnd
+      SModuleTop -> void (optional (kw kwEnd >> kw kwSemicolon))
 
 -- | An ExpressionAtom which is a valid expression on its own.
 atomicExpression :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (ExpressionAtoms 'Parsed)

src/Juvix/Compiler/Core/Extra/Base.hs

@@ -68,6 +68,9 @@ mkLet i bi v b = NLet (Let i (LetItem bi v) b)
 mkLet' :: Type -> Node -> Node -> Node
 mkLet' ty = mkLet Info.empty (mkBinder' ty)
 
+mkLets' :: [(Type, Node)] -> Node -> Node
+mkLets' tvs n = foldl' (\n' (ty, v) -> mkLet' ty v n') n (reverse tvs)
+
 mkLetRec :: Info -> NonEmpty LetItem -> Node -> Node
 mkLetRec i vs b = NRec (LetRec i vs b)