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