
  0 | module TTImp.Elab.Prim
  1 | 
  2 | import Core.TT
  3 | 
  4 | %default total
  5 | 
  6 | export
  7 | checkPrim : FC -> Constant -> (Term vars, Term vars)
  8 | checkPrim fc (I i)    = (PrimVal fc (I i),    PrimVal fc $ PrT IntType)
  9 | checkPrim fc (I8 i)   = (PrimVal fc (I8 i),   PrimVal fc $ PrT Int8Type)
 10 | checkPrim fc (I16 i)  = (PrimVal fc (I16 i),  PrimVal fc $ PrT Int16Type)
 11 | checkPrim fc (I32 i)  = (PrimVal fc (I32 i),  PrimVal fc $ PrT Int32Type)
 12 | checkPrim fc (I64 i)  = (PrimVal fc (I64 i),  PrimVal fc $ PrT Int64Type)
 13 | checkPrim fc (BI i)   = (PrimVal fc (BI i),   PrimVal fc $ PrT IntegerType)
 14 | checkPrim fc (B8 i)   = (PrimVal fc (B8 i),   PrimVal fc $ PrT Bits8Type)
 15 | checkPrim fc (B16 i)  = (PrimVal fc (B16 i),  PrimVal fc $ PrT Bits16Type)
 16 | checkPrim fc (B32 i)  = (PrimVal fc (B32 i),  PrimVal fc $ PrT Bits32Type)
 17 | checkPrim fc (B64 i)  = (PrimVal fc (B64 i),  PrimVal fc $ PrT Bits64Type)
 18 | checkPrim fc (Str s)  = (PrimVal fc (Str s),  PrimVal fc $ PrT StringType)
 19 | checkPrim fc (Ch c)   = (PrimVal fc (Ch c),   PrimVal fc $ PrT CharType)
 20 | checkPrim fc (Db d)   = (PrimVal fc (Db d),   PrimVal fc $ PrT DoubleType)
 21 | checkPrim fc (PrT t)  = (PrimVal fc (PrT t),  TType fc (MN "top" 0))
 22 | checkPrim fc WorldVal = (PrimVal fc WorldVal, PrimVal fc $ PrT WorldType)
 23 |