module Agda.Auto.Print where
import Data.IORef
import Data.Char
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax
printExp :: [MId] -> MExp o -> IO String
printExp = pexp 0
pexp :: Int -> [MId] -> MExp o -> IO String
pexp p ctx e = case e of
Meta m -> do
bind <- readIORef $ mbind m
case bind of
Nothing -> return "?"
Just e -> pexp p ctx (NotM e)
NotM e -> case e of
App elr args -> do
let p' = case args of {NotM ALNil -> 4; _ -> 3}
elr' <- pelr ctx elr
args' <- pargs ctx args
par p p' $ elr' ++ args'
Lam _ (Abs id b) -> do
b' <- pexp 1 (id : ctx) b
par p 1 $ "\\" ++ pid ctx id ++ " -> " ++ b'
Fun _ it ot -> do
it' <- pexp 3 ctx it
ot' <- pexp 2 ctx ot
par p 2 $ it' ++ " -> " ++ ot'
Pi _ _ it (Abs id ot) -> do
it' <- pexp 1 ctx it
ot' <- pexp 2 (id : ctx) ot
par p 2 $ "[" ++ pid ctx id ++ ":" ++ it' ++ "] -> " ++ ot'
Sort (SortLevel 0) -> par p 4 "*"
Sort (SortLevel n) -> par p 4 $ "*" ++ show n
Sort Type -> par p 4 "Type"
pid :: [MId] -> MId -> String
pid _ (Id s) = printId s
pid ctx NoId = "\"#" ++ show (length ctx) ++ "\""
par :: Monad m => Int -> Int -> String -> m String
par n1 n2 s | n1 > n2 = return $ "(" ++ s ++ ")"
par _ _ s = return s
pelr :: [MId] -> Elr o -> IO String
pelr ctx elr = case elr of
Var v ->
if v >= length ctx then
return $ "@" ++ show (v length ctx)
else
case ctx !! v of
Id v -> return $ printId v
NoId -> return $ "\"#" ++ show (length ctx v 1) ++ "\""
Const c -> do
c <- readIORef c
return $ printId (cdname c)
pargs :: [MId] -> MArgList o -> IO String
pargs ctx args = case args of
Meta m -> do
bind <- readIORef $ mbind m
case bind of
Nothing -> return "[?]"
Just args -> pargs ctx (NotM args)
NotM args -> case args of
ALNil -> return ""
ALCons _ arg args -> do
arg' <- pexp 4 ctx arg
args' <- pargs ctx args
return $ " " ++ arg' ++ args'
ALConPar args -> do
args' <- pargs ctx args
return $ " " ++ "$" ++ args'
printConst :: ConstRef o -> IO String
printConst c = do
cdef <- readIORef c
typs <- printExp [] (cdtype cdef)
case cdcont cdef of
Def narg cls -> do
clss <- mapM printClause cls
return $ printId (cdname cdef) ++ " : " ++ typs ++ " {\n" ++ concatMap (\x -> x ++ "\n") clss ++ "};\n"
Datatype cons -> do
cons' <- mapM (\c -> do
cdef <- readIORef c
typs <- printExp [] (cdtype cdef)
return $ " " ++ printId (cdname cdef) ++ " : " ++ typs ++ ";\n"
) cons
return $ "data " ++ printId (cdname cdef) ++ " : " ++ typs ++ " {\n" ++ concat cons' ++ "};\n"
Constructor -> return ""
Postulate ->
return $ "postulate " ++ printId (cdname cdef) ++ " : " ++ typs ++ ";\n"
printClause :: Clause o -> IO String
printClause (pats, e) = do
(nv, patss) <- printPats 0 pats
es <- printExp (replicate nv NoId) e
return $ patss ++ " = " ++ es ++ ";"
printPats :: Nat -> [Pat o] -> IO (Nat, String)
printPats nv [] = return (nv, "")
printPats nv (p:ps) = do
(nv', p') <- printPat nv p
(nv'', ps') <- printPats nv' ps
return (nv'', " " ++ p' ++ ps')
printPat :: Nat -> Pat o -> IO (Nat, String)
printPat nv (PatConApp c pats) = do
cd <- readIORef c
(nv', patss) <- printPats nv pats
return (nv', "(" ++ printId (cdname cd) ++ patss ++ ")")
printPat nv PatVar = return (nv + 1, printId $ "#" ++ show nv)
printPat nv PatExp = return (nv, ".*")
printId :: String -> String
printId "" = "!!empty string id!!"
printId s@(c : cs) =
if (isAlpha c || (c == '_')) && all (\c -> isAlpha c || isDigit c || (c == '_') || (c == '\'')) cs then
s
else
"\"" ++ s ++ "\""