Skip to content

Commit 731ac04

Browse files
flupeflupe
committed
add prettyprinting to sexpr
1 parent 4204456 commit 731ac04

File tree

3 files changed

+199
-2
lines changed

3 files changed

+199
-2
lines changed

‎agda2lambox.cabal‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,12 +33,14 @@ executable agda2lambox
3333
LambdaBox.Env,
3434
LambdaBox,
3535
CoqGen,
36+
SExpr,
3637
Paths_agda2lambox
3738
autogen-modules: Paths_agda2lambox
3839
build-depends: base >= 4.10 && < 4.22,
3940
Agda >= 2.8 && < 2.9,
4041
deepseq >= 1.4.4 && < 1.6,
4142
queues >= 1.0.0 && < 1.2,
43+
sexpresso >= 1.2.5 && < 1.3,
4244
pretty-show,
4345
containers,
4446
directory,

‎src/Main.hs‎

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ import System.Console.GetOpt ( OptDescr(Option), ArgDescr(..) )
1616
import System.Directory ( createDirectoryIfMissing )
1717
import System.FilePath ( (</>) )
1818
import Data.Kind (Type)
19+
import Data.Text.Lazy.IO qualified as LText
1920

2021
import Paths_agda2lambox ( version )
2122

@@ -30,7 +31,8 @@ import Agda.Utils ( pp, hasPragma, isDataOrRecDef )
3031
import Agda2Lambox.Compile.Target
3132
import Agda2Lambox.Compile.Utils
3233
import Agda2Lambox.Compile (compile)
33-
import CoqGen ( prettyCoq )
34+
import CoqGen ( prettyCoq )
35+
import SExpr ( prettySexp )
3436
import LambdaBox.Env
3537

3638

@@ -115,10 +117,13 @@ writeModule Options{..} menv IsMain m defs = do
115117
coqMod = CoqModule env (map qnameToKName programs)
116118

117119
liftIO do
118-
putStrLn $ "Writing " <> fileName ".{v,txt}"
120+
putStrLn $ "Writing " <> fileName ".{v,txt,ast}"
119121

120122
pp coqMod <> "\n"
121123
& writeFile (fileName ".txt")
122124

123125
prettyCoq optTarget coqMod <> "\n"
124126
& writeFile (fileName ".v")
127+
128+
prettySexp optTarget coqMod <> "\n"
129+
& LText.writeFile (fileName ".ast")

‎src/SExpr.hs‎

