0 | module Deriving.DepTyCheck.Util.Primitives
 1 |
 2 | import public Language.Reflection.Compat
 3 |
 4 | %default total
 5 |
 6 | ---------------------------------------------------
 7 | --- Working around primitive and special values ---
 8 | ---------------------------------------------------
 9 |
10 | primTypeInfo : String -> TypeInfo
11 | primTypeInfo s = MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic s) [] []
12 |
13 | export
14 | typeInfoForPrimType : PrimType -> TypeInfo
15 | typeInfoForPrimType IntType     = primTypeInfo "Int"
16 | typeInfoForPrimType IntegerType = primTypeInfo "Integer"
17 | typeInfoForPrimType Int8Type    = primTypeInfo "Int8"
18 | typeInfoForPrimType Int16Type   = primTypeInfo "Int16"
19 | typeInfoForPrimType Int32Type   = primTypeInfo "Int32"
20 | typeInfoForPrimType Int64Type   = primTypeInfo "Int64"
21 | typeInfoForPrimType Bits8Type   = primTypeInfo "Bits8"
22 | typeInfoForPrimType Bits16Type  = primTypeInfo "Bits16"
23 | typeInfoForPrimType Bits32Type  = primTypeInfo "Bits32"
24 | typeInfoForPrimType Bits64Type  = primTypeInfo "Bits64"
25 | typeInfoForPrimType StringType  = primTypeInfo "String"
26 | typeInfoForPrimType CharType    = primTypeInfo "Char"
27 | typeInfoForPrimType DoubleType  = primTypeInfo "Double"
28 | typeInfoForPrimType WorldType   = primTypeInfo "%World"
29 |
30 | export
31 | typeInfoForTypeOfTypes : TypeInfo
32 | typeInfoForTypeOfTypes = primTypeInfo "Type"
33 |
34 | export
35 | extractTargetTyExpr : TypeInfo -> TTImp
36 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Int"    ) [] [] = primVal $ PrT IntType
37 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Integer") [] [] = primVal $ PrT IntegerType
38 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Int8"   ) [] [] = primVal $ PrT Int8Type
39 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Int16"  ) [] [] = primVal $ PrT Int16Type
40 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Int32"  ) [] [] = primVal $ PrT Int32Type
41 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Int64"  ) [] [] = primVal $ PrT Int64Type
42 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Bits8"  ) [] [] = primVal $ PrT Bits8Type
43 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Bits16" ) [] [] = primVal $ PrT Bits16Type
44 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Bits32" ) [] [] = primVal $ PrT Bits32Type
45 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Bits64" ) [] [] = primVal $ PrT Bits64Type
46 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "String" ) [] [] = primVal $ PrT StringType
47 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Char"   ) [] [] = primVal $ PrT CharType
48 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Double" ) [] [] = primVal $ PrT DoubleType
49 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "%World" ) [] [] = primVal $ PrT WorldType
50 | extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Type"   ) [] [] = type
51 | extractTargetTyExpr ti = var ti.name
52 |
53 | export
54 | isTypeInfoPrim : TypeInfo -> Bool
55 | isTypeInfoPrim $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic s) [] [] = True
56 | isTypeInfoPrim _ = False
57 | --isTypeInfoPrim = not . isVar . extractTragetTyExpr
58 |
59 | 0 isTypeInfoPrim_correct : (s : String) -> isTypeInfoPrim (primTypeInfo s) = True
60 | isTypeInfoPrim_correct s = Refl
61 |