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 qualified PropSyntaxStruct as PPS -- (Q((:=>)))
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 =&lt;&lt; transModule

isabelle m =
  do -- simplify &lt;- 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 _ _ (c :=> t))) = (pp i, P2I.transQType (c PPS.:=> t))