module Prop2Alfa(Prop2Alfa.transModule,modPath) where
import TiPropDecorate
import PropSyntax(HsModuleI,HsPatI,prop,Prop,Rec(..))
import qualified PropSyntax as PS
import HsConstants(mod_Prelude)
import PNT
import TypedIds
import HsPropStruct
import HsPropMaps
import HsIdent
import QualNames(mkUnqual,getQualified)
import UniqueNames(noSrcLoc,origModule)
import DefinedNames(definedType)
import PrettyPrint(Printable,pp)
import TI hiding (getEnv,inst,tapp,sch,inEnv,extend,restrict,conName,definedType)
import NameMapsPropDecorate
import BaseStruct2Alfa
import qualified UAbstract as U
import qualified AbstractOps as U
import qualified UMatch as U
import MUtils
import EnvM
import Maybe(fromMaybe)
import Char(isAlpha)

transModule = trans :: HsModuleI m i (TiDecls NName) -> EnvM Env U.Module

instance (Trans b u,Trans p u) => Trans (Prop b p) u where
  transTyped t p = prop tt tt p
    where tt x = transTyped t x

instance Trans (TiAssertion NName) U.Exp where transTyped = transTypedRec
instance Trans (TiPredicate NName) U.Exp where transTyped = transTypedRec

instance Trans (OTiAssertion NName) U.Exp where
  trans (OA is ds pa) = 
      --U.uAbsExp
      U.piExp . map (flip (,) (missing "assertion dictionary type"))
        # ltrans is <# (eLet # mapM transT ds <# trans pa)
    where
      transT (i:>:t,e) =
	do i' <- transUnqualVar i
	   t' <- trans t
	   e' <- trans e
	   return $ U.decl' [valdef i' ([],([],t')) e']
			  
instance (Printable pa,Printable pp,
	  Trans pa U.Exp,Trans pp U.Exp)
       => Trans (PD NName pa pp) [U.Def] where
  trans pd =
      case pd of
        HsAssertion s optnm pa -> maybe cmnt (transAssert pa) optnm
        HsPropDecl s nm is pp -> transPropDecl nm  is pp
    where
      cmnt = return [commentdef pd]

      transAssert pa nm =
	do (gs,cs:=>t) <- schak (HsCon nm)
	   extendTyvars gs $ do
	     -- assume t=Prop
	     -- t' <- trans t -- should be Prop
	     gs' <- ltrans gs
	     cs' <- ltrans cs
	     nm' <- trans nm
	     pa' <- trans pa
	     let cnt=length gs
	     return $
               --hide' nm' cnt++
	       [valdef nm' ([],([],{-U.eFuns cs'-}eAssertion))
		           (U.piExp gs' (dictTypes cs' pa'))]

      dictTypes ts = uncurry U.piExp . apFst dictTypes' . U.flatPi
        where dictTypes' xts = zip (map fst xts) ts++drop (length ts) xts

      transPropDecl n is pp =
        do n' <- transUnqualVar n
           sch@(gs,cs:=>t) <- schk (HsCon n) -- or schak...
	   extendTyvars gs $ do
	     tctx <- ltrans gs
	     cs' <- ltrans cs
	     (targs,tres) <- U.flatFun # trans t
	     is' <- ltrans (map getHSName is)
	     let (ctx,tres') = args' is' (cs'++targs) tres
	         cnt=length gs
	     pp' <- trans pp
	     return $ hide' n' cnt++[valdef n' (tctx++ctx,tres') pp']

eProp = un "Prop"
eAssertion = un "Assertion"
--eProp = U.eType
ePred = uApp (un "Pred")

instance (Trans e U.Exp,Trans t U.Exp,Trans pa U.Exp,Trans pp U.Exp)
      => Trans (PA NName e t pa pp) U.Exp where
    trans pa =
      case pa of
	Quant All i optt pa -> do i' <- trans i
                                  optt' <- trans optt
				  U.EPi (i' U.:- opt "type in universal quantifier" optt') # trans pa
	Quant q i optt pa -> do i' <- trans i
				optt' <- trans optt
                                uApp # transQ q optt' <#
				     (eAbs i' optt' # trans pa)
			     
--	PropId i -> U.EVar # i
	PropApp i ts es -> appqvar # transConId i <# ltrans ts <# mapM (either trans trans) es
	PropNeg a -> uApp eNot # trans a
	PropOp op a1 a2 -> U.app # trans op <# ltrans [a1,a2]
	PropEqual e1 e2 -> equal # trans e1 <# trans e2
	PropHas e p -> uApp # trans p <# trans e
	PropParen a -> trans a

eAbs n optt e = U.EAbs (n U.:-opt "type in abstraction" optt) e
eNot = un "Not"
ePredNot = un "NegPred"
--eEq =  m1 (un "Identical")

m1 s e =uApp e (missing s)
m2 s = m1 s . m1 s

-- The type checker is assumed to add a type annotation to the left operand
equal (U.ETyped e1 t1) e2 = U.app (un "===") [t1,e1,e2]
equal e1 e2 = U.app (un "===") [missing "type in equality prop",e1,e2]

transQ q optt = flip uApp (opt "type in quantifier" optt) # trans q

instance Trans Quantifier U.Exp where
  trans q =
    return $
    case q of
      All   -> un "ForAll"
      Exist -> un "Exists"

instance Trans PropOp U.Exp where
  trans op =
    return $
    case op of
     Conj  -> un "And"
     Disj  -> un "Or"
     Imp   -> un "Implies"
     Equiv -> un "Equivalence"

appvar i ts es = U.app (U.EVar i) (ts++es)
appqvar e ts es = U.app e (ts++es)

instance (Trans c U.Exp,Trans t U.Exp) => Trans (PS.Q [c] t) U.Exp where
  trans (c PS.:=> t) = U.eFuns # ltrans c <# trans t

instance (Trans e U.Exp,Trans p U.Pat,Trans t U.Exp,
	  Trans pa U.Exp,Trans pp U.Exp,
	  Printable e,Printable p,Printable t,Printable pa,Printable pp)
      => Trans (PP NName e p t pa pp) U.Exp where
  trans p =
    case p of
--    PredId i -> U.EVar # trans i
      PredApp i ts ps -> appqvar # transConId i
                               <# ltrans ts <# mapM (either trans trans) ps
      PredArrow p1 p2 -> U.app (m2 "type for arrow predicate" (un "Arrow")) # ltrans [p1,p2]
      PredInfixApp p1 i p2 -> U.app . U.EVar # trans i <# ltrans [p1,p2]
      PredNeg optt p -> liftNeg # trans optt <# trans p
      PredOp op optt p1 p2 -> liftOp # trans op <# trans optt <# trans p1 <# trans p2
      PredLfp i optt p -> fix "Lfp" # trans i <# trans optt <# trans p
      PredGfp i optt p -> fix "Gfp" # trans i <# trans optt <# trans p
      PredNil -> return (m1 "type for IsNil" (un "IsNil"))
      PredLifted e -> uApp (m1 "type for !" (un "Lift")) # trans e
      PredStrong p -> trans p -- !!
      PredParen p -> trans p
      PredComp pts a -> foldr abstr # trans a <# ltrans pts
      _ -> return $ missing (comment (pp p)) -- for unimplemented things
    where
      abstr (U.PVar x,optt) e = eAbs x optt e
      abstr _ _ = missing "pattern in predicate comprehension" -- !!!

      liftNeg optt p =
          U.app ePredNot [opt "type of lifted negation" (deep # optt),p]

      liftOp op optt p1 p2 =
          U.app (un "predOp")
                [opt "type of lifted connective" (deep # optt),op,p1,p2]

      fix op i optt p = U.app (un op) [opt "type in Gfp/Lfp" optt,eAbs i (ePred # optt) p]

      deep t =
        case t of
	  U.EApp f t2 | f==un "predT" -> deep t2 -- compensation for shallow translation of t
	  U.EPi (x U.:-t1) t2 -> U.app predCon [t1,deep t2]
	  _ -> if t==propType
	       then propCon
	       else t -- must be a type variable of kind Prop
		
      predCon = U.ECon (U.Con "Pred")
      propCon = U.ECon (U.Con "Prop")
      propType = qn (transM mod_Prelude) "Prop"
----

instance Trans (TiDecls NName) [U.Def] where
  trans (Decs ds env) = concat # extend env (ltrans ds)

instance Trans (TiDecl NName) [U.Def] where
  trans (Dec d) = prop transBase trans d
    where transBase d = (++) # trans d <# liftedCons d

instance Trans (HsPatI NName) U.Pat where trans = trans . struct

instance Trans (TiExp NName) U.Exp where
  trans (Exp e) = trans e
  trans (TiSpec c@(HsCon _) sc ts) = transECon c sc ts
  --trans (TiSpec x _ []) = transEVar x
  trans s@(TiSpec x _ ts) = U.app # inst x <# ltrans ts
  trans (TiTyped e t) = transTyped (Just t) e

  transTyped t (Exp e) = transTyped t e
  transTyped t e = optTransTyped t =<< trans e

------

transRec = trans . struct
transTypedRec t = transTyped t . struct

------

liftedCons d =
  concat #
  case d of
    PS.HsNewTypeDecl s ctx lhs con  der -> liftedCons' lhs
    PS.HsDataDecl    s ctx lhs cons der -> liftedCons' lhs
    _ -> return []
  where
    liftedCons' = liftedCons'' . definedType

    liftedCons'' t@(PNT tn _ _) =
        mapM liftedCon [splitAt i cs'|i<-[0..length cs'-1]]
      where
        cs' = [(pnt (conName c) cty,conArity c)|c<-cs]
        Type tinfo@(TypeInfo {constructors=cs}) = idTy t
	cty = ConstrOf (getQualified tn) tinfo

    liftedCon (cs1,(c,n):cs2) =
	do (gs,qt) <- schk (HsCon c)
	   gs' <- ltrans gs
	   qt' <- extendTyvars gs (trans qt)
	   let ps = gs'++zip pns (map ePred args)++[(x0,res)]
	       (args,res)=U.flatFun qt'
	   c' <- transUnqualVar c
	   other <- mapFstM (\c -> trConName # trans c) (cs1++cs2)
	   let cpred = trPredName c'
	       ccon = trConName c'
	       body = predBody ccon n other
	   return $ hide cpred gs ++[valdef cpred (ps,([],eProp)) body]

       where
         pns = [U.Var ("P"++show i)|i<-[1..n]]
	 x0:xs =[U.Var ("x"++show i)|i<-[0..]]

         predBody c n other = U.ECase (U.EVar x0)
				      (rightBranch:map otherBranch other)
           where
	     rightBranch       = br c n (conj (zipWith varapp pns xs))
	     otherBranch (c,n) = br c n (un "Absurdity")

	     br (U.Var c) n e = U.Branch (U.Con c,(take n xs,e))
	     varapp p x = U.EVar p `uApp` U.EVar x

	     conj [] = un "Triviality"
	     conj ps = foldr1 (uApp . uApp (un "And")) ps

    pnt c idty = PNT (mkUnqual c) idty noSrcLoc

    trPredName (U.Var s) = U.Var . predName . transConName $ s
    trConName (U.Var s) = U.Var . transConName $ s

transConId i =
  if isCon i
  then qn' (transM (origModule i)) # getMEnv <# (liftedConName # trans i)
  else U.EVar # trans i

qn' m ms v@(U.Var x) = if m `elem` ms then U.EVar v else qn m x

liftedConName (U.Var s) = U.Var (predName s)

predName s =
  case s of
    c:_ | isAlpha c -> "Pred"++s
    _ -> "%"++s