From 426cd8eb553cf8caa5f4ab5d9b7032e2b31531bf Mon Sep 17 00:00:00 2001 From: Mikhail Lavrentiev Date: Fri, 25 Oct 2024 19:45:14 +0300 Subject: [PATCH] [ example ] Add Lua5.4 pretty printer to `pil-fun` --- .../src/Language/PilFun/Pretty/Lua5_4.idr | 182 ++++++++++++ examples/pil-fun/src/Runner.idr | 18 ++ examples/pil-fun/tests/gens/scala3/expected | 262 +++++++++--------- 3 files changed, 332 insertions(+), 130 deletions(-) create mode 100644 examples/pil-fun/src/Language/PilFun/Pretty/Lua5_4.idr diff --git a/examples/pil-fun/src/Language/PilFun/Pretty/Lua5_4.idr b/examples/pil-fun/src/Language/PilFun/Pretty/Lua5_4.idr new file mode 100644 index 000000000..e2c801037 --- /dev/null +++ b/examples/pil-fun/src/Language/PilFun/Pretty/Lua5_4.idr @@ -0,0 +1,182 @@ +module Language.PilFun.Pretty.Lua5_4 + +import Data.Fuel +import Data.List +import Data.Maybe +import Data.SnocList +import Data.Vect + +import public Language.PilFun +import public Language.PilFun.Pretty + +import Test.DepTyCheck.Gen + +import public Text.PrettyPrint.Bernardy + +%default total + +printTy : Ty -> Doc opts +printTy Int' = "number" +printTy Bool' = "boolean" + +NamesRestrictions where + reservedKeywords = fromList + [ "and", "break", "do", "else", "elseif", "end" + , "false", "for", "function", "goto", "if", "in" + , "local", "nil", "not", "or", "repeat", "return" + , "then", "true", "until", "while" + ] + +Priority : Type +Priority = Fin 12 + +priorities : List (String, Priority) +priorities = [ ("or", 11) + , ("and", 10) + , ("<", 9), (">", 9), ("<=", 9), (">=", 9), ("~=", 9), ("==", 9) + , ("|", 8) + , ("~", 7) + , ("&", 6) + , ("<<", 5), (">>", 5) + , ("..", 4) + , ("+", 3), ("-", 3) + , ("*", 2), ("/", 2), ("//", 2), ("%", 2) + , ("not", 1), ("#", 1), ("-", 1), ("~", 1) + , ("^", 0) + ] + +priority : String -> Maybe Priority +priority func = lookup func priorities + +printExpr : {funs : _} -> {vars : _} -> {opts : _} -> + (names : UniqNames funs vars) => + Fuel -> + (lastPriority : Maybe Priority) -> + Expr funs vars ty -> Gen0 $ Doc opts +printFunCall : {funs : _} -> {vars : _} -> {opts : _} -> + (names : UniqNames funs vars) => + Fuel -> + (lastPriority : Maybe Priority) -> + IndexIn funs -> ExprsSnocList funs vars argTys -> + Gen0 $ Doc opts +printStmts : {funs : _} -> {vars : _} -> {retTy : _} -> {opts : _} -> + (names : UniqNames funs vars) => + (newNames : Gen0 String) => + Fuel -> + Stmts funs vars retTy -> Gen0 $ Doc opts + +printExpr fuel _ (C $ I x) = pure $ line $ show x +printExpr fuel _ (C $ B True) = pure "true" +printExpr fuel _ (C $ B False) = pure "false" +printExpr fuel _ (V n) = pure $ line $ varName {funs} n +printExpr fuel lastPrior (F n x) = printFunCall fuel lastPrior n x + +addCommas : {opts : _} -> List (Doc opts) -> List (Doc opts) +addCommas [] = [] +addCommas [x] = [x] +addCommas (x::xs) = (x <+> comma) :: addCommas xs + +printFunCall fuel lastPrior fun args = do + let name = funName {vars} fun + let thisPrior = priority name + let addParens = !(chooseAnyOf Bool) + || isJust lastPrior && thisPrior >= lastPrior + args' <- for (toList $ getExprs args) (\(Evidence _ e) => assert_total printExpr fuel Nothing e) + case (isFunInfix @{names} fun, args') of + (True, [lhv, rhv]) => do + pure $ parenthesise addParens $ hangSep 2 (lhv <++> line name) rhv + (_, [x]) => do + -- note: two minus signs may be interpreted as a comment + pure $ parenthesise addParens $ line name + <+> when (name == "not" || name == "-") space + <+> x + (_, _) => do + let argsWithCommas = sep' $ addCommas args' + let applyShort = line name <+> "(" <+> argsWithCommas <+> ")" + let applyLong = vsep [ line name <+> "(" + , indent 2 argsWithCommas + , ")" + ] + pure $ ifMultiline applyShort applyLong + +newVarLhv : {opts : _} -> (name : String) -> (mut : Mut) -> Gen0 $ Doc opts +newVarLhv name mut = do + let attr = case mut of + Mutable => empty + Immutable => space <+> angles "const" + pure $ "local" <++> line name <+> attr + +withCont : {opts : _} -> (cont : Doc opts) -> (stmt : Doc opts) -> Gen0 (Doc opts) +withCont cont stmt = + pure $ stmt `vappend` cont + +printStmts fuel (NewV ty mut initial cont) = do + (name ** _) <- genNewName fuel _ _ 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 + let funArgs' = reverse (toList funArgs) + let argHints = funArgs' <&> \(name, ty) => + the (Doc opts) "---@param" <++> line name <++> printTy ty + let hints = vsep $ case sig.To of + Just retTy => argHints ++ ["---@return" <++> printTy retTy] + Nothing => argHints + let argNames = funArgs' <&> \(name, _) => the (Doc opts) (line name) + let argList = sep' $ addCommas argNames + let fnHeaderShort = "local" <++> "function" <++> (line name) <+> + "(" <+> argList <+> ")" + let fnHeaderLong = vsep [ "function" <++> (line name) <+> "(" + , indent 2 argList + , ")" + ] + let fnHeader = ifMultiline fnHeaderShort fnHeaderLong + fnBody <- printStmts @{localNames} fuel body + cont' <- printStmts fuel cont + withCont cont' $ vsep [ hints + , fnHeader + , indent' 2 fnBody + , "end" + ] + +printStmts fuel ((#=) lhv rhv cont) = do + let lhv' = line (varName {funs} lhv) <++> "=" + rhv' <- printExpr fuel Nothing rhv + withCont !(printStmts fuel cont) $ hangSep' 2 lhv' rhv' + +printStmts fuel (If cond th el cont) = do + cond' <- printExpr fuel Nothing cond + th' <- printStmts fuel th + let skipElse = isNop el && !(chooseAnyOf Bool) + el' <- if skipElse + then pure empty + else do + body <- printStmts @{names} @{newNames} fuel el + pure $ "else" `vappend` indent' 2 body + let top = hangSep 0 ("if" <++> cond') "then" + withCont !(printStmts fuel cont) $ vsep + [ top + , indent' 2 th' + , el' + , "end" + ] + +printStmts fuel (Call n x cont) = do + call <- printFunCall fuel Nothing n x + withCont !(printStmts fuel cont) call + +printStmts fuel (Ret res) = + pure $ "return" <++> !(printExpr fuel Nothing res) + +printStmts fuel Nop = do + useSemicolon <- chooseAnyOf Bool + if useSemicolon + then pure ";" + else pure empty + +export +printLua5_4 : PP +printLua5_4 fl = printStmts {names} {newNames} fl diff --git a/examples/pil-fun/src/Runner.idr b/examples/pil-fun/src/Runner.idr index 4e8c1412b..413908f1b 100644 --- a/examples/pil-fun/src/Runner.idr +++ b/examples/pil-fun/src/Runner.idr @@ -10,6 +10,7 @@ import Language.PilFun.Derived import Language.PilFun.Pretty.Derived import Language.PilFun.Pretty.DSL import Language.PilFun.Pretty.Scala3 +import Language.PilFun.Pretty.Lua5_4 import Test.DepTyCheck.Gen @@ -120,6 +121,8 @@ run conf ctxt pp = do scala3StdFuns : NamedCtxt 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' @@ -129,9 +132,24 @@ scala3StdFuns = do AddFun False "Console.println" $ [< Int'] ==> Nothing Enough +lua5_4StdFuns : NamedCtxt +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 + Enough + supportedLanguages : SortedMap String (NamedCtxt, PP) supportedLanguages = fromList [ ("scala3", scala3StdFuns, printScala3) + , ("lua5.4", lua5_4StdFuns, printLua5_4) ] --------------- diff --git a/examples/pil-fun/tests/gens/scala3/expected b/examples/pil-fun/tests/gens/scala3/expected index 7e594f27c..3805de0cc 100644 --- a/examples/pil-fun/tests/gens/scala3/expected +++ b/examples/pil-fun/tests/gens/scala3/expected @@ -2,166 +2,168 @@ @main -def tvlt(): Unit = { - if (5.+(0)) < (2.+(2)) then { - var lybokfpr = (4.+(5)).+(4.+(5)) - lybokfpr = lybokfpr - lybokfpr = 4.+(lybokfpr + 1) - lybokfpr = lybokfpr - var uo: Boolean = (lybokfpr + lybokfpr).==(3 + 0) +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 qemiujv = (jjh: Int, gxdtmng: Int, zdkvk: Int, n: Int, zadrbgu: Boolean) => { - if (jjh + n) == zdkvk then - extension (cuohsl: Int) - def zmuqm(lnevjvz: Boolean, ssl: Int, ltiv: Int): Int = { - if (true.&&(true)).||(zadrbgu) then - if lnevjvz.&&(false && (!(zadrbgu))) then - {} - - else - if (ltiv.==(zdkvk)) || (ssl.<(4)) then - {} - else - {} - - (ssl.+(5)) + (n.+(6)) - } : Int + 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 - else - extension (r: Int) - def mrew(nbasrya: Int, jqaak: Boolean, jpinulqg: Boolean, kazmm: Boolean) = - {} - def qsokaogqmr() = { } + } : Unit + val utlg = (p: Int) => { + pmdvj(ccciiux, 0.*(ccciiux * 0)) - val mbn = jjh.+(1) - val ltpicdael: Int = 6 - var woyvgazf: Int = (4 + 0).+(6 + n) + } : Unit + hqwnmbq * (x.*(-(hqwnmbq))) + if 5 <= (4.*(-(hqwnmbq))) then { - } : Unit - if (3 == 1) && (0.==(4)) then - if (2 + 1).==(1 + 2) then - extension (r: Int) def naqxvjgxmb() = { 4 <= (r + 1) } - qemiujv(1, 6, 5.+(4), 4.+(0), (1.naqxvjgxmb()).||(false.||(true))) - - else - if false then - {} - else - if true.||(false && false) then { + } else { + + } + if (-(2)) <= (4 * hqwnmbq) then + {} + extension (u: Int) def qlxoze(mreec: Boolean, mmjsrcpeqw: Boolean): Unit = { {} } : Unit + + } + 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 + def gia() = + {} - } - var wf: Boolean = (2.+(2)).<(2 + 2) - - extension (xmfo: Boolean) - def qnog(jg: Boolean, tzmk: Int, ogkzgnyugn: Int, bzyegcnug: Int) = { - qemiujv(3, 0, 0, tzmk.+(6), 5 < (tzmk + 6)) + else + val jx = 0 * (6 + mozthbn) - } + def mhqody(crdri: Int): Unit = + extension (wh: Boolean) def cocwhnb(azlde: Int, lbda: Boolean, e: Boolean, jqcyn: Int): Int = { -(crdri) } : Int + + val ieosux = () => + ecv + + (-(4)).uebcvuox(3 == 0, 5 * (-(4)), -(1 * 6)) + if (1 * 0) <= (-(0)) then + if false then { + + } else - var yqavod = false && true - qemiujv(6, 0, 0.+(4), 4.+(1), yqavod || (yqavod && yqavod)) - val sxfdzhrrh = (zbdd: Boolean, acoykh: Boolean, cbde: Boolean, dngc: Boolean, bqf: Boolean, drzqpmieuq: Boolean) => - {} + (-(5)).uebcvuox(2 < 1, 5 * 6, (-(5)) * 5) - if false || (2 <= 4) then - val obaztbbz: Boolean = (1.+(2)).==(2 + 6) + val jeiqv: Int = 6 + + 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 - else - val ji: Boolean = (2 + 4).==(0.+(1)) - val xsjzzhjk = (rbjd: Boolean, msoanazo: Int, dbbygddcsy: Boolean, j: Int, ots: Boolean, axwjjdtw: Boolean) => { } + } else { + } + if (6 * 1).==(0.*(1)) then { + + } else { + if false.||(false.||(true)) then + {} + else + {} + + } + extension (x: Boolean) def vnd() = { (2 * 1) * (0.*(-(5))) } + + } : Unit + var h = (0.*(0)).<=(0) + def digtlljisa(yog: Int, lylptqjv: Boolean, rdjrbt: Boolean, shn: Boolean, yflaeizbbc: Int): Unit = { + n() - } - val jrqa: Boolean = !(false) - extension (yannoshffy: Int) - def kwc(qnbouij: Int, mtsapbnquq: Int): Unit = - var k: Boolean = true - k = !(!(!(jrqa))) - - val llqkzrga = (deszncso: Boolean, dtwbodm: Boolean, wvqqvju: Boolean) => { - var x = (wvqqvju.&&(true)).||(4 == 5) - x = true - (6.+(3)).+(0.+(1)) } + n() } ------------------- -val kwyflaeizb = (0.+(5)).+(3.+(5)) -val wfjunn = kwyflaeizb.+(kwyflaeizb + kwyflaeizb) -var lisrdrrgc: Int = 4.+(1) -val bh = (agieo: Boolean, qazggfrct: Int) => - if (0.<=(3)) && (!(false)) then { - var fwiklya = lisrdrrgc - - } else { - extension (psmyvssee: Int) def kmcysd(mc: Boolean, m: Int, kpwfobj: Int, g: Boolean, sk: Boolean) = { } - - } - lisrdrrgc = (kwyflaeizb + qazggfrct).+(kwyflaeizb.+(5)) - 6 -val qrnqnfy = (yovn: Boolean, t: Boolean) => { - if (true.||(yovn)) || yovn then { - - } - yovn -} +val mfusqmki: Int = (0 * 4).*(0.*(3)) +var gfknyi = true || (true.||(false)) @main -def chojxe(): Unit = { - if 1 < (kwyflaeizb.+(5)) then - {} - else - {} +def u(): Unit = { } ------------------- -extension (xirzqm: Boolean) - def efqu(): Unit = - val tmxsbu = (5 == 6) && (!(false)) - var xnzeyxyo: Boolean = 4 == (3 + 4) - extension (kg: Boolean) - def doxdnly() = { - if (1.+(5)).<=(5 + 4) then { - xnzeyxyo = true - - } - if true then - {} - else - {} - - } - var drjp: Boolean = (0 == 0).||(xirzqm && false) - if tmxsbu && (tmxsbu && false) then { - - } - -var cstczqacp = (0 + 3) == (5 + 5) +val qdwuca: Int = (6.*(0)).*(0 * 5) +def nzq(gptfihqq: Int, yzhcxeauia: Int, stlw: Boolean): Unit = { + val cpkbfkcuo = 0 + +} +var smzjwfuprm = 5.<(6) @main -def japky(): Unit = { - if cstczqacp then { - (4 < (0.+(1))).efqu() - extension (faco: Boolean) - def f(vunluob: Int, xgriaerel: Boolean, rhn: Boolean, ffmlvduuc: Boolean, l: Boolean): Unit = { - (5.==(vunluob)).efqu() - - } : Unit - val tkhyrdnc = () => { (0.+(0)).==(3) } : Boolean +def ptziubj(): Unit = { + if qdwuca == (qdwuca.*(3)) then + val afqw = (qdwuca + qdwuca).*(qdwuca * (-(qdwuca))) + smzjwfuprm = qdwuca.<=(0) + + else + val fmdn = qdwuca * qdwuca + def zilrhuky(ovmiu: Boolean, jtdachxqn: Boolean, hsw: Int, czjsfl: Int): Boolean = { false } + + nzq(4 * qdwuca, 3, smzjwfuprm) + if (qdwuca.*(qdwuca)) <= (qdwuca.*(-(3))) then { } else { - var gfknyi: Int = (1.+(3)) + (5.+(6)) - var quusqeb = (4 + 4) + (gfknyi.+(2)) - cstczqacp.efqu() } - var cyopq: Int = (0 + 2) + (3 + 2) - cstczqacp = cstczqacp && (true.&&(cstczqacp)) - val ycchap: Boolean = false }