Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Idris2 pretty printer initial support #208

Open
wants to merge 12 commits into
base: master
Choose a base branch
from
8 changes: 8 additions & 0 deletions examples/pil-fun/src/Language/PilFun.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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) ->
Expand Down
123 changes: 80 additions & 43 deletions examples/pil-fun/src/Language/PilFun/Pretty.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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:<fun) vars
NewVar : (ss : UniqNames funs vars) => (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:<fun} {vars} (NewFun @{ss} {isInfix} s @{sub} @{infixCond}) x
V : (0 _ : So $ x /= s) -> 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 === ([<a, b] ==> 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
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you please put where in the line with data if it fits the line length

[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:<fun) vars
NewVar : (ss : UniqNames l funs vars) => (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:<fun) vars (NewFun @{ss} {isInfix} {isPure} s @{sub} @{infixCond}) x
V : (0 _ : So $ x /= s) -> 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)
Comment on lines +76 to +78
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please put l after auto-implicits, it's better for auto-implicits that do not depend on other arguments to go first


export
genNewName : Fuel -> (Fuel -> Gen MaybeEmpty String) =>
genNewName : {l : SupportedLanguage} -> Fuel -> Gen MaybeEmpty String ->
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it so nesessary to make existing Fuel -> Gen MaybeEmpty String argument to be not-autoimplicit? It's okay in case when every or almost every usage needs to set this explicitly, but it this the case? I see that in some places alphaNames are used, but it seems that in other cases auto-implicit still can be used. Am I wrong?

Additionally, please, put l after the fuel and auto-implicits to make all generators' signatures to look more or less uniformly

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
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe, signatures of existing projection functions like varName, funName and isFunInfix should be changed like in this function, i.e. passing UniqNames explicitly

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:<v) names = do
(names', vts) <- newVars fl vs names
(nm ** _) <- genNewName fl _ _ names'
(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 newNames (vs:<v) names = do
(names', vts) <- newVars fl newNames vs names
(nm ** _) <- genNewName {l} fl newNames _ _ names'
pure (NewVar @{names'} nm, (nm, v)::vts)

isNop : Stmts funs vars retTy -> Bool
Expand All @@ -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
22 changes: 12 additions & 10 deletions examples/pil-fun/src/Language/PilFun/Pretty/DSL.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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:<fun) vars $ NewFun @{names} {isInfix} {fun} s
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) =>
NamedCtxt l
AddFun isInfix isPure s fun $ MkNamedCtxt funs vars names = MkNamedCtxt (funs:<fun) vars $ NewFun @{names} {isInfix} {isPure} {fun} {languageCondition = lCond} s

public export %inline
(>>) : {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
Loading