diff --git a/examples/pil-fun/src/Language/PilFun.idr b/examples/pil-fun/src/Language/PilFun.idr index 46e670b6..140bdedf 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 @@ -193,6 +198,8 @@ data Expr : Funs -> Vars -> Ty -> Type where Expr funs vars ty F : (n : IndexIn funs) -> + {from : _} -> + {to : _} -> AtIndex n (from ==> Just to) => ExprsSnocList funs vars from -> Expr funs vars to @@ -231,6 +238,7 @@ data Stmts : (funs : Funs) -> Stmts funs vars retTy Call : (n : IndexIn funs) -> + {from : _} -> AtIndex n (from ==> Nothing) => ExprsSnocList funs vars from -> (cont : 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 98d4bdaa..86762e67 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty.idr @@ -19,72 +19,110 @@ import System.Random.Pure.StdGen %default total public export -data UniqNames : Funs -> Vars -> Type +data SupportedLanguage = Scala3 + | Idris2 + | Lua5_4 + +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 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 IdrisCondition : FunSig -> (isInfix : Bool) -> (isPure : Bool) -> Type + where + 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 +public export +data NameIsNew : (l : SupportedLanguage) -> (funs : Funs) -> (vars : Vars) -> UniqNames l funs vars -> String -> Type + +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 + NewFun : (ss : UniqNames l funs vars) => (s : String) -> (0 _ : NameIsNew l funs vars ss s) => + {default False isInfix : Bool} -> {default False isPure : Bool} -> + (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 : 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: 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 : 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 : Fuel -> (Fuel -> Gen MaybeEmpty String) => +genNewName : {l : SupportedLanguage} -> Fuel -> Gen MaybeEmpty String -> NamesRestrictions => - (funs : Funs) -> (vars : Vars) -> (names : UniqNames funs vars) -> - Gen MaybeEmpty (s ** NameIsNew names s) -genNewName fl @{genStr} funs vars names = do - nn@(nm ** _) <- rawNewName fl @{genStr} vars funs names + (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 @{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 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 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 => - {funs : _} -> {vars : _} -> +newVars : NamesRestrictions => + {l : _} -> {funs : _} -> {vars : _} -> Fuel -> - (extraVars : _) -> UniqNames funs vars -> - Gen0 (UniqNames funs (vars ++ extraVars), Vect extraVars.length (String, Ty)) -newVars _ [<] names = pure (names, []) -newVars fl (vs: + (extraVars : _) -> UniqNames l funs vars -> + Gen0 (UniqNames l funs (vars ++ extraVars), Vect extraVars.length (String, Ty)) +newVars _ _ [<] names = pure (names, []) +newVars fl newNames (vs: Bool @@ -104,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/DSL.idr b/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr index 29f98f20..de43e7c1 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr @@ -7,24 +7,26 @@ import public Language.PilFun.Pretty %default total public export -record NamedCtxt where +record NamedCtxt (l : SupportedLanguage) where constructor MkNamedCtxt functions : Funs variables : Vars - fvNames : UniqNames functions variables + fvNames : UniqNames l functions variables public export %inline -AddFun : (isInfix : Bool) -> (s : String) -> (fun : FunSig) -> - (0 _ : So $ not isInfix || fun.From.length >= 1) => - (ctx : NamedCtxt) -> - (0 _ : NameIsNew ctx.fvNames s) => - NamedCtxt -AddFun isInfix s fun $ MkNamedCtxt funs vars names = MkNamedCtxt (funs: (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) => + NamedCtxt l +AddFun isInfix isPure 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 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 -Enough : NamedCtxt +Enough : NamedCtxt l Enough = MkNamedCtxt [<] [<] 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 00000000..1e2c0eae --- /dev/null +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Idris2.idr @@ -0,0 +1,226 @@ +module Language.PilFun.Pretty.Idris2 + +import Data.Alternative +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 + +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"] + +alphaNames : Gen0 String +alphaNames = pack <$> listOf {length = choose (1,10)} (choose ('a', 'z')) + +infixNames : Gen0 String +infixNames = flip suchThat (not . isPrefixOf "--") $ pack <$> listOf {length = choose (1,4)} (elements + [':', '+', '-', '*', '\\', '/', '=', '.', '?', '|', '&', '>', '<', '!', '@', '$', '%', '^', '~', '#']) + +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 : _} -> {from : _} -> {to : _} -> {opts : _} -> + (names : UniqNames Idris2 funs vars) => + (n : IndexIn funs) -> + (ati : AtIndex 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 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 + 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 {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) + pure finalDoc + +printStmts : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> + (names : UniqNames Idris2 funs vars) => + Fuel -> + Stmts funs vars retTy -> Gen0 $ Doc 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 <++> ":" <++> printTy ty <++> "=" + rhs <- printExpr initial + 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 <++> ":" <++> "IORef" <++> printTy ty <++> "<-" + 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 {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 _ (JustNew @{names} nm) + let prerparedArgs = hsep $ reverse (toList funArgs) <&> \(n, t) => line n + 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 + 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 : PP Idris2 +printIdris2 fl stmts = do + pure $ vsep ["module Main", + "", + "import Data.IORef", + "", + "main : IO ()", + "main = do", + indent' 2 $ !(printStmts fl stmts)] 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 e2c80103..400dca20 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 b61fec4d..4e5c6535 100644 --- a/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Scala3.idr @@ -43,11 +43,14 @@ NamesRestrictions where , "@" , "=>>" , "?=>" ] +namesGenScala : Gen0 String +namesGenScala = pack <$> listOf {length = choose (1,10)} (choose ('a', 'z')) + 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 +73,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 -> @@ -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 @@ -100,7 +103,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) -> @@ -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 ** 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 - (namesInside, funArgs) <- newVars fl _ names + 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 newNames _ names brBody <- chooseAny funBody <- if brBody then printStmts @{namesInside} fl False body @@ -170,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 413908f1..3beb96a9 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 @@ -98,18 +99,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 +117,53 @@ 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 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' + 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' 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 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' + 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' + 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 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') 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))) + , ("idris2", (Idris2 ** (idris2StdFuns, printIdris2))) ] --------------- @@ -170,7 +184,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 diff --git a/examples/pil-fun/tests/gens/scala3/expected b/examples/pil-fun/tests/gens/scala3/expected index 3805de0c..8ef967d7 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)) }