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 | 
  67 |      |||  given a type constructor, get positions of parameters in type, and the pairs of data constructors that can have the same type.
  68 |      GetDecEqConPairs : a -> Elab (List Nat, List (String, String))
  69 | 
  70 |      ||| Quote a concrete expression back to a TTImp
  71 |      Quote : (0 _ : val) -> Elab TTImp
  72 | 
  73 |      ||| Elaborate under a lambda
  74 |      Lambda : (0 x : Type) ->
  75 |               {0 ty : x -> Type} ->
  76 |               ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val))
  77 | 
  78 |      ||| Get the current goal type, if known
  79 |      ||| (it might need to be inferred from the solution)
  80 |      Goal : Elab (Maybe TTImp)
  81 |      ||| Get the names of local variables in scope
  82 |      LocalVars : Elab (List Name)
  83 |      ||| Generate a new unique name, based on the given string
  84 |      GenSym : String -> Elab Name
  85 |      ||| Put a name in the current namespace
  86 |      InCurrentNS : Name -> Elab Name
  87 |      ||| Get the types of every name which matches.
  88 |      ||| There may be ambiguities - returns a list of fully explicit names
  89 |      ||| and their types. If there's no results, the name is undefined.
  90 |      GetType : Name -> Elab (List (Name, TTImp))
  91 |      ||| Get the metadata associated with a name
  92 |      GetInfo : Name -> Elab (List (Name, NameInfo))
  93 |      ||| Get the visibility associated with a name
  94 |      GetVis : Name -> Elab (List (Name, Visibility))
  95 |      ||| Get the type of a local variable
  96 |      GetLocalType : Name -> Elab TTImp
  97 |      ||| Get the constructors of a data type. The name must be fully resolved.
  98 |      GetCons : Name -> Elab (List Name)
  99 |      ||| Get all function definition names referred in a definition. The name must be fully resolved.
 100 |      GetReferredFns : Name -> Elab (List Name)
 101 |      ||| Get the name of the current and outer functions, if it is applicable
 102 |      GetCurrentFn : Elab (SnocList Name)
 103 |      ||| Get the source location of the macro call site
 104 |      GetFC : Elab FC
 105 |      ||| Check a group of top level declarations
 106 |      Declare : List Decl -> Elab ()
 107 |      ||| Read the contents of a file, if it is present
 108 |      ReadFile : LookupDir -> (path : String) -> Elab $ Maybe String
 109 |      ||| Writes to a file, replacing existing contents, if were present
 110 |      WriteFile : LookupDir -> (path : String) -> (contents : String) -> Elab ()
 111 |      ||| Returns the specified type of dir related to the current idris project
 112 |      IdrisDir : LookupDir -> Elab String
 113 | 
 114 | export
 115 | Functor Elab where
 116 |   map = Map
 117 | 
 118 | export
 119 | Applicative Elab where
 120 |   pure = Pure
 121 |   (<*>) = Ap
 122 | 
 123 | export
 124 | Alternative Elab where
 125 |   empty = Fail EmptyFC ""
 126 |   l <|> r = Try l r
 127 | 
 128 | export
 129 | Monad Elab where
 130 |   (>>=) = Bind
 131 | 
 132 | -----------------------------
 133 | --- Elaboration interface ---
 134 | -----------------------------
 135 | 
 136 | public export
 137 | interface Monad m => Elaboration m where
 138 | 
 139 |   ||| Report an error in elaboration at some location
 140 |   failAt : FC -> String -> m a
 141 | 
 142 |   ||| Report a warning in elaboration at some location
 143 |   warnAt : FC -> String -> m ()
 144 | 
 145 |   ||| Try the first elaborator. If it fails, reset the elaborator state and
 146 |   ||| run the second
 147 |   try : Elab a -> Elab a -> m a
 148 | 
 149 |   ||| Write a log message, if the log level is >= the given level
 150 |   logMsg : String -> Nat -> String -> m ()
 151 | 
 152 |   ||| Write a log message and a rendered term, if the log level is >= the given level
 153 |   logTerm : String -> Nat -> String -> TTImp -> m ()
 154 | 
 155 |   ||| Write a log message and a resugared & rendered term, if the log level is >= the given level
 156 |   logSugaredTerm : String -> Nat -> String -> TTImp -> m ()
 157 | 
 158 |   ||| Resugar given term to a pretty string
 159 |   resugarTerm : (maxLineWidth : Maybe Nat) -> TTImp -> m String
 160 | 
 161 |   ||| Check that some TTImp syntax has the expected type
 162 |   ||| Returns the type checked value
 163 |   check : TTImp -> m expected
 164 | 
 165 |   ||| For a given type constructor, return param positions and pairs of data constructors that could have the same type
 166 |   ||| Returns a List of nats for parameter positions, and List of pairs of constructor names as strings
 167 |   ||| Util for automated derivation of decidable equality
 168 |   getDecEqConPairs : a -> m (List Nat, List (String, String))
 169 |   ||| Return TTImp syntax of a given value
 170 |   quote : (0 _ : val) -> m TTImp
 171 | 
 172 |   ||| Build a lambda expression
 173 |   lambda : (0 x : Type) ->
 174 |            {0 ty : x -> Type} ->
 175 |            ((val : x) -> Elab (ty val)) -> m ((val : x) -> (ty val))
 176 | 
 177 |   ||| Get the goal type of the current elaboration
 178 |   |||
 179 |   ||| `Nothing` means the script is run in the top-level `%runElab` clause.
 180 |   ||| If elaboration script is run in expression mode, this function will always return `Just`.
 181 |   ||| In the case of unknown result type in the expression mode, returned `TTImp` would be an `IHole`.
 182 |   goal : m (Maybe TTImp)
 183 | 
 184 |   ||| Get the names of the local variables in scope
 185 |   localVars : m (List Name)
 186 | 
 187 |   ||| Generate a new unique name
 188 |   genSym : String -> m Name
 189 | 
 190 |   ||| Given a name, return the name decorated with the current namespace
 191 |   inCurrentNS : Name -> m Name
 192 | 
 193 |   ||| Given a possibly ambiguous name, get all the matching names and their types
 194 |   getType : Name -> m (List (Name, TTImp))
 195 | 
 196 |   ||| Get the metadata associated with a name. Returns all matching names and their types
 197 |   getInfo : Name -> m (List (Name, NameInfo))
 198 | 
 199 |   ||| Get the visibility associated with a name. Returns all matching names and their visibilities
 200 |   getVis : Name -> m (List (Name, Visibility))
 201 | 
 202 |   ||| Get the type of a local variable
 203 |   getLocalType : Name -> m TTImp
 204 | 
 205 |   ||| Get the constructors of a fully qualified data type name
 206 |   getCons : Name -> m (List Name)
 207 | 
 208 |   ||| Get all the name of function definitions that a given definition refers to (transitively)
 209 |   getReferredFns : Name -> m (List Name)
 210 | 
 211 |   ||| Get the name of the current and outer functions, if we are in a function
 212 |   getCurrentFn : m (SnocList Name)
 213 | 
 214 |   ||| Get the source location of the macro call site.
 215 |   getFC : m FC
 216 | 
 217 |   ||| Make some top level declarations
 218 |   declare : List Decl -> m ()
 219 | 
 220 |   ||| Read the contents of a file, if it is present
 221 |   readFile : LookupDir -> (path : String) -> m $ Maybe String
 222 | 
 223 |   ||| Writes to a file, replacing existing contents, if were present
 224 |   writeFile : LookupDir -> (path : String) -> (contents : String) -> m ()
 225 | 
 226 |   ||| Returns the specified type of dir related to the current idris project
 227 |   idrisDir : LookupDir -> m String
 228 | 
 229 | export %inline
 230 | ||| Report an error in elaboration
 231 | fail : Elaboration m => String -> m a
 232 | fail = failAt EmptyFC
 233 | 
 234 | export %inline
 235 | ||| Report an error in elaboration
 236 | warn : Elaboration m => String -> m ()
 237 | warn = warnAt EmptyFC
 238 | 
 239 | ||| Log the current goal type, if the log level is >= the given level
 240 | export %inline
 241 | logGoal : Elaboration m => String -> Nat -> String -> m ()
 242 | logGoal str n msg = whenJust !goal $ logTerm str n msg
 243 | 
 244 | export
 245 | Elaboration Elab where
 246 |   failAt           = Fail
 247 |   warnAt           = Warn
 248 |   try              = Try
 249 |   logMsg           = LogMsg
 250 |   logTerm          = LogTerm
 251 |   logSugaredTerm   = LogSugaredTerm
 252 |   resugarTerm      = ResugarTerm
 253 |   check            = Check
 254 |   getDecEqConPairs = GetDecEqConPairs
 255 |   quote            = Quote
 256 |   lambda           = Lambda
 257 |   goal             = Goal
 258 |   localVars        = LocalVars
 259 |   genSym           = GenSym
 260 |   inCurrentNS      = InCurrentNS
 261 |   getType          = GetType
 262 |   getInfo          = GetInfo
 263 |   getVis           = GetVis
 264 |   getLocalType     = GetLocalType
 265 |   getCons          = GetCons
 266 |   getReferredFns   = GetReferredFns
 267 |   getCurrentFn     = GetCurrentFn
 268 |   getFC            = GetFC
 269 |   declare          = Declare
 270 |   readFile         = ReadFile
 271 |   writeFile        = WriteFile
 272 |   idrisDir         = IdrisDir
 273 | 
 274 | public export
 275 | Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
 276 |   failAt              = lift .: failAt
 277 |   warnAt              = lift .: warnAt
 278 |   try                 = lift .: try
 279 |   logMsg s            = lift .: logMsg s
 280 |   logTerm s n         = lift .: logTerm s n
 281 |   logSugaredTerm s n  = lift .: logSugaredTerm s n
 282 |   resugarTerm         = lift .: resugarTerm
 283 |   check               = lift . check
 284 |   getDecEqConPairs    = lift . getDecEqConPairs
 285 |   quote v             = lift $ quote v
 286 |   lambda x            = lift . lambda x
 287 |   goal                = lift goal
 288 |   localVars           = lift localVars
 289 |   genSym              = lift . genSym
 290 |   inCurrentNS         = lift . inCurrentNS
 291 |   getType             = lift . getType
 292 |   getInfo             = lift . getInfo
 293 |   getVis              = lift . getVis
 294 |   getLocalType        = lift . getLocalType
 295 |   getCons             = lift . getCons
 296 |   getReferredFns      = lift . getReferredFns
 297 |   getCurrentFn        = lift getCurrentFn
 298 |   getFC               = lift getFC
 299 |   declare             = lift . declare
 300 |   readFile            = lift .: readFile
 301 |   writeFile d         = lift .: writeFile d
 302 |   idrisDir            = lift . idrisDir
 303 | 
 304 | ||| Catch failures and use the `Maybe` monad instead
 305 | export
 306 | catch : Elaboration m => Elab a -> m (Maybe a)
 307 | catch elab = try (Just <$> elab) (pure Nothing)
 308 | 
 309 | ||| Run proof search to attempt to find a value of the input type.
 310 | ||| Useful to check whether a give interface constraint is satisfied.
 311 | export
 312 | search : Elaboration m => (0 ty : Type) -> m (Maybe ty)
 313 | search ty = catch $ check {expected = ty} `(%search)
 314 | 
 315 | export
 316 | isPublic : Elaboration m => Name -> m Bool
 317 | isPublic n = pure $ case !(getVis n) of
 318 |   [(_, Public)] => True
 319 |   _ => False
 320 |