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 ++ "\""