CurryInfo: verify-3.1.0 / ToAgda.theoremToAgda

 
theoremToAgda :: Options -> QName -> [CFuncDecl] -> [CTypeDecl] -> IO ()
theoremToAgda opts qtheo@(_,theoname) allfuncs alltypes = do
  let (rename, orgtypedrules)  = funcDeclsToTypedRules allfuncs
      transform = if optScheme opts == "nondet" then transformRuleWithNondet
                                                else transformRuleWithChoices
      typedrules = concatMap (transform opts) orgtypedrules
      (theorules,funcrules) = partition (\ (fn,_,_,_) -> fn == qtheo)
                                        typedrules
      mname = "TO-PROVE-" ++ theoname
      hrule = take 75 (repeat '-')
      agdaprog = unlines $
                  agdaHeader opts mname ++
                  [hrule, "-- Translated Curry operations:",""] ++
                  map typeDeclAsAgda alltypes ++
                  showTypedTRSAsAgda opts rename [] funcrules ++
                  [hrule, ""] ++
                  concatMap (theoremAsAgda rename) theorules ++
                  [hrule]
  --putStr agdaprog
  let agdafile = mname ++ ".agda"
  when (optVerb opts > 1 || not (optStore opts)) $ putStr agdaprog
  when (optStore opts) $ do
    writeFile agdafile agdaprog
    when (optScheme opts == "nondet") $
      mapM_ copyImport ["nondet.agda","nondet-thms.agda"]
    when (optVerb opts > 0) $ putStrLn $
     "Agda module '" ++ agdafile ++ "' written.\n" ++
     "If you completed the proof, rename it to 'PROOF-" ++ theoname ++ ".agda'."

 argument 2

 deterministic operation

 
Generate an Agda program file for a given theorem name and the
list of all functions involved in this theorem.

 <FAILING>

 referentially transparent operation

 no fixity defined

 {(_,{(,)},_,_) |-> _}

 theoremToAgda

 no precedence defined

 _

 VerifyOptions.Options -> (String, String) -> [AbstractCurry.Types.CFuncDecl]
-> [AbstractCurry.Types.CTypeDecl] -> Prelude.IO ()

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term