{- Basic combinator for generating the text of a lemma declaration. -}

lemmaText :: ResolveHint -- Resolve hint?
          -> RewriteHint -- Rewrite hint?
          -> DocHide     -- Hide documentation?
          -> [String]    -- Hint databases.
          -> String      -- Name of the lemma
          -> String      -- Statment of the lemma
          -> String      -- Proof of the lemma
          -> M String
lemmaText resolve rewrite hide dbs name stmt proof =
    do { (flags, _) <- get
       ; return $ printf "%s\
                         \Lemma %s :\n\
                         \%s.\n\
                         \%s\
                         \%s%s%s%s"
         (case hide of
            NoHide -> ""
            Hide   -> "(* begin hide *)\n\n")
         name
         stmt
         (if CoqAdmitted `elem` flags
          then "Proof. Admitted.\n\n"
          else printf "Proof.\n\
                      \%s\n\
                      \Qed.\n\
                      \\n"
                      proof)
         (case resolve of
            NoResolve -> ""
            Resolve   -> printf "Hint Resolve %s : %s.\n" name (sepStrings " " dbs)
            Immediate -> printf "Hint Immediate %s : %s.\n" name (sepStrings " " dbs))
         (case rewrite of
            NoRewrite -> ""
            Rewrite   -> printf "Hint Rewrite %s using solve [auto] : %s.\n" name (sepStrings " " dbs))
         (case (resolve, rewrite) of
            (NoResolve, NoRewrite) -> ""
            _ -> "\n")
         (case hide of
            NoHide -> ""
            Hide   -> "(* end hide *)\n\n")
       }
lemmaText :: ResolveHint -- Resolve hint?
          -> RewriteHint -- Rewrite hint?
          -> DocHide     -- Hide documentation?
          -> [String]    -- Hint databases.
          -> String      -- Name of the lemma
          -> String      -- Statment of the lemma
          -> String      -- Proof of the lemma
          -> M String
lemmaText resolve rewrite hide dbs name stmt proof =
    do { (flags, _) <- get
       ; return $ printf "%s\
                         \Lemma %s :\n\
                         \%s.\n\
                         \%s\
                         \%s%s%s%s"
         (case hide of
            NoHide -> ""
            Hide   -> "(* begin hide *)\n\n")
         name
         stmt
         (if CoqAdmitted `elem` flags
          then "Proof. Admitted.\n\n"
          else printf "Proof.\n\
                      \%s\n\
                      \Qed.\n\
                      \\n"
                      proof)
         (case resolve of
            NoResolve -> ""
            Resolve   -> printf "Hint Resolve %s : %s.\n" name (sepStrings " " dbs)
            Immediate -> printf "Hint Immediate %s : %s.\n" name (sepStrings " " dbs))
         (case rewrite of
            NoRewrite -> ""
            Rewrite   -> printf "Hint Rewrite %s using solve [auto] : %s.\n" name (sepStrings " " dbs))
         (case (resolve, rewrite) of
            (NoResolve, NoRewrite) -> ""
            _ -> "\n")
         (case hide of
            NoHide -> ""
            Hide   -> "(* end hide *)\n\n")
       }
lemmaText resolve rewrite hide dbs name stmt proof =
    do { (flags, _) <- get
       ; return $ printf "%s\
                         \Lemma %s :\n\
                         \%s.\n\
                         \%s\
                         \%s%s%s%s"
         (case hide of
            NoHide -> ""
            Hide   -> "(* begin hide *)\n\n")
         name
         stmt
         (if CoqAdmitted `elem` flags
          then "Proof. Admitted.\n\n"
          else printf "Proof.\n\
                      \%s\n\
                      \Qed.\n\
                      \\n"
                      proof)
         (case resolve of
            NoResolve -> ""
            Resolve   -> printf "Hint Resolve %s : %s.\n" name (sepStrings " " dbs)
            Immediate -> printf "Hint Immediate %s : %s.\n" name (sepStrings " " dbs))
         (case rewrite of
            NoRewrite -> ""
            Rewrite   -> printf "Hint Rewrite %s using solve [auto] : %s.\n" name (sepStrings " " dbs))
         (case (resolve, rewrite) of
            (NoResolve, NoRewrite) -> ""
            _ -> "\n")
         (case hide of
            NoHide -> ""
            Hide   -> "(* end hide *)\n\n")
       }