content: module ToQC(moduleToQC) where
  
  -- haskell syntax
  import HsName
  import HasBaseStruct
  --import PrettyPrint(pp)
  import HsExp(EI,mapEI,seqEI)
  import HsPat(PI,isPVar)
  import HsDecl(DI,HsMatchI(..),mapDI,seqDI)
  import HsGuards(HsRhs(..))
  import HsFields(HsFieldI(..))
  import HsLiteral(HsLiteral(..))
  import SrcLoc(loc0)
  
  import WorkModule(inscpRel)
  import Relations(applyRel)
  --import Ents(Ent(..))
  import TypedIds(IdTy(..),idTy)
  import SourceNames(fakeSN)
  import QualNames(getQualified)
  
  -- property syntax
  import PropSyntax as Prop hiding (quant)
  import Syntax     as Hs
  
  
  -- utils
  import List(nub)
  import Maybe(isJust,fromJust)
  import MUtils (( # ))
  import StateM
  
  
  
  class Trans t e | t -> e where trans :: t -> e
  
  
  -- names of combinators
  qc = Qual (PlainModule "QC") 
  
  neg     = qc "not"
  conj    = qc "/\\"
  disj    = qc "\\/"
  impl    = qc "==>"
  equiv   = qc "<==>"
  false   = qc "false"
  true    = qc "true"
  forAll  = qc "forAll"
  exists  = qc "exists"
  arrow   = qc "-=>"
  nil     = Qual mod_Prelude "nil"
  lft     = qc "!"
  lfp     = qc "lfp"
  gfp     = qc "gfp"
  equal   = qc "==="
  formula_type  = qc "F"
  
  pneg     = qc "pNot"
  pconj    = qc "^/\\"
  pdisj    = qc "^\\/"
  pimpl    = qc "^==>"
  pequiv   = qc "^<==>"
  
  
  transOp Conj  = HsVar conj 
  transOp Disj  = HsVar disj
  transOp Imp   = HsVar impl
  transOp Equiv = HsVar equiv
  
  transPredOp Conj  = HsVar pconj 
  transPredOp Disj  = HsVar pdisj
  transPredOp Imp   = HsVar pimpl
  transPredOp Equiv = HsVar pequiv
  
  
  predName y  
    | isConOp y = mapHsName ("%" ++) y
    | isTuple y = mapHsName (\s ->"pred_Tuple"++show (tupleArity s)) y
    | otherwise = mapHsName ("pred_" ++) y
    where
      isTuple y = case hsUnQual y of
  		 '(':_ -> True
  		 _ -> False
  
      tupleArity "()" = 0
      tupleArity s = 1+length (filter (==',') s)
  
  assertName  = mapHsName ("assert_" ++)
  
  
  string (UnQual x) = hsLit loc0 (HsString x)
  string _          = error "Qualified names not allowd in quantifiers."
  
  f $$ x = hsApp f x
  
  pInfixApp e1 op e2 = hsInfixApp (hsParen e1) op (hsParen e2)
  
  class SplitType t' c t | t' -> t c where
    splitType :: t' -> (c,t)
  
  instance SplitType (Q [c] t) [c] t where
    splitType (c :=> t) = (c,t)
  
  
  instance (Trans pa e, Trans pp e, Trans e' e, SplitType t' [c] t,
            HasBaseStruct e (EI HsName e p [d] t [c]), 
            HasBaseStruct p (PI HsName p),
            HasBaseStruct t (TI HsName t))
    => Trans (PA HsName e' t' pa pp) e where
    trans (Quant All x t pa)      = quant forAll x t pa
    trans (Quant Exist x t pa)    = quant exists x t pa
  --trans (PropId i)              = hsEVar (assertName i)
    trans (PropApp i ts es)       = foldl ($$) (hsEVar (predName i)) (map (either trans trans) es)
    trans (PropNeg pa)            = hsEVar neg $$ trans pa
    trans (PropOp op p1 p2)       = pInfixApp (trans p1) (transOp op) (trans p2)
    trans (PropEqual e1 e2)       = pInfixApp (trans e1) (HsVar equal) (trans e2)
    trans (PropHas e pp)          = hsParen (trans pp) $$ trans e
    trans (PropParen pa)          = hsParen (trans pa)
  
  
  quant name x t pa               = hsEVar name $$ string x $$ body
    where exp                     = hsLambda [hsPVar x] (trans pa)
          body                    = case t of 
                                      Nothing -> exp
                                      Just t  -> hsExpTypeSig loc0 (hsParen exp) ctxt (hsTyFun ty (hsTyCon formula_type))
                                        where (ctxt,ty) = splitType t
  
  
  
  instance (Trans pa e, Trans pp e, Trans e' e,
            HasBaseStruct e (EI HsName e p [d] t [c]),  
            HasBaseStruct p (PI HsName p),
            GetBaseStruct p (PI HsName p),
            HasBaseStruct d (DI HsName e p [d] t [c] tp))
    => Trans (PP HsName e' p t1 pa pp) e where
  --trans (PredId i)              = hsEVar (predName i)
    trans (PredApp i ts xs)       = foldl ($$) p (map (either trans trans) xs)
      where p                     = hsEVar (predName i)
    trans (PredArrow p1 p2)       = pInfixApp (trans p1) (HsVar arrow) (trans p2)
    trans (PredInfixApp p1 i p2)  = pInfixApp (trans p1) p (trans p2) 
      where p                     = HsVar (predName i)
    trans (PredNeg oppt p)        = hsEVar pneg $$ trans p
    trans (PredOp op optt p1 p2)	= pInfixApp (trans p1) (transPredOp op) (trans p2)
    trans (PredLfp i _ pp)        = hsEVar lfp $$ hsLambda [hsPVar (predName i)] (trans pp)
    trans (PredGfp i _ pp)        = hsEVar gfp $$ hsLambda [hsPVar (predName i)] (trans pp)
    trans PredNil                 = hsEVar nil
    trans (PredLifted e)          = hsEVar lft $$ trans e
    trans (PredStrong pp)         = trans pp
    trans (PredComp ps pa) 
      | allVars                   = hsLambda pats exp 
      | otherwise                 = hsLet [hsFunBind loc0 ms] (hsEVar x)
      where allVars               = all isJust (map isPVar pats)
            (pats,tys)            = unzip ps
            exp                   = trans pa
            ms                    = [ HsMatch loc0 x pats (HsBody exp) []
                                    , HsMatch loc0 x (map und ps) (HsBody $ hsEVar false) []
                                    ]
            und _                 = hsPWildCard
            x                     = UnQual "it"
    trans (PredParen pp)          = hsParen (trans pp)  
  
  
  instance (HasBaseStruct e (EI HsName e p [d] t [c]), Trans d' d, Trans e' e) => Trans (EI HsName e' p [d'] t [c]) e where
    trans = base . mapEI id trans id (map trans) id id
  
  instance (HasBaseStruct d (DI HsName e p [d] t [c] tp), Trans d' d, Trans e' e) => Trans (DI HsName e' p [d'] t [c] tp) d where
    trans = base . mapDI id trans id (map trans) id id id
  
  
  instance (Trans d' d, Trans e' e, Trans pa e, Trans pp e,
             HasBaseStruct d (DI HsName e p [d] t [c] tp),
             HasBaseStruct e (EI HsName e p [d] t [c]),
             GetBaseStruct e (EI HsName e p [d] t [c]),
             HasBaseStruct p (PI HsName p))
            => Trans (PropDI HsName e' p [d'] t [c] tp pa pp) d where
    trans = prop trans transPD
  
  
  -- PRE: all assertions are named
  
  transPD :: (Trans pa e, Trans pp e, 
              HasBaseStruct d (DI HsName e p [d] t [c] tp),
              HasBaseStruct e (EI HsName e p [d] t [c]),
              GetBaseStruct e (EI HsName e p [d] t [c]),
              HasBaseStruct p (PI HsName p))
          => PD HsName pa pp -> d
  transPD (HsAssertion loc (Just i) pa) =
      hsPatBind loc (hsPVar (assertName i)) (HsBody (trans pa)) []
  transPD (HsPropDecl loc i xs pp)      =
      case basestruct body of
        Just (HsLambda ps e) -> bind (map cvt xs ++ ps) e
        _    -> if null xs then bind [hsPVar x]
  			           (hsParen body $$ hsEVar x)
                           else bind (map cvt xs) body
  
    where cvt (HsCon i)                 = hsPVar (predName i)
          cvt (HsVar i)                 = hsPVar i
          body                          = trans pp
          bind ps body                  = hsFunBind loc [HsMatch loc (predName i) ps (HsBody body) []]
          x                             = UnQual "x"
  
  transPD (HsAssertion _ Nothing _)     = error "unnamed assertion?"
  
  
  
  
  
  --- recursive -----------------------------------------------------------------
  instance Trans (AssertionI HsName) (Hs.HsExpI HsName)     where trans = trans . struct
  instance Trans (PredicateI HsName) (Hs.HsExpI HsName)     where trans = trans . struct
  instance Trans (Prop.HsExpI HsName) (Hs.HsExpI HsName)    where trans = trans . struct
  instance Trans (Prop.HsDeclI HsName) (Hs.HsDeclI HsName)  where trans = trans . struct
  
  
  
  
  --------------------------------------------------------------------------------
  -- generating predicates for lifted constructors
  --------------------------------------------------------------------------------
  
  gen' compNum pat loc name     = hsFunBind loc matches
    where matches               = [ HsMatch loc lftCon (predPats ++ [pat compNames]) (HsBody body) []
                                  , HsMatch loc lftCon (predPats ++ [hsPWildCard])   (HsBody (hsEVar false)) []
                                  ] 
          lftCon                = predName name
          body                  = foldr app (hsEVar true) (zipWith ($$) (map hsEVar predNames) (map hsEVar compNames))
            where app e1 e2     = pInfixApp e1 (HsVar conj) e2
          names x               = take compNum [ UnQual (x ++ show n) | n <- [1..] ]
          predPats              = map hsPVar predNames
          predNames             = names "p"
          compNames             = names "x"
  
  
  gen                           :: (HasBaseStruct d (DI HsName e p [d] t c tp), 
                                    HasBaseStruct e (EI HsName e p [d] t c), 
                                    HasBaseStruct p (PI HsName p)) 
                                => HsConDeclI HsName t c -> d
  gen (HsConDecl loc _ _ name ts) = gen' (length ts) pat loc name
    where pat compNames         = hsPApp name (map hsPVar compNames)
  gen (HsRecDecl loc _ _ name fs) = gen' (length fieldNames) pat loc name
    where fieldNames              = concatMap fst fs
          pat compNames           = hsPRec name $ zipWith HsField fieldNames (map hsPVar compNames)
  
  
  
  genLiftedCon                            :: (HasBaseStruct d (DI HsName e p [d] t c tp), HasBaseStruct e (EI HsName e p [d] t c), 
                                              HasBaseStruct p (PI HsName p)) => DI HsName e p [d] t c tp -> [d]
  genLiftedCon (HsDataDecl _ _ _ ds _)    = map gen ds 
  genLiftedCon (HsNewTypeDecl _ _ _ d _)  = [gen d]
  genLiftedCon _                          = []
  
  
  genLiftedConRec               :: Hs.HsDeclI HsName -> [Hs.HsDeclI HsName]
  genLiftedConRec d             = genLiftedCon (struct d)
  
  
  -- translation of imports and exports ------------------------------------------
  
  transImps exs = map (transImp exs)
  transImp exs (Prop.HsImportDecl s mn q as optspecs) =
      Hs.HsImportDecl s mn q as (fmap (transImpSpec ex) optspecs)
    where ex = applyRel (fromJust (lookup mn exs)) . getQualified . fakeSN
  
  transImpSpec ex (hiding,ents) = (hiding,concatMap (transEnt hiding ex) ents)
  
  transExps ex = fmap (concatMap (transExp (applyRel ex.fakeSN)))
  transExp ex exp =
    case exp of
      EntE e-> map EntE (transEnt False ex e)
      _ -> [exp]
  
  transEnt hiding rel ent =
    case ent of
      Abs i -> nub $ concatMap (absEnt hiding i) (rel i)
      ListSubs i is -> ent:[Var (predName c)|HsCon c<-is]
      _ -> [ent] -- no constrcutors/assertions/predicates on other cases
  
  absEnt hiding i ent =
    case idTy ent of
      Assertion -> [Var (assertName i)]
      Property -> [Var (predName i)]
      ConstrOf{} | hiding -> [Abs i,Var (predName i)]
      _ -> [Abs i]
  
  --- translation of modules -----------------------------------------------------
  
  moduleToQC ((wm,ex),HsModule loc name exps imps decls) =
      HsModule loc name newExps newImps newDecls
    where
      newDecls = addLiftedCons . map trans . addNames $ decls
      newExps = transExps (inscpRel wm) exps
      newImps = imp "QC_combinators" True (as "QC") Nothing :
  	      imp "QC_prelude" False (as "Prelude") Nothing :
  	      transImps ex imps
  
      addNames = withSt names . mapM nameAssert
        where names = [UnQual ("unnamed_" ++ show n) | n <- [1..]]
  
      addLiftedCons ds  = concatMap genLiftedConRec ds ++ ds
  
      imp = HsImportDecl loc . PlainModule -- !!! no import from Main
      as = Just . PlainModule -- hmm
  
  
  -- name all assertions
  class NameAssert t i | t -> i where
    nameAssert :: t -> StateM [i] t
    
  instance NameAssert (PD i pa pp) i where
    nameAssert (HsAssertion loc Nothing pa) = do n <- newName
                                                 return (HsAssertion loc (Just n) pa)
    nameAssert x                            = return x
  
  instance NameAssert (PropDecl i) i where
    nameAssert = mapMProp nameAssert nameAssert
  
  instance (NameAssert e i, NameAssert d i) => NameAssert (DI i e p [d] t c tp) i where
    nameAssert = seqDI . mapDI return nameAssert return (mapM nameAssert) return return return 
  
  instance (NameAssert e i, NameAssert d i) => NameAssert (EI i e p [d] t c) i where
    nameAssert = seqEI . mapEI return nameAssert return (mapM nameAssert) return return
  
  instance NameAssert (Prop.HsDeclI i) i where nameAssert x = rec # nameAssert (struct x)
  instance NameAssert (Prop.HsExpI i) i where nameAssert x = rec # nameAssert (struct x)
  
  newName :: StateM [i] i
  newName = head # updSt tail
  