
   0 | module Core.Reflect
   1 | 
   2 | import Data.List1
   3 | 
   4 | import Core.Context
   5 | import Core.Env
   6 | import Core.Normalise
   7 | import Core.Value
   8 | 
   9 | import Libraries.Data.WithDefault
  10 | 
  11 | %default covering
  12 | 
  13 | 
  14 | public export
  15 | interface Reify a where
  16 |   reify : {auto c : Ref Ctxt Defs} ->
  17 |           {vars : _} ->
  18 |           Defs -> NF vars -> Core a
  19 | 
  20 | public export
  21 | interface Reflect a where
  22 |   reflect : {vars : _} ->
  23 |             FC -> Defs -> (onLHS : Bool) ->
  24 |             Env Term vars -> a -> Core (Term vars)
  25 | 
  26 | export
  27 | getCon : {vars : _} ->
  28 |          FC -> Defs -> Name -> Core (Term vars)
  29 | getCon fc defs n
  30 |     = case !(lookupDefExact n (gamma defs)) of
  31 |            Just (DCon t a _) => resolved (gamma defs) (Ref fc (DataCon t a) n)
  32 |            Just (TCon a _ _ _ _ _ _) => resolved (gamma defs) (Ref fc (TyCon a) n)
  33 |            Just _ => resolved (gamma defs) (Ref fc Func n)
  34 |            _ => throw (UndefinedName fc n)
  35 | 
  36 | export
  37 | appCon : {vars : _} ->
  38 |          FC -> Defs -> Name -> List (Term vars) -> Core (Term vars)
  39 | appCon fc defs n args
  40 |     = do fn <- getCon fc defs n
  41 |          resolved (gamma defs) (apply fc fn args)
  42 | 
  43 | export
  44 | preludetypes : String -> Name
  45 | preludetypes n = NS typesNS (UN $ Basic n)
  46 | 
  47 | export
  48 | basics : String -> Name
  49 | basics n = NS basicsNS (UN $ Basic n)
  50 | 
  51 | export
  52 | builtin : String -> Name
  53 | builtin n = NS builtinNS (UN $ Basic n)
  54 | 
  55 | export
  56 | primio : String -> Name
  57 | primio n = NS primIONS (UN $ Basic n)
  58 | 
  59 | export
  60 | reflection : String -> Name
  61 | reflection n = NS reflectionNS (UN $ Basic n)
  62 | 
  63 | export
  64 | reflectiontt : String -> Name
  65 | reflectiontt n = NS reflectionTTNS (UN $ Basic n)
  66 | 
  67 | export
  68 | reflectionttimp : String -> Name
  69 | reflectionttimp n = NS reflectionTTImpNS (UN $ Basic n)
  70 | 
  71 | export
  72 | cantReify : Ref Ctxt Defs => {vars : _} -> NF vars -> String -> Core a
  73 | cantReify val ty = do
  74 |   logNF "reflection.reify" 10 "Can't reify as \{ty}" (mkEnv emptyFC vars) val
  75 |   throw (GenericMsg (getLoc val) ("Can't reify as " ++ ty))
  76 | 
  77 | export
  78 | cantReflect : FC -> String -> Core a
  79 | cantReflect fc ty
  80 |     = throw (GenericMsg fc ("Can't reflect as " ++ ty))
  81 | 
  82 | export
  83 | Reify () where
  84 |   reify defs _ = pure ()
  85 | 
  86 | export
  87 | Reflect () where
  88 |   reflect fc defs lhs env _ = getCon fc defs (builtin "MkUnit")
  89 | 
  90 | export
  91 | Reify String where
  92 |   reify defs (NPrimVal _ (Str str)) = pure str
  93 |   reify defs val = cantReify val "String"
  94 | 
  95 | export
  96 | Reflect String where
  97 |   reflect fc defs lhs env x = pure (PrimVal fc (Str x))
  98 | 
  99 | export
 100 | Reify Int where
 101 |   reify defs (NPrimVal _ (I v)) = pure v
 102 |   reify defs val = cantReify val "Int"
 103 | 
 104 | export
 105 | Reflect Int where
 106 |   reflect fc defs lhs env x = pure (PrimVal fc (I x))
 107 | 
 108 | export
 109 | Reify Int8 where
 110 |   reify defs (NPrimVal _ (I8 v)) = pure v
 111 |   reify defs val = cantReify val "Int8"
 112 | 
 113 | export
 114 | Reflect Int8 where
 115 |   reflect fc defs lhs env x = pure (PrimVal fc (I8 x))
 116 | 
 117 | export
 118 | Reify Int16 where
 119 |   reify defs (NPrimVal _ (I16 v)) = pure v
 120 |   reify defs val = cantReify val "Int16"
 121 | 
 122 | export
 123 | Reflect Int16 where
 124 |   reflect fc defs lhs env x = pure (PrimVal fc (I16 x))
 125 | 
 126 | export
 127 | Reify Int32 where
 128 |   reify defs (NPrimVal _ (I32 v)) = pure v
 129 |   reify defs val = cantReify val "Int32"
 130 | 
 131 | export
 132 | Reflect Int32 where
 133 |   reflect fc defs lhs env x = pure (PrimVal fc (I32 x))
 134 | 
 135 | export
 136 | Reify Int64 where
 137 |   reify defs (NPrimVal _ (I64 v)) = pure v
 138 |   reify defs val = cantReify val "Int64"
 139 | 
 140 | export
 141 | Reflect Int64 where
 142 |   reflect fc defs lhs env x = pure (PrimVal fc (I64 x))
 143 | 
 144 | export
 145 | Reify Bits8 where
 146 |   reify defs (NPrimVal _ (B8 v)) = pure v
 147 |   reify defs val = cantReify val "Bits8"
 148 | 
 149 | export
 150 | Reflect Bits8 where
 151 |   reflect fc defs lhs env x = pure (PrimVal fc (B8 x))
 152 | 
 153 | export
 154 | Reify Bits16 where
 155 |   reify defs (NPrimVal _ (B16 v)) = pure v
 156 |   reify defs val = cantReify val "Bits16"
 157 | 
 158 | export
 159 | Reflect Bits16 where
 160 |   reflect fc defs lhs env x = pure (PrimVal fc (B16 x))
 161 | 
 162 | export
 163 | Reify Bits32 where
 164 |   reify defs (NPrimVal _ (B32 v)) = pure v
 165 |   reify defs val = cantReify val "Bits32"
 166 | 
 167 | export
 168 | Reflect Bits32 where
 169 |   reflect fc defs lhs env x = pure (PrimVal fc (B32 x))
 170 | 
 171 | export
 172 | Reify Bits64 where
 173 |   reify defs (NPrimVal _ (B64 v)) = pure v
 174 |   reify defs val = cantReify val "Bits64"
 175 | 
 176 | export
 177 | Reflect Bits64 where
 178 |   reflect fc defs lhs env x = pure (PrimVal fc (B64 x))
 179 | 
 180 | export
 181 | Reify Integer where
 182 |   reify defs (NPrimVal _ (BI v)) = pure v
 183 |   reify defs val = cantReify val "Integer"
 184 | 
 185 | export
 186 | Reflect Integer where
 187 |   reflect fc defs lhs env x = pure (PrimVal fc (BI x))
 188 | 
 189 | export
 190 | Reify Char where
 191 |   reify defs (NPrimVal _ (Ch v)) = pure v
 192 |   reify defs val = cantReify val "Char"
 193 | 
 194 | export
 195 | Reflect Char where
 196 |   reflect fc defs lhs env x = pure (PrimVal fc (Ch x))
 197 | 
 198 | export
 199 | Reify Double where
 200 |   reify defs (NPrimVal _ (Db v)) = pure v
 201 |   reify defs val = cantReify val "Double"
 202 | 
 203 | export
 204 | Reflect Double where
 205 |   reflect fc defs lhs env x = pure (PrimVal fc (Db x))
 206 | 
 207 | export
 208 | Reify Bool where
 209 |   reify defs val@(NDCon _ n _ _ _)
 210 |       = case dropAllNS !(full (gamma defs) n) of
 211 |             UN (Basic "True") => pure True
 212 |             UN (Basic "False") => pure False
 213 |             _ => cantReify val "Bool"
 214 |   reify defs val = cantReify val "Bool"
 215 | 
 216 | export
 217 | Reflect Bool where
 218 |   reflect fc defs lhs env True = getCon fc defs (basics "True")
 219 |   reflect fc defs lhs env False = getCon fc defs (basics "False")
 220 | 
 221 | export
 222 | Reify Nat where
 223 |   reify defs val@(NDCon _ n _ _ args)
 224 |       = case (dropAllNS !(full (gamma defs) n), args) of
 225 |              (UN (Basic "Z"), _) => pure Z
 226 |              (UN (Basic "S"), [(_, k)])
 227 |                  => do k' <- reify defs !(evalClosure defs k)
 228 |                        pure (S k')
 229 |              _ => cantReify val "Nat"
 230 |   reify defs val = cantReify val "Nat"
 231 | 
 232 | export
 233 | Reflect Nat where
 234 |   reflect fc defs lhs env Z = getCon fc defs (preludetypes "Z")
 235 |   reflect fc defs lhs env (S k)
 236 |       = do k' <- reflect fc defs lhs env k
 237 |            appCon fc defs (preludetypes "S") [k']
 238 | 
 239 | export
 240 | Reify a => Reify (List a) where
 241 |   reify defs val@(NDCon _ n _ _ args)
 242 |       = case (dropAllNS !(full (gamma defs) n), args) of
 243 |              (UN (Basic "Nil"), _) => pure []
 244 |              (UN (Basic "::"), [_, (_, x), (_, xs)])
 245 |                   => do x' <- reify defs !(evalClosure defs x)
 246 |                         xs' <- reify defs !(evalClosure defs xs)
 247 |                         pure (x' :: xs')
 248 |              _ => cantReify val "List"
 249 |   reify defs val = cantReify val "List"
 250 | 
 251 | export
 252 | Reflect a => Reflect (List a) where
 253 |   reflect fc defs lhs env [] = appCon fc defs (basics "Nil") [Erased fc Placeholder]
 254 |   reflect fc defs lhs env (x :: xs)
 255 |       = do x' <- reflect fc defs lhs env x
 256 |            xs' <- reflect fc defs lhs env xs
 257 |            appCon fc defs (basics "::") [Erased fc Placeholder, x', xs']
 258 | 
 259 | export
 260 | Reify a => Reify (List1 a) where
 261 |   reify defs val@(NDCon _ n _ _ [_, (_, x), (_, xs)])
 262 |       = case dropAllNS !(full (gamma defs) n) of
 263 |              UN (Basic ":::")
 264 |                   => do x' <- reify defs !(evalClosure defs x)
 265 |                         xs' <- reify defs !(evalClosure defs xs)
 266 |                         pure (x' ::: xs')
 267 |              _ => cantReify val "List1"
 268 |   reify defs val = cantReify val "List1"
 269 | 
 270 | export
 271 | Reflect a => Reflect (List1 a) where
 272 |   reflect fc defs lhs env xxs
 273 |       = do x' <- reflect fc defs lhs env (head xxs)
 274 |            xs' <- reflect fc defs lhs env (tail xxs)
 275 |            appCon fc defs (NS (mkNamespace "Data.List1")
 276 |                   (UN $ Basic ":::")) [Erased fc Placeholder, x', xs']
 277 | 
 278 | export
 279 | Reify a => Reify (SnocList a) where
 280 |   reify defs val@(NDCon _ n _ _ args)
 281 |       = case (dropAllNS !(full (gamma defs) n), args) of
 282 |              (UN (Basic "Lin"), _) => pure [<]
 283 |              (UN (Basic ":<"), [_, (_, sx), (_, x)])
 284 |                   => do sx' <- reify defs !(evalClosure defs sx)
 285 |                         x' <- reify defs !(evalClosure defs x)
 286 |                         pure (sx' :< x')
 287 |              _ => cantReify val "SnocList"
 288 |   reify defs val = cantReify val "SnocList"
 289 | 
 290 | export
 291 | Reflect a => Reflect (SnocList a) where
 292 |   reflect fc defs lhs env [<] = appCon fc defs (basics "Lin") [Erased fc Placeholder]
 293 |   reflect fc defs lhs env (sx :< x)
 294 |       = do sx' <- reflect fc defs lhs env sx
 295 |            x' <- reflect fc defs lhs env x
 296 |            appCon fc defs (basics ":<") [Erased fc Placeholder, sx', x']
 297 | 
 298 | export
 299 | Reify a => Reify (Maybe a) where
 300 |   reify defs val@(NDCon _ n _ _ args)
 301 |       = case (dropAllNS !(full (gamma defs) n), args) of
 302 |              (UN (Basic "Nothing"), _) => pure Nothing
 303 |              (UN (Basic "Just"), [_, (_, x)])
 304 |                   => do x' <- reify defs !(evalClosure defs x)
 305 |                         pure (Just x')
 306 |              _ => cantReify val "Maybe"
 307 |   reify defs val = cantReify val "Maybe"
 308 | 
 309 | export
 310 | Reflect a => Reflect (Maybe a) where
 311 |   reflect fc defs lhs env Nothing = appCon fc defs (preludetypes "Nothing") [Erased fc Placeholder]
 312 |   reflect fc defs lhs env (Just x)
 313 |       = do x' <- reflect fc defs lhs env x
 314 |            appCon fc defs (preludetypes "Just") [Erased fc Placeholder, x']
 315 | 
 316 | 
 317 | export
 318 | Reify a => Reify (WithDefault a def) where
 319 |   reify defs val@(NDCon _ n _ _ args)
 320 |       = case (dropAllNS !(full (gamma defs) n), args) of
 321 |              (UN (Basic "DefaultedValue"), _) => pure defaulted
 322 |              (UN (Basic "SpecifiedValue"), [_, _, (_, x)])
 323 |                   => do x' <- reify defs !(evalClosure defs x)
 324 |                         pure (specified x')
 325 |              _ => cantReify val "WithDefault"
 326 |   reify defs val = cantReify val "WithDefault"
 327 | 
 328 | export
 329 | Reflect a => Reflect (WithDefault a def) where
 330 |   reflect fc defs lhs env def
 331 |     = onWithDefault
 332 |         (appCon fc defs (reflectionttimp "DefaultedValue") [Erased fc Placeholder, Erased fc Placeholder])
 333 |         (\x => do x' <- reflect fc defs lhs env x
 334 |                   appCon fc defs (reflectionttimp "SpecifiedValue") [Erased fc Placeholder, Erased fc Placeholder, x'])
 335 |         def
 336 | 
 337 | export
 338 | (Reify a, Reify b) => Reify (a, b) where
 339 |   reify defs val@(NDCon _ n _ _ [_, _, (_, x), (_, y)])
 340 |       = case dropAllNS !(full (gamma defs) n) of
 341 |              UN (Basic "MkPair")
 342 |                  => do x' <- reify defs !(evalClosure defs x)
 343 |                        y' <- reify defs !(evalClosure defs y)
 344 |                        pure (x', y')
 345 |              _ => cantReify val "Pair"
 346 |   reify defs val = cantReify val "Pair"
 347 | 
 348 | export
 349 | (Reflect a, Reflect b) => Reflect (a, b) where
 350 |   reflect fc defs lhs env (x, y)
 351 |       = do x' <- reflect fc defs lhs env x
 352 |            y' <- reflect fc defs lhs env y
 353 |            appCon fc defs (builtin "MkPair") [Erased fc Placeholder, Erased fc Placeholder, x', y']
 354 | 
 355 | export
 356 | Reify Namespace where
 357 |   reify defs val@(NDCon _ n _ _ [(_, ns)])
 358 |     = case dropAllNS !(full (gamma defs) n) of
 359 |         UN (Basic "MkNS")
 360 |           => do ns' <- reify defs !(evalClosure defs ns)
 361 |                 pure (unsafeFoldNamespace ns')
 362 |         _ => cantReify val "Namespace"
 363 |   reify defs val = cantReify val "Namespace"
 364 | 
 365 | export
 366 | Reflect Namespace where
 367 |   reflect fc defs lhs env ns
 368 |     = do ns' <- reflect fc defs lhs env (unsafeUnfoldNamespace ns)
 369 |          appCon fc defs (reflectiontt "MkNS") [ns']
 370 | 
 371 | export
 372 | Reify ModuleIdent where
 373 |   reify defs val@(NDCon _ n _ _ [(_, ns)])
 374 |     = case dropAllNS !(full (gamma defs) n) of
 375 |         UN (Basic "MkMI")
 376 |           => do ns' <- reify defs !(evalClosure defs ns)
 377 |                 pure (unsafeFoldModuleIdent ns')
 378 |         _ => cantReify val "ModuleIdent"
 379 |   reify defs val = cantReify val "ModuleIdent"
 380 | 
 381 | export
 382 | Reflect ModuleIdent where
 383 |   reflect fc defs lhs env ns
 384 |     = do ns' <- reflect fc defs lhs env (unsafeUnfoldModuleIdent ns)
 385 |          appCon fc defs (reflectiontt "MkMI") [ns']
 386 | 
 387 | export
 388 | Reify UserName where
 389 |   reify defs val@(NDCon _ n _ _ args)
 390 |       = case (dropAllNS !(full (gamma defs) n), args) of
 391 |              (UN (Basic "Basic"), [(_, str)])
 392 |                  => do str' <- reify defs !(evalClosure defs str)
 393 |                        pure (Basic str')
 394 |              (UN (Basic "Field"), [(_, str)])
 395 |                  => do str' <- reify defs !(evalClosure defs str)
 396 |                        pure (Field str')
 397 |              (UN (Basic "Underscore"), [])
 398 |                  => pure Underscore
 399 |              (NS _ (UN _), _)
 400 |                  => cantReify val "Name, reifying it is unimplemented or intentionally internal"
 401 |              _ => cantReify val "Name, the name was not found in context"
 402 |   reify defs val = cantReify val "Name, value is not an NDCon interally"
 403 | 
 404 | export
 405 | Reflect UserName where
 406 |   reflect fc defs lhs env (Basic x)
 407 |       = do x' <- reflect fc defs lhs env x
 408 |            appCon fc defs (reflectiontt "Basic") [x']
 409 |   reflect fc defs lhs env (Field x)
 410 |       = do x' <- reflect fc defs lhs env x
 411 |            appCon fc defs (reflectiontt "Field") [x']
 412 |   reflect fc defs lhs env Underscore
 413 |       = do appCon fc defs (reflectiontt "Underscore") []
 414 | 
 415 | export
 416 | Reify Name where
 417 |   reify defs val@(NDCon _ n _ _ args)
 418 |       = case (dropAllNS !(full (gamma defs) n), args) of
 419 |              (UN (Basic "UN"), [(_, str)])
 420 |                  => do str' <- reify defs !(evalClosure defs str)
 421 |                        pure (UN str')
 422 |              (UN (Basic "MN"), [(_, str), (_, i)])
 423 |                  => do str' <- reify defs !(evalClosure defs str)
 424 |                        i' <- reify defs !(evalClosure defs i)
 425 |                        pure (MN str' i')
 426 |              (UN (Basic "NS"), [(_, ns), (_, n)])
 427 |                  => do ns' <- reify defs !(evalClosure defs ns)
 428 |                        n' <- reify defs !(evalClosure defs n)
 429 |                        pure (NS ns' n')
 430 |              (UN (Basic "DN"), [(_, str), (_, n)])
 431 |                  => do str' <- reify defs !(evalClosure defs str)
 432 |                        n' <- reify defs !(evalClosure defs n)
 433 |                        pure (DN str' n')
 434 |              (UN (Basic "Nested"), [(_, ix), (_, n)])
 435 |                  => do ix' <- reify defs !(evalClosure defs ix)
 436 |                        n' <- reify defs !(evalClosure defs n)
 437 |                        pure (Nested ix' n')
 438 |              (UN (Basic "CaseBlock"), [(_, outer), (_, i)])
 439 |                  => do outer' <- reify defs !(evalClosure defs outer)
 440 |                        i' <- reify defs !(evalClosure defs i)
 441 |                        pure (CaseBlock outer' i')
 442 |              (UN (Basic "WithBlock"), [(_, outer), (_, i)])
 443 |                  => do outer' <- reify defs !(evalClosure defs outer)
 444 |                        i' <- reify defs !(evalClosure defs i)
 445 |                        pure (WithBlock outer' i')
 446 |              (NS _ (UN _), _)
 447 |                  => cantReify val "Name, reifying it is unimplemented or intentionally internal"
 448 |              _ => cantReify val "Name, the name was not found in context"
 449 |   reify defs val = cantReify val "Name, value is not an NDCon interally"
 450 | 
 451 | export
 452 | Reflect Name where
 453 |   reflect fc defs lhs env (UN x)
 454 |       = do x' <- reflect fc defs lhs env x
 455 |            appCon fc defs (reflectiontt "UN") [x']
 456 |   reflect fc defs lhs env (MN x i)
 457 |       = do x' <- reflect fc defs lhs env x
 458 |            i' <- reflect fc defs lhs env i
 459 |            appCon fc defs (reflectiontt "MN") [x', i']
 460 |   reflect fc defs lhs env (NS ns n)
 461 |       = do ns' <- reflect fc defs lhs env ns
 462 |            n' <- reflect fc defs lhs env n
 463 |            appCon fc defs (reflectiontt "NS") [ns', n']
 464 |   reflect fc defs lhs env (DN str n)
 465 |       = do str' <- reflect fc defs lhs env str
 466 |            n' <- reflect fc defs lhs env n
 467 |            appCon fc defs (reflectiontt "DN") [str', n']
 468 |   reflect fc defs lhs env (Nested ix n)
 469 |       = do ix' <- reflect fc defs lhs env ix
 470 |            n'  <- reflect fc defs lhs env n
 471 |            appCon fc defs (reflectiontt "Nested") [ix',n']
 472 |   reflect fc defs lhs env (CaseBlock outer i)
 473 |       = do outer' <- reflect fc defs lhs env outer
 474 |            i' <- reflect fc defs lhs env i
 475 |            appCon fc defs (reflectiontt "CaseBlock") [outer',i']
 476 |   reflect fc defs lhs env (WithBlock outer i)
 477 |       = do outer' <- reflect fc defs lhs env outer
 478 |            i' <- reflect fc defs lhs env i
 479 |            appCon fc defs (reflectiontt "WithBlock") [outer',i']
 480 |   reflect fc defs lhs env (Resolved i)
 481 |       = case !(full (gamma defs) (Resolved i)) of
 482 |              Resolved _ => cantReflect fc
 483 |                       "Name directly, Resolved is intentionally internal"
 484 |              n => reflect fc defs lhs env n
 485 |   reflect fc defs lhs env n = cantReflect fc
 486 |     "Name, reflecting it is unimplemented or intentionally internal"
 487 | 
 488 | export
 489 | Reify NameType where
 490 |   reify defs val@(NDCon _ n _ _ args)
 491 |       = case (dropAllNS !(full (gamma defs) n), args) of
 492 |              (UN (Basic "Bound"), _) => pure Bound
 493 |              (UN (Basic "Func"), _) => pure Func
 494 |              (UN (Basic "DataCon"), [(_, t), (_, i)])
 495 |                   => do t' <- reify defs !(evalClosure defs t)
 496 |                         i' <- reify defs !(evalClosure defs i)
 497 |                         pure (DataCon t' i')
 498 |              (UN (Basic "TyCon"), [(_, i)])
 499 |                   => do i' <- reify defs !(evalClosure defs i)
 500 |                         pure (TyCon i')
 501 |              _ => cantReify val "NameType"
 502 |   reify defs val = cantReify val "NameType"
 503 | 
 504 | export
 505 | Reflect NameType where
 506 |   reflect fc defs lhs env Bound = getCon fc defs (reflectiontt "Bound")
 507 |   reflect fc defs lhs env Func = getCon fc defs (reflectiontt "Func")
 508 |   reflect fc defs lhs env (DataCon t i)
 509 |       = do t' <- reflect fc defs lhs env t
 510 |            i' <- reflect fc defs lhs env i
 511 |            appCon fc defs (reflectiontt "DataCon") [t', i']
 512 |   reflect fc defs lhs env (TyCon i)
 513 |       = do i' <- reflect fc defs lhs env i
 514 |            appCon fc defs (reflectiontt "TyCon") [PrimVal fc (I 0), i']
 515 | 
 516 | export
 517 | Reify PrimType where
 518 |   reify defs val@(NDCon _ n _ _ args)
 519 |       = case (dropAllNS !(full (gamma defs) n), args) of
 520 |              (UN (Basic "IntType"), [])
 521 |                   => pure IntType
 522 |              (UN (Basic "Int8Type"), [])
 523 |                   => pure Int8Type
 524 |              (UN (Basic "Int16Type"), [])
 525 |                   => pure Int16Type
 526 |              (UN (Basic "Int32Type"), [])
 527 |                   => pure Int32Type
 528 |              (UN (Basic "Int64Type"), [])
 529 |                   => pure Int64Type
 530 |              (UN (Basic "IntegerType"), [])
 531 |                   => pure IntegerType
 532 |              (UN (Basic "Bits8Type"), [])
 533 |                   => pure Bits8Type
 534 |              (UN (Basic "Bits16Type"), [])
 535 |                   => pure Bits16Type
 536 |              (UN (Basic "Bits32Type"), [])
 537 |                   => pure Bits32Type
 538 |              (UN (Basic "Bits64Type"), [])
 539 |                   => pure Bits64Type
 540 |              (UN (Basic "StringType"), [])
 541 |                   => pure StringType
 542 |              (UN (Basic "CharType"), [])
 543 |                   => pure CharType
 544 |              (UN (Basic "DoubleType"), [])
 545 |                   => pure DoubleType
 546 |              (UN (Basic "WorldType"), [])
 547 |                   => pure WorldType
 548 |              _ => cantReify val "PrimType"
 549 |   reify defs val = cantReify val "PrimType"
 550 | 
 551 | export
 552 | Reify Constant where
 553 |   reify defs val@(NDCon _ n _ _ args)
 554 |       = case (dropAllNS !(full (gamma defs) n), args) of
 555 |              (UN (Basic "I"), [(_, x)])
 556 |                   => do x' <- reify defs !(evalClosure defs x)
 557 |                         pure (I x')
 558 |              (UN (Basic "I8"), [(_, x)])
 559 |                   => do x' <- reify defs !(evalClosure defs x)
 560 |                         pure (I8 x')
 561 |              (UN (Basic "I16"), [(_, x)])
 562 |                   => do x' <- reify defs !(evalClosure defs x)
 563 |                         pure (I16 x')
 564 |              (UN (Basic "I32"), [(_, x)])
 565 |                   => do x' <- reify defs !(evalClosure defs x)
 566 |                         pure (I32 x')
 567 |              (UN (Basic "I64"), [(_, x)])
 568 |                   => do x' <- reify defs !(evalClosure defs x)
 569 |                         pure (I64 x')
 570 |              (UN (Basic "BI"), [(_, x)])
 571 |                   => do x' <- reify defs !(evalClosure defs x)
 572 |                         pure (BI x')
 573 |              (UN (Basic "B8"), [(_, x)])
 574 |                   => do x' <- reify defs !(evalClosure defs x)
 575 |                         pure (B8 x')
 576 |              (UN (Basic "B16"), [(_, x)])
 577 |                   => do x' <- reify defs !(evalClosure defs x)
 578 |                         pure (B16 x')
 579 |              (UN (Basic "B32"), [(_, x)])
 580 |                   => do x' <- reify defs !(evalClosure defs x)
 581 |                         pure (B32 x')
 582 |              (UN (Basic "B64"), [(_, x)])
 583 |                   => do x' <- reify defs !(evalClosure defs x)
 584 |                         pure (B64 x')
 585 |              (UN (Basic "Str"), [(_, x)])
 586 |                   => do x' <- reify defs !(evalClosure defs x)
 587 |                         pure (Str x')
 588 |              (UN (Basic "Ch"), [(_, x)])
 589 |                   => do x' <- reify defs !(evalClosure defs x)
 590 |                         pure (Ch x')
 591 |              (UN (Basic "Db"), [(_, x)])
 592 |                   => do x' <- reify defs !(evalClosure defs x)
 593 |                         pure (Db x')
 594 |              (UN (Basic "PrT"), [(_, x)])
 595 |                   => do x' <- reify defs !(evalClosure defs x)
 596 |                         pure (PrT x')
 597 |              (UN (Basic "WorldVal"), [])
 598 |                   => pure WorldVal
 599 |              _ => cantReify val "Constant"
 600 |   reify defs val = cantReify val "Constant"
 601 | 
 602 | export
 603 | Reflect PrimType where
 604 |   reflect fc defs lhs env IntType
 605 |       = getCon fc defs (reflectiontt "IntType")
 606 |   reflect fc defs lhs env Int8Type
 607 |       = getCon fc defs (reflectiontt "Int8Type")
 608 |   reflect fc defs lhs env Int16Type
 609 |       = getCon fc defs (reflectiontt "Int16Type")
 610 |   reflect fc defs lhs env Int32Type
 611 |       = getCon fc defs (reflectiontt "Int32Type")
 612 |   reflect fc defs lhs env Int64Type
 613 |       = getCon fc defs (reflectiontt "Int64Type")
 614 |   reflect fc defs lhs env IntegerType
 615 |       = getCon fc defs (reflectiontt "IntegerType")
 616 |   reflect fc defs lhs env Bits8Type
 617 |       = getCon fc defs (reflectiontt "Bits8Type")
 618 |   reflect fc defs lhs env Bits16Type
 619 |       = getCon fc defs (reflectiontt "Bits16Type")
 620 |   reflect fc defs lhs env Bits32Type
 621 |       = getCon fc defs (reflectiontt "Bits32Type")
 622 |   reflect fc defs lhs env Bits64Type
 623 |       = getCon fc defs (reflectiontt "Bits64Type")
 624 |   reflect fc defs lhs env StringType
 625 |       = getCon fc defs (reflectiontt "StringType")
 626 |   reflect fc defs lhs env CharType
 627 |       = getCon fc defs (reflectiontt "CharType")
 628 |   reflect fc defs lhs env DoubleType
 629 |       = getCon fc defs (reflectiontt "DoubleType")
 630 |   reflect fc defs lhs env WorldType
 631 |       = getCon fc defs (reflectiontt "WorldType")
 632 | 
 633 | export
 634 | Reflect Constant where
 635 |   reflect fc defs lhs env (I x)
 636 |       = do x' <- reflect fc defs lhs env x
 637 |            appCon fc defs (reflectiontt "I") [x']
 638 |   reflect fc defs lhs env (I8 x)
 639 |       = do x' <- reflect fc defs lhs env x
 640 |            appCon fc defs (reflectiontt "I8") [x']
 641 |   reflect fc defs lhs env (I16 x)
 642 |       = do x' <- reflect fc defs lhs env x
 643 |            appCon fc defs (reflectiontt "I16") [x']
 644 |   reflect fc defs lhs env (I32 x)
 645 |       = do x' <- reflect fc defs lhs env x
 646 |            appCon fc defs (reflectiontt "I32") [x']
 647 |   reflect fc defs lhs env (I64 x)
 648 |       = do x' <- reflect fc defs lhs env x
 649 |            appCon fc defs (reflectiontt "I64") [x']
 650 |   reflect fc defs lhs env (BI x)
 651 |       = do x' <- reflect fc defs lhs env x
 652 |            appCon fc defs (reflectiontt "BI") [x']
 653 |   reflect fc defs lhs env (B8 x)
 654 |       = do x' <- reflect fc defs lhs env x
 655 |            appCon fc defs (reflectiontt "B8") [x']
 656 |   reflect fc defs lhs env (B16 x)
 657 |       = do x' <- reflect fc defs lhs env x
 658 |            appCon fc defs (reflectiontt "B16") [x']
 659 |   reflect fc defs lhs env (B32 x)
 660 |       = do x' <- reflect fc defs lhs env x
 661 |            appCon fc defs (reflectiontt "B32") [x']
 662 |   reflect fc defs lhs env (B64 x)
 663 |       = do x' <- reflect fc defs lhs env x
 664 |            appCon fc defs (reflectiontt "B64") [x']
 665 |   reflect fc defs lhs env (Str x)
 666 |       = do x' <- reflect fc defs lhs env x
 667 |            appCon fc defs (reflectiontt "Str") [x']
 668 |   reflect fc defs lhs env (Ch x)
 669 |       = do x' <- reflect fc defs lhs env x
 670 |            appCon fc defs (reflectiontt "Ch") [x']
 671 |   reflect fc defs lhs env (Db x)
 672 |       = do x' <- reflect fc defs lhs env x
 673 |            appCon fc defs (reflectiontt "Db") [x']
 674 |   reflect fc defs lhs env (PrT x)
 675 |       = do x' <- reflect fc defs lhs env x
 676 |            appCon fc defs (reflectiontt "PrT") [x']
 677 |   reflect fc defs lhs env WorldVal
 678 |       = getCon fc defs (reflectiontt "WorldVal")
 679 | 
 680 | export
 681 | Reify Visibility where
 682 |   reify defs val@(NDCon _ n _ _ _)
 683 |       = case dropAllNS !(full (gamma defs) n) of
 684 |              UN (Basic "Private") => pure Private
 685 |              UN (Basic "Export") => pure Export
 686 |              UN (Basic "Public") => pure Public
 687 |              _ => cantReify val "Visibility"
 688 |   reify defs val = cantReify val "Visibility"
 689 | 
 690 | export
 691 | Reflect Visibility where
 692 |   reflect fc defs lhs env Private = getCon fc defs (reflectiontt "Private")
 693 |   reflect fc defs lhs env Export = getCon fc defs (reflectiontt "Export")
 694 |   reflect fc defs lhs env Public = getCon fc defs (reflectiontt "Public")
 695 | 
 696 | export
 697 | Reify TotalReq where
 698 |   reify defs val@(NDCon _ n _ _ _)
 699 |       = case dropAllNS !(full (gamma defs) n) of
 700 |              UN (Basic "Total") => pure Total
 701 |              UN (Basic "CoveringOnly") => pure CoveringOnly
 702 |              UN (Basic "PartialOK") => pure PartialOK
 703 |              _ => cantReify val "TotalReq"
 704 |   reify defs val = cantReify val "TotalReq"
 705 | 
 706 | export
 707 | Reflect TotalReq where
 708 |   reflect fc defs lhs env Total = getCon fc defs (reflectiontt "Total")
 709 |   reflect fc defs lhs env CoveringOnly = getCon fc defs (reflectiontt "CoveringOnly")
 710 |   reflect fc defs lhs env PartialOK = getCon fc defs (reflectiontt "PartialOK")
 711 | 
 712 | export
 713 | Reify RigCount where
 714 |   reify defs val@(NDCon _ n _ _ _)
 715 |       = case dropAllNS !(full (gamma defs) n) of
 716 |              UN (Basic "M0") => pure erased
 717 |              UN (Basic "M1") => pure linear
 718 |              UN (Basic "MW") => pure top
 719 |              _ => cantReify val "Count"
 720 |   reify defs val = cantReify val "Count"
 721 | 
 722 | export
 723 | Reflect RigCount where
 724 |   reflect fc defs lhs env r
 725 |       = elimSemi (getCon fc defs (reflectiontt "M0"))
 726 |                  (getCon fc defs (reflectiontt "M1"))
 727 |                  (const (getCon fc defs (reflectiontt "MW")))
 728 |                  r
 729 | 
 730 | export
 731 | Reify t => Reify (PiInfo t) where
 732 |   reify defs val@(NDCon _ n _ _ args)
 733 |       = case (dropAllNS !(full (gamma defs) n), args) of
 734 |              (UN (Basic "ImplicitArg"), _) => pure Implicit
 735 |              (UN (Basic "ExplicitArg"), _) => pure Explicit
 736 |              (UN (Basic "AutoImplicit"), _) => pure AutoImplicit
 737 |              (UN (Basic "DefImplicit"), [_, (_, t)])
 738 |                  => do t' <- reify defs !(evalClosure defs t)
 739 |                        pure (DefImplicit t')
 740 |              _ => cantReify val "PiInfo"
 741 |   reify defs val = cantReify val "PiInfo"
 742 | 
 743 | export
 744 | Reflect t => Reflect (PiInfo t) where
 745 |   reflect fc defs lhs env Implicit
 746 |       = appCon fc defs (reflectiontt "ImplicitArg") [Erased fc Placeholder]
 747 |   reflect fc defs lhs env Explicit
 748 |       = appCon fc defs (reflectiontt "ExplicitArg") [Erased fc Placeholder]
 749 |   reflect fc defs lhs env AutoImplicit
 750 |       = appCon fc defs (reflectiontt "AutoImplicit") [Erased fc Placeholder]
 751 |   reflect fc defs lhs env (DefImplicit t)
 752 |       = do t' <- reflect fc defs lhs env t
 753 |            appCon fc defs (reflectiontt "DefImplicit") [Erased fc Placeholder, t']
 754 | 
 755 | export
 756 | Reify LazyReason where
 757 |   reify defs val@(NDCon _ n _ _ _)
 758 |       = case dropAllNS !(full (gamma defs) n) of
 759 |              UN (Basic "LInf") => pure LInf
 760 |              UN (Basic "LLazy") => pure LLazy
 761 |              UN (Basic "LUnknown") => pure LUnknown
 762 |              _ => cantReify val "LazyReason"
 763 |   reify defs val = cantReify val "LazyReason"
 764 | 
 765 | export
 766 | Reflect LazyReason where
 767 |   reflect fc defs lhs env LInf = getCon fc defs (reflectiontt "LInf")
 768 |   reflect fc defs lhs env LLazy = getCon fc defs (reflectiontt "LLazy")
 769 |   reflect fc defs lhs env LUnknown = getCon fc defs (reflectiontt "LUnknown")
 770 | 
 771 | export
 772 | Reify VirtualIdent where
 773 |   reify defs val@(NDCon _ n _ _ args)
 774 |       = case (dropAllNS !(full (gamma defs) n), args) of
 775 |              (UN (Basic "Interactive"), [])
 776 |                    => pure Interactive
 777 |              _ => cantReify val "VirtualIdent"
 778 |   reify defs val = cantReify val "VirtualIdent"
 779 | 
 780 | export
 781 | Reflect BuiltinType where
 782 |   reflect fc defs lhs env BuiltinNatural
 783 |       = getCon fc defs (reflectiontt "BuiltinNatural")
 784 |   reflect fc defs lhs env NaturalToInteger
 785 |       = getCon fc defs (reflectiontt "NaturalToInteger")
 786 |   reflect fc defs lhs env IntegerToNatural
 787 |       = getCon fc defs (reflectiontt "IntegerToNatural")
 788 | 
 789 | export
 790 | Reify BuiltinType where
 791 |   reify defs val@(NDCon _ n _ _ args)
 792 |       = case (dropAllNS !(full (gamma defs) n), args) of
 793 |              (UN (Basic "BuiltinNatural"), [])
 794 |                    => pure BuiltinNatural
 795 |              (UN (Basic "NaturalToInteger"), [])
 796 |                    => pure NaturalToInteger
 797 |              (UN (Basic "IntegerToNatural"), [])
 798 |                    => pure IntegerToNatural
 799 |              _ => cantReify val "BuiltinType"
 800 |   reify defs val = cantReify val "BuiltinType"
 801 | 
 802 | export
 803 | Reflect VirtualIdent where
 804 |   reflect fc defs lhs env Interactive
 805 |       = getCon fc defs (reflectiontt "Interactive")
 806 | 
 807 | export
 808 | Reify OriginDesc where
 809 |   reify defs val@(NDCon _ n _ _ args)
 810 |       = case (dropAllNS !(full (gamma defs) n), args) of
 811 |              (UN (Basic "PhysicalIdrSrc"), [(_, ident)])
 812 |                    => do ident' <- reify defs !(evalClosure defs ident)
 813 |                          pure (PhysicalIdrSrc ident')
 814 |              (UN (Basic "PhysicalPkgSrc"), [(_, fname)])
 815 |                    => do fname' <- reify defs !(evalClosure defs fname)
 816 |                          pure (PhysicalPkgSrc fname')
 817 |              (UN (Basic "Virtual"), [(_, ident)])
 818 |                    => do ident' <- reify defs !(evalClosure defs ident)
 819 |                          pure (Virtual ident')
 820 |              _ => cantReify val "OriginDesc"
 821 |   reify defs val = cantReify val "OriginDesc"
 822 | 
 823 | export
 824 | Reflect OriginDesc where
 825 |   reflect fc defs lhs env (PhysicalIdrSrc ident)
 826 |       = do ident' <- reflect fc defs lhs env ident
 827 |            appCon fc defs (reflectiontt "PhysicalIdrSrc") [ident']
 828 |   reflect fc defs lhs env (PhysicalPkgSrc fname)
 829 |       = do fname' <- reflect fc defs lhs env fname
 830 |            appCon fc defs (reflectiontt "PhysicalPkgSrc") [fname']
 831 |   reflect fc defs lhs env (Virtual ident)
 832 |       = do ident' <- reflect fc defs lhs env ident
 833 |            appCon fc defs (reflectiontt "Virtual") [ident']
 834 | 
 835 | export
 836 | Reify FC where
 837 |   reify defs val@(NDCon _ n _ _ args)
 838 |       = case (dropAllNS !(full (gamma defs) n), args) of
 839 |              (UN (Basic "MkFC"), [(_, fn), (_, start), (_, end)])
 840 |                    => do fn' <- reify defs !(evalClosure defs fn)
 841 |                          start' <- reify defs !(evalClosure defs start)
 842 |                          end' <- reify defs !(evalClosure defs end)
 843 |                          pure (MkFC fn' start' end')
 844 |              (UN (Basic "EmptyFC"), _) => pure EmptyFC
 845 |              _ => cantReify val "FC"
 846 |   reify defs val = cantReify val "FC"
 847 | 
 848 | export
 849 | Reflect FC where
 850 |   reflect fc defs True env _ = pure $ Erased fc Placeholder
 851 |   reflect fc defs lhs env (MkFC fn start end)
 852 |       = do fn' <- reflect fc defs lhs env fn
 853 |            start' <- reflect fc defs lhs env start
 854 |            end' <- reflect fc defs lhs env end
 855 |            appCon fc defs (reflectiontt "MkFC") [fn', start', end']
 856 |   reflect fc defs lhs env (MkVirtualFC fn start end)
 857 |       = do fn' <- reflect fc defs lhs env fn
 858 |            start' <- reflect fc defs lhs env start
 859 |            end' <- reflect fc defs lhs env end
 860 |            appCon fc defs (reflectiontt "MkFC") [fn', start', end']
 861 |   reflect fc defs lhs env EmptyFC = getCon fc defs (reflectiontt "EmptyFC")
 862 | 
 863 | export
 864 | Reify a => Reify (WithFC a) where
 865 |   reify defs val@(NDCon _ n _ _ args)
 866 |       = case (dropAllNS !(full (gamma defs) n), map snd args) of
 867 |              (UN (Basic "MkFCVal"), [fcterm, nestedVal]) => do
 868 |                  fc <- reify defs !(evalClosure defs fcterm)
 869 |                  val <- reify defs !(evalClosure defs nestedVal)
 870 |                  pure $ MkFCVal fc val
 871 |              (UN (Basic "MkFCVal"), [_, fc, l2]) => do
 872 |                  fc' <- reify defs !(evalClosure defs fc)
 873 |                  val' <- reify defs !(evalClosure defs l2)
 874 |                  pure $ MkFCVal fc' val'
 875 |              (t, l) => cantReify val "WithFC constructor: \{show t}, args: \{show (length l)}"
 876 |   reify defs val = cantReify val "Expected WithFC, found something else"
 877 | 
 878 | export
 879 | Reflect a => Reflect (WithFC a) where
 880 |   reflect fc defs lhs env value
 881 |       = do loc' <- reflect fc defs lhs env value.fc
 882 |            val' <- reflect fc defs lhs env value.val
 883 |            appCon fc defs (reflectiontt "MkFCVal") [Erased fc Placeholder, loc', val']
 884 | 
 885 | {-
 886 | -- Reflection of well typed terms: We don't reify terms because that involves
 887 | -- type checking, but we can reflect them
 888 | 
 889 | -- TODO: Do we need this? Fix reify if we do.
 890 | 
 891 | export
 892 | Reflect (IsVar name idx vs) where
 893 |   reflect fc defs lhs env First
 894 |       = appCon fc defs (reflectiontt "First") [Erased fc Placeholder, Erased fc Placeholder]
 895 |   reflect fc defs lhs env (Later p)
 896 |       = do p' <- reflect fc defs lhs env p
 897 |            appCon fc defs (reflectiontt "Later")
 898 |                   [Erased fc Placeholder, Erased fc Placeholder,
 899 |                    Erased fc Placeholder, Erased fc Placeholder, p']
 900 | 
 901 | -- Assume terms are normalised so there's not Let bindings in particular
 902 | export
 903 | Reflect (Term vs) where
 904 |   reflect fc defs lhs env (Local {name} lfc _ idx prf)
 905 |       = do lfc' <- reflect fc defs lhs env lfc
 906 |            idx' <- reflect fc defs lhs env idx
 907 |            appCon fc defs (reflectiontt "Local")
 908 |                   [Erased fc Placeholder, Erased fc Placeholder, lfc', idx', Erased fc Placeholder]
 909 |   reflect fc defs lhs env (Ref rfc nt n)
 910 |       = do rfc' <- reflect fc defs lhs env rfc
 911 |            nt' <- reflect fc defs lhs env nt
 912 |            n' <- reflect fc defs lhs env n
 913 |            appCon fc defs (reflectiontt "Ref")
 914 |                   [Erased fc Placeholder, rfc', nt', n']
 915 |   reflect fc defs lhs env (Bind bfc x (Pi c p ty) sc)
 916 |       = do bfc' <- reflect fc defs lhs env bfc
 917 |            x' <- reflect fc defs lhs env x
 918 |            c' <- reflect fc defs lhs env c
 919 |            p' <- reflect fc defs lhs env p
 920 |            ty' <- reflect fc defs lhs env ty
 921 |            sc' <- reflect fc defs lhs env sc
 922 |            appCon fc defs (reflectiontt "Pi")
 923 |                   [Erased fc Placeholder, bfc', c', p', x', ty', sc']
 924 |   reflect fc defs lhs env (Bind bfc x (Lam c p ty) sc)
 925 |       = do bfc' <- reflect fc defs lhs env bfc
 926 |            x' <- reflect fc defs lhs env x
 927 |            c' <- reflect fc defs lhs env c
 928 |            p' <- reflect fc defs lhs env p
 929 |            ty' <- reflect fc defs lhs env ty
 930 |            sc' <- reflect fc defs lhs env sc
 931 |            appCon fc defs (reflectiontt "Lam")
 932 |                   [Erased fc Placeholder, bfc', c', p', x', ty', sc']
 933 |   reflect fc defs lhs env (App afc fn arg)
 934 |       = do afc' <- reflect fc defs lhs env afc
 935 |            fn' <- reflect fc defs lhs env fn
 936 |            arg' <- reflect fc defs lhs env arg
 937 |            appCon fc defs (reflectiontt "App")
 938 |                   [Erased fc Placeholder, afc', fn', arg']
 939 |   reflect fc defs lhs env (TDelayed dfc r tm)
 940 |       = do dfc' <- reflect fc defs lhs env dfc
 941 |            r' <- reflect fc defs lhs env r
 942 |            tm' <- reflect fc defs lhs env tm
 943 |            appCon fc defs (reflectiontt "TDelayed")
 944 |                   [Erased fc Placeholder, dfc', r', tm']
 945 |   reflect fc defs lhs env (TDelay dfc r ty tm)
 946 |       = do dfc' <- reflect fc defs lhs env dfc
 947 |            r' <- reflect fc defs lhs env r
 948 |            ty' <- reflect fc defs lhs env ty
 949 |            tm' <- reflect fc defs lhs env tm
 950 |            appCon fc defs (reflectiontt "TDelay")
 951 |                   [Erased fc Placeholder, dfc', r', ty', tm']
 952 |   reflect fc defs lhs env (TForce dfc r tm)
 953 |       = do dfc' <- reflect fc defs lhs env dfc
 954 |            r' <- reflect fc defs lhs env r
 955 |            tm' <- reflect fc defs lhs env tm
 956 |            appCon fc defs (reflectiontt "TForce")
 957 |                   [Erased fc Placeholder, r', dfc', tm']
 958 |   reflect fc defs lhs env (PrimVal pfc c)
 959 |       = do pfc' <- reflect fc defs lhs env pfc
 960 |            c' <- reflect fc defs lhs env c
 961 |            appCon fc defs (reflectiontt "PrimVal")
 962 |                   [Erased fc Placeholder, pfc', c']
 963 |   reflect fc defs lhs env (Erased efc _)
 964 |       = do efc' <- reflect fc defs lhs env efc
 965 |            appCon fc defs (reflectiontt "Erased")
 966 |                   [Erased fc Placeholder, efc']
 967 |   reflect fc defs lhs env (TType tfc)
 968 |       = do tfc' <- reflect fc defs lhs env tfc
 969 |            appCon fc defs (reflectiontt "TType")
 970 |                   [Erased fc Placeholder, tfc']
 971 |   reflect fc defs lhs env val = cantReflect fc "Term"
 972 |   -}
 973 |