module Agda.Compiler.Agate.UntypedPrinter where
import Data.List
#include "../../undefined.h"
import Agda.Utils.Impossible
import Agda.Compiler.Agate.TranslateName
import Agda.Compiler.Agate.Common
import Agda.Compiler.Agate.OptimizedPrinter
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.Utils.Pretty
showAsUntypedConstructor :: QName -> TCM Doc
showAsUntypedConstructor name =
return $ text $ translateNameAsUntypedConstructor $ show name
class ShowAsUntypedTerm a where
showAsUntypedTerm :: a -> TCM Doc
instance ShowAsUntypedTerm Name where
showAsUntypedTerm t = return $ text $ translateNameAsUntypedTerm $ show t
instance ShowAsUntypedTerm QName where
showAsUntypedTerm t = return $ text $ translateNameAsUntypedTerm $ show t
instance ShowAsUntypedTerm Term where
showAsUntypedTerm (Var n args) = do
varname <- nameOfBV n
showUntypedApp varname args
showAsUntypedTerm (Lam h abs) = underAbstraction_ abs $ \body -> do
dvar <- showAsUntypedTerm $ Var 0 []
dbody <- showAsUntypedTerm body
return $ parens $ text "VAbs" <+>
parens (sep [ text "\\" <> dvar, text "->", dbody ])
showAsUntypedTerm (Con name args) = showUntypedApp name args
showAsUntypedTerm (Def name args) = showUntypedApp name args
showAsUntypedTerm (Lit lit) = return $ parens $ showUntypedLiteral lit
showAsUntypedTerm (Pi _ _) = return $ text "VNonData"
showAsUntypedTerm (Fun _ _) = return $ text "VNonData"
showAsUntypedTerm (Sort _) = return $ text "VNonData"
showAsUntypedTerm (MetaV _ _) = __IMPOSSIBLE__
showUntypedApp :: ShowAsUntypedTerm a => a -> [Arg Term] -> TCM Doc
showUntypedApp head args = do
dhead <- showAsUntypedTerm head
dargs <- mapM (showAsUntypedTerm . unArg) args
return $ foldl (\f a -> parens (f <+> text "|$|" <+> a)) dhead dargs
showUntypedDefinition :: (QName, Definition) -> TCM Doc
showUntypedDefinition (name, defn) = do
dname <- showAsUntypedTerm name
case theDef defn of
Axiom{} ->
return $ sep [ dname, equals ] <+>
sep [ text "undefined {- postulate -}" ]
Function {funClauses = []} -> __IMPOSSIBLE__
Function {funClauses = clauses} -> do
let pats = clausePats $ head clauses
let dvars = map (\i -> text ("v" ++ show i)) [1 .. length pats]
let drhs = untypedAbs dvars $ sep (text "f" : dvars)
dclauses <- mapM showUntypedClause clauses
return $ (dname <+> equals) <+> drhs <+> text "where" $+$
nest 2 (vcat dclauses)
Datatype{ dataPars = np, dataIxs = ni, dataCons = cnames } -> do
let dvars = map (\i -> text ("v" ++ show i)) [1 .. np + ni]
let drhs = untypedAbs dvars $ text "VNonData"
return $ sep [ dname, equals ] <+> drhs <+> text "{- datatype -}"
Record{ recPars = np, recFields = flds } -> do
dcname <- showAsUntypedConstructor name
let arity = length flds
let dvars = map (\i -> text ("v" ++ show i)) [1 .. arity]
let drhs = untypedAbs dvars $ sep $
text "VCon" <> text (show arity) : dcname : dvars
return $ sep [ dname, equals ] <+> drhs
Constructor{ conPars = np } -> do
dcname <- showAsUntypedConstructor name
ty <- instantiate $ defType defn
(args,_) <- splitType ty
let arity = genericLength args np
let dvars = map (\i -> text ("v" ++ show i)) [1 .. arity]
let drhs = untypedAbs dvars $ sep $
text "VCon" <> text (show arity) : dcname : dvars
return $ sep [ dname, equals ] <+> drhs
Primitive{ primName = pf } -> do
doptname <- showAsOptimizedTerm name
return $ sep [ dname, equals ] <+>
sep [ text "box", doptname, text "{- primitive -}" ]
untypedAbs :: [Doc] -> Doc -> Doc
untypedAbs dvars dtail = foldr
(\dvar d -> sep [ text "VAbs (\\" <> dvar <+> text "->",
d <> text ")" ]) dtail dvars
showUntypedClause :: Clause -> TCM Doc
showUntypedClause = showClause fTerm fCon fBody where
fTerm = showAsUntypedTerm
fCon name dargs = do
dname <- showAsUntypedConstructor name
return $ parens $ (text "VCon" <> text (show (length dargs))) <+>
sep (dname : dargs)
fBody dpats term = do
dterm <- showAsUntypedTerm term
return $ text "f" <+> sep [ sep [ sep dpats, equals ], dterm ]