Lines changed: 190 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,190 @@
1+
{-# LANGUAGE FlexibleInstances, FlexibleContexts, OverloadedStrings #-}
2+
{-# LANGUAGE DataKinds, MonadComprehensions, GADTs #-}
3+
-- | Converting the LambdaBox AST to s-expressions
4+
module SExpr (ToSexp, prettySexp) where
5+
6+
import Data.Bifunctor(bimap)
7+
import Data.List(intercalate)
8+
9+
import Agda.Syntax.Common.Pretty
10+
import LambdaBox
11+
import Agda.Utils.Function (applyWhen)
12+
import Agda2Lambox.Compile.Target
13+
import Data.SExpresso.SExpr
14+
import Data.SExpresso.Print.Lazy
15+
import Data.Text (Text, pack)
16+
import Data.Text.Lazy qualified as LText
17+
18+
type Exp = Sexp Atom
19+
20+
data Sexpable t = forall a. ToSexp t a => S a
21+
22+
-- | SExpr atoms.
23+
data Atom
24+
= ANode Text -- ^ An AST node (i.e a constructor name)
25+
| AInt Int -- ^ A literal integer
26+
| ABool Bool -- ^ A literal boolean
27+
| AString String -- ^ A literal bytestring
28+
29+
30+
-- | Convert to S-expression (rendered as lazy 'Data.Lazy.Text').
31+
prettySexp :: ToSexp t a => Target t -> a -> LText.Text
32+
prettySexp t = flatPrint printer . toSexp t
33+
where
34+
printer :: SExprPrinter () Atom
35+
printer = mkPrinter \case
36+
ANode kw -> kw
37+
AInt i -> pack $ show i
38+
ABool b -> if b then "true" else "false"
39+
AString str -> pack $ show str
40+
41+
42+
class ToSexp t a where
43+
toSexp :: Target t -> a -> Exp
44+
45+
instance ToSexp t (Sexpable t) where
46+
toSexp t (S x) = toSexp t x
47+
48+
ctor :: Target t -> Text -> [Sexpable t] -> Exp
49+
ctor t n [] = SAtom (ANode n)
50+
ctor t n xs = SList () (SAtom (ANode n) : map (toSexp t) xs)
51+
52+
instance ToSexp t (Sexp Atom) where toSexp _ d = d
53+
instance ToSexp t Int where toSexp _ s = SAtom (AInt s)
54+
instance ToSexp t Bool where toSexp _ s = SAtom (ABool s)
55+
56+
instance {-# OVERLAPPING #-} ToSexp t String where
57+
toSexp _ s = SAtom (AString s)
58+
59+
instance ToSexp t a => ToSexp t (Maybe a) where
60+
toSexp t x = case x of
61+
Nothing -> ctor t "None" []
62+
Just y -> ctor t "Some" [S y]
63+
64+
instance ToSexp t a => ToSexp t [a] where
65+
toSexp t xs = SList () $ map (toSexp t) xs
66+
67+
instance (ToSexp t a, ToSexp t b) => ToSexp t (a, b) where
68+
toSexp t (a, b) = SList () [toSexp t a, toSexp t b]
69+
70+
instance ToSexp t Name where
71+
toSexp t n = case n of
72+
Anon -> ctor t "nAnon" []
73+
Named i -> ctor t "nNamed" [S i]
74+
75+
instance ToSexp t ModPath where
76+
toSexp t = \case
77+
MPFile dp -> ctor t "MPfile" [S dp]
78+
MPBound dp id i -> ctor t "MPbound" [S dp, S id, S i]
79+
MPDot mp id -> ctor t "MPdot" [S mp, S id]
80+
81+
instance ToSexp t KerName where
82+
toSexp t KerName{..} = toSexp t (kerModPath, kerName)
83+
84+
instance ToSexp t Inductive where
85+
toSexp t Inductive{..} = ctor t "inductive" [S indMInd, S indInd]
86+
87+
instance ToSexp t d => ToSexp t (Def d) where
88+
toSexp t Def{..} = ctor t "def" [S dName, S dBody, S dArgs]
89+
90+
instance ToSexp t Term where
91+
toSexp t = \case
92+
LBox -> ctor t "tBox" []
93+
LRel k -> ctor t "tRel" [S k]
94+
LLambda n u -> ctor t "tLambda" [S n, S u]
95+
LLetIn n u v -> ctor t "tLetIn" [S n, S u, S v]
96+
LApp u v -> ctor t "tApp" [S u, S v]
97+
LConst c -> ctor t "tConst" [S c]
98+
LConstruct ind i es -> ctor t "tConstruct" [S ind, S i, S es]
99+
LCase ind n u bs -> ctor t "tCase" [S (ind, n), S u, S bs]
100+
LFix mf i -> ctor t "tFix" [S mf, S i]
101+
102+
instance ToSexp t Type where
103+
toSexp t = \case
104+
TBox -> ctor t "TBox" []
105+
TAny -> ctor t "TAny" []
106+
TArr a b -> ctor t "TArr" [S a, S b]
107+
TApp a b -> ctor t "TApp" [S a, S b]
108+
TVar k -> ctor t "TVar" [S k]
109+
TInd ind -> ctor t "TInd" [S ind]
110+
TConst kn -> ctor t "TConst" [S kn]
111+
112+
instance ToSexp t RecursivityKind where
113+
toSexp t = \case
114+
Finite -> ctor t "Finite" []
115+
CoFinite -> ctor t "CoFinite" []
116+
BiFinite -> ctor t "BiFinite" []
117+
118+
instance ToSexp t AllowedElims where
119+
toSexp t = \case
120+
IntoSProp -> ctor t "IntoSProp" []
121+
IntoPropSProp -> ctor t "IntoPropSProp" []
122+
IntoSetPropSProp -> ctor t "IntoSetPropSProp" []
123+
IntoAny -> ctor t "IntoAny" []
124+
125+
instance ToSexp t (ConstructorBody t) where
126+
toSexp t@ToUntyped Constructor{..} =
127+
ctor t "constructor_body" [S cstrName, S cstrArgs]
128+
129+
toSexp t@ToTyped Constructor{..} =
130+
toSexp t ((cstrName, getTyped cstrTypes), cstrArgs)
131+
132+
instance ToSexp t (ProjectionBody t) where
133+
toSexp t@ToUntyped Projection{..} = ctor t "projection_body" [S projName]
134+
toSexp t@ToTyped Projection{..} = toSexp t (projName, getTyped projType)
135+
136+
instance ToSexp t TypeVarInfo where
137+
toSexp t TypeVarInfo{..} =
138+
ctor t "type_var_info"
139+
[ S tvarName
140+
, S tvarIsLogical
141+
, S tvarIsArity
142+
, S tvarIsSort
143+
]
144+
145+
instance ToSexp t (OneInductiveBody t) where
146+
toSexp t OneInductive{..} =
147+
ctor t "one_inductive_body" $
148+
[ S indName
149+
, S indPropositional
150+
, S indKElim
151+
]
152+
++ -- NOTE(flupe): in the SExp format, order is important
153+
case t of
154+
ToUntyped -> []
155+
ToTyped -> [S $ getTyped indTypeVars]
156+
++
157+
[ S indCtors
158+
, S indProjs
159+
]
160+
161+
instance ToSexp t (MutualInductiveBody t) where
162+
toSexp t MutualInductive{..} =
163+
ctor t "mutual_inductive_body"
164+
[ S indFinite
165+
, S indPars
166+
, S indBodies
167+
]
168+
169+
instance ToSexp t (ConstantBody t) where
170+
toSexp t ConstantBody{..} =
171+
ctor t "constant_body" $
172+
case t of
173+
ToUntyped -> []
174+
ToTyped -> [S $ getTyped cstType]
175+
++ [S cstBody]
176+
177+
instance ToSexp t (GlobalDecl t) where
178+
toSexp t = \case
179+
ConstantDecl body -> ctor t "ConstantDecl" [S body]
180+
InductiveDecl minds -> ctor t "InductiveDecl" [S minds]
181+
TypeAliasDecl typ -> ctor t "TypeAliasDecl" [S typ]
182+
183+
instance ToSexp t (GlobalEnv t) where
184+
toSexp t@ToUntyped (GlobalEnv env) = toSexp t env
185+
toSexp t@ToTyped (GlobalEnv env) = toSexp t $ flip map env \(kn, decl) -> ((kn, True), decl)
186+
187+
-- TODO(flupe): handle programs
188+
instance ToSexp t (CoqModule t) where
189+
toSexp t@ToUntyped CoqModule{..} = toSexp t coqEnv
190+
toSexp t@ToTyped CoqModule{..} = toSexp t coqEnv

0 commit comments

Comments
 (0)