module SkelHOL where

-- Haskell module generated by the BNF converter

import AbsHOL
import ErrM
type Result = Err String

failure :: Show a => a -> Result
failure x = Bad $ "Undefined case: " ++ show x

transIdents :: Idents -> Result
transIdents x = case x of
  Idents str  -> failure x


transPredId :: PredId -> Result
transPredId x = case x of
  PredId str  -> failure x


transFunctId :: FunctId -> Result
transFunctId x = case x of
  FunctId str  -> failure x


transPROGRAM :: PROGRAM -> Result
transPROGRAM x = case x of
  PROGRAM sents  -> failure x


transDEF :: DEF -> Result
transDEF x = case x of
  DefSent idents sent  -> failure x


transSENT :: SENT -> Result
transSENT x = case x of
  ASentPred predid termss  -> failure x
  TrueSent  -> failure x
  FalseSent  -> failure x
  IdentSent idents  -> failure x
  ASentEq term0 term  -> failure x
  NegSent sent  -> failure x
  IfSent sent0 sent1 sent  -> failure x
  AndSent sent0 sent  -> failure x
  OrSent sent0 sent  -> failure x
  ImpSent sent0 sent  -> failure x
  LetSent defs sent  -> failure x
  ForallSent terms sent  -> failure x
  ExistsSent terms sent  -> failure x


transTERM :: TERM -> Result
transTERM x = case x of
  FunctTerm functid termss  -> failure x
  ConstVarTerm idents  -> failure x


transTERMS :: TERMS -> Result
transTERMS x = case x of
  Terms terms  -> failure x