-- Translator from Agda 1 to Agda 2
--
-- $Id: Translator.hs,v 1.6 2006/11/07 12:23:53 ulfn Exp $
--

module Translator where

import Control.Monad.State
import Data.Char
import Data.List
import Data.Maybe
import Debug.Trace
import System.Environment
import System.IO
import System.IO.Unsafe

-- Agda
import Position
import Id
import Monads
import Error
import Parse
import qualified NewCParser as New
import qualified OldCParser as Old
import Lex
import CSyntax
import FString
import PreStrings
import Literal
import PPrint
import CPrinter

-- Agda 2
import Agda.Utils.Pretty
import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Pretty
import Agda.Syntax.Literal
import Agda.Syntax.Position

starling :: (a -> b -> c) -> (a -> b) -> (a -> c)
starling f g x = f x (g x)

----------------------------------------------------------------------
-- Interfaces
----------------------------------------------------------------------

agda1Lexer :: Bool -> FilePath -> String -> [Token]
agda1Lexer alfa file = lexStart alfa file preStrTable

agda1Parser :: Bool -> [Token] -> Error ([CLetDef],StrTable)
agda1Parser True  = New.finalP New.pLetDefs
agda1Parser False = Old.finalP Old.pLetDefs

agda1to2 :: ([CLetDef] -> StrTable -> IO ())
         -> Error ([CLetDef],StrTable) -> IO ()
agda1to2 _  (Err e)            = hPutStrLn stderr $ prEMsg e
agda1to2 io (Done (ctree,tab)) = io ctree tab


----------------------------------------------------------------------
-- normalise functions from Agda 1 to Agda 1
----------------------------------------------------------------------

-- eliminate top level lambda abstraction ----------------------------

elimTopLam :: CLetDef -> CLetDef
elimTopLam = mapCLetDef elimTopLamCDef

elimTopLamCDef :: CDef -> CDef
elimTopLamCDef cdef = case cdef of
  CDef props cdefn -> CDef props $ elimTopLamCDefn cdefn
  _                -> cdef

elimTopLamCDefn :: CDefn -> CDefn
elimTopLamCDefn cdefn = case cdefn of
  CValueS i args ty clause -> CValueS i args ty (elimLamCClause clause)
  _                        -> cdefn

elimLamCClause :: CClause -> CClause
elimLamCClause cclause = case cclause of
  CClause pats (Clam (flg,CBind [i] mctype) cexpr)
    -> elimLamCClause (CClause (pats++[pat]) (elimLamCExpr cexpr))
         where pat = case mctype of
                 Nothing -> (flg,CPVar (CPatId i))
                 Just e  -> (flg,CPVar (CPatT i e))
  _ -> cclause

elimLamCExpr :: CExpr -> CExpr
elimLamCExpr ce = case ce of
  Clam b e        -> Clam b (elimLamCExpr e)
  Clet defs e     -> Clet (map elimTopLam defs) (elimLamCExpr e)
  Ccase e arms    -> Ccase e [(pat,elimLamCExpr expr) | (pat,expr) <- arms]
  CApply f args   -> CApply (elimLamCExpr f) [(b,elimLamCExpr e) | (b,e) <- args]
  _               -> ce

-- eliminate top level case

elimTopCase :: CLetDef -> [CLetDef]
elimTopCase = (:[])                       -- do nothing

convCase :: CLetDef -> State StrTable [CLetDef]
convCase = return . (:[])                 -- do nothing

-- replace free occurrence of "x" with CExpr -------------------------

substdfn :: Id -> CExpr -> Bool -> CLetDef -> (Bool,CLetDef)
substdfn i new True ldf = (True,ldf)
substdfn i new _    ldf = substLetDef i new ldf

substLetDef :: Id -> CExpr -> CLetDef -> (Bool,CLetDef)
substLetDef i new ld = case ld of
  CSimple d  -> case substcdef i new d of
		  (b,d') -> (b,CSimple d')
  CMutual ds -> case unzip $ map (substcdef i new) ds of
                  (bs,ds') -> if or bs then (True,CMutual ds) else (False,CMutual ds')
  _          -> (False,ld)

substcdef :: Id -> CExpr -> CDef -> (Bool,CDef)
substcdef i new cdef = case cdef of
  CDef cprops cdefn -> case substcdefn i new cdefn of
		         (b,cdefn') -> (b,CDef cprops cdefn')
  _                 -> (False,cdef)

substcdefn :: Id -> CExpr -> CDefn -> (Bool,CDefn)
substcdefn i new cdefn = case cdefn of
  CValueS i' cargs ctype cclause
    -> (i == i', CValueS i' cargs ctype $ substcclause i new cclause)
  _ -> (False, cdefn)

substcclause :: Id -> CExpr -> CClause -> CClause
substcclause i new (CClause bcps cexpr)
 = if elem i (concatMap (exid . snd) bcps)
      then CClause bcps cexpr
      else CClause bcps (substcexpr i new cexpr)
   where exid (CPCon i cpats) = i : concatMap exid cpats
         exid (CPVar (CPatT i _)) = [i]
         exid (CPVar (CPatId i))  = [i]

substcexpr :: Id -> CExpr -> CExpr -> CExpr
substcexpr i new ce = case ce of
  CVar x | i == x  -> new
  Clam b@(_,CBind is _) e
    | notElem i is -> Clam b (substcexpr i new e)
  Clet dfs e       -> case mapAccumL (substdfn i new) False dfs  of
                        (True, dfs') -> Clet dfs' e
                        (_   , dfs') -> Clet dfs' (substcexpr i new e)
  Ccase e arms     -> Ccase (substcexpr i new e)
                            [(pat,substcexpr i new expr) | (pat,expr) <- arms]
  CApply f args    -> CApply (substcexpr i new f) [(b,substcexpr i new x) | (b,x) <- args ]
  CBinOp e1 o e2   -> CBinOp (substcexpr i new e1) o (substcexpr i new e2)
  _                -> ce

exchcpat :: CPat -> Int -> [(Bool,CPat)] -> [(Bool,CPat)]
exchcpat pat i cpats
 = case splitAt i cpats of
     (xs,y:ys) -> xs++(fst y, pat):ys
     _         -> error "exchcpat: impossible pattern"

-- Kludge!
-- CValueT --> CValueS ; not valid in Agda

valueT2valueS :: CLetDef -> CLetDef
valueT2valueS = mapCLetDef t2sCDef

t2sCDef :: CDef -> CDef
t2sCDef cdef = case cdef of
  CDef props cdefn -> CDef props $ t2sCDefn cdefn
  _                -> cdef

t2sCDefn :: CDefn -> CDefn
t2sCDefn cdefn = case cdefn of
  CValueT i args ctype cexpr -> CValueS i args ctype (CClause cpats $ t2sCExpr cexpr)
                                  where cpats = concatMap carg2bcpat args
                                        carg2bcpat (CArg bis _) = map f bis
                                        f (b,i) = (b, CPVar (CPatId i))
  _                          -> cdefn

t2sCExpr :: CExpr -> CExpr
t2sCExpr ce = case ce of
  CUniv arg expr   -> CUniv arg (t2sCExpr expr)
  Clam bnd expr    -> Clam bnd (t2sCExpr expr)
  Clet defs expr   -> Clet (map valueT2valueS defs) (t2sCExpr expr)
  CProduct pos signs
                   -> CProduct pos $ map t2sCSign signs
  CRecord props pos defs
                   -> CRecord props pos $ map valueT2valueS defs
  CSelect expr i   -> CSelect (t2sCExpr expr) i
  Ccase expr arms  -> Ccase (t2sCExpr expr) [(pat,t2sCExpr e)| (pat,e) <- arms]
  CApply expr args -> case expr of
			CVar i | isSym (head $ getIdString i)
		          -> CApply (CBinOp (snd $ head args) i (snd $ head $ tail  args))
                                    [(flg,t2sCExpr e) | (flg,e) <- tail (tail args)]
                        _ -> CApply (t2sCExpr expr) [(flg,t2sCExpr e) | (flg,e) <- args ]
  CBinOp e1 op e2  -> CBinOp (t2sCExpr e1) op (t2sCExpr e2)
  Cif e0 e1 e2     -> Cif (t2sCExpr e0) (t2sCExpr e1) (t2sCExpr e2)
  CDo pos dbnds    -> CDo pos $ map t2sCDoBind dbnds
  CList pos exprs  -> CList pos $ map t2sCExpr exprs
  _                -> ce

t2sCSign :: CSign -> CSign
t2sCSign csign = case csign of
  CSignDef defn -> CSignDef (t2sCDefn defn)
  _             -> csign

t2sCDoBind :: CDoBind -> CDoBind
t2sCDoBind cdobind = case cdobind of
  CDoBind i expr -> CDoBind i (t2sCExpr expr)
  CDoBind_ expr  -> CDoBind_ (t2sCExpr expr)
  CDoLet defs    -> CDoLet (map valueT2valueS defs)

----------------------------------------------------------------------
-- translator from Agda1 definition syntax to Agda2 declaration syntax
----------------------------------------------------------------------

translate :: [CLetDef] -> [Declaration]
translate = concatMap transCLetDef

transCLetDef :: CLetDef -> [Declaration]
transCLetDef cletdef = case cletdef of
  CSimple cdef  -> transCDef cdef
  CMutual cdefs -> [Mutual noRange (concatMap transCDef cdefs)]
  CLetDefComment cs
    | not ("--#include" `isPrefixOf` cs)
                -> commentDecls cs
    | otherwise -> maybe []
                     (\ md -> [Import noRange
 		                      (QName (Name noRange [Id md]))
 				      Nothing
			              DontOpen
 				      (ImportDirective noRange (Hiding []) [] False) ])
                     mdlname
   where
     trim str = case break ('\"'==) str of
                    (_,[])   -> Nothing
                    (_,_:xs) -> Just xs
     mdlname = trim cs >>= trim . reverse >>= return . takeWhile ('.'/=) . reverse . takeWhile ('/'/=)

transCDef :: CDef -> [Declaration]
transCDef (CDef cprops cdefn)
  | elem Cprivate  cprops = [Private  noRange (transCDefn cdefn)]
  | elem Cabstract cprops = [Abstract noRange (transCDefn cdefn)]
  | otherwise             = transCDefn cdefn
transCDef _               = []

transCDefn :: CDefn -> [Declaration]
transCDefn cdefn = case cdefn of
  CValueT i args ctype cexpr
    -> transCDefn (CValueS i args ctype (CClause cpats cexpr))
         where cpats = concatMap carg2bcpat args
               carg2bcpat (CArg bis _) = map f bis
	       f (b,i) = (b, CPVar (CPatId i))
  CValueS i [] ctype cclause@(CClause cpats cexpr)
    -> case cexpr of
         CProduct pos csigs
           -> case ctype of
                CUniv carg e
                  -> [Record noRange name
                             (carg2telescope carg)
                             (transCExpr e)
                             (concatMap csig2fields csigs)]
                CStar _ 0 _
                  -> [Record noRange name [] (Set noRange) (concatMap csig2fields csigs)]
                CStar _ n _
                  -> [Record noRange name [] (SetN noRange $ fromIntegral n) (concatMap csig2fields csigs)]
                _ -> errorDecls $ pp "" cdefn
         CRecord cprops pos cletdefs
           -> ctype2typesig flg i [] ctype
           :  [FunClause (LHS (RawAppP noRange (op : pats)) [] [] [])
                         (RHS (Rec noRange $ map decls2namexpr decls))
                         (localdefs undefined)]
               where
                 decls = map transCLetDef cletdefs
                 op  = IdentP $ str2qname $ getIdString i
	         pats = ctype2pats ctype
         _ -> ctype2typesig flg i [] ctype : cclause2funclauses i flg cclause
       where flg = isInfixOp i
             name = if flg then id2infixName i else id2name i
  CValueS i args ctype cclause
    -> transCDefn (CValueS i [] ctype' cclause)
       where ctype' = foldr (\ carg e -> CUniv carg e) ctype args
  Ctype i args ctype
    -> transCDefn (CValueT i args (CStar undefined 0 undefined) ctype)
  Cnewtype i args ctype csum
    -> transCDefn (Cdata i args (Just ctype) [csum])
  Cdata i args mctype csums
    -> [Data noRange Inductive n tls t (map (csummand2constructor ot) csums)]
       where
        t = maybe (Set noRange) transCExpr mctype
        tls = concatMap carg2telescope args
        n = id2name i
        ot = foldl (\ f (TypedBindings _ _ [TBind _ [BName x _] _]) -> RawApp noRange [f, Ident (QName x)]) (Ident (QName n)) tls
  Cidata i args ctype cindsums
    -> if not (isLastSet ctype) || any (not . isSet) args then errorDecls $ pp "" cdefn
       else -- errorDecls $ pp (show cdefn) cdefn
            [Data noRange Inductive n (concatMap carg2telescope args) (transCExpr ctype) (mapMaybe cindsum2constructor cindsums)]
       where
         isLastSet (CStar _ 0 _)   = True
         isLastSet (CUniv ca cty)  = not (isSet' ca) && isLastSet cty
         isLastSet _               = False
         isSet (CArg bis (CStar _ 0 _)) = not (any fst bis)
         isSet _                        = False
         isSet' (CArg _ (CStar _ _ _))  = True
         isSet' _                       = False
         n = id2name i
  CValue i cexpr
    -> cclause2funclauses i (isInfixOp i) (CClause [] cexpr)
  CAxiom i args ctype
    -> [Postulate noRange [ctype2typesig flg i [] ctype']]
       where ctype' = foldr (\ carg e -> CUniv carg e) ctype args
             flg = isInfixOp i
  CNative i ctype
    -> errorDecls $ pp "" cdefn
  CPackage i args pkgbody
    -> case pkgbody of
         CPackageDef [] _ cletdefs
           -> [Module noRange (QName (id2name i)) (concatMap carg2telescope args)
	       (concatMap transCLetDef cletdefs)]
         _ -> errorDecls $ pp "" cdefn
  COpen cexpr (COpenArgs coargs)
    -> case cexpr of
         (CVar i)
           -> [Open noRange (QName (id2name i)) (copenargs2importdirective coargs)]
         (CApply (CVar i) bces)
           -> [Open noRange (QName (id2name i)) (copenargs2importdirective coargs)]
         _ -> errorDecls $ pp "" cdefn
  CClass classargs b csigns
    -> errorDecls $ pp "" cdefn
  CInstance i cargs cinsarg cletdefs
    -> errorDecls $ pp "" cdefn

-- Utilities

cletdef2bind :: CLetDef -> Maybe (Name,Expr)
cletdef2bind cletdef = case cletdef of
  CSimple cdef
    -> case [ (lhs,rhs) | FunClause lhs rhs ld <- transCDef cdef ] of
         (LHS p _ _ _,RHS e):_
           -> case p of
                IdentP    qn            -> Just (qn2n qn, e)
                RawAppP _ (IdentP qn:_) -> Just (qn2n qn, e)
                _ -> Nothing
         _ -> Nothing
  _ -> Nothing
  where
    qn2n (QName n)  = n
    qn2n (Qual n _) = n

ctype2pats :: CType -> [Pattern]
ctype2pats (CUniv carg cexpr)
  = map (IdentP . QName. id2name) (exIds carg) ++ ctype2pats cexpr
    where exIds (CArg bis _) = map snd $ filter (not . fst) bis
ctype2pats _ = []

ctype2typesig :: InfixP -> Id -> CArgs -> CType -> Declaration
ctype2typesig flg i args ctype
  | flg = TypeSig (id2infixName i) ys
  | otherwise = TypeSig (id2name i) ys
  where xs = concatMap (\ (CArg bns ct) -> bns) args
        ys = foldr (\ (b,i) e -> Fun noRange ((if b then HiddenArg noRange . unnamed else id) (Ident $ QName $ id2name i)) e)
		   (transCExpr ctype) xs

csig2fields :: CSign -> [TypeSignature]
csig2fields (CSign is ctype)
 = map (f ctype) is
   where f cty i = TypeSig (name i) (transCExpr cty)
         name i = if isSym $ head $ getIdString i then id2infixName i
                  else id2name i
csig2fields csign
 = errorDecls $ "csig2fields cannot translate ("++pp "" csign++")"

carg2telescope :: CArg -> Telescope
carg2telescope (CArg bis ctype)
  = map (\ (b,i) -> TypedBindings noRange (bool2hiding b) [TBind noRange [mkBoundName_ $ id2name i] (transCExpr ctype)]) bis

csummand2constructor :: Expr -> CSummand -> Constructor
csummand2constructor otype (i,cargs)
 = TypeSig (id2name i)
 $ foldr (\ (b,i,t) e -> Fun noRange (transCExpr t) e) otype (concatMap excargs cargs)

csummand2constructor' otype (i,cargs)
 = TypeSig (id2name i)
 $ foldr (\ carg e -> Pi (carg2telescope carg) e) otype cargs

cindsum2constructor :: CIndSummand -> Maybe Constructor
cindsum2constructor (CIndExpl csum i bexps)
 = Just $ csummand2constructor' otype csum
   where otype = RawApp noRange (Ident (QName (id2name i)):map (paren . transCExpr . snd) bexps)
cindsum2constructor _ = Nothing

paren :: Expr -> Expr
paren e = case e of
 RawApp r _    -> Paren r e
 App r _ _     -> Paren r e
 OpApp r _ _   -> Paren r e
 WithApp r _ _ -> Paren r e
 Lam r _ _     -> Paren r e
 Fun r _ _     -> Paren r e
 Rec r _       -> Paren r e
 Let r _ _     -> Paren r e
 _             -> e

copenargs2importdirective :: [COArg] -> ImportDirective
copenargs2importdirective coargs
 = case unzip $ map coarg2urm coargs of
     (ns, rns) -> ImportDirective noRange (Using (map ImportedName (catMaybes ns)))
                                             (map mkRenaming $ catMaybes rns) False
  where coarg2urm (COArgT _ i t)     = (Just $ id2name i,Nothing)
        coarg2urm (COArg _ i)        = (Just $ id2name i,Nothing)
        coarg2urm (COArgAs _ i j)    = (Nothing,Just (ImportedName $ id2name i,id2name j))
        coarg2urm (COArgAsT _ i t j) = (Nothing,Just (ImportedName $ id2name i,id2name j))

        mkRenaming (i, x) = Renaming i x noRange

-- Translator from Agda1 expression syntax to Agda2 expression syntax

transCExpr :: CExpr -> Expr
transCExpr ce = case ce of
  CVar i      -> Ident (QName (id2name i))
  CStar _ 0 _ -> Set noRange
  CStar _ n _ -> SetN noRange (fromIntegral n)
  Clam (flg,CBind [x] Nothing) e
              -> Lam noRange [DomainFree (bool2hiding flg) (mkBoundName_ $ id2name x)] (transCExpr e)
  Clam (flg,CBind xs (Just t)) e
              -> Lam noRange
                     [DomainFull (TypedBindings
                                    noRange
                                    (bool2hiding flg)
                                    [TBind noRange (map (mkBoundName_ . id2name) xs) (transCExpr t)]
                                 )
                     ]
                     (transCExpr e)
  Clam _ _    -> error $ "transCExpr: Never!! "++pp' ce
  CUniv a e   -> case a of
		   CArg bis ctype
                     -> foldr (\ (b,i) expr
                               -> Pi [TypedBindings noRange
                                                    (bool2hiding b)
                                                    [TBind noRange
                                                           [mkBoundName_ $ id2name i]
                                                           (transCExpr ctype)]
                                     ]
                                     expr)
                              (transCExpr e) bis
  CArrow flg ce1 ce2
              -> Fun noRange (parenExpr (transCExpr ce1)) (transCExpr ce2)
  Clet defs cexpr
              -> Let noRange (translate defs) (transCExpr cexpr)
  CProduct pos csigs
              -> errorExpr $ pp' ce
  CRecord cprops pos cletdefs
              -> let len   = length cletdefs
                     binds = mapMaybe cletdef2bind cletdefs
                     len'  = length binds
                 in if len /= len' then errorExpr $ pp (show (len,len')) ce
                    else Rec noRange binds
  Copen cexpr1 coargs cexpr2
              -> errorExpr $ pp' ce
  CApply f args
              -> case f of
                   CVar i | isSym (head (getIdString i))
                     -> transCExpr
                     $  CApply (CBinOp (snd $ head args) i (snd $ head $ tail  args))
                               [(flg,t2sCExpr e) | (flg,e) <- tail (tail args)]
                   _        -> foldl (\ e (flg,cexpr)
                                      -> App noRange
                                             e
                                             (Arg { argHiding = bool2hiding flg
                                                  , unArg = unnamed (parenExpr (transCExpr cexpr)) }))
                                     (parenExpr (transCExpr f))
                                     args
  CBinOp o1 b o2
    | isSym (head (getIdString b))
              -> OpApp noRange (id2infixName b) (map (parenExpr . transCExpr) [o1,o2])
    | otherwise
              -> transCExpr (CApply (CVar b) [(False,o1),(False,o2)])
  CMeta _ _ _ _
              -> QuestionMark noRange Nothing
  Cif ec et ee-> RawApp noRange (Ident ifQName : map (parenExpr . transCExpr) [ec,et,ee])
  CCConS i    -> transCExpr (CVar i)
  CSelect _ _ -> errorExpr $ pp' ce
  CSum _      -> errorExpr $ pp' ce
  CCCon _ _   -> errorExpr $ pp' ce
  Ccase _ _   -> errorExpr $ pp' ce
  CClos _ _   -> errorExpr $ pp' ce
--  Ccomment _ c e -> App noRange (commentExpr c) (transCExpr e)
  Ccomment _ c e
              -> transCExpr e
  CPackageType-> errorExpr $ pp' ce
  CIndSum _ _ -> errorExpr $ pp' ce
  CExternal _ -> errorExpr $ pp' ce
  CLit _ l    -> case l of
      LString s   -> Lit (LitString noRange s)
      LChar c     -> Lit (LitChar noRange c)
      LInt i      -> Lit (LitInt noRange (fromInteger i))
      LRational r -> Lit (LitFloat noRange (fromRational r))
      _           -> errorExpr $ pp' ce
  CDo _ _     -> errorExpr $ pp' ce
  CList _ _   -> errorExpr $ pp' ce

----

ifQName :: QName
ifQName = str2qname "iF"

excargs :: CArg -> [(Bool,Id,CType)]
excargs (CArg bis ctype) = [ (b,i,ctype) | (b,i) <- bis ]

parenExpr :: Expr -> Expr
parenExpr e@(Ident _)          = e
parenExpr e@(Lit _)            = e
parenExpr e@(QuestionMark _ _) = e
parenExpr e@(Underscore _ _)   = e
parenExpr e@(Set _)            = e
parenExpr e@(Prop _)           = e
parenExpr e@(SetN _ _)         = e
parenExpr e                    = Paren noRange e

-- Utilities

---- for non-supported translation and for comment (all of these kluges !)
-- debugFlg = True
debugFlg = elem "-D" $ unsafePerformIO getArgs

pp :: (PPrint a) => String -> a -> String
pp s = if debugFlg then (++ (" (D-> "++s++" <-D) ")) . ppAll else ppAll

pp' = starling (flip pp) show

errorDecls :: String -> [Declaration]
errorDecls msg
 = [TypeSig (str2name "{- translation error! ") (errorExpr' msg)]

errorExpr :: String -> Expr
errorExpr s = Ident $ str2qname $ "{! "++ s ++ " !}"

errorExpr' :: String -> Expr
errorExpr' s = Ident $ str2qname $ s ++ " -}"

commentDecls :: String -> [Declaration]
commentDecls msg
 = [TypeSig (str2name "{- ") (commentExpr' msg)]

commentExpr :: String -> Expr
commentExpr s = Ident (str2qname $ "{- " ++ s ++ " -}")

commentExpr' :: String -> Expr
commentExpr' s = Ident (str2qname $ s ++ " -}")

str2qname :: String -> QName
str2qname = QName . str2name

str2name :: String -> Name
str2name s = Name noRange [Id s]

----

isInfixOp :: Id -> Bool
isInfixOp = all (not . isAlphaNum) . getIdString

id2name :: Id -> Name
id2name i = str2name (getIdString i)

id2infixName :: Id -> Name
id2infixName i = Name noRange [Hole,Id (getIdString i),Hole]

bool2hiding :: Bool -> Hiding
bool2hiding True = Hidden
bool2hiding _    = NotHidden

bool2isinfix :: Bool -> IsInfix
bool2isinfix True = InfixDef
bool2isinfix _    = PrefixDef

type InfixP = Bool

cclause2funclauses
 :: Id -> InfixP -> CClause -> [Declaration]
cclause2funclauses i flg (CClause cpats expr)
 = case expr of
     Ccase _ _
       -> liftCcase i flg cpats expr
     _ | flg
       -> [FunClause (LHS (RawAppP noRange (intersperse op pats)) [] [] [])
		     (RHS (transCExpr expr))
                     (localdefs expr)]
     _ | otherwise
       -> [FunClause (LHS (RawAppP noRange (op : pats)) [] [] [])
	             (RHS (transCExpr expr))
		     (localdefs expr)]
  where twoargs = 2 == length cpats
        op  = IdentP $ str2qname $ getIdString i
        pats = map (parenPattern .
                    (\(b, p) -> if b == Hidden
                                  then HiddenP noRange $ unnamed p
                                  else p)) (map cpat2pat cpats)

cclause2funclause _ _ = error "Never apply cclause2funclause any but CClause"

localdefs :: CExpr -> WhereClause
localdefs cexpr = NoWhere

isCcase :: CExpr -> Bool
isCcase (Ccase _ _) = True
isCcase _           = False

isCBinOp :: CExpr -> Bool
isCBinOp (CBinOp _ _ _) = True
isCBinOp _              = False

liftCcase :: Id -> Bool -> [(Bool,CPat)] -> CExpr -> [Declaration]
liftCcase n flg pats (Ccase cexpr ccasearms)
  = case cexpr of
      CVar x -> case within x (zip [0..] pats) of
                  Just iv
                    -> case ccasearms of
                         [] -> absurdcc n flg pats iv
                         _  -> concatMap (liftcc n flg pats iv) ccasearms
                  _ -> errorDecls ("cannot translate this case: "
                                  ++ show cexpr ++ " not in args")
      _      -> errorDecls "cannot translate 'case' on any but simple variable"
    where
      within x ((i,(_,CPVar (CPatId x'))):_)  | x == x' = Just i
      within x ((i,(_,CPVar (CPatT x' _))):_) | x == x' = Just i
      within x (_:ps)                                   = within x ps
      within _ _                                        = Nothing
      liftcc n flg pats i (pat,expr@(Ccase e arms))
       = liftCcase n flg (exchcpat pat i pats) expr'
         where expr' = substcexpr x (cpat2cexpr pat) expr
               x = case cexpr of {CVar v -> v; _ -> error "Never"}
      liftcc n flg pats i (pat,expr)
             | flg = [FunClause (LHS (RawAppP noRange (intersperse (IdentP (QName (id2name n))) (cpat2pattern pat i pats))) [] [] [])
                                (RHS (transCExpr expr')) (localdefs expr')]
             | otherwise = [FunClause (LHS (RawAppP noRange (IdentP (QName (id2name n)):cpat2pattern pat i pats)) [] [] [])
                                      (RHS (transCExpr expr')) (localdefs expr')]
         where expr' = substcexpr x (cpat2cexpr pat) expr
               x = case cexpr of {CVar v -> v; _ -> error "Never"}
      absurdcc n flg pats i
             | flg = [FunClause (LHS (RawAppP noRange (intersperse (IdentP (QName (id2name n))) [abpat])) [] [] [])
                                AbsurdRHS NoWhere]
             | otherwise = [FunClause (LHS (RawAppP noRange (IdentP (QName (id2name n)):[abpat])) [] [] [])
                                      AbsurdRHS NoWhere]
         where abpat = AbsurdP noRange
liftCcase _ _ _ _ = error "Never apply liftCcase to any but Ccase"

cpat2cexpr :: CPat -> CExpr
cpat2cexpr (CPCon i pats) = CApply (CVar i) (map ((,) False . cpat2cexpr) pats)
cpat2cexpr (CPVar (CPatT i _)) = CVar i
cpat2cexpr (CPVar (CPatId i )) = CVar i

cpat2pattern :: CPat -> Int -> [(Bool,CPat)] -> [Pattern]
cpat2pattern pat i cpats
 = map (\(b, p) -> if b == Hidden
                      then HiddenP noRange $ unnamed p
                      else p) $ map cpat2pat $ exchcpat pat i cpats

cpat2arg :: (Bool,CPat) -> Arg Pattern
cpat2arg bcpat = uncurry Arg $ cpat2pat bcpat

cpat2pat :: (Bool,CPat) -> (Hiding, Pattern)
cpat2pat (flg,CPVar (CPatId i))
 = (bool2hiding flg,IdentP (QName (id2name i)))
cpat2pat (flg,CPVar (CPatT i _))
 = (bool2hiding flg,IdentP (QName (id2name i)))
cpat2pat (flg,CPCon i pats)
 = (h
   , parenPattern
   $ foldl (\ p a -> RawAppP noRange [p, (snd $ cpat2pat (flg, a))])
           (IdentP (QName (id2name i)))
           pats
   )
   where h = bool2hiding flg

parenPattern :: Pattern -> Pattern
parenPattern (AppP p1 p2) = ParenP noRange (AppP p1' (Arg {argHiding = argHiding p2, unArg = unnamed p2'}))
  where [p1',p2'] = map parenPattern [p1,namedThing $ unArg p2]
parenPattern (OpAppP r n ps) = ParenP r (OpAppP r n ps')
  where ps' = map parenPattern ps
parenPattern (RawAppP r ps) = ParenP r (RawAppP r ps')
  where ps' = map parenPattern ps
parenPattern p = p

decls2namexpr :: [Declaration] -> (Name,Expr)
decls2namexpr ds
 = case head $ reverse ds of
     FunClause (LHS (IdentP (QName name)) _ _ _) (RHS e) w
       -> (name, e)
     FunClause (LHS pat _ _ _) (RHS e) w
       -> case pat of
           RawAppP _ [IdentP (QName n)] -> (n,e)
           _                            -> (str2name "%%var%%", e)
     _ -> (str2name "", errorExpr "in translating CRecord")