
   0 | module Idris.Syntax.Pragmas
   1 | 
   2 | import Data.String
   3 | 
   4 | %default total
   5 | 
   6 | public export
   7 | data KwPragma
   8 |   = KwHint
   9 |   | KwHide
  10 |   | KwUnhide
  11 |   | KwLogging
  12 |   | KwAutoLazy
  13 |   | KwUnboundImplicits
  14 |   | KwAmbiguityDepth
  15 |   | KwPair
  16 |   | KwRewrite
  17 |   | KwIntegerLit
  18 |   | KwStringLit
  19 |   | KwCharLit
  20 |   | KwDoubleLit
  21 |   | KwName
  22 |   | KwStart
  23 |   | KwAllowOverloads
  24 |   | KwLanguage
  25 |   | KwDefault
  26 |   | KwPrefixRecordProjections
  27 |   | KwAutoImplicitDepth
  28 |   | KwNfMetavarThreshold
  29 |   | KwSearchTimeOut
  30 | 
  31 | public export
  32 | data LangExt
  33 |   = ElabReflection
  34 | 
  35 | export
  36 | allLangExts : List LangExt
  37 | allLangExts = [ElabReflection]
  38 | 
  39 | export
  40 | Show LangExt where
  41 |   show ElabReflection = "ElabReflection"
  42 | 
  43 | export
  44 | Eq LangExt where
  45 |   ElabReflection == ElabReflection = True
  46 | 
  47 | public export
  48 | data PragmaArg
  49 |   = AName String
  50 |   | ANameList
  51 |   | APairArg
  52 |   | ARewriteArg
  53 |   | AnOnOff
  54 |   | AnOptionalLoggingTopic
  55 |   | ANat
  56 |   | AnExpr
  57 |   | ALangExt
  58 |   | ATotalityLevel
  59 | 
  60 | export
  61 | Show PragmaArg where
  62 |   show (AName str) = str
  63 |   show ANameList = "nm xs f"
  64 |   show APairArg = "ty fst snd"
  65 |   show ARewriteArg = "eq rew"
  66 |   show AnOnOff = "on|off"
  67 |   show AnOptionalLoggingTopic = "[topic]"
  68 |   show ANat = "nat"
  69 |   show AnExpr = "expr"
  70 |   show ALangExt = concat $ intersperse "|" $ map show allLangExts
  71 |   show ATotalityLevel = "partial|total|covering"
  72 | 
  73 | export
  74 | pragmaArgs : KwPragma -> List PragmaArg
  75 | pragmaArgs KwHint = []
  76 | pragmaArgs KwHide = [AName "nm"]
  77 | pragmaArgs KwUnhide = [AName "nm"]
  78 | pragmaArgs KwLogging = [AnOptionalLoggingTopic, ANat]
  79 | pragmaArgs KwAutoLazy = [AnOnOff]
  80 | pragmaArgs KwUnboundImplicits = [AnOnOff]
  81 | pragmaArgs KwAmbiguityDepth = [ANat]
  82 | pragmaArgs KwPair = [APairArg]
  83 | pragmaArgs KwRewrite = [ARewriteArg]
  84 | pragmaArgs KwIntegerLit = [AName "nm"]
  85 | pragmaArgs KwStringLit = [AName "nm"]
  86 | pragmaArgs KwCharLit = [AName "nm"]
  87 | pragmaArgs KwDoubleLit = [AName "nm"]
  88 | pragmaArgs KwName = [ANameList]
  89 | pragmaArgs KwStart = [AnExpr]
  90 | pragmaArgs KwAllowOverloads = [AName "nm"]
  91 | pragmaArgs KwLanguage = [ALangExt]
  92 | pragmaArgs KwDefault = [ATotalityLevel]
  93 | pragmaArgs KwPrefixRecordProjections = [AnOnOff]
  94 | pragmaArgs KwAutoImplicitDepth = [ANat]
  95 | pragmaArgs KwNfMetavarThreshold = [ANat]
  96 | pragmaArgs KwSearchTimeOut = [ANat]
  97 | 
  98 | export
  99 | Show KwPragma where
 100 |   show kw = case kw of
 101 |     KwHint => "%hint"
 102 |     KwHide => "%hide"
 103 |     KwUnhide => "%unhide"
 104 |     KwLogging => "%logging"
 105 |     KwAutoLazy => "%auto_lazy"
 106 |     KwUnboundImplicits => "%unbound_implicits"
 107 |     KwAmbiguityDepth => "%ambiguity_depth"
 108 |     KwPair => "%pair"
 109 |     KwRewrite => "%rewrite"
 110 |     KwIntegerLit => "%integerLit"
 111 |     KwStringLit => "%stringLit"
 112 |     KwCharLit => "%charLit"
 113 |     KwDoubleLit => "%doubleLit"
 114 |     KwName => "%name"
 115 |     KwStart => "%start"
 116 |     KwAllowOverloads => "%allow_overloads"
 117 |     KwLanguage => "%language"
 118 |     KwDefault => "%default"
 119 |     KwPrefixRecordProjections => "%prefix_record_projections"
 120 |     KwAutoImplicitDepth => "%auto_implicit_depth"
 121 |     KwNfMetavarThreshold => "%nf_metavar_threshold"
 122 |     KwSearchTimeOut => "%search_timeout"
 123 | 
 124 | export
 125 | allPragmas : List KwPragma
 126 | allPragmas =
 127 |   [ KwHint
 128 |   , KwHide
 129 |   , KwUnhide
 130 |   , KwLogging
 131 |   , KwAutoLazy
 132 |   , KwUnboundImplicits
 133 |   , KwAmbiguityDepth
 134 |   , KwPair
 135 |   , KwRewrite
 136 |   , KwIntegerLit
 137 |   , KwStringLit
 138 |   , KwCharLit
 139 |   , KwDoubleLit
 140 |   , KwName
 141 |   , KwStart
 142 |   , KwAllowOverloads
 143 |   , KwLanguage
 144 |   , KwDefault
 145 |   , KwPrefixRecordProjections
 146 |   , KwAutoImplicitDepth
 147 |   , KwNfMetavarThreshold
 148 |   , KwSearchTimeOut
 149 |   ]
 150 | 
 151 | export
 152 | pragmaTopics : String
 153 | pragmaTopics
 154 |   = concat $ intersperse "\n" $ map ("+ " ++)
 155 |   $ map (\ kw => unwords (show kw :: map show (pragmaArgs kw)))
 156 |   $ allPragmas
 157 |