{- Combinator used for generating the text of a lemma proved by mutual
   induction/recursion. -}

mutualLemmaText :: ResolveHint -- Resolve hint?
                -> RewriteHint -- Rewrite hint?
                -> DocHide     -- Hide documentation?
                -> [String]    -- Hint databases.
                -> Sort        -- Sort
                -> [String]    -- Names for the parts.
                -> [String]    -- Statments for the parts.
                -> String      -- Proof of the lemma.
                -> M String
mutualLemmaText resolve rewrite hide dbs sort names stmts proof =
    do { let mut_name  = sepStrings "_" names ++ "_mutual"
             mut_stmts = combine sort $ map wrap stmts
             cproof      = printf "pose proof %s as H; intuition eauto." mut_name
       ; lemma <- lemmaText NoResolve NoRewrite Hide dbs mut_name mut_stmts proof
       ; corollaries <- mapM (\(name, stmt) ->
                                  lemmaText resolve rewrite hide dbs name stmt cproof)
                             (zip names stmts)
       ; return $ lemma ++ concat corollaries
       }
    where
      combine Set  = sepStrings " *\n"
      combine Prop = sepStrings " /\\\n"
      wrap str     = printf "(%s)" str

{- Combinator used for generating the text of a lemma proved by mutual
   induction/recursion. -}
mutualLemmaText :: ResolveHint -- Resolve hint?
                -> RewriteHint -- Rewrite hint?
                -> DocHide     -- Hide documentation?
                -> [String]    -- Hint databases.
                -> Sort        -- Sort
                -> [String]    -- Names for the parts.
                -> [String]    -- Statments for the parts.
                -> String      -- Proof of the lemma.
                -> M String
mutualLemmaText resolve rewrite hide dbs sort names stmts proof =
    do { let mut_name  = sepStrings "_" names ++ "_mutual"
             mut_stmts = combine sort $ map wrap stmts
             cproof      = printf "pose proof %s as H; intuition eauto." mut_name
       ; lemma <- lemmaText NoResolve NoRewrite Hide dbs mut_name mut_stmts proof
       ; corollaries <- mapM (\(name, stmt) ->
                                  lemmaText resolve rewrite hide dbs name stmt cproof)
                             (zip names stmts)
       ; return $ lemma ++ concat corollaries
       }
    where
      combine Set  = sepStrings " *\n"
      combine Prop = sepStrings " /\\\n"
      wrap str     = printf "(%s)" str

{- Combinator used for generating the text of a lemma proved by mutual
   induction/recursion. -}
mutualLemmaText resolve rewrite hide dbs sort names stmts proof =
    do { let mut_name  = sepStrings "_" names ++ "_mutual"
             mut_stmts = combine sort $ map wrap stmts
             cproof      = printf "pose proof %s as H; intuition eauto." mut_name
       ; lemma <- lemmaText NoResolve NoRewrite Hide dbs mut_name mut_stmts proof
       ; corollaries <- mapM (\(name, stmt) ->
                                  lemmaText resolve rewrite hide dbs name stmt cproof)
                             (zip names stmts)
       ; return $ lemma ++ concat corollaries
       }
    where
      combine Set  = sepStrings " *\n"
      combine Prop = sepStrings " /\\\n"
      wrap str     = printf "(%s)" str

{- Combinator used for generating the text of a lemma proved by mutual
   induction/recursion. -}