Fixed print rare occurrences; Added missing reserved idris2 operator

buzden · Oct 28, 2024 · be10da9 · be10da9
1 parent 851ae3f
commit be10da9
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 9 deletions.
diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr
@@ -20,7 +20,7 @@ import System.Random.Pure.StdGen
 
 NamesRestrictions where
   reservedKeywords = fromList [
-    "**", ",", "->", ".", "..", ".[|", ":", "; _", ";", "<-", "=", "=>", "%", "=", "===", "!", "&",
+    "**", ",", "->", ".", "..", ".[|", ":", "; _", ";", "<-", "=", "=>", "%", "=", "===", "!", "&", "|",
     "@", "[|", "\\", "_", "{", "|]", "}", "$=", "as", "auto", "case", "covering", "data", "default", "Delay",
     "do", "else", "export", "forall", "Force", "if", "import", "impossible", "in", "infix", "infixl", "infixr",
     "let", "module", "namespace", "of", "partial", "prefix", "private", "proof", "public", "record", "rewrite",
@@ -132,14 +132,14 @@ printStmts : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} ->
 printStmts fl $ NewV ty Immutable initial cont = do
   (nm ** _) <- genNewName fl alphaNames _ _ names
   rest <- printStmts @{NewVar nm} fl cont
-  let lhs = "let" <++> line nm <++> "="
+  let lhs = "let" <++> line nm <++> ":" <++> printTy ty <++> "="
   rhs <- printExpr initial
-  pure $ flip vappend rest $ hangSep' 2 lhs rhs
+  pure $ flip vappend rest $ hangSep' 4 lhs rhs
 
 printStmts fl $ NewV ty Mutable initial cont = do
   (nm ** _) <- genNewName fl alphaNames _ _ names
   rest <- printStmts @{NewVar nm} fl cont
-  let lhs = line nm <++> "<-"
+  let lhs = line nm <++> ":" <++> "IORef" <++> printTy ty <++> "<-"
   rhs <- printExpr initial
   pure $ flip vappend rest $ hangSep' 2 lhs $ "newIORef" <++> rhs
 

diff --git a/examples/pil-fun/src/Runner.idr b/examples/pil-fun/src/Runner.idr
@@ -119,6 +119,7 @@ run conf ctxt pp = do
 
 scala3StdFuns : NamedCtxt Scala3
 scala3StdFuns = do
+  AddFun False False "Console.println" $ [< Int'] ==> Nothing
   AddFun True  True "+"                $ [< Int', Int'] ==> Just Int'
   AddFun True  True "*"                $ [< Int', Int'] ==> Just Int'
   AddFun False True "-"                $ [< Int'] ==> Just Int'
@@ -128,11 +129,11 @@ scala3StdFuns = do
   AddFun True  True "||"               $ [< Bool', Bool'] ==> Just Bool'
   AddFun True  True "&&"               $ [< Bool', Bool'] ==> Just Bool'
   AddFun False True "!"                $ [< Bool'] ==> Just Bool'
-  AddFun False False "Console.println" $ [< Int'] ==> Nothing
   Enough
 
 lua5_4StdFuns : NamedCtxt Lua5_4
 lua5_4StdFuns = do
+  AddFun False False "print" $ [< Int'] ==> Nothing
   AddFun True  True  "+"     $ [< Int', Int'] ==> Just Int'
   AddFun True  True  "*"     $ [< Int', Int'] ==> Just Int'
   AddFun False True  "-"     $ [< Int'] ==> Just Int'
@@ -142,21 +143,20 @@ lua5_4StdFuns = do
   AddFun True  True  "or"    $ [< Bool', Bool'] ==> Just Bool'
   AddFun True  True  "and"   $ [< Bool', Bool'] ==> Just Bool'
   AddFun False True  "not"   $ [< Bool'] ==> Just Bool'
-  AddFun False False "print" $ [< Int'] ==> Nothing
   Enough
 
 idris2StdFuns : NamedCtxt Idris2
 idris2StdFuns = do
+  AddFun False False "printLn" ([< Int'] ==> Nothing)
   AddFun True  True  "+"       ([< Int', Int'] ==> Just Int')    {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Int' ** Refl) True)}
   AddFun True  True  "*"       ([< Int', Int'] ==> Just Int')    {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Int' ** Refl) True)}
-  AddFun False True  "-"       ([< Int'] ==> Just Int')          
+  AddFun True  True  "-"       ([< Int', Int'] ==> Just Int')    {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Int' ** Refl) True)}      
   AddFun True  True  "<"       ([< Int', Int'] ==> Just Bool')   {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Bool' ** Refl) True)}
   AddFun True  True  "<="      ([< Int', Int'] ==> Just Bool')   {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Bool' ** Refl) True)}
   AddFun True  True  "=="      ([< Int', Int'] ==> Just Bool')   {lCond = Idris2Cond (IsInfix (Int' ** Int' ** Just Bool' ** Refl) True)}
   AddFun True  True  "||"      ([< Bool', Bool'] ==> Just Bool') {lCond = Idris2Cond (IsInfix (Bool' ** Bool' ** Just Bool' ** Refl) True)}
   AddFun True  True  "&&"      ([< Bool', Bool'] ==> Just Bool') {lCond = Idris2Cond (IsInfix (Bool' ** Bool' ** Just Bool' ** Refl) True)}
-  AddFun False True  "not"     ([< Bool'] ==> Just Bool')        
-  AddFun False False "printLn" ([< Int'] ==> Nothing)            
+  AddFun False True  "not"     ([< Bool'] ==> Just Bool')                    
   Enough
 
 supportedLanguages : SortedMap String (l : SupportedLanguage ** (NamedCtxt l, PP l))