-- | This module exports lists for keywords of the Gallina specification
--   language and Vernacular commands.
module FreeC.Backend.Coq.Keywords where

-- | Keywords of the Gallina specification language.
--
--   This list has been taken from the Coq documentation
--   <https://coq.inria.fr/refman/language/gallina-specification-language.html>.
coqKeywords :: [String]
coqKeywords
  = [ "as"
    , "at"
    , "cofix"
    , "else"
    , "end"
    , "exists"
    , "exists2"
    , "fix"
    , "for"
    , "forall"
    , "fun"
    , "if"
    , "IF"
    , "in"
    , "let"
    , "match"
    , "mod"
    , "Prop"
    , "return"
    , "Set"
    , "then"
    , "Type"
    , "using"
    , "where"
    , "with"
    ]

-- | Identifiers that should not be used in Coq, because they are used in
--   a command of The Vernacular.
--
--   This list contains all words of the commands listed in
--   <https://coq.inria.fr/refman/coq-cmdindex.html>.
vernacularCommands :: [String]
vernacularCommands
  = [ "Abort"
    , "About"
    , "Add"
    , "Admit"
    , "Admitted"
    , "All"
    , "Arguments"
    , "Assumptions"
    , "Axiom"
    , "Axioms"
    , "Back"
    , "BackTo"
    , "Backtrack"
    , "Bind"
    , "Blacklist"
    , "Canonical"
    , "Cd"
    , "Check"
    , "Class"
    , "Classes"
    , "Close"
    , "CoFixpoint"
    , "CoInductive"
    , "Coercion"
    , "Coercions"
    , "Collection"
    , "Combined"
    , "Compute"
    , "Conjecture"
    , "Conjectures"
    , "Constant"
    , "Constants"
    , "Constraint"
    , "Constructors"
    , "Context"
    , "Corollary"
    , "Create"
    , "Cumulative"
    , "Custom"
    , "Cut"
    , "Declare"
    , "Defined"
    , "Definition"
    , "Delimit"
    , "Dependencies"
    , "Derive"
    , "Drop"
    , "End"
    , "Entry"
    , "Equality"
    , "Eval"
    , "Example"
    , "Existential"
    , "Existentials"
    , "Existing"
    , "Export"
    , "Extern"
    , "Extract"
    , "Extraction"
    , "Fact"
    , "Fail"
    , "Field"
    , "File"
    , "Firstorder"
    , "Fixpoint"
    , "Focus"
    , "Function"
    , "Functional"
    , "Generalizable"
    , "Global"
    , "Goal"
    , "Grab"
    , "Grammar"
    , "Graph"
    , "Guarded"
    , "Heap"
    , "Hint"
    , "HintDb"
    , "Hints"
    , "Hypotheses"
    , "Hypothesis"
    , "Identity"
    , "Immediate"
    , "Implicit"
    , "Implicits"
    , "Import"
    , "Include"
    , "Inductive"
    , "Infix"
    , "Info"
    , "Inline"
    , "Inlined"
    , "Inspect"
    , "Instance"
    , "Instances"
    , "Intro"
    , "Intros"
    , "Inversion"
    , "Language"
    , "Left"
    , "Lemma"
    , "Let"
    , "Libraries"
    , "Library"
    , "Load"
    , "LoadPath"
    , "Local"
    , "Locate"
    , "Ltac"
    , "ML"
    , "Mode"
    , "Module"
    , "Modules"
    , "Monomorphic"
    , "Morphism"
    , "Next"
    , "No"
    , "NoInline"
    , "NonCumulative"
    , "Notation"
    , "Numeral"
    , "Obligation"
    , "Obligations"
    , "Opaque"
    , "Open"
    , "Optimize"
    , "Options"
    , "Parameter"
    , "Parameters"
    , "Parametric"
    , "Path"
    , "Paths"
    , "Polymorphic"
    , "Prenex"
    , "Preterm"
    , "Print"
    , "Profile"
    , "Program"
    , "Projections"
    , "Proof"
    , "Proposition"
    , "Pwd"
    , "Qed"
    , "Quit"
    , "Rec"
    , "Record"
    , "Recursive"
    , "Redirect"
    , "Reduction"
    , "Relation"
    , "Remark"
    , "Remove"
    , "Require"
    , "Reset"
    , "Resolve"
    , "Restart"
    , "Rewrite"
    , "Right"
    , "Ring"
    , "Save"
    , "Scheme"
    , "Scope"
    , "Scopes"
    , "Script"
    , "Search"
    , "SearchAbout"
    , "SearchHead"
    , "SearchPattern"
    , "SearchRewrite"
    , "Section"
    , "Separate"
    , "Set"
    , "Setoid"
    , "Show"
    , "Signatures"
    , "Solve"
    , "Solver"
    , "Step"
    , "Strategy"
    , "Structure"
    , "SubClass"
    , "Table"
    , "Tables"
    , "Tactic"
    , "Term"
    , "Test"
    , "TestCompile"
    , "Theorem"
    , "Time"
    , "Timeout"
    , "Transparent"
    , "Type"
    , "Typeclasses"
    , "Types"
    , "Undelimit"
    , "Undo"
    , "Unfocus"
    , "Unfocused"
    , "Unfold"
    , "Universe"
    , "Universes"
    , "Unset"
    , "Unshelve"
    , "Variable"
    , "Variables"
    , "Variant"
    , "View"
    , "Visibility"
    ]