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