{-+
Reusable functions for translation from the (non-recursive) base structure
to Isabelle.
-}

module BaseStruct2Isabelle where
import IsabelleAST
import BaseSyntax -- non-recursive base syntax structure
import PrettyPrint(pp)
import PropSyntaxStruct(Q((:=>)))
import Char(isAlpha)

-- translate identifiers
transId x = pp x
{-
transId x = 
  case orig x of
    G m n _ -> pp m++"."++pp n
    _ -> pp x
-}

-- translate literals
transL lit =
  case lit of
    HsInt   i  -> HInt i
    HsChar  c  -> not_supported "character literal" lit
    HsString s -> not_supported "string literal" lit
    HsFrac   x -> not_supported "fraction literal" lit

-- translate patterns
transP trId trP p =
  case mapPI trId trP p of
    HsPId (HsVar x) -> HVar x
    HsPId (HsCon c) -> HVar c
    HsPLit _ lit -> transL lit -- new
--  HsPSucc _ n l -> ...
    HsPInfixApp x op y -> HInfix x op y
    HsPApp c ps -> hApps (HVar c) ps
    HsPTuple s ps -> HTuple ps
    HsPList s ps -> HList ps
    HsPParen p -> p
--  HsPRec
    HsPAsPat _ _ -> not_supported "as-pattern" p
    HsPWildCard -> HVar "dummy" -- not_supported "wildcard pattern" p
    HsPIrrPat _ -> not_supported "irrefutable pattern" p
    _ -> not_supported "Pattern" p

-- translate declarations
transD trId trE trP trDs trT trC trTp d =
  case mapDI trId trE trP trDs trT trC trTp d of
    HsPatBind _ p rhs ds ->
      IsaFixrec (FixrecDecl [HMatches [HMatch p (transRhs rhs)]])
    HsFunBind _ ms ->
      IsaFixrec (FixrecDecl [HMatches (map transMatch ms)])
    HsTypeDecl _ tp t ->
      IsaTypes (TypesDecl tp t)
    HsDataDecl _ c tp cons ds ->
      IsaDomain (DomainDecl [DomainType tp (map transCon cons)])
    HsNewTypeDecl _ c tp con ds ->
      IsaDomain (DomainDecl [DomainType tp [transCon con]])
    {-
    HsClassDecl SrcLoc c tp (HsFunDeps i) ds |
    HsInstDecl SrcLoc (Maybe i) c t ds |
    HsDefaultDecl SrcLoc [t] |
    HsTypeSig SrcLoc [i] c t |
    HsInfixDecl SrcLoc HsFixity [HsIdentI i] |
    HsPrimitiveTypeDecl SrcLoc c tp |
    HsPrimitiveBind SrcLoc i t
    -}
    _ -> IsaComment (pp d)
  where
    transMatch (HsMatch _ i ps rhs ds) = if isAlpha (head i)
      then HMatch (hApps (HVar i) ps) (transRhs rhs)
      else case ps of [x,y] -> HMatch (HInfix x i y) (transRhs rhs)

    transRhs (HsBody e) = e
    transRhs _ = error "guarded rhs"
    
    transCon con =
      case con of
        HsConDecl loc _ _ c args -> DomainCons c (map transConArg args)
        HsRecDecl loc _ _ c args -> DomainCons c (concatMap transRecArg args)

    transConArg arg =
      case arg of
        HsBangedType t -> DomainArg Strict "" t
        HsUnBangedType t -> DomainArg Lazy "" t
    
    transRecArg (names, arg) =
      case arg of
        HsBangedType t -> [DomainArg Strict n t | n <- names]
        HsUnBangedType t -> [DomainArg Lazy n t | n <- names]


-- translate expressions
transE trId trE trP trDs trT trC e =
  case mapEI trId trE trP trDs trT trC e of 
    HsId (HsVar x)              -> HVar x
    HsId (HsCon c)              -> HVar c
    HsApp x y                   -> HApp x y
    HsLit _ lit                 -> transL lit -- new
    HsInfixApp x (HsVar op) z   -> HInfix x op z
    HsInfixApp x (HsCon c) z    -> HInfix x c z
    -- HsNegApp _ x                -> HVar "Prelude.negate" `HApp` x
    HsLambda ps e               -> hAbss ps e
    -- HsLet ds e                  -> HLet ds e
    HsIf x y z                  -> HIte x y z
    HsCase e alts               -> HCase e (map transAlt alts)
    HsTuple xs                  -> HTuple xs
    HsList xs                   -> HList xs
    HsParen x                   -> x
{-
    HsLeftSection x (HsVar op)  -> hleftsection x op 
    HsRightSection (HsVar op) y -> hrightsection op y
    HsLeftSection x (HsCon c)   -> hConleftsection x c
    HsRightSection (HsCon c) y  -> hConrightsection c y
-}
    -- The following removed by the type checker too...
{-
    HsEnumFrom e1	       -> HVar "Prelude.enumFrom" `HApp` e1
    HsEnumFromTo e1 e2	       -> HVar "Prelude.enumFromTo" `HApp` e1 `HApp` e2
    HsEnumFromThen e1 e2	       ->
       HVar "Prelude.enumFromThen" `HApp` e1 `HApp` e2
    HsEnumFromThenTo e1 e2 e3   ->
       HVar "Prelude.enumFromThenTo" `HApp` e1 `HApp` e2 `HApp` e3
-}
    HsExpTypeSig _ e c t        -> HConstrain e t -- !! what about context?
    _ -> HVar (not_supported_msg "Expression" e) -- !!
  where
    -- translate case alternatives
    transAlt alt =
      case alt of
	HsAlt _ pat (HsBody rhs) _ -> HAlt pat rhs -- !!!
	 --_ -> not_supported "Case branch" "'where' clauses"
      --where
	--transRhs (HsBody e)       = e -- [NonGuarded e]
	--transRhs (HsGuard gdrhss) = undefined -- [Guarded g e|(_,g,e)<-gdrhss]

-- translate types
transT trId trT t =
  case mapTI trId trT t of
    HsTyFun t1 t2 -> TCfun t1 t2
    HsTyApp t1 t2 -> tApp t1 t2
    HsTyVar a -> tVar a
    HsTyCon c -> TType c []
    _ -> not_supported "Type" t

-- translate type declaration LHS
transTp trId trTp trTa t =
  case t of
    HsTyApp t1 t2 -> tApp (trTp t1) (trTa t2)
    HsTyCon c -> TType (trId c) []
    _ -> not_supported "LHS in type decl" t

-- translate type declaration argument LHS
transTa trId t =
  case t of
    HsTyVar a -> tVar (trId a)
    _ -> not_supported "Type parameter in LHS of type decl" t

-- translate qualified types
transQ trC trT (c:=>t) = trT t  -- ignore context for now

not_supported s x = error $ not_supported_msg s x
not_supported_msg s x = s++" not supported (yet): "++pp x