content: 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
  