PropStruct2Isabelle.hs

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

module PropStruct2Isabelle where
import IsabelleAST as S
import PropSyntaxStruct as P
import HsPropMaps
import PrettyPrint(pp)
import Maybe(fromMaybe)

-- translate property declarations: PD i pa pp -> IsaDecl
transPD trId trPA trPP pd =
  case mapPD trId trPA trPP pd of
    HsPropDecl _ n ns p ->
      IsaPredDecl (PredDecl (PredAbs n (map getHSName ns)) p)
    HsAssertion _ (Just n) a ->
      IsaPropDecl (PropDecl n a)
    _ -> IsaComment (pp pd)
    {-
  where
    transPredParam (HsCon c) = PredParam c
    transPredParam (HsVar x) = TermParam x
    -}
    --predParam (HsVar x) = "Not supported: Predicate definition: values as parameters" -- !!!

-- translate property assertions: PA i e t pa pp -> Prop
transPA trId trE trT trPA trPP pa =
  case mapPA trId trE trT trPA trPP pa of
    P.Quant P.All i optt pa -> propForall (i,optt) pa
    P.Quant P.Exist i optt pa -> propExists (i,optt) pa
    P.PropApp i ts [] -> PropVar i
    P.PropApp i ts es -> S.PropHas (map arg es) (PredVar i) -- !!
    P.PropNeg a -> S.PropNeg a
    P.PropOp op a1 a2 -> propOp op a1 a2
    P.PropEqual e1 e2 -> S.PropEqual e1 e2
    P.PropHas e p -> S.PropHas [TermArg e] p
    P.PropParen a -> a
    -- _ -> not_supported "Assertion" pa
  where
    propOp op =
      case op of
        P.Conj -> S.PropConj
        P.Disj -> S.PropDisj
        P.Imp  -> S.PropImpl
        P.Equiv-> S.PropEquiv

    arg = either TermArg PredArg
    -- bad _ = not_supported "Predicate application" "predicates as arguments"

-- translate predicate formulas: PP i e p t pa pp -> Pred
transPP trId trE trP trT trPA trPP pred =
  case mapPP trId trE trP trT trPA trPP pred of
    P.PredApp i ts [] -> S.PredVar i
    P.PredApp i ts ps -> S.PredCong i (map transPredArg ps) -- !!!
    P.PredArrow p1 p2 -> S.PredArrow p1 p2
    P.PredInfixApp p1 i p2 -> PredCong i (map PredArg [p1,p2])
    P.PredNeg optt p -> S.PredNeg p
    P.PredOp op optt p1 p2 -> predOp op p1 p2
    P.PredLfp i _ p -> S.PredLfp i p
    P.PredGfp i _ p -> S.PredGfp i p
    P.PredNil -> S.PredCong "Nil" []
    P.PredLifted e -> S.PredLifted e
    P.PredStrong p -> S.PredStrong p
    P.PredParen p -> p
    P.PredComp pts a -> S.PredComp (map fst pts) a
    -- _ -> not_supported "Predicate" pred
  where
    transPredArg = either TermArg PredArg
    --bad _ = not_supported "Predicate application" "values as arguments"

    predOp op =
      case op of
        P.Conj -> S.PredConj
        P.Disj -> S.PredDisj
        P.Imp  -> S.PredImpl
        P.Equiv-> S.PredEquiv

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