Language.Reflection


   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 |      -- Check a group of top level declarations
 100 |      Declare : List Decl -> Elab ()
 101 | 
 102 |      -- Read the contents of a file, if it is present
 103 |      ReadFile : LookupDir -> (path : String) -> Elab $ Maybe String
 104 |      -- Writes to a file, replacing existing contents, if were present
 105 |      WriteFile : LookupDir -> (path : String) -> (contents : String) -> Elab ()
 106 |      -- Returns the specified type of dir related to the current idris project
 107 |      IdrisDir : LookupDir -> Elab String
 108 | 
 109 | export
 110 | Functor Elab where
 111 |   map = Map
 112 | 
 113 | export
 114 | Applicative Elab where
 115 |   pure = Pure
 116 |   (<*>) = Ap
 117 | 
 118 | export
 119 | Alternative Elab where
 120 |   empty = Fail EmptyFC ""
 121 |   l <|> r = Try l r
 122 | 
 123 | export
 124 | Monad Elab where
 125 |   (>>=) = Bind
 126 | 
 127 | -----------------------------
 128 | --- Elaboration interface ---
 129 | -----------------------------
 130 | 
 131 | public export
 132 | interface Monad m => Elaboration m where
 133 | 
 134 |   ||| Report an error in elaboration at some location
 135 |   failAt : FC -> String -> m a
 136 | 
 137 |   ||| Report a warning in elaboration at some location
 138 |   warnAt : FC -> String -> m ()
 139 | 
 140 |   ||| Try the first elaborator. If it fails, reset the elaborator state and
 141 |   ||| run the second
 142 |   try : Elab a -> Elab a -> m a
 143 | 
 144 |   ||| Write a log message, if the log level is >= the given level
 145 |   logMsg : String -> Nat -> String -> m ()
 146 | 
 147 |   ||| Write a log message and a rendered term, if the log level is >= the given level
 148 |   logTerm : String -> Nat -> String -> TTImp -> m ()
 149 | 
 150 |   ||| Write a log message and a resugared & rendered term, if the log level is >= the given level
 151 |   logSugaredTerm : String -> Nat -> String -> TTImp -> m ()
 152 | 
 153 |   ||| Resugar given term to a pretty string
 154 |   resugarTerm : (maxLineWidth : Maybe Nat) -> TTImp -> m String
 155 | 
 156 |   ||| Check that some TTImp syntax has the expected type
 157 |   ||| Returns the type checked value
 158 |   check : TTImp -> m expected
 159 | 
 160 |   ||| Return TTImp syntax of a given value
 161 |   quote : (0 _ : val) -> m TTImp
 162 | 
 163 |   ||| Build a lambda expression
 164 |   lambda : (0 x : Type) ->
 165 |            {0 ty : x -> Type} ->
 166 |            ((val : x) -> Elab (ty val)) -> m ((val : x) -> (ty val))
 167 | 
 168 |   ||| Get the goal type of the current elaboration
 169 |   |||
 170 |   ||| `Nothing` means the script is run in the top-level `%runElab` clause.
 171 |   ||| If elaboration script is run in expression mode, this function will always return `Just`.
 172 |   ||| In the case of unknown result type in the expression mode, returned `TTImp` would be an `IHole`.
 173 |   goal : m (Maybe TTImp)
 174 | 
 175 |   ||| Get the names of the local variables in scope
 176 |   localVars : m (List Name)
 177 | 
 178 |   ||| Generate a new unique name
 179 |   genSym : String -> m Name
 180 | 
 181 |   ||| Given a name, return the name decorated with the current namespace
 182 |   inCurrentNS : Name -> m Name
 183 | 
 184 |   ||| Given a possibly ambiguous name, get all the matching names and their types
 185 |   getType : Name -> m (List (Name, TTImp))
 186 | 
 187 |   ||| Get the metadata associated with a name. Returns all matching names and their types
 188 |   getInfo : Name -> m (List (Name, NameInfo))
 189 | 
 190 |   ||| Get the visibility associated with a name. Returns all matching names and their visibilities
 191 |   getVis : Name -> m (List (Name, Visibility))
 192 | 
 193 |   ||| Get the type of a local variable
 194 |   getLocalType : Name -> m TTImp
 195 | 
 196 |   ||| Get the constructors of a fully qualified data type name
 197 |   getCons : Name -> m (List Name)
 198 | 
 199 |   ||| Get all the name of function definitions that a given definition refers to (transitively)
 200 |   getReferredFns : Name -> m (List Name)
 201 | 
 202 |   ||| Get the name of the current and outer functions, if we are in a function
 203 |   getCurrentFn : m (SnocList Name)
 204 | 
 205 |   ||| Make some top level declarations
 206 |   declare : List Decl -> m ()
 207 | 
 208 |   ||| Read the contents of a file, if it is present
 209 |   readFile : LookupDir -> (path : String) -> m $ Maybe String
 210 | 
 211 |   ||| Writes to a file, replacing existing contents, if were present
 212 |   writeFile : LookupDir -> (path : String) -> (contents : String) -> m ()
 213 | 
 214 |   ||| Returns the specified type of dir related to the current idris project
 215 |   idrisDir : LookupDir -> m String
 216 | 
 217 | export %inline
 218 | ||| Report an error in elaboration
 219 | fail : Elaboration m => String -> m a
 220 | fail = failAt EmptyFC
 221 | 
 222 | export %inline
 223 | ||| Report an error in elaboration
 224 | warn : Elaboration m => String -> m ()
 225 | warn = warnAt EmptyFC
 226 | 
 227 | ||| Log the current goal type, if the log level is >= the given level
 228 | export %inline
 229 | logGoal : Elaboration m => String -> Nat -> String -> m ()
 230 | logGoal str n msg = whenJust !goal $ logTerm str n msg
 231 | 
 232 | export
 233 | Elaboration Elab where
 234 |   failAt         = Fail
 235 |   warnAt         = Warn
 236 |   try            = Try
 237 |   logMsg         = LogMsg
 238 |   logTerm        = LogTerm
 239 |   logSugaredTerm = LogSugaredTerm
 240 |   resugarTerm    = ResugarTerm
 241 |   check          = Check
 242 |   quote          = Quote
 243 |   lambda         = Lambda
 244 |   goal           = Goal
 245 |   localVars      = LocalVars
 246 |   genSym         = GenSym
 247 |   inCurrentNS    = InCurrentNS
 248 |   getType        = GetType
 249 |   getInfo        = GetInfo
 250 |   getVis         = GetVis
 251 |   getLocalType   = GetLocalType
 252 |   getCons        = GetCons
 253 |   getReferredFns = GetReferredFns
 254 |   getCurrentFn   = GetCurrentFn
 255 |   declare        = Declare
 256 |   readFile       = ReadFile
 257 |   writeFile      = WriteFile
 258 |   idrisDir       = IdrisDir
 259 | 
 260 | public export
 261 | Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
 262 |   failAt              = lift .: failAt
 263 |   warnAt              = lift .: warnAt
 264 |   try                 = lift .: try
 265 |   logMsg s            = lift .: logMsg s
 266 |   logTerm s n         = lift .: logTerm s n
 267 |   logSugaredTerm s n  = lift .: logSugaredTerm s n
 268 |   resugarTerm         = lift .: resugarTerm
 269 |   check               = lift . check
 270 |   quote v             = lift $ quote v
 271 |   lambda x            = lift . lambda x
 272 |   goal                = lift goal
 273 |   localVars           = lift localVars
 274 |   genSym              = lift . genSym
 275 |   inCurrentNS         = lift . inCurrentNS
 276 |   getType             = lift . getType
 277 |   getInfo             = lift . getInfo
 278 |   getVis              = lift . getVis
 279 |   getLocalType        = lift . getLocalType
 280 |   getCons             = lift . getCons
 281 |   getReferredFns      = lift . getReferredFns
 282 |   getCurrentFn        = lift getCurrentFn
 283 |   declare             = lift . declare
 284 |   readFile            = lift .: readFile
 285 |   writeFile d         = lift .: writeFile d
 286 |   idrisDir            = lift . idrisDir
 287 | 
 288 | ||| Catch failures and use the `Maybe` monad instead
 289 | export
 290 | catch : Elaboration m => Elab a -> m (Maybe a)
 291 | catch elab = try (Just <$> elab) (pure Nothing)
 292 | 
 293 | ||| Run proof search to attempt to find a value of the input type.
 294 | ||| Useful to check whether a give interface constraint is satisfied.
 295 | export
 296 | search : Elaboration m => (0 ty : Type) -> m (Maybe ty)
 297 | search ty = catch $ check {expected = ty} `(%search)
 298 |