
   0 | module Language.Reflection
   1 | 
   2 | import public Language.Reflection.TT
   3 | import public Language.Reflection.TTImp
   4 | 
   5 | import public Control.Monad.Trans
   6 | 
   7 | %default total
   8 | 
   9 | ----------------------------------
  10 | --- Elaboration data structure ---
  11 | ----------------------------------
  12 | 
  13 | public export
  14 | data LookupDir =
  15 |   ||| The dir of the `ipkg`-file, or the current dir if there is no one
  16 |   ProjectDir |
  17 |   ||| The source dir set in the `ipkg`-file, or the current dir if there is no one
  18 |   SourceDir |
  19 |   ||| The dir where the current module is located
  20 |   |||
  21 |   ||| For the module `Language.Reflection` it would be `<source_dir>/Language/`
  22 |   CurrentModuleDir |
  23 |   ||| The dir where submodules of the current module are located
  24 |   |||
  25 |   ||| For the module `Language.Reflection` it would be `<source_dir>/Language/Reflection/`
  26 |   SubmodulesDir |
  27 |   ||| The dir where built files are located, set in the `ipkg`-file and defaulted to `build`
  28 |   BuildDir
  29 | 
  30 | ||| Elaboration scripts
  31 | ||| Where types/terms are returned, binders will have unique, if not
  32 | ||| necessarily human readable, names
  33 | export
  34 | data Elab : Type -> Type where
  35 |      Pure : a -> Elab a
  36 |      Map  : (a -> b) -> Elab a -> Elab b
  37 |      Ap   : Elab (a -> b) -> Elab a -> Elab b
  38 |      Bind : Elab a -> (a -> Elab b) -> Elab b
  39 |      Fail : FC -> String -> Elab a
  40 |      Warn : FC -> String -> Elab ()
  41 | 
  42 |      Try : Elab a -> Elab a -> Elab a
  43 | 
  44 |      ||| Log a message. Takes a
  45 |      ||| * topic
  46 |      ||| * level
  47 |      ||| * message
  48 |      LogMsg : String -> Nat -> String -> Elab ()
  49 |      ||| Print and log a term. Takes a
  50 |      ||| * topic
  51 |      ||| * level
  52 |      ||| * message
  53 |      ||| * term
  54 |      LogTerm : String -> Nat -> String -> TTImp -> Elab ()
  55 |      ||| Resugar, print and log a term. Takes a
  56 |      ||| * topic
  57 |      ||| * level
  58 |      ||| * message
  59 |      ||| * term
  60 |      LogSugaredTerm : String -> Nat -> String -> TTImp -> Elab ()
  61 | 
  62 |      ResugarTerm : (maxLineWidth : Maybe Nat) -> TTImp -> Elab String
  63 | 
  64 |      -- Elaborate a TTImp term to a concrete value
  65 |      Check : TTImp -> Elab expected
  66 |      -- Quote a concrete expression back to a TTImp
  67 |      Quote : (0 _ : val) -> Elab TTImp
  68 | 
  69 |      -- Elaborate under a lambda
  70 |      Lambda : (0 x : Type) ->
  71 |               {0 ty : x -> Type} ->
  72 |               ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val))
  73 | 
  74 |      -- Get the current goal type, if known
  75 |      -- (it might need to be inferred from the solution)
  76 |      Goal : Elab (Maybe TTImp)
  77 |      -- Get the names of local variables in scope
  78 |      LocalVars : Elab (List Name)
  79 |      -- Generate a new unique name, based on the given string
  80 |      GenSym : String -> Elab Name
  81 |      -- Put a name in the current namespace
  82 |      InCurrentNS : Name -> Elab Name
  83 |      -- Get the types of every name which matches.
  84 |      -- There may be ambiguities - returns a list of fully explicit names
  85 |      -- and their types. If there's no results, the name is undefined.
  86 |      GetType : Name -> Elab (List (Name, TTImp))
  87 |      -- Get the metadata associated with a name
  88 |      GetInfo : Name -> Elab (List (Name, NameInfo))
  89 |      -- Get the visibility associated with a name
  90 |      GetVis : Name -> Elab (List (Name, Visibility))
  91 |      -- Get the type of a local variable
  92 |      GetLocalType : Name -> Elab TTImp
  93 |      -- Get the constructors of a data type. The name must be fully resolved.
  94 |      GetCons : Name -> Elab (List Name)
  95 |      -- Get all function definition names referred in a definition. The name must be fully resolved.
  96 |      GetReferredFns : Name -> Elab (List Name)
  97 |      -- Get the name of the current and outer functions, if it is applicable
  98 |      GetCurrentFn : Elab (SnocList Name)
  99 |      -- Get the source location of the macro call site
 100 |      GetFC : Elab FC
 101 |      -- Check a group of top level declarations
 102 |      Declare : List Decl -> Elab ()
 103 | 
 104 |      -- Read the contents of a file, if it is present
 105 |      ReadFile : LookupDir -> (path : String) -> Elab $ Maybe String
 106 |      -- Writes to a file, replacing existing contents, if were present
 107 |      WriteFile : LookupDir -> (path : String) -> (contents : String) -> Elab ()
 108 |      -- Returns the specified type of dir related to the current idris project
 109 |      IdrisDir : LookupDir -> Elab String
 110 | 
 111 | export
 112 | Functor Elab where
 113 |   map = Map
 114 | 
 115 | export
 116 | Applicative Elab where
 117 |   pure = Pure
 118 |   (<*>) = Ap
 119 | 
 120 | export
 121 | Alternative Elab where
 122 |   empty = Fail EmptyFC ""
 123 |   l <|> r = Try l r
 124 | 
 125 | export
 126 | Monad Elab where
 127 |   (>>=) = Bind
 128 | 
 129 | -----------------------------
 130 | --- Elaboration interface ---
 131 | -----------------------------
 132 | 
 133 | public export
 134 | interface Monad m => Elaboration m where
 135 | 
 136 |   ||| Report an error in elaboration at some location
 137 |   failAt : FC -> String -> m a
 138 | 
 139 |   ||| Report a warning in elaboration at some location
 140 |   warnAt : FC -> String -> m ()
 141 | 
 142 |   ||| Try the first elaborator. If it fails, reset the elaborator state and
 143 |   ||| run the second
 144 |   try : Elab a -> Elab a -> m a
 145 | 
 146 |   ||| Write a log message, if the log level is >= the given level
 147 |   logMsg : String -> Nat -> String -> m ()
 148 | 
 149 |   ||| Write a log message and a rendered term, if the log level is >= the given level
 150 |   logTerm : String -> Nat -> String -> TTImp -> m ()
 151 | 
 152 |   ||| Write a log message and a resugared & rendered term, if the log level is >= the given level
 153 |   logSugaredTerm : String -> Nat -> String -> TTImp -> m ()
 154 | 
 155 |   ||| Resugar given term to a pretty string
 156 |   resugarTerm : (maxLineWidth : Maybe Nat) -> TTImp -> m String
 157 | 
 158 |   ||| Check that some TTImp syntax has the expected type
 159 |   ||| Returns the type checked value
 160 |   check : TTImp -> m expected
 161 | 
 162 |   ||| Return TTImp syntax of a given value
 163 |   quote : (0 _ : val) -> m TTImp
 164 | 
 165 |   ||| Build a lambda expression
 166 |   lambda : (0 x : Type) ->
 167 |            {0 ty : x -> Type} ->
 168 |            ((val : x) -> Elab (ty val)) -> m ((val : x) -> (ty val))
 169 | 
 170 |   ||| Get the goal type of the current elaboration
 171 |   |||
 172 |   ||| `Nothing` means the script is run in the top-level `%runElab` clause.
 173 |   ||| If elaboration script is run in expression mode, this function will always return `Just`.
 174 |   ||| In the case of unknown result type in the expression mode, returned `TTImp` would be an `IHole`.
 175 |   goal : m (Maybe TTImp)
 176 | 
 177 |   ||| Get the names of the local variables in scope
 178 |   localVars : m (List Name)
 179 | 
 180 |   ||| Generate a new unique name
 181 |   genSym : String -> m Name
 182 | 
 183 |   ||| Given a name, return the name decorated with the current namespace
 184 |   inCurrentNS : Name -> m Name
 185 | 
 186 |   ||| Given a possibly ambiguous name, get all the matching names and their types
 187 |   getType : Name -> m (List (Name, TTImp))
 188 | 
 189 |   ||| Get the metadata associated with a name. Returns all matching names and their types
 190 |   getInfo : Name -> m (List (Name, NameInfo))
 191 | 
 192 |   ||| Get the visibility associated with a name. Returns all matching names and their visibilities
 193 |   getVis : Name -> m (List (Name, Visibility))
 194 | 
 195 |   ||| Get the type of a local variable
 196 |   getLocalType : Name -> m TTImp
 197 | 
 198 |   ||| Get the constructors of a fully qualified data type name
 199 |   getCons : Name -> m (List Name)
 200 | 
 201 |   ||| Get all the name of function definitions that a given definition refers to (transitively)
 202 |   getReferredFns : Name -> m (List Name)
 203 | 
 204 |   ||| Get the name of the current and outer functions, if we are in a function
 205 |   getCurrentFn : m (SnocList Name)
 206 | 
 207 |   ||| Get the source location of the macro call site.
 208 |   getFC : m FC
 209 | 
 210 |   ||| Make some top level declarations
 211 |   declare : List Decl -> m ()
 212 | 
 213 |   ||| Read the contents of a file, if it is present
 214 |   readFile : LookupDir -> (path : String) -> m $ Maybe String
 215 | 
 216 |   ||| Writes to a file, replacing existing contents, if were present
 217 |   writeFile : LookupDir -> (path : String) -> (contents : String) -> m ()
 218 | 
 219 |   ||| Returns the specified type of dir related to the current idris project
 220 |   idrisDir : LookupDir -> m String
 221 | 
 222 | export %inline
 223 | ||| Report an error in elaboration
 224 | fail : Elaboration m => String -> m a
 225 | fail = failAt EmptyFC
 226 | 
 227 | export %inline
 228 | ||| Report an error in elaboration
 229 | warn : Elaboration m => String -> m ()
 230 | warn = warnAt EmptyFC
 231 | 
 232 | ||| Log the current goal type, if the log level is >= the given level
 233 | export %inline
 234 | logGoal : Elaboration m => String -> Nat -> String -> m ()
 235 | logGoal str n msg = whenJust !goal $ logTerm str n msg
 236 | 
 237 | export
 238 | Elaboration Elab where
 239 |   failAt         = Fail
 240 |   warnAt         = Warn
 241 |   try            = Try
 242 |   logMsg         = LogMsg
 243 |   logTerm        = LogTerm
 244 |   logSugaredTerm = LogSugaredTerm
 245 |   resugarTerm    = ResugarTerm
 246 |   check          = Check
 247 |   quote          = Quote
 248 |   lambda         = Lambda
 249 |   goal           = Goal
 250 |   localVars      = LocalVars
 251 |   genSym         = GenSym
 252 |   inCurrentNS    = InCurrentNS
 253 |   getType        = GetType
 254 |   getInfo        = GetInfo
 255 |   getVis         = GetVis
 256 |   getLocalType   = GetLocalType
 257 |   getCons        = GetCons
 258 |   getReferredFns = GetReferredFns
 259 |   getCurrentFn   = GetCurrentFn
 260 |   getFC          = GetFC
 261 |   declare        = Declare
 262 |   readFile       = ReadFile
 263 |   writeFile      = WriteFile
 264 |   idrisDir       = IdrisDir
 265 | 
 266 | public export
 267 | Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
 268 |   failAt              = lift .: failAt
 269 |   warnAt              = lift .: warnAt
 270 |   try                 = lift .: try
 271 |   logMsg s            = lift .: logMsg s
 272 |   logTerm s n         = lift .: logTerm s n
 273 |   logSugaredTerm s n  = lift .: logSugaredTerm s n
 274 |   resugarTerm         = lift .: resugarTerm
 275 |   check               = lift . check
 276 |   quote v             = lift $ quote v
 277 |   lambda x            = lift . lambda x
 278 |   goal                = lift goal
 279 |   localVars           = lift localVars
 280 |   genSym              = lift . genSym
 281 |   inCurrentNS         = lift . inCurrentNS
 282 |   getType             = lift . getType
 283 |   getInfo             = lift . getInfo
 284 |   getVis              = lift . getVis
 285 |   getLocalType        = lift . getLocalType
 286 |   getCons             = lift . getCons
 287 |   getReferredFns      = lift . getReferredFns
 288 |   getCurrentFn        = lift getCurrentFn
 289 |   getFC               = lift getFC
 290 |   declare             = lift . declare
 291 |   readFile            = lift .: readFile
 292 |   writeFile d         = lift .: writeFile d
 293 |   idrisDir            = lift . idrisDir
 294 | 
 295 | ||| Catch failures and use the `Maybe` monad instead
 296 | export
 297 | catch : Elaboration m => Elab a -> m (Maybe a)
 298 | catch elab = try (Just <$> elab) (pure Nothing)
 299 | 
 300 | ||| Run proof search to attempt to find a value of the input type.
 301 | ||| Useful to check whether a give interface constraint is satisfied.
 302 | export
 303 | search : Elaboration m => (0 ty : Type) -> m (Maybe ty)
 304 | search ty = catch $ check {expected = ty} `(%search)
 305 |