IsabelleCmds.hs

module IsabelleCmds where
import Prelude hiding (print)
import PFE0(pput,epput,getSubGraph)
import PFE3(parseModule)
import PFE4(rewriteAndTypeCheckModule,topTypes)
import PFE_Rewrites(fbRewrite,lcRewrite,flRewrite,pmRewrite,compRw,rwFun)
import HsModule(HsModuleI(..),hsModImportsFrom)
import PfeDepCmds(tdepgraph)
import PfeParse(moduleArg,qualId)
import PfePropCmds(baseNames)
import TiClasses(filterDefs,fromDefs)
import TiSCC(sccD')
import PFEdeps(tdefinedNames,splitDecls,isDefaultDecl)
import HsIdent(getHSName)
import MapDeclMProp() -- ?
import DefinedNames(addName,definedNames)
import FreeNames(freeNames)
--import TiPropInstances()
import TiProp() -- for PFE, instance CheckRecursion ...
import TiTypes(Scheme(Forall),Typing((:>:)),Qual((:=>)))
import RemoveListCompProp()
--import TiPropDecorate(TiDecl)
--import PNT(PNT)

import qualified Prop2Isabelle as P2I
import qualified IsabelleAST as AST
--import qualified PropDecorate2Isabelle2 as Ti2S
import SimpFunBind
import RemoveListComp
import SimpFieldLabels(simpFieldLabels)

import AbstractIO(print)
import MUtils(( # ),(@@),apSnd)
import Sets(mkSet,elementOf)
import PrettyPrint((<+>),pp)

isabelleCmds =
  [("isabelle", (moduleArg isabelle,"simple translation of one module to Isabelle")),
   ("isabelleslice", (qualId isabelleSlice,"translate a slice to Isabelle"))]

isabelleSlice qn = undefined -- slice' qn =<< transModule

isabelle m =
  do simplify <- rwFun $ foldr1 compRw [lcRewrite]
     let transM = simplify . addName
     parsed <- fmap snd (parseModule m)
     Just types <- fmap (lookup m) (topTypes (Just [m]))
     let decls1 = hsModDecls parsed
         decls2 = transM decls1
         decls3 = sccD2 decls2
         decls4 = map P2I.transDecs decls3
         decls5 = map P2I.combineDecls decls4
         decls6 = P2I.addConstsDecls (typetable types) decls5
         isamod = AST.Module (header parsed) decls6
     print isamod

sccD2 ds = sccD' names ds
  where names d = (map fst (definedNames d), map fst (freeNames d))

header m = (pp (hsModName m), map pp (hsModImportsFrom m))

typetable (_,(_,(_,(_,xs)))) = map f xs
  where f (i :>: (Forall _ _ (_ :=> t))) = (pp i, P2I.transType t)

{-
use function besides hsModDecls to get module name, imports, exports
topTypes [m] returns PFE4Info
-}
{-
transModule =
  do simplify <- rwFun $ foldr1 compRw [lcRewrite]
     let transM = P2I.transDecs . simplify . addName
     return transM

slice' q@(m,n) trans =
  do ms <- map (fst.snd) # getSubGraph (Just [m])
     (_,(_,_,used)) <- tdepgraph [q]
     let needed = mkSet used
     slices <- mapM (moduleSlice needed) ms
     let defs = concatMap trans slices
         isamod = P2I.defs2module "" [] defs
     print isamod

moduleSlice needed m =
    --filter isNeeded . t . splitDecls . fromDefs . hsModDecls # rewriteAndTypeCheckModule simplify m
    filter isNeeded . splitDecls . hsModDecls . snd # parseModule m
  where
    isNeeded d = isDefaultDecl d || isNeeded' d
    isNeeded' = any (`elementOf` needed) . map getHSName . tdefinedNames False m
    --t = id :: [TiDecl PNT] -> [TiDecl PNT]
-}