{-|
Module      : HsToCoq.Coq.Preamble
Description : Static preamble for all hs-to-coq output
Copyright   : Copyright © 2017 Antal Spector-Zabusky, University of Pennsylvania
License     : MIT
Maintainer  : antal.b.sz@gmail.com
Stability   : experimental
-}

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE OverloadedLists #-}

module HsToCoq.Coq.Preamble
    ( staticPreamble
    , builtInAxioms
    ) where

import Data.Text (Text)
import qualified Data.Text as T
import HsToCoq.Coq.Gallina
import HsToCoq.Coq.Gallina.Orphans ()
import qualified Data.Map as M
import Data.Bifunctor

staticPreamble :: Text
staticPreamble = T.unlines
 [ "(* Default settings (from HsToCoq.Coq.Preamble) *)"
 , ""
 , "Generalizable All Variables."
 , ""
 , "Unset Implicit Arguments."
 , "Set Maximal Implicit Insertion."
 , "Unset Strict Implicit."
 , "Unset Printing Implicit Defensive."
 , ""
 , "Require Coq.Program.Tactics."
 , "Require Coq.Program.Wf."
 ]

-- | When a free variable of this name appears in the output,
-- an axiom of the type given here is added to the preamble
builtInAxioms :: M.Map Qualid Term
builtInAxioms = M.fromList $ map (first Bare)
    [ "missingValue"   =: Forall [ ImplicitBinders (pure (Ident (Bare "a"))) ] a
    ]
  where
   a = "a"
   (=:) = (,)
   infix 0 =:
