From e6316bc2072382ed66e1a8f3d6f2245fefe06594 Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Thu, 22 Aug 2024 19:07:23 +0300 Subject: [PATCH 01/12] Basic support for Idris2 pretty printer added --- examples/pil-fun/src/Language/PilFun.idr | 5 + .../pil-fun/src/Language/PilFun/Pretty.idr | 88 +++++++----- .../src/Language/PilFun/Pretty/DSL.idr | 19 +-- .../src/Language/PilFun/Pretty/Idris2.idr | 127 ++++++++++++++++++ .../src/Language/PilFun/Pretty/Scala3.idr | 18 +-- 5 files changed, 210 insertions(+), 47 deletions(-) create mode 100644 examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr diff --git a/examples/pil-fun/src/Language/PilFun.idr b/examples/pil-fun/src/Language/PilFun.idr index 46e670b63..bbdab8030 100644 --- a/examples/pil-fun/src/Language/PilFun.idr +++ b/examples/pil-fun/src/Language/PilFun.idr @@ -53,6 +53,11 @@ namespace SnocListTy Lin : SnocListTy (:<) : SnocListTy -> Ty -> SnocListTy + public export + snocListTyToList : SnocListTy -> List Ty + snocListTyToList Lin = [] + snocListTyToList (xs :< x) = (snocListTyToList xs) ++ [x] + public export length : SnocListTy -> Nat length Lin = Z diff --git a/examples/pil-fun/src/Language/PilFun/Pretty.idr b/examples/pil-fun/src/Language/PilFun/Pretty.idr index 98d4bdaab..9365336cc 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty.idr @@ -19,56 +19,84 @@ import System.Random.Pure.StdGen %default total public export -data UniqNames : Funs -> Vars -> Type +data SupportedLanguages = Scala3 + | Idris2 + +public export +ConditionType : Type +ConditionType = FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type + +public export +data ScalaCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type + where + IsNotInfix : ScalaCondition funSig False b + MoreThanOneArg : So (funSig.From.length >= 1) -> ScalaCondition funSig isInfix b + +public export +data IdrisCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type + where + Trivial : IdrisCondition funSig isInfix isPure + +public export +data LanguageToCondition : (l : SupportedLanguages) -> FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type + where + [search l] + Scala3Cond : ScalaCondition funSig isInfix isPure -> LanguageToCondition Scala3 funSig isInfix isPure + Idris2Cond : IdrisCondition funSig isInfix isPure -> LanguageToCondition Idris2 funSig isInfix isPure + +public export +data UniqNames : (l : SupportedLanguages) -> (funs : Funs) -> (vars : Vars) -> Type public export -data NameIsNew : UniqNames funs vars -> String -> Type - -data UniqNames : Funs -> Vars -> Type where - Empty : UniqNames [<] [<] - JustNew : (ss : UniqNames funs vars) => (s : String) -> (0 _ : NameIsNew ss s) => UniqNames funs vars - NewFun : (ss : UniqNames funs vars) => (s : String) -> (0 _ : NameIsNew ss s) => - {default False isInfix : Bool} -> (0 infixCond : So $ not isInfix || fun.From.length >= 1) => - UniqNames (funs: (s : String) -> (0 _ : NameIsNew ss s) => UniqNames funs ((:<) vars var mut) - -data NameIsNew : UniqNames funs vars -> String -> Type where - E : NameIsNew {funs=[<]} {vars=[<]} Empty x - J : (0 _ : So $ x /= s) -> NameIsNew {funs} {vars} ss x -> NameIsNew {funs} {vars} (JustNew @{ss} s @{sub}) x - F : (0 _ : So $ x /= s) -> NameIsNew {funs} {vars} ss x -> NameIsNew {funs=funs: NameIsNew {funs} {vars} ss x -> NameIsNew {funs} {vars=(:<) vars var mut} (NewVar @{ss} s @{sub}) x +data NameIsNew : (l : SupportedLanguages) -> (funs : Funs) -> (vars : Vars) -> UniqNames l funs vars -> String -> Type + +data UniqNames : (l : SupportedLanguages) -> (funs : Funs) -> (vars : Vars) -> Type where + [search funs vars] + Empty : UniqNames l [<] [<] + JustNew : (ss : UniqNames l funs vars) => (s : String) -> (0 _ : NameIsNew l funs vars ss s) => UniqNames l funs vars + NewFun : (ss : UniqNames l funs vars) => (s : String) -> (0 _ : NameIsNew l funs vars ss s) => + {default False isInfix : Bool} -> {default False isPure : Bool} -> + (0 languageCondition : LanguageToCondition l fun isInfix isPure) => + UniqNames l (funs: (s : String) -> (0 _ : NameIsNew l funs vars ss s) => UniqNames l funs ((:<) vars var mut) + +data NameIsNew : (l : SupportedLanguages) -> (funs : Funs) -> (vars : Vars) -> UniqNames l funs vars -> String -> Type where + E : NameIsNew l [<] [<] Empty x + J : (0 _ : So $ x /= s) -> NameIsNew l funs vars ss x -> NameIsNew l funs vars (JustNew @{ss} s @{sub}) x + F : (0 _ : So $ x /= s) -> NameIsNew l funs vars ss x -> NameIsNew l (funs: NameIsNew l funs vars ss x -> NameIsNew l funs ((:<) vars var mut) (NewVar @{ss} s @{sub}) x public export interface NamesRestrictions where reservedKeywords : SortedSet String -rawNewName : Fuel -> (Fuel -> Gen MaybeEmpty String) => - (vars : Vars) -> (funs : Funs) -> (names : UniqNames funs vars) -> - Gen MaybeEmpty (s ** NameIsNew names s) +rawNewName : Fuel -> (l : SupportedLanguages) -> (Fuel -> Gen MaybeEmpty String) => + (funs : Funs) -> (vars : Vars) -> (names : UniqNames l funs vars) -> + Gen MaybeEmpty (s ** NameIsNew l funs vars names s) export -genNewName : Fuel -> (Fuel -> Gen MaybeEmpty String) => +genNewName : {l : SupportedLanguages} -> Fuel -> (Fuel -> Gen MaybeEmpty String) => NamesRestrictions => - (funs : Funs) -> (vars : Vars) -> (names : UniqNames funs vars) -> - Gen MaybeEmpty (s ** NameIsNew names s) + (funs : Funs) -> (vars : Vars) -> (names : UniqNames l funs vars) -> + Gen MaybeEmpty (s ** NameIsNew l funs vars names s) genNewName fl @{genStr} funs vars names = do - nn@(nm ** _) <- rawNewName fl @{genStr} vars funs names + nn@(nm ** _) <- rawNewName fl l @{genStr} funs vars names if reservedKeywords `contains'` nm then assert_total $ genNewName fl @{genStr} funs vars names -- we could reduce fuel instead of `assert_total` else pure nn -varName : UniqNames funs vars => IndexIn vars -> String +varName : UniqNames l funs vars => IndexIn vars -> String varName @{JustNew @{ss} _} i = varName @{ss} i varName @{NewFun @{ss} _} i = varName @{ss} i varName @{NewVar s} Here = s varName @{NewVar @{ss} _} (There i) = varName @{ss} i -funName : UniqNames funs vars => IndexIn funs -> String +funName : UniqNames l funs vars => IndexIn funs -> String funName @{JustNew @{ss} _} i = funName @{ss} i funName @{NewFun s} Here = s funName @{NewFun @{ss} _} (There i) = funName @{ss} i funName @{NewVar @{ss} _} i = funName @{ss} i -isFunInfix : UniqNames funs vars => IndexIn funs -> Bool +isFunInfix : UniqNames l funs vars => IndexIn funs -> Bool isFunInfix @{JustNew @{ss} _} i = isFunInfix @{ss} i isFunInfix @{NewFun {isInfix} _} Here = isInfix isFunInfix @{NewFun @{ss} s} (There i) = isFunInfix @{ss} i @@ -77,14 +105,14 @@ isFunInfix @{NewVar @{ss} s} i = isFunInfix @{ss} i -- Returned vect has a reverse order; I'd like some `SnocVect` here. newVars : (newNames : Gen0 String) => NamesRestrictions => - {funs : _} -> {vars : _} -> + {l : _} -> {funs : _} -> {vars : _} -> Fuel -> - (extraVars : _) -> UniqNames funs vars -> - Gen0 (UniqNames funs (vars ++ extraVars), Vect extraVars.length (String, Ty)) + (extraVars : _) -> UniqNames l funs vars -> + Gen0 (UniqNames l funs (vars ++ extraVars), Vect extraVars.length (String, Ty)) newVars _ [<] names = pure (names, []) newVars fl (vs: Bool diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr b/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr index 29f98f207..8265eb30f 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr @@ -9,22 +9,25 @@ import public Language.PilFun.Pretty public export record NamedCtxt where constructor MkNamedCtxt + language : SupportedLanguages functions : Funs variables : Vars - fvNames : UniqNames functions variables + fvNames : UniqNames language functions variables public export %inline -AddFun : (isInfix : Bool) -> (s : String) -> (fun : FunSig) -> - (0 _ : So $ not isInfix || fun.From.length >= 1) => +AddFun : (isInfix : Bool) -> (isPure : Bool) -> (s : String) -> (fun : FunSig) -> (ctx : NamedCtxt) -> - (0 _ : NameIsNew ctx.fvNames s) => + (0 _ : LanguageToCondition ctx.language fun isInfix isPure) => + (0 _ : NameIsNew ctx.language ctx.functions ctx.variables ctx.fvNames s) => NamedCtxt -AddFun isInfix s fun $ MkNamedCtxt funs vars names = MkNamedCtxt (funs:>) : {0 arg : NamedCtxt -> Type} -> ((ctx : NamedCtxt) -> (0 _ : arg ctx) => NamedCtxt) -> (ctx : NamedCtxt) -> (0 _ : arg ctx) => NamedCtxt +(>>) : {0 arg : NamedCtxt -> Type} -> {0 arg' : NamedCtxt -> Type} -> + ((ctx : NamedCtxt) -> (0 _ : arg ctx) => (0 _ : arg' ctx) => NamedCtxt) -> + (ctx : NamedCtxt) -> (0 _ : arg ctx) => (0 _ : arg' ctx) => NamedCtxt (>>) f x = f x public export %inline -Enough : NamedCtxt -Enough = MkNamedCtxt [<] [<] Empty +Enough : SupportedLanguages -> NamedCtxt +Enough l = MkNamedCtxt l [<] [<] Empty diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr new file mode 100644 index 000000000..ce3b3215d --- /dev/null +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr @@ -0,0 +1,127 @@ +module Language.PilFun.Pretty.Idris2 + +import Data.Alternative +import Data.Fuel +import Data.SnocList +import public Data.So +import Data.Vect + +import public Language.PilFun +import public Language.PilFun.Pretty + +import Test.DepTyCheck.Gen + +import public Text.PrettyPrint.Bernardy + +import System.Random.Pure.StdGen + +%default total + +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", + "then", "total", "where", "with", "main", "IO", "Int", "Bool"] + +printTy : Ty -> Doc opts +printTy Int' = "Int" +printTy Bool' = "Bool" + +printMaybeTy : MaybeTy -> Doc opts +printMaybeTy Nothing = "()" +printMaybeTy $ Just ty = printTy ty + +printExpr : {funs : _} -> {vars : _} -> {opts : _} -> + (names : UniqNames Idris2 funs vars) => + Expr funs vars ty -> Gen0 $ Doc opts + +printFunCall : {funs : _} -> {vars : _} -> {opts : _} -> + (names : UniqNames Idris2 funs vars) => + IndexIn funs -> ExprsSnocList funs vars argTys -> Gen0 $ Doc opts + +printFunCall n args = do + let f_name = funName {vars} n + let f_doc : Doc opts = line f_name + let ars = toList $ getExprs args + let preparedArgs : List (Exists (Expr funs vars)) -> Gen0 $ Doc opts = + \as => map hsep $ for as $ \(Evidence _ e) => (printExpr e >>= \x => pure $ parenthesise True x) + pure $ parenthesise True $ hangSep' 2 f_doc !(preparedArgs ars) + +printExpr $ C $ I k = pure $ line $ show k +printExpr $ C $ B False = pure "False" +printExpr $ C $ B True = pure "True" +printExpr $ V n = case index vars n of + (_, Mutable) => pure $ "!" <+> (parenthesise True $ "readIORef" <++> line (varName {funs} n)) + (_, Immutable) => pure $ line $ varName {funs} n +printExpr $ F n args = assert_total printFunCall n args + +printStmts : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> + (names : UniqNames Idris2 funs vars) => + (newNames : Gen0 String) => + Fuel -> + Stmts funs vars retTy -> Gen0 $ Doc opts + +printStmts fl $ NewV ty Immutable initial cont = do + (nm ** _) <- genNewName fl _ _ names + rest <- printStmts @{NewVar nm} fl cont + let lhs = "let" <++> line nm <++> "=" + rhs <- printExpr initial + pure $ flip vappend rest $ hangSep' 2 lhs rhs + +printStmts fl $ NewV ty Mutable initial cont = do + (nm ** _) <- genNewName fl _ _ names + rest <- printStmts @{NewVar nm} fl cont + let lhs = line nm <++> "<-" + rhs <- printExpr initial + pure $ flip vappend rest $ hangSep' 2 lhs $ "newIORef" <++> rhs + +printStmts fl $ NewF (typesFrom ==> maybeRet) body cont = do + (nm ** _) <- genNewName fl _ _ names + rest <- printStmts @{NewFun nm} fl cont + let processedInputTypes = hsep $ (snocListTyToList typesFrom) <&> (\ty => printTy ty <++> "->") + let processedOutputType = "IO" <++> printMaybeTy maybeRet + let idrisTypeSignature = processedInputTypes <++> processedOutputType + (namesInside, funArgs) <- newVars fl _ names + let prerparedArgs = hsep $ toList funArgs <&> \(n, t) => line n + body <- printStmts @{namesInside} fl body <&> indent' 6 + pure $ flip vappend rest $ vsep + [ "let" <++> line nm <++> ":" <++> idrisTypeSignature, + indent 4 $ line nm <++> prerparedArgs <++> "=" <++> "do", + body ] + +printStmts fl $ (#=) n v cont = do + v_doc <- printExpr v + rest <- printStmts fl cont + pure $ flip vappend rest $ line "writeIORef" <++> line (varName {funs} n) <++> v_doc + +printStmts fl $ If cond th el cont = do + rest <- printStmts fl cont + condExprDoc <- printExpr cond + thenDoc <- printStmts fl th + elseDoc <- printStmts fl el + pure $ flip vappend rest $ vsep ["if" <++> condExprDoc <++> "then do", indent' 4 thenDoc, indent 2 "else do", indent' 6 elseDoc] + +printStmts fl $ Call n args cont = do + rest <- printStmts fl cont + pure $ flip vappend rest $ !(printFunCall n args) + +printStmts fl $ Ret expr = do + exprDoc <- printExpr expr + pure $ "pure" <++> exprDoc + +printStmts fl $ Nop = pure "pure ()" + +export +printIdris2 : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> + (names : UniqNames Idris2 funs vars) => + (newNames : Gen0 String) => + Fuel -> + Stmts funs vars retTy -> Gen0 $ Doc opts +printIdris2 fl stmts = do + pure $ vsep ["module Main", + "", + "main : IO ()", + "main = do", + indent' 2 $ !(printStmts fl stmts)] diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr index b61fec4dc..e7967e7e5 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr @@ -44,10 +44,10 @@ NamesRestrictions where ] printExpr : {funs : _} -> {vars : _} -> {opts : _} -> - (names : UniqNames funs vars) => + (names : UniqNames Scala3 funs vars) => Prec -> Expr funs vars ty -> Gen0 $ Doc opts printFunCall : {funs : _} -> {vars : _} -> {opts : _} -> - (names : UniqNames funs vars) => + (names : UniqNames Scala3 funs vars) => Prec -> IndexIn funs -> ExprsSnocList funs vars argTys -> Gen0 $ Doc opts printFunCall p n args = do @@ -70,14 +70,14 @@ printExpr p $ V n = pure $ line $ varName {funs} n printExpr p $ F n args = assert_total printFunCall p n args printStmts : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> - (names : UniqNames funs vars) => + (names : UniqNames Scala3 funs vars) => (newNames : Gen0 String) => Fuel -> (toplevel : Bool) -> Stmts funs vars retTy -> Gen0 $ Doc opts wrapMain : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> - (names : UniqNames funs vars) => + (names : UniqNames Scala3 funs vars) => (newNames : Gen0 String) => (0 _ : IfUnsolved retTy Nothing) => Fuel -> @@ -100,7 +100,7 @@ wrapMain fl True cont body = do ] printSubStmts : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> - (names : UniqNames funs vars) => + (names : UniqNames Scala3 funs vars) => (newNames : Gen0 String) => Fuel -> (noEmpty : Bool) -> @@ -122,10 +122,10 @@ printStmts fl tl $ NewV ty mut initial cont = do printStmts fl tl $ NewF sig body cont = do (nm ** _) <- genNewName fl _ _ names isInfix <- chooseAny - let (isInfix ** infixCond) : (b ** So (not b || sig.From.length >= 1)) = case decSo _ of - Yes condMet => (isInfix ** condMet) - No _ => (False ** Oh) - rest <- printStmts @{NewFun {isInfix} {infixCond} nm} fl tl cont + let (isInfix ** infixCond) : (b ** ScalaCondition sig b _) = case decSo _ of + Yes condMet => (isInfix ** MoreThanOneArg condMet) + No _ => (False ** IsNotInfix) + rest <- printStmts @{NewFun {isInfix} {languageCondition = Scala3Cond infixCond} nm} fl tl cont (namesInside, funArgs) <- newVars fl _ names brBody <- chooseAny funBody <- if brBody From 05fe03ca73b10c113dfc42f58f307179ada3587e Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Tue, 27 Aug 2024 18:30:21 +0300 Subject: [PATCH 02/12] Small fix for NamedCtxt --- .../src/Language/PilFun/Pretty/DSL.idr | 27 +++++++++---------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr b/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr index 8265eb30f..c37302c75 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr @@ -7,27 +7,26 @@ import public Language.PilFun.Pretty %default total public export -record NamedCtxt where +record NamedCtxt (l : SupportedLanguages) where constructor MkNamedCtxt - language : SupportedLanguages functions : Funs variables : Vars - fvNames : UniqNames language functions variables + fvNames : UniqNames l functions variables public export %inline -AddFun : (isInfix : Bool) -> (isPure : Bool) -> (s : String) -> (fun : FunSig) -> - (ctx : NamedCtxt) -> - (0 _ : LanguageToCondition ctx.language fun isInfix isPure) => - (0 _ : NameIsNew ctx.language ctx.functions ctx.variables ctx.fvNames s) => - NamedCtxt -AddFun isInfix isPure s fun $ MkNamedCtxt language funs vars names = MkNamedCtxt language (funs: (isInfix : Bool) -> (isPure : Bool) -> (s : String) -> (fun : FunSig) -> + (ctx : NamedCtxt l) -> + (0 _ : LanguageToCondition l fun isInfix isPure) => + (0 _ : NameIsNew l ctx.functions ctx.variables ctx.fvNames s) => + NamedCtxt l +AddFun isInfix isPure s fun $ MkNamedCtxt funs vars names = MkNamedCtxt (funs:>) : {0 arg : NamedCtxt -> Type} -> {0 arg' : NamedCtxt -> Type} -> - ((ctx : NamedCtxt) -> (0 _ : arg ctx) => (0 _ : arg' ctx) => NamedCtxt) -> - (ctx : NamedCtxt) -> (0 _ : arg ctx) => (0 _ : arg' ctx) => NamedCtxt +(>>) : {0 arg : NamedCtxt l -> Type} -> {0 arg' : NamedCtxt l -> Type} -> + ((ctx : NamedCtxt l) -> (0 _ : arg ctx) => (0 _ : arg' ctx) => NamedCtxt l) -> + (ctx : NamedCtxt l) -> (0 _ : arg ctx) => (0 _ : arg' ctx) => NamedCtxt l (>>) f x = f x public export %inline -Enough : SupportedLanguages -> NamedCtxt -Enough l = MkNamedCtxt l [<] [<] Empty +Enough : NamedCtxt l +Enough = MkNamedCtxt [<] [<] Empty From ca77e57f37fbb31e33899006dbec28dbc69bbd25 Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Thu, 29 Aug 2024 17:44:55 +0300 Subject: [PATCH 03/12] Fixed order of variables in the Idris2 pretty printer --- examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr index ce3b3215d..059e95102 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr @@ -84,7 +84,7 @@ printStmts fl $ NewF (typesFrom ==> maybeRet) body cont = do let processedOutputType = "IO" <++> printMaybeTy maybeRet let idrisTypeSignature = processedInputTypes <++> processedOutputType (namesInside, funArgs) <- newVars fl _ names - let prerparedArgs = hsep $ toList funArgs <&> \(n, t) => line n + let prerparedArgs = hsep $ reverse (toList funArgs) <&> \(n, t) => line n body <- printStmts @{namesInside} fl body <&> indent' 6 pure $ flip vappend rest $ vsep [ "let" <++> line nm <++> ":" <++> idrisTypeSignature, From 6a0c7fbdb08aa38c3c92344690153fa2a5ddf993 Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Thu, 29 Aug 2024 18:04:14 +0300 Subject: [PATCH 04/12] Removed ConditionType binding (due to the bug in derivation) --- examples/pil-fun/src/Language/PilFun/Pretty.idr | 4 ---- 1 file changed, 4 deletions(-) diff --git a/examples/pil-fun/src/Language/PilFun/Pretty.idr b/examples/pil-fun/src/Language/PilFun/Pretty.idr index 9365336cc..004cbc453 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty.idr @@ -22,10 +22,6 @@ public export data SupportedLanguages = Scala3 | Idris2 -public export -ConditionType : Type -ConditionType = FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type - public export data ScalaCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type where From bbb0087d2e0921a8dfbe7ddb3ffb71a38c1a8e21 Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Mon, 2 Sep 2024 16:04:34 +0300 Subject: [PATCH 05/12] Idris 2 pretty printer is fully functional now --- examples/pil-fun/src/Language/PilFun/Pretty.idr | 8 +++++++- .../pil-fun/src/Language/PilFun/Pretty/Idris2.idr | 14 ++++++++++---- 2 files changed, 17 insertions(+), 5 deletions(-) diff --git a/examples/pil-fun/src/Language/PilFun/Pretty.idr b/examples/pil-fun/src/Language/PilFun/Pretty.idr index 004cbc453..272406e89 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty.idr @@ -31,7 +31,7 @@ data ScalaCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type public export data IdrisCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type where - Trivial : IdrisCondition funSig isInfix isPure + IsPure : (isPure : Bool) -> IdrisCondition funSig isInfix isPure public export data LanguageToCondition : (l : SupportedLanguages) -> FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type @@ -98,6 +98,12 @@ isFunInfix @{NewFun {isInfix} _} Here = isInfix isFunInfix @{NewFun @{ss} s} (There i) = isFunInfix @{ss} i isFunInfix @{NewVar @{ss} s} i = isFunInfix @{ss} i +isFunPure : UniqNames l funs vars => IndexIn funs -> Bool +isFunPure @{JustNew @{ss} _} i = isFunPure @{ss} i +isFunPure @{NewFun {isPure} _} Here = isPure +isFunPure @{NewFun @{ss} _} (There i) = isFunPure @{ss} i +isFunPure @{NewVar @{ss} _} i = isFunPure @{ss} i + -- Returned vect has a reverse order; I'd like some `SnocVect` here. newVars : (newNames : Gen0 String) => NamesRestrictions => diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr index 059e95102..769a7bb6a 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr @@ -44,10 +44,10 @@ printFunCall : {funs : _} -> {vars : _} -> {opts : _} -> printFunCall n args = do let f_name = funName {vars} n let f_doc : Doc opts = line f_name - let ars = toList $ getExprs args + let arExps = toList $ getExprs args let preparedArgs : List (Exists (Expr funs vars)) -> Gen0 $ Doc opts = - \as => map hsep $ for as $ \(Evidence _ e) => (printExpr e >>= \x => pure $ parenthesise True x) - pure $ parenthesise True $ hangSep' 2 f_doc !(preparedArgs ars) + \as => map hsep $ for as $ \(Evidence _ e) => printExpr e + pure $ hangSep' 2 f_doc !(preparedArgs arExps) printExpr $ C $ I k = pure $ line $ show k printExpr $ C $ B False = pure "False" @@ -55,7 +55,11 @@ printExpr $ C $ B True = pure "True" printExpr $ V n = case index vars n of (_, Mutable) => pure $ "!" <+> (parenthesise True $ "readIORef" <++> line (varName {funs} n)) (_, Immutable) => pure $ line $ varName {funs} n -printExpr $ F n args = assert_total printFunCall n args +printExpr @{uniqNames} $ F n args = do + funCallDoc <- assert_total printFunCall n args + let proccesedDoc = parenthesise True funCallDoc + let finalDoc = if isFunPure @{uniqNames} n then proccesedDoc else ("!" <+> proccesedDoc) + pure finalDoc printStmts : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> (names : UniqNames Idris2 funs vars) => @@ -121,6 +125,8 @@ printIdris2 : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> Stmts funs vars retTy -> Gen0 $ Doc opts printIdris2 fl stmts = do pure $ vsep ["module Main", + "", + "import Data.IORef", "", "main : IO ()", "main = do", From fc8d7f5a62a5237117f10655f82bec2a6897ee8c Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Tue, 3 Sep 2024 16:58:51 +0300 Subject: [PATCH 06/12] Move name generators out of runner --- .../pil-fun/src/Language/PilFun/Pretty.idr | 20 +++++++++---------- .../src/Language/PilFun/Pretty/Idris2.idr | 17 ++++++++++------ .../src/Language/PilFun/Pretty/Scala3.idr | 11 ++++++---- 3 files changed, 28 insertions(+), 20 deletions(-) diff --git a/examples/pil-fun/src/Language/PilFun/Pretty.idr b/examples/pil-fun/src/Language/PilFun/Pretty.idr index 272406e89..0e1be4041 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty.idr @@ -70,14 +70,14 @@ rawNewName : Fuel -> (l : SupportedLanguages) -> (Fuel -> Gen MaybeEmpty String) Gen MaybeEmpty (s ** NameIsNew l funs vars names s) export -genNewName : {l : SupportedLanguages} -> Fuel -> (Fuel -> Gen MaybeEmpty String) => +genNewName : {l : SupportedLanguages} -> Fuel -> Gen MaybeEmpty String -> NamesRestrictions => (funs : Funs) -> (vars : Vars) -> (names : UniqNames l funs vars) -> Gen MaybeEmpty (s ** NameIsNew l funs vars names s) -genNewName fl @{genStr} funs vars names = do - nn@(nm ** _) <- rawNewName fl l @{genStr} funs vars names +genNewName fl genStr funs vars names = do + nn@(nm ** _) <- rawNewName fl l @{const genStr} funs vars names if reservedKeywords `contains'` nm - then assert_total $ genNewName fl @{genStr} funs vars names -- we could reduce fuel instead of `assert_total` + then assert_total $ genNewName fl genStr funs vars names -- we could reduce fuel instead of `assert_total` else pure nn varName : UniqNames l funs vars => IndexIn vars -> String @@ -105,16 +105,16 @@ isFunPure @{NewFun @{ss} _} (There i) = isFunPure @{ss} i isFunPure @{NewVar @{ss} _} i = isFunPure @{ss} i -- Returned vect has a reverse order; I'd like some `SnocVect` here. -newVars : (newNames : Gen0 String) => - NamesRestrictions => +newVars : NamesRestrictions => {l : _} -> {funs : _} -> {vars : _} -> Fuel -> + (newNames : Gen0 String) -> (extraVars : _) -> UniqNames l funs vars -> Gen0 (UniqNames l funs (vars ++ extraVars), Vect extraVars.length (String, Ty)) -newVars _ [<] names = pure (names, []) -newVars fl (vs: Bool diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr index 769a7bb6a..7314094d5 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr @@ -25,6 +25,13 @@ NamesRestrictions where "let", "module", "namespace", "of", "partial", "prefix", "private", "proof", "public", "record", "rewrite", "then", "total", "where", "with", "main", "IO", "Int", "Bool"] +alphaNames : Gen0 String +alphaNames = pack <$> listOf {length = choose (1,10)} (choose ('a', 'z')) + +infixNames : Gen0 String +infixNames = pack <$> listOf {length = choose (1,4)} (elements + [':', '+', '-', '*', '\\', '/', '=', '.', '?', '|', '&', '>', '<', '!', '@', '$', '%', '^', '~', '#']) + printTy : Ty -> Doc opts printTy Int' = "Int" printTy Bool' = "Bool" @@ -63,31 +70,30 @@ printExpr @{uniqNames} $ F n args = do printStmts : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> (names : UniqNames Idris2 funs vars) => - (newNames : Gen0 String) => Fuel -> Stmts funs vars retTy -> Gen0 $ Doc opts printStmts fl $ NewV ty Immutable initial cont = do - (nm ** _) <- genNewName fl _ _ names + (nm ** _) <- genNewName fl alphaNames _ _ names rest <- printStmts @{NewVar nm} fl cont let lhs = "let" <++> line nm <++> "=" rhs <- printExpr initial pure $ flip vappend rest $ hangSep' 2 lhs rhs printStmts fl $ NewV ty Mutable initial cont = do - (nm ** _) <- genNewName fl _ _ names + (nm ** _) <- genNewName fl alphaNames _ _ names rest <- printStmts @{NewVar nm} fl cont let lhs = line nm <++> "<-" rhs <- printExpr initial pure $ flip vappend rest $ hangSep' 2 lhs $ "newIORef" <++> rhs printStmts fl $ NewF (typesFrom ==> maybeRet) body cont = do - (nm ** _) <- genNewName fl _ _ names + (nm ** _) <- genNewName fl alphaNames _ _ names rest <- printStmts @{NewFun nm} fl cont let processedInputTypes = hsep $ (snocListTyToList typesFrom) <&> (\ty => printTy ty <++> "->") let processedOutputType = "IO" <++> printMaybeTy maybeRet let idrisTypeSignature = processedInputTypes <++> processedOutputType - (namesInside, funArgs) <- newVars fl _ names + (namesInside, funArgs) <- newVars fl alphaNames _ names let prerparedArgs = hsep $ reverse (toList funArgs) <&> \(n, t) => line n body <- printStmts @{namesInside} fl body <&> indent' 6 pure $ flip vappend rest $ vsep @@ -120,7 +126,6 @@ printStmts fl $ Nop = pure "pure ()" export printIdris2 : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> (names : UniqNames Idris2 funs vars) => - (newNames : Gen0 String) => Fuel -> Stmts funs vars retTy -> Gen0 $ Doc opts printIdris2 fl stmts = do diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr index e7967e7e5..9624f828b 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr @@ -43,6 +43,9 @@ NamesRestrictions where , "@" , "=>>" , "?=>" ] +namesGenScala : Gen0 String +namesGenScala = pack <$> listOf {length = choose (1,10)} (choose ('a', 'z')) + printExpr : {funs : _} -> {vars : _} -> {opts : _} -> (names : UniqNames Scala3 funs vars) => Prec -> Expr funs vars ty -> Gen0 $ Doc opts @@ -87,7 +90,7 @@ wrapMain : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> wrapMain fl False Nothing x = x wrapMain fl False (Just cont) x = [| x `vappend` assert_total printStmts fl False cont |] wrapMain fl True cont body = do - (nm ** _) <- genNewName fl _ _ names + (nm ** _) <- genNewName fl newNames _ _ names b <- body cnt <- for cont $ assert_total $ printStmts @{JustNew nm} fl False let b = maybe b (b `vappend`) cnt @@ -109,7 +112,7 @@ printSubStmts _ True Nop = pure "{}" printSubStmts fl _ ss = printStmts fl False ss printStmts fl tl $ NewV ty mut initial cont = do - (nm ** _) <- genNewName fl _ _ names + (nm ** _) <- genNewName fl newNames _ _ names rest <- printStmts @{NewVar nm} fl tl cont let tyAscr = if !chooseAny then ":" <++> printTy ty else empty let declPref = case mut of @@ -120,13 +123,13 @@ printStmts fl tl $ NewV ty mut initial cont = do pure $ flip vappend rest $ hangSep' 2 lhs rhs printStmts fl tl $ NewF sig body cont = do - (nm ** _) <- genNewName fl _ _ names + (nm ** _) <- genNewName fl newNames _ _ names isInfix <- chooseAny let (isInfix ** infixCond) : (b ** ScalaCondition sig b _) = case decSo _ of Yes condMet => (isInfix ** MoreThanOneArg condMet) No _ => (False ** IsNotInfix) rest <- printStmts @{NewFun {isInfix} {languageCondition = Scala3Cond infixCond} nm} fl tl cont - (namesInside, funArgs) <- newVars fl _ names + (namesInside, funArgs) <- newVars fl newNames _ names brBody <- chooseAny funBody <- if brBody then printStmts @{namesInside} fl False body From 149e7f912512774206aecbe8cff7edab5d86be39 Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Fri, 25 Oct 2024 11:38:35 +0300 Subject: [PATCH 07/12] Idris2 pretty printer is fully operational --- examples/pil-fun/src/Language/PilFun.idr | 7 +- .../pil-fun/src/Language/PilFun/Pretty.idr | 15 +- .../src/Language/PilFun/Pretty/DSL.idr | 10 +- .../src/Language/PilFun/Pretty/Idris2.idr | 137 +++++++++++++++--- 4 files changed, 132 insertions(+), 37 deletions(-) diff --git a/examples/pil-fun/src/Language/PilFun.idr b/examples/pil-fun/src/Language/PilFun.idr index bbdab8030..2f6296cbf 100644 --- a/examples/pil-fun/src/Language/PilFun.idr +++ b/examples/pil-fun/src/Language/PilFun.idr @@ -198,7 +198,9 @@ data Expr : Funs -> Vars -> Ty -> Type where Expr funs vars ty F : (n : IndexIn funs) -> - AtIndex n (from ==> Just to) => + {from : _} -> + {to : _} -> + AtIndex funs n (from ==> Just to) => ExprsSnocList funs vars from -> Expr funs vars to @@ -236,7 +238,8 @@ data Stmts : (funs : Funs) -> Stmts funs vars retTy Call : (n : IndexIn funs) -> - AtIndex n (from ==> Nothing) => + {from : _} -> + AtIndex funs n (from ==> Nothing) => ExprsSnocList funs vars from -> (cont : Stmts funs vars retTy) -> Stmts funs vars retTy diff --git a/examples/pil-fun/src/Language/PilFun/Pretty.idr b/examples/pil-fun/src/Language/PilFun/Pretty.idr index 0e1be4041..ce5fdc786 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty.idr @@ -31,7 +31,8 @@ data ScalaCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type public export data IdrisCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type where - IsPure : (isPure : Bool) -> IdrisCondition funSig isInfix isPure + IsInfix : (a : Ty ** b : Ty ** to : MaybeTy ** funSig === ([ to)) -> (isPure : Bool) -> IdrisCondition funSig True isPure + NotInfix : (isPure : Bool) -> IdrisCondition funSig False isPure public export data LanguageToCondition : (l : SupportedLanguages) -> FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type @@ -51,7 +52,7 @@ data UniqNames : (l : SupportedLanguages) -> (funs : Funs) -> (vars : Vars) -> T JustNew : (ss : UniqNames l funs vars) => (s : String) -> (0 _ : NameIsNew l funs vars ss s) => UniqNames l funs vars NewFun : (ss : UniqNames l funs vars) => (s : String) -> (0 _ : NameIsNew l funs vars ss s) => {default False isInfix : Bool} -> {default False isPure : Bool} -> - (0 languageCondition : LanguageToCondition l fun isInfix isPure) => + (languageCondition : LanguageToCondition l fun isInfix isPure) => UniqNames l (funs: (s : String) -> (0 _ : NameIsNew l funs vars ss s) => UniqNames l funs ((:<) vars var mut) @@ -98,11 +99,11 @@ isFunInfix @{NewFun {isInfix} _} Here = isInfix isFunInfix @{NewFun @{ss} s} (There i) = isFunInfix @{ss} i isFunInfix @{NewVar @{ss} s} i = isFunInfix @{ss} i -isFunPure : UniqNames l funs vars => IndexIn funs -> Bool -isFunPure @{JustNew @{ss} _} i = isFunPure @{ss} i -isFunPure @{NewFun {isPure} _} Here = isPure -isFunPure @{NewFun @{ss} _} (There i) = isFunPure @{ss} i -isFunPure @{NewVar @{ss} _} i = isFunPure @{ss} i +isFunPure : UniqNames l funs vars -> IndexIn funs -> Bool +isFunPure (JustNew @{ss} _) i = isFunPure ss i +isFunPure (NewFun {isPure} _) Here = isPure +isFunPure (NewFun @{ss} _) (There i) = isFunPure ss i +isFunPure (NewVar @{ss} _) i = isFunPure ss i -- Returned vect has a reverse order; I'd like some `SnocVect` here. newVars : NamesRestrictions => diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr b/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr index c37302c75..157874b23 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr @@ -15,16 +15,16 @@ record NamedCtxt (l : SupportedLanguages) where public export %inline AddFun : {0 l : SupportedLanguages} -> (isInfix : Bool) -> (isPure : Bool) -> (s : String) -> (fun : FunSig) -> + (lCond : LanguageToCondition l fun isInfix isPure) => (ctx : NamedCtxt l) -> - (0 _ : LanguageToCondition l fun isInfix isPure) => (0 _ : NameIsNew l ctx.functions ctx.variables ctx.fvNames s) => NamedCtxt l -AddFun isInfix isPure s fun $ MkNamedCtxt funs vars names = MkNamedCtxt (funs:>) : {0 arg : NamedCtxt l -> Type} -> {0 arg' : NamedCtxt l -> Type} -> - ((ctx : NamedCtxt l) -> (0 _ : arg ctx) => (0 _ : arg' ctx) => NamedCtxt l) -> - (ctx : NamedCtxt l) -> (0 _ : arg ctx) => (0 _ : arg' ctx) => NamedCtxt l +(>>) : {0 arg : NamedCtxt l -> Type} -> + ((ctx : NamedCtxt l) -> (0 _ : arg ctx) => NamedCtxt l) -> + (ctx : NamedCtxt l) -> (0 _ : arg ctx) => NamedCtxt l (>>) f x = f x public export %inline diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr index 7314094d5..a207a0593 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr @@ -5,6 +5,7 @@ import Data.Fuel import Data.SnocList import public Data.So import Data.Vect +import Data.String import public Language.PilFun import public Language.PilFun.Pretty @@ -19,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", @@ -29,7 +30,7 @@ alphaNames : Gen0 String alphaNames = pack <$> listOf {length = choose (1,10)} (choose ('a', 'z')) infixNames : Gen0 String -infixNames = pack <$> listOf {length = choose (1,4)} (elements +infixNames = flip suchThat (not . isPrefixOf "--") $ pack <$> listOf {length = choose (1,4)} (elements [':', '+', '-', '*', '\\', '/', '=', '.', '?', '|', '&', '>', '<', '!', '@', '$', '%', '^', '~', '#']) printTy : Ty -> Doc opts @@ -44,28 +45,83 @@ printExpr : {funs : _} -> {vars : _} -> {opts : _} -> (names : UniqNames Idris2 funs vars) => Expr funs vars ty -> Gen0 $ Doc opts -printFunCall : {funs : _} -> {vars : _} -> {opts : _} -> +printFunCall : {funs : _} -> {vars : _} -> {from : _} -> {to : _} -> {opts : _} -> (names : UniqNames Idris2 funs vars) => - IndexIn funs -> ExprsSnocList funs vars argTys -> Gen0 $ Doc opts + (n : IndexIn funs) -> + (ati : AtIndex funs n (from ==> to)) => + ExprsSnocList funs vars from -> Gen0 $ Doc opts + +data ArgStruct : LayoutOpts -> Type where + InfixTwoArgs : {opts : _} -> Doc opts -> Doc opts -> ArgStruct opts + PrefixTwoArgs : {opts : _} -> Doc opts -> Doc opts -> ArgStruct opts + ManyArgs : {opts : _} -> List (Doc opts) -> ArgStruct opts + NoArgs : {opts : _} -> ArgStruct opts + +getArgs : {from' : SnocListTy} -> + {to' : MaybeTy} -> + (argFs : Funs ** argVs : Vars ** argNms : UniqNames Idris2 argFs argVs ** ExprsSnocList argFs argVs from') -> + {fs : Funs} -> + {vs : Vars} -> + (nms : UniqNames Idris2 fs vs) -> + (i : IndexIn fs) -> + (ati : AtIndex fs i (from' ==> to')) -> + {opts : _} -> + Gen0 (ArgStruct opts) + +getArgs (_ ** _ ** _ ** [<]) _ _ _ = pure NoArgs + +getArgs argedLst (JustNew _ {ss}) i ati = getArgs argedLst ss i ati +getArgs argedLst (NewVar _ {ss}) i ati = getArgs argedLst ss i ati + +getArgs argedLst (NewFun _ {ss}) (There i) (There' i') = getArgs argedLst ss i i' + +getArgs {from'} argedLst (NewFun _ {languageCondition}) Here Here' with (languageCondition) + + getArgs {from'} argedLst (NewFun _ {languageCondition}) Here Here' | Idris2Cond (IsInfix (a ** b ** to ** rst) isPure) with (rst) + getArgs {from' = [< a, b ]} (argFs ** argVs ** argNms ** [< a', b' ]) (NewFun _ {languageCondition}) Here Here' | Idris2Cond (IsInfix (a ** b ** to ** Refl) isPure) | Refl = do + aDoc <- printExpr a' + bDoc <- printExpr b' + pure $ InfixTwoArgs aDoc bDoc + + getArgs {from'} argedLst (NewFun _ {languageCondition}) Here Here' | Idris2Cond (NotInfix isPure) with (from') + _ | [< a, b ] with (argedLst) + _ | (_ ** _ ** _ ** [< a', b' ]) = do + aDoc <- printExpr a' + bDoc <- printExpr b' + pure $ PrefixTwoArgs aDoc bDoc + _ | from'' with (argedLst) + _ | (_ ** _ ** _ ** lst) = do + argsDocs : List (Doc _) <- for ((toList . getExprs) lst) (\(Evidence _ e) => printExpr e) + pure $ ManyArgs argsDocs -printFunCall n args = do - let f_name = funName {vars} n - let f_doc : Doc opts = line f_name - let arExps = toList $ getExprs args - let preparedArgs : List (Exists (Expr funs vars)) -> Gen0 $ Doc opts = - \as => map hsep $ for as $ \(Evidence _ e) => printExpr e - pure $ hangSep' 2 f_doc !(preparedArgs arExps) +printFunCall n args = do + wantInfix <- chooseAnyOf Bool + let f_name = funName {vars} n + let f_doc : Doc opts = line f_name + processedArgs <- getArgs (funs ** vars ** names ** args) names n ati + case (wantInfix, processedArgs) of + (True, InfixTwoArgs a b) => pure $ a <++> f_doc <++> b + (False, InfixTwoArgs a b) => pure $ "(" <+> f_doc <+> ")" <++> a <++> b + (True, PrefixTwoArgs a b) => pure $ a <++> "`" <+> f_doc <+> "`" <++> b + (False, PrefixTwoArgs a b) => pure $ f_doc <++> a <++> b + (_, ManyArgs argsDocs) => pure $ f_doc <++> hsep argsDocs + (_, NoArgs)=> pure f_doc + printExpr $ C $ I k = pure $ line $ show k printExpr $ C $ B False = pure "False" printExpr $ C $ B True = pure "True" printExpr $ V n = case index vars n of - (_, Mutable) => pure $ "!" <+> (parenthesise True $ "readIORef" <++> line (varName {funs} n)) - (_, Immutable) => pure $ line $ varName {funs} n -printExpr @{uniqNames} $ F n args = do + (_, Mutable) => pure $ "!" <+> (parenthesise True $ "readIORef" <++> line (varName {funs} n)) + (_, Immutable) => pure $ line $ varName {funs} n +printExpr @{uniqNames} $ F {from = [<]} n args = do + funCallDoc <- assert_total printFunCall n args + let finalDoc = if isFunPure uniqNames n then funCallDoc else ("!" <+> funCallDoc) + pure finalDoc +printExpr @{uniqNames} $ F {from} n args = do funCallDoc <- assert_total printFunCall n args let proccesedDoc = parenthesise True funCallDoc - let finalDoc = if isFunPure @{uniqNames} n then proccesedDoc else ("!" <+> proccesedDoc) + let finalDoc = if isFunPure uniqNames n then proccesedDoc else ("!" <+> proccesedDoc) pure finalDoc printStmts : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> @@ -87,19 +143,54 @@ printStmts fl $ NewV ty Mutable initial cont = do rhs <- printExpr initial pure $ flip vappend rest $ hangSep' 2 lhs $ "newIORef" <++> rhs +printStmts fl $ NewF ([<] ==> maybeRet) body cont = do + let (isInfix ** infixCond) : (b ** IdrisCondition ([<] ==> maybeRet) b False) = (False ** NotInfix False) + (nm ** _) <- genNewName fl alphaNames _ _ names + rest <- printStmts @{NewFun nm {isInfix}} fl cont + let funName = line nm + let processedOutputType = "IO" <++> printMaybeTy maybeRet + printedBody <- printStmts fl body <&> indent' 6 + pure $ flip vappend rest $ vsep + [ "let" <++> funName <++> ":" <++> processedOutputType, + indent 4 $ funName <++> "=" <++> "do", + printedBody ] + +printStmts fl $ NewF ([< a, b ] ==> maybeRet) body cont = do + wantInfix <- chooseAnyOf Bool + let (isInfix ** infixCond) : (inf ** IdrisCondition ([< a, b ] ==> maybeRet) inf False) = case wantInfix of + True => (True ** IsInfix (a ** b ** maybeRet ** Refl) False) + False => (False ** NotInfix False) + let nameGen = if isInfix then infixNames else alphaNames + (nm ** _) <- genNewName fl nameGen _ _ names + rest <- printStmts @{NewFun nm {isInfix} @{names}} fl cont + let infixAwareName : Doc opts = if isInfix then "(" <+> line nm <+> ")" else line nm + let processedInputTypes : Doc opts = hsep $ (snocListTyToList [< a, b ]) <&> (\ty => printTy ty <++> "->") + let processedOutputType = "IO" <++> printMaybeTy maybeRet + let idrisTypeSignature = processedInputTypes <++> processedOutputType + (namesInside, funArgs) <- newVars fl alphaNames [< a, b ] (JustNew @{names} nm) + let prerparedArgs = hsep $ reverse (toList funArgs) <&> \(n, t) => line n + printedBody <- printStmts @{namesInside} fl body <&> indent' 6 + let declAndDefintion = [ "let" <++> infixAwareName <++> ":" <++> idrisTypeSignature, + indent 4 $ infixAwareName <++> prerparedArgs <++> "=" <++> "do", + printedBody ] + let final = if isInfix then ("let infix 1" <++> line nm) :: declAndDefintion else declAndDefintion + pure $ flip vappend rest $ vsep final + printStmts fl $ NewF (typesFrom ==> maybeRet) body cont = do + let (isInfix ** infixCond) : (b ** IdrisCondition (typesFrom ==> maybeRet) b False) = (False ** NotInfix False) (nm ** _) <- genNewName fl alphaNames _ _ names - rest <- printStmts @{NewFun nm} fl cont - let processedInputTypes = hsep $ (snocListTyToList typesFrom) <&> (\ty => printTy ty <++> "->") + rest <- printStmts @{NewFun nm {isInfix} @{names}} fl cont + let funName = line nm + let processedInputTypes : Doc opts = hsep $ (snocListTyToList typesFrom) <&> (\ty => printTy ty <++> "->") let processedOutputType = "IO" <++> printMaybeTy maybeRet let idrisTypeSignature = processedInputTypes <++> processedOutputType - (namesInside, funArgs) <- newVars fl alphaNames _ names + (namesInside, funArgs) <- newVars fl alphaNames _ (JustNew @{names} nm) let prerparedArgs = hsep $ reverse (toList funArgs) <&> \(n, t) => line n - body <- printStmts @{namesInside} fl body <&> indent' 6 - pure $ flip vappend rest $ vsep - [ "let" <++> line nm <++> ":" <++> idrisTypeSignature, - indent 4 $ line nm <++> prerparedArgs <++> "=" <++> "do", - body ] + printedBody <- printStmts @{namesInside} fl body <&> indent' 6 + let declAndDefintion = vsep [ "let" <++> funName <++> ":" <++> idrisTypeSignature, + indent 4 $ funName <++> prerparedArgs <++> "=" <++> "do", + printedBody ] + pure $ vappend declAndDefintion rest printStmts fl $ (#=) n v cont = do v_doc <- printExpr v From 09d73b2453af4a3784020b8f3be5f63233a70481 Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Fri, 25 Oct 2024 12:50:31 +0300 Subject: [PATCH 08/12] Small naming fix --- .../pil-fun/src/Language/PilFun/Pretty.idr | 18 +++++++++--------- .../pil-fun/src/Language/PilFun/Pretty/DSL.idr | 4 ++-- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/examples/pil-fun/src/Language/PilFun/Pretty.idr b/examples/pil-fun/src/Language/PilFun/Pretty.idr index ce5fdc786..deae964d1 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty.idr @@ -19,8 +19,8 @@ import System.Random.Pure.StdGen %default total public export -data SupportedLanguages = Scala3 - | Idris2 +data SupportedLanguage = Scala3 + | Idris2 public export data ScalaCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type @@ -35,18 +35,18 @@ data IdrisCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type NotInfix : (isPure : Bool) -> IdrisCondition funSig False isPure public export -data LanguageToCondition : (l : SupportedLanguages) -> FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type +data LanguageToCondition : (l : SupportedLanguage) -> FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type where [search l] Scala3Cond : ScalaCondition funSig isInfix isPure -> LanguageToCondition Scala3 funSig isInfix isPure Idris2Cond : IdrisCondition funSig isInfix isPure -> LanguageToCondition Idris2 funSig isInfix isPure public export -data UniqNames : (l : SupportedLanguages) -> (funs : Funs) -> (vars : Vars) -> Type +data UniqNames : (l : SupportedLanguage) -> (funs : Funs) -> (vars : Vars) -> Type public export -data NameIsNew : (l : SupportedLanguages) -> (funs : Funs) -> (vars : Vars) -> UniqNames l funs vars -> String -> Type +data NameIsNew : (l : SupportedLanguage) -> (funs : Funs) -> (vars : Vars) -> UniqNames l funs vars -> String -> Type -data UniqNames : (l : SupportedLanguages) -> (funs : Funs) -> (vars : Vars) -> Type where +data UniqNames : (l : SupportedLanguage) -> (funs : Funs) -> (vars : Vars) -> Type where [search funs vars] Empty : UniqNames l [<] [<] JustNew : (ss : UniqNames l funs vars) => (s : String) -> (0 _ : NameIsNew l funs vars ss s) => UniqNames l funs vars @@ -56,7 +56,7 @@ data UniqNames : (l : SupportedLanguages) -> (funs : Funs) -> (vars : Vars) -> T UniqNames l (funs: (s : String) -> (0 _ : NameIsNew l funs vars ss s) => UniqNames l funs ((:<) vars var mut) -data NameIsNew : (l : SupportedLanguages) -> (funs : Funs) -> (vars : Vars) -> UniqNames l funs vars -> String -> Type where +data NameIsNew : (l : SupportedLanguage) -> (funs : Funs) -> (vars : Vars) -> UniqNames l funs vars -> String -> Type where E : NameIsNew l [<] [<] Empty x J : (0 _ : So $ x /= s) -> NameIsNew l funs vars ss x -> NameIsNew l funs vars (JustNew @{ss} s @{sub}) x F : (0 _ : So $ x /= s) -> NameIsNew l funs vars ss x -> NameIsNew l (funs: (l : SupportedLanguages) -> (Fuel -> Gen MaybeEmpty String) => +rawNewName : Fuel -> (l : SupportedLanguage) -> (Fuel -> Gen MaybeEmpty String) => (funs : Funs) -> (vars : Vars) -> (names : UniqNames l funs vars) -> Gen MaybeEmpty (s ** NameIsNew l funs vars names s) export -genNewName : {l : SupportedLanguages} -> Fuel -> Gen MaybeEmpty String -> +genNewName : {l : SupportedLanguage} -> Fuel -> Gen MaybeEmpty String -> NamesRestrictions => (funs : Funs) -> (vars : Vars) -> (names : UniqNames l funs vars) -> Gen MaybeEmpty (s ** NameIsNew l funs vars names s) diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr b/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr index 157874b23..de43e7c1d 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr @@ -7,14 +7,14 @@ import public Language.PilFun.Pretty %default total public export -record NamedCtxt (l : SupportedLanguages) where +record NamedCtxt (l : SupportedLanguage) where constructor MkNamedCtxt functions : Funs variables : Vars fvNames : UniqNames l functions variables public export %inline -AddFun : {0 l : SupportedLanguages} -> (isInfix : Bool) -> (isPure : Bool) -> (s : String) -> (fun : FunSig) -> +AddFun : {0 l : SupportedLanguage} -> (isInfix : Bool) -> (isPure : Bool) -> (s : String) -> (fun : FunSig) -> (lCond : LanguageToCondition l fun isInfix isPure) => (ctx : NamedCtxt l) -> (0 _ : NameIsNew l ctx.functions ctx.variables ctx.fvNames s) => From c7cbbc5ff6c4b23d568b1ca0c46d1e5a1eea3098 Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Mon, 28 Oct 2024 13:37:52 +0300 Subject: [PATCH 09/12] Update branch for new Runner and Lua support --- examples/pil-fun/src/Language/PilFun.idr | 4 +- .../pil-fun/src/Language/PilFun/Pretty.idr | 18 ++++-- .../src/Language/PilFun/Pretty/Idris2.idr | 9 +-- .../src/Language/PilFun/Pretty/Lua5_4.idr | 19 +++--- .../src/Language/PilFun/Pretty/Scala3.idr | 4 +- examples/pil-fun/src/Runner.idr | 62 +++++++++---------- 6 files changed, 60 insertions(+), 56 deletions(-) diff --git a/examples/pil-fun/src/Language/PilFun.idr b/examples/pil-fun/src/Language/PilFun.idr index 2f6296cbf..140bdedf9 100644 --- a/examples/pil-fun/src/Language/PilFun.idr +++ b/examples/pil-fun/src/Language/PilFun.idr @@ -200,7 +200,7 @@ data Expr : Funs -> Vars -> Ty -> Type where F : (n : IndexIn funs) -> {from : _} -> {to : _} -> - AtIndex funs n (from ==> Just to) => + AtIndex n (from ==> Just to) => ExprsSnocList funs vars from -> Expr funs vars to @@ -239,7 +239,7 @@ data Stmts : (funs : Funs) -> Call : (n : IndexIn funs) -> {from : _} -> - AtIndex funs n (from ==> Nothing) => + AtIndex n (from ==> Nothing) => ExprsSnocList funs vars from -> (cont : Stmts funs vars retTy) -> Stmts funs vars retTy diff --git a/examples/pil-fun/src/Language/PilFun/Pretty.idr b/examples/pil-fun/src/Language/PilFun/Pretty.idr index deae964d1..86762e671 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty.idr @@ -21,6 +21,7 @@ import System.Random.Pure.StdGen public export data SupportedLanguage = Scala3 | Idris2 + | Lua5_4 public export data ScalaCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type @@ -34,12 +35,18 @@ data IdrisCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type IsInfix : (a : Ty ** b : Ty ** to : MaybeTy ** funSig === ([ to)) -> (isPure : Bool) -> IdrisCondition funSig True isPure NotInfix : (isPure : Bool) -> IdrisCondition funSig False isPure +public export +data LuaCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type + where + TrivialLuaCondition : LuaCondition funSig isInfix isPure + public export data LanguageToCondition : (l : SupportedLanguage) -> FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type where [search l] Scala3Cond : ScalaCondition funSig isInfix isPure -> LanguageToCondition Scala3 funSig isInfix isPure Idris2Cond : IdrisCondition funSig isInfix isPure -> LanguageToCondition Idris2 funSig isInfix isPure + Lua5_4Cond : LuaCondition funSig isInfix isPure -> LanguageToCondition Lua5_4 funSig isInfix isPure public export data UniqNames : (l : SupportedLanguage) -> (funs : Funs) -> (vars : Vars) -> Type @@ -135,9 +142,8 @@ wrapBrIf False pre x = pre `vappend` indent' 2 x wrapBrIf True pre x = ifMultiline (pre <++> "{" <++> x <++> "}") (vsep [pre <++> "{", indent' 2 x, "}"]) public export -0 PP : Type -PP = {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> - (names : UniqNames funs vars) => - (newNames : Gen0 String) => - Fuel -> - Stmts funs vars retTy -> Gen0 $ Doc opts +0 PP : SupportedLanguage -> Type +PP language = {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> + (names : UniqNames language funs vars) => + Fuel -> + Stmts funs vars retTy -> Gen0 $ Doc opts diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr index a207a0593..e491a7b6a 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr @@ -48,7 +48,7 @@ printExpr : {funs : _} -> {vars : _} -> {opts : _} -> printFunCall : {funs : _} -> {vars : _} -> {from : _} -> {to : _} -> {opts : _} -> (names : UniqNames Idris2 funs vars) => (n : IndexIn funs) -> - (ati : AtIndex funs n (from ==> to)) => + (ati : AtIndex n (from ==> to)) => ExprsSnocList funs vars from -> Gen0 $ Doc opts data ArgStruct : LayoutOpts -> Type where @@ -64,7 +64,7 @@ getArgs : {from' : SnocListTy} -> {vs : Vars} -> (nms : UniqNames Idris2 fs vs) -> (i : IndexIn fs) -> - (ati : AtIndex fs i (from' ==> to')) -> + (ati : AtIndex i (from' ==> to')) -> {opts : _} -> Gen0 (ArgStruct opts) @@ -215,10 +215,7 @@ printStmts fl $ Ret expr = do printStmts fl $ Nop = pure "pure ()" export -printIdris2 : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> - (names : UniqNames Idris2 funs vars) => - Fuel -> - Stmts funs vars retTy -> Gen0 $ Doc opts +printIdris2 : PP Idris2 printIdris2 fl stmts = do pure $ vsep ["module Main", "", diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Lua5_4.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Lua5_4.idr index e2c801037..400dca204 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Lua5_4.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Lua5_4.idr @@ -15,6 +15,9 @@ import public Text.PrettyPrint.Bernardy %default total +luaNamesGen : Gen0 String +luaNamesGen = pack <$> listOf {length = choose (1,10)} (choose ('a', 'z')) + printTy : Ty -> Doc opts printTy Int' = "number" printTy Bool' = "boolean" @@ -49,18 +52,18 @@ priority : String -> Maybe Priority priority func = lookup func priorities printExpr : {funs : _} -> {vars : _} -> {opts : _} -> - (names : UniqNames funs vars) => + (names : UniqNames Lua5_4 funs vars) => Fuel -> (lastPriority : Maybe Priority) -> Expr funs vars ty -> Gen0 $ Doc opts printFunCall : {funs : _} -> {vars : _} -> {opts : _} -> - (names : UniqNames funs vars) => + (names : UniqNames Lua5_4 funs vars) => Fuel -> (lastPriority : Maybe Priority) -> IndexIn funs -> ExprsSnocList funs vars argTys -> Gen0 $ Doc opts printStmts : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> - (names : UniqNames funs vars) => + (names : UniqNames Lua5_4 funs vars) => (newNames : Gen0 String) => Fuel -> Stmts funs vars retTy -> Gen0 $ Doc opts @@ -111,14 +114,14 @@ withCont cont stmt = pure $ stmt `vappend` cont printStmts fuel (NewV ty mut initial cont) = do - (name ** _) <- genNewName fuel _ _ names + (name ** _) <- genNewName fuel newNames _ _ names lhv <- newVarLhv name mut rhv <- printExpr fuel Nothing initial withCont !(printStmts fuel cont) $ hangSep' 2 (lhv <++> "=") rhv printStmts fuel (NewF sig body cont) = do - (name ** _) <- genNewName fuel _ _ names - (localNames, funArgs) <- newVars fuel _ names + (name ** _) <- genNewName fuel newNames _ _ names + (localNames, funArgs) <- newVars fuel newNames _ names let funArgs' = reverse (toList funArgs) let argHints = funArgs' <&> \(name, ty) => the (Doc opts) "---@param" <++> line name <++> printTy ty @@ -178,5 +181,5 @@ printStmts fuel Nop = do else pure empty export -printLua5_4 : PP -printLua5_4 fl = printStmts {names} {newNames} fl +printLua5_4 : PP Lua5_4 +printLua5_4 fl = printStmts {names} {newNames = luaNamesGen} fl diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr index 9624f828b..4e5c65356 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr @@ -173,5 +173,5 @@ printStmts fl tl $ Ret x = wrapMain {funs} {vars} fl tl Nothing $ printExpr Open printStmts fl tl $ Nop = wrapMain {funs} {vars} fl tl Nothing $ pure empty export -printScala3 : PP -printScala3 fl = printStmts {names} {newNames} fl True +printScala3 : PP Scala3 +printScala3 fl = printStmts {names} {newNames = namesGenScala} fl True diff --git a/examples/pil-fun/src/Runner.idr b/examples/pil-fun/src/Runner.idr index 413908f1b..7eba35225 100644 --- a/examples/pil-fun/src/Runner.idr +++ b/examples/pil-fun/src/Runner.idr @@ -98,18 +98,16 @@ cliOpts = --- Running --- --------------- -namesGen : Gen0 String -namesGen = pack <$> listOf {length = choose (1,10)} (choose ('a', 'z')) - run : Config -> - NamedCtxt -> - (pp : PP) -> + {0 language : SupportedLanguage} -> + NamedCtxt language -> + (pp : PP language) -> IO () run conf ctxt pp = do seed <- conf.usedSeed let vals = unGenTryN conf.testsCnt seed $ genStmts conf.modelFuel ctxt.functions ctxt.variables Nothing >>= - pp @{ctxt.fvNames} @{namesGen} conf.ppFuel + pp @{ctxt.fvNames} conf.ppFuel Lazy.for_ vals $ \val => do putStrLn "-------------------\n" putStr $ render conf.layoutOpts val @@ -118,38 +116,38 @@ run conf ctxt pp = do --- Language config --- ----------------------- -scala3StdFuns : NamedCtxt +scala3StdFuns : NamedCtxt Scala3 scala3StdFuns = do - AddFun True "+" $ [< Int', Int'] ==> Just Int' - AddFun True "*" $ [< Int', Int'] ==> Just Int' - AddFun False "-" $ [< Int'] ==> Just Int' - AddFun True "<" $ [< Int', Int'] ==> Just Bool' - AddFun True "<=" $ [< Int', Int'] ==> Just Bool' - AddFun True "==" $ [< Int', Int'] ==> Just Bool' - AddFun True "||" $ [< Bool', Bool'] ==> Just Bool' - AddFun True "&&" $ [< Bool', Bool'] ==> Just Bool' - AddFun False "!" $ [< Bool'] ==> Just Bool' - AddFun 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' + AddFun True True "<" $ [< Int', Int'] ==> Just Bool' + AddFun True True "<=" $ [< Int', Int'] ==> Just Bool' + AddFun True True "==" $ [< Int', Int'] ==> Just Bool' + 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_4StdFuns : NamedCtxt Lua5_4 lua5_4StdFuns = do - AddFun True "+" $ [< Int', Int'] ==> Just Int' - AddFun True "*" $ [< Int', Int'] ==> Just Int' - AddFun False "-" $ [< Int'] ==> Just Int' - AddFun True "<" $ [< Int', Int'] ==> Just Bool' - AddFun True "<=" $ [< Int', Int'] ==> Just Bool' - AddFun True "==" $ [< Int', Int'] ==> Just Bool' - AddFun True "or" $ [< Bool', Bool'] ==> Just Bool' - AddFun True "and" $ [< Bool', Bool'] ==> Just Bool' - AddFun False "not" $ [< Bool'] ==> Just Bool' - AddFun False "print" $ [< Int'] ==> Nothing + AddFun True True "+" $ [< Int', Int'] ==> Just Int' + AddFun True True "*" $ [< Int', Int'] ==> Just Int' + AddFun False True "-" $ [< Int'] ==> Just Int' + AddFun True True "<" $ [< Int', Int'] ==> Just Bool' + AddFun True True "<=" $ [< Int', Int'] ==> Just Bool' + AddFun True True "==" $ [< Int', Int'] ==> Just Bool' + 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 -supportedLanguages : SortedMap String (NamedCtxt, PP) +supportedLanguages : SortedMap String (l : SupportedLanguage ** (NamedCtxt l, PP l)) supportedLanguages = fromList - [ ("scala3", scala3StdFuns, printScala3) - , ("lua5.4", lua5_4StdFuns, printLua5_4) + [ ("scala3", (Scala3 ** (scala3StdFuns, printScala3))) + , ("lua5.4", (Lua5_4 ** (lua5_4StdFuns, printLua5_4))) ] --------------- @@ -170,7 +168,7 @@ main = do let [lang] = nonOptions | [] => die "no language is given, supported languages: \{langs}\n\{usage}" | many => die "too many languages are given\n\{usage}" - let Just (ctxt, pp) = lookup lang supportedLanguages + let Just (_ ** (ctxt, pp)) = lookup lang supportedLanguages | Nothing => die "unknown language \{lang}, supported languages \{langs}\n\{usage}" let config = foldl (flip apply) defaultConfig options From 851ae3f73953521c39195b4efb0f741cf1b81253 Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Mon, 28 Oct 2024 14:31:36 +0300 Subject: [PATCH 10/12] Introduce Idris2 support back to the Runner --- examples/pil-fun/src/Runner.idr | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/examples/pil-fun/src/Runner.idr b/examples/pil-fun/src/Runner.idr index 7eba35225..6955ba8f2 100644 --- a/examples/pil-fun/src/Runner.idr +++ b/examples/pil-fun/src/Runner.idr @@ -11,6 +11,7 @@ import Language.PilFun.Pretty.Derived import Language.PilFun.Pretty.DSL import Language.PilFun.Pretty.Scala3 import Language.PilFun.Pretty.Lua5_4 +import Language.PilFun.Pretty.Idris2 import Test.DepTyCheck.Gen @@ -144,10 +145,25 @@ lua5_4StdFuns = do AddFun False False "print" $ [< Int'] ==> Nothing Enough +idris2StdFuns : NamedCtxt Idris2 +idris2StdFuns = do + 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 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) + Enough + supportedLanguages : SortedMap String (l : SupportedLanguage ** (NamedCtxt l, PP l)) supportedLanguages = fromList [ ("scala3", (Scala3 ** (scala3StdFuns, printScala3))) , ("lua5.4", (Lua5_4 ** (lua5_4StdFuns, printLua5_4))) + , ("idris2", (Idris2 ** (idris2StdFuns, printIdris2))) ] --------------- From be10da94c3fb508dc1b4b14292b14d2910076ce9 Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Mon, 28 Oct 2024 16:41:17 +0300 Subject: [PATCH 11/12] Fixed print rare occurrences; Added missing reserved idris2 operator --- examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr | 8 ++++---- examples/pil-fun/src/Runner.idr | 10 +++++----- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr index e491a7b6a..1e2c0eaed 100644 --- 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 index 6955ba8f2..3beb96a9e 100644 --- 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)) From 4a5ae49e897bb5be7935f5f6fa681f9a37c44d10 Mon Sep 17 00:00:00 2001 From: Gleb Krasilich Date: Mon, 28 Oct 2024 16:57:36 +0300 Subject: [PATCH 12/12] Regenerated test filles --- examples/pil-fun/tests/gens/scala3/expected | 370 ++++++++++++++------ 1 file changed, 255 insertions(+), 115 deletions(-) diff --git a/examples/pil-fun/tests/gens/scala3/expected b/examples/pil-fun/tests/gens/scala3/expected index 3805de0cc..8ef967d7d 100644 --- a/examples/pil-fun/tests/gens/scala3/expected +++ b/examples/pil-fun/tests/gens/scala3/expected @@ -2,168 +2,308 @@ @main -def mnsa(): Unit = { - if true.||(false.||(false)) then { - var fdzhrrhm: Boolean = true - val adzbd = (nrhvs: Int, xrjrwx: Boolean) => { - var juaggj: Boolean = false - var f = (nrhvs.*(nrhvs)).+(3.*(0)) - fdzhrrhm = 4.<(f.*(0)) - - } : Unit - extension (mngs: Int) - def c(dkvkpmkzgs: Boolean, i: Boolean, bjihb: Boolean) = { - fdzhrrhm = 2.<=(mngs.*(-(mngs))) - extension (qs: Boolean) - def ye(yz: Boolean, wuxaq: Int, en: Boolean, f: Boolean): Boolean = - wuxaq <= wuxaq - - } - val e = (h: Int, rjmijkncbq: Boolean, ojdrz: Int, jfhtsyzw: Int) => - (0 * 5) * (4.*(1)) - - } else { - val hqwnmbq: Int = (-(0)) * (5.+(2)) - def hdoup(a: Boolean, ccciiux: Int, rgaqgckocj: Boolean, xrcubtog: Int, esgwvqqvj: Boolean, x: Int) = - val pmdvj = (ws: Int, m: Int) => { - if ccciiux.<=(3 * ccciiux) then { - extension (qprxvr: Int) def z(ey: Boolean) = { 3 } - - } else { - val jhthzccdm = (4.==(4)) || rgaqgckocj - - } - val rwbc: Int = (x.*(2)) * m +def ltpic(): Unit = { + if 5 == (5.+(-(0))) then + val s = (4.+(4)).*(6.*(-(0))) + if 4 <= (0 * s) then + Console.println(3) + + else + {} + if (s * 1).==(4) then { + if 2.<(-(-(2))) then + val vztsa = (lsg: Int, qnt: Boolean, xeuwshq: Boolean, jpzgmtm: Boolean, pujqsokaog: Int, qi: Boolean) => + (pujqsokaog.*(2)) * (2.+(lsg)) - } : Unit - val utlg = (p: Int) => { - pmdvj(ccciiux, 0.*(ccciiux * 0)) + else + if (3 * 5).<=(2) then + {} - } : Unit - hqwnmbq * (x.*(-(hqwnmbq))) - if 5 <= (4.*(-(hqwnmbq))) then { + def egvcuohs(): Int = + (5 * s) * s } else { + if (s.*(s)) == (-(-(4))) then + var dtek: Boolean = 5 == (5 * (-(s))) + + else + if 1 < 5 then + {} + + var k = (6.*(s)) < (-(-(s))) } - if (-(2)) <= (4 * hqwnmbq) then - {} - extension (u: Int) def qlxoze(mreec: Boolean, mmjsrcpeqw: Boolean): Unit = { {} } : Unit + if 1 == (-(-(3))) then + if (s + 2) <= 5 then { + + } else { + + } + + val yzurw = (s.*(0)).<(-(-(s))) - } - if 0 == (4.*(-(5))) then - extension (mozthbn: Int) - def uebcvuox(xmd: Boolean, gsilgnw: Int, ecv: Int) = - if xmd || (mozthbn == (-(5))) then - if true || (2.<(2)) then - val fkmcysdfrd = xmd.||(ecv.<(-(mozthbn))) + else + var raq = (5.*(6)).<(-(5)) + extension (jyanno: Boolean) + def mmjsrcpeqw(tut: Boolean, rdazry: Int) = + if (1 * 6).<=(rdazry.*(rdazry)) then + if true then { + Console.println(rdazry * (rdazry * 0)) - else - def gia() = - {} + } else { + Console.println((-(3)).+(-(6))) + } + def b(cttc: Int, a: Int, pqvycwxbs: Int, whr: Boolean) = { } else - val jx = 0 * (6 + mozthbn) + raq = (-(rdazry)).==(-(rdazry)) + Console.println(-(-(rdazry))) - def mhqody(crdri: Int): Unit = - extension (wh: Boolean) def cocwhnb(azlde: Int, lbda: Boolean, e: Boolean, jqcyn: Int): Int = { -(crdri) } : Int - - val ieosux = () => - ecv + val xcvpw: Boolean = (rdazry.+(5)).==(rdazry.*(6)) - (-(4)).uebcvuox(3 == 0, 5 * (-(4)), -(1 * 6)) - if (1 * 0) <= (-(0)) then - if false then { - - } - + if (4.+(3)) <= (5.*(5)) then + {} else - (-(5)).uebcvuox(2 < 1, 5 * 6, (-(5)) * 5) + raq = 0 <= (4 * 6) + extension (eszncsoh: Int) + def sohllqkz(wbod: Int, wvqqvju: Boolean, x: Boolean): Boolean = + (-(wbod)).<(0.*(-(wbod))) - val jeiqv: Int = 6 + val rqay: Boolean = (2 * 5).<(0) + (2.<=(0)).mmjsrcpeqw(6.<=(-(4)), 4.*(1)) - else - var xofqxp: Boolean = (true.||(true)) || (false.||(false)) - extension (fneq: Int) - def fgcyhaxpe(o: Boolean): Int = { - val ch = (sojkbqw: Int, mdefqu: Boolean, a: Int, xemxfjaoz: Int) => - var h = sojkbqw.*(5 * (-(a))) - 6 - val zxsuzivv: Int = fneq - ch(fneq, true, -(1), 3) - } : Int - extension (ahahw: Int) - def p(tdqtckpnsx: Int, xw: Int, fwmpzhvupi: Boolean, o: Boolean, p: Boolean) = { - extension (rrrmmcqlp: Boolean) - def plqagg(et: Int, mpdscof: Boolean, kgtopycdns: Boolean): Unit = - {} - xw fgcyhaxpe (ahahw.<=(-(ahahw))) - } - xofqxp = 5 <= 0 - - val n = () => { - if (true.||(true)) || (0 == (-(5))) then { - extension (jho: Int) def fwi(juwqgswj: Boolean, nshxpnn: Int): Unit = { } : Unit - val rdszhhqhhf = (fobjrlxn: Int, ereaqyqmh: Boolean, uhobkwqyx: Boolean, s: Int, poszubn: Boolean, xejgssqh: Int) => - ((2 * 6) * (6 * (-(5)))) : Int + var pisaijht = (-(0)).<=(4 + 5) + if false then { + if true then { + pisaijht = (1 * 3) <= (2 * (-(4))) + pisaijht = true } else { + if (-(5)).==(5 + (-(3))) then { + pisaijht = pisaijht + + } else { + Console.println(4.*(1.*(0))) + + } + def djeiqvgbbg(whun: Boolean, lbn: Boolean, nvvwfj: Boolean, owgqgsil: Int) = { 3 } } - if (6 * 1).==(0.*(1)) then { + if true then + Console.println((-(4)) + (3.*(0))) + + def ioxl(uebcvuox: Int, isalquq: Boolean, duyogah: Boolean, o: Int, shnguy: Boolean, unnpimoz: Int) = + (2.*(6)) * (6 * (-(5))) + + } else { + pisaijht = (6.+(1)).==(2.*(-(2))) + if 3 <= (3 * (-(1))) then { + pisaijht = (1 * 5) < (0.*(-(4))) } else { - if false.||(false.||(true)) then + if 5.==(5) then {} else {} } - extension (x: Boolean) def vnd() = { (2 * 1) * (0.*(-(5))) } + def hojxen(dhgxdq: Boolean, rgt: Int, xbq: Int, nhqrgmmzyh: Int, ekfzq: Int, xiyxlczips: Boolean): Unit = { } - } : Unit - var h = (0.*(0)).<=(0) - def digtlljisa(yog: Int, lylptqjv: Boolean, rdjrbt: Boolean, shn: Boolean, yflaeizbbc: Int): Unit = { - n() + } + if pisaijht then + var gerrlsbc: Int = 3 + if (-(gerrlsbc)).<(5 * gerrlsbc) then { + + } + + else + pisaijht = (-(6)) <= 1 + Console.println((-(6)) * (6 * 6)) - } - n() } ------------------- -val mfusqmki: Int = (0 * 4).*(0.*(3)) -var gfknyi = true || (true.||(false)) @main -def u(): Unit = { +def sgieoz(): Unit = { + if 3 == (0.+(-(2))) then { + if (1.*(3)) <= 0 then + Console.println(3) + if false then { + + } else { + var zbzyduovm: Boolean = (6 * 0).<=(0.*(-(0))) + def cogci(hfczjsf: Int, apwdzgs: Boolean, ptfihqq: Int): Int = { hfczjsf * (6.*(-(hfczjsf))) } + + } + val rx = 1.*(2 * (-(0))) + var iuesckliu: Int = (4.*(rx)) * 1 + + else + Console.println((-(4)).*(0)) + val rvxbpfyynu = (rsvjos: Int, ikhn: Int, rgnq: Int, jbircjmehe: Int) => { + extension (brej: Boolean) + def cimhsnfho(gmpsvvdk: Int, wiajyefeuk: Boolean) = { + if brej then { + + } else { + + } + + } + var l: Int = (ikhn * 4).*(rgnq) + + } + val cxsjf = (wtonjtgcne: Boolean, vikzzcbnv: Int, rlanw: Boolean, xyecvjwqz: Boolean, gx: Boolean, cbauzpb: Boolean) => { {} } : Unit + var ybtomym: Boolean = (6.*(0)) < (6 * (-(0))) + + extension (icpkbfkc: Int) + def oslkymdjd(opieb: Int, dmm: Int) = + var uga: Int = (icpkbfkc.*(5)).*(icpkbfkc) + uga = -(0 * icpkbfkc) + if (0.*(icpkbfkc)) <= icpkbfkc then + {} + else + {} + + if (-(2)) < (4 + (-(3))) then + if (-(3)) <= (-(-(1))) then + 5.oslkymdjd(4 * (-(0)), -(4 * 3)) + + Console.println(-(1 + 3)) + + else + Console.println(6 * 2) + var imvazbtyk: Int = (1 + 1) + (3.*(3)) + + (3.*(2)).oslkymdjd(4.*(-(0)), 1 + (-(3))) + (0.*(6)).oslkymdjd(2 * 4, 0) + + } else { + Console.println((-(3)).+(5.*(6))) + var ry: Boolean = (2 * 6) == 5 + ry = (1.*(4)).==(5.*(0)) + ry = (-(3)) == (4 + (-(4))) + if (0.*(4)).==(6) then + {} + else + {} + + } + val k = (6.+(6)) <= (4.*(6)) } ------------------- -val qdwuca: Int = (6.*(0)).*(0 * 5) -def nzq(gptfihqq: Int, yzhcxeauia: Int, stlw: Boolean): Unit = { - val cpkbfkcuo = 0 - -} -var smzjwfuprm = 5.<(6) +val aa = (wa: Int, nrgydimrbn: Int, eioalbfmhk: Int, odvsmyt: Int, d: Boolean) => { + if (wa + wa) == (eioalbfmhk.+(0)) then { + Console.println(wa.*(1)) + Console.println(-(nrgydimrbn.*(4))) + val qnkfzi: Int = 1 + val ziciefv = (ygoemy: Boolean, fkcwflab: Int, ocfrdy: Int, kir: Int, dlxrzk: Int) => { {} } : Unit + + } else { + if 1 < wa then { + Console.println(wa.*(2)) + Console.println(5) + + } else { + if wa.<=(odvsmyt) then { + Console.println(6.*(odvsmyt * 6)) + + } else { + Console.println((-(6)) * (-(odvsmyt))) + if (eioalbfmhk.+(wa)).<=(0.*(-(eioalbfmhk))) then { + + } else { + + } + + } + + } + def ea(): Unit = + if (4 * wa).<(5) then + var vpkegepjjn = (6.*(eioalbfmhk)) * wa + + else + Console.println(0) + + val ghh = d + + extension (zhlqmpiw: Boolean) + def ywebthud(fbcyq: Boolean, uykfht: Int, ghotg: Boolean, yey: Boolean): Int = + (1 * uykfht).+(uykfht.*(odvsmyt)) + + } + Console.println((-(eioalbfmhk)).+(-(5))) + val hcnf = (kwhyj: Int, ccdqhntypz: Boolean, b: Int, jq: Int, ifwmyvedi: Int, nzekacnbt: Int) => + Console.println((-(kwhyj)).*(2)) + var w = kwhyj.==(2.+(-(6))) + 2 + Console.println(4) + val qldfxdq = nrgydimrbn + wa + -(0) +} : Int @main -def ptziubj(): Unit = { - if qdwuca == (qdwuca.*(3)) then - val afqw = (qdwuca + qdwuca).*(qdwuca * (-(qdwuca))) - smzjwfuprm = qdwuca.<=(0) +def rqiuzwbjav(): Unit = { + if (5.+(2)).<=(2 + (-(1))) then { + if (4 * 3) < (3.*(1)) then { + Console.println((-(6)) * (6 * 5)) + + } else { + if (2.*(0)).<(2 * (-(5))) then + Console.println((-(4)).+(1.*(5))) + + else + if (6.*(0)).<(-(-(6))) then + if (5.*(5)).<=(3.+(1)) then + {} + + else + val x = false + + + Console.println((-(2)).*(4.*(4))) + Console.println((-(4)).*(3 * 4)) + + } + Console.println(3 + (0.*(0))) + def dpr() = { } + + } + extension (t: Int) + def ysjxsox(z: Boolean) = { + Console.println(0.*(t * t)) + var bs = aa(6, 1, -(t), t, 6.<=(2)) + 1 < t + } + if (-(4)).ysjxsox(2 < (-(5))) then + Console.println((-(0)) + (-(3))) + var nagar = (3.*(2)) < (1 * 0) else - val fmdn = qdwuca * qdwuca - def zilrhuky(ovmiu: Boolean, jtdachxqn: Boolean, hsw: Int, czjsfl: Int): Boolean = { false } + extension (d: Boolean) + def wbvyjvgcq(xto: Boolean, sejwopjk: Boolean, vdggfvogi: Boolean, fy: Boolean, bsifubv: Boolean) = + Console.println(1) + (6 * 0).ysjxsox(4.ysjxsox(false)) + val cqwo = (miilc: Int) => { {} } : Unit - nzq(4 * qdwuca, 3, smzjwfuprm) - if (qdwuca.*(qdwuca)) <= (qdwuca.*(-(3))) then { + if 5 < (4.*(1)) then { + if (4.*(4)).<(0 + (-(1))) then { + + } else { + + } } else { + if 3 < (5.+(3)) then + {} } + var qmlipxuzy: Int = aa(1, 4, -(4), 0 * 5, 2.ysjxsox(true)) }