content: -- Notices:
  --
  -- Copyright 2020 United States Government as represented by the Administrator of the National Aeronautics and Space Administration. All Rights Reserved.
  
  -- Disclaimers
  -- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE.  FURTHER, GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES IT "AS IS."
  
  -- Waiver and Indemnity:  RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY PRIOR RECIPIENT.  IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW.  RECIPIENT'S SOLE REMEDY FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS AGREEMENT.
  
  
  module PVSCert where
  
  import AbsPVSLang hiding (fpGuardList,letExpr,varName)
  import AbsSpecLang
  import AbstractSemantics
  import AbstractDomain
  import Common.DecisionPath
  import Common.ControlFlow
  import Common.TypesUtils (VarName,PredAbs(..))
  import Data.Maybe (fromMaybe)
  import qualified Data.Map as Map
  import Kodiak.Runner
  import Numeric
  import Prelude hiding ((<>))
  import PPExt
  
  genFpProgFile :: PVSType -> String -> Program -> Doc
  genFpProgFile fp progFileName prog =
    text "% This file is automatically generated by PRECiSA \n"
    $$
    text (progFileName ++ ": THEORY")
    $$
    text "BEGIN" <> text "\n"
    $$
    importFPTheory fp <> text "\n"
    $$
    prettyDoc prog <> text "\n"
    $$
    text ("END " ++ progFileName)
      where
        importFPTheory FPSingle = text "IMPORTING float_bounded_axiomatic@ieee754_single"
        importFPTheory FPDouble = text "IMPORTING float_bounded_axiomatic@ieee754_double"
        importFPTheory _ = emptyDoc
  
  genCertFile :: String -> String -> String -> Program -> Interpretation -> Doc
  genCertFile inputFileName certFileName realFileName prog sem =
    text "% This file is automatically generated by PRECiSA \n"
    $$
    text (certFileName ++ ": THEORY")
    $$
    text "BEGIN"
    $$
    text "IMPORTING PRECiSA@strategies"
    $$
    text "IMPORTING float_bounded_axiomatic@aerr_ulp__double"
    $$
    text "IMPORTING float_bounded_axiomatic@aerr_ulp__single"
    $$
    text ("IMPORTING " ++ inputFileName)
    $$
    text ("IMPORTING " ++ realFileName  ++ "\n")
    $$
    text "%|- *_TCC* : PROOF"
    $$
    text "%|- (precisa-gen-cert-tcc)"
    $$
    text "%|- QED\n"
    $$
    printCerts sem prog
    $$
    text ("END " ++ certFileName)
  
  genRealProgFile :: PPExt a => String -> String -> a -> Doc
  genRealProgFile inputFileName realProgFileName prog =
    text "% This file is automatically generated by PRECiSA \n"
    $$
    text (realProgFileName ++ ": THEORY")
    $$
    text "BEGIN"
    $$
    text ("IMPORTING " ++ inputFileName ++ "\n")
    $$
    prettyDoc prog
    $$
    text ("END " ++ realProgFileName)
  
  genNumCertFile :: String
                 -> String
                 -> [(String,PVSType,[Arg]
                    ,[(ResultField, [(Conditions,LDecisionPath,ControlFlow,KodiakResult,AExpr,[FAExpr],[AExpr])])])]
                 -> [Decl]
                 -> Spec
                 -> Int
                 -> Int
                 -> Bool
                 -> Doc
  genNumCertFile certFileName numCertFileName kodiakResult decls (Spec specBinds) maxBBDepth prec isTran =
    text "% This file is automatically generated by PRECiSA \n"
    $$
    text ("% maxDepth: " ++ show maxBBDepth ++ " , prec: 10^-" ++ show prec ++ "\n")
    $$
    text (numCertFileName ++ ": THEORY")
    $$
    text "BEGIN"
    $$
    text ("IMPORTING " ++ certFileName)
    $$
    text "IMPORTING PRECiSA@bbiasp"
    $$
    text "IMPORTING PRECiSA@bbiadp"
    $$
    text "IMPORTING PRECiSA@strategies \n"
    $$
    text "%|- *_TCC* : PROOF"
    $$
    text "%|- (precisa-gen-cert-tcc)"
    $$
    text "%|- QED\n"
    $$
    printNumCerts kodiakResult decls specBinds maxBBDepth prec isTran
    $$
    text ("END " ++ numCertFileName)
  
  printNumCerts :: [(String,PVSType,[Arg]
                    ,[(ResultField, [(Conditions,LDecisionPath,ControlFlow,KodiakResult,AExpr,[FAExpr],[AExpr])])])]
                -> [Decl]
                -> [SpecBind]
                -> Int
                -> Int
                -> Bool
                -> Doc
  printNumCerts [] _ _ _ _ _ = emptyDoc
  printNumCerts ((_,Boolean,_,_):_) _ _ _ _ _ = emptyDoc
  printNumCerts ((f,fp,args,fSem):res') decls spec maxBBDepth prec isTran =
    printNumCertsField f fp args fSem decls spec maxBBDepth prec isTran
    $$
    printNumCerts res' decls spec maxBBDepth prec isTran
  
  
  printNumCertsField :: String
                -> PVSType
                -> [Arg]
                -> [(ResultField, [(Conditions,LDecisionPath,ControlFlow,KodiakResult,AExpr,[FAExpr],[AExpr])])]
                -> [Decl]
                -> [SpecBind]
                -> Int
                -> Int
                -> Bool
                -> Doc
  printNumCertsField _ _ _ [] _ _ _ _ _ = emptyDoc
  printNumCertsField f t args ((field,res):res') decls spec maxBBDepth prec isTran =
    printNumCertsFun fFP fReal field args res ranges 0 fp prec maxBBDepth isTran fpGuardList
    $$
    printNumCertsField f t args res' decls spec maxBBDepth prec isTran
    where
      fp = case t of
        Tuple ts -> case field of
                        ResTupleIndex idx -> ts !! fromInteger (idx - 1)
                        _ -> error $ "printCertsField: " ++ show field ++ " is not a valid tuple index."
        Record ts -> case field of
                        ResRecordField rField -> fromMaybe (error $ "printCertsField: field " ++ show rField ++ " not found.")
                                                $ lookup rField ts
                        _ -> error $ "printCertsField: " ++ show field ++ " is not a valid record field."
        _ -> t
      fpGuardList = case findInDecls f decls of
                       Just (_,_,body@(AExprBody _ae)) -> listFPGuards body
                       Just (_,_,body@(CExprBody _ae)) -> listFPGuards body
                       Just (_,_,BExprBody _) -> error $ "printNumCerts: function " ++ f ++ " is of type Boolean."
                       Nothing -> error $ "printNumCerts: function " ++ f ++ " not found."
      ranges = fromMaybe (error $ "printNumCerts: function " ++ show f ++ " not found.") (findInSpec f spec)
      fFP   = if isTran then f ++ "_fp" else f
      fReal = if isTran then f else f ++ "_real"
  
  printNumCertsFun :: String
                   -> String
                   -> ResultField
                   -> [Arg]
                   -> [(Conditions,LDecisionPath,ControlFlow,KodiakResult,AExpr,[FAExpr],[AExpr])]
                   -> [VarBind]
                   -> Int
                   -> PVSType
                   -> Int
                   -> Int
                   -> Bool
                   -> [FAExpr]
                   -> Doc
  printNumCertsFun _ _ _ _ [] _ _ _ _ _ _ _ = emptyDoc
  printNumCertsFun f fReal field args ((cond, _, _, res, err, _, _):result') ranges n fp prec maxBBDepth isTran fpGuardList =
    prPvsNumLemma numLemma f fReal field args cond roundOffError ranges fp Nothing fpGuardList
    $$
    prPvsNumProof numLemma symbLemma prec maxBBDepth
    $$
    (if isTran
       then prPvsNumLemma auxLemmaName f fReal field args cond roundOffError ranges fp (Just err) fpGuardList
       else emptyDoc)
    $$
    printNumCertsFun f fReal field args result' ranges (n+1) fp prec maxBBDepth isTran fpGuardList
    where
      auxLemmaName = name field <> text "_err_" <> int n
      numLemma = name field <> text "_c_" <> int n
      roundOffError = maximumUpperBound res
      symbLemma = name field <> text "_" <> int n
      name ResValue = text f
      name (ResRecordField recField) = text f <> text "_" <> text recField
      name (ResTupleIndex tupleIdx) = text f <> text "_" <> integer tupleIdx
  
  printCertsField :: FunName
                  -> Bool
                  -> PVSType
                  -> FAExpr
                  -> [Arg]
                  -> ResultField
                  -> ACebS
                  -> Doc
                  -> Doc
  printCertsField f isTrans t stm args field cset certDocField
    = printLemmasAndProofs fFP fReal field args stm cset fp 0
      $$ certDocField
    where
      fp = case t of
        Tuple ts -> case field of
                        ResTupleIndex idx -> ts !! fromInteger (idx - 1)
                        _ -> error $ "printCertsField: " ++ show field ++ " is not a valid tuple index."
        Record ts -> case field of
                        ResRecordField rField -> fromMaybe (error $ "printCertsField: field " ++ show rField ++ " not found.")
                                                $ lookup rField ts
                        _ -> error $ "printCertsField: " ++ show field ++ " is not a valid record field."
        _ -> t
      fFP   = if isTrans then f ++ "_fp" else f
      fReal = if isTrans then f else f ++ "_real"
  
  printCerts :: Interpretation -> Program -> Doc
  printCerts interp decls = Map.foldrWithKey printCertsFun emptyDoc interp
    where
      printCertsFun _ (_,Boolean, _, _) certDoc = certDoc
      printCertsFun f (isTrans,t, args, sem) certDoc = case findInDecls f decls of
        Just (_,_,AExprBody stm) -> Map.foldrWithKey (printCertsField f isTrans t stm args) certDoc sem
        _ -> error $ "printCerts: function " ++ show f ++ " not found."
  
  printLemmasAndProofs :: String -> String -> ResultField -> [Arg] -> FAExpr -> ACebS -> PVSType -> Int -> Doc
  printLemmasAndProofs f _ _ args _ [] _ n
    = text f <> text "_error"
      <> argsDoc
      <>  text ": nonneg_real"
      <+> text "=" <+>
           (if n==1 then text f <> text "_0_error" <> actArgsDoc
            else text "max" <> parens (hsep (punctuate comma $ map errFunDoc [0..(n-1)])))
      <> text "\n"
      where
        prRealInt  (Arg x _) = text "r_" <> text x
        prErrorInt (Arg x _) = text "e_" <> text x
        argsDoc = parens (hsep (punctuate comma $ map prErrorInt args)
          <>  text ": nonneg_real" <> comma
          <+> hsep (punctuate comma $ map prRealInt args)
          <>  text ": real")
        actArgsDoc = parens (hsep (punctuate comma $ map prErrorInt args)
          <> comma
          <+> hsep (punctuate comma $ map prRealInt args))
        errFunDoc m = text f <> text "_" <> int m <> text "_error" <> argsDoc
  
  printLemmasAndProofs f fReal field args stm (aceb:acebs) fp n
    = prErrorDef f fReal field args aceb fp n
      $$
      prPvsLemma f fReal field args aceb fp n (listFPGuardsFAExpr stm)
      $$
      prPvsProof f n
      $$
      printLemmasAndProofs f fReal field args stm acebs fp (n+1)
  
  prPvsProof :: String -> Int -> Doc
  prPvsProof f n =
      text "%|- " <> text f <> text "_" <> int n <> text ": PROOF"
      $$ text "%|- (precisa)"
      $$ text "%|- QED"
      $$ text "\n"
  
  prIsFinite :: FAExpr -> Doc
  prIsFinite ae | getPVSType ae == FPSingle = text "finite?_single" <> parens (prettyDoc ae)
                | getPVSType ae == FPDouble = text "finite?_double" <> parens (prettyDoc ae)
                | getPVSType ae == TInt = text "int_in_range?_double" <> parens (prettyDoc ae)
                | otherwise = error $ "prIsFinite: " ++ show ae ++ " is not a floating-point or integer expression."
  
  prIsFiniteHp :: [FAExpr] -> [(VarName, FAExpr)] -> Doc
  prIsFiniteHp [] _ = emptyDoc
  prIsFiniteHp isFiniteCheckList localVars' = prLocalVars localVars' isFiniteListDoc
    where
      isFiniteListDoc = hsep (punctuate (text " AND") (map prIsFinite isFiniteCheckList))
  
  prLocalVars :: [(VarName, FAExpr)] -> Doc -> Doc
  prLocalVars [] doc = doc
  prLocalVars locVarList doc =
    text "LET"
    <+> vcat (punctuate comma (map
         (\(varName, letExpr) -> text varName <> text "=" <> prettyDoc letExpr) locVarList))
          $$ text "IN" <+> parens doc
  
  prErrorDef :: String -> String -> ResultField -> [Arg] -> ACeb -> PVSType -> Int -> Doc
  prErrorDef f _fReal _field args aceb _fp n  =
    text f <> text "_" <> int n <> text "_error"
                       <+> parens (hsep (punctuate comma $ map prErrorInt args)
                       <>  text ": nonneg_real" <> comma
                       <+> hsep (punctuate comma $ map prRealInt args)
                       <>  text ": real")
                       <>  text ": nonneg_real"
                       <+> text "=" <+> prettyError (fromMaybe (error "prPvsLemma: unexpected argument.") err)
    $$ text "\n"
    where
      prRealInt  (Arg x _) = text "r_" <> text x
      prErrorInt (Arg x _) = text "e_" <> text x
      ACeb {eExpr = err} = aceb
  
  prPvsLemma :: String -> String -> ResultField -> [Arg] -> ACeb -> PVSType -> Int -> [FAExpr] -> Doc
  prPvsLemma f fReal field args aceb fp n _fpGuards =
    text f <> text "_" <> int n <+> text ": LEMMA"
    $$ text "FORALL(" <>  hsep (punctuate comma $ map prErrorInt args)
                      <>  text ": nonneg_real" <> comma
                      <+> hsep (punctuate comma $ map prRealInt args)
                      <>  text ": real" <> comma
                      <+> hsep (punctuate comma $ map prettyDoc args)
                      <> text ")" <> text ":"
    $$ prIsFiniteHp isFiniteExprs locVars
    $$ text "AND"
    $$ prPvsArgsSymb args
    $$ (if isTrueCondition c then empty else text "AND" <+> parens (prettyDoc c))
    $$ text "IMPLIES"
    $$ text "abs(" <> f2r fp (printNameWithField (text f <> text "(" <>
       hsep (punctuate comma $ map (prettyDoc . arg2var) args) <> text ")" ) field)
       <+> text "-"
       <+> printNameWithField (text fReal <> text "("
       <> hsep (punctuate comma $ map (prettyDoc . realVar . arg2var) args) <> text ")") field
       <> text ")"
       <+> text "<=" <+> text f <> text "_" <> int n <> text "_error"
      <> parens (hsep (punctuate comma $ map prErrorInt args)
                  <> comma
                  <+> hsep (punctuate comma $ map prRealInt args))
    $$ text "\n"
    where
      isFiniteExprs = concatMap subExpressions (fDeclRes $ fpExprs aceb)
      locVars = concatMap localVars (fDeclRes $ fpExprs aceb)
      prRealInt  (Arg x _) = text "r_" <> text x
      prErrorInt (Arg x _) = text "e_" <> text x
      ACeb {conds = c} = aceb
  
  prInfoLemma :: ControlFlow -> [FAExpr] -> [AExpr] -> Doc
  prInfoLemma cflow fpes reales = text "% Floating-Point Results:"<+> hsep (punctuate comma $ map prettyDoc fpes)
    $$
    text "% Real Results:"<+> hsep (punctuate comma $ map prettyDoc reales)
    $$
    text "% Control Flow: "<+> prettyDoc cflow
  
  prPvsNumProof :: Doc -> Doc -> Int -> Int -> Doc
  prPvsNumProof numLemma symbLemma prec maxBBDepth =
       text "%|-" <+> numLemma <+> text ": PROOF"
    $$ text "%|-" <+> parens (text "prove-concrete-lemma" <+> symbLemma <+> int prec <+> int maxBBDepth)
    $$ text "%|- QED\n"
  
  prPvsNumLemma :: Doc
                  -> String
                  -> String
                  -> ResultField
                  -> [Arg]
                  -> Conditions
                  -> Double
                  -> [VarBind]
                  -> PVSType
                  -> Maybe AExpr
                  -> [FAExpr]
                  -> Doc
  prPvsNumLemma nameLemma f fReal field args cond roundOffError ranges fp symbError _fpGuards =
    nameLemma <+> text ": LEMMA"
    $$ text "FORALL(" <>  hsep (punctuate comma $ map (prettyDoc . realVar . arg2var) args)
                      <>  text ": real" <> comma
                      <+> hsep (punctuate comma $ map prettyDoc args) <> text ")" <> text ":"
    $$ prPvsArgs args
    $$ (if isTrueCondition cond then empty else text "AND" <+> parens (prettyDoc cond))
    <+> text "AND"
    $$ hsep (punctuate (text " AND ") $ map printVarRange ranges)
    $$ text "IMPLIES"
    $$ lhs
    <+> text "<="
    <+> prettyRatNumError roundOffError <> text "\n"
    where
      divergence =  text "abs("
        <>  f2r fp (printNameWithField (text f <> text "("
        <>  hsep (punctuate comma $ map (prettyDoc . arg2var) args) <> text ")") field)
        <+> text "-"
        <+> printNameWithField (text fReal <> text "("
        <>  hsep (punctuate comma $ map (prettyDoc . realVar . arg2var) args) <> text ")") field
        <>  text ")"
      lhs = maybe divergence prettyDoc symbError
  
  prPvsArgsSymb :: [Arg] -> Doc
  prPvsArgsSymb arguments = hsep $ punctuate (text " AND") $ map prPVSVarIdSymb arguments
  
  prPVSVarIdSymb :: Arg -> Doc
  prPVSVarIdSymb (Arg x (Tuple ts)) = vcat $ zipWith (curry (prPVSVarIdSymb . tuple2Arg)) ts indexes
    where
      tuple2Arg (idxType, idx) = Arg (x ++ "_" ++ show idx) idxType
      indexes = [1..] :: [Int]
  prPVSVarIdSymb (Arg x (Record fs)) = vcat $ map (prPVSVarIdSymb . record2Arg) fs
    where
      record2Arg (field,fieldType) = Arg (x ++ "_" ++ field) fieldType
  prPVSVarIdSymb (Arg x t) = text "abs(" <> f2r t (text x)
                                 <+> text "-" <+> text "r_" <> text x <> text ")"
                                 <> text "<=" <> text "e_" <> text x
  
  prPvsArgs :: [Arg] -> Doc
  prPvsArgs arguments = hsep $ punctuate (text " AND") $ map (uncurry prPVSVarId . mapArg2Pair) arguments
  
  prPVSVarId :: VarName -> PVSType -> Doc
  prPVSVarId _ (TypeFun _ _) = empty
  prPVSVarId x (Tuple ts) = vcat $ zipWith (curry (uncurry prPVSVarId . tuple2Arg)) ts indexes
    where
      tuple2Arg (idxType, idx) = (x ++ "_" ++ show idx, idxType)
      indexes = [1..] :: [Int]
  prPVSVarId x (Record fs) = vcat $ map (uncurry prPVSVarId . record2Arg) fs
    where
      record2Arg (field,fieldType) = (x ++ "_" ++ field, fieldType)
  prPVSVarId x TInt = text "abs("<> text x <+> text "-" <+> text "r_" <> text x <> text ")" <> text "<= 0"
  prPVSVarId x fpx  = text "abs(" <> f2r fpx (text x)
                         <+> text "-" <+> text "r_" <> text x <> text ")"
                         <> text "<=" <> prettyDoc (HalfUlp (RealMark x ResValue) fpx)
  
  printVarRange :: VarBind -> Doc
  printVarRange (VarBind x ResValue _ lb ub) =
    text "r_" <> text x <+> text "##" <+> text "[|" <> prettyDoc lb <> comma <> prettyDoc ub <> text "|]"
  printVarRange (VarBind x (ResRecordField field) _ lb ub) =
    text "r_" <> text x <> text "`" <> text field <+> text "##" <+> text "[|" <> prettyDoc lb <> comma <> prettyDoc ub <> text "|]"
  printVarRange (VarBind x (ResTupleIndex idx) _ lb ub) =
    text "r_" <> text x <> text "`" <> integer idx <+> text "##" <+> text "[|" <> prettyDoc lb <> comma <> prettyDoc ub <> text "|]"
  
  prettyRatNumError :: RealFloat a => a -> Doc
  prettyRatNumError roundOffError = text $ showRational (toRational roundOffError )
  
  prettyNumError :: RealFloat a => a -> Doc
  prettyNumError roundOffError = text $ showFFloat Nothing roundOffError "" -- (nextUp' roundOffError) ""
  
  f2r :: PVSType -> Doc -> Doc
  f2r fp doc = case fp of
    FPSingle -> text "StoR" <> parens doc
    FPDouble -> text "DtoR" <> parens doc
    TInt -> doc
    Boolean -> doc
    Array _ FPSingle -> text "StoR" <> parens doc
    Array _ FPDouble -> text "DtoR" <> parens doc
    Array _ _ -> doc
    List  FPSingle -> text "StoR" <> parens doc
    List  FPDouble -> text "DtoR" <> parens doc
    List  _ -> doc
    TypeFun _ _ -> doc
    t -> error $ "f2r: something went wrong, f2r not defined for " ++ show t
  
  genExprCertFile :: PVSType -> String -> String -> String -> Doc -> Doc
  genExprCertFile fp inputFileName fpFileName fileName printTranProgPairs =
    text "% This file is automatically generated by PRECiSA \n"
    $$
    text (fileName ++ ": THEORY")
    $$
    text "BEGIN"
    $$
    text "IMPORTING" <+> ieeeFormalization fp <> text ", PRECiSA@strategies, PRECiSA@bbiasp, PRECiSA@bbiadp,"
    <+>
    text inputFileName
    <>
    comma
    <+>
    text fpFileName
    $$
    text "\n%|- *_TCC* : PROOF"
    $$
    text "%|- (precisa-gen-cert-tcc)"
    $$
    text "%|- QED\n"
    $$
    printTranProgPairs
    $$
    text ("\nEND " ++ fileName)
    where
      ieeeFormalization FPDouble = text "float_bounded_axiomatic@ieee754_double"
      ieeeFormalization FPSingle = text "float_bounded_axiomatic@ieee754_single"
      ieeeFormalization t = error $ "genExprCertFile: PVS type " ++ show t ++ " not supported."
  
  prIsFiniteHpExpr :: [FAExpr] -> Doc
  prIsFiniteHpExpr [] = emptyDoc
  prIsFiniteHpExpr aes = text "AND"
                         $$ hsep (punctuate (text " AND") (map prIsFinite aes))
  
  printSymbExprCert :: PVSType -> String -> [FAExpr] -> [AExpr] -> [AExpr] -> FAExpr -> AExpr -> FBExpr -> EExpr -> Int -> Doc
  printSymbExprCert fp f faeVarList errVarList realVarList fae ae be symbErr n =
    text f <> text "_expr_" <> int n <+> text ": LEMMA"
    $$ text "FORALL(" <>  hsep (punctuate comma $ map prettyVarWithType faeVarList)
                      <> comma
                      <+> hsep (punctuate comma $ map prettyDoc errVarList)
                      <>  text ": nonneg_real" <> comma
                      <+> hsep (punctuate comma $ map prettyDoc realVarList)
                      <>  text ": real"
                      <> text ")" <> text ":"
    $$ hsep (punctuate (text " AND") (map (printVarErrBound fp) faeVarList))
    $$ text "AND" <+> parens (prettyDoc be)
    -- $$ prIsFiniteHpExpr (fae:faeVarList)
    $$ text "IMPLIES"
    $$ text "abs(" <> f2r fp (prettyDoc fae)
       <+> text "-"
       <+> prettyDoc ae <> text ")"
       <+> text "<="
       <+> prettyError symbErr
    $$ text "\n%|- " <> text f <> text "_" <> int n <> text ": PROOF"
    $$ text "%|- (precisa)"
    $$ text "%|- QED"
    $$ text "\n"
  
  printNumExprCert :: PVSType -> String -> [FAExpr] -> [AExpr] -> FAExpr -> AExpr -> FBExpr -> Double -> [VarBind] -> Int -> Int -> Int -> Doc
  printNumExprCert fp f faeVarList realVarList fae ae be roundOffError ranges n maxBBDepth prec  =
    text f <> text "_expr_num_" <> int n <+> text ": LEMMA"
    $$ text "FORALL(" <>  hsep (punctuate comma $ map prettyVarWithType faeVarList)
                      <>  comma
                      <+> hsep (punctuate comma $ map prettyDoc realVarList)
                      <>  text ": real"
                      <>  text ")" <> text ":"
    $$ hsep (punctuate (text " AND") $ map (uncurry prPVSVarId . (\a -> (nameFVar a, precFVar a))) faeVarList)
    $$ text "AND"
    <+> parens (prettyDoc be)
    $$ text "AND" <+> hsep (punctuate (text " AND ") $ map printVarRange ranges)
    $$ text "IMPLIES"
    $$ text "abs(" <> f2r fp (prettyDoc fae)
       <+> text "-"
       <+> prettyDoc ae <> text ")"
       <+> text "<="
    <> prettyRatNumError roundOffError  <> text "\n"
    $$ text "%|-" <+> text f <> text "_c_" <> int n <+> text ": PROOF"
    $$ text "%|-" <+> parens (text "prove-concrete-lemma" <+> text f <> text "_expr_" <> int n <+> int prec <+> int maxBBDepth)
    $$ text "%|- QED\n"
  
  printVarErrBound :: PVSType -> FAExpr -> Doc
  printVarErrBound fp var@(FVar _ _) = text "abs(" <> f2r fp (prettyDoc var)
                                                   <> text "-"
                                                   <> prettyDoc (realVar var)
                                                   <> text ")<=" <> prettyDoc (errVar var)
  printVarErrBound _ ae = error $ "printVarErrBound: case " ++ show ae ++ " not expected."
  
  printExprFunCert :: Int -> Int -> PVSType -> (Decl, [(VarName,FAExpr,AExpr,FBExpr,EExpr,Double,[FAExpr],[AExpr],[EExpr],[VarBind])]) -> Doc
  printExprFunCert maxDepth minPrec fp (Decl _ _ f _ _, exprList) = vcat $ zipWith (printExprCert' maxDepth minPrec fp f) exprList [1 :: Int, 2 ..]
  printExprFunCert        _       _ _ (Pred _ TauMinus _ _ _, _) = emptyDoc
  printExprFunCert maxDepth minPrec fp (Pred _ _ f _ _, exprList) = vcat $ zipWith (printExprCert' maxDepth minPrec fp f) exprList [1 :: Int, 2 ..]
  printExprFunCert _ _ _ x = error $ "[printExprFunCert] Unhandled case: " ++ show x
  
  printExprCert' :: Int -> Int -> PVSType -> String -> (VarName,FAExpr,AExpr,FBExpr,EExpr,Double,[FAExpr],[AExpr],[EExpr],[VarBind]) -> Int -> Doc
  printExprCert' maxDepth minPrec fp f (_,fae, ae, be, symbErr, numErr, faeVarList, realVarList, errVarList,varBinds) n =
    printSymbExprCert fp f faeVarList errVarList realVarList fae ae be symbErr n
    $$
    printNumExprCert fp f faeVarList realVarList fae ae be numErr varBindsRestricted n maxDepth minPrec
    where
      varBindsRestricted = filter (isVarInList (map fvarName faeVarList)) varBinds
      isVarInList vars (VarBind x _ _ _ _) = x `elem` vars
